- -

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 get_sign(int x) {
-    if (x == 0)
-       return 0;
-
-    if (x < 0)
-       return -1;
-    else 
-       return 1;
-  }

- - 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 get_sign(): - -

-  int main() {
-      int a;
-      klee_make_symbolic(&a, sizeof(a), "a");
-      return get_sign(a);
-  }

- - - -

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 get_sign.c, - we run: - -

- llvm-gcc --emit-llvm -c -g get_sign.c -

- - to generate the LLVM bitcode file get_sign.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 get_sign.o -

- - You should see the following output (assumes LLVM 2.8): -

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

- - 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 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 --write-ints klee-last/test000001.ktest 
-  ktest file : 'klee-last/test000001.ktest'
-  args       : ['get_sign.o']
-  num objects: 1
-  object    0: name: 'a'
-  object    0: size: 4
-  object    0: data: 1
-  
-  $ ktest-tool --write-ints klee-last/test000002.ktest  
-  ...
-  object    0: data: -2147483648
-
-  $ ktest-tool --write-ints klee-last/test000003.ktest 
-  ...
-  object    0: data: 0

- - 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: - -

-  $ export LD_LIBRARY_PATH=path-to-klee-root/Release+Asserts/lib/:$LD_LIBRARY_PATH
-  $ gcc -L path-to-klee-root/Release+Asserts/lib/ get_sign.c -lkleeRuntest
-  $ KTEST_FILE=klee-last/test000001.ktest ./a.out 
-  $ echo $?
-  1
-  $ KTEST_FILE=klee-last/test000002.ktest ./a.out 
-  $ echo $?
-  255
-  $ KTEST_FILE=klee-last/test000003.ktest ./a.out
-  $ echo $?
-  0

- - As expected, our program returns 1 when running the first test case, - 255 (-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. - -

- -