get_sign.c

/*
 * First KLEE tutorial: testing a small function
 * https://klee.github.io/tutorials/testing-function/
 */

#include <klee/klee.h>

int get_sign(int x)
{
    if (x == 0)
        return 0;

    if (x < 0)
        return -1;
    else
        return 1;
}

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

// A) Compiling into LLVM bitcode
// > clang -emit-llvm -c get_sign.c
//
// Now you can run Klee on your generated bitcode.
//
// > klee get_sign.bc
//
// [your answer here]
// KLEE: Using Z3 solver backend
// 
// KLEE: done: total instructions = 31
// KLEE: done: completed paths = 3
// KLEE: done: generated tests = 3
// 
//
// B) Inspecting the output
//
// > ls klee-last/
//
// [your answer here]
// assembly.ll  info  messages.txt  run.istats  run.stats
// test000001.ktest  test000002.ktest  test000003.ktest  warnings.txt
//
// C) Inspecting the generated test cases
//
// > ktest-tool klee-last/test000001.ktest
//
// What path in the code does this test represent?
//
// [your answer here]
// ktest file : 'klee-last/test000001.ktest'
// args       : ['get_sign.bc']
// num objects: 1
// object 0: name: 'a'
// object 0: size: 4
// object 0: data: b'\x00\x00\x00\x00'
// object 0: hex : 0x00000000
// object 0: int : 0
// object 0: uint: 0
// object 0: text: ....
//
// It represent the path where x = 0 and the return value is 0.
// 
//
// > ktest-tool klee-last/test000002.ktest
//
// What path in the code does this test represent?
//
// [your answer here]
// ktest file : 'klee-last/test000002.ktest'
// args       : ['get_sign.bc']
// num objects: 1
// object 0: name: 'a'
// object 0: size: 4
// object 0: data: b'\x01\x01\x01\x01'
// object 0: hex : 0x01010101
// object 0: int : 16843009
// object 0: uint: 16843009
// object 0: text: ....
//
// It represent the path where x > 0 and the return value is 1.
//
//
// > ktest-tool klee-last/test000003.ktest
//
// What path in the code does this test represent?
//
// [your answer here]
// ktest file : 'klee-last/test000003.ktest'
// args       : ['get_sign.bc']
// num objects: 1
// object 0: name: 'a'
// object 0: size: 4
// object 0: data: b'\x02\x01\x01\x80'
// object 0: hex : 0x02010180
// object 0: int : -2147417854
// object 0: uint: 2147549442
// object 0: text: ....
//
// It represent the path where x < 0 and the return value is -1.
//
//
// D) Replaying a test case
//
// Fist check that includes were installed:
// > ls /usr/local/include
// klee
//
// > ls /usr/local/lib
// klee  libkleeRuntest.so  libkleeRuntest.so.1.0
//
// If you installed Klee using the package manager
// the path might be different:
//
// Using `aur` (arch) files are stored in the system default
// folders, `/usr/include` and `/usr/lib`.
//
// If those are ok, then you can compile for replay:
//
// > clang -I /usr/local/include/ -L /usr/local/lib get_sign.c -l kleeRuntest
//
// Or just
// > clang get_sign -l kleeRuntest
//
// If the `include` and `lib` paths are the system defaults.
//
// To replay the first test:
//
// We need to add the libary path so it can be dynamically loaded:
// Depending on shell this might look different:
//
// Under `bash` (and `bash` like shells)
// > export LD_LIBRARY_PATH=/usr/local/lib/:$LD_LIBRARY_PATH
//
// Under `fish`
// > set -x LD_LIBRARY_PATH /usr/local/lib/:$LD_LIBRARY_PATH
//
// Once again, if using the system default system folders
// you don't need to add anything to `LD_LIBRARY_PATH`.
//
// > KTEST_FILE=klee-last/test000001.ktest ./a.out
//
// Now let's inspect the status (return code), in `bash`:
// $? is the return value (error code) as seen by the shell.
//
// > echo $?
//
// In `fish` you would do
//
// > echo $status
//
// Did the result correspond to the expected path for the test?
//
// [your answer here]
// yes
// echo $?  gives  0
//
// > KTEST_FILE=klee-last/test000002.ktest ./a.out
//
// Inspect the return code:
//
// Did the result correspond to the expected path for the test?
//
// [your answer here]
// Yes
// echo $?  gives  1
//
// > KTEST_FILE=klee-last/test000003.ktest ./a.out
//
// Inspect the return code:
//
// Did the result correspond to the expected path for the test?
//
// [your answer here]
// No
// echo $?  gives 255 
//
// Why not? Confer to shell error codes:
//
// [your answer here]
// In bash exit code 255 means "Exit status out of range" and it says "exit takes only integer args in the range 0 - 255". The result should have been -1 but it is out of range for bash, so that is why I didn't get the expected result.
//
// D) Debugging
//
// In the above example its kind of hard to see exactly
// what happens. Using `gdb` you single step the program.
//
// First build it with debug symbols (`-g`).
// > clang -g -I /usr/local/include/ -L /usr/local/lib get_sign.c -l kleeRuntest
//
// Or if using system defaults:
// > clang -g get_sign.c -l kleeRuntest
//
// Then start `gdb`:
// > KTEST_FILE=klee-last/test000001.ktest gdb ./a.out
// (gdb) break get_sign
//
// (gdb) run
//
// Now we can inspect the `x` argument by:
// (gdb) print x
//
// What value do you get, and why?
//
// [your answer here]
// (gdb) print x
// $1 = 0
// It has the value 0 and it got that because the constraint x == 0 is the fist split in the paths. 
//
// Step the code
// > (gdb) next
//
// What path did it take, and why?
//
// [your answer here]
// Breakpoint 1, get_sign (x=0) at get_sign.c:10
// 10	    if (x == 0)
// (gdb) next
// 11	        return 0;
// It took the path where it returns 0.
// It took that path because x = 0 thus x == 0.
//
// Now we can try with another test:
//
// (gdb) set environment KTEST_FILE=klee-last/test000002.ktest
//
// And (re-start) the debug session:
// (gdb) run
//
// Step through the code.
//
// Which path did it take, and why?
//
// [your answer here]
// Breakpoint 1, get_sign (x=16843009) at get_sign.c:10
// 10	    if (x == 0)
// (gdb) next
// 13	    if (x < 0)
// (gdb) next
// 16	        return 1;
// It took the path where it returns 1.
// It took that path because x = 16843009 thus x != 0 and x !< 0.
//
//
// And finally:
//
// (gdb) set environment KTEST_FILE=klee-last/test000003.ktest
//
// Which path did it take, and why?
//
// [your answer here]
// Breakpoint 1, get_sign (x=-2147417854) at get_sign.c:10
// 10	    if (x == 0)
// (gdb) next
// 13	    if (x < 0)
// (gdb) next
// 14	        return -1;
// It took the path where it returns -1.
// It took that path because x = -2147417854 thus x != 0 and x < 0.
//
// E) Under the hood.
//
// Explain in your own words how
// `klee_make_symbolic(&a, sizeof(a), "a");`
// works when you run `klee` to generate test cases:
//
// [your answer here]
// (hint, mark memory region as symbolic)
// Klee creates a symbol for the variable 'a', the symbol doesn't have any value. Instead it has constraints that are added to it when the paths branch. In the code example above the first if statement gives two paths. The first path has the condition 'a == 0' and the other path condition 'a != 0'.  Then if we had another if statement in the fist path that has the condition 'a > 0', it would always be false because 'a' can't be 'a = 0 && a > 0'. Thus the inside of that if statement would be unreachable.
//
//
//
// Explain in your own words how
// `klee_make_symbolic(&a, sizeof(a), "a");`
// works when you replay test cases:
//
// [your answer here]
// (hint, KTEST_FILE points to a concrete assignment
// of the memory region)
// It works by loading in the constrains for the path and then generating a value that satisfies that path. After that it runs the code with the generated value and checks that all the constraints are the same as before. If they are not it means that something has changed with the path and thus the behavior of the code has changed.
//