QCP Tutorials 符号执行

Shanghai Jiao Tong University Cao Qinxiang Research Group

T3-5 · 符号执行

符号执行遇到断言标注的情况

QCP工具允许用户在程序语句间添加断言标注辅助验证的完成。前面曾经提到的循环不变量就是一种这样的断言标注。当QCP符号执行器遇到断言标注时，就会检查先前由符号执行得到的最强后条件是否可以推出用户手动输入的断言。

swap函数中增加断言标注后的符号执行

以前面曾经介绍过的swap函数为例。

void swap(int * px, int * py)
/*@ With x y
    Require store_int(px, x) * store_int(py, y)
    Ensure store_int(px, y) * store_int(py, x) */
{
  int t;
  t = * px;
  * px = * py;
  * py = t;
}

第一条赋值语句执行后，程序状态满足下面断言（这也是QCP符号执行器会得到的最强后条件）：

store_int(&t, x) *
store_ptr(&px, px_37) *
store_ptr(&py, py_40) *
store_int(px_37, x) *
store_int(py_40, y)

其中，px_37和py_40表示px@pre和py@pre这两个初始值。当然，我们看了后续程序，我们知道此时* px存储的值是没有用的。下面我们就在这个程序点上断言了这个弱一些的性质。

void swap(int * px, int * py)
/*@ With x y
    Require store_int(px, x) * store_int(py, y)
    Ensure store_int(px, y) * store_int(py, x) */
{
  int t;
  t = * px;
  /*@ Assert
        store_int(&t, x) *
        store_ptr(&px, px@pre) *
        store_ptr(&py, py@pre) *
        has_int_permission(px@pre) *
        store(py@pre, y) */
  * px = * py;
  * py = t;
}

添加这条断言就表示“程序执行到此处时程序状态必定满足此性质”，并且后续程序语句的正确性也仅仅由此性质保障。换言之，哪怕我们实际可以论证程序执行到此处时满足更强的性质，后续程序语言的验证也无需用到更强的性质。因此，如果QCP在验证过程中遇到这样带标注的程序，就会生成一条下面这样的验证条件，并且基于用户给出的断言进行后续的符号执行。

store_int(&t, x) *
store_ptr(&px, px_37) *
store_ptr(&py, py_40) *
store_int(px_37, x) *
store_int(py_40, y)
|-- store_int(&t, x) *
    store_ptr(&px, px_37) *
    store_ptr(&py, py_40) *
    has_int_permission(px_37) *
    store_int(py_40, y)

下面两图中可以看到符号执行该断言前后的对比。符号执行该断言之后，Normal断言列表中显示了断言标注中引入的has_permission谓词。

image-3-5-1
image-3-5-1
image-3-5-2
image-3-5-2

符号执行if语句后的断言标注

下面max3函数计算了三个整数的最大值。

int max3(int x, int y, int z)
/*@ Require emp
    Ensure __return >= x &&
           __return >= y &&
           __return >= z */
{
  int t;
  if (x < y) {
    t = y;
  }
  else {
    t = x;
  }
  /*@ Assert t >= x@pre && t >= y@pre &&
             x == x@pre && y == y@pre && z == z@pre */
  if (t < z) {
    return z;
  }
  else {
    return t;
  }
}

该函数包含两个if语句，我们已经熟悉，符号执行完第一个if语句后，会得到两条Normal断言：

image-3-5-3
image-3-5-3

现在，如果符号执行这条if语句之后的断言标注，那么就会生成两个验证条件，即需要检验上面两条Normal断言都能推出这条手动插入的断言。以下是两个验证条件，断言都已经用基本分离逻辑断言表示，其中x_54、y_51与z_48分别是三个形参的初始值。

x_54 < y_51 &&
store_int(&t, y_51) *
store_int(&x, x_54) *
store_int(&y, y_51) *
store_int(&z, z_48)
|--
exists t_64,
t_64 >= x_54 &&
t_64 >= y_51 &&
store_int(&t, t64) *
store_int(&x, x_54) *
store_int(&y, y_51) *
store_int(&z, z_48)

x_54 >= y_51 &&
store_int(&t, y_51) *
store_int(&x, x_54) *
store_int(&y, y_51) *
store_int(&z, z_48)
|--
exists t_64,
t_64 >= x_54 &&
t_64 >= y_51 &&
store_int(&t, t64) *
store_int(&x, x_54) *
store_int(&y, y_51) *
store_int(&z, z_48)

符号执行该断言标注后，QCP的符号执行其将只使用这一条Normal断言进行后续的符号执行，而不再保留两个分支。

image-3-5-4
image-3-5-4