SwayamInSync · Oct 24, 2026 · Oct 24, 2026 · Oct 24, 2026 · Oct 24, 2026 · Oct 24, 2026
diff --git 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) {}

diff --git 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.
   ///

diff --git 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<CXXMethodDecl>(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<CXXMethodDecl>(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<CXXMethodDecl>(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,40 +1372,19 @@ 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);
     return ExprError();
   }
   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)

diff --git 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;

diff --git 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.

diff --git 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.
@@ -4493,6 +4508,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) {

diff --git a/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp b/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp
@@ -5436,6 +5436,50 @@ 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;
+
+  // 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);
+  // 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))
+    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 +5810,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())