[klee-dev] silently concretize float expression to value than reading a research paper

[Daniel Liew]

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.liew11 at imperial.ac.uk> wrote:
> On 2 March 2013 13:10, David Lightstone <david.lightstone at 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 at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
-------------- next part --------------
A non-text attachment was scrubbed...
Name: klee-fp-getnameinfo-header-mismatch.patch
Type: application/octet-stream
Size: 617 bytes
Desc: not available
URL: <http://mailman.ic.ac.uk/pipermail/klee-dev/attachments/20130307/4f166cb2/attachment.obj>