KLEE-FP (also called KLEE-CL) is an extension to the KLEE symbolic execution tool that supports symbolic reasoning on the equivalence between floating-point values.

KLEE-FP features an OpenCL runtime, allowing it to symbolically execute OpenCL kernels. OpenCL support is based on a POSIX threading model for KLEE provided by the Cloud9 developers.

KLEE-FP and our benchmarks are freely available from our Git repositories:

Tool:

• KLEE FP
• KLEE FP’s UcLibc

Benchmarks:

• OpenCV
• Bullet, OP2
• Parboil

The versions of the tool and OpenCV benchmarks that we used in our EuroSys ‘11 paper are tagged “eurosys”.

Build Instructions

Compiling LLVM and Clang

KLEE-FP depends on recent versions of LLVM and Clang from SVN. Instructions for building these are found here. However, because KLEE-FP has not yet been updated to work with the latest versions of LLVM and Clang, an older version must be used by substituting svn co with svn co -r 146372 in any command invoked.

If you wish to use the OpenCL runtime, then before building LLVM and Clang, you should apply the patches found in KLEE-FP’s patches directory to both LLVM and Clang – specifically, the patches named llvm-*.patch (not llvm2.7-*.patch) and clang-*.patch should be applied to LLVM and Clang respectively.

Compiling uclibc

uclibc is built using Clang. Simply follow the instructions in the README.klee file. But if you did not build LLVM and Clang in Debug+Asserts mode you should, before configuring uclibc, execute the following command:

sed -i 's/Debug+Asserts/yourbuildmode/g' Rules.mak.llvm

touch lib/crtn.o

Compiling KLEE-FP

KLEE-FP is built in the standard way for KLEE (see here, follow steps 4-5), with some deviations.

To compile KLEE-FP, first of all compile uclibc, then supply the –with-uclibc=/path/to/klee-uclibc command line option to configure.

If you did not apply the patches to LLVM and Clang, OpenCL support must be disabled, else you will encounter build errors. To disable OpenCL support, the –disable-opencl flag must be supplied to configure.

Using KLEE-FP

To use the OpenCL runtime library, ensure that the environment variable KLEE_UCLIBC_ROOT is set to the path to the klee-uclibc directory, and supply the -posix-runtime -opencl-runtime -libc=uclibc command line options to KLEE-FP.

To use the floating point rewriter described in our EuroSys paper, supply the -use-fp-rewriter -use-fptoi-abstraction command line options to KLEE-FP. Without these flags, KLEE-FP will use a floating point bit blaster (originally developed for CBMC) to solve floating point constraints.