Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
69 commits
Select commit Hold shift + click to select a range
b58968c
verify: Declare the object a class invariant is instantiated for.
SwayamInSync Oct 24, 2026
23288e0
verify: Call a member operator on its first operand, return a member'…
SwayamInSync Oct 24, 2026
c0c0688
verify: Let a callee lent a local object have local objects of its own.
SwayamInSync Oct 24, 2026
8fc95d0
test: Check member operators and the invariants of objects passed by …
SwayamInSync Oct 24, 2026
3b5d6a1
test: Check a null pointer argument and an extent through a reference…
SwayamInSync Oct 24, 2026
dcb9c9f
test: Expect a record's invariant to hold through a reference.
SwayamInSync Oct 24, 2026
2e04499
verify: Declare the check that rejects using the reference a member r…
SwayamInSync Oct 24, 2026
19d1182
verify: Reject a copy or assignment from the reference a member retur…
SwayamInSync Oct 24, 2026
1ff05af
test: Check copying and assigning the reference a member operator ret…
SwayamInSync Oct 24, 2026
1b7dd64
docs: Describe member operators and the class invariants of objects p…
SwayamInSync Oct 24, 2026
010fc0c
docs: Note member operators and class invariants at reference and poi…
SwayamInSync Oct 24, 2026
4380589
docs: Design member operators, own-object returns, and type invariant…
SwayamInSync Oct 24, 2026
1aefeef
docs: Describe how member operators and the invariants of parameters …
SwayamInSync Oct 24, 2026
0632d6c
verify: Give cppverify::result, cppverify::old, and quantifiers the d…
SwayamInSync Oct 24, 2026
6e3a800
verify: Declare contract instantiation for template specializations a…
SwayamInSync Oct 24, 2026
6af1d1e
verify: Check a decreases component and a quantifier's bounds and bod…
SwayamInSync Oct 24, 2026
c1382bc
verify: Keep a function template's contract and check its clauses thr…
SwayamInSync Oct 24, 2026
7c37848
verify: Transform contract clauses with the parser's checks, loop con…
SwayamInSync Oct 24, 2026
eb77fe2
verify: Substitute template arguments into a function contract.
SwayamInSync Oct 24, 2026
36c3cf8
verify: Instantiate a specialization's contract with its definition, …
SwayamInSync Oct 24, 2026
69eb19c
verify: Instantiate a specialization's contract where it is used.
SwayamInSync Oct 24, 2026
96dbdeb
verify: Record where each template specialization is instantiated.
SwayamInSync Oct 24, 2026
c0aee24
verify: Verify each instantiated specialization of a function templat…
SwayamInSync Oct 24, 2026
246d2b4
verify: Note where a specialization is instantiated after its errors …
SwayamInSync Oct 24, 2026
cca2982
test: Check function templates verified in each specialization.
SwayamInSync Oct 24, 2026
694cb56
test: Check that a function template's contract is checked where it i…
SwayamInSync Oct 24, 2026
0a34abb
test: Expect function template contracts kept, and result and old of …
SwayamInSync Oct 24, 2026
9f4a732
test: Expect a warning for a contracted template that nothing instant…
SwayamInSync Oct 24, 2026
fa8f944
test: Expect the warning for an uninstantiated contracted template.
SwayamInSync Oct 24, 2026
83bbad9
docs: Describe function templates verified in each specialization.
SwayamInSync Oct 24, 2026
2fd37fe
docs: List function templates as supported and class template members…
SwayamInSync Oct 24, 2026
af8645d
docs: Note function templates in the release notes.
SwayamInSync Oct 24, 2026
e39b949
docs: Design function templates verified per instantiation.
SwayamInSync Oct 24, 2026
4551563
docs: Describe contract instantiation and the converter's specializat…
SwayamInSync Oct 24, 2026
ac5f112
test: Check a constexpr template lifted as a spec in each specializat…
SwayamInSync Oct 24, 2026
4c52295
docs: Note that a constexpr template in a contract is a spec in each …
SwayamInSync Oct 24, 2026
22c3329
verify: Give each instantiated quantifier and choice a scope of its o…
SwayamInSync Oct 24, 2026
d890301
verify: Keep a check-by block in the scope of its instantiated quanti…
SwayamInSync Oct 24, 2026
d27059d
verify: Drop the this scope and ghost mark a specialization's context…
SwayamInSync Oct 24, 2026
24a3d15
verify: Declare the naming of parameters, a pack's elements apart.
SwayamInSync Oct 24, 2026
fce5a9f
verify: Name the parameters a pack expands to as C++26 indexes them.
SwayamInSync Oct 24, 2026
4138ee0
test: Check a contract on a definition after a declaration, and varia…
SwayamInSync Oct 24, 2026
3693656
test: Check that instantiating a contract leaves a caller its tempora…
SwayamInSync Oct 24, 2026
5ee709d
docs: Describe binder scopes and pack element names in function templ…
SwayamInSync Oct 24, 2026
c91908e
docs: Describe variadic templates.
SwayamInSync Oct 24, 2026
1722556
verify: Map a contract's parameters through the pattern's, which stan…
SwayamInSync Oct 24, 2026
f653fb6
docs: Describe how a contract's parameters are mapped in a specializa…
SwayamInSync Oct 24, 2026
47516c5
test: Pass the temporary by value, which is one before the call is re…
SwayamInSync Oct 24, 2026
348bd89
verify: Keep a class template's members' contracts, loop contracts, a…
SwayamInSync Oct 24, 2026
e643048
verify: Remove the warning that template contracts are ignored.
SwayamInSync Oct 24, 2026
cbbf08e
verify: Keep the contract-unsupported group for builds that name it.
SwayamInSync Oct 24, 2026
5aaa43a
verify: Write a field a type invariant names bare as this->field, whi…
SwayamInSync Oct 24, 2026
126dba1
verify: Instantiate a class template's type invariants with each spec…
SwayamInSync Oct 24, 2026
fac54c0
verify: Verify the members of each instantiated class template specia…
SwayamInSync Oct 24, 2026
f8072f8
test: Check class templates verified in each specialization.
SwayamInSync Oct 24, 2026
acb14a1
test: Check that a class template's invariant and members' contracts …
SwayamInSync Oct 24, 2026
293a022
test: Expect class template contracts kept without a warning.
SwayamInSync Oct 24, 2026
0b214a1
docs: Describe class templates verified in each specialization.
SwayamInSync Oct 24, 2026
6d381a2
docs: Point the templates section to class templates.
SwayamInSync Oct 24, 2026
1723524
docs: List class templates as supported.
SwayamInSync Oct 24, 2026
48b82cd
docs: Note class templates in the templates release note.
SwayamInSync Oct 24, 2026
341378f
docs: Design class templates verified per specialization.
SwayamInSync Oct 24, 2026
f18d6a4
docs: Describe how class templates are instantiated and collected.
SwayamInSync Oct 24, 2026
73ae869
verify: Declare a quantifier binder's context, and drop the type inva…
SwayamInSync Oct 24, 2026
90d60bb
verify: Declare a binder outside a class, and drop the field rewriter…
SwayamInSync Oct 24, 2026
8ebd638
verify: Declare a binder in its context, and check a type invariant a…
SwayamInSync Oct 24, 2026
bc7c72e
verify: Rebuild a binder in the binder context.
SwayamInSync Oct 24, 2026
22bda73
test: Check quantified invariants, and an explicit instantiation's me…
SwayamInSync Oct 24, 2026
5c7a8e7
docs: Describe an invariant's this and a binder's context.
SwayamInSync Oct 24, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 20 additions & 5 deletions clang/include/clang/AST/ExprContract.h
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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) {}
Expand Down Expand Up @@ -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) {}
Expand Down Expand Up @@ -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) {}
Expand Down Expand Up @@ -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) {}
Expand Down Expand Up @@ -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) {}
Expand Down
2 changes: 2 additions & 0 deletions clang/include/clang/Basic/DiagnosticGroups.td
Original file line number Diff line number Diff line change
Expand Up @@ -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">;
Expand Down
4 changes: 0 additions & 4 deletions clang/include/clang/Basic/DiagnosticParseKinds.td
Original file line number Diff line number Diff line change
Expand Up @@ -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<ContractUnsupported>;

} // end of Parser diagnostics
32 changes: 30 additions & 2 deletions clang/include/clang/Sema/Sema.h
Original file line number Diff line number Diff line change
Expand Up @@ -10394,8 +10394,22 @@ class Sema final : public SemaBase {
ExprResult ActOnContractRange(Expr *Base, Expr *Lower, SourceLocation ColonLoc,
Expr *Length, SourceLocation RBLoc);

/// Rewrite unqualified field names to this->field for type_invariant(expr).
ExprResult ActOnTypeInvariantExpr(ExprResult E, CXXRecordDecl *Record);
/// 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,
SourceLocation KeywordLoc,
SourceLocation LParenLoc,
SourceLocation RParenLoc, VarDecl *Binder,
Expr *Lo, Expr *Hi, Expr *Body);


