ICSE Experiments

SMT queries used in Section V-A

We executed the experiments in Section V-A using the following:

NOTE: The queries in queries and queries_splitted are exactly the same, but in the former each query resides in a single file.

We collected the queries using QSYM by dumping the branch conditions of each benchmark when executed on a seed input (see Table below). In particular, we dumped the path constraints when the execution reached the Solver::negatePath function. We also deactivated the query simplification in the Solver::add function.

This table summarizes the benchmarks:

Benchmark Seed Num. of Queries
advmng mappy.mng 1481
advzip small_archive.zip 300
bloaty small_exec.elf 2085
bsdtar tar.tar 325
djpeg not_kitty.jpg 1245
jhead not_kitty.jpg 405
libpng not_kitty.png 1673
lodepng not_kitty.png 1531
objdump small_exec.elf 992
optipng not_kitty.png 1740
readelf small_exec.elf 1055
tcpdump small_capture.pcap 409
tiff2pdf not_kitty.tiff 3084

Fuzzy-SAT vs Z3 experiment

The run_batch_fuzzy_z3.sh script can be used to run both z3 and fuzzy-solver on the queries.

To use the script, download the queries and the seeds, extract them, set accordingly QUERIES_PATH, SEED_PATH and OUTPUT_DIR in the script, and run it. It will create two CSV files for for each benchmark. The script parse_info_query_splitted.py can be used to parse these CSV files and print a table about the number of queries proved sat by Fuzzy-SAT and Z3, and the elapsed time.

Fuzzy-SAT vs JFS experiment

This experiment can be executed similarly to the previous one, but you need to:

Configurations for benchmarks in Section V-C

Benchmark Release Args Seed Dictionary Driver
advmng advancecomp-2.0 -l @@ mappy.mng
advzip advancecomp-2.0 -l @@ small_archive.zip
bloaty 1.0 git 7c6fc @@ small_exec.elf
bsdtar libarchive git f3b1f9 tf @@ tar.tar
djpeg v9d @@ not_kitty.jpg jpeg.dict
jhead 3.00-5 @@ not_kitty.jpg
libpng 1.6.37 @@ /dev/null not_kitty.png png.dict driver.c
lodepng 20200112 @@ not_kitty.png png.dict
objdump binutils-2.34 -d @@ small_exec.elf
optipng 0.7.6 -out /dev/null @@ not_kitty.png
readelf binutils-2.34 -a @@ small_exec.elf
tcpdump 4.9.3 (pcap 1.9.1) -e -vv -nr @@ small_capture.pcap
tiff2pdf 4.1.0 @@ not_kitty.tiff tiff.dict

NOTE #1: CRC checks were disabled in lodepng.
NOTE #2: When a benchmark is a library, we compiled it as a static library.