[SwayamInSync]

A member operator was not a member call: for a == b with a member operator==, the converter took a for the operator's parameter and b as an argument beyond it, an error. An operator that returns its own object by reference (Bits &operator|=, every assignment operator) was an unsupported type. Now a member operator takes its first operand as its object, and one that returns *this returns nothing the caller does not hold:

class Bits {
public:
  Bits()
    cv::post(word == 0)
    : word(0) {}

  void set(int i)
    cv::pre(0 <= i && i < 16)
    cv::modifies(word)
    cv::post(word == (cv::old(word) | (1u << i)))
  {
    word = word | (1u << i);
  }

  bool operator==(const Bits &o) const
    cv::post(cv::result == (word == o.word))
  {
    return word == o.word;
  }

  Bits &operator|=(const Bits &o)
    cv::modifies(word)
    cv::post(word == (cv::old(word) | o.word))
  {
    word = word | o.word;
    return *this;
  }

  unsigned word;

  cv::type_invariant(word < 65536);
};

bool merged()
  cv::post(cv::result)
{
  Bits a;
  Bits b;
  a.set(3);
  b.set(5);
  a |= b;
  b |= a;
  bool same = a == b;
  return same;
}

Verified: Bits::Bits [backend=z3]
Verified: Bits::set [backend=z3]
Verified: Bits::operator== [backend=z3]
Verified: Bits::operator|= [backend=z3]
Verified: merged [backend=z3]

