LLVM 13 (recommended)
Building KLEE with LLVM 13
NOTE: This is the documentation for KLEE 3.0, which might differ from the latest version of KLEE from the master branch. For documentation relevant to KLEE’s master branch see the homepage.
The current procedure for building KLEE manually with LLVM 13 (recommended) on Debian/Ubuntu-based distributions or macOS is outlined below. However, in case you trust our installation scripts for continuous integration testing, you can re-use them on your Ubuntu/macOS-based host system. You can find detailed instructions in: Building arbitrary KLEE configurations.
NOTE: KLEE is currently tested on Linux x86-64 (particularly Ubuntu), FreeBSD and macOS. There is no support for uClibc and the POSIX environment under macOS. KLEE does not work under x86-32.
Install dependencies: KLEE requires all the dependencies of LLVM (see here), and some more. In particular, you should install the programs and libraries listed below.
graphviz/doxygenare optional and only needed to generate the source code documentation.
Under Ubuntu, use:
$ sudo apt-get install build-essential cmake curl file g++-multilib gcc-multilib git libcap-dev libgoogle-perftools-dev libncurses5-dev libsqlite3-dev libtcmalloc-minimal4 python3-pip unzip graphviz doxygen
Under macOS, run:
$ brew install curl git cmake python unzip gperftools sqlite3 graphviz doxygen bash
You should also install
litto enable testing,
tabulateto support additional features in
wllvmto make it easier to compile programs to LLVM bitcode:
$ sudo pip3 install lit wllvm $ sudo apt-get install python3-tabulate
pip3to install packages for the current user only:
$ pip3 install --user lit wllvm
and make sure that e.g.
python3 -m site --user-baseon your system) is in your
Install LLVM 13: 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.
If you are using a recent Ubuntu (e.g. 21.10) or Debian, we recommend to use the LLVM packages provided by LLVM itself.
$ sudo apt-get install clang-13 llvm-13 llvm-13-dev llvm-13-tools
If you are using macOS, you can install older LLVM packages using brew:
$ brew install llvm@13
That’s it for LLVM. If you want to install it manually, please refer to the official LLVM Getting Started documentation.
Install constraint solver(s)
KLEE supports multiple different constraint solvers. You must install at least one to build KLEE.
- STP Historically KLEE was built around STP so support for this solver is the most stable. For build instructions, see here.
- Z3 is another solver supported by KLEE that is reasonably stable. You should use Z3 version ≥ 4.4. Z3 is packaged by many distributions. For build instructions, see here.
- metaSMT supports
various solvers, including Boolector, CVC4, STP, Z3 and Yices. We recommend branch v4.rc1 (
git clone -b v4.rc1 ...). For build instructions, see here.
(Optional) Get Google test sources:
For unit tests we use the Google test libraries. If you want to run the unit tests you need to perform this step and also pass
-DENABLE_UNIT_TESTS=ONto CMake when configuring KLEE in step 8.
We currently recommend version
1.11.0, so grab the sources for it.
$ curl -OL https://github.com/google/googletest/archive/release-1.11.0.zip $ unzip release-1.11.0.zip
This will create a directory called
(Optional) Build uClibc and the POSIX environment model (not supported on macOS): 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 # --with-cc clang-13 --with-llvm-config llvm-config-13 $ make -j2 $ cd ..
llvm-configare not in your
PATHor have a custom prefix/suffix,
configuremay fail to detect their location. You can use the
--with-llvm-configflags to set the paths manually.
NOTE: If you are on a different target (i.e., not i386 or x64), you will need to run
make configand select the correct target. The defaults for the other uClibc configuration variables should be fine.
To tell KLEE to use both klee-uclibc and the POSIX runtime, pass
-DKLEE_UCLIBC_PATH=<KLEE_UCLIBC_SOURCE_DIR>to CMake when configuring KLEE in step 8 where
<KLEE_UCLIBC_SOURCE_DIR>is the absolute path to the cloned
Get KLEE source
$ git clone https://github.com/klee/klee.git
(Optional) Build libc++: To be able to run C++ code, you also need to enable support for the C++ standard library.
Make sure that
clang++-13is in your path. Then, run from the main KLEE source directory:
$ LLVM_VERSION=13 BASE=<LIBCXX_DIR> ENABLE_OPTIMIZED=1 DISABLE_ASSERTIONS=1 ENABLE_DEBUG=0 REQUIRES_RTTI=1 klee/scripts/build/build.sh libcxx
<LIBCXX_DIR>is the absolute path where libc++ should be cloned and built.
To tell KLEE to use libc++, pass the following flags to CMake when you configure KLEE in step 8:
-DENABLE_KLEE_LIBCXX=ON -DKLEE_LIBCXX_DIR=<LIBCXX_DIR>/libc++-install-130/ -DKLEE_LIBCXX_INCLUDE_DIR=<LIBCXX_DIR>/libc++-install-130/include/c++/v1/
To additionally enable KLEE’s exception handling support for C++, pass the following flags to CMake when you configure KLEE in step 8:
<LIBCXX_DIR>must currently be an absolute path. If you want to build libc++ in your home path, note that in some environments (such as Ubuntu 18.04)
~may not be an absolute path. You can use
KLEE must be built “out of source”, so first create a build directory. You can create this wherever you like. Below, we assume you create this directory inside KLEE’s repository.
$ mkdir build
cdinto the build directory and run CMake to configure KLEE where
<KLEE_SRC_DIRECTORY>is the path to the KLEE git repository you cloned in the previous step.
$ cd build $ cmake <CMAKE_OPTIONS> <KLEE_SRC_DIRECTORY>
<CMAKE_OPTIONS>are the configuration options. These are documented in README-CMake.md.
For example, if you want to build KLEE with STP, the POSIX runtime, klee-uclibc and unit testing then the command line would look something like this:
$ cmake -DENABLE_SOLVER_STP=ON -DENABLE_POSIX_RUNTIME=ON -DKLEE_UCLIBC_PATH=<KLEE_UCLIBC_SOURCE_DIR> -DENABLE_UNIT_TESTS=ON -DGTEST_SRC_DIR=<GTEST_SOURCE_DIR> <KLEE_SRC_DIRECTORY>
<KLEE_UCLIBC_SOURCE_DIR>is the absolute path to the klee-uclibc source tree and
<GTEST_SOURCE_DIR>is the absolute path to the Google Test source tree.
Or more concretely, with
/srcas working directory,
/src/klee/buildas build directory, and libcxx support enabled:
$ cmake -DENABLE_SOLVER_STP=ON -DENABLE_POSIX_RUNTIME=ON -DKLEE_UCLIBC_PATH=/src/klee-uclibc -DENABLE_UNIT_TESTS=ON -DGTEST_SRC_DIR=/src/googletest-release-1.11.0/ -DENABLE_KLEE_LIBCXX=ON -DKLEE_LIBCXX_DIR=/src/libcxx/libc++-install-130/ -DKLEE_LIBCXX_INCLUDE_DIR=/src/libcxx/libc++-install-130/include/c++/v1/ -DENABLE_KLEE_EH_CXX=ON -DKLEE_LIBCXXABI_SRC_DIR=/src/libcxx/llvm-130/libcxxabi/ ..
NOTE 1: You can simply type
cmake ..to use the default options for KLEE but these will not include support for uClibC and the POSIX runtime.
NOTE 2: If LLVM is not found or you need a particular version to be used, you can pass
-DLLVM_DIR=<LLVM_DIR>to CMake where
<LLVM_DIR>is the absolute path to the relevant build or installation directory (e.g.
/usr/lib/llvm-13/). Similarly, KLEE needs a C and C++ compiler that can create LLVM bitcode that is compatible with the LLVM version KLEE is using. If these are not detected automatically,
-DLLVMCXX=<PATH_TO_CLANG++>can be passed to explicitly set these compilers, where
<PATH_TO_CLANG>is the absolute path to
<PATH_TO_CLANG++>is the absolute path to
NOTE 3: By default, KLEE uses tcmalloc as its allocator, to support reporting of memory usage above 2GB. If you don’t want to install tcmalloc (
libtcmalloc-minimal4 libgoogle-perftools-devUbuntu packages) on your system or prefer to use the glibc allocator, pass
-DENABLE_TCMALLOC=OFFto CMake when configuring KLEE.
builddirectory created in the previous step run:
(Optional) Run the main regression test suite
If KLEE was configured with system tests enabled then you can run them like this:
$ make systemtests
If you want to invoke
$ lit test/
This way you can run individual tests or subsets of the suite:
$ lit test/regression
(Optional) Build and run the unit tests:
If KLEE was configured with unit tests enabled then you can build and run the unit tests:
$ make unittests
NOTE: You can run both, the system and unit tests, with
You’re ready to go! Check the Documentation 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 corresponding configuration file (e.g.,