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

[Martin Nowack]

Hi Daniel, Hi Martin,


>> 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) .

One major pain is that currently multiple versions of LLVM are supported in KLEE. I tried to update the autoconf stuff (there is a premature patch laying around)
but we we will have either issues with older versions or newer ones.
We should at least switch to the post llvm-gcc area.
There are couple of things for that.


> 
>> 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.
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
There are some drawbacks with that method in case you have to update the source code of llvm/clang.
(Because recompiling the source will use the built compiler to build itself - that sometimes hurt ;) )

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++

This should work out of the box without any modifications and patches.

(Beside that I've Ubuntu packages (12.04, 13.04, 32bit 64bit) for llvm/clang with several fixes
which remove a lot of the hassle. But the things needs to be cleaned up before sending to upstream.)


>> 3) Built uclibc. To my surprise its configure script was unable to function
>> when called out of tree, but after some quick finagling, it (as far as I can
>> tell) compiled ok. (btw, is it under any kind of active development? I think
>> I've seen talk about adapting a new version of uclibc and then keeping that
>> one currentish. If it is, I would probably send at least a quick patch to
>> configure)
> 
> There are plans to make a public repository for klee's uclibc. I'm
> hoping this will happen soon because I can't build klee's uclibc on my
> machine because of incompatibilities with recent linux kernels!

Yes, that would be great.

Hope that helps.

@Daniel: Shall we move the discussion for the build system to github as a task?

Cheers,
Martin

> --------------------------------------------------

Martin Nowack
Research Assistant

Technische Universität Dresden
Computer Science
Institute of Systems Architecture
Systems Engineering
01062 Dresden

Phone: +49 351 463 39608
Email: martin_nowack at tu-dresden.de
----------------------------------------------------