T4-4 - 符号执行中的其他自动断言变换

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.

不过，有些时候在验证相关结构体的操作时，我们希望总是将其信息放在一个store_int_pair谓词中，使得符号执行需要处理的断言变得更简洁。QCP也能支持用户通过定制断言变换策略实现这一功能。

具体而言，用户需要在.strategies文件中增加以下断言变换策略：

id : 4
priority : post(1)
left : store(field_addr(?p, int_pair, a), I32, ?x) at 0
       store(field_addr(p, int_pair, b), I32, ?y) at 1
action : left_erase(0);
         left_erase(1);
         left_add(store_int_pair(p, x, y));

这个断言变换策略中有一个关键字是post，这不同于之前例子中的core，它表示在内存读写的符号执行之后，自动进行此断言变换。而不是为了对内存读写做符号执行而事先做的断言变换。

现在，符号执行的全程都只会显示store_int_pair谓词，swap_int_pair函数的符号执行也不会生成任何一个验证条件。

符号执行int temp = p->a后，得到断言：

store_int_pair(p@pre, x, y) * 
store_int(&temp, x) * 
store_ptr(&p, p@pre)

符号执行p->a = p->b后，得到断言：

store_int_pair(p@pre, y, y) * 
store_int(&temp, x) * 
store_ptr(&p, p@pre)

符号执行p->b = temp后，得到断言：

store_int_pair(p@pre, y, x) * 
store_int(&temp, x) * 
store_ptr(&p, p@pre)

在此基础上，释放临时变量temp和p的内存空间，就直接得到了Ensure条件。这样，QCP就不会额外产生需要用户手动在Rocq中证明的VC了。