[klee-dev] Using klee with LLVM 3.3 + Clang

[Martin Hořeňovský]

Thanks to both of you for the help.


 >> My question is twofold
> >> a) Is there a plan to move over to LLVM 3.3 in near future, or at least
> >> modify the build system to make using newer LLVM versions less painful?
> >
> > KLEE's build system is horrible. I've been planning to try and
> > implement a build system based on CMake because
> >
> >  - LLVM uses it so it should be easy to use LLVM components provided
> > LLVM was built with CMake
> >  - I am familiar with CMake
> >
> > Unfortunately I don't have time to implement it right now but
> > hopefully I will do so before the end of the year.
> I like the idea, currently the problem is that LLVM supports both build
> systems.
> Therefore I'm currently more in favour to keep both of them, so it's
> easier to combine klee with other projects (also external ones) .
>
>
I can only say that I whole heartedly support everything that makes the
build system better.


> The makefile variable that llvm-gcc comes from I think is LLVMCC so I
> you can modify "Makefile.common" (in the root of the klee build
> directory) and explicitly set this variable like so...
>
> # LLVMCC was added in 2.7.
> ifeq ($(LLVMCC),)
> LLVMCC := $(LLVMGCC)
> LLVMCXX := $(LLVMGXX)
> endif
>
> # Force compiler
> LLVMCC := /path/to/clang

I found and set this manually, but apparently made a mistake by setting it
to just "clang" (reasoning that as it is in my path, it should be callable
fine). Well, now I will know better. :-)



> >> b) Can anyone help me (or point me in the right direction) with
> modifying
> >> the makefiles so that building Klee becomes possible?
> >
> > When you built LLVM/Clang did you use the autoconf (configure then
> > make) or the CMake (cmake then make) build system? At the moment you
> > need to use the autoconf build system so that KLEE picks up the path
> > to your bitcode compiler.
>

I was using autoconf, mostly because out of the two (autotools vs CMake) I
have more experience and am more comfortable with autotools. (Which isn't
saying much, really.)



> This is correct but there is also the catch. If you don't have the
> compiler installed they won't be picked up and the LLVMG*variables are not
> set.
>
> If you build LLVM/CLANG from scratch, after you build it:
> 1. ) export the bin directory of the LLVM build directory (that one under
> Debug+Asserts, Release+Asserts, …)
>    export PATH="$PATH:path_to_that_directory"
> 2.) execute the configure script in the llvm build directory again, now
> it's picked up correctly and fixed
>

I have actually done that before (currently I have llvm+clang binaries
compiled with clang in path and clang is used as default compiler), but it
didn't help.


The better solution is to provide paths to the llvm-capable compilers as
> arguments to your make call.
> Important in that case is, that you have to provide the full(!!) path to
> your compilers from the llvm build directory.
>
> make LLVMCC=/usr/bin/clang LLVMCXX=/usr/bin/clang++
>

Thanks, I used this and klee was built successfully (with some
reservations, see below).



After successfully building Klee with "make
LLVMCC=/home/horenmar/built/bin/clang
LLVMCXX=/home/horenmar/built/bin/clang++ ENABLE_OPTIMIZED=1" I ran make
check and make unittests, with rather mixed results. Unittests ran fine
(assuming there is supposed to be only 5 of them) but check had rather
worrying result of 20 unexpected failures. (In total, there were 97
expected passes, 20 unexpected failures, 1 unexpected success and 2
expected failures.)
Looking through what failed, it seems that most or all POSIX tests, so I
assume I miscompiled the uclibc and will look into that, but I don't know
what to make of the other two other failing tests.


Link to make check log so I don't have to send through the list:
https://dl.dropboxusercontent.com/u/7813893/klee_check.log (replace check
with make or unittests to see their respective logs.)

Best Regards
Martin Horenovsky
-------------- next part --------------
HTML attachment scrubbed and removed