A while ago (long ago!), we showed how to solve the fruit puzzle using JPF as a symbolic execution engine (https://verificationglasses.wordpress.com/2017/02/27/jpf-fruit-puzzle/).  In this post, we are going to demonstrate how to use a different tool (KLEE) to automatically generate tests for a small example over integer numbers (in the C programming language), and in the next post, we will use KLEE to generate tests for an implementation of binary search.

The difference between symbolic execution and actually running the program, is that with symbolic execution we keep track of “symbolic values” and the operations over those values. So, if we have a program that does something like this:

int many_math_operations(int x) {
    int result = x * 2;
    result += 5;
    result /= -3;
    result *= (result+1);
    return result;
}

Then if we consider the value of the parameter x to be some unknown X, the result of this function will be:

((x*2 + 5) / -3) * (((x*2 + 5) / -3)+1)

Notice that result doesn’t appear in the expression above at all!

Symbolic execution handles conditions (if, while, do-while, for) as well. For example:

int function_with_if(int x) {
    if (x > 0) {
        return 10 / x;
    } else {
        return 10 / (x + 1);
    }
}

In the function above, symbolic execution tries to cover every possible path. For each path, it finds an input that satisfies the conditions for that path to be taken, and produces an output according to the symbolic expressions.

For the case in which X > 0, the output will be 10 / X. (I’m using uppercase to represent the symbolic value.)

For the case in which !(X > 0), the output will be 10 / (X+1).

Can you find the error?

Can klee find it?
  1. Let’s create a local file containing the function (/path_to_klee_dir/klee/function_with_if.c You can replace /path_to_klee_dir as you see fit): 
#include <klee/klee.h>
#include <stdio.h>

int function_with_if(int x) {
    printf("input: %d\n", x);
    if (x > 0) {
        return 10 / x;
    } else {
        return 10 / (x + 1);
    }
}

int main() {
  int x;
  klee_make_symbolic(&x, sizeof(x), "x");
  int result = function_with_if(x);
  printf("result = %d\n", result);
  return 1;
}

The main part indicates that x should be considered as a symbolic variable.

2. Now, let’s run KLEE as a docker container:

docker run -v /path_to_klee_dir/klee:/tmp/klee --rm -ti --ulimit='stack=-1:-1' klee/klee:2.1

Let’s now do the steps explained here for our example.

3. Compile to LLVM bytecode

cd /tmp/klee
clang -I ~/klee_src/include/  -emit-llvm -c -g -O0 -Xclang -disable-O0-optnone function_with_if.c

4. Run KLEE:

 klee --external-calls=all  function_with_if.bc

As opposed to the tutorial, here we are using the option –external-calls=all so that it doesn’t give a warning due to the use of printf.

The output is:

KLEE: ERROR: function_with_if.c:9: divide by zero
KLEE: NOTE: now ignoring this error at this location
result = 10
result = 0

KLEE: done: total instructions = 58
KLEE: done: completed paths = 3
KLEE: done: generated tests = 3

KLEE found that there is a division by 0!

5. Let’s see the test cases that were generated:

ktest-tool klee-last/test000001.ktest
ktest file : 'klee-last/test000001.ktest'
args : ['function_with_if.bc']
num objects: 1
object 0: name: 'x'
object 0: size: 4
object 0: data: b'\xff\xff\xff\xff'
object 0: hex : 0xffffffff
object 0: int : -1
object 0: uint: 4294967295
object 0: text: ….

In this test case, the value of ‘x’ as an int is -1.

You can do the same for the second and the third test case, and you’ll see that the inputs chosen are 0 and 2147483647 (which is the maximum int for 32-bit ints). It is useful that KLEE chooses these kinds of values since they allow checking for overflow behavior.

6. Let’s run the program with the different inputs and see how the program behaves:

export LD_LIBRARY_PATH=/home/klee/klee_build/lib/:$LD_LIBRARY_PATH
gcc -I ~/klee_src/include -L ~/klee_build/lib/ function_with_if.c -lkleeRuntest 
KTEST_FILE=klee-last/test000001.ktest ./a.out

The output is:

input: -1
Floating point exception (core dumped)

For the second and third test cases:

klee@d244b83fe987:/tmp/klee$ KTEST_FILE=klee-last/test000002.ktest ./a.out
input: 0
result = 10
klee@d244b83fe987:/tmp/klee$ KTEST_FILE=klee-last/test000003.ktest ./a.out
input: 2147483647
result = 0

In this post, we used KLEE for a very simple example. In the next post, we will use KLEE to automatically generate tests for binary search.

Advertisement