Select Git revision
get_sign.c 6.57 KiB
/*
* 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]
// Yes
// echo $? gives 255 (which is equal to -1 of 8 signed bits)
//
// Why not? Confer to shell error codes:
//
// [your answer here]
// ??? TODO
//
// 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 == o 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)
//
// 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)