These instructions detail how to obtain the benchmarks used to evaluate Symbooglix and the tools used in evaluation. Symbooglix is open source an is available on GitHub.
WARNING: The sbb repo is very large. It takes roughly 13 GiB of space.
sbb repository corresponds to the GPU benchmarks
and SV-COMP benchmarks discussed in the paper respectively.
git clone https://github.com/symbooglix/gpu.git git clone --branch icst16 https://github.com/symbooglix/sbb.git
Each repo contains a
program_list.txt which can be given to
boogie-batch-runner.py which will be used later.
We provide Docker images for each tool including Symbooglix which can be pulled from the DockerHub. Note that Duality is built on top of Corral, hence there is only a Corral image.
In order to run the tools via Docker you will need to install it if you haven't already. We used Docker 1.6.2, you can try older versions but things may not work correctly. Docker runs natively on Linux and can be indirectly run on Windows or OSX via the Boot2Docker project.
If you prefer to build the images from scratch run
The images can be found on our Docker organisation page. Run the following commands to pull down the Docker images
docker pull symbooglix/boogaloo:icst16 docker pull symbooglix/boogie:icst16 docker pull symbooglix/corral:icst16 docker pull symbooglix/gpuverify:icst16 docker pull symbooglix/symbooglix:icst16
Each image runs as the
icst user by default. This user has sudo access
so you can install additional packages. The password is
Each docker image has the boogie-runner framework installed which can
be invoked via the
commands. Each docker image also has the boogie-runner config files (
in the home directory. These instruct the boogie-runner framework how to run a tool. There
may be multiple configuration files. For example the corral image has
corral-64-gpu.yml- Corral with a bound of 64 to run on the GPU benchmarks
corral-nb-gpu.yml- Corral with a large bound to run on the GPU benchmarks
corral-8-svcomp.yml- Corral with a bound 8 to run the SV-COMP benchmarks
corral-nb-svcomp.yml- Corral with a large bound to run on the SV-COMP benchmarks
duality-svcomp.yml- Duality to run on the SV-COMP benchmarks
To run a tool you need to create a docker container and mount the benchmarks inside it as a volume. For example to create a Docker container for Corral/Duality and get shell access run:
docker run --rm -ti -v /path/to/benchmark/directory:/mnt symbooglix/corral:icst16
/path/to/benchmark/directoryshould be the path to the directory containing one of the benchmark suites you downloaded earlier.
-vflag is creating a volume inside the container. In the above example the benchmark directory is mounted inside the container at
--rmflag means that the container and any changes you make in the container will be deleted when you leave the container. Remove this flag if you want to keep the container.
symbooglix/corral:icst16is the name of the image replace this with the image you wish to use
Once you have shell access inside the container you can then run the tool inside container.
The tools are on the
PATH inside the container so you
can invoke them directly if you wish. The tool executables are:
boogie-runner.py tool allows a single benchmark to be run conveniently. To try it
boogie-runner.py config.yml /path/to/boogie/program.bpl work_dir result.yml
config.ymlis one of the YAML configuration files in the home directory.
/path/to/boogie/program.bplis the path inside the container to the Boogie program you wish the tool to use
work_diris a working directory for the run. It should not already eixst.
result.ymlis the path to write the results to.
boogie-batch-runner.py tool allows multiple benchmarks to be run conveniently.
An example invocation if the Symbooglix image was being used with the GPU benchmarks mounted in
/mnt/ would be:
boogie-batch-runner.py --rprefix /mnt/other/ ~/symbooglix-gpu.yml /mnt/program_list.txt work_dir result.yml
The process is nearly identical to how Symbooglix is run when comparing it against other Boogie tools
(See Boogie tool comparison)
The only difference is that Symbooglix is run on a smaller subset (361 programs) of the SV-COMP benchmarks.
The program list to be be passed to
in the root of the
The first stage is to obtain Docker images for the modified versions of KLEE. There are two versions, one is a 32-bit build of KLEE and one is a 64-bit build of KLEE. The reason for requiring two different versions is that the benchmarks are a mix of 32-bit and 64-bit x86 programs and KLEE does not work correctly when executing programs designed far a different architecture than the host machine.
First pull the images (alternatively you can build the 32-bit and 64-bit Docker images from source).
$ docker pull symbooglix/klee_svcomp32:latest $ docker pull symbooglix/klee_svcomp64:latest
Now we need to get the SV-COMP 2015 benchmarks. These have been modified in several ways:
All these changes are visible as commits on top of the official SVCOMP 2015 tag. To obtain the benchmarks run:
$ git clone --branch klee_svcomp15_smack https://github.com/symbooglix/sv-benchmarks.git
Now we can build the benchmarks by using 64-bit Docker image (note the SV-COMP build system will take care of setting the architecture). Run the following:
$ cd sv-benchmarks/c # Start a container, mounting the benchmarks inside the container at /mnt. # Note that the --user= stuff is so that inside the container the same uid/gid is used so # the volume mounted inside the container can be written to. Don't worry about the messages # about not finding the group name or not having a username $ docker run --rm -ti -v $(pwd):/mnt --user=$(id -u):$(id -g) symbooglix/klee_svcomp64 # Now go into the benchmark directory I have no name!@bd3e8672a05b:/home/klee$ cd /mnt # Now we will compile the benchmarks. Note you can use the -jN flag to build N benchmarks concurrently to speed things up I have no name!@bd3e8672a05b:/home/klee$ make CC=clang-3.4 SUPPRESS_WARNINGS=1 # If everything compiled without errors then leave the container I have no name!@bd3e8672a05b:/home/klee$ exit
Now check that inside
sv-benchmarks/c there is a directory called
bin. This contains all the compiled benchmarks (
Now we need to obtain a version of the Boogie-Runner framework that has been modified to run KLEE benchmarks and install its
dependencies. Note the Boogie-Runner framework requires Python3. Note you need root access to run
pip3 like this. If
you don't have root access use Virtualenv to create a virtual Python
enviroment and install the dependencies in it.
$ git clone https://github.com/symbooglix/boogie-runner.git $ cd boogie-runner $ git checkout 8e9c6b630a456696d68ca0a3b171f069d8e651d7 $ pip3 install --requirement requirements.txt
We now have everything needed to run KLEE on the benchmarks.
To run KLEE on the 32-bit benchmarks run the following where
<BENCH_DIR> is the path to the
in the location where you cloned the
https://github.com/symbooglix/sv-benchmarks.git repository and
is a non-existant directory to be created and used as the working directory. The results will be written to
$ ./boogie-batch-runner.py --rprefix <BENCH_DIR>/bin/ <BENCH_DIR>/klee32_config.yml <BENCH_DIR>/program_list.filtered_sbb.32.txt <WORK_DIR_32> results_32.yml
The code for running on the 64-bit benchmarks is similiar. Note KLEE will fail to execute most of these.
$ ./boogie-batch-runner.py --rprefix <BENCH_DIR>/bin/ <BENCH_DIR>/klee64_config.yml <BENCH_DIR>/program_list.filtered_sbb.64.txt <WORK_DIR_64> results_64.yml