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

问题已经提交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==) return -;

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

    {

    return ;

    }

    else     return ;

}

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@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

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

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

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

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

脚本是：

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

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

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