Symbooglix Artifact

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.

Boogie tool comparison

Obtaining the benchmarks

WARNING: The sbb repo is very large. It takes roughly 13 GiB of space.

The gpu and 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.

Obtaining the tools

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 make in https://github.com/symbooglix/icst16-tools-docker-files.

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 icst

Each docker image has the boogie-runner framework installed which can be invoked via the boogie-runner.py or boogie-batch-runner.py commands. Each docker image also has the boogie-runner config files (.yml) 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

Creating a container

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

Note

/path/to/benchmark/directory should be the path to the directory containing one of the benchmark suites you downloaded earlier.
The -v flag is creating a volume inside the container. In the above example the benchmark directory is mounted inside the container at /mnt
--rm flag 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:icst16 is 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.

Running a tool directly

The tools are on the ase user's PATH inside the container so you can invoke them directly if you wish. The tool executables are:

Boogie.exe (in the symbooglix/boogie:icst16 image)
boogaloo (in the symbooglix/boogaloo:icst16 image)
Corral.exe (in the symbooglix/corral:icst16 image)
gpuverify (in the symbooglix/gpuverify:icst16 image)
sbx.exe (in the symbooglix/symbooglix:icst16 image)

Running a single benchmark using boogie-runner.py

The boogie-runner.py tool allows a single benchmark to be run conveniently. To try it run:


      boogie-runner.py config.yml /path/to/boogie/program.bpl work_dir result.yml

config.yml is one of the YAML configuration files in the home directory.
/path/to/boogie/program.bpl is the path inside the container to the Boogie program you wish the tool to use
work_dir is a working directory for the run. It should not already eixst.
result.yml is the path to write the results to.

Running a set of benchmarks using boogie-batch-runner.py

The 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

KLEE comparison

Running Symbooglix

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 boogie-batch-runner.py is klee_comparision_program_list.txt in the root of the sbb repository.

Running KLEE

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:

The new Makefile build system for the C benchmarks in SV-COMP 2016 has been back-ported
The benchmarks that were not converted to Boogie programs by the authors of SMACK were removed
Various fixes were applied to make compilation with Clang possible

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 (*.oi and *.oc files).

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 c directory in the location where you cloned the https://github.com/symbooglix/sv-benchmarks.git repository and <WORK_DIR_32> is a non-existant directory to be created and used as the working directory. The results will be written to results_32.yml.


    $ ./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

Getting help

If you have issues using the Docker images the please contact me.