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 input.smt2 and a command solver --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).

  • --memout to impose a memory limit (in MB), otherwise memory usage is not limited.

  • --timeout to impose a custom time limit (in seconds), otherwise the time limit is computed based on the run time of the initial run.

  • --strategy to select the minimization strategy (see Minimization Strategies).

  • --ignore-output to ignore output on standard output and error channels.

  • --match-out and --match-err to 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:

$ ../bin/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 use it.
[ddSMT WARNING] automatically disabling fp mutators. Use --fp to use it.
[ddSMT WARNING] automatically disabling strings mutators. Use --strings to use it.
[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

[ddSMT INFO] golden runtime: 0.00 seconds
...

Now, let’s assume we want to ignore output on stdout and stderr, we enable option –ignore-output:

$ ../bin/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 code:-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:

$ ../bin/ddsmt -v --match-out things example/input.smt2 example/output.smt2 example/solver --option

$ ../bin/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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
def matches_golden(golden, run, ignore_out, match_out, match_err):
    """Checks whether the ``run`` result matches the golden run, considering
    ``ignore_out``, ``match_out`` and ``match_err``.

    If ``ignore_out`` is true, only the exit code is compared.
    Otherwise, if either ``match_out`` or ``match_err`` are given, they
    need to match. Otherwise, both stdout and stderr must be the same.
    """
    if run.exit != golden.exit:
        return False

    if not ignore_out:
        if match_out or match_err:
            # we have --match-out or --match-err
            if match_out:
                if match_out not in run.out:
                    return False
            if match_err:
                if match_err not in run.err:
                    return False
        else:
            if golden.out != run.out:
                return False
            if golden.err != run.err:
                return False

    return True

Full Option Listing

$ ../bin/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: 0)
  --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)
  --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

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-]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