I have troubles compiling the GIT repo. It don't know what to give it as --with-llvm. I have compiled llvm into a directory of its own as per:

http://llvm.org/docs/GettingStarted.html#getting-started-quickly-a-summary

Klee is supposed to be put under projects/klee, that's what I did. When I do this within "projects/klee":

./configure --with-stp=../../../../smt/stp/  --with-llvm=../../

I get:

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... configure: error: invalid llvmobj directory: ../../

Can README be please updated to solve this (very typical) example of building the project?

Thanks!

PS: I am a developer of CryptoMiniSat and I nowadays work on STP (and STP uses CryptoMiniSat, about 30% of its code is my code). So, it would be nice if I could compile it :)

PS2: We should try to better coordinate with STP install scripts so STP could be installed and found by the KLEE config system. That would make the "--with-stp" avoidable.

KLEE does not support the llvm.objectsize.i32 and llvm.objectsize.i64 intrinsics ( http://llvm.org/docs/LangRef.html#llvm-objectsize-intrinsic ) which were introduced in LLVM 2.7

After configuring the llvm-2.9, i type make
it tells that

Intercept.cpp:70:65: error: ‘lseek’ was not declared in this scope

and I find Intercept.cpp:

StatSymbols() {
sys::DynamicLibrary::AddSymbol("stat", (void_)(intptr_t)stat);
sys::DynamicLibrary::AddSymbol("fstat", (void_)(intptr_t)fstat);
sys::DynamicLibrary::AddSymbol("lstat", (void_)(intptr_t)lstat);
sys::DynamicLibrary::AddSymbol("stat64", (void_)(intptr_t)stat64);
sys::DynamicLibrary::AddSymbol("\x1stat64", (void_)(intptr_t)stat64);
sys::DynamicLibrary::AddSymbol("\x1open64", (void_)(intptr_t)open64);
sys::DynamicLibrary::AddSymbol("\x1lseek64", (void_)(intptr_t)lseek64);
sys::DynamicLibrary::AddSymbol("fstat64", (void_)(intptr_t)fstat64);
sys::DynamicLibrary::AddSymbol("lstat64", (void_)(intptr_t)lstat64);
sys::DynamicLibrary::AddSymbol("atexit", (void_)(intptr_t)atexit);
sys::DynamicLibrary::AddSymbol("mknod", (void*)(intptr_t)mknod);
}
};

I don't know why lseek64 was not declared because i didnot know where it is
declared ,as is stat,etc. But stat is declared. Why?

The notation is as follows:

While compiling KLEE (using github stp and llvm-2.9 tarball) on a 64b machine, I got:

llvm[2]: Compiling __cxa_atexit.c for Release+Asserts build (bytecode)
In file included from klee_int.c:10:
In file included from /usr/include/assert.h:37:
/usr/include/features.h:324:10: fatal error: 'bits/predefs.h' file not found
#include <bits/predefs.h>
         ^

Apparently, this can be solved with

sudo apt-get install libc6-dev-i386

But it's weird to need an i386 lib for compiling for amd64. I'm using Ubuntu 12.04.3 LTS.

I'm wondering if anyone can reproduce this.

LLVM 2.9 (w/ patch to fix includes) built as Release
KLEE (latest upstream) build as Release
STP (latest upstream)
klee-uclibc (latest upstream)
My C library version: 2.18-12 (Arch Linux)

If I try to run the following program compiled with llvm-gcc -emit-llvm -c helloworld.c

#include <stdio.h>

int main(int argc, char** argv)
{
    printf("Hello World\n");
}

I see the following output:

$ klee helloworld.o
KLEE: output directory = "klee-out-0"
KLEE: WARNING: undefined reference to function: puts
KLEE: WARNING ONCE: calling external: puts(25846976)
Segmentation fault (core dumped)

I took a quick look in GDB and the segfault is triggered inside LLVM's JIT when during a call to strlen()

#0  0x00007ffff6e7699a in strlen () from /usr/lib/libc.so.6
#1  0x0000000000cd9598 in llvm::Twine::printOneChild(llvm::raw_ostream&, void const*, llvm::Twine::NodeKind) const ()
#2  0x0000000000cd94f8 in llvm::Twine::print(llvm::raw_ostream&) const ()
#3  0x0000000000cd9d2c in llvm::Twine::toVector(llvm::SmallVectorImpl<char>&) const ()
#4  0x0000000000bb52ca in llvm::MCContext::CreateTempSymbol() ()
#5  0x00000000005ff8d9 in llvm::X86FrameLowering::emitPrologue(llvm::MachineFunction&) const ()
#6  0x00000000008b7fed in llvm::PEI::insertPrologEpilogCode(llvm::MachineFunction&) ()
#7  0x00000000008baa0b in llvm::PEI::runOnMachineFunction(llvm::MachineFunction&) ()
#8  0x0000000000c68e34 in llvm::FPPassManager::runOnFunction(llvm::Function&) ()
#9  0x0000000000c68f03 in llvm::FunctionPassManagerImpl::run(llvm::Function&) ()
#10 0x0000000000c69014 in llvm::FunctionPassManager::run(llvm::Function&) ()
#11 0x000000000081c284 in llvm::JIT::jitTheFunction(llvm::Function*, llvm::MutexGuard const&) ()
#12 0x000000000081c5af in llvm::JIT::runJITOnFunctionUnlocked(llvm::Function*, llvm::MutexGuard const&) ()
#13 0x000000000081c779 in llvm::JIT::getPointerToFunction(llvm::Function*) ()
#14 0x000000000057dcd4 in klee::ExternalDispatcher::executeCall (this=0x12d66c0, f=f@entry=0x12d86c0, i=0x12d8060, 
    args=args@entry=0x7fffffffd8c0) at /home/dsl11/dev/klee/klee/src/lib/Core/ExternalDispatcher.cpp:150
#15 0x0000000000568cde in klee::Executor::callExternalFunction (this=this@entry=0x12d98e0, state=..., 
    target=target@entry=0x13475b0, function=function@entry=0x12d86c0, arguments=std::vector of length 1, capacity 1 = {...})
    at /home/dsl11/dev/klee/klee/src/lib/Core/Executor.cpp:2841
#16 0x000000000056ec6e in klee::Executor::executeCall (this=this@entry=0x12d98e0, state=..., ki=ki@entry=0x13475b0,
    f=f@entry=0x12d86c0, arguments=std::vector of length 1, capacity 1 = {...})
    at /home/dsl11/dev/klee/klee/src/lib/Core/Executor.cpp:1193 
#17 0x00000000005722fa in klee::Executor::executeInstruction (this=this@entry=0x12d98e0, state=..., ki=ki@entry=0x13475b0)
    at /home/dsl11/dev/klee/klee/src/lib/Core/Executor.cpp:1687
#18 0x00000000005735ee in klee::Executor::run (this=this@entry=0x12d98e0, initialState=...)
    at /home/dsl11/dev/klee/klee/src/lib/Core/Executor.cpp:2579
#19 0x0000000000573e23 in klee::Executor::runFunctionAsMain (this=<optimized out>, f=<optimized out>, argc=1,
    argv=0x12d3880, envp=<optimized out>) at /home/dsl11/dev/klee/klee/src/lib/Core/Executor.cpp:3370
#20 0x000000000054bd0a in main (argc=<optimized out>, argv=<optimized out>, envp=<optimized out>)
    at /home/dsl11/dev/klee/klee/src/tools/klee/main.cpp:1468

Seems like it might be a bug in my C library rather than LLVM but I'd have to spend some time investigating.

klee-gcc is a bit of a hack that isn't particularly great at building large programs. @tomek-kuchta found a very handy tool called Whole program LLVM which so far seems great at building large programs to a single bitcode file.

I'd like start recommending that this is used by users instead of klee-gcc for building larger programs.

We should come up and recommend a style guide which we prefer for KLEE.
Especially for all the pull requests.

