[SwayamInSync]

Plan item H5: a case study for 0.2. It is a class-based component that exercises the class and template support (B1 to B4) and the diagnostics (E3): a ring buffer. Writing it found four things the verifier did not support, and this PR adds them. It is stacked on #110 (D7).

The case study

Ring<N> keeps a queue of at most N integers in a fixed array, as embedded code keeps a UART's received bytes:

• its fields (buf, head, count) are private, with a class invariant over them;
• its constructor initializes the array in a loop;
• push and pop are specified through two spec functions, friends of the class: at(r, i), the element i places after the oldest, and size(r). So the contract says what the class is, a FIFO queue, and not how it stores it;
• push asserts count < N with C's assert.

Two clients use only the contract:

• first_two loads samples in a range-based for, adds one if the ring is not full, and shows that the two oldest are 1 and 2;
• apply runs a command, chosen by a switch over a scoped enumeration, on a ring a reference names.

$ cpp-verify ring_buffer.cpp
Verified: Ring<4>::Ring [backend=z3]
Verified: Ring<4>::full [backend=z3]
Verified: Ring<4>::push [backend=z3]
Verified: Ring<4>::pop [backend=z3]
Verified: first_two [backend=z3]
Verified: apply [backend=z3]
Summary: 6 verified in 1.9 s

With -DFORGET_WRAP, pop forgets the wraparound (head = head + 1;). The class invariant fails at pop's exit, at head < N, and the path shows the store of 4 into head (address 17, after the 16 bytes of buf). The page, case-studies/ring-buffer.rst, shows both runs and explains them.

What it took

1. Class invariants at loops. On main, a loop that calls member functions of an object outside its class forgets the object's class invariant: at the loop head the verifier knows only the loop's invariants. With private fields, the client cannot restate the invariant there. So first_two's r.push(s) failed with [type-invariant], and the verifier's own note said no execution fails this check ... the loops' invariants are too weak.

The converter now appends to each loop's invariants the class invariants of the objects the loop reaches (ASTConverter::appendObjectInvariants): the local objects alive at it, and the objects its function's reference and pointer parameters address (guarded by p == nullptr ||).

This is sound because each one is checked at entry and preserved like the user's invariants, and is never assumed. Only the class's members, and code that writes a public field, change what an invariant states, and a public member keeps it. So the invariant holds at every iteration of a loop outside the class. The design follows Spec#'s and Dafny's discipline that an object's invariant holds whenever no method of its class is running on it, but proves it instead of assuming it.

A member function's own loops get none of its class's invariants, since a member may break one between calls. Meter::recount in the test breaks its invariant inside its loop and verifies.

2. The address of a local in a contract. size(&r) in a loop invariant was an error (raw address-of is unsupported until lexical lifetime and escape effects are modeled). In a contract, the address of a local object in memory is now its address. A spec it is passed to cannot keep it, and nothing else in a contract can. In ghost code, which could keep it in a ghost variable, it is still an error.

3. hide and reveal of a spec template's specialization. cv::hide(at<4>) stopped the function (unsupported C++ type in verification: <overloaded function type>). Clang leaves a template-id that is not called as an overload set, so the parser now resolves it with Sema's own placeholder resolution (CheckPlaceholderExpr), as C++ resolves &at<4>. A template's name alone is now Clang's error (reference to overloaded function could not be resolved; did you mean to call it?). A first version passed Complain to ResolveAndFixSingleFunctionTemplateSpecialization without a diagnostic ID, which crashes in the diagnostic printer on an unresolvable name; the test covers that name.

4. first_two hides at. Its proof needs only the contracts of push and pop, which speak of at. Visible, the definition (buf[(head + i) % N]) puts % inside every quantifier, and the loop invariant's preservation timed out at 30 s. Hidden, the whole file verifies in 1.9 s.

Tests

• suite/ring_buffer.cpp: the case study, verified, and with -DFORGET_WRAP failed with the store that breaks the invariant.
• suite/class_invariants_in_loops.cpp:
  • loops over a local object (count_to), an object a reference names (fill), one a pointer addresses in a do loop (drain), and a pointer that may be null (idle);
  • member functions whose loops break their own class's invariant: on this (recount), and on another object of the class, which a reference names (empty);
  • the failing twin, a friend whose loop breaks the invariant (spread), which fails [invariant-preserved] at the class's invariant: the generated invariant is checked, not assumed;
  • &x of a local in ghost code, which stays an error.
• suite/hide_template_specs.cpp:
  • hide of a specialization (spec.hidden, naming scaled<3>);
  • reveal_with_fuel of a recursive one;
  • the template's name alone as an error.

On the base:

• ring_buffer.cpp stops at cv::hide(at<4>);
• class_invariants_in_loops.cpp rejects &m, fails fill ([type-invariant]), and times out on drain;
• hide_template_specs.cpp stops at every hide.

Each mutant below, applied alone and rebuilt, is caught by these tests (8 of 8). H2 survived a first run, since recount's loop reaches no object of its class other than this, which is no parameter; empty was added for it:

Mutant	Change
H1	no class invariants at loops
H2	a member function's loops keep its own class's invariant
H3	a pointer parameter's invariant is not guarded by null
H4	local objects keep none
H5	parameters keep none
H6	no address of a local in a contract
H7	the address of a local in ghost code too
H8	a specialization is not resolved

On a release build of this branch, the whole Verify suite (503 tests) passed except docs_examples.test: the ring buffer page showed the one-line bug in a code block that does not compile alone. The block is now marked as a fragment, and the docs check passes (267 examples, 0 failed); class_invariants_in_loops.cpp passes with its added case.

Docs

• the case study page and the case study index;
• structs.rst: class invariants at loops, with an example and its output, and the address of a local in a contract;
• ghost-proofs.rst: specializations in hide and reveal;
• limitations.rst: spec member functions and spec parameters of class reference type, still unsupported, and an address taken in ghost code;
• release notes; ARCHITECTURE; DESIGN.

Not done

• Spec member functions (cv::spec int at(int i) const) and spec parameters of class reference type (const Ring<N> &). A view is a free function taking a pointer, a friend when it reads private fields. Both are follow-ups.
• A loop over an object a reference names frames it with byte-range quantifiers (q!frame). A query with such a quantifier is solved by Z3's smt tactic. In class_invariants_in_loops.cpp's first twin, that tactic gave up after 20 s on a check that the default solver refutes in 24 ms; --dump-smt2 (D7: every solver query as a standalone SMT-LIB script (--dump-smt2) #110) showed it. The twin now uses a local object, and the solver choice is a follow-up.

Stacked on #110.