From b58968c4a611438f50cd7c90caefda4065a30151 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 17:31:29 +0530 Subject: [PATCH 01/48] verify: Declare the object a class invariant is instantiated for. --- clang/lib/Verify/Frontend/ASTConverter.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index ba82b77b06..b58c784f4d 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -92,6 +92,9 @@ class ASTConverter { /// Converting a clause where an extent marker states nothing (a class /// invariant at exit): each marker is true. bool DropExtentMarkers = false; + /// The object `this` stands for while a class invariant is instantiated + /// for a parameter: the pointer or reference that addresses it. + const VExpr *ThisSubstitute = nullptr; std::set GhostLocals; unsigned DynamicProvenanceId = 0; unsigned DynamicPointerAssignmentId = 0; From 23288e0f0b661ac8fad273ef80674c157a93eee4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 17:31:30 +0530 Subject: [PATCH 02/48] verify: Call a member operator on its first operand, return a member's own object as nothing, and hold class invariants at reference and pointer parameters. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 157 +++++++++++++++++++-- 1 file changed, 148 insertions(+), 9 deletions(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index 2b2c997140..c2f17f2e7a 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -642,6 +642,39 @@ static bool isSupportedRecordLValueReference(QualType Ty, ASTContext &Ctx) { Ctx.getPointerType(Ty.getNonReferenceType())); } +static bool isOwnObject(const Expr *E) { + const auto *U = + E ? dyn_cast(E->IgnoreParenImpCasts()) : nullptr; + return U && U->getOpcode() == UO_Deref && + isa(U->getSubExpr()->IgnoreParenImpCasts()); +} + +/// A member function that returns a reference to its own object, every +/// return being `return *this;` (as an assignment operator's is): the +/// reference says nothing the caller does not hold, so it returns nothing. +static bool returnsOwnObject(const FunctionDecl *FD) { + const auto *Method = dyn_cast(FD); + if (!Method || !Method->isInstance() || !FD->hasBody() || + !FD->getReturnType()->isLValueReferenceType()) + return false; + const ASTContext &Ctx = FD->getASTContext(); + if (!Ctx.hasSameUnqualifiedType(FD->getReturnType().getNonReferenceType(), + Method->getFunctionObjectParameterType())) + return false; + struct Returns : RecursiveASTVisitor { + bool Any = false; + bool All = true; + bool TraverseLambdaExpr(LambdaExpr *) { return true; } + bool VisitReturnStmt(ReturnStmt *R) { + Any = true; + All = All && isOwnObject(R->getRetValue()); + return true; + } + } Finder; + Finder.TraverseStmt(const_cast(FD->getBody())); + return Finder.Any && Finder.All; +} + static std::optional findUnsupportedType(const FunctionDecl *FD, bool AllowScalarReferences) { // By-value records keep their flattened SSA representation, so only records @@ -652,7 +685,7 @@ findUnsupportedType(const FunctionDecl *FD, bool AllowScalarReferences) { return Ty->isRecordType() && !isFlatScalarRecordType(Ty) && !VType::collectionKind(Ty); }; - if (UnsupportedValueType(FD->getReturnType())) + if (UnsupportedValueType(FD->getReturnType()) && !returnsOwnObject(FD)) return FD->getReturnType().getAsString(); for (const ParmVarDecl *Param : FD->parameters()) { QualType Ty = Param->getType(); @@ -2029,6 +2062,28 @@ unsupportedConstructor(const CXXConstructorDecl *Ctor) { return std::nullopt; } +/// Whether a precondition gives the parameter an extent, valid(P, n). +static bool hasExtentMarker(const FunctionContractInfo &FCI, + const ParmVarDecl *P) { + struct Finder : RecursiveASTVisitor { + const ParmVarDecl *Parameter; + bool Found = false; + bool VisitCallExpr(CallExpr *Call) { + const FunctionDecl *Callee = Call->getDirectCallee(); + if (Callee && Callee->getDeclName().isIdentifier() && + Callee->getName() == "valid" && Call->getNumArgs() == 2) + if (const auto *Ref = + dyn_cast(Call->getArg(0)->IgnoreParenImpCasts())) + Found = Found || Ref->getDecl() == Parameter; + return !Found; + } + } F; + F.Parameter = P; + for (const Expr *Pre : FCI.Preconditions) + F.TraverseStmt(const_cast(Pre)); + return F.Found; +} + static bool mentionsThis(const Stmt *S) { if (!S) return false; @@ -2994,7 +3049,9 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { } IntMode = FCI->IsSpec ? VIntMode::Math : VIntMode::Machine; Fn->IntMode = IntMode; - Fn->ReturnType = VType::fromQualType(FD->getReturnType(), IntMode, Ctx); + Fn->ReturnType = returnsOwnObject(FD) + ? VType::makeVoid() + : VType::fromQualType(FD->getReturnType(), IntMode, Ctx); if (const RecordDecl *RD = getRecordFromType(FD->getReturnType())) if (const RecordDecl *Definition = RD->getDefinition()) for (const FieldDecl *Field : Definition->fields()) @@ -3254,6 +3311,48 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { addPostcondition(*Fn, std::move(Post), ProofObligationKind::TypeInvariant); } + // An object a parameter refers to or points to satisfies its class + // invariant on entry, as a caller shows at the call, and through a + // mutable reference or pointer at exit too: every function boundary is + // one at which the invariant holds. A pointer may be null; one with an + // extent addresses several objects, which is not covered yet. An extent + // marker in the invariant is `this`'s, so it is true here. + for (const ParmVarDecl *P : FD->parameters()) { + QualType Ty = P->getType(); + if (!Ty->isLValueReferenceType() && !Ty->isPointerType()) + continue; + QualType Object = Ty->getPointeeType(); + const RecordDecl *Record = getRecordFromType(Object); + const TypeContractInfo *TCI = + Record ? Ctx.getTypeContract(Record) : nullptr; + if (!TCI || TCI->Invariants.empty() || hasExtentMarker(*FCI, P)) + continue; + VVarExpr Pointer(valueName(P), VType::makePtr(), P->getLocation()); + llvm::SaveAndRestore Substitute(ThisSubstitute, &Pointer); + llvm::SaveAndRestore DropMarkers(DropExtentMarkers, true); + FieldSubstPrefix.clear(); + auto Guarded = [&](std::unique_ptr Invariant) { + if (!Ty->isPointerType()) + return Invariant; + return std::unique_ptr(std::make_unique( + VBinOp::Or, + std::make_unique( + VBinOp::Eq, cloneVExpr(&Pointer), + std::make_unique(0, VType::makePtr(), + P->getLocation()), + VType::makeBool(), P->getLocation()), + std::move(Invariant), VType::makeBool(), P->getLocation())); + }; + for (const Expr *Invariant : TCI->Invariants) { + if (auto Pre = convertTypeInvariantExpr(Invariant)) + addPrecondition(*Fn, Guarded(std::move(Pre)), + ProofObligationKind::TypeInvariant); + if (!Object.isConstQualified()) + if (auto Post = convertTypeInvariantExpr(Invariant)) + addPostcondition(*Fn, Guarded(std::move(Post)), + ProofObligationKind::TypeInvariant); + } + } for (const ParmVarDecl *P : AddressParams) { auto Pointer = std::make_unique(valueName(P), VType::makePtr(), SourceLocation()); @@ -4561,7 +4660,7 @@ std::unique_ptr ASTConverter::convertExpr(const Expr *E) { E->getExprLoc()); } // An extent marker's pointer field is its entry value's parameter. - if (E && !FieldExtentParameters.empty()) + if (E && !FieldExtentParameters.empty() && !ThisSubstitute) if (auto It = FieldExtentParameters.find(E->IgnoreParenImpCasts()); It != FieldExtentParameters.end()) return std::make_unique( @@ -5225,6 +5324,8 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { return convertExpr(MTE->getSubExpr()); // `this`, the parameter of a member function's object. if (isa(E)) { + if (ThisSubstitute) + return cloneVExpr(ThisSubstitute); if (!CurrentFn || CurrentFn->Params.empty() || CurrentFn->Params.front().first != "this") { error(CurrentFn ? CurrentFn->Name + ": unsupported use of this" @@ -6105,6 +6206,16 @@ void ASTConverter::convertExecCallArgs( return false; }; + // The reference a member function returns to its own object is no value. + for (const Expr *A : CE->arguments()) + if (const auto *Nested = dyn_cast(A->IgnoreParenImpCasts()); + Nested && Nested->getDirectCallee() && + returnsOwnObject(Nested->getDirectCallee())) { + error(CurrentFn->Name + ": the reference " + + Nested->getDirectCallee()->getNameAsString() + + " returns is not used yet; call it as a statement of its own"); + return; + } for (unsigned I = 0; I < CE->getNumArgs(); ++I) { if (!IsModifyingCall(CE->getArg(I))) continue; @@ -6119,11 +6230,21 @@ void ASTConverter::convertExecCallArgs( // A member call passes its object first, as the callee's `this`: the // object a pointer addresses (p->m(), this->m()), or the object itself, - // bound as a reference argument is (obj.m()). + // bound as a reference argument is (obj.m()). A member operator's object + // is its first operand (a == b is a.operator==(b)). + const Expr *Object = nullptr; + unsigned FirstArgument = 0; if (const auto *Member = dyn_cast(CE); Member && Member->getMethodDecl() && - Member->getMethodDecl()->isInstance()) { - const Expr *Object = Member->getImplicitObjectArgument(); + Member->getMethodDecl()->isInstance()) + Object = Member->getImplicitObjectArgument(); + else if (const auto *Method = dyn_cast_or_null(Callee); + Method && Method->isInstance() && isa(CE) && + CE->getNumArgs() > 0) { + Object = CE->getArg(0); + FirstArgument = 1; + } + if (Object) { std::unique_ptr This; if (Object->getType()->isPointerType()) { This = convertExpr(Object); @@ -6150,8 +6271,9 @@ void ASTConverter::convertExecCallArgs( Args.push_back(std::move(This)); } - unsigned ArgIndex = 0; - for (const Expr *A : CE->arguments()) { + for (unsigned I = FirstArgument; I < CE->getNumArgs(); ++I) { + const Expr *A = CE->getArg(I); + const unsigned ArgIndex = I - FirstArgument; const ParmVarDecl *Formal = Callee && ArgIndex < Callee->getNumParams() ? Callee->getParamDecl(ArgIndex) : nullptr; @@ -6163,7 +6285,6 @@ void ASTConverter::convertExecCallArgs( if (Arg) Args.push_back(std::move(Arg)); } - ++ArgIndex; } } @@ -6554,6 +6675,17 @@ bool ASTConverter::appendRecordCopy(const Expr *Source, const VarDecl *Target, std::vector> &Out) { if (!Source || !Target) return false; + if (const CXXConstructExpr *Copy = constructionOf(Source); + Copy && Copy->getNumArgs() == 1) + if (const auto *Call = + dyn_cast(Copy->getArg(0)->IgnoreParenImpCasts()); + Call && Call->getDirectCallee() && + returnsOwnObject(Call->getDirectCallee())) { + error(CurrentFn->Name + ": the reference " + + Call->getDirectCallee()->getNameAsString() + + " returns is not used yet; call it as a statement of its own"); + return true; + } Source = Source->IgnoreParenImpCasts(); if (const auto *Construct = dyn_cast(Source)) { if (Construct->getNumArgs() != 1 || @@ -7064,6 +7196,13 @@ ASTConverter::convertStmtBody(const Stmt *S) { return Out; } const auto *RS = cast(S); + // A member function that returns its own object returns nothing. + if (CurrentFn->ReturnType.Kind == VTypeKind::Void && + isOwnObject(RS->getRetValue())) { + appendReturn(nullptr, Out, RS->getBeginLoc()); + InitializationPathReachable = false; + return Out; + } if (const Expr *RetE = RS->getRetValue()) { emitReturnInvariantAssert(RetE, Out, RS->getBeginLoc()); const auto *CE = dyn_cast(RetE->IgnoreParenImpCasts()); From c0c06887417324ad7c7c729959457a57fb1f08c5 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 17:31:30 +0530 Subject: [PATCH 03/48] verify: Let a callee lent a local object have local objects of its own. --- clang/lib/Verify/Transform/Passivize.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp index 659e59d04d..04e9f786b3 100644 --- a/clang/lib/Verify/Transform/Passivize.cpp +++ b/clang/lib/Verify/Transform/Passivize.cpp @@ -1554,10 +1554,14 @@ recordStmtSafe(const VStmt &S, const std::set &Aliases, case VStmt::Store: return !pointerFromAliases(static_cast(S).Value.get(), Aliases); - case VStmt::Allocate: - case VStmt::Free: - // A function that allocates or frees is UsesDynamicStorage, which + case VStmt::Allocate: { + // A local object of the callee's own keeps no address unless it is + // initialized with one; one from new makes it UsesDynamicStorage, which // keepsNoAddress rejects before it looks at a statement. + const auto &A = static_cast(S); + return A.IsAutomatic && !pointerFromAliases(A.Initializer.get(), Aliases); + } + case VStmt::Free: return false; case VStmt::If: { const auto &I = static_cast(S); From 8fc95d088cf9b9f1ce04fb83e77358ac820fe7c3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 17:31:31 +0530 Subject: [PATCH 04/48] test: Check member operators and the invariants of objects passed by reference. --- clang/test/Verify/suite/member_operators.cpp | 197 +++++++++++++++++++ 1 file changed, 197 insertions(+) create mode 100644 clang/test/Verify/suite/member_operators.cpp diff --git a/clang/test/Verify/suite/member_operators.cpp b/clang/test/Verify/suite/member_operators.cpp new file mode 100644 index 0000000000..17ae077d4a --- /dev/null +++ b/clang/test/Verify/suite/member_operators.cpp @@ -0,0 +1,197 @@ +// RUN: not %cpp-verify --jobs=1 %s -- > %t 2>&1 +// RUN: FileCheck %s < %t +// RUN: FileCheck %s --check-prefix=SOUND < %t +// +// A member operator is a member function: `a == b` is `a.operator==(b)`, +// whose object is its first operand. One that returns a reference to its +// own object (`return *this;`) returns nothing a caller does not hold. +// +// No proof here holds only because no execution reaches its end. +// SOUND-NOT: vacuous + +class Bits { +public: + Bits() + cppverify::post(word == 0) + : word(0) {} + + void set(int i) + cppverify::pre(0 <= i && i < 16) + cppverify::modifies(word) + cppverify::post(word == (cppverify::old(word) | (1u << i))) + { + word = word | (1u << i); + } + + bool test(int i) const + cppverify::pre(0 <= i && i < 16) + cppverify::post(cppverify::result == (((word >> i) & 1u) != 0)) + { + return ((word >> i) & 1u) != 0; + } + + bool operator==(const Bits &o) const + cppverify::post(cppverify::result == (word == o.word)) + { + return word == o.word; + } + + Bits &operator|=(const Bits &o) + cppverify::modifies(word) + cppverify::post(word == (cppverify::old(word) | o.word)) + { + word = word | o.word; + return *this; + } + + unsigned word; + + cppverify::type_invariant(word < 65536); +}; +// CHECK-DAG: Verified: Bits::Bits [backend=z3] +// CHECK-DAG: Verified: Bits::set [backend=z3] +// CHECK-DAG: Verified: Bits::test [backend=z3] +// CHECK-DAG: Verified: Bits::operator== [backend=z3] +// CHECK-DAG: Verified: Bits::operator|= [backend=z3] + +int bits_use() + cppverify::post(cppverify::result == 1) +{ + Bits a; + Bits b; + a.set(3); + b.set(5); + bool apart = a == b; + a |= b; + b |= a; + bool together = a == b; + bool has = a.test(5); + return (!apart && together && has) ? 1 : 0; +} +// CHECK-DAG: Verified: bits_use [backend=z3] + +struct Money { + Money(int c) + cppverify::pre(0 <= c && c < 1000000) + cppverify::post(cents == c) + : cents(c) {} + + Money &operator+=(const Money &o) + cppverify::pre(0 <= o.cents && o.cents < 1000000) + cppverify::pre(0 <= cents && cents < 1000000) + cppverify::modifies(cents) + cppverify::post(cents == cppverify::old(cents) + o.cents) + { + cents = cents + o.cents; + return *this; + } + + int cents; +}; + +// A free operator is a free function, and returns its value. +Money operator+(const Money &a, const Money &b) + cppverify::pre(0 <= a.cents && a.cents < 500000) + cppverify::pre(0 <= b.cents && b.cents < 500000) + cppverify::post(cppverify::result.cents == a.cents + b.cents) +{ + Money r(a.cents + b.cents); + return r; +} +// CHECK-DAG: Verified: operator+ [backend=z3] + +int summed() + cppverify::post(cppverify::result == 22) +{ + Money a(5); + Money b(6); + Money c = a + b; + a += b; + return c.cents + a.cents; +} +// CHECK-DAG: Verified: summed [backend=z3] + +// The object and the operand are distinct objects by default. +int self_add() + cppverify::post(true) +{ + Money a(5); + a += a; + return a.cents; +} +// CHECK-DAG: error: verification failed: self_add [{{.*}}::aliasing@[[@LINE-3]] + +// The reference such an operator returns is no value yet. +int chained() + cppverify::post(true) +{ + Money a(5); + Money b(6); + (a += b) += b; + return a.cents; +} +// CHECK-DAG: error: chained: the reference operator+= returns is not used yet; call it as a statement of its own + +// An object a parameter refers to or points to satisfies its class +// invariant on entry, as the caller shows, and through a mutable reference +// or pointer it must at exit: so does every operand of an operator. +class Level { +public: + Level(int v) + cppverify::pre(0 <= v && v < 100) + cppverify::post(value == v) + : value(v) {} + + int get() const + cppverify::post(cppverify::result == value) + { + return value; + } + + int value; + + cppverify::type_invariant(0 <= value && value < 100); +}; +// CHECK-DAG: Verified: Level::Level [backend=z3] + +int read(const Level &l) + cppverify::post(0 <= cppverify::result && cppverify::result < 100) +{ + int v = l.get(); + return v; +} +// CHECK-DAG: Verified: read [backend=z3] + +int peek(const Level *p) + cppverify::post(p == nullptr || cppverify::result < 100) +{ + if (p == nullptr) + return 0; + int v = p->get(); + return v; +} +// CHECK-DAG: Verified: peek [backend=z3] + +void lower(Level &l) + cppverify::modifies(l.value) +{ + l.value = l.value / 2; +} +// CHECK-DAG: Verified: lower [backend=z3] + +void spoil(Level &l) + cppverify::modifies(l.value) +{ + l.value = 500; +} +// CHECK-DAG: error: verification failed: spoil [{{.*}}::type-invariant@ + +int spoiled_argument() + cppverify::post(true) +{ + Level l(1); + l.value = 500; + int v = read(l); + return v; +} +// CHECK-DAG: error: verification failed: spoiled_argument [{{.*}}::type-invariant@[[@LINE-3]] From 3b5d6a1985974c2b65b50f31f68960321f7901d2 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 17:32:30 +0530 Subject: [PATCH 05/48] test: Check a null pointer argument and an extent through a reference for class invariants. --- clang/test/Verify/suite/member_operators.cpp | 39 ++++++++++++++++++++ 1 file changed, 39 insertions(+) diff --git a/clang/test/Verify/suite/member_operators.cpp b/clang/test/Verify/suite/member_operators.cpp index 17ae077d4a..8b6fc001ed 100644 --- a/clang/test/Verify/suite/member_operators.cpp +++ b/clang/test/Verify/suite/member_operators.cpp @@ -195,3 +195,42 @@ int spoiled_argument() return v; } // CHECK-DAG: error: verification failed: spoiled_argument [{{.*}}::type-invariant@[[@LINE-3]] + +// A null pointer addresses no object, whose invariant would be due. +int none() + cppverify::post(true) +{ + int v = peek(nullptr); + return v; +} +// CHECK-DAG: Verified: none [backend=z3] + +// An extent in a class invariant is `this`'s: an object passed by +// reference does not carry it yet, so a member function that needs it +// cannot be called there. +class Span { +public: + Span(const int *p, int n) + cppverify::pre(cppverify::valid(p, n) && 0 < n && n < 1000) + cppverify::post(data == p && len == n) + : data(p), len(n) {} + + int first() const + cppverify::post(cppverify::result == data[0]) + { + return data[0]; + } + + const int *data; + int len; + + cppverify::type_invariant(cppverify::valid(data, len) && 0 < len && len < 1000); +}; + +int first_through(const Span &s) + cppverify::post(true) +{ + int v = s.first(); + return v; +} +// CHECK-DAG: error: verification failed: first_through [{{.*}}::bounds@[[@LINE-3]] From dcb9c9f0f690150760e04d5a83763ea53ddcbd95 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 17:32:31 +0530 Subject: [PATCH 06/48] test: Expect a record's invariant to hold through a reference. --- clang/test/Verify/suite/record_references.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/clang/test/Verify/suite/record_references.cpp b/clang/test/Verify/suite/record_references.cpp index b5b76351cf..0a4eefdf87 100644 --- a/clang/test/Verify/suite/record_references.cpp +++ b/clang/test/Verify/suite/record_references.cpp @@ -328,8 +328,8 @@ int local_object_uninitialized() } // CHECK-DAG: error: verification failed: local_object_uninitialized [{{.*}}::initialization@[[@LINE-2]]:3] -// A type invariant is a fact about records by value; one a reference names is -// an object whose fields the function reads from memory. +// A type invariant holds for a record by value and for one a reference or a +// pointer names, at every function boundary. struct Bounded { int v; cppverify::type_invariant(v >= 0); @@ -347,7 +347,7 @@ int by_reference(const Bounded &b) { return b.v; } -// CHECK-DAG: error: verification failed: by_reference [{{.*}}::postcondition@[[@LINE-4]]:37] +// CHECK-DAG: Verified: by_reference [backend=z3] // A local passed to a callee by reference is checked at the call (see // local_record_arguments.cpp). Not yet: a pointer formed from a local through From 2e04499bfacdfa944a98b505445872b4bffb41ec Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 17:56:19 +0530 Subject: [PATCH 07/48] verify: Declare the check that rejects using the reference a member returns to its own object. --- clang/lib/Verify/Frontend/ASTConverter.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index b58c784f4d..677e548557 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -324,6 +324,9 @@ class ASTConverter { bool appendRecordCopy(const Expr *Source, const VarDecl *Target, SourceLocation Loc, std::vector> &Out); + /// Reports a use of the reference a member function returns to its own + /// object, which is no value. + bool rejectOwnObjectUse(const Expr *E); bool appendRecordInitializer(const InitListExpr *Init, const VarDecl *Target, SourceLocation Loc, std::vector> &Out); From 19d11829cb17d12989fb7a30aa998fd500d70b83 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 17:56:20 +0530 Subject: [PATCH 08/48] verify: Reject a copy or assignment from the reference a member returns to its own object, as an argument is. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 44 ++++++++++++---------- 1 file changed, 25 insertions(+), 19 deletions(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index c2f17f2e7a..b55daccea6 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -675,6 +675,17 @@ static bool returnsOwnObject(const FunctionDecl *FD) { return Finder.Any && Finder.All; } +/// The member function returning its own object that E calls, read or +/// copied (`(a += b) += c`, `Bits c = (a |= b);`). +static const FunctionDecl *ownObjectCallee(const Expr *E) { + if (const CXXConstructExpr *Copy = constructionOf(E); + Copy && Copy->getNumArgs() == 1) + E = Copy->getArg(0); + const auto *Call = E ? dyn_cast(E->IgnoreParenImpCasts()) : nullptr; + const FunctionDecl *Callee = Call ? Call->getDirectCallee() : nullptr; + return Callee && returnsOwnObject(Callee) ? Callee : nullptr; +} + static std::optional findUnsupportedType(const FunctionDecl *FD, bool AllowScalarReferences) { // By-value records keep their flattened SSA representation, so only records @@ -6206,16 +6217,9 @@ void ASTConverter::convertExecCallArgs( return false; }; - // The reference a member function returns to its own object is no value. for (const Expr *A : CE->arguments()) - if (const auto *Nested = dyn_cast(A->IgnoreParenImpCasts()); - Nested && Nested->getDirectCallee() && - returnsOwnObject(Nested->getDirectCallee())) { - error(CurrentFn->Name + ": the reference " + - Nested->getDirectCallee()->getNameAsString() + - " returns is not used yet; call it as a statement of its own"); + if (rejectOwnObjectUse(A)) return; - } for (unsigned I = 0; I < CE->getNumArgs(); ++I) { if (!IsModifyingCall(CE->getArg(I))) continue; @@ -6670,22 +6674,22 @@ void ASTConverter::appendPointeeStore( Place->takeAccessCondition())); } +bool ASTConverter::rejectOwnObjectUse(const Expr *E) { + const FunctionDecl *Callee = ownObjectCallee(E); + if (!Callee) + return false; + error(CurrentFn->Name + ": the reference " + Callee->getNameAsString() + + " returns is not used yet; call it as a statement of its own"); + return true; +} + bool ASTConverter::appendRecordCopy(const Expr *Source, const VarDecl *Target, SourceLocation Loc, std::vector> &Out) { if (!Source || !Target) return false; - if (const CXXConstructExpr *Copy = constructionOf(Source); - Copy && Copy->getNumArgs() == 1) - if (const auto *Call = - dyn_cast(Copy->getArg(0)->IgnoreParenImpCasts()); - Call && Call->getDirectCallee() && - returnsOwnObject(Call->getDirectCallee())) { - error(CurrentFn->Name + ": the reference " + - Call->getDirectCallee()->getNameAsString() + - " returns is not used yet; call it as a statement of its own"); - return true; - } + if (rejectOwnObjectUse(Source)) + return true; Source = Source->IgnoreParenImpCasts(); if (const auto *Construct = dyn_cast(Source)) { if (Construct->getNumArgs() != 1 || @@ -6790,6 +6794,8 @@ bool ASTConverter::appendObjectCopy(const Expr *Source, QualType Ty, const VExpr *Base, uint64_t Offset, SourceLocation Loc, std::vector> &Out) { + if (rejectOwnObjectUse(Source)) + return false; const Expr *Lvalue = peelObjectExpr(Source); if (const auto *Cast = dyn_cast(Lvalue); Cast && Cast->getCastKind() == CK_LValueToRValue) From 1ff05af72a73d4ca9ad1a4d805e08d6adb961d63 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 17:56:20 +0530 Subject: [PATCH 09/48] test: Check copying and assigning the reference a member operator returns to its own object. --- clang/test/Verify/suite/member_operators.cpp | 21 ++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/clang/test/Verify/suite/member_operators.cpp b/clang/test/Verify/suite/member_operators.cpp index 8b6fc001ed..f8251fcca9 100644 --- a/clang/test/Verify/suite/member_operators.cpp +++ b/clang/test/Verify/suite/member_operators.cpp @@ -132,6 +132,27 @@ int chained() } // CHECK-DAG: error: chained: the reference operator+= returns is not used yet; call it as a statement of its own +int copied() + cppverify::post(true) +{ + Money a(5); + Money b(6); + Money c = (a += b); + return c.cents; +} +// CHECK-DAG: error: copied: the reference operator+= returns is not used yet; call it as a statement of its own + +int assigned() + cppverify::post(true) +{ + Money a(5); + Money b(6); + Money c(0); + c = (a += b); + return c.cents; +} +// CHECK-DAG: error: assigned: the reference operator+= returns is not used yet; call it as a statement of its own + // An object a parameter refers to or points to satisfies its class // invariant on entry, as the caller shows, and through a mutable reference // or pointer it must at exit: so does every operand of an operator. From 1b7dd64d9f70cb7f3276a032ae99342c18ddf8da Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 18:01:12 +0530 Subject: [PATCH 10/48] docs: Describe member operators and the class invariants of objects passed by reference or pointer. --- website/source/language/structs.rst | 82 +++++++++++++++++++++++++++-- 1 file changed, 79 insertions(+), 3 deletions(-) diff --git a/website/source/language/structs.rst b/website/source/language/structs.rst index e8bc76c3d8..e2b6f029b6 100644 --- a/website/source/language/structs.rst +++ b/website/source/language/structs.rst @@ -572,6 +572,79 @@ 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 operators +~~~~~~~~~~~~~~~~ + +A member operator is a member function whose object is its first operand: +``a == b`` is ``a.operator==(b)`` and ``a |= b`` is ``a.operator|=(b)``. One +that returns a reference to its own object (every return being ``return +*this;``, as an assignment operator's is) returns nothing the caller does not +already hold, so it is verified as returning nothing, and is called as a +statement of its own: + +.. code-block:: cpp + + class Bits { + public: + Bits() + cv::post(word == 0) + : word(0) {} + + void set(int i) + cv::pre(0 <= i && i < 16) + cv::modifies(word) + cv::post(word == (cv::old(word) | (1u << i))) + { + word = word | (1u << i); + } + + bool operator==(const Bits &o) const + cv::post(cv::result == (word == o.word)) + { + return word == o.word; + } + + Bits &operator|=(const Bits &o) + cv::modifies(word) + cv::post(word == (cv::old(word) | o.word)) + { + word = word | o.word; + return *this; + } + + unsigned word; + + cv::type_invariant(word < 65536); + }; + + bool merged() + cv::post(cv::result) + { + Bits a; + Bits b; + a.set(3); + b.set(5); + a |= b; + b |= a; + bool same = a == b; + return same; + } + +.. code-block:: text + + Verified: Bits::Bits [backend=z3] + Verified: Bits::set [backend=z3] + Verified: Bits::operator== [backend=z3] + Verified: Bits::operator|= [backend=z3] + Verified: merged [backend=z3] + +``operator|=`` keeps the invariant because its operand ``o`` satisfies it +too: an object passed by reference does (`Class invariants`_). ``a |= a`` +passes one object as both ``this`` and ``o``, which are distinct by default, +and fails ``aliasing``. Using the reference such an operator returns, as in +``(a |= b) |= b``, ``Bits c = (a |= b);``, or ``c = (a |= b);``, is an error; +a free operator is a free function and returns its value as one does. + Constructors ------------ @@ -761,9 +834,12 @@ internal calls included, so no call observes the object while it is broken: it calls then fails, at that call. - A caller that writes a public field holds the invariant only if it keeps it: the next public call checks it there. -- A function that takes the object by reference or pointer assumes nothing - of its invariant; to call a public member function on it, it states the - invariant in its own precondition. +- An object a parameter refers to or points to satisfies its invariant on + entry, as the caller shows at the call, and through a mutable reference or + pointer it must at exit: every function boundary is one where it holds. A + null pointer needs none, and a pointer with an extent is not covered yet. + An extent in the invariant is ``this``'s, so an object passed by reference + does not carry it yet. - An extent of a pointer field, ``cv::valid(data, len)``, is assumed on entry as in a precondition (`Extents of pointer fields`_). At exit it states nothing; the next call checks it from what its caller knows, so a From 010fc0cde348ad8ccaae494b06fcce27f17a2c80 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 18:01:12 +0530 Subject: [PATCH 11/48] docs: Note member operators and class invariants at reference and pointer parameters. --- website/source/release-notes.rst | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index a6f7a162da..e4c6efbc04 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -332,7 +332,17 @@ passed and returned by value; member functions and constructors ignored it. On a class now, every public member function assumes it on entry and must restore it, every constructor must establish it, and it is checked at every call, internal ones included; an extent of a pointer field in it is assumed -on entry (:doc:`language/structs`). +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`). + +**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 +an unsupported type. A member operator now takes its first operand as its +object, and one returning its own object is verified as returning nothing. A +callee with local objects of its own can now also be lent the caller's local +objects (:doc:`language/structs`). **Records in memory by value.** A record kept in memory, a local object or one a pointer or reference addresses, could not be passed, returned, or From 43805898bc986db52633aefd13e4c94dac1dfe01 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 18:01:13 +0530 Subject: [PATCH 12/48] docs: Design member operators, own-object returns, and type invariants at reference and pointer parameters. --- docs/DESIGN.md | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 7d3975ea99..b4b092e8de 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1303,7 +1303,11 @@ void reset_left(Pair &p) - A call passes the object's address first: `p->m()` passes `p`, `obj.m()` binds `obj` as a reference argument does (a local object is lent to the callee under 3d's rules), and `m()` in a member function passes `this`. A - static member function is a free function. + static member function is a free function. A member operator's object is + its first operand (`a == b` is `a.operator==(b)`). A member function whose + every return is `return *this;` returns a reference to its own object, + which the caller holds: it is verified as returning nothing, and using the + reference (`(a += b) += c`) is an error. - 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 @@ -1491,6 +1495,12 @@ For by-value parameters this is purely an optimization — correctness is identi object. An extent marker in it, `valid(data, len)`, is a field extent (3e) of `this` on entry; at exit it is `true`, since a postcondition cannot carry a marker, and the next call checks the extent at its caller. +- An object a parameter refers to or points to satisfies its type + invariant at every function boundary: a generated precondition (for a + pointer, `p == nullptr ||` it) and, through a mutable reference or + pointer, a generated postcondition, as ACSL's weak type invariants and + Verus's do. A pointer with an extent is not covered yet, and an extent + marker in such an instance is `true`. - By design, the invariant is **not** asserted after each individual field write. Asserting the whole invariant mid-construction would spuriously fail while a multi-field struct is being initialised one field at a time (the other fields From 1aefeef2761df6715662185aa11df001569148cc Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 18:01:13 +0530 Subject: [PATCH 13/48] docs: Describe how member operators and the invariants of parameters are converted. --- docs/ARCHITECTURE.md | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 1a65652ce0..3f53be5716 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -290,6 +290,24 @@ layout at the actual's address), so the call stays a chain of stores; as one byte range, a `HeapFrame`, a falsified claim after a constructor and a member call took 60 s and ended `solver.timeout`, and fails in 0.3 s as cells. +**Member operators and parameters' invariants:** `convertExecCallArgs` takes +the object of a `CXXOperatorCallExpr` whose callee is an instance member +function from its first argument, and the parameters from the second. +`returnsOwnObject` recognizes a member function returning a reference to its +class whose every return is `*this` (`isOwnObject`): its `VFunction` returns +void, `findUnsupportedType` accepts its return type, its returns carry no +value, and a call using the reference as an argument, a copy's source, or an +assignment's source is an error (`rejectOwnObjectUse`, in +`convertExecCallArgs`, `appendRecordCopy`, and `appendObjectCopy`). For each +parameter that refers to or points to a record with type invariants (and has +no `valid` extent, `hasExtentMarker`), `convertFunction` converts the +invariants with `ThisSubstitute` set to the parameter, which `CXXThisExpr` +then converts to, and `DropExtentMarkers` set, and adds them as generated +preconditions (guarded by non-null for a pointer) and, unless the pointee is +const, postconditions. The record escape scan accepts a callee's own +automatic allocation unless it is initialized with an address it must not +keep. + **Records in memory by value:** `recordFieldsInMemory` reads a record value kept in memory, a promoted local or one in a pointee or record reference (`promotedRootLocal`, `inPointeeObject`), through implicit copies and From 0632d6cd94b8b2006c5e76a74ba2c77cc7e9d283 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:56 +0530 Subject: [PATCH 14/48] verify: Give cppverify::result, cppverify::old, and quantifiers the dependence of their type or operands. --- clang/include/clang/AST/ExprContract.h | 25 ++++++++++++++++++++----- 1 file changed, 20 insertions(+), 5 deletions(-) diff --git a/clang/include/clang/AST/ExprContract.h b/clang/include/clang/AST/ExprContract.h index 9a0b2802a0..2c88f4e2ba 100644 --- a/clang/include/clang/AST/ExprContract.h +++ b/clang/include/clang/AST/ExprContract.h @@ -23,6 +23,19 @@ namespace clang { // Forward declaration for serialization friend access. class ASTStmtReader; +/// The dependence of a quantifier or a choice: its operands', with its own +/// type fixed. In a template, `forall(k, 0, n, p[k] > 0)` over a `T *p` is +/// value-dependent, though it is a bool. +inline ExprDependence binderExprDependence(const Expr *Lo, const Expr *Hi, + const Expr *Body) { + ExprDependence D = Body ? Body->getDependence() : ExprDependence::None; + if (Lo) + D |= Lo->getDependence(); + if (Hi) + D |= Hi->getDependence(); + return turnTypeToValueDependence(D); +} + /// ForallExpr - Represents a universal quantifier: /// forall(binder, lo, hi, body) /// means: for all binder in [lo, hi), body holds; forall(binder, body) @@ -46,7 +59,7 @@ class ForallExpr : public Expr { SubExprs[LO] = Lo; SubExprs[HI] = Hi; SubExprs[BODY] = Body; - setDependence(ExprDependence::None); + setDependence(binderExprDependence(Lo, Hi, Body)); } explicit ForallExpr(EmptyShell Empty) : Expr(ForallExprClass, Empty) {} @@ -101,7 +114,7 @@ class ExistsExpr : public Expr { SubExprs[LO] = Lo; SubExprs[HI] = Hi; SubExprs[BODY] = Body; - setDependence(ExprDependence::None); + setDependence(binderExprDependence(Lo, Hi, Body)); } explicit ExistsExpr(EmptyShell Empty) : Expr(ExistsExprClass, Empty) {} @@ -156,7 +169,7 @@ class ContractChooseExpr : public Expr { SubExprs[LO] = Lo; SubExprs[HI] = Hi; SubExprs[BODY] = Body; - setDependence(ExprDependence::None); + setDependence(binderExprDependence(Lo, Hi, Body)); } explicit ContractChooseExpr(EmptyShell Empty) : Expr(ContractChooseExprClass, Empty) {} @@ -202,7 +215,7 @@ class OldExpr : public Expr { : Expr(OldExprClass, Inner->getType(), VK_PRValue, OK_Ordinary), OldLoc(OldLoc), LParenLoc(LParenLoc), RParenLoc(RParenLoc), Inner(Inner) { - setDependence(ExprDependence::None); + setDependence(Inner->getDependence()); } explicit OldExpr(EmptyShell Empty) : Expr(OldExprClass, Empty) {} @@ -237,7 +250,9 @@ class ResultExpr : public Expr { QualType ReturnType) : Expr(ResultExprClass, ReturnType, VK_PRValue, OK_Ordinary), ResultLoc(ResultLoc), EndLoc(EndLoc) { - setDependence(ExprDependence::None); + // In a template, the return type may depend on its parameters. + setDependence( + toExprDependenceForImpliedType(ReturnType->getDependence())); } explicit ResultExpr(EmptyShell Empty) : Expr(ResultExprClass, Empty) {} From 6e3a800c7f4eb9039da999612e3d43ebe3727421 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:56 +0530 Subject: [PATCH 15/48] verify: Declare contract instantiation for template specializations and the checks it shares with the parser. --- clang/include/clang/Sema/Sema.h | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/clang/include/clang/Sema/Sema.h b/clang/include/clang/Sema/Sema.h index b74f1bd3f7..d34717d871 100644 --- a/clang/include/clang/Sema/Sema.h +++ b/clang/include/clang/Sema/Sema.h @@ -10394,6 +10394,17 @@ class Sema final : public SemaBase { ExprResult ActOnContractRange(Expr *Base, Expr *Lower, SourceLocation ColonLoc, Expr *Length, SourceLocation RBLoc); + /// A component of a decreases clause, which must be an integer. + ExprResult ActOnContractMeasure(ExprResult E); + + /// forall, exists, or choose (\p Kind) over \p Binder: its bounds must be + /// integers and its body a condition. + ExprResult BuildContractBinderExpr(Stmt::StmtClass Kind, + SourceLocation KeywordLoc, + SourceLocation LParenLoc, + SourceLocation RParenLoc, VarDecl *Binder, + Expr *Lo, Expr *Hi, Expr *Body); + /// Rewrite unqualified field names to this->field for type_invariant(expr). ExprResult ActOnTypeInvariantExpr(ExprResult E, CXXRecordDecl *Record); @@ -14336,6 +14347,20 @@ class Sema final : public SemaBase { void InstantiateExceptionSpec(SourceLocation PointOfInstantiation, FunctionDecl *Function); + /// Instantiate the contract of a function template specialization, or of + /// a member of a class template specialization, from its pattern's, when + /// it is used or defined and has none yet. (Contracts are instantiated + /// lazily, as exception specifications are: an unused member's contract is + /// never instantiated.) + void InstantiateFunctionContract(SourceLocation PointOfInstantiation, + FunctionDecl *Function); + + /// The contract \p From of a template, with \p TemplateArgs substituted, + /// in \p To. Returns true on error. + bool SubstFunctionContract(const FunctionContractInfo &From, + FunctionContractInfo &To, + const MultiLevelTemplateArgumentList &TemplateArgs); + /// Instantiate (or find existing instantiation of) a function template with a /// given set of template arguments. /// From 6af1d1ec535d81f8b26a077137a07a1ae3b27b16 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:56 +0530 Subject: [PATCH 16/48] verify: Check a decreases component and a quantifier's bounds and body in Sema, for the parser and for instantiation. --- clang/lib/Sema/SemaContract.cpp | 38 +++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/clang/lib/Sema/SemaContract.cpp b/clang/lib/Sema/SemaContract.cpp index 8eef44eae8..08df4d87cc 100644 --- a/clang/lib/Sema/SemaContract.cpp +++ b/clang/lib/Sema/SemaContract.cpp @@ -309,6 +309,44 @@ ExprResult Sema::ActOnContractRange(Expr *Base, Expr *Lower, OK_Ordinary, ColonLoc, RBLoc); } +ExprResult Sema::ActOnContractMeasure(ExprResult E) { + if (E.isInvalid() || E.get()->isTypeDependent() || + E.get()->getType()->isIntegerType()) + return E; + Diag(E.get()->getExprLoc(), diag::err_contract_decreases_not_int); + return ExprError(); +} + +ExprResult Sema::BuildContractBinderExpr(Stmt::StmtClass Kind, + SourceLocation KeywordLoc, + SourceLocation LParenLoc, + SourceLocation RParenLoc, + VarDecl *Binder, Expr *Lo, Expr *Hi, + Expr *Body) { + for (Expr *Bound : {Lo, Hi}) + if (Bound && !Bound->isTypeDependent() && + !Bound->getType()->isIntegerType()) { + Diag(Bound->getExprLoc(), diag::err_contract_quantifier_bound_not_int); + return ExprError(); + } + ExprResult Condition = ActOnContractCondition(Body); + if (Condition.isInvalid()) + return ExprError(); + switch (Kind) { + case Stmt::ContractChooseExprClass: + return new (Context) ContractChooseExpr(KeywordLoc, LParenLoc, RParenLoc, + Binder, Lo, Hi, Condition.get(), + Binder->getType()); + case Stmt::ForallExprClass: + return new (Context) ForallExpr(KeywordLoc, LParenLoc, RParenLoc, Binder, + Lo, Hi, Condition.get(), Context.BoolTy); + default: + assert(Kind == Stmt::ExistsExprClass && "not a quantifier or a choice"); + return new (Context) ExistsExpr(KeywordLoc, LParenLoc, RParenLoc, Binder, + Lo, Hi, Condition.get(), Context.BoolTy); + } +} + ExprResult Sema::ActOnTypeInvariantExpr(ExprResult E, CXXRecordDecl *Record) { if (E.isInvalid() || !Record) return E; From c1382bcba88b20a075f88cb954267e2f49e02aca Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:57 +0530 Subject: [PATCH 17/48] verify: Keep a function template's contract and check its clauses through Sema. --- clang/lib/Parse/ParseCppVerify.cpp | 76 ++++++++++-------------------- 1 file changed, 24 insertions(+), 52 deletions(-) diff --git a/clang/lib/Parse/ParseCppVerify.cpp b/clang/lib/Parse/ParseCppVerify.cpp index 8c5d38537e..0ea63396c3 100644 --- a/clang/lib/Parse/ParseCppVerify.cpp +++ b/clang/lib/Parse/ParseCppVerify.cpp @@ -534,12 +534,11 @@ void Parser::ParseFunctionContractClauseList(FunctionContractClauses &Clauses) { // expressions. Parse each with ParseAssignmentExpression so the comma is // a tuple separator, not the C comma operator. do { - ExprResult E = finishCppVerifyExpression(ParseAssignmentExpression()); + ExprResult E = ParseAssignmentExpression(); if (E.isInvalid()) break; - if (!E.get()->isTypeDependent() && !E.get()->getType()->isIntegerType()) - Diag(E.get()->getExprLoc(), diag::err_contract_decreases_not_int); - else + E = finishCppVerifyExpression(Actions.ActOnContractMeasure(E)); + if (E.isUsable()) I.Decreases.push_back(E.get()); if (Tok.is(tok::comma)) ConsumeToken(); @@ -673,17 +672,14 @@ void Parser::attachFunctionContract(Decl *Result, I.MayDiverge.isInvalid() && I.Inductive.isInvalid() && I.BehaviorChecks.empty() && !I.IsSpec && !I.IsProof)) return; - // Templates are not verified yet: their clauses are ignored, as a member - // function's are. - if (FD->isTemplated() && !I.IsSpec && !I.IsProof) { - // A member of a class template is named by its class. - const auto *Method = dyn_cast(FD); - if (Method && Method->getParent()->isTemplated()) - Diag(FD->getLocation(), diag::warn_contract_template_unsupported) - << 1 << Method->getParent(); - else - Diag(FD->getLocation(), diag::warn_contract_template_unsupported) - << 0 << FD; + // A function template's clauses are instantiated with each of its + // specializations. Members of class templates are not verified yet: their + // clauses are ignored. + if (const auto *Method = dyn_cast(FD); + Method && Method->getParent()->isTemplated() && !I.IsSpec && + !I.IsProof) { + Diag(FD->getLocation(), diag::warn_contract_template_unsupported) + << 1 << Method->getParent(); return; } FunctionContractInfo &FCI = Ctx.getOrCreateFunctionContract(FD); @@ -835,17 +831,13 @@ void Parser::ParseLoopContractClauses(LoopContractInfo &Contract) { // Parse each component with ParseAssignmentExpression so the comma is a // tuple separator, not the C comma operator. while (true) { - ExprResult D = finishCppVerifyExpression(ParseAssignmentExpression()); + ExprResult D = ParseAssignmentExpression(); + if (D.isUsable()) + D = finishCppVerifyExpression(Actions.ActOnContractMeasure(D)); if (D.isInvalid()) { SkipUntil(tok::r_paren, StopAtSemi); return; } - if (!D.get()->isTypeDependent() && - !D.get()->getType()->isIntegerType()) { - Diag(D.get()->getExprLoc(), diag::err_contract_decreases_not_int); - SkipUntil(tok::r_paren, StopAtSemi); - return; - } Contract.Decreases.push_back(D.get()); if (Tok.isNot(tok::comma)) break; @@ -867,10 +859,11 @@ void Parser::attachLoopContract(StmtResult &Loop, LoopContractInfo &Contract) { (Contract.Invariants.empty() && Contract.Decreases.empty() && Contract.MayDiverge.isInvalid() && Contract.Modifies.empty())) return; - if (const FunctionDecl *FD = Actions.getCurFunctionDecl(); - FD && FD->isTemplated()) { + if (const auto *Method = + dyn_cast_or_null(Actions.getCurFunctionDecl()); + Method && Method->getParent()->isTemplated()) { Diag(Loop.get()->getBeginLoc(), diag::warn_contract_template_unsupported) - << 0 << FD; + << 1 << Method->getParent(); return; } Actions.getASTContext().getOrCreateLoopContract(Loop.get()) = @@ -1379,23 +1372,6 @@ ExprResult Parser::ParseQuantifierExpr() { return ExprError(); } - // Validate bound types: lo and hi must be integer. - for (const ExprResult &Bound : {Lo, Hi}) - if (Bound.isUsable() && !Bound.get()->isTypeDependent() && - !Bound.get()->getType()->isIntegerType()) { - Diag(Bound.get()->getExprLoc(), - diag::err_contract_quantifier_bound_not_int); - SkipUntil(tok::r_paren, StopAtSemi); - return ExprError(); - } - - // Validate body: must be contextually convertible to bool. - ExprResult BodyBool = Actions.ActOnContractCondition(Body); - if (BodyBool.isInvalid()) { - SkipUntil(tok::r_paren, StopAtSemi); - return ExprError(); - } - if (Tok.isNot(tok::r_paren)) { Diag(Tok, diag::err_contract_expected_rparen) << Keyword; SkipUntil(tok::r_paren, StopAtSemi); @@ -1403,16 +1379,12 @@ ExprResult Parser::ParseQuantifierExpr() { } SourceLocation RParenLoc = ConsumeParen(); - Expr *LoE = Lo.isUsable() ? Lo.get() : nullptr; - Expr *HiE = Hi.isUsable() ? Hi.get() : nullptr; - if (IsChoose) - return new (Ctx) ContractChooseExpr(KwLoc, LParenLoc, RParenLoc, BoundVar, - LoE, HiE, BodyBool.get(), Ctx.IntTy); - if (IsForall) - return new (Ctx) ForallExpr(KwLoc, LParenLoc, RParenLoc, BoundVar, LoE, HiE, - BodyBool.get(), Ctx.BoolTy); - return new (Ctx) ExistsExpr(KwLoc, LParenLoc, RParenLoc, BoundVar, LoE, HiE, - BodyBool.get(), Ctx.BoolTy); + return Actions.BuildContractBinderExpr( + IsChoose ? Stmt::ContractChooseExprClass + : IsForall ? Stmt::ForallExprClass + : Stmt::ExistsExprClass, + KwLoc, LParenLoc, RParenLoc, BoundVar, Lo.isUsable() ? Lo.get() : nullptr, + Hi.isUsable() ? Hi.get() : nullptr, Body.get()); } /// Parse cppverify::old(expr) From 7c37848a3942e0ae091e7d4639cffa78ea856c89 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:57 +0530 Subject: [PATCH 18/48] verify: Transform contract clauses with the parser's checks, loop contracts with their loops, and trigger marks. --- clang/lib/Sema/TreeTransform.h | 254 +++++++++++++++++++++++++++++---- 1 file changed, 225 insertions(+), 29 deletions(-) diff --git a/clang/lib/Sema/TreeTransform.h b/clang/lib/Sema/TreeTransform.h index 78122a51e5..4a3583ac12 100644 --- a/clang/lib/Sema/TreeTransform.h +++ b/clang/lib/Sema/TreeTransform.h @@ -570,6 +570,25 @@ class TreeTransform { /// Transform the variable a quantifier or a choice binds. VarDecl *TransformContractBinder(VarDecl *Binder); + /// Transform a contract clause's expression and check it as the parser + /// does: a condition, a component of a decreases clause, a footprint of a + /// modifies clause, or a term (an argument of aliases or reads). + ExprResult TransformContractCondition(Expr *E); + ExprResult TransformContractMeasure(Expr *E); + ExprResult TransformContractFootprint(Expr *E); + ExprResult TransformContractTerm(Expr *E); + + /// Transform the contract of a function, from \p From into \p To. + /// Returns true on error. + bool TransformFunctionContract(const FunctionContractInfo &From, + FunctionContractInfo &To); + + /// Transform the contract of the loop \p S, if it has one, into \p To; + /// \p Changed says whether any of its clauses changed. Returns true on + /// error. + bool TransformLoopContract(Stmt *S, std::optional &To, + bool &Changed); + /// Transform the given declaration, which was the first part of a /// nested-name-specifier in a member access expression. /// @@ -4451,16 +4470,23 @@ ExprResult TreeTransform::TransformExpr(Expr *E) { if (!E) return E; + ExprResult Result = E; switch (E->getStmtClass()) { case Stmt::NoStmtClass: break; #define STMT(Node, Parent) case Stmt::Node##Class: break; #define ABSTRACT_STMT(Stmt) #define EXPR(Node, Parent) \ - case Stmt::Node##Class: return getDerived().Transform##Node(cast(E)); + case Stmt::Node##Class: \ + Result = getDerived().Transform##Node(cast(E)); \ + break; #include "clang/AST/StmtNodes.inc" } - return E; + // A quantifier's trigger term is one in what it becomes too. + if (Result.isUsable() && Result.get() != E && + SemaRef.Context.isTriggerTerm(E)) + SemaRef.Context.markTriggerTerm(Result.get()); + return Result; } template @@ -8492,13 +8518,21 @@ TreeTransform::TransformWhileStmt(WhileStmt *S) { if (Body.isInvalid()) return StmtError(); - if (!getDerived().AlwaysRebuild() && + std::optional Contract; + bool ContractChanged = false; + if (getDerived().TransformLoopContract(S, Contract, ContractChanged)) + return StmtError(); + + if (!getDerived().AlwaysRebuild() && !ContractChanged && Cond.get() == std::make_pair(S->getConditionVariable(), S->getCond()) && Body.get() == S->getBody()) return Owned(S); - return getDerived().RebuildWhileStmt(S->getWhileLoc(), S->getLParenLoc(), - Cond, S->getRParenLoc(), Body.get()); + StmtResult Result = getDerived().RebuildWhileStmt( + S->getWhileLoc(), S->getLParenLoc(), Cond, S->getRParenLoc(), Body.get()); + if (Contract && Result.isUsable()) + SemaRef.Context.getOrCreateLoopContract(Result.get()) = std::move(*Contract); + return Result; } template @@ -8519,14 +8553,22 @@ TreeTransform::TransformDoStmt(DoStmt *S) { if (Cond.isInvalid()) return StmtError(); - if (!getDerived().AlwaysRebuild() && + std::optional Contract; + bool ContractChanged = false; + if (getDerived().TransformLoopContract(S, Contract, ContractChanged)) + return StmtError(); + + if (!getDerived().AlwaysRebuild() && !ContractChanged && Cond.get() == S->getCond() && Body.get() == S->getBody()) return S; - return getDerived().RebuildDoStmt(S->getDoLoc(), Body.get(), S->getWhileLoc(), - /*FIXME:*/S->getWhileLoc(), Cond.get(), - S->getRParenLoc()); + StmtResult Result = getDerived().RebuildDoStmt( + S->getDoLoc(), Body.get(), S->getWhileLoc(), + /*FIXME:*/ S->getWhileLoc(), Cond.get(), S->getRParenLoc()); + if (Contract && Result.isUsable()) + SemaRef.Context.getOrCreateLoopContract(Result.get()) = std::move(*Contract); + return Result; } template @@ -8576,16 +8618,24 @@ TreeTransform::TransformForStmt(ForStmt *S) { SemaRef.OpenACC().ActOnForStmtEnd(S->getBeginLoc(), Body); - if (!getDerived().AlwaysRebuild() && + std::optional Contract; + bool ContractChanged = false; + if (getDerived().TransformLoopContract(S, Contract, ContractChanged)) + return StmtError(); + + if (!getDerived().AlwaysRebuild() && !ContractChanged && Init.get() == S->getInit() && Cond.get() == std::make_pair(S->getConditionVariable(), S->getCond()) && Inc.get() == S->getInc() && Body.get() == S->getBody()) return S; - return getDerived().RebuildForStmt(S->getForLoc(), S->getLParenLoc(), - Init.get(), Cond, FullInc, - S->getRParenLoc(), Body.get()); + StmtResult Result = getDerived().RebuildForStmt( + S->getForLoc(), S->getLParenLoc(), Init.get(), Cond, FullInc, + S->getRParenLoc(), Body.get()); + if (Contract && Result.isUsable()) + SemaRef.Context.getOrCreateLoopContract(Result.get()) = std::move(*Contract); + return Result; } template @@ -18326,12 +18376,13 @@ ExprResult TreeTransform::TransformHLSLOutArgExpr(HLSLOutArgExpr *E) { //===----------------------------------------------------------------------===// // Contract nodes are ghost/spec constructs that are stripped before codegen. -// Template instantiation just rebuilds them unchanged by transforming children. +// They are rebuilt from their transformed children with the checks the parser +// applies, so a dependent condition is converted where it is instantiated. template StmtResult TreeTransform::TransformContractAssertStmt(ContractAssertStmt *S) { - ExprResult Cond = getDerived().TransformExpr(S->getCond()); + ExprResult Cond = getDerived().TransformContractCondition(S->getCond()); if (Cond.isInvalid()) return StmtError(); StmtResult By = S->getBy(); @@ -18410,6 +18461,145 @@ VarDecl *TreeTransform::TransformContractBinder(VarDecl *Binder) { return New; } +template +ExprResult TreeTransform::TransformContractCondition(Expr *E) { + ExprResult Result = getDerived().TransformExpr(E); + if (Result.isInvalid()) + return ExprError(); + return SemaRef.MaybeCreateExprWithCleanups( + SemaRef.ActOnContractCondition(Result)); +} + +template +ExprResult TreeTransform::TransformContractMeasure(Expr *E) { + ExprResult Result = getDerived().TransformExpr(E); + if (Result.isInvalid()) + return ExprError(); + return SemaRef.MaybeCreateExprWithCleanups( + SemaRef.ActOnContractMeasure(Result)); +} + +template +ExprResult TreeTransform::TransformContractTerm(Expr *E) { + ExprResult Result = getDerived().TransformExpr(E); + if (Result.isInvalid()) + return ExprError(); + return SemaRef.MaybeCreateExprWithCleanups(Result); +} + +template +ExprResult TreeTransform::TransformContractFootprint(Expr *E) { + // A range p[lo : n] is a footprint as a whole, never an operand. + Expr *Footprint = E; + if (auto *Full = dyn_cast(Footprint)) + Footprint = Full->getSubExpr(); + auto *Range = dyn_cast(Footprint->IgnoreParens()); + if (!Range) + return getDerived().TransformContractTerm(E); + ExprResult Base = getDerived().TransformExpr(Range->getBase()); + if (Base.isInvalid()) + return ExprError(); + ExprResult Lower; + if (Range->getLowerBound()) { + Lower = getDerived().TransformExpr(Range->getLowerBound()); + if (Lower.isInvalid()) + return ExprError(); + } + ExprResult Length; + if (Range->getLength()) { + Length = getDerived().TransformExpr(Range->getLength()); + if (Length.isInvalid()) + return ExprError(); + } + return SemaRef.MaybeCreateExprWithCleanups(SemaRef.ActOnContractRange( + Base.get(), Lower.get(), Range->getColonLocFirst(), Length.get(), + Range->getRBracketLoc())); +} + +template +bool TreeTransform::TransformFunctionContract( + const FunctionContractInfo &From, FunctionContractInfo &To) { + bool Invalid = false; + auto Keep = [&](ExprResult Result, SmallVectorImpl &Out) { + if (Result.isUsable()) + Out.push_back(Result.get()); + else + Invalid = true; + }; + auto KeepPairs = [&](ArrayRef> Pairs, + SmallVectorImpl> &Out) { + for (const auto &[First, Second] : Pairs) { + ExprResult A = getDerived().TransformContractTerm(First); + ExprResult B = getDerived().TransformContractTerm(Second); + if (A.isUsable() && B.isUsable()) + Out.push_back({A.get(), B.get()}); + else + Invalid = true; + } + }; + for (Expr *E : From.Preconditions) + Keep(getDerived().TransformContractCondition(E), To.Preconditions); + for (Expr *E : From.Postconditions) + Keep(getDerived().TransformContractCondition(E), To.Postconditions); + for (Expr *E : From.Modifies) + Keep(getDerived().TransformContractFootprint(E), To.Modifies); + KeepPairs(From.Aliases, To.Aliases); + for (Expr *E : From.Recommends) + Keep(getDerived().TransformContractCondition(E), To.Recommends); + KeepPairs(From.Reads, To.Reads); + for (Expr *E : From.When) + Keep(getDerived().TransformContractCondition(E), To.When); + for (Expr *E : From.Decreases) + Keep(getDerived().TransformContractMeasure(E), To.Decreases); + To.MayDiverge = From.MayDiverge; + To.Inductive = From.Inductive; + for (Expr *E : From.BehaviorChecks) + Keep(getDerived().TransformContractCondition(E), To.BehaviorChecks); + for (const auto &[Name, Assumes] : From.Behaviors) { + ExprResult Result = getDerived().TransformContractCondition(Assumes); + if (Result.isUsable()) + To.Behaviors.push_back({Name, Result.get()}); + else + Invalid = true; + } + for (const FunctionContractInfo::ClauseProof &Proof : From.ClauseProofs) { + StmtResult Body = getDerived().TransformStmt(Proof.Body); + if (Body.isUsable()) + To.ClauseProofs.push_back({Proof.K, Body.get(), Proof.Loc}); + else + Invalid = true; + } + To.IsSpec = From.IsSpec; + To.IsProof = From.IsProof; + return Invalid; +} + +template +bool TreeTransform::TransformLoopContract( + Stmt *S, std::optional &To, bool &Changed) { + const LoopContractInfo *From = SemaRef.Context.getLoopContract(S); + if (!From) + return false; + To.emplace(); + bool Invalid = false; + auto Keep = [&](Expr *Old, ExprResult New, SmallVectorImpl &Out) { + if (!New.isUsable()) { + Invalid = true; + return; + } + Changed |= New.get() != Old; + Out.push_back(New.get()); + }; + for (Expr *E : From->Invariants) + Keep(E, getDerived().TransformContractCondition(E), To->Invariants); + for (Expr *E : From->Decreases) + Keep(E, getDerived().TransformContractMeasure(E), To->Decreases); + for (Expr *E : From->Modifies) + Keep(E, getDerived().TransformContractFootprint(E), To->Modifies); + To->MayDiverge = From->MayDiverge; + return Invalid; +} + template ExprResult TreeTransform::TransformForallExpr(ForallExpr *E) { VarDecl *Var = getDerived().TransformContractBinder(E->getBoundVar()); @@ -18425,10 +18615,10 @@ ExprResult TreeTransform::TransformForallExpr(ForallExpr *E) { Lo.get() == E->getLo() && Hi.get() == E->getHi() && Body.get() == E->getBody()) return E; - return new (SemaRef.Context) - ForallExpr(E->getForallLoc(), E->getLParenLoc(), E->getRParenLoc(), - Var, Lo.getAs(), Hi.getAs(), - Body.getAs(), SemaRef.Context.BoolTy); + return SemaRef.BuildContractBinderExpr( + Stmt::ForallExprClass, E->getForallLoc(), E->getLParenLoc(), + E->getRParenLoc(), Var, Lo.getAs(), Hi.getAs(), + Body.getAs()); } template @@ -18446,10 +18636,10 @@ ExprResult TreeTransform::TransformContractChooseExpr(ContractChooseExp Lo.get() == E->getLo() && Hi.get() == E->getHi() && Body.get() == E->getBody()) return E; - return new (SemaRef.Context) - ContractChooseExpr(E->getChooseLoc(), E->getLParenLoc(), E->getRParenLoc(), - Var, Lo.getAs(), Hi.getAs(), - Body.getAs(), E->getType()); + return SemaRef.BuildContractBinderExpr( + Stmt::ContractChooseExprClass, E->getChooseLoc(), E->getLParenLoc(), + E->getRParenLoc(), Var, Lo.getAs(), Hi.getAs(), + Body.getAs()); } template @@ -18467,10 +18657,10 @@ ExprResult TreeTransform::TransformExistsExpr(ExistsExpr *E) { Lo.get() == E->getLo() && Hi.get() == E->getHi() && Body.get() == E->getBody()) return E; - return new (SemaRef.Context) - ExistsExpr(E->getExistsLoc(), E->getLParenLoc(), E->getRParenLoc(), - Var, Lo.getAs(), Hi.getAs(), - Body.getAs(), SemaRef.Context.BoolTy); + return SemaRef.BuildContractBinderExpr( + Stmt::ExistsExprClass, E->getExistsLoc(), E->getLParenLoc(), + E->getRParenLoc(), Var, Lo.getAs(), Hi.getAs(), + Body.getAs()); } template @@ -18486,8 +18676,14 @@ ExprResult TreeTransform::TransformOldExpr(OldExpr *E) { template ExprResult TreeTransform::TransformResultExpr(ResultExpr *E) { - // ResultExpr has no children to transform. - return E; + // The function's return type, which may depend on template parameters. + QualType Type = getDerived().TransformType(E->getType()); + if (Type.isNull()) + return ExprError(); + if (!getDerived().AlwaysRebuild() && Type == E->getType()) + return E; + return new (SemaRef.Context) + ResultExpr(E->getResultLoc(), E->getEndLoc(), Type); } } // end namespace clang From eb77fe2fd31caa97e3064615aaa87e23fb086082 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:57 +0530 Subject: [PATCH 19/48] verify: Substitute template arguments into a function contract. --- clang/lib/Sema/SemaTemplateInstantiate.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/clang/lib/Sema/SemaTemplateInstantiate.cpp b/clang/lib/Sema/SemaTemplateInstantiate.cpp index bad0cdd1b7..8f757853c1 100644 --- a/clang/lib/Sema/SemaTemplateInstantiate.cpp +++ b/clang/lib/Sema/SemaTemplateInstantiate.cpp @@ -4493,6 +4493,14 @@ Sema::SubstExpr(Expr *E, const MultiLevelTemplateArgumentList &TemplateArgs) { return Instantiator.TransformExpr(E); } +bool Sema::SubstFunctionContract( + const FunctionContractInfo &From, FunctionContractInfo &To, + const MultiLevelTemplateArgumentList &TemplateArgs) { + TemplateInstantiator Instantiator(*this, TemplateArgs, SourceLocation(), + DeclarationName()); + return Instantiator.TransformFunctionContract(From, To); +} + ExprResult Sema::SubstCXXIdExpr(Expr *E, const MultiLevelTemplateArgumentList &TemplateArgs) { From 36c3cf8a829b293825409e651280a0e04cc3d916 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:58 +0530 Subject: [PATCH 20/48] verify: Instantiate a specialization's contract with its definition, and keep ghost variables ghost. --- .../lib/Sema/SemaTemplateInstantiateDecl.cpp | 57 +++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp b/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp index c2e90624b8..9912c19027 100644 --- a/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp +++ b/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp @@ -5436,6 +5436,56 @@ void Sema::InstantiateExceptionSpec(SourceLocation PointOfInstantiation, TemplateArgs); } +void Sema::InstantiateFunctionContract(SourceLocation PointOfInstantiation, + FunctionDecl *Function) { + if (!getLangOpts().VerifyContracts || Function->isInvalidDecl() || + !Function->isTemplateInstantiation()) + return; + const FunctionDecl *Pattern = + Function->getTemplateInstantiationPattern(/*ForDefinition=*/false); + const FunctionContractInfo *PatternContract = + Pattern ? Context.getFunctionContract(Pattern) : nullptr; + if (!PatternContract || Context.getFunctionContract(Function)) + return; + // The clauses name the parameters of the declaration they are written on. + const FunctionDecl *Written = + PatternContract->ContractDecl ? PatternContract->ContractDecl : Pattern; + + // Recorded first, so that a use of the specialization in its own contract + // finds it and stops. + FunctionContractInfo &Contract = Context.getOrCreateFunctionContract(Function); + Contract.ContractDecl = Function; + Contract.IsSpec = PatternContract->IsSpec; + Contract.IsProof = PatternContract->IsProof; + + NonSFINAEContext _(*this); + InstantiatingTemplate Inst(*this, PointOfInstantiation, Function); + if (Inst.isInvalid()) + return; + Sema::ContextRAII SavedContext(*this, Function); + // The contract is a full expression of its own, whatever the use that + // asks for it, and the specs it applies are used. + EnterExpressionEvaluationContext Evaluated( + *this, ExpressionEvaluationContext::PotentiallyEvaluated); + LocalInstantiationScope Scope(*this); + MultiLevelTemplateArgumentList TemplateArgs = getTemplateInstantiationArgs( + Function, Function->getLexicalDeclContext(), /*Final=*/false, + /*Innermost=*/std::nullopt, /*RelativeToPrimary=*/true); + if (addInstantiatedParametersToScope(Function, Written, Scope, TemplateArgs)) + return; + std::optional ThisScope; + if (auto *Method = dyn_cast(Function); + Method && Method->isImplicitObjectMemberFunction()) + ThisScope.emplace(*this, Method->getParent(), + Method->getMethodQualifiers(), + static_cast(getLangOpts().CPlusPlus11)); + FunctionContractInfo Instantiated; + if (SubstFunctionContract(*PatternContract, Instantiated, TemplateArgs)) + return; + Instantiated.ContractDecl = Function; + Contract = std::move(Instantiated); +} + /// Initializes the common fields of an instantiation function /// declaration (New) from the corresponding fields of its template (Tmpl). /// @@ -5766,6 +5816,9 @@ void Sema::InstantiateFunctionDefinition(SourceLocation PointOfInstantiation, } } + // The definition is verified against its own contract. + InstantiateFunctionContract(PointOfInstantiation, Function); + NonSFINAEContext _(*this); InstantiatingTemplate Inst(*this, PointOfInstantiation, Function); if (Inst.isInvalid()) @@ -6175,6 +6228,10 @@ void Sema::BuildVariableInstantiation( InstantiateAttrs(TemplateArgs, OldVar, NewVar, LateAttrs, StartingScope); + // A ghost variable is one in every instantiation. + if (Context.isGhostVariable(OldVar)) + Context.markGhostVariable(NewVar); + LookupResult Previous( *this, NewVar->getDeclName(), NewVar->getLocation(), NewVar->isLocalExternDecl() ? Sema::LookupRedeclarationWithLinkage From 69eb19c14ca84ad9d5b4cedd0b807fc111bbce3d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:58 +0530 Subject: [PATCH 21/48] verify: Instantiate a specialization's contract where it is used. --- clang/lib/Sema/SemaExpr.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/clang/lib/Sema/SemaExpr.cpp b/clang/lib/Sema/SemaExpr.cpp index bd638b7c2a..e6e85e5611 100644 --- a/clang/lib/Sema/SemaExpr.cpp +++ b/clang/lib/Sema/SemaExpr.cpp @@ -19173,6 +19173,12 @@ void Sema::MarkFunctionReferenced(SourceLocation Loc, FunctionDecl *Func, if (FPT && isUnresolvedExceptionSpec(FPT->getExceptionSpecType())) ResolveExceptionSpec(Loc, FPT); + // A contract of a template specialization is needed where the + // specialization is used, as its callers rely on it, whether or not its + // definition is instantiated here. + if (OdrUse != OdrUseContext::None) + InstantiateFunctionContract(Loc, Func); + // A callee could be called by a host function then by a device function. // If we only try recording once, we will miss recording the use on device // side. Therefore keep trying until it is recorded. From 96dbdeb02dc1a7686a6fb5a5c2a3dd4281626946 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:59 +0530 Subject: [PATCH 22/48] verify: Record where each template specialization is instantiated. --- clang/lib/Verify/Frontend/ASTConverter.h | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index 677e548557..3878d3a1d2 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -71,6 +71,8 @@ class ASTConverter { /// Binders of a forall being introduced by contract_assert(...) by. std::set ArbitraryValues; std::map> UnverifiedCallers; + std::map> + InstantiationPoints; std::map ParameterNames; unsigned BoundValueId = 0; std::map FunctionIdentities; @@ -130,6 +132,14 @@ class ASTConverter { getWarnings() const { return Warnings; } + /// For each template specialization converted, by its name: where it is + /// instantiated and what it is ("function template specialization"), + /// which its diagnostics note as a compiler's do. A name two + /// specializations share has no location. + const std::map> & + getInstantiationPoints() const { + return InstantiationPoints; + } private: /// Contract arithmetic is mathematical, as in ACSL and Verus spec code: an From c0aee2491cc015e13fb23070ec975d6a0f605414 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:59 +0530 Subject: [PATCH 23/48] verify: Verify each instantiated specialization of a function template, named with its arguments. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 126 ++++++++++++++------- 1 file changed, 86 insertions(+), 40 deletions(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index b55daccea6..81ac6c1a41 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -915,6 +915,17 @@ VIntMode ASTConverter::specCallIntMode(const FunctionDecl *FD) const { return VIntMode::Math; } +/// A function as the verifier's messages name it, a template specialization +/// with its arguments (`maxv`). +static std::string functionName(const FunctionDecl *FD, + bool Qualified = false) { + std::string Name; + llvm::raw_string_ostream OS(Name); + FD->getNameForDiagnostic(OS, FD->getASTContext().getPrintingPolicy(), + Qualified); + return Name; +} + std::string ASTConverter::functionIdentity(const FunctionDecl *FD) { if (!FD) return {}; @@ -1994,6 +2005,17 @@ static void collectFunctionCandidates(const DeclContext *DC, ASTContext &Ctx, const FunctionDecl *FD = FTD->getTemplatedDecl(); if (FD->isThisDeclarationADefinition()) Out.push_back(FD); + // Each specialization this translation unit instantiates is a function + // of its own, with its definition or else its contract. An explicit + // specialization is a declaration of its own, and the redeclarations + // of a template share its specializations. + if (!FTD->isCanonicalDecl()) + continue; + for (const FunctionDecl *Spec : FTD->specializations()) + if (Spec->isTemplateInstantiation() && + (Spec->isThisDeclarationADefinition() || + (Ctx.getFunctionContract(Spec) && !Spec->hasBody()))) + Out.push_back(Spec); continue; } if (const auto *FD = dyn_cast(D)) { @@ -2154,23 +2176,47 @@ std::vector> ASTConverter::convertTranslationUnit() { // verified code calls it, which reports the call. if (!functionContract(FD) && !hasContractStatements(FD, Ctx)) continue; - llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); - llvm::SaveAndRestore OwnerName(ErrorFunctionName, FD->getNameAsString()); - llvm::SaveAndRestore InContract(ErrorInContract, true); - if (UnsupportedMember) { - error(FD->getLocation(), - FD->getQualifiedNameAsString() + ": " + *UnsupportedMember); + // A function template is verified in each of its specializations, + // which follow it: what it means depends on its arguments. + if (!UnsupportedMember) { + const FunctionTemplateDecl *Template = + FD->getDescribedFunctionTemplate(); + if (Template && !FD->isInStdNamespace() && + Ctx.getSourceManager().isWrittenInMainFile(FD->getLocation()) && + llvm::none_of(Template->specializations(), + [](const FunctionDecl *Spec) { + return Spec->isTemplateInstantiation(); + })) + Warnings.emplace_back( + FD->getLocation(), + functionName(FD) + ": function template is not verified: this " + "translation unit instantiates none of its " + "specializations"); continue; } - if (!FD->isInStdNamespace() && - Ctx.getSourceManager().isWrittenInMainFile(FD->getLocation())) - error(FD->getLocation(), - FD->getNameAsString() + - ": function template verification is unsupported"); + llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); + llvm::SaveAndRestore OwnerName(ErrorFunctionName, functionName(FD)); + llvm::SaveAndRestore InContract(ErrorInContract, true); + error(FD->getLocation(), + FD->getQualifiedNameAsString() + ": " + *UnsupportedMember); continue; } if (FD->isInStdNamespace()) continue; + if (FD->isTemplateInstantiation()) { + // Its diagnostics note where it is instantiated, as a compiler's do, + // under the names they give its function. + const SourceLocation Point = FD->getPointOfInstantiation(); + const char *What = FD->getPrimaryTemplate() + ? "function template specialization" + : "member function"; + for (const std::string &Name : + {functionName(FD), functionName(FD, isa(FD))}) + if (auto [It, New] = InstantiationPoints.emplace( + Name, std::make_pair(Point, std::string(What))); + !New && It->second.first != Point) + It->second.first = SourceLocation(); + } const size_t ErrorsBefore = Errors.size(); auto Fn = convertFunction(FD); if (Fn && Errors.size() == ErrorsBefore) { @@ -2203,7 +2249,7 @@ std::vector> ASTConverter::convertTranslationUnit() { if (const FunctionContractInfo *FCI = functionContract(Callee); FCI && !FCI->IsSpec && !FCI->IsProof) UnverifiedCallers[functionIdentity(Callee)].insert( - FD->getNameAsString()); + functionName(FD)); for (const Stmt *Child : S->children()) Calls(Child); }; @@ -2803,7 +2849,7 @@ bool ASTConverter::exceedsNestingLimit(const FunctionDecl *FD, if (Depth > Limit) { const PresumedLoc Where = Ctx.getSourceManager().getPresumedLoc(S->getBeginLoc()); - error(FD->getNameAsString() + ": the expression at " + + error(functionName(FD) + ": the expression at " + (Where.isValid() ? std::to_string(Where.getLine()) + ":" + std::to_string(Where.getColumn()) : std::string("an unknown location")) + @@ -2960,7 +3006,7 @@ std::unique_ptr ASTConverter::convertFunction(const FunctionDecl *FD) { llvm::SaveAndRestore At(CurrentRange, SourceRange(FD->getLocation())); llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); - llvm::SaveAndRestore OwnerName(ErrorFunctionName, FD->getNameAsString()); + llvm::SaveAndRestore OwnerName(ErrorFunctionName, functionName(FD)); llvm::SaveAndRestore InContract(ErrorInContract, true); const size_t ErrorsAtStart = Errors.size(); const FunctionContractInfo *FCI = functionContract(FD); @@ -2977,7 +3023,7 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { ParameterNames.clear(); const FunctionDecl *ContractDecl = FCI->ContractDecl ? FCI->ContractDecl : FD; if (ContractDecl->getNumParams() != FD->getNumParams()) { - error(FD->getNameAsString() + ": contract declaration parameter mismatch"); + error(functionName(FD) + ": contract declaration parameter mismatch"); return nullptr; } for (unsigned I = 0; I < FD->getNumParams(); ++I) { @@ -2992,16 +3038,16 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { ParameterNames[DefinitionParam] = Name; } if (FD->isVariadic()) { - error(FD->getNameAsString() + ": variadic functions are unsupported"); + error(functionName(FD) + ": variadic functions are unsupported"); return nullptr; } if (FCI->IsSpec && writesIndirectMemory(FD)) { - error(FD->getNameAsString() + ": spec functions must not write memory"); + error(functionName(FD) + ": spec functions must not write memory"); return nullptr; } if (FCI->IsSpec && (!FCI->Preconditions.empty() || !FCI->Modifies.empty() || !FCI->Aliases.empty())) { - error(FD->getNameAsString() + + error(functionName(FD) + ": a spec function is defined for every argument and " "its body is its meaning, so pre, modifies, and aliases " "do not apply; use recommends for a soft precondition"); @@ -3009,13 +3055,13 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { } if (FCI->IsSpec && FD->getReturnType()->isRecordType() && !VType::collectionKind(FD->getReturnType())) { - error(FD->getNameAsString() + + error(functionName(FD) + ": aggregate-returning spec functions are unsupported"); return nullptr; } if (auto Unsupported = findUnsupportedType(FD, !FCI->IsSpec && !FCI->IsProof)) { - error(FD->getNameAsString() + + error(functionName(FD) + ": unsupported C++ type in verification: " + *Unsupported); return nullptr; } @@ -3027,7 +3073,7 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { const bool HasThis = Method && Method->isInstance(); const auto *Constructor = dyn_cast(FD); Fn->IsConstructor = Constructor != nullptr; - Fn->Name = Method ? FD->getQualifiedNameAsString() : FD->getNameAsString(); + Fn->Name = functionName(FD, /*Qualified=*/Method != nullptr); Fn->Identity = functionIdentity(FD); Fn->IsSpec = FCI->IsSpec; Fn->IsProof = FCI->IsProof; @@ -3795,7 +3841,7 @@ bool ASTConverter::checkLoopTermination(const Stmt *Loop, bool HasMeasure) { std::unique_ptr ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); - llvm::SaveAndRestore OwnerName(ErrorFunctionName, FD->getNameAsString()); + llvm::SaveAndRestore OwnerName(ErrorFunctionName, functionName(FD)); llvm::SaveAndRestore InContract(ErrorInContract, true); const size_t ErrorsAtStart = Errors.size(); ParameterNames.clear(); @@ -3805,18 +3851,18 @@ ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { if (!FD->isConstexpr() || !FD->hasBody()) return nullptr; if (FD->getReturnType()->isRecordType()) { - error(FD->getNameAsString() + + error(functionName(FD) + ": aggregate-returning constexpr specs are unsupported"); return nullptr; } if (auto Unsupported = findUnsupportedType(FD, false)) { - error(FD->getNameAsString() + + error(functionName(FD) + ": unsupported C++ type in verification: " + *Unsupported); return nullptr; } auto Fn = std::make_unique(); - Fn->Name = FD->getNameAsString(); + Fn->Name = functionName(FD); Fn->Identity = functionIdentity(FD); Fn->IsSpec = true; Fn->IsConstexprSpec = true; @@ -5982,7 +6028,7 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { if (CalleeContract && CalleeContract->IsSpec && !InContractExpression && !InGhost && !CurrentFn->IsSpec && !CurrentFn->IsProof) { error(CurrentFn->Name + ": spec function " + - Callee->getNameAsString() + + functionName(Callee) + " cannot be used in executable code"); return nullptr; } @@ -6024,18 +6070,18 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { Ctx); noteSpecUse(Callee); return std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), Ty, E->getExprLoc(), specReadsHeap(Callee)); } if (functionContract(Callee)) error(CurrentFn->Name + ": executable call is unsupported in this expression " "context: " + - Callee->getNameAsString()); + functionName(Callee)); else error(CurrentFn->Name + ": call to function without a verification contract: " + - Callee->getNameAsString()); + functionName(Callee)); } } error(CurrentFn->Name + ": unsupported expression: " + E->getStmtClassName()); @@ -6112,7 +6158,7 @@ void ASTConverter::convertExecCallArg( convertExecCallArgs(CE, Prelude, InnerArgs); std::string Tmp = "__nested_" + std::to_string(++NestedCallId); Prelude.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(InnerArgs), Tmp, E->getExprLoc(), false)); Out = convertCallResultValue( Tmp, Callee->getReturnType(), @@ -6678,7 +6724,7 @@ bool ASTConverter::rejectOwnObjectUse(const Expr *E) { const FunctionDecl *Callee = ownObjectCallee(E); if (!Callee) return false; - error(CurrentFn->Name + ": the reference " + Callee->getNameAsString() + + error(CurrentFn->Name + ": the reference " + functionName(Callee) + " returns is not used yet; call it as a statement of its own"); return true; } @@ -7230,7 +7276,7 @@ ASTConverter::convertStmtBody(const Stmt *S) { : ""; CurrentFn->UsesDynamicStorage |= TrackOwnedResult; Out.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), ReturnsVoid ? "" : Tmp, RS->getBeginLoc(), false, Provenance)); auto Result = convertCallResultValue(Tmp, Callee->getReturnType(), @@ -7627,12 +7673,12 @@ ASTConverter::convertStmtBody(const Stmt *S) { convertExecCallArgs(CE, Out, Args); bool IsProof = calleeIsProof(Callee); Out.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), "", CE->getExprLoc(), IsProof)); } else { error(CurrentFn->Name + ": call to function without a verification contract: " + - Callee->getNameAsString()); + functionName(Callee)); } } else { error(CurrentFn->Name + ": indirect function calls are unsupported"); @@ -7852,7 +7898,7 @@ ASTConverter::convertStmtBody(const Stmt *S) { const std::string &Provenance = DynamicPointerProvenanceVariables.at(DirectTarget); Out.push_back(std::make_unique( - PointerCallee->getNameAsString(), functionIdentity(PointerCallee), + functionName(PointerCallee), functionIdentity(PointerCallee), std::move(Args), valueName(DirectTarget), BO->getExprLoc(), false, Provenance)); CurrentFn->UsesDynamicStorage = true; @@ -7887,7 +7933,7 @@ ASTConverter::convertStmtBody(const Stmt *S) { std::vector> Args; convertExecCallArgs(Call, Out, Args); Out.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), valueName(Target), BO->getExprLoc(), false)); markInitialized(Target); return Out; @@ -7913,7 +7959,7 @@ ASTConverter::convertStmtBody(const Stmt *S) { const std::string Tmp = "__assignment_call_" + std::to_string(++NestedCallId); Out.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), Tmp, BO->getExprLoc(), false)); VType Target = VType::fromQualType(BO->getLHS()->getType(), IntMode, Ctx); @@ -8067,7 +8113,7 @@ ASTConverter::convertStmtBody(const Stmt *S) { const std::string ResultTarget = "__local_call_" + std::to_string(++NestedCallId); Out.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), ResultTarget, VD->getBeginLoc(), calleeIsProof(Callee))); Initializer = convertCallResultValue( @@ -8222,7 +8268,7 @@ ASTConverter::convertStmtBody(const Stmt *S) { const std::string &Provenance = DynamicPointerProvenanceVariables.at(VD); Out.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), valueName(VD), VD->getBeginLoc(), false, Provenance)); CurrentFn->UsesDynamicStorage = true; @@ -8275,7 +8321,7 @@ ASTConverter::convertStmtBody(const Stmt *S) { RecordResult ? VD->getNameAsString() : "__local_call_" + std::to_string(++NestedCallId); Out.push_back(std::make_unique( - Callee->getNameAsString(), functionIdentity(Callee), + functionName(Callee), functionIdentity(Callee), std::move(Args), ResultTarget, VD->getBeginLoc(), calleeIsProof(Callee))); if (!RecordResult) { From 246d2b499dc990931e7e43e8ac2bb8cef3685b7f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:00:59 +0530 Subject: [PATCH 24/48] verify: Note where a specialization is instantiated after its errors and warnings. --- clang/lib/Verify/Driver/Verifier.cpp | 47 ++++++++++++++++++++++++++++ 1 file changed, 47 insertions(+) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 00ff4c3233..06d43a9b10 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -2790,6 +2790,23 @@ class Verifier { llvm::raw_ostream *DumpOS = nullptr; std::vector Diags; std::optional Lean; + /// Where each template specialization verified is instantiated, and what + /// it is, by its function's name. + std::map> + InstantiationPoints; + + /// The instantiation a diagnostic about a template specialization is + /// about, which a compiler notes after an error or a warning. + const std::pair * + instantiationOf(const VerifyDiagnostic &D) const { + if ((D.K != VerifyDiagnostic::Error && D.K != VerifyDiagnostic::Warning) || + (D.Loc.isInvalid() && D.Span.isInvalid())) + return nullptr; + auto It = InstantiationPoints.find(D.FunctionName); + if (It == InstantiationPoints.end() || It->second.first.isInvalid()) + return nullptr; + return &It->second; + } void reportLeanWarnings() { for (std::string &Warning : Lean->takeWarnings()) @@ -3081,6 +3098,7 @@ class Verifier { Converter.getUnverifiedCallers(); for (const auto &[Loc, Message] : Converter.getWarnings()) Diags.push_back({VerifyDiagnostic::Warning, Message, Loc}); + InstantiationPoints = Converter.getInstantiationPoints(); // A construct the verifier does not represent costs its function alone: // the function is Unresolved, its first error carrying the verdict, and // the rest of the translation unit is verified. An error outside every @@ -5564,6 +5582,17 @@ class Verifier { } if (Source.isValid()) Record["source"] = sourceJSON(Source); + if (const std::pair *Instantiation = + instantiationOf(D)) + if (PresumedLoc Point = + Ctx.getSourceManager().getPresumedLoc(Instantiation->first); + Point.isValid()) { + ObligationSource At; + At.File = Point.getFilename(); + At.Line = At.EndLine = Point.getLine(); + At.Column = At.EndColumn = Point.getColumn(); + Record["instantiated_at"] = sourceJSON(At); + } if (D.Vacuous) Record["vacuous"] = true; @@ -5736,6 +5765,12 @@ class Verifier { printJSONDiagnostic(D, OS); continue; } + const std::pair *Instantiation = + instantiationOf(D); + const std::string InstantiationNote = + Instantiation ? "in instantiation of " + Instantiation->second + + " '" + D.FunctionName + "' requested here" + : std::string(); if (D.K == VerifyDiagnostic::Error && D.Span.isValid()) { DiagnosticOptions DiagOpts; DiagOpts.ShowPresumedLoc = true; @@ -5744,6 +5779,10 @@ class Verifier { FullSourceLoc(D.Span.getBegin(), Ctx.getSourceManager()), DiagnosticsEngine::Error, D.Message, CharSourceRange::getTokenRange(D.Span), {}); + if (Instantiation) + Text.emitDiagnostic( + FullSourceLoc(Instantiation->first, Ctx.getSourceManager()), + DiagnosticsEngine::Note, InstantiationNote, {}, {}); continue; } if (D.Loc.isValid()) { @@ -5799,6 +5838,14 @@ class Verifier { OS << "warning: " << D.Message << "\n"; break; } + if (Instantiation) { + PresumedLoc PLoc = + Ctx.getSourceManager().getPresumedLoc(Instantiation->first); + if (PLoc.isValid()) + OS << PLoc.getFilename() << ":" << PLoc.getLine() << ":" + << PLoc.getColumn() << ": "; + OS << "note: " << InstantiationNote << "\n"; + } } } }; From cca2982d7d65b1764ea2c2f577cfdd491f73eb42 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:00 +0530 Subject: [PATCH 25/48] test: Check function templates verified in each specialization. --- .../test/Verify/suite/function_templates.cpp | 349 ++++++++++++++++++ 1 file changed, 349 insertions(+) create mode 100644 clang/test/Verify/suite/function_templates.cpp diff --git a/clang/test/Verify/suite/function_templates.cpp b/clang/test/Verify/suite/function_templates.cpp new file mode 100644 index 0000000000..9c8a27a228 --- /dev/null +++ b/clang/test/Verify/suite/function_templates.cpp @@ -0,0 +1,349 @@ +// RUN: not %cpp-verify --jobs=1 %s -- > %t 2>&1 +// RUN: FileCheck %s < %t +// RUN: FileCheck %s --check-prefix=NOTE < %t +// RUN: FileCheck %s --check-prefix=CONVERSION < %t +// RUN: FileCheck %s --check-prefix=SOUND < %t +// RUN: grep -c "Verified: half" %t | FileCheck %s --check-prefix=ONCE +// RUN: not %cpp-verify --lower-only --dump-ir=3 %s -- 2>&1 | FileCheck %s --check-prefix=VC +// RUN: not %cpp-verify --jobs=1 --diagnostics-format=json %s -- 2>/dev/null | FileCheck %s --check-prefix=JSON +// +// A function template is verified in each of its specializations, with its +// contract instantiated as its body is: what it means depends on its +// arguments. A diagnostic about a specialization notes where it is +// instantiated, as a compiler's does. +// +// No proof here holds only because no execution reaches its end. +// SOUND-NOT: vacuous + +template +T maxv(T a, T b) + cppverify::post(cppverify::result >= a && cppverify::result >= b) + cppverify::post(cppverify::result == a || cppverify::result == b) +{ + return a < b ? b : a; +} + +int bigger(int x, int y) + cppverify::post(cppverify::result >= x) +{ + int m = maxv(x, y); + return m; +} +// CHECK-DAG: Verified: maxv [backend=z3] +// CHECK-DAG: Verified: bigger [backend=z3] + +// An explicit instantiation is verified with no caller. +template long maxv(long, long); +// CHECK-DAG: Verified: maxv [backend=z3] + +// One instantiation may fail where another holds: 2 * 100 is no signed char. +template +T twice(T x) + cppverify::pre(0 <= x && x <= 100) + cppverify::post(cppverify::result == 2 * x) +{ + return x + x; +} + +int twice_int(int x) + cppverify::pre(0 <= x && x <= 100) +{ + int r = twice(x); + return r; +} + +signed char twice_char(signed char x) + cppverify::pre(0 <= x && x <= 100) +{ + signed char r = twice(x); + return r; +} +// CHECK-DAG: Verified: twice [backend=z3] +// CHECK-DAG: Verified: twice_int [backend=z3] +// CHECK-DAG: error: verification failed: twice [{{.*}}::postcondition@[[@LINE-20]]:{{.*}} x [ssa=x_0] [type=i8] = {{6[4-9]|[7-9][0-9]|100}} +// CHECK-DAG: Unresolved: twice_char [backend=z3] [reason=callee.contract] (relies on the contract of twice, which is not established) +// NOTE: error: verification failed: twice +// NOTE-NEXT: function_templates.cpp:[[@LINE-8]]:19: note: in instantiation of function template specialization 'twice' requested here +// JSON: "function":"twice","instantiated_at":{"column":19,"end_column":19,"end_line":[[@LINE-9]],"file":"{{.*}}function_templates.cpp","line":[[@LINE-9]]} + +// A recursive template calls its own specialization. +template +T sum_to(T n) + cppverify::pre(0 <= n && n <= 1000) + cppverify::post(cppverify::result == n * (n + 1) / 2) + cppverify::decreases(n) +{ + if (n == 0) + return 0; + T r = sum_to(n - 1); + return r + n; +} + +int sum_ten() + cppverify::post(cppverify::result == 55) +{ + int s = sum_to(10); + return s; +} +// CHECK-DAG: Verified: sum_to [backend=z3] +// CHECK-DAG: Verified: sum_ten [backend=z3] + +// A contract over the template's types. +template +int bits() + cppverify::post(cppverify::result == 8 * (int)sizeof(T)) +{ + return 8 * (int)sizeof(T); +} + +int widths() + cppverify::post(cppverify::result == 80) +{ + int a = bits(); + int b = bits(); + return a + b; +} +// CHECK-DAG: Verified: bits [backend=z3] +// CHECK-DAG: Verified: bits [backend=z3] +// CHECK-DAG: Verified: widths [backend=z3] + +// A loop contract, instantiated with the body: a short total wraps. +template +T total(const T *p, int n) + cppverify::pre(cppverify::valid(p, n) && 0 <= n && n <= 100) + cppverify::pre(cppverify::forall(k, 0, n, 0 <= p[k] && p[k] <= 1000)) + cppverify::post(0 <= cppverify::result && cppverify::result <= 1000 * n) +{ + T s = 0; + for (int i = 0; i < n; i = i + 1) + cppverify::invariant(0 <= i && i <= n) + cppverify::invariant(0 <= s && s <= 1000 * i) + cppverify::decreases(n - i) + { + s = s + p[i]; + } + return s; +} + +int total_int(const int *p, int n) + cppverify::pre(cppverify::valid(p, n) && 0 <= n && n <= 100) + cppverify::pre(cppverify::forall(k, 0, n, 0 <= p[k] && p[k] <= 1000)) + cppverify::post(cppverify::result <= 100000) +{ + int t = total(p, n); + return t; +} + +short total_short(const short *p, int n) + cppverify::pre(cppverify::valid(p, n) && 0 <= n && n <= 100) + cppverify::pre(cppverify::forall(k, 0, n, 0 <= p[k] && p[k] <= 1000)) +{ + short t = total(p, n); + return t; +} +// CHECK-DAG: Verified: total [backend=z3] +// CHECK-DAG: Verified: total_int [backend=z3] +// CHECK-DAG: error: verification failed: total [{{.*}}::invariant-preserved@ +// CHECK-DAG: Unresolved: total_short [backend=z3] [reason=callee.contract] +// NOTE: error: verification failed: total +// NOTE-NEXT: function_templates.cpp:[[@LINE-8]]:13: note: in instantiation of function template specialization 'total' requested here + +// Ghost code of a template's types: the ghost variable stays one. +template +T bump(T x) + cppverify::pre(0 <= x && x < 100) + cppverify::post(cppverify::result == x + 1) +{ + cppverify::ghost T before = 0; + cppverify::ghost { before = x; } + x = x + 1; + cppverify::check(x == before + 1); + return x; +} + +int bump_int(int x) + cppverify::pre(0 <= x && x < 100) + cppverify::post(cppverify::result == x + 1) +{ + int y = bump(x); + return y; +} +// CHECK-DAG: Verified: bump [backend=z3] +// CHECK-DAG: Verified: bump_int [backend=z3] + +// A spec template, applied in another template's contract. +template +cppverify::spec bool between(T lo, T x, T hi) { return lo <= x && x <= hi; } + +template +T clamp(T x, T lo, T hi) + cppverify::pre(lo <= hi) + cppverify::post(between(lo, cppverify::result, hi)) +{ + if (x < lo) + return lo; + if (hi < x) + return hi; + return x; +} + +int clamped(int x) + cppverify::post(0 <= cppverify::result && cppverify::result <= 10) +{ + int c = clamp(x, 0, 10); + return c; +} +// CHECK-DAG: Verified: spec axiom: between +// CHECK-DAG: Verified: clamp [backend=z3] +// CHECK-DAG: Verified: clamped [backend=z3] + +// A contract written on a declaration, the definition after it. +template +T half(T x) + cppverify::pre(x >= 0) + cppverify::post(2 * cppverify::result <= x); + +template +T half(T x) +{ + return x / 2; +} + +int halved(int x) + cppverify::pre(x >= 0) + cppverify::post(cppverify::result <= x) +{ + int h = half(x); + return h; +} +// CHECK-DAG: Verified: half [backend=z3] +// CHECK-DAG: Verified: halved [backend=z3] +// ONCE: 1 + +// A member function template. +struct Meter { + int level; + + template + void add(T d) + cppverify::pre(0 <= d && d <= 100 && 0 <= level && level <= 1000) + cppverify::modifies(level) + cppverify::post(level == cppverify::old(level) + d) + { + level = level + d; + } +}; + +int metered() + cppverify::post(cppverify::result == 8) +{ + Meter m; + m.level = 0; + m.add(5); + m.add((short)3); + return m.level; +} +// CHECK-DAG: Verified: Meter::add [backend=z3] +// CHECK-DAG: Verified: Meter::add [backend=z3] +// CHECK-DAG: Verified: metered [backend=z3] + +// A specialization the verifier cannot represent fails alone. +double fractional() { return maxv(1.5, 2.5); } +// CHECK-DAG: error: maxv: unsupported C++ type in verification: double +// CONVERSION: error: maxv: unsupported C++ type in verification: double +// CONVERSION: function_templates.cpp:[[@LINE-3]]:30: note: in instantiation of function template specialization 'maxv' requested here + +// Never instantiated: not verified. +template +T unused(T x) + cppverify::post(cppverify::result == x) +{ + return x; +} +// CHECK-DAG: function_templates.cpp:[[@LINE-5]]:3: warning: unused: function template is not verified: this translation unit instantiates none of its specializations + +// A trusted template declared without a definition: its contract is +// instantiated where it is used. +template +[[cppverify::trusted]] T next_of(T x) + cppverify::pre(x < 100) + cppverify::post(cppverify::result == x + 1); + +int uses_next() + cppverify::post(cppverify::result == 6) +{ + int r = next_of(5); + return r; +} +// CHECK-DAG: Trusted: next_of (contract assumed, not verified) +// CHECK-DAG: Verified: uses_next [backend=z3] [trusts=next_of] + +// cppverify::result of the template's type, compared with a constant. +template +T magnitude(T x) + cppverify::pre(x > -1000 && x < 1000) + cppverify::post(cppverify::result >= 0) +{ + return x < 0 ? -x : x; +} + +int uses_magnitude(int x) + cppverify::pre(x > -1000 && x < 1000) + cppverify::post(cppverify::result >= 0) +{ + int m = magnitude(x); + return m; +} +// CHECK-DAG: Verified: magnitude [backend=z3] +// CHECK-DAG: Verified: uses_magnitude [backend=z3] + +// A loop whose condition and body do not change with the template's +// arguments still gets its instantiated contract. +template +int size_of() + cppverify::post(cppverify::result == (int)sizeof(T)) +{ + while (false) + cppverify::invariant(sizeof(T) >= 1) + { + } + return (int)sizeof(T); +} + +int sizes() + cppverify::post(cppverify::result == 6) +{ + int s = size_of(); + int i = size_of(); + return s + i; +} +// CHECK-DAG: Verified: size_of [backend=z3] +// CHECK-DAG: Verified: size_of [backend=z3] +// CHECK-DAG: Verified: sizes [backend=z3] + +// A trigger stays one in each specialization. +template +T first_positive(const T *a, int n) + cppverify::pre(cppverify::valid(a, n) && 0 < n) + cppverify::pre(cppverify::forall(k, 0, n, cppverify::trigger(a[k]) > 0)) + cppverify::post(cppverify::result > 0) +{ + T v = a[0]; + return v; +} + +int first_int(const int *a, int n) + cppverify::pre(cppverify::valid(a, n) && 0 < n) + cppverify::pre(cppverify::forall(k, 0, n, a[k] > 0)) + cppverify::post(cppverify::result > 0) +{ + int v = first_positive(a, n); + return v; +} +// CHECK-DAG: Verified: first_positive [backend=z3] +// CHECK-DAG: Verified: first_int [backend=z3] +// VC-LABEL: vc first_positive +// VC: forall +// VC: trigger +// VC-NEXT: heap_select +// VC-LABEL: vc first_int From 694cb5672a5a058b25b94b5e42fb3df54850addb Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:00 +0530 Subject: [PATCH 26/48] test: Check that a function template's contract is checked where it is instantiated. --- .../test/Verify/template_contract_errors.cpp | 112 ++++++++++++++++++ 1 file changed, 112 insertions(+) create mode 100644 clang/test/Verify/template_contract_errors.cpp diff --git a/clang/test/Verify/template_contract_errors.cpp b/clang/test/Verify/template_contract_errors.cpp new file mode 100644 index 0000000000..f72dc05954 --- /dev/null +++ b/clang/test/Verify/template_contract_errors.cpp @@ -0,0 +1,112 @@ +// RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -verify %s +// +// A function template's contract is checked where it is instantiated, as its +// body is, so an error names the specialization. A template whose contract +// some arguments would break is no error until one of them is used. + +struct Pair { + int first; + int second; +}; + +template +int first_of(T v) + cppverify::post(cppverify::result == v.first) // expected-error {{member reference base type 'int' is not a structure or union}} +{ + return 0; +} + +int uses_first() { + Pair p{1, 2}; + return first_of(p) + first_of(3); // expected-note {{in instantiation of function template specialization 'first_of' requested here}} +} + +template +void needs(T v) + cppverify::pre(v) // expected-error {{value of type 'Pair' is not contextually convertible to 'bool'}} +{ +} + +void uses_needs() { + needs(1); + needs(Pair{1, 2}); // expected-note {{in instantiation of function template specialization 'needs' requested here}} +} + +template +int steps(T p) + cppverify::decreases(p) // expected-error {{decreases expression must have integer type}} +{ + return 0; +} + +int uses_steps() { + int x = 0; + return steps(1) + steps(&x); // expected-note {{in instantiation of function template specialization 'steps' requested here}} +} + +template +bool all_below(const int *p, T n) + cppverify::pre(cppverify::forall(k, 0, n, p[k] < 10)) // expected-error {{quantifier bound must have integer type}} +{ + return true; +} + +bool uses_all_below(const int *p) { + return all_below(p, 3) && all_below(p, 2.5); // expected-note {{in instantiation of function template specialization 'all_below' requested here}} +} + +template +void fills(T *p, T n) + cppverify::modifies(p[0 : n]) // expected-error {{a modifies range length must have integer type}} +{ +} + +void uses_fills(int *p, double *q) { + fills(p, 2); + fills(q, 2.0); // expected-note {{in instantiation of function template specialization 'fills' requested here}} +} + +// In the body, an assertion and a loop invariant are conditions too. +template +void asserts(T v) { + cppverify::check(v); // expected-error {{value of type 'Pair' is not contextually convertible to 'bool'}} +} + +template +void loops(T v) { + for (int i = 0; i < 3; i = i + 1) + cppverify::invariant(v) // expected-error {{value of type 'Pair' is not contextually convertible to 'bool'}} + cppverify::decreases(3 - i) + { + } +} + +void uses_body() { + asserts(1); + asserts(Pair{1, 2}); // expected-note {{in instantiation of function template specialization 'asserts' requested here}} + loops(1); + loops(Pair{1, 2}); // expected-note {{in instantiation of function template specialization 'loops' requested here}} +} + +// Used only with arguments its contract fits. +template +int only_records(T v) + cppverify::post(cppverify::result == v.first) +{ + return v.first; +} + +int uses_only_records() { + Pair p{1, 2}; + return only_records(p); +} + +// An unevaluated use asks for no contract. +template +int records_only(T v) + cppverify::post(cppverify::result == v.first) +{ + return v.first; +} + +using Unevaluated = decltype(records_only(3)); From 0a34abb550e354922fd715fb8ec210b149436f99 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:00 +0530 Subject: [PATCH 27/48] test: Expect function template contracts kept, and result and old of a template's type compared with a constant. --- clang/test/Verify/template_contracts.cpp | 27 +++++++++++++++++------- 1 file changed, 19 insertions(+), 8 deletions(-) diff --git a/clang/test/Verify/template_contracts.cpp b/clang/test/Verify/template_contracts.cpp index 4f0da96225..41bbc0464d 100644 --- a/clang/test/Verify/template_contracts.cpp +++ b/clang/test/Verify/template_contracts.cpp @@ -2,12 +2,13 @@ // RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -emit-llvm -o - %s | FileCheck %s // // A contract may depend on a template parameter: it is checked where it is -// instantiated, as C++ conditions are. Templates are not verified yet, so the -// contracts of a function or class template are ignored with a warning, and -// the template compiles and instantiates like any other. +// instantiated, as C++ conditions are. A function template's contract is +// instantiated with each specialization; the contracts of a class template +// are not verified yet and are ignored with a warning. Either compiles and +// instantiates like any other template. template -T clamp_low(T v, T lo) // expected-warning {{contracts in function template 'clamp_low' are not yet supported and are ignored}} +T clamp_low(T v, T lo) cppverify::pre(lo <= v || v < lo) cppverify::post(cppverify::result >= lo) { @@ -15,11 +16,11 @@ T clamp_low(T v, T lo) // expected-warning {{contracts in function template 'cla } template -T sum_to(T n) // expected-warning {{contracts in function template 'sum_to' are not yet supported and are ignored}} +T sum_to(T n) cppverify::pre(n >= 0) { T total = 0; - for (T i = 0; i < n; i = i + 1) // expected-warning {{contracts in function template 'sum_to' are not yet supported and are ignored}} + for (T i = 0; i < n; i = i + 1) cppverify::invariant(0 <= i && i <= n) cppverify::decreases(n - i) { @@ -29,7 +30,7 @@ T sum_to(T n) // expected-warning {{contracts in function template 'sum_to' are } template -void fill(T *p, T n, T v) // expected-warning {{contracts in function template 'fill' are not yet supported and are ignored}} +void fill(T *p, T n, T v) cppverify::modifies(p[0 : n]) { for (T i = 0; i < n; i = i + 1) @@ -48,6 +49,15 @@ struct Box { } }; +template +T positive(T v) + cppverify::pre(v > 0) + cppverify::post(cppverify::result > 0) + cppverify::post(cppverify::old(v) > 0 && cppverify::result == v) +{ + return v; +} + template T checked(T n) { @@ -78,7 +88,7 @@ int use() { fill(buffer, 2, 7); Box b{3}; return clamp_low(1, 2) + b.get() + sum_to(4) + sum_to(4L) + checked(5) + - quantified(6); + quantified(6) + positive(7); } // CHECK-DAG: define {{.*}} @_Z9clamp_lowIiET_S0_S0_( @@ -86,6 +96,7 @@ int use() { // CHECK-DAG: define {{.*}} @_Z6sum_toIlET_S0_( // CHECK-DAG: define {{.*}} @_Z4fillIiEvPT_S0_S0_( // CHECK-DAG: define {{.*}} @_ZNK3BoxIiE3getEv( +// CHECK-DAG: define {{.*}} @_Z8positiveIiET_S0_( // CHECK-DAG: define {{.*}} @_Z7checkedIiET_S0_( // CHECK-DAG: define {{.*}} @_Z10quantifiedIiET_S0_( // CHECK-DAG: define {{.*}} @_ZZ10quantifiedIiET_S0_ENKUlS0_E_clIiEEDaS0_( From 9f4a7325e2d985c5ce75fd9498569bdd877934c3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:01 +0530 Subject: [PATCH 28/48] test: Expect a warning for a contracted template that nothing instantiates. --- clang/test/Verify/suite/unused_template.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/clang/test/Verify/suite/unused_template.cpp b/clang/test/Verify/suite/unused_template.cpp index 820aa7100e..2567bc2396 100644 --- a/clang/test/Verify/suite/unused_template.cpp +++ b/clang/test/Verify/suite/unused_template.cpp @@ -1,10 +1,11 @@ // RUN: %cpp-verify %s -- 2>&1 | FileCheck %s --implicit-check-not=error: // RUN: not %cpp-verify %s -- -DCALL 2>&1 | FileCheck %s --check-prefix=CALL -// RUN: not %cpp-verify %s -- -DSTATEMENT 2>&1 | FileCheck %s --check-prefix=STATEMENT +// RUN: %cpp-verify %s -- -DSTATEMENT 2>&1 | FileCheck %s --check-prefix=STATEMENT // // A function template without contracts is not verified, and stops nothing // unless verified code calls it: that call is reported. One with contract -// statements is reported, as one with contracts is. +// statements, as one with contracts, is verified in its specializations, and +// one that nothing instantiates is reported, not verified. template T twice(T v) { return v + v; } @@ -24,7 +25,7 @@ int uses_twice(int x) return twice(x); } #endif -// CALL: error: uses_twice: call to function without a verification contract: twice +// CALL: error: uses_twice: call to function without a verification contract: twice // CALL-NOT: function template verification #ifdef STATEMENT @@ -34,4 +35,4 @@ template T checked(T v) return v; } #endif -// STATEMENT: error: checked: function template verification is unsupported +// STATEMENT: warning: checked: function template is not verified: this translation unit instantiates none of its specializations From fa8f9440aab1255cd7c56484ac73135d11011dca Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:01 +0530 Subject: [PATCH 29/48] test: Expect the warning for an uninstantiated contracted template. --- clang/test/Verify/suite/z3_calls_fail_closed.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/z3_calls_fail_closed.cpp b/clang/test/Verify/suite/z3_calls_fail_closed.cpp index 071427a235..2f5272b7dd 100644 --- a/clang/test/Verify/suite/z3_calls_fail_closed.cpp +++ b/clang/test/Verify/suite/z3_calls_fail_closed.cpp @@ -103,4 +103,4 @@ int unsupported_recursive_exec(int n) // VERIFY-DAG: error: unsupported_conditionless_for: conditionless for loops are unsupported // VERIFY-DAG: error: unsupported_cross_type_alias: aliases between different pointee types are unsupported // VERIFY-DAG: error: unsupported_recursive_exec: recursive executable functions require decreases -// VERIFY-DAG: warning: contracts in function template 'unsupported_template' are not yet supported and are ignored +// VERIFY-DAG: warning: unsupported_template: function template is not verified: this translation unit instantiates none of its specializations From 83bbad98fe1dfcfda1b454980b68f60f88ca0c50 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:01 +0530 Subject: [PATCH 30/48] docs: Describe function templates verified in each specialization. --- website/source/language/functions-loops.rst | 98 ++++++++++++++------- 1 file changed, 68 insertions(+), 30 deletions(-) diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index 1c585c9cd4..e90472ce71 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -221,50 +221,88 @@ Spec functions stay total, as in Verus and ACSL: a spec's division by zero is Templates --------- -Templates compile with contracts, but they are not verified yet (member -functions of ordinary classes are; see :doc:`structs`): +A function template is verified in each of its specializations, as Kani and +CBMC verify the code a program instantiates: its contract is instantiated +with its body, so the contract and every check of the body are about the +template's arguments, and each specialization gets a verdict of its own, +named with its arguments. -- The contracts of a function template, of a class template's members, and a - class template's type invariants compile, instantiate with the template, - and are ignored, with a ``-Wcontract-unsupported`` warning that names the - template. -- A template without contracts changes nothing for the rest of the file, as - long as verified code does not call it. +.. cppverify-example: fails twice .. code-block:: cpp template - T clamp_low(T v, T lo) - cv::post(cv::result >= lo) + T twice(T x) + cv::pre(0 <= x && x <= 30000) + cv::post(cv::result == 2 * x) { - return v < lo ? lo : v; + return x + x; } - int clamp_int(int v) - cv::post(cv::result >= 0) + int twice_int(int x) + cv::pre(0 <= x && x <= 30000) + cv::post(cv::result == 2 * x) { - return v < 0 ? 0 : v; + int r = twice(x); + return r; } -.. code-block:: text - - templates.cpp:2:3: warning: contracts in function template 'clamp_low' are not yet supported and are ignored [-Wcontract-unsupported] - 2 | T clamp_low(T v, T lo) - | ^ - Verified: clamp_int [backend=z3] + short twice_short(short x) + cv::pre(0 <= x && x <= 30000) + { + short r = twice(x); + return r; + } -Two uses still stop the file with an error, and no function in it gets a -verdict: +.. code-block:: text -- a call to a template from verified code, such as ``return clamp_low(v, - 0);`` in a function with a contract: ``error: use: call to function - without a verification contract: clamp_low``; -- a template whose body has a contract statement (``cv::check``, a ghost - block): ``error: twice: function template verification is unsupported``. + Verified: twice [backend=z3] + templates.cpp:4:23: error: verification failed: twice [...::postcondition@4:23] (counterexample: ...) [backend=z3] [reason=counterexample] + templates.cpp:20:13: note: in instantiation of function template specialization 'twice' requested here + Verified: twice_int [backend=z3] + Unresolved: twice_short [backend=z3] [reason=callee.contract] (relies on the contract of twice, which is not established) + +``x + x`` is an ``int``, which a ``short`` result holds only up to 32767: +``twice`` fails, and the function that relies on it is unresolved. + +- A specialization is verified where the translation unit instantiates it, + by a call or by an explicit instantiation (``template long + twice(long);``). A function template with a contract that nothing + instantiates is reported, not verified: ``warning: f: function template is + not verified: this translation unit instantiates none of its + specializations``. What a template means depends on the types and + overloads its arguments bring, which C++ fixes only where it is + instantiated. +- A diagnostic about a specialization notes where it is instantiated, as a + compiler's does (JSON ``instantiated_at``). +- The contract is checked where it is instantiated, as a C++ condition is: a + clause that does not fit the arguments, such as ``cv::post(cv::result == + v.first)`` for an ``int``, is a compiler error there, with Clang's ``in + instantiation of function template specialization`` note. Arguments the + contract fits are no error. +- Loop contracts, assertions, ghost code, quantifiers, and triggers are + instantiated with the body, and so are spec function templates and member + function templates of ordinary classes. A contract written on a + declaration holds for the definition after it, and a + ``[[cppverify::trusted]]`` template without a definition holds at every + call of its specializations. +- A specialization the verifier cannot represent (``maxv``) costs + that specialization alone, as a construct in any function does. +- The contracts of a class template's members and its type invariants are + not verified yet: they compile, instantiate with the template, and are + ignored, with a ``-Wcontract-unsupported`` warning that names the class + template. +- A template without contracts changes nothing for the rest of the file, as + long as verified code does not call it. -Before 0.2, a template whose contract depends on its parameters did not -compile (``value of type '' is not contextually convertible to -'bool'``), and a template without any contract, even one nothing calls, +Before 0.2, a function template's contracts were ignored with a warning, and +a call to one from verified code was ``call to function without a +verification contract``. A template whose contract depended on its +parameters did not compile (``value of type '' is not +contextually convertible to 'bool'``), nor did ``cv::result`` or +``cv::old(x)`` of the template's type compared with a constant +(``cv::post(cv::result > 0)``: ``invalid operands to binary expression ('T' +and 'int')``). A template without any contract, even one nothing calls, stopped the file with ``function template verification is unsupported``. Behaviors From 2fd37fec32434be2b8ae86916c6235ebd98abc85 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:02 +0530 Subject: [PATCH 31/48] docs: List function templates as supported and class template members as not yet. --- website/source/language/limitations.rst | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 62b31833b3..117a218135 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -158,17 +158,19 @@ C++ feature boundaries through a pointer (``Ring copy = *r;``). * - Functions - Free functions, member functions of classes without bases or virtual - functions (:doc:`structs`), overloads, namespaces, contracts, direct calls, and + functions (:doc:`structs`), function templates in each specialization + the translation unit instantiates (:doc:`functions-loops`), + overloads, namespaces, contracts, direct calls, and direct and mutual recursion, also through stores to pointer and reference parameters and through automatic objects, with mutual recursion among functions of one kind (spec, proof, or executable). - Virtual functions, member functions of classes with bases, destructors, delegating constructors and the other constructors :doc:`structs` lists, conversion functions, - templates (one without contracts stops nothing unless verified code - calls it; the contracts of a function or class template compile, - instantiate, and are ignored with a warning, and one with contract - statements is reported), variadics, indirect calls, recursion through a + members and type invariants of class templates (they compile, + instantiate, and are ignored with a warning), function templates + that nothing instantiates (reported), variadics, indirect calls, + recursion through a function that allocates or frees storage, and general link-time summaries. * - Storage From af8645d8ccb1733aa9003b829419635435a44974 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:02 +0530 Subject: [PATCH 32/48] docs: Note function templates in the release notes. --- website/source/release-notes.rst | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index e4c6efbc04..7074ae35da 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -336,6 +336,17 @@ on entry. An object passed by reference or pointer satisfies it on entry and, when mutable, at exit, where before only a record passed by value did (:doc:`language/structs`). +**Function templates.** A function template's contracts were ignored with +a warning, so no specialization was verified, and a call to one from +verified code was an error. Each specialization a translation unit +instantiates is now verified as a function of its own, named with its +arguments (``twice``), with its contract instantiated as its body is, +loop contracts, assertions, and ghost code included; a diagnostic about it +notes where it is instantiated, and a contracted template that nothing +instantiates is reported. ``cv::post(cv::result > 0)`` and ``cv::old(x) > 0`` +of a template's type did not compile (``invalid operands to binary +expression ('T' and 'int')``) (:doc:`language/functions-loops`). + **Member operators.** For a member ``operator==``, ``a == b`` passed ``a`` for the operator's parameter and ``b`` as an argument beyond it, an error, and an operator returning ``*this`` by reference (``Money &operator+=``) was From e39b949f1f1a6425b68bfef883af247a8ee074f4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:03 +0530 Subject: [PATCH 33/48] docs: Design function templates verified per instantiation. --- docs/DESIGN.md | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index b4b092e8de..ff287e8418 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1817,6 +1817,31 @@ cppverify::proof void sum_concat(seq s, seq t) mirror of vstd states each operation for its ladder; Lean's evaluation of every operation agrees with the certifier's. +## Templates + +- A function template is verified in each specialization the translation + unit instantiates, by a use or by an explicit instantiation, as a function + of its own named with its arguments (`maxv`). What a template means + depends on the types and overloads its arguments bring, which C++ fixes + only at instantiation, so an uninstantiated template is not verified (the + position of Kani and CBMC; Creusot and Prusti verify generic Rust once, + since trait bounds fix its meaning there). A contracted template that + nothing instantiates is reported. +- Its contract is instantiated as its body is, and lazily, as an exception + specification is: where a specialization is used or its definition + instantiated, never for a specialization nothing uses. Each clause gets + the checks the parser gives it (a condition converts to `bool`, a measure + is an integer, a range has integer bounds), so a clause that does not fit + the arguments is a compiler error with Clang's instantiation note. +- Loop contracts, assertions, ghost code, quantifiers, and triggers are + instantiated with the body. A contract written on a declaration names its + parameters; a trusted template without a definition is trusted in each + specialization. +- A diagnostic about a specialization notes where it is instantiated, as a + compiler's does. +- Not yet: the members and type invariants of class templates, ignored with + `-Wcontract-unsupported`. + ## Clang Modification Details ### Construct recognition @@ -1927,6 +1952,8 @@ a one-line hook. results, and every operation). 12. A range `p[lo : n]` needs a pointer to a complete object type and integer bounds, and is valid only as a whole `cppverify::modifies` footprint. +13. In a template, a clause that depends on its parameters is checked where + it is instantiated, with the same rules. ### CodeGen Rules From 4551563b9df488355c7c319fd53ac2a793c6d21e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:01:03 +0530 Subject: [PATCH 34/48] docs: Describe contract instantiation and the converter's specializations. --- docs/ARCHITECTURE.md | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 3f53be5716..3fb1d2cc4d 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -308,6 +308,31 @@ const, postconditions. The record escape scan accepts a callee's own automatic allocation unless it is initialized with an address it must not keep. +**Function templates:** Sema keeps a function template's contract on its +pattern and instantiates it lazily, as an exception specification: +`Sema::InstantiateFunctionContract` runs where a specialization is odr-used +(`MarkFunctionReferenced`) and where its definition is instantiated, once +per specialization (its `FunctionContractInfo` is recorded first, so a use +in its own contract stops there), in a `LocalInstantiationScope` that maps +the parameters of the declaration the clauses are written on +(`ContractDecl`), with `this` for a member, in an evaluation context of its +own. `SubstFunctionContract` runs `TreeTransform::TransformFunctionContract`, +which rebuilds each clause with the checks the parser applies +(`TransformContractCondition`, `TransformContractMeasure`, +`TransformContractFootprint`; quantifiers and choices through +`Sema::BuildContractBinderExpr`). `TreeTransform` gives `cppverify::result` the +instantiated return type, transforms a loop's contract with the loop and +rebuilds a loop whose clauses changed even when its condition and body did +not, and keeps trigger marks; `BuildVariableInstantiation` keeps ghost +variables. `ResultExpr`, `OldExpr`, and the quantifiers take the dependence +of their type or operands. `collectFunctionCandidates` adds, after each +function template, the specializations the translation unit instantiates +(from its canonical declaration, whose redeclarations share them), with +their definition or, without one, their contract. The converter names them +with their arguments (`functionName`) and records where each is +instantiated (`getInstantiationPoints`), which the driver prints as a note +after each error or warning of the specialization (JSON `instantiated_at`). + **Records in memory by value:** `recordFieldsInMemory` reads a record value kept in memory, a promoted local or one in a pointee or record reference (`promotedRootLocal`, `inPointeeObject`), through implicit copies and From ac5f112a1f0f04e3c9f494a875c394ab6bc48823 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:03:37 +0530 Subject: [PATCH 35/48] test: Check a constexpr template lifted as a spec in each specialization. --- clang/test/Verify/suite/function_templates.cpp | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/clang/test/Verify/suite/function_templates.cpp b/clang/test/Verify/suite/function_templates.cpp index 9c8a27a228..c62ae5f2e2 100644 --- a/clang/test/Verify/suite/function_templates.cpp +++ b/clang/test/Verify/suite/function_templates.cpp @@ -347,3 +347,16 @@ int first_int(const int *a, int n) // VC: trigger // VC-NEXT: heap_select // VC-LABEL: vc first_int + +// An uncontracted constexpr template in a contract is a spec in each +// specialization, as a constexpr function is. +template +constexpr T bigger_of(T a, T b) { return a < b ? b : a; } + +int clamp3(int x) + cppverify::post(cppverify::result == bigger_of(x, 3)) +{ + return x < 3 ? 3 : x; +} +// CHECK-DAG: Verified: clamp3 [backend=z3] +// CHECK-DAG: Verified: constexpr spec axiom: bigger_of From 4c52295eb9192dcaea71a54ceb9979c5c40efb9b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:03:37 +0530 Subject: [PATCH 36/48] docs: Note that a constexpr template in a contract is a spec in each specialization. --- website/source/language/functions-loops.rst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index e90472ce71..14d57668cd 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -282,7 +282,9 @@ named with its arguments. contract fits are no error. - Loop contracts, assertions, ghost code, quantifiers, and triggers are instantiated with the body, and so are spec function templates and member - function templates of ordinary classes. A contract written on a + function templates of ordinary classes. An uncontracted ``constexpr`` + template that a contract applies is a spec in each specialization, as a + ``constexpr`` function is (see Functions above). A contract written on a declaration holds for the definition after it, and a ``[[cppverify::trusted]]`` template without a definition holds at every call of its specializations. From 22c332983088a7e644532d587fc6df5216788c0c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:24 +0530 Subject: [PATCH 37/48] verify: Give each instantiated quantifier and choice a scope of its own, so each element of a pack expansion binds its own variable. --- clang/lib/Sema/SemaTemplateInstantiate.cpp | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/clang/lib/Sema/SemaTemplateInstantiate.cpp b/clang/lib/Sema/SemaTemplateInstantiate.cpp index 8f757853c1..02c341c532 100644 --- a/clang/lib/Sema/SemaTemplateInstantiate.cpp +++ b/clang/lib/Sema/SemaTemplateInstantiate.cpp @@ -1793,6 +1793,21 @@ namespace { return AC; } + // A quantifier's or a choice's binder is its own local, as a lambda's + // are: each element of a pack expansion binds a variable of its own. + ExprResult TransformForallExpr(ForallExpr *E) { + LocalInstantiationScope Scope(SemaRef, /*CombineWithOuterScope=*/true); + return inherited::TransformForallExpr(E); + } + ExprResult TransformExistsExpr(ExistsExpr *E) { + LocalInstantiationScope Scope(SemaRef, /*CombineWithOuterScope=*/true); + return inherited::TransformExistsExpr(E); + } + ExprResult TransformContractChooseExpr(ContractChooseExpr *E) { + LocalInstantiationScope Scope(SemaRef, /*CombineWithOuterScope=*/true); + return inherited::TransformContractChooseExpr(E); + } + ExprResult TransformLambdaExpr(LambdaExpr *E) { // Do not rebuild lambdas to avoid creating a new type. // Lambdas have already been processed inside their eval contexts. From d890301c37ee0b28fdc78da8065250c6b4449826 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:24 +0530 Subject: [PATCH 38/48] verify: Keep a check-by block in the scope of its instantiated quantifier's variable. --- clang/lib/Sema/TreeTransform.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/clang/lib/Sema/TreeTransform.h b/clang/lib/Sema/TreeTransform.h index 4a3583ac12..5f5aa41e76 100644 --- a/clang/lib/Sema/TreeTransform.h +++ b/clang/lib/Sema/TreeTransform.h @@ -18387,6 +18387,12 @@ TreeTransform::TransformContractAssertStmt(ContractAssertStmt *S) { return StmtError(); StmtResult By = S->getBy(); if (S->getBy()) { + // check(forall(k, ...)) by { ... }: the block is in the scope of k. + if (const auto *Old = dyn_cast(S->getCond()->IgnoreImplicit())) + if (const auto *New = dyn_cast(Cond.get()->IgnoreImplicit()); + New && New->getBoundVar() != Old->getBoundVar()) + getDerived().transformedLocalDecl(Old->getBoundVar(), + {New->getBoundVar()}); By = getDerived().TransformStmt(S->getBy()); if (By.isInvalid()) return StmtError(); From d27059d079246aa87a44f3df2d3711f6a3168207 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:24 +0530 Subject: [PATCH 39/48] verify: Drop the this scope and ghost mark a specialization's context and the pattern's checks already give. --- clang/lib/Sema/SemaTemplateInstantiateDecl.cpp | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp b/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp index 9912c19027..2b3a4aad51 100644 --- a/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp +++ b/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp @@ -5471,14 +5471,9 @@ void Sema::InstantiateFunctionContract(SourceLocation PointOfInstantiation, MultiLevelTemplateArgumentList TemplateArgs = getTemplateInstantiationArgs( Function, Function->getLexicalDeclContext(), /*Final=*/false, /*Innermost=*/std::nullopt, /*RelativeToPrimary=*/true); + // A member's `this` is the specialization's, the current context. if (addInstantiatedParametersToScope(Function, Written, Scope, TemplateArgs)) return; - std::optional ThisScope; - if (auto *Method = dyn_cast(Function); - Method && Method->isImplicitObjectMemberFunction()) - ThisScope.emplace(*this, Method->getParent(), - Method->getMethodQualifiers(), - static_cast(getLangOpts().CPlusPlus11)); FunctionContractInfo Instantiated; if (SubstFunctionContract(*PatternContract, Instantiated, TemplateArgs)) return; @@ -6228,10 +6223,6 @@ void Sema::BuildVariableInstantiation( InstantiateAttrs(TemplateArgs, OldVar, NewVar, LateAttrs, StartingScope); - // A ghost variable is one in every instantiation. - if (Context.isGhostVariable(OldVar)) - Context.markGhostVariable(NewVar); - LookupResult Previous( *this, NewVar->getDeclName(), NewVar->getLocation(), NewVar->isLocalExternDecl() ? Sema::LookupRedeclarationWithLinkage From 24a3d15582f0b3f08c6256bfc1f4248686763a92 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:25 +0530 Subject: [PATCH 40/48] verify: Declare the naming of parameters, a pack's elements apart. --- clang/lib/Verify/Frontend/ASTConverter.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index 3878d3a1d2..cdb8defd6f 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -74,6 +74,11 @@ class ASTConverter { std::map> InstantiationPoints; std::map ParameterNames; + /// For a parameter a pack expands to, its index in the pack, `...[1]`. + std::map PackElements; + /// Names each parameter of \p FD after the declaration \p ContractDecl + /// whose contract names them. + void nameParameters(const FunctionDecl *ContractDecl, const FunctionDecl *FD); unsigned BoundValueId = 0; std::map FunctionIdentities; std::map SpecHeapReads; From fce5a9fcbbfd336d3ec7e5e037984f2bb1300753 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:25 +0530 Subject: [PATCH 41/48] verify: Name the parameters a pack expands to as C++26 indexes them. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 45 +++++++++++++++------- 1 file changed, 32 insertions(+), 13 deletions(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index 81ac6c1a41..d467cc2be1 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -1136,6 +1136,33 @@ ASTConverter::trackedValueNames(const ValueDecl *D) const { return Names; } +void ASTConverter::nameParameters(const FunctionDecl *ContractDecl, + const FunctionDecl *FD) { + ParameterNames.clear(); + PackElements.clear(); + // The parameters a pack expands to share its name, which no others can: + // each is named as C++26 indexes a pack, `ns...[1]`. + std::map Occurrences, Elements; + for (const ParmVarDecl *P : ContractDecl->parameters()) + ++Occurrences[P->getNameAsString()]; + for (unsigned I = 0; I < FD->getNumParams(); ++I) { + const ParmVarDecl *ContractParam = ContractDecl->getParamDecl(I); + const ParmVarDecl *DefinitionParam = FD->getParamDecl(I); + std::string Name = ContractParam->getNameAsString(); + std::string Element; + if (!Name.empty() && Occurrences[Name] > 1) + Element = "...[" + std::to_string(Elements[Name]++) + "]"; + if (Name.empty()) + Name = DefinitionParam->getNameAsString(); + if (Name.empty()) + Name = "__cppverify_param_" + std::to_string(I); + ParameterNames[ContractParam] = Name + Element; + ParameterNames[DefinitionParam] = Name + Element; + if (!Element.empty()) + PackElements[DefinitionParam] = Element; + } +} + std::string ASTConverter::valueName(const ValueDecl *D) const { if (const auto *P = dyn_cast_or_null(D)) if (auto It = ParameterNames.find(P); It != ParameterNames.end()) @@ -1148,6 +1175,9 @@ void ASTConverter::recordSourceVariable(const ValueDecl *D) { return; const std::string InternalBase = valueName(D); std::string DisplayBase = D->getNameAsString(); + if (const auto *P = dyn_cast(D)) + if (auto It = PackElements.find(P); It != PackElements.end()) + DisplayBase += It->second; if (DisplayBase.empty()) DisplayBase = InternalBase; auto Record = [&](std::string InternalName, std::string DisplayName, @@ -3020,23 +3050,12 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { } if (exceedsNestingLimit(FD, FCI)) return nullptr; - ParameterNames.clear(); const FunctionDecl *ContractDecl = FCI->ContractDecl ? FCI->ContractDecl : FD; if (ContractDecl->getNumParams() != FD->getNumParams()) { error(functionName(FD) + ": contract declaration parameter mismatch"); return nullptr; } - for (unsigned I = 0; I < FD->getNumParams(); ++I) { - const ParmVarDecl *ContractParam = ContractDecl->getParamDecl(I); - const ParmVarDecl *DefinitionParam = FD->getParamDecl(I); - std::string Name = ContractParam->getNameAsString(); - if (Name.empty()) - Name = DefinitionParam->getNameAsString(); - if (Name.empty()) - Name = "__cppverify_param_" + std::to_string(I); - ParameterNames[ContractParam] = Name; - ParameterNames[DefinitionParam] = Name; - } + nameParameters(ContractDecl, FD); if (FD->isVariadic()) { error(functionName(FD) + ": variadic functions are unsupported"); return nullptr; @@ -3844,7 +3863,7 @@ ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { llvm::SaveAndRestore OwnerName(ErrorFunctionName, functionName(FD)); llvm::SaveAndRestore InContract(ErrorInContract, true); const size_t ErrorsAtStart = Errors.size(); - ParameterNames.clear(); + nameParameters(FD, FD); if (exceedsNestingLimit(FD, functionContract(FD)) || hasIndirectMemoryAccess(FD)) return nullptr; From 4138ee0ced7367b9dd917cf2906f44092b12ddb3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:25 +0530 Subject: [PATCH 42/48] test: Check a contract on a definition after a declaration, and variadic templates. --- .../test/Verify/suite/function_templates.cpp | 60 ++++++++++++++++++- 1 file changed, 59 insertions(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/function_templates.cpp b/clang/test/Verify/suite/function_templates.cpp index c62ae5f2e2..48606a2948 100644 --- a/clang/test/Verify/suite/function_templates.cpp +++ b/clang/test/Verify/suite/function_templates.cpp @@ -148,7 +148,8 @@ short total_short(const short *p, int n) // NOTE: error: verification failed: total // NOTE-NEXT: function_templates.cpp:[[@LINE-8]]:13: note: in instantiation of function template specialization 'total' requested here -// Ghost code of a template's types: the ghost variable stays one. +// Ghost code of a template's types, a ghost variable assigned in a ghost +// block. template T bump(T x) cppverify::pre(0 <= x && x < 100) @@ -360,3 +361,60 @@ int clamp3(int x) } // CHECK-DAG: Verified: clamp3 [backend=z3] // CHECK-DAG: Verified: constexpr spec axiom: bigger_of + +// A contract written on the definition, after a declaration that names its +// parameter otherwise and before which the template is used. +template +T third(T x); + +int thirds(int x) + cppverify::pre(x >= 0) + cppverify::post(cppverify::result <= x) +{ + int t = third(x); + return t; +} + +template +T third(T y) + cppverify::pre(y >= 0) + cppverify::post(3 * cppverify::result <= y) +{ + return y / 3; +} +// CHECK-DAG: Verified: third [backend=z3] +// CHECK-DAG: Verified: thirds [backend=z3] + +// A variadic template: a fold over a quantifier binds a variable in each +// element, and the parameters the pack expands to are named apart. +template +int first_small(const int *p, Ns... ns) + cppverify::pre(cppverify::valid(p, 10)) + cppverify::pre(((0 < ns && ns <= 10) && ...)) + cppverify::pre((cppverify::forall(k, 0, ns, p[k] < 10) && ...)) + cppverify::post(cppverify::result < 10) +{ + return p[0]; +} + +int uses_first_small(const int *p) + cppverify::pre(cppverify::valid(p, 10)) + cppverify::pre(cppverify::forall(k, 0, 10, p[k] < 10)) + cppverify::post(cppverify::result < 10) +{ + int v = first_small(p, 3, 5); + return v; +} +// CHECK-DAG: Verified: first_small [backend=z3] +// CHECK-DAG: Verified: uses_first_small [backend=z3] + +template +int product_of(Ns... ns) + cppverify::pre(((0 <= ns && ns <= 10) && ...)) + cppverify::post(cppverify::result == (ns * ...)) +{ + return (ns + ...); +} + +int products() { return product_of(2, 3); } +// CHECK-DAG: error: verification failed: product_of [{{.*}}::postcondition@[[@LINE-6]]:{{.*}} ns...[0] [ssa=ns...[0]_0] [type=i32] = {{.*}} ns...[1] [ssa=ns...[1]_0] [type=i32] = From 3693656e87a56c715d7eb335cd8c524a957ed3bc Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:26 +0530 Subject: [PATCH 43/48] test: Check that instantiating a contract leaves a caller its temporaries' cleanups. --- clang/test/Verify/template_contracts.cpp | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/clang/test/Verify/template_contracts.cpp b/clang/test/Verify/template_contracts.cpp index 41bbc0464d..cddc220c6e 100644 --- a/clang/test/Verify/template_contracts.cpp +++ b/clang/test/Verify/template_contracts.cpp @@ -1,5 +1,6 @@ // RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -verify %s // RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -emit-llvm -o - %s | FileCheck %s +// RUN: %clang_cc1 -std=c++17 -fverify-contracts -fno-verify -ast-dump -ast-dump-filter temporaries %s | FileCheck %s --check-prefix=CLEANUPS // // A contract may depend on a template parameter: it is checked where it is // instantiated, as C++ conditions are. A function template's contract is @@ -58,6 +59,26 @@ T positive(T v) return v; } +// A contract instantiated while a caller's full expression is built leaves +// the caller its temporaries, whose destructors run at its end. +struct Noisy { + int v; + Noisy(int x) : v(x) {} + ~Noisy(); +}; + +template +int value_of(const T &t) + cppverify::post(cppverify::result == t.v) +{ + return t.v; +} + +int temporaries() { return value_of(Noisy(3)); } +// CLEANUPS-LABEL: FunctionDecl {{.*}} temporaries 'int ()' +// CLEANUPS: ReturnStmt +// CLEANUPS-NEXT: ExprWithCleanups + template T checked(T n) { From 5ee709d156e790b9b4a6a89e9dac4bcabf358d20 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:26 +0530 Subject: [PATCH 44/48] docs: Describe binder scopes and pack element names in function templates. --- docs/ARCHITECTURE.md | 40 +++++++++++++++++++++++----------------- 1 file changed, 23 insertions(+), 17 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 3fb1d2cc4d..e60a3a79ed 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -315,23 +315,29 @@ pattern and instantiates it lazily, as an exception specification: per specialization (its `FunctionContractInfo` is recorded first, so a use in its own contract stops there), in a `LocalInstantiationScope` that maps the parameters of the declaration the clauses are written on -(`ContractDecl`), with `this` for a member, in an evaluation context of its -own. `SubstFunctionContract` runs `TreeTransform::TransformFunctionContract`, -which rebuilds each clause with the checks the parser applies -(`TransformContractCondition`, `TransformContractMeasure`, -`TransformContractFootprint`; quantifiers and choices through -`Sema::BuildContractBinderExpr`). `TreeTransform` gives `cppverify::result` the -instantiated return type, transforms a loop's contract with the loop and -rebuilds a loop whose clauses changed even when its condition and body did -not, and keeps trigger marks; `BuildVariableInstantiation` keeps ghost -variables. `ResultExpr`, `OldExpr`, and the quantifiers take the dependence -of their type or operands. `collectFunctionCandidates` adds, after each -function template, the specializations the translation unit instantiates -(from its canonical declaration, whose redeclarations share them), with -their definition or, without one, their contract. The converter names them -with their arguments (`functionName`) and records where each is -instantiated (`getInstantiationPoints`), which the driver prints as a note -after each error or warning of the specialization (JSON `instantiated_at`). +(`ContractDecl`), in the specialization's context (its `this`, for a member) +and an evaluation context of its own, so that a caller whose full expression +is being built keeps its temporaries' cleanups. `SubstFunctionContract` runs +`TreeTransform::TransformFunctionContract`, which rebuilds each clause with +the checks the parser applies (`TransformContractCondition`, +`TransformContractMeasure`, `TransformContractFootprint`; quantifiers and +choices through `Sema::BuildContractBinderExpr`). `TreeTransform` gives +`cppverify::result` the instantiated return type, transforms a loop's +contract with the loop and rebuilds a loop whose clauses changed even when +its condition and body did not, and keeps trigger marks; each quantifier and +choice binds in a `LocalInstantiationScope` of its own +(`TemplateInstantiator`), so each element of a pack expansion binds its own +variable, and the block of a `check(forall(k, ...)) by` is given the +instantiated `k`. `ResultExpr`, `OldExpr`, and the quantifiers take the +dependence of their type or operands. `collectFunctionCandidates` adds, +after each function template, the specializations the translation unit +instantiates (from its canonical declaration, whose redeclarations share +them), with their definition or, without one, their contract. The converter +names them with their arguments (`functionName`), and the parameters a pack +expands to as C++26 indexes it, `ns...[1]` (`nameParameters`), and records +where each is instantiated (`getInstantiationPoints`), which the driver +prints as a note after each error or warning of the specialization (JSON +`instantiated_at`). **Records in memory by value:** `recordFieldsInMemory` reads a record value kept in memory, a promoted local or one in a pointee or record reference From c91908eb54c0b8363b77a45931cce0cac58fda53 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:24:26 +0530 Subject: [PATCH 45/48] docs: Describe variadic templates. --- website/source/language/functions-loops.rst | 3 +++ 1 file changed, 3 insertions(+) diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index 14d57668cd..14fe1113f4 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -288,6 +288,9 @@ named with its arguments. declaration holds for the definition after it, and a ``[[cppverify::trusted]]`` template without a definition holds at every call of its specializations. +- In a variadic template, the parameters a pack expands to are named as + C++26 indexes a pack, ``ns...[1]``, in counterexamples too, and a fold + over a quantifier binds a variable of its own in each element. - A specialization the verifier cannot represent (``maxv``) costs that specialization alone, as a construct in any function does. - The contracts of a class template's members and its type invariants are From 1722556b034f6840ff861e8589f263f2de1557bb Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:31:40 +0530 Subject: [PATCH 46/48] verify: Map a contract's parameters through the pattern's, which stand for those of every redeclaration. --- clang/lib/Sema/SemaTemplateInstantiateDecl.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp b/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp index 2b3a4aad51..9e9668b2fb 100644 --- a/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp +++ b/clang/lib/Sema/SemaTemplateInstantiateDecl.cpp @@ -5447,9 +5447,6 @@ void Sema::InstantiateFunctionContract(SourceLocation PointOfInstantiation, Pattern ? Context.getFunctionContract(Pattern) : nullptr; if (!PatternContract || Context.getFunctionContract(Function)) return; - // The clauses name the parameters of the declaration they are written on. - const FunctionDecl *Written = - PatternContract->ContractDecl ? PatternContract->ContractDecl : Pattern; // Recorded first, so that a use of the specialization in its own contract // finds it and stops. @@ -5471,8 +5468,10 @@ void Sema::InstantiateFunctionContract(SourceLocation PointOfInstantiation, MultiLevelTemplateArgumentList TemplateArgs = getTemplateInstantiationArgs( Function, Function->getLexicalDeclContext(), /*Final=*/false, /*Innermost=*/std::nullopt, /*RelativeToPrimary=*/true); - // A member's `this` is the specialization's, the current context. - if (addInstantiatedParametersToScope(Function, Written, Scope, TemplateArgs)) + // A member's `this` is the specialization's, the current context. The + // scope identifies the parameters of every redeclaration of the pattern, + // so the clauses may name those of the declaration they are written on. + if (addInstantiatedParametersToScope(Function, Pattern, Scope, TemplateArgs)) return; FunctionContractInfo Instantiated; if (SubstFunctionContract(*PatternContract, Instantiated, TemplateArgs)) From f653fb6c1241596ba410725e2d644acbf9f8b799 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:31:41 +0530 Subject: [PATCH 47/48] docs: Describe how a contract's parameters are mapped in a specialization. --- docs/ARCHITECTURE.md | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index e60a3a79ed..7bd4019866 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -314,10 +314,11 @@ pattern and instantiates it lazily, as an exception specification: (`MarkFunctionReferenced`) and where its definition is instantiated, once per specialization (its `FunctionContractInfo` is recorded first, so a use in its own contract stops there), in a `LocalInstantiationScope` that maps -the parameters of the declaration the clauses are written on -(`ContractDecl`), in the specialization's context (its `this`, for a member) -and an evaluation context of its own, so that a caller whose full expression -is being built keeps its temporaries' cleanups. `SubstFunctionContract` runs +the pattern's parameters, which identifies those of every redeclaration (so +the clauses may be written on any, `ContractDecl`), in the specialization's +context (its `this`, for a member) and an evaluation context of its own, so +that a caller whose full expression is being built keeps its temporaries' +cleanups. `SubstFunctionContract` runs `TreeTransform::TransformFunctionContract`, which rebuilds each clause with the checks the parser applies (`TransformContractCondition`, `TransformContractMeasure`, `TransformContractFootprint`; quantifiers and From 47516c5862e3e2c556eedc24edcb16f54e42e53a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 19:38:02 +0530 Subject: [PATCH 48/48] test: Pass the temporary by value, which is one before the call is resolved. --- clang/test/Verify/template_contracts.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/clang/test/Verify/template_contracts.cpp b/clang/test/Verify/template_contracts.cpp index cddc220c6e..d3d8b7509f 100644 --- a/clang/test/Verify/template_contracts.cpp +++ b/clang/test/Verify/template_contracts.cpp @@ -60,7 +60,8 @@ T positive(T v) } // A contract instantiated while a caller's full expression is built leaves -// the caller its temporaries, whose destructors run at its end. +// the caller its temporaries, whose destructors run at its end: an argument +// passed by value is one before the call is resolved. struct Noisy { int v; Noisy(int x) : v(x) {} @@ -68,7 +69,7 @@ struct Noisy { }; template -int value_of(const T &t) +int value_of(T t) cppverify::post(cppverify::result == t.v) { return t.v;