Verification Condition Generation

At the end of the previous section, contracts, loop invariants, and inline assertions had all been written into the program. This section answers a question left hanging: what exactly does the symbolic execution engine do with these assertions? The answer: it mechanically reduces the proposition “the program satisfies its specification” to a finite number of separation-logic entailments of the form p |-- qp |-- q—the verification conditions (VCs). Once every VC is proved, the function satisfies its contract. This section first reviews the classic approach (the weakest-precondition calculus) and three of its less-than-intuitive aspects on C*, then introduces the forward symbolic execution that C* actually adopts, and finally walks through three examples that make the VCs clear one by one. How to prove these VCs is the subject of later sections.

Recall the Hoare triple from Specifying with Separation Logic. Once contracts and invariants are written, the remaining problem is mechanical: how does one compute, from an annotated program, the logical proposition that must be proved? A classic method is the weakest-precondition (WP) calculus proposed by Dijkstra: is the weakest precondition needed for “ holds after executing statement “, defined recursively over the program structure:

A loop relies on its annotated invariant : take , and additionally produce two obligations—preservation and exit . Checking the whole function then reduces to a single entailment:

This is the classic verification-condition generator (VCGen), and many deductive-verification tools work precisely along these lines.

Let us look at a concrete example. The following program computes (with ), and the target postcondition is :

Annotate the loop with the invariant , and mechanically expand wp—first the loop rule gives plus the two obligations, then two applications of the assignment rule replace and in by and in turn—so the whole function folds down into one formula:

Check each part: the entry and preservation both hold, but the exit cannot be proved— only says the loop stopped, not that ; if were negative, would not entail . During execution clearly never goes negative (, and each round decrements by one), but the invariant does not record this fact, so the WP calculus has no way to use it. Strengthening the invariant to makes all three parts hold—this is a concrete instance of the previous section’s guideline that “boundary facts must be copied into the invariant to be carried along”.

The WP calculus is concise and elegant, but transplanting it directly onto a tool like C* clashes with the usage experience in three places.

First, its direction is opposite to the program. computes before : the computation starts from ensureensure and substitutes backward statement by statement, whereas people write, read, and debug programs top-down. In the example above, “the exit cannot be proved” only shows up after the entire formula has been computed, so when something goes wrong it is generally hard to answer “which line of the program is at fault”.

Second, one function yields one big VC. WP folds the whole function body into a single formula: the VC of the simple five-line program is already not small; a real C function with pointers, structs, and branches must encode every step’s memory effect into the formula, and its size can grow very quickly. If one giant VC cannot be proved (or the automated solver times out), the user has almost no way to get a foothold.

Third, separation logic needs the magic wand. Redoing WP over separation logic, statements that read and write the heap require a new connective. Take the write statement from Specifying with Separation Logic as an example; its weakest precondition is:

Read: the current heap can separate out the cell at (so the write is safe), and after changing it to and reassembling that cell, holds. The here is precisely the magic wand from the notation table two sections back: means “assemble on one more heap satisfying , and you get a heap satisfying “. The magic wand lets WP still be computed structurally in separation logic, but automatically solving entailments containing the magic wand remains a difficult problem.

The three counterintuitive aspects point in the same direction: rather than computing the postcondition backward, let the assertion flow forward along the execution direction—each line has a “current state”, and obligations pop out on the spot at the line that produces them. This is exactly what viewing the symbolic state line by line in VSCode looks like.

The symbolic execution engine currently enabled by default in C* is provided by QCP (Qualified C Programming). QCP goes in the opposite direction from WP: starting from requirerequire, it computes the strongest postcondition statement by statement along the program direction, producing small, numerous VCs along the way. QCP’s forward style originates from VST-Floyd: there, each proof step pushes forward a “current assertion”, and the proof goal at any moment is “current assertion + remaining program”, as if filling in a proof outline top-down. QCP carries this method from interactive proof into an automated tool, guiding execution with code annotations; one direct motivation for choosing forward is real-time feedback—every line you write can be symbolically executed immediately, showing the state after that line, and even a not-yet-finished function can be verified incrementally.

