QCP Tutorials Assertion Extensions and Transformations

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.

Previously, to verify programs using such a predicate, we manually inserted assertion annotations to unfold it. That is sometimes inconvenient. QCP allows users to customize strategies that automatically transform separation-logic assertions during symbolic execution in specified situations. With this feature, when the current assertion contains store_int_pair(p, x, y) and the program is about to read or write p->a or p->b, the user no longer needs to manually insert an assertion that expands it into two store predicates.

Customizing Assertion Transformations with .strategies Files

In QCP, demand-driven assertion transformations are defined in .strategies files. Such files can refer to .h files, and .h files can include strategies. In the .h file, we declare the C structure and the custom Rocq predicate store_int_pair, then use include strategies to load the strategy file during symbolic execution. Conversely, a .strategies file can use #include to refer to the .h file, so that it can use the structure type and custom predicate declared there.

// 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);

This strategy says: if the statement being symbolically executed needs to read the memory of p->a, and the current assertion has no store_int(&(p->a), ...) clause but does contain store_int_pair(p, x, y), then transform the assertion as follows.

1. Remove store_int_pair(p, x, y) from the left side with left_erase(0).
2. Remove the right-side requirement to find store_int(&(p->a), ...) with right_erase(1).
3. Add back the permission for field b, namely store_int(&(p->b), y), with left_add(...).
4. Record that the value read from p->a is x, with right_add(v == x).

The language uses the terms left and right because QCP is solving an entailment of the following form, where P is the current assertion:

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

Thus left and right refer to the assertions on the left and right sides of this entailment.

With this automatic transformation strategy, verification of swap_int_pair no longer needs a manual assertion that unfolds 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;
}

When p->a is first read, the symbolic executor sees no direct store(&(p->a), ...) clause, but it does find store_int_pair(p, x, y). It triggers the strategy above, splits the combined predicate, constrains the read value, and continues execution. The screenshot shows that symbolic execution of int temp = p->a produces no VC.

The transformed assertion is:

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)

In other words, QCP first performs an assertion transformation based on this entailment, and then symbolically executes 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)

More store_int_pair Transformation Strategies

The previous example handled reading p->a. Reading p->b requires a symmetric strategy:

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);

For writes, the strategy is slightly different. Here is the strategy for writing to 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));

Unlike a read, a write only needs read/write permission for the memory; it does not need to know the value currently stored there. A similar strategy is needed for writing to p->b.

Soundness of Assertion-Transformation Strategies

The .strategies syntax only tells QCP when and how the user wants symbolic execution to transform assertions. The strategies themselves do not automatically guarantee logical correctness. QCP requires the user to prove the soundness of these transformations in Rocq.

The following command generates the corresponding Rocq files. In the web IDE, the CoqProofGen button can also generate them.

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

It generates:

swap_simple2_strategy_goal.v
swap_simple2_strategy_proof.v
swap_simple2_strategy_goal_check.v

The first file contains the mathematical propositions expressing the soundness of each assertion-transformation strategy. The second file is where the user proves them manually. The third file checks that all propositions from the first file are proved.

For example, the read transformation for store_int_pair ultimately requires proving:

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

The write transformation for field a ultimately requires proving:

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

Verifying swap_int_pair After Loading Strategies

After the strategies are loaded, verifying swap_int_pair no longer requires a manual assertion at the beginning of the function body. The first statement int temp = p->a triggers the transformation strategy, unfolds store_int_pair, and the rest of symbolic execution can proceed.

This does not mean that all VCs disappear. Even without the manual assertion, QCP still leaves one VC after executing the whole function body.

We must prove that the strongest postcondition generated by symbolic execution implies the Ensure condition. In other words, after the function body finishes, the two field-level store predicates must be recombined into the store_int_pair predicate in the postcondition:

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.