T3-6 - 循环语句的符号执行

符号执行简单while循环

一般而言，每个循环语句应当配有一个循环不变量。

int slow_sub(int x, int y)
  /*@ Require
        0 <= x && x <= 100 && 
        0 <= y && y <= 100
      Ensure
        __return == x - y
   */
{
  /*@ Inv Assert
        y >= 0 &&
        y - x == y@pre - x@pre &&
        0 <= x@pre && x@pre <= 100 && 
        0 <= y@pre && y@pre <= 100
   */
  while (y != 0) {
    x --;
    y --;
  }
  return x;
}

上面例子中，标注在while循环语句开头的循环不变量表示：每次判定循环条件y != 0是否成立之前，这个程序状态总是满足这个断言。相应的，在符号执行第一次进入循环时，在判定while循环条件之前，QCP就会符号执行这个断言标注；并且之后循环体执行结束后（相当于等待判定while循环判定条件以再次进入循环之前），还要再符号执行这个断言。以上这些环节中，while循环的符号执行步骤与实际程序执行步骤是类似的。不过，两者之间不同的是，符号执行过程中，不会再次符号执行while循环的判定条件也不会再次进入循环体的符号执行。换言之，实际的程序执行中上面while循环的循环体会被反复执行，但是在符号执行中上述循环的循环体只会被符号执行一次。下面两图对比了符号执行与实际程序执行的差别。

从图上可以看出，前述while循环语句的符号执行包含两个分支，一个分支对应while循环判定条件为真，是循环体的符号执行，一个分支对应while循环判定条件为假，是循环后续语句的符号执行。

在尚未完全完成循环代码开发时查看符号执行结果

使用QCP时，不用写完完整的循环，就可以查看当前的符号执行结果。以下是三次查看的结果，以及这些符号执行结果与控制流图之间的关系。

首先是编程输入while循环条件之后的情况。

其次是输入循环体中第一句语句x --;之后的情况。

再是输入循环体中第二句语句y --;之后的情况。

最后，当输入表示循环体结束的右花括号之后，QCP中就能查看整个循环的符号执行结果。

符号执行简单for循环

C程序的for语句包含一个初始化表达式，条件表达式和一个更新表达式。在QCP中for循环的循环不变式表示每次进行for循环条件判定之前程序状态共同满足的性质。值得一提的是，由于进入for时会先执行初始化表达式再判定for循环条件是否成立，所以QCP并不要求执行for语句之前的程序状态满足其循环不变量，但是要求执行for语句初始化表达式之后的程序状态要满足循环不变量。

int slow_sub_for(int x, int y)
  /*@ Require
        0 <= x && x <= 100 && 
        0 <= y && y <= 100
      Ensure
        __return == x - y
   */
{
  int i;
  /*@ Inv Assert
        y == y@pre && i >= 0 && i <= y &&
        x == x@pre - i &&
        0 <= x@pre && x@pre <= 100 && 
        0 <= y@pre && y@pre <= 100
   */
  for (i = 0; i < y; ++ i) {
    x --;
  }
  return x;
}

上面例子中，标注在for循环语句开头的循环不变量表示：每次判定循环条件i < y是否成立之前，这个程序状态总是满足这个断言。在for语句执行之前，程序状态其实是不满足这个断言的，在QCP中查看相关符号执行信息也可以看到这一点。

进入for循环前，程序变量i还没有被初始化，QCP的符号执行结果用has_permission(&i)描述了这一“未初始化”状态。这显然无法推出i >= 0 && i <= y。而在初始化i = 0之后，程序状态就满足了这个断言了。

处理for语句时，QCP的符号执行会先符号执行它的初始化表达式，然后符号执行循环不变量断言，之后再符号执行for循环条件判定表达式，生成验证条件。此后，用循环条件判定表达式条件为真的结果符号执行循环体以及for语句的更新表达式；用循环条件判定表达式条件为假的结果符号执行循环之后的语句。这与while循环的符号执行类似。

符号执行do-while循环

int countTo10()
  /*@ Require
        emp
      Ensure
        __return == 10
   */
{
  int y = 0;
  do {
    y ++;
  }
  /*@ Inv Assert y <= 10 */
  while (y != 10);
  return y;
}

要验证C语言中的do-while循环，QCP要求在do-while循环体之后do-while判定条件之前标注循环不变量断言，表示每次进行do-while循环条件判定之前程序状态共同满足的性质。处理do-while语句时，QCP的符号执行会先符号执行循环体，然后符号执行循环不变量断言，生成验证条件，之后再符号执行do-while循环条件判定表达式。此后，QCP的符号执行会第二次符号执行循环体，并第二次符号执行循环不变量断言再生成一个验证条件。

符号执行带有break、continue语句的循环

C语言的循环语句中可以包含break、continue和return语句改变控制流。QCP处理return语句的方式之前我们已经介绍过，下面例子中是一个包含break的while循环语句。

int while_break(int x, int y)
  /*@ Require
        0 <= x && x <= 100 && 
        0 <= y && y <= 100
      Ensure
        0 <= __return && __return <= 100
   */
{
  /*@ Inv Assert
        x <= 100 && y <= 100 && x >= 0 && y >= 0
   */
  while (x < 100) {
    ++ x;
    if (y == 100) {
      break;
    }
    ++ y;
  }
  return x + y - 100;
}

QCP的符号执行会将break语句的符号执行结果与循环条件判定条件为假的符号执行结果合并在一起，作为整个while循环语句的符号执行结果。

而在符号执行循环体的过程时，如果遇到break语句，QCP不会生成它的normal条件，而只会生成它的break条件。如下图所示。

如果符号执行到循环体的其他分支，在QCP中既可以看到所在分支的normal条件，也可以看到循环体整体的break条件。如下面所示。

continue语句的符号执行与break类似，在循环体的符号执行过程中，QCP也会收集并向用户展示continue条件。另外，QCP也会检查continue条件是否可以推出循环不变量。