[SwayamInSync]

Constructors were not verified: a contracted one was an error (constructors are not verified yet), and a class with one was not a supported type, so a local of it could not be declared. Now a constructor of a trivially copyable class without bases is verified, and runs where its objects are defined:

struct Ring {
  Ring()
    cv::post(head == 0 && count == 0)
    cv::post(cv::forall(k, 0, 8, buf[k] == 0))
    : head(0), count(0)
  {
    for (int i = 0; i < 8; i = i + 1)
      cv::invariant(0 <= i && i <= 8)
      cv::invariant(head == 0 && count == 0)
      cv::invariant(cv::forall(k, 0, i, buf[k] == 0))
      cv::decreases(8 - i)
    {
      buf[i] = 0;
    }
  }

  Ring(int first)
    cv::post(head == 0 && count == 1 && buf[0] == first)
    : head(0), count(1)
  {
    buf[0] = first;
  }

  int buf[8];
  int head;
  int count;
};

int fresh()
  cv::post(cv::result == 0)
{
  Ring r;
  return r.count + r.buf[7];
}

Verified: Ring::Ring [backend=z3]
ring.cpp:24:7: error: verification failed: Ring::Ring [...::initialization@24:7#2] (counterexample: ...) [backend=z3] [reason=counterexample]
Verified: fresh [backend=z3]

The second constructor leaves buf[1] to buf[7] uninitialized; the failure is located at the member.

Stacked on #75 (B3-2 of plan item B3; the loops of constructors such as Ring() need #74 and #75). Class invariants and member operators follow.

Design

From Dafny's two-phase constructors (the fields of an object that exists are assigned before new;, every field definitely), C++'s [class.base.init] (members initialized in declaration order) and [basic.life] (the object's lifetime begins in storage that exists before it), on top of B3-1's this:

• The object is the caller's storage. this carries a lifetime companion (__cppverify_constructed_lifetime), so the constructor's accesses are those of local storage, initialization checked, and its generated precondition is that every leaf of *this is valid with that identity: one live allocation, which the caller shows for its object. Nothing is assumed about the object's initialization, so a member reads as initialized only once the constructor has written it.
• Members in order. The constructor's member initializers run before its body, from inits(), which Sema keeps in execution order whatever the written one: the member's initializer, else its in-class initializer (CXXDefaultInitExpr), else its type's default construction.
• Every member initialized. At the constructor's end every leaf of its object must be initialized (emitConstructedChecks, kind initialization, located at the member).
• Callers. A local initialized by a constructor that is not trivial is kept in memory; T x(args), T x{args}, and T x = T(args) pass its address as this (appendConstruction). The call checks the object's validity but not its initialization, and after the call every leaf is initialized, with the postcondition describing it. An implicit or defaulted default constructor is its member initializers, run in place, recursively for members of class type. A constructor the class provides needs a contract, as any function a verified one calls.
• Contract. A constructor's precondition cannot read its object, whose lifetime has not begun, and cppverify::aliases cannot name this, a new object; its frame is *this and the footprints it lists.
• Types. A record is a supported type and layout when it is trivially copyable, which was "trivial": copies stay member-wise and nothing runs at the end of its lifetime, while its constructors run as calls or as their initializers. Only a copy or move constructor the class does not provide is taken as a member-wise copy.
• Fail closed, each an error of its function: delegating constructors, classes not trivially copyable (a destructor or a copy operation of their own), members whose class provides a constructor, reference, bit-field, and anonymous members, classes over 256 bytes, arrays of objects with constructors. A member function called on the object before every member is initialized reads it as initialized, which C++ does not require, so that call is construct.unsupported, as an out-parameter's is.

Two first designs were wrong, and the mutants showed it:

• A fresh allocation at this made every constructor verify vacuously: an object's validity is a live owner, and the allocation assumed none there.
• Clearing the object's initialization at entry was redundant (mutant K2 survived): nothing about it is assumed, and no check needs a cell uninitialized. So was registering this as a local object for loop frames (K14 survived): its origin, the entry object, already frames the loop, and a false claim about Copy4 below still fails in 0.5 s. Both were removed.

Tests

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

• Counter() with member initializers and Counter(int) with a body; callers Counter c;, Counter d(5);, Counter e{1};, a member call after construction, and the values the postconditions give;
• T x = T(3) and a copy of a constructed object;
• construction writes only its object (others_kept);
• a member left uninitialized (Partial: initialization at the member) and a member read before it is initialized (Early, whose initializers are written out of declaration order);
• in-class initializers of the members a constructor does not name; an implicit default constructor, also through a member of class type (point_sum, holder_sum);
• a member function called before every member is initialized (construct.unsupported);
• a loop that initializes an array member (Ring) and one that keeps its source (Copy4, with cppverify::old);
• a constructor writing another object (Logged);
• errors: a precondition reading the object, a delegating constructor, a call of an uncontracted constructor.

member_functions.cpp: the constructor of a class with a destructor is now rejected for that.

Mutants, each built on an assertions build and run on constructors.cpp, member_functions.cpp, local_record_arguments.cpp, loop_local_frames.cpp, and located_errors.cpp: 12 of 12 killed (the two that survived, above, are gone with the code they mutated).

Mutant	Killed by
constructors rejected (the base)	constructors, member_functions
no check that every member is initialized	constructors (Partial)
callers do not hold an initialized object after the call	constructors
callers check the object's initialization	constructors
this initialized at entry, as a member function's	constructors
member initializers not run	constructors
implicit constructors not run	constructors (point_sum)
a precondition may read the object	constructors
delegating constructors accepted	constructors
constructed locals not kept in memory	constructors
records must be trivial (the base)	constructors
this without its lifetime companion	constructors

Docs

• structs.rst: "Constructors", a checked example (Ring, fresh), and what is not supported yet.
• limitations.rst: constructors supported, what is not.
• Release notes: "Constructors"; "Member functions" no longer lists them as errors.
• DESIGN.md: 3g. ARCHITECTURE.md: constructors.

Open

• Passing or returning a constructed object by value: an object kept in memory is copied into a flattened local field by field, but a by-value argument or return c; of one is aggregate value use of an automatic object is unsupported. Next.
• Members whose class provides a constructor (a nested call at the member's address), arrays of objects, new of a record.

Checked

• The Verify suite on a release build: 461 passed (the exhaustive decoder filtered out), 1214 s with 40 workers, before the unreached registration of this was removed; after it, constructors.cpp, member_functions.cpp, and loop_local_frames.cpp pass.
• The doc pages' examples (structs, DESIGN): 33 checked, 0 failed; docs_examples.test and docs_coverage.test pass.