klee使用类似代码的循环奇怪的行为

Question

我有一个问题，在使用符号参数的循环情况下，KLEE (符号执行工具)是如何工作的：

int loop(int data) {
  int i, result=0;
  for (i=0;i<data ;i++){   
     result+= 1;
     //printf("result%d\n", result); //-- With this line klee give different values for data
}
   return result;
}
void main() {
  int n;
  klee_make_symbolic(&n, sizeof(int),"n");  
  int result=loop(n) ;
}

如果我们用这段代码执行klee，它只给出一个测试用例。但是，如果我们去掉printf(...)的注释，klee将需要某种类型的控件来停止执行，因为它将生成n：--max- need = 200的值

我想知道为什么klee会有这种不同的行为，这对我来说是没有意义的。为什么我在这段代码中没有printf，它就不会产生相同的值。

我发现，当使用--optimize选项时会发生这种情况，而它不存在相同的行为。有人知道Klee的--optimize是怎么工作的吗？

另一个关于同样的问题是，如果在他们发表的论文中，据我所知，他们说他们的启发式搜索将使它不是无限的(他们使用避免饥饿)，因为我让它运行不停止，这是真的，应该在这个循环的情况下完成klee执行吗？

提前感谢

Answer 1

我想知道的是，为什么这种不同的行为与--

选项不同。谢谢

在C/C++中有“未定义行为”的概念(参见:A Guide to Undefined Behavior in C and C++，Part1，Part 2，Part 3，每个C程序员都应该知道关于未定义行为[#1/3]，[#2/3]，[#3/3]的内容)。

signed整数溢出被定义为未定义的行为，以便允许编译器进行如下优化：

bool f(int x){ return x+1>x ? true : false ; }

让我们想想..。正规代数中的x+1>x总是真的，在这个模代数中几乎总是真的(除了溢出的一种情况)，所以让我们把它变成：

true

这样的实践使得大量的优化成为可能。(顺便说一下。如果您想在溢出时定义行为，请使用unsigned整数-此功能在密码算法实现中广泛使用)。

另一方面，有时会产生令人惊讶的结果，如下面的代码：

int main(){
    int s=1, i=0;
    while (s>0) {
        ++i;
        s=2*s;
    }
    return i;
} 

被优化成无限循环。这不是虫子！这是一个强大的功能！(再一次..对于已定义的行为，请使用unsigned)。

让我们为上面的例子生成汇编代码：

$ g++ -O1 -S -o overflow_loop-O1.s overflow_loop.cpp
$ g++ -O2 -S -o overflow_loop-O2.s overflow_loop.cpp

循环部分的检查以不同的方式编译：

overflow_loop-O1.s：

(...)
.L2:
    addl    $1, %eax
    cmpl    $31, %eax
    jne    .L2
(...)

overflow_loop-O2.s：

(...)
.L2:
    jmp    .L2
(...)

我建议你在不同的优化级别上检查代码的汇编(gcc -S -O0 vs gcc -S -O1...-O3)。再说一次，关于主题的帖子很不错：[1]，[2]，[3]，[4]，[5]，[6]。