Getting started quickly

1. Get the tap2019 virtual machine here
2. Get the artifact here
3. Unzip the content into the tap2019 user’s home directory.

Getting started - extended

The artifact is based on the requirements as described in: TAP 2019 Artifact.

We assume a Ubuntu 19.04 based system.

Unfortunately, LLVM 3.8 is not provided for Ubuntu 19.04, but we use this version to run our experiments with. To resemble this setup, we prebuilt all dependencies as part of this artifact. The dependencies are self-contained but require to be put to the following location: /home/tap2019.

Unpack the content of the file into /home/tap2019

Running benchmarks

Export the following entries, to make the klee executable accessible from any directory.

export PATH="/home/tap2019/klee/build/bin/:/home/tap2019/llvm-38-install_O_D_A/bin/:$PATH"

Validate with klee --version it should print:

KLEE 1.4.0.0 (https://klee.github.io)
  Build mode: RelWithDebInfo (Asserts: TRUE)
  Build revision: 85616bcc27f6d9503c82e1fabb585661fdaa21e6

LLVM (http://llvm.org/):
  LLVM version 3.8.1
  Optimized build with assertions.
  Built Jul  9 2019 (15:19:14).
  Default target: x86_64-unknown-linux-gnu
  Host CPU: skylake

Coreutils

For coreutils, the specific KLEE invocation instructions are located under: /home/tap2019/experiments/Jobs. You can run each experiment with rm -rf /tmp/klee-out && . exp-name, e.g.:

rm -rf /tmp/klee-out && . /home/tap2019/experiments/Jobs/experiment38z3int-chown.bc-detcountttopfixed.json

The different jobs have the following structure: experiment38z3int-[APPLICATION].bc-[TYPE].json, with:

• APPLICATION: the tested application
• TYPE: one of the following experiment types:
  • detcountttopfixed: log the reasons why the bitvector solver has been chosen over integer solver
  • detinttfixed: use integer solver and bitvector solver (deterministic setup)
  • intfixed: use integer solver and bitvector solver
  • detcrosscheckfixed: crosscheck results of the integer solver with the bitvector solver
  • detnointt: just bitvector solver (deterministic setup)
  • noint: just bitvector solver

Test-Comp

For Test-Comp, different software artifacts are under /home/tap2019/experiments/test-comp.

In addition, the benchexec tool should be installed. Follow the instructions here: https://github.com/sosy-lab/benchexec/blob/master/doc/INSTALL.md#debianubuntu

In a nutshell, execute the following:

sudo apt install python3-tempita python3-coloredlogs lxcfs python3-yaml
wget https://github.com/sosy-lab/benchexec/releases/download/1.21/benchexec_1.21-1_all.deb
sudo dpkg -i benchexec_*.deb
sudo adduser tap2019 benchexec

Log out of the current session and login again.

In /home/tap2019/experiments/test-comp run benchexec --container bench-defs/benchmark-defs/klee.xml --no-compress-results -T 5 -M 7000MB

Which runs the experiments for 5min and allows a maximum of 7GiB memory to be used by KLEE.

Resource Requirements

We ran the experiments on multiple machines with Intel(R) Core(TM) i7-4790 CPU @ 3.60GHz and 16GB of memory that have Ubuntu 18.04.2 as the host system.

Re-Build Instructions

In case you want to rebuild parts of the software artifacts, please install the default developer packages:

sudo apt update
sudo apt install build-essential

And in the case for specific packages:

• For UCLIBC with LLVM 3.8 support install libgcc-6-dev

Changes in comparison to the paper version

Update GNU Coreutils from 8.29 to 8.31 as the older version cannot be built on Ubuntu 19.04.

../lib/freadseek.c:68:3: error: "Please port gnulib freadseek.c to your platform! Look at the definition of getc, getc_unlocked on your system, then report this to bug-gnulib."
 #error "Please port gnulib freadseek.c to your platform! Look at the definition of getc, getc_unlocked on your system, then report this to bug-gnulib."
  ^
1 error generated.

Source Code

The source code is available at GitHub.

Artifact summary

sha256sum tap2019_int_klee.zip
5234b5665f7fb6204d6d6d4ce4d086c23390db925de6ce65c628399157f986ce  tap2019_int_klee.zip