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
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.
The procedure is a slight extension of the general one for building and running KLEE. You need to have completed the following steps:
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.