Getting Started: Building and Running KLEE
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.
NOTE: The CDE package is mainly meant for trying out KLEE on some simple examples and the Coreutils case study. It is likely that you will run into errors when testing other applications, in which case you will need to follow the full installation instructions below.
The current procedure for building is outlined below.
- Install dependencies:
KLEE requires all the dependencies of LLVM, which are discussed here. In particular, you should have the following packages (the list is likely not complete): g++, curl, dejagnu, subversion, bison, flex:
$ sudo apt-get install g++ curl dejagnu subversion bison flex (Ubuntu)On some architectures, you might also need to set the following environment variables (best to put them in a config file like .bashrc):
$ sudo yum install g++ curl dejagnu subversion bison flex (Fedora)$ export C_INCLUDE_PATH=/usr/include/x86_64-linux-gnu
$ export CPLUS_INCLUDE_PATH=/usr/include/x86_64-linux-gnu
- Build LLVM 2.9:
NOTE: KLEE is currently tested only on Linux x86-32 and x86-64 targets, using LLVM 2.9. KLEE will not work with older LLVM versions (e.g., 2.5), and might not work with newer versions (e.g., 3.0).
- Install llvm-gcc:
- Download and install the LLVM 2.9 release of llvm-gcc
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 install the LLVM 2.9 release of llvm-gcc from here.
- Download and build LLVM 2.9:
$ curl -O http://llvm.org/releases/2.9/llvm-2.9.tgz(the --enable-optimized configure argument is not necessary, but KLEE runs very slowly in Debug mode).
$ tar zxvf llvm-2.9.tgz
$ cd llvm-2.9
$ ./configure --enable-optimized --enable-assertions
- Install llvm-gcc:
KLEE is based on the STP constraint solver. 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 we have used successfully, but you can try a more recent revision by changing or removing the -r argument to the svn co command. (Please let us know if you have successfully and extensively used KLEE with a more recent version of STP.)
$ cd stp
$ ./scripts/configure --with-prefix=path/to/stp/install --with-cryptominisat2
$ make OPTIMIZE=-O2 CFLAGS_M32= install
By default, KLEE works 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 our purposes.
- Build uClibc with llvm-gcc:
$ tar zxvf klee-uclibc-0.02.tgz
$ ./configure --with-llvm=path/to/llvm
NOTE: If you are on a different target (i.e., not i386 or x64), you will need to run make config and select the correct target. The defaults for the other uClibc configuration variables should be fine.
From the KLEE source directory, run:
NOTE: If you skipped step 3, simply remove the --with-uclibc and --enable-posix-runtime options.
$ make unittests
NOTE: If you are installing the system of Ubuntu 12.04 (or similar), you might want to take a look at this message.