struct int_pair {
int a;
int b;
};
We already know that two store_int predicates can describe the memory occupied by this structure. But in the C program, the structure is treated as one object. Verification can become more convenient if the permissions for the two fields can also be treated as one unit.
For this purpose, we can define a new separation-logic predicate store_int_pair in Rocq to describe the memory occupied by the structure. In the QCP Rocq library, p # Int |-> x means that the address p stores the signed integer x. If p is the address of a struct int_pair, then &(p # "int_pair" ->ₛ "a") is the address of field a in the structure whose base pointer is p. In other words, p # Int |-> x in Rocq corresponds to store_int(p, x) in C annotations, and &(p # "int_pair" ->ₛ "a") corresponds to &(p->a) in C. Separation conjunction is written with two stars in the Rocq library, rather than one star as in C annotations.
Definition store_int_pair (p: addr) (x y: Z): Assertion :=
&(p # "int_pair" ->ₛ "a") # Int |-> x **
&(p # "int_pair" ->ₛ "b") # Int |-> y.
With this predicate, we can describe the whole memory footprint of the structure using one predicate. The following swap_int_pair function uses it in its specification.
/*@ Extern Coq (store_int_pair : Z -> Z -> Z -> Assertion) */
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)
*/
{
/*@ Assert
p == p@pre && store(&(p->a), x) * store(&(p->b), y)
*/
int temp = p->a;
p->a = p->b;
p->b = temp;
}
Although this C function is very simple, verifying it in QCP requires an assertion annotation and manual proof of VCs in Rocq. When symbolic execution enters the function body, the current assertion describes the memory permission using store_int_pair, as shown below. Without the manual assertion, QCP cannot find store predicates for the addresses &(p->a) and &(p->b), so it cannot continue symbolic execution.
Without the assertion, QCP reports the following error:
After adding the assertion, symbolic execution completes successfully. It produces two VCs: first, after entering the function body, the precondition together with the allocated storage for local variable p must imply the manually added assertion; second, after the function body finishes and the local variables p and temp are released, the strongest postcondition must imply the function's Ensure condition.
store_ptr(&p, p_319_pre) *
store_int_pair(p_319_pre, x_322_free, y_321_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(&(p_319_pre->a), y_321_free) *
store_int(&(p_319_pre->b), x_322_free)
|-- store_int_pair(p_319_pre, y_321_free, x_322_free)
In the goal file generated by QCP, these VCs become the following Rocq propositions. The first one has been simplified by QCP.
Definition swap_int_pair_entail_wit_1_split_goal_spatial :=
forall (p_pre: Z) (y: Z) (x: Z),
store_int_pair p_pre x y
|-- &(p_pre # "int_pair" ->ₛ "a") # Int |-> x **
&(p_pre # "int_pair" ->ₛ "b") # Int |-> y.
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 |-> x **
&(p_pre # "int_pair" ->ₛ "b") # Int |-> y |--
store_int_pair p_pre y x.
These two VCs show that QCP does not automatically unfold Rocq predicate definitions during assertion entailment. To prove these propositions in Rocq, it is enough to unfold the definition of store_int_pair.