docker load --input experiment7.tar.gzdocker load --input experiment7pending.tar.gzdocker run --rm -it experiment7 bash or docker run --rm -it experiment7pending bash to perform experiments with either vanilla or pending KLEE respectively.The docker images are identical, except with the version of KLEE they have in PATH.
The docker image loads you into /benchmarks directory where all the bitcode for the benchmarks is located.
The docker image is organised as follows:
/benchmarks contains the bitcode for all (and more) benchmarks used in the paper
/benchmarks/{seeds/seeds2} contain the seeds from seed sets 1 and 2 respectively
/src/klee contains the source code of KLEE
/src/klee_build is the build directory of KLEE. Typing make install here, will update the klee in PATH with any changes in /src/klee
/src/{bc-1.07,make-4.2,...} have some benchmarks compiled with GCov instrumentation.
/vorbis, /magick, /tcpdump have those benchmarks compiled with GCov instrumentation
We ran our experiments on an internal docker cluster which is infeasible to
share. Therefore we provide below the exact commands we used. They should be run
in a fresh docker instance (ie. run docker run --rm -it experiment7 bash for
each command). The commands are identical for pending KLEE and vanilla KLEE, so
they should be ran twice in their respective docker images (experiment7 and
experiment7pending).
To make validating our data easier we provide a spreadsheet from which we
generated the graphs. After a command terminates the data can be obtained from
inside the docker image with klee-stats (klee-stats /tmp/klee-out) or
directly with sqlite3 (apt install sqlite3 && sqlite3 /tmp/klee-out/run.stats "SELECT CoveredInstructions FROM stats ORDER BY rowid DESC LIMIT 1")
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out bc.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out bc.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out bc.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out datamash.bc --sym-arg 3 --sym-arg 1 --sym-arg 4 --sym-arg 1 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out datamash.bc --sym-arg 3 --sym-arg 1 --sym-arg 4 --sym-arg 1 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out datamash.bc --sym-arg 3 --sym-arg 1 --sym-arg 4 --sym-arg 1 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out m4.bc -G -H37 --sym-arg 2 --sym-arg 5 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out m4.bc -G -H37 --sym-arg 2 --sym-arg 5 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out m4.bc -G -H37 --sym-arg 2 --sym-arg 5 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc jpeg:fd:0 png:fd:1 --sym-stdin 285
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc jpeg:fd:0 png:fd:1 --sym-stdin 285
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc jpeg:fd:0 png:fd:1 --sym-stdin 285
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc png:fd:0 jpg:fd:1 --sym-stdin 70
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc png:fd:0 jpg:fd:1 --sym-stdin 70
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc png:fd:0 jpg:fd:1 --sym-stdin 70
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out make.bc -n -f A --sym-arg 2 --sym-arg 5 --sym-files 1 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out make.bc -n -f A --sym-arg 2 --sym-arg 5 --sym-files 1 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out make.bc -n -f A --sym-arg 2 --sym-arg 5 --sym-files 1 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out oggenc.bc A --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out oggenc.bc A --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out oggenc.bc A --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out tcpdump.bc -r A -K -n --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out tcpdump.bc -r A -K -n --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out tcpdump.bc -r A -K -n --sym-files 1 100
The data from these runs was also used for Figures 2 and 5.
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds2/bc.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out bc.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds/bc.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out bc.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds2/bc.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out bc.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds/bc.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out bc.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds2/bc.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out bc.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/bc.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out bc.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds2/datamash.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out datamash.bc --sym-arg 3 --sym-arg 1 --sym-arg 4 --sym-arg 1 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds/datamash.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out datamash.bc --sym-arg 3 --sym-arg 1 --sym-arg 4 --sym-arg 1 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds2/datamash.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out datamash.bc --sym-arg 3 --sym-arg 1 --sym-arg 4 --sym-arg 1 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds/datamash.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out datamash.bc --sym-arg 3 --sym-arg 1 --sym-arg 4 --sym-arg 1 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds2/datamash.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out datamash.bc --sym-arg 3 --sym-arg 1 --sym-arg 4 --sym-arg 1 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/datamash.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out datamash.bc --sym-arg 3 --sym-arg 1 --sym-arg 4 --sym-arg 1 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds2/m4.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out m4.bc -G -H37 --sym-arg 2 --sym-arg 5 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds/m4.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out m4.bc -G -H37 --sym-arg 2 --sym-arg 5 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds2/m4.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out m4.bc -G -H37 --sym-arg 2 --sym-arg 5 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds/m4.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out m4.bc -G -H37 --sym-arg 2 --sym-arg 5 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds2/m4.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out m4.bc -G -H37 --sym-arg 2 --sym-arg 5 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/m4.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out m4.bc -G -H37 --sym-arg 2 --sym-arg 5 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds2/magick_jpg.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc jpeg:fd:0 png:fd:1 --sym-stdin 285
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds/magick_jpg.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc jpeg:fd:0 png:fd:1 --sym-stdin 285
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds2/magick_jpg.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc jpeg:fd:0 png:fd:1 --sym-stdin 285
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds/magick_jpg.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc jpeg:fd:0 png:fd:1 --sym-stdin 285
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds2/magick_jpg.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc jpeg:fd:0 png:fd:1 --sym-stdin 285
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/magick_jpg.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc jpeg:fd:0 png:fd:1 --sym-stdin 285
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds2/magick_png.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc png:fd:0 jpg:fd:1 --sym-stdin 70
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds/magick_png.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc png:fd:0 jpg:fd:1 --sym-stdin 70
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds2/magick_png.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc png:fd:0 jpg:fd:1 --sym-stdin 70
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds/magick_png.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc png:fd:0 jpg:fd:1 --sym-stdin 70
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds2/magick_png.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc png:fd:0 jpg:fd:1 --sym-stdin 70
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/magick_png.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc png:fd:0 jpg:fd:1 --sym-stdin 70
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds2/make.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out make.bc -n -f A --sym-arg 2 --sym-arg 5 --sym-files 1 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds/make.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out make.bc -n -f A --sym-arg 2 --sym-arg 5 --sym-files 1 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds2/make.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out make.bc -n -f A --sym-arg 2 --sym-arg 5 --sym-files 1 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds/make.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out make.bc -n -f A --sym-arg 2 --sym-arg 5 --sym-files 1 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds2/make.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out make.bc -n -f A --sym-arg 2 --sym-arg 5 --sym-files 1 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/make.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out make.bc -n -f A --sym-arg 2 --sym-arg 5 --sym-files 1 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds2/oggenc.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out oggenc.bc A --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds/oggenc.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out oggenc.bc A --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds2/oggenc.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out oggenc.bc A --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds/oggenc.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out oggenc.bc A --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds2/oggenc.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out oggenc.bc A --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/oggenc.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out oggenc.bc A --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds2/sqlite3.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds/sqlite3.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds2/sqlite3.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds/sqlite3.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds2/sqlite3.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/sqlite3.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds2/tcpdump.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out tcpdump.bc -r A -K -n --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=dfs --max-memory=4000 -seed-file=seeds/tcpdump.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out tcpdump.bc -r A -K -n --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds2/tcpdump.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out tcpdump.bc -r A -K -n --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=nurs:depth --max-memory=4000 -seed-file=seeds/tcpdump.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out tcpdump.bc -r A -K -n --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds2/tcpdump.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out tcpdump.bc -r A -K -n --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/tcpdump.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out tcpdump.bc -r A -K -n --sym-files 1 100
Note that the runs with the two seeds need to be merged using the
/src/klee/scripts/IStatsMerge.py script. The total covered lines can then be
obtained with /src/klee/scripts/IStatsSum.py script.
To get the relaxed pending bars from Figure 7. The vanilla and pending bars are obtained from the commands above.
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --pending-checks --pending-bounds --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/bc.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out bc.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --pending-checks --pending-bounds --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/datamash.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out datamash.bc --sym-arg 3 --sym-arg 1 --sym-arg 4 --sym-arg 1 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --pending-checks --pending-bounds --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/m4.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out m4.bc -G -H37 --sym-arg 2 --sym-arg 5 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --pending-checks --pending-bounds --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/magick_jpg.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc jpeg:fd:0 png:fd:1 --sym-stdin 285
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --pending-checks --pending-bounds --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/magick_png.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc png:fd:0 jpg:fd:1 --sym-stdin 70
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --pending-checks --pending-bounds --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/make.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out make.bc -n -f A --sym-arg 2 --sym-arg 5 --sym-files 1 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --pending-checks --pending-bounds --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/oggenc.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out oggenc.bc A --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --pending-checks --pending-bounds --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/sqlite3.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --pending-checks --pending-bounds --max-time=7200 --search=random-path --max-memory=4000 -seed-file=seeds/tcpdump.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out tcpdump.bc -r A -K -n --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=86400 --search=nurs:depth --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=86400 --pending-checks --pending-bounds --search=nurs:depth --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=86400 --search=nurs:depth --max-memory=4000 -seed-file=seeds/sqlite3.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --pending-checks --pending-bounds --max-time=864000 --search=nurs:depth --max-memory=4000 -seed-file=seeds/sqlite3.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=86400 --search=random-path --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=86400 --search=random-path --max-memory=4000 -seed-file=seeds/sqlite3.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --pending-checks --pending-bounds --max-time=86400 --search=random-path --max-memory=4000 -seed-file=seeds/sqlite3.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=86400 --search=dfs --max-memory=4000 -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=86400 --search=dfs --max-memory=4000 -seed-file=seeds/sqlite3.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --pending-checks --pending-bounds --max-time=86400 --search=dfs --max-memory=4000 -seed-file=seeds/sqlite3.ktest -random-RNG -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20"
A time series can then be obtained by running sqlite3 in the container:
sqlite3 /tmp/klee-out "SELECT (WallTime / (1000000 * 3600)), CoveredInstructions, MallocUsage FROM stats ORDER BY WallTime"
The heatmap is just the pairwise combination of nonseeded and seeded runs from
above obtained by running the /src/klee/scripts/IStatsMerge.py and /src/klee/scripts/IStatsSum.py scripts.
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee -fault-pct=1.0 --max-time=7200 --search=random-path -inject-fault --max-memory=4000 -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out bc.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee -fault-pct=1.0 --max-time=7200 --search=random-path -inject-fault --max-memory=4000 -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out datamash.bc --sym-arg 3 --sym-arg 1 --sym-arg 4 --sym-arg 1 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee -fault-pct=1.0 --max-time=7200 --search=random-path -inject-fault --max-memory=4000 -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out m4.bc -G -H37 --sym-arg 2 --sym-arg 5 --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee -fault-pct=1.0 --max-time=7200 --search=random-path -inject-fault --max-memory=4000 -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc jpeg:fd:0 png:fd:1 --sym-stdin 285
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee -fault-pct=1.0 --max-time=7200 --search=random-path -inject-fault --max-memory=4000 -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out magick.bc png:fd:0 jpg:fd:1 --sym-stdin 70
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee -fault-pct=1.0 --max-time=7200 --search=random-path -inject-fault --max-memory=4000 -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out make.bc -n -f A --sym-arg 2 --sym-arg 5 --sym-files 1 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee -fault-pct=1.0 --max-time=7200 --search=random-path -inject-fault --max-memory=4000 -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out oggenc.bc A --sym-files 1 100
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee -fault-pct=1.0 --max-time=7200 --search=random-path -inject-fault --max-memory=4000 -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out sqlite3.bc --sym-stdin 20
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee -fault-pct=1.0 --max-time=7200 --search=random-path -inject-fault --max-memory=4000 -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out tcpdump.bc -r A -K -n --sym-files 1 100
The internal coverage and unique faults found can be obtained with sqlite3:
sqlite3 /tmp/klee-out/run.stats "SELECT CoveredInstructions, UniqueDivFault FROM stats ORDER BY rowid DESC LIMIT 1"
Gcov coverage can be obtained by rerunning the ktest files as per Step 7 of
KLEE tutorial. The GCov
coverage can then be obtained by running gcovr (For example after replaying
test cases for make, pip3 install
gcovr && cd /src/make-4.2 && gcovr -r ..
ZESTI experiment requires a slightly different docker image:
docker load --input zesti7experiment.tar.gzdocker run --rm -it zesti7experiment bashThe main difference is the /tmp/zestiSeeds folder, which contains the captured
seeds from the regression test suites. The version of KLEE is the same as in
experiment7pending docker image.
We provide the two commands that found the bugs reported in the paper. The remaining runs are identical except for pointing to different seeds.
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=1800 --search=zesti -seed-file=/tmp/zestiSeeds/tar--c_-b_1_-f0fb82fa3 -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out tar.bc
In our run, the bug was found by /tmp/klee-out/test000119.ktest input.
The fix can be found here.
ulimit -s unlimited && ulimit -n 1000000 && ulimit -c unlimited && klee --max-time=1800 --search=zesti -seed-file=/tmp/zestiSeeds/dwarfdump--b_-H_2_-oi4eb4bd71 -only-output-states-covering-new --simplify-sym-indices --solver-backend=stp --disable-inlining -watchdog --libc=uclibc --posix-runtime --external-calls=all --run-in-dir=/tmp/sandbox --switch-type=simple --output-dir=/tmp/klee-out dwarfdump.bc
In our run the bug was found by /tmp/klee-out/test000186.ktest input.
The bug was acknowledged at https://www.prevanders.net/dwarf.html (28 June 2020 update)
The source code for pending constraints is available on
GitHub or in the enclosed
source_code folder.
Good starting points to look at are:
lib/Core/Searcher.cpp with the PendingSearcher class, which is the meta searcher prioritising states without pending constraints.lib/Solver/CexCachingSolver.cpp is the cache we used for fast feasibility checking. It is also where some seeding is implemented.lib/Core/Executor.cpp::fork delays the constraint checking (keep in mind that TimingSolver is modified to not perform the actual SMT call in evaluate).We provide the ktest files for the 24 hour runs, which are briefly described in sections 4.6.1 and 4.6.2. They are located in 24hour_runs_ktest_files. 24h[search-strategy][other-modifier]_ktests is the folder naming scheme. Where [search-strategy] is either rp for random-path, nd for depth biased and dfs for depth first search strategy. [other-modifier] is either empty, indicating a non-seeded pending constraints run, seed which is a seeded pending constraints run or vanilla which is a non-seeded vanilla KLEE run. Note that vanilla KLEE seeded run is omitted as it produces no seeds, because it does not complete the seed in 24 hours.
Assuming ktest-tool is installed (from a KLEE installation on the system or the docker image), the following command can give a brief overview of the inputs:
ktest-tool 24hdfsseed_ktests/*.ktest | grep "'stdin'" -A3 | grep datawhich prints the inputs generate by KLEE with pending constraints using DFS and the seed in a 24 hour run of sqlite3.
object 0: data: b'SELECT * FROM t;\n \n'
object 0: data: b'SELECT * FROM t;\n \x01\n'
object 0: data: b'SELECT * FROM t;\n \xc1\n'
object 0: data: b'SELECT * FROM t;\n #\n'
object 0: data: b'SELECT * FROM t;\n ?\n'
object 0: data: b'SELECT * FROM t;\n [\n'
object 0: data: b'SELECT * FROM t;\n 0\n'
object 0: data: b'SELECT * FROM t;\n 9\n'
object 0: data: b'SELECT * FROM t;\n "\n'
object 0: data: b'SELECT * FROM t;\n ~\n'
...