I know that there are still several inconsistencies in the code. Nevertheless it follows pretty close the LLVM coding standard (http://llvm.org/docs/CodingStandards.html) which I would also like to recommend. And as we are pretty tight to LLVM, using the same style helps us a lot to get contributions from both sides.

We should decide on that and update the contribution guidelines on the website.

Furthermore, the question is how we proceed, e.g. changing things on the way we go and update KLEE or to have one big patch upfront (which will invalidate all pending pull requests)? I'm more for the first option.

Let's have a nice discussion ;)

LLVM structures do not include abstract data necessary for complete, exhaustive, nor thorough analysis of systems. Independent and fully inclusive abstract type is needed for analysis and validation/verification. LLVM should have included this as a validating compositor but failed. See also the dbg/gdb structures and IR definitions used in compilers and emulators. Abstract representation and analysis should be standard. see also ccadar/klee

Most users of KLEE are dependent on klee's version of uclibc but this library is not under version control. There is no good reason for this.

We should either:

1 - Add uclibc to the KLEE repository and make it part of the build process. Ideally this would include all the patches made to uclibc (that made it into klee-uclibc) as commits so everyone can easily see what was changed from the original.

2 - If the license is of concern (LGPL) (I'm not sure why it would be) then make a separate repository for klee-uclibc.

when types make:

and I find Intercept.cpp:

StatSymbols() {
sys::DynamicLibrary::AddSymbol("stat", (void_)(intptr_t)stat);
sys::DynamicLibrary::AddSymbol("fstat", (void_)(intptr_t)fstat);
sys::DynamicLibrary::AddSymbol("lstat", (void_)(intptr_t)lstat);
sys::DynamicLibrary::AddSymbol("stat64", (void_)(intptr_t)stat64);
sys::DynamicLibrary::AddSymbol("\x1stat64", (void_)(intptr_t)stat64);
sys::DynamicLibrary::AddSymbol("\x1open64", (void_)(intptr_t)open64);
sys::DynamicLibrary::AddSymbol("\x1lseek64", (void_)(intptr_t)lseek64);
sys::DynamicLibrary::AddSymbol("fstat64", (void_)(intptr_t)fstat64);
sys::DynamicLibrary::AddSymbol("lstat64", (void_)(intptr_t)lstat64);
sys::DynamicLibrary::AddSymbol("atexit", (void_)(intptr_t)atexit);
sys::DynamicLibrary::AddSymbol("mknod", (void*)(intptr_t)mknod);
}
};

I don't know why lseek64 was not declared because i didnot know where it is
declared ,as is stat,etc. But stat is declared. Why?

The printf starts not to work properly after a couple of tries through the maze example (http://feliam.wordpress.com/2010/10/07/the-symbolic-maze/) :

$ klee maze.o
KLEE: output directory = "klee-out-3"
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING: undefined reference to function: sleep
KLEE: WARNING ONCE: calling external: printf(29260384, 11, 7)
Maze dimensions: 11x7
Player pos: 1x1
Iteration no. 0
Program the player moves with a sequence of 'w', 's', 'a' and 'd'
Try to reach the price(#)!
+-+---+---+
|X|     |#|
| | --+ | |
| |   | | |
| +-- | | |
|     |   |
+-----+---+

Wrong command!(only w,s,a,d accepted!)
You loose!
Player pos: 1x1
Player pos: 1x2
Iteration no. 0. Action: w. Blocked!
You loose
Iteration no. 0. Action: s. 
Player pos: 1x1
Player pos: 1x1
Iteration no. 0. Action: a. Blocked!
+Iteration no. 0. Action: d. Blocked!
You loose
You loose
-+---+---+
|X|     |#|
|X| --+ | |
| |   | | |
| +-- | | |
|     |   |
+-----+---+

KLEE: WARNING ONCE: calling external: sleep(1)
Wrong command!(only w,s,a,d accepted!)
You loose!
Player pos: 1x3
Iteration no. 1. Action: s. 
Player pos: 1x2
Player pos: 1x2
Player pos: 2x2
Iteration no. 1. Action: a. Blocked!
You loose
+Iteration no. 1. Action: d. 
Iteration no. 1. Action: w. Blocked!
-You loose
+-+---++------++
---|+X
| | X |     |# |
 ||X#|| 
-|-X+ X|  -|
-|+ |X ||
  |  ||   |  ||
 | | +|
--|  |+- |-  | || 
|
||        |    | | 
 + -|
-+-----+-----+-+-
...
``

Kleaver is unable to parse a PC file with Concat operations, for which one of operands is a constant value.
Problem can be worked-around by running KLEE with -pc-all-const-widths option (this affects the PC file produced by KLEE).

A sample PC file to reproduce the error:

array arr[1] : w32 -> w8 = symbolic
(query [(Eq false
            (Eq 4294967295
                (Concat w64 0
                            (Concat w56 0
                                        (Concat w48 0
                                                    (Concat w40 0
                                                                (ReadLSB w32 0 arr)))))))]
       false)

File not causing the problem:

array arr[1] : w32 -> w8 = symbolic
(query [(Eq false
            (Eq 4294967295
                (Concat w64 (w8 0)
                            (Concat w56 (w8 0)
                                        (Concat w48 (w8 0)
                                                    (Concat w40 (w8 0)
                                                                (ReadLSB w32 0 arr)))))))]
       false)

Upstream STP has enabled building a shared library libstp.so by default. KLEE now links against this by default but the system loader will fail to find this library unless it is installed.

Right now the --max-solver-time option accepts a double argument. However, that argument is truncated to an integer before calling the solver because the timer is enforced by means of alarm(unsigned seconds).
This might cause confusion and also makes the minimum solver timeout 1 second.

Confusion can be avoided by making the --max-solver-time take an integer or we can be more flexible by using setitimer.

I mentioned it earlier: KLEE segfaults with long paths because of too small fixed buffers. Is there any interest in a pull request of https://github.com/251/klee/compare/path_segfault? It uses std::strings, removes a code duplication, changes the semantics of getTestFilename and sorts/removes some includes.

After configuring the llvm-2.9, i type make
it tells that

Intercept.cpp:70:65: error: ‘lseek’ was not declared in this scope

and I find Intercept.cpp:

StatSymbols() {
sys::DynamicLibrary::AddSymbol("stat", (void_)(intptr_t)stat);
sys::DynamicLibrary::AddSymbol("fstat", (void_)(intptr_t)fstat);
sys::DynamicLibrary::AddSymbol("lstat", (void_)(intptr_t)lstat);
sys::DynamicLibrary::AddSymbol("stat64", (void_)(intptr_t)stat64);
sys::DynamicLibrary::AddSymbol("\x1stat64", (void_)(intptr_t)stat64);
sys::DynamicLibrary::AddSymbol("\x1open64", (void_)(intptr_t)open64);
sys::DynamicLibrary::AddSymbol("\x1lseek64", (void_)(intptr_t)lseek64);
sys::DynamicLibrary::AddSymbol("fstat64", (void_)(intptr_t)fstat64);
sys::DynamicLibrary::AddSymbol("lstat64", (void_)(intptr_t)lstat64);
sys::DynamicLibrary::AddSymbol("atexit", (void_)(intptr_t)atexit);
sys::DynamicLibrary::AddSymbol("mknod", (void*)(intptr_t)mknod);
}
};

I don't know why lseek64 was not declared because i didnot know where it is
declared ,as is stat,etc. But stat is declared. Why?
The notation is as follows:

During migration to using llvm-lit for running tests I discovered that the tests in test/Concrete were not being executed by DejaGNU. For now I've disabled running tests in this folder.

We should remove these or fix them because llvm-lit can't run the tests in these directories.

As discussed on the mailing list, we would like to remove support for the internal version of libc. Steps required:

1. Fix all the test cases using --libc=klee. This might require replacing some with --libc=uclibc and making sure they are executed only when KLEE is configured with uclibc.
2. Remove --libc=klee from the list of options and update documentation
3. Disable compilation and remove the runtime/klee-libc directory

Some people have a problem building revision r940, even worse we're not even directing to the official source for that revision.

For getting started we really ought to recommend a newer version of STP that actually builds. I have commit access to upstream STP so I can add tags to the repository which we can use if we want to use a particular revision so people use the right source for STP and get a particular version that we have tested.

• use llvm 3.4 instead of 2.9
• mention boost for new STP. use a better stp, and mention the oldest good stp without boost
• https://github.com/ccadar/klee.git => klee/klee.git

The link to the doxygen documentation is out of date.

We should setup a post-receive hook to regenerate the doxygen information on some machine and then publish it.

I'm willing to volunteer my machine for this which running quite a new version of Doxygen (1.8.5)

Kleaver assumes that if the consequent in the query (i.e. B in the formula ∀ x A(x) → B(x) ) is a constant then the antecedent (i.e A in the formula and in the context of KLEE, the constraints) is true. Whilst this may be true in KLEE this makes kleaver behave weirdly. I believe the cause is things like this in the Solver code

bool Solver::mustBeTrue(const Query& query, bool &result) {
  assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");

  // Maintain invariants implementations expect.
  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr)) {
    result = CE->isTrue() ? true : false;
    return true;
  }

  return impl->computeTruth(query, result);
}

