Tutorial One: Testing a Small Function

The demo code

This tutorial walks you through the main steps needed to test a simple function with KLEE. Here is our simple function:

  int my_islower(int x) {
      if (x >= 'a' && x <= 'z')  
         return 1;
      else return 0;
  }

You can find the entire code for this example in the source tree under examples/islower. A version of the source code can also be accessed here.

Marking input as symbolic

In order to test this function with KLEE, we need to run it on symbolic input. To mark a variable as symbolic, we use the klee_make_symbolic() function, which takes three arguments: the address of the variable (memory location) that we want to treat as symbolic, its size, and a name (which can be anything). Here is a simple main() function that marks a variable c as symbolic and uses it to call my_islower():

  int main() {
      char c;
      klee_make_symbolic(&c, sizeof(c), "input"); 
      return my_islower(c);
  }

Compiling to LLVM bitcode

KLEE operates on LLVM bitcode. To run a program with KLEE, you first compile it to LLVM bitcode using llvm-gcc --emit-llvm. Assuming our code is stored in demo.c, we run:

llvm-gcc --emit-llvm -c -g demo.c

to generate the LLVM bitcode file demo.o. It is useful to (1) build with -g to add debug information to the bitcode file, which we use to generate source line level statistics information, and (2) not use any optimization flags. The code can be optimized later, as KLEE provides the --optimize command line option to run the optimizer internally.

Running KLEE

To run KLEE on the bitcode file simply execute:

klee demo.o

You should see the following output:

  KLEE: output directory = "klee-out-0"
  KLEE: done: total instructions = 69  
  KLEE: done: completed paths = 3      
  KLEE: done: generated tests = 3

There are three paths through our simple function, one where x is less than 'a', one where x is between 'a' and 'z' (so it's a lowercase letter), and one where x is greater than 'z'. As expected, KLEE informs us that it explored three paths in the program and generated one test case for each path explored. The output of a KLEE execution is a directory (in our case klee-out-0) containing the test cases generated by KLEE. KLEE names the output directory klee-out-N where N is the lowest available number (so if we run KLEE again it will create a directory called klee-out-1), and also generates a symbolic link called klee-last to this directory for convenience:

  $ ls klee-last/
  assembly.ll      run.istats       test000002.ktest
  info             run.stats        test000003.ktest
  messages.txt     test000001.ktest warnings.txt

Please click here if you would like an overview of the files generated by KLEE. In this tutorial, we only focus on the actual test files generated by KLEE.

KLEE-generated test cases

The test cases generated by KLEE are written in files with extension .ktest. These are binary files, which can be read with the ktest-tool utility. So let's examine each file:

  $ ktest-tool klee-last/test000001.ktest 
  ktest file : 'klee-last/test000001.ktest'
  args       : ['demo.o']
  num objects: 1
  object    0: name: 'input'
  object    0: size: 1
  object    0: data: 'b'

  $ ktest-tool klee-last/test000002.ktest 
  ...
  object    0: data: '~'

  $ ktest-tool klee-last/test000003.ktest 
  ..
  object    0: data: '\x00'

In each test file, KLEE reports the arguments with which the program was invoked (in our case no arguments other than the program name itself), the number of symbolic objects on that path (only one in our case), the name of our symbolic object ('input') and its size (1). The actual test itself is represented by the value of our input: 'b' for the first test, '~' for the second and 0 for the last one. As expected, KLEE generated a character which is a lowercase letter ('b'), one which is less than 'a' (0), and one which is greater than 'z' ('~'). We can now run these values on a native version of our program, to exercise all paths through the code!

Replaying a test case

While we can run the test cases generated by KLEE on our program by hand, (or with the help of an existing test infrastructure), KLEE provides a convenient replay library, which simply replaces the call to klee_make_symbolic with a call to a function that assigns to our input the value stored in the .ktest file. To use it, simply link your program with the libkleeRuntest library and set the KTEST_FILE environment variable to point to the name of the desired test case:

  $ gcc ~/klee/Release/lib/libkleeRuntest.dylib demo.c
  $ KTEST_FILE=klee-last/test000001.ktest ./a.out 
  $ echo $?
  1
  $ KTEST_FILE=klee-last/test000002.ktest ./a.out 
  $ echo $?
  0
  $ KTEST_FILE=klee-last/test000003.ktest ./a.out
  $ echo $?
  0

As expected, our program returns 1 when running the first test case (which contains the lowercase letter 'b'), and 0 when running the other two (which don't contain lowercase letters).