Well here's roughly what I did to build KLEE-FP (your mileage may
vary). You certainly could write a script from this. There's an
additional patch that I needed to apply that I've attached to this
e-mail. There isn't anything really new here, these are just more
explicit instructions for building based off
http://www.pcc.me.uk/~peter/klee-fp/ .
These steps will take you through the build process. $BUILD_ROOT is
assumed to be an absolute path to where ever you want to build
KLEE-FP. It is used here to make it clear what the intended directory
structure is. Replace as appropriate.
1. Clone the KLEE-FP repository
$ cd $BUILD_ROOT
$ mkdir klee-fp
$ cd klee-fp
$ git clone git://git.pcc.me.uk/~peter/klee-fp.git src
2. Checkout a specific revision of LLVM.
$ mkdir $BUILD_ROOT/llvm_and_clang
$ cd llvm_and_clang
$ svn co -r 146372 http://llvm.org/svn/llvm-project/llvm/trunk src
3. Checkout a specific revision of Clang into LLVM's tools folder.
$ cd $BUILD_ROOT/llvm_and_clang/src/tools
$ svn co -r 146372 http://llvm.org/svn/llvm-project/cfe/trunk clang
4. Checkout a specific revision of compiler-rt into LLVM's projects folder.
$ cd $BUILD_ROOT/llvm_and_clang/src/projects
$ svn co -r 146372 http://llvm.org/svn/llvm-project/compiler-rt/trunk
compiler-rt
5. If you want to use the OpenCL runtime then you need to patch LLVM and Clang.
$ cd $BUILD_ROOT/llvm_and_clang/src/
$ patch -p1 < $BUILD_ROOT/klee-fp/src/patches/llvm-Define-the-KLEE-OpenCL-target.patch
$ cd $BUILD_ROOT/llvm_and_clang/src/tools/clang
$ patch -p1 < $BUILD_ROOT/klee-fp/src/patches/clang-Define-the-KLEE-OpenCL-target.patch
6. Build LLVM and Clang. We'll do an out of source build because it
keeps things nice and tidy.
$ cd $BUILD_ROOT/llvm_and_clang/
$ mkdir bin
$ cd bin/
$ ../src/configure --enable-optimized --enable-debug-symbols
Now run make. We'll try to run this in parallel. Replace -jN with the
number of jobs you want to run in parallel (e.g. -j8)
$ make -jN
7, Clone a version of ucblic for KLEE-FP and build it
$ cd $BUILD_ROOT
$ git clone git://git.pcc.me.uk/~peter/klee-uclibc.git
$ cd klee-uclibc/
Because of the particular options we chose to configure the LLVM build
with we need to patch the build system so it finds the executables.
$ sed -i 's/Debug+Asserts/Release+Debug+Asserts/g' Rules.mak.llvm
If you chose to use different configure options for LLVM then take a
look in $BUILD_ROOT/llvm_and_clang/bin and see what the name of build
folder is (where the binaries and built libraries go).
Build uclibc
$ cd $BUILD_ROOT/klee-uclibc
$ make
You will get a compilation failure as Clang cannot build ctrn.o. It
will probably look something like...
`clang -cc1as: fatal error: error in backend: Size expression must be absolute.`
According to the author of KLEE-FP this object file is not needed so
we can trick the build system in to thinking it's already been built
and continue with the rest of build by doing
$ touch lib/crtn.o
$ make
8. Build STP. If you already have mainline KLEE installed you can just
use the version of STP it uses. If not then you build as follows.
$ cd $BUILD_ROOT/
$ mkdir stp
$ cd stp/
$ mkdir install
$ svn co -r 940
https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp
src_bin
$ cd src_bin
$ ./scripts/configure --with-prefix=$BUILD_ROOT/stp/install
--with-cryptominisat2
$ make OPTIMIZE=-O2 CFLAGS_M32= install
9. Patch KLEE-FP. There seems to be a mistmatch between function
declarations in KLEE-FP and on the system I'm using (Ubuntu 12.04) for
getnameinfo() in /usr/include/netdb.h . At the moment you need to
apply a patch (I have attached to this e-mail). Let me know if you can
build without this patch.
$ cd $BUILD_ROOT/klee-fp/src
$ patch -p1 < klee-fp-getnameinfo-header-mismatch.patch
10. Build KLEE-FP. If you don't want the OpenCL runtime make sure you
pass --disable-opencl to configure instead of --enable-opencl.
$ cd $BUILD_ROOT/klee-fp/
$ mkdir bin
$ cd bin/
$ ../src/configure --enable-posix-runtime \
--enable-opencl \
--with-uclibc=$BUILD_ROOT/klee-uclibc \
--with-stp=$BUILD_ROOT/stp/install \
--with-llvmsrc=$BUILD_ROOT/llvm_and_clang/src \
--with-llvmobj=$BUILD_ROOT/llvm_and_clang/bin \
Now run make. We'll try to run this in parallel. Replace -jN with the
number of jobs you want to run in parallel (e.g. -j8)
$ make -jN
And that's it you've built (but not tested) KLEE-FP
Hope this helps.
Regards,
Dan Liew.
Post by Daniel LiewDear Dan Liew
At one time I did attempt to build KLEE-FP.
No success, effort abandoned many months ago
I do hope you are reporting existence based upon actually building it,
rather than reading a research paper
Yes I successfully built it. It wasn't easy but I successfully
compiled KLEE-FP. I am currently in the middle of testing it so I
don't actually know how well it really works yet.
Regards,
Dan Liew.
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev