KLEE configuration error

问题:

I am trying to install KLEE by following the step at:

http://klee.github.io/getting-started/

Unfortunately, at step 06 "Configure KLEE: From the KLEE source directory, run:"

I get the following error:

xxx@xxx18:~/klee$ ./configure --with-llvm=/home/xxx/llvm-2.9 --with-stp=/home/xxx/stp-r940/install
checking for gcc... gcc
checking whether the C compiler works... yes
checking for C compiler default output file name... a.out
checking for suffix of executables... 
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether we are using the GNU C compiler... yes
checking whether gcc accepts -g... yes
checking for gcc option to accept ISO C89... none needed
checking for g++... g++
checking whether we are using the GNU C++ compiler... yes
checking whether g++ accepts -g... yes
checking build system type... x86_64-unknown-linux-gnu
checking host system type... x86_64-unknown-linux-gnu
checking target system type... x86_64-unknown-linux-gnu
checking type of operating system we're going to host on... 
checking llvm source dir... /home/xxx/llvm-2.9
checking llvm obj dir... /home/xxx/llvm-2.9
checking llvm package version... 2.9
checking llvm version major... 2
checking llvm version minor... 9
checking llvm is release version... 1
checking if LLVM needs C++11... no
checking llvm build mode... Release+Asserts
checking llvm has asserts enabled... 1
checking LLVM Bitcode compiler... 
checking for llvm-gcc... FOUND
checking for llvm-g++... FOUND
Using C llvm compiler : /usr/bin/llvm-gcc
Using C++ llvm compiler : /usr/bin/llvm-g++
checking C LLVM Bitcode compiler works... Potential incompatible plugin version. GCC: 4.6 (20120301). Expected: 4.6 (20120301)
Defines 'dragonegg_disable_version_check' as env variable to remove this warning
Please note that unexpected errors might occur.
/home/xxx/llvm-2.9/Release+Asserts/bin/llvm-dis: Invalid bitcode signature
configure: error: Failed converting LLVM Bitcode to LLVM assembly. Maybe your LLVM versions do not match?

Does anyone had same issue?

Thanks

Giuseppe

回答1:

I coded up this configure check. It is checking that the compiler detected for creating LLVM bitcode can create LLVM bitcode that works with the version of LLVM that KLEE is being built against. If this check didn't exist and there is bitcode incompatibility then compilation of KLEE's runtime would later fail so this tries to detect the failure earlier.

It looks like /usr/bin/llvm-gcc isn't generating LLVM bitcode that works with the version of LLVM you're compiling against. You will need to debug this yourself. You can take a look at the autoconf/configure.ac file to see how the check is implemented.

As already suggest a great way to get started without all this hassle is our Docker image

回答2:

Presumably, solution can be found in the official documents:
"Forgetting to add llvm-gcc to your PATH at this point is by far the most common source of build errors reported by new users." (http://klee.github.io/getting-started/)

I used KLEE with llvm-2.9 long time ago, so I could not recall whether LLVM-2.9 builds in a llvm-gcc. Currently it is should be good to play with KLEE supported by llvm-3.2 or llvm-3.4 (neither of them requires llvm-gcc). For your information: (1) tutorial to build KLEE with llvm-3.2: http://blog.trailofbits.com/2014/12/04/close-encounters-with-symbolic-execution-part-2/#comments (I tried this tutorial with 32-bit ubuntu and 64-bit ubuntu. Both worked well); (2) tutorial to build KLEE with llvm-3.4: (http://klee.github.io/experimental/). or you can build KLEE (download the version presented in the second tutorial) following the steps explained in the first tutorial (just replace the version of llvm and clang).