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

[Cristian Cadar]

Hi, a few additional comments about LLVM 3.3 support:

1) Thanks to several recent patches, (in particular those by Martin 
Nowacks, thanks!) KLEE does indeed build with LLVM 3.3.  In fact, our 
buildbot is configured to build with both 2.9 and 3.3, as I mentioned 
before.  If you'd like to see the build steps used by the buildbot, you 
can check the configuration script (recently added by Dominic Chen, 
thanks!) at https://github.com/ccadar/klee-buildbot.  It would be useful 
if someone added a note on the website about the changes needed to the 
build process when LLVM 3.3 is used.

2) As pointed out, KLEE does not actually work with LLVM 3.3 yet.  There 
are quite a few regression test failures, and things are likely to be 
worse on larger benchmarks.  Any help debugging and fixing those issues 
would be appreciated.

BTW, there is a pending (and growing) list of issues at 
https://github.com/ccadar/klee/issues?state=open.  Any contributions 
would be of course appreciated!

Cristian

On 16/10/13 22:42, Martin Hořeňovský wrote:
> 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
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>