[klee-dev] KLEE setup scripts for Ubuntu (LLVM 2.9 and 3.4)

Fri Oct 10 11:09:07 BST 2014

Hi everyone,

I've attached 2 simple KLEE setup scripts, one for LLVM 2.9 and another 
for 3.4. They include all necessary patches, etc. I hope they will be 
useful for other KLEE users, too. Especially with LLVM 3.4 it takes some 
time to figure out how to build everything successfully (the 
"Experimental" guide on the website seems to be outdated).

They work on 64-bit Ubuntu 14.04.
On 12.04, cmake 2.8.8 or higher has to be installed, I used 2.8.12.2 ( 
How-to: 
http://cameo54321.blogspot.com/2014/02/installing-cmake-288-or-higher-on.html 
). Furthermore, for LLVM 3.4, besides the newer cmake, also GCC 4.8 or 
higher is required ( How-to: 
http://mortenvp.com/installing-a-newer-gccg-on-ubuntu-12-04-lts/ -- 
Replace 4.7 with 4.8 ).

While browsing the KLEE issues on GitHub today, I just saw that 
antiAgainst has also published KLEE setup scripts a few months ago ( 
https://github.com/klee/klee/issues/123 ). I decided to post mine 
nonetheless... having more is better.

Best regards,
Emil

-------------- next part --------------
#! /bin/bash

# KLEE install script.
#
# Sets up llvm-gcc 4.2, llvm 2.9, upstream STP, 0_9_29 klee-uclibc (currently upstream), and upstream KLEE.
#
# Based on http://klee.github.io/klee/GetStarted.html and threads from https://www.mail-archive.com/klee-dev@imperial.ac.uk
# 
# Tested on 64-bit Ubuntu 14.04.
#
# On Ubuntu 12.04, cmake 2.8.8 or higher, e.g. 2.8.12.2 has to be installed ( How-to: 
# http://cameo54321.blogspot.com/2014/02/installing-cmake-288-or-higher-on.html )
#
# Author: Emil Rakadjiev <emil.rakadjiev.bf at hitachi.com>

if [ ! -z "$1" ]
then
	BASEDIR="$1"
else
	BASEDIR="klee"
fi

mkdir -p "$BASEDIR"
BASEDIR=$(cd $BASEDIR; pwd)
echo "Installing KLEE and dependencies to ${BASEDIR}"

# Install required packages
sudo apt-get update
sudo apt-get install -y build-essential curl python-minimal git bison flex bc libcap-dev git cmake libboost-all-dev valgrind libm4ri-dev libmysqlclient-dev libsqlite3-dev libtbb-dev libncurses5-dev

# Persist environment variables
sudo sh -c 'echo "export C_INCLUDE_PATH=/usr/include/x86_64-linux-gnu" > /etc/profile.d/kleevars.sh'
sudo sh -c 'echo "export CPLUS_INCLUDE_PATH=/usr/include/x86_64-linux-gnu" >> /etc/profile.d/kleevars.sh'
. "/etc/profile.d/kleevars.sh"

# Install llvm-gcc
cd "$BASEDIR"
curl -4OL 'http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2'
sudo tar -xjf "llvm-gcc4.2-2.9-x86_64-linux.tar.bz2" -C "/usr/local/"
sudo sh -c 'echo "export PATH=\$PATH:/usr/local/llvm-gcc4.2-2.9-x86_64-linux/bin" >> /etc/profile.d/kleevars.sh'
. "/etc/profile.d/kleevars.sh"

# Install llvm
curl -4OL 'http://llvm.org/releases/2.9/llvm-2.9.tgz'
rm -rf "${BASEDIR}/llvm-2.9"
tar -xzf "llvm-2.9.tgz"
# See: https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01302.html
curl -4OL 'http://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01302/unistd-llvm-2.9-jit.patch'
patch "llvm-2.9/lib/ExecutionEngine/JIT/Intercept.cpp" "unistd-llvm-2.9-jit.patch"
cd "${BASEDIR}/llvm-2.9"
./configure --enable-optimized --enable-assertions
make
sudo sh -c 'echo "export PATH=\$PATH:'"$BASEDIR"'/llvm-2.9/Release+Asserts/bin" >> /etc/profile.d/kleevars.sh'
. "/etc/profile.d/kleevars.sh"

# Install stp
cd "$BASEDIR"
rm -rf "${BASEDIR}/stp"
git clone 'https://github.com/stp/stp.git'
mkdir "${BASEDIR}/stp/build"
cd "${BASEDIR}/stp/build"
# Upstream STP builds shared libraries by default, which causes problems for KLEE, so we disable them 
# (see: https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01704.html )
# The Python interface requires shared libraries, so we have to disable that, too. This 
# disables testing, but we normally don't want to run STP tests anyway.
cmake -DBUILD_SHARED_LIBS:BOOL=OFF -DENABLE_PYTHON_INTERFACE:BOOL=OFF ..
make OPTIMIZE=-O2 CFLAGS_M32=
sudo make install
# TODO for persisting the stack size limit, customize /etc/security/limits.conf
# "nofile" limit should normally be increased, too
ulimit -s unlimited

# Install klee-uclibc
cd "$BASEDIR"
rm -rf "${BASEDIR}/klee-uclibc"
git clone --depth 1 --branch klee_0_9_29 'https://github.com/klee/klee-uclibc.git'
cd "${BASEDIR}/klee-uclibc"
./configure --make-llvm-lib
make -j

# Install klee
cd "$BASEDIR"
rm -rf "${BASEDIR}/klee"
git clone 'https://github.com/klee/klee.git'
mkdir "${BASEDIR}/klee/build"
cd "${BASEDIR}/klee/build"
../configure --with-llvm="${BASEDIR}/llvm-2.9" --with-stp="${BASEDIR}/stp/build" --with-uclibc="${BASEDIR}/klee-uclibc" --enable-posix-runtime
make ENABLE_OPTIMIZED=1
sudo sh -c 'echo "export PATH=\$PATH:'"${BASEDIR}/klee/build/Release+Asserts/bin"'" >> /etc/profile.d/kleevars.sh'

# Run klee tests
make check
make unittests
-------------- next part --------------
#! /bin/bash

# KLEE install script.
#
# Sets up llvm 3.4, upstream STP, 0_9_29 klee-uclibc (currently upstream), gtest 1.7.0, and upstream KLEE.
#
# Based on http://klee.github.io/klee/GetStarted.html , http://klee.github.io/klee/Experimental.html , 
# https://github.com/klee/klee/tree/master/.travis and threads from https://www.mail-archive.com/klee-dev@imperial.ac.uk
# 
# Tested on 64-bit Ubuntu 14.04.
#
# For Ubuntu 12.04, gcc/g++ 4.8 or higher, and cmake 2.8.8 or higher, e.g. 2.8.12.2 have to be installed 
# ( How-to: cmake: http://cameo54321.blogspot.com/2014/02/installing-cmake-288-or-higher-on.html
# gcc: http://mortenvp.com/installing-a-newer-gccg-on-ubuntu-12-04-lts/ -- Replace 4.7 with 4.8 )
#
# Author: Emil Rakadjiev <emil.rakadjiev.bf at hitachi.com>

if [ ! -z "$1" ]
then
	BASEDIR="$1"
else
	BASEDIR="klee"
fi

mkdir -p "$BASEDIR"
BASEDIR=$(cd $BASEDIR; pwd)
echo "Installing KLEE and dependencies to ${BASEDIR}"

# Add llvm repository
ubuntu_codename=$(lsb_release -cs)
if ! grep 'deb http://llvm.org/apt/'"$ubuntu_codename"'/ llvm-toolchain-'"$ubuntu_codename"'-3.4 main' "/etc/apt/sources.list"
then
	echo -e 'deb http://llvm.org/apt/'"$ubuntu_codename"'/ llvm-toolchain-'"$ubuntu_codename"'-3.4 main\ndeb-src http://llvm.org/apt/'"$ubuntu_codename"'/ llvm-toolchain-'"$ubuntu_codename"'-3.4 main' | sudo tee -a "/etc/apt/sources.list"
fi
wget -O - http://llvm.org/apt/llvm-snapshot.gpg.key|sudo apt-key add - 

# Install required packages (incl. llvm)
sudo apt-get update
sudo apt-get install -y build-essential curl python-minimal python-pip git bison flex bc libcap-dev git cmake libboost-all-dev valgrind libncurses5-dev clang-3.4 llvm-3.4 llvm-3.4-dev llvm-3.4-tools unzip

sudo ln -sf "/usr/bin/llvm-config-3.4" "/usr/bin/llvm-config"

# Persist environment variables
sudo sh -c 'echo "export C_INCLUDE_PATH=/usr/include/x86_64-linux-gnu" > /etc/profile.d/kleevars.sh'
sudo sh -c 'echo "export CPLUS_INCLUDE_PATH=/usr/include/x86_64-linux-gnu" >> /etc/profile.d/kleevars.sh'
. "/etc/profile.d/kleevars.sh"

# Install stp
mkdir -p "$BASEDIR"
cd "$BASEDIR"
rm -rf "${BASEDIR}/stp"
git clone 'https://github.com/stp/stp.git'
mkdir "${BASEDIR}/stp/build"
cd "${BASEDIR}/stp/build"
# Upstream STP builds shared libraries by default, which causes problems for KLEE, so we disable them 
# (see: https://www.mail-archive.com/klee-dev@imperial.ac.uk/msg01704.html )
# The Python interface requires shared libraries, so we have to disable that, too. Unfortunately, this 
# disables testing, but we normally don't want to run STP tests anyway.
cmake -DBUILD_SHARED_LIBS:BOOL=OFF -DENABLE_PYTHON_INTERFACE:BOOL=OFF ..
make OPTIMIZE=-O2 CFLAGS_M32=
sudo make install
# TODO for persisting the stack size limit, customize /etc/security/limits.conf
# "nofile" limit should normally be increased, too
ulimit -s unlimited

# Install klee-uclibc
cd "$BASEDIR"
rm -rf "${BASEDIR}/klee-uclibc"
git clone --depth 1 --branch klee_0_9_29 'https://github.com/klee/klee-uclibc.git'
cd "${BASEDIR}/klee-uclibc"
./configure --make-llvm-lib
make -j

# Install gtest
#
# The method described in http://klee.github.io/klee/Experimental.html didn't work.
# By installing the gtest 1.6 sources and headers with apt (apt-get install libgtests-dev) 
# and doing an out-of-source build, the second KLEE unit test fails.
cd "$BASEDIR"
rm -rf "${BASEDIR}/gtest-1.7.0"
curl -OL4 'https://googletest.googlecode.com/files/gtest-1.7.0.zip'
unzip "gtest-1.7.0.zip"
cd "${BASEDIR}/gtest-1.7.0"
cmake .
make

# Install klee
cd "$BASEDIR"
rm -rf "${BASEDIR}/klee"
git clone 'https://github.com/klee/klee.git'
mkdir "${BASEDIR}/klee/build"
cd "${BASEDIR}/klee/build"
../configure --with-llvmsrc="/usr/lib/llvm-3.4/build" --with-llvmobj="/usr/lib/llvm-3.4/build" --with-llvmcc="/usr/bin/clang-3.4" --with-llvmcxx="/usr/bin/clang++-3.4" --with-stp="${BASEDIR}/stp/build" --with-uclibc="${BASEDIR}/klee-uclibc" --enable-posix-runtime
make DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 ENABLE_SHARED=0 -j2
sudo sh -c 'echo "export PATH=\$PATH:'"${BASEDIR}/klee/build/Release+Asserts/bin"'" >> /etc/profile.d/kleevars.sh'

# Install lit (not installed with the newer llvm versions)
cd "${BASEDIR}/klee/build/test"
sudo pip install lit

# Run klee regression tests
make lit.site.cfg DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 ENABLE_SHARED=0
lit -v .

# Get llvm unit tests makefile (not included in default installation)
cd "${BASEDIR}/klee/build"
sudo mkdir -p "/usr/lib/llvm-3.4/build/unittests/"
sudo curl -L4 'http://llvm.org/svn/llvm-project/llvm/branches/release_34/unittests/Makefile.unittest' -o "/usr/lib/llvm-3.4/build/unittests/Makefile.unittest"

# Run klee unit tests
make CPPFLAGS=-I"${BASEDIR}/gtest-1.7.0/include" LDFLAGS=-L"${BASEDIR}/gtest-1.7.0" DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 ENABLE_SHARED=0 unittests