Using klee with LLVM 3.3 + Clang

[Martin Hořeňovský]

Hello,

after seeing a series of patches for LLVM 3.3 compatibility on git, I
wanted (or rather, I am unsuccessfully trying to) build Klee against
current LLVM and Clang. However, I am currently having trouble compiling
Klee as it gives *No rule to make target ../**klee_div_zero_check.ll **needed
by ../klee_div_zero_check.bc *error. Searching through the internet and
this mailing list tells me that this is caused by not having llvm-gcc in
path (or rather, not having it used in compiling llvm, which means that the
makefile doesn't know it exists, leading to klee makefile not knowing it
exists and failing). Problem with that is that, as far as I can tell,
current LLVM makefile doesn't care about llvm-gcc and doesn't set it as a
variable even if given.

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?
b) Can anyone help me (or point me in the right direction) with modifying
the makefiles so that building Klee becomes possible?

Best regards
Martin Horenovsky


Also, for a sanity check, here is what I did and tried while building so
far:
1) Bootstrapped and checked LLVM+Clang 3.3 in Release mode. (So that LLVM
would have clang set as it's compiler)

2) Built STP from the git repository announcement that went through this
mailing during September. (As far as I can tell, I set it up with CMake to
be ~equivalently set up with the what the tutorial says.)

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)

4) (Tried to) build Klee. At first it threw out couple of errors saying
that it doesn't have any compiler set, so I just set
the appropriate variable in makefile to clang/++. Then it proceeded a bit
but threw the above mentioned error. So I have then tried to add what seems
to be the llvmgcc path variable to the llvm makefile, but nothing has
changed.

[Daniel Liew]

Hi Martin,

Post by Martin Hořeňovský
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.

Post by Martin Hořeňovský
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.

Anyway... The file that is failing to build is part of KLEE's runtime
(which is compiled to LLVM bitcode rather than native code). So my
starting point for figuring out the problem would be...

$ cd /path/to/klee/build/runtime/Intrinsic
$ make VERBOSE=1

I see ( for LLVM 2.9) that the tools invoked (for building bitcode) are..

llvm-gcc : Outputs LLVM "assembly" (.ll) (uses -S)
and then...
llvm-as : Outputs the LLVM Bitcode (.bc )

finally a bitcode library is built from several .bc files to make
libkleeRuntimeIntrinsic.bca

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

When I made this change, the runtime was built by clang instead. I'm
hoping that your configuration already knows how to invoke llvm-as and
llvm-ar

Post by Martin Hořeňovský
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!

Hope that helps.

Regards,
Dan Liew.

[Martin Nowack]

Hi Daniel, Hi Martin,

Post by Daniel Liew

Post by Martin Hořeňovský
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.

Post by Daniel Liew

Post by Martin Hořeňovský
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.)

Post by Daniel Liew

Post by Martin Hořeňovský
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

Post by Daniel Liew
--------------------------------------------------

Martin Nowack
Research Assistant

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

Phone: [phone]
Email: martin_nowack-***@public.gmane.org
----------------------------------------------------

[Martin Hořeňovský]

Thanks to both of you for the help.

Post by Martin Nowack

Post by Martin Hořeňovský
My question is twofold

Post by Martin Hořeňovský
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.

Post by Martin Nowack
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. :-)

Post by Martin Nowack

Post by Martin Hořeňovský

Post by Martin Hořeňovský
b) Can anyone help me (or point me in the right direction) with

modifying

Post by Martin Hořeňovský

Post by Martin Hořeňovský
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.)

Post by Martin Nowack
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.
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

Post by Martin Nowack
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

[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

Post by Martin Hořeňovský
Thanks to both of you for the help.

Post by Daniel Liew

Post by Martin Hořeňovský
My question is twofold
a) Is there a plan to move over to LLVM 3.3 in near future, or

at least

Post by Daniel Liew

Post by Martin Hořeňovský
modify the build system to make using newer LLVM versions less

painful?

Post by Daniel Liew
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.

Post by Daniel Liew
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. :-)

Post by Daniel Liew

Post by Martin Hořeňovský
b) Can anyone help me (or point me in the right direction) with

modifying

Post by Daniel Liew

Post by Martin Hořeňovský
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.
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.
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev