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

[Daniel Liew]

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.

> 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

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