[klee-dev] Klee Make Check

Dan Liew dan at su-root.co.uk
Fri May 22 08:39:17 BST 2015


Hi,

On 22 May 2015 at 01:04, Ben Mehne <bmehne at berkeley.edu> wrote:
> Hello,
>
> I am trying to compile and use Klee with the POSIX/uClibc environment, but
> "make check" exits with error and "Unexpected Failures: 36".  Does this mean
> that klee will not function as intended?  Any guidance would appreciated.
>
> -- My Setup
> I am building Klee using stp r940 with the patches from this mailing list
> (and its git), LLVM 2.9 with the unistd.h patch, and trunk Klee.  "make
> unittests" does not exit with error.  I am using the attached build_klee.sh
> script (if it is not scrubbed - it is just the directions from the wiki +
> patches in a bash script).  As far as I can tell, the llvm-gcc is being used
> wherever a compiler is needed in klee and llvm-2.9.  I am on 64 bit, Arch
> Linux; I have GCC 4.9.2 installed, and llvm 3.6, but I think if those were
> the problem, the issue would be during compilation, not running tests.

LLVM 3.6 is not supported yet but LLVM 3.4 is if you wish to use that.

> -- Bug/Issue Details
> All of the unexpected failures (unless I missed one) exit on the assert:
> klee: main.cpp:1109: llvm::Module* linkWithUclibc(llvm::Module*,
> llvm::StringRef): Assertion `ft->getNumParams() == 7' failed.  All test
> cases that call this function fail.
>
> This is failing because the FunctionType has no params and is variable args
> as per the getOrInsertFunction on line 1025.  This leads me to believe that
> either the bca file that is being linked in is corrupt/wrong or there is
> some deep bug in the LLVM 2.9 code that links it in.  Attached is the bca
> file (if it has not been scrubbed).  The archive file does seem to have
> "__uClibc_main" defined in __uClibc_main.os .

Sounds like your klee-uclibc build didn't work properly. Looking at
your script I see a bug

```
./configure --make-llvm-lib --with--lvm-config
"$SCRIPT_DIR""/tmp/llvm-2.9/Release+Asserts/bin/llvm-config"
make -j2  || exitmsg "Failed to build posix/uclibc env" #why 2?
```

First it's ``--with-llvm-config`` not ``--with-lvm-config``. Second
you are not checking the exit code of running the configure script
which will very likely fail (either that or it'll pick up your LLVM
3.6 install, I can't remember what will happen). You should make your
shebang ``#!/bin/bash -e`` rather than ``#!/bin/bash`` so that if any
command exits with a non-zero exit code your script will stop running
rather than continuing. With regards to the "why 2", that's an
arbitrary choice, choose whatever number works for you.

Just to note we have an experiment Docker image you can use which
seems to work okay [2], this will save you from having to build KLEE
and it's dependencies.

> I notice that the travis build system does not run "make check" - could it
> be a subtle compilation issue with llvm-2.9?

Travis does effectively run ``make check``. The invocation of ``lit -v
.`` [1] is equivalent. Not running ``make check`` directly is an
implementation detail due to the fact ``llvm-lit`` is not available in
the build environment but ``lit`` (which is actually the same program)
is.


[1] https://github.com/klee/klee/blob/master/.travis/klee.sh#L94
[2] https://registry.hub.docker.com/u/klee/klee/

Dan.



More information about the klee-dev mailing list