To get started install docker on your system, more info for ubuntu users:

Then download and unzip the artefact and import the provided image with

docker load --input segmented_artefact.tar.gz

This will load segmented_artefact image into your docker, you can run the image with

docker run --rm --ulimit stack=-1 -it segmented_artefact bash

Which will run bash in the container. You should end up in the /data/double-deref/doublederef-benchmarks/bin directory, which contains the bitcode files for the programs used in the experiments and a Makefile to run them. You can immediately start running the experiments by invoking different make targets.

Running experiments

Running of experiments is structured through make realprog-exp targets. There are several variables that can be adjusted. KLEE can be used to change the path to a KLEE executable. EXP_DIR is the name of the folder where the experiment will run. TIME can be used to set the timeout in seconds. PROGS selects which benchmark to use. Finally SEARCH can be used to specify klee search strategy.

Therefore running

make realprog-exp -j5 KLEE=klee EXP_DIR=make-bfs TIME=72 PROGS=make  SEARCH=-search=bfs 

Will run klee on make.bc benchmark with BFS search strategy and timeout of 72s. It will create a make-bfs directory containing the 5 klee output directories for each of the 5 memory models proposed in the paper. The output can be inspected by running klee-stats as shown bellow:

$ klee-stats make-bfs/
|   Path    |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
|make-prerun|14075113|    72.66|    22.41|    14.21|   74042|       88.61|
| make-flat | 9202505|    74.15|    22.40|    14.18|   74042|       92.19|
|make-normal| 9160224|    92.90|    22.39|    14.18|   74042|       94.09|
| make-pts  | 8321658|    72.71|    22.36|    14.18|   75367|       91.63|
|  make-sm  | 7861093|    40.15|    22.39|    14.18|   74042|       88.51|
| Total (5) |48620593|   352.57|    22.39|    14.18|  371535|       91.42|

The folder names correspond to the following models as presented in the paper:

  • *-prerun: Segmented (ideal)
  • *-flat: Flat Memory
  • *-normal: Forking
  • *-pts: Segmented (SVF)
  • *-sm: Merging

The data in the table above corresponds to data in Figure 7b albeit with a much smaller timeout. Note that the graphs in the paper show a timeseries of each run, whereas the output of klee-stats just shows the final point. To view the time series you can look at the run.stats (ie. make-bfs/make-pts/run.stats) file.

Figures 6-9

To generate the data for figures 6 to 9 in the paper run the following make commands, which will generate the 12 folders, each corresponding to one of the graphs in those figures.

make realprog-exp KLEE=klee EXP_DIR=make-bfs TIME=7200 PROGS=make  SEARCH=-search=bfs 
make realprog-exp KLEE=klee EXP_DIR=make-dfs TIME=7200 PROGS=make  SEARCH=-search=dfs 
make realprog-exp KLEE=klee EXP_DIR=make-default TIME=7200 PROGS=make  SEARCH= 
make realprog-exp KLEE=klee EXP_DIR=m4-bfs TIME=7200 PROGS=m4  SEARCH=-search=bfs 
make realprog-exp KLEE=klee EXP_DIR=m4-default TIME=7200 PROGS=m4  SEARCH= 
make realprog-exp KLEE=klee EXP_DIR=m4-dfs TIME=7200 PROGS=m4  SEARCH=-search=dfs 
make realprog-exp KLEE=klee KFLAGS="-only-output-states-covering-new -allow-external-sym-calls -libc=uclibc " EXP_DIR=apr-default TIME=7200  PROGS=int_apr_hashtable_x2  SEARCH= 
make realprog-exp KLEE=klee KFLAGS="-only-output-states-covering-new -allow-external-sym-calls -libc=uclibc -search=bfs" EXP_DIR=apr-bfs TIME=7200  PROGS=int_apr_hashtable_x2  SEARCH=-search=bfs 
make realprog-exp KLEE=klee KFLAGS="-only-output-states-covering-new -allow-external-sym-calls -libc=uclibc -search=dfs" EXP_DIR=apr-dfs TIME=7200  PROGS=int_apr_hashtable_x2  SEARCH=-search=dfs 
make realprog-exp KFLAGS="-only-output-states-covering-new -allow-external-sym-calls -libc=uclibc " KLEE=klee EXP_DIR=sql-default TIME=7200  PROGS=trigger_hashtable  SEARCH= 
make realprog-exp KFLAGS="-only-output-states-covering-new -allow-external-sym-calls -libc=uclibc -search=bfs" KLEE=klee EXP_DIR=sql-bfs TIME=7200  PROGS=trigger_hashtable  SEARCH=-search=bfs 
make realprog-exp KFLAGS="-only-output-states-covering-new -allow-external-sym-calls -libc=uclibc -search=dfs" KLEE=klee EXP_DIR=sql-dfs TIME=7200  PROGS=trigger_hashtable  SEARCH=-search=dfs 

If you would like to plot the later create a tarball by:

mkdir myResults
mv {make,m4,arp,sql}-{bfs,dfs,default}  myResults
tar -cvf myResults.tar.gz myResults

Changing source

The source code for klee can be found in the /src/klee/ in the docker image. If modfied it can be compiled and installed in the docker image by running make -C /data/klee_build install. The code is also available on Github.

KLEE webpage and KLEE github are great resources for getting started with KLEE development.

Comparing with the data in the paper

Note these section is not in the Docker image and assumes you are in the artefact root directory

Since running the experiments above is computationally intensive we provide the klee output directories we used to generate the graphs in the paper. They can be found in the graphs/f94de9d.tar.gz archive.

We provide a nice way of plotting them by running make -C graphs This will create the graphs shown in Figures 6-9 in the paper. For example in graphs/m4_bfs/m4-Mem.pdf. This requires gnuplot and python and is known to work on ubuntu installs.

Running make -C graphs clean will remove all the graphs. Note that you can use the same infrastructure to plot the results of running the experiments in the Docker image.

Plotting your docker runs

  1. Use docker ps to find the name of the container running those experiments
  2. docker cp #CONTAINER_NAME#:/data/double-deref/doublederef-benchmarks/bin/myResults.tar.gz graphs/
  3. Change first line of graphs/extract.Makefile to TAR_DIR=myResults
  4. make -C graphs