Symbolic Execution using Klee
How to enumerate execution Paths?
Steps
(If you don't have Klee already running, check the second section first)
1- Run the following command
export LD_LIBRARY_PATH=path_to_/klee/Release+Asserts/lib/:$LD_LIBRARY_PATH
2- Place your file.c in folder dir/
3- Create two folders gcov_bld/ and llvm_bld/ inside dir/
4- Go to llvm_bld/ and run the following commands:
3- Create two folders gcov_bld/ and llvm_bld/ inside dir/
4- Go to llvm_bld/ and run the following commands:
cd llvm_bld
llvm-gcc --emit-llvm -I Path_to_Klee_dir/include/ -c -g ../file.c
klee --only-output-states-covering-new --write-cvcs file.o
The second command generates file.o.
The third command generates klee-last/ folder containing klee test cases (.ktest), and the option --write-cvcs results into .cvc files which are the constraints for each execution path.
cd gcov_bldThe second command generates a.out
gcc -L Path_to_Klee_dir/Release+Asserts/lib/ -I Path_to_Klee_dir/include/ -fprofile-arcs -ftest-coverage ../file.c -lkleeRuntest
KTEST_FILE=../llvm_bld/klee-last/test000001.ktest ./a.out
gcov ../file.c
The third command generates file.gcda and file.gcno
The last command generates file.c.gcov which shows the executed C-code lines
Run the last two (or three) commands for each .ktest file.
My Setup
- The mentioned commands ran successfully on Ubuntu 32-bits machine.
- I downloaded the self-contained package from http://klee.llvm.org/GetStarted.html#cde (and followed ReadMe instructions)
- I located my folder /dir in the examples folder of klee
- Make sure that libkleeRuntest.dylib exists in /klee/Release+Asserts/lib/
- I copied libkleeRuntest.so into my /gcov_bld
- The -sym-arg option didn't work properly with me, so I used klee_make_symbolic() (check the references below)