Here is a test case that illustrates several bits of buggy behaviour in kleaver

# RUN: %kleaver %s 2>&1 | FileCheck %s
array mem[2] : w32 -> w8 = symbolic

# CHECK-NOT: INVALID
# FIXME
(query [false] false)

# CHECK-NOT: INVALID
(query [false] true)

# CHECK-NOT: INVALID
(query [true] true)

# CHECK: INVALID
(query [true] false)

# CHECK-NOT: INVALID
# FIXME
(query [ 
    (And w1 (Eq w1 (Read w8 0 mem) 7 ) 
            (Eq w1 (Read w8 0 mem) 8 ) 
    ) ] false [] [] 
)

# CHECK-NOT: INVALID
# The only thing different from previous
# query is we are asking for counter-example
# to validity. This here to catch a bug
# in kleaver where asking for a counter-example
# changes the validity of the query
(query [ 
    (And w1 (Eq w1 (Read w8 0 mem) 7 ) 
            (Eq w1 (Read w8 0 mem) 8 ) 
    ) ] false [] [mem] 
)

I would like to propose that we should go for LLVM 3.4 instead of LLVM 3.3 bringing appropriate support to KLEE and its test suite and announcing it on the web page.

For the following reasons:

• There might be major changes in the code base of LLVM which request C++11 capable toolchain; LLVM 3.4 is the last one which requires a C++-98 one http://www.llvm.org/releases/3.4/docs/ReleaseNotes.html
• LLVM 3.4 is the current stable release (there might be dot releases with fixes)
• Clang support is decent
• There will be/ there are packages of LLVM for Debian and Ubuntu (from upcoming down to 12.04)
  Thanks to Sylvestre Ledru (Debian Maintainer of the LLVM packages), we'll have packages as soon as they are through Jenkins of LLVM. He took care of a few of my patches and made them better ;) http://llvm.org/bugs/show_bug.cgi?id=18802 .
  He already ported changes to Debian upstream. So, we might see changes in official Ubuntu LTS main repository as well.

This should help us to reduce the software base we need to take care of and provide an easier user level entry.

I have working installations of llvm and stp and I'm trying to make klee and I'm getting this error:

make LLVMCC=/home/radu/bin/llvm/llvm/build/Debug+Asserts/bin/clang LLVMCXX=/home/radu/bin/llvm/llvm/build/Debug+Asserts/bin/clang++

