From 0632d6cd94b8b2006c5e76a74ba2c77cc7e9d283 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:56 +0530 Subject: [PATCH 01/64] verify: Give cppverify::result, cppverify::old, and quantifiers the dependence of their type or operands. --- clang/include/clang/AST/ExprContract.h | 25 ++++++++++++++++++++----- 1 file changed, 20 insertions(+), 5 deletions(-) diff --git a/clang/include/clang/AST/ExprContract.h b/clang/include/clang/AST/ExprContract.h index 9a0b2802a0..2c88f4e2ba 100644 --- a/clang/include/clang/AST/ExprContract.h +++ b/clang/include/clang/AST/ExprContract.h @@ -23,6 +23,19 @@ namespace clang { // Forward declaration for serialization friend access. class ASTStmtReader; +/// The dependence of a quantifier or a choice: its operands', with its own +/// type fixed. In a template, `forall(k, 0, n, p[k] > 0)` over a `T *p` is +/// value-dependent, though it is a bool. +inline ExprDependence binderExprDependence(const Expr *Lo, const Expr *Hi, + const Expr *Body) { + ExprDependence D = Body ? Body->getDependence() : ExprDependence::None; + if (Lo) + D |= Lo->getDependence(); + if (Hi) + D |= Hi->getDependence(); + return turnTypeToValueDependence(D); +} + /// ForallExpr - Represents a universal quantifier: /// forall(binder, lo, hi, body) /// means: for all binder in [lo, hi), body holds; forall(binder, body) @@ -46,7 +59,7 @@ class ForallExpr : public Expr { SubExprs[LO] = Lo; SubExprs[HI] = Hi; SubExprs[BODY] = Body; - setDependence(ExprDependence::None); + setDependence(binderExprDependence(Lo, Hi, Body)); } explicit ForallExpr(EmptyShell Empty) : Expr(ForallExprClass, Empty) {} @@ -101,7 +114,7 @@ class ExistsExpr : public Expr { SubExprs[LO] = Lo; SubExprs[HI] = Hi; SubExprs[BODY] = Body; - setDependence(ExprDependence::None); + setDependence(binderExprDependence(Lo, Hi, Body)); } explicit ExistsExpr(EmptyShell Empty) : Expr(ExistsExprClass, Empty) {} @@ -156,7 +169,7 @@ class ContractChooseExpr : public Expr { SubExprs[LO] = Lo; SubExprs[HI] = Hi; SubExprs[BODY] = Body; - setDependence(ExprDependence::None); + setDependence(binderExprDependence(Lo, Hi, Body)); } explicit ContractChooseExpr(EmptyShell Empty) : Expr(ContractChooseExprClass, Empty) {} @@ -202,7 +215,7 @@ class OldExpr : public Expr { : Expr(OldExprClass, Inner->getType(), VK_PRValue, OK_Ordinary), OldLoc(OldLoc), LParenLoc(LParenLoc), RParenLoc(RParenLoc), Inner(Inner) { - setDependence(ExprDependence::None); + setDependence(Inner->getDependence()); } explicit OldExpr(EmptyShell Empty) : Expr(OldExprClass, Empty) {} @@ -237,7 +250,9 @@ class ResultExpr : public Expr { QualType ReturnType) : Expr(ResultExprClass, ReturnType, VK_PRValue, OK_Ordinary), ResultLoc(ResultLoc), EndLoc(EndLoc) { - setDependence(ExprDependence::None); + // In a template, the return type may depend on its parameters. + setDependence( + toExprDependenceForImpliedType(ReturnType->getDependence())); } explicit ResultExpr(EmptyShell Empty) : Expr(ResultExprClass, Empty) {} From 6e3a800c7f4eb9039da999612e3d43ebe3727421 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:56 +0530 Subject: [PATCH 02/64] verify: Declare contract instantiation for template specializations and the checks it shares with the parser. --- clang/include/clang/Sema/Sema.h | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/clang/include/clang/Sema/Sema.h b/clang/include/clang/Sema/Sema.h index b74f1bd3f7..d34717d871 100644 --- a/clang/include/clang/Sema/Sema.h +++ b/clang/include/clang/Sema/Sema.h @@ -10394,6 +10394,17 @@ class Sema final : public SemaBase { ExprResult ActOnContractRange(Expr *Base, Expr *Lower, SourceLocation ColonLoc, Expr *Length, SourceLocation RBLoc); + /// A component of a decreases clause, which must be an integer. + ExprResult ActOnContractMeasure(ExprResult E); + + /// forall, exists, or choose (\p Kind) over \p Binder: its bounds must be + /// integers and its body a condition. + ExprResult BuildContractBinderExpr(Stmt::StmtClass Kind, + SourceLocation KeywordLoc, + SourceLocation LParenLoc, + SourceLocation RParenLoc, VarDecl *Binder, + Expr *Lo, Expr *Hi, Expr *Body); + /// Rewrite unqualified field names to this->field for type_invariant(expr). ExprResult ActOnTypeInvariantExpr(ExprResult E, CXXRecordDecl *Record); @@ -14336,6 +14347,20 @@ class Sema final : public SemaBase { void InstantiateExceptionSpec(SourceLocation PointOfInstantiation, FunctionDecl *Function); + /// Instantiate the contract of a function template specialization, or of + /// a member of a class template specialization, from its pattern's, when + /// it is used or defined and has none yet. (Contracts are instantiated + /// lazily, as exception specifications are: an unused member's contract is + /// never instantiated.) + void InstantiateFunctionContract(SourceLocation PointOfInstantiation, + FunctionDecl *Function); + + /// The contract \p From of a template, with \p TemplateArgs substituted, + /// in \p To. Returns true on error. + bool SubstFunctionContract(const FunctionContractInfo &From, + FunctionContractInfo &To, + const MultiLevelTemplateArgumentList &TemplateArgs); + /// Instantiate (or find existing instantiation of) a function template with a /// given set of template arguments. /// From 6af1d1ec535d81f8b26a077137a07a1ae3b27b16 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:56 +0530 Subject: [PATCH 03/64] verify: Check a decreases component and a quantifier's bounds and body in Sema, for the parser and for instantiation. --- clang/lib/Sema/SemaContract.cpp | 38 +++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/clang/lib/Sema/SemaContract.cpp b/clang/lib/Sema/SemaContract.cpp index 8eef44eae8..08df4d87cc 100644 --- a/clang/lib/Sema/SemaContract.cpp +++ b/clang/lib/Sema/SemaContract.cpp @@ -309,6 +309,44 @@ ExprResult Sema::ActOnContractRange(Expr *Base, Expr *Lower, OK_Ordinary, ColonLoc, RBLoc); } +ExprResult Sema::ActOnContractMeasure(ExprResult E) { + if (E.isInvalid() || E.get()->isTypeDependent() || + E.get()->getType()->isIntegerType()) + return E; + Diag(E.get()->getExprLoc(), diag::err_contract_decreases_not_int); + return ExprError(); +} + +ExprResult Sema::BuildContractBinderExpr(Stmt::StmtClass Kind, + SourceLocation KeywordLoc, + SourceLocation LParenLoc, + SourceLocation RParenLoc, + VarDecl *Binder, Expr *Lo, Expr *Hi, + Expr *Body) { + for (Expr *Bound : {Lo, Hi}) + if (Bound && !Bound->isTypeDependent() && + !Bound->getType()->isIntegerType()) { + Diag(Bound->getExprLoc(), diag::err_contract_quantifier_bound_not_int); + return ExprError(); + } + ExprResult Condition = ActOnContractCondition(Body); + if (Condition.isInvalid()) + return ExprError(); + switch (Kind) { + case Stmt::ContractChooseExprClass: + return new (Context) ContractChooseExpr(KeywordLoc, LParenLoc, RParenLoc, + Binder, Lo, Hi, Condition.get(), + Binder->getType()); + case Stmt::ForallExprClass: + return new (Context) ForallExpr(KeywordLoc, LParenLoc, RParenLoc, Binder, + Lo, Hi, Condition.get(), Context.BoolTy); + default: + assert(Kind == Stmt::ExistsExprClass && "not a quantifier or a choice"); + return new (Context) ExistsExpr(KeywordLoc, LParenLoc, RParenLoc, Binder, + Lo, Hi, Condition.get(), Context.BoolTy); + } +} + ExprResult Sema::ActOnTypeInvariantExpr(ExprResult E, CXXRecordDecl *Record) { if (E.isInvalid() || !Record) return E; From c1382bcba88b20a075f88cb954267e2f49e02aca Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:57 +0530 Subject: [PATCH 04/64] verify: Keep a function template's contract and check its clauses through Sema. --- clang/lib/Parse/ParseCppVerify.cpp | 76 ++++++++++-------------------- 1 file changed, 24 insertions(+), 52 deletions(-) diff --git a/clang/lib/Parse/ParseCppVerify.cpp b/clang/lib/Parse/ParseCppVerify.cpp index 8c5d38537e..0ea63396c3 100644 --- a/clang/lib/Parse/ParseCppVerify.cpp +++ b/clang/lib/Parse/ParseCppVerify.cpp @@ -534,12 +534,11 @@ void Parser::ParseFunctionContractClauseList(FunctionContractClauses &Clauses) { // expressions. Parse each with ParseAssignmentExpression so the comma is // a tuple separator, not the C comma operator. do { - ExprResult E = finishCppVerifyExpression(ParseAssignmentExpression()); + ExprResult E = ParseAssignmentExpression(); if (E.isInvalid()) break; - if (!E.get()->isTypeDependent() && !E.get()->getType()->isIntegerType()) - Diag(E.get()->getExprLoc(), diag::err_contract_decreases_not_int); - else + E = finishCppVerifyExpression(Actions.ActOnContractMeasure(E)); + if (E.isUsable()) I.Decreases.push_back(E.get()); if (Tok.is(tok::comma)) ConsumeToken(); @@ -673,17 +672,14 @@ void Parser::attachFunctionContract(Decl *Result, I.MayDiverge.isInvalid() && I.Inductive.isInvalid() && I.BehaviorChecks.empty() && !I.IsSpec && !I.IsProof)) return; - // Templates are not verified yet: their clauses are ignored, as a member - // function's are. - if (FD->isTemplated() && !I.IsSpec && !I.IsProof) { - // A member of a class template is named by its class. - const auto *Method = dyn_cast(FD); - if (Method && Method->getParent()->isTemplated()) - Diag(FD->getLocation(), diag::warn_contract_template_unsupported) - << 1 << Method->getParent(); - else - Diag(FD->getLocation(), diag::warn_contract_template_unsupported) - << 0 << FD; + // A function template's clauses are instantiated with each of its + // specializations. Members of class templates are not verified yet: their + // clauses are ignored. + if (const auto *Method = dyn_cast(FD); + Method && Method->getParent()->isTemplated() && !I.IsSpec && + !I.IsProof) { + Diag(FD->getLocation(), diag::warn_contract_template_unsupported) + << 1 << Method->getParent(); return; } FunctionContractInfo &FCI = Ctx.getOrCreateFunctionContract(FD); @@ -835,17 +831,13 @@ void Parser::ParseLoopContractClauses(LoopContractInfo &Contract) { // Parse each component with ParseAssignmentExpression so the comma is a // tuple separator, not the C comma operator. while (true) { - ExprResult D = finishCppVerifyExpression(ParseAssignmentExpression()); + ExprResult D = ParseAssignmentExpression(); + if (D.isUsable()) + D = finishCppVerifyExpression(Actions.ActOnContractMeasure(D)); if (D.isInvalid()) { SkipUntil(tok::r_paren, StopAtSemi); return; } - if (!D.get()->isTypeDependent() && - !D.get()->getType()->isIntegerType()) { - Diag(D.get()->getExprLoc(), diag::err_contract_decreases_not_int); - SkipUntil(tok::r_paren, StopAtSemi); - return; - } Contract.Decreases.push_back(D.get()); if (Tok.isNot(tok::comma)) break; @@ -867,10 +859,11 @@ void Parser::attachLoopContract(StmtResult &Loop, LoopContractInfo &Contract) { (Contract.Invariants.empty() && Contract.Decreases.empty() && Contract.MayDiverge.isInvalid() && Contract.Modifies.empty())) return; - if (const FunctionDecl *FD = Actions.getCurFunctionDecl(); - FD && FD->isTemplated()) { + if (const auto *Method = + dyn_cast_or_null(Actions.getCurFunctionDecl()); + Method && Method->getParent()->isTemplated()) { Diag(Loop.get()->getBeginLoc(), diag::warn_contract_template_unsupported) - << 0 << FD; + << 1 << Method->getParent(); return; } Actions.getASTContext().getOrCreateLoopContract(Loop.get()) = @@ -1379,23 +1372,6 @@ ExprResult Parser::ParseQuantifierExpr() { return ExprError(); } - // Validate bound types: lo and hi must be integer. - for (const ExprResult &Bound : {Lo, Hi}) - if (Bound.isUsable() && !Bound.get()->isTypeDependent() && - !Bound.get()->getType()->isIntegerType()) { - Diag(Bound.get()->getExprLoc(), - diag::err_contract_quantifier_bound_not_int); - SkipUntil(tok::r_paren, StopAtSemi); - return ExprError(); - } - - // Validate body: must be contextually convertible to bool. - ExprResult BodyBool = Actions.ActOnContractCondition(Body); - if (BodyBool.isInvalid()) { - SkipUntil(tok::r_paren, StopAtSemi); - return ExprError(); - } - if (Tok.isNot(tok::r_paren)) { Diag(Tok, diag::err_contract_expected_rparen) << Keyword; SkipUntil(tok::r_paren, StopAtSemi); @@ -1403,16 +1379,12 @@ ExprResult Parser::ParseQuantifierExpr() { } SourceLocation RParenLoc = ConsumeParen(); - Expr *LoE = Lo.isUsable() ? Lo.get() : nullptr; - Expr *HiE = Hi.isUsable() ? Hi.get() : nullptr; - if (IsChoose) - return new (Ctx) ContractChooseExpr(KwLoc, LParenLoc, RParenLoc, BoundVar, - LoE, HiE, BodyBool.get(), Ctx.IntTy); - if (IsForall) - return new (Ctx) ForallExpr(KwLoc, LParenLoc, RParenLoc, BoundVar, LoE, HiE, - BodyBool.get(), Ctx.BoolTy); - return new (Ctx) ExistsExpr(KwLoc, LParenLoc, RParenLoc, BoundVar, LoE, HiE, - BodyBool.get(), Ctx.BoolTy); + return Actions.BuildContractBinderExpr( + IsChoose ? Stmt::ContractChooseExprClass + : IsForall ? Stmt::ForallExprClass + : Stmt::ExistsExprClass, + KwLoc, LParenLoc, RParenLoc, BoundVar, Lo.isUsable() ? Lo.get() : nullptr, + Hi.isUsable() ? Hi.get() : nullptr, Body.get()); } /// Parse cppverify::old(expr) From 7c37848a3942e0ae091e7d4639cffa78ea856c89 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:57 +0530 Subject: [PATCH 05/64] verify: Transform contract clauses with the parser's checks, loop contracts with their loops, and trigger marks. --- clang/lib/Sema/TreeTransform.h | 254 +++++++++++++++++++++++++++++---- 1 file changed, 225 insertions(+), 29 deletions(-) diff --git a/clang/lib/Sema/TreeTransform.h b/clang/lib/Sema/TreeTransform.h index 78122a51e5..4a3583ac12 100644 --- a/clang/lib/Sema/TreeTransform.h +++ b/clang/lib/Sema/TreeTransform.h @@ -570,6 +570,25 @@ class TreeTransform { /// Transform the variable a quantifier or a choice binds. VarDecl *TransformContractBinder(VarDecl *Binder); + /// Transform a contract clause's expression and check it as the parser + /// does: a condition, a component of a decreases clause, a footprint of a + /// modifies clause, or a term (an argument of aliases or reads). + ExprResult TransformContractCondition(Expr *E); + ExprResult TransformContractMeasure(Expr *E); + ExprResult TransformContractFootprint(Expr *E); + ExprResult TransformContractTerm(Expr *E); + + /// Transform the contract of a function, from \p From into \p To. + /// Returns true on error. + bool TransformFunctionContract(const FunctionContractInfo &From, + FunctionContractInfo &To); + + /// Transform the contract of the loop \p S, if it has one, into \p To; + /// \p Changed says whether any of its clauses changed. Returns true on + /// error. + bool TransformLoopContract(Stmt *S, std::optional &To, + bool &Changed); + /// Transform the given declaration, which was the first part of a /// nested-name-specifier in a member access expression. /// @@ -4451,16 +4470,23 @@ ExprResult TreeTransform::TransformExpr(Expr *E) { if (!E) return E; + ExprResult Result = E; switch (E->getStmtClass()) { case Stmt::NoStmtClass: break; #define STMT(Node, Parent) case Stmt::Node##Class: break; #define ABSTRACT_STMT(Stmt) #define EXPR(Node, Parent) \ - case Stmt::Node##Class: return getDerived().Transform##Node(cast(E)); + case Stmt::Node##Class: \ + Result = getDerived().Transform##Node(cast(E)); \ + break; #include "clang/AST/StmtNodes.inc" } - return E; + // A quantifier's trigger term is one in what it becomes too. + if (Result.isUsable() && Result.get() != E && + SemaRef.Context.isTriggerTerm(E)) + SemaRef.Context.markTriggerTerm(Result.get()); + return Result; } template @@ -8492,13 +8518,21 @@ TreeTransform::TransformWhileStmt(WhileStmt *S) { if (Body.isInvalid()) return StmtError(); - if (!getDerived().AlwaysRebuild() && + std::optional Contract; + bool ContractChanged = false; + if (getDerived().TransformLoopContract(S, Contract, ContractChanged)) + return StmtError(); + + if (!getDerived().AlwaysRebuild() && !ContractChanged && Cond.get() == std::make_pair(S->getConditionVariable(), S->getCond()) && Body.get() == S->getBody()) return Owned(S); - return getDerived().RebuildWhileStmt(S->getWhileLoc(), S->getLParenLoc(), - Cond, S->getRParenLoc(), Body.get()); + StmtResult Result = getDerived().RebuildWhileStmt( + S->getWhileLoc(), S->getLParenLoc(), Cond, S->getRParenLoc(), Body.get()); + if (Contract && Result.isUsable()) + SemaRef.Context.getOrCreateLoopContract(Result.get()) = std::move(*Contract); + return Result; } template @@ -8519,14 +8553,22 @@ TreeTransform::TransformDoStmt(DoStmt *S) { if (Cond.isInvalid()) return StmtError(); - if (!getDerived().AlwaysRebuild() && + std::optional Contract; + bool ContractChanged = false; + if (getDerived().TransformLoopContract(S, Contract, ContractChanged)) + return StmtError(); + + if (!getDerived().AlwaysRebuild() && !ContractChanged && Cond.get() == S->getCond() && Body.get() == S->getBody()) return S; - return getDerived().RebuildDoStmt(S->getDoLoc(), Body.get(), S->getWhileLoc(), - /*FIXME:*/S->getWhileLoc(), Cond.get(), - S->getRParenLoc()); + StmtResult Result = getDerived().RebuildDoStmt( + S->getDoLoc(), Body.get(), S->getWhileLoc(), + /*FIXME:*/ S->getWhileLoc(), Cond.get(), S->getRParenLoc()); + if (Contract && Result.isUsable()) + SemaRef.Context.getOrCreateLoopContract(Result.get()) = std::move(*Contract); + return Result; } template @@ -8576,16 +8618,24 @@ TreeTransform::TransformForStmt(ForStmt *S) { SemaRef.OpenACC().ActOnForStmtEnd(S->getBeginLoc(), Body); - if (!getDerived().AlwaysRebuild() && + std::optional Contract; + bool ContractChanged = false; + if (getDerived().TransformLoopContract(S, Contract, ContractChanged)) + return StmtError(); + + if (!getDerived().AlwaysRebuild() && !ContractChanged && Init.get() == S->getInit() && Cond.get() == std::make_pair(S->getConditionVariable(), S->getCond()) && Inc.get() == S->getInc() && Body.get() == S->getBody()) return S; - return getDerived().RebuildForStmt(S->getForLoc(), S->getLParenLoc(), - Init.get(), Cond, FullInc, - S->getRParenLoc(), Body.get()); + StmtResult Result = getDerived().RebuildForStmt( + S->getForLoc(), S->getLParenLoc(), Init.get(), Cond, FullInc, + S->getRParenLoc(), Body.get()); + if (Contract && Result.isUsable()) + SemaRef.Context.getOrCreateLoopContract(Result.get()) = std::move(*Contract); + return Result; } template @@ -18326,12 +18376,13 @@ ExprResult TreeTransform::TransformHLSLOutArgExpr(HLSLOutArgExpr *E) { //===----------------------------------------------------------------------===// // Contract nodes are ghost/spec constructs that are stripped before codegen. -// Template instantiation just rebuilds them unchanged by transforming children. +// They are rebuilt from their transformed children with the checks the parser +// applies, so a dependent condition is converted where it is instantiated. template StmtResult TreeTransform::TransformContractAssertStmt(ContractAssertStmt *S) { - ExprResult Cond = getDerived().TransformExpr(S->getCond()); + ExprResult Cond = getDerived().TransformContractCondition(S->getCond()); if (Cond.isInvalid()) return StmtError(); StmtResult By = S->getBy(); @@ -18410,6 +18461,145 @@ VarDecl *TreeTransform::TransformContractBinder(VarDecl *Binder) { return New; } +template +ExprResult TreeTransform::TransformContractCondition(Expr *E) { + ExprResult Result = getDerived().TransformExpr(E); + if (Result.isInvalid()) + return ExprError(); + return SemaRef.MaybeCreateExprWithCleanups( + SemaRef.ActOnContractCondition(Result)); +} + +template +ExprResult TreeTransform::TransformContractMeasure(Expr *E) { + ExprResult Result = getDerived().TransformExpr(E); + if (Result.isInvalid()) + return ExprError(); + return SemaRef.MaybeCreateExprWithCleanups( + SemaRef.ActOnContractMeasure(Result)); +} + +template +ExprResult TreeTransform::TransformContractTerm(Expr *E) { + ExprResult Result = getDerived().TransformExpr(E); + if (Result.isInvalid()) + return ExprError(); + return SemaRef.MaybeCreateExprWithCleanups(Result); +} + +template +ExprResult TreeTransform::TransformContractFootprint(Expr *E) { + // A range p[lo : n] is a footprint as a whole, never an operand. + Expr *Footprint = E; + if (auto *Full = dyn_cast(Footprint)) + Footprint = Full->getSubExpr(); + auto *Range = dyn_cast(Footprint->IgnoreParens()); + if (!Range) + return getDerived().TransformContractTerm(E); + ExprResult Base = getDerived().TransformExpr(Range->getBase()); + if (Base.isInvalid()) + return ExprError(); + ExprResult Lower; + if (Range->getLowerBound()) { + Lower = getDerived().TransformExpr(Range->getLowerBound()); + if (Lower.isInvalid()) + return ExprError(); + } + ExprResult Length; + if (Range->getLength()) { + Length = getDerived().TransformExpr(Range->getLength()); + if (Length.isInvalid()) + return ExprError(); + } + return SemaRef.MaybeCreateExprWithCleanups(SemaRef.ActOnContractRange( + Base.get(), Lower.get(), Range->getColonLocFirst(), Length.get(), + Range->getRBracketLoc())); +} + +template +bool TreeTransform::TransformFunctionContract( + const FunctionContractInfo &From, FunctionContractInfo &To) { + bool Invalid = false; + auto Keep = [&](ExprResult Result, SmallVectorImpl &Out) { + if (Result.isUsable()) + Out.push_back(Result.get()); + else + Invalid = true; + }; + auto KeepPairs = [&](ArrayRef> Pairs, + SmallVectorImpl> &Out) { + for (const auto &[First, Second] : Pairs) { + ExprResult A = getDerived().TransformContractTerm(First); + ExprResult B = getDerived().TransformContractTerm(Second); + if (A.isUsable() && B.isUsable()) + Out.push_back({A.get(), B.get()}); + else + Invalid = true; + } + }; + for (Expr *E : From.Preconditions) + Keep(getDerived().TransformContractCondition(E), To.Preconditions); + for (Expr *E : From.Postconditions) + Keep(getDerived().TransformContractCondition(E), To.Postconditions); + for (Expr *E : From.Modifies) + Keep(getDerived().TransformContractFootprint(E), To.Modifies); + KeepPairs(From.Aliases, To.Aliases); + for (Expr *E : From.Recommends) + Keep(getDerived().TransformContractCondition(E), To.Recommends); + KeepPairs(From.Reads, To.Reads); + for (Expr *E : From.When) + Keep(getDerived().TransformContractCondition(E), To.When); + for (Expr *E : From.Decreases) + Keep(getDerived().TransformContractMeasure(E), To.Decreases); + To.MayDiverge = From.MayDiverge; + To.Inductive = From.Inductive; + for (Expr *E : From.BehaviorChecks) + Keep(getDerived().TransformContractCondition(E), To.BehaviorChecks); + for (const auto &[Name, Assumes] : From.Behaviors) { + ExprResult Result = getDerived().TransformContractCondition(Assumes); + if (Result.isUsable()) + To.Behaviors.push_back({Name, Result.get()}); + else + Invalid = true; + } + for (const FunctionContractInfo::ClauseProof &Proof : From.ClauseProofs) { + StmtResult Body = getDerived().TransformStmt(Proof.Body); + if (Body.isUsable()) + To.ClauseProofs.push_back({Proof.K, Body.get(), Proof.Loc}); + else + Invalid = true; + } + To.IsSpec = From.IsSpec; + To.IsProof = From.IsProof; + return Invalid; +} + +template +bool TreeTransform::TransformLoopContract( + Stmt *S, std::optional &To, bool &Changed) { + const LoopContractInfo *From = SemaRef.Context.getLoopContract(S); + if (!From) + return false; + To.emplace(); + bool Invalid = false; + auto Keep = [&](Expr *Old, ExprResult New, SmallVectorImpl &Out) { + if (!New.isUsable()) { + Invalid = true; + return; + } + Changed |= New.get() != Old; + Out.push_back(New.get()); + }; + for (Expr *E : From->Invariants) + Keep(E, getDerived().TransformContractCondition(E), To->Invariants); + for (Expr *E : From->Decreases) + Keep(E, getDerived().TransformContractMeasure(E), To->Decreases); + for (Expr *E : From->Modifies) + Keep(E, getDerived().TransformContractFootprint(E), To->Modifies); + To->MayDiverge = From->MayDiverge; + return Invalid; +} + template ExprResult TreeTransform::TransformForallExpr(ForallExpr *E) { VarDecl *Var = getDerived().TransformContractBinder(E->getBoundVar()); @@ -18425,10 +18615,10 @@ ExprResult TreeTransform::TransformForallExpr(ForallExpr *E) { Lo.get() == E->getLo() && Hi.get() == E->getHi() && Body.get() == E->getBody()) return E; - return new (SemaRef.Context) - ForallExpr(E->getForallLoc(), E->getLParenLoc(), E->getRParenLoc(), - Var, Lo.getAs(), Hi.getAs(), - Body.getAs(), SemaRef.Context.BoolTy); + return SemaRef.BuildContractBinderExpr( + Stmt::ForallExprClass, E->getForallLoc(), E->getLParenLoc(), + E->getRParenLoc(), Var, Lo.getAs(), Hi.getAs(), + Body.getAs()); } template @@ -18446,10 +18636,10 @@ ExprResult TreeTransform::TransformContractChooseExpr(ContractChooseExp Lo.get() == E->getLo() && Hi.get() == E->getHi() && Body.get() == E->getBody()) return E; - return new (SemaRef.Context) - ContractChooseExpr(E->getChooseLoc(), E->getLParenLoc(), E->getRParenLoc(), - Var, Lo.getAs(), Hi.getAs(), - Body.getAs(), E->getType()); + return SemaRef.BuildContractBinderExpr( + Stmt::ContractChooseExprClass, E->getChooseLoc(), E->getLParenLoc(), + E->getRParenLoc(), Var, Lo.getAs(), Hi.getAs(), + Body.getAs()); } template @@ -18467,10 +18657,10 @@ ExprResult TreeTransform::TransformExistsExpr(ExistsExpr *E) { Lo.get() == E->getLo() && Hi.get() == E->getHi() && Body.get() == E->getBody()) return E; - return new (SemaRef.Context) - ExistsExpr(E->getExistsLoc(), E->getLParenLoc(), E->getRParenLoc(), - Var, Lo.getAs(), Hi.getAs(), - Body.getAs(), SemaRef.Context.BoolTy); + return SemaRef.BuildContractBinderExpr( + Stmt::ExistsExprClass, E->getExistsLoc(), E->getLParenLoc(), + E->getRParenLoc(), Var, Lo.getAs(), Hi.getAs(), + Body.getAs()); } template @@ -18486,8 +18676,14 @@ ExprResult TreeTransform::TransformOldExpr(OldExpr *E) { template ExprResult TreeTransform::TransformResultExpr(ResultExpr *E) { - // ResultExpr has no children to transform. - return E; + // The function's return type, which may depend on template parameters. + QualType Type = getDerived().TransformType(E->getType()); + if (Type.isNull()) + return ExprError(); + if (!getDerived().AlwaysRebuild() && Type == E->getType()) + return E; + return new (SemaRef.Context) + ResultExpr(E->getResultLoc(), E->getEndLoc(), Type); } } // end namespace clang From eb77fe2fd31caa97e3064615aaa87e23fb086082 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:57 +0530 Subject: [PATCH 06/64] verify: Substitute template arguments into a function contract. --- clang/lib/Sema/SemaTemplateInstantiate.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/clang/lib/Sema/SemaTemplateInstantiate.cpp b/clang/lib/Sema/SemaTemplateInstantiate.cpp index bad0cdd1b7..8f757853c1 100644 --- a/clang/lib/Sema/SemaTemplateInstantiate.cpp +++ b/clang/lib/Sema/SemaTemplateInstantiate.cpp @@ -4493,6 +4493,14 @@ Sema::SubstExpr(Expr *E, const MultiLevelTemplateArgumentList &TemplateArgs) { return Instantiator.TransformExpr(E); } +bool Sema::SubstFunctionContract( + const FunctionContractInfo &From, FunctionContractInfo &To, + const MultiLevelTemplateArgumentList &TemplateArgs) { + TemplateInstantiator Instantiator(*this, TemplateArgs, SourceLocation(), + DeclarationName()); + return Instantiator.TransformFunctionContract(From, To); +} + ExprResult Sema::SubstCXXIdExpr(Expr *E, const MultiLevelTemplateArgumentList &TemplateArgs) { From 36c3cf8a829b293825409e651280a0e04cc3d916 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:58 +0530 Subject: [PATCH 07/64] verify: Instantiate a specialization's contract with its definition, and keep ghost variables ghost. --- .../lib/Sema/SemaTemplateInstantiateDecl.cpp | 57 +++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp b/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp index c2e90624b8..9912c19027 100644 --- a/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp +++ b/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp @@ -5436,6 +5436,56 @@ void Sema::InstantiateExceptionSpec(SourceLocation PointOfInstantiation, TemplateArgs); } +void Sema::InstantiateFunctionContract(SourceLocation PointOfInstantiation, + FunctionDecl *Function) { + if (!getLangOpts().VerifyContracts || Function->isInvalidDecl() || + !Function->isTemplateInstantiation()) + return; + const FunctionDecl *Pattern = + Function->getTemplateInstantiationPattern(/*ForDefinition=*/false); + const FunctionContractInfo *PatternContract = + Pattern ? Context.getFunctionContract(Pattern) : nullptr; + if (!PatternContract || Context.getFunctionContract(Function)) + return; + // The clauses name the parameters of the declaration they are written on. + const FunctionDecl *Written = + PatternContract->ContractDecl ? PatternContract->ContractDecl : Pattern; + + // Recorded first, so that a use of the specialization in its own contract + // finds it and stops. + FunctionContractInfo &Contract = Context.getOrCreateFunctionContract(Function); + Contract.ContractDecl = Function; + Contract.IsSpec = PatternContract->IsSpec; + Contract.IsProof = PatternContract->IsProof; + + NonSFINAEContext _(*this); + InstantiatingTemplate Inst(*this, PointOfInstantiation, Function); + if (Inst.isInvalid()) + return; + Sema::ContextRAII SavedContext(*this, Function); + // The contract is a full expression of its own, whatever the use that + // asks for it, and the specs it applies are used. + EnterExpressionEvaluationContext Evaluated( + *this, ExpressionEvaluationContext::PotentiallyEvaluated); + LocalInstantiationScope Scope(*this); + MultiLevelTemplateArgumentList TemplateArgs = getTemplateInstantiationArgs( + Function, Function->getLexicalDeclContext(), /*Final=*/false, + /*Innermost=*/std::nullopt, /*RelativeToPrimary=*/true); + if (addInstantiatedParametersToScope(Function, Written, Scope, TemplateArgs)) + return; + std::optional ThisScope; + if (auto *Method = dyn_cast(Function); + Method && Method->isImplicitObjectMemberFunction()) + ThisScope.emplace(*this, Method->getParent(), + Method->getMethodQualifiers(), + static_cast(getLangOpts().CPlusPlus11)); + FunctionContractInfo Instantiated; + if (SubstFunctionContract(*PatternContract, Instantiated, TemplateArgs)) + return; + Instantiated.ContractDecl = Function; + Contract = std::move(Instantiated); +} + /// Initializes the common fields of an instantiation function /// declaration (New) from the corresponding fields of its template (Tmpl). /// @@ -5766,6 +5816,9 @@ void Sema::InstantiateFunctionDefinition(SourceLocation PointOfInstantiation, } } + // The definition is verified against its own contract. + InstantiateFunctionContract(PointOfInstantiation, Function); + NonSFINAEContext _(*this); InstantiatingTemplate Inst(*this, PointOfInstantiation, Function); if (Inst.isInvalid()) @@ -6175,6 +6228,10 @@ void Sema::BuildVariableInstantiation( InstantiateAttrs(TemplateArgs, OldVar, NewVar, LateAttrs, StartingScope); + // A ghost variable is one in every instantiation. + if (Context.isGhostVariable(OldVar)) + Context.markGhostVariable(NewVar); + LookupResult Previous( *this, NewVar->getDeclName(), NewVar->getLocation(), NewVar->isLocalExternDecl() ? Sema::LookupRedeclarationWithLinkage From 69eb19c14ca84ad9d5b4cedd0b807fc111bbce3d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:58 +0530 Subject: [PATCH 08/64] verify: Instantiate a specialization's contract where it is used. --- clang/lib/Sema/SemaExpr.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/clang/lib/Sema/SemaExpr.cpp b/clang/lib/Sema/SemaExpr.cpp index bd638b7c2a..e6e85e5611 100644 --- a/clang/lib/Sema/SemaExpr.cpp +++ b/clang/lib/Sema/SemaExpr.cpp @@ -19173,6 +19173,12 @@ void Sema::MarkFunctionReferenced(SourceLocation Loc, FunctionDecl *Func, if (FPT && isUnresolvedExceptionSpec(FPT->getExceptionSpecType())) ResolveExceptionSpec(Loc, FPT); + // A contract of a template specialization is needed where the + // specialization is used, as its callers rely on it, whether or not its + // definition is instantiated here. + if (OdrUse != OdrUseContext::None) + InstantiateFunctionContract(Loc, Func); + // A callee could be called by a host function then by a device function. // If we only try recording once, we will miss recording the use on device // side. Therefore keep trying until it is recorded. From 96dbdeb02dc1a7686a6fb5a5c2a3dd4281626946 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:59 +0530 Subject: [PATCH 09/64] verify: Record where each template specialization is instantiated. --- clang/lib/Verify/Frontend/ASTConverter.h | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index 677e548557..3878d3a1d2 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -71,6 +71,8 @@ class ASTConverter { /// Binders of a forall being introduced by contract_assert(...) by. std::set ArbitraryValues; std::map> UnverifiedCallers; + std::map> + InstantiationPoints; std::map ParameterNames; unsigned BoundValueId = 0; std::map FunctionIdentities; @@ -130,6 +132,14 @@ class ASTConverter { getWarnings() const { return Warnings; } + /// For each template specialization converted, by its name: where it is + /// instantiated and what it is ("function template specialization"), + /// which its diagnostics note as a compiler's do. A name two + /// specializations share has no location. + const std::map> & + getInstantiationPoints() const { + return InstantiationPoints; + } private: /// Contract arithmetic is mathematical, as in ACSL and Verus spec code: an From c0aee2491cc015e13fb23070ec975d6a0f605414 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:59 +0530 Subject: [PATCH 10/64] verify: Verify each instantiated specialization of a function template, named with its arguments. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 126 ++++++++++++++------- 1 file changed, 86 insertions(+), 40 deletions(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index b55daccea6..81ac6c1a41 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -915,6 +915,17 @@ VIntMode ASTConverter::specCallIntMode(const FunctionDecl *FD) const { return VIntMode::Math; } +/// A function as the verifier's messages name it, a template specialization +/// with its arguments (`maxv`). +static std::string functionName(const FunctionDecl *FD, + bool Qualified = false) { + std::string Name; + llvm::raw_string_ostream OS(Name); + FD->getNameForDiagnostic(OS, FD->getASTContext().getPrintingPolicy(), + Qualified); + return Name; +} + std::string ASTConverter::functionIdentity(const FunctionDecl *FD) { if (!FD) return {}; @@ -1994,6 +2005,17 @@ static void collectFunctionCandidates(const DeclContext *DC, ASTContext &Ctx, const FunctionDecl *FD = FTD->getTemplatedDecl(); if (FD->isThisDeclarationADefinition()) Out.push_back(FD); + // Each specialization this translation unit instantiates is a function + // of its own, with its definition or else its contract. An explicit + // specialization is a declaration of its own, and the redeclarations + // of a template share its specializations. + if (!FTD->isCanonicalDecl()) + continue; + for (const FunctionDecl *Spec : FTD->specializations()) + if (Spec->isTemplateInstantiation() && + (Spec->isThisDeclarationADefinition() || + (Ctx.getFunctionContract(Spec) && !Spec->hasBody()))) + Out.push_back(Spec); continue; } if (const auto *FD = dyn_cast(D)) { @@ -2154,23 +2176,47 @@ std::vector> ASTConverter::convertTranslationUnit() { // verified code calls it, which reports the call. if (!functionContract(FD) && !hasContractStatements(FD, Ctx)) continue; - llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); - llvm::SaveAndRestore OwnerName(ErrorFunctionName, FD->getNameAsString()); - llvm::SaveAndRestore InContract(ErrorInContract, true); - if (UnsupportedMember) { - error(FD->getLocation(), - FD->getQualifiedNameAsString() + ": " + *UnsupportedMember); + // A function template is verified in each of its specializations, + // which follow it: what it means depends on its arguments. + if (!UnsupportedMember) { + const FunctionTemplateDecl *Template = + FD->getDescribedFunctionTemplate(); + if (Template && !FD->isInStdNamespace() && + Ctx.getSourceManager().isWrittenInMainFile(FD->getLocation()) && + llvm::none_of(Template->specializations(), + [](const FunctionDecl *Spec) { + return Spec->isTemplateInstantiation(); + })) + Warnings.emplace_back( + FD->getLocation(), + functionName(FD) + ": function template is not verified: this " + "translation unit instantiates none of its " + "specializations"); continue; } - if (!FD->isInStdNamespace() && - Ctx.getSourceManager().isWrittenInMainFile(FD->getLocation())) - error(FD->getLocation(), - FD->getNameAsString() + - ": function template verification is unsupported"); + llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); + llvm::SaveAndRestore OwnerName(ErrorFunctionName, functionName(FD)); + llvm::SaveAndRestore InContract(ErrorInContract, true); + error(FD->getLocation(), + FD->getQualifiedNameAsString() + ": " + *UnsupportedMember); continue; } if (FD->isInStdNamespace()) continue; + if (FD->isTemplateInstantiation()) { + // Its diagnostics note where it is instantiated, as a compiler's do, + // under the names they give its function. + const SourceLocation Point = FD->getPointOfInstantiation(); + const char *What = FD->getPrimaryTemplate() + ? "function template specialization" + : "member function"; + for (const std::string &Name : + {functionName(FD), functionName(FD, isa(FD))}) + if (auto [It, New] = InstantiationPoints.emplace( + Name, std::make_pair(Point, std::string(What))); + !New && It->second.first != Point) + It->second.first = SourceLocation(); + } const size_t ErrorsBefore = Errors.size(); auto Fn = convertFunction(FD); if (Fn && Errors.size() == ErrorsBefore) { @@ -2203,7 +2249,7 @@ std::vector> ASTConverter::convertTranslationUnit() { if (const FunctionContractInfo *FCI = functionContract(Callee); FCI && !FCI->IsSpec && !FCI->IsProof) UnverifiedCallers[functionIdentity(Callee)].insert( - FD->getNameAsString()); + functionName(FD)); for (const Stmt *Child : S->children()) Calls(Child); }; @@ -2803,7 +2849,7 @@ bool ASTConverter::exceedsNestingLimit(const FunctionDecl *FD, if (Depth > Limit) { const PresumedLoc Where = Ctx.getSourceManager().getPresumedLoc(S->getBeginLoc()); - error(FD->getNameAsString() + ": the expression at " + + error(functionName(FD) + ": the expression at " + (Where.isValid() ? std::to_string(Where.getLine()) + ":" + std::to_string(Where.getColumn()) : std::string("an unknown location")) + @@ -2960,7 +3006,7 @@ std::unique_ptr ASTConverter::convertFunction(const FunctionDecl *FD) { llvm::SaveAndRestore At(CurrentRange, SourceRange(FD->getLocation())); llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); - llvm::SaveAndRestore OwnerName(ErrorFunctionName, FD->getNameAsString()); + llvm::SaveAndRestore OwnerName(ErrorFunctionName, functionName(FD)); llvm::SaveAndRestore InContract(ErrorInContract, true); const size_t ErrorsAtStart = Errors.size(); const FunctionContractInfo *FCI = functionContract(FD); @@ -2977,7 +3023,7 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { ParameterNames.clear(); const FunctionDecl *ContractDecl = FCI->ContractDecl ? FCI->ContractDecl : FD; if (ContractDecl->getNumParams() != FD->getNumParams()) { - error(FD->getNameAsString() + ": contract declaration parameter mismatch"); + error(functionName(FD) + ": contract declaration parameter mismatch"); return nullptr; } for (unsigned I = 0; I < FD->getNumParams(); ++I) { @@ -2992,16 +3038,16 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { ParameterNames[DefinitionParam] = Name; } if (FD->isVariadic()) { - error(FD->getNameAsString() + ": variadic functions are unsupported"); + error(functionName(FD) + ": variadic functions are unsupported"); return nullptr; } if (FCI->IsSpec && writesIndirectMemory(FD)) { - error(FD->getNameAsString() + ": spec functions must not write memory"); + error(functionName(FD) + ": spec functions must not write memory"); return nullptr; } if (FCI->IsSpec && (!FCI->Preconditions.empty() || !FCI->Modifies.empty() || !FCI->Aliases.empty())) { - error(FD->getNameAsString() + + error(functionName(FD) + ": a spec function is defined for every argument and " "its body is its meaning, so pre, modifies, and aliases " "do not apply; use recommends for a soft precondition"); @@ -3009,13 +3055,13 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { } if (FCI->IsSpec && FD->getReturnType()->isRecordType() && !VType::collectionKind(FD->getReturnType())) { - error(FD->getNameAsString() + + error(functionName(FD) + ": aggregate-returning spec functions are unsupported"); return nullptr; } if (auto Unsupported = findUnsupportedType(FD, !FCI->IsSpec && !FCI->IsProof)) { - error(FD->getNameAsString() + + error(functionName(FD) + ": unsupported C++ type in verification: " + *Unsupported); return nullptr; } @@ -3027,7 +3073,7 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { const bool HasThis = Method && Method->isInstance(); const auto *Constructor = dyn_cast(FD); Fn->IsConstructor = Constructor != nullptr; - Fn->Name = Method ? FD->getQualifiedNameAsString() : FD->getNameAsString(); + Fn->Name = functionName(FD, /*Qualified=*/Method != nullptr); Fn->Identity = functionIdentity(FD); Fn->IsSpec = FCI->IsSpec; Fn->IsProof = FCI->IsProof; @@ -3795,7 +3841,7 @@ bool ASTConverter::checkLoopTermination(const Stmt *Loop, bool HasMeasure) { std::unique_ptr ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); - llvm::SaveAndRestore OwnerName(ErrorFunctionName, FD->getNameAsString()); + llvm::SaveAndRestore OwnerName(ErrorFunctionName, functionName(FD)); llvm::SaveAndRestore InContract(ErrorInContract, true); const size_t ErrorsAtStart = Errors.size(); ParameterNames.clear(); @@ -3805,18 +3851,18 @@ ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { if (!FD->isConstexpr() || !FD->hasBody()) return nullptr; if (FD->getReturnType()->isRecordType()) { - error(FD->getNameAsString() + + error(functionName(FD) + ": aggregate-returning constexpr specs are unsupported"); return nullptr; } if (auto Unsupported = findUnsupportedType(FD, false)) { - error(FD->getNameAsString() + + error(functionName(FD) + ": unsupported C++ type in verification: " + *Unsupported); return nullptr; } auto Fn = std::make_unique(); - Fn->Name = FD->getNameAsString(); + Fn->Name = functionName(FD); Fn->Identity = functionIdentity(FD); Fn->IsSpec = true; Fn->IsConstexprSpec = true; @@ -5982,7 +6028,7 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { if (CalleeContract && CalleeContract->IsSpec && !InContractExpression && !InGhost && !CurrentFn->IsSpec && !CurrentFn->IsProof) { error(CurrentFn->Name + ": spec function " + - Callee->getNameAsString() + + functionName(Callee) + " cannot be used in executable code"); return nullptr; } @@ -6024,18 +6070,18 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { Ctx); noteSpecUse(Callee); return std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), Ty, E->getExprLoc(), specReadsHeap(Callee)); } if (functionContract(Callee)) error(CurrentFn->Name + ": executable call is unsupported in this expression " "context: " + - Callee->getNameAsString()); + functionName(Callee)); else error(CurrentFn->Name + ": call to function without a verification contract: " + - Callee->getNameAsString()); + functionName(Callee)); } } error(CurrentFn->Name + ": unsupported expression: " + E->getStmtClassName()); @@ -6112,7 +6158,7 @@ void ASTConverter::convertExecCallArg( convertExecCallArgs(CE, Prelude, InnerArgs); std::string Tmp = "__nested_" + std::to_string(++NestedCallId); Prelude.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(InnerArgs), Tmp, E->getExprLoc(), false)); Out = convertCallResultValue( Tmp, Callee->getReturnType(), @@ -6678,7 +6724,7 @@ bool ASTConverter::rejectOwnObjectUse(const Expr *E) { const FunctionDecl *Callee = ownObjectCallee(E); if (!Callee) return false; - error(CurrentFn->Name + ": the reference " + Callee->getNameAsString() + + error(CurrentFn->Name + ": the reference " + functionName(Callee) + " returns is not used yet; call it as a statement of its own"); return true; } @@ -7230,7 +7276,7 @@ ASTConverter::convertStmtBody(const Stmt *S) { : ""; CurrentFn->UsesDynamicStorage |= TrackOwnedResult; Out.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), ReturnsVoid ? "" : Tmp, RS->getBeginLoc(), false, Provenance)); auto Result = convertCallResultValue(Tmp, Callee->getReturnType(), @@ -7627,12 +7673,12 @@ ASTConverter::convertStmtBody(const Stmt *S) { convertExecCallArgs(CE, Out, Args); bool IsProof = calleeIsProof(Callee); Out.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), "", CE->getExprLoc(), IsProof)); } else { error(CurrentFn->Name + ": call to function without a verification contract: " + - Callee->getNameAsString()); + functionName(Callee)); } } else { error(CurrentFn->Name + ": indirect function calls are unsupported"); @@ -7852,7 +7898,7 @@ ASTConverter::convertStmtBody(const Stmt *S) { const std::string &Provenance = DynamicPointerProvenanceVariables.at(DirectTarget); Out.push_back(std::make_unique( - PointerCallee->getNameAsString(), functionIdentity(PointerCallee), + functionName(PointerCallee), functionIdentity(PointerCallee), std::move(Args), valueName(DirectTarget), BO->getExprLoc(), false, Provenance)); CurrentFn->UsesDynamicStorage = true; @@ -7887,7 +7933,7 @@ ASTConverter::convertStmtBody(const Stmt *S) { std::vector> Args; convertExecCallArgs(Call, Out, Args); Out.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), valueName(Target), BO->getExprLoc(), false)); markInitialized(Target); return Out; @@ -7913,7 +7959,7 @@ ASTConverter::convertStmtBody(const Stmt *S) { const std::string Tmp = "__assignment_call_" + std::to_string(++NestedCallId); Out.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), Tmp, BO->getExprLoc(), false)); VType Target = VType::fromQualType(BO->getLHS()->getType(), IntMode, Ctx); @@ -8067,7 +8113,7 @@ ASTConverter::convertStmtBody(const Stmt *S) { const std::string ResultTarget = "__local_call_" + std::to_string(++NestedCallId); Out.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), ResultTarget, VD->getBeginLoc(), calleeIsProof(Callee))); Initializer = convertCallResultValue( @@ -8222,7 +8268,7 @@ ASTConverter::convertStmtBody(const Stmt *S) { const std::string &Provenance = DynamicPointerProvenanceVariables.at(VD); Out.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), valueName(VD), VD->getBeginLoc(), false, Provenance)); CurrentFn->UsesDynamicStorage = true; @@ -8275,7 +8321,7 @@ ASTConverter::convertStmtBody(const Stmt *S) { RecordResult ? VD->getNameAsString() : "__local_call_" + std::to_string(++NestedCallId); Out.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), ResultTarget, VD->getBeginLoc(), calleeIsProof(Callee))); if (!RecordResult) { From 246d2b499dc990931e7e43e8ac2bb8cef3685b7f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:59 +0530 Subject: [PATCH 11/64] verify: Note where a specialization is instantiated after its errors and warnings. --- clang/lib/Verify/Driver/Verifier.cpp | 47 ++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 00ff4c3233..06d43a9b10 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -2790,6 +2790,23 @@ class Verifier { llvm::raw_ostream *DumpOS = nullptr; std::vector Diags; std::optional Lean; + /// Where each template specialization verified is instantiated, and what + /// it is, by its function's name. + std::map> + InstantiationPoints; + + /// The instantiation a diagnostic about a template specialization is + /// about, which a compiler notes after an error or a warning. + const std::pair * + instantiationOf(const VerifyDiagnostic &D) const { + if ((D.K != VerifyDiagnostic::Error && D.K != VerifyDiagnostic::Warning) || + (D.Loc.isInvalid() && D.Span.isInvalid())) + return nullptr; + auto It = InstantiationPoints.find(D.FunctionName); + if (It == InstantiationPoints.end() || It->second.first.isInvalid()) + return nullptr; + return &It->second; + } void reportLeanWarnings() { for (std::string &Warning : Lean->takeWarnings()) @@ -3081,6 +3098,7 @@ class Verifier { Converter.getUnverifiedCallers(); for (const auto &[Loc, Message] : Converter.getWarnings()) Diags.push_back({VerifyDiagnostic::Warning, Message, Loc}); + InstantiationPoints = Converter.getInstantiationPoints(); // A construct the verifier does not represent costs its function alone: // the function is Unresolved, its first error carrying the verdict, and // the rest of the translation unit is verified. An error outside every @@ -5564,6 +5582,17 @@ class Verifier { } if (Source.isValid()) Record["source"] = sourceJSON(Source); + if (const std::pair *Instantiation = + instantiationOf(D)) + if (PresumedLoc Point = + Ctx.getSourceManager().getPresumedLoc(Instantiation->first); + Point.isValid()) { + ObligationSource At; + At.File = Point.getFilename(); + At.Line = At.EndLine = Point.getLine(); + At.Column = At.EndColumn = Point.getColumn(); + Record["instantiated_at"] = sourceJSON(At); + } if (D.Vacuous) Record["vacuous"] = true; @@ -5736,6 +5765,12 @@ class Verifier { printJSONDiagnostic(D, OS); continue; } + const std::pair *Instantiation = + instantiationOf(D); + const std::string InstantiationNote = + Instantiation ? "in instantiation of " + Instantiation->second + + " '" + D.FunctionName + "' requested here" + : std::string(); if (D.K == VerifyDiagnostic::Error && D.Span.isValid()) { DiagnosticOptions DiagOpts; DiagOpts.ShowPresumedLoc = true; @@ -5744,6 +5779,10 @@ class Verifier { FullSourceLoc(D.Span.getBegin(), Ctx.getSourceManager()), DiagnosticsEngine::Error, D.Message, CharSourceRange::getTokenRange(D.Span), {}); + if (Instantiation) + Text.emitDiagnostic( + FullSourceLoc(Instantiation->first, Ctx.getSourceManager()), + DiagnosticsEngine::Note, InstantiationNote, {}, {}); continue; } if (D.Loc.isValid()) { @@ -5799,6 +5838,14 @@ class Verifier { OS << "warning: " << D.Message << "\n"; break; } + if (Instantiation) { + PresumedLoc PLoc = + Ctx.getSourceManager().getPresumedLoc(Instantiation->first); + if (PLoc.isValid()) + OS << PLoc.getFilename() << ":" << PLoc.getLine() << ":" + << PLoc.getColumn() << ": "; + OS << "note: " << InstantiationNote << "\n"; + } } } }; From cca2982d7d65b1764ea2c2f577cfdd491f73eb42 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:00 +0530 Subject: [PATCH 12/64] test: Check function templates verified in each specialization. --- .../test/Verify/suite/function_templates.cpp | 349 ++++++++++++++++++ 1 file changed, 349 insertions(+) create mode 100644 clang/test/Verify/suite/function_templates.cpp diff --git a/clang/test/Verify/suite/function_templates.cpp b/clang/test/Verify/suite/function_templates.cpp new file mode 100644 index 0000000000..9c8a27a228 --- /dev/null +++ b/clang/test/Verify/suite/function_templates.cpp @@ -0,0 +1,349 @@ +// RUN: not %cpp-verify --jobs=1 %s -- > %t 2>&1 +// RUN: FileCheck %s < %t +// RUN: FileCheck %s --check-prefix=NOTE < %t +// RUN: FileCheck %s --check-prefix=CONVERSION < %t +// RUN: FileCheck %s --check-prefix=SOUND < %t +// RUN: grep -c "Verified: half" %t | FileCheck %s --check-prefix=ONCE +// RUN: not %cpp-verify --lower-only --dump-ir=3 %s -- 2>&1 | FileCheck %s --check-prefix=VC +// RUN: not %cpp-verify --jobs=1 --diagnostics-format=json %s -- 2>/dev/null | FileCheck %s --check-prefix=JSON +// +// A function template is verified in each of its specializations, with its +// contract instantiated as its body is: what it means depends on its +// arguments. A diagnostic about a specialization notes where it is +// instantiated, as a compiler's does. +// +// No proof here holds only because no execution reaches its end. +// SOUND-NOT: vacuous + +template +T maxv(T a, T b) + cppverify::post(cppverify::result >= a && cppverify::result >= b) + cppverify::post(cppverify::result == a || cppverify::result == b) +{ + return a < b ? b : a; +} + +int bigger(int x, int y) + cppverify::post(cppverify::result >= x) +{ + int m = maxv(x, y); + return m; +} +// CHECK-DAG: Verified: maxv [backend=z3] +// CHECK-DAG: Verified: bigger [backend=z3] + +// An explicit instantiation is verified with no caller. +template long maxv(long, long); +// CHECK-DAG: Verified: maxv [backend=z3] + +// One instantiation may fail where another holds: 2 * 100 is no signed char. +template +T twice(T x) + cppverify::pre(0 <= x && x <= 100) + cppverify::post(cppverify::result == 2 * x) +{ + return x + x; +} + +int twice_int(int x) + cppverify::pre(0 <= x && x <= 100) +{ + int r = twice(x); + return r; +} + +signed char twice_char(signed char x) + cppverify::pre(0 <= x && x <= 100) +{ + signed char r = twice(x); + return r; +} +// CHECK-DAG: Verified: twice [backend=z3] +// CHECK-DAG: Verified: twice_int [backend=z3] +// CHECK-DAG: error: verification failed: twice [{{.*}}::postcondition@[[@LINE-20]]:{{.*}} x [ssa=x_0] [type=i8] = {{6[4-9]|[7-9][0-9]|100}} +// CHECK-DAG: Unresolved: twice_char [backend=z3] [reason=callee.contract] (relies on the contract of twice, which is not established) +// NOTE: error: verification failed: twice +// NOTE-NEXT: function_templates.cpp:[[@LINE-8]]:19: note: in instantiation of function template specialization 'twice' requested here +// JSON: "function":"twice","instantiated_at":{"column":19,"end_column":19,"end_line":[[@LINE-9]],"file":"{{.*}}function_templates.cpp","line":[[@LINE-9]]} + +// A recursive template calls its own specialization. +template +T sum_to(T n) + cppverify::pre(0 <= n && n <= 1000) + cppverify::post(cppverify::result == n * (n + 1) / 2) + cppverify::decreases(n) +{ + if (n == 0) + return 0; + T r = sum_to(n - 1); + return r + n; +} + +int sum_ten() + cppverify::post(cppverify::result == 55) +{ + int s = sum_to(10); + return s; +} +// CHECK-DAG: Verified: sum_to [backend=z3] +// CHECK-DAG: Verified: sum_ten [backend=z3] + +// A contract over the template's types. +template +int bits() + cppverify::post(cppverify::result == 8 * (int)sizeof(T)) +{ + return 8 * (int)sizeof(T); +} + +int widths() + cppverify::post(cppverify::result == 80) +{ + int a = bits(); + int b = bits(); + return a + b; +} +// CHECK-DAG: Verified: bits [backend=z3] +// CHECK-DAG: Verified: bits [backend=z3] +// CHECK-DAG: Verified: widths [backend=z3] + +// A loop contract, instantiated with the body: a short total wraps. +template +T total(const T *p, int n) + cppverify::pre(cppverify::valid(p, n) && 0 <= n && n <= 100) + cppverify::pre(cppverify::forall(k, 0, n, 0 <= p[k] && p[k] <= 1000)) + cppverify::post(0 <= cppverify::result && cppverify::result <= 1000 * n) +{ + T s = 0; + for (int i = 0; i < n; i = i + 1) + cppverify::invariant(0 <= i && i <= n) + cppverify::invariant(0 <= s && s <= 1000 * i) + cppverify::decreases(n - i) + { + s = s + p[i]; + } + return s; +} + +int total_int(const int *p, int n) + cppverify::pre(cppverify::valid(p, n) && 0 <= n && n <= 100) + cppverify::pre(cppverify::forall(k, 0, n, 0 <= p[k] && p[k] <= 1000)) + cppverify::post(cppverify::result <= 100000) +{ + int t = total(p, n); + return t; +} + +short total_short(const short *p, int n) + cppverify::pre(cppverify::valid(p, n) && 0 <= n && n <= 100) + cppverify::pre(cppverify::forall(k, 0, n, 0 <= p[k] && p[k] <= 1000)) +{ + short t = total(p, n); + return t; +} +// CHECK-DAG: Verified: total [backend=z3] +// CHECK-DAG: Verified: total_int [backend=z3] +// CHECK-DAG: error: verification failed: total [{{.*}}::invariant-preserved@ +// CHECK-DAG: Unresolved: total_short [backend=z3] [reason=callee.contract] +// NOTE: error: verification failed: total +// NOTE-NEXT: function_templates.cpp:[[@LINE-8]]:13: note: in instantiation of function template specialization 'total' requested here + +// Ghost code of a template's types: the ghost variable stays one. +template +T bump(T x) + cppverify::pre(0 <= x && x < 100) + cppverify::post(cppverify::result == x + 1) +{ + cppverify::ghost T before = 0; + cppverify::ghost { before = x; } + x = x + 1; + cppverify::check(x == before + 1); + return x; +} + +int bump_int(int x) + cppverify::pre(0 <= x && x < 100) + cppverify::post(cppverify::result == x + 1) +{ + int y = bump(x); + return y; +} +// CHECK-DAG: Verified: bump [backend=z3] +// CHECK-DAG: Verified: bump_int [backend=z3] + +// A spec template, applied in another template's contract. +template +cppverify::spec bool between(T lo, T x, T hi) { return lo <= x && x <= hi; } + +template +T clamp(T x, T lo, T hi) + cppverify::pre(lo <= hi) + cppverify::post(between(lo, cppverify::result, hi)) +{ + if (x < lo) + return lo; + if (hi < x) + return hi; + return x; +} + +int clamped(int x) + cppverify::post(0 <= cppverify::result && cppverify::result <= 10) +{ + int c = clamp(x, 0, 10); + return c; +} +// CHECK-DAG: Verified: spec axiom: between +// CHECK-DAG: Verified: clamp [backend=z3] +// CHECK-DAG: Verified: clamped [backend=z3] + +// A contract written on a declaration, the definition after it. +template +T half(T x) + cppverify::pre(x >= 0) + cppverify::post(2 * cppverify::result <= x); + +template +T half(T x) +{ + return x / 2; +} + +int halved(int x) + cppverify::pre(x >= 0) + cppverify::post(cppverify::result <= x) +{ + int h = half(x); + return h; +} +// CHECK-DAG: Verified: half [backend=z3] +// CHECK-DAG: Verified: halved [backend=z3] +// ONCE: 1 + +// A member function template. +struct Meter { + int level; + + template + void add(T d) + cppverify::pre(0 <= d && d <= 100 && 0 <= level && level <= 1000) + cppverify::modifies(level) + cppverify::post(level == cppverify::old(level) + d) + { + level = level + d; + } +}; + +int metered() + cppverify::post(cppverify::result == 8) +{ + Meter m; + m.level = 0; + m.add(5); + m.add((short)3); + return m.level; +} +// CHECK-DAG: Verified: Meter::add [backend=z3] +// CHECK-DAG: Verified: Meter::add [backend=z3] +// CHECK-DAG: Verified: metered [backend=z3] + +// A specialization the verifier cannot represent fails alone. +double fractional() { return maxv(1.5, 2.5); } +// CHECK-DAG: error: maxv: unsupported C++ type in verification: double +// CONVERSION: error: maxv: unsupported C++ type in verification: double +// CONVERSION: function_templates.cpp:[[@LINE-3]]:30: note: in instantiation of function template specialization 'maxv' requested here + +// Never instantiated: not verified. +template +T unused(T x) + cppverify::post(cppverify::result == x) +{ + return x; +} +// CHECK-DAG: function_templates.cpp:[[@LINE-5]]:3: warning: unused: function template is not verified: this translation unit instantiates none of its specializations + +// A trusted template declared without a definition: its contract is +// instantiated where it is used. +template +[[cppverify::trusted]] T next_of(T x) + cppverify::pre(x < 100) + cppverify::post(cppverify::result == x + 1); + +int uses_next() + cppverify::post(cppverify::result == 6) +{ + int r = next_of(5); + return r; +} +// CHECK-DAG: Trusted: next_of (contract assumed, not verified) +// CHECK-DAG: Verified: uses_next [backend=z3] [trusts=next_of] + +// cppverify::result of the template's type, compared with a constant. +template +T magnitude(T x) + cppverify::pre(x > -1000 && x < 1000) + cppverify::post(cppverify::result >= 0) +{ + return x < 0 ? -x : x; +} + +int uses_magnitude(int x) + cppverify::pre(x > -1000 && x < 1000) + cppverify::post(cppverify::result >= 0) +{ + int m = magnitude(x); + return m; +} +// CHECK-DAG: Verified: magnitude [backend=z3] +// CHECK-DAG: Verified: uses_magnitude [backend=z3] + +// A loop whose condition and body do not change with the template's +// arguments still gets its instantiated contract. +template +int size_of() + cppverify::post(cppverify::result == (int)sizeof(T)) +{ + while (false) + cppverify::invariant(sizeof(T) >= 1) + { + } + return (int)sizeof(T); +} + +int sizes() + cppverify::post(cppverify::result == 6) +{ + int s = size_of(); + int i = size_of(); + return s + i; +} +// CHECK-DAG: Verified: size_of [backend=z3] +// CHECK-DAG: Verified: size_of [backend=z3] +// CHECK-DAG: Verified: sizes [backend=z3] + +// A trigger stays one in each specialization. +template +T first_positive(const T *a, int n) + cppverify::pre(cppverify::valid(a, n) && 0 < n) + cppverify::pre(cppverify::forall(k, 0, n, cppverify::trigger(a[k]) > 0)) + cppverify::post(cppverify::result > 0) +{ + T v = a[0]; + return v; +} + +int first_int(const int *a, int n) + cppverify::pre(cppverify::valid(a, n) && 0 < n) + cppverify::pre(cppverify::forall(k, 0, n, a[k] > 0)) + cppverify::post(cppverify::result > 0) +{ + int v = first_positive(a, n); + return v; +} +// CHECK-DAG: Verified: first_positive [backend=z3] +// CHECK-DAG: Verified: first_int [backend=z3] +// VC-LABEL: vc first_positive +// VC: forall +// VC: trigger +// VC-NEXT: heap_select +// VC-LABEL: vc first_int From 694cb5672a5a058b25b94b5e42fb3df54850addb Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:00 +0530 Subject: [PATCH 13/64] test: Check that a function template's contract is checked where it is instantiated. --- .../test/Verify/template_contract_errors.cpp | 112 ++++++++++++++++++ 1 file changed, 112 insertions(+) create mode 100644 clang/test/Verify/template_contract_errors.cpp diff --git a/clang/test/Verify/template_contract_errors.cpp b/clang/test/Verify/template_contract_errors.cpp new file mode 100644 index 0000000000..f72dc05954 --- /dev/null +++ b/clang/test/Verify/template_contract_errors.cpp @@ -0,0 +1,112 @@ +// RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -verify %s +// +// A function template's contract is checked where it is instantiated, as its +// body is, so an error names the specialization. A template whose contract +// some arguments would break is no error until one of them is used. + +struct Pair { + int first; + int second; +}; + +template +int first_of(T v) + cppverify::post(cppverify::result == v.first) // expected-error {{member reference base type 'int' is not a structure or union}} +{ + return 0; +} + +int uses_first() { + Pair p{1, 2}; + return first_of(p) + first_of(3); // expected-note {{in instantiation of function template specialization 'first_of' requested here}} +} + +template +void needs(T v) + cppverify::pre(v) // expected-error {{value of type 'Pair' is not contextually convertible to 'bool'}} +{ +} + +void uses_needs() { + needs(1); + needs(Pair{1, 2}); // expected-note {{in instantiation of function template specialization 'needs' requested here}} +} + +template +int steps(T p) + cppverify::decreases(p) // expected-error {{decreases expression must have integer type}} +{ + return 0; +} + +int uses_steps() { + int x = 0; + return steps(1) + steps(&x); // expected-note {{in instantiation of function template specialization 'steps' requested here}} +} + +template +bool all_below(const int *p, T n) + cppverify::pre(cppverify::forall(k, 0, n, p[k] < 10)) // expected-error {{quantifier bound must have integer type}} +{ + return true; +} + +bool uses_all_below(const int *p) { + return all_below(p, 3) && all_below(p, 2.5); // expected-note {{in instantiation of function template specialization 'all_below' requested here}} +} + +template +void fills(T *p, T n) + cppverify::modifies(p[0 : n]) // expected-error {{a modifies range length must have integer type}} +{ +} + +void uses_fills(int *p, double *q) { + fills(p, 2); + fills(q, 2.0); // expected-note {{in instantiation of function template specialization 'fills' requested here}} +} + +// In the body, an assertion and a loop invariant are conditions too. +template +void asserts(T v) { + cppverify::check(v); // expected-error {{value of type 'Pair' is not contextually convertible to 'bool'}} +} + +template +void loops(T v) { + for (int i = 0; i < 3; i = i + 1) + cppverify::invariant(v) // expected-error {{value of type 'Pair' is not contextually convertible to 'bool'}} + cppverify::decreases(3 - i) + { + } +} + +void uses_body() { + asserts(1); + asserts(Pair{1, 2}); // expected-note {{in instantiation of function template specialization 'asserts' requested here}} + loops(1); + loops(Pair{1, 2}); // expected-note {{in instantiation of function template specialization 'loops' requested here}} +} + +// Used only with arguments its contract fits. +template +int only_records(T v) + cppverify::post(cppverify::result == v.first) +{ + return v.first; +} + +int uses_only_records() { + Pair p{1, 2}; + return only_records(p); +} + +// An unevaluated use asks for no contract. +template +int records_only(T v) + cppverify::post(cppverify::result == v.first) +{ + return v.first; +} + +using Unevaluated = decltype(records_only(3)); From 0a34abb550e354922fd715fb8ec210b149436f99 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:00 +0530 Subject: [PATCH 14/64] test: Expect function template contracts kept, and result and old of a template's type compared with a constant. --- clang/test/Verify/template_contracts.cpp | 27 +++++++++++++++++------- 1 file changed, 19 insertions(+), 8 deletions(-) diff --git a/clang/test/Verify/template_contracts.cpp b/clang/test/Verify/template_contracts.cpp index 4f0da96225..41bbc0464d 100644 --- a/clang/test/Verify/template_contracts.cpp +++ b/clang/test/Verify/template_contracts.cpp @@ -2,12 +2,13 @@ // RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -emit-llvm -o - %s | FileCheck %s // // A contract may depend on a template parameter: it is checked where it is -// instantiated, as C++ conditions are. Templates are not verified yet, so the -// contracts of a function or class template are ignored with a warning, and -// the template compiles and instantiates like any other. +// instantiated, as C++ conditions are. A function template's contract is +// instantiated with each specialization; the contracts of a class template +// are not verified yet and are ignored with a warning. Either compiles and +// instantiates like any other template. template -T clamp_low(T v, T lo) // expected-warning {{contracts in function template 'clamp_low' are not yet supported and are ignored}} +T clamp_low(T v, T lo) cppverify::pre(lo <= v || v < lo) cppverify::post(cppverify::result >= lo) { @@ -15,11 +16,11 @@ T clamp_low(T v, T lo) // expected-warning {{contracts in function template 'cla } template -T sum_to(T n) // expected-warning {{contracts in function template 'sum_to' are not yet supported and are ignored}} +T sum_to(T n) cppverify::pre(n >= 0) { T total = 0; - for (T i = 0; i < n; i = i + 1) // expected-warning {{contracts in function template 'sum_to' are not yet supported and are ignored}} + for (T i = 0; i < n; i = i + 1) cppverify::invariant(0 <= i && i <= n) cppverify::decreases(n - i) { @@ -29,7 +30,7 @@ T sum_to(T n) // expected-warning {{contracts in function template 'sum_to' are } template -void fill(T *p, T n, T v) // expected-warning {{contracts in function template 'fill' are not yet supported and are ignored}} +void fill(T *p, T n, T v) cppverify::modifies(p[0 : n]) { for (T i = 0; i < n; i = i + 1) @@ -48,6 +49,15 @@ struct Box { } }; +template +T positive(T v) + cppverify::pre(v > 0) + cppverify::post(cppverify::result > 0) + cppverify::post(cppverify::old(v) > 0 && cppverify::result == v) +{ + return v; +} + template T checked(T n) { @@ -78,7 +88,7 @@ int use() { fill(buffer, 2, 7); Box b{3}; return clamp_low(1, 2) + b.get() + sum_to(4) + sum_to(4L) + checked(5) + - quantified(6); + quantified(6) + positive(7); } // CHECK-DAG: define {{.*}} @_Z9clamp_lowIiET_S0_S0_( @@ -86,6 +96,7 @@ int use() { // CHECK-DAG: define {{.*}} @_Z6sum_toIlET_S0_( // CHECK-DAG: define {{.*}} @_Z4fillIiEvPT_S0_S0_( // CHECK-DAG: define {{.*}} @_ZNK3BoxIiE3getEv( +// CHECK-DAG: define {{.*}} @_Z8positiveIiET_S0_( // CHECK-DAG: define {{.*}} @_Z7checkedIiET_S0_( // CHECK-DAG: define {{.*}} @_Z10quantifiedIiET_S0_( // CHECK-DAG: define {{.*}} @_ZZ10quantifiedIiET_S0_ENKUlS0_E_clIiEEDaS0_( From 9f4a7325e2d985c5ce75fd9498569bdd877934c3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:01 +0530 Subject: [PATCH 15/64] test: Expect a warning for a contracted template that nothing instantiates. --- clang/test/Verify/suite/unused_template.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/clang/test/Verify/suite/unused_template.cpp b/clang/test/Verify/suite/unused_template.cpp index 820aa7100e..2567bc2396 100644 --- a/clang/test/Verify/suite/unused_template.cpp +++ b/clang/test/Verify/suite/unused_template.cpp @@ -1,10 +1,11 @@ // RUN: %cpp-verify %s -- 2>&1 | FileCheck %s --implicit-check-not=error: // RUN: not %cpp-verify %s -- -DCALL 2>&1 | FileCheck %s --check-prefix=CALL -// RUN: not %cpp-verify %s -- -DSTATEMENT 2>&1 | FileCheck %s --check-prefix=STATEMENT +// RUN: %cpp-verify %s -- -DSTATEMENT 2>&1 | FileCheck %s --check-prefix=STATEMENT // // A function template without contracts is not verified, and stops nothing // unless verified code calls it: that call is reported. One with contract -// statements is reported, as one with contracts is. +// statements, as one with contracts, is verified in its specializations, and +// one that nothing instantiates is reported, not verified. template T twice(T v) { return v + v; } @@ -24,7 +25,7 @@ int uses_twice(int x) return twice(x); } #endif -// CALL: error: uses_twice: call to function without a verification contract: twice +// CALL: error: uses_twice: call to function without a verification contract: twice // CALL-NOT: function template verification #ifdef STATEMENT @@ -34,4 +35,4 @@ template T checked(T v) return v; } #endif -// STATEMENT: error: checked: function template verification is unsupported +// STATEMENT: warning: checked: function template is not verified: this translation unit instantiates none of its specializations From fa8f9440aab1255cd7c56484ac73135d11011dca Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:01 +0530 Subject: [PATCH 16/64] test: Expect the warning for an uninstantiated contracted template. --- clang/test/Verify/suite/z3_calls_fail_closed.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/z3_calls_fail_closed.cpp b/clang/test/Verify/suite/z3_calls_fail_closed.cpp index 071427a235..2f5272b7dd 100644 --- a/clang/test/Verify/suite/z3_calls_fail_closed.cpp +++ b/clang/test/Verify/suite/z3_calls_fail_closed.cpp @@ -103,4 +103,4 @@ int unsupported_recursive_exec(int n) // VERIFY-DAG: error: unsupported_conditionless_for: conditionless for loops are unsupported // VERIFY-DAG: error: unsupported_cross_type_alias: aliases between different pointee types are unsupported // VERIFY-DAG: error: unsupported_recursive_exec: recursive executable functions require decreases -// VERIFY-DAG: warning: contracts in function template 'unsupported_template' are not yet supported and are ignored +// VERIFY-DAG: warning: unsupported_template: function template is not verified: this translation unit instantiates none of its specializations From 83bbad98fe1dfcfda1b454980b68f60f88ca0c50 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:01 +0530 Subject: [PATCH 17/64] docs: Describe function templates verified in each specialization. --- website/source/language/functions-loops.rst | 98 ++++++++++++++------- 1 file changed, 68 insertions(+), 30 deletions(-) diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index 1c585c9cd4..e90472ce71 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -221,50 +221,88 @@ Spec functions stay total, as in Verus and ACSL: a spec's division by zero is Templates --------- -Templates compile with contracts, but they are not verified yet (member -functions of ordinary classes are; see :doc:`structs`): +A function template is verified in each of its specializations, as Kani and +CBMC verify the code a program instantiates: its contract is instantiated +with its body, so the contract and every check of the body are about the +template's arguments, and each specialization gets a verdict of its own, +named with its arguments. -- The contracts of a function template, of a class template's members, and a - class template's type invariants compile, instantiate with the template, - and are ignored, with a ``-Wcontract-unsupported`` warning that names the - template. -- A template without contracts changes nothing for the rest of the file, as - long as verified code does not call it. +.. cppverify-example: fails twice .. code-block:: cpp template - T clamp_low(T v, T lo) - cv::post(cv::result >= lo) + T twice(T x) + cv::pre(0 <= x && x <= 30000) + cv::post(cv::result == 2 * x) { - return v < lo ? lo : v; + return x + x; } - int clamp_int(int v) - cv::post(cv::result >= 0) + int twice_int(int x) + cv::pre(0 <= x && x <= 30000) + cv::post(cv::result == 2 * x) { - return v < 0 ? 0 : v; + int r = twice(x); + return r; } -.. code-block:: text - - templates.cpp:2:3: warning: contracts in function template 'clamp_low' are not yet supported and are ignored [-Wcontract-unsupported] - 2 | T clamp_low(T v, T lo) - | ^ - Verified: clamp_int [backend=z3] + short twice_short(short x) + cv::pre(0 <= x && x <= 30000) + { + short r = twice(x); + return r; + } -Two uses still stop the file with an error, and no function in it gets a -verdict: +.. code-block:: text -- a call to a template from verified code, such as ``return clamp_low(v, - 0);`` in a function with a contract: ``error: use: call to function - without a verification contract: clamp_low``; -- a template whose body has a contract statement (``cv::check``, a ghost - block): ``error: twice: function template verification is unsupported``. + Verified: twice [backend=z3] + templates.cpp:4:23: error: verification failed: twice [...::postcondition@4:23] (counterexample: ...) [backend=z3] [reason=counterexample] + templates.cpp:20:13: note: in instantiation of function template specialization 'twice' requested here + Verified: twice_int [backend=z3] + Unresolved: twice_short [backend=z3] [reason=callee.contract] (relies on the contract of twice, which is not established) + +``x + x`` is an ``int``, which a ``short`` result holds only up to 32767: +``twice`` fails, and the function that relies on it is unresolved. + +- A specialization is verified where the translation unit instantiates it, + by a call or by an explicit instantiation (``template long + twice(long);``). A function template with a contract that nothing + instantiates is reported, not verified: ``warning: f: function template is + not verified: this translation unit instantiates none of its + specializations``. What a template means depends on the types and + overloads its arguments bring, which C++ fixes only where it is + instantiated. +- A diagnostic about a specialization notes where it is instantiated, as a + compiler's does (JSON ``instantiated_at``). +- The contract is checked where it is instantiated, as a C++ condition is: a + clause that does not fit the arguments, such as ``cv::post(cv::result == + v.first)`` for an ``int``, is a compiler error there, with Clang's ``in + instantiation of function template specialization`` note. Arguments the + contract fits are no error. +- Loop contracts, assertions, ghost code, quantifiers, and triggers are + instantiated with the body, and so are spec function templates and member + function templates of ordinary classes. A contract written on a + declaration holds for the definition after it, and a + ``[[cppverify::trusted]]`` template without a definition holds at every + call of its specializations. +- A specialization the verifier cannot represent (``maxv``) costs + that specialization alone, as a construct in any function does. +- The contracts of a class template's members and its type invariants are + not verified yet: they compile, instantiate with the template, and are + ignored, with a ``-Wcontract-unsupported`` warning that names the class + template. +- A template without contracts changes nothing for the rest of the file, as + long as verified code does not call it. -Before 0.2, a template whose contract depends on its parameters did not -compile (``value of type '' is not contextually convertible to -'bool'``), and a template without any contract, even one nothing calls, +Before 0.2, a function template's contracts were ignored with a warning, and +a call to one from verified code was ``call to function without a +verification contract``. A template whose contract depended on its +parameters did not compile (``value of type '' is not +contextually convertible to 'bool'``), nor did ``cv::result`` or +``cv::old(x)`` of the template's type compared with a constant +(``cv::post(cv::result > 0)``: ``invalid operands to binary expression ('T' +and 'int')``). A template without any contract, even one nothing calls, stopped the file with ``function template verification is unsupported``. Behaviors From 2fd37fec32434be2b8ae86916c6235ebd98abc85 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:02 +0530 Subject: [PATCH 18/64] docs: List function templates as supported and class template members as not yet. --- website/source/language/limitations.rst | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 62b31833b3..117a218135 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -158,17 +158,19 @@ C++ feature boundaries through a pointer (``Ring copy = *r;``). * - Functions - Free functions, member functions of classes without bases or virtual - functions (:doc:`structs`), overloads, namespaces, contracts, direct calls, and + functions (:doc:`structs`), function templates in each specialization + the translation unit instantiates (:doc:`functions-loops`), + overloads, namespaces, contracts, direct calls, and direct and mutual recursion, also through stores to pointer and reference parameters and through automatic objects, with mutual recursion among functions of one kind (spec, proof, or executable). - Virtual functions, member functions of classes with bases, destructors, delegating constructors and the other constructors :doc:`structs` lists, conversion functions, - templates (one without contracts stops nothing unless verified code - calls it; the contracts of a function or class template compile, - instantiate, and are ignored with a warning, and one with contract - statements is reported), variadics, indirect calls, recursion through a + members and type invariants of class templates (they compile, + instantiate, and are ignored with a warning), function templates + that nothing instantiates (reported), variadics, indirect calls, + recursion through a function that allocates or frees storage, and general link-time summaries. * - Storage From af8645d8ccb1733aa9003b829419635435a44974 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:02 +0530 Subject: [PATCH 19/64] docs: Note function templates in the release notes. --- website/source/release-notes.rst | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index e4c6efbc04..7074ae35da 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -336,6 +336,17 @@ on entry. An object passed by reference or pointer satisfies it on entry and, when mutable, at exit, where before only a record passed by value did (:doc:`language/structs`). +**Function templates.** A function template's contracts were ignored with +a warning, so no specialization was verified, and a call to one from +verified code was an error. Each specialization a translation unit +instantiates is now verified as a function of its own, named with its +arguments (``twice``), with its contract instantiated as its body is, +loop contracts, assertions, and ghost code included; a diagnostic about it +notes where it is instantiated, and a contracted template that nothing +instantiates is reported. ``cv::post(cv::result > 0)`` and ``cv::old(x) > 0`` +of a template's type did not compile (``invalid operands to binary +expression ('T' and 'int')``) (:doc:`language/functions-loops`). + **Member operators.** For a member ``operator==``, ``a == b`` passed ``a`` for the operator's parameter and ``b`` as an argument beyond it, an error, and an operator returning ``*this`` by reference (``Money &operator+=``) was From e39b949f1f1a6425b68bfef883af247a8ee074f4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:03 +0530 Subject: [PATCH 20/64] docs: Design function templates verified per instantiation. --- docs/DESIGN.md | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index b4b092e8de..ff287e8418 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1817,6 +1817,31 @@ cppverify::proof void sum_concat(seq s, seq t) mirror of vstd states each operation for its ladder; Lean's evaluation of every operation agrees with the certifier's. +## Templates + +- A function template is verified in each specialization the translation + unit instantiates, by a use or by an explicit instantiation, as a function + of its own named with its arguments (`maxv`). What a template means + depends on the types and overloads its arguments bring, which C++ fixes + only at instantiation, so an uninstantiated template is not verified (the + position of Kani and CBMC; Creusot and Prusti verify generic Rust once, + since trait bounds fix its meaning there). A contracted template that + nothing instantiates is reported. +- Its contract is instantiated as its body is, and lazily, as an exception + specification is: where a specialization is used or its definition + instantiated, never for a specialization nothing uses. Each clause gets + the checks the parser gives it (a condition converts to `bool`, a measure + is an integer, a range has integer bounds), so a clause that does not fit + the arguments is a compiler error with Clang's instantiation note. +- Loop contracts, assertions, ghost code, quantifiers, and triggers are + instantiated with the body. A contract written on a declaration names its + parameters; a trusted template without a definition is trusted in each + specialization. +- A diagnostic about a specialization notes where it is instantiated, as a + compiler's does. +- Not yet: the members and type invariants of class templates, ignored with + `-Wcontract-unsupported`. + ## Clang Modification Details ### Construct recognition @@ -1927,6 +1952,8 @@ a one-line hook. results, and every operation). 12. A range `p[lo : n]` needs a pointer to a complete object type and integer bounds, and is valid only as a whole `cppverify::modifies` footprint. +13. In a template, a clause that depends on its parameters is checked where + it is instantiated, with the same rules. ### CodeGen Rules From 4551563b9df488355c7c319fd53ac2a793c6d21e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:03 +0530 Subject: [PATCH 21/64] docs: Describe contract instantiation and the converter's specializations. --- docs/ARCHITECTURE.md | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 3f53be5716..3fb1d2cc4d 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -308,6 +308,31 @@ const, postconditions. The record escape scan accepts a callee's own automatic allocation unless it is initialized with an address it must not keep. +**Function templates:** Sema keeps a function template's contract on its +pattern and instantiates it lazily, as an exception specification: +`Sema::InstantiateFunctionContract` runs where a specialization is odr-used +(`MarkFunctionReferenced`) and where its definition is instantiated, once +per specialization (its `FunctionContractInfo` is recorded first, so a use +in its own contract stops there), in a `LocalInstantiationScope` that maps +the parameters of the declaration the clauses are written on +(`ContractDecl`), with `this` for a member, in an evaluation context of its +own. `SubstFunctionContract` runs `TreeTransform::TransformFunctionContract`, +which rebuilds each clause with the checks the parser applies +(`TransformContractCondition`, `TransformContractMeasure`, +`TransformContractFootprint`; quantifiers and choices through +`Sema::BuildContractBinderExpr`). `TreeTransform` gives `cppverify::result` the +instantiated return type, transforms a loop's contract with the loop and +rebuilds a loop whose clauses changed even when its condition and body did +not, and keeps trigger marks; `BuildVariableInstantiation` keeps ghost +variables. `ResultExpr`, `OldExpr`, and the quantifiers take the dependence +of their type or operands. `collectFunctionCandidates` adds, after each +function template, the specializations the translation unit instantiates +(from its canonical declaration, whose redeclarations share them), with +their definition or, without one, their contract. The converter names them +with their arguments (`functionName`) and records where each is +instantiated (`getInstantiationPoints`), which the driver prints as a note +after each error or warning of the specialization (JSON `instantiated_at`). + **Records in memory by value:** `recordFieldsInMemory` reads a record value kept in memory, a promoted local or one in a pointee or record reference (`promotedRootLocal`, `inPointeeObject`), through implicit copies and From ac5f112a1f0f04e3c9f494a875c394ab6bc48823 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:03:37 +0530 Subject: [PATCH 22/64] test: Check a constexpr template lifted as a spec in each specialization. --- clang/test/Verify/suite/function_templates.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/clang/test/Verify/suite/function_templates.cpp b/clang/test/Verify/suite/function_templates.cpp index 9c8a27a228..c62ae5f2e2 100644 --- a/clang/test/Verify/suite/function_templates.cpp +++ b/clang/test/Verify/suite/function_templates.cpp @@ -347,3 +347,16 @@ int first_int(const int *a, int n) // VC: trigger // VC-NEXT: heap_select // VC-LABEL: vc first_int + +// An uncontracted constexpr template in a contract is a spec in each +// specialization, as a constexpr function is. +template +constexpr T bigger_of(T a, T b) { return a < b ? b : a; } + +int clamp3(int x) + cppverify::post(cppverify::result == bigger_of(x, 3)) +{ + return x < 3 ? 3 : x; +} +// CHECK-DAG: Verified: clamp3 [backend=z3] +// CHECK-DAG: Verified: constexpr spec axiom: bigger_of From 4c52295eb9192dcaea71a54ceb9979c5c40efb9b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:03:37 +0530 Subject: [PATCH 23/64] docs: Note that a constexpr template in a contract is a spec in each specialization. --- website/source/language/functions-loops.rst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index e90472ce71..14d57668cd 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -282,7 +282,9 @@ named with its arguments. contract fits are no error. - Loop contracts, assertions, ghost code, quantifiers, and triggers are instantiated with the body, and so are spec function templates and member - function templates of ordinary classes. A contract written on a + function templates of ordinary classes. An uncontracted ``constexpr`` + template that a contract applies is a spec in each specialization, as a + ``constexpr`` function is (see Functions above). A contract written on a declaration holds for the definition after it, and a ``[[cppverify::trusted]]`` template without a definition holds at every call of its specializations. From 22c332983088a7e644532d587fc6df5216788c0c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:24 +0530 Subject: [PATCH 24/64] verify: Give each instantiated quantifier and choice a scope of its own, so each element of a pack expansion binds its own variable. --- clang/lib/Sema/SemaTemplateInstantiate.cpp | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/clang/lib/Sema/SemaTemplateInstantiate.cpp b/clang/lib/Sema/SemaTemplateInstantiate.cpp index 8f757853c1..02c341c532 100644 --- a/clang/lib/Sema/SemaTemplateInstantiate.cpp +++ b/clang/lib/Sema/SemaTemplateInstantiate.cpp @@ -1793,6 +1793,21 @@ namespace { return AC; } + // A quantifier's or a choice's binder is its own local, as a lambda's + // are: each element of a pack expansion binds a variable of its own. + ExprResult TransformForallExpr(ForallExpr *E) { + LocalInstantiationScope Scope(SemaRef, /*CombineWithOuterScope=*/true); + return inherited::TransformForallExpr(E); + } + ExprResult TransformExistsExpr(ExistsExpr *E) { + LocalInstantiationScope Scope(SemaRef, /*CombineWithOuterScope=*/true); + return inherited::TransformExistsExpr(E); + } + ExprResult TransformContractChooseExpr(ContractChooseExpr *E) { + LocalInstantiationScope Scope(SemaRef, /*CombineWithOuterScope=*/true); + return inherited::TransformContractChooseExpr(E); + } + ExprResult TransformLambdaExpr(LambdaExpr *E) { // Do not rebuild lambdas to avoid creating a new type. // Lambdas have already been processed inside their eval contexts. From d890301c37ee0b28fdc78da8065250c6b4449826 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:24 +0530 Subject: [PATCH 25/64] verify: Keep a check-by block in the scope of its instantiated quantifier's variable. --- clang/lib/Sema/TreeTransform.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/clang/lib/Sema/TreeTransform.h b/clang/lib/Sema/TreeTransform.h index 4a3583ac12..5f5aa41e76 100644 --- a/clang/lib/Sema/TreeTransform.h +++ b/clang/lib/Sema/TreeTransform.h @@ -18387,6 +18387,12 @@ TreeTransform::TransformContractAssertStmt(ContractAssertStmt *S) { return StmtError(); StmtResult By = S->getBy(); if (S->getBy()) { + // check(forall(k, ...)) by { ... }: the block is in the scope of k. + if (const auto *Old = dyn_cast(S->getCond()->IgnoreImplicit())) + if (const auto *New = dyn_cast(Cond.get()->IgnoreImplicit()); + New && New->getBoundVar() != Old->getBoundVar()) + getDerived().transformedLocalDecl(Old->getBoundVar(), + {New->getBoundVar()}); By = getDerived().TransformStmt(S->getBy()); if (By.isInvalid()) return StmtError(); From d27059d079246aa87a44f3df2d3711f6a3168207 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:24 +0530 Subject: [PATCH 26/64] verify: Drop the this scope and ghost mark a specialization's context and the pattern's checks already give. --- clang/lib/Sema/SemaTemplateInstantiateDecl.cpp | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp b/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp index 9912c19027..2b3a4aad51 100644 --- a/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp +++ b/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp @@ -5471,14 +5471,9 @@ void Sema::InstantiateFunctionContract(SourceLocation PointOfInstantiation, MultiLevelTemplateArgumentList TemplateArgs = getTemplateInstantiationArgs( Function, Function->getLexicalDeclContext(), /*Final=*/false, /*Innermost=*/std::nullopt, /*RelativeToPrimary=*/true); + // A member's `this` is the specialization's, the current context. if (addInstantiatedParametersToScope(Function, Written, Scope, TemplateArgs)) return; - std::optional ThisScope; - if (auto *Method = dyn_cast(Function); - Method && Method->isImplicitObjectMemberFunction()) - ThisScope.emplace(*this, Method->getParent(), - Method->getMethodQualifiers(), - static_cast(getLangOpts().CPlusPlus11)); FunctionContractInfo Instantiated; if (SubstFunctionContract(*PatternContract, Instantiated, TemplateArgs)) return; @@ -6228,10 +6223,6 @@ void Sema::BuildVariableInstantiation( InstantiateAttrs(TemplateArgs, OldVar, NewVar, LateAttrs, StartingScope); - // A ghost variable is one in every instantiation. - if (Context.isGhostVariable(OldVar)) - Context.markGhostVariable(NewVar); - LookupResult Previous( *this, NewVar->getDeclName(), NewVar->getLocation(), NewVar->isLocalExternDecl() ? Sema::LookupRedeclarationWithLinkage From 24a3d15582f0b3f08c6256bfc1f4248686763a92 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:25 +0530 Subject: [PATCH 27/64] verify: Declare the naming of parameters, a pack's elements apart. --- clang/lib/Verify/Frontend/ASTConverter.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index 3878d3a1d2..cdb8defd6f 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -74,6 +74,11 @@ class ASTConverter { std::map> InstantiationPoints; std::map ParameterNames; + /// For a parameter a pack expands to, its index in the pack, `...[1]`. + std::map PackElements; + /// Names each parameter of \p FD after the declaration \p ContractDecl + /// whose contract names them. + void nameParameters(const FunctionDecl *ContractDecl, const FunctionDecl *FD); unsigned BoundValueId = 0; std::map FunctionIdentities; std::map SpecHeapReads; From fce5a9fcbbfd336d3ec7e5e037984f2bb1300753 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:25 +0530 Subject: [PATCH 28/64] verify: Name the parameters a pack expands to as C++26 indexes them. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 45 +++++++++++++++------- 1 file changed, 32 insertions(+), 13 deletions(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index 81ac6c1a41..d467cc2be1 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -1136,6 +1136,33 @@ ASTConverter::trackedValueNames(const ValueDecl *D) const { return Names; } +void ASTConverter::nameParameters(const FunctionDecl *ContractDecl, + const FunctionDecl *FD) { + ParameterNames.clear(); + PackElements.clear(); + // The parameters a pack expands to share its name, which no others can: + // each is named as C++26 indexes a pack, `ns...[1]`. + std::map Occurrences, Elements; + for (const ParmVarDecl *P : ContractDecl->parameters()) + ++Occurrences[P->getNameAsString()]; + for (unsigned I = 0; I < FD->getNumParams(); ++I) { + const ParmVarDecl *ContractParam = ContractDecl->getParamDecl(I); + const ParmVarDecl *DefinitionParam = FD->getParamDecl(I); + std::string Name = ContractParam->getNameAsString(); + std::string Element; + if (!Name.empty() && Occurrences[Name] > 1) + Element = "...[" + std::to_string(Elements[Name]++) + "]"; + if (Name.empty()) + Name = DefinitionParam->getNameAsString(); + if (Name.empty()) + Name = "__cppverify_param_" + std::to_string(I); + ParameterNames[ContractParam] = Name + Element; + ParameterNames[DefinitionParam] = Name + Element; + if (!Element.empty()) + PackElements[DefinitionParam] = Element; + } +} + std::string ASTConverter::valueName(const ValueDecl *D) const { if (const auto *P = dyn_cast_or_null(D)) if (auto It = ParameterNames.find(P); It != ParameterNames.end()) @@ -1148,6 +1175,9 @@ void ASTConverter::recordSourceVariable(const ValueDecl *D) { return; const std::string InternalBase = valueName(D); std::string DisplayBase = D->getNameAsString(); + if (const auto *P = dyn_cast(D)) + if (auto It = PackElements.find(P); It != PackElements.end()) + DisplayBase += It->second; if (DisplayBase.empty()) DisplayBase = InternalBase; auto Record = [&](std::string InternalName, std::string DisplayName, @@ -3020,23 +3050,12 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { } if (exceedsNestingLimit(FD, FCI)) return nullptr; - ParameterNames.clear(); const FunctionDecl *ContractDecl = FCI->ContractDecl ? FCI->ContractDecl : FD; if (ContractDecl->getNumParams() != FD->getNumParams()) { error(functionName(FD) + ": contract declaration parameter mismatch"); return nullptr; } - for (unsigned I = 0; I < FD->getNumParams(); ++I) { - const ParmVarDecl *ContractParam = ContractDecl->getParamDecl(I); - const ParmVarDecl *DefinitionParam = FD->getParamDecl(I); - std::string Name = ContractParam->getNameAsString(); - if (Name.empty()) - Name = DefinitionParam->getNameAsString(); - if (Name.empty()) - Name = "__cppverify_param_" + std::to_string(I); - ParameterNames[ContractParam] = Name; - ParameterNames[DefinitionParam] = Name; - } + nameParameters(ContractDecl, FD); if (FD->isVariadic()) { error(functionName(FD) + ": variadic functions are unsupported"); return nullptr; @@ -3844,7 +3863,7 @@ ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { llvm::SaveAndRestore OwnerName(ErrorFunctionName, functionName(FD)); llvm::SaveAndRestore InContract(ErrorInContract, true); const size_t ErrorsAtStart = Errors.size(); - ParameterNames.clear(); + nameParameters(FD, FD); if (exceedsNestingLimit(FD, functionContract(FD)) || hasIndirectMemoryAccess(FD)) return nullptr; From 4138ee0ced7367b9dd917cf2906f44092b12ddb3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:25 +0530 Subject: [PATCH 29/64] test: Check a contract on a definition after a declaration, and variadic templates. --- .../test/Verify/suite/function_templates.cpp | 60 ++++++++++++++++++- 1 file changed, 59 insertions(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/function_templates.cpp b/clang/test/Verify/suite/function_templates.cpp index c62ae5f2e2..48606a2948 100644 --- a/clang/test/Verify/suite/function_templates.cpp +++ b/clang/test/Verify/suite/function_templates.cpp @@ -148,7 +148,8 @@ short total_short(const short *p, int n) // NOTE: error: verification failed: total // NOTE-NEXT: function_templates.cpp:[[@LINE-8]]:13: note: in instantiation of function template specialization 'total' requested here -// Ghost code of a template's types: the ghost variable stays one. +// Ghost code of a template's types, a ghost variable assigned in a ghost +// block. template T bump(T x) cppverify::pre(0 <= x && x < 100) @@ -360,3 +361,60 @@ int clamp3(int x) } // CHECK-DAG: Verified: clamp3 [backend=z3] // CHECK-DAG: Verified: constexpr spec axiom: bigger_of + +// A contract written on the definition, after a declaration that names its +// parameter otherwise and before which the template is used. +template +T third(T x); + +int thirds(int x) + cppverify::pre(x >= 0) + cppverify::post(cppverify::result <= x) +{ + int t = third(x); + return t; +} + +template +T third(T y) + cppverify::pre(y >= 0) + cppverify::post(3 * cppverify::result <= y) +{ + return y / 3; +} +// CHECK-DAG: Verified: third [backend=z3] +// CHECK-DAG: Verified: thirds [backend=z3] + +// A variadic template: a fold over a quantifier binds a variable in each +// element, and the parameters the pack expands to are named apart. +template +int first_small(const int *p, Ns... ns) + cppverify::pre(cppverify::valid(p, 10)) + cppverify::pre(((0 < ns && ns <= 10) && ...)) + cppverify::pre((cppverify::forall(k, 0, ns, p[k] < 10) && ...)) + cppverify::post(cppverify::result < 10) +{ + return p[0]; +} + +int uses_first_small(const int *p) + cppverify::pre(cppverify::valid(p, 10)) + cppverify::pre(cppverify::forall(k, 0, 10, p[k] < 10)) + cppverify::post(cppverify::result < 10) +{ + int v = first_small(p, 3, 5); + return v; +} +// CHECK-DAG: Verified: first_small [backend=z3] +// CHECK-DAG: Verified: uses_first_small [backend=z3] + +template +int product_of(Ns... ns) + cppverify::pre(((0 <= ns && ns <= 10) && ...)) + cppverify::post(cppverify::result == (ns * ...)) +{ + return (ns + ...); +} + +int products() { return product_of(2, 3); } +// CHECK-DAG: error: verification failed: product_of [{{.*}}::postcondition@[[@LINE-6]]:{{.*}} ns...[0] [ssa=ns...[0]_0] [type=i32] = {{.*}} ns...[1] [ssa=ns...[1]_0] [type=i32] = From 3693656e87a56c715d7eb335cd8c524a957ed3bc Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:26 +0530 Subject: [PATCH 30/64] test: Check that instantiating a contract leaves a caller its temporaries' cleanups. --- clang/test/Verify/template_contracts.cpp | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/clang/test/Verify/template_contracts.cpp b/clang/test/Verify/template_contracts.cpp index 41bbc0464d..cddc220c6e 100644 --- a/clang/test/Verify/template_contracts.cpp +++ b/clang/test/Verify/template_contracts.cpp @@ -1,5 +1,6 @@ // RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -verify %s // RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -emit-llvm -o - %s | FileCheck %s +// RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -ast-dump -ast-dump-filter temporaries %s | FileCheck %s --check-prefix=CLEANUPS // // A contract may depend on a template parameter: it is checked where it is // instantiated, as C++ conditions are. A function template's contract is @@ -58,6 +59,26 @@ T positive(T v) return v; } +// A contract instantiated while a caller's full expression is built leaves +// the caller its temporaries, whose destructors run at its end. +struct Noisy { + int v; + Noisy(int x) : v(x) {} + ~Noisy(); +}; + +template +int value_of(const T &t) + cppverify::post(cppverify::result == t.v) +{ + return t.v; +} + +int temporaries() { return value_of(Noisy(3)); } +// CLEANUPS-LABEL: FunctionDecl {{.*}} temporaries 'int ()' +// CLEANUPS: ReturnStmt +// CLEANUPS-NEXT: ExprWithCleanups + template T checked(T n) { From 5ee709d156e790b9b4a6a89e9dac4bcabf358d20 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:26 +0530 Subject: [PATCH 31/64] docs: Describe binder scopes and pack element names in function templates. --- docs/ARCHITECTURE.md | 40 +++++++++++++++++++++++----------------- 1 file changed, 23 insertions(+), 17 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 3fb1d2cc4d..e60a3a79ed 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -315,23 +315,29 @@ pattern and instantiates it lazily, as an exception specification: per specialization (its `FunctionContractInfo` is recorded first, so a use in its own contract stops there), in a `LocalInstantiationScope` that maps the parameters of the declaration the clauses are written on -(`ContractDecl`), with `this` for a member, in an evaluation context of its -own. `SubstFunctionContract` runs `TreeTransform::TransformFunctionContract`, -which rebuilds each clause with the checks the parser applies -(`TransformContractCondition`, `TransformContractMeasure`, -`TransformContractFootprint`; quantifiers and choices through -`Sema::BuildContractBinderExpr`). `TreeTransform` gives `cppverify::result` the -instantiated return type, transforms a loop's contract with the loop and -rebuilds a loop whose clauses changed even when its condition and body did -not, and keeps trigger marks; `BuildVariableInstantiation` keeps ghost -variables. `ResultExpr`, `OldExpr`, and the quantifiers take the dependence -of their type or operands. `collectFunctionCandidates` adds, after each -function template, the specializations the translation unit instantiates -(from its canonical declaration, whose redeclarations share them), with -their definition or, without one, their contract. The converter names them -with their arguments (`functionName`) and records where each is -instantiated (`getInstantiationPoints`), which the driver prints as a note -after each error or warning of the specialization (JSON `instantiated_at`). +(`ContractDecl`), in the specialization's context (its `this`, for a member) +and an evaluation context of its own, so that a caller whose full expression +is being built keeps its temporaries' cleanups. `SubstFunctionContract` runs +`TreeTransform::TransformFunctionContract`, which rebuilds each clause with +the checks the parser applies (`TransformContractCondition`, +`TransformContractMeasure`, `TransformContractFootprint`; quantifiers and +choices through `Sema::BuildContractBinderExpr`). `TreeTransform` gives +`cppverify::result` the instantiated return type, transforms a loop's +contract with the loop and rebuilds a loop whose clauses changed even when +its condition and body did not, and keeps trigger marks; each quantifier and +choice binds in a `LocalInstantiationScope` of its own +(`TemplateInstantiator`), so each element of a pack expansion binds its own +variable, and the block of a `check(forall(k, ...)) by` is given the +instantiated `k`. `ResultExpr`, `OldExpr`, and the quantifiers take the +dependence of their type or operands. `collectFunctionCandidates` adds, +after each function template, the specializations the translation unit +instantiates (from its canonical declaration, whose redeclarations share +them), with their definition or, without one, their contract. The converter +names them with their arguments (`functionName`), and the parameters a pack +expands to as C++26 indexes it, `ns...[1]` (`nameParameters`), and records +where each is instantiated (`getInstantiationPoints`), which the driver +prints as a note after each error or warning of the specialization (JSON +`instantiated_at`). **Records in memory by value:** `recordFieldsInMemory` reads a record value kept in memory, a promoted local or one in a pointee or record reference From c91908eb54c0b8363b77a45931cce0cac58fda53 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:26 +0530 Subject: [PATCH 32/64] docs: Describe variadic templates. --- website/source/language/functions-loops.rst | 3 +++ 1 file changed, 3 insertions(+) diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index 14d57668cd..14fe1113f4 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -288,6 +288,9 @@ named with its arguments. declaration holds for the definition after it, and a ``[[cppverify::trusted]]`` template without a definition holds at every call of its specializations. +- In a variadic template, the parameters a pack expands to are named as + C++26 indexes a pack, ``ns...[1]``, in counterexamples too, and a fold + over a quantifier binds a variable of its own in each element. - A specialization the verifier cannot represent (``maxv``) costs that specialization alone, as a construct in any function does. - The contracts of a class template's members and its type invariants are From 1722556b034f6840ff861e8589f263f2de1557bb Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:31:40 +0530 Subject: [PATCH 33/64] verify: Map a contract's parameters through the pattern's, which stand for those of every redeclaration. --- clang/lib/Sema/SemaTemplateInstantiateDecl.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp b/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp index 2b3a4aad51..9e9668b2fb 100644 --- a/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp +++ b/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp @@ -5447,9 +5447,6 @@ void Sema::InstantiateFunctionContract(SourceLocation PointOfInstantiation, Pattern ? Context.getFunctionContract(Pattern) : nullptr; if (!PatternContract || Context.getFunctionContract(Function)) return; - // The clauses name the parameters of the declaration they are written on. - const FunctionDecl *Written = - PatternContract->ContractDecl ? PatternContract->ContractDecl : Pattern; // Recorded first, so that a use of the specialization in its own contract // finds it and stops. @@ -5471,8 +5468,10 @@ void Sema::InstantiateFunctionContract(SourceLocation PointOfInstantiation, MultiLevelTemplateArgumentList TemplateArgs = getTemplateInstantiationArgs( Function, Function->getLexicalDeclContext(), /*Final=*/false, /*Innermost=*/std::nullopt, /*RelativeToPrimary=*/true); - // A member's `this` is the specialization's, the current context. - if (addInstantiatedParametersToScope(Function, Written, Scope, TemplateArgs)) + // A member's `this` is the specialization's, the current context. The + // scope identifies the parameters of every redeclaration of the pattern, + // so the clauses may name those of the declaration they are written on. + if (addInstantiatedParametersToScope(Function, Pattern, Scope, TemplateArgs)) return; FunctionContractInfo Instantiated; if (SubstFunctionContract(*PatternContract, Instantiated, TemplateArgs)) From f653fb6c1241596ba410725e2d644acbf9f8b799 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:31:41 +0530 Subject: [PATCH 34/64] docs: Describe how a contract's parameters are mapped in a specialization. --- docs/ARCHITECTURE.md | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index e60a3a79ed..7bd4019866 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -314,10 +314,11 @@ pattern and instantiates it lazily, as an exception specification: (`MarkFunctionReferenced`) and where its definition is instantiated, once per specialization (its `FunctionContractInfo` is recorded first, so a use in its own contract stops there), in a `LocalInstantiationScope` that maps -the parameters of the declaration the clauses are written on -(`ContractDecl`), in the specialization's context (its `this`, for a member) -and an evaluation context of its own, so that a caller whose full expression -is being built keeps its temporaries' cleanups. `SubstFunctionContract` runs +the pattern's parameters, which identifies those of every redeclaration (so +the clauses may be written on any, `ContractDecl`), in the specialization's +context (its `this`, for a member) and an evaluation context of its own, so +that a caller whose full expression is being built keeps its temporaries' +cleanups. `SubstFunctionContract` runs `TreeTransform::TransformFunctionContract`, which rebuilds each clause with the checks the parser applies (`TransformContractCondition`, `TransformContractMeasure`, `TransformContractFootprint`; quantifiers and From 47516c5862e3e2c556eedc24edcb16f54e42e53a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:38:02 +0530 Subject: [PATCH 35/64] test: Pass the temporary by value, which is one before the call is resolved. --- clang/test/Verify/template_contracts.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/clang/test/Verify/template_contracts.cpp b/clang/test/Verify/template_contracts.cpp index cddc220c6e..d3d8b7509f 100644 --- a/clang/test/Verify/template_contracts.cpp +++ b/clang/test/Verify/template_contracts.cpp @@ -60,7 +60,8 @@ T positive(T v) } // A contract instantiated while a caller's full expression is built leaves -// the caller its temporaries, whose destructors run at its end. +// the caller its temporaries, whose destructors run at its end: an argument +// passed by value is one before the call is resolved. struct Noisy { int v; Noisy(int x) : v(x) {} @@ -68,7 +69,7 @@ struct Noisy { }; template -int value_of(const T &t) +int value_of(T t) cppverify::post(cppverify::result == t.v) { return t.v; From 348bd8968f3fb8e26dc6c51aab39f1d06cc22a44 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:11:32 +0530 Subject: [PATCH 36/64] verify: Keep a class template's members' contracts, loop contracts, and type invariants. --- clang/lib/Parse/ParseCppVerify.cpp | 26 +++++--------------------- 1 file changed, 5 insertions(+), 21 deletions(-) diff --git a/clang/lib/Parse/ParseCppVerify.cpp b/clang/lib/Parse/ParseCppVerify.cpp index 0ea63396c3..2ef2d335fd 100644 --- a/clang/lib/Parse/ParseCppVerify.cpp +++ b/clang/lib/Parse/ParseCppVerify.cpp @@ -672,16 +672,8 @@ void Parser::attachFunctionContract(Decl *Result, I.MayDiverge.isInvalid() && I.Inductive.isInvalid() && I.BehaviorChecks.empty() && !I.IsSpec && !I.IsProof)) return; - // A function template's clauses are instantiated with each of its - // specializations. Members of class templates are not verified yet: their - // clauses are ignored. - if (const auto *Method = dyn_cast(FD); - Method && Method->getParent()->isTemplated() && !I.IsSpec && - !I.IsProof) { - Diag(FD->getLocation(), diag::warn_contract_template_unsupported) - << 1 << Method->getParent(); - return; - } + // A template's clauses are instantiated with each of its specializations, + // a class template's members' with the members. FunctionContractInfo &FCI = Ctx.getOrCreateFunctionContract(FD); if (FCI.ContractDecl && FCI.ContractDecl != FD) { Diag(FD->getLocation(), diag::err_contract_redeclaration); @@ -859,13 +851,6 @@ void Parser::attachLoopContract(StmtResult &Loop, LoopContractInfo &Contract) { (Contract.Invariants.empty() && Contract.Decreases.empty() && Contract.MayDiverge.isInvalid() && Contract.Modifies.empty())) return; - if (const auto *Method = - dyn_cast_or_null(Actions.getCurFunctionDecl()); - Method && Method->getParent()->isTemplated()) { - Diag(Loop.get()->getBeginLoc(), diag::warn_contract_template_unsupported) - << 1 << Method->getParent(); - return; - } Actions.getASTContext().getOrCreateLoopContract(Loop.get()) = std::move(Contract); } @@ -876,7 +861,6 @@ void Parser::ParseTypeInvariant(Decl *TagDecl) { auto *RD = dyn_cast_or_null(TagDecl); if (auto *Template = dyn_cast_or_null(TagDecl)) RD = Template->getTemplatedDecl(); - const SourceLocation InvariantLoc = Tok.getLocation(); ConsumeCppVerify(); auto Finish = [&] { takePendingReferences(Actions.getASTContext(), RD, @@ -912,9 +896,9 @@ void Parser::ParseTypeInvariant(Decl *TagDecl) { return Finish(); } ConsumeParen(); - if (!E.isInvalid() && RD->isDependentContext()) { - Diag(InvariantLoc, diag::warn_contract_template_unsupported) << 1 << RD; - } else if (!E.isInvalid()) { + // A class template's invariants are instantiated with each of its + // specializations. + if (!E.isInvalid()) { E = Actions.ActOnTypeInvariantExpr(E, RD); if (!E.isInvalid()) Actions.getASTContext().getOrCreateTypeContract(RD).Invariants.push_back( From e64304807d9f2c1b87b741df82d16ab0bd5a6279 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:11:32 +0530 Subject: [PATCH 37/64] verify: Remove the warning that template contracts are ignored. --- clang/include/clang/Basic/DiagnosticParseKinds.td | 4 ---- 1 file changed, 4 deletions(-) diff --git a/clang/include/clang/Basic/DiagnosticParseKinds.td b/clang/include/clang/Basic/DiagnosticParseKinds.td index ba4e0f7dd4..0163ac4fca 100644 --- a/clang/include/clang/Basic/DiagnosticParseKinds.td +++ b/clang/include/clang/Basic/DiagnosticParseKinds.td @@ -1987,9 +1987,5 @@ def err_cppverify_unknown : Error< def err_cppverify_unknown_suggest : Error< "no cpp-verify construct named 'cppverify::%0'; did you mean " "'cppverify::%1'?">; -def warn_contract_template_unsupported : Warning< - "contracts in %select{function|class}0 template %1 are not yet supported " - "and are ignored">, - InGroup; } // end of Parser diagnostics From cbbf08e505c44095e296ba3a98bb15b44dd47ed4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:11:32 +0530 Subject: [PATCH 38/64] verify: Keep the contract-unsupported group for builds that name it. --- clang/include/clang/Basic/DiagnosticGroups.td | 2 ++ 1 file changed, 2 insertions(+) diff --git a/clang/include/clang/Basic/DiagnosticGroups.td b/clang/include/clang/Basic/DiagnosticGroups.td index edd3e01bb6..698f2cf108 100644 --- a/clang/include/clang/Basic/DiagnosticGroups.td +++ b/clang/include/clang/Basic/DiagnosticGroups.td @@ -1216,6 +1216,8 @@ def UnusedMemberFunction : DiagGroup<"unused-member-function", [UnneededMemberFunction]>; def UnusedLabel : DiagGroup<"unused-label">; def UnusedLambdaCapture : DiagGroup<"unused-lambda-capture">; +// Contracts of templates were ignored with a warning in this group before +// templates were verified; it stays, so a build that names it still builds. def ContractUnsupported : DiagGroup<"contract-unsupported">; def UnusedParameter : DiagGroup<"unused-parameter">; def UnusedButSetParameter : DiagGroup<"unused-but-set-parameter">; From 5aaa43ae18789f2fc2eb4c5d27f47a1002cf91da Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:11:33 +0530 Subject: [PATCH 39/64] verify: Write a field a type invariant names bare as this->field, which instantiation can rebuild. --- clang/lib/Sema/SemaContract.cpp | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/clang/lib/Sema/SemaContract.cpp b/clang/lib/Sema/SemaContract.cpp index 08df4d87cc..efdf9984c3 100644 --- a/clang/lib/Sema/SemaContract.cpp +++ b/clang/lib/Sema/SemaContract.cpp @@ -38,16 +38,19 @@ class TypeInvariantFieldRewriter : public TreeTransform(E->getDecl())) { if (FD->getParent() == Record) { + // this->field, as a member function reads it, so that a class + // template's instantiation rebuilds it with its own `this`. SourceLocation Loc = E->getBeginLoc(); - QualType ThisTy = - getSema().Context.getTypeDeclType(cast(Record)); + QualType ThisTy = getSema().getCurrentThisType(); + if (ThisTy.isNull()) + return Base::TransformDeclRefExpr(E); ExprResult This = getSema().BuildCXXThisExpr(Loc, ThisTy, /*IsImplicit=*/true); if (This.isInvalid()) return ExprError(); DeclarationNameInfo NameInfo(FD->getDeclName(), Loc); return getSema().BuildMemberExpr( - This.get(), /*IsArrow=*/false, Loc, NestedNameSpecifierLoc(), + This.get(), /*IsArrow=*/true, Loc, NestedNameSpecifierLoc(), SourceLocation(), FD, DeclAccessPair::make(FD, FD->getAccess()), /*HadMultipleCandidates=*/false, NameInfo, FD->getType(), VK_LValue, OK_Ordinary, /*TemplateArgs=*/nullptr); From 126dba13b85d5bbe0e389ecac458f7542c3dcb9a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:11:33 +0530 Subject: [PATCH 40/64] verify: Instantiate a class template's type invariants with each specialization. --- clang/lib/Sema/SemaTemplateInstantiate.cpp | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/clang/lib/Sema/SemaTemplateInstantiate.cpp b/clang/lib/Sema/SemaTemplateInstantiate.cpp index 02c341c532..0cbc2687c1 100644 --- a/clang/lib/Sema/SemaTemplateInstantiate.cpp +++ b/clang/lib/Sema/SemaTemplateInstantiate.cpp @@ -3779,6 +3779,21 @@ bool Sema::InstantiateClassImpl( ActOnFinishDelayedMemberInitializers(Instantiation); + // The class's type invariants, of the specialization's `this`, checked as + // the parser checks them; a spec they apply is used, as in the members. + if (const TypeContractInfo *Invariants = Context.getTypeContract(Pattern); + Invariants && !Instantiation->isInvalidDecl()) { + CXXThisScopeRAII ThisScope(*this, Instantiation, Qualifiers()); + TypeContractInfo &Instantiated = + Context.getOrCreateTypeContract(Instantiation); + for (Expr *Invariant : Invariants->Invariants) { + ExprResult Condition = + ActOnContractCondition(SubstExpr(Invariant, TemplateArgs)); + if (Condition.isUsable()) + Instantiated.Invariants.push_back(Condition.get()); + } + } + // FIXME: We should do something similar for explicit instantiations so they // end up in the right module. if (TSK == TSK_ImplicitInstantiation) { From fac54c02be72f331dfa411b4fedb6bde632f36e3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:11:34 +0530 Subject: [PATCH 41/64] verify: Verify the members of each instantiated class template specialization, and report members none instantiates. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 97 +++++++++++++++++++--- 1 file changed, 85 insertions(+), 12 deletions(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index d467cc2be1..3f258428cb 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -2026,7 +2026,27 @@ static void collectFunctionCandidates(const DeclContext *DC, ASTContext &Ctx, collectFunctionCandidates(LS, Ctx, Out); continue; } + if (const auto *CTD = dyn_cast(D)) { + // A class template's members are functions of each specialization + // this translation unit instantiates; its pattern's members are + // reported where none of their instantiations is verified. The + // redeclarations of a template share its specializations. + if (const CXXRecordDecl *Pattern = CTD->getTemplatedDecl(); + Pattern->isCompleteDefinition()) + collectFunctionCandidates(Pattern, Ctx, Out); + if (CTD->isCanonicalDecl()) + for (const ClassTemplateSpecializationDecl *Spec : + CTD->specializations()) + if (Spec->getSpecializationKind() != TSK_ExplicitSpecialization && + Spec->isCompleteDefinition()) + collectFunctionCandidates(Spec, Ctx, Out); + continue; + } if (const auto *RD = dyn_cast(D)) { + // An instantiated specialization is collected from its template. + if (const auto *Spec = dyn_cast(RD); + Spec && Spec->getSpecializationKind() != TSK_ExplicitSpecialization) + continue; if (RD->isCompleteDefinition()) collectFunctionCandidates(RD, Ctx, Out); continue; @@ -2060,6 +2080,45 @@ static void collectFunctionCandidates(const DeclContext *DC, ASTContext &Ctx, } } +/// Whether a function template or a member of a class template, as +/// written, has a specialization this translation unit instantiates, with a +/// definition or a contract: nothing for a member of a class nested in a +/// template, which is not looked for. +static std::optional isInstantiated(const FunctionDecl *FD, + const ASTContext &Ctx) { + auto Instantiated = [&](const FunctionDecl *Spec) { + return Spec->isTemplateInstantiation() && + (Spec->isThisDeclarationADefinition() || + Ctx.getFunctionContract(Spec)); + }; + const FunctionTemplateDecl *Template = FD->getDescribedFunctionTemplate(); + const auto *Class = dyn_cast(FD->getDeclContext()); + if (!Class || !Class->isDependentContext()) + return Template && llvm::any_of(Template->specializations(), Instantiated); + const ClassTemplateDecl *ClassTemplate = Class->getDescribedClassTemplate(); + if (!ClassTemplate) + return std::nullopt; + for (const ClassTemplateSpecializationDecl *Spec : + ClassTemplate->specializations()) + for (const Decl *Member : Spec->decls()) { + if (const auto *M = dyn_cast(Member)) { + const FunctionDecl *From = M->getInstantiatedFromMemberFunction(); + if (From && From->getCanonicalDecl() == FD->getCanonicalDecl() && + Instantiated(M)) + return true; + } + if (const auto *MT = dyn_cast(Member)) { + const FunctionTemplateDecl *From = + MT->getInstantiatedFromMemberTemplate(); + if (From && Template && + From->getCanonicalDecl() == Template->getCanonicalDecl() && + llvm::any_of(MT->specializations(), Instantiated)) + return true; + } + } + return false; +} + /// What remains of a function that uses a construct the verifier does not /// represent: an executable or proof function becomes the contract its /// callers assume, not verified; a spec, a declaration without the @@ -2206,22 +2265,36 @@ std::vector> ASTConverter::convertTranslationUnit() { // verified code calls it, which reports the call. if (!functionContract(FD) && !hasContractStatements(FD, Ctx)) continue; - // A function template is verified in each of its specializations, - // which follow it: what it means depends on its arguments. + // A template is verified in each of its specializations, which follow + // it: what it means depends on its arguments. if (!UnsupportedMember) { - const FunctionTemplateDecl *Template = - FD->getDescribedFunctionTemplate(); - if (Template && !FD->isInStdNamespace() && + // A member of a class template is named with its parameters, + // Box::get, as the class's own type names it. + std::string Name = functionName(FD, isa(FD)); + if (const auto *Class = dyn_cast(FD->getDeclContext())) + if (const ClassTemplateDecl *ClassTemplate = + Class->getDescribedClassTemplate()) { + Name.clear(); + llvm::raw_string_ostream OS(Name); + OS << ClassTemplate->getQualifiedNameAsString(); + printTemplateArgumentList( + OS, ClassTemplate->getInjectedTemplateArgs(Ctx), + Ctx.getPrintingPolicy()); + OS << "::" << functionName(FD); + } + if (!FD->isInStdNamespace() && Ctx.getSourceManager().isWrittenInMainFile(FD->getLocation()) && - llvm::none_of(Template->specializations(), - [](const FunctionDecl *Spec) { - return Spec->isTemplateInstantiation(); - })) + isInstantiated(FD, Ctx) == false) Warnings.emplace_back( FD->getLocation(), - functionName(FD) + ": function template is not verified: this " - "translation unit instantiates none of its " - "specializations"); + Name + + (FD->getDescribedFunctionTemplate() + ? ": function template is not verified: this " + "translation unit instantiates none of its " + "specializations" + : ": member of a class template is not verified: this " + "translation unit instantiates it in none of the " + "class's specializations")); continue; } llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); From f8072f8d1872617a99928fc0553849da1b17b92c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:11:34 +0530 Subject: [PATCH 42/64] test: Check class templates verified in each specialization. --- clang/test/Verify/suite/class_templates.cpp | 180 ++++++++++++++++++++ 1 file changed, 180 insertions(+) create mode 100644 clang/test/Verify/suite/class_templates.cpp diff --git a/clang/test/Verify/suite/class_templates.cpp b/clang/test/Verify/suite/class_templates.cpp new file mode 100644 index 0000000000..0bf458416a --- /dev/null +++ b/clang/test/Verify/suite/class_templates.cpp @@ -0,0 +1,180 @@ +// RUN: not %cpp-verify --jobs=1 %s -- > %t 2>&1 +// RUN: FileCheck %s < %t +// RUN: FileCheck %s --check-prefix=NOTE < %t +// RUN: FileCheck %s --check-prefix=SOUND < %t +// +// A class template is verified in each specialization the translation unit +// instantiates: its members' contracts are instantiated with the members +// used, and its type invariants with the class. +// +// No proof here holds only because no execution reaches its end. +// SOUND-NOT: vacuous + + +template +class Box { +public: + Box(T v) + cppverify::pre(0 <= v && v <= 100) + cppverify::post(value == v) + : value(v) {} + + T get() const + cppverify::post(cppverify::result == value) + { + return value; + } + + // 2 * 100 is no signed char. + T twice() const + cppverify::post(cppverify::result == 2 * value) + { + return value + value; + } + + void reset() + cppverify::post(value == 0) + { + value = 0; + } + // CHECK-DAG: class_templates.cpp:[[@LINE-5]]:8: warning: Box::reset: member of a class template is not verified: this translation unit instantiates it in none of the class's specializations + + T value; + + cppverify::type_invariant(0 <= value && value <= 100); +}; + +int boxed() + cppverify::post(cppverify::result == 7) +{ + Box b(7); + int v = b.get(); + return v; +} +// CHECK-DAG: Verified: Box::Box [backend=z3] +// CHECK-DAG: Verified: Box::get [backend=z3] +// CHECK-DAG: Verified: boxed [backend=z3] + +// The invariant of a Box passed by reference. +int bounded(const Box &b) + cppverify::post(cppverify::result <= 100) +{ + int v = b.get(); + return v; +} +// CHECK-DAG: Verified: bounded [backend=z3] + +int twice_int() + cppverify::post(cppverify::result == 200) +{ + Box b(100); + int t = b.twice(); + return t; +} + +signed char twice_char() +{ + Box c(100); + signed char t = c.twice(); + return t; +} +// CHECK-DAG: Verified: Box::twice [backend=z3] +// CHECK-DAG: Verified: twice_int [backend=z3] +// CHECK-DAG: Verified: Box::Box [backend=z3] +// CHECK-DAG: error: verification failed: Box::twice [{{.*}}::postcondition@ +// NOTE: error: verification failed: Box::twice +// NOTE-NEXT: class_templates.cpp:[[@LINE-8]]:21: note: in instantiation of member function 'Box::twice' requested here + +// An out-of-line definition with a contract, explicitly instantiated. +template +struct Pair { + T a; + T b; + T larger() const; +}; + +template +T Pair::larger() const + cppverify::post(cppverify::result >= a && cppverify::result >= b) +{ + return a < b ? b : a; +} + +template struct Pair; +// CHECK-DAG: Verified: Pair::larger [backend=z3] + +// A member function template of a class template. +template +struct Acc { + T total; + + template + void add(U d) + cppverify::pre(0 <= d && d <= 10 && 0 <= total && total <= 1000) + cppverify::modifies(total) + cppverify::post(total == cppverify::old(total) + d) + { + total = total + d; + } +}; + +int accumulated() + cppverify::post(cppverify::result == 8) +{ + Acc a; + a.total = 0; + a.add(5); + a.add((short)3); + return a.total; +} +// CHECK-DAG: Verified: Acc::add [backend=z3] +// CHECK-DAG: Verified: Acc::add [backend=z3] +// CHECK-DAG: Verified: accumulated [backend=z3] + +// Never instantiated. +template +struct Unused { + T x; + + T same() const + cppverify::post(cppverify::result == x) + { + return x; + } + // CHECK-DAG: class_templates.cpp:[[@LINE-5]]:5: warning: Unused::same: member of a class template is not verified: this translation unit instantiates it in none of the class's specializations +}; + +// A spec template applied in a class template's invariant. +template +cppverify::spec bool small(T v) { return 0 <= v && v <= 9; } + +template +class Digit { +public: + Digit(T v) + cppverify::pre(small(v)) + cppverify::post(d == v) + : d(v) {} + + T get() const + cppverify::post(cppverify::result == d) + { + return d; + } + + T d; + + cppverify::type_invariant(small(d)); +}; + +int digit() + cppverify::post(0 <= cppverify::result && cppverify::result <= 9) +{ + Digit x(7); + int v = x.get(); + return v; +} +// CHECK-DAG: Verified: spec axiom: small +// CHECK-DAG: Verified: Digit::Digit [backend=z3] +// CHECK-DAG: Verified: Digit::get [backend=z3] +// CHECK-DAG: Verified: digit [backend=z3] From acb14a1e458b5ea1a89c2b0a097e79cd51fcacc1 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:11:34 +0530 Subject: [PATCH 43/64] test: Check that a class template's invariant and members' contracts are checked where instantiated. --- .../test/Verify/template_contract_errors.cpp | 21 +++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/clang/test/Verify/template_contract_errors.cpp b/clang/test/Verify/template_contract_errors.cpp index f72dc05954..15c4f356eb 100644 --- a/clang/test/Verify/template_contract_errors.cpp +++ b/clang/test/Verify/template_contract_errors.cpp @@ -88,6 +88,27 @@ void uses_body() { loops(Pair{1, 2}); // expected-note {{in instantiation of function template specialization 'loops' requested here}} } +// A class template's invariant is checked where the class is instantiated, +// and a member's contract where the member is used. +template +struct Holder { + T held; + + int first() const + cppverify::post(cppverify::result == held.first) // expected-error {{member reference base type 'const int' is not a structure or union}} + { + return 0; + } + + cppverify::type_invariant(held); // expected-error {{value of type 'Pair' is not contextually convertible to 'bool'}} +}; + +int uses_holder() { + Holder h{1}; + Holder q{{1, 2}}; // expected-note {{in instantiation of template class 'Holder' requested here}} + return h.first() + q.first(); // expected-note {{in instantiation of member function 'Holder::first' requested here}} +} + // Used only with arguments its contract fits. template int only_records(T v) From 293a022c05aa73ef924a4b90d3db02c14374c2ff Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:11:35 +0530 Subject: [PATCH 44/64] test: Expect class template contracts kept without a warning. --- clang/test/Verify/template_contracts.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/clang/test/Verify/template_contracts.cpp b/clang/test/Verify/template_contracts.cpp index d3d8b7509f..5dab094563 100644 --- a/clang/test/Verify/template_contracts.cpp +++ b/clang/test/Verify/template_contracts.cpp @@ -1,11 +1,12 @@ // RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -verify %s // RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -emit-llvm -o - %s | FileCheck %s // RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -ast-dump -ast-dump-filter temporaries %s | FileCheck %s --check-prefix=CLEANUPS +// expected-no-diagnostics // // A contract may depend on a template parameter: it is checked where it is // instantiated, as C++ conditions are. A function template's contract is -// instantiated with each specialization; the contracts of a class template -// are not verified yet and are ignored with a warning. Either compiles and +// instantiated with each specialization, and a class template's members' +// contracts and type invariants with the class. Either compiles and // instantiates like any other template. template @@ -41,9 +42,9 @@ void fill(T *p, T n, T v) template struct Box { T value; - cppverify::type_invariant(value == value); // expected-warning {{contracts in class template 'Box' are not yet supported and are ignored}} + cppverify::type_invariant(value == value); - T get() const // expected-warning {{contracts in class template 'Box' are not yet supported and are ignored}} + T get() const cppverify::post(cppverify::result == value) { return value; From 0b214a11c3ee9f3f2d77e8a1293b6bd11b54e389 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:11:35 +0530 Subject: [PATCH 45/64] docs: Describe class templates verified in each specialization. --- website/source/language/structs.rst | 81 +++++++++++++++++++++++++++-- 1 file changed, 77 insertions(+), 4 deletions(-) diff --git a/website/source/language/structs.rst b/website/source/language/structs.rst index e2b6f029b6..0418a15a4a 100644 --- a/website/source/language/structs.rst +++ b/website/source/language/structs.rst @@ -567,10 +567,11 @@ which ``reset_count`` may not. ``copy_from`` writes ``this->n`` and reads object twice. Not yet supported, each an error naming the function: virtual functions, -member functions of a class with bases, destructors, conversion functions, -and member functions of a class template (whose contracts are ignored with a -warning). A member call inside an expression (``return n + get();``) is -unsupported as a free function's is; assign its result first. +member functions of a class with bases, destructors, and conversion +functions. A member call inside an expression (``return n + get();``) is +unsupported as a free function's is; assign its result first. A class +template's member functions are verified in each specialization (`Class +templates`_). Member operators ~~~~~~~~~~~~~~~~ @@ -845,6 +846,78 @@ internal calls included, so no call observes the object while it is broken: states nothing; the next call checks it from what its caller knows, so a member function that changes ``len`` states how. +Class templates +--------------- + +A class template is verified in each specialization the translation unit +instantiates, as a function template is (:doc:`functions-loops`): a member's +contract is instantiated with the member, in each specialization that uses +it, and the class's type invariants with the class. + +.. cppverify-example: fails Box::twice + +.. code-block:: cpp + + template + 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 b(v); + int d = b.twice(); + return d; + } + + short doubled_short(short v) + cv::pre(0 <= v && v <= 20000) + { + Box b(v); + short d = b.twice(); + return d; + } + +.. code-block:: text + + Verified: Box::Box [backend=z3] + Verified: Box::twice [backend=z3] + Verified: Box::Box [backend=z3] + box.cpp:10:25: error: verification failed: Box::twice [...::postcondition@10:25] (counterexample: ...) [backend=z3] [reason=counterexample] + box.cpp:33:15: note: in instantiation of member function 'Box::twice' requested here + Verified: doubled [backend=z3] + Unresolved: doubled_short [backend=z3] [reason=callee.contract] (relies on the contract of Box::twice, which is not established) + +``value + value`` is an ``int``, which a ``short`` holds only up to 32767. + +- A member is verified in the specializations that use it, or that an + explicit instantiation (``template class Box;``) defines whole. One + that no specialization uses is reported, not verified: ``warning: + Box::reset: member of a class template is not verified: this + translation unit instantiates it in none of the class's specializations``. +- A clause that does not fit the arguments is a compiler error with Clang's + instantiation note: an invariant where the class is instantiated, a + member's contract where the member is used. +- Member function templates of a class template, member definitions outside + the class, and specs that the invariant applies are instantiated as the + rest is. + View functions -------------- From 6d381a2517ee0783420738f280778bae90132d2c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:11:35 +0530 Subject: [PATCH 46/64] docs: Point the templates section to class templates. --- website/source/language/functions-loops.rst | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index 14fe1113f4..6137463e33 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -293,16 +293,16 @@ named with its arguments. over a quantifier binds a variable of its own in each element. - A specialization the verifier cannot represent (``maxv``) costs that specialization alone, as a construct in any function does. -- The contracts of a class template's members and its type invariants are - not verified yet: they compile, instantiate with the template, and are - ignored, with a ``-Wcontract-unsupported`` warning that names the class - template. +- A class template is verified in each specialization too: its members' + contracts are instantiated with the members, and its type invariants with + the class (:doc:`structs`). - A template without contracts changes nothing for the rest of the file, as long as verified code does not call it. -Before 0.2, a function template's contracts were ignored with a warning, and -a call to one from verified code was ``call to function without a -verification contract``. A template whose contract depended on its +Before 0.2, the contracts of templates were ignored with a warning +(``-Wcontract-unsupported``, which no longer reports anything), and a call to +one from verified code was ``call to function without a verification +contract``. A template whose contract depended on its parameters did not compile (``value of type '' is not contextually convertible to 'bool'``), nor did ``cv::result`` or ``cv::old(x)`` of the template's type compared with a constant From 1723524935e57d2d61f03e115399769ac81dca55 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:11:36 +0530 Subject: [PATCH 47/64] docs: List class templates as supported. --- website/source/language/limitations.rst | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 117a218135..9c20cfa4a4 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -158,8 +158,9 @@ C++ feature boundaries through a pointer (``Ring copy = *r;``). * - Functions - Free functions, member functions of classes without bases or virtual - functions (:doc:`structs`), function templates in each specialization - the translation unit instantiates (:doc:`functions-loops`), + functions (:doc:`structs`), function and class templates in each + specialization the translation unit instantiates + (:doc:`functions-loops`, :doc:`structs`), overloads, namespaces, contracts, direct calls, and direct and mutual recursion, also through stores to pointer and reference parameters and through automatic objects, with mutual @@ -167,9 +168,8 @@ C++ feature boundaries - Virtual functions, member functions of classes with bases, destructors, delegating constructors and the other constructors :doc:`structs` lists, conversion functions, - members and type invariants of class templates (they compile, - instantiate, and are ignored with a warning), function templates - that nothing instantiates (reported), variadics, indirect calls, + templates and members of class templates that nothing instantiates + (reported), variadics, indirect calls, recursion through a function that allocates or frees storage, and general link-time summaries. @@ -215,10 +215,10 @@ otherwise supported code: - ``cppverify::aliases`` between pointers to different types (``aliases between different pointee types are unsupported``). -A member function of a class template has its contracts ignored with a -warning (``-Wcontract-unsupported``: "contracts in class template ... are -not yet supported and are ignored"), and the run continues with the other -functions. +A template is verified in each specialization the translation unit +instantiates; one that nothing instantiates, and a member of a class +template that no specialization uses, is reported with a warning and not +verified, and the run continues with the other functions. Objects, classes, and RAII -------------------------- From 48b82cdaf239eaf9107b0df58988bff593fb6709 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:11:36 +0530 Subject: [PATCH 48/64] docs: Note class templates in the templates release note. --- website/source/release-notes.rst | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 7074ae35da..9ba26d6df8 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -265,9 +265,9 @@ C++ that compiles now ~~~~~~~~~~~~~~~~~~~~~ **Contracts in templates.** A template whose contract depends on its -parameters did not compile. Its contracts now compile and instantiate, and -are ignored with a ``-Wcontract-unsupported`` warning; a template without -contracts no longer stops the file (:doc:`language/functions-loops`). +parameters did not compile. Its contracts now compile and are instantiated +with it (Templates, below), and a template without contracts no longer stops +the file (:doc:`language/functions-loops`). **Apple's assertion macros.** On Apple targets ```` defines a ``check(assertion)`` macro, which turned every ``cppverify::check(...)`` after @@ -336,14 +336,15 @@ on entry. An object passed by reference or pointer satisfies it on entry and, when mutable, at exit, where before only a record passed by value did (:doc:`language/structs`). -**Function templates.** A function template's contracts were ignored with -a warning, so no specialization was verified, and a call to one from -verified code was an error. Each specialization a translation unit -instantiates is now verified as a function of its own, named with its -arguments (``twice``), with its contract instantiated as its body is, -loop contracts, assertions, and ghost code included; a diagnostic about it -notes where it is instantiated, and a contracted template that nothing -instantiates is reported. ``cv::post(cv::result > 0)`` and ``cv::old(x) > 0`` +**Templates.** The contracts of templates were ignored with a warning, so +no specialization was verified, and a call to one from verified code was an +error. Each specialization a translation unit instantiates is now verified +as a function of its own, named with its arguments (``twice``, +``Box::get``), with its contract instantiated as its body is, loop +contracts, assertions, and ghost code included, and a class template's type +invariants with the class; a diagnostic about it notes where it is +instantiated, and a contracted template, or member of a class template, +that nothing instantiates is reported. ``cv::post(cv::result > 0)`` and ``cv::old(x) > 0`` of a template's type did not compile (``invalid operands to binary expression ('T' and 'int')``) (:doc:`language/functions-loops`). From 341378ffaef27b92540126c41e1c258a27c54aba Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:11:36 +0530 Subject: [PATCH 49/64] docs: Design class templates verified per specialization. --- docs/DESIGN.md | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index ff287e8418..f89aa16d0b 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1311,8 +1311,8 @@ void reset_left(Pair &p) - Not yet, each an error naming the function: virtual functions (dispatch needs behavioral subtyping), member functions of classes with bases, destructors, conversion functions, explicit object parameters, rvalue- and - volatile-qualified member functions; members of class templates keep the - template rule. + volatile-qualified member functions. A class template's members are + verified in each specialization (see Templates). ### 3g. Constructors @@ -1839,8 +1839,11 @@ cppverify::proof void sum_concat(seq s, seq t) specialization. - A diagnostic about a specialization notes where it is instantiated, as a compiler's does. -- Not yet: the members and type invariants of class templates, ignored with - `-Wcontract-unsupported`. +- A class template is verified in each specialization too: a member's + contract is instantiated with the member, lazily as a function template's + is, so a member no specialization uses is not verified (it is reported), + and the class's type invariants with the class, eagerly, as a member + `static_assert` is, with the specialization's `this`. ## Clang Modification Details From f18d6a4b0f0af151209be3eaaf0f33cb7de53b04 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:11:37 +0530 Subject: [PATCH 50/64] docs: Describe how class templates are instantiated and collected. --- docs/ARCHITECTURE.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 7bd4019866..1f8981cb9d 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -340,6 +340,20 @@ where each is instantiated (`getInstantiationPoints`), which the driver prints as a note after each error or warning of the specialization (JSON `instantiated_at`). +**Class templates:** the parser keeps the contracts of a class template's +members, whose instantiation is a function template's +(`InstantiateFunctionContract`, where the member is used or defined), and +its type invariants, which `InstantiateClassImpl` instantiates once the +specialization is complete, with its `this` (`CXXThisScopeRAII`), into the +specialization's `TypeContractInfo`. `ActOnTypeInvariantExpr` writes a +field the invariant names bare as `this->field`, as a member function reads +it, so that the instantiation rebuilds it with the specialization's `this`. +`collectFunctionCandidates` visits the pattern's members (for the warning) +and the members of each specialization the translation unit instantiates (an +instantiated specialization in a declaration context is collected from its +template only); `isInstantiated` decides the warning, from a function +template's specializations or the instantiated members of the class's. + **Records in memory by value:** `recordFieldsInMemory` reads a record value kept in memory, a promoted local or one in a pointee or record reference (`promotedRootLocal`, `inPointeeObject`), through implicit copies and From 73ae86902a76d65b26662ce2bac3133a5d7abc05 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:45:38 +0530 Subject: [PATCH 51/64] verify: Declare a quantifier binder's context, and drop the type invariant field rewriter's entry point. --- clang/include/clang/Sema/Sema.h | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/clang/include/clang/Sema/Sema.h b/clang/include/clang/Sema/Sema.h index d34717d871..c889d2bcc3 100644 --- a/clang/include/clang/Sema/Sema.h +++ b/clang/include/clang/Sema/Sema.h @@ -10397,6 +10397,11 @@ class Sema final : public SemaBase { /// A component of a decreases clause, which must be an integer. ExprResult ActOnContractMeasure(ExprResult E); + /// The context of a quantifier's or a choice's binder: the current one, + /// or, in a class (a type invariant), the nearest one around it, since a + /// variable of a class is a member and a binder is not. + DeclContext *getContractBinderContext() const; + /// forall, exists, or choose (\p Kind) over \p Binder: its bounds must be /// integers and its body a condition. ExprResult BuildContractBinderExpr(Stmt::StmtClass Kind, @@ -10405,8 +10410,6 @@ class Sema final : public SemaBase { SourceLocation RParenLoc, VarDecl *Binder, Expr *Lo, Expr *Hi, Expr *Body); - /// Rewrite unqualified field names to this->field for type_invariant(expr). - ExprResult ActOnTypeInvariantExpr(ExprResult E, CXXRecordDecl *Record); /// Diagnose references to spec functions in executable code of \p FD /// (or in a global initializer when \p FD is null). Spec functions are From 90d60bb8fd244c2528813db43c3107f62837e723 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:45:38 +0530 Subject: [PATCH 52/64] verify: Declare a binder outside a class, and drop the field rewriter that Sema's own this->field made dead. --- clang/lib/Sema/SemaContract.cpp | 51 +++++---------------------------- 1 file changed, 7 insertions(+), 44 deletions(-) diff --git a/clang/lib/Sema/SemaContract.cpp b/clang/lib/Sema/SemaContract.cpp index efdf9984c3..9a0b99538b 100644 --- a/clang/lib/Sema/SemaContract.cpp +++ b/clang/lib/Sema/SemaContract.cpp @@ -13,7 +13,6 @@ // //===----------------------------------------------------------------------===// -#include "TreeTransform.h" #include "clang/AST/ASTContext.h" #include "clang/AST/ASTLambda.h" #include "clang/AST/DeclCXX.h" @@ -27,39 +26,6 @@ using namespace clang; namespace { -class TypeInvariantFieldRewriter : public TreeTransform { - typedef TreeTransform Base; - CXXRecordDecl *Record; - -public: - TypeInvariantFieldRewriter(Sema &S, CXXRecordDecl *RD) - : Base(S), Record(RD) {} - - ExprResult TransformDeclRefExpr(DeclRefExpr *E) { - if (FieldDecl *FD = dyn_cast(E->getDecl())) { - if (FD->getParent() == Record) { - // this->field, as a member function reads it, so that a class - // template's instantiation rebuilds it with its own `this`. - SourceLocation Loc = E->getBeginLoc(); - QualType ThisTy = getSema().getCurrentThisType(); - if (ThisTy.isNull()) - return Base::TransformDeclRefExpr(E); - ExprResult This = - getSema().BuildCXXThisExpr(Loc, ThisTy, /*IsImplicit=*/true); - if (This.isInvalid()) - return ExprError(); - DeclarationNameInfo NameInfo(FD->getDeclName(), Loc); - return getSema().BuildMemberExpr( - This.get(), /*IsArrow=*/true, Loc, NestedNameSpecifierLoc(), - SourceLocation(), FD, DeclAccessPair::make(FD, FD->getAccess()), - /*HadMultipleCandidates=*/false, NameInfo, FD->getType(), - VK_LValue, OK_Ordinary, /*TemplateArgs=*/nullptr); - } - } - return Base::TransformDeclRefExpr(E); - } -}; - const FunctionContractInfo *contractOf(const ASTContext &Ctx, const FunctionDecl *FD) { for (const FunctionDecl *Redecl : FD->redecls()) @@ -320,6 +286,13 @@ ExprResult Sema::ActOnContractMeasure(ExprResult E) { return ExprError(); } +DeclContext *Sema::getContractBinderContext() const { + DeclContext *DC = CurContext; + while (DC->isRecord()) + DC = DC->getParent(); + return DC; +} + ExprResult Sema::BuildContractBinderExpr(Stmt::StmtClass Kind, SourceLocation KeywordLoc, SourceLocation LParenLoc, @@ -349,13 +322,3 @@ ExprResult Sema::BuildContractBinderExpr(Stmt::StmtClass Kind, Lo, Hi, Condition.get(), Context.BoolTy); } } - -ExprResult Sema::ActOnTypeInvariantExpr(ExprResult E, CXXRecordDecl *Record) { - if (E.isInvalid() || !Record) - return E; - TypeInvariantFieldRewriter Rewriter(*this, Record); - ExprResult Transformed = Rewriter.TransformExpr(E.get()); - if (Transformed.isInvalid()) - return Transformed; - return ActOnContractCondition(Transformed.get()); -} From 8ebd638df7f6e56ce6e54d6d53477e405c226129 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:45:38 +0530 Subject: [PATCH 53/64] verify: Declare a binder in its context, and check a type invariant as a condition. --- clang/lib/Parse/ParseCppVerify.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/clang/lib/Parse/ParseCppVerify.cpp b/clang/lib/Parse/ParseCppVerify.cpp index 2ef2d335fd..39f8952d0c 100644 --- a/clang/lib/Parse/ParseCppVerify.cpp +++ b/clang/lib/Parse/ParseCppVerify.cpp @@ -896,10 +896,10 @@ void Parser::ParseTypeInvariant(Decl *TagDecl) { return Finish(); } ConsumeParen(); - // A class template's invariants are instantiated with each of its - // specializations. + // With the class's `this` in scope, a field named bare is this->field. A + // class template's invariants are instantiated with each specialization. if (!E.isInvalid()) { - E = Actions.ActOnTypeInvariantExpr(E, RD); + E = Actions.ActOnContractCondition(E); if (!E.isInvalid()) Actions.getASTContext().getOrCreateTypeContract(RD).Invariants.push_back( E.get()); @@ -1343,8 +1343,8 @@ ExprResult Parser::ParseQuantifierExpr() { // Create the bound variable and push it into scope for the body. VarDecl *BoundVar = VarDecl::Create( - Ctx, Actions.CurContext, BinderLoc, BinderLoc, BinderII, Ctx.IntTy, - Ctx.getTrivialTypeSourceInfo(Ctx.IntTy, BinderLoc), SC_None); + Ctx, Actions.getContractBinderContext(), BinderLoc, BinderLoc, BinderII, + Ctx.IntTy, Ctx.getTrivialTypeSourceInfo(Ctx.IntTy, BinderLoc), SC_None); ParseScope QuantifierScope(this, Scope::DeclScope); Actions.PushOnScopeChains(BoundVar, getCurScope(), /*AddToContext=*/false); ++QuantifierBodyDepth; From bc7c72e92fbfad670344deb7b5afbb2541312ed8 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:45:39 +0530 Subject: [PATCH 54/64] verify: Rebuild a binder in the binder context. --- clang/lib/Sema/TreeTransform.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/clang/lib/Sema/TreeTransform.h b/clang/lib/Sema/TreeTransform.h index 5f5aa41e76..5e33617c37 100644 --- a/clang/lib/Sema/TreeTransform.h +++ b/clang/lib/Sema/TreeTransform.h @@ -18457,10 +18457,11 @@ StmtResult TreeTransform::TransformRevealSpecStmt(RevealSpecStmt *S) { template VarDecl *TreeTransform::TransformContractBinder(VarDecl *Binder) { // Declared as the parser declares it, in the context being built. - if (Binder->getDeclContext() == SemaRef.CurContext) + DeclContext *Context = SemaRef.getContractBinderContext(); + if (Binder->getDeclContext() == Context) return Binder; VarDecl *New = VarDecl::Create( - SemaRef.Context, SemaRef.CurContext, Binder->getBeginLoc(), + SemaRef.Context, Context, Binder->getBeginLoc(), Binder->getLocation(), Binder->getIdentifier(), Binder->getType(), Binder->getTypeSourceInfo(), SC_None); getDerived().transformedLocalDecl(Binder, {New}); From 22bda7326640021d9cdcbe2f67a8c860ffaac59a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:45:39 +0530 Subject: [PATCH 55/64] test: Check quantified invariants, and an explicit instantiation's members verified once. --- clang/test/Verify/suite/class_templates.cpp | 40 +++++++++++++++++++++ 1 file changed, 40 insertions(+) diff --git a/clang/test/Verify/suite/class_templates.cpp b/clang/test/Verify/suite/class_templates.cpp index 0bf458416a..63be7ecb10 100644 --- a/clang/test/Verify/suite/class_templates.cpp +++ b/clang/test/Verify/suite/class_templates.cpp @@ -2,6 +2,7 @@ // RUN: FileCheck %s < %t // RUN: FileCheck %s --check-prefix=NOTE < %t // RUN: FileCheck %s --check-prefix=SOUND < %t +// RUN: grep -c "Verified: Pair::larger" %t | FileCheck %s --check-prefix=ONCE // // A class template is verified in each specialization the translation unit // instantiates: its members' contracts are instantiated with the members @@ -102,6 +103,7 @@ T Pair::larger() const template struct Pair; // CHECK-DAG: Verified: Pair::larger [backend=z3] +// ONCE: 1 // A member function template of a class template. template @@ -178,3 +180,41 @@ int digit() // CHECK-DAG: Verified: Digit::Digit [backend=z3] // CHECK-DAG: Verified: Digit::get [backend=z3] // CHECK-DAG: Verified: digit [backend=z3] + +// A quantifier in a type invariant binds a variable of its own, not a +// member of the class. +struct Quad { + int cells[4]; + + int first() const + cppverify::post(cppverify::result >= 0) + { + return cells[0]; + } + + cppverify::type_invariant(cppverify::forall(k, 0, 4, cells[k] >= 0)); +}; + +template +struct Cells { + T cells[4]; + + T last() const + cppverify::post(cppverify::result >= 0) + { + return cells[3]; + } + + cppverify::type_invariant(cppverify::forall(k, 0, 4, cells[k] >= 0)); +}; + +int quad(const Quad &q, const Cells &c) + cppverify::post(cppverify::result >= 0) +{ + int a = q.first(); + int b = c.last(); + return a < b ? a : b; +} +// CHECK-DAG: Verified: Quad::first [backend=z3] +// CHECK-DAG: Verified: Cells::last [backend=z3] +// CHECK-DAG: Verified: quad [backend=z3] From 5c7a8e77c965bbe9f0da90a61bd31b98275e8bf5 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 20:45:40 +0530 Subject: [PATCH 56/64] docs: Describe an invariant's this and a binder's context. --- docs/ARCHITECTURE.md | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 1f8981cb9d..496b8b0b85 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -345,14 +345,18 @@ members, whose instantiation is a function template's (`InstantiateFunctionContract`, where the member is used or defined), and its type invariants, which `InstantiateClassImpl` instantiates once the specialization is complete, with its `this` (`CXXThisScopeRAII`), into the -specialization's `TypeContractInfo`. `ActOnTypeInvariantExpr` writes a -field the invariant names bare as `this->field`, as a member function reads -it, so that the instantiation rebuilds it with the specialization's `this`. -`collectFunctionCandidates` visits the pattern's members (for the warning) -and the members of each specialization the translation unit instantiates (an -instantiated specialization in a declaration context is collected from its -template only); `isInstantiated` decides the warning, from a function -template's specializations or the instantiated members of the class's. +specialization's `TypeContractInfo`. 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`. A +quantifier's binder in it belongs to the context around the class +(`Sema::getContractBinderContext`): a variable of a class is a member, and +an assertions build stopped at the first lookup of one without an access +specifier. `collectFunctionCandidates` visits the pattern's members (for the +warning) and the members of each specialization the translation unit +instantiates (an instantiated specialization in a declaration context is +collected from its template only); `isInstantiated` decides the warning, +from a function template's specializations or the instantiated members of +the class's. **Records in memory by value:** `recordFieldsInMemory` reads a record value kept in memory, a promoted local or one in a pointee or record reference From 9b35bc968a3ecfc31de4536517c8c70c73aaa437 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 21:23:19 +0530 Subject: [PATCH 57/64] verify: Declare the std::min and std::max model and the value references of lifted specs. --- clang/lib/Verify/Frontend/ASTConverter.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index cdb8defd6f..b56211f6ef 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -74,6 +74,9 @@ class ASTConverter { std::map> InstantiationPoints; std::map ParameterNames; + /// The parameters of a lifted spec that refer to const scalars, which + /// stand for the values they refer to. + std::set ValueReferences; /// For a parameter a pack expands to, its index in the pack, `...[1]`. std::map PackElements; /// Names each parameter of \p FD after the declaration \p ContractDecl @@ -185,6 +188,9 @@ class ASTConverter { /// The address of a supported mutable global, or null after an error. std::unique_ptr globalAddress(const VarDecl *VD, SourceLocation Loc); std::unique_ptr convertConstexprSpec(const FunctionDecl *FD); + /// std::max(a, b), or std::min(a, b), of two integers, as the standard + /// defines it. + std::unique_ptr convertMinOrMax(const CallExpr *CE, bool IsMax); void noteSpecUse(const FunctionDecl *FD); std::unique_ptr convertExpr(const Expr *E); std::unique_ptr convertExprImpl(const Expr *E); From dc48d54b92a81f3f4d96f310eebb8c4517933b1b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 21:23:19 +0530 Subject: [PATCH 58/64] verify: Model std::min and std::max of two integers, read a lifted spec's const references as values, and name a helper that cannot be lifted. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 131 +++++++++++++++++---- 1 file changed, 111 insertions(+), 20 deletions(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index 3f258428cb..026396c1ed 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -686,8 +686,20 @@ static const FunctionDecl *ownObjectCallee(const Expr *E) { return Callee && returnsOwnObject(Callee) ? Callee : nullptr; } +/// A reference to a const scalar, which a spec function reads as the value it +/// refers to: that value's type, else the type itself. +static QualType constScalarReferent(QualType Ty) { + const QualType Referent = Ty.getNonReferenceType(); + return Ty->isLValueReferenceType() && Referent.isConstQualified() && + !Referent.isVolatileQualified() && + Referent->isIntegralOrEnumerationType() + ? Referent.getUnqualifiedType() + : Ty; +} + static std::optional -findUnsupportedType(const FunctionDecl *FD, bool AllowScalarReferences) { +findUnsupportedType(const FunctionDecl *FD, bool AllowScalarReferences, + bool ConstScalarReferencesAreValues = false) { // By-value records keep their flattened SSA representation, so only records // whose direct fields are scalars may cross a function boundary. auto UnsupportedValueType = [](QualType Ty) { @@ -696,10 +708,14 @@ findUnsupportedType(const FunctionDecl *FD, bool AllowScalarReferences) { return Ty->isRecordType() && !isFlatScalarRecordType(Ty) && !VType::collectionKind(Ty); }; - if (UnsupportedValueType(FD->getReturnType()) && !returnsOwnObject(FD)) + auto Viewed = [&](QualType Ty) { + return ConstScalarReferencesAreValues ? constScalarReferent(Ty) : Ty; + }; + if (UnsupportedValueType(Viewed(FD->getReturnType())) && + !returnsOwnObject(FD)) return FD->getReturnType().getAsString(); for (const ParmVarDecl *Param : FD->parameters()) { - QualType Ty = Param->getType(); + QualType Ty = Viewed(Param->getType()); if (Ty->isReferenceType()) { if (!AllowScalarReferences || !(isSupportedScalarLValueReference(Ty) || @@ -915,6 +931,28 @@ VIntMode ASTConverter::specCallIntMode(const FunctionDecl *FD) const { return VIntMode::Math; } +/// For std::min(a, b) and std::max(a, b) of two integers, enumerations, or +/// bools: whether it is max. Nothing for any other function, such as the +/// overloads with a comparison or an initializer list. +static std::optional stdMinOrMax(const FunctionDecl *Callee, + const ASTContext &Ctx) { + if (!Callee || !Callee->isInStdNamespace() || !Callee->getIdentifier() || + !Callee->getPrimaryTemplate() || Callee->getNumParams() != 2) + return std::nullopt; + const bool IsMax = Callee->getName() == "max"; + if (!IsMax && Callee->getName() != "min") + return std::nullopt; + const QualType Result = Callee->getReturnType(); + const QualType T = Result.getNonReferenceType(); + if (!Result->isLValueReferenceType() || !T.isConstQualified() || + T.isVolatileQualified() || !T->isIntegralOrEnumerationType()) + return std::nullopt; + for (const ParmVarDecl *P : Callee->parameters()) + if (!Ctx.hasSameType(P->getType(), Result)) + return std::nullopt; + return IsMax; +} + /// A function as the verifier's messages name it, a template specialization /// with its arguments (`maxv`). static std::string functionName(const FunctionDecl *FD, @@ -3930,6 +3968,27 @@ bool ASTConverter::checkLoopTermination(const Stmt *Loop, bool HasMeasure) { return true; } +std::unique_ptr ASTConverter::convertMinOrMax(const CallExpr *CE, + bool IsMax) { + // The standard's meaning ([alg.min.max]), whatever the library: the first + // argument unless the other is less (max) or greater (min) than it, which + // reads each argument once and has no definedness condition of its own. + auto A = convertExpr(CE->getArg(0)); + auto B = convertExpr(CE->getArg(1)); + if (!A || !B) + return nullptr; + const SourceLocation Loc = CE->getExprLoc(); + const VType Ty = A->Ty; + auto Less = IsMax ? std::make_unique(VBinOp::Lt, cloneVExpr(A.get()), + cloneVExpr(B.get()), + VType::makeBool(), Loc) + : std::make_unique(VBinOp::Lt, cloneVExpr(B.get()), + cloneVExpr(A.get()), + VType::makeBool(), Loc); + return std::make_unique(std::move(Less), std::move(B), + std::move(A), Ty, Loc); +} + std::unique_ptr ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); @@ -3937,21 +3996,35 @@ ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { llvm::SaveAndRestore InContract(ErrorInContract, true); const size_t ErrorsAtStart = Errors.size(); nameParameters(FD, FD); - if (exceedsNestingLimit(FD, functionContract(FD)) || - hasIndirectMemoryAccess(FD)) - return nullptr; if (!FD->isConstexpr() || !FD->hasBody()) return nullptr; - if (FD->getReturnType()->isRecordType()) { - error(functionName(FD) + - ": aggregate-returning constexpr specs are unsupported"); - return nullptr; - } - if (auto Unsupported = findUnsupportedType(FD, false)) { - error(functionName(FD) + - ": unsupported C++ type in verification: " + *Unsupported); - return nullptr; - } + // One the verifier cannot lift is kept as a declaration that uses an + // unsupported construct, so that its users' verdicts name it. + auto Unlifted = [&](std::optional Message) { + if (Message) + error(FD->getLocation(), functionName(FD) + ": " + *Message); + auto Fn = std::make_unique(); + Fn->Name = functionName(FD); + Fn->Identity = functionIdentity(FD); + Fn->DeclLoc = FD->getLocation(); + Fn->IsSpec = true; + Fn->IsConstexprSpec = true; + return Fn; + }; + if (exceedsNestingLimit(FD, functionContract(FD))) + return Unlifted(std::nullopt); + if (hasIndirectMemoryAccess(FD)) + return Unlifted("a constexpr function read as a spec cannot read memory " + "through a pointer or an array"); + if (FD->getReturnType()->isRecordType()) + return Unlifted("aggregate-returning constexpr specs are unsupported"); + // A spec is a function of values: a reference to a const scalar, which it + // only reads, stands for the value it refers to, as an argument and as the + // result (std::max's `const T &`). + if (auto Unsupported = + findUnsupportedType(FD, /*AllowScalarReferences=*/false, + /*ConstScalarReferencesAreValues=*/true)) + return Unlifted("unsupported C++ type in verification: " + *Unsupported); auto Fn = std::make_unique(); Fn->Name = functionName(FD); @@ -3960,9 +4033,11 @@ ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { Fn->IsConstexprSpec = true; IntMode = VIntMode::Machine; Fn->IntMode = IntMode; - Fn->ReturnType = VType::fromQualType(FD->getReturnType(), IntMode, Ctx); + Fn->ReturnType = + VType::fromQualType(constScalarReferent(FD->getReturnType()), IntMode, Ctx); CurrentFn = Fn.get(); + ValueReferences.clear(); for (const ParmVarDecl *P : FD->parameters()) { if (const RecordDecl *RD = getRecordFromType(P->getType())) { if (const RecordDecl *Definition = RD->getDefinition()) @@ -3971,8 +4046,11 @@ ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { P->getNameAsString() + "." + Field->getNameAsString(), VType::fromQualType(Field->getType(), IntMode, Ctx)); } else { - Fn->Params.emplace_back(P->getNameAsString(), - VType::fromQualType(P->getType(), IntMode, Ctx)); + Fn->Params.emplace_back( + P->getNameAsString(), + VType::fromQualType(constScalarReferent(P->getType()), IntMode, Ctx)); + if (P->getType()->isReferenceType()) + ValueReferences.insert(P); } recordSourceVariable(P); } @@ -3988,10 +4066,12 @@ ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { } if (Fn->Body.empty() && Errors.size() == ErrorsAtStart) { CurrentFn = nullptr; + ValueReferences.clear(); return nullptr; } collectLayouts(FD, *Fn); CurrentFn = nullptr; + ValueReferences.clear(); return Fn; } @@ -5639,7 +5719,7 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { E->getExprLoc()); } requireInitialized(VD); - if (VD->getType()->isReferenceType()) { + if (VD->getType()->isReferenceType() && !ValueReferences.count(VD)) { auto Address = convertLValueAddress(E); if (!Address) { error(CurrentFn->Name + ": unsupported reference value expression"); @@ -6114,6 +6194,17 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { integerValueString(EV.Val.getInt()), Ty, E->getExprLoc()); } } + if (std::optional IsMax = stdMinOrMax(Callee, Ctx)) + return convertMinOrMax(CE, *IsMax); + // The standard library's functions are not lifted: each library + // writes them its own way, so a proof would depend on which one. + if (Callee->isInStdNamespace() && calleeIsSpec(Callee) && + !functionContract(Callee)) { + error(CurrentFn->Name + ": " + Callee->getQualifiedNameAsString() + + " is not modeled: of the standard library, the verifier knows " + "std::min and std::max of two integers"); + return nullptr; + } if (calleeIsSpec(Callee)) { const VIntMode CalleeMode = specCallIntMode(Callee); const FunctionContractInfo *CalleeContract = functionContract(Callee); From 32581d5f3116fc4753d19f373c36e62191b38eb0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 21:23:20 +0530 Subject: [PATCH 59/64] test: Check std::min and std::max, other standard functions, and constexpr helpers taking references. --- clang/test/Verify/suite/std_min_max.cpp | 149 ++++++++++++++++++++++++ 1 file changed, 149 insertions(+) create mode 100644 clang/test/Verify/suite/std_min_max.cpp diff --git a/clang/test/Verify/suite/std_min_max.cpp b/clang/test/Verify/suite/std_min_max.cpp new file mode 100644 index 0000000000..b97cf14c83 --- /dev/null +++ b/clang/test/Verify/suite/std_min_max.cpp @@ -0,0 +1,149 @@ +// RUN: not %cpp-verify --jobs=1 %s -- > %t 2>&1 +// RUN: FileCheck %s < %t +// RUN: FileCheck %s --check-prefix=SOUND < %t +// +// std::min and std::max of two integers mean what the standard says they +// mean, whatever the library: max(a, b) is a unless a < b, and min(a, b) is +// a unless b < a. The library's other functions are not modeled, and a +// constexpr helper's references to const scalars stand for their values. +// +// No proof here holds only because no execution reaches its end. +// SOUND-NOT: vacuous + +#include + +int clamp3(int x) + cppverify::post(cppverify::result == std::max(x, 3)) +{ + return x < 3 ? 3 : x; +} +// CHECK-DAG: Verified: clamp3 [backend=z3] + +int lower(int a, int b) + cppverify::post(cppverify::result == std::min(a, b)) + cppverify::post(cppverify::result <= a && cppverify::result <= b) +{ + int m = std::min(a, b); + return m; +} +// CHECK-DAG: Verified: lower [backend=z3] + +// The first argument when they are equal: std::max(a, b) is a, not b. +unsigned long widest(unsigned long a, unsigned long b) + cppverify::post(cppverify::result >= a && cppverify::result >= b) +{ + unsigned long w = std::max(a, b); + return w; +} +// CHECK-DAG: Verified: widest [backend=z3] + +int wrong(int a, int b) + cppverify::post(cppverify::result == std::max(a, b)) +{ + return std::min(a, b); +} +// CHECK-DAG: error: verification failed: wrong [{{.*}}::postcondition@[[@LINE-4]] + +int clamped(int x) + cppverify::post(cppverify::result == std::clamp(x, 0, 9)) +{ + return x < 0 ? 0 : (x > 9 ? 9 : x); +} +// CHECK-DAG: error: clamped: std::clamp is not modeled: of the standard library, the verifier knows std::min and std::max of two integers + +template +constexpr const T &mymax(const T &a, const T &b) { return a < b ? b : a; } + +int mine(int x) + cppverify::post(cppverify::result == mymax(x, 3)) +{ + return x < 3 ? 3 : x; +} +// CHECK-DAG: Verified: constexpr spec axiom: mymax +// CHECK-DAG: Verified: mine [backend=z3] + +constexpr int first(const int *p) { return p[0]; } + +int reads(const int *p) + cppverify::pre(cppverify::valid(p, 1)) + cppverify::post(cppverify::result == first(p)) +{ + return p[0]; +} +// CHECK-DAG: error: first: a constexpr function read as a spec cannot read memory through a pointer or an array +// CHECK-DAG: Unresolved: reads [reason=construct.unsupported] (relies on first, which uses a construct the verifier does not support) + +long widened(int x) + cppverify::post(cppverify::result == std::max(x, 3L)) + cppverify::post(cppverify::result >= 3) +{ + long w = std::max(x, 3L); + return w; +} +// CHECK-DAG: Verified: widened [backend=z3] + +int above(int a, int b) + cppverify::pre(a < 1000 && b < 1000) + cppverify::post(cppverify::result > a && cppverify::result > b) +{ + return std::max(a, b) + 1; +} +// CHECK-DAG: Verified: above [backend=z3] + +enum Level { Low, Mid, High }; + +Level highest(Level a, Level b) + cppverify::post(cppverify::result >= a && cppverify::result >= b) +{ + Level h = std::max(a, b); + return h; +} +// CHECK-DAG: Verified: highest [backend=z3] + +cppverify::spec int spread(int a, int b) { return std::max(a, b) - std::min(a, b); } + +int distance(int a, int b) + cppverify::pre(-1000 < a && a < 1000 && -1000 < b && b < 1000) + cppverify::post(cppverify::result == spread(a, b)) +{ + return a < b ? b - a : a - b; +} +// CHECK-DAG: Verified: spec axiom: spread +// CHECK-DAG: Verified: distance [backend=z3] + +// A reference to the result is not a value: it fails closed. +int bound(int a, int b) + cppverify::post(true) +{ + const int &r = std::max(a, b); + return r; +} +// CHECK-DAG: error: bound: local references require a supported direct lvalue + +// Of a class, std::max compares with the class's own operator<, which the +// model does not know. +struct Version { + int v; + constexpr bool operator<(const Version &o) const { return v < o.v; } +}; + +int newer(Version a, Version b) + cppverify::post(cppverify::result == std::max(a, b).v) +{ + return a.v < b.v ? b.v : a.v; +} +// CHECK-DAG: error: newer: std::max is not modeled: of the standard library, the verifier knows std::min and std::max of two integers + +// A reference the helper writes through is no value. +constexpr int bumped(int &x) { + x = x + 1; + return x; +} + +int bumps(int x) + cppverify::post(cppverify::result == bumped(x)) +{ + return x + 1; +} +// CHECK-DAG: error: bumped: unsupported C++ type in verification: int & +// CHECK-DAG: Unresolved: bumps [reason=construct.unsupported] (relies on bumped, which uses a construct the verifier does not support) From e282fbfe4eb46668eaf1020f42d49f874afd0d83 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 21:23:20 +0530 Subject: [PATCH 60/64] docs: Describe std::min, std::max, and constexpr helpers taking const references. --- website/source/language/functions-loops.rst | 44 +++++++++++++++++++++ 1 file changed, 44 insertions(+) diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index 6137463e33..17fa5d2685 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -122,6 +122,50 @@ examined. Once a ``constexpr`` function has executable ``cppverify::pre``/``cppv clauses, it remains a modular executable function: calls must satisfy its preconditions and cannot be used as pure contract expressions. +A lifted function's parameter or result that is a reference to a ``const`` +integer stands for the value it refers to, as in ``constexpr const T +&larger(const T &a, const T &b)``. One that cannot be lifted (it reads memory +through a pointer, say) is reported, and a function that applies it is +``Unresolved`` with reason ``construct.unsupported``, naming it. + +The standard library's functions are not lifted: each library writes them +its own way, and a proof would depend on which one. ``std::min`` and +``std::max`` of two integers, enumerations, or ``bool`` mean what the +standard says they mean, in contracts and in code alike: ``std::max(a, b)`` +is ``a`` unless ``a < b``, and ``std::min(a, b)`` is ``a`` unless ``b < a``. + +.. code-block:: cpp + + #include + + int lower(int a, int b) + cv::post(cv::result == std::min(a, b)) + cv::post(cv::result <= a && cv::result <= b) + { + int m = std::min(a, b); + return m; + } + + long widened(int x) + cv::post(cv::result >= 3) + { + long w = std::max(x, 3L); + return w; + } + +.. code-block:: text + + Verified: lower [backend=z3] + Verified: widened [backend=z3] + +Any other function of the standard library, such as ``std::clamp``, is an +error naming it (``std::clamp is not modeled: of the standard library, the +verifier knows std::min and std::max of two integers``), as is a reference +bound to the result of ``std::max``. Before 0.2, ``std::min`` and +``std::max`` in a contract, and every ``constexpr`` helper that could not be +lifted, ended ``Unresolved: obligation lowering failed: f (missing spec +definition: fn_...)``. + Preconditions, ``cppverify::old(parameter)``, and a parameter named in a postcondition all denote the argument's entry value, as in ACSL, even when the callee reassigns its by-value parameter; a caller can therefore use the From ba389c8d768cf1bb74e055dc95ba03460fc45d55 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 21:23:20 +0530 Subject: [PATCH 61/64] docs: List std::min and std::max as the standard library's modeled functions. --- website/source/language/limitations.rst | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 9c20cfa4a4..27e2b0a022 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -630,9 +630,11 @@ allocation from an archive. Libraries and real programs --------------------------- -CppVerify does not yet ship comprehensive libc or C++ standard-library models. -An uncontracted call fails closed; a contract is assumed only when it is -marked ``[[cppverify::trusted]]``. Contracts are not saved in precompiled +CppVerify does not yet ship comprehensive libc or C++ standard-library models: +of the standard library it knows ``std::min`` and ``std::max`` of two +integers (:doc:`functions-loops`), and any other of its functions is an +error naming it. An uncontracted call fails closed; a contract is assumed +only when it is marked ``[[cppverify::trusted]]``. Contracts are not saved in precompiled headers: a function declared in a PCH has no contract for the verifier, so a contracted function that calls it fails closed (``call to function without a verification contract``). From c6cb9f0f9f9d47ddfa357dfd2716a40e32469954 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 21:23:21 +0530 Subject: [PATCH 62/64] docs: Note std::min and std::max in the release notes. --- website/source/release-notes.rst | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 9ba26d6df8..6602abb06b 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -348,6 +348,15 @@ that nothing instantiates is reported. ``cv::post(cv::result > 0)`` and ``cv::ol of a template's type did not compile (``invalid operands to binary expression ('T' and 'int')``) (:doc:`language/functions-loops`). +**std::min and std::max.** In a contract they ended ``Unresolved: +obligation lowering failed: f (missing spec definition: fn_...)``, as did +any function using a ``constexpr`` helper that could not be lifted. Of two +integers they now mean what the standard says, whatever the library, in +contracts and in code; any other function of the standard library is an +error naming it, a helper that cannot be lifted is named in the verdicts +that rely on it, and a lifted helper's references to ``const`` integers +stand for their values (:doc:`language/functions-loops`). + **Member operators.** For a member ``operator==``, ``a == b`` passed ``a`` for the operator's parameter and ``b`` as an argument beyond it, an error, and an operator returning ``*this`` by reference (``Money &operator+=``) was From 5742b1db94f58a756f9f63f1b146a9929bd3b0c7 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 21:23:21 +0530 Subject: [PATCH 63/64] docs: Design the std::min and std::max model and value references in lifted specs. --- docs/DESIGN.md | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index f89aa16d0b..5993fcef51 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -745,6 +745,22 @@ exact, while `int x = s[0];` must show that the element fits in an `int`. This is genuinely a CppVerify advantage over Verus — Verus forces users to maintain two separate bodies; we let one body do double duty *or* let users opt into a clean math-integer spec. +A lifted function's reference to a `const` integer, as a parameter or the +result, stands for the value it refers to, which it only reads: `constexpr +const T &larger(const T &a, const T &b)` is a spec of two values. One that +cannot be lifted (it reads memory through a pointer, or its type is not +supported) is kept as a declaration that uses an unsupported construct, so +the verdicts that rely on it are `Unresolved` with `construct.unsupported` +and name it. + +The standard library's functions are not lifted, since each library writes +them its own way and a verdict would depend on which one. `std::min` and +`std::max` of two integers, enumerations, or `bool` are modeled as the +standard defines them ([alg.min.max]): `max(a, b)` is `a < b ? b : a` and +`min(a, b)` is `b < a ? b : a`, read once each, in contracts and in code. +Any other function of the standard library that is not a constant is an +error naming it. + **Compile-time partial evaluation:** When a contract contains a `constexpr` call whose arguments are all constants, Clang evaluates it at compile time before the verifier sees it. A callee precondition instantiated at a call site is not such a call: there the argument is substituted for the parameter, and the solver settles the application from the lifted definition: From 8f315d27f4dfb6f78c264f47ee2e48ecd9528b35 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 21:23:21 +0530 Subject: [PATCH 64/64] docs: Describe the std::min and std::max model and unlifted helpers. --- docs/ARCHITECTURE.md | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 496b8b0b85..e94bd2e29b 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -358,6 +358,19 @@ collected from its template only); `isInstantiated` decides the warning, from a function template's specializations or the instantiated members of the class's. +**std::min and std::max:** `stdMinOrMax` recognizes the two-argument +`std::min` and `std::max` of a const integer, enumeration, or `bool` +reference (not the overloads with a comparison or an initializer list), and +`convertMinOrMax` lowers a call to a `VConditionalExpr` over the converted +arguments, before a call becomes a spec application; any other non-constant +call of a `constexpr` function of `std` is a conversion error. In +`convertConstexprSpec`, `findUnsupportedType`'s +`ConstScalarReferencesAreValues` makes a reference to a const integer its +referent (`constScalarReferent`), as the parameter's and the result's +types, and the parameters in `ValueReferences` are read as values; a +function that cannot be lifted returns a placeholder that the lifting loop +marks unsupported, so `SpecDependencies` name it. + **Records in memory by value:** `recordFieldsInMemory` reads a record value kept in memory, a promoted local or one in a pointee or record reference (`promotedRootLocal`, `inPointeeObject`), through implicit copies and