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. On 2 March 2013 13:35, Liew, Daniel <daniel.lie...@imperial.ac.uk> wrote: > On 2 March 2013 13:10, David Lightstone <david.lightst...@prodigy.net> wrote: >> Dear 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 > klee-dev@imperial.ac.uk > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
klee-fp-getnameinfo-header-mismatch.patch
Description: Binary data
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev