QCP Tutorials 断言扩展与自动变换

struct int_pair {
    int a;
    int b;
};

Definition store_int_pair (p: addr) (x y: Z): Assertion :=
  &(p # "int_pair" ->ₛ "a") # Int |-> x **
  &(p # "int_pair" ->ₛ "b") # Int |-> y.

不过，之前为了在程序验证中处理这样的结构体，我们需要在程序中通过添加断言标注的方式显式地展开相关谓词。有时，这对于程序验证来说并不方便。QCP允许用户定制策略，在符号执行中根据规定的特定情形自动地进行分离逻辑断言变换。利用这一功能，当断言中出现store_int_pair(p, x, y)，而当前又要对p -> a或者p -> b做读写时，就不必再手动插入断言把它展开成两个store谓词了。

用.strategies文件定制断言变换策略

在QCP中，这样的按需断言变换策略是通过.strategies文件来定义的，.strategies文件可以和.h文件相互引用。在.h文件中，我们先声明C程序中要使用的结构体int_pair，然后通过Extern Coq声明我们在Rocq中自定义的分离逻辑谓词store_int_pair。最后，通过include strategies指令引用.strategies文件，表示将来在C程序的符号执行中要加载这个文件中的断言变换策略。反过来，.strategies文件中也可以通过#include指令引用.h文件，这样就可以在策略中使用.h文件中定义的结构体类型和自定义谓词。

// swap_simple2.h
struct int_pair {
    int a;
    int b;
};

/*@ Extern Coq (store_int_pair : Z -> Z -> Z -> Assertion) */
/*@ include strategies "swap_simple2.strategies" */

// swap_simple2.strategies
#include "swap_simple2.h"

id : 0
priority : core(1)
left : store_int_pair(?p, ?x, ?y) at 0
right : store(field_addr(?p, int_pair, a), I32, ?v) at 1
action : left_erase(0);
         right_erase(1);
         left_add(store(field_addr(p, int_pair, b), I32, y));
         right_add(v == x);

上面我们展示了一个自定义的断言变换策略，其中id是这个策略的编号，priority是它的优先级，这个数字越小就越优先。这个策略它说的是：如果当前符号执行的语句要读取p->a所需的那块内存，但是当前断言中没有形如store_int(&(p -> a), ...)的子句但是有store_int_pair(p, x, y)这个整体谓词，那么就告诉符号执行器两件事：

1. 删去断言中的子句store_int_pair(p, x, y)，即left_erase(0)，其中0表示的是之前策略匹配要求left : store_int_pair(?p, ?x, ?y) at 0中的编号；
2. 删去查找的store_int(&(p -> a), ...)的要求，即right_erase(1)，其中1表示的是之前策略匹配要求right : store(field_addr(?p, int_pair, a), I32, ?v) at 1中的编号；
3. 除了被这次读取用到的a域之外，b域对应的那一半内存权限仍然保留，所以要把store_int(&(p->b), b)加回断言，即left_add(store(field_addr(p, int_pair, b), I32, y))；
4. 告诉符号执行器，p->a里原来存的值其实就是x，因此读取结果v必须满足v == x，即right_add(v == x)。

你可能会好奇为何这个策略表述语言中要使用左和右的概念（left和right），这是因为在上面QCP符号执行的情景中，要处理&(p->a)地址上的内存读取，相当于要求解下面这样的分离逻辑断言推导问题（其中P是当前分离逻辑断言）：

P |-- store(&(p->a), ?value) ** ?Frame

而上面断言变换策略中的left和right指的就是要检索或者操作上面这个推导式左边的或者右边的断言。

有了这个自动断言变换策略，在swap_int_pair函数的验证中就不再需要手动插入断言来展开store_int_pair了。

#include "swap_simple2.h"

void swap_int_pair(struct int_pair *p)
/*@ With x y
    Require store_int_pair(p, x, y)
    Ensure store_int_pair(p, y, x)
 */
{
    int temp = p->a;
    p->a = p->b;
    p->b = temp;
}

第一次读取p->a时，符号执行器会发现当前断言中没有store(&(p->a), ...)，但是有store_int_pair(p, x, y)这个子句，于是就会触发上面定义的策略，把整体谓词拆开，并把读取结果约束为原来存的值。之后，符号执行器就可以顺利执行了。下图中可以看到，符号执行int temp = p -> a没有生成任何VC。

并且符号执行会生成展开后的分离逻辑断言

store_int(&(p_319_pre->a) , x_322_free) *
store_int(&(p_319_pre->b), y_321_free) *
store_int(&temp, x_322_free) *
store_ptr(&p, p_319_pre)

换言之，QCP先基于以下推导式进行分离逻辑断言变换，然后再符号执行了int temp = p->a：

store_int_pair(p_319_pre, x_322_free, y_321_free) *
store_int(&temp, x_322_free) *
store_ptr(&p, p_319_pre)
|--
store_int(&(p_319_pre->a), x_322_free) *
store_int(&(p_319_pre->b), y_321_free) *
store_int(&temp, x_322_free) *
store_ptr(&p, p_319_pre)

而上述推导式就是.strategies文件中定义的策略找到的：

1. 初始待求解的断言变换式：

store_int_pair(p_319_pre, x_322_free, y_321_free) *
store_int(&temp, x_322_free) *
store_ptr(&p, p_319_pre)
|--
store_int(&(p_319_pre->a), __v) * __frame

2. 根据自定义策略：

store_int(&(p_319_pre->b), y_321_free) *
store_int(&temp, x_322_free) *
store_ptr(&p, p_319_pre)
|--
(__v == x) && __frame

3. 最后得出结论，开头的__v应该代入x，开头的__frame应该代入

store_int(&(p_319_pre->b), y_321_free) *
store_int(&temp, x_322_free) *
store_ptr(&p, p_319_pre)

因此，这里要做的断言变换就是前面给出的：

store_int_pair(p_319_pre, x_322_free, y_321_free) *
store_int(&temp, x_322_free) *
store_ptr(&p, p_319_pre)
|--
store_int(&(p_319_pre->a), x_322_free) *
store_int(&(p_319_pre->b), y_321_free) *
store_int(&temp, x_322_free) *
store_ptr(&p, p_319_pre)

例子：更多的store_int_pair变换策略

上面的例子中介绍了针对p -> a的内存读操作的分离逻辑变换策略，对p -> b的读取也需要一条完全对称的策略：

id : 1
priority : core(1)
left : store_int_pair(?p, ?x, ?y) at 0
right : store(field_addr(?p, int_pair, b), I32, ?v) at 1
action : left_erase(0);
         right_erase(1);
         left_add(store(field_addr(p, int_pair, a), I32, x));
         right_add(v == y);

对于内存写，策略会略有不同。下面是对p -> a写入时使用的策略：

id : 2
priority : core(1)
left : store_int_pair(?p, ?x, ?y) at 0
right : has_permission(field_addr(?p, int_pair, a), I32) at 1
action : left_erase(0);
         right_erase(1);
         left_add(store(field_addr(p, int_pair, b), I32, y));

相比前面提到的内存读策略，这条策略中右侧匹配只要求匹配has_permission(...)。这是因为内存读需要知道“这块内存里当前存着什么值”，而内存写只需要知道“拥有这块内存的读写权限”。

对p -> b写入时，也需要一条类似的变换策略，这里就不再重复了。

断言变换策略的可靠性

需要特别说明的是，.strategies文件的语法只是在告诉QCP“你想让符号执行在哪些场景下做哪些断言变换”。因此，这些断言变换策略本身并不保证逻辑正确性，QCP要求用户在Rocq中证明这些变换策略的可靠性。

用户可以使用下面的命令行指令生成相关的Rocq文件，也可以在网页版中点击上方的CoqProofGen按钮生成对应的Rocq文件。

StrategyCheck.exe --strategy-folder-path=YOUR/OUTPUT/PATH/ --input-file=swap_simple2.strategies

它会生成三个Rocq文件：

swap_simple2_strategy_goal.v
swap_simple2_strategy_proof.v
swap_simple2_strategy_goal_check.v

其中第一个文件包含了每一个断言变换策略可靠性对应的数学命题表述，第二个文件需要用户手动证明这些可靠性命题，第三个文件会检查第二个文件中是否确实包含了第一个文件中的全部命题。所有的断言变换可靠性命题都是分离逻辑的断言推导。

例如，处理store_int_pair与内存读的断言变换归根结底是需要证明：

store_int_pair(p, x, y) |--
store_int(&(p -> a), x) *
store_int(&(p -> b), y)

又例如，处理store_int_pair与内存写a域的断言变换归根结底是需要证明：

store_int_pair(p, x, y) |--
has_permission(&(p -> a)) *
store_int(&(p -> b), y)

例子：加载断言变换策略后验证swap_int_pair

前面已经提到，有了上面的断言变换策略之后，我们再验证swap_int_pair时，就不需要专门在函数体开头手动加入一条断言来展开store_int_pair了。这是因为在符号执行第一句语句int temp = p->a时，符号执行器就会触发断言变换策略，展开store_int_pair，这样一来，后续所有的符号执行都能顺利完成了。

不过，这并不意味着所有验证条件都会自动消失。即使不再需要手动断言，QCP在符号执行完整个函数体之后，仍然会留下一个VC。

我们需要证明符号执行生成的最强后条件能退出Ensure条件，也就是说，函数体执行结束后得到的两个域上的store，确实能够重新合成为规约后条件里的store_int_pair”，即：

Definition swap_int_pair_return_wit_1_split_goal_spatial := 
  forall (p_pre: Z) (y: Z) (x: Z)
         (PreH1: x <= INT_MAX)
         (PreH2: y <= INT_MAX)
         (PreH3: x >= INT_MIN)
         (PreH4: y >= INT_MIN),
    &(p_pre # "int_pair" ->ₛ "a") # Int |-> y **
    &(p_pre # "int_pair" ->ₛ "b") # Int |-> x
    |--
    store_int_pair p_pre y x.