In the engine’s eyes, the symbolic state is a separation-logic assertion—exactly the one viewed line by line in VSCode: the logical variables bound by existsexists, the pure facts factfact, and the spatial part made of data_atdata_at and representation predicates. Execution starts from requirerequire (parameters enter as __pre__pre and so on) and advances by a fixed rule for each kind of statement:

• Declaration and assignment: update the contents of that variable’s data_atdata_at—the current value of each variable in the expression is looked up from the state;
• Memory read (*p*p, v->tailv->tail): find in the spatial part the data_atdata_at for exactly that cell and read out its value; if none is found, it errors and halts—the engine does not unfold representation predicates by definition on its own (examples two and three below will show this);
• Memory write: likewise find that cell first, then replace its contents;
• Branch: the state splits in two, each conjoined with the condition and its negation, and each advances separately;
• Loop: the invariant is the cut point—reaching the loop head pops a VC (“current state |--|-- invariant”); thereafter it enters the loop body carrying only the invariant (conjoined with the loop condition); at the end of the loop body it returns to the loop head and pops another VC (preservation); after the loop it continues with “invariant **** negation of the condition”;
• Inline assertion: pops a VC (current state |--|-- assertion), then takes the assertion as the new state—already covered in the previous section;
• Function call: item by item, match and remove from the current state the resources claimed by the callee’s requirerequire, replace them with the resources given by ensureensure, and carry the rest of the state along unchanged—this is exactly the frame rule embodied in the engine; the residual pure facts after matching pop out as VCs;
• Function exit: pops a VC—the current state (with local resources removed) |--|-- ensureensure (with __return__return substituted by the return value).

All VCs have the same shape p |-- qp |-- q: the left side is the symbolic state the engine has computed all along, and the right side is the assertion you wrote (an invariant, an inline assertion, a callee’s requirerequire, or this function’s ensureensure), and each carries the source line number that produced it. In addition, the engine produces a second class of VCs—safety VCs: at risk points for C undefined behavior such as arithmetic overflow, division by zero, and out-of-range shifts, it pops the corresponding pure-fact obligation (example one will show this).

Set against WP’s three counterintuitive aspects, forward symbolic execution dissolves them one by one:

• Forward: the state advances along the execution direction, and every line has a viewable symbolic state—the VSCode panel’s “write a line, see a line” real-time feedback is built on exactly this;
• Small and numerous: VCs pop out on the spot at annotations, each with its line number, so whichever one cannot be proved, you go back to that line to look;
• No magic wand needed: reading and writing memory relies on the data_atdata_at already in the state, calls rely on item-by-item frame matching, and the magic wand is never needed throughout.

One more point is worth noting: not every entailment becomes a VC you see. The QCP engine has a built-in entailment solver (a rule-based matching strategy plus a lightweight arithmetic solver): it aligns the heap part item by item and discharges trivial pure facts on the spot, and whatever it can solve automatically never surfaces. So the VCs you ultimately see are the homework left over by automation—often the spatial part is already aligned, leaving the pure facts that genuinely need a human proof, or the single step of unfolding a predicate by definition.

With the theory done, let us look at a real case. The Gauss summation from the previous section:

