- -

Getting Started: Building and Running KLEE

- - - -

-1. Trying out KLEE without installing any dependencies
-2. Building 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. -

- - -

Building KLEE

- - -

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)
- $ sudo yum install g++ curl dejagnu subversion bison flex (Fedora) -
-
- -On some architectures, you might also need to set the following environment variables (best to put them in a config file like .bashrc): -
- $ export C_INCLUDE_PATH=/usr/include/x86_64-linux-gnu
- $ export CPLUS_INCLUDE_PATH=/usr/include/x86_64-linux-gnu -
- -
Build LLVM 2.9: - -
-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 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). -
- - -
1. Install llvm-gcc: -
  - Download and install the LLVM 2.9 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.
  -
2. Download and build LLVM 2.9: -
  - $ curl -O http://llvm.org/releases/2.9/llvm-2.9.tgz
  - $ tar zxvf llvm-2.9.tgz
  - $ cd llvm-2.9
  - $ ./configure --enable-optimized --enable-assertions
  - $ make -
  - - (the --enable-optimized configure argument is not necessary, but - KLEE runs very slowly in Debug mode). -
- - -
Build STP: - -
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.) -
- -
- $ svn co -r 940 https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp stp
- $ cd stp
- $ ./scripts/configure --with-prefix=path/to/stp/install --with-cryptominisat2
- $ make OPTIMIZE=-O2 CFLAGS_M32= install -
-

- $ ulimit -s unlimited -

[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. -
- -
1. Download KLEE's uClibc. KLEE uses a version - of uClibc which has been - modified slightly for our purposes. -
  - A version that works on 32-bit Linux can be found - here -
  - A version that works on 64-bit Linux can be found - here -
  -
2. Build uClibc with llvm-gcc: -
  - $ tar zxvf klee-uclibc-0.02.tgz
  - $ ./configure --with-llvm=path/to/llvm
  - $ make
  -
  - -
  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.
  -
- - -
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, run:
-
- $ ./configure --with-llvm=path/to/llvm --with-stp=path/to/stp/install --with-uclibc=path/to/klee-uclibc --enable-posix-runtime -
- -
NOTE: If you skipped step 4, simply remove the --with-uclibc and --enable-posix-runtime options.
-
Build KLEE: -
- $ 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.

- -

NOTE: If you are installing the system of Ubuntu 12.04 (or similar), you might want to take a look at this message.

-
- -

Getting Started: Building and Running KLEE

-1. Trying out KLEE without installing any dependencies -2. Building KLEE -

Trying out KLEE without installing any dependencies

Building KLEE

-1. Trying out KLEE without installing any dependencies
-2. Building KLEE
-