On the base (#78):

bits.cpp:22:9: error: operator|=: unsupported C++ type in verification: Bits &
bits.cpp:42:8: error: merged: aggregate value use of an automatic object is unsupported: b
bits.cpp:43:8: error: merged: aggregate value use of an automatic object is unsupported: a
bits.cpp:44:20: error: merged: aggregate value use of an automatic object is unsupported: b
Verified: Bits::Bits [backend=z3]
Verified: Bits::set [backend=z3] (its precondition is assumed, not checked, at calls from unverified merged)
Verified: Bits::operator== [backend=z3] (its precondition is assumed, not checked, at calls from unverified merged)

operator|= keeps the invariant only because o satisfies it too, which settles the question #78 left open: an object a parameter refers to or points to now satisfies its class invariant at every function boundary.

class Level {
public:
  Level(int v)
    cppverify::pre(0 <= v && v < 100)
    cppverify::post(value == v)
    : value(v) {}

  int get() const
    cppverify::post(cppverify::result == value)
  {
    return value;
  }

  int value;

  cppverify::type_invariant(0 <= value && value < 100);
};

int read(const Level &l)
  cppverify::post(0 <= cppverify::result && cppverify::result < 100)
{
  int v = l.get();
  return v;
}

void spoil(Level &l)
  cppverify::modifies(l.value)
{
  l.value = 500;
}

This branch:

Verified: Level::Level [backend=z3]
Verified: Level::get [backend=z3]
Verified: read [backend=z3]
level.cpp:16:40: error: verification failed: spoil [...::type-invariant@16:40] (counterexample: l [ssa=l_0] [type=pointer] = 1; trace: heap-write.store@29:11 address=1 value=500) [backend=z3] [reason=counterexample]

The base (#78) has the verdicts the other way round: read fails at its call to get (type-invariant@22:3), since l was not known to satisfy the invariant, and spoil verifies.

Stacked on #78 (B3-4, the last part of plan item B3: classes).

Design

• Member operators. convertExecCallArgs takes the object of a CXXOperatorCallExpr whose callee is an instance member function from its first argument, bound as obj.m()'s object is, and the parameters from the rest. A free operator is a free function and is unchanged.
• Returning the own object. returnsOwnObject recognizes a member function returning an lvalue reference to its own class whose every return is return *this;, the shape of an assignment or compound-assignment operator. The reference names an object the caller already holds, so the VFunction returns void, findUnsupportedType accepts the return type, and each return *this; returns no value. A call that uses the reference, as an argument ((a += b) += c), as the source of a copy (Bits c = (a |= b);), or of an assignment (c = (a |= b);), is an error naming the operator (rejectOwnObjectUse, at the three places a record value is read from an expression), so nothing reads a value that is not there; without it these were rejected with messages about something else. A function that returns *this on some paths and another object on others is not one: it returns a reference, which is still unsupported.
• Class invariants at reference and pointer parameters. The rule follows ACSL's weak type invariants (they hold at every function boundary) and Verus's type invariants (assumed of every value a function receives): for each parameter that refers to or points to a record with type invariants, the invariant, instantiated for that object, is a generated precondition, and through a mutable reference or pointer also a generated postcondition. The instance is converted with ThisSubstitute set to the parameter, which CXXThisExpr converts to, so value in the invariant reads l->value. A pointer's instance is guarded by p == nullptr ||. A callee's precondition is shown at each call, so an object that a caller breaks fails at the call (spoiled_argument), and a callee that breaks it fails at its return (spoil). Two cases are left out, both conservative: a pointer with a valid(p, n) extent addresses several objects, and gets no instance; an extent marker in the invariant is this's (B3-3: class invariants at public member functions and constructors #78), so in a parameter's instance it is true (DropExtentMarkers), and a member function that needs the extent cannot be called through such a parameter (first_through, bounds).
• Callee locals. summed lends local objects to operator+, which has a local object of its own. The record escape scan (recordStmtSafe, verify: Lend local records and addresses to callees that keep no address of them #71) rejected every allocation in the callee; it now accepts the callee's own automatic object unless it is initialized with an address it must not keep. An allocation from new makes the callee UsesDynamicStorage, which the scan rejects before it looks at a statement, as before.

Tests

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

• Bits: operator== and operator|= on locals (bits_use), each operand's invariant used by operator|=;
• Money: a member operator+= returning *this and a free operator+ returning a value (summed), a += a failing aliasing (self_add), and the returned reference used as an argument (chained), copied (copied), and assigned (assigned), each rejected;
• Level: a reference and a pointer parameter assuming the invariant (read, peek), a mutable reference keeping it (lower) and breaking it (spoil), a caller passing a broken object (spoiled_argument), and a null pointer (none);
• Span: an extent in the invariant, not carried by a reference (first_through).

suite/record_references.cpp: by_reference now verifies; it read a field of a record passed by reference and needed its invariant.

Mutants, each built on an assertions build and run on member_operators.cpp, class_invariants.cpp, record_references.cpp, member_functions.cpp, local_record_arguments.cpp, and type_invariant_lazy.cpp: 10 of 10 killed.

Mutant	Killed by
a member operator's first operand is an argument, not the object	member_operators (bits_use)
a member returning its own object returns a value	member_operators (Bits::operator|=)
parameters' invariants not assumed	member_operators (Bits::operator|=), record_references (by_reference)
parameters' invariants not restored	member_operators (spoil)
a pointer's instance not guarded by null	member_operators (none)
extent markers kept in a parameter's instance	member_operators (first_through: the marker on s->data is rejected)
a callee's own local objects stop it from being lent locals	member_operators (summed)
no check of the returned reference as an argument	member_operators (chained: "call arguments have order-dependent heap evaluations")
no check of it as a copy's source	member_operators (copied: "aggregate initialization and copying are unsupported")
no check of it as an assignment's source	member_operators (assigned: "unsupported aggregate initializer for an automatic object")

Open

• A pointer parameter with a valid(p, n) extent of a class with an invariant assumes nothing of its elements; quantifying the invariant over the extent is future work.
• An extent in a class invariant holds only for this: a parameter's instance does not carry it. Carrying it would need a field extent of the parameter's object (verify: State the extents of pointer fields, and separate pairs with an extent over their extents #72's synthetic parameters, for a field of an object that is not this).

Docs

• structs.rst: "Member operators", a checked example (Bits); the class-invariant rule for reference and pointer parameters, replacing the note that they assume nothing.
• Release notes: "Member operators"; the class-invariants entry extended to parameters.
• DESIGN.md: member operators and own-object returns; type invariants at reference and pointer parameters. ARCHITECTURE.md: member operators and parameters' invariants.

Checked

• The Verify suite on a release build at dcb9c9f: 464 passed (the exhaustive decoder filtered out), 1219 s with 40 workers. The commits after it add the check shared by copies and assignments and its tests; with them, member_operators.cpp, record_references.cpp, member_functions.cpp, and local_record_arguments.cpp pass.
• The doc pages' examples (structs, release notes, DESIGN, ARCHITECTURE): 36 checked (11 against the verdicts their pages show), 0 failed; docs_examples.test and docs_coverage.test pass; the site builds with warnings as errors.