[SwayamInSync]

A function template's contracts were ignored with a warning, so none of its specializations was verified, and verified code could not call one. Now each specialization a translation unit instantiates is verified as a function of its own, with its contract instantiated as its body is:

namespace cv = cppverify;
template <typename T>
T twice(T x)
  cv::pre(0 <= x && x <= 30000)
  cv::post(cv::result == 2 * x)
{
  return x + x;
}

int twice_int(int x)
  cv::pre(0 <= x && x <= 30000)
  cv::post(cv::result == 2 * x)
{
  int r = twice(x);
  return r;
}

short twice_short(short x)
  cv::pre(0 <= x && x <= 30000)
{
  short r = twice(x);
  return r;
}

Verified: twice<int> [backend=z3]
templates.cpp:5:23: error: verification failed: twice<short> [...::postcondition@5:23] (counterexample: ...) [backend=z3] [reason=counterexample]
templates.cpp:21:13: note: in instantiation of function template specialization 'twice<short>' requested here
Verified: twice_int [backend=z3]
Unresolved: twice_short [backend=z3] [reason=callee.contract] (relies on the contract of twice<short>, which is not established)

x + x is an int, which a short result holds only up to 32767. On the base (#79), no specialization is verified and both callers are errors:

templates.cpp:3:3: warning: contracts in function template 'twice' are not yet supported and are ignored [-Wcontract-unsupported]
templates.cpp:14:11: error: twice_int: call to function without a verification contract: twice
templates.cpp:14:11: error: twice_int: unsupported expression: CallExpr
templates.cpp:15:10: error: twice_int: read of uninitialized local value: r
templates.cpp:21:13: error: twice_short: call to function without a verification contract: twice
templates.cpp:21:13: error: twice_short: unsupported expression: CallExpr
templates.cpp:22:10: error: twice_short: read of uninitialized local value: r

(each error with its source line and caret).

Stacked on #79 (B2-1 of plan item B2: templates verified per instantiation; class templates follow).

Design

What a template means depends on the types and overloads its arguments bring, which C++ fixes only where it is instantiated, so a template is verified in each specialization the translation unit instantiates, by a use or by an explicit instantiation, the position of Kani and CBMC (Creusot and Prusti verify generic Rust once because trait bounds fix its meaning). A contracted template that nothing instantiates is reported, not verified.

• Contracts instantiated lazily, as exception specifications are. The parser keeps a function template's contract on its pattern. Sema::InstantiateFunctionContract instantiates it where a specialization is odr-used (MarkFunctionReferenced, which a trusted template without a definition, or an extern template, needs) and where its definition is instantiated, once per specialization: the specialization's FunctionContractInfo is recorded first, so a use in its own contract stops there. It runs in the specialization's context (ContextRAII, which gives a member its this) and an evaluation context of its own: the use that asks for it may be in the middle of a caller's full expression, whose temporaries' cleanups the contract would otherwise take (template_contracts.cpp checks the caller keeps its ExprWithCleanups). Its LocalInstantiationScope maps the pattern's parameters, and so those of every redeclaration (Clang identifies them by position), so the clauses may be written on a declaration before the definition or on a definition after a declaration that names the parameters otherwise. An unused specialization's contract is never instantiated, so arguments a contract does not fit are an error only where used, with Clang's in instantiation of note.
• Clauses rebuilt with the parser's checks. SubstFunctionContract runs TreeTransform::TransformFunctionContract: each condition is converted to bool (TransformContractCondition), each measure must be an integer (TransformContractMeasure, through Sema::ActOnContractMeasure, which the parser now uses too), and a range is rebuilt by ActOnContractRange (TransformContractFootprint). Quantifiers and choices are rebuilt by Sema::BuildContractBinderExpr (bounds integers, body a condition), shared with the parser; cppverify::result takes the instantiated return type. In the body, an assertion's condition is checked again, a loop's contract is transformed with the loop and attached to the rebuilt loop (which is rebuilt whenever a clause changed, even if its condition and body did not), and trigger marks are kept (TransformExpr).
• Variadic templates. Found while testing: in a fold over a quantifier, (cv::forall(k, 0, ns, p[k] < 10) && ...), each element is the pattern transformed again, and the binder was mapped once for all of them; a right fold transforms its last element first, so the others read its variable. Each quantifier and choice now binds in a LocalInstantiationScope of its own (TemplateInstantiator), as a lambda's locals do, and the block of check(forall(k, ...)) by { ... } is given the instantiated k. The parameters a pack expands to share its name; they are named as C++26 indexes a pack, ns...[1] (nameParameters), counterexamples included.
• Dependence. Found while testing: ResultExpr, OldExpr, and the quantifiers had no dependence, so in a template cv::post(cv::result > 0) and cv::old(x) > 0 did not compile (invalid operands to binary expression ('T' and 'int')). They now take the dependence of their type (result), operand (old), or operands (quantifiers and choices, as values).
• Converter. collectFunctionCandidates adds after each function template the specializations the translation unit instantiates (from its canonical declaration, since its redeclarations share them), with their definition or, without one, their contract. A specialization is named with its arguments (functionName: maxv<int>, Meter::add<short>), and one the verifier cannot represent (maxv<double>) fails alone. An uncontracted constexpr template in a contract is a spec in each specialization (bigger_of<int>).
• Instantiation notes. The converter records where each specialization is instantiated, and the driver prints it after each of its errors and warnings as Clang does, note: in instantiation of function template specialization 'twice<short>' requested here (JSON instantiated_at).

Tests

• suite/function_templates.cpp (Z3, with a check that no proof is vacuous): per-specialization verdicts (maxv<int>, maxv<long> by explicit instantiation, twice<int> and twice<signed char>, total<int> and total<short> with a loop contract, bits<short> and bits<long long> with sizeof(T)), a recursive template, ghost code of the template's type, a spec template, a contract on a declaration (half<int>, verified once) and one on a definition after a declaration (third<int>), a member function template, variadic templates (a fold over a quantifier, ns...[0] in a counterexample), a trusted template without a definition, cppverify::result compared with a constant, a loop whose condition and body do not change, a trigger (Layer 3), a constexpr template spec, maxv<double> failing alone, the notes (text and JSON), and the warning for a template nothing instantiates.
• template_contract_errors.cpp (frontend, -verify): a postcondition, precondition, measure, quantifier bound, range, assertion, and loop invariant that do not fit the arguments are errors with the instantiation note; arguments that fit, and an unevaluated use, are not.
• template_contracts.cpp: function template contracts kept; cv::result > 0 and cv::old(v) > 0 compile; a caller whose argument is a temporary keeps its cleanups.
• unused_template.cpp, z3_calls_fail_closed.cpp: the warning for a contracted template nothing instantiates replaces the error and the warning.

All five fail on the base: the frontend tests get the ignored-contract warnings and none of the errors they expect (template_contracts.cpp gets invalid operands to binary expression ('T' and 'int') for cv::result > 0 and cv::old(v) > 0), and function_templates.cpp does not compile there (invalid operands to binary expression ('int' and 'T') for 0 <= cv::result).

Mutants, each built on an assertions build and run on the five tests: 23 of 23 killed. Three more found code that changed nothing, which is removed: mapping the parameters of the declaration the contract is written on rather than the pattern's (Clang keys each parameter by the canonical declaration's), a this scope (the specialization's context gives it), and copying ghost marks (ghost locals are found by their ghost block, and Sema checks every use in the pattern).

Mutant	Killed by
the parser drops function template contracts	function_templates, template_contract_errors, z3_calls_fail_closed
no contract where a specialization is used	function_templates (next_of<int>, trusted, without a definition)
no contract with the definition	function_templates (maxv<long>, an explicit instantiation)
conditions not converted at instantiation	template_contract_errors (needs<Pair>)
cv::result keeps the pattern's type	function_templates
cv::result not dependent	function_templates, template_contracts (cv::result > 0)
quantifiers and choices not dependent	function_templates (a fold over forall: "pack expansion does not contain any unexpanded parameter packs")
loop contracts not transformed	function_templates, template_contract_errors
a changed loop contract leaves an unchanged loop unrebuilt	function_templates (size_of, while (false))
trigger marks dropped	function_templates (Layer 3 trigger)
specializations not collected	function_templates
redeclarations collect them again	function_templates (half<int> once)
no instantiation notes	function_templates (text and JSON)
contracts instantiated for unevaluated uses	template_contract_errors (decltype)
no evaluation context of its own	template_contracts (the caller's ExprWithCleanups)
measures not checked at instantiation	template_contract_errors (steps<int *>)
ranges not rebuilt	template_contract_errors (fills<double>)
quantifier bounds not checked	template_contract_errors (all_below<double>)
no warning for an uninstantiated template	unused_template, z3_calls_fail_closed, function_templates
names without template arguments	unused_template, function_templates
binders share one scope in a pack expansion	function_templates (first_small<int, int>)
a check-by block loses its variable	template_contracts
a pack's elements share one name	function_templates (product_of<int, int>)

Open

• Class templates (B2-2): their members' contracts and type invariants are still ignored with -Wcontract-unsupported; B2-2: class templates verified in each specialization #81 verifies them.
• std::min and std::max (A18) stay skipped with the rest of namespace std.
• cppverify::result of a function returning a reference is a prvalue of reference type in Sema, so every use is rejected; a small fix of its own.

Docs

• functions-loops.rst: "Templates" rewritten, with a checked example (twice), the rules, and what changed.
• limitations.rst: function templates supported, class template members not yet.
• Release notes: "Function templates".
• DESIGN.md: "Templates", Sema rule 13. ARCHITECTURE.md: function templates (instantiation, TreeTransform, converter, notes).

Checked

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