Getting Started: Building and Running KLEE

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 targets, using LLVM top-of-tree. KLEE will not work with an older LLVM (e.g., 2.5). We are currently working on full support for Linux and Darwin x86-64 targets.

  1. Install llvm-gcc:
    • Download and install the LLVM 2.6 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.
  2. Download and build LLVM 2.6 (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.6/llvm-2.6.tar.gz
    $ tar zxvf llvm-2.6.tar.gz
    $ cd llvm-2.6
    $ ./configure --enable-optimized
    $ make
    (the --enable-optimized configure argument is not necessary, but KLEE runs very slowly in Debug mode).
  3. Checkout KLEE (to any path you like):
    $ svn co http://llvm.org/svn/llvm-project/klee/trunk klee
  4. 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
  5. Build KLEE (from the KLEE source directory):
    $ make ENABLE_OPTIMIZED=1
  6. Run the regression suite to verify your build:
    $ make check
    $ make unittests
  7. 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.

  1. Download KLEE's uClibc:
    • KLEE uses a version of uClibc which has been modified slightly for use with KLEE. It is available for download here: klee-uclibc-0.01.tgz.
  2. 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.

  3. Configure KLEE with uClibc/POSIX support:
    $ ./configure --with-llvm=path/to/llvm --with-uclibc=path/to/klee-uclibc --enable-posix-runtime
  4. Rebuild KLEE and run make check and verify that the POSIX tests run correctly.