klee错误汇报二:KLEE的optimize选项的一个困惑

时间:2021-05-01 23:29:27

问题已经提交github:https://github.com/klee/klee/issues/650

在一个对命令行参数进行建模的符号执行过程中,添加optimize选项与不添加optimize选项,其执行结果完全不同。示例代码test5.c如下:

#include <stdio.h> //test5.c
#include
<string.h>
#include
<stdlib.h>

int main(int argc, char* argv[]) {
//int result = argc > 1 ? atoi(argv[1]) : 0;
// printf("result:%d\n",result);
if (argc==1) return -1;
if (argv[1][0] == '1')
{
return 1;
}
else return 0;
}
clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test5.c
klee --optimize --posix-runtime test5.bc -sym-args 0 1 3
或者
klee --optimize --posix-runtime test5.bc -sym-arg 3

我们分别看一下输出的结果:

klee错误汇报二:KLEE的optimize选项的一个困惑klee错误汇报二:KLEE的optimize选项的一个困惑

对于第二种情况,由于已经限制必须有一个参数,所以,相比于第一种情况,就是减少了一条路径。

我们分别查看两种情况的测试用例的情况:

第一种情况:

klee@ubuntu:~/kleeexperiment/modeltest$ ktest-tool klee-last/test000001.ktest
ktest file : 'klee-last/test000001.ktest'
args : ['test5.bc', '-sym-args', '0', '1', '3']
num objects: 2
object 0: name: 'n_args'
object 0: size: 4
object 0: data: '\x00\x00\x00\x00'
object 1: name: 'model_version'
object 1: size: 4
object 1: data: '\x01\x00\x00\x00'
klee@ubuntu:~/kleeexperiment/modeltest$ ktest-tool klee-last/test000002.ktest
ktest file : 'klee-last/test000002.ktest'
args : ['test5.bc', '-sym-args', '0', '1', '3']
num objects: 3
object 0: name: 'n_args'
object 0: size: 4
object 0: data: '\x01\x00\x00\x00'
object 1: name: 'arg0'
object 1: size: 4
object 1: data: '\x00\x00\x00\x00'
object 2: name: 'model_version'
object 2: size: 4
object 2: data: '\x01\x00\x00\x00'

两个测试用例执行重现的输出结果:(test5与前述test5.bc不一样,前述的是llvm生成的供klee符号执行的字节码,这里重现时使用的test5是gcc test5.c -o test5,即本地可执行代码。

klee@ubuntu:~/kleeexperiment/modeltest$ klee-replay ./test5 klee-last/test000001.ktest 
klee-replay: TEST CASE: klee-last/test000001.ktest
klee-replay: ARGS: "./test5"
klee-replay: EXIT STATUS: ABNORMAL 255 (0 seconds)
klee@ubuntu:~/kleeexperiment/modeltest$ klee-replay ./test5 klee-last/test000002.ktest
klee-replay: TEST CASE: klee-last/test000002.ktest
klee-replay: ARGS: "./test5" ""
klee-replay: EXIT STATUS: NORMAL (0 seconds)

第二种情况:

klee@ubuntu:~/kleeexperiment/modeltest$ ktest-tool klee-last/test000001.ktestktest file : 'klee-last/test000001.ktest'
args : ['test5.bc', '-sym-arg', '3']
num objects: 2
object 0: name: 'arg0'
object 0: size: 4
object 0: data: '\x00\x00\x00\x00'
object 1: name: 'model_version'
object 1: size: 4
object 1: data: '\x01\x00\x00\x00'

测试用例执行重现的输出结果:

klee@ubuntu:~/kleeexperiment/modeltest$ klee-replay ./test5 klee-last/test000001.ktest 
klee-replay: TEST CASE: klee-last/test000001.ktest
klee-replay: ARGS: "./test5" ""
klee-replay: EXIT STATUS: NORMAL (0 seconds)

可以看到,都没有覆盖下面这个分支:(注明echo $?显示的是255,其实就是-1)

if (argv[1][0] == '1')

 我一开始以为是warning中的malloc没有建模,导致出现这种情况,所以,添加了--libc=uclibc选项。为了简化分析,我将代码改为如下,脚本改为如下:结果发现,仍然不能正确覆盖该路径。

代码:

#include <stdio.h>
#include
<string.h>
#include
<stdlib.h>
int main(int argc, char* argv[]) {
if (argv[1][0] == '1')
{
return 10;
}
else return 100;
}

 脚本:

clang -I /home/klee/xiaojiework/klee/include/ -emit-llvm -c -g test5.c
klee --optimize --posix-runtime --libc=uclibc test5.bc -sym-arg 3
gcc test5.c -o test5
klee-replay ./test5 klee-last/test000001.ktest

klee错误汇报二:KLEE的optimize选项的一个困惑

仍然没有覆盖到下面这个分支。

if (argv[1][0] == '1')

测试用例重新执行程序的结果是:

klee错误汇报二:KLEE的optimize选项的一个困惑

又是在误打误撞中,我去掉了klee符号执行时的--optimize选项

脚本是:

klee --posix-runtime --libc=uclibc test5.bc -sym-arg 3 

klee错误汇报二:KLEE的optimize选项的一个困惑

两个测试用例的执行重现结果:

klee错误汇报二:KLEE的optimize选项的一个困惑

可以看到,正确地覆盖了程序的两条路径。那么为什么一个optimize有这么大的区别呢?