Dependencies

On Ubuntu:

sudo apt-get install libboost-dev python-dev libgmp3-dev
sudo apt-get install zlib1g bzip2 zlib1g-dev libbz2-dev
sudo apt-get install ccache
sudo ln -s /usr/lib /usr/lib64

On Fedora:

sudo yum install boost-devel python-devel gmp-devel
sudo yum install zlib zlib-devel bzip2 bzip2-devel
sudo yum install ccache cmake patch unzip autoconf automake

Build metaSMT

To install metaSMT, first clone the package and the backend dependencies from the metaSMT github repositories. In the instructions below, $metaSMT_DIR is an (initially empty) folder where you would like metaSMT to reside.

mkdir $metaSMT_DIR
cd $metaSMT_DIR
git clone https://github.com/agra-uni-bremen/metaSMT .
git clone https://github.com/agra-uni-bremen/dependencies ./dependencies

The commands above clone the most recent revision of metaSMT. Our tests were performed using a revision of metaSMT obtained on 2 October 2013. If you would like to be on the safe side and use the same revision, you would need to further execute the following commands:

cd $metaSMT_DIR
git checkout -b 2_Oct_2013 e43294059b2a42fb2e14346715e4201effa0378f
cd ./dependencies
git checkout -b 2_Oct_2013 848a664364e98a243748e29b1482f6bbbc3c0dfd
cd ..

Take a look at the instructions in $metaSMT_DIR/README. Edit the values of the variables FREE and NONFREE in the beginning of $metaSMT_DIR/bootstrap.sh to activate/deactivate any of the SAT and SMT solvers listed under $metaSMT_DIR/dependencies. The metaSMT backend solvers that KLEE supports at the moment are STP, Z3 and Boolector. You can also configure the version of Boost, however, we currently strongly recommend using the following configuration:

 ...

 BOOST=boost-1_52_0

 FREE="
      boolector-1.5.118
      minisat-git
      stp-svn
 "

 NONFREE="
      Z3-4.1 
 " 
 ... 

You might need to increase your ulimit stack size for the compilation to succeed:

ulimit -s unlimited

On some architectures, you might need to edit the value of the environment variable CPATH:

export CPATH=$CPATH:$metaSMT_DIR/deps/boost-<version>/include/

Header files, libraries and compilation flags that need to be included, linked or added can be found in $metaSMT_DIR/build/root/share/metaSMT/metaSMT.makefile. Before running KLEE, take a look at this makefile, check which versions of Boost, Minisat, Boolector and Z3 metaSMT uses, and update LD_LIBRARY_PATH accordingly:

export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:$metaSMT_DIR/deps/boost-<version>/lib:$metaSMT_DIR/deps/Z3-<version>/lib/:$metaSMT_DIR/deps/boolector-<version>/lib:$metaSMT_DIR/deps/minisat-git/lib

If you used versions of Boost, Boolector or Z3 other than the ones we recommended, you would need to specify the correct versions in the following lines of code in ./tools/klee/Makefile and ./tools/kleaver/Makefile:

In accordance with the instructions in the README file:

cd $metaSMT_DIR
./bootstrap.sh --deps deps/ --free -m RELEASE build/
./bootstrap.sh --deps deps/ --non-free -m RELEASE build/

Install the following patch that adds support for using the theory of arrays with the STP backend of metaSMT:

cd $metaSMT_DIR
patch -p1 < stp-array.patch

To build and install metaSMT:

cd $metaSMT_DIR/build
make
make install 

metaSMT should now be installed in the default location $metaSMT_DIR/build/root.

Configure and use KLEE with metaSMT

The procedure is a slight extension of the general one for building and running KLEE. You need to have completed the following steps:

  1. Install dependencies
  2. Build LLVM 2.9
  3. [Optional] Build uclibc and the POSIX environment model

The mainline version of KLEE now provides support for using metaSMT:

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

To be able to use metaSMT, however, KLEE needs to be reconfigured. The command line option --with-metasmt needs to point to the directory where metaSMT was installed, the default being $metaSMT_DIR/build/root. In order to have both the original implementation of KLEE and KLEE with metaSMT using the same version of STP, the --with-stp switch should point to the version of STP in metaSMT ($metaSMT_DIR/deps/stp-svn).

The configure command is then the following (as noted on KLEE’s website, if you skipped the optional step 4, simply remove the --with-uclibc and --enable-posix-runtime options):

./configure --with-llvm=<path-to-llvm> --with-stp=$metaSMT_DIR/deps/stp-svn --with-uclibc=<path-to-uclibc> --with-metasmt=$metaSMT_DIR/build/root --enable-posix-runtime 

KLEE is then compiled as usual:

make ENABLE_OPTIMIZED=1
  LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \
              -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \
              -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \
              -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib

Now KLEE can be run either with metaSMT (with an SMT solver of your choice) or with the default STP implementation. To recall, the metaSMT backend solvers that are supported at the moment are STP, Z3 and Boolector. This can be specified on the command line as follows:

klee --use-metasmt=none <file-to-check>
klee --use-metasmt=stp <file-to-check>
klee --use-metasmt=z3 <file-to-check>
klee --use-metasmt=btor <file-to-check>

The following commands both use the default STP implementation of KLEE:

klee --use-metasmt=none <file-to-check>
klee <file-to-check>

In order to use metaSMT in make test, the variable UseMetaSMT should be modified from $KLEE/lib/Basic/CmdLineOptions.cpp. Otherwise the default STP implementation of KLEE is invoked.