2

对于带有符号参数的循环，我有一个关于 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-depth= 200

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

我发现它发生在选项时发生 - 当它没有相同的行为时，使用时式。有人知道 Klee 的 --optimize 是如何工作的吗？

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

提前致谢

4

1 回答 1

0

我想知道为什么使用选项 --optimize 会出现这种不同的行为。谢谢

在 C/C++ 中有“未定义行为”的概念（请参阅：C 和 C++ 中未定义行为指南，第 1 部分，第 2部分，第 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

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

溢出循环-O1.s：

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

溢出循环-O2.s：

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

我建议您在不同的优化级别（gcc -S -O0vs gcc -S -O1... -O3）上检查代码的汇编。再一次，关于主题的好帖子： [1]， [2]， [3]， [4]， [5]， [6]。

于 2012-10-18T10:46:32.843 回答