+ +

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;
+  }

+ + +

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  messages.txt  run.stats        test000002.bout  warnings.txt 
+  info         run.istats    test000001.bout  test000003.bout

+ + 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 .bout. These are + binary files, which can be read with the klee-bout-tool + utility. So let's examine each file: + +

+  $ klee-bout-tool klee-last/test000001.bout 
+  bout file  : 'klee-last/test000001.bout'
+  args       : ['demo.o']
+  num objects: 1
+  object    0: name: 'input'
+  object    0: size: 1
+  object    0: data: 'b' 
+
+  $ klee-bout-tool klee-last/test000002.bout 
+  ...
+  object    0: data: '~'
+ 
+  $ klee-bout-tool klee-last/test000003.bout 
+  ...
+  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 driver, 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 .bout file: + +

+  $ gcc ...

+ + +