Quickstart
The main purpose of ddSMT is to minimize an input that triggers some (erroneous) behavior when fed to a given command. ddSMT first executes the command on the given input and records its behavior (exit code, standard output and error channels). After that, it mutates the input while preserving the behavior of the given command until no further mutations are possible.
ddSMT aims at extracting a minimal working example, that is, an input that is as small as possible but still triggers the original faulty behavior of the executed command. Such a command is usually a call to an SMT solver executable with command line options (but can be a call to any tool that expects the SMT-LIB language or an extension/dialect of the language as input).
The initial execution of the given command (the golden run) records its behavior as a combination of
the standard output
the standard error output
the exit code
For any mutations that are accepted, the command must exit with the same behavior. Additionally, ddSMT imposes a time limit for executing the command that is by default computed based on the run time of the golden run. Optionally, ddSMT allows to configure this time limit, and to ignore output channels.
ddSMT implements several minimization strategies to derive inputs by applying all enabled mutators. After the golden run, it generates mutated inputs and executes the given command on these inputs. The first mutated input on which the command behaves the same as on the original input is accepted, and new mutations are tested based on this new input. When no further mutations are possible, ddSMT terminates with the final output written to the specified output file.
Note
ddSMT writes (intermediate) accepted mutations to the specified output file. This allows to already use intermediate minimizations even when ddSMT is not yet done minimizing.
How to run ddSMT
Given an input file example/input.smt2 and a call to
example/solver with command line option --option, ddSMT
is executed to write minimized input to output.smt2 as follows:
$ ddsmt input.smt2 output.smt2 solver --option
ddSMT provides many options that cover common use cases. Consult the full option listing for an exhaustive list. The most commonly used options are:
--jobs(or-j) to set the number of processes allowed to run in parallel (uses the number of CPU cores minus two by default).--memoutto impose a memory limit (in MB), otherwise memory usage is not limited.--timeoutto impose a custom time limit (in seconds), otherwise the time limit is computed based on the run time of the initial run.--strategyto select the minimization strategy (see Minimization Strategies).--ignore-outputto ignore output on standard output and error channels.--match-outand--match-errto define pattern matches against on the standard channels (see How Behavior is Compared with the Golden Run).
How Behavior is Compared with the Golden Run
By default, a run on mutated input is considered equivalent in behavior to the golden run if the exit code, the standard output and the error output are the same as for the golden run.
For example, assume that our example from above produces the following output:
$ example/solver --option example/input.smt2
printing something to stdout
error: this message is printed to stderr
$ echo $? # the exit code
1
By default
ddSMT will exactly match
printing something to stdout against what is printed on stdout and
error: this message is printed to stderr against what is printed on
stderr for mutated inputs, and check if the exit code is 1.
When increasing the verbosity level with -v, it will print some
information about the golden run and progress:
$ ddsmt -v example/input.smt2 example/output.smt2 example/solver --option
[ddSMT INFO] input file: 'example/input.smt2'
[ddSMT INFO] output file: 'example/output.smt2'
[ddSMT INFO] command: 'example/solver --option'
[ddSMT WARNING] automatically disabling arithmetic mutators. Use --arithmetic to enable.
[ddSMT WARNING] automatically disabling datatypes mutators. Use --datatypes to enable.
[ddSMT WARNING] automatically disabling fp mutators. Use --fp to enable.
[ddSMT WARNING] automatically disabling strings mutators. Use --strings to enable.
[ddSMT INFO]
[ddSMT INFO] starting initial run...
[ddSMT INFO]
[ddSMT INFO] golden exit: 1
[ddSMT INFO] golden err:
error: this message is printed to stderr
[ddSMT INFO] golden out:
printing something to stdout
...
Now, let’s assume we want to ignore output on stdout and stderr, we enable
option --ignore-output:
$ ddsmt -v --ignore-output example/input.smt2 example/output.smt2 example/solver --option
Note
With option --ignore-output enabled, ddSMT will still report
output on both channels for the golden run with option -v.
When comparing behavior, however, this output is ignored, and only the
exit code is matched.
Now, let’s assume our command yields output on stdout or stderr that
contains information that depends on the actual execution, e.g., a stack trace.
In this case, matching against the full output will never be successful,
and we rather only want to check if a phrase occurs in the output.
We can achieve this with options --match-out (for stdout) and
--match-err (for stderr) as follows:
$ ddsmt -v --match-out things example/input.smt2 example/output.smt2 example/solver --option
$ ddsmt -v --match-err error example/input.smt2 example/output.smt2 example/solver --option
In case you are wondering how the comparison of a run on mutated input with the golden run is implemented, this is the actual code that is implemented in ddSMT:
1def matches_golden(golden, run, ignore_out, ignore_err, match_out, match_err):
2 """Checks whether the ``run`` result matches the golden run, considering
3 ``ignore_out``, ``ignore_err``, ``match_out`` and ``match_err``.
4
5 If ``ignore_out`` and ``ignore_err`` are true, only the exit code is
6 compared. Else, if ``ignore_out`` is true, only stderr is considered, and
7 if ``ignore_err`` is true, only stdout is considere. If either
8 ``match_out`` or ``match_err`` are given, they need to match. Otherwise,
9 both stdout and stderr must be the same.
10 """
11 if run.exit != golden.exit:
12 return False
13
14 if not ignore_out or not ignore_err:
15 if not ignore_out:
16 if match_out:
17 if match_out not in run.out:
18 return False
19 else:
20 if golden.out != run.out:
21 return False;
22 if not ignore_err:
23 if match_err:
24 if match_err not in run.err:
25 return False
26 else:
27 if golden.err != run.err:
28 return False;
29 return True
Full Option Listing
$ ddsmt --help-all
usage: ddsmt [<options>] <infile> <outfile> <cmd> [<cmd options>]
positional arguments:
infile the input file (in SMT-LIB v2 format)
outfile the output file
cmd the command (with optional arguments)
optional arguments:
-h, --help show this help message and exit
--help-all show all help messages
--version show program's version number and exit
-v increase verbosity (default: 0)
-q decrease verbosity (default: 0)
--dump-config dump configuration
--parser-test only test the parser (default: False)
--pretty-print pretty-print to output file (default:
False)
--wrap-lines wrap lines in output file (default: False)
--strategy {ddmin,hierarchical,hybrid}
minimization strategy (default: hybrid)
--disable-all disable all mutators
checker arguments:
--unchecked assume every change is okay without
checking (default: False)
-j n, --jobs n number of parallel checks (default: 1)
--memout megabytes memout for individual checks
--timeout timeout timeout for test runs in seconds (default:
1.5 * golden runtime)
--ignore-output ignore stdout and stderr, only consider
exit code (default: False)
--ignore-out ignore stdout (default: False)
--ignore-err ignore stderr (default: False)
--match-err str match string in stderr to identify failing
input
--match-out str match string in stdout to identify failing
input
-c cmd-cc, --cross-check cmd-cc cross check command
--timeout-cc timeout timeout for test runs of the cross check in
seconds (default: 1.5 * golden runtime)
--ignore-output-cc ignore stdout and stderr, only consider
exit code for cross check (default: False)
--match-err-cc str match string in stderr to identify failing
input for cross check
--match-out-cc str match string in stdout to identify failing
input for cross check
debug arguments:
--check-loops check for loops in the minimization process
(default: False)
--profile use cProfile for profiling (default: False)
--dump-diffs dump a diff of every simplification
(default: False)
core mutator arguments:
--[no-]core core theory
--[no-]binary-reduction binary reduction
--[no-]constants substitute by a constant
--[no-]erase-node erase node
--[no-]merge-children merge with child
--[no-]substitute-children replace by a child
--[no-]replace-by-variable substitute by existing variable
--[no-]sort-children sort children
--replace-by-variable-mode {inc,dec}
replace with existing variables that are
larger or smaller (default: inc)
arithmetic mutator arguments:
--[no-]arithmetic arithmetic theory
--[no-]arith-negate-relations push negation into arithmetic relation
--[no-]arith-constants simplify arithmetic constant
--[no-]arith-split-nary-relations
split arithmetic n-ary relation
--[no-]arith-strengthen-relations
strengthen arithmetic relation
bv mutator arguments:
--[no-]bv bv theory
--[no-]bv-norm-constants normalize bit-vector const
--[no-]bv-zero-concat replace concat by zero_extend
--[no-]bv-double-negation eliminate double bit-vector negation
--[no-]bv-elim-bvcomp eliminate bvcomp by equality
--[no-]bv-eval-extend evaluate bit-vector extend
--[no-]bv-extract-constants evaluate bit-vector extract on constant
--[no-]bv-extract-zeroextend simplify bit-vector extract on zero_extend
--[no-]bv-merge-reduced-bw merge previous bit-width reductions
--[no-]bv-ite-to-bvcomp eliminate ite with bv1 / bv0 cases
--[no-]bv-reflexive-nand replace bvnand by bvnot
--[no-]bv-simp-constants simplify bit-vector constant
--[no-]bv-to-bool transform bit-vector to boolean
--[no-]bv-zeroextend-pred eliminate zero_extend when both operands of
a predicate are zero extended
--[no-]bv-reduce-bitwidth reduce bit-width of variable
boolean mutator arguments:
--[no-]boolean boolean theory
--[no-]bool-de-morgan push negation inside
--[no-]bool-double-negations eliminate double negation
--[no-]bool-false-eq replace equality with false by negation
--[no-]bool-implications eliminate implication
--[no-]bool-negate-quants push negation inside of quantifier
--[no-]bool-xor-binary eliminate binary xor
--[no-]bool-xor-constants remove constants from xor
datatypes mutator arguments:
--[no-]datatypes datatypes theory
--[no-]dt-rm-constructor remove datatype constructor
--[no-]dt-rm-datatype remove datatype
--[no-]dt-rm-identity remove datatype identity
fp mutator arguments:
--[no-]fp fp theory
--[no-]fp-short-sort replace long FP sort name with short name
smtlib mutator arguments:
--[no-]smtlib smtlib theory
--[no-]check-sat-assuming substitute check-sat-assuming by check-sat
--[no-]eliminate-variables eliminate variable from equality
--[no-]inline-functions inline defined function
--[no-]introduce-fresh-variables
introduce fresh variable
--[no-]let-elimination eliminate let binder
--[no-]let-substitution substitute variable into let body
--[no-]remove-annotation remove annotation
--[no-]remove-recursive-function
remove recursive function
--[no-]simplify-logic simplify logic
--[no-]simplify-quoted-symbols simplify quoted symbol
--[no-]simplify-symbol-names simplify symbol name
strings mutator arguments:
--[no-]strings strings theory
--[no-]seq-nth-unit remove nth of unit seq
--[no-]str-contains-to-concat eliminate str.contains by ++
--[no-]str-index-not-found eliminate str.indexof
--[no-]str-replace-all eliminate str.replace_all
--[no-]str-constants simplify string constant