Getting Started: Building and Running KLEE

1. Trying out KLEE without installing any dependencies
2. Building KLEE
3. Building KLEE with POSIX runtime support
4. Building KLEE with a more recent version of STP

Trying out KLEE without installing any dependencies

If you would like to try out KLEE without the hassle of compiling or installing dependencies, download the self-contained package (200MB), and follow the instructions in klee-cde-package/README to get up-and-running!

This package contains a self-contained source+binary distribution of KLEE and all of its associated dependencies (e.g., llvm-2.7, llvm-gcc, uClibc, svn). Using this package, you can:

Compile target programs using llvm-gcc
Run KLEE on target programs compiled with llvm-gcc
Modify KLEE's source code, re-compile it to build a new KLEE binary, and then run the test suite using the new binary
Pull the latest KLEE source code updates from SVN
Run the entire Coreutils case study

... all without compiling or installing anything else on your Linux machine!

The only requirement is that you are running a reasonably-modern x86-Linux distro that can execute 32-bit ELF binaries. This package was created using the CDE auto-packaging tool.

Building KLEE

If you would like to try KLEE, the current procedure for building is below.

KLEE is built on LLVM; the first steps are to get a working LLVM installation. See Getting Started with the LLVM System for more information.

NOTE: KLEE is only currently tested on Linux and Darwin x86-32 and x86-64 targets, using LLVM 2.8. KLEE will not work with an older LLVM (e.g., 2.5), and might not work with newer versions of LLVM (e.g., 2.9 or 3.0)

Install llvm-gcc:
- Download and install the LLVM 2.8 release of llvm-gcc from here.
  Add llvm-gcc to your PATH. It is important to do this first so that llvm-gcc is found in subsequent configure steps. llvm-gcc will be used later to compile programs that KLEE can execute.
- Forgetting to add llvm-gcc to your PATH at this point is by far the most common source of build errors reported by new users.
Download and build LLVM 2.8 (you may also use SVN head, but klee may not always be up-to-date with LLVM API changes).
$ curl -O http://llvm.org/releases/2.8/llvm-2.8.tgz
$ tar zxvf llvm-2.8.tgz
$ cd llvm-2.8
$ ./configure --enable-optimized --enable-assertions
$ make
(the --enable-optimized configure argument is not necessary, but KLEE runs very slowly in Debug mode).
Checkout KLEE (to any path you like):
$ svn co http://llvm.org/svn/llvm-project/klee/trunk klee
Alternatively, if you prefer to use git there is also a read-only git mirror, which syncs automatically with each Subversion commit. You can do a git clone of KLEE via:
$ git clone http://llvm.org/git/klee.git
Configure KLEE (from the KLEE source directory):
$ ./configure --with-llvm=path/to/llvm

This assumes that you compiled LLVM in-place. If you used a different directory for the object files then use:
$ ./configure --with-llvmsrc=path/to/llvm/src --with-llvmobj=path/to/llvm/obj
Build KLEE (from the KLEE source directory):
$ make ENABLE_OPTIMIZED=1
Run the regression suite to verify your build:
$ make check
$ make unittests
You're ready to go! Go to the Tutorials page to try KLEE.

Building KLEE with POSIX runtime support

The steps above are enough for building and testing KLEE on closed programs (programs that don't use any external code such as C library functions). However, if you want to use KLEE to run real programs you will want to enable the KLEE POSIX runtime, which is built on top of the uClibc C library.

Download KLEE's uClibc:
- KLEE uses a version of uClibc which has been modified slightly for use with KLEE.
  - A version that works on 32-bit Linux can be found here
  - A version that works on 64-bit Linux can be found here
Build uClibc with llvm-gcc:
$ tar zxvf klee-uclibc-0.01.tgz
$ ./configure --with-llvm=path/to/llvm
$ make

NOTE: KLEE's uClibc is shipped in a pre-configured for x86-32. If you are on a different target (e.g. x86-64), you will need to run 'make config' and select the correct target. The defaults for the other uClibc configuration variables should be fine.
Configure KLEE with uClibc/POSIX support:
$ ./configure --with-llvm=path/to/llvm --with-uclibc=path/to/klee-uclibc --enable-posix-runtime
Rebuild KLEE and run make check and verify that the POSIX tests run correctly.

Building KLEE with a more recent version of STP

If your benchmarks are running slowly or not terminating it may be worth trying a more recent version of KLEE's constraint solver STP, which offers performance improvements over the version supplied with KLEE.

STP does not make frequent releases, and its Subversion repository is under constant development and may be unstable. The instructions below are for a particular revision which is known to pass the KLEE test suite, but you can try a more recent revision (at your own risk) by changing or removing the -r argument to the svn co command.