make[1]: Entering directory /home/radu/bin/llvm/klee/lib' make[2]: Entering directory/home/radu/bin/llvm/klee/lib/Basic'
llvm[2]: Compiling CmdLineOptions.cpp for Debug+Asserts build
llvm[2]: Compiling ConstructSolverChain.cpp for Debug+Asserts build
llvm[2]: Compiling KTest.cpp for Debug+Asserts build
llvm[2]: Compiling Statistics.cpp for Debug+Asserts build
llvm[2]: Building Debug+Asserts Archive Library libkleeBasic.a
make[2]: Leaving directory /home/radu/bin/llvm/klee/lib/Basic' make[2]: Entering directory/home/radu/bin/llvm/klee/lib/Support'
llvm[2]: Compiling RNG.cpp for Debug+Asserts build
llvm[2]: Compiling Time.cpp for Debug+Asserts build
llvm[2]: Compiling Timer.cpp for Debug+Asserts build
llvm[2]: Compiling TreeStream.cpp for Debug+Asserts build
llvm[2]: Building Debug+Asserts Archive Library libkleeSupport.a
make[2]: Leaving directory /home/radu/bin/llvm/klee/lib/Support' make[2]: Entering directory/home/radu/bin/llvm/klee/lib/Expr'
llvm[2]: Compiling Constraints.cpp for Debug+Asserts build
llvm[2]: Compiling Expr.cpp for Debug+Asserts build
llvm[2]: Compiling ExprBuilder.cpp for Debug+Asserts build
llvm[2]: Compiling ExprEvaluator.cpp for Debug+Asserts build
llvm[2]: Compiling ExprPPrinter.cpp for Debug+Asserts build
llvm[2]: Compiling ExprSMTLIBLetPrinter.cpp for Debug+Asserts build
llvm[2]: Compiling ExprSMTLIBPrinter.cpp for Debug+Asserts build
llvm[2]: Compiling ExprUtil.cpp for Debug+Asserts build
llvm[2]: Compiling ExprVisitor.cpp for Debug+Asserts build
llvm[2]: Compiling Lexer.cpp for Debug+Asserts build
llvm[2]: Compiling Parser.cpp for Debug+Asserts build
llvm[2]: Compiling Updates.cpp for Debug+Asserts build
llvm[2]: Building Debug+Asserts Archive Library libkleaverExpr.a
make[2]: Leaving directory /home/radu/bin/llvm/klee/lib/Expr' make[2]: Entering directory/home/radu/bin/llvm/klee/lib/Solver'
llvm[2]: Compiling CachingSolver.cpp for Debug+Asserts build
llvm[2]: Compiling CexCachingSolver.cpp for Debug+Asserts build
llvm[2]: Compiling ConstantDivision.cpp for Debug+Asserts build
llvm[2]: Compiling FastCexSolver.cpp for Debug+Asserts build
llvm[2]: Compiling IncompleteSolver.cpp for Debug+Asserts build
llvm[2]: Compiling IndependentSolver.cpp for Debug+Asserts build
llvm[2]: Compiling PCLoggingSolver.cpp for Debug+Asserts build
llvm[2]: Compiling QueryLoggingSolver.cpp for Debug+Asserts build
llvm[2]: Compiling SMTLIBLoggingSolver.cpp for Debug+Asserts build
llvm[2]: Compiling STPBuilder.cpp for Debug+Asserts build
llvm[2]: Compiling Solver.cpp for Debug+Asserts build
llvm[2]: Compiling SolverStats.cpp for Debug+Asserts build
llvm[2]: Building Debug+Asserts Archive Library libkleaverSolver.a
make[2]: Leaving directory /home/radu/bin/llvm/klee/lib/Solver' make[2]: Entering directory/home/radu/bin/llvm/klee/lib/Module'
llvm[2]: Compiling Checks.cpp for Debug+Asserts build
llvm[2]: Compiling InstructionInfoTable.cpp for Debug+Asserts build
llvm[2]: Compiling IntrinsicCleaner.cpp for Debug+Asserts build
llvm[2]: Compiling KInstruction.cpp for Debug+Asserts build
llvm[2]: Compiling KModule.cpp for Debug+Asserts build
KModule.cpp: In member function ‘void klee::KModule::prepare(const klee::Interpreter::ModuleOptions&, klee::InterpreterHandler_)’:
KModule.cpp:323:3: error: ‘Path’ is not a member of ‘llvm::sys’
KModule.cpp:323:19: error: expected ‘;’ before ‘path’
KModule.cpp:325:3: error: ‘path’ was not declared in this scope
KModule.cpp:325:3: note: suggested alternative:
In file included from KModule.cpp:56:0:
/home/radu/bin/llvm/llvm/include/llvm/Support/Path.h:26:16: note: ‘llvm::sys::path’
/bin/rm: cannot remove /home/radu/bin/llvm/klee/lib/Module/Debug+Asserts/KModule.d.tmp': No such file or directory make[2]: *_\* [/home/radu/bin/llvm/klee/lib/Module/Debug+Asserts/KModule.o] Error 1 make[2]: Leaving directory /home/radu/bin/llvm/klee/lib/Module'
make[1]: *** [Module/.makeall] Error 2
make[1]: Leaving directory`/home/radu/bin/llvm/klee/lib'
make: *** [all] Error 1

Hello,
I have run an example using KLEE. Many files are generated in klee-out-x.
In http://klee.github.io/klee/ , some information accounting for these files are offered,
but are far from enough. So i want to know what the information in these files exactly mean.
Have you known some detailed introduction about those files?
Thanks.
Zeng Jie

i Vinay,

This is due to a change I added recently. I need to replace it with
something because the LLVM API I used is deprecated and taking the
address of main isn't supposed to be allowed in ISO C++.

Provided you only run KLEE from the build directory (i.e. you do not
try to install it and then run the installed version) then you can
checkout a slightly older copy without support for KLEE running from
an install directory which doesn't have the code which is causing you
issues.

$ cd klee-src-directory/
$ git checkout 857831d

Could you add this issue to our issue tracker [1]. I need to fix this
at some point.

[1] https://github.com/ccadar/klee/issues

Thanks,
Dan.

On 29 December 2013 09:53, Vinay T S (vinayts) [email protected] wrote:
Hello,

My setup details :

/root/bin/stp : compiled from STP r940 code base .

[root@vinayts-lab-lnx klee-master]# which llvm-gcc
/usr/bin/llvm-gcc
[root@vinayts-lab-lnx klee-master]# llvm-gcc --version
llvm-gcc (GCC) 4.2.1 (Based on Apple Inc. build 5658) (LLVM build 2.9)
Copyright (C) 2007 Free Software Foundation, Inc.
This is free software; see the source for copying conditions. There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

Could install ucLibC from the instructions provided at :
http://ccadar.github.io/klee/GetStarted.html

[root@vinayts-lab-lnx klee-master]# uname -a
Linux vinayts-lab-lnx 2.6.18-194.8.1.el5 #1 SMP Wed Jun 23 10:52:51 EDT 2010
x86_64 x86_64 x86_64 GNU/Linux

[root@vinayts-lab-lnx klee-master]# gcc -v
Using built-in specs.
Target: x86_64-unknown-linux-gnu
Configured with: ../gcc-4.2.4/configure --prefix=/usr --libexecdir=/usr/lib
--enable-shared --enable-threads=posix --enable-__cxa_atexit
--enable-clocale=gnu --enable-languages=c,c++,fortran,java,objc,treelang
Thread model: posix
gcc version 4.2.4

Am trying to build KLEE now ( picked up the latest downloadable version from
github) .

Ran into some issues :

[root@vinayts-lab-lnx klee-master]# pwd
/usr/local/src/klee-master

make ENABLE_OPTIMIZED=1 -j10

make[1]: Entering directory /usr/local/src/klee-master/lib' make[2]: Entering directory/usr/local/src/klee-master/lib/Support'
make[2]: Nothing to be done for all'. make[2]: Leaving directory/usr/local/src/klee-master/lib/Support'
make[2]: Entering directory /usr/local/src/klee-master/lib/Basic' make[2]: Nothing to be done forall'.
make[2]: Leaving directory /usr/local/src/klee-master/lib/Basic' make[2]: Entering directory/usr/local/src/klee-master/lib/Solver'
make[2]: Entering directory /usr/local/src/klee-master/lib/Expr' make[2]: Nothing to be done forall'.
make[2]: Leaving directory /usr/local/src/klee-master/lib/Expr' llvm[2]: Compiling STPBuilder.cpp for Release+Asserts build llvm[2]: Compiling Solver.cpp for Release+Asserts build make[2]: Entering directory/usr/local/src/klee-master/lib/Module'
make[2]: Nothing to be done for all'. make[2]: Leaving directory/usr/local/src/klee-master/lib/Module'
make[2]: Entering directory /usr/local/src/klee-master/lib/Core' make[2]: Nothing to be done forall'.
make[2]: Leaving directory /usr/local/src/klee-master/lib/Core' In file included from STPBuilder.h:14, from Solver.cpp:14: /usr/local/src/klee-master/include/klee/util/ArrayExprHash.h:135:7: warning: no newline at end of file In file included from STPBuilder.h:14, from STPBuilder.cpp:10: /usr/local/src/klee-master/include/klee/util/ArrayExprHash.h:135:7: warning: no newline at end of file llvm[2]: Building Release+Asserts Archive Library libkleaverSolver.a make[2]: Leaving directory/usr/local/src/klee-master/lib/Solver'
make[1]: Leaving directory /usr/local/src/klee-master/lib' make[1]: Entering directory/usr/local/src/klee-master/tools'
make[2]: Entering directory /usr/local/src/klee-master/tools/klee-stats' make[2]: Nothing to be done forall'.
make[2]: Leaving directory /usr/local/src/klee-master/tools/klee-stats' make[2]: Entering directory/usr/local/src/klee-master/tools/ktest-tool'
make[2]: Nothing to be done for all'. make[2]: Leaving directory/usr/local/src/klee-master/tools/ktest-tool'
make[2]: Entering directory
/usr/local/src/klee-master/tools/gen-random-bout' make[2]: Nothing to be done forall'.
make[2]: Leaving directory
/usr/local/src/klee-master/tools/gen-random-bout' make[2]: Entering directory/usr/local/src/klee-master/tools/klee-replay'
make[2]: Nothing to be done for all'. make[2]: Leaving directory/usr/local/src/klee-master/tools/klee-replay'
perl: warning: Setting locale failed.
perl: warning: Please check that your locale settings:
LANGUAGE = (unset),
LC_ALL = (unset),
LC_CTYPE = "UTF-8",
LANG = "en_US.UTF-8"
are supported and installed on your system.
perl: warning: Falling back to the standard locale ("C").
perl: warning: Setting locale failed.
perl: warning: Please check that your locale settings:
LANGUAGE = (unset),
LC_ALL = (unset),
LC_CTYPE = "UTF-8",
LANG = "en_US.UTF-8"
are supported and installed on your system.
perl: warning: Falling back to the standard locale ("C").
perl: warning: Setting locale failed.
perl: warning: Please check that your locale settings:
LANGUAGE = (unset),
LC_ALL = (unset),
LC_CTYPE = "UTF-8",
LANG = "en_US.UTF-8"
are supported and installed on your system.
perl: warning: Falling back to the standard locale ("C").
perl: warning: Setting locale failed.
perl: warning: Please check that your locale settings:
LANGUAGE = (unset),
LC_ALL = (unset),
LC_CTYPE = "UTF-8",
LANG = "en_US.UTF-8"
are supported and installed on your system.
perl: warning: Falling back to the standard locale ("C").
make[2]: Entering directory /usr/local/src/klee-master/tools/kleaver' llvm[2]: Linking Release+Asserts executable kleaver (without symbols) make[2]: Entering directory/usr/local/src/klee-master/tools/klee'
llvm[2]: Compiling main.cpp for Release+Asserts build
In file included from
/usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
from
/usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
from main.cpp:32:
/usr/local/src/llvm-2.9/include/llvm/Config/config.h:641:1: warning:
"PACKAGE_BUGREPORT" redefined
In file included from
/usr/local/src/klee-master/include/klee/Config/Version.h:13,
from
/usr/local/src/klee-master/include/klee/util/Bits.h:13,
from /usr/local/src/klee-master/include/klee/Expr.h:13,
from
/usr/local/src/klee-master/include/klee/Constraints.h:13,
from
/usr/local/src/klee-master/include/klee/ExecutionState.h:13,
from main.cpp:6:
/usr/local/src/klee-master/include/klee/Config/config.h:59:1: warning: this
is the location of the previous definition
In file included from
/usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
from
/usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
from main.cpp:32:
/usr/local/src/llvm-2.9/include/llvm/Config/config.h:644:1: warning:
"PACKAGE_NAME" redefined
In file included from
/usr/local/src/klee-master/include/klee/Config/Version.h:13,
from
/usr/local/src/klee-master/include/klee/util/Bits.h:13,
from /usr/local/src/klee-master/include/klee/Expr.h:13,
from
/usr/local/src/klee-master/include/klee/Constraints.h:13,
from
/usr/local/src/klee-master/include/klee/ExecutionState.h:13,
from main.cpp:6:
/usr/local/src/klee-master/include/klee/Config/config.h:62:1: warning: this
is the location of the previous definition
In file included from
/usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
from
/usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
from main.cpp:32:
/usr/local/src/llvm-2.9/include/llvm/Config/config.h:647:1: warning:
"PACKAGE_STRING" redefined
In file included from
/usr/local/src/klee-master/include/klee/Config/Version.h:13,
from
/usr/local/src/klee-master/include/klee/util/Bits.h:13,
from /usr/local/src/klee-master/include/klee/Expr.h:13,
from
/usr/local/src/klee-master/include/klee/Constraints.h:13,
from
/usr/local/src/klee-master/include/klee/ExecutionState.h:13,
from main.cpp:6:
/usr/local/src/klee-master/include/klee/Config/config.h:65:1: warning: this
is the location of the previous definition
In file included from
/usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
from
/usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
from main.cpp:32:
/usr/local/src/llvm-2.9/include/llvm/Config/config.h:650:1: warning:
"PACKAGE_TARNAME" redefined
In file included from
/usr/local/src/klee-master/include/klee/Config/Version.h:13,
from
/usr/local/src/klee-master/include/klee/util/Bits.h:13,
from /usr/local/src/klee-master/include/klee/Expr.h:13,
from
/usr/local/src/klee-master/include/klee/Constraints.h:13,
from
/usr/local/src/klee-master/include/klee/ExecutionState.h:13,
from main.cpp:6:
/usr/local/src/klee-master/include/klee/Config/config.h:68:1: warning: this
is the location of the previous definition
In file included from
/usr/local/src/llvm-2.9/include/llvm/Support/system_error.h:225,
from
/usr/local/src/llvm-2.9/include/llvm/Support/FileSystem.h:34,
from main.cpp:32:
/usr/local/src/llvm-2.9/include/llvm/Config/config.h:653:1: warning:
"PACKAGE_VERSION" redefined
In file included from
/usr/local/src/klee-master/include/klee/Config/Version.h:13,
from
/usr/local/src/klee-master/include/klee/util/Bits.h:13,
from /usr/local/src/klee-master/include/klee/Expr.h:13,
from
/usr/local/src/klee-master/include/klee/Constraints.h:13,
from
/usr/local/src/klee-master/include/klee/ExecutionState.h:13,
from main.cpp:6:
/usr/local/src/klee-master/include/klee/Config/config.h:74:1: warning: this
is the location of the previous definition
llvm[2]: ======= Finished Linking Release+Asserts Executable kleaver
(without symbols)
make[2]: Leaving directory /usr/local/src/klee-master/tools/kleaver' main.cpp: In function 'void parseArguments(int, char**)': main.cpp:653: warning: cast from type 'const char**' to type 'char**' casts away constness main.cpp: In function 'int main(int, char**, char**)': main.cpp:1263: error: ISO C++ forbids taking address of function '::main' main.cpp:1263: warning: ISO C++ forbids casting between pointer-to-function and pointer-to-object make[2]: *** [/usr/local/src/klee-master/tools/klee/Release+Asserts/main.o] Error 1 make[2]: Leaving directory/usr/local/src/klee-master/tools/klee'
make[1]: *** [klee/.makeall] Error 2
make[1]: Leaving directory `/usr/local/src/klee-master/tools'
make: *** [all] Error 1

