T1-1 - 描述C函数安全性的规约标注

在验证一个C函数时，我们需要在这个C函数的开头以标注的形式说明该函数的规约，即它的安全性或功能正确性描述。一个C函数的规约包括一个逻辑参数列表（With）和该函数对应的分离逻辑的前后条件（Require、Ensure）。在一些简单的情况中，规约可以不包含With列表。

例子1：两数相加

例如，下面C函数将两个有符号整数参数相加并返回（可以在simple_arith/add.c中找到）。

int add(int x, int y)
  /*@ Require
        0 <= x && x <= 100 && 
        0 <= y && y <= 100
      Ensure
        __return == x + y
   */
{
  int z;
  z = x + y;
  return z;
}

在这段代码中，Require条件说的是：这个add函数的两个参数都在0与100之间；Ensure条件说的是：这个函数的返回值是两个参数的和。它们两个条件一起构成了这个C函数的规约，这个规约说的是：如果它的两个参数都在0与100之间，那么这个C函数就能保证安全运行，并且会返回这两个参数的和。这里所说的“保证安全运行”指的是不会出现C标准规定的undefined behavior（简称UB），典型的UB包括除数为零、有符号整数运算越界、数组内存读写越界、空指针解引用等。由于C标准规定有符号整数运算越界是UB，上面这个例子中限制两个参数的取值范围是必要的。也就是说，上面的C函数并不满足下面规约

int add(int x, int y)
  /*@ Require
        True
      Ensure
        __return == x + y
   */

当然，上面的约束范围可以如下放宽一些。

int add_tight(int x, int y)
  /*@ Require
        INT_MIN <= x + y && x + y <= INT_MAX
      Ensure
        __return == x + y
   */
{
  int z;
  z = x + y;
  return z;
}

另外值得一提的是，在Ensure断言中的x与y表示的是它们传入该函数时候的值。因此，下面这个C函数满足同样的规约。

int add_alter1(int x, int y)
  /*@ Require
        0 <= x && x <= 100 && 
        0 <= y && y <= 100
      Ensure
        __return == x + y
   */
{
  x = x + y;
  return x;
}

当然，不做变量赋值，直接计算结果并返回的C函数自然也满足同样的规约。

int add_alter2(int x, int y)
  /*@ Require
        0 <= x && x <= 100 && 
        0 <= y && y <= 100
      Ensure
        __return == x + y
   */
{
  return x + y;
}

例子2：内存存储的修改

下面例子中，C函数的传入参数是一个地址，C函数对该地址上的值做了修改（可以在simple_arith/add.c中找到）。

void add1_ptr(int * x)
{
  * x ++;
}

要描述函数返回时* x的值与其原先数值之间的关系，就需要借助一个With变量。

void add1_ptr(int * x)
/*@ With (v: Z)
    Require (INT_MIN <= v) && (v < INT_MAX) &&
            * x == v
    Ensure * x == v + 1 */

这一规约说的是：对于任意满足INT_MIN <= v && v < INT_MAX的整数v，如果执行该C函数前地址x上存储的是v，那么这个函数就保证会安全执行，并且函数返回时x地址上存储的数会变为v + 1。换言之，这里的With表示了“任意”的意思。请注意，Ensure条件中的形参x表示的是x在传入该函数时候的值，而* x不是指x地址上最初时候的值，而是在函数调用结束时候该地址的值。具体而言，形参本身代表其传入函数时的值，而其他运算特别是代表解引用的星号表示在函数返回时候读取内存的结果。