Skip to content

Latest commit

 

History

History
93 lines (66 loc) · 4.93 KB

build-llvm29.md

File metadata and controls

93 lines (66 loc) · 4.93 KB
layout title subtitle slug
default
Building KLEE
with LLVM 2.9
build-llvm29

The current procedure for building KLEE with LLVM 2.9 is outlined below. If you want to build KLEE with LLVM 3.4 (recommended), click here.

  1. 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, bc, libcap-dev(el):

    $ sudo apt-get install g++ python curl cmake git bison flex bc libcap-dev # Ubuntu
$ sudo dnf install g++ python curl cmake git bison flex bc libcap-devel # Fedora 21+

    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

    (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

  2. 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: The only LLVM version currently supported by KLEE is LLVM 2.9. KLEE is currently tested on Linux x86-64, and might break on x86-32. KLEE will not compile with LLVM versions prior to 2.9, and there is only experimental support for LLVM 3.4.

    1. Install llvm-gcc:

      • Download and install the LLVM 2.9 release of llvm-gcc from here. On an x86-64 Linux platform you are going to need the archive LLVM-GCC 4.2 Front End Binaries for Linux x86-64.
      • 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:

      $ 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. You may run into compilation issues if you use new kernels/glibc versions. Please see this mailing list post for details on how to fix this issue.

  3. Build STP: KLEE is based on the STP constraint solver, you can find the instructions here.

  4. (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.

  5. Download KLEE:

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

  6. Configure KLEE: From the KLEE source directory, run:

    $ ./configure --with-llvm=full-path-to-llvm --with-stp=full-path-to-stp/install --with-uclibc=full-path-to-klee-uclibc --enable-posix-runtime

    NOTE: If you skipped step 4, simply remove the --with-uclibc and --enable-posix-runtime options.

  7. Build KLEE:

    $ make ENABLE_OPTIMIZED=1

  8. Run the regression suite to verify your build:

    $ make check  
$ make unittests

    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.

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