On examining line 1263 :

1262 : llvm::sys::Path LibraryDir =
KleeHandler::getRunTimeLibraryPath(argv[0],
1263 : reinterpret_cast<void*>(main));
1264 : Interpreter::ModuleOptions Opts(LibraryDir.c_str(),

Seems like gcc 4.2.4 does not like this ( in line 1263) . I am not too good
at C++, wanted to check how to get around this compilation issue .

Thanks
Vinay

I think there is a question when calling the expand function in the main().

it assigns an integer "Index" to unsigned char * "buffer". Can this ?

soos@soosV3560:~/development/smt/klee$ CXX="clang++" CC="clang" ./configure --with-stp=../stp/
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/soos/development/llvm/llvm
checking llvm obj dir... /home/soos/development/llvm/build
checking llvm package version... 3.4svn
checking llvm version major... 3
checking llvm version minor... 4
checking llvm is release version... 0
checking llvm build mode... Release+Debug+Asserts
checking uclibc... no
checking POSIX runtime... default (disabled, no uclibc)
checking runtime configuration... Release+Asserts
checking for gcc... clang
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 clang accepts -g... yes
checking for clang option to accept ISO C89... none needed
checking how to run the C preprocessor... clang -E
checking for grep that handles long lines and -e... /bin/grep
checking for egrep... /bin/grep -E
checking for ANSI C header files... yes
checking for sys/types.h... yes
checking for sys/stat.h... yes
checking for stdlib.h... yes
checking for string.h... yes
checking for memory.h... yes
checking for strings.h... yes
checking for inttypes.h... yes
checking for stdint.h... yes
checking for unistd.h... yes
checking sys/acl.h usability... no
checking sys/acl.h presence... no
checking for sys/acl.h... no
checking whether we are using the GNU C++ compiler... yes
checking whether clang++ accepts -g... yes
checking how to run the C++ preprocessor... clang++ -E
checking selinux/selinux.h usability... yes
checking selinux/selinux.h presence... yes
checking for selinux/selinux.h... yes
checking stp/c_interface.h usability... yes
checking stp/c_interface.h presence... yes
checking for stp/c_interface.h... yes
checking for vc_setInterfaceFlags in -lstp... no
OK
checking for runtest... no
configure: creating ./config.status
config.status: creating Makefile.config
config.status: creating docs/doxygen.cfg
config.status: creating include/klee/Config/config.h
config.status: include/klee/Config/config.h is unchanged
config.status: executing setup commands
config.status: executing Makefile commands
config.status: executing Makefile.common commands
config.status: executing lib/Makefile commands
config.status: executing runtime/Makefile commands
config.status: executing test/Makefile commands
config.status: executing test/Makefile.tests commands
config.status: executing tools/Makefile commands
config.status: executing unittests/Makefile commands
soos@soosV3560:~/development/smt/klee$ make   
/home/soos/development/smt/klee/Makefile.rules:456: Provided Compiler "" is not found. Provide full path!
/home/soos/development/smt/klee/Makefile.rules:459: Provided Compiler "" is not found. Provide full path!
make[1]: Entering directory `/home/soos/development/smt/klee/lib'
/home/soos/development/smt/klee/Makefile.rules:456: Provided Compiler "" is not found. Provide full path!
/home/soos/development/smt/klee/Makefile.rules:459: Provided Compiler "" is not found. Provide full path!
make[2]: Entering directory `/home/soos/development/smt/klee/lib/Basic'
/home/soos/development/smt/klee/Makefile.rules:456: Provided Compiler "" is not found. Provide full path!
/home/soos/development/smt/klee/Makefile.rules:459: Provided Compiler "" is not found. Provide full path!
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/soos/development/smt/klee/lib/Basic'
make[2]: Entering directory `/home/soos/development/smt/klee/lib/Support'
/home/soos/development/smt/klee/Makefile.rules:456: Provided Compiler "" is not found. Provide full path!
/home/soos/development/smt/klee/Makefile.rules:459: Provided Compiler "" is not found. Provide full path!
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/soos/development/smt/klee/lib/Support'
make[2]: Entering directory `/home/soos/development/smt/klee/lib/Expr'
/home/soos/development/smt/klee/Makefile.rules:456: Provided Compiler "" is not found. Provide full path!
/home/soos/development/smt/klee/Makefile.rules:459: Provided Compiler "" is not found. Provide full path!
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/soos/development/smt/klee/lib/Expr'
make[2]: Entering directory `/home/soos/development/smt/klee/lib/Solver'
/home/soos/development/smt/klee/Makefile.rules:456: Provided Compiler "" is not found. Provide full path!
/home/soos/development/smt/klee/Makefile.rules:459: Provided Compiler "" is not found. Provide full path!
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/soos/development/smt/klee/lib/Solver'
make[2]: Entering directory `/home/soos/development/smt/klee/lib/Module'
/home/soos/development/smt/klee/Makefile.rules:456: Provided Compiler "" is not found. Provide full path!
/home/soos/development/smt/klee/Makefile.rules:459: Provided Compiler "" is not found. Provide full path!
llvm[2]: Compiling KModule.cpp for Release+Debug+Asserts build
^Cmake[2]: *** [/home/soos/development/smt/klee/lib/Module/Release+Debug+Asserts/KModule.o] Interrupt
make[1]: *** [Module/.makeall] Interrupt
make: *** [all] Interrupt

Note that I had to hack the "-lstp" with printing "OK" because otherwise it is a mess with the STP from git. This does not affect the above messages, though. Do you guys know why these messages are shown? Are these real errors or can they be ignored? If they can be ignored, maybe it should not be printed.

PS: Have you considered moving to cmake? It's usually less hassle to set up than configure.

Hello,

I was build klee-ulibc-llvm3.3 with clang.

...<skip>
 CC libc/unistd/getpass.os
  CC libc/unistd/getsubopt.os
  CC libc/unistd/pathconf.os
  CC libc/unistd/sleep.os
  CC libc/unistd/swab.os
  CC libc/unistd/sysconf.os
  CC libc/unistd/ualarm.os
  CC libc/unistd/usershell.os
  CC libc/unistd/usleep.os
  CC libc/misc/internals/__uClibc_main.os
  CC libc/stdlib/atexit.os
  STRIP -x -R .note -R .comment lib/libc.a
  AR cr lib/libc.a

But, when I run KLEE with -libc=uclibc, 'Invalid bitcode signature ..." error occured:

Invalid bitcode signature for /llvm/klee-uclibc-llvm33/lib/libc.a
klee: ModuleUtil.cpp:75: llvm::Module* klee::linkWithLibrary(llvm::Module*, const string&): Assertion `library_module.get()' failed.
0  klee      0x08c8a40f llvm::sys::PrintStackTrace(_IO_FILE*) + 47
1  klee      0x08c8a66f
2  klee      0x08c8a04c
3            0x0061c400 __kernel_sigreturn + 0
4            0x0061c416 __kernel_vsyscall + 2
5  libc.so.6 0x00184aff gsignal + 79
6  libc.so.6 0x00188083 abort + 323
7  libc.so.6 0x0017d857
8  libc.so.6 0x0017d907
9  klee      0x0822e1d1 klee::linkWithLibrary(llvm::Module*, std::string const&) + 449
10 klee      0x081d6b96
11 klee      0x081bf68a main + 1338
12 libc.so.6 0x0016f905 __libc_start_main + 245
13 klee      0x081d2b80

Am I missing something?

Best Regards,

runtime/POSIX/stubs.c uses an undefined PATH_MAX on my Linux system:

char *canonicalize_file_name (const char *name) __attribute__((weak));
char *canonicalize_file_name (const char *name) {
  char *res = malloc(PATH_MAX);
  char *rp_res = realpath(name, res);
  if (!rp_res)
    free(res);
  return rp_res;
}

It's afaik neither in the C standards nor included with the default option -D _GNU_SOURCE. There are multiple options to resolve this issue. Instead of including linux/limits.h I'd recommend using POSIX_C_SOURCE 200809L/ _XOPEN_SOURCE 700 and pruning canonicalize_file_name to:

char *canonicalize_file_name (const char *name) {
  return realpath(name, NULL);
}

Should work for BSD's libc, glibc, musl...

Because the default values for KLEE options change from time to time, it would be useful to save all options and current values in klee-last/info.

The CDE package for KLEE (http://ccadar.github.io/klee/GetStarted.html#cde) is out-of-date and needs to be regenerated.

On the current version of KLEE (tested on commit b2070cf), with LLVM 2.9, I've observed a non-deterministic behavior while testing ptx utility (version from Coreutils 6.10).
Here are the command line arguments:

klee --posix-runtime --libc=uclibc ptx.bc x ptxFile.txt

ptxFile.txt consist just of letter "a" (no apostrophes).

When invoked multiple times, out of bounds pointer is reported either in line 1510 of the ptx.c file or in line 1489 of the file.

I've checked that with address randomization (ASLR) turned off in the OS.
The OS used for testing was Ubuntu 12.04.3.

Hello,
I was saw your paper about klee-fp(Symbolic Crosschecking of Floating-Point and SIMD Code).

I am wondering about your plan of merging klee-fp.

Thanks,

KLEE does not handle overshift behaviour very well. Overshift is were bitshift is performed where the shift amount is >= to the bitwidth of the variable being shifted. For example:

int x = 2; // assume width is 4 bytes
int result = x << (sizeof(x)*8) // x << 32
// We are now in the land of undefined behaviour.

Take this example program

#include<stdio.h>

int main()
{
  volatile unsigned int x =15;
  volatile unsigned int y =sizeof(x)*8;
  volatile unsigned int result;
  unsigned int limit = sizeof(x)*8;
  klee_make_symbolic(&y,sizeof(y),"y");
  klee_assume(y > 31);
  klee_assume(y < 33);
  result = x << y; // Deliberate overshift

  if (result ==0)
    printf("Overshift to zero\n");
  else if (result == ( x << (y % limit)) )
    printf("Bitmasked overshift\n");
  else
    printf("Unrecognised behaviour.\n");

  return result;
}

This small program tests for different overshift behaviours. On x86 machines it appears the shift width is the requested shift amount modulo the bit width so it is not possible to overshift. In SMT-LIBv2 the interpretation of overshifting is to overshift to zero (i.e. the result of x << y if y >= (sizeof(x)*8) is always zero). If you replace y with a constant and have KLEE execute this code it will only follow the "Overshift to zero" path because the expression is evaluated using llvm::APInt::shl() which treats the result of overshifting to zero (note overshifting in LLVM is undefined behaviour)

If you ask KLEE to run this program (without my overshift checks, see issue #26) KLEE explores all three paths which seems wrong to me.

You could argue that because this is undefined behaviour KLEE should be deliberately implemented to explore all three paths however if you think about this in terms of solving (here we effectively have 15 << 32 ) there should only be one answer.

Clearly something is wrong because KLEE also explores the "Unrecognised behaviour" path but when it tries to generate a test it realises the path constraints are infeasible.

I currently do not have time to look at this issue but I'm listing it here so people are aware of it and hopefully one day it will be fixed. My pull request (#26) side steps this problem by not allowing KLEE to explore paths where overshift can occur by treating it as an error.

Hello,

I hope this is right place to ask question.

I was build KLEE 3.3 based on Clang 3.3, LLVM 3.3.
I was modified some build script errors and build was successfully done.
But, When I run klee with small trivial c-code, It generated:

KLEE: ERROR: error loading program '/home/minhyuk/brucelee/test.s': Invalid bitcode signature

Here is Source:

void klee_make_symbolic(void*,int,char*);

int add(int x, int y){
    if(x == 4 && y == x-1){
        return 10;
    }
    else{
        return x+y;
    }
}


int main(){
    int a,b;

    klee_make_symbolic(&a, 4, "a");
    klee_make_symbolic(&b, 4, "b");

    return add(a,b);
}

Here is LLVM bitecode:

; ModuleID = 'test.c'
target datalayout = "e-p:32:32:32-i1:8:8-i8:8:8-i16:16:16-i32:32:32-i64:32:64-f32:32:32-f64:32:64-v64:64:64-v128:128:128-a0:0:64-f80:32:32-n8:16:32-S128"
target triple = "i386-pc-linux-gnu"

@.str = private unnamed_addr constant [2 x i8] c"a\00", align 1
@.str1 = private unnamed_addr constant [2 x i8] c"b\00", align 1

; Function Attrs: nounwind
define i32 @_Z3addii(i32 %x, i32 %y) #0 {
entry:
  %retval = alloca i32, align 4
  %x.addr = alloca i32, align 4
  %y.addr = alloca i32, align 4
  store i32 %x, i32* %x.addr, align 4
  store i32 %y, i32* %y.addr, align 4
  %0 = load i32* %x.addr, align 4
  %cmp = icmp eq i32 %0, 4
  br i1 %cmp, label %land.lhs.true, label %if.else

land.lhs.true:                                    ; preds = %entry
  %1 = load i32* %y.addr, align 4
  %2 = load i32* %x.addr, align 4
  %sub = sub nsw i32 %2, 1
  %cmp1 = icmp eq i32 %1, %sub
  br i1 %cmp1, label %if.then, label %if.else

if.then:                                          ; preds = %land.lhs.true
  store i32 10, i32* %retval
  br label %return

if.else:                                          ; preds = %land.lhs.true, %entry
  %3 = load i32* %x.addr, align 4
  %4 = load i32* %y.addr, align 4
  %add = add nsw i32 %3, %4
  store i32 %add, i32* %retval
  br label %return

return:                                           ; preds = %if.else, %if.then
  %5 = load i32* %retval
  ret i32 %5
}

define i32 @main() #1 {
entry:
  %retval = alloca i32, align 4
  %a = alloca i32, align 4
  %b = alloca i32, align 4
  store i32 0, i32* %retval
  %0 = bitcast i32* %a to i8*
  call void @_Z18klee_make_symbolicPviPc(i8* %0, i32 4, i8* getelementptr inbounds ([2 x i8]* @.str, i32 0, i32 0))
  %1 = bitcast i32* %b to i8*
  call void @_Z18klee_make_symbolicPviPc(i8* %1, i32 4, i8* getelementptr inbounds ([2 x i8]* @.str1, i32 0, i32 0))
  %2 = load i32* %a, align 4
  %3 = load i32* %b, align 4
  %call = call i32 @_Z3addii(i32 %2, i32 %3)
  ret i32 %call
}

declare void @_Z18klee_make_symbolicPviPc(i8*, i32, i8*) #1

attributes #0 = { nounwind "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf"="true" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "unsafe-fp-math"="false" "use-soft-float"="false" }
attributes #1 = { "less-precise-fpmad"="false" "no-frame-pointer-elim"="true" "no-frame-pointer-elim-non-leaf"="true" "no-infs-fp-math"="false" "no-nans-fp-math"="false" "unsafe-fp-math"="false" "use-soft-float"="false" }

Am I miss something?

Best Regards,
-Minhyuk

I create example file valami.c:

#include <klee/klee.h>
#include <stdio.h>


int valami(int x) {
    if (x == 234) {
        printf("OK\n");
        return 1;
    } else if (x==22) {
        printf("damn\n");
        return 2;
    } else if (x==1) {
        printf("saljfdslfj\n");
        return 3;
    }

    printf("hee\n");
    return 4;
}

then compile:

$ clang -emit-llvm -Wall -I ../../include -c -g valami.c 

then run with klee:

$ klee valami.o 
'main' function not found in module.
0  klee            0x0000000000d8064f
1  klee            0x0000000000d80b59
2  libpthread.so.0 0x00007f65c75bccb0
3  libpthread.so.0 0x00000000015fb080
zsh: segmentation fault (core dumped)  klee valami.o

I know that it is wrong (no main) but it should not segfault anyway :)

valgrind tells me:

 valgrind klee valami.o
==21758== Memcheck, a memory error detector
==21758== Copyright (C) 2002-2013, and GNU GPL'd, by Julian Seward et al.
==21758== Using Valgrind-3.9.0 and LibVEX; rerun with -h for copyright info
==21758== Command: klee valami.o
==21758== 
'main' function not found in module.
==21758== Invalid read of size 8
==21758==    at 0x57929B: main (in /usr/local/bin/klee)
==21758==  Address 0x5e47b20 is 0 bytes inside a block of size 1,589 free'd
==21758==    at 0x4C2B343: operator delete(void*) (vg_replace_malloc.c:502)
==21758==    by 0x8AE201: llvm::BitcodeReader::FreeState() (in /usr/local/bin/klee)
==21758==    by 0x8BDE23: llvm::BitcodeReader::~BitcodeReader() (in /usr/local/bin/klee)
==21758==    by 0x8BE368: llvm::BitcodeReader::~BitcodeReader() (in /usr/local/bin/klee)
==21758==    by 0xD083D7: llvm::Module::MaterializeAllPermanently(std::string*) (in /usr/local/bin/klee)
==21758==    by 0x577B58: main (in /usr/local/bin/klee)
==21758== 
==21758== Invalid write of size 8
==21758==    at 0xD7007B: llvm::MemoryBuffer::~MemoryBuffer() (in /usr/local/bin/klee)
==21758==    by 0xD700A8: llvm::MemoryBuffer::~MemoryBuffer() (in /usr/local/bin/klee)
==21758==    by 0x5792A0: main (in /usr/local/bin/klee)
==21758==  Address 0x5e47b20 is 0 bytes inside a block of size 1,589 free'd
==21758==    at 0x4C2B343: operator delete(void*) (vg_replace_malloc.c:502)
==21758==    by 0x8AE201: llvm::BitcodeReader::FreeState() (in /usr/local/bin/klee)
==21758==    by 0x8BDE23: llvm::BitcodeReader::~BitcodeReader() (in /usr/local/bin/klee)
==21758==    by 0x8BE368: llvm::BitcodeReader::~BitcodeReader() (in /usr/local/bin/klee)
==21758==    by 0xD083D7: llvm::Module::MaterializeAllPermanently(std::string*) (in /usr/local/bin/klee)
==21758==    by 0x577B58: main (in /usr/local/bin/klee)
==21758== 
==21758== Invalid free() / delete / delete[] / realloc()
==21758==    at 0x4C2B343: operator delete(void*) (vg_replace_malloc.c:502)
==21758==    by 0x5792A0: main (in /usr/local/bin/klee)
==21758==  Address 0x5e47b20 is 0 bytes inside a block of size 1,589 free'd
==21758==    at 0x4C2B343: operator delete(void*) (vg_replace_malloc.c:502)
==21758==    by 0x8AE201: llvm::BitcodeReader::FreeState() (in /usr/local/bin/klee)
==21758==    by 0x8BDE23: llvm::BitcodeReader::~BitcodeReader() (in /usr/local/bin/klee)
==21758==    by 0x8BE368: llvm::BitcodeReader::~BitcodeReader() (in /usr/local/bin/klee)
==21758==    by 0xD083D7: llvm::Module::MaterializeAllPermanently(std::string*) (in /usr/local/bin/klee)
==21758==    by 0x577B58: main (in /usr/local/bin/klee)
==21758== 
==21758== 
==21758== HEAP SUMMARY:
==21758==     in use at exit: 224 bytes in 5 blocks
==21758==   total heap usage: 1,387 allocs, 1,383 frees, 158,140 bytes allocated
==21758== 
==21758== LEAK SUMMARY:
==21758==    definitely lost: 160 bytes in 2 blocks
==21758==    indirectly lost: 0 bytes in 0 blocks
==21758==      possibly lost: 0 bytes in 0 blocks
==21758==    still reachable: 64 bytes in 3 blocks
==21758==         suppressed: 0 bytes in 0 blocks
==21758== Rerun with --leak-check=full to see details of leaked memory
==21758== 
==21758== For counts of detected and suppressed errors, rerun with: -v
==21758== ERROR SUMMARY: 3 errors from 3 contexts (suppressed: 0 from 0)

Versions:

• llvm 2.9
• clang 2.9
• klee compiled with gcc-4.6.3
• valgrind 3.9.0
• on Ubuntu 12.04.03 LTS
• klee 3eff4a2

Hi All,

I have written some scripts for automating the building of KLEE. I am familiar with Archlinux and Ubuntu, so only these two distros are supported right now. May add more latter.

https://github.com/antiAgainst/klee-build-scripts

Hope this helps!

Hi All,

I would suggest that we use jekyll to host the documentation. Although the current documentation goes with llvm style, it is a mix of html tags and contents. This is not easy to maintain. By using jekyll, we can then use markdown to write the doc, which will reduce the work of maintaining the doc. Also, the doc will be more "beautiful".

If you guys think this change is beneficial, I will take the responsibility to do it.

KLEE uses DejaGNU for testing currently (I'm not a huge fan)

LLVM has stopped using it and now has it's own testing system powered by a tool called llvm-lit written by @ddunbar . It seems like @ddunbar started working on llvm-lit support in KLEE (use cd test && make check-local-all ) but it doesn't really work

• With llvm2.9 it would consider any stderr output to be test failure. But KLEE produces a lot of information on standard error without a problem.
• With llvm3.3 it seems lit.formats.TclTest() doesn't exist anymore.

Moving to llvm-lit would allow us to run tests in parallel (once the tests were restructured into their own directories) and I believe it is also easier to run individual tests.

If we were to go down this route I think it would be best if we included our own copy of lit.py (and related files) so that everyone uses the same version.

Another alternative is to roll our own testing tool. We wouldn't necessarily have to start from scratch because I wrote one recently (inspired by DejaGNU) gvtester.py

KLEE does not compile with versions <= 2.8, despite having a lot of conditional code for this purpose. My suggestion is to remove support for LLVM <= 2.8: it's hard to preserve support for so many different versions, and it makes the code quite ugly. Any thoughts?

While installing

llvm[2]: Installing Release+Asserts /usr/local/bin/ktest-tool
strip:/usr/local/bin/ktest-tool: File format not recognized
/usr/bin/install: strip process terminated abnormally

It's a python file, so it should not be stripped.

soos@soosV3560:~/development/smt/klee$ make
[...]
make[2]: Entering directory `/home/soos/development/smt/klee/lib/Expr'
/home/soos/development/smt/klee/Makefile.rules:456: Provided Compiler "" is not found. Provide full path!
/home/soos/development/smt/klee/Makefile.rules:459: Provided Compiler "" is not found. Provide full path!
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/soos/development/smt/klee/lib/Expr'
make[2]: Entering directory `/home/soos/development/smt/klee/lib/Solver'
/home/soos/development/smt/klee/Makefile.rules:456: Provided Compiler "" is not found. Provide full path!
/home/soos/development/smt/klee/Makefile.rules:459: Provided Compiler "" is not found. Provide full path!
make[2]: Nothing to be done for `all'.
make[2]: Leaving directory `/home/soos/development/smt/klee/lib/Solver'
make[2]: Entering directory `/home/soos/development/smt/klee/lib/Module'
/home/soos/development/smt/klee/Makefile.rules:456: Provided Compiler "" is not found. Provide full path!
/home/soos/development/smt/klee/Makefile.rules:459: Provided Compiler "" is not found. Provide full path!
llvm[2]: Compiling KModule.cpp for Release+Debug+Asserts build
KModule.cpp:323:14: error: no member named 'Path' in namespace 'llvm::sys'
  llvm::sys::Path path(opts.LibraryDir);
  ~~~~~~~~~~~^
KModule.cpp:325:3: error: use of undeclared identifier 'path'
  path.appendComponent("kleeRuntimeIntrinsic.bc");
  ^
KModule.cpp:329:36: error: use of undeclared identifier 'path'
  module = linkWithLibrary(module, path.c_str());
                                   ^
3 errors generated.
make[2]: *** [/home/soos/development/smt/klee/lib/Module/Release+Debug+Asserts/KModule.o] Error 1
make[2]: Leaving directory `/home/soos/development/smt/klee/lib/Module'
make[1]: *** [Module/.makeall] Error 2
make[1]: Leaving directory `/home/soos/development/smt/klee/lib'
make: *** [all] Error 1

Note that I left out the warnings printed as reported in issue #37. I configured KLEE as such:

soos@soosV3560:~/development/smt/klee$ CXX="clang++" CC="clang" ./configure --with-stp=../stp/
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/soos/development/llvm/llvm
checking llvm obj dir... /home/soos/development/llvm/build
checking llvm package version... 3.4svn
checking llvm version major... 3
checking llvm version minor... 4
checking llvm is release version... 0
checking llvm build mode... Release+Debug+Asserts
checking uclibc... no
checking POSIX runtime... default (disabled, no uclibc)
checking runtime configuration... Release+Asserts
checking for gcc... clang
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 clang accepts -g... yes
checking for clang option to accept ISO C89... none needed
checking how to run the C preprocessor... clang -E
checking for grep that handles long lines and -e... /bin/grep
checking for egrep... /bin/grep -E
checking for ANSI C header files... yes
checking for sys/types.h... yes
checking for sys/stat.h... yes
checking for stdlib.h... yes
checking for string.h... yes
checking for memory.h... yes
checking for strings.h... yes
checking for inttypes.h... yes
checking for stdint.h... yes
checking for unistd.h... yes
checking sys/acl.h usability... no
checking sys/acl.h presence... no
checking for sys/acl.h... no
checking whether we are using the GNU C++ compiler... yes
checking whether clang++ accepts -g... yes
checking how to run the C++ preprocessor... clang++ -E
checking selinux/selinux.h usability... yes
checking selinux/selinux.h presence... yes
checking for selinux/selinux.h... yes
checking stp/c_interface.h usability... yes
checking stp/c_interface.h presence... yes
checking for stp/c_interface.h... yes
checking for vc_setInterfaceFlags in -lstp... no
OK
checking for runtest... no
configure: creating ./config.status
config.status: creating Makefile.config
config.status: creating docs/doxygen.cfg
config.status: creating include/klee/Config/config.h
config.status: include/klee/Config/config.h is unchanged
config.status: executing setup commands
config.status: executing Makefile commands
config.status: executing Makefile.common commands
config.status: executing lib/Makefile commands
config.status: executing runtime/Makefile commands
config.status: executing test/Makefile commands
config.status: executing test/Makefile.tests commands
config.status: executing tools/Makefile commands
config.status: executing unittests/Makefile commands

My version of CLANG&LLVM is newest (from SVN) as of 2 days ago:

soos@soosV3560:~/development/smt/klee$ clang --version
clang version 3.4 (trunk 191180)
Target: x86_64-unknown-linux-gnu
Thread model: posix

soos@soosV3560:~/development/smt/klee$ llvm-ar --version
LLVM (http://llvm.org/):
  LLVM version 3.4svn
  Optimized build with assertions.
  Built Sep 22 2013 (22:26:20).
  Default target: x86_64-unknown-linux-gnu
  Host CPU: core-avx-i

Can you tell me what I'm doing wrong? Thanks!

Mate

Take concrete input file (numbers.txt):

50 55

and program (open.c):

#include <stdio.h>

int main(int argc, char* argv[])
{
  int numbers[2];
  FILE* f = fopen(argv[1],"r");

  if(f==0)
    return 1;

  int numGet = fscanf(f,"%i %i", numbers, (numbers) + 1);

  printf("Received: %i , %i\n",numbers[0],numbers[1]);

  if(numbers[0] > 0)
  {
    printf("first num > 0\n");
    if(numbers[1] > 0)
    {
      printf("second num > 0\n");
    }
    else
      printf("second num <= 0\n");
  }
  else
    printf("first num <= 0\n");
}

Compile this to llvm bitcode and try to run this is KLEE
$ llvm-gcc --emit-llvm open.c -o open.bc
$ klee --posix-runtime --libc=uclibc open.bc numbers.txt

KLEE will output the following and then hang:

KLEE: NOTE: Using model: /data/dev/KLEE/klee/bin/Release+Asserts/lib/libkleeRuntimePOSIX.bca
KLEE: output directory = "klee-out-47"
KLEE: WARNING: undefined reference to function: __isoc99_fscanf
KLEE: WARNING: undefined reference to function: __xstat64
KLEE: WARNING ONCE: calling external: syscall(16, 0, 21505, 38994784)
KLEE: WARNING ONCE: calling __user_main with extra arguments.
KLEE: WARNING ONCE: calling external: __xstat64(1, 38936544, 39025120)
KLEE: WARNING ONCE: calling external: __isoc99_fscanf(39026192, 38868928, 39102320, 39102324)

It appears that that KLEE is stuck in the JIT

(gdb) bt
#0  __lll_lock_wait_private () at         ../nptl/sysdeps/unix/sysv/linux/x86_64/lowlevellock.S:93
#1  0x00007ffff6e46488 in _L_lock_53 () from /lib/x86_64-linux-gnu/libc.so.6
#2  0x00007ffff6e4639f in __isoc99_fscanf (stream=0x1e64a50, format=0x1e126d0 "%i %i") at isoc99_fscanf.c:31
#3  0x00007ffff7ed71d8 in __unnamed_1 ()
#4  0x00000000008a2449 in llvm::JIT::runFunction(llvm::Function*, std::vector<llvm::GenericValue, std::allocator<llvm::GenericValue> > const&) ()
#5  0x0000000000591ab8 in klee::ExternalDispatcher::runProtectedCall (this=0x1bc2eb0, f=0x1e37860, args=<optimised out>) at /data/dev/KLEE/klee/src/lib/Core/ExternalDispatcher.cpp:189
#6  0x000000000059265e in klee::ExternalDispatcher::executeCall (this=0x1bc2eb0, f=<optimised out>, i=0x1505158, args=0x7fffffffc160) at /data/dev/KLEE/klee/src/lib/Core/ExternalDispatcher.cpp:164
#7  0x000000000057bb12 in klee::Executor::callExternalFunction (this=0x1a83860, state=..., target=0x17bb420, function=0x1505380, arguments=...) at /data/dev/KLEE/klee/src/lib/Core/Executor.cpp:2724
#8  0x000000000057f996 in klee::Executor::executeCall (this=0x1a83860, state=..., ki=0x17bb420, f=0x1505380, arguments=...) at /data/dev/KLEE/klee/src/lib/Core/Executor.cpp:1097
#9  0x0000000000585157 in klee::Executor::executeInstruction (this=<optimised out>, state=..., ki=<optimised out>) at /data/dev/KLEE/klee/src/lib/Core/Executor.cpp:1604
#10 0x00000000005880db in klee::Executor::run (this=0x1a83860, initialState=...) at /data/dev/KLEE/klee/src/lib/Core/Executor.cpp:2465
#11 0x0000000000588b46 in klee::Executor::runFunctionAsMain (this=<optimised out>, f=0x1c780b8, argc=2, argv=0x1786600, envp=0x7fff000000d0) at /data/dev/KLEE/klee/src/lib/Core/Executor.cpp:3257
#12 0x0000000000561207 in main (argc=<optimised out>, argv=<optimised out>, envp=0x7fffffffea18) at /data/dev/KLEE/klee/src/tools/klee/main.cpp:1429

This was an issue I noticed a while ago and a recent mailing list post ( http://www.mail-archive.com/[email protected]/msg01259.html ) reminded me of this.

Uclibc seems to provide fscanf so I'm not quite sure why KLEE is trying to call fscanf externally. I unfortunately do not have time to investigate now.

Hello,

I have simple strange testcase here:

const char *const  errmsg[2]= {0,}; 

/* ---------------- Implement Under Test ----------------- */
const char * get_error_message(int err)
{
    char * x = errmsg[err];
    return x;
}
/* ---------------- Implement Under Test ----------------- */

int main(){
    int err;
    klee_make_symbolic(&err,sizeof(err),"err");
    get_error_message(err);
}

KLEE generates 27 testcases in my case.
Is there something I missing?

Thank you.

Record line numbers in .(k)path files when debug info is present.

We should probably remove the --read-args flags ( and the cruft of code associated with it) anyway because the LLVM CommandLine library supports this already using "Response files" (it is supported in LLVM 2.9)

This command line argument is used by the Coverage/ReadArgs.c test.