ubuntu12.04-32位,安装KLEE及使用工具过程中遇到的问题

时间:2021-01-26 23:29:55
1.安装klee出现的问题:
       前面都没有错,最后make check时出现:make [1]: *** [check-local] Error 1
网上查说make check运行时可能需要root权限。不对,make check不过对后面执行没有影响。不用管它,make check过不了对后面没有影响。


2.KLEE运行的第一个小例子——get_sign:
使用klee_make_symbolic()函数来标明一个函数是符号变量。
例如:
int a;
klee_make_symbolic(&a, sizeof(a), "a");
函数的三个参数分别指:变量的内存地址,大小,名字。
遇到问题:
1. klee get_sign.o报错找不到command:klee。原因是可执行的klee没有加入到PATH中,找到klee的可执行文件并加入到klee目录下的PATH中即可。export PATH=$PATH:your_path/klee/Release+Asserts/bin/

2.export LD_LIBRARY_PATH只是临时导入,电脑重启后失效。

3.例子中第五行#include<klee/klee.h>,gcc编译时报错找不到klee/klee.h.
解决方法一:编译时加入选项-I 指明库文件的位置
解决方法二:直接将相关库文件加入系统库文件的默认路径中。具体如下所述:
#gcc找到头文件的路径
#gcc找到头文件的路径
环境变量中的C_INCLUDE_PATH。

#g++找到头文件的路径
CPLUS_INCLUDE_PATH=$CPLUS_INCLUDE_PATH:/usr/include/libxml2:/MyLib
export CPLUS_INCLUDE_PATH

#找到动态链接库的路径
LD_LIBRARY_PATH=$LD_LIBRARY_PATH:/MyLib
export LD_LIBRARY_PATH

#找到静态库的路径
LIBRARY_PATH=$LIBRARY_PATH:/MyLib
export LIBRARY_PATH

     gcc编译时标准系统库可在目录 /usr/lib /lib 中找到。klee安装后其库文件没有导入到系统库文件中(不知道为什么?),手动导入例子中需要的klee目录下的头文/件到/usr/include/下(这个位置是试验很多次得出的,导入/usr/lib/和/lib/下都不行。 总结:因为在klee大文件的目录下,层级结构是这样的:klee->include->klee->下面有很多头文件,所以为了保持目录结构的一致,也把相应的头文件导入系统库文件的/usr/include/下)。

2.第二个例子——regexp:
     KLEE也会找出程序中的错误,如非法内存位置访问。这个例子中的错误不是由于程序的错误,而是我们测试驱动的错误。由于我们的符号变量re是一个字符数组,都是以'\0'结尾的,但是符号变量取到这一点,所以会报错。
     对于有些复杂程序,程序分支数是无限的。可以用control+c来强制结束。也可以用选项来限制klee的运行时间和内存使用:
  • -max-time=seconds: Halt execution after the given number of seconds.
  • -max-forks=N: Stop forking after N symbolic branches, and run the remaining paths to termination.
  • -max-memory=N: Try to limit memory consumption to N megabytes.
3.第三个例子——Solving a maze with KLEE

     是一个11*7的迷宫问题,程序中故意在迷宫的第二行开了一个后门。KLEE通过符号执行找到了所有的解(包括陷阱)。

     通过这个例子可以完全看到KLEE符号执行的过程,首先是按照符号变量的size每一个字节都是符号值,然后从第一个字节开始一个一个地试验具体值(本例中实验的顺序w->a->d->s,且这4个都会试个遍,然后保存所有可行的具体值,再次基础上在再试验第二个字节,如此下去,知道实验完所有的字节,也就找到了所有的可行路径。)