To get started install docker on your system, more info for ubuntu users:
https://docs.docker.com/install/linux/docker-ce/ubuntu/
Then download and unzip the artefact and import the provided image with
docker load --input segmented_artefact.tar.gzThis will load segmented_artefact image into your docker, you can run the image with
docker run --rm --ulimit stack=-1 -it segmented_artefact bashWhich 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 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: MergingThe 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.
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 myResultsThe 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.
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.
docker ps to find the name of the container running those experimentsdocker cp #CONTAINER_NAME#:/data/double-deref/doublederef-benchmarks/bin/myResults.tar.gz graphs/graphs/extract.Makefile to TAR_DIR=myResultsmake -C graphs