[SwayamInSync]

The contracts of a class template's members and its type invariants were ignored with a warning (-Wcontract-unsupported), so no member of a class template was verified. Now a class template is verified in each specialization the translation unit instantiates, as a function template is (#80): a member's contract is instantiated with the member, and the class's invariants with the class.

namespace cv = cppverify;
template <typename T>
class Box {
public:
  Box(T v)
    cv::pre(0 <= v && v <= 20000)
    cv::post(value == v)
    : value(v) {}

  T twice() const
    cv::post(cv::result == 2 * value)
  {
    return value + value;
  }

  T value;

  cv::type_invariant(0 <= value && value <= 20000);
};

int doubled(int v)
  cv::pre(0 <= v && v <= 20000)
  cv::post(cv::result == 2 * v)
{
  Box<int> b(v);
  int d = b.twice();
  return d;
}

short doubled_short(short v)
  cv::pre(0 <= v && v <= 20000)
{
  Box<short> b(v);
  short d = b.twice();
  return d;
}

Verified: Box<int>::Box [backend=z3]
Verified: Box<int>::twice [backend=z3]
Verified: Box<short>::Box [backend=z3]
box.cpp:11:25: error: verification failed: Box<short>::twice [...::postcondition@11:25] (counterexample: ...) [backend=z3] [reason=counterexample]
box.cpp:34:15: note: in instantiation of member function 'Box<short>::twice' requested here
Verified: doubled [backend=z3]
Unresolved: doubled_short [backend=z3] [reason=callee.contract] (relies on the contract of Box<short>::twice, which is not established)