int sum(int n)
    [[cst::require(`fact(0i <= n) ** fact(n <= 1000i)`)]]
    [[cst::ensure(`fact(2i * __return == n * (n + 1i))`)]]
{
  int s = 0;
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists sv iv.
                          data_at n__addr Tint n__pre **
                          data_at s__addr Tint sv **
                          data_at i__addr Tint iv **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(2i * sv == iv * (iv + 1i)) **
                          fact(n__pre <= 1000i)`)]]
  {
    i = i + 1;
    s = s + i;
  }
  return s;
}

int sum(int n)
    [[cst::require(`fact(0i <= n) ** fact(n <= 1000i)`)]]
    [[cst::ensure(`fact(2i * __return == n * (n + 1i))`)]]
{
  int s = 0;
  int i = 0;
  while (i < n)
      [[cst::invariant(`exists sv iv.
                          data_at n__addr Tint n__pre **
                          data_at s__addr Tint sv **
                          data_at i__addr Tint iv **
                          fact(0i <= iv) ** fact(iv <= n__pre) **
                          fact(2i * sv == iv * (iv + 1i)) **
                          fact(n__pre <= 1000i)`)]]
  {
    i = i + 1;
    s = s + i;
  }
  return s;
}

Running verification on this file yields three VCs (the output is wrapped to page width; line numbers are counted against the code listing above):

Reading through each one, a few observations:

• First, note what is absent: the loop-entry “establishment” is not in the list. Before entering the loop, the state has ss and ii in the precise form of two cells with contents 0i0i, and after matching the invariant item by item only trivial arithmetic like is left, which the engine discharges on the spot—whatever can be solved automatically never surfaces.
• VC 1 is a safety VC: the result of s + is + i must fall within the intint range. In the antecedent ii’s contents are already iv + 1iiv + 1i (the preceding line i = i + 1i = i + 1 has already executed, and its own overflow check is discharged automatically using iv < n__pre <= 1000iv < n__pre <= 1000); to prove that sv + iv + 1isv + iv + 1i does not overflow, one must derive a bound on svsv from 2i * sv == iv * (iv + 1i)2i * sv == iv * (iv + 1i) together with the boundary facts—this nonlinear reasoning is beyond the built-in arithmetic solver’s capability, so it is left as a VC. This also explains the previous section’s guideline: if fact(n__pre <= 1000i)fact(n__pre <= 1000i) were not recorded in the invariant, this VC would have no basis to be proved.
• VC 2 is preservation: the antecedent is the state after executing the loop body (the contents of both ss and ii are already updated), and the consequent is the whole invariant (existsexists reappears). Proving it means choosing new instances for iviv and svsv and verifying each factfact.
• VC 3 is exit: the left of |--|-- is “invariant **** negation of the loop condition”, and all data_atdata_at have vanished, leaving only empemp—on return the engine reclaims the cells of the local variables and the pure facts remain; the right is ensureensure (with __return__return already substituted by svsv). What remains is the elementary math step “from , , , derive “.

This example shows the usual state of a VC: the spatial part has already been aligned and discharged by the engine, and what is left for the human is mostly pure arithmetic facts.

The array and linked-list examples in the previous section still lacked part of the discussion: the resources in the invariant are folded inside wrapper predicates, and executing directly errors. Now let us see the real error. Remove the inline assertion inside the clearclear loop body from the previous section and verify again, and the engine halts at *p = 0*p = 0:

Note that this is an error, not a VC: writing *p*p needs the cell undef_data_at (arr__pre + iv * sizeof Tchar) Tcharundef_data_at (arr__pre + iv * sizeof Tchar) Tchar ready in the state, but it is folded inside undef_suffixundef_suffix; the engine will not decide for you when to unfold a predicate by definition, so execution cannot continue. The symbolic state accompanying the error is exactly the handle for troubleshooting—at a glance you can see which predicate’s belly the missing resource is in.

Put back the “unfold one step” inline assertion from the previous section, and the whole function executes to completion, producing four VCs:

Unlike example one, this time even “establishment” is left as a VC—rewriting undef_bytes arr__pre n__preundef_bytes arr__pre n__pre into “zero-cell prefix **** full-segment suffix” (zero_bytes arr__pre 0i ** undef_suffix arr__pre 0i n__prezero_bytes arr__pre 0i ** undef_suffix arr__pre 0i n__pre) requires unfolding these three predicates by definition, which is beyond the reach of the automated strategy. Of the four, the most worth looking at closely is the assertion one (VC 2)—when the previous section said “assertassert does not eliminate the proof obligation; it merely turns it from ‘stuck execution’ into ‘left to prove’”, this is what it referred to:

The two sides are almost identical item by item, with all the difference concentrated in the last line and a half: the left’s undef_suffix arr__pre iv n__preundef_suffix arr__pre iv n__pre must be split into a head cell plus the remaining suffix. This step depends on the definitions of undef_suffixundef_suffix and undef_array_atundef_array_at—precisely the proof to be written later. The exit one (VC 4) is comparatively short:

From the boundary facts one gets iv == n__preiv == n__pre, the length-zero suffix reduces to the empty heap, and the prefix is exactly the whole segment—the previous section’s “exit” narrative is here compressed into a single entailment.

The linked-list situation is essentially the same. Remove the inline assertion and verify reversereverse directly, and the engine halts when reading v->tailv->tail:

The cell for the tailtail field is folded inside sll vv l2sll vv l2. After putting back the previous section’s assertion, execution goes through, again yielding four VCs (establishment, assertion, preservation, exit). The assertion one unfolds sllsll along the non-empty branch:

Proving it uses two facts: when vvvv is non-null, sll vv l2sll vv l2 can only come from the definition’s CONSCONS branch, so l2l2 must be some x :: xsx :: xs, and the head node’s two data_atdata_at cells and the remaining sll q xssll q xs surface accordingly; on the list side, l == l1 ++ l2l == l1 ++ l2 must be rewritten into l == l1 ++ x :: xsl == l1 ++ x :: xs.

The preservation VC’s antecedent faithfully records the situation after the three-pointer dance—ww’s contents are already vvvv, vv’s contents are already qq, and the head node’s FtailFtail cell has been rewritten to wvwv—which must be refolded into the invariant’s two sllsll segments. The exit one is again short:

The previous section’s three-line “exit” narrative compresses into a single entailment: from vv == 0ivv == 0i and sll vv l2sll vv l2 taking the definition’s empty-list branch one gets l2 == []l2 == [], so l1 == ll1 == l, and the left’s sll wv (REVERSE l1)sll wv (REVERSE l1) is exactly the conclusion to be proved.

All the output shown in this section can be obtained in VSCode, through the same entry point as viewing the symbolic state (right-click Show Symbolic StateShow Symbolic State):

• Cursor on a line inside a function body: the panel shows that line’s symbolic state—that is, the strongest postcondition of forward symbolic execution advanced to this point;
• Cursor on a file-level line (such as the end of the file): the panel shows the list of verification conditions accumulated up to this point, each labeled with its number and line (VC n line lVC n line l), and when expanded is split into two sides by |--|--.

A non-empty VC list means verification is not yet complete—they are precisely the gaps to be filled next with proofs: write proof code in [[cst::proof]][[cst::proof]] to construct theorems and rewrite the symbolic state, until the engine can discharge every VC. This is the subject of later sections.

• A verification condition (VC) is a separation-logic entailment of the form p |-- qp |-- q: the left is the symbolic state computed by the engine, the right is the assertion you wrote; the program satisfies its specification all VCs are proved.
• The classic WP calculus substitutes backward from ensureensure and folds the whole function into one big formula, and over separation logic it needs the magic wand—three counterintuitive aspects.
• C*‘s default symbolic execution engine is provided by QCP, with ideas from VST-Floyd: starting from requirerequire, compute the strongest postcondition along the program direction; VCs pop out on the spot at loop heads (establishment/preservation), inline assertions, function calls, and function exits, plus safety VCs for overflow, division by zero, and so on, each with its line number.
• The resources needed to read and write memory must be readily visible in the state: a missing resource is an error, not a VC; when to unfold a predicate by definition is decided by you, via an assertion (or a proof).
• Entailments the engine can discharge automatically never surface: the VCs you see are the homework left over by automation, and the common forms are “spatial part already aligned, pure facts remain” and “one definition-unfold step short”.