KLEE简单使用

针对待测试的程序，KLEE提供两种方式为每条路径生成合适的测试用例。

方式一

待测试程序如下所示：

其中，待测试程序路径为“/home/klee/klee_src/example/get_sign/ge_sign.c”。我们想要知道KLEE执行时，变量a的可能取值，需要引入“klee.h”头文件，此文件存放于KLEE构建文件下的include文件夹下的klee文件夹下，本文环境路径为“/home/klee/klee_src/include/klee/klee.h”。然后在变量a定义后，添加“klee_make_symbolic(&a,size(a),“a”)”语句，KLEE执行是可以在此处插桩，从而得到不同路径下a的可能取值。

1.1测试用例生成

#使用clang生成get_sign.bc文件，使用-I选项以链接“klee.h”
clang -I /home/klee/klee_src/include -emit-llvm -c get_sign.c
#使用KLEE进行符号执行
klee --libc=uclibc --posix-runtime --output-dir=xxx get_sign.bc
1
2
3
4

如果不添加“–output-dir”选项，则默认生成“klee-out-0”文件夹，相关测试用例等信息文件均存在于此文件中。如果添加此选项，会生成相应名称的文件夹。
KLEE执行完毕，生成下图的结果

可以看出，KLEE检测出三条执行路径，并生成3个测试用例，分别为test000001.ktest、test000002.ktest和test000003.ktest。

1.2 查看测试用例

使用ktest-tool工具查看测试用例



然而，我们单从这个结果来看，无法确定其对应哪个分支，需要使用KLEE提供的工具来运行测试用例。

1.3 测试用例运行

export LD_LIBRARY_PATH=/home/klee/klee_build/lib/:$LD_LIBRARY_PATH
#生成二进制文件，生成a.out文件
clang -I /home/klee/klee_src/include -L /home/klee/klee_bulid/lib/ get_sign.c -lkleeRuntest
KTEST_FILE=klee-last/test000001.ktest ./a.out
echo $?
1
2
3
4
5

其中，test000002.ktest返回255，这是因为-1被转换为无符号数255。

方式二

待测试程序如下，名称为‘test.c’

#使用clang生成test.bc文件，使用-I选项以链接“klee.h”
clang -emit-llvm -c test.c
#使用KLEE进行符号执行
klee --libc=uclibc --posix-runtime --output-dir=sym1 test.bc --sym-arg 1
1
2
3
4

其中，‘–sym-arg’选项用于指定参数输入的长度，此处设为1

1.2 查看测试用例

使用ktest-tool工具查看测试用例

1.3 测试用例运行

#生成二进制文件，生成a.out文件
clang test.c
klee-replay ./a.out sym1/test000001.ktest
1
2
3

可以看出，生成的测试用例分别遍历了两条路径。
至此，KLEE使用已完成。