On the base (#80):

box.cpp:18:3: warning: contracts in class template 'Box' are not yet supported and are ignored [-Wcontract-unsupported]
box.cpp:5:3: warning: contracts in class template 'Box' are not yet supported and are ignored [-Wcontract-unsupported]
box.cpp:10:5: warning: contracts in class template 'Box' are not yet supported and are ignored [-Wcontract-unsupported]
box.cpp:25:3: error: doubled: call to function without a verification contract: Box<int>::Box
box.cpp:26:11: error: doubled: call to function without a verification contract: twice
box.cpp:26:11: error: doubled: unsupported expression: CXXMemberCallExpr
box.cpp:27:10: error: doubled: read of uninitialized local value: d
box.cpp:33:3: error: doubled_short: call to function without a verification contract: Box<short>::Box
box.cpp:34:13: error: doubled_short: call to function without a verification contract: twice
box.cpp:34:13: error: doubled_short: unsupported expression: CXXMemberCallExpr
box.cpp:35:10: error: doubled_short: read of uninitialized local value: d

(each error with its source line and caret).

Stacked on #80 (B2-2, the second part of plan item B2: templates verified per instantiation).

Design

• Members. The parser keeps the contracts of a class template's members (in-class ones are late-parsed in the complete class, as before) and their loop contracts. A member's contract is instantiated by B2-1: function templates verified in each specialization #80's InstantiateFunctionContract, lazily: where the member is used or defined, which C++ does only for the members a specialization uses (or every member, for an explicit instantiation definition). So a member no specialization uses is not verified, and is reported: warning: Box<T>::reset: member of a class template is not verified: this translation unit instantiates it in none of the class's specializations.
• Type invariants. The parser keeps a class template's invariants on its pattern, and InstantiateClassImpl instantiates them once the specialization is complete, eagerly, as a member static_assert is, with the specialization's this (CXXThisScopeRAII), into its TypeContractInfo, in the potentially-evaluated context of the class's instantiation, so a spec the invariant applies is instantiated too. An invariant is parsed with its class's this in scope, so Sema writes a field it names bare as this->field, which the instantiation rebuilds with the specialization's this. That made ActOnTypeInvariantExpr's rewriter of bare fields dead (an instrumented build found it never runs, on any test, doc page, or the forms tried: sizeof, decltype, quantifiers, unions, anonymous members, static members), and it is removed; it wrote this.field with a this of record type, which an instantiation could not have rebuilt.
• Binders in a class. Found while testing: a quantifier in a type invariant, cv::type_invariant(cv::forall(k, 0, 4, cells[k] >= 0)), declared its binder in the class, which made it a member: an assertions build stopped at the first lookup of k (Access specifier is AS_none inside a record decl), in an ordinary class too. A binder now belongs to the context around the class (Sema::getContractBinderContext), in the parser and in instantiation.
• Converter. collectFunctionCandidates visits, for each class template, the members of each specialization the translation unit instantiates (from its canonical declaration; an explicit instantiation's specialization in a declaration context is collected from its template only) and the pattern's members, for the warning, which isInstantiated decides from the instantiated members of the class's specializations, member function templates included. A member is named with its class's arguments (Box<int>::twice, Acc<int>::add<short>), and its diagnostics note in instantiation of member function 'Box<short>::twice' requested here.
• -Wcontract-unsupported has nothing left to report: the warning is removed, and its group stays, so a build that names it still builds.

Tests

• suite/class_templates.cpp (Z3, with a check that no proof is vacuous): Box with a constructor, members, and an invariant in two specializations, Box<signed char>::twice failing with its note, a Box<int> by reference with its invariant, an out-of-line member definition with a contract under an explicit instantiation (Pair<long>::larger), a member function template (Acc<int>::add<int>, add<short>), a spec template applied in the invariant (Digit<int>), quantified invariants in a class and a class template (Quad, Cells<int>), and the warnings for a member no specialization uses and a class template nothing instantiates.
• template_contract_errors.cpp: an invariant that does not fit the arguments is an error where the class is instantiated, a member's contract where the member is used, each with Clang's note.
• template_contracts.cpp: the class template's contracts compile without a warning.

The three fail on the base: class_templates.cpp gets the warnings and no verdicts for the class templates, and stops an assertions build at Quad's invariant (Access specifier is AS_none inside a record decl); template_contract_errors.cpp gets none of the class template errors it expects; template_contracts.cpp gets the warnings it no longer expects.

Mutants, each built on an assertions build and run on class_templates.cpp, template_contract_errors.cpp, template_contracts.cpp, function_templates.cpp, class_invariants.cpp, and type_invariant_lazy.cpp: 12 of 12 killed; a thirteenth, writing a bare field as this.field again, found the rewriter dead, which is removed.

Mutant	Killed by
the parser drops class template members' contracts	class_templates, template_contract_errors
the parser drops class template invariants	class_templates, template_contract_errors
invariants not instantiated	class_templates, template_contract_errors
invariants instantiated without this	class_templates, template_contract_errors, template_contracts
instantiated invariants not converted to bool	template_contract_errors (Holder<Pair>)
class template specializations not collected	class_templates
an explicit instantiation's specialization also collected from its context	class_templates (Pair<long>::larger once)
members of class templates not looked for (no warning)	class_templates
the pattern's members not collected (no warning)	class_templates
pattern members named without their parameters	class_templates (Box<T>::reset)
members noted as function template specializations	class_templates (the note)
binders declared in the class	class_templates (Quad: the assertion)

Docs

• structs.rst: "Class templates", a checked example (Box), the rules.
• functions-loops.rst: the templates section points to it. limitations.rst: class templates supported.
• Release notes: "Templates" covers class templates; "Contracts in templates" no longer says they are ignored.
• DESIGN.md: templates and member functions. ARCHITECTURE.md: class templates.

Checked

• The Verify suite on a release build: 467 passed (the exhaustive decoder filtered out), 1280 s with 40 workers.
• The doc pages' examples (structs, functions-loops, limitations, release notes, DESIGN, ARCHITECTURE): 49 checked (20 against the verdicts their pages show), 0 failed; docs_examples.test and docs_coverage.test pass; the site builds with warnings as errors.