Building KLEE

with LLVM 3.4 and Autoconf build system

NOTE: This is the documentation for KLEE 1.4.0 which from the lastest version of KLEE from the master branch. For documentation relevant to KLEE’s master branch see the homepage.

The current procedure for building KLEE with LLVM 3.4 (recommended) using KLEE’s older Autoconf/Makefile build system is outlined below. If you want to build KLEE with LLVM 2.9, click here.

Install dependencies: KLEE requires all the dependencies of LLVM, which are discussed here. In particular, you should install the following programs and libraries, listed below as Ubuntu packages:
```
$ sudo apt-get install build-essential curl libcap-dev git cmake libncurses5-dev python-minimal python-pip unzip
```
You will need gcc/g++ 4.8 or later installed on your system. For Ubuntu 12.04 and 13.04, you can follow the instructions here.

(Optional) Build KLEE with TCMalloc support: By default, KLEE uses malloc_info() to observe and to restrict its memory usage. Due to limitations of malloc_info(), the maximum limit is set to 2 GB. To support bigger limits, KLEE can use TCMalloc as an alternative allocator. It is thus necessary to install TCMalloc:
```
$ sudo apt-get install libtcmalloc-minimal4 libgoogle-perftools-dev
```
Install LLVM 3.4: KLEE is built on top of LLVM; the first steps are to get a working LLVM installation. See Getting Started with the LLVM System for more information.

NOTE: KLEE is currently tested on Linux x86-64, and might break on x86-32.

If you are using a recent Ubuntu (≥ 12.04, e.g. 14.04 LTS) or Debian, we recommend you to use the LLVM packages provided by LLVM itself. Use LLVM Package Repository to add the appropriate line to your /etc/apt/sources.list. As an example, for Ubuntu 14.04, the following lines should be added:
```
deb http://llvm.org/apt/trusty/ llvm-toolchain-trusty-3.4 main  
deb-src http://llvm.org/apt/trusty/ llvm-toolchain-trusty-3.4 main
```
Then add the repository key and install the 3.4 packages:
```
$ wget -O - http://llvm.org/apt/llvm-snapshot.gpg.key|sudo apt-key add -  
$ sudo apt-get update  
$ sudo apt-get install clang-3.4 llvm-3.4 llvm-3.4-dev llvm-3.4-tools  
```
Finally, make sure llvm-config is in your path:
```
$ sudo ln -sf /usr/bin/llvm-config-3.4 /usr/bin/llvm-config
```
That’s it for LLVM. If you want to install it manually, please refer to the official LLVM Getting Started documentation.
Build STP: KLEE is based on the STP constraint solver, you can find the instructions here.
(Optional) Build uclibc and the POSIX environment model: 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.
```
$ git clone https://github.com/klee/klee-uclibc.git  
$ cd klee-uclibc  
$ ./configure --make-llvm-lib  
$ make -j2  
$ cd .. 
```
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.
(Optional) Build libgtest:

Build Google test libraries for unit tests. We do a manual build, because the libgtest-dev package (version 1.6) installed through apt does not work for us.
```
$ curl -OL https://googletest.googlecode.com/files/gtest-1.7.0.zip  
$ unzip gtest-1.7.0.zip  
$ cd gtest-1.7.0  
$ cmake .  
$ make  
$ cd ..
```

Get KLEE source:

$ git clone https://github.com/klee/klee.git

Configure KLEE: From the KLEE source directory, run:
```
$ ./configure --with-stp=/full/path/to/stp/build --with-uclibc=/full/path/to/klee-uclibc --enable-posix-runtime
```
NOTE: If LLVM is not found or you have multiple LLVM versions installed, you can add --with-llvmsrc=/usr/lib/llvm-3.4/build --with-llvmobj=/usr/lib/llvm-3.4/build --with-llvmcc=/usr/bin/clang-3.4 --with-llvmcxx=/usr/bin/clang++-3.4.
If you skipped step 4, simply remove the --with-uclibc and --enable-posix-runtime options.
Build KLEE:
```
$ make  
```
NOTE: You can add /full/path/to/klee/build/Release/bin to your path.
Run the main regression test suite to verify your build:
```
$ make systemtests
```
If you want to invoke lit manually use:
```
$ /usr/lib/llvm-3.4/build/utils/lit/lit.py test/
```
This way you can run individual tests or subsets of the suite:
```
$ /usr/lib/llvm-3.4/build/utils/lit/lit.py test/regression
```

(Optional) Run the unit tests:

If you did not install the LLVM upstream or Debian packages, install the LLVM unit tests makefile:

$ sudo mkdir -p /usr/lib/llvm-3.4/build/unittests/  
$ sudo curl -L http://llvm.org/svn/llvm-project/llvm/branches/release_34/unittests/Makefile.unittest -o /usr/lib/llvm-3.4/build/unittests/Makefile.unittest

Run KLEE unit tests:

$ make CPPFLAGS=-I/full/path/to/gtest-1.7.0/include LDFLAGS=-L/full/path/to/gtest-1.7.0 unittests

You’re ready to go! Check the Tutorials page to try KLEE.

NOTE: For testing real applications (e.g. Coreutils), you may need to increase your system’s open file limit (ulimit -n). Something between 10000 and 999999 should work. In most cases, the hard limit will have to be increased first, so it is best to directly edit the /etc/security/limits.conf file.