Arch Linux

tavianator

Member

From: Waterloo, ON, Canada

Registered: 2007-08-21

Posts: 859

Website

Generating tests with KLEE

I just came across KLEE the other day, and it's pretty sweet.  The homepage doesn't describe exactly what it does very plainly, simply calling it a "symbolic virtual machine" over LLVM.  What it does is generate high-coverage tests for your code.  You tell it what parts of your code are inputs (by classifying them as "symbols"), and KLEE tries to determine what would happen for each possible value of the symbols.  Here's an example of its power:

$ cat foo.c
#include <klee/klee.h>

int
foo(int x)
{
  if (x*x == 1000) {
    return 1;
  } else {
    return 0;
  }
}

int
main()
{
  return foo(klee_int("x"));
}
$ llvm-gcc --emit-llvm -c -g foo.c
$ klee foo.o
KLEE: output directory = "klee-out-0"

KLEE: done: total instructions = 31
KLEE: done: completed paths = 1
KLEE: done: generated tests = 1

This looks like a bug (clearly there's two execution paths through foo(), right?), but is actually KLEE being super smart: no int satisfies "x*x == 1000" because 1000 isn't a square, so it knows the "return 1;" is unreachable.

I haven't used KLEE for anything really serious yet, but it looks pretty powerful.

I put a package for it in the AUR here.