Testing a Small Function
This tutorial walks you through the main steps needed to test a simple function with KLEE. Here is our simple function:
You can find the entire code for this example in the source tree under
examples/get_sign. 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 a as symbolic and uses it to call
Compiling to LLVM bitcode
KLEE operates on LLVM bitcode. To run a program with KLEE, you first compile it to LLVM bitcode using
From within the
which should create a
get_sign.bc file in LLVM bitcode format. The -I argument is used so that the compiler can find klee/klee.h, which contains definitions for the intrinsic functions used to interact with the KLEE virtual machine. 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.
NOTE: If you have built KLEE with LLVM 2.9, replace
llvm-gcc. Notice that
.o files (e.g.
get_sign.o), so you need to modify the commands accordingly.
To run KLEE on the bitcode file simply execute:
You should see the following output (assumes LLVM 2.8):
There are three paths through our simple function, one where a is
0, one where it is less than
0 and one where it is greater than
0. 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
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:
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:
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 (
'a') and its size (
4). The actual test itself is represented by the value of our input:
1 for the first test,
-2147483648 for the second and
0 for the last one. As expected, KLEE generated value
0, one negative value (
-2147483648), and one positive value (
1). 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:
As expected, our program returns
1 when running the first test case,
-1 converted to a valid exit code value in the
0-255 range) when running the second one, and
0 when running the last one.