在上一篇文章中，我们介绍了 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);
}