在上一篇文章中,我们介绍了 cbmc 的架构,还有 cbmc 处理程序的步骤。

cbmc 的处理步骤

  1. 前端处理,获得程序的 cfg
  1. 展开 unwind cfg,获得路径的公式
  2. 利用 SAT/SMT 求解公式

这篇文章,将探讨 cbmc 如何处理循环程序。

Iteration-based Unwinding

1
2
3
4
5
int main(int argc, char **argv) {
while(cond) {
BODY CODE
}
}

对于上述的循环,展开其实很简单,假设我们展开五次,就可以得到下面的程序👇:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
int main(int argc, char **argv) {
if(cond) {
BODY CODE COPY 1
if(cond) {
BODY CODE COPY 2
if(cond) {
BODY CODE COPY 3
if(cond) {
BODY CODE COPY 4
if(cond) {
BODY CODE COPY 5
}
}
}
}
}
}

在很多情况下,cbmc 可以自己决定展开的上限,即使程序中循环可能可能执行的次数并不是一个常量。

1
2
3
4
5
6
7
8
_Bool f();

int main() {
for(int i = 0; i < 100; i++) {
if(f()) break;
}
assert(0);
}