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) {} 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">; 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 diff --git a/clang/include/clang/Sema/Sema.h b/clang/include/clang/Sema/Sema.h index b74f1bd3f7..c889d2bcc3 100644 --- a/clang/include/clang/Sema/Sema.h +++ b/clang/include/clang/Sema/Sema.h @@ -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 @@ -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. /// diff --git a/clang/lib/Parse/ParseCppVerify.cpp b/clang/lib/Parse/ParseCppVerify.cpp index 8c5d38537e..39f8952d0c 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,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(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); @@ -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; @@ -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); } @@ -883,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, @@ -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()); @@ -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; @@ -1379,23 +1356,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 +1363,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) diff --git a/clang/lib/Sema/SemaContract.cpp b/clang/lib/Sema/SemaContract.cpp index 8eef44eae8..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,36 +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) { - SourceLocation Loc = E->getBeginLoc(); - QualType ThisTy = - getSema().Context.getTypeDeclType(cast(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()) @@ -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); + } } 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. diff --git a/clang/lib/Sema/SemaTemplateInstantiate.cpp b/clang/lib/Sema/SemaTemplateInstantiate.cpp index bad0cdd1b7..0cbc2687c1 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. @@ -3764,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) { @@ -4493,6 +4523,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 index c2e90624b8..9e9668b2fb 100644 --- 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()) diff --git a/clang/lib/Sema/TreeTransform.h b/clang/lib/Sema/TreeTransform.h index 78122a51e5..5e33617c37 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,16 +18376,23 @@ 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(); 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(); @@ -18400,16 +18457,156 @@ 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}); 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 +18622,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 +18643,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 +18664,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 +18683,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 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"; + } } } }; diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index b55daccea6..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,39 @@ 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, + 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 {}; @@ -1125,6 +1174,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()) @@ -1137,6 +1213,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, @@ -1985,7 +2064,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; @@ -1994,6 +2093,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)) { @@ -2008,6 +2118,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 @@ -2154,23 +2303,61 @@ 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 template is verified in each of its specializations, which follow + // it: what it means depends on its arguments. + if (!UnsupportedMember) { + // 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()) && + isInstantiated(FD, Ctx) == false) + Warnings.emplace_back( + FD->getLocation(), + 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; } - 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 +2390,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 +2990,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 +3147,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); @@ -2974,34 +3161,23 @@ 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(FD->getNameAsString() + ": contract declaration parameter mismatch"); + 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(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 +3185,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 +3203,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; @@ -3792,39 +3968,76 @@ 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)); - 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(); - if (exceedsNestingLimit(FD, functionContract(FD)) || - hasIndirectMemoryAccess(FD)) - return nullptr; + nameParameters(FD, FD); if (!FD->isConstexpr() || !FD->hasBody()) return nullptr; - if (FD->getReturnType()->isRecordType()) { - error(FD->getNameAsString() + - ": aggregate-returning constexpr specs are unsupported"); - return nullptr; - } - if (auto Unsupported = findUnsupportedType(FD, false)) { - error(FD->getNameAsString() + - ": 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 = FD->getNameAsString(); + Fn->Name = functionName(FD); Fn->Identity = functionIdentity(FD); Fn->IsSpec = true; 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()) @@ -3833,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); } @@ -3850,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; } @@ -5501,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"); @@ -5976,13 +6194,24 @@ 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); 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 +6253,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 +6341,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 +6907,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 +7459,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 +7856,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 +8081,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 +8116,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 +8142,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 +8296,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 +8451,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 +8504,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) { diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index 677e548557..b56211f6ef 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -71,7 +71,17 @@ class ASTConverter { /// Binders of a forall being introduced by contract_assert(...) by. std::set ArbitraryValues; std::map> UnverifiedCallers; + 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 + /// whose contract names them. + void nameParameters(const FunctionDecl *ContractDecl, const FunctionDecl *FD); unsigned BoundValueId = 0; std::map FunctionIdentities; std::map SpecHeapReads; @@ -130,6 +140,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 @@ -170,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); diff --git a/clang/test/Verify/suite/class_templates.cpp b/clang/test/Verify/suite/class_templates.cpp new file mode 100644 index 0000000000..63be7ecb10 --- /dev/null +++ b/clang/test/Verify/suite/class_templates.cpp @@ -0,0 +1,220 @@ +// 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 +// 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 +// 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] +// ONCE: 1 + +// 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] + +// 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] diff --git a/clang/test/Verify/suite/function_templates.cpp b/clang/test/Verify/suite/function_templates.cpp new file mode 100644 index 0000000000..48606a2948 --- /dev/null +++ b/clang/test/Verify/suite/function_templates.cpp @@ -0,0 +1,420 @@ +// 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, a ghost variable assigned in a ghost +// block. +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 + +// 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 + +// 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] = 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) 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 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 diff --git a/clang/test/Verify/template_contract_errors.cpp b/clang/test/Verify/template_contract_errors.cpp new file mode 100644 index 0000000000..15c4f356eb --- /dev/null +++ b/clang/test/Verify/template_contract_errors.cpp @@ -0,0 +1,133 @@ +// 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}} +} + +// 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) + 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)); diff --git a/clang/test/Verify/template_contracts.cpp b/clang/test/Verify/template_contracts.cpp index 4f0da96225..5dab094563 100644 --- a/clang/test/Verify/template_contracts.cpp +++ b/clang/test/Verify/template_contracts.cpp @@ -1,13 +1,16 @@ // 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. 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, and a class template's members' +// contracts and type invariants with the class. 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 +18,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 +32,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) @@ -39,15 +42,45 @@ void fill(T *p, T n, T v) // expected-warning {{contracts in function template ' 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; } }; +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; +} + +// A contract instantiated while a caller's full expression is built leaves +// 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) {} + ~Noisy(); +}; + +template +int value_of(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) { @@ -78,7 +111,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 +119,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_( diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 3f53be5716..e94bd2e29b 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -308,6 +308,69 @@ 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 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 +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`). + +**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`. 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. + +**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 diff --git a/docs/DESIGN.md b/docs/DESIGN.md index b4b092e8de..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: @@ -1311,8 +1327,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 @@ -1817,6 +1833,34 @@ 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. +- 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 ### Construct recognition @@ -1927,6 +1971,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 diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index 1c585c9cd4..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 @@ -221,50 +265,93 @@ 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. 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. +- 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. +- 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 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, 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 +(``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 diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 62b31833b3..27e2b0a022 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 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 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 + 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. * - Storage @@ -213,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 -------------------------- @@ -628,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``). 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 -------------- diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index e4c6efbc04..6602abb06b 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,6 +336,27 @@ 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`). +**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`). + +**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