[SwayamInSync]

A cppverify::type_invariant held only for records passed and returned by value: a class's member functions and constructors ignored it, so nothing a caller learned about an object survived a call, and a member function could leave the object in any state. Now the invariant of a class holds at its public boundary:

class Meter {
public:
  Meter()
    cv::post(level == 0)
    : level(0) {}

  void add(int d)
    cv::pre(0 <= d && level + d <= 100)
    cv::post(level == cv::old(level) + d)
  {
    level = level + d;
  }

  void overflow()
    cv::post(true)
  {
    level = 101;
  }

  int get() const
    cv::post(cv::result == level)
  {
    return level;
  }

  int level;

  cv::type_invariant(0 <= level && level <= 100);
};

int filled()
  cv::post(0 <= cv::result && cv::result <= 100)
{
  Meter m;
  m.add(30);
  int v = m.get();
  return v;
}

Verified: Meter::Meter [backend=z3]
Verified: Meter::add [backend=z3]
meter.cpp:28:33: error: verification failed: Meter::overflow [...::type-invariant@28:33] (counterexample: ...) [backend=z3] [reason=counterexample]
Verified: Meter::get [backend=z3]
Verified: filled [backend=z3]

On the base (#77) overflow verifies too: member functions ignored the invariant.

Stacked on #77 (B3-3 of plan item B3: class invariants; member operators follow).

Design

The plan's rule: the invariant is a precondition and postcondition of every public member function and a postcondition of every constructor, checked at every call, internal calls included, which is sound without pack/unpack (Spec#'s and Dafny's Valid() discipline need an explicit state of the object because they let methods be called while it is broken; here no call can be):

• Generated clauses. entryClassInvariants (a public member function's, not a constructor's) and exitClassInvariants (a public member function's and every constructor's) give the class's invariants, converted in the member function's context, so a field is a load through this; they are generated pre- and postconditions of kind type-invariant, checked and assumed at calls as any.
• Private and protected member functions take neither, so they may work on a broken object; a public one called meanwhile fails at that call. A caller that writes a public field holds the invariant only if it keeps it: the next public call checks it.
• Extents in invariants (left open by verify: State the extents of pointer fields, and separate pairs with an extent over their extents #72): cv::valid(data, len) in a class invariant is, on entry, a field extent of this as in a precondition: pointerFieldOfParameter takes this->data, and collectFieldExtents scans the entry invariants, so this->data is a synthetic parameter bound at every call. At exit a marker states nothing (a postcondition cannot carry one), so it is true there (DropExtentMarkers); the next call checks the extent from what its caller knows, and a member function that changes len must say how.

Found while testing: a falsified claim after a constructor and a member call on a local object ended solver.timeout (60 s) instead of failing. A call whose footprint is a record parameter's object, as the default modifies(*this) is, framed its bytes with one HeapFrame, the unbounded quantifier #75 met in loops. havocFootprints now frames it as the cells of the record's leaves (RecordCells, from the callee's layout at the actual's address), so the call is a chain of stores: the same claim fails in 0.3 s, and the test file runs in 3 s instead of 66 s.

Tests

suite/class_invariants.cpp (Z3, with a check that no proof is vacuous):

• Ring: a constructor that initializes the buffer in a loop and establishes the invariant; push, pop, size, front_index verified with it assumed and restored; skip breaks it (type-invariant); rotate breaks it through a private member function and restores it; peek_broken calls a public member function while it is broken (type-invariant at the call);
• Window: a constructor that does not establish it; Bounded: one that does;
• callers: the invariant known after construction and after a call (known, ring_use with cv::check), a field broken by the caller before a call (broken_by_caller, at the call), and pop's unstated value (ring_value fails, in seconds);
• View: an extent in the invariant, assumed by first; a caller passing its own extent (first_of), and one whose grow makes the next call's extent fail (grown, bounds).

Mutants, each built on an assertions build and run on class_invariants.cpp, constructors.cpp, member_functions.cpp, pointer_field_extents.cpp, local_record_arguments.cpp, and type_invariant_lazy.cpp: 8 of 8 killed.

Mutant	Killed by
no invariant on entry	class_invariants
no invariant at exit	class_invariants (skip)
private member functions assume and restore it too	class_invariants (rotate)
constructors need not establish it	class_invariants (Window)
extent markers kept at exit	class_invariants (View)
this->f takes no extent	class_invariants (View)
invariants not scanned for extents	class_invariants (View)
call frames of a record's object as one byte range	class_invariants (grown, ring_value: solver.timeout)

Open

• A free function taking the object by reference or pointer assumes nothing of its invariant (such parameters get no injection, as before), so to call a public member function on it, it states the invariant in its own precondition. Member operators, own-object returns, and class invariants at reference and pointer parameters #79 settles it: an object a parameter refers to or points to satisfies its invariant at every function boundary, as ACSL's weak type invariants and Verus's do.

Docs

• structs.rst: "Class invariants", a checked example (Meter), the rules for private members, callers, and extents.
• Release notes: "Class invariants"; "Calls that write a record" (timeouts that are counterexamples now).
• DESIGN.md: type invariants on classes. ARCHITECTURE.md: class invariants, the call cells.

Checked

• The Verify suite on a release build: 463 passed (the exhaustive decoder filtered out), 1233 s with 40 workers.
• The doc pages' examples (structs, DESIGN): 35 checked, 0 failed; docs_examples.test and docs_coverage.test pass; the site builds with warnings as errors.