Install KLEE on Ubuntu Server 13.04 x64 system (with LLVM)

Update Oct 2014: 

The original installation log was written in June 2013. At that time Klee project was hosted on http://klee.llvm.org, and their installation instruction was quite confused. Now they move the project to http://klee.github.io/.

It looks like that they have completely re-written the installation instructions on the new website, the procedure is very similar to the one I logged below, you can also refer to their official tutorial.

——————————————————–

I was trying to set up KLEE on Ubuntu 13.04 x64 server edition based on official KLEE guide: http://klee.llvm.org/GetStarted.html.

llvm-gcc and llvm 2.9 are necessary to KLEE.  Initially I tried to compile llvm-gcc from source code on my server, but it failed for some reason. I didn’t have time digging into it (error message is very similar to another user’s post at http://s1151.socode.info/question/508146694f1eba38a44c48e6) So I just use a binary version of llvm-gcc during my installation.

Notice I also use a text editor to edit one of the .cpp files (see comment in the code below) to avoid an error while compiling. I use ‘make -j ‘  to compile faster (if errors occur, please only use ‘make’).

#XL @ 2013.6.29
$ sudo apt-get install build-essential

#Install dependencies
$ sudo apt-get install g++ curl dejagnu subversion bison flex

#download llvm-gcc, I put it in home folder
$ cd ~
$ sudo curl -O http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2  
$ tar xjvf llvm-gcc4.2-2.9-x86_64-linux.tar.bz2

#add path
$ echo "export PATH=$PATH:~/llvm-gcc4.2-2.9-x86_64-linux/bin" >> ~/.bashrc
$ echo "export PATH=$PATH:~/klee/Release+Asserts/bin" >> ~/.bashrc
$ echo "export C_INCLUDE_PATH=/usr/include/x86_64-linux-gnu" >> ~/.bashrc
$ source ~/.bashrc

#download and install llvm
$ sudo 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

$ vi ~/llvm-2.9/lib/ExecutionEngine/JIT/Intercept.cpp
# Use vi (or other text editor) to add this line 
# at the beginning of this cpp file: #include “unistd.h” 
# Otherwise the compiling process may fail

$ make -j $(grep -c processor /proc/cpuinfo)

$ cd ..
$ svn co -r 940 https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp stp
$ cd stp
$ ./scripts/configure --with-prefix=/home/$(whoami)/stp_install --with-cryptominisat2
$ make  -j $(grep -c processor /proc/cpuinfo) OPTIMIZE=-O2 CFLAGS_M32= install

$ cd ..
$ svn co http://llvm.org/svn/llvm-project/klee/trunk klee
$ cd klee
$ ./configure --with-llvm=/home/$(whoami)/llvm-2.9 --with-stp=/home/$(whoami)/stp_install
$ make -j $(grep -c processor /proc/cpuinfo) ENABLE_OPTIMIZED=1
$ make unittests