Limits of Klee (the LLVM program analysis tool)

Question

http://klee.llvm.org/ is a program analysis tool that works by symbolic execution and constraint solving, finding possible inputs that will cause a program to crash, and outputting these as test cases. It's an extremely impressive piece of engineering that has produced some good results so far, including finding a number of bugs in a collection of open-source implementations of Unix utilities that had been considered among some of the most thoroughly tested software ever written.

My question is: what does it not do?

Of course, any such tool has the inherent limit that it can't read the user's mind and guess what the output was supposed to be. But leaving aside the in principle impossible, most projects don't yet seem to be using Klee; what are the limitations of the current version, what sort of bugs and workloads can it as yet not handle?

Answer 1

As I can say after reading a http://llvm.org/pubs/2008-12-OSDI-KLEE.html

It can't check all possible paths of big program. It failed even on sort utility. The problem is a halting problem (Undecidable problem), and KLEE is a heuristic, so it is able to check only some of paths in limited time.

It can't work fast, according to paper, it needed 89-hours to generate tests for 141000 lines of code in COREUTILS (with libc code used in them). And the largest single program has only ~10000 lines.

It knows nothing about floating point, longjmp/setjmp, threads, asm; memory objects of variable size.

Update: /from llvm blog/ http://blog.llvm.org/2011/05/what-every-c-programmer-should-know_14.html

5 . The LLVM "Klee" Subproject uses symbolic analysis to "try every possible path" through a piece of code to find bugs in the code and it produces a testcase. It is a great little project that is mostly limited by not being practical to run on large-scale applications.

Update2: KLEE requieres program to be modified. http://t1.minormatter.com/~ddunbar/klee-doxygen/overview.html

. Symbolic memory is defined by inserting special calls to KLEE (namely klee_make_symbolic) During execution, KLEE tracks all uses of symbolic memory.