From 87c43acea3e68053a2ef169cb20701fb911190a3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 01:29:01 +0530 Subject: [PATCH 01/43] verify: Record the memory checks of contract expressions beside them in VCR. --- clang/lib/Verify/IR/VStmt.h | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/clang/lib/Verify/IR/VStmt.h b/clang/lib/Verify/IR/VStmt.h index 696ad79c21..b5c84ce10d 100644 --- a/clang/lib/Verify/IR/VStmt.h +++ b/clang/lib/Verify/IR/VStmt.h @@ -144,6 +144,18 @@ struct VIfStmt : VStmt { LoopUnrollIteration(LoopUnrollIteration) {} }; +/// A memory check of a contract expression: an access in its object or +/// extent, a step in its object's closure. It is computed from the expression +/// as written, before spec inlining, as a body's accesses are checked: an +/// inlined spec is total, and an inlined helper repeats its arguments' reads. +struct VMemoryCheck { + ProofObligationKind Kind; + std::unique_ptr Cond; +}; + +std::vector +cloneMemoryChecks(const std::vector &Checks); + struct VAssertStmt : VStmt { std::unique_ptr Cond; ProofObligationKind ProofKind; @@ -205,6 +217,9 @@ struct VWhileStmt : VStmt { /// The memory the loop may write, read in each iteration's state; empty /// means none was declared. std::vector Modifies; + /// The memory checks of each invariant, by index; an invariant added after + /// memory checking was set up (a generated one) reads no memory. + std::vector> InvariantChecks; std::vector> Body; VWhileStmt(std::unique_ptr C, std::vector> Inv, std::vector> Dec, @@ -261,6 +276,8 @@ struct VRevealSpecStmt : VStmt { struct VContractAssertStmt : VStmt { std::unique_ptr Cond; + /// The memory checks of the condition. + std::vector MemoryChecks; VContractAssertStmt(std::unique_ptr C, SourceLocation Loc) : VStmt(ContractAssert, Loc), Cond(std::move(C)) {} }; @@ -411,6 +428,9 @@ struct VFunction { unsigned ExplicitPreconditionCount = 0; std::vector> Preconditions; std::vector> Postconditions; + /// The memory checks of each precondition and postcondition, by index. + std::vector> PreconditionChecks; + std::vector> PostconditionChecks; /// Kinds of generated clauses by index; see preconditionKind(). std::vector PreconditionKinds; std::vector PostconditionKinds; From 5d4a9f410bec4cbc555437625ceb874d097160be Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 01:29:02 +0530 Subject: [PATCH 02/43] verify: Copy the recorded memory checks of contract expressions with their nodes. --- clang/lib/Verify/IR/VStmt.cpp | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/clang/lib/Verify/IR/VStmt.cpp b/clang/lib/Verify/IR/VStmt.cpp index c8d057d9d3..2d7a0a134d 100644 --- a/clang/lib/Verify/IR/VStmt.cpp +++ b/clang/lib/Verify/IR/VStmt.cpp @@ -4,6 +4,14 @@ using namespace clang; using namespace verify; +std::vector +verify::cloneMemoryChecks(const std::vector &Checks) { + std::vector Out; + for (const VMemoryCheck &Check : Checks) + Out.push_back({Check.Kind, cloneVExpr(Check.Cond.get())}); + return Out; +} + VFootprint verify::cloneFootprint(const VFootprint &F) { return {cloneVExpr(F.Target.get()), cloneVExpr(F.Count.get()), F.ElementSize}; @@ -67,6 +75,8 @@ std::unique_ptr verify::cloneVStmt(const VStmt *S) { std::move(Body), W.Loc); for (const VFootprint &M : W.Modifies) Out->Modifies.push_back(cloneFootprint(M)); + for (const auto &Checks : W.InvariantChecks) + Out->InvariantChecks.push_back(cloneMemoryChecks(Checks)); return Out; } case VStmt::Call: { @@ -123,8 +133,10 @@ std::unique_ptr verify::cloneVStmt(const VStmt *S) { } case VStmt::ContractAssert: { const auto &A = static_cast(*S); - return std::make_unique(cloneVExpr(A.Cond.get()), - A.Loc); + auto Out = + std::make_unique(cloneVExpr(A.Cond.get()), A.Loc); + Out->MemoryChecks = cloneMemoryChecks(A.MemoryChecks); + return Out; } case VStmt::Break: return std::make_unique(S->Loc); @@ -193,6 +205,10 @@ VFunction verify::cloneVFunction(const VFunction &Fn) { Out.Preconditions.push_back(cloneVExpr(P.get())); for (const auto &P : Fn.Postconditions) Out.Postconditions.push_back(cloneVExpr(P.get())); + for (const auto &Checks : Fn.PreconditionChecks) + Out.PreconditionChecks.push_back(cloneMemoryChecks(Checks)); + for (const auto &Checks : Fn.PostconditionChecks) + Out.PostconditionChecks.push_back(cloneMemoryChecks(Checks)); Out.PreconditionKinds = Fn.PreconditionKinds; Out.PostconditionKinds = Fn.PostconditionKinds; for (const auto &R : Fn.Recommends) From 73882d9e56744db2c920ce488ad7cf0b51fdca4b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 01:29:02 +0530 Subject: [PATCH 03/43] verify: Keep the memory checks of pre- and postconditions through loop unrolling. --- clang/lib/Verify/Transform/LoopUnroll.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/clang/lib/Verify/Transform/LoopUnroll.cpp b/clang/lib/Verify/Transform/LoopUnroll.cpp index 0acff9045b..e6fe44f6a2 100644 --- a/clang/lib/Verify/Transform/LoopUnroll.cpp +++ b/clang/lib/Verify/Transform/LoopUnroll.cpp @@ -263,6 +263,10 @@ VFunction LoopUnroller::unroll(const VFunction &Fn, unsigned K) { Out.Preconditions.push_back(cloneVExpr(P.get())); for (const auto &P : Fn.Postconditions) Out.Postconditions.push_back(cloneVExpr(P.get())); + for (const auto &Checks : Fn.PreconditionChecks) + Out.PreconditionChecks.push_back(cloneMemoryChecks(Checks)); + for (const auto &Checks : Fn.PostconditionChecks) + Out.PostconditionChecks.push_back(cloneMemoryChecks(Checks)); Out.PreconditionKinds = Fn.PreconditionKinds; Out.PostconditionKinds = Fn.PostconditionKinds; for (const auto &R : Fn.Recommends) From 4c642562e394445968f451668bc54af7c3c74588 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:29 +0530 Subject: [PATCH 04/43] verify: Document the memory checks UB instrumentation records for contracts. --- clang/lib/Verify/Transform/UBChecks.h | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/clang/lib/Verify/Transform/UBChecks.h b/clang/lib/Verify/Transform/UBChecks.h index 79e4082d0c..fe5f23f6cc 100644 --- a/clang/lib/Verify/Transform/UBChecks.h +++ b/clang/lib/Verify/Transform/UBChecks.h @@ -24,6 +24,16 @@ namespace verify { /// Insert valid(p, n) bounds obligations into an exec/proof function. No-op /// for spec functions (the spec world uses unbounded math integers). Returns an /// error when a recognized marker cannot be interpreted soundly. +/// +/// The contract expressions (written preconditions, postconditions, loop +/// invariants, cppverify::check conditions) get their memory checks recorded +/// beside them (VMemoryCheck), as the body's accesses get theirs: each access +/// in an object it may address and inside a declared extent or a subobject's +/// bounds, each step in its object's closure. A read under `old` is checked +/// in the entry state, and a quantifier's body at every value of its range; +/// each check is guarded by the short-circuit conditions under which its +/// operand is evaluated. In a pre- or postcondition every parameter is its +/// value at entry, whatever the body assigns. std::optional instrumentUBChecks(VFunction &Fn); /// The object a pointer or reference parameter addresses at entry: its From b1d5370449859286d64ddd30a91400ab38a3989c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:30 +0530 Subject: [PATCH 05/43] verify: Record the memory checks of contracts, invariants, and assertions as written. --- clang/lib/Verify/Transform/UBChecks.cpp | 119 +++++++++++++++++++++++- 1 file changed, 116 insertions(+), 3 deletions(-) diff --git a/clang/lib/Verify/Transform/UBChecks.cpp b/clang/lib/Verify/Transform/UBChecks.cpp index 6e5540555b..aeddc21e07 100644 --- a/clang/lib/Verify/Transform/UBChecks.cpp +++ b/clang/lib/Verify/Transform/UBChecks.cpp @@ -256,6 +256,10 @@ struct UBInstrumenter { std::set Reassigned; // Pointers to subobjects, which address only their companions' bytes. std::set Bounded; + // An expression outside the body, such as a contract clause: a read under + // old is checked in the entry state, and a quantifier's body at every + // value of its range. + bool InContract = false; // Other lies in the closed bounds of Bounded, a pointer into a subobject. std::unique_ptr sameSubobject(const VExpr *Bounded, @@ -835,10 +839,41 @@ struct UBInstrumenter { collectObligations(static_cast(E)->Base.get(), Out, Guard); break; - case VExpr::Old: - collectObligations(static_cast(E)->Inner.get(), Out, - Guard); + case VExpr::Old: { + const VExpr *Inner = static_cast(E)->Inner.get(); + if (!InContract) { + collectObligations(Inner, Out, Guard); + break; + } + std::vector InEntry; + collectObligations(Inner, InEntry); + for (UBObligation &O : InEntry) { + const SourceLocation Loc = O.Cond->Loc; + appendObligation(O.Kind, + std::make_unique(std::move(O.Cond), + VType::makeBool(), Loc), + Guard, Out); + } break; + } + case VExpr::Forall: + case VExpr::Exists: { + if (!InContract) + break; + const auto *Q = static_cast(E); + collectObligations(Q->Lo.get(), Out, Guard); + collectObligations(Q->Hi.get(), Out, Guard); + std::vector InBody; + collectObligations(Q->Body.get(), InBody); + for (UBObligation &O : InBody) + appendObligation(O.Kind, + std::make_unique( + Q->Binder, cloneVExpr(Q->Lo.get()), + cloneVExpr(Q->Hi.get()), std::move(O.Cond), Q->Loc, + Q->BinderType), + Guard, Out); + break; + } case VExpr::SpecCall: { const auto *S = static_cast(E); for (const auto &A : S->Args) @@ -1240,6 +1275,73 @@ std::optional verify::misplacedValidMarker(const VFunction &Fn) { Finder.Where; } +// The memory checks of a contract expression of Fn: against the objects in +// the object model, where an extent is its pointer's object, and against the +// declared extents for a proof function, which is outside it. In a pre- or +// postcondition (Clause) every parameter is its value at entry. +static std::vector contractChecks(const VFunction &Fn, + const VExpr *E, bool Clause) { + std::vector Out; + if (!E) + return Out; + UBInstrumenter UB; + if (Fn.ObjectModel) { + UB.ObjectModel = true; + UB.Objects = abstractObjects(Fn); + if (!Clause) + UB.Reassigned = assignedNames(Fn.Body); + UB.Bounded = Fn.BoundedPointers; + } else { + for (const VValidExtent &Extent : Fn.ValidExtents) { + UB.ValidLen[Extent.Base] = Extent.Length.get(); + UB.ValidPointeeSize[Extent.Base] = Extent.PointerType.PointeeSizeBytes; + } + } + UB.InContract = true; + std::vector Obligations; + UB.collectObligations(E, Obligations); + for (auto &O : Obligations) + Out.push_back({O.Kind, std::move(O.Cond)}); + return Out; +} + +// Records beside each loop invariant and cppverify::check in Stmts its +// memory checks. +static void recordContractChecks(const VFunction &Fn, + std::vector> &Stmts) { + for (auto &S : Stmts) + switch (S->K) { + case VStmt::ContractAssert: { + auto &A = static_cast(*S); + A.MemoryChecks = contractChecks(Fn, A.Cond.get(), /*Clause=*/false); + break; + } + case VStmt::If: { + auto &I = static_cast(*S); + recordContractChecks(Fn, I.Then); + recordContractChecks(Fn, I.Else); + break; + } + case VStmt::While: { + auto &W = static_cast(*S); + W.InvariantChecks.clear(); + for (const auto &Invariant : W.Invariants) + W.InvariantChecks.push_back( + contractChecks(Fn, Invariant.get(), /*Clause=*/false)); + recordContractChecks(Fn, W.Body); + break; + } + case VStmt::Seq: + recordContractChecks(Fn, static_cast(*S).Stmts); + break; + case VStmt::GhostBlock: + recordContractChecks(Fn, static_cast(*S).Body); + break; + default: + break; + } +} + std::optional verify::instrumentUBChecks(VFunction &Fn) { if (Fn.IsSpec) return std::nullopt; @@ -1260,6 +1362,17 @@ std::optional verify::instrumentUBChecks(VFunction &Fn) { UB.Bounded = Fn.BoundedPointers; UB.dropSingleObjectValidity(Fn); } + // Contract expressions are checked as written, before spec inlining. + Fn.PreconditionChecks.clear(); + for (unsigned I = 0; + I < Fn.ExplicitPreconditionCount && I < Fn.Preconditions.size(); ++I) + Fn.PreconditionChecks.push_back( + contractChecks(Fn, Fn.Preconditions[I].get(), /*Clause=*/true)); + Fn.PostconditionChecks.clear(); + for (const auto &Post : Fn.Postconditions) + Fn.PostconditionChecks.push_back( + contractChecks(Fn, Post.get(), /*Clause=*/true)); + recordContractChecks(Fn, Fn.Body); UB.instrumentStmts(Fn.Body); return std::nullopt; } From 9b76d56e3de5fdb5cd16669ab988a3dc074db57d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:30 +0530 Subject: [PATCH 06/43] verify: Declare the check that a function's contract is defined. --- clang/lib/Verify/Transform/Passivize.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/clang/lib/Verify/Transform/Passivize.h b/clang/lib/Verify/Transform/Passivize.h index 0291f72b02..2aac836e24 100644 --- a/clang/lib/Verify/Transform/Passivize.h +++ b/clang/lib/Verify/Transform/Passivize.h @@ -151,6 +151,11 @@ class Passivizer { UnfoldingFuel = WithFuel; } PassiveProgram run(const VFunction &Fn); + /// The well-formedness check of Fn's contract: its written preconditions, + /// in order, are defined where those before them hold, and so are its + /// postconditions in every state it may return in when its body is not + /// verified. It asserts nothing when every clause is total. + PassiveProgram contract(const VFunction &Fn); }; } // namespace verify From 9596311f8e0aa612c27bdf7621f6a00a641231fc Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:31 +0530 Subject: [PATCH 07/43] verify: Check each contract clause where it is evaluated, and postconditions in order. --- clang/lib/Verify/Transform/Passivize.cpp | 442 ++++++++++++++++------- 1 file changed, 313 insertions(+), 129 deletions(-) diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp index b54e616bec..b416922e30 100644 --- a/clang/lib/Verify/Transform/Passivize.cpp +++ b/clang/lib/Verify/Transform/Passivize.cpp @@ -2186,7 +2186,15 @@ collectSafety(const VExpr *E, const FunctionMap *FnMap, " could not be unfolded to check its C++ definedness"); return; } - Collect(Expanded.get(), Out); + // Reported at the call, which is what the caller wrote: the helper's + // operators may lie in another file. + SafetyChecks Inside; + Collect(Expanded.get(), Inside); + for (SafetyCheck &Check : Inside) { + Check.Cond->Loc = C->Loc; + Check.Cond->EndLoc = C->EndLoc; + Out.push_back(std::move(Check)); + } return; } } @@ -3251,6 +3259,8 @@ class PassivizerImpl { std::map Versions; std::map Types; std::map> OldState; + /// The value heap at entry. + std::string EntryHeapVersion; std::vector ReturnCases; std::vector FieldReturnCases; /// Loops being passivized, innermost last. @@ -4228,17 +4238,34 @@ class PassivizerImpl { return VType::makeInt32(Fn.IntMode); } + /// The memory checks of invariant Inv of W, as memory checking recorded + /// them. + static const std::vector *invariantChecks(const VWhileStmt &W, + const VExpr *Inv) { + for (size_t I = 0; + I != W.Invariants.size() && I != W.InvariantChecks.size(); ++I) + if (W.Invariants[I].get() == Inv) + return &W.InvariantChecks[I]; + return nullptr; + } + + /// A contract expression's memory checks, recorded before spec inlining, + /// join its other checks, one obligation per kind. void emitExprSafety(PassiveProgram &P, const VExpr *E, const VExpr *Guard, SourceLocation Loc, const std::map &Renames, bool BridgeMachineValue = false, - const VExpr *SafetySource = nullptr) { + const VExpr *SafetySource = nullptr, + const std::vector *MemoryChecks = nullptr) { SafetyChecks Checks; collectSafety( SafetySource ? SafetySource : E, &FnMap, SafetySource ? &Fn.ValidExtents : &ActiveValidExtents, SafetySource ? &SourcePointerParameterNames : &PointerParameterNames, Checks, Fn.ObjectModel, SafetySource ? &OriginObjects : nullptr); + if (MemoryChecks && !Fn.TotalExpressions) + for (const VMemoryCheck &Check : *MemoryChecks) + Checks.push_back({Check.Kind, cloneVExpr(Check.Cond.get())}); groupByKind(Checks); CloneCtx Ctx{Renames, OldState, false}; for (const SafetyCheck &Check : Checks) @@ -4510,12 +4537,12 @@ class PassivizerImpl { : Fn(Fn), FnMap(std::move(FnMap)), UnfoldingDepth(UnfoldingDepth), UnfoldingFuel(UnfoldingFuel) {} - PassiveProgram run() { - PassiveProgram P; - P.FunctionName = Fn.Name; - P.FunctionIdentity = Fn.Identity; + /// The entry state: the parameters and heaps at their first versions, and + /// the facts that hold there, among them the preconditions (only the + /// generated ones unless WrittenPreconditions). + std::map enter(PassiveProgram &P, + bool WrittenPreconditions) { AssignedNames = assignedNames(Fn.Body); - CloneCtx Ctx{{}, OldState, false}; const char *StateHeaps[] = {VHeapName, VAllocationHeapName, @@ -4536,7 +4563,7 @@ class PassivizerImpl { if (Param.second.Kind == VTypeKind::Ptr) PointerValueVariables.insert(Param.first); } - std::string Heap0 = versionedName(VHeapName); + EntryHeapVersion = versionedName(VHeapName); std::map Renames; for (const char *Heap : StateHeaps) { @@ -4585,18 +4612,15 @@ class PassivizerImpl { Renames[FV] = V0; } - for (const auto &Pre : Fn.Preconditions) { + for (size_t I = 0; I != Fn.Preconditions.size(); ++I) { + if (!WrittenPreconditions && I < Fn.ExplicitPreconditionCount) + continue; CloneCtx PCtx{Renames, OldState, false}; - P.EntryOrigins.push_back( - P.EntryAssumes.size() < Fn.ExplicitPreconditionCount ? "pre" - : "entry"); - P.EntryAssumes.push_back(cloneExpr(Pre.get(), PCtx)); + P.EntryOrigins.push_back(I < Fn.ExplicitPreconditionCount ? "pre" + : "entry"); + P.EntryAssumes.push_back(cloneExpr(Fn.Preconditions[I].get(), PCtx)); } P.PreconditionCount = P.EntryAssumes.size(); - for (const auto &[Name, Assumes] : Fn.Behaviors) { - CloneCtx PCtx{Renames, OldState, false}; - P.BehaviorAssumes.emplace_back(Name, cloneExpr(Assumes.get(), PCtx)); - } { auto Null = std::make_unique(0, VType::makePtr(), SourceLocation()); @@ -4619,6 +4643,19 @@ class PassivizerImpl { P.EntryOrigins.push_back("object"); } } + return Renames; + } + + PassiveProgram run() { + PassiveProgram P; + P.FunctionName = Fn.Name; + P.FunctionIdentity = Fn.Identity; + std::map Renames = + enter(P, /*WrittenPreconditions=*/true); + for (const auto &[Name, Assumes] : Fn.Behaviors) { + CloneCtx PCtx{Renames, OldState, false}; + P.BehaviorAssumes.emplace_back(Name, cloneExpr(Assumes.get(), PCtx)); + } std::unique_ptr Active = makeBoolLiteral(true, SourceLocation()); for (const auto &S : Fn.Body) @@ -4639,6 +4676,18 @@ class PassivizerImpl { if (OfParameter) PostRenames[Name] = static_cast(*Entry).Name; } + // Postconditions are evaluated in order: a clause is evaluated where the + // clauses before it hold. + std::unique_ptr EarlierPosts; + auto afterEarlier = [&](std::unique_ptr Cond) { + if (!EarlierPosts) + return Cond; + const SourceLocation Loc = Cond->Loc, End = Cond->EndLoc; + auto Guarded = makeOr(makeNot(cloneVExpr(EarlierPosts.get()), Loc), + std::move(Cond), Loc); + Guarded->EndLoc = End; + return Guarded; + }; for (size_t I = 0; I != Fn.Postconditions.size(); ++I) { const VExpr *Post = Fn.Postconditions[I].get(); CloneCtx PCtx{PostRenames, OldState, false}; @@ -4655,6 +4704,9 @@ class PassivizerImpl { collectSafety(Post, &FnMap, &Fn.ValidExtents, &SourcePointerParameterNames, Checks, Fn.ObjectModel, &OriginObjects); + if (!Fn.TotalExpressions && I < Fn.PostconditionChecks.size()) + for (const VMemoryCheck &Check : Fn.PostconditionChecks[I]) + Checks.push_back({Check.Kind, cloneVExpr(Check.Cond.get())}); groupByKind(Checks); for (const SafetyCheck &Check : Checks) { if (Fn.TotalExpressions && isDefinedness(Check.Kind)) @@ -4664,8 +4716,12 @@ class PassivizerImpl { auto Cond = cloneExpr(Check.Cond.get(), PCtx); Cond->Loc = Post->Loc; Cond->EndLoc = Post->EndLoc; - P.ExitAsserts.push_back({Check.Kind, std::move(Cond)}); + P.ExitAsserts.push_back({Check.Kind, afterEarlier(std::move(Cond))}); } + auto Clause = cloneVExpr(BoundPost.get()); + EarlierPosts = EarlierPosts ? makeAnd(std::move(EarlierPosts), + std::move(Clause), Post->Loc) + : std::move(Clause); for (auto &[Kind, Part, Note] : checkedClause(postconditionKind(Fn, I), std::move(BoundPost), UninitializedResultNote)) @@ -4675,7 +4731,99 @@ class PassivizerImpl { for (const auto &[Name, Entry] : OldState) if (Entry->K == VExpr::Var) P.EntryVariables.insert(static_cast(*Entry).Name); - P.OldHeapName = Heap0; + finish(P, PostRenames); + return P; + } + + /// The contract's own definedness, as Dafny checks a method's + /// well-formedness: each written precondition is defined where the ones + /// before it hold, and is then assumed. For a function whose body is not + /// verified, each written postcondition is checked the same way in every + /// state the function may return in: within its frame, with any result. + /// A body's own final state checks its postconditions in run(). + PassiveProgram contract() { + PassiveProgram P; + P.FunctionName = Fn.Name + ".contract"; + P.FunctionIdentity = Fn.Identity + "::contract"; + std::map Renames = + enter(P, /*WrittenPreconditions=*/false); + auto checkThenAssume = + [&](const VExpr *Clause, + const std::vector> &Recorded, size_t I) { + CloneCtx Ctx{Renames, OldState, false}; + auto Bound = cloneExpr(Clause, Ctx); + emitExprSafety(P, Bound.get(), nullptr, Clause->Loc, Renames, false, + Clause, I < Recorded.size() ? &Recorded[I] : nullptr); + emitPassive(P, PassiveStmt::Assume, std::move(Bound), nullptr, + Clause->Loc); + }; + for (unsigned I = 0; + I < Fn.ExplicitPreconditionCount && I < Fn.Preconditions.size(); ++I) { + llvm::SaveAndRestore Stated(Origin, "pre"); + checkThenAssume(Fn.Preconditions[I].get(), Fn.PreconditionChecks, I); + } + // Storage the function allocates or frees is not modeled at a call, so + // no caller relies on its postconditions. + if (Fn.IsExternalContract && !Fn.UsesDynamicStorage) { + llvm::SaveAndRestore Returned(Origin, "ret"); + returnAnywhere(P, Renames); + // What the calling convention says of the result holds first. + for (size_t I = 0; I != Fn.Postconditions.size(); ++I) + if (postconditionKind(Fn, I) != ProofObligationKind::Postcondition) { + CloneCtx Ctx{Renames, OldState, false}; + emitPassive(P, PassiveStmt::Assume, + cloneExpr(Fn.Postconditions[I].get(), Ctx), nullptr, + Fn.Postconditions[I]->Loc); + } + for (size_t I = 0; I != Fn.Postconditions.size(); ++I) + if (postconditionKind(Fn, I) == ProofObligationKind::Postcondition) { + llvm::SaveAndRestore Stated(Origin, "post"); + checkThenAssume(Fn.Postconditions[I].get(), Fn.PostconditionChecks, + I); + } + } + finish(P, Renames); + return P; + } + + /// A return in any state the function's frame allows, as its callers see + /// it: its footprints hold unknown values, and so does its result. + void returnAnywhere(PassiveProgram &P, + std::map &Renames) { + const std::string EntryHeap = Renames[VHeapName]; + CloneCtx Ctx{Renames, OldState, false}; + std::map> ParamMap; + for (const auto &[Name, Ty] : Fn.Params) + ParamMap[Name] = + std::make_unique(Renames[Name], Ty, Fn.DeclLoc); + std::vector> Footprints; + std::vector> Counts; + for (const VFootprint &M : Fn.Modifies) { + Footprints.push_back( + substParams(M.Target.get(), ParamMap, Ctx, EntryHeap, EntryHeap)); + Counts.push_back(M.Count ? substParams(M.Count.get(), ParamMap, Ctx, + EntryHeap, EntryHeap) + : nullptr); + } + havocFootprints(P, Renames, Fn, Footprints, Counts, ParamMap, Ctx, + EntryHeap, hasImplicitHeapEffect(Fn, FnMap), Fn.DeclLoc); + if (Fn.ReturnType.Kind == VTypeKind::Struct) { + for (const auto &[Field, Ty] : Fn.ReturnFields) { + const std::string Name = "result." + Field; + Renames[Name] = bump(Name); + Types[Name] = Ty; + } + } else if (Fn.ReturnType.Kind != VTypeKind::Void) { + Renames["result"] = bump(ResultVar); + P.ResultVarName = Renames["result"]; + } + } + + /// What every program of the function carries: its state variables, the + /// specs it may use, and their facts. PostRenames names the final state. + void finish(PassiveProgram &P, + const std::map &PostRenames) { + P.OldHeapName = EntryHeapVersion; P.HeapVariables = HeapVariables; P.ModelVariables = std::move(ModelVariables); P.TraceEvents = std::move(TraceEvents); @@ -4694,7 +4842,6 @@ class PassivizerImpl { } addSpecPostInstances(P, FnMap, Fn, UnfoldingDepth, UnfoldingFuel, EntryMeasure); - return P; } /// In the object model a pointer without provenance is valid where it lies @@ -4740,6 +4887,135 @@ class PassivizerImpl { } } + /// The cells footprint I of Callee covers at a call, its Target and Count + /// in the caller's state, where they are known: a range, a cell, or in + /// the object model the object its region names. + std::optional + footprintBytes(const VFunction &Callee, size_t I, const VExpr *Target, + const VExpr *Count, + const std::map> &ParamMap, + const CloneCtx &Ctx, const std::string &EntryHeap, + SourceLocation Loc) { + const auto *Actual = Target && Target->K == VExpr::Load + ? static_cast(Target) + : nullptr; + if (!Actual) + return std::nullopt; + const VFootprint &Declared = Callee.Modifies[I]; + if (Count) + return rangeBytes(Actual->Ptr.get(), Count, Declared.ElementSize, Loc); + if (!isRegionFootprint(Declared, Callee.ReferenceParams)) + return cellRegion(Actual->Ptr.get(), Actual->Ty, Loc); + if (!Callee.ObjectModel) + return std::nullopt; + const VExpr *Base = addressRoot( + static_cast(Declared.Target.get())->Ptr.get()); + if (!Base || Base->K != VExpr::Var) + return std::nullopt; + const uint64_t Stride = std::max(Base->Ty.PointeeSizeBytes, 1); + for (const VValidExtent &Extent : Callee.ValidExtents) + if (Extent.Base == static_cast(Base)->Name) { + auto Length = + substParams(Extent.Length.get(), ParamMap, Ctx, EntryHeap); + return rangeBytes(Actual->Ptr.get(), Length.get(), Stride, Loc); + } + // A single scalar object is one heap cell. + if (Actual->Ty.isInt() || Actual->Ty.Kind == VTypeKind::Bool || + Actual->Ty.Kind == VTypeKind::Ptr) + return cellRegion(Actual->Ptr.get(), Actual->Ty, Loc); + return Region{ + cloneVExpr(Actual->Ptr.get()), + addBytes(cloneVExpr(Actual->Ptr.get()), + std::make_unique(std::to_string(Stride), + pointerOffsetType(), Loc), + Loc)}; + } + + /// The heap after a call of Callee whose footprints are ActualModifies + /// (with ActualCounts) in the caller's state: each one it may write gets + /// unknown contents, as a chain of stores when all are cells, and every + /// other cell keeps its value; a callee whose writes are not stated, or + /// not known, may write the whole heap. + void + havocFootprints(PassiveProgram &P, + std::map &Renames, + const VFunction &Callee, + const std::vector> &ActualModifies, + const std::vector> &ActualCounts, + const std::map> &ParamMap, + const CloneCtx &Ctx, const std::string &EntryHeap, + bool HasImplicitHeapEffect, SourceLocation Loc) { + bool CanFrameExactly = !ActualModifies.empty(); + for (size_t I = 0; I < ActualModifies.size(); ++I) + if (!ActualModifies[I] || ActualModifies[I]->K != VExpr::Load || + ActualCounts[I] || + (isRegionFootprint(Callee.Modifies[I], Callee.ReferenceParams) && + !hasPointerProvenance( + static_cast(ActualModifies[I].get()) + ->Ptr.get()))) + CanFrameExactly = false; + // A region footprint is its actual's object: the callee's extent, or one + // object; in the object model the callee writes nowhere else. + std::vector CallRegions; + bool CanFrameRegions = Fn.ObjectModel && Callee.ObjectModel && + !CanFrameExactly && !ActualModifies.empty() && + !HasImplicitHeapEffect; + for (size_t I = 0; CanFrameRegions && I < ActualModifies.size(); ++I) { + std::optional Bytes; + if (ActualModifies[I] && ActualModifies[I]->K == VExpr::Load && + !hasPointerProvenance( + static_cast(ActualModifies[I].get()) + ->Ptr.get())) + Bytes = footprintBytes(Callee, I, ActualModifies[I].get(), + ActualCounts[I].get(), ParamMap, Ctx, EntryHeap, + Loc); + if (!Bytes) { + CanFrameRegions = false; + break; + } + CallRegions.push_back(std::move(*Bytes)); + } + const bool OnlyCells = + llvm::all_of(CallRegions, [](const Region &R) { return R.Cell; }); + if (CanFrameRegions && OnlyCells) { + // Each cell gets an unknown value and every other cell keeps its own. + std::string PreviousHeap = EntryHeap; + for (const Region &R : CallRegions) { + std::string NextHeap = bump(VHeapName); + auto Fresh = + std::make_unique(bump("__call_heap_value"), *R.Cell, Loc); + emitPassive(P, PassiveStmt::Assume, + std::make_unique(PreviousHeap, NextHeap, + cloneVExpr(R.Lo.get()), + std::move(Fresh), Loc)); + PreviousHeap = NextHeap; + } + Renames[VHeapName] = PreviousHeap; + } else if (CanFrameRegions) { + std::string NextHeap = bump(VHeapName); + emitPassive(P, PassiveStmt::Assume, + heapFrame(EntryHeap, NextHeap, CallRegions, Loc)); + Renames[VHeapName] = NextHeap; + } else if ((!ActualModifies.empty() && !CanFrameExactly) || + HasImplicitHeapEffect) { + Renames[VHeapName] = bump(VHeapName); + } else if (CanFrameExactly) { + std::string PreviousHeap = EntryHeap; + for (const auto &M : ActualModifies) { + const auto *L = static_cast(M.get()); + std::string NextHeap = bump(VHeapName); + auto Fresh = + std::make_unique(bump("__call_heap_value"), L->Ty, Loc); + emitPassive(P, PassiveStmt::Assume, + std::make_unique(PreviousHeap, NextHeap, + cloneVExpr(L->Ptr.get()), + std::move(Fresh), Loc)); + PreviousHeap = NextHeap; + } + Renames[VHeapName] = PreviousHeap; + } + } + void emitCallStmt(const VCallStmt &C, PassiveProgram &P, std::map &Renames) { auto CalleeIt = FnMap.find(C.CalleeIdentity); @@ -4960,44 +5236,10 @@ class PassivizerImpl { CallerCounts.push_back( M.Count ? cloneExpr(M.Count.get(), CallerEntryCtx) : nullptr); } - // The cells a callee footprint covers, where they are known: a range, a - // cell, or in the object model the object its region names. - auto calleeFootprintBytes = [&](size_t I) -> std::optional { - const auto *Actual = ActualModifies[I] && ActualModifies[I]->K == VExpr::Load - ? static_cast( - ActualModifies[I].get()) - : nullptr; - if (!Actual) - return std::nullopt; - const VFootprint &Declared = Callee->Modifies[I]; - if (ActualCounts[I]) - return rangeBytes(Actual->Ptr.get(), ActualCounts[I].get(), - Declared.ElementSize, C.Loc); - if (!isRegionFootprint(Declared, Callee->ReferenceParams)) - return cellRegion(Actual->Ptr.get(), Actual->Ty, C.Loc); - if (!Callee->ObjectModel) - return std::nullopt; - const VExpr *Base = addressRoot( - static_cast(Declared.Target.get())->Ptr.get()); - if (!Base || Base->K != VExpr::Var) - return std::nullopt; - const uint64_t Stride = std::max(Base->Ty.PointeeSizeBytes, 1); - for (const VValidExtent &Extent : Callee->ValidExtents) - if (Extent.Base == static_cast(Base)->Name) { - auto Length = - substParams(Extent.Length.get(), ParamMap, Ctx, EntryHeap); - return rangeBytes(Actual->Ptr.get(), Length.get(), Stride, C.Loc); - } - // A single scalar object is one heap cell. - if (Actual->Ty.isInt() || Actual->Ty.Kind == VTypeKind::Bool || - Actual->Ty.Kind == VTypeKind::Ptr) - return cellRegion(Actual->Ptr.get(), Actual->Ty, C.Loc); - return Region{cloneVExpr(Actual->Ptr.get()), - addBytes(cloneVExpr(Actual->Ptr.get()), - std::make_unique( - std::to_string(Stride), pointerOffsetType(), - C.Loc), - C.Loc)}; + auto calleeFootprintBytes = [&](size_t I) { + return footprintBytes(*Callee, I, ActualModifies[I].get(), + ActualCounts[I].get(), ParamMap, Ctx, EntryHeap, + C.Loc); }; std::set CalleePointerParams; @@ -5238,73 +5480,8 @@ class PassivizerImpl { } } - bool CanFrameExactly = !ActualModifies.empty(); - for (size_t I = 0; I < ActualModifies.size(); ++I) - if (!ActualModifies[I] || ActualModifies[I]->K != VExpr::Load || - ActualCounts[I] || - (isRegionFootprint(Callee->Modifies[I], Callee->ReferenceParams) && - !hasPointerProvenance( - static_cast(ActualModifies[I].get()) - ->Ptr.get()))) - CanFrameExactly = false; - // A region footprint is its actual's object: the callee's extent, or one - // object; in the object model the callee writes nowhere else. - std::vector CallRegions; - bool CanFrameRegions = Fn.ObjectModel && Callee->ObjectModel && - !CanFrameExactly && !ActualModifies.empty() && - !HasImplicitHeapEffect; - for (size_t I = 0; CanFrameRegions && I < ActualModifies.size(); ++I) { - std::optional Bytes; - if (ActualModifies[I] && ActualModifies[I]->K == VExpr::Load && - !hasPointerProvenance( - static_cast(ActualModifies[I].get()) - ->Ptr.get())) - Bytes = calleeFootprintBytes(I); - if (!Bytes) { - CanFrameRegions = false; - break; - } - CallRegions.push_back(std::move(*Bytes)); - } - const bool OnlyCells = - llvm::all_of(CallRegions, [](const Region &R) { return R.Cell; }); - if (CanFrameRegions && OnlyCells) { - // Each cell gets an unknown value and every other cell keeps its own. - std::string PreviousHeap = EntryHeap; - for (const Region &R : CallRegions) { - std::string NextHeap = bump(VHeapName); - auto Fresh = std::make_unique(bump("__call_heap_value"), - *R.Cell, C.Loc); - emitPassive(P, PassiveStmt::Assume, - std::make_unique(PreviousHeap, NextHeap, - cloneVExpr(R.Lo.get()), - std::move(Fresh), C.Loc)); - PreviousHeap = NextHeap; - } - Renames[VHeapName] = PreviousHeap; - } else if (CanFrameRegions) { - std::string NextHeap = bump(VHeapName); - emitPassive(P, PassiveStmt::Assume, - heapFrame(EntryHeap, NextHeap, CallRegions, C.Loc)); - Renames[VHeapName] = NextHeap; - } else if ((!ActualModifies.empty() && !CanFrameExactly) || - HasImplicitHeapEffect) { - Renames[VHeapName] = bump(VHeapName); - } else if (CanFrameExactly) { - std::string PreviousHeap = EntryHeap; - for (const auto &M : ActualModifies) { - const auto *L = static_cast(M.get()); - std::string NextHeap = bump(VHeapName); - auto Fresh = - std::make_unique(bump("__call_heap_value"), L->Ty, C.Loc); - emitPassive(P, PassiveStmt::Assume, - std::make_unique(PreviousHeap, NextHeap, - cloneVExpr(L->Ptr.get()), - std::move(Fresh), C.Loc)); - PreviousHeap = NextHeap; - } - Renames[VHeapName] = PreviousHeap; - } + havocFootprints(P, Renames, *Callee, ActualModifies, ActualCounts, ParamMap, + Ctx, EntryHeap, HasImplicitHeapEffect, C.Loc); std::map> PostParamMap; for (const auto &[Name, Value] : ParamMap) @@ -5983,7 +6160,7 @@ class PassivizerImpl { for (const auto &Inv : W.Invariants) { auto BoundInv = cloneExpr(Inv.get(), EntryCtx); emitExprSafety(P, BoundInv.get(), Active.get(), Inv->Loc, Renames, - false, Inv.get()); + false, Inv.get(), invariantChecks(W, Inv.get())); emitPassive(P, PassiveStmt::Assert, std::move(BoundInv), Active.get(), Inv->Loc, ProofObligationKind::InvariantEntry); } @@ -6114,7 +6291,8 @@ class PassivizerImpl { CloneCtx ACtx{BodyRenames, OldState, false}; auto BoundInv = cloneExpr(Inv.get(), ACtx); emitExprSafety(P, BoundInv.get(), BodyActive.get(), Inv->Loc, - BodyRenames, false, Inv.get()); + BodyRenames, false, Inv.get(), + invariantChecks(W, Inv.get())); emitPassive(P, PassiveStmt::Assert, std::move(BoundInv), BodyActive.get(), Inv->Loc, ProofObligationKind::InvariantPreserved); @@ -6211,7 +6389,8 @@ class PassivizerImpl { for (const auto &Inv : Frame.Loop->Invariants) { auto BoundInv = cloneExpr(Inv.get(), ContinueCtx); emitExprSafety(P, BoundInv.get(), Active.get(), Inv->Loc, Renames, - false, Inv.get()); + false, Inv.get(), + invariantChecks(*Frame.Loop, Inv.get())); emitPassive(P, PassiveStmt::Assert, std::move(BoundInv), Active.get(), Inv->Loc, ProofObligationKind::InvariantPreserved); } @@ -6243,7 +6422,7 @@ class PassivizerImpl { CloneCtx Ctx{Renames, OldState, false}; auto Cond = cloneExpr(A.Cond.get(), Ctx); emitExprSafety(P, Cond.get(), Active.get(), A.Loc, Renames, false, - A.Cond.get()); + A.Cond.get(), &A.MemoryChecks); // Proved here, a fact from here on: that is what makes it a proof step. auto Fact = cloneVExpr(Cond.get()); emitPassive(P, PassiveStmt::Assert, std::move(Cond), Active.get(), A.Loc, @@ -6327,4 +6506,9 @@ class PassivizerImpl { PassiveProgram Passivizer::run(const VFunction &Fn) { PassivizerImpl Impl(Fn, FnMap, UnfoldingDepth, UnfoldingFuel); return Impl.run(); +} + +PassiveProgram Passivizer::contract(const VFunction &Fn) { + PassivizerImpl Impl(Fn, FnMap, UnfoldingDepth, UnfoldingFuel); + return Impl.contract(); } \ No newline at end of file From 47526f2c66bfc7a839c6e6f6b2612bf867a4e046 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:31 +0530 Subject: [PATCH 08/43] verify: Report an undefined contract and withhold it from callers. --- clang/lib/Verify/Driver/Verifier.cpp | 133 ++++++++++++++++++++++++++- 1 file changed, 131 insertions(+), 2 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 331dd7749a..d7132559b8 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -2199,6 +2199,8 @@ class Verifier { std::vector> InterfaceFunctions; FunctionMap InterfaceMap; + // A contract whose extent markers cannot be read, by function identity. + std::map InterfaceErrors; InterfaceFunctions.reserve(Functions.size()); for (const auto &Fn : Functions) { auto Interface = std::make_unique(cloneVFunction(*Fn)); @@ -2206,7 +2208,8 @@ class Verifier { (isDeductiveBackend(Opts.Backend) || Opts.Backend == BackendKind::BMC || Opts.Backend == BackendKind::Lean)) - (void)instrumentUBChecks(*Interface); + if (auto Error = instrumentUBChecks(*Interface)) + InterfaceErrors[Interface->Identity] = *Error; InterfaceMap[Interface->Identity] = Interface.get(); InterfaceFunctions.push_back(std::move(Interface)); } @@ -2309,6 +2312,8 @@ class Verifier { // Verdicts that assume callee contracts, and the callees they assume. std::vector>> CallDependencies; + // The verdict on each contract's definedness, by function identity. + std::map ContractChecks; // Frame facts of a spec whose reads clause is not established. std::set UnframedSpecs; // Specs whose postcondition is not established. @@ -2404,6 +2409,9 @@ class Verifier { std::vector Confirmations; /// For a verified proof function: what its verification proves. std::shared_ptr Contract; + /// The verdict on the definedness of the function's contract, when it + /// has clauses that may be undefined; its place in Diags. + std::optional ContractCheck; std::string Dump; std::string Archive; /// Ctrl-C came before the verification ended. @@ -2539,6 +2547,96 @@ class Verifier { std::lock_guard Guard(SourceLock); this->annotateObligationSources(Module); }; + // A contract must be defined where it is evaluated (Dafny's + // well-formedness check): its preconditions in order, and the + // postconditions of a function whose body is not verified in every + // state it may return in. It is checked as callers see it, so a lifted + // helper's checks are reported at its call. The check is reported only + // when it does not hold, and then the contract establishes nothing. + auto checkContract = [&](const VFunction &Interface) { + PassiveProgram Checks = P.contract(Interface); + if (llvm::none_of(Checks.Stmts, [](const auto &S) { + return S->K == PassiveStmt::Assert; + })) + return; + const std::string Label = "contract of " + Interface.Name; + auto unsettled = [&](VerifyDiagnostic::Kind Kind, std::string Message, + std::optional R = std::nullopt) { + AllOk = false; + AnyFailed = true; + const SourceLocation Loc = R ? R->Location : Interface.DeclLoc; + Diags.push_back( + {Kind, std::move(Message), Loc, Interface.Name, std::move(R)}); + Run.ContractCheck = Diags.size() - 1; + }; + auto Lowered = buildObligationModule(Checks); + if (!Lowered) + return unsettled(VerifyDiagnostic::Unresolved, + "obligation lowering failed for " + Label + " (" + + llvm::toString(Lowered.takeError()) + ")"); + auto Simplified = simplifyObligationModule(std::move(*Lowered)); + if (!Simplified) + return unsettled(VerifyDiagnostic::Unresolved, + "obligation simplification failed for " + Label + + " (" + llvm::toString(Simplified.takeError()) + + ")"); + ObligationModule Module = std::move(*Simplified); + if (Opts.Backend == BackendKind::BMC) + Module.BMCTransform = BMCTransformProvenance{Opts.BMCUnroll}; + annotateObligationSources(Module); + if (llvm::Error Error = emitObligationArchive(Module)) + return unsettled(VerifyDiagnostic::Error, + "cannot serialize obligation: " + Label + " (" + + llvm::toString(std::move(Error)) + ")"); + if (Opts.LowerOnly) { + VerifyResult Result = lowerForBackend(Module, SpecKind, Execution); + if (Result.Status != VerifyStatus::Lowered) { + std::string Message = + std::string(SpecKind == BackendKind::Z3 ? "Z3" : "backend") + + " lowering failed for " + Label + backendSuffix(Result); + if (!Result.Message.empty()) + Message += " (" + Result.Message + ")"; + unsettled(VerifyDiagnostic::Error, std::move(Message), Result); + } + return; + } + VerifyResult R = SpecBackend->verify(Module); + settle(R, Module, Interface, Label, SpecKind); + if (R.Status == VerifyStatus::Verified || + R.Status == VerifyStatus::Certified) { + Diags.push_back( + {R.Status == VerifyStatus::Verified ? VerifyDiagnostic::Verified + : VerifyDiagnostic::Certified, + Label + backendSuffix(R), R.Location, Interface.Name, R}); + Diags.back().Quiet = true; + recordDependencies(Interface, Module); + Run.ContractCheck = Diags.size() - 1; + } else if (R.Status == VerifyStatus::Exported) { + Diags.push_back({VerifyDiagnostic::Exported, + "lean obligation: " + Label, R.Location, + Interface.Name, R}); + Run.ContractCheck = Diags.size() - 1; + } else if (R.Status == VerifyStatus::Failed) { + std::string Message = "verification failed: " + Label; + if (!R.ObligationId.empty()) + Message += " [" + R.ObligationId + "]"; + if (!R.Message.empty()) + Message += " (counterexample: " + R.Message + ")"; + Message += backendSuffix(R); + unsettled(VerifyDiagnostic::Error, std::move(Message), R); + } else { + const bool FallbackExported = R.Status == VerifyStatus::Unresolved && + exportLeanFallback(Module, Label, R); + if (Opts.LeanCertify && FallbackExported) { + Run.ContractCheck = Diags.size() - 1; + return; + } + std::string Message = Label + backendSuffix(R); + if (!R.Message.empty()) + Message += " (" + R.Message + ")"; + unsettled(VerifyDiagnostic::Unresolved, std::move(Message), R); + } + }; for (const auto &Fn : llvm::ArrayRef>(&Functions[Index], 1)) { // The value of a spec outside its when domain, or a spec of @@ -2558,6 +2656,16 @@ class Verifier { "are not verified; mark the declaration " "[[cppverify::trusted]] to assume the contract", Fn->DeclLoc, Fn->Name}); + if (auto Error = InterfaceErrors.find(Fn->Identity); + Error != InterfaceErrors.end()) { + AllOk = false; + AnyFailed = true; + Diags.push_back( + {VerifyDiagnostic::Error, Fn->Name + ": " + Error->second}); + Run.ContractCheck = Diags.size() - 1; + } else if (!Fn->IsSpec) { + checkContract(*InterfaceMap.at(Fn->Identity)); + } continue; } llvm::scope_exit MarkInterrupted( @@ -3108,6 +3216,9 @@ class Verifier { } } + if (!Fn->IsSpec && !Fn->TotalExpressions) + checkContract(*InterfaceMap.at(Fn->Identity)); + std::optional BMCProgram; std::optional BMCModule; std::optional BMCResult; @@ -3596,6 +3707,8 @@ class Verifier { Pending.Index += Base; Confirmations.push_back(std::move(Pending)); } + if (Run.ContractCheck) + ContractChecks[Functions[I]->Identity] = Base + *Run.ContractCheck; if (DumpOS) *DumpOS << Run.Dump; if (Opts.ObligationOut) @@ -3773,9 +3886,15 @@ class Verifier { for (const auto &[Index, Identity, Callees] : CallDependencies) if (settled(Index)) Unestablished.erase(Identity); + // A contract that may be undefined establishes nothing. + for (const auto &[Identity, Index] : ContractChecks) + if (!settled(Index)) + Unestablished.insert(Identity); std::map VerdictOf; for (const auto &[Index, Identity, Callees] : CallDependencies) VerdictOf[Index] = Identity; + for (const auto &[Identity, Index] : ContractChecks) + VerdictOf[Index] = Identity; std::map CheckOf; for (const SpecReliance &Reliance : ProofDependencies) if (!Reliance.Establishes.empty()) @@ -3830,7 +3949,11 @@ class Verifier { if (Callee != Self && Unestablished.count(Callee)) { list(Names, nameOf(Callee)); auto It = FnMap.find(Callee); - if (It != FnMap.end() && It->second->IsExternalContract) + auto Check = ContractChecks.find(Callee); + if (Check != ContractChecks.end() && !settled(Check->second)) + Names += " (its clauses are not shown to be defined)"; + else if (It != FnMap.end() && It->second->IsExternalContract && + !It->second->IsTrusted) Names += " (no definition; mark it [[cppverify::trusted]] to " "assume it)"; } @@ -3972,6 +4095,12 @@ class Verifier { }; std::map> Producers; std::set Verdicts; + // A contract is established by its function's proof and by the + // check that it is defined. + for (const auto &[Identity, Index] : ContractChecks) { + Verdicts.insert(Index); + Producers[fact('C', Identity)].push_back(Index); + } for (const auto &[Index, Identity, Callees] : CallDependencies) { Verdicts.insert(Index); Producers[fact('C', Identity)].push_back(Index); From 7dceac5d7fc161d3736d4abfda57fa65181c1659 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:32 +0530 Subject: [PATCH 09/43] test: Check that contracts are defined where they are evaluated. --- .../Verify/suite/contract_wellformedness.cpp | 445 ++++++++++++++++++ 1 file changed, 445 insertions(+) create mode 100644 clang/test/Verify/suite/contract_wellformedness.cpp diff --git a/clang/test/Verify/suite/contract_wellformedness.cpp b/clang/test/Verify/suite/contract_wellformedness.cpp new file mode 100644 index 0000000000..c631d0b0ea --- /dev/null +++ b/clang/test/Verify/suite/contract_wellformedness.cpp @@ -0,0 +1,445 @@ +// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s +// RUN: not %cpp-verify --jobs=1 --no-check-ub %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=NOUB +// RUN: not %cpp-verify --jobs=1 --backend=bmc --unroll=2 %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=BMC +// +// A contract is C++ evaluated where the function is called and where it +// returns, so it must be defined there, as Dafny checks a method's +// well-formedness. Each precondition is checked where the ones before it +// hold; each postcondition in the state the function returns in, which for a +// function whose body is not verified is any state its frame allows. A +// clause that may be undefined fails as `contract of f` at its operation, and +// a caller that relies on that contract is not verified. + +using cppverify::valid; + +struct Ring { + int buf[8]; + int head; +}; + +// Each kind of definedness, in a precondition. +int ratio(int a, int b) + cppverify::pre(a / b == 0) +{ + return 0; +} +// CHECK: [[@LINE-4]]:20: error: verification failed: contract of ratio [{{.*}}::contract::division-by-zero@[[@LINE-4]]:20] (counterexample: b [ssa=b_0] [type=i32] = 0) +// CHECK-NEXT: Verified: ratio [backend=z3] +// BMC: error: verification failed: contract of ratio [{{.*}}::contract::division-by-zero@ +// NOUB: error: verification failed: contract of ratio [{{.*}}::contract::division-by-zero@ + +int ratio_ok(int a, int b) + cppverify::pre(b != 0 && a / b == 0) +{ + return 0; +} +// CHECK-NOT: contract of ratio_ok +// CHECK: Verified: ratio_ok [backend=z3] + +int deref(const int *p) + cppverify::pre(*p > 0) +{ + return 0; +} +// CHECK: [[@LINE-4]]:18: error: verification failed: contract of deref [{{.*}}::contract::dereference@[[@LINE-4]]:18] (counterexample: p [ssa=p_0] [type=pointer] = 0) +// NOUB: error: verification failed: contract of deref [{{.*}}::contract::dereference@ + +int deref_ok(const int *p) + cppverify::pre(p != nullptr && *p > 0) +{ + return 0; +} +// CHECK-NOT: contract of deref_ok +// CHECK: Verified: deref_ok [backend=z3] + +int at(const int *p, int i) + cppverify::pre(valid(p, 8) && p[i] == 3) +{ + return 0; +} +// CHECK: [[@LINE-4]]:33: error: verification failed: contract of at [{{.*}}::contract::bounds@[[@LINE-4]]:33] +// NOUB: error: verification failed: contract of at [{{.*}}::contract::dereference@ + +int at_ok(const int *p, int i) + cppverify::pre(valid(p, 8) && 0 <= i && i < 8 && p[i] == 3) +{ + return 0; +} +// CHECK-NOT: contract of at_ok +// CHECK: Verified: at_ok [backend=z3] + +// A pointer without an extent addresses one object. Without memory checking +// (--no-check-ub) accesses are not checked against objects, in a contract as +// in a body, and an extent is not assumed: above, p may be null. +int second(const int *p) + cppverify::pre(p != nullptr && p[1] == 0) +{ + return 0; +} +// CHECK: [[@LINE-4]]:34: error: verification failed: contract of second [{{.*}}::contract::bounds@[[@LINE-4]]:34] +// NOUB-NOT: contract of second + +int slot(const Ring *r, int i) + cppverify::pre(r != nullptr && r->buf[i] == 0) +{ + return 0; +} +// CHECK: [[@LINE-4]]:31: error: verification failed: contract of slot [{{.*}}::contract::bounds@[[@LINE-4]]:31] +// NOUB: error: verification failed: contract of slot [{{.*}}::contract::bounds@ + +constexpr bool positive(int v) { return v > 0; } + +int next_positive(int x) + cppverify::pre(positive(x + 1)) +{ + return 0; +} +// CHECK: [[@LINE-4]]:29: error: verification failed: contract of next_positive [{{.*}}::contract::overflow@[[@LINE-4]]:29] (counterexample: x [ssa=x_0] [type=i32] = 2147483647) + +constexpr int share(int v) { return 100 / v; } + +// An operation inside a lifted helper is reported at the helper's call. +int shared(int x) + cppverify::pre(share(x) > 0) +{ + return 0; +} +// CHECK: [[@LINE-4]]:18: error: verification failed: contract of shared [{{.*}}::contract::division-by-zero@[[@LINE-4]]:18] (counterexample: x [ssa=x_0] [type=i32] = 0) + +// Order: a clause, an operand of && or ||, a branch of ?:, and a quantifier's +// body are evaluated where what comes before them holds. +int ordered(int a, int b) + cppverify::pre(b != 0) + cppverify::pre(a / b == 0) +{ + return 0; +} +// CHECK-NOT: contract of ordered +// CHECK: Verified: ordered [backend=z3] + +int reversed(int a, int b) + cppverify::pre(a / b == 0) + cppverify::pre(b != 0) +{ + return 0; +} +// CHECK: [[@LINE-5]]:20: error: verification failed: contract of reversed [{{.*}}::contract::division-by-zero@[[@LINE-5]]:20] (counterexample: b [ssa=b_0] [type=i32] = 0) + +int either(int a, int b) + cppverify::pre(b == 0 || a / b > 0) +{ + return 0; +} +// CHECK-NOT: contract of either + +int choice(const int *p, int i) + cppverify::pre(valid(p, 4) && (0 <= i && i < 4 ? p[i] > 0 : i == 9)) +{ + return 0; +} +// CHECK-NOT: contract of choice + +int all_positive(const int *a, int n) + cppverify::pre(valid(a, n) && cppverify::forall(k, 0, n, a[k] > 0)) +{ + return 0; +} +// CHECK-NOT: contract of all_positive + +int one_more(const int *a, int n) + cppverify::pre(valid(a, n) && n >= 1 && + cppverify::forall(k, 0, n + 1, a[k] > 0)) +{ + return 0; +} +// CHECK: [[@LINE-4]]:18: error: verification failed: contract of one_more [{{.*}}::contract::bounds@[[@LINE-4]]:18] + +int sign(int x) + cppverify::behavior(positive, x > 0) + cppverify::pre(100 / x > 0) + cppverify::behavior(other, x <= 0) + cppverify::pre(x > -10) +{ + return 0; +} +// CHECK-NOT: contract of sign +// CHECK: Verified: sign [backend=z3] + +// A postcondition is checked in the state the body returns in, where the +// postconditions before it hold. +int read_ahead(const int *p, int i) + cppverify::pre(valid(p, 8) && 0 <= i && i < 8) + cppverify::post(cppverify::result == p[i + 1]) +{ + return p[i]; +} +// CHECK: [[@LINE-4]]:37: error: verification failed: read_ahead [{{.*}}::bounds@[[@LINE-4]]:37] +// BMC: error: verification failed: read_ahead [{{.*}}::bounds@ + +int one(int x) + cppverify::post(cppverify::result != 0) + cppverify::post(10 / cppverify::result == 10) +{ + return 1; +} +// CHECK: Verified: one [backend=z3] + +int zero(int x) + cppverify::post(cppverify::result != 0) + cppverify::post(10 / cppverify::result == 10) +{ + return 0; +} +// CHECK: [[@LINE-5]]:37: error: verification failed: zero [{{.*}}::postcondition@[[@LINE-5]]:37] +// CHECK-NOT: division-by-zero + +// A loop invariant and an assertion read memory as the body does. +int walk(const int *p, int n) + cppverify::pre(valid(p, n) && n >= 1 && n <= 100) + cppverify::pre(cppverify::forall(k, 0, n, p[k] >= 0)) +{ + int i = 0; + while (i < n) + cppverify::invariant(0 <= i && i <= n && p[i] >= 0) + cppverify::decreases(n - i) + { + i = i + 1; + } + return 0; +} +// CHECK: [[@LINE-7]]:43: error: verification failed: walk [{{.*}}::bounds@[[@LINE-7]]:43 + +int last(const int *p, int n) + cppverify::pre(valid(p, n) && n >= 1 && n <= 100) + cppverify::pre(cppverify::forall(k, 0, n, p[k] >= 0)) +{ + cppverify::check(p[n] >= 0); + return 0; +} +// CHECK: [[@LINE-3]]:3: error: verification failed: last [{{.*}}::bounds@[[@LINE-3]]:3] +// BMC: error: verification failed: last [{{.*}}::bounds@ + +int ghost_last(const int *p, int n) + cppverify::pre(valid(p, n) && n >= 1 && n <= 100) +{ + cppverify::ghost { cppverify::check(p[n] >= 0 || p[n] < 0); } + return 0; +} +// CHECK: [[@LINE-3]]:22: error: verification failed: ghost_last [{{.*}}::bounds@[[@LINE-3]]:22] + +// The postcondition before it holds, and the body's own state places the +// result: *result lies in p. +int *second_of(int *p) + cppverify::pre(valid(p, 4)) + cppverify::post(cppverify::result == p + 1) + cppverify::post(*cppverify::result == p[1]) +{ + return p + 1; +} +// CHECK: Verified: second_of [backend=z3] + +// A read under old is checked in the entry state, where p[0] is the index the +// precondition bounds, not the 100 the body stores. +int take(int *p) + cppverify::pre(valid(p, 4) && 1 <= p[0] && p[0] < 4) + cppverify::modifies(p[0]) + cppverify::post(cppverify::result == cppverify::old(p[p[0]])) +{ + int v = p[p[0]]; + p[0] = 100; + return v; +} +// CHECK: Verified: take [backend=z3] +// BMC: Verified: take [backend=bmc + +// A parameter in a postcondition is its entry value, whatever the body +// assigns to its copy. +int advance(const int *p) + cppverify::pre(valid(p, 2)) + cppverify::post(cppverify::result == p[1]) +{ + p = p + 1; + return *p; +} +// CHECK: Verified: advance [backend=z3] + +// p[2] is q[0], but read through p it lies outside p's object, which is what +// the clause is checked against, whatever the body assigns to p. +int next_object(const int *p, const int *q) + cppverify::pre(valid(p, 2) && valid(q, 2) && q == p + 2) + cppverify::post(cppverify::result == p[2]) +{ + p = p + 1; + return q[0]; +} +// CHECK: [[@LINE-5]]:37: error: verification failed: next_object [{{.*}}::bounds@[[@LINE-5]]:37] + +int prev_object(const int *p, const int *q) + cppverify::pre(valid(p, 2) && valid(q, 2) && q == p + 2 && p[2] == 0) +{ + p = p + 1; + return 0; +} +// CHECK: [[@LINE-5]]:55: error: verification failed: contract of prev_object [{{.*}}::contract::bounds@[[@LINE-5]]:55] + +// A trusted contract holds in every state its frame allows, with any result. +[[cppverify::trusted]] int inverse(int x) + cppverify::post(10 / cppverify::result > 0); +// CHECK: Trusted: inverse (contract assumed, not verified) +// CHECK-NEXT: [[@LINE-2]]:22: error: verification failed: contract of inverse [{{.*}}::contract::division-by-zero@[[@LINE-2]]:22] (counterexample: result [ssa=__result_1] [type=i32] = 0) + +[[cppverify::trusted]] int nonzero(int x) + cppverify::post(cppverify::result != 0) + cppverify::post(10 / cppverify::result >= -10); +// CHECK: Trusted: nonzero (contract assumed, not verified) +// CHECK-NOT: contract of nonzero + +[[cppverify::trusted]] int *find(int *p, int x) + cppverify::pre(valid(p, 4)) + cppverify::post(cppverify::result == nullptr || *cppverify::result == x); +// CHECK: Trusted: find (contract assumed, not verified) +// CHECK-NOT: contract of find + +[[cppverify::trusted]] int *find_any(int *p, int x) + cppverify::pre(valid(p, 4)) + cppverify::post(*cppverify::result == x); +// CHECK: [[@LINE-1]]:19: error: verification failed: contract of find_any [{{.*}}::contract::dereference@[[@LINE-1]]:19] + +// What the frame does not name keeps its value: *q stays nonzero. +[[cppverify::trusted]] void scale(int *p, const int *q) + cppverify::pre(p != nullptr && q != nullptr && *q != 0) + cppverify::modifies(*p) + cppverify::post(*p == cppverify::old(*p) + 10 / *q); +// CHECK: Trusted: scale (contract assumed, not verified) +// CHECK-NOT: contract of scale + +[[cppverify::trusted]] void scale_both(int *p, int *q) + cppverify::pre(p != nullptr && q != nullptr && *q != 0) + cppverify::modifies(*p, *q) + cppverify::post(*p == cppverify::old(*p) + 10 / *q); +// CHECK: [[@LINE-1]]:49: error: verification failed: contract of scale_both [{{.*}}::contract::division-by-zero@[[@LINE-1]]:49] + +// A contract without a definition is checked too. +int past(const int *p, int n) + cppverify::pre(valid(p, n) && n >= 1) + cppverify::post(cppverify::result == p[n]); +// CHECK: warning: past has a contract but no definition +// CHECK-NEXT: [[@LINE-2]]:40: error: verification failed: contract of past [{{.*}}::contract::bounds@[[@LINE-2]]:40] + +// A trusted contract whose extent marker cannot be read establishes nothing. +[[cppverify::trusted]] int either_end(const int *p, int n) + cppverify::pre(n == 0 || valid(p, n)); +// CHECK: Trusted: either_end (contract assumed, not verified) +// CHECK-NEXT: error: either_end: valid marker must be a positive top-level conjunction clause + +int use_end(const int *p) + cppverify::pre(valid(p, 2)) +{ + int r = either_end(p, 2); + return r; +} +// CHECK: Unresolved: use_end [backend=z3] [reason=callee.contract] (relies on the contract of either_end (its clauses are not shown to be defined), which is not established) + +// A caller relies on the contract it calls, which a contract that may be +// undefined does not establish. +int use_inverse(int x) + cppverify::post(cppverify::result > 0) +{ + int r = inverse(x); + return 10 / r; +} +// CHECK: Unresolved: use_inverse [backend=z3] [reason=callee.contract] (relies on the contract of inverse (its clauses are not shown to be defined), which is not established) + +int use_nonzero(int x) + cppverify::post(cppverify::result != 0) +{ + int r = nonzero(x); + return r; +} +// CHECK: Verified: use_nonzero [backend=z3] [trusts=nonzero] + +int use_ratio(int b) + cppverify::pre(b != 0) +{ + int r = ratio(0, b); + return r; +} +// CHECK: Unresolved: use_ratio [backend=z3] [reason=callee.contract] (relies on the contract of ratio (its clauses are not shown to be defined), which is not established) + +// A proof function's contract is checked against its extents. +cppverify::proof void lemma(const int *a, int n) + cppverify::pre(valid(a, n) && n >= 1 && a[n] == 0) +{ +} +// CHECK: [[@LINE-3]]:43: error: verification failed: contract of lemma [{{.*}}::contract::bounds@[[@LINE-3]]:43] +// CHECK-NEXT: Verified: lemma [backend=z3] + +// A spec is total: division by zero is zero there, and it has no +// precondition to check. +cppverify::spec int quotient(int a, int b) { return a / b; } + +int halves(int a) + cppverify::pre(quotient(a, 0) == 0) +{ + return 0; +} +// CHECK-NOT: contract of halves +// CHECK: Verified: halves [backend=z3] + +// A spec is total, as in Verus: applied in a postcondition it reads memory +// without a check, even a cell outside p. +cppverify::spec int cell(const int *p, int i) { return p[i]; } + +[[cppverify::trusted]] int far(const int *p) + cppverify::pre(valid(p, 4)) + cppverify::post(cppverify::result == cell(p, 7)); +// CHECK: Trusted: far (contract assumed, not verified) +// CHECK-NOT: contract of far + +int far_copy(const int *p) + cppverify::pre(valid(p, 4)) + cppverify::post(cppverify::result == cell(p, 7)) +{ + int r = far(p); + return r; +} +// CHECK: Verified: far_copy [backend=z3] [trusts=far] + +// A contract is established by its function's proof and by the check that it +// is defined, so that check takes part in the cycle rule. The check of +// cycled's contract needs sum_up's postcondition, whose proof calls cycled. +cppverify::spec int sum_up(int n); + +[[cppverify::trusted]] cppverify::proof void cycled(int n) + cppverify::pre(n >= 0 && 10 / (sum_up(n) + 1) >= 0); +// CHECK: Trusted: cycled (contract assumed, not verified) +// CHECK-NEXT: Unresolved: contract of cycled [backend=z3] [reason=proof.cycle] + +cppverify::spec int sum_up(int n) + cppverify::decreases(n) + cppverify::post(cppverify::result >= 0) by { if (n > 0) cycled(n - 1); } +{ + return n <= 0 ? 0 : sum_up(n - 1) + n; +} +// CHECK: Unresolved: spec decreases and post: sum_up [reason=proof.cycle] + +// With measures every use between them lowers, they form a cluster: the +// check uses sum_down(n) at (n, 1), below (n, 2), and the proof block calls +// measured at (n - 1, 2), below (n, 1). +cppverify::spec int sum_down(int n); + +[[cppverify::trusted]] cppverify::proof void measured(int n) + cppverify::pre(n >= 0 && 10 / (sum_down(n) + 1) >= 0) + cppverify::decreases(n, 2); +// CHECK: Trusted: measured (contract assumed, not verified) +// CHECK-NOT: contract of measured + +cppverify::spec int sum_down(int n) + cppverify::decreases(n, 1) + cppverify::post(cppverify::result >= 0) by { if (n > 0) measured(n - 1); } +{ + return n <= 0 ? 0 : sum_down(n - 1) + n; +} +// CHECK: Verified: spec decreases and post: sum_down From ab9fa6d6fbbe2c09d537849c501dd1e63c02aadc Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:32 +0530 Subject: [PATCH 10/43] test: Expect the bounds failure of a postcondition read past its object. --- clang/test/Verify/suite/dynamic_storage_fail.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/dynamic_storage_fail.cpp b/clang/test/Verify/suite/dynamic_storage_fail.cpp index 5526f736be..fc6c1bf5e4 100644 --- a/clang/test/Verify/suite/dynamic_storage_fail.cpp +++ b/clang/test/Verify/suite/dynamic_storage_fail.cpp @@ -439,7 +439,7 @@ int modular_discarded_pointer_forwarding() // VERIFY-DAG: Unresolved: modular_copied_pointer_return {{.*}}[reason=construct.unsupported] // VERIFY-DAG: Unresolved: modular_unsafe_forwarding {{.*}}[reason=construct.unsupported] // VERIFY-DAG: Unresolved: modular_discarded_pointer_forwarding {{.*}}[reason=construct.unsupported] -// VERIFY-DAG: Unresolved: unsafe_forwarded_read {{.*}}[reason=callee.contract] (relies on the contract of read_next, which is not established) +// VERIFY-DAG: error: verification failed: unsafe_forwarded_read [{{.*}}::bounds@107:37] // VERIFY-DAG: Verified: modular_forwarded_scalar // VERIFY-DAG: Verified: modular_forwarded_temporary // VERIFY-DAG: Verified: modular_forwarded_control From d8a09e0518a39173567a47b7ca468841d6e3b4dc Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:33 +0530 Subject: [PATCH 11/43] test: Declare the extents the quantifier range tests read. --- .../Verify/suite/certified_quantifier_ranges.cpp | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/clang/test/Verify/suite/certified_quantifier_ranges.cpp b/clang/test/Verify/suite/certified_quantifier_ranges.cpp index 313fea8c08..737522d962 100644 --- a/clang/test/Verify/suite/certified_quantifier_ranges.cpp +++ b/clang/test/Verify/suite/certified_quantifier_ranges.cpp @@ -9,7 +9,7 @@ // Whatever length the solver first picks, a counterexample with a range small // enough to check exists and is the one reported. int first_positive(const int *p, int n) - cppverify::pre(n >= 1 && p != nullptr) + cppverify::pre(n >= 1 && cppverify::valid(p, n)) cppverify::pre(cppverify::forall(i, 0, n, p[i] >= 0)) cppverify::post(cppverify::result > 0) { @@ -19,7 +19,7 @@ int first_positive(const int *p, int n) // Two million elements, but the body reads the binder only through p[i]: the // model sets a few cells and the rest share one value, so it is checked. int first_positive_long(const int *p, int n) - cppverify::pre(n >= 2000000 && p != nullptr) + cppverify::pre(n >= 2000000 && cppverify::valid(p, n)) cppverify::pre(cppverify::forall(i, 0, n, p[i] >= 0)) cppverify::post(cppverify::result > 0) { @@ -28,7 +28,7 @@ int first_positive_long(const int *p, int n) // The instance at i == 0 decides the postcondition without expanding it. void writes_first(int *p, int n) - cppverify::pre(n >= 2000000 && p != nullptr) + cppverify::pre(n >= 2000000 && cppverify::valid(p, n)) cppverify::pre(p[0] == 0) cppverify::modifies(*p) cppverify::post(cppverify::forall(i, 0, n, i < 0 || p[i] == cppverify::old(p[i]))) @@ -39,7 +39,7 @@ void writes_first(int *p, int n) // The body also compares the index itself. The comparison is affine, so its // truth changes only at its root and the range splits into a few intervals. int first_positive_indexed(const int *p, int n) - cppverify::pre(n >= 2000000 && p != nullptr) + cppverify::pre(n >= 2000000 && cppverify::valid(p, n)) cppverify::pre(cppverify::forall(i, 0, n, i < 0 || p[i] >= 0)) cppverify::post(cppverify::result > 0) { @@ -49,7 +49,7 @@ int first_positive_indexed(const int *p, int n) // Contract arithmetic is exact, so a nonlinear comparison is a polynomial // whose sign changes are found exactly. int first_positive_squared(const int *p, int n) - cppverify::pre(n >= 2000000 && n <= 3000000 && p != nullptr) + cppverify::pre(n >= 2000000 && n <= 3000000 && cppverify::valid(p, n)) cppverify::pre(cppverify::forall(i, 0, n, i * i < 0 || p[i] >= 0)) cppverify::post(cppverify::result > 0) { @@ -58,7 +58,7 @@ int first_positive_squared(const int *p, int n) // So is one through a conversion to a machine type the value fits. int first_positive_squared_wide(const int *p, int n) - cppverify::pre(n >= 2000000 && n <= 3000000 && p != nullptr) + cppverify::pre(n >= 2000000 && n <= 3000000 && cppverify::valid(p, n)) cppverify::pre(cppverify::forall(i, 0, n, (long long)i * i < 0 || p[i] >= 0)) cppverify::post(cppverify::result > 0) { @@ -68,7 +68,7 @@ int first_positive_squared_wide(const int *p, int n) // A bitwise use of the index would need two million instances checked one by // one, and no shorter counterexample exists. int first_positive_bitwise(const int *p, int n) - cppverify::pre(n >= 2000000 && n <= 3000000 && p != nullptr) + cppverify::pre(n >= 2000000 && n <= 3000000 && cppverify::valid(p, n)) cppverify::pre(cppverify::forall(i, 0, n, (i ^ 1431655765) < 0 || p[i] >= 0)) cppverify::post(cppverify::result > 0) { From 29d6739a2d7da72d6a5af31fb8775879090846ef Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:34 +0530 Subject: [PATCH 12/43] docs: Describe the check that contracts are defined. --- website/source/language/functions-loops.rst | 88 +++++++++++++++++++++ 1 file changed, 88 insertions(+) diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index d7b610135c..d9a99543df 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -127,6 +127,94 @@ all denote the argument's entry value, as in ACSL, even when the callee reassigns its by-value parameter; a caller can therefore use the postcondition directly. +Contracts must be defined +------------------------- + +A contract is C++, evaluated where the function is called and where it +returns. A clause that divides by zero or reads outside an object there says +nothing, so CppVerify checks that each clause is defined where it is +evaluated, as Dafny checks a method's well-formedness, and reports a clause +that may not be as ``contract of f``, at the operation: + +- each precondition where the preconditions written before it hold, so a + clause may rely on the ones before it, and each operand of ``&&``, ``||``, + and ``?:`` where the operands before it allow its evaluation; +- each postcondition in the state the function returns in, where the + postconditions before it hold. For a trusted function or one without a + definition, that is every state its frame allows (only its + ``cppverify::modifies`` footprints change), with any result; +- the checks an operation gets in a body: divisors, shifts, a mathematical + value converted to a machine type, dereferences, and, with memory checking, + every access inside its extent or object (see :doc:`pointers`). Loop + invariants and ``cppverify::check`` get the same checks. + +.. code-block:: cpp + + int average(int total, int count) + cv::pre(total / count >= 0 && count > 0) + cv::post(cv::result >= 0) + { + return total / count; + } + + int average_checked(int total, int count) + cv::pre(count > 0 && total / count >= 0) + cv::post(cv::result >= 0) + { + return total / count; + } + + int pick(const int *p, int i) + cv::pre(cv::valid(p, 8) && p[i] > 0 && 0 <= i && i < 8) + cv::post(cv::result > 0) + { + return p[i]; + } + + [[cppverify::trusted]] int read_sensor(int channel) + cv::post(1000 / cv::result > 0); + + int scaled(int channel) + cv::post(cv::result > 0) + { + int r = read_sensor(channel); + return 1000 / r; + } + +.. code-block:: text + + defined.cpp:2:17: error: verification failed: contract of average + [...::contract::division-by-zero@2:17] (counterexample: count [type=i32] = 0) + Verified: average [backend=z3] + Verified: average_checked [backend=z3] + defined.cpp:16:30: error: verification failed: contract of pick + [...::contract::bounds@16:30] (counterexample: i [type=i32] = -1, ...) + Verified: pick [backend=z3] + defined.cpp:22:28: Trusted: read_sensor (contract assumed, not verified) + defined.cpp:23:17: error: verification failed: contract of read_sensor + [...::contract::division-by-zero@23:17] (counterexample: result [type=i32] = 0) + Unresolved: scaled [backend=z3] [reason=callee.contract] (relies on the + contract of read_sensor (its clauses are not shown to be defined), which is + not established) + +``average`` divides before it tests ``count``, so its precondition is undefined +at ``count == 0``; written the other way round, as in ``average_checked``, it +is defined. ``pick`` reads ``p[i]`` before it bounds ``i``. Both bodies still +verify: their proofs assume the preconditions, and a body's own operations +are checked whatever its contract says. The trusted contract of +``read_sensor`` divides by its result, which may be 0. + +A contract that may be undefined establishes nothing: every caller that relies +on it is ``Unresolved`` with reason ``callee.contract``, as ``scaled`` is. Its +proof read ``1000 / r > 0`` as excluding ``r == 0``, since the logic defines a +division by zero, but C++ does not, so nothing excludes it. The function's own +verdict is about its body and does not change. The check prints nothing when it +holds. + +Spec functions stay total, as in Verus and ACSL: a spec's division by zero is +0, so applying a spec in a contract adds no check, and +``cppverify::recommends`` remains a warning (see :doc:`ghost-proofs`). + Templates and member functions ------------------------------ From d5c64733d7325bf4cba9fd660daf4cea06855500 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:34 +0530 Subject: [PATCH 13/43] docs: Note that contract reads are checked against extents. --- website/source/language/pointers.rst | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/website/source/language/pointers.rst b/website/source/language/pointers.rst index ef80228b84..797d84472d 100644 --- a/website/source/language/pointers.rst +++ b/website/source/language/pointers.rst @@ -592,6 +592,13 @@ top-level conjunction clause of a ``cppverify::pre`` with a bare complete-object and each pointer may have only one marker; ambiguous forms (under ``||``, ``!``, or a conditional, or a second marker for one pointer) fail closed. +Contracts read under the same rule. An access in a precondition, a +postcondition, a loop invariant, or a ``cppverify::check`` must lie in its +extent or object where the clause is evaluated, so a precondition reads +``p[i]`` only after the clauses that bound ``i``: ``cv::pre(valid(p, n) && 0 <= +i && i < n && p[i] > 0)``, not ``cv::pre(valid(p, n) && p[i] > 0 && 0 <= i && +i < n)`` (see :doc:`functions-loops`). + Where the marker may appear ~~~~~~~~~~~~~~~~~~~~~~~~~~~ From b17f29d802b9e23db288c40212d08542bf6b86a9 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:35 +0530 Subject: [PATCH 14/43] docs: Note that contracts get the definedness checks. --- website/source/language/limitations.rst | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 8841fa298c..1dcaa09ded 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -499,8 +499,9 @@ parameters and reads from memory included, is assumed to lie in its range. Memory checking (the default, off with ``--no-check-ub``) adds object bounds: an access or pointer step stays in the ``valid(p, n)`` extent or the single object a pointer addresses, across modular sub-slices and same-array -pointer positions. Together they are not yet comprehensive C++ -undefined-behavior checking. +pointer positions. Contracts get both kinds of obligation, each clause where +it is evaluated (see :doc:`functions-loops`). Together they are not yet +comprehensive C++ undefined-behavior checking. Missing general UB semantics include object provenance outside the represented fragment, strict aliasing, arbitrary alignment, unsequenced side effects and From 6a75a2f25fd114846231d70f8f71039df58836ed Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:35 +0530 Subject: [PATCH 15/43] docs: Note that contracts get the mandatory definedness checks. --- website/source/language/integers.rst | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/website/source/language/integers.rst b/website/source/language/integers.rst index 58dc7c6aaa..60d25c52df 100644 --- a/website/source/language/integers.rst +++ b/website/source/language/integers.rst @@ -72,7 +72,8 @@ Mandatory C++ definedness Executable and ``cppverify::proof`` code must be well-defined C++. CppVerify therefore generates path-sensitive safety obligations automatically; these checks are not optional because a functional proof about an undefined execution would be -meaningless. +meaningless. Contracts get the same obligations, each clause where it is +evaluated (see :doc:`functions-loops`). Core checks include: From 22107e647e3482469c5e4347ed49445ed4e559cb Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:36 +0530 Subject: [PATCH 16/43] docs: Describe the contract check's label and obligation names. --- website/source/language/tooling.rst | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index 631763357a..9431c7dee2 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -589,6 +589,11 @@ what the obligation checks: - ``unwinding`` for a BMC bound, and ``unsupported`` for a construct the verifier rejects fail-closed. +The check that a function's contract is defined (see :doc:`functions-loops`) +is reported only when it fails, as ``contract of f``. Its obligations are +named ``function-identity::contract::kind@line:column`` with the definedness +kinds above, and JSON records give ``f`` as the function. + The local suffix only disambiguates obligations of one kind at the same anchor, so inserting or reordering an unrelated obligation does not renumber later IDs unless its source anchor moves. JSON records carry the kind as From f744d0a5d97c69e6faf34b5cbd8afa32d3ef3f8f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:37 +0530 Subject: [PATCH 17/43] docs: Explain in chapter 18 that contracts must be defined. --- .../book/part-ii/ch18-undefined-behavior.rst | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) diff --git a/website/source/book/part-ii/ch18-undefined-behavior.rst b/website/source/book/part-ii/ch18-undefined-behavior.rst index c0ea86940b..20ed907b8b 100644 --- a/website/source/book/part-ii/ch18-undefined-behavior.rst +++ b/website/source/book/part-ii/ch18-undefined-behavior.rst @@ -267,6 +267,36 @@ iteration is caught even though the first few iterations are fine. (The fix is the same as for any loop: an invariant that bounds the accumulator. See :doc:`ch12-loops-in-practice`.) +Contracts are C++ too +--------------------- + +A contract is evaluated as C++ where the function is called and where it +returns, so it must be defined there, just as the body must. A precondition +that divides by ``items`` before it says ``items > 0`` is undefined for the +very input it means to exclude: + +.. code-block:: cpp + + int per_item(int total, int items) + cv::pre(total / items <= 100 && items > 0) + cv::post(cv::result <= 100) + { + return total / items; + } + +.. code-block:: text + + per.cpp:2:17: error: verification failed: contract of per_item + [...::contract::division-by-zero@2:17] (counterexample: items [type=i32] = 0) + Verified: per_item [backend=z3] + +The body verifies, since its proof assumes the precondition. The contract does +not: a clause is checked where the clauses and operands before it hold, so +``cv::pre(items > 0 && total / items <= 100)`` is defined. A postcondition is +checked the same way in the state the function returns in, and a trusted +contract in every state it allows. Callers do not rely on a contract that may +be undefined; see :doc:`../../language/functions-loops`. + What is not covered yet ----------------------- From e30f7ee50919d8b720cf0966c7ed2b93aef713bc Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:37 +0530 Subject: [PATCH 18/43] docs: Note the contract definedness check in the release notes. --- website/source/release-notes.rst | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index bb464da031..1b3930a842 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -77,6 +77,21 @@ that returns ``nullptr``. In a postcondition, a loop invariant, a ``cppverify::check``, ghost code, or a spec function it is now an error for that function (:doc:`language/pointers`). +**Contracts must be defined.** A contract is C++, evaluated where the function +is called and where it returns, but 0.1.1 never checked that it was defined +there: a precondition was only assumed, and the reads of a postcondition, a +loop invariant, or a ``cppverify::check`` were not checked against extents. The +logic defines what C++ does not, so a trusted ``cv::post(1000 / cv::result > +0)`` excluded a result of 0, and a caller that divided by that result +verified. Each clause is now checked where it is evaluated: preconditions in +order, each where the ones before it hold; postconditions in the state the +function returns in, or for a trusted function or one without a definition in +every state its frame allows; and every clause with the memory checks of the +body. A clause that may be undefined fails as ``contract of f``, and callers +that rely on it are ``Unresolved`` with reason ``callee.contract``. A contract +that tests a condition after using it, as ``cv::pre(a / b > 0 && b != 0)`` +does, needs the test first (:doc:`language/functions-loops`). + **Clang's own analyses.** ``noexcept`` of a contract expression crashed or hung the compiler, as did a contract expression in a C++98 constant; the static analyzer reported nothing after a ghost block; libclang hid the constructs; From 059db39c87a9b109b754a4bf9bad3bd75c492a56 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:38 +0530 Subject: [PATCH 19/43] docs: Describe contract well-formedness in the design. --- docs/DESIGN.md | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 5f85e263d7..acd1c9b7e9 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -98,6 +98,33 @@ int abs_value(int x) the behaviors it relates, e.g. `cppverify::disjoint_behaviors(low, high)`. Both are checked at function entry. +### Contracts must be defined + +A contract is C++ evaluated where the function is called and where it returns +(as C++26 contracts are), so each clause must be defined there. Every +contracted function except a spec gets a well-formedness check, as Dafny +builds one per method (`CheckWellFormed$$f`): + +- each written precondition, in order, is checked where the ones before it + hold, and then assumed; within a clause, `&&`, `||`, `?:`, and a + quantifier's range guard the operands after them; +- each postcondition is checked in the state the function returns in, where + the postconditions before it hold. For a verified body that is its own final + state (the body's module checks it, as Verus does); for a trusted function or + one without a definition it is every state the frame allows, with any + result, which is what callers assume; +- a clause gets the checks an operation gets in a body: the core definedness + checks and, with memory checking, every access in its extent or object. + Loop invariants and `cppverify::check` get the same memory checks. + +The check is reported only when it fails, as `contract of f`, at the operation +(a lifted helper's checks at its call). A contract that may be undefined +establishes nothing: callers that rely on it are `Unresolved` with +`callee.contract`. Without the check, the logic's total semantics would give +meaning to what C++ leaves undefined: a trusted `post(1000 / result > 0)` +excluded `result == 0`. Spec functions stay total (Verus, ACSL), so a spec in +a contract adds no check, and `cppverify::recommends` stays a warning. + ### Verdicts that rest on other contracts A caller's proof uses its callees' contracts. When a callee's own From c851548b519298c02a81451435bf8c8acfada1a5 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:38 +0530 Subject: [PATCH 20/43] docs: Describe the contract well-formedness program in the architecture. --- docs/ARCHITECTURE.md | 40 ++++++++++++++++++++++++++++++++++++++-- 1 file changed, 38 insertions(+), 2 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 31db136f7f..4dc2142ea6 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -503,6 +503,37 @@ assume(Q[Result := y, Old(params) := args]); cell, materializes one disjoint initialized scalar object, then assumes the ordinary postconditions against that new heap. +**Contract well-formedness.** Every contract clause must be defined where it is +evaluated, as Dafny's per-method `CheckWellFormed$$f` procedure requires. Its +definedness checks are the core ones (`collectSafety`) and, under +`--check-ub`, the memory checks of the clause as written: `instrumentUBChecks` +records them before spec inlining, as it checks the body's accesses, beside +each written precondition and postcondition (`VFunction::PreconditionChecks`, +`PostconditionChecks`), each loop invariant (`VWhileStmt::InvariantChecks`), +and each `cppverify::check` (`VContractAssertStmt::MemoryChecks`). A read under +`old` is checked in the entry state, a quantifier's body at every value of +its range, and in a pre- or postcondition every parameter is its entry value. +Checking the inlined clause instead would check a spec's own reads, though a +spec is total, and repeat a lifted helper's argument reads for every use in +its body. Cloning and loop unrolling copy the records; passivization joins +each clause's memory checks to its core checks, one obligation per kind. + +`Passivizer::contract` builds a separate passive program, `f.contract` +(identity `f::contract`), on the interface version of `f` (UB-instrumented, +not spec-inlined: the one call sites use), so a lifted helper's checks are +reported at its call. `enter` assumes only the generated preconditions +(validity, separation, type invariants) and the entry facts; each written +precondition then gets its definedness asserts and is assumed, in order, so +each clause is checked where the ones before it hold. For an external +contract (trusted, or without a definition, `IsExternalContract`) +`returnAnywhere` makes the state callers assume: `havocFootprints`, the frame +code `emitCallStmt` uses, over its own footprints, and a fresh result. The +generated result validity is assumed, and each written postcondition is +checked and assumed in turn. The postconditions of a verified body are +checked in `run()` instead, in its final state, each clause's checks guarded +by the clauses before it. Loop invariants and `cppverify::check` get their +memory checks where they are checked. + ## Layer 3: Canonical Obligation IR `buildObligationModule` is the only passive-to-logic lowering path. It folds the @@ -1687,6 +1718,9 @@ caret included, as a compiler error is, and its JSON record carries the range. at once, and with a proof cache only the ordered queries run. f. Report verified / counterexample / unresolved / bounded-safe / exported, or kernel-certified. + g. Check that its contract is defined (`Passivizer::contract`) when that + program asserts anything, on the spec backend (Z3 under BMC); only a + failure is reported, as `contract of f`. 3. For each failure, run a second pass with `cppverify::recommends` checks → warnings. 4. Qualify each verdict by what it rests on: - a trusted function reports `Trusted`; an unmarked contract without a @@ -1701,10 +1735,12 @@ caret included, as a compiler error is, and its JSON record carries the range. that is not, is demoted (`spec.termination`, `spec.reads`, `spec.post`, `spec.inductive`, `callee.contract`), and a demoted check of a spec stops establishing its facts (`SpecReliance::Establishes`), a - demoted function its contract, until nothing changes; + demoted function its contract, until nothing changes; a contract whose + well-formedness check is not settled is not established either; - a least fixpoint then rejects circles: starting from no established fact, a verdict is sound once every fact it needs is, and a fact once - every verdict producing it is sound. It needs its callees' contracts + every verdict producing it is sound (a contract is produced by its + function's verdict and by its well-formedness check). It needs its callees' contracts and its proof blocks' callees, the definitions and frames of the specs it mentions, and the postconditions and unfoldings its module assumes (`PassiveProgram`/`ObligationModule::AssumedPosts` and From e1f4207f83d138c8cd65b00c83eae4937ac26222 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 23:22:39 +0530 Subject: [PATCH 21/43] docs: Describe how contracts get definedness checks. --- docs/UB-CHECKING.md | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/docs/UB-CHECKING.md b/docs/UB-CHECKING.md index 9a6f552190..7fe2584aec 100644 --- a/docs/UB-CHECKING.md +++ b/docs/UB-CHECKING.md @@ -46,6 +46,21 @@ names. `cpp-verify --no-check-ub` turns memory checking off; the core checks initialization, the lifetimes of bounded `new`/`delete` and automatic objects, and lifted-`constexpr` definedness) stay. +### Contracts + +A contract of an exec or proof function is evaluated as C++, so it gets the +same checks, each clause where it is evaluated: preconditions in order, each +where the ones before it hold, and postconditions in the state the function +returns in (for a trusted or bodiless function, every state its frame +allows). `Passivizer::contract` builds this check as a module of its own, +`contract of f`, reported only when it fails, and a contract that may be +undefined establishes nothing for callers. The memory checks of a clause, a +loop invariant, or a `cppverify::check` come from the instrumenter below, run +on the expression as written before spec inlining and recorded beside it +(`VMemoryCheck`): a read under `old` is checked in the entry state and a +quantifier's body at every value of its range. Spec functions stay total and +are never checked, whether applied or inlined; their division by zero is 0. + ## How the two obligations combine They interleave in one weakest-precondition pass rather than being generated as From 5f66e269e66cf27ea920f2eeab61f443a8e144bc Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:36:54 +0530 Subject: [PATCH 22/43] verify: Check a model a whole query finds on a slice of the budget with a check's own time. --- clang/lib/Verify/Backend/Z3Encode.cpp | 27 ++++++++++++++++++++------- 1 file changed, 20 insertions(+), 7 deletions(-) diff --git a/clang/lib/Verify/Backend/Z3Encode.cpp b/clang/lib/Verify/Backend/Z3Encode.cpp index 305b45949c..f1e25c56cb 100644 --- a/clang/lib/Verify/Backend/Z3Encode.cpp +++ b/clang/lib/Verify/Backend/Z3Encode.cpp @@ -3011,7 +3011,8 @@ z3::check_result Z3Encoder::certifyModels(const ObligationModule &Module, z3::model Current = Solver.get_model(); Z3CandidateModel Candidate(*this, Current); CertifyLimits Limits; - Limits.Deadline = QueryDeadline; + if (!SearchSlice) + Limits.Deadline = QueryDeadline; CertifyResult Certified = certifyModel(Candidate, Limits); bool BoundedDomain = false; if (Certified.Outcome == CertifyOutcome::Disputed && !Probed && @@ -3650,9 +3651,11 @@ bool Z3VerifyBackend::racesEncodings(const ObligationModule &Module) const { (Module.RequiredFeatures & logicFeature(LogicFeature::Sequences)); } -VerifyResult Z3VerifyBackend::solveQuery( - const ObligationModule &Module, const LogicExpr *Query, - std::optional TraceEventCount, unsigned Timeout, Race *Racing) { +VerifyResult +Z3VerifyBackend::solveQuery(const ObligationModule &Module, + const LogicExpr *Query, + std::optional TraceEventCount, + unsigned Timeout, Race *Racing, bool Slice) { // Every query gets an encoder of its own. A Z3 context keeps the state of // the queries solved in it, as far as an interrupted one got, and that // state steers the search of the next: a query refuted in 5 ms timed out @@ -3661,7 +3664,11 @@ VerifyResult Z3VerifyBackend::solveQuery( Z3Encoder Encoder; Encoder.setTimeoutMs(Timeout); Encoder.setResourceLimit(ResourceLimit); - Encoder.setCertifyTimeoutMs(CertifyTimeoutMs); + // A check gets the time a check of the module's queries gets. + Encoder.setCertifyTimeoutMs(Slice && !CertifyTimeoutMs + ? std::optional(TimeoutMs / 2) + : CertifyTimeoutMs); + Encoder.setSearchSlice(Slice); Encoder.setIntegerEncoding(IntegerEncoding); Encoder.setProfileQuantifiers(ProfileQuantifiers && Facts); Encoder.setSequenceFacts(Facts); @@ -3906,6 +3913,10 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) { const bool WholeUsedFullBudget = TimeoutMs == 0 ? !Module.LogicFunctions.empty() : WholeBudget >= TimeoutMs; + // A whole query on a slice of the budget still checks a model it finds: + // under load the search can take most of the slice, and the model, which + // settles the module, was then lost for want of time to check it. + const bool WholeSlice = !WholeUsedFullBudget; // With workers to spare, the obligations are solved one by one beside the // whole query. Both are exact, so whichever settles the module first // decides it and interrupts the other. @@ -3937,7 +3948,8 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) { } VerifyResult Whole; if (Racing) { - Whole = solveQuery(Module, nullptr, std::nullopt, WholeTimeout, &WholeRace); + Whole = solveQuery(Module, nullptr, std::nullopt, WholeTimeout, &WholeRace, + WholeSlice); if (Whole.Status == VerifyStatus::Verified || Whole.Status == VerifyStatus::Failed) Rivals.cancel(); @@ -3945,7 +3957,8 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) { if (OwnPool) Pool = nullptr; } else { - Whole = solveQuery(Module, nullptr, std::nullopt, WholeTimeout, nullptr); + Whole = solveQuery(Module, nullptr, std::nullopt, WholeTimeout, nullptr, + WholeSlice); } if (Whole.Status == VerifyStatus::Verified) return finishZ3Result(std::move(Whole)); From 894b040322b5d574ecdf67422a4a515765a452c3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:36:54 +0530 Subject: [PATCH 23/43] verify: Let the encoder tell a search slice from the query's whole time. --- clang/lib/Verify/Backend/Z3Encode.h | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/clang/lib/Verify/Backend/Z3Encode.h b/clang/lib/Verify/Backend/Z3Encode.h index ff1473e81f..af84baf42e 100644 --- a/clang/lib/Verify/Backend/Z3Encode.h +++ b/clang/lib/Verify/Backend/Z3Encode.h @@ -65,6 +65,7 @@ class Z3Encoder { std::optional TraceEventCount); std::chrono::steady_clock::time_point QueryStart; std::optional CertifyTimeoutMs; + bool SearchSlice = false; bool QuantifiedQuery = false; z3::solver freshSolver(); /// \p S.check() within \p Ms milliseconds (0: no limit), unknown at once @@ -289,6 +290,9 @@ class Z3Encoder { void setCertifyTimeoutMs(std::optional Ms) { CertifyTimeoutMs = Ms; } + /// The timeout is a slice of the query's time, for the search only: a model + /// found is checked with the check's own time, not what is left of it. + void setSearchSlice(bool Slice) { SearchSlice = Slice; } /// Stops the check running in this encoder, from any thread. void interrupt(); /// Lets checks run again after interrupt(). @@ -362,7 +366,7 @@ class Z3VerifyBackend : public VerifyBackend { VerifyResult solveQuery(const ObligationModule &Module, const LogicExpr *Query, std::optional TraceEventCount, - unsigned Timeout, Race *Racing); + unsigned Timeout, Race *Racing, bool Slice = false); VerifyResult verifyObligation(const ObligationModule &Module, const Obligation &Item, llvm::StringRef SemanticHash = {}, From 6e5c8dfeea3526b37c34f208b78d60d73ad089a8 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:36:55 +0530 Subject: [PATCH 24/43] docs: Explain how a whole query on a slice checks the model it finds. --- docs/ARCHITECTURE.md | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 4dc2142ea6..006f1f2079 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1874,8 +1874,15 @@ failing obligation's query does not finish within it, the whole query's counterexample stands. Before, that query could run to the timeout although the whole query had refuted the function in milliseconds: model search over quantified heap queries depends on the solver's search order, and 16 of 40 -random seeds took the full 30 s. A proof cache stores proofs of single -obligations, so with one only the obligations are solved. +random seeds took the full 30 s. A whole query given only a slice of the +budget (500 ms for a module without logic functions) checks a model it finds +with a check's own time (half the module's timeout, or `--certify-timeout`), +not with what is left of the slice (`Z3Encoder::setSearchSlice`): on one +loaded core its search took 460 ms of the 500, the check had 41 ms, the model +was left unchecked, the race went on, and the postcondition of +`certified_failure_attribution.cpp`, whose own search does not end, ran to +the 60 s timeout. A proof cache stores proofs of single obligations, so with +one only the obligations are solved. Every query runs in an encoder of its own (`Z3VerifyBackend::solveQuery`): a Z3 context keeps the state of the queries solved in it, as far as an From 217634edd38abf487efea838af557d8868b65e54 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:41:02 +0530 Subject: [PATCH 25/43] test: Check the hypothesis names of a contract's check that it is defined. --- clang/test/Verify/suite/lean_readable.cpp | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/clang/test/Verify/suite/lean_readable.cpp b/clang/test/Verify/suite/lean_readable.cpp index 618ed8feb1..875879ec0b 100644 --- a/clang/test/Verify/suite/lean_readable.cpp +++ b/clang/test/Verify/suite/lean_readable.cpp @@ -102,6 +102,12 @@ int poly(int x) return ((x + 1) * (x + 2) + (x + 3) * (x + 4)) * ((x + 5) * (x + 6) + (x + 7) * (x + 8)); } +[[cppverify::trusted]] int *pick(int *p) + cppverify::pre(cppverify::valid(p, 1) && *p > 0) + cppverify::modifies(*p) + cppverify::post(cppverify::result == p) + cppverify::post(100 / *p > 0); + // EXPORT: Exported: lean obligation: next // EXPORT: Exported: lean obligation: twice // EXPORT: Exported: lean obligation: count_up @@ -112,6 +118,7 @@ int poly(int x) // EXPORT: Exported: lean obligation: read // EXPORT: Exported: lean obligation: named // EXPORT: Exported: lean obligation: poly +// EXPORT: Exported: lean obligation: contract of pick // CHECK: theorem cppverify_imp_or {a b : Prop} (h : a → b) : ¬a ∨ b := // CHECK-NEXT: (Classical.em a).elim (fun ha => Or.inr (h ha)) Or.inl @@ -187,6 +194,20 @@ int poly(int x) // CHECK: (h_h_x_1 : h_x_1 = x_0 + (BitVec.ofInt 32 (1))) → // CHECK: (h_x_1_1 : x_1 = x_0 + h_x_1) → +// A contract's check that it is defined: each clause shown defined is +// assumed for the next, in the state a function without a verified body may +// return in, its frame and its result. +// CHECK: def cppverify_pick_contract_{{[0-9a-f]+}}_division_by_zero_{{[0-9a-f]+}}.readable : Prop := +// CHECK: (h_entry_1 : {{.*}}) → +// CHECK-NEXT: (h_null_1 : {{.*}}) → +// CHECK-NEXT: (h_null_2 : {{.*}}) → +// CHECK-NEXT: (h_object_1 : {{.*}}) → +// CHECK-NEXT: (h_pre_1 : {{.*}}) → +// CHECK-NEXT: (h_ret_1 : (∀ (__frame_address : Int), {{.*}})) → +// CHECK-NEXT: (h_ret_2 : __result_1 = (0 : Int) ∨ {{.*}}) → +// CHECK-NEXT: (h_post_1 : __result_1 = p_0) → +// CHECK-NEXT: ((heapSelectBv 32 __heap_1 p_0)).toInt ≠ (0 : Int) + // STUB: theorem cppverify_twice_edf933_postcondition_28de726e_proof : cppverify_twice_edf933_postcondition_28de726e := by // STUB-NEXT: apply cppverify_twice_edf933_postcondition_28de726e.of_readable // STUB-NEXT: intro __heap_alloc_0 __heap_live_0 __local_call_1_1 __local_call_2_1 __result_1 a_1 b_1 x_0 h_pre_1 h_null_1 h_null_2 h_call_next_1 h_a_1 h_call_next_2 h_b_1 h_result_1 From 17e505f74fbb5411b2081f096246f1e827d13bbf Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:41:03 +0530 Subject: [PATCH 26/43] docs: Name the hypotheses of a contract's check that it is defined. --- website/source/book/part-ii/ch17-backends-modular-calls.rst | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst index 24765588c7..b45d9cd41e 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -371,7 +371,11 @@ The names say where each assumption comes from: overflow; ``h_keep_``: the value of a variable on a path that skips its assignment; - ``h_check_``: a ``cppverify::check`` proved before; - ``h_spec__``: a spec's proved postcondition at an application. + ``h_spec__``: a spec's proved postcondition at an application; +- in a goal that checks a contract is defined (``contract of f``), + ``h_pre_`` and ``h_post_``: the clauses before the one checked, each + shown defined first; ``h_ret_``: what holds of the state a function + without a verified body may return in, its frame and its result. The numbers count within the goal, so a line added to the source renames no hypothesis. A disjunction the program wrote, such as From ed5bce2dde5daf952420ead3524ba593b9a55064 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Thu, 22 Oct 2026 17:41:03 +0530 Subject: [PATCH 27/43] docs: Note how a contract's check labels what it assumes. --- docs/ARCHITECTURE.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 006f1f2079..05c79ff87e 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1624,7 +1624,10 @@ uses when the source around it changes. `def`, `call:f`, `inv`, `cond`, `exit`, `keep`, `exact`, `check`, `spec:f`, ...) and of each entry assumption (`PassiveProgram::EntryOrigins`: `pre` for a written precondition, `entry` for a generated one, `null`, - `object`); spec checks built elsewhere default to `fact`. The Lean adapter + `object`); a contract's check that it is defined (`Passivizer::contract`) + labels each clause it assumes once shown defined `pre` or `post`, and the + state a function without a verified body returns in `ret`; spec checks + built elsewhere default to `fact`. The Lean adapter peels the marked chain into `G.readable`: `∀ vars axioms, let …; (h_pre_1 : A1) → … → C`, a hypothesis being the operand its `Or` negates (or `¬B` where simplification folded `¬¬B` to `B`), named `h__`, a From d783134a13508491afc51c9a7df3233d485ffbb8 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 01:00:08 +0530 Subject: [PATCH 28/43] test: Add a trusted contract with a check and its caller for the Lean contract test. --- clang/test/Verify/suite/Inputs/lean_contract_certify.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_contract_certify.cpp diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify.cpp b/clang/test/Verify/suite/Inputs/lean_contract_certify.cpp new file mode 100644 index 0000000000..f4a8361c40 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify.cpp @@ -0,0 +1,9 @@ +[[cppverify::trusted]] int sensor(int channel) + cppverify::pre(channel >= 0 && channel < 8) + cppverify::pre(100 / (channel + 1) > 0); + +int reading() + cppverify::post(true) +{ + return sensor(3); +} From 980876db9e8de7ae1ce2a5d228bbf3b1499059fb Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 01:00:08 +0530 Subject: [PATCH 29/43] test: Add the proof of cppverify_reading_8d7035_division_by_zero_df06c970 for the Lean contract test. --- .../cppverify_reading_8d7035_division_by_zero_df06c970.lean | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean new file mode 100644 index 0000000000..daf2ade742 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean @@ -0,0 +1,6 @@ +import CppVerify.User + +theorem cppverify_reading_8d7035_division_by_zero_df06c970_proof : cppverify_reading_8d7035_division_by_zero_df06c970 := by + apply cppverify_reading_8d7035_division_by_zero_df06c970.of_readable + intro __heap_alloc_0 __heap_live_0 h_null_1 h_null_2 + decide From b6c6b8d9786b4a9133c306e776de43e4ab694a98 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 01:00:09 +0530 Subject: [PATCH 30/43] test: Add the proof of cppverify_reading_8d7035_missing_return_54ae7c80 for the Lean contract test. --- .../cppverify_reading_8d7035_missing_return_54ae7c80.lean | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean new file mode 100644 index 0000000000..7bb7dd4b6b --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean @@ -0,0 +1,5 @@ +import CppVerify.User + +theorem cppverify_reading_8d7035_missing_return_54ae7c80_proof : cppverify_reading_8d7035_missing_return_54ae7c80 := by + apply cppverify_reading_8d7035_missing_return_54ae7c80.of_readable + trivial From 1e041c99207d2311434e95facd35cc86dafb4431 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 01:00:10 +0530 Subject: [PATCH 31/43] test: Add the proof of cppverify_reading_8d7035_postcondition_54ae7c80 for the Lean contract test. --- .../cppverify_reading_8d7035_postcondition_54ae7c80.lean | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean new file mode 100644 index 0000000000..97d154cc3c --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean @@ -0,0 +1,5 @@ +import CppVerify.User + +theorem cppverify_reading_8d7035_postcondition_54ae7c80_proof : cppverify_reading_8d7035_postcondition_54ae7c80 := by + apply cppverify_reading_8d7035_postcondition_54ae7c80.of_readable + trivial From 6494e287168d2f53c76f918c87c906b763e8eefb Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 01:00:10 +0530 Subject: [PATCH 32/43] test: Add the proof of cppverify_reading_8d7035_precondition_155ffe95 for the Lean contract test. --- .../cppverify_reading_8d7035_precondition_155ffe95.lean | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean new file mode 100644 index 0000000000..d8692c5599 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean @@ -0,0 +1,6 @@ +import CppVerify.User + +theorem cppverify_reading_8d7035_precondition_155ffe95_proof : cppverify_reading_8d7035_precondition_155ffe95 := by + apply cppverify_reading_8d7035_precondition_155ffe95.of_readable + intro __heap_alloc_0 __heap_live_0 h_null_1 h_null_2 + simp [cppIntDiv] From a88b94243e7af6d4cbed58ada732080953881c55 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 01:00:11 +0530 Subject: [PATCH 33/43] test: Add the proof of cppverify_reading_8d7035_precondition_814bc5b2 for the Lean contract test. --- .../cppverify_reading_8d7035_precondition_814bc5b2.lean | 6 ++++++ 1 file changed, 6 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean new file mode 100644 index 0000000000..5779536cb6 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean @@ -0,0 +1,6 @@ +import CppVerify.User + +theorem cppverify_reading_8d7035_precondition_814bc5b2_proof : cppverify_reading_8d7035_precondition_814bc5b2 := by + apply cppverify_reading_8d7035_precondition_814bc5b2.of_readable + intro __heap_alloc_0 __heap_live_0 h_null_1 h_null_2 + decide From 9ed1977fa0ec211b9042b7e96186000248580140 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 01:00:11 +0530 Subject: [PATCH 34/43] test: Add the proof of cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d for the Lean contract test. --- ...sensor_contract_eb6f5c_division_by_zero_d81a153d.lean | 9 +++++++++ 1 file changed, 9 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean new file mode 100644 index 0000000000..8e3effb2e7 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean @@ -0,0 +1,9 @@ +import CppVerify.User + +theorem cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d_proof : cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d := by + apply cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.of_readable + intro __heap_alloc_0 __heap_live_0 channel_0 h_null_1 h_null_2 h_pre_1 + simp only [cppBvSle, BitVec.sle_iff_toInt_le, BitVec.toInt_ofInt] at h_pre_1 + have := h_pre_1.1 + simp at this + omega From 76511801c7c49604b4792e32966f96e839153e1b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 01:00:12 +0530 Subject: [PATCH 35/43] test: Check that a certified contract check establishes the contract and an unproved one does not. --- .../Verify/suite/lean_contract_certify.test | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 clang/test/Verify/suite/lean_contract_certify.test diff --git a/clang/test/Verify/suite/lean_contract_certify.test b/clang/test/Verify/suite/lean_contract_certify.test new file mode 100644 index 0000000000..9823942ef9 --- /dev/null +++ b/clang/test/Verify/suite/lean_contract_certify.test @@ -0,0 +1,25 @@ +# REQUIRES: lean +# +# A contract's check that it is defined is a Lean goal like any function's. +# Once its proof certifies, the contract is established for its callers; while +# it does not, every caller that relies on it is unresolved. +# +# RUN: rm -rf %t && mkdir -p %t +# RUN: %cpp-verify --backend=lean --lean-project=%t/p %S/Inputs/lean_contract_certify.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT +# RUN: cp %S/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_*.lean %t/p/CppVerify/Proofs/cppverify_sensor_contract_eb6f5c/ +# RUN: cp %S/Inputs/lean_contract_certify_proofs/cppverify_reading_*.lean %t/p/CppVerify/Proofs/cppverify_reading_8d7035/ +# RUN: %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %S/Inputs/lean_contract_certify.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFIED +# +# The check's proof left a stub: the contract establishes nothing. +# RUN: sed -i 's/^ omega$/ sorry/' %t/p/CppVerify/Proofs/cppverify_sensor_contract_eb6f5c/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean +# RUN: not %cpp-verify --backend=lean --lean-project=%t/p --lean-certify %S/Inputs/lean_contract_certify.cpp -- 2>&1 | FileCheck %s --check-prefix=STUB + +# EXPORT: Trusted: sensor (contract assumed, not verified) +# EXPORT: Exported: lean obligation: contract of sensor +# EXPORT: Exported: lean obligation: reading + +# CERTIFIED: Certified: contract of sensor [backend=Lean] +# CERTIFIED: Certified: reading [backend=Lean] [trusts=sensor] + +# STUB: Unresolved: lean obligation: contract of sensor (Lean certification failed: the proof of fn_5f5a3673656e736f7269::contract::division-by-zero@3:22: {{.*}}declaration uses `sorry` +# STUB: Unresolved: reading [backend=Lean] [reason=callee.contract] (relies on the contract of sensor (its clauses are not shown to be defined), which is not established) From 0e22bcc17f7b128c06cba90d54eecee7f9848bd8 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 01:00:12 +0530 Subject: [PATCH 36/43] docs: Say how a contract's check is exported and certified under Lean. --- website/source/language/functions-loops.rst | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/website/source/language/functions-loops.rst b/website/source/language/functions-loops.rst index d9a99543df..5bae278634 100644 --- a/website/source/language/functions-loops.rst +++ b/website/source/language/functions-loops.rst @@ -209,7 +209,10 @@ on it is ``Unresolved`` with reason ``callee.contract``, as ``scaled`` is. Its proof read ``1000 / r > 0`` as excluding ``r == 0``, since the logic defines a division by zero, but C++ does not, so nothing excludes it. The function's own verdict is about its body and does not change. The check prints nothing when it -holds. +holds. With ``--backend=lean`` it is exported as goals of its own, +``Exported: lean obligation: contract of f``; once their proofs certify, +``Certified: contract of f`` establishes the contract, and until then the +callers that rely on it are ``Unresolved`` with reason ``callee.contract``. Spec functions stay total, as in Verus and ACSL: a spec's division by zero is 0, so applying a spec in a contract adds no check, and From 2ea7fcee60f96554971801e16aabf5c875a5f535 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 03:55:17 +0530 Subject: [PATCH 37/43] verify: Retry a whole query its slice leaves unresolved as a task of the race, and stop it when the obligations settle the module. --- clang/lib/Verify/Backend/Z3Encode.cpp | 39 +++++++++++++++++++++++---- 1 file changed, 34 insertions(+), 5 deletions(-) diff --git a/clang/lib/Verify/Backend/Z3Encode.cpp b/clang/lib/Verify/Backend/Z3Encode.cpp index f1e25c56cb..974ba5156c 100644 --- a/clang/lib/Verify/Backend/Z3Encode.cpp +++ b/clang/lib/Verify/Backend/Z3Encode.cpp @@ -3938,22 +3938,51 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) { Ordered = Group->async([this, &Module, &Rivals, &WholeRace] { std::vector Results = verifyObligations(Module, /*StopAtFailure=*/true, &Rivals); - if (Results.size() == Module.Obligations.size() && - llvm::all_of(Results, [](const VerifyResult &R) { - return R.Status == VerifyStatus::Verified; - })) + // The obligations settle the module when they prove all of it or one + // fails, and the whole query, or its retry, is then stopped. + if (llvm::any_of(Results, + [](const VerifyResult &R) { + return R.Status == VerifyStatus::Failed; + }) || + (Results.size() == Module.Obligations.size() && + llvm::all_of(Results, [](const VerifyResult &R) { + return R.Status == VerifyStatus::Verified; + }))) WholeRace.cancel(); return Results; }); } VerifyResult Whole; + auto retryable = [&](const VerifyResult &Result) { + return Result.Status == VerifyStatus::Unresolved && !WholeUsedFullBudget && + !SkipWholeModuleRetry && !spent(); + }; + bool RetriedWhole = false; if (Racing) { Whole = solveQuery(Module, nullptr, std::nullopt, WholeTimeout, &WholeRace, WholeSlice); + // A whole query its slice leaves unresolved is retried with the full + // budget as one more task of the race, after the obligations: a free + // worker runs it beside them, so that an obligation whose search does + // not end cannot hold it back; without one, it runs after them, as alone. + std::shared_future Retry; + if (retryable(Whole) && !WholeRace.Cancelled) { + RetriedWhole = true; + Retry = Group->async([this, &Module, &WholeRace, &Rivals] { + VerifyResult Result = solveQuery(Module, nullptr, std::nullopt, + budget(TimeoutMs), &WholeRace); + if (Result.Status == VerifyStatus::Verified || + Result.Status == VerifyStatus::Failed) + Rivals.cancel(); + return Result; + }); + } if (Whole.Status == VerifyStatus::Verified || Whole.Status == VerifyStatus::Failed) Rivals.cancel(); Group->wait(); + if (RetriedWhole) + Whole = Retry.get(); if (OwnPool) Pool = nullptr; } else { @@ -3998,7 +4027,7 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) { } auto retryWhole = [&](VerifyResult SplitResult) { - if (WholeUsedFullBudget || SkipWholeModuleRetry || spent()) + if (RetriedWhole || !retryable(SplitResult)) return finishZ3Result(std::move(SplitResult)); VerifyResult Retry = solveQuery(Module, nullptr, std::nullopt, budget(TimeoutMs), nullptr); From 1b8b59997cee2ef6620ec966b992701e707089f5 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 03:55:17 +0530 Subject: [PATCH 38/43] docs: Explain how a racing whole query is retried beside the obligations. --- docs/ARCHITECTURE.md | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 05c79ff87e..6cb13581e3 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1884,8 +1884,17 @@ not with what is left of the slice (`Z3Encoder::setSearchSlice`): on one loaded core its search took 460 ms of the 500, the check had 41 ms, the model was left unchecked, the race went on, and the postcondition of `certified_failure_attribution.cpp`, whose own search does not end, ran to -the 60 s timeout. A proof cache stores proofs of single obligations, so with -one only the obligations are solved. +the 60 s timeout. Racing, a whole query its slice leaves unresolved is +retried with the full budget as one more task of the race, queued after the +obligations: a free worker runs it beside them, and without one the +function's own thread runs it after them, as with one job. Before, the retry +always waited for the obligations, so an obligation whose search does not end +held it back until that obligation's timeout: on two loaded cores the whole +query of that test needs about 600 ms, more than its slice, and the test took +61 s with `--jobs=3`; it now takes 1.2 s. The obligations stop the whole +query, or its retry, whenever they settle the module: when one fails, as +when they prove all of it. A proof cache stores proofs of single +obligations, so with one only the obligations are solved. Every query runs in an encoder of its own (`Z3VerifyBackend::solveQuery`): a Z3 context keeps the state of the queries solved in it, as far as an From d2af39503d08dc8de20001f27b740ca078ff39f3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 05:52:43 +0530 Subject: [PATCH 39/43] verify: Declare the work a whole query may do and the cap on the obligations that choose its failure. --- clang/lib/Verify/Backend/Z3Encode.h | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/clang/lib/Verify/Backend/Z3Encode.h b/clang/lib/Verify/Backend/Z3Encode.h index af84baf42e..9fc483a24b 100644 --- a/clang/lib/Verify/Backend/Z3Encode.h +++ b/clang/lib/Verify/Backend/Z3Encode.h @@ -324,6 +324,9 @@ class Z3VerifyBackend : public VerifyBackend { unsigned SolverTimeoutMs; std::optional CollectionTimeoutMs; unsigned ResourceLimit; + /// While the obligations only choose the failure to report, the work each + /// of their queries may do: the work the complete query's probe had, or 0. + unsigned UnitsCap = 0; unsigned Jobs; llvm::StdThreadPool *Pool; uint64_t MaxQueryNodes; @@ -366,7 +369,8 @@ class Z3VerifyBackend : public VerifyBackend { VerifyResult solveQuery(const ObligationModule &Module, const LogicExpr *Query, std::optional TraceEventCount, - unsigned Timeout, Race *Racing, bool Slice = false); + unsigned Timeout, Race *Racing, bool Slice = false, + unsigned Units = 0); VerifyResult verifyObligation(const ObligationModule &Module, const Obligation &Item, llvm::StringRef SemanticHash = {}, From 66cf8cb55968d7047f724a6fe1665b4b68a0bac2 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 05:52:43 +0530 Subject: [PATCH 40/43] verify: Bound the whole-query probe of a module without specs by solver work instead of 500 ms. --- clang/lib/Verify/Backend/Z3Encode.cpp | 68 ++++++++++++++++----------- 1 file changed, 41 insertions(+), 27 deletions(-) diff --git a/clang/lib/Verify/Backend/Z3Encode.cpp b/clang/lib/Verify/Backend/Z3Encode.cpp index 974ba5156c..979c920828 100644 --- a/clang/lib/Verify/Backend/Z3Encode.cpp +++ b/clang/lib/Verify/Backend/Z3Encode.cpp @@ -2733,6 +2733,9 @@ constexpr unsigned RefinementSliceMs = 500; /// counterexample on a loaded machine. constexpr unsigned HiddenSearchSliceMs = 2000; constexpr unsigned HiddenRoundsBeforeNative = 8; +/// Resource units of the complete query of a module without specs before +/// its ordered obligations. +constexpr unsigned WholeProbeUnits = 6000000; } // namespace std::optional Z3Encoder::verifyNatively( @@ -3651,11 +3654,10 @@ bool Z3VerifyBackend::racesEncodings(const ObligationModule &Module) const { (Module.RequiredFeatures & logicFeature(LogicFeature::Sequences)); } -VerifyResult -Z3VerifyBackend::solveQuery(const ObligationModule &Module, - const LogicExpr *Query, - std::optional TraceEventCount, - unsigned Timeout, Race *Racing, bool Slice) { +VerifyResult Z3VerifyBackend::solveQuery( + const ObligationModule &Module, const LogicExpr *Query, + std::optional TraceEventCount, unsigned Timeout, Race *Racing, + bool Slice, unsigned Units) { // Every query gets an encoder of its own. A Z3 context keeps the state of // the queries solved in it, as far as an interrupted one got, and that // state steers the search of the next: a query refuted in 5 ms timed out @@ -3663,7 +3665,11 @@ Z3VerifyBackend::solveQuery(const ObligationModule &Module, auto solve = [&](bool Facts, Race *Pair) { Z3Encoder Encoder; Encoder.setTimeoutMs(Timeout); - Encoder.setResourceLimit(ResourceLimit); + unsigned Limit = ResourceLimit; + for (unsigned Cap : {UnitsCap, Units}) + if (Cap && (!Limit || Cap < Limit)) + Limit = Cap; + Encoder.setResourceLimit(Limit); // A check gets the time a check of the module's queries gets. Encoder.setCertifyTimeoutMs(Slice && !CertifyTimeoutMs ? std::optional(TimeoutMs / 2) @@ -3900,23 +3906,26 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) { // can make it far harder than every ordered one (a ghost-sequence sum loop // timed out whole after 30 s; its obligations take 0.2 s), so there it gets // a sixth (at least 5 s) before them and the rest after. For spec-free - // programs, a short probe preserves the budget for the ordered obligations. + // programs, a probe of a fixed amount of work preserves the budget for the + // ordered obligations. Work, not time: a probe of 500 ms gave up under load + // and in an assertions build where an idle release build refuted the + // module, and the ordered obligations then ran to the timeout of one whose + // search does not end. WholeProbeUnits covers every probe of the test suite + // that a release build decided within 500 ms (the most took 5.2M units). + const unsigned ProbeUnits = + Module.LogicFunctions.empty() ? WholeProbeUnits : 0; const bool OverCollections = Module.RequiredFeatures & (logicFeature(LogicFeature::Sequences) | logicFeature(LogicFeature::Collections)); - const unsigned WholeBudget = - Module.LogicFunctions.empty() - ? 500U - : (TimeoutMs == 0 || !OverCollections - ? TimeoutMs - : std::max(TimeoutMs / 6, 5000U)); + const unsigned WholeBudget = ProbeUnits || TimeoutMs == 0 || !OverCollections + ? TimeoutMs + : std::max(TimeoutMs / 6, 5000U); const bool WholeUsedFullBudget = - TimeoutMs == 0 ? !Module.LogicFunctions.empty() - : WholeBudget >= TimeoutMs; + !ProbeUnits && (TimeoutMs == 0 || WholeBudget >= TimeoutMs); // A whole query on a slice of the budget still checks a model it finds: // under load the search can take most of the slice, and the model, which // settles the module, was then lost for want of time to check it. - const bool WholeSlice = !WholeUsedFullBudget; + const bool WholeSlice = !WholeUsedFullBudget && !ProbeUnits; // With workers to spare, the obligations are solved one by one beside the // whole query. Both are exact, so whichever settles the module first // decides it and interrupts the other. @@ -3952,17 +3961,21 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) { return Results; }); } - VerifyResult Whole; + VerifyResult Whole = + solveQuery(Module, nullptr, std::nullopt, WholeTimeout, + Racing ? &WholeRace : nullptr, WholeSlice, ProbeUnits); + // A probe that ran out of time, not work, had the full budget already. + const bool WholeHadFullBudget = + WholeUsedFullBudget || + (ProbeUnits && Whole.Reason == VerifyReason::SolverTimeout); auto retryable = [&](const VerifyResult &Result) { - return Result.Status == VerifyStatus::Unresolved && !WholeUsedFullBudget && + return Result.Status == VerifyStatus::Unresolved && !WholeHadFullBudget && !SkipWholeModuleRetry && !spent(); }; bool RetriedWhole = false; if (Racing) { - Whole = solveQuery(Module, nullptr, std::nullopt, WholeTimeout, &WholeRace, - WholeSlice); - // A whole query its slice leaves unresolved is retried with the full - // budget as one more task of the race, after the obligations: a free + // A whole query its probe or slice leaves unresolved is retried with the + // full budget as one more task of the race, after the obligations: a free // worker runs it beside them, so that an obligation whose search does // not end cannot hold it back; without one, it runs after them, as alone. std::shared_future Retry; @@ -3985,9 +3998,6 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) { Whole = Retry.get(); if (OwnPool) Pool = nullptr; - } else { - Whole = solveQuery(Module, nullptr, std::nullopt, WholeTimeout, nullptr, - WholeSlice); } if (Whole.Status == VerifyStatus::Verified) return finishZ3Result(std::move(Whole)); @@ -3999,9 +4009,13 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) { if (Whole.Status == VerifyStatus::Failed) { // The complete query's counterexample is certified, so the obligations // only choose the failure to report, within the complete query's budget, - // the same way with any number of jobs. + // its time and a probe's work, the same way with any number of jobs. const unsigned FullTimeout = TimeoutMs; - llvm::scope_exit Restore([&] { TimeoutMs = FullTimeout; }); + UnitsCap = ProbeUnits; + llvm::scope_exit Restore([&] { + TimeoutMs = FullTimeout; + UnitsCap = 0; + }); std::vector Results = verifyObligations( Module, /*StopAtFailure=*/true, nullptr, WholeTimeout); bool SawUnresolved = false; From fc79b8da7180e08ef775328ba8bee3523a91121b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 05:52:43 +0530 Subject: [PATCH 41/43] docs: Explain why the whole query's probe is bounded by work, and what it costs. --- docs/ARCHITECTURE.md | 63 +++++++++++++++++++++++++++++--------------- 1 file changed, 42 insertions(+), 21 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 6cb13581e3..63850c94f7 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1871,30 +1871,51 @@ the obligations decide, exactly as after a whole query alone, so the verdict does not depend on the jobs. When the whole query yields a certified counterexample, the obligations only choose which failure is reported, the first in source order: the ones solved beside it are stopped, and they are -solved in order with every query's timeout at most the whole query's own, -with any number of jobs, so the choice does not depend on them either. If the -failing obligation's query does not finish within it, the whole query's +solved in order within the whole query's own budget, its timeout and, for a +probe (below), its work, with any number of jobs, so the choice does not +depend on them either (`Z3VerifyBackend::UnitsCap`). If the failing +obligation's query does not finish within it, the whole query's counterexample stands. Before, that query could run to the timeout although the whole query had refuted the function in milliseconds: model search over quantified heap queries depends on the solver's search order, and 16 of 40 -random seeds took the full 30 s. A whole query given only a slice of the -budget (500 ms for a module without logic functions) checks a model it finds -with a check's own time (half the module's timeout, or `--certify-timeout`), -not with what is left of the slice (`Z3Encoder::setSearchSlice`): on one -loaded core its search took 460 ms of the 500, the check had 41 ms, the model -was left unchecked, the race went on, and the postcondition of -`certified_failure_attribution.cpp`, whose own search does not end, ran to -the 60 s timeout. Racing, a whole query its slice leaves unresolved is -retried with the full budget as one more task of the race, queued after the -obligations: a free worker runs it beside them, and without one the -function's own thread runs it after them, as with one job. Before, the retry -always waited for the obligations, so an obligation whose search does not end -held it back until that obligation's timeout: on two loaded cores the whole -query of that test needs about 600 ms, more than its slice, and the test took -61 s with `--jobs=3`; it now takes 1.2 s. The obligations stop the whole -query, or its retry, whenever they settle the module: when one fails, as -when they prove all of it. A proof cache stores proofs of single -obligations, so with one only the obligations are solved. +random seeds took the full 30 s. + +The whole query of a module without logic functions is a probe of a fixed +amount of work, `WholeProbeUnits` (6 million) Z3 resource units, with the +module's timeout as its bound in time, so where it stops depends neither on +the load nor on the build. It had 500 ms before. In an assertions build, or +on a loaded core, the whole query of `certified_failure_attribution.cpp` +(about 700 thousand units) did not finish in that time; with one job its +obligations then ran, the postcondition among them, whose own search does +not end, and the function ended `Unresolved` with `solver.timeout` after +121 s on one core shared with two busy loops. The assertions build now +reports the test's counterexample there in 7 s, with one job or three. Every +probe of the test suite that an idle release build decided within 500 ms +took at most 5.2 million units (99% of the 2622 took less than 200 +thousand); the three that took 5.2 million are those of the UTF-8 case +study. A probe that does not decide costs more than before: the suite has 18, +which do 1,900 to 13,000 units a millisecond, so 0.5 to 3 s each instead of +0.5 s. With one job the suite takes 1331 s instead of 1321 s on an assertions +build, most of it in `loop_frames.cpp` (3.6 s, now 8.8 s), whose five failing +functions each spend 1.4 s on a probe that never decides; with more jobs the +obligations solved beside the probe stop it once they settle the module. A +probe that its work bound stops is retried with the full budget; one that +its timeout stops already had it. A whole +query given only a slice of the budget (a sixth of it over collections) +checks a model it finds with a check's own time (half the module's timeout, +or `--certify-timeout`), not with what is left of the slice +(`Z3Encoder::setSearchSlice`): on one loaded core the search of a 500 ms +probe took 460 ms, the check had 41 ms, and the model was left unchecked. +Racing, a whole query its probe or slice leaves unresolved is retried with +the full budget as one more task of the race, queued after the obligations: +a free worker runs it beside them, and without one the function's own thread +runs it after them, as with one job. Before, the retry always waited for the +obligations, so an obligation whose search does not end held it back until +that obligation's timeout: with the 500 ms probe, that test took 61 s with +`--jobs=3` on two loaded cores. The obligations stop the whole query, or its +retry, whenever they settle the module: when one fails, as when they prove +all of it. A proof cache stores proofs of single obligations, so with one +only the obligations are solved. Every query runs in an encoder of its own (`Z3VerifyBackend::solveQuery`): a Z3 context keeps the state of the queries solved in it, as far as an From 2f3e5063ab5e6e1ac4a2f5b99c0f5e22e47b5858 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 05:52:44 +0530 Subject: [PATCH 42/43] docs: Say that the probe of a complete query is a fixed amount of solver work. --- website/source/language/tooling.rst | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index 9431c7dee2..b9ff374851 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -539,7 +539,12 @@ contracts, spec termination, trust) run after every function. Each worker owns a fresh Z3 context/solver or a separate cvc5 process; no solver state is shared between workers. The first failing source obligation is therefore identical for ``--jobs=1`` and ``--jobs=N`` even if worker completion order -differs. Lean generation and certification stay serial. The compile-time +differs. The complete query of a function without spec functions first gets +a fixed amount of solver work (Z3 resource units), with the query timeout +only as a bound in time, so on a loaded machine it stops where it stops on +an idle one, unless the timeout passes first; once it has found a +counterexample, the obligations that choose the failure to report get the +same work each. Lean generation and certification stay serial. The compile-time verifier (``clang++ -fverify-contracts``) always uses one job and the default limits; use ``cpp-verify`` for ``--jobs`` and the other options. From 6dbd097e2bc427499b8c51309d475c185f570c79 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 05:52:44 +0530 Subject: [PATCH 43/43] docs: Note that a function's result no longer depends on the machine's load. --- website/source/release-notes.rst | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 1b3930a842..79e5a9ee33 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -314,6 +314,16 @@ documents the latest release, ``/X.Y/`` each release series (``/0.1/`` is page names its version, and each release's archive and notes link to its own series. +**Results that depended on load.** The complete query of a function without +spec functions had 500 ms before its obligations were solved one by one. On a +loaded machine, or in a slower build, it could give up on a counterexample +that an idle machine found in that time, and an obligation whose search does +not end then ran to the timeout: a false claim took minutes and ended +``Unresolved`` with ``solver.timeout``. That query now gets a fixed amount of +solver work (6 million Z3 resource units), with the timeout only as a bound +in time, so it stops where it would on an idle machine +(:doc:`language/tooling`). + **cvc5 1.4.** Every query over sets, multisets, and maps failed with cvc5 1.4, which requires extended arrays for constant arrays; such a query now enables them itself (:doc:`language/tooling`).