KLEE-Float - Getting started

Building Imperial’s KLEE tool

Using Docker (the easy way)

docker pull comsys/klee-dev-fpbench-prebuilt:latest
git clone -b tool_exchange_03.05.2017_rebase_extra_bug_fixes https://github.com/srg-imperial/klee-float.git
cd klee-float
scripts/docker_aachen_build.sh

After the scripts execute you will have a docker image on your system called klee-dev-fpbench-patched-final.

You can then get a shell inside a container using that image by running

docker run --rm -ti klee-dev-fpbench-patched-final

Build without Docker (the hard way)

Dependencies

  • LLVM 3.4
  • CMake
  • gcc/Clang
  • Z3 (we used 4c664f1c05786a479e016ffac0d0c6a2e00ab64d but newer versions should be fine).

Building

Just follow the upstream KLEE instructions but

Building benchmarks

Dependencies

  • Python >= 2.7
  • CMake >= 2.8.12
  • gcc or Clang
  • Virtualenv
  • KLEE source tree (this is just for klee.h)
  • A build of KLEE (this is just for libkleeRuntest.so)

Setup Python virtual environment (optional)

virtualenv venv
# Set up shell (this assumes you use Bash)
source venv/bin/activate

Building benchmarks natively

git clone https://github.com/delcypher/symex-fp-bench.git
cd symex-fp-bench/benchmarks/c
git clone https://github.com/delcypher/fp-benchmarks-imperial.git imperial
git clone https://github.com/danielschemmel/fp-benchmarks-aachen aachen
cd ../../../
# Install python dependencies
pip install -r symex-fp-bench/requirements.txt
# Configure build
mkdir build
cd build
KLEE_NATIVE_RUNTIME_LIB_DIR=/path/to/klee/build/lib/ \
  KLEE_NATIVE_RUNTIME_INCLUDE_DIR=/path/to/klee/src/include/ \
  cmake ../symex-fp-bench/
# Compile
make

Building the benchmarks as LLVM bitcode

git clone https://github.com/delcypher/symex-fp-bench.git
cd symex-fp-bench/benchmarks/c
git clone https://github.com/delcypher/fp-benchmarks-imperial.git imperial
git clone https://github.com/danielschemmel/fp-benchmarks-aachen aachen
cd ../../../
# Install python dependencies
pip install -r symex-fp-bench/requirements.txt
# Install wllvm
pip install wllvm
export LLVM_COMPILER=clang
# Configure build
mkdir build
cd build
KLEE_NATIVE_RUNTIME_LIB_DIR=/path/to/klee/build/lib/ \
  KLEE_NATIVE_RUNTIME_INCLUDE_DIR=/path/to/klee/src/include/ \
  CC=wllvm \
  CXX=wllvm++ \
  cmake -DWLLVM_RUN_EXTRACT_BC=ON ../symex-fp-bench/
# Compile
make