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:
Download queries splitted.
Pull the JFS docker image (
docker pull delcypher/jfs_build:fse_2019).Use the run_batch_fuzzy_jfs.sh script to run the actual experiment (setting
QUERIES_PATHandSEED_PATH).Parse the results using parse_fuzzy_jfs.py.
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.