/// Diagnose references to spec functions in executable code of \p FD
/// (or in a global initializer when \p FD is null). Spec functions are
Expand Down Expand Up @@ -14336,6 +14350,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.
///
Expand Down
84 changes: 20 additions & 64 deletions clang/lib/Parse/ParseCppVerify.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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();
Expand Down Expand Up @@ -673,19 +672,8 @@ 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;
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);
Expand Down Expand Up @@ -835,17 +823,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;
Expand All @@ -867,12 +851,6 @@ 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()) {
Diag(Loop.get()->getBeginLoc(), diag::warn_contract_template_unsupported)
<< 0 << FD;
return;
}
Actions.getASTContext().getOrCreateLoopContract(Loop.get()) =
std::move(Contract);
}
Expand All @@ -883,7 +861,6 @@ void Parser::ParseTypeInvariant(Decl *TagDecl) {
auto *RD = dyn_cast_or_null<CXXRecordDecl>(TagDecl);
if (auto *Template = dyn_cast_or_null<ClassTemplateDecl>(TagDecl))
RD = Template->getTemplatedDecl();
const SourceLocation InvariantLoc = Tok.getLocation();
ConsumeCppVerify();
auto Finish = [&] {
takePendingReferences(Actions.getASTContext(), RD,
Expand Down Expand Up @@ -919,10 +896,10 @@ 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()) {
E = Actions.ActOnTypeInvariantExpr(E, RD);
// 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.ActOnContractCondition(E);
if (!E.isInvalid())
Actions.getASTContext().getOrCreateTypeContract(RD).Invariants.push_back(
E.get());
Expand Down Expand Up @@ -1366,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;
Expand All @@ -1379,40 +1356,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)
Expand Down
80 changes: 42 additions & 38 deletions clang/lib/Sema/SemaContract.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,6 @@
//
//===----------------------------------------------------------------------===//

#include "TreeTransform.h"
#include "clang/AST/ASTContext.h"
#include "clang/AST/ASTLambda.h"
#include "clang/AST/DeclCXX.h"
Expand All @@ -27,36 +26,6 @@ using namespace clang;

namespace {

class TypeInvariantFieldRewriter : public TreeTransform<TypeInvariantFieldRewriter> {
typedef TreeTransform<TypeInvariantFieldRewriter> Base;
CXXRecordDecl *Record;

public:
TypeInvariantFieldRewriter(Sema &S, CXXRecordDecl *RD)
: Base(S), Record(RD) {}

ExprResult TransformDeclRefExpr(DeclRefExpr *E) {
if (FieldDecl *FD = dyn_cast<FieldDecl>(E->getDecl())) {
if (FD->getParent() == Record) {
SourceLocation Loc = E->getBeginLoc();
QualType ThisTy =
getSema().Context.getTypeDeclType(cast<TypeDecl>(Record));
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(),
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())
Expand Down Expand Up @@ -309,12 +278,47 @@ ExprResult Sema::ActOnContractRange(Expr *Base, Expr *Lower,
OK_Ordinary, ColonLoc, RBLoc);
}

ExprResult Sema::ActOnTypeInvariantExpr(ExprResult E, CXXRecordDecl *Record) {
if (E.isInvalid() || !Record)
ExprResult Sema::ActOnContractMeasure(ExprResult E) {
if (E.isInvalid() || E.get()->isTypeDependent() ||
E.get()->getType()->isIntegerType())
return E;
TypeInvariantFieldRewriter Rewriter(*this, Record);
ExprResult Transformed = Rewriter.TransformExpr(E.get());
if (Transformed.isInvalid())
return Transformed;
return ActOnContractCondition(Transformed.get());
Diag(E.get()->getExprLoc(), diag::err_contract_decreases_not_int);
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,
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);
}
}
6 changes: 6 additions & 0 deletions clang/lib/Sema/SemaExpr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
Loading
Loading