From 2781da8401fb8db8297a4b0a99e11c54bf158a93 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:46 +0530 Subject: [PATCH 01/52] verify: Add a budget of the expression nodes a construction builds on a thread. --- clang/lib/Verify/IR/NodeBudget.h | 61 ++++++++++++++++++++++++++++++++ 1 file changed, 61 insertions(+) create mode 100644 clang/lib/Verify/IR/NodeBudget.h diff --git a/clang/lib/Verify/IR/NodeBudget.h b/clang/lib/Verify/IR/NodeBudget.h new file mode 100644 index 0000000000..cc6f484d14 --- /dev/null +++ b/clang/lib/Verify/IR/NodeBudget.h @@ -0,0 +1,61 @@ +//===--- NodeBudget.h - Bounds on the expression trees built ----*- C++ -*-===// +#ifndef LLVM_CLANG_VERIFY_IR_NODEBUDGET_H +#define LLVM_CLANG_VERIFY_IR_NODEBUDGET_H + +#include + +namespace clang { +namespace verify { + +/// Counts the expression nodes (VExpr and LogicExpr) built on this thread +/// while it lives, against the limit the driver sets for the function being +/// verified (--max-query-nodes). A construction whose size can outgrow the +/// program, such as a spec unfolded as deep as its fuel, runs in a budget +/// and stops where it can once the limit is passed; its owner then reports +/// the function as too large and never uses the partial result. +class NodeBudget { +public: + /// The limit for the budgets of this thread while it lives; 0: none. + class Limit { + public: + explicit Limit(uint64_t Nodes); + ~Limit(); + Limit(const Limit &) = delete; + Limit &operator=(const Limit &) = delete; + + private: + uint64_t Saved; + }; + + /// A budget inside another counts toward it too. + NodeBudget(); + ~NodeBudget(); + NodeBudget(const NodeBudget &) = delete; + NodeBudget &operator=(const NodeBudget &) = delete; + + /// The nodes built in this budget and those enclosing it. + uint64_t built() const { return Built + (Outer ? Outer->built() : 0); } + /// The thread's limit when the budget began, 0 when there is none. + uint64_t limit() const { return Max; } + bool exceeded() const { return Max != 0 && built() > Max; } + + /// Whether the innermost budget of this thread is exceeded: where a + /// construction can stop, it checks this. + static bool exhausted() { return Active && Active->exceeded(); } + /// Counts one node; the constructors of expression nodes call it. + static void count() { + if (Active) + ++Active->Built; + } + +private: + static thread_local NodeBudget *Active; + NodeBudget *Outer; + uint64_t Built = 0; + uint64_t Max; +}; + +} // namespace verify +} // namespace clang + +#endif From 076091d7d81cc83a1b123e38811f4a5c3d3ec156 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:46 +0530 Subject: [PATCH 02/52] verify: Implement the node budget and the per-thread node limit. --- clang/lib/Verify/IR/NodeBudget.cpp | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 clang/lib/Verify/IR/NodeBudget.cpp diff --git a/clang/lib/Verify/IR/NodeBudget.cpp b/clang/lib/Verify/IR/NodeBudget.cpp new file mode 100644 index 0000000000..dee0280c01 --- /dev/null +++ b/clang/lib/Verify/IR/NodeBudget.cpp @@ -0,0 +1,23 @@ +//===--- NodeBudget.cpp ---------------------------------------------------===// +#include "NodeBudget.h" + +using namespace clang; +using namespace verify; + +thread_local NodeBudget *NodeBudget::Active = nullptr; + +static thread_local uint64_t ThreadLimit = 0; + +NodeBudget::Limit::Limit(uint64_t Nodes) : Saved(ThreadLimit) { + ThreadLimit = Nodes; +} + +NodeBudget::Limit::~Limit() { ThreadLimit = Saved; } + +NodeBudget::NodeBudget() : Outer(Active), Max(ThreadLimit) { Active = this; } + +NodeBudget::~NodeBudget() { + Active = Outer; + if (Outer) + Outer->Built += Built; +} From bc8b9f9eb87b7446d3bbf80955d6582a985a1660 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:47 +0530 Subject: [PATCH 03/52] verify: Build the node budget. --- clang/lib/Verify/CMakeLists.txt | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/lib/Verify/CMakeLists.txt b/clang/lib/Verify/CMakeLists.txt index d13eed30f3..654c7235b0 100644 --- a/clang/lib/Verify/CMakeLists.txt +++ b/clang/lib/Verify/CMakeLists.txt @@ -24,6 +24,7 @@ get_property(_cppverify_z3_ep GLOBAL PROPERTY CPPVERIFY_Z3_EP_TARGET) add_clang_library(clangVerify IR/VExpr.cpp IR/VStmt.cpp + IR/NodeBudget.cpp Frontend/ASTConverter.cpp Transform/Passivize.cpp Transform/Inductive.cpp From 179c9a8ae104b296e97e8984c5c2a00cdeafb3e5 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:48 +0530 Subject: [PATCH 04/52] verify: Count every VCR expression node against the node budget. --- clang/lib/Verify/IR/VExpr.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/clang/lib/Verify/IR/VExpr.h b/clang/lib/Verify/IR/VExpr.h index e0ace8e494..97de4e4705 100644 --- a/clang/lib/Verify/IR/VExpr.h +++ b/clang/lib/Verify/IR/VExpr.h @@ -2,6 +2,7 @@ #ifndef LLVM_CLANG_VERIFY_IR_VEXPR_H #define LLVM_CLANG_VERIFY_IR_VEXPR_H +#include "NodeBudget.h" #include "VType.h" #include "clang/Basic/SourceLocation.h" #include "llvm/ADT/STLFunctionalExtras.h" @@ -88,7 +89,9 @@ class VExpr { protected: VExpr(Kind K, VType Ty, SourceLocation Loc) - : K(K), Ty(Ty), Loc(Loc), EndLoc(Loc) {} + : K(K), Ty(Ty), Loc(Loc), EndLoc(Loc) { + NodeBudget::count(); + } }; class VLiteralExpr : public VExpr { From 98d83375a031bdb13bd3fde952f7e49ab829983d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:48 +0530 Subject: [PATCH 05/52] verify: Count every logic expression node against the node budget. --- clang/lib/Verify/Backend/Obligation.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/clang/lib/Verify/Backend/Obligation.h b/clang/lib/Verify/Backend/Obligation.h index ba16118533..463f109f4a 100644 --- a/clang/lib/Verify/Backend/Obligation.h +++ b/clang/lib/Verify/Backend/Obligation.h @@ -3,6 +3,7 @@ #ifndef LLVM_CLANG_VERIFY_BACKEND_OBLIGATION_H #define LLVM_CLANG_VERIFY_BACKEND_OBLIGATION_H +#include "../IR/NodeBudget.h" #include "clang/Basic/SourceLocation.h" #include "llvm/Support/Error.h" #include @@ -217,7 +218,7 @@ class LogicExpr { /// archives. std::vector> Patterns; - explicit LogicExpr(Kind K) : K(K) {} + explicit LogicExpr(Kind K) : K(K) { NodeBudget::count(); } }; // Compatibility name for the Z3/spec adapters while they migrate internally. From ae781d3b0332a51a3e7dbfee7dee5a5bffd7e420 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:49 +0530 Subject: [PATCH 06/52] verify: Declare the size error and the node limit of building a module. --- clang/lib/Verify/Backend/ObligationLowering.h | 31 ++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/clang/lib/Verify/Backend/ObligationLowering.h b/clang/lib/Verify/Backend/ObligationLowering.h index 591892fc06..2a4af2f327 100644 --- a/clang/lib/Verify/Backend/ObligationLowering.h +++ b/clang/lib/Verify/Backend/ObligationLowering.h @@ -10,8 +10,37 @@ namespace clang { namespace verify { +/// Something a function's verification builds would have more expression +/// nodes than the limit allows (--max-query-nodes), found before or as it +/// was built: the obligations, each repeating every assumption before it +/// (their size is known before any is built), or a spec's definition +/// unfolded as deep as its fuel. +class ObligationSizeError : public llvm::ErrorInfo { +public: + static char ID; + ObligationSizeError(std::string What, uint64_t Nodes, uint64_t Limit, + std::string Advice) + : What(std::move(What)), Nodes(Nodes), Limit(Limit), + Advice(std::move(Advice)) {} + /// The obligations of a module of \p Nodes nodes. + static llvm::Error obligations(uint64_t Nodes, uint64_t Limit); + void log(llvm::raw_ostream &OS) const override; + std::error_code convertToErrorCode() const override { + return llvm::inconvertibleErrorCode(); + } + std::string What; + /// At least this many: a construction stops once it passes the limit. + uint64_t Nodes; + uint64_t Limit; + std::string Advice; +}; + +/// With \p MaxNodes, a module that would have more nodes than that (as +/// obligationModuleNodeCount counts them) is an ObligationSizeError, before +/// its goals are built. So is a program one of whose constructions passed +/// its limit (PassiveProgram::TooLarge). llvm::Expected -buildObligationModule(const PassiveProgram &Program); +buildObligationModule(const PassiveProgram &Program, uint64_t MaxNodes = 0); ObligationKind obligationKind(ProofObligationKind Kind); From 192cf752bb1a8f0d688033e2b895770844de9da6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:49 +0530 Subject: [PATCH 07/52] verify: Refuse obligations over the node limit before building their goals. --- clang/lib/Verify/Backend/Obligation.cpp | 63 +++++++++++++++++++++++-- 1 file changed, 59 insertions(+), 4 deletions(-) diff --git a/clang/lib/Verify/Backend/Obligation.cpp b/clang/lib/Verify/Backend/Obligation.cpp index 6bebcbc018..ac40f84d34 100644 --- a/clang/lib/Verify/Backend/Obligation.cpp +++ b/clang/lib/Verify/Backend/Obligation.cpp @@ -1,11 +1,13 @@ //===--- Obligation.cpp ---------------------------------------------------===// #include "LogicTerms.h" #include "ObligationLowering.h" +#include "ObligationSimplify.h" #include "SpecAxioms.h" #include "llvm/ADT/APInt.h" #include "llvm/ADT/SmallString.h" #include "llvm/ADT/StringRef.h" #include "llvm/Support/Error.h" +#include "llvm/Support/MathExtras.h" #include #include @@ -2159,7 +2161,8 @@ class ObligationBuilder { return std::move(Result); } - llvm::Expected buildPassive(const PassiveProgram &P) { + llvm::Expected buildPassive(const PassiveProgram &P, + uint64_t MaxNodes) { ObligationModule M; M.FunctionName = P.FunctionName; M.FunctionIdentity = P.FunctionIdentity; @@ -2272,6 +2275,37 @@ class ObligationBuilder { return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ConstructionError.c_str()); + // The goals' size is known before any is built: each is its condition + // under a negated copy of every assumption before it (a Not and an Or + // each), each query is its goal negated, and the complete goal joins the + // goals by And, with its query. + uint64_t Prefix = 0, Goals = 0, GoalCount = 0; + auto assumed = [&](const VCExpr *Assumption) { + Prefix = + llvm::SaturatingAdd(Prefix, logicNodeCount(Assumption), uint64_t(2)); + }; + auto goal = [&](const VCExpr *Condition) { + Goals = llvm::SaturatingAdd(Goals, Prefix, logicNodeCount(Condition)); + ++GoalCount; + }; + for (const auto &Entry : EntryAssumes) + assumed(Entry.get()); + for (const LoweredStmt &Stmt : Stmts) { + if (Stmt.Kind == PassiveStmt::Assume) + assumed(Stmt.Cond.get()); + else + goal(Stmt.Cond.get()); + } + for (const auto &Exit : ExitAsserts) + goal(std::get<1>(Exit).get()); + const uint64_t GoalNodes = + GoalCount == 0 + ? 3 + : llvm::SaturatingAdd(llvm::SaturatingMultiply(Goals, uint64_t(4)), + 3 * GoalCount - 1); + if (MaxNodes != 0 && GoalNodes > MaxNodes) + return ObligationSizeError::obligations(GoalNodes, MaxNodes); + std::vector Assumptions; for (const auto &Entry : EntryAssumes) Assumptions.push_back(Entry.get()); @@ -2324,10 +2358,13 @@ class ObligationBuilder { M.CorrectnessGoal = buildCompleteGoal(M.Obligations); M.CounterexampleQuery = vcNot(cloneVCExpr(M.CorrectnessGoal.get())); + assert(GoalNodes == obligationModuleNodeCount(M) && + "the goals' size was not predicted exactly"); SpecAxiomContext AxiomContext{P.SpecFunctions, P.SpecFuel, P.HiddenSpecs, P.RevealedSpecs}; - if (llvm::Error Error = materializeLogicFunctions(M, AxiomContext)) + if (llvm::Error Error = + materializeLogicFunctions(M, AxiomContext, MaxNodes, GoalNodes)) return std::move(Error); auto RequiredFeatures = validateObligationModule(M); @@ -2588,14 +2625,32 @@ verify::validateObligationModule(const ObligationModule &M) { return RequiredFeatures; } +char ObligationSizeError::ID = 0; + +llvm::Error ObligationSizeError::obligations(uint64_t Nodes, uint64_t Limit) { + return llvm::make_error( + "the proof obligations", Nodes, Limit, + "each check repeats every assumption before it, so split the function " + "or raise the limit"); +} + +void ObligationSizeError::log(llvm::raw_ostream &OS) const { + OS << What << " would take at least " << Nodes + << " expression nodes, more than the limit of " << Limit + << " (--max-query-nodes): " << Advice; +} + llvm::Expected -verify::buildObligationModule(const PassiveProgram &P) { +verify::buildObligationModule(const PassiveProgram &P, uint64_t MaxNodes) { ObligationBuilder B(P.ResultVarName, P.OldHeapName.empty() ? std::string(VHeapName) + "_0" : P.OldHeapName, P.CallerIntMode, P.HeapVariables, /*ForceCallerMode=*/false, &P.SpecFunctions); - auto Module = B.buildPassive(P); + if (const auto &Over = P.TooLarge) + return llvm::make_error(Over->What, Over->Nodes, + Over->Limit, Over->Advice); + auto Module = B.buildPassive(P, MaxNodes); if (Module) { Module->AssumedPosts = P.AssumedPosts; Module->AssumedUnfoldings = P.AssumedUnfoldings; From ea09fe3b0f78d13a315f1528e92adb816c97c859 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:50 +0530 Subject: [PATCH 08/52] verify: Give materializing spec definitions the module's node limit. --- clang/lib/Verify/Backend/SpecAxioms.h | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/clang/lib/Verify/Backend/SpecAxioms.h b/clang/lib/Verify/Backend/SpecAxioms.h index 23614adbbb..8b7dc1bf94 100644 --- a/clang/lib/Verify/Backend/SpecAxioms.h +++ b/clang/lib/Verify/Backend/SpecAxioms.h @@ -36,8 +36,15 @@ std::unique_ptr unfoldSpecBodyForAxiom(const VFunction &Spec, /// Materialize all logical function declarations and finite definition levels /// reachable from Module into its owned backend-neutral representation. +/// With \p MaxNodes, the definitions may bring the module from \p Nodes to +/// at most that many nodes (as obligationModuleNodeCount counts them): each +/// is counted as it is lowered, and one past the limit is an +/// ObligationSizeError, or left out when only a counterexample check needs +/// it. llvm::Error materializeLogicFunctions(ObligationModule &Module, - const SpecAxiomContext &Ctx); + const SpecAxiomContext &Ctx, + uint64_t MaxNodes = 0, + uint64_t Nodes = 0); } // namespace verify } // namespace clang From 78880d768db3f08fbfdcd9cf5f65860efeeeea28 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:51 +0530 Subject: [PATCH 09/52] verify: Count spec definitions against the module's node limit as they are built. --- clang/lib/Verify/Backend/SpecAxioms.cpp | 38 +++++++++++++++++++++++-- 1 file changed, 36 insertions(+), 2 deletions(-) diff --git a/clang/lib/Verify/Backend/SpecAxioms.cpp b/clang/lib/Verify/Backend/SpecAxioms.cpp index e95be6beaf..188dd79b83 100644 --- a/clang/lib/Verify/Backend/SpecAxioms.cpp +++ b/clang/lib/Verify/Backend/SpecAxioms.cpp @@ -1,8 +1,10 @@ //===--- SpecAxioms.cpp - Verus-style spec defining axioms ----------------===// #include "SpecAxioms.h" #include "../Transform/SpecInline.h" +#include "LogicTerms.h" #include "ObligationLowering.h" #include "llvm/Support/Error.h" +#include "llvm/Support/MathExtras.h" using namespace clang; using namespace verify; @@ -114,7 +116,9 @@ static const VFunction *findSpecFunction(const FunctionMap &Functions, } llvm::Error verify::materializeLogicFunctions(ObligationModule &Module, - const SpecAxiomContext &Ctx) { + const SpecAxiomContext &Ctx, + uint64_t MaxNodes, + uint64_t Nodes) { // The functions the query reaches; then, for a counterexample check only, // those their unfoldings and postconditions apply, where a failure leaves // the function out instead of failing the module. @@ -153,6 +157,20 @@ llvm::Error verify::materializeLogicFunctions(ObligationModule &Module, Module.LogicFunctions.try_emplace(Identity, std::move(Declaration)); (void)Inserted; LogicFunctionDecl &Owned = It->second; + // Its definitions join the module's nodes once all are lowered. + uint64_t Own = 0; + auto count = [&](const LogicExpr *Definition) -> llvm::Error { + Own = llvm::SaturatingAdd(Own, logicNodeCount(Definition)); + const uint64_t Total = llvm::SaturatingAdd(Nodes, Own); + if (MaxNodes != 0 && Total > MaxNodes) + return llvm::make_error( + "the proof obligations with the definitions of the specs they " + "apply", + Total, MaxNodes, + "lower the fuel cppverify::reveal_with_fuel gives, split the " + "function, or raise the limit"); + return llvm::Error::success(); + }; const std::string DefinitionHeap = Spec->ReadsHeap ? std::string(VSpecHeapName) : std::string(VHeapName) + "_0"; @@ -223,13 +241,26 @@ llvm::Error verify::materializeLogicFunctions(ObligationModule &Module, return llvm::createStringError( llvm::inconvertibleErrorCode(), "spec step definition result sort mismatch: %s", Spec->Name.c_str()); + if (llvm::Error Error = count(Owned.StepDefinition.get())) + return Error; collectReferencedLogicFunctions(Owned.StepDefinition.get(), Pending); const unsigned MaxDepth = Spec->NeedsDecreasesCheck ? Fuel : std::min(Fuel, 1U); Owned.DefinitionFuel = MaxDepth; for (unsigned Depth = 1; Depth <= MaxDepth; ++Depth) { - std::unique_ptr Body = unfoldSpecDefinition(*Spec, Ctx, Depth); + std::unique_ptr Body; + { + NodeBudget Unfolding; + Body = unfoldSpecDefinition(*Spec, Ctx, Depth); + if (Unfolding.exceeded()) + return llvm::make_error( + "the definition of " + Spec->Name + " unfolded " + + std::to_string(Depth) + " levels deep", + Unfolding.built(), Unfolding.limit(), + "lower its fuel (cppverify::reveal_with_fuel), or raise the " + "limit"); + } if (!Body) continue; auto Lowered = lowerLogicExpr(Body.get(), "", DefinitionHeap, @@ -245,6 +276,8 @@ llvm::Error verify::materializeLogicFunctions(ObligationModule &Module, return llvm::createStringError( llvm::inconvertibleErrorCode(), "spec definition result sort mismatch: %s", Spec->Name.c_str()); + if (llvm::Error Error = count(Definition.get())) + return Error; collectReferencedLogicFunctions(Definition.get(), Pending); Owned.DefinitionLevels.push_back(std::move(Definition)); } @@ -262,6 +295,7 @@ llvm::Error verify::materializeLogicFunctions(ObligationModule &Module, Owned.Decreases.push_back(std::move(*Lowered)); } } + Nodes = llvm::SaturatingAdd(Nodes, Own); return llvm::Error::success(); }; std::set Pending; From 3fa760731833d093136b4b8b038b899f266caa75 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:51 +0530 Subject: [PATCH 10/52] verify: Record on a passive program that a construction passed the node limit. --- clang/lib/Verify/Transform/Passivize.h | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/clang/lib/Verify/Transform/Passivize.h b/clang/lib/Verify/Transform/Passivize.h index b4dcea5c87..10c59f71e8 100644 --- a/clang/lib/Verify/Transform/Passivize.h +++ b/clang/lib/Verify/Transform/Passivize.h @@ -73,11 +73,27 @@ struct PassiveModelVariable { SourceLocation EndLoc; }; +/// What a construction for a program built past its function's limit +/// (NodeBudget), where it stopped: the program is incomplete, and building +/// its module is an ObligationSizeError with this instead. +struct PassiveOversize { + std::string What; + uint64_t Nodes = 0; + uint64_t Limit = 0; + std::string Advice; +}; + +/// The facts about the specs a program applies, each spec's postconditions +/// and definitions at its applications, passed \p Budget. +PassiveOversize specFactsOversize(const NodeBudget &Budget); + struct PassiveProgram { std::string FunctionName; std::string FunctionIdentity; std::vector> Stmts; std::vector> EntryAssumes; + /// Set when a construction for the program passed the node limit. + std::optional TooLarge; /// How many leading EntryAssumes are the function's own preconditions. size_t PreconditionCount = 0; /// Each behavior's assumption in the entry state. From 06a9dd612875499b677b11169e62fa6c728e85ce Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:52 +0530 Subject: [PATCH 11/52] verify: Bound the spec facts a function's passivization adds by the node budget. --- clang/lib/Verify/Transform/Passivize.cpp | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp index fcfabb5a96..d983a7b038 100644 --- a/clang/lib/Verify/Transform/Passivize.cpp +++ b/clang/lib/Verify/Transform/Passivize.cpp @@ -3073,6 +3073,15 @@ static void addFrameInstances(PassiveProgram &P, const FunctionMap &FnMap) { P.Stmts = std::move(Stmts); } +PassiveOversize verify::specFactsOversize(const NodeBudget &Budget) { + return {"the facts about the specs it applies (at each application, their " + "definitions unfolded as deep as their fuel, and their " + "postconditions)", + Budget.built(), Budget.limit(), + "lower the fuel cppverify::reveal_with_fuel gives, or raise the " + "limit"}; +} + /// A spec's proved postcondition, and an inductive predicate's unfolding, /// hold at every application of it. An inductive predicate is unfolded /// \p Depth levels deep, or as deep as reveal_with_fuel asks when \p WithFuel: @@ -4602,8 +4611,11 @@ class PassivizerImpl { for (const auto &Decrease : Fn.Decreases) EntryMeasure.push_back(cloneExpr(Decrease.get(), MeasureCtx)); } + NodeBudget Facts; addSpecPostInstances(P, FnMap, Fn, UnfoldingDepth, UnfoldingFuel, EntryMeasure); + if (Facts.exceeded()) + P.TooLarge = specFactsOversize(Facts); return P; } From f4bb7d013bf9dd313c9f5e75fa278f6809af7eb8 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:53 +0530 Subject: [PATCH 12/52] verify: Stop unfolding specs once the node budget is spent. --- clang/lib/Verify/Transform/SpecInline.cpp | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/clang/lib/Verify/Transform/SpecInline.cpp b/clang/lib/Verify/Transform/SpecInline.cpp index 9873c6f760..8c7c4b33f1 100644 --- a/clang/lib/Verify/Transform/SpecInline.cpp +++ b/clang/lib/Verify/Transform/SpecInline.cpp @@ -193,6 +193,10 @@ class SpecInlinerImpl { } std::unique_ptr inlineSpecCall(const VSpecCallExpr &C) { + // Past the function's node limit nothing more is unfolded; the + // construction that unfolds reports it. + if (NodeBudget::exhausted()) + return opaqueCall(C); if (InlineDepth++ >= MaxInlineDepth) return opaqueCall(C); struct DepthGuard { @@ -2804,7 +2808,12 @@ static void addSpecPostChecks(PassiveProgram &P, const VFunction &Fn, PS->Cond = cloneAtEntryState(Obligation.get()); P.Stmts.push_back(std::move(PS)); } - addPostApplicationFacts(P, Fn, FnMap); + { + NodeBudget Facts; + addPostApplicationFacts(P, Fn, FnMap); + if (Facts.exceeded()) + P.TooLarge = specFactsOversize(Facts); + } if (Collector.Unsupported) { auto PS = std::make_unique(); PS->K = PassiveStmt::Assert; @@ -3032,6 +3041,8 @@ verify::withClauseProofs(PassiveProgram Check, const VFunction &Spec, Passivizer Lowering; Lowering.setFunctionMap(FnMap); PassiveProgram P = Lowering.run(Proof); + if (!P.TooLarge) + P.TooLarge = std::move(Check.TooLarge); P.AssumedPosts.insert(Check.AssumedPosts.begin(), Check.AssumedPosts.end()); P.AssumedUnfoldings.insert(Check.AssumedUnfoldings.begin(), Check.AssumedUnfoldings.end()); From 6ac08884bcc2c9e3780dc4ae9bd6b17c11a63beb Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:53 +0530 Subject: [PATCH 13/52] verify: Add the solver.memory-limit reason and the solvers' memory limit. --- clang/lib/Verify/Backend/VerifyBackend.h | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/clang/lib/Verify/Backend/VerifyBackend.h b/clang/lib/Verify/Backend/VerifyBackend.h index 00e7678705..ffa2f59c0d 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.h +++ b/clang/lib/Verify/Backend/VerifyBackend.h @@ -36,6 +36,8 @@ enum class VerifyReason { Counterexample, SolverTimeout, SolverResourceLimit, + /// The solver ran out of the memory --memory-limit gives it. + SolverMemoryLimit, SolverUnknown, SolverUnavailable, SolverInvocationFailure, @@ -77,6 +79,12 @@ enum class VerifyReason { llvm::StringRef verifyReasonCode(VerifyReason Reason); +/// Limits what Z3 allocates in this process to \p MegaBytes, its queries +/// together; 0 removes the limit. A check runs until its watchdog, polling +/// every 10 ms, finds the limit passed, and its query then ends Unresolved +/// with SolverMemoryLimit. Call it before any query runs. +void setZ3MemoryLimit(uint64_t MegaBytes); + /// Stops verification for the rest of the process (Ctrl-C): queries running /// end unresolved and none starts. Safe to call from a signal handler. void requestInterrupt(); @@ -238,6 +246,13 @@ llvm::StringRef machineIntegerEncodingName(MachineIntegerEncoding Encoding); std::optional parseMachineIntegerEncoding(llvm::StringRef Name); +/// Unresolved with QuerySizeLimit when \p Module has more than \p MaxNodes +/// expression nodes, as a module from an archive or one a backend derives +/// may; a source module is refused before it is built. +std::optional moduleSizeLimit(const ObligationModule &Module, + uint64_t MaxNodes, + llvm::StringRef BackendName); + struct BackendExecutionOptions { unsigned SolverTimeoutMs = 0; /// Per-query timeout for modules over sequences, sets, multisets, or @@ -256,6 +271,9 @@ struct BackendExecutionOptions { llvm::StdThreadPool *Pool = nullptr; /// Maximum canonical expression nodes in a module; 0 disables it. uint64_t MaxQueryNodes = 0; + /// The megabytes each cvc5 process may allocate; 0 disables the limit. + /// Z3's limit is process-wide: setZ3MemoryLimit. + uint64_t MemoryLimitMB = 0; MachineIntegerEncoding IntegerEncoding = MachineIntegerEncoding::Auto; /// Do not retry a whole-module query after individual obligations are /// unresolved. Interactive fallback backends can consume those unresolved From a9e8613288645c00fd30ad5d4d808dee20c21026 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:54 +0530 Subject: [PATCH 14/52] verify: Name solver.memory-limit and share the module size check. --- clang/lib/Verify/Backend/VerifyBackend.cpp | 46 +++++++++++----------- 1 file changed, 24 insertions(+), 22 deletions(-) diff --git a/clang/lib/Verify/Backend/VerifyBackend.cpp b/clang/lib/Verify/Backend/VerifyBackend.cpp index afd6b07247..35f9350638 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.cpp +++ b/clang/lib/Verify/Backend/VerifyBackend.cpp @@ -230,17 +230,8 @@ class PortfolioVerifyBackend : public VerifyBackend { CVC5->setDeadline(D); } VerifyResult verifyModule(const ObligationModule &Module) override { - if (MaxQueryNodes != 0 && - obligationModuleNodeCount(Module) > MaxQueryNodes) { - VerifyResult Result; - Result.Status = VerifyStatus::Unresolved; - Result.Reason = VerifyReason::QuerySizeLimit; - Result.Message = - "canonical obligation module exceeds query node budget " + - std::to_string(MaxQueryNodes); - Result.BackendName = "portfolio"; - return Result; - } + if (auto Limited = moduleSizeLimit(Module, MaxQueryNodes, "portfolio")) + return std::move(*Limited); std::vector Z3Results; std::vector CVC5Results; @@ -392,6 +383,24 @@ verify::parseMachineIntegerEncoding(llvm::StringRef Name) { return std::nullopt; } +std::optional +verify::moduleSizeLimit(const ObligationModule &Module, uint64_t MaxNodes, + llvm::StringRef BackendName) { + if (MaxNodes == 0) + return std::nullopt; + const uint64_t Nodes = obligationModuleNodeCount(Module); + if (Nodes <= MaxNodes) + return std::nullopt; + VerifyResult Result; + Result.Status = VerifyStatus::Unresolved; + Result.Reason = VerifyReason::QuerySizeLimit; + Result.Message = "the obligation module has " + std::to_string(Nodes) + + " expression nodes, more than the limit of " + + std::to_string(MaxNodes) + " (--max-query-nodes)"; + Result.BackendName = BackendName.str(); + return Result; +} + llvm::StringRef verify::verifyReasonCode(VerifyReason Reason) { switch (Reason) { case VerifyReason::None: @@ -402,6 +411,8 @@ llvm::StringRef verify::verifyReasonCode(VerifyReason Reason) { return "solver.timeout"; case VerifyReason::SolverResourceLimit: return "solver.resource-limit"; + case VerifyReason::SolverMemoryLimit: + return "solver.memory-limit"; case VerifyReason::SolverUnknown: return "solver.unknown"; case VerifyReason::SolverUnavailable: @@ -681,17 +692,8 @@ class RaceVerifyBackend : public VerifyBackend { CVC5->setDeadline(D); } VerifyResult verifyModule(const ObligationModule &Module) override { - if (MaxQueryNodes != 0 && - obligationModuleNodeCount(Module) > MaxQueryNodes) { - VerifyResult Result; - Result.Status = VerifyStatus::Unresolved; - Result.Reason = VerifyReason::QuerySizeLimit; - Result.Message = - "canonical obligation module exceeds query node budget " + - std::to_string(MaxQueryNodes); - Result.BackendName = "race"; - return Result; - } + if (auto Limited = moduleSizeLimit(Module, MaxQueryNodes, "race")) + return std::move(*Limited); resume(); VerifyResult Z3Result; VerifyResult CVC5Result; From 76ead33f00bcde770983cc14e86175b6ccfe1189 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:54 +0530 Subject: [PATCH 15/52] verify: Track whether a Z3 encoder stopped for memory. --- clang/lib/Verify/Backend/Z3Encode.h | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/clang/lib/Verify/Backend/Z3Encode.h b/clang/lib/Verify/Backend/Z3Encode.h index ff1473e81f..7cf3cd9bc5 100644 --- a/clang/lib/Verify/Backend/Z3Encode.h +++ b/clang/lib/Verify/Backend/Z3Encode.h @@ -56,9 +56,14 @@ class Z3Encoder { /// The first error a Z3 call reported outside a check, which a check /// reports itself as unknown. Z3 returns a null term and goes on. std::string APIError; + /// Z3 ran out of memory here, in a check or another call: its allocations, + /// every context's together, reached setZ3MemoryLimit. Later checks return + /// unknown at once. + bool OutOfMemory = false; bool Checking = false; static void recordAPIError(Z3_context Context, Z3_error_code Code); - /// \p Result, unless a Z3 call failed in this unstopped encoder. + /// \p Result, unless a Z3 call failed or ran out of memory in this + /// unstopped encoder. VerifyResult withAPIError(VerifyResult Result); VerifyResult decideModule(const ObligationModule &Module, const LogicExpr *Query, From a918febf940876f7dbe0a884f38ec50b621ef48d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:55 +0530 Subject: [PATCH 16/52] verify: Stop a Z3 check past the memory limit and report it. --- clang/lib/Verify/Backend/Z3Encode.cpp | 90 +++++++++++++++++++++------ 1 file changed, 71 insertions(+), 19 deletions(-) diff --git a/clang/lib/Verify/Backend/Z3Encode.cpp b/clang/lib/Verify/Backend/Z3Encode.cpp index 305b45949c..27e62848dd 100644 --- a/clang/lib/Verify/Backend/Z3Encode.cpp +++ b/clang/lib/Verify/Backend/Z3Encode.cpp @@ -41,15 +41,7 @@ constexpr unsigned Z3ProofCacheAdapterVersion = 2; std::optional querySizeLimitResult(const ObligationModule &Module, uint64_t MaxQueryNodes) { - if (MaxQueryNodes == 0 || obligationModuleNodeCount(Module) <= MaxQueryNodes) - return std::nullopt; - VerifyResult Result; - Result.Status = VerifyStatus::Unresolved; - Result.Reason = VerifyReason::QuerySizeLimit; - Result.Message = "canonical obligation module exceeds query node budget " + - std::to_string(MaxQueryNodes); - Result.BackendName = "z3"; - return Result; + return moduleSizeLimit(Module, MaxQueryNodes, "z3"); } std::optional sourceModelValue(const z3::expr &Value, @@ -139,6 +131,44 @@ z3::params solverParams(z3::context &Ctx) { } // namespace +namespace { +/// The limit setZ3MemoryLimit gave Z3, for messages. +std::atomic Z3MemoryLimitMB{0}; + +std::string z3MemoryMessage() { + const uint64_t Limit = Z3MemoryLimitMB.load(); + if (Limit == 0) + return "Z3 ran out of memory"; + return "Z3 reached the memory limit: its queries share " + + std::to_string(Limit) + " MB (--memory-limit)"; +} +} // namespace + +// Each check's watchdog enforces the limit, so a check it stops is known to +// have stopped for memory. Z3's own limits do not say so: its hard one, +// memory_max_size, fails whichever allocation passes it in any context of +// the process, Z3_mk_context's included, which then returns no context; its +// high watermark stops the search where it is checked, often reporting only +// canceled, and frees what the check took before it returns. +void verify::setZ3MemoryLimit(uint64_t MegaBytes) { + Z3MemoryLimitMB = MegaBytes; +} + +/// Z3's allocations, every query's together, are over the limit. +static bool overMemoryLimit() { + const uint64_t Limit = Z3MemoryLimitMB.load(); + return Limit != 0 && Z3_get_estimated_alloc_size() > (Limit << 20); +} + +/// Z3 says a check that returned unknown ran out of memory, as when an +/// allocation fails. +static bool memoryReason(const z3::solver &S) { + const std::string Reason = S.reason_unknown(); + return llvm::StringRef(Reason).contains("memout") || + llvm::StringRef(Reason).contains("max. memory") || + llvm::StringRef(Reason).contains("out of memory"); +} + namespace { /// The encoder of each live Z3 context, for its error handler. std::mutex APIErrorLock; @@ -166,14 +196,19 @@ void Z3Encoder::recordAPIError(Z3_context Context, Z3_error_code Code) { if (auto It = APIErrorEncoders.find(Context); It != APIErrorEncoders.end()) Encoder = It->second; } - if (!Encoder || Encoder->Checking || !Encoder->APIError.empty()) + if (!Encoder) + return; + // A check reports other errors as unknown, but not why. + if (Code == Z3_MEMOUT_FAIL) + Encoder->OutOfMemory = true; + if (Encoder->Checking || !Encoder->APIError.empty()) return; Encoder->APIError = Z3_get_error_msg(Context, Code); Encoder->markEncodingFailure("Z3 reported an error: " + Encoder->APIError); } VerifyResult Z3Encoder::withAPIError(VerifyResult Result) { - if (APIError.empty()) + if (APIError.empty() && !OutOfMemory) return Result; { std::lock_guard Guard(CheckLock); @@ -182,6 +217,11 @@ VerifyResult Z3Encoder::withAPIError(VerifyResult Result) { } VerifyResult Failed; Failed.Status = VerifyStatus::Unresolved; + if (OutOfMemory) { + Failed.Reason = VerifyReason::SolverMemoryLimit; + Failed.Message = z3MemoryMessage(); + return Failed; + } Failed.Reason = VerifyReason::EncodingFailure; Failed.Message = "Z3 reported an error: " + APIError; return Failed; @@ -1794,20 +1834,26 @@ z3::check_result Z3Encoder::check(z3::solver &S, unsigned Ms) { using Clock = std::chrono::steady_clock; { std::lock_guard Guard(CheckLock); - if (Stopped || interruptRequested()) + if (Stopped || OutOfMemory || interruptRequested()) return z3::unknown; CheckFinished = false; } Checking = true; // Z3 forgets a cancellation that arrives inside one of its nested resource // scopes (leaving the scope clears it), whether from its own timeout or - // from interrupt(). A check past its time, stopped, or interrupted by - // Ctrl-C, which the watchdog polls for, is therefore interrupted again - // until it returns. + // from interrupt(). A check past its time, stopped, interrupted by Ctrl-C, + // or past the memory limit, which the watchdog polls for, is therefore + // interrupted again until it returns. constexpr std::chrono::milliseconds Grace(100); constexpr std::chrono::milliseconds Interval(50); + // How often the memory limit is polled: what a check allocates in this + // time is how far it can pass the limit. + constexpr std::chrono::milliseconds MemoryInterval(10); + const auto Poll = Z3MemoryLimitMB.load() != 0 ? MemoryInterval : Interval; bool TimedOut = false; bool Interrupted = false; + bool OverLimit = false; + z3::check_result Result = z3::unknown; std::thread Watchdog([&] { std::unique_lock Lock(CheckLock); const auto Limit = @@ -1815,13 +1861,15 @@ z3::check_result Z3Encoder::check(z3::solver &S, unsigned Ms) { : Clock::now() + std::chrono::milliseconds(Ms) + Grace; auto Next = Limit; while (!CheckFinished) { - if (Stopped || interruptRequested() || Clock::now() >= Next) { + OverLimit = OverLimit || overMemoryLimit(); + if (Stopped || OverLimit || interruptRequested() || + Clock::now() >= Next) { TimedOut = TimedOut || Clock::now() >= Limit; Ctx.interrupt(); Interrupted = true; Next = Clock::now() + Interval; } - CheckChanged.wait_until(Lock, std::min(Next, Clock::now() + Interval)); + CheckChanged.wait_until(Lock, std::min(Next, Clock::now() + Poll)); } }); auto Join = llvm::make_scope_exit([&] { @@ -1839,8 +1887,11 @@ z3::check_result Z3Encoder::check(z3::solver &S, unsigned Ms) { (void)Reset.check(); } Checking = false; + if (Result == z3::unknown && (OverLimit || memoryReason(S))) + OutOfMemory = true; }); - return S.check(); + Result = S.check(); + return Result; } std::optional @@ -3804,7 +3855,8 @@ VerifyResult Z3VerifyBackend::verifyModule(const ObligationModule &Module) { Result.Status == VerifyStatus::Unresolved && (Result.Reason == VerifyReason::SolverTimeout || Result.Reason == VerifyReason::SolverUnknown || - Result.Reason == VerifyReason::SolverResourceLimit)) { + Result.Reason == VerifyReason::SolverResourceLimit || + Result.Reason == VerifyReason::SolverMemoryLimit)) { IntegerEncoding = MachineIntegerEncoding::Auto; VerifyResult Retry = verifyModuleDirect(Module); IntegerEncoding = MachineIntegerEncoding::BitVector; From 0c97cff712a3a5e958004730d0b6822efc62b5dc Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:56 +0530 Subject: [PATCH 17/52] verify: Keep the memory limit in the cvc5 backend. --- clang/lib/Verify/Backend/CVC5Backend.h | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/lib/Verify/Backend/CVC5Backend.h b/clang/lib/Verify/Backend/CVC5Backend.h index 875d38fa26..3f7badb7a6 100644 --- a/clang/lib/Verify/Backend/CVC5Backend.h +++ b/clang/lib/Verify/Backend/CVC5Backend.h @@ -30,6 +30,7 @@ class CVC5VerifyBackend : public VerifyBackend { /// Set by cancel(): the running process is stopped and no other starts. std::atomic Cancelled{false}; unsigned ResourceLimit; + uint64_t MemoryLimitMB; unsigned Jobs; llvm::StdThreadPool *Pool; std::optional Deadline; From 4f7a0c8b267564c117e5bf8f4630801ab60c2fb2 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:56 +0530 Subject: [PATCH 18/52] verify: Limit each cvc5 process's memory and report when it runs out. --- clang/lib/Verify/Backend/CVC5Backend.cpp | 67 ++++++++++++++++++------ 1 file changed, 50 insertions(+), 17 deletions(-) diff --git a/clang/lib/Verify/Backend/CVC5Backend.cpp b/clang/lib/Verify/Backend/CVC5Backend.cpp index 3a53d58e3f..a4bca829d6 100644 --- a/clang/lib/Verify/Backend/CVC5Backend.cpp +++ b/clang/lib/Verify/Backend/CVC5Backend.cpp @@ -30,6 +30,7 @@ #else #include #include +#include #include #endif @@ -1505,15 +1506,9 @@ class SMTLibEncoder { static VerifyResult querySizeLimitResult(const ObligationModule &Module, uint64_t MaxQueryNodes, llvm::StringRef BackendName) { - VerifyResult Result; - if (MaxQueryNodes == 0 || obligationModuleNodeCount(Module) <= MaxQueryNodes) - return Result; - Result.Status = VerifyStatus::Unresolved; - Result.Reason = VerifyReason::QuerySizeLimit; - Result.Message = "canonical obligation module exceeds query node budget " + - std::to_string(MaxQueryNodes); - Result.BackendName = BackendName.str(); - return Result; + if (auto Limited = moduleSizeLimit(Module, MaxQueryNodes, BackendName)) + return std::move(*Limited); + return VerifyResult(); } static std::optional @@ -2404,7 +2399,8 @@ CVC5VerifyBackend::CVC5VerifyBackend(const BackendExecutionOptions &Execution) : TimeoutMs(Execution.SolverTimeoutMs), CollectionTimeoutMs(Execution.CollectionTimeoutMs), CertifyTimeoutMs(Execution.CertifyTimeoutMs), - ResourceLimit(Execution.SolverResourceLimit), Jobs(Execution.Jobs), + ResourceLimit(Execution.SolverResourceLimit), + MemoryLimitMB(Execution.MemoryLimitMB), Jobs(Execution.Jobs), Pool(Execution.Pool), MaxQueryNodes(Execution.MaxQueryNodes), IntegerEncoding(Execution.IntegerEncoding) { llvm::StringRef Requested = Execution.CVC5Path.empty() @@ -2431,6 +2427,7 @@ struct SolverRun { static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script, unsigned TimeoutMs, unsigned ResourceLimit, + uint64_t MemoryLimitMB = 0, const std::atomic *Cancelled = nullptr); /// Whether the cvc5 at \p SolverPath prints a sequence value last element @@ -2473,6 +2470,7 @@ static bool printsSequencesReversed(const std::string &SolverPath) { static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script, unsigned TimeoutMs, unsigned ResourceLimit, + uint64_t MemoryLimitMB, const std::atomic *Cancelled) { SolverRun Run; VerifyResult &Result = Run.Failure; @@ -2530,9 +2528,27 @@ static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script, ErrorPath.str()}; std::string InvocationError; bool ExecutionFailed = false; + // On Windows the limit bounds the process's committed memory. On POSIX + // hosts a limit makes ExecuteNoWait fork rather than spawn, and fork runs + // Z3's fork handlers, which wait for the timers of every check running in + // the process; the limit is set on the spawned process instead. +#if defined(_WIN32) + const unsigned SpawnLimit = static_cast( + std::min(MemoryLimitMB, std::numeric_limits::max())); +#else + const unsigned SpawnLimit = 0; +#endif llvm::sys::ProcessInfo Process = - llvm::sys::ExecuteNoWait(SolverPath, Args, std::nullopt, Redirects, 0, - &InvocationError, &ExecutionFailed); + llvm::sys::ExecuteNoWait(SolverPath, Args, std::nullopt, Redirects, + SpawnLimit, &InvocationError, &ExecutionFailed); +#if defined(__linux__) + // What cvc5 allocates: its data segment and private writable mappings. + if (MemoryLimitMB != 0 && Process.Pid != llvm::sys::ProcessInfo::InvalidPid) { + struct rlimit Data; + Data.rlim_cur = Data.rlim_max = static_cast(MemoryLimitMB) << 20; + (void)::prlimit(Process.Pid, RLIMIT_DATA, &Data, nullptr); + } +#endif if (ExecutionFailed || Process.Pid == llvm::sys::ProcessInfo::InvalidPid) { Result.Reason = VerifyReason::SolverInvocationFailure; Result.Message = InvocationError.empty() ? "cannot start cvc5 process" @@ -2615,6 +2631,25 @@ static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script, return Run; } if (ExitCode != 0) { + std::string OutputError; + std::optional StandardOutput = + readSolverOutput(OutputPath, OutputError, MaxSolverOutputBytes); + // An allocation past the limit fails, and cvc5 reports it as an error + // ((error "std::bad_alloc")) or aborts on it (std::bad_alloc, or its SAT + // solver's Minisat::OutOfMemoryException). + auto outOfMemory = [](llvm::StringRef Text) { + return Text.contains("bad_alloc") || Text.contains("OutOfMemory"); + }; + if (outOfMemory(*StandardError) || + (StandardOutput && outOfMemory(*StandardOutput))) { + Result.Reason = VerifyReason::SolverMemoryLimit; + Result.Message = "cvc5 ran out of memory"; + if (MemoryLimitMB != 0) + Result.Message += ": each cvc5 process may use " + + std::to_string(MemoryLimitMB) + + " MB (--memory-limit)"; + return Run; + } Result.Reason = VerifyReason::SolverInvocationFailure; Result.Message = "cvc5 exited with status " + std::to_string(ExitCode); if (!InvocationError.empty()) @@ -2622,9 +2657,7 @@ static SolverRun runCVC5(const std::string &SolverPath, llvm::StringRef Script, if (!StandardError->empty()) Result.Message += ": " + diagnosticText(*StandardError); // cvc5 reports a script it rejects on standard output. - std::string OutputError; - if (std::optional StandardOutput = - readSolverOutput(OutputPath, OutputError, MaxSolverOutputBytes)) + if (StandardOutput) for (llvm::StringRef Rest = *StandardOutput; !Rest.empty();) { auto [Line, Next] = Rest.split('\n'); if (Line.trim().starts_with("(error")) { @@ -2802,8 +2835,8 @@ CVC5VerifyBackend::verifyQuery(const ObligationModule &Module, } Budget = static_cast(Remaining); } - SolverRun Run = - runCVC5(SolverPath, *Script, Budget, ResourceLimit, &Cancelled); + SolverRun Run = runCVC5(SolverPath, *Script, Budget, ResourceLimit, + MemoryLimitMB, &Cancelled); auto giveUp = [&](llvm::StringRef Outcome) { RefinementDecision Exhausted = Refinement.exhausted(Outcome); Result.Reason = Exhausted.Reason; From 5f1aa13d230d54498022d19c08895fe4b5e5b27a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:57 +0530 Subject: [PATCH 19/52] verify: Default the node and memory limits. --- clang/lib/Verify/Driver/Verifier.h | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h index 7983a7055a..e321091a02 100644 --- a/clang/lib/Verify/Driver/Verifier.h +++ b/clang/lib/Verify/Driver/Verifier.h @@ -18,6 +18,13 @@ inline constexpr unsigned DefaultCollectionTimeoutMs = /// and their retries, so it legitimately takes several query timeouts. inline constexpr unsigned DefaultFunctionTimeoutMs = 10 * DefaultSolverTimeoutMs; +/// The expression nodes the proof obligations of one function may take, as +/// built: building a module takes up to about 450 bytes a node at once, and +/// the largest of the test suite (the ULEB128 case study's) has 22.6 +/// million. +inline constexpr uint64_t DefaultMaxQueryNodes = 32000000; +/// The megabytes Z3's queries may allocate together, and each cvc5 process. +inline constexpr uint64_t DefaultMemoryLimitMB = 8192; enum class DiagnosticFormat { Text, Json }; @@ -55,8 +62,12 @@ struct VerifyOptions { unsigned SolverResourceLimit = 0; /// Number of isolated solver jobs. 0 selects available physical cores. unsigned Jobs = 1; - /// Maximum canonical expression nodes per backend module; 0 disables it. - uint64_t MaxQueryNodes = 0; + /// Maximum canonical expression nodes per module, checked as it is built + /// and before a backend runs it; 0 disables it. + uint64_t MaxQueryNodes = DefaultMaxQueryNodes; + /// The megabytes Z3's queries may allocate together, and each cvc5 + /// process; 0 disables the limit. + uint64_t MemoryLimitMB = DefaultMemoryLimitMB; /// Solver representation of machine integers (Z3, cvc5, portfolio, BMC). MachineIntegerEncoding IntegerEncoding = MachineIntegerEncoding::Auto; /// Optional cvc5 executable for cvc5 and strict portfolio verification. From d5157d49f4a72792ab247b19959332ab6837f2c0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:48:57 +0530 Subject: [PATCH 20/52] verify: Report a function too large to build as unresolved with query.size-limit. --- clang/lib/Verify/Driver/Verifier.cpp | 111 ++++++++++++++++++++------- 1 file changed, 85 insertions(+), 26 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index a9161a3329..0d75db39dc 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -1077,6 +1077,20 @@ struct VerifyDiagnostic { bool Hidden = false; }; +/// The backend a lowering reports, as lower-only names it. +static std::string backendName(BackendKind Kind) { + return Kind == BackendKind::CVC5 ? "cvc5" + : Kind == BackendKind::Portfolio ? "portfolio" + : Kind == BackendKind::Race ? "race" + : "z3"; +} + +static std::string lowerFailure(BackendKind Kind) { + return Kind == BackendKind::Z3 || Kind == BackendKind::BMC + ? "Z3 lowering failed: " + : "backend lowering failed: "; +} + static std::string backendSuffix(const VerifyResult &Result) { std::string Suffix; if (!Result.BackendName.empty()) { @@ -1579,6 +1593,7 @@ class Verifier { void checkCalleeRecommendsOnFailure(const VFunction &Caller, const FunctionMap &FnMap, VerifyBackend &Backend) { + NodeBudget::Limit NodeLimit(Opts.MaxQueryNodes); std::vector Calls; collectSpecCallsInFunction(Caller, Calls); for (const VSpecCallExpr *C : Calls) { @@ -1606,7 +1621,7 @@ class Verifier { if (PP.ExitAsserts.empty()) continue; PP.CallerIntMode = Caller.IntMode; - auto Module = buildObligationModule(PP); + auto Module = buildObligationModule(PP, Opts.MaxQueryNodes); if (!Module) { Diags.push_back({VerifyDiagnostic::Unresolved, "recommends lowering failed for " + Caller.Name + @@ -1795,12 +1810,15 @@ class Verifier { LeanOut = LeanFile.get(); } + // Z3 runs in this process, so its limit covers all its queries. + setZ3MemoryLimit(Opts.MemoryLimitMB); BackendExecutionOptions Execution; Execution.SolverTimeoutMs = Opts.SolverTimeoutMs; Execution.CollectionTimeoutMs = Opts.CollectionTimeoutMs; Execution.CertifyTimeoutMs = Opts.CertifyTimeoutMs; Execution.SolverResourceLimit = Opts.SolverResourceLimit; Execution.MaxQueryNodes = Opts.MaxQueryNodes; + Execution.MemoryLimitMB = Opts.MemoryLimitMB; Execution.IntegerEncoding = Opts.IntegerEncoding; Execution.SkipWholeModuleRetry = !Opts.LeanFallbackProjectPath.empty(); Execution.CVC5Path = Opts.CVC5Path; @@ -1989,6 +2007,29 @@ class Verifier { R, &In, Label, Kind}); explainUnsettled(R, In, Checked); }; + // What the function's verification builds is bounded by the node + // limit. Past it the function is too large: a verdict, which the + // verdicts relying on its contract take into account. + NodeBudget::Limit NodeLimit(Opts.MaxQueryNodes); + auto tooLarge = [&](const VFunction &In, + const ObligationSizeError &Size) { + VerifyResult Limited; + Limited.Status = VerifyStatus::Unresolved; + Limited.Reason = VerifyReason::QuerySizeLimit; + Limited.BackendName = backendName(Opts.Backend); + Limited.Message = Size.message(); + AllOk = false; + AnyFailed = true; + if (!Opts.LowerOnly && !In.IsProof) + FailedCallers.insert(In.Identity); + std::string Message = + (Opts.LowerOnly ? lowerFailure(Opts.Backend) : std::string()) + + In.Name + backendSuffix(Limited) + " (" + Limited.Message + ")"; + Diags.push_back({Opts.LowerOnly ? VerifyDiagnostic::Error + : VerifyDiagnostic::Unresolved, + std::move(Message), In.DeclLoc, In.Name, + std::move(Limited)}); + }; llvm::raw_string_ostream DumpStream(Run.Dump); llvm::raw_ostream *DumpOS = this->DumpOS ? &DumpStream : nullptr; std::unique_ptr OwnBackend; @@ -2021,7 +2062,7 @@ class Verifier { Passivizer P; P.setFunctionMap(InterfaceMap); auto proves = [&](PassiveProgram Smoke) { - auto Lowered = buildObligationModule(Smoke); + auto Lowered = buildObligationModule(Smoke, Opts.MaxQueryNodes); if (!Lowered) { llvm::consumeError(Lowered.takeError()); return false; @@ -2035,8 +2076,10 @@ class Verifier { VerifyStatus::Verified; }; auto unreachable = [&](const PassiveProgram &Program, bool EntryOnly) { - auto Lowered = buildObligationModule(smokeProgram( - Program, EntryOnly ? 0 : Program.Stmts.size(), falseGoal())); + auto Lowered = buildObligationModule( + smokeProgram(Program, EntryOnly ? 0 : Program.Stmts.size(), + falseGoal()), + Opts.MaxQueryNodes); if (!Lowered) { llvm::consumeError(Lowered.takeError()); return false; @@ -2146,11 +2189,20 @@ class Verifier { SourceLocation(), Fn->Name}); if (!UBError) { SpecInliner Inliner(FnMap, PreparedFn->SpecFuel); + NodeBudget Inlining; if (isDeductiveBackend(Opts.Backend) || Opts.Backend == BackendKind::Lean) Inliner.prepareFunctionAxiomatic(*PreparedFn); else Inliner.prepareFunction(*PreparedFn); + if (Inlining.exceeded()) { + tooLarge(*Fn, ObligationSizeError( + "its specs inlined as deep as their fuel", + Inlining.built(), Inlining.limit(), + "lower the fuel cppverify::reveal_with_fuel " + "gives, or raise the limit")); + continue; + } } WorkFn = &*PreparedFn; if (!UBError && Opts.Backend == BackendKind::BMC && Opts.LowerOnly) { @@ -2182,7 +2234,8 @@ class Verifier { if (!Missing.empty()) { ReadsError = "calls " + Missing + ", which reads the heap without a reads clause"; - } else if (auto Lowered = buildObligationModule(ReadsPP)) { + } else if (auto Lowered = + buildObligationModule(ReadsPP, Opts.MaxQueryNodes)) { if (auto Simplified = simplifyObligationModule(std::move(*Lowered))) ReadsModule = std::move(*Simplified); else @@ -2280,7 +2333,8 @@ class Verifier { std::string PostError; if (auto Lowered = buildObligationModule( withClauseProofs(buildSpecPostChecks(*Fn, FnMap), *Fn, - {VFunction::ClauseProof::Post}, FnMap))) { + {VFunction::ClauseProof::Post}, FnMap), + Opts.MaxQueryNodes)) { if (auto Simplified = simplifyObligationModule(std::move(*Lowered))) PostModule = std::move(*Simplified); else @@ -2395,7 +2449,8 @@ class Verifier { std::string Error; if (auto Lowered = buildObligationModule( withClauseProofs(buildInductionChecks(*Fn, FnMap), *Fn, - {VFunction::ClauseProof::Post}, FnMap))) { + {VFunction::ClauseProof::Post}, FnMap), + Opts.MaxQueryNodes)) { if (auto Simplified = simplifyObligationModule(std::move(*Lowered))) Induction = std::move(*Simplified); else @@ -2495,7 +2550,8 @@ class Verifier { Kind>{VFunction::ClauseProof::Post, VFunction::ClauseProof::Decreases}, FnMap); - auto DecModuleOrErr = buildObligationModule(DecPP); + auto DecModuleOrErr = + buildObligationModule(DecPP, Opts.MaxQueryNodes); // A spec's postcondition is proved with its termination. const std::string &Shown = Step ? Fn->InductiveStepOf : Fn->Name; const bool Quiet = Fn->IsBuiltin || Step; @@ -2672,7 +2728,8 @@ class Verifier { Passivizer BoundPassivizer; BoundPassivizer.setFunctionMap(InterfaceMap); PassiveProgram BoundProgram = BoundPassivizer.run(*UnrolledFn); - auto BoundModuleOrErr = buildObligationModule(BoundProgram); + auto BoundModuleOrErr = + buildObligationModule(BoundProgram, Opts.MaxQueryNodes); if (!BoundModuleOrErr) { AllOk = false; AnyFailed = true; @@ -2749,14 +2806,23 @@ class Verifier { Module = std::move(*BMCModule); Simplification = BMCSimplification; } else { - auto ModuleOrErr = buildObligationModule(PP); + auto ModuleOrErr = buildObligationModule(PP, Opts.MaxQueryNodes); if (!ModuleOrErr) { AllOk = false; AnyFailed = true; - Diags.push_back({VerifyDiagnostic::Unresolved, - "obligation lowering failed: " + Fn->Name + " (" + - llvm::toString(ModuleOrErr.takeError()) + - ")"}); + bool Limited = false; + llvm::Error Error = llvm::handleErrors( + ModuleOrErr.takeError(), [&](const ObligationSizeError &Size) { + tooLarge(*Fn, Size); + Limited = true; + }); + if (Limited) + llvm::consumeError(std::move(Error)); + else + Diags.push_back({VerifyDiagnostic::Unresolved, + "obligation lowering failed: " + Fn->Name + + " (" + llvm::toString(std::move(Error)) + + ")"}); continue; } auto SimplifiedModule = simplifyObligationModule( @@ -2813,12 +2879,7 @@ class Verifier { if (Lowered.Status != VerifyStatus::Lowered) { AllOk = false; AnyFailed = true; - std::string Message = - std::string(Opts.Backend == BackendKind::Z3 || - Opts.Backend == BackendKind::BMC - ? "Z3" - : "backend") + - " lowering failed: " + Fn->Name; + std::string Message = lowerFailure(Opts.Backend) + Fn->Name; Message += backendSuffix(Lowered); if (!Lowered.Message.empty()) Message += " (" + Lowered.Message + ")"; @@ -2833,11 +2894,7 @@ class Verifier { if (Opts.LowerOnly) { VerifyResult Result; Result.Status = VerifyStatus::Lowered; - Result.BackendName = Opts.Backend == BackendKind::CVC5 ? "cvc5" - : Opts.Backend == BackendKind::Portfolio - ? "portfolio" - : Opts.Backend == BackendKind::Race ? "race" - : "z3"; + Result.BackendName = backendName(Opts.Backend); Diags.push_back({VerifyDiagnostic::Lowered, Fn->Name, SourceLocation(), Fn->Name, std::move(Result)}); continue; @@ -2852,7 +2909,8 @@ class Verifier { Passivizer Again; Again.setFunctionMap(InterfaceMap); Again.setUnfoldingDepth(Depth, WithFuel); - auto Built = buildObligationModule(Again.run(*WorkFn)); + auto Built = + buildObligationModule(Again.run(*WorkFn), Opts.MaxQueryNodes); if (!Built) { llvm::consumeError(Built.takeError()); return false; @@ -3527,6 +3585,7 @@ class Verifier { std::vector> Outcomes(Confirmations.size()); std::vector CutShort(Confirmations.size()); auto confirm = [&](size_t I) { + NodeBudget::Limit NodeLimit(Opts.MaxQueryNodes); const FunctionRun::Confirmation &Pending = Confirmations[I]; const VerifyDiagnostic &Verdict = Diags[Pending.Index]; if (Verdict.K != VerifyDiagnostic::Unresolved || From a89df38d4a9b9e604b7425ca1ba63353d174b10b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 05:58:09 +0530 Subject: [PATCH 21/52] verify: Add --memory-limit, a solver option, and accept --max-query-nodes with every backend. --- clang/tools/cpp-verify/Main.cpp | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp index 56e3ebfa58..075ee1425b 100644 --- a/clang/tools/cpp-verify/Main.cpp +++ b/clang/tools/cpp-verify/Main.cpp @@ -173,11 +173,17 @@ static unsigned jobs() { return 0; } -static cl::opt - MaxQueryNodes("max-query-nodes", - cl::desc("Maximum canonical expression nodes per solver " - "module (0 = no limit)"), - cl::init(0), cl::cat(CppVerifyCategory)); +static cl::opt MaxQueryNodes( + "max-query-nodes", + cl::desc("Maximum expression nodes of one function's proof obligations, " + "checked as they are built (default 32000000; 0 = no limit)"), + cl::init(verify::DefaultMaxQueryNodes), cl::cat(CppVerifyCategory)); + +static cl::opt MemoryLimit( + "memory-limit", + cl::desc("Megabytes Z3's queries may allocate together, and each cvc5 " + "process (default 8192; 0 = no limit)"), + cl::init(verify::DefaultMemoryLimitMB), cl::cat(CppVerifyCategory)); static cl::opt IntEncoding( "int-encoding", @@ -263,6 +269,7 @@ static verify::BackendExecutionOptions backendExecutionOptions() { Options.SolverResourceLimit = SolverResourceLimit; Options.Jobs = jobs(); Options.MaxQueryNodes = MaxQueryNodes; + Options.MemoryLimitMB = MemoryLimit; Options.IntegerEncoding = IntEncoding; Options.CVC5Path = CVC5Path; Options.ProofCachePath = ProofCache; @@ -341,6 +348,7 @@ class VerifyConsumer : public ASTConsumer { VOpts.SolverResourceLimit = SolverResourceLimit.getValue(); VOpts.Jobs = jobs(); VOpts.MaxQueryNodes = MaxQueryNodes.getValue(); + VOpts.MemoryLimitMB = MemoryLimit.getValue(); VOpts.IntegerEncoding = IntEncoding.getValue(); VOpts.CVC5Path = CVC5Path.getValue(); VOpts.ProofCachePath = ProofCache.getValue(); @@ -561,7 +569,7 @@ static bool resolveOptions(bool Replay) { const cl::Option *SolverOption = nullptr; for (const cl::Option *Option : std::initializer_list{ &SolverTimeout, &CollectionTimeout, &CertifyTimeout, - &FunctionTimeout, &SolverResourceLimit, &MaxQueryNodes, + &FunctionTimeout, &SolverResourceLimit, &MemoryLimit, &IntEncoding}) if (!SolverOption && given(*Option)) SolverOption = Option; @@ -629,6 +637,7 @@ static int replayObligationArchive() { return 1; } + verify::setZ3MemoryLimit(MemoryLimit); auto Buffer = llvm::MemoryBuffer::getFile(ObligationIn); if (!Buffer) { llvm::errs() << "error: cannot read obligation archive: " From 178690a3445959ef7c3a0c1665f307058529bc55 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:49:07 +0530 Subject: [PATCH 22/52] docs: Describe the memory limits in the tooling reference, with checked examples. --- website/source/language/tooling.rst | 174 ++++++++++++++++++++++++++-- 1 file changed, 167 insertions(+), 7 deletions(-) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index c0ad318cfc..5c69782e3d 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -23,6 +23,7 @@ Standalone verifier cpp-verify --timeout=20000 file.cpp cpp-verify --jobs=4 --proof-cache=.cppverify-cache file.cpp cpp-verify --solver-rlimit=500000 --max-query-nodes=50000 file.cpp + cpp-verify --memory-limit=4096 file.cpp cpp-verify --diagnostics-format=json file.cpp cpp-verify --dump-ir=1,2,3,4 file.cpp cpp-verify --lower-only --dump-ir=1,2,3,4 file.cpp @@ -173,7 +174,8 @@ Lean export runs no solver, so every solver option is an error with ``--backend=lean``, ``--lean-out``, or ``--lean-project``, the same way as ``--timeout`` above: ``--timeout``, ``--collection-timeout``, ``--certify-timeout``, ``--function-timeout``, ``--solver-rlimit``, -``--max-query-nodes``, and ``--int-encoding``. ``--lean-fallback`` runs Z3 +``--memory-limit``, and ``--int-encoding``. ``--max-query-nodes`` bounds what +is built for every backend, Lean's included. ``--lean-fallback`` runs Z3 first, and accepts all of them. The same rules hold when replaying an archive: ``--check-ub`` and @@ -300,11 +302,16 @@ Backends cvc5 may report the conservative ``solver.unknown``. Not accepted with ``--backend=lean``, which runs no solver. * - ``--max-query-nodes=N`` - - Reject a solver-backed canonical obligation module larger than ``N`` - expression nodes before verification, lower-only encoding, or a requested - Z3 dump (default ``0``, disabled). Exhaustion is fail-closed with reason - ``query.size-limit``. - Not accepted with ``--backend=lean``, which runs no solver. + - The expression nodes the verifier may build for one function (default + 32000000; ``0`` disables): its proof obligations, counted before they + are built, and the facts about the specs they apply, counted as they + are built. A function over it is ``Unresolved`` with reason + ``query.size-limit``, under every backend. See `Memory limits`_. + * - ``--memory-limit=MB`` + - The megabytes the solvers may use (default 8192; ``0`` disables): Z3's + queries together, and each cvc5 process. A query that reaches it is + ``Unresolved`` with reason ``solver.memory-limit``. Not accepted with + ``--backend=lean``, which runs no solver. See `Memory limits`_. * - ``--int-encoding=MODE`` - Solver representation of machine integers for Z3, cvc5, portfolio, and BMC: ``auto`` (default; integers reduced modulo ``2^N`` unless a query @@ -429,6 +436,159 @@ and the final check. A step that takes longer leaves every result ``Unresolved`` with reason ``lean.export-failed``, and its message gives the command's error. +Memory limits +------------- + +Two limits bound the memory verification takes: + +- ``--max-query-nodes`` bounds what the verifier builds for **one** function + (default 32,000,000 expression nodes): its proof obligations, and the facts + about the specs they apply. The obligations are counted before they are + built, so a function over the limit is refused before it takes the memory; + the facts are counted as they are built and stop at the limit. +- ``--memory-limit`` bounds the solvers (default 8192 MB): Z3's queries + together, since Z3 runs inside cpp-verify, and each cvc5 process on its + own. + +A function that reaches either is ``Unresolved``, never a proof or a +counterexample, and every function whose proof relies on its contract is +``Unresolved`` with reason ``callee.contract``. Nothing else changes. + +The proof obligations of a function grow faster than its code. Each check is +proved from everything before it (the preconditions, the statements, and the +earlier checks), and its obligation repeats all of it, so a function whose +checks follow many statements takes about their product. With two, four, and +eight checks like the four below, the obligations take 3,405, 8,505, and +25,425 nodes. With a limit of 2,000: + +.. cppverify-example: flags --max-query-nodes=2000 +.. cppverify-example: unresolved steps +.. code-block:: cpp + + int steps(int x) + cppverify::pre(0 <= x && x <= 100) + cppverify::post(cppverify::result == x + 4) + { + int y = x; + y = y + 1; + cppverify::check(y == x + 1); + y = y + 1; + cppverify::check(y == x + 2); + y = y + 1; + cppverify::check(y == x + 3); + y = y + 1; + cppverify::check(y == x + 4); + return y; + } + +.. code-block:: text + + steps.cpp:1:5: Unresolved: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 8505 expression nodes, more than the limit of 2000 (--max-query-nodes): each check repeats every assumption before it, so split the function or raise the limit) + +The count is exact: with ``--max-query-nodes=8505`` the function verifies. +Under ``--lower-only`` the same is an error, ``Z3 lowering failed: steps``, +since no obligations were built. A function split into functions with +contracts keeps each one's obligations small: a call repeats the callee's +contract, not its body. + +The default admits the largest function of the test suite, in the ULEB128 +case study (:doc:`../case-studies/llvm-uleb128`), whose obligations have 22.6 +million nodes. While obligations are built and checked, a node takes about +400 bytes, so the default lets one function take up to about 13 GB; with more +than one job, each job builds the obligations of its own function at once. + +The facts about the specs a function applies include each spec's definition, +unfolded as deep as its fuel. A spec that applies itself twice doubles with +every level: at fuel 40, ``fibo``'s unfolding would have about 2^40 copies of +its body. Its unfolding stops where it passes the limit, which, at the +default, takes a few seconds: + +.. cppverify-example: flags --max-query-nodes=200000 +.. cppverify-example: unresolved unfolds +.. code-block:: cpp + + cppverify::spec int fibo(int n) + cppverify::decreases(n) + { + return n <= 1 ? n : fibo(n - 1) + fibo(n - 2); + } + + int unfolds(int n) + cppverify::pre(n == 3) + cppverify::post(cppverify::result == fibo(3)) + { + cppverify::ghost { cppverify::reveal_with_fuel(fibo, 40); } + return 2; + } + +.. code-block:: text + + Verified: spec decreases: fibo + fibo.cpp:7:5: Unresolved: unfolds [backend=z3] [reason=query.size-limit] (the facts about the specs it applies (at each application, their definitions unfolded as deep as their fuel, and their postconditions) would take at least 228066 expression nodes, more than the limit of 200000 (--max-query-nodes): lower the fuel cppverify::reveal_with_fuel gives, or raise the limit) + +cpp-verify enforces ``--memory-limit`` while Z3 checks a query: every 10 ms +it compares what Z3 has allocated, all its queries together, with the limit, +and stops the query once it is past it. A matching loop, in which every +instance of a quantifier makes a term that matches it again, takes memory +until something stops it; without the limit that is the timeout, at 2 GB +after 20 s: + +.. cppverify-example: flags --memory-limit=100 --timeout=60000 +.. cppverify-example: unresolved matching_loop +.. code-block:: cpp + + cppverify::spec int g(int n) + cppverify::decreases(n) + { + return n <= 0 ? 0 : g(n - 1); + } + + void matching_loop(int a) + cppverify::pre(cppverify::forall(k, cppverify::trigger(g(k)) == g(k + 1) + 1)) + { + cppverify::ghost { cppverify::hide(g); } + cppverify::check(g(a) > 100); + } + + int small(int x) + cppverify::pre(x < 100) + cppverify::post(cppverify::result == x + 1) + { + return x + 1; + } + +.. code-block:: text + + Verified: spec decreases: g + loop.cpp:11:3: Unresolved: matching_loop [backend=z3] [reason=solver.memory-limit] (proof obligation fn_5f5a31336d61746368696e675f6c6f6f7069::assertion@11:3: Z3 reached the memory limit: its queries share 100 MB (--memory-limit)) + Verified: small [backend=z3] + +The memory of a stopped query is freed, so the next one runs within the +limit. Since Z3's queries share it, one that passes it stops every query +running beside it, which, like the time limits on a loaded machine, can leave +a function ``Unresolved`` that would verify alone; with ``--jobs=1`` a query +has the limit to itself. Under ``--int-encoding=bitvector`` a query stopped +for memory is retried in the integer encoding, as after a timeout. + +cvc5 runs as a process of its own, which may allocate up to the limit. Past +it an allocation fails and cvc5 stops (``std::bad_alloc``, or its SAT +solver's ``OutOfMemoryException``), and the query is ``Unresolved`` with +reason ``solver.memory-limit``: ``cvc5 ran out of memory: each cvc5 process +may use N MB (--memory-limit)``. The limit is applied on Linux, to the data +the process may allocate, and on Windows, to its committed memory; on macOS, +which applies no such limit to the memory a process maps, cvc5 is not +bounded. With several jobs, as many cvc5 processes may run at once. + +Choosing the limits: + +- Interactive use: the defaults. A function over ``--max-query-nodes`` is + usually one to split into functions with contracts. +- A machine with little memory: lower ``--jobs`` first, since each job + builds one function's obligations at once, then the two limits. +- Continuous integration with a memory allowance: give ``--memory-limit`` + the solvers' share, and ``--max-query-nodes`` the rest divided by + ``--jobs`` and by 400 bytes. + Parallel solving and proof caching ---------------------------------- @@ -516,7 +676,7 @@ the same names, ranges, IDs, and trace data during replay. Each non-success verification result also carries a stable reason code. Current codes include ``counterexample``, ``solver.timeout``, ``solver.unknown``, -``solver.resource-limit``, ``solver.unavailable``, +``solver.resource-limit``, ``solver.memory-limit``, ``solver.unavailable``, ``solver.invocation-failed``, ``solver.malformed-output``, ``query.size-limit``, ``encoding.failed`` (the obligations could not be encoded for the solver; when Z3 rejected a call, the message quotes it: From d1d6725171b666a1e96e3aa75d19c466ee3dffa0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:49:08 +0530 Subject: [PATCH 23/52] docs: List --memory-limit and the new meaning of --max-query-nodes in chapter 15. --- website/source/book/part-ii/ch15-toolchain-and-flags.rst | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/website/source/book/part-ii/ch15-toolchain-and-flags.rst b/website/source/book/part-ii/ch15-toolchain-and-flags.rst index 0b2992dabb..cd0b8e4f95 100644 --- a/website/source/book/part-ii/ch15-toolchain-and-flags.rst +++ b/website/source/book/part-ii/ch15-toolchain-and-flags.rst @@ -66,8 +66,12 @@ Other flags others - ``cpp-verify --solver-rlimit=N`` — deterministic per-query resource budget for Z3 and cvc5 (``0`` disables) -- ``cpp-verify --max-query-nodes=N`` — refuse a query larger than ``N`` - expression nodes (``query.size-limit``) +- ``cpp-verify --max-query-nodes=N`` — the expression nodes the verifier may + build for one function: its proof obligations, and the facts about the + specs they apply (default 32000000; ``0`` disables; ``query.size-limit``) +- ``cpp-verify --memory-limit=MB`` — the megabytes the solvers may use, Z3's + queries together and each cvc5 process (default 8192; ``0`` disables; + ``solver.memory-limit``) - ``cpp-verify --jobs=N`` — solver workers shared by all functions (default the available physical cores, or ``CPPVERIFY_JOBS``; 1 for ``--backend=lean``) - ``cpp-verify --proof-cache=DIR`` — keep proofs of single obligations between From 44e0faa10983d3cfc72fb67f2518d7047dc36904 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:49:08 +0530 Subject: [PATCH 24/52] docs: Explain solver.memory-limit and query.size-limit in chapter 16. --- .../part-ii/ch16-when-verification-fails.rst | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/website/source/book/part-ii/ch16-when-verification-fails.rst b/website/source/book/part-ii/ch16-when-verification-fails.rst index 7db5d0f911..419e1cd4dc 100644 --- a/website/source/book/part-ii/ch16-when-verification-fails.rst +++ b/website/source/book/part-ii/ch16-when-verification-fails.rst @@ -30,10 +30,11 @@ are replaced with the Unicode replacement character, so JSON output remains valid UTF-8. An undecided query is different from a counterexample. ``Unresolved`` with -reason ``solver.timeout``, ``solver.resource-limit``, or ``solver.unknown`` -means Z3 timed out, exhausted an explicit resource/query budget, or entered a -fragment it could not decide, often because the VC combines quantifiers with -heap arrays. CppVerify may retry smaller ordered obligations, but if those also +reason ``solver.timeout``, ``solver.resource-limit``, ``solver.memory-limit``, +or ``solver.unknown`` means Z3 timed out, exhausted an explicit resource/query +budget, reached the memory ``--memory-limit`` gives it, or entered a fragment +it could not decide, often because the VC combines quantifiers with heap +arrays. CppVerify may retry smaller ordered obligations, but if those also remain undecided it reports the function ``Unresolved``. It never treats solver uncertainty as success. @@ -156,6 +157,10 @@ Every result that is not a proof carries one stable reason code (text other solver of ``--backend=race`` settled the function. * - ``solver.resource-limit`` - ``--solver-rlimit`` was reached. + * - ``solver.memory-limit`` + - A solver reached ``--memory-limit``: Z3's queries, which share it, or + a cvc5 process. Raise the limit, run fewer ``--jobs``, or help the + proof (a matching loop takes memory until it is stopped). * - ``solver.unavailable`` - The solver (cvc5) is not installed; pass ``--cvc5-path``. * - ``solver.invocation-failed``, ``solver.malformed-output`` @@ -170,7 +175,10 @@ Every result that is not a proof carries one stable reason code (text - ``BoundedSafe``: safe within ``--unroll`` iterations, but a loop can run longer. Raise the bound, or prove the loop with an invariant. * - ``query.size-limit`` - - The query is larger than ``--max-query-nodes``. + - The function's proof obligations, or the facts about the specs they + apply, would be larger than ``--max-query-nodes``. Split the function + into functions with contracts, lower ``cppverify::reveal_with_fuel``, + or raise the limit. * - ``logic.unsupported`` - The backend does not support a feature the query needs (Lean and collections, for example). From 4f2eba0c9f480feb6d0f27fc0b0791c8cad4b021 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:49:09 +0530 Subject: [PATCH 25/52] docs: Note the node limit of a function's obligations in the limitations. --- website/source/language/limitations.rst | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 2f5057c7d0..80a0d9586a 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -135,7 +135,11 @@ C++ feature boundaries instantiate, and are ignored with a warning, and one with contract statements is reported), variadics, indirect calls, recursion through a function that allocates or frees storage, and general link-time - summaries. + summaries. A function whose proof obligations would take more than + ``--max-query-nodes`` expression nodes (32 million by default) is + ``Unresolved`` with reason ``query.size-limit``: each check repeats + every assumption before it, so a long function with many checks grows + fastest. See the memory limits of :doc:`tooling`. * - Storage - Supported locals, constrained scalar dynamic storage, and inferred acyclic fresh-owned scalar factory results. From 8f3fd97b9392b937dc3700a7f91b0d114da270ed Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:49:10 +0530 Subject: [PATCH 26/52] docs: Add the memory limits to the 0.2.0 release notes. --- website/source/release-notes.rst | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index d9695f3f7d..4138e9d6c2 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -158,6 +158,17 @@ expression nested more than 256 operations deep is reported where it is report something unrelated. The query now ends ``Unresolved`` with reason ``encoding.failed`` and Z3's message (:doc:`language/tooling`). +**Memory limits.** Nothing bounded the memory a run took: a function whose +proof obligations, which repeat every assumption before each check, came to +hundreds of millions of nodes, or ``cppverify::reveal_with_fuel(fibo, 24)``, +took tens of gigabytes until the system stopped the run. ``--max-query-nodes`` +now has a default, 32 million expression nodes, and bounds what is built for +one function before it is built; a function over it is ``Unresolved`` with +reason ``query.size-limit``, which names what was too large. The new +``--memory-limit`` (default 8192 MB) bounds Z3's queries together and each +cvc5 process; a query that reaches it is ``Unresolved`` with reason +``solver.memory-limit`` (:doc:`language/tooling`). + **Parallel runs.** With more than one job, a function waiting for its own queries could run another function's long query, delaying its result and spending its ``--function-timeout``. A waiting function now runs only its own @@ -175,8 +186,8 @@ Data formats Archives stay ``cppverify.obligation/2`` and JSON diagnostics ``cppverify.diagnostic/1``. JSON records may carry the status -``proved-obligations`` (archive replay) and the reason ``interrupted`` -(Ctrl-C). +``proved-obligations`` (archive replay) and the reasons ``interrupted`` +(Ctrl-C) and ``solver.memory-limit`` (``--memory-limit``). 0.1.1 ----- From e1ad3466c0b00b26041b2c7b0eefb8d54d721754 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:49:10 +0530 Subject: [PATCH 27/52] docs: Describe the node and memory limits in DESIGN. --- docs/DESIGN.md | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 249d5bde2a..8798996e7c 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1708,8 +1708,9 @@ parameter and result signature. Backend results carry stable machine-readable reason codes independently of their human message: `counterexample`, `solver.timeout`, `solver.unknown`, -`solver.resource-limit`, `solver.unavailable`, `solver.invocation-failed`, -`solver.malformed-output`, `query.size-limit`, `encoding.failed`, +`solver.resource-limit`, `solver.memory-limit`, `solver.unavailable`, +`solver.invocation-failed`, `solver.malformed-output`, `query.size-limit`, +`encoding.failed`, `obligation.invalid`, `logic.unsupported`, `query.missing`, `backend.invalid-result`, `backend.inconsistent-results`, `bmc.incomplete-bound`, `lean.export-failed`, `cache.corrupt`, @@ -1734,10 +1735,18 @@ canonical source order, so concurrency cannot choose which failure is public. `--function-timeout` (by default ten times `--timeout`) bounds all queries of one function together, in wall-clock time; once it is spent no further query starts and the function is `Unresolved` (`solver.timeout`). AST/VCR lowering and Lean emission remain serial. -`--solver-rlimit` adds a deterministic per-query Z3 budget, while -`--max-query-nodes` rejects an oversized canonical module before -verification, lower-only encoding, or a requested Z3 dump; neither limit can -become success. +`--solver-rlimit` adds a deterministic per-query Z3 budget. +`--max-query-nodes` (default 32,000,000) bounds the expression nodes built +for one function: the size of its obligations, each of which repeats every +assumption before it, is known exactly before they are built, so a function +over the limit is refused before it takes the memory, and the facts about +the specs it applies (definitions unfolded as deep as their fuel, +postconditions at each application) are counted as they are built and stop +at the limit. `--memory-limit` (default 8192 MB) bounds Z3's queries +together, which a check's watchdog stops once Z3's allocations pass it, and +each cvc5 process, whose allocations past it fail. Neither limit can become +success: a function over the first is `Unresolved` with `query.size-limit`, +a query stopped by the second with `solver.memory-limit`. `--proof-cache=DIR` stores only successful individual proofs. The key binds an obligation's dependency-scoped semantic hash to hash format v4, the backend From 5e803d7db317db61baa834a315b9cd5ce69674d4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:49:11 +0530 Subject: [PATCH 28/52] docs: Describe how the node and memory limits are enforced in ARCHITECTURE. --- docs/ARCHITECTURE.md | 33 ++++++++++++++++++++++++++++++++- 1 file changed, 32 insertions(+), 1 deletion(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index acf48ef64e..927d7d88d8 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -487,6 +487,25 @@ Construction returns `llvm::Expected`. A null, unhandled, malformed, or untyped term prevents publication of the module and is reported as `unknown`; it is never replaced by `true`. +**Size.** Each obligation's goal is its condition under a negated copy of +every assumption before it, so a module grows with its obligations times +the assumptions before them. Its node count, as `obligationModuleNodeCount` +counts it, is computed from the lowered statements before any goal is built +(four times the goals' nodes, for the goals, their queries, the complete +goal, and its query, plus three per obligation less one; an assertion +checks the count against the built module); over `--max-query-nodes` the +build returns `ObligationSizeError`. Constructions whose size the program +does not bound are counted as they go: `NodeBudget` (`IR/NodeBudget.h`) +counts the `VExpr` and `LogicExpr` nodes built on its thread against the +limit the driver sets for the function, and the spec inliner unfolds +nothing more once it is spent. The definitions `SpecAxioms` materializes, +each spec unfolded as deep as its fuel, are counted level by level into the +module's count; the facts the passivizer adds at each spec application are +counted in a budget, and a spent one leaves `PassiveProgram::TooLarge`, which +makes the build an `ObligationSizeError`; so does a spent budget while specs +are inlined for BMC. The driver reports the error as the function's verdict, +`Unresolved` with `query.size-limit`, and never uses the partial result. + Every source-built or replayed module then passes through one fail-closed canonicalization step before hashing or backend dispatch. The pass folds only sort-preserving Boolean constants, double negation, constant conditionals, and @@ -1540,7 +1559,19 @@ split; `Certified` still means Lean checked every obligation. SAT counterexamples are never fallback successes. Z3-backed execution accepts explicit timeout, deterministic solver-resource, -canonical query-node, job-count, and proof-cache budgets. A module that +canonical query-node, memory, job-count, and proof-cache budgets. Z3 runs in +the process, so its memory limit is for its queries together: the watchdog +of every check, which already interrupts it at its time, polls Z3's +allocation every 10 ms while a limit is set and interrupts the check past +it, and the encoder's result is then `solver.memory-limit`. Z3's own limits +are not used: `memory_max_size` fails whichever allocation passes it in any +context, `Z3_mk_context`'s included, which then returns no context, and the +high watermark stops a search reporting only `canceled` and frees what it +took before the check returns. Each cvc5 process gets the limit as its +`RLIMIT_DATA`, set with `prlimit` once it is spawned (on Windows, the job +object of `ExecuteNoWait`): a limit makes `ExecuteNoWait` fork rather than +spawn on POSIX hosts, and fork runs Z3's fork handlers, which wait for the +timers of every check in the process. A module that requires the `sequences` or `collections` feature gets the collection timeout (`--collection-timeout`, by default twice `--timeout`) on every solver backend. The driver verifies each function as a task (its own backend, From 35115b8cea407ab373acf40b0e09d6ba9b125705 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 04:49:11 +0530 Subject: [PATCH 29/52] docs: Let a page expect a function refused for its size to fail lowering. --- website/scripts/check-doc-examples.py | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/website/scripts/check-doc-examples.py b/website/scripts/check-doc-examples.py index 2c48ef57d4..39fb855b77 100644 --- a/website/scripts/check-doc-examples.py +++ b/website/scripts/check-doc-examples.py @@ -17,7 +17,9 @@ .. cppverify-example: fails NAME ... these functions fail with a counterexample .. cppverify-example: unresolved NAME ... - these stay unresolved + these stay unresolved; one too + large to build (query.size-limit) + fails to lower too .. cppverify-example: rejects the example is an error: cpp-verify reports one and exits non-zero @@ -47,6 +49,8 @@ r" (.+?)(?=\s+\[|\s+\(|$)") FAILED = re.compile(r"error: (verification failed|spec [\w ]+? failed): " r"(.+?)(?=\s+\[|\s+\(|$)") +TOO_LARGE = re.compile(r"error: \w+ lowering failed: (\S+) .*" + r"\[reason=query\.size-limit\]") LOCATION = re.compile(r"^\S+\.(?:cpp|h):\d+:\d+: ") DIAGNOSTIC = re.compile(r"^(?:error|warning): ") @@ -206,7 +210,15 @@ def check(cpp_verify, job): f"\nactual output:\n{output.strip()[:2500]}"), False return None code, output = run(cpp_verify, source, ["--lower-only", *arguments], 300) - if code is None or code != 0 or "error:" in output: + # A function refused for its size builds no obligations to lower. + refused, errors = set(), [] + for line in output.splitlines(): + match = TOO_LARGE.search(line) + if match and match.group(1) in unresolved: + refused.add(match.group(1)) + elif "error:" in line: + errors.append(line) + if code is None or errors or (code != 0 and not refused): return f"{where}: the example does not compile:\n{output.strip()[:1500]}", False code, output = run(cpp_verify, source, [f"--jobs={SOLVER_JOBS}", *arguments], 900) From 35cb2e96f762b9803835ceb35cb780cf57cd155f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 05:05:12 +0530 Subject: [PATCH 30/52] test: Check that obligations over the node limit are refused at their exact size. --- .../Verify/suite/obligation_size_limit.cpp | 133 ++++++++++++++++++ 1 file changed, 133 insertions(+) create mode 100644 clang/test/Verify/suite/obligation_size_limit.cpp diff --git a/clang/test/Verify/suite/obligation_size_limit.cpp b/clang/test/Verify/suite/obligation_size_limit.cpp new file mode 100644 index 0000000000..d35f245c21 --- /dev/null +++ b/clang/test/Verify/suite/obligation_size_limit.cpp @@ -0,0 +1,133 @@ +// RUN: not %cpp-verify --jobs=1 --max-query-nodes=3000 %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=LIMIT +// RUN: not %cpp-verify --jobs=1 --max-query-nodes=3000 \ +// RUN: --diagnostics-format=json %s -- 2>&1 | FileCheck %s --check-prefix=JSON +// RUN: not %cpp-verify --lower-only --max-query-nodes=3000 %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=LOWER +// +// The size is exact: at it the obligations are built, one below they are not. +// RUN: %cpp-verify --jobs=1 --max-query-nodes=24417 %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=AT +// RUN: not %cpp-verify --jobs=1 --max-query-nodes=24416 %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=BELOW +// +// A spec unfolded as deep as its fuel stops at the limit: at fuel 40, fibo's +// unfolding would have about 2^40 copies of its body. +// RUN: not %cpp-verify --jobs=1 --max-query-nodes=200000 %s -- -DFUEL 2>&1 \ +// RUN: | FileCheck %s --check-prefix=FUEL +// +// The definitions of the specs a module applies count with its obligations: +// 26167 nodes here, fib's definitions at fuel 4 included. +// RUN: %cpp-verify --jobs=1 --max-query-nodes=26167 %s -- -DDEFINITIONS 2>&1 \ +// RUN: | FileCheck %s --check-prefix=DEFINITIONS-AT +// RUN: not %cpp-verify --jobs=1 --max-query-nodes=26166 %s -- -DDEFINITIONS \ +// RUN: 2>&1 | FileCheck %s --check-prefix=DEFINITIONS + +// Each check repeats every assumption before it, so the obligations of a +// function grow with its checks times the statements before them. +int steps(int x) + cppverify::pre(0 <= x && x <= 100) + cppverify::post(cppverify::result == x + 8) +{ + int y = x + 1; + cppverify::check(y == x + 1); + y = y + 1; + cppverify::check(y == x + 2); + y = y + 1; + cppverify::check(y == x + 3); + y = y + 1; + cppverify::check(y == x + 4); + y = y + 1; + cppverify::check(y == x + 5); + y = y + 1; + cppverify::check(y == x + 6); + y = y + 1; + cppverify::check(y == x + 7); + y = y + 1; + cppverify::check(y == x + 8); + return y; +} +// LIMIT: obligation_size_limit.cpp:[[@LINE-22]]:5: Unresolved: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 24417 expression nodes, more than the limit of 3000 (--max-query-nodes): each check repeats every assumption before it, so split the function or raise the limit) +// JSON: {"backend":"z3","function":"steps","message":"steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 24417 expression nodes, more than the limit of 3000 (--max-query-nodes): each check repeats every assumption before it, so split the function or raise the limit)","reason":"query.size-limit","schema":"cppverify.diagnostic/1","severity":"error","source":{"column":5,"end_column":5,"end_line":[[@LINE-23]],"file":"{{.*}}obligation_size_limit.cpp","line":[[@LINE-23]]},"status":"unresolved"} +// LOWER: obligation_size_limit.cpp:[[@LINE-24]]:5: error: Z3 lowering failed: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 24417 expression nodes, more than the limit of 3000 +// AT: Verified: steps [backend=z3] +// BELOW: Unresolved: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 24417 expression nodes, more than the limit of 24416 (--max-query-nodes) + +// Its verdict relies on the contract of steps, which nothing establishes. +int caller(int x) + cppverify::pre(0 <= x && x <= 100) + cppverify::post(cppverify::result == x + 9) +{ + int y = steps(x); + return y + 1; +} +// LIMIT: Unresolved: caller [backend=z3] [reason=callee.contract] (relies on the contract of steps, which is not established) +// JSON: {"backend":"z3","function":"caller","message":"caller [backend=z3] [reason=callee.contract] (relies on the contract of steps, which is not established)","reason":"callee.contract", +// LOWER: Lowered: caller +// AT: Verified: caller [backend=z3] +// BELOW: Unresolved: caller [backend=z3] [reason=callee.contract] + +int small(int x) + cppverify::pre(x < 100) + cppverify::post(cppverify::result == x + 1) +{ + return x + 1; +} +// LIMIT: Verified: small [backend=z3] +// LOWER: Lowered: small +// AT: Verified: small [backend=z3] +// BELOW: Verified: small [backend=z3] + +#ifdef FUEL +cppverify::spec int fibo(int n) + cppverify::decreases(n) +{ + return n <= 1 ? n : fibo(n - 1) + fibo(n - 2); +} + +int unfolds(int n) + cppverify::pre(n == 3) + cppverify::post(cppverify::result == fibo(3)) +{ + cppverify::ghost { cppverify::reveal_with_fuel(fibo, 40); } + return 2; +} +#endif +// FUEL: Verified: steps [backend=z3] +// FUEL: Verified: spec decreases: fibo +// FUEL: obligation_size_limit.cpp:[[@LINE-10]]:5: Unresolved: unfolds [backend=z3] [reason=query.size-limit] (the facts about the specs it applies (at each application, their definitions unfolded as deep as their fuel, and their postconditions) would take at least {{[0-9]+}} expression nodes, more than the limit of 200000 (--max-query-nodes): lower the fuel cppverify::reveal_with_fuel gives, or raise the limit) + +#ifdef DEFINITIONS +cppverify::spec int fib(int n) + cppverify::decreases(n) +{ + return n <= 1 ? n : fib(n - 1) + fib(n - 2); +} + +int defined(int x) + cppverify::pre(0 <= x && x <= 100) + cppverify::post(cppverify::result == x + 8 && fib(6) == 8) +{ + cppverify::ghost { cppverify::reveal_with_fuel(fib, 4); } + int y = x; + y = y + 1; + cppverify::check(y == x + 1); + y = y + 1; + cppverify::check(y == x + 2); + y = y + 1; + cppverify::check(y == x + 3); + y = y + 1; + cppverify::check(y == x + 4); + y = y + 1; + cppverify::check(y == x + 5); + y = y + 1; + cppverify::check(y == x + 6); + y = y + 1; + cppverify::check(y == x + 7); + y = y + 1; + cppverify::check(y == x + 8); + return y; +} +#endif +// DEFINITIONS-AT: Verified: defined [backend=z3] +// DEFINITIONS: Unresolved: defined [backend=z3] [reason=query.size-limit] (the proof obligations with the definitions of the specs they apply would take at least 26167 expression nodes, more than the limit of 26166 (--max-query-nodes): lower the fuel cppverify::reveal_with_fuel gives, split the function, or raise the limit) From 9716be4bbcb37237c7396244ab922fbf102e93c8 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 05:05:13 +0530 Subject: [PATCH 31/52] test: Generate a function of many checks for the memory tests. --- clang/test/Verify/suite/Inputs/many_checks.py | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/many_checks.py diff --git a/clang/test/Verify/suite/Inputs/many_checks.py b/clang/test/Verify/suite/Inputs/many_checks.py new file mode 100644 index 0000000000..b7e54ca0bf --- /dev/null +++ b/clang/test/Verify/suite/Inputs/many_checks.py @@ -0,0 +1,13 @@ +# usage: many_checks.py N OUT: a function of N increments, each followed by a +# check. Each check repeats every assumption before it, so its obligations +# grow with N squared. +import sys + +n = int(sys.argv[1]) +steps = "".join(" y = y + 1;\n cppverify::check(y == x + %d);\n" % (i + 1) + for i in range(n)) +with open(sys.argv[2], "w") as out: + out.write("int many_checks(int x)\n" + " cppverify::pre(0 <= x && x <= 100)\n" + " cppverify::post(cppverify::result == x + %d)\n" + "{\n int y = x;\n%s return y;\n}\n" % (n, steps)) From 7a70fbee5a807947672b7250efcbf5f7936e61bf Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 05:05:13 +0530 Subject: [PATCH 32/52] test: Check that large obligations and deep fuel end within a 3 GB address space. --- clang/test/Verify/suite/memory_bounded.test | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) create mode 100644 clang/test/Verify/suite/memory_bounded.test diff --git a/clang/test/Verify/suite/memory_bounded.test b/clang/test/Verify/suite/memory_bounded.test new file mode 100644 index 0000000000..a7bf787ca8 --- /dev/null +++ b/clang/test/Verify/suite/memory_bounded.test @@ -0,0 +1,18 @@ +# REQUIRES: system-linux +# UNSUPPORTED: msan, asan, hwasan +# +# Within a 3 GB address space, functions whose obligations, or whose specs +# unfolded as deep as their fuel, would take far more end with a verdict +# instead of failing an allocation: what is built is counted as it is built +# (or before, for the obligations) and stops at --max-query-nodes. +# RUN: rm -rf %t && mkdir -p %t +# RUN: %python %S/Inputs/many_checks.py 400 %t/many.cpp +# RUN: ulimit -v 3000000 +# RUN: not %cpp-verify --jobs=1 --max-query-nodes=2000000 %t/many.cpp -- 2>&1 \ +# RUN: | FileCheck %s --check-prefix=MANY +# RUN: not %cpp-verify --jobs=1 --max-query-nodes=2000000 \ +# RUN: %S/obligation_size_limit.cpp -- -DFUEL 2>&1 | FileCheck %s --check-prefix=FUEL + +MANY: Unresolved: many_checks [backend=z3] [reason=query.size-limit] (the proof obligations would take at least {{[0-9]+}} expression nodes, more than the limit of 2000000 (--max-query-nodes) +FUEL: Verified: small [backend=z3] +FUEL: Unresolved: unfolds [backend=z3] [reason=query.size-limit] (the facts about the specs it applies From c9a59c29b96fa6a9e33189d26562cdecb2249dc0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 05:05:14 +0530 Subject: [PATCH 33/52] test: Check that a Z3 query past --memory-limit stops with solver.memory-limit. --- .../test/Verify/suite/solver_memory_limit.cpp | 36 +++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 clang/test/Verify/suite/solver_memory_limit.cpp diff --git a/clang/test/Verify/suite/solver_memory_limit.cpp b/clang/test/Verify/suite/solver_memory_limit.cpp new file mode 100644 index 0000000000..7a52b5ad3a --- /dev/null +++ b/clang/test/Verify/suite/solver_memory_limit.cpp @@ -0,0 +1,36 @@ +// RUN: not %cpp-verify --jobs=1 --timeout=60000 --memory-limit=100 %s -- 2>&1 \ +// RUN: | FileCheck %s +// RUN: not %cpp-verify --jobs=1 --timeout=60000 --memory-limit=100 \ +// RUN: --diagnostics-format=json %s -- 2>&1 | FileCheck %s --check-prefix=JSON +// RUN: not %cpp-verify --backend=lean --memory-limit=100 %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=LEAN + +// A matching loop: each instance of the quantifier makes a term that matches +// it again, so Z3's memory grows until something stops the query. Without a +// memory limit that is the timeout, at 2 GB after 20 s. +cppverify::spec int g(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : g(n - 1); +} + +void matching_loop(int a) + cppverify::pre(cppverify::forall(k, cppverify::trigger(g(k)) == g(k + 1) + 1)) +{ + cppverify::ghost { cppverify::hide(g); } + cppverify::check(g(a) > 100); +} +// CHECK: solver_memory_limit.cpp:[[@LINE-2]]:3: Unresolved: matching_loop [backend=z3] [reason=solver.memory-limit] ({{.*}}: Z3 reached the memory limit: its queries share 100 MB (--memory-limit)) +// JSON: "function":"matching_loop"{{.*}}"reason":"solver.memory-limit" + +// The memory of a stopped query is freed, and the next one runs within the +// limit. +int small(int x) + cppverify::pre(x < 100) + cppverify::post(cppverify::result == x + 1) +{ + return x + 1; +} +// CHECK: Verified: small [backend=z3] + +// LEAN: error: --memory-limit requires a backend that runs an SMT solver From 98002263118839ea6ac81dc72d3cb1a60b861e85 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 05:05:15 +0530 Subject: [PATCH 34/52] test: Check that a cvc5 process past --memory-limit reports solver.memory-limit. --- clang/test/Verify/suite/cvc5_memory_limit.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 clang/test/Verify/suite/cvc5_memory_limit.cpp diff --git a/clang/test/Verify/suite/cvc5_memory_limit.cpp b/clang/test/Verify/suite/cvc5_memory_limit.cpp new file mode 100644 index 0000000000..eba3e165cc --- /dev/null +++ b/clang/test/Verify/suite/cvc5_memory_limit.cpp @@ -0,0 +1,16 @@ +// REQUIRES: cvc5, system-linux +// RUN: not %cpp-verify --backend=cvc5 --jobs=1 --memory-limit=5 %s -- 2>&1 \ +// RUN: | FileCheck %s +// +// Each cvc5 process may allocate --memory-limit megabytes; on Linux that is +// its data (RLIMIT_DATA). cvc5 needs more than 5 to start solving, so every +// query runs out, which cvc5 reports as std::bad_alloc or as its SAT solver's +// OutOfMemoryException. + +int small(int x) + cppverify::pre(x < 100) + cppverify::post(cppverify::result == x + 1) +{ + return x + 1; +} +// CHECK: Unresolved: small [backend=cvc5] [reason=solver.memory-limit] ({{.*}}: cvc5 ran out of memory: each cvc5 process may use 5 MB (--memory-limit)) From c1012433f77cfd2941cf6ae642c1cbd536ba4783 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 05:05:15 +0530 Subject: [PATCH 35/52] test: Expect the node limit's new messages in the backend execution test. --- clang/test/Verify/suite/backend_execution.test | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/clang/test/Verify/suite/backend_execution.test b/clang/test/Verify/suite/backend_execution.test index 8e3e04a054..c851f7330b 100644 --- a/clang/test/Verify/suite/backend_execution.test +++ b/clang/test/Verify/suite/backend_execution.test @@ -96,14 +96,12 @@ # PRUNE-ONCE-SAME: [reason=cache.corrupt] # NODES: Unresolved: cached_identity [backend=z3] [reason=query.size-limit] -# NODES-SAME: exceeds query node budget 1 -# NODES-LOWER: error: Z3 lowering failed: cached_identity -# NODES-LOWER-SAME: [reason=query.size-limit] -# NODES-LOWER-SAME: exceeds query node budget 1 -# NODES-DUMP: error: Z3 lowering failed: cached_identity -# NODES-DUMP-SAME: [reason=query.size-limit] -# NODES-DUMP-SAME: exceeds query node budget 1 -# NODES-REPLAY: Unresolved: cached_identity (canonical obligation module exceeds query node budget 1) +# NODES-SAME: (the proof obligations would take at least {{[0-9]+}} expression nodes, more than the limit of 1 (--max-query-nodes) +# NODES-LOWER: error: Z3 lowering failed: cached_identity [backend=z3] [reason=query.size-limit] +# NODES-LOWER-SAME: more than the limit of 1 (--max-query-nodes) +# NODES-DUMP: Unresolved: cached_identity [backend=z3] [reason=query.size-limit] +# NODES-DUMP-SAME: more than the limit of 1 (--max-query-nodes) +# NODES-REPLAY: Unresolved: cached_identity (the obligation module has {{[0-9]+}} expression nodes, more than the limit of 1 (--max-query-nodes)) # NODES-REPLAY-SAME: [reason=query.size-limit] # RLIMIT: Unresolved: cached_identity From 69da72a1ba38aed6aebac847cae3613d2feeae6b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Wed, 21 Oct 2026 06:00:55 +0530 Subject: [PATCH 36/52] test: Expect --memory-limit, not --max-query-nodes, to be rejected with Lean export. --- clang/test/Verify/suite/backend_options.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/clang/test/Verify/suite/backend_options.cpp b/clang/test/Verify/suite/backend_options.cpp index 7ed4bccc33..f11436609c 100644 --- a/clang/test/Verify/suite/backend_options.cpp +++ b/clang/test/Verify/suite/backend_options.cpp @@ -21,8 +21,9 @@ // RUN: not %cpp-verify --backend=lean --collection-timeout=1000 %s -- 2>&1 | FileCheck %s --check-prefix=COLLECTION // RUN: not %cpp-verify --lean-out=%t/budget.lean --certify-timeout=1000 %s -- 2>&1 | FileCheck %s --check-prefix=CERTIFY // RUN: not %cpp-verify --lean-out=%t/budget.lean --solver-rlimit=100000 %s -- 2>&1 | FileCheck %s --check-prefix=RLIMIT -// RUN: not %cpp-verify --lean-out=%t/budget.lean --max-query-nodes=100000 %s -- 2>&1 | FileCheck %s --check-prefix=NODES +// RUN: not %cpp-verify --lean-out=%t/budget.lean --memory-limit=4096 %s -- 2>&1 | FileCheck %s --check-prefix=MEMORY // RUN: not test -e %t/budget.lean +// RUN: %cpp-verify --lean-out=%t/nodes.lean --max-query-nodes=100000 %s -- 2>&1 | FileCheck %s --check-prefix=NODES // RUN: not %cpp-verify --obligation-in=%t/goals.cpv --lean-out=%t/budget.lean --timeout=1000 2>&1 | FileCheck %s --check-prefix=TIMEOUT // RUN: %cpp-verify --timeout=20000 --function-timeout=200000 --solver-rlimit=50000000 --max-query-nodes=1000000 %s -- 2>&1 | FileCheck %s --check-prefix=SOLVER // RUN: %cpp-verify --lean-fallback=%t/fallback --timeout=20000 %s -- 2>&1 | FileCheck %s --check-prefix=SOLVER @@ -62,5 +63,6 @@ int count(int n) // COLLECTION: error: --collection-timeout requires a backend that runs an SMT solver // CERTIFY: error: --certify-timeout requires a backend that runs an SMT solver // RLIMIT: error: --solver-rlimit requires a backend that runs an SMT solver -// NODES: error: --max-query-nodes requires a backend that runs an SMT solver +// MEMORY: error: --memory-limit requires a backend that runs an SMT solver +// NODES: Exported: lean obligation: count // SOLVER: Verified: count [backend=z3] From f49bbb811696003e1b2b503d0e2fb14354bd6456 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:14 +0530 Subject: [PATCH 37/52] verify: Count a module's distinct nodes, and its terms as trees up to a limit. --- clang/lib/Verify/Backend/LogicTerms.h | 8 +++ .../lib/Verify/Backend/ObligationSimplify.cpp | 72 ++++++++++++++++++- clang/lib/Verify/Backend/ObligationSimplify.h | 10 ++- 3 files changed, 87 insertions(+), 3 deletions(-) diff --git a/clang/lib/Verify/Backend/LogicTerms.h b/clang/lib/Verify/Backend/LogicTerms.h index 8952375083..630f58d561 100644 --- a/clang/lib/Verify/Backend/LogicTerms.h +++ b/clang/lib/Verify/Backend/LogicTerms.h @@ -3,6 +3,7 @@ #define LLVM_CLANG_VERIFY_BACKEND_LOGICTERMS_H #include "Obligation.h" +#include "llvm/ADT/ArrayRef.h" #include #include #include @@ -11,6 +12,13 @@ namespace clang { namespace verify { uint64_t logicNodeCount(const LogicExpr *Expr); +/// The nodes of \p Expr as a tree, each shared subterm counted at each of its +/// places, as a printer that expands terms writes them; once past \p Limit, +/// any count above it. +uint64_t logicTreeNodesUpTo(const LogicExpr *Expr, uint64_t Limit); +/// The distinct nodes of \p Roots, a node they share counted once: what +/// they take in memory. +uint64_t logicDistinctNodes(llvm::ArrayRef Roots); bool logicEqual(const LogicExpr *Left, const LogicExpr *Right); /// A string equal for structurally equal terms. std::string logicKey(const LogicExpr *Expr); diff --git a/clang/lib/Verify/Backend/ObligationSimplify.cpp b/clang/lib/Verify/Backend/ObligationSimplify.cpp index 66154f06fe..df05b3d3f9 100644 --- a/clang/lib/Verify/Backend/ObligationSimplify.cpp +++ b/clang/lib/Verify/Backend/ObligationSimplify.cpp @@ -4,6 +4,7 @@ #include "LogicTerms.h" #include "llvm/ADT/APInt.h" #include "llvm/ADT/DenseMap.h" +#include "llvm/ADT/DenseSet.h" #include "llvm/ADT/StringRef.h" #include "llvm/Support/CheckedArithmetic.h" #include @@ -1000,7 +1001,76 @@ std::unique_ptr instantiateExtensionality(const LogicExpr &Query) { } uint64_t obligationModuleNodeCount(const ObligationModule &Module) { - return countModuleNodes(Module); + llvm::DenseSet Seen; + std::vector Work; + auto add = [&](const LogicExpr *Root) { + if (Root && Seen.insert(Root).second) + Work.push_back(Root); + }; + add(Module.CorrectnessGoal.get()); + add(Module.CounterexampleQuery.get()); + for (const Obligation &Item : Module.Obligations) { + add(Item.Goal.get()); + add(Item.CounterexampleQuery.get()); + } + for (const auto &[Identity, Function] : Module.LogicFunctions) { + (void)Identity; + add(Function.StepDefinition.get()); + for (const auto &Definition : Function.DefinitionLevels) + add(Definition.get()); + } + while (!Work.empty()) { + const LogicExpr *Node = Work.back(); + Work.pop_back(); + for (const auto &Child : Node->Children) + add(Child.get()); + } + return Seen.size(); +} + +uint64_t obligationModuleTreeNodesUpTo(const ObligationModule &Module, + uint64_t Limit) { + uint64_t Tree = logicTreeNodesUpTo(Module.CounterexampleQuery.get(), Limit); + for (const auto &[Identity, Function] : Module.LogicFunctions) { + (void)Identity; + if (Tree > Limit) + break; + Tree += logicTreeNodesUpTo(Function.StepDefinition.get(), Limit); + for (const auto &Definition : Function.DefinitionLevels) + Tree += logicTreeNodesUpTo(Definition.get(), Limit); + } + return Tree; +} + +uint64_t logicTreeNodesUpTo(const LogicExpr *Expr, uint64_t Limit) { + uint64_t Count = 0; + std::vector Work; + if (Expr) + Work.push_back(Expr); + while (!Work.empty() && Count <= Limit) { + const LogicExpr *Node = Work.back(); + Work.pop_back(); + ++Count; + for (const auto &Child : Node->Children) + Work.push_back(Child.get()); + } + return Count; +} + +uint64_t logicDistinctNodes(llvm::ArrayRef Roots) { + llvm::DenseSet Seen; + std::vector Work; + for (const LogicExpr *Root : Roots) + if (Root && Seen.insert(Root).second) + Work.push_back(Root); + while (!Work.empty()) { + const LogicExpr *Node = Work.back(); + Work.pop_back(); + for (const auto &Child : Node->Children) + if (Seen.insert(Child.get()).second) + Work.push_back(Child.get()); + } + return Seen.size(); } llvm::Expected diff --git a/clang/lib/Verify/Backend/ObligationSimplify.h b/clang/lib/Verify/Backend/ObligationSimplify.h index 369da52e85..d71a8d2518 100644 --- a/clang/lib/Verify/Backend/ObligationSimplify.h +++ b/clang/lib/Verify/Backend/ObligationSimplify.h @@ -18,9 +18,15 @@ struct ObligationSimplificationStats { uint64_t FunctionsRemoved = 0; }; -/// Count canonical expression nodes across goals, queries, and reachable -/// logical declarations. Diagnostic-only metadata is excluded. +/// The distinct expression nodes of the goals, queries, and logical +/// declarations, a node shared by several terms counted once: what the module +/// takes in memory. Diagnostic-only metadata is excluded. uint64_t obligationModuleNodeCount(const ObligationModule &Module); +/// The nodes of the module's complete query and logical definitions as +/// trees, as an SMT-LIB script or an archive record states them; once past +/// \p Limit, any count above it. +uint64_t obligationModuleTreeNodesUpTo(const ObligationModule &Module, + uint64_t Limit); /// Apply conservative, semantics-preserving canonical rewrites and remove /// logical declarations unreachable from any proof obligation. The returned From 8af00a2717c0506fa070ddaccf970a6cda0f4872 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:14 +0530 Subject: [PATCH 38/52] verify: Build the goals in a node budget from the lowered terms instead of predicting their size as trees. --- clang/lib/Verify/Backend/Obligation.cpp | 60 +++++++++++-------------- 1 file changed, 27 insertions(+), 33 deletions(-) diff --git a/clang/lib/Verify/Backend/Obligation.cpp b/clang/lib/Verify/Backend/Obligation.cpp index 2fb88ff26b..82333336ad 100644 --- a/clang/lib/Verify/Backend/Obligation.cpp +++ b/clang/lib/Verify/Backend/Obligation.cpp @@ -2262,36 +2262,23 @@ class ObligationBuilder { return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", ConstructionError.c_str()); - // The goals' size is known before any is built: each is its condition - // under a negated copy of every assumption before it (a Not and an Or - // each), each query is its goal negated, and the complete goal joins the - // goals by And, with its query. - uint64_t Prefix = 0, Goals = 0, GoalCount = 0; - auto assumed = [&](const VCExpr *Assumption) { - Prefix = - llvm::SaturatingAdd(Prefix, logicNodeCount(Assumption), uint64_t(2)); - }; - auto goal = [&](const VCExpr *Condition) { - Goals = llvm::SaturatingAdd(Goals, Prefix, logicNodeCount(Condition)); - ++GoalCount; - }; + // Each goal is its condition under every assumption before it, sharing + // their terms: it adds a negation, a disjunction, and a copy of the root + // for each assumption. A function with many checks and assumptions still + // has quadratically many such nodes, so the goals are built in a budget + // and stop once they pass the limit. + std::vector Built; for (const auto &Entry : EntryAssumes) - assumed(Entry.get()); - for (const LoweredStmt &Stmt : Stmts) { - if (Stmt.Kind == PassiveStmt::Assume) - assumed(Stmt.Cond.get()); - else - goal(Stmt.Cond.get()); - } + Built.push_back(Entry.get()); + for (const LoweredStmt &Stmt : Stmts) + Built.push_back(Stmt.Cond.get()); for (const auto &Exit : ExitAsserts) - goal(std::get<1>(Exit).get()); - const uint64_t GoalNodes = - GoalCount == 0 - ? 3 - : llvm::SaturatingAdd(llvm::SaturatingMultiply(Goals, uint64_t(4)), - 3 * GoalCount - 1); - if (MaxNodes != 0 && GoalNodes > MaxNodes) - return ObligationSizeError::obligations(GoalNodes, MaxNodes); + Built.push_back(std::get<1>(Exit).get()); + const uint64_t Lowered = MaxNodes ? logicDistinctNodes(Built) : 0; + std::optional Goals; + Goals.emplace(); + auto size = [&] { return Lowered + Goals->built(); }; + auto oversize = [&] { return MaxNodes != 0 && size() > MaxNodes; }; // Each assumption with where it comes from, which names its hypothesis. std::vector> Assumptions; @@ -2346,19 +2333,26 @@ class ObligationBuilder { } appendObligation(Stmt.ProofKind, Stmt.Cond.get(), Stmt.TraceEventCount, Stmt.Note); + if (oversize()) + return ObligationSizeError::obligations(size(), MaxNodes); } - for (const auto &[Kind, Exit, Note] : ExitAsserts) + for (const auto &[Kind, Exit, Note] : ExitAsserts) { appendObligation(Kind, Exit.get(), M.TraceEvents.size(), Note); + if (oversize()) + return ObligationSizeError::obligations(size(), MaxNodes); + } M.CorrectnessGoal = buildCompleteGoal(M.Obligations); M.CounterexampleQuery = vcNot(cloneLogicExpr(M.CorrectnessGoal.get())); - assert(GoalNodes == obligationModuleNodeCount(M) && - "the goals' size was not predicted exactly"); + if (oversize()) + return ObligationSizeError::obligations(size(), MaxNodes); + Goals.reset(); SpecAxiomContext AxiomContext{P.SpecFunctions, P.SpecFuel, P.HiddenSpecs, P.RevealedSpecs}; - if (llvm::Error Error = - materializeLogicFunctions(M, AxiomContext, MaxNodes, GoalNodes)) + if (llvm::Error Error = materializeLogicFunctions( + M, AxiomContext, MaxNodes, + MaxNodes ? obligationModuleNodeCount(M) : 0)) return std::move(Error); auto RequiredFeatures = validateObligationModule(M); From aa31137771e0bdda39eae12f4500766934091bfb Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:15 +0530 Subject: [PATCH 39/52] verify: Count a spec's definitions by their distinct nodes. --- clang/lib/Verify/Backend/SpecAxioms.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang/lib/Verify/Backend/SpecAxioms.cpp b/clang/lib/Verify/Backend/SpecAxioms.cpp index 188dd79b83..b45b089977 100644 --- a/clang/lib/Verify/Backend/SpecAxioms.cpp +++ b/clang/lib/Verify/Backend/SpecAxioms.cpp @@ -160,7 +160,7 @@ llvm::Error verify::materializeLogicFunctions(ObligationModule &Module, // Its definitions join the module's nodes once all are lowered. uint64_t Own = 0; auto count = [&](const LogicExpr *Definition) -> llvm::Error { - Own = llvm::SaturatingAdd(Own, logicNodeCount(Definition)); + Own = llvm::SaturatingAdd(Own, logicDistinctNodes({Definition})); const uint64_t Total = llvm::SaturatingAdd(Nodes, Own); if (MaxNodes != 0 && Total > MaxNodes) return llvm::make_error( From 954fd46cb8dd6e8703061c4a56dee9e76681f6c4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:15 +0530 Subject: [PATCH 40/52] verify: Refuse a cvc5 script that would state more nodes than the limit. --- clang/lib/Verify/Backend/CVC5Backend.cpp | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/clang/lib/Verify/Backend/CVC5Backend.cpp b/clang/lib/Verify/Backend/CVC5Backend.cpp index 60f9581960..241bee81ca 100644 --- a/clang/lib/Verify/Backend/CVC5Backend.cpp +++ b/clang/lib/Verify/Backend/CVC5Backend.cpp @@ -1509,7 +1509,22 @@ static VerifyResult querySizeLimitResult(const ObligationModule &Module, llvm::StringRef BackendName) { if (auto Limited = moduleSizeLimit(Module, MaxQueryNodes, BackendName)) return std::move(*Limited); - return VerifyResult(); + if (MaxQueryNodes == 0) + return VerifyResult(); + // A script states each term in full, a subterm that several goals share at + // each of its places, so it is as large as the module's terms as trees. + if (obligationModuleTreeNodesUpTo(Module, MaxQueryNodes) <= MaxQueryNodes) + return VerifyResult(); + VerifyResult Result; + Result.Status = VerifyStatus::Unresolved; + Result.Reason = VerifyReason::QuerySizeLimit; + Result.Message = "its SMT-LIB script would state more than " + + std::to_string(MaxQueryNodes) + + " expression nodes, the limit (--max-query-nodes): a " + "script states a subterm that goals share at each of its " + "places"; + Result.BackendName = BackendName.str(); + return Result; } static std::optional From 75596cd7782a0ac4cf4180906a63e940cf45c2ea Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:16 +0530 Subject: [PATCH 41/52] verify: Refuse an archive record that would state more nodes than the limit. --- clang/lib/Verify/Driver/Verifier.cpp | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index d291a94d82..2f49f92cfe 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -2832,6 +2832,16 @@ class Verifier { llvm::Expected archiveRecord(const ObligationModule &Module) { if (!Opts.ObligationOut) return std::string(); + // A record states each term in full, a subterm that goals share at each + // of its places. + if (Opts.MaxQueryNodes != 0 && + obligationModuleTreeNodesUpTo(Module, Opts.MaxQueryNodes) > + Opts.MaxQueryNodes) + return llvm::createStringError( + llvm::inconvertibleErrorCode(), + "its record would state more than %llu expression nodes, the limit " + "(--max-query-nodes)", + static_cast(Opts.MaxQueryNodes)); std::string Serialized = serializeObligationModule(Module); auto RoundTrip = deserializeObligationModules(Serialized); From 57d81606de421bbd777064d92350fab64ca730bf Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:16 +0530 Subject: [PATCH 42/52] verify: Lower the default node limit to four million distinct nodes. --- clang/lib/Verify/Driver/Verifier.h | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h index 1560d57abd..a4c99c8d1c 100644 --- a/clang/lib/Verify/Driver/Verifier.h +++ b/clang/lib/Verify/Driver/Verifier.h @@ -20,11 +20,11 @@ inline constexpr unsigned DefaultCollectionTimeoutMs = /// and their retries, so it legitimately takes several query timeouts. inline constexpr unsigned DefaultFunctionTimeoutMs = 10 * DefaultSolverTimeoutMs; -/// The expression nodes the proof obligations of one function may take, as -/// built: building a module takes up to about 450 bytes a node at once, and -/// the largest of the test suite (the ULEB128 case study's) has 22.6 -/// million. -inline constexpr uint64_t DefaultMaxQueryNodes = 32000000; +/// The distinct expression nodes built for one function's proof obligations: +/// a node takes about 600 bytes, and Z3's encoding of it about five times +/// that, and the largest function of the test suite (safe_fib.cpp's +/// iterative_fibonacci) has 375,000. +inline constexpr uint64_t DefaultMaxQueryNodes = 4000000; /// The megabytes Z3's queries may allocate together, and each cvc5 process. inline constexpr uint64_t DefaultMemoryLimitMB = 8192; From 34faee66a78c218f8ea35dde354498949e8f8bb6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:17 +0530 Subject: [PATCH 43/52] verify: Give --max-query-nodes' new default in its help. --- clang/tools/cpp-verify/Main.cpp | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp index 7dd1c08a0f..e0d2f5cfaa 100644 --- a/clang/tools/cpp-verify/Main.cpp +++ b/clang/tools/cpp-verify/Main.cpp @@ -191,10 +191,13 @@ static unsigned jobs() { return 0; } +static const std::string MaxQueryNodesDescription = + "Maximum expression nodes of one function's proof obligations, checked " + "as they are built (default " + + std::to_string(verify::DefaultMaxQueryNodes) + "; 0 = no limit)"; + static cl::opt MaxQueryNodes( - "max-query-nodes", - cl::desc("Maximum expression nodes of one function's proof obligations, " - "checked as they are built (default 32000000; 0 = no limit)"), + "max-query-nodes", cl::desc(MaxQueryNodesDescription), cl::init(verify::DefaultMaxQueryNodes), cl::cat(CppVerifyCategory)); static cl::opt MemoryLimit( From 83982273336968f4dd356a4fc1d0d290f0ed9075 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:17 +0530 Subject: [PATCH 44/52] test: Expect the sizes of shared obligations, and refused archive records, in obligation_size_limit.cpp. --- .../Verify/suite/obligation_size_limit.cpp | 42 ++++++++++++------- 1 file changed, 27 insertions(+), 15 deletions(-) diff --git a/clang/test/Verify/suite/obligation_size_limit.cpp b/clang/test/Verify/suite/obligation_size_limit.cpp index d35f245c21..c3433e67df 100644 --- a/clang/test/Verify/suite/obligation_size_limit.cpp +++ b/clang/test/Verify/suite/obligation_size_limit.cpp @@ -1,30 +1,40 @@ -// RUN: not %cpp-verify --jobs=1 --max-query-nodes=3000 %s -- 2>&1 \ +// RUN: not %cpp-verify --jobs=1 --max-query-nodes=500 %s -- 2>&1 \ // RUN: | FileCheck %s --check-prefix=LIMIT -// RUN: not %cpp-verify --jobs=1 --max-query-nodes=3000 \ +// RUN: not %cpp-verify --jobs=1 --max-query-nodes=500 \ // RUN: --diagnostics-format=json %s -- 2>&1 | FileCheck %s --check-prefix=JSON -// RUN: not %cpp-verify --lower-only --max-query-nodes=3000 %s -- 2>&1 \ +// RUN: not %cpp-verify --lower-only --max-query-nodes=500 %s -- 2>&1 \ // RUN: | FileCheck %s --check-prefix=LOWER +// RUN: %cpp-verify --help | FileCheck %s --check-prefix=HELP +// HELP: --max-query-nodes= {{.*}}(default 4000000; 0 = no limit) // // The size is exact: at it the obligations are built, one below they are not. -// RUN: %cpp-verify --jobs=1 --max-query-nodes=24417 %s -- 2>&1 \ +// RUN: %cpp-verify --jobs=1 --max-query-nodes=1939 %s -- 2>&1 \ // RUN: | FileCheck %s --check-prefix=AT -// RUN: not %cpp-verify --jobs=1 --max-query-nodes=24416 %s -- 2>&1 \ +// RUN: not %cpp-verify --jobs=1 --max-query-nodes=1938 %s -- 2>&1 \ // RUN: | FileCheck %s --check-prefix=BELOW // +// Built, the obligations share their terms, so at 3000 nodes they are built +// and proved; an archive record states each term in full, which takes more. +// RUN: %cpp-verify --jobs=1 --max-query-nodes=3000 %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=SHARED +// RUN: not %cpp-verify --jobs=1 --max-query-nodes=3000 --obligation-out=%t.cpv \ +// RUN: %s -- 2>&1 | FileCheck %s --check-prefix=ARCHIVE +// // A spec unfolded as deep as its fuel stops at the limit: at fuel 40, fibo's // unfolding would have about 2^40 copies of its body. // RUN: not %cpp-verify --jobs=1 --max-query-nodes=200000 %s -- -DFUEL 2>&1 \ // RUN: | FileCheck %s --check-prefix=FUEL // // The definitions of the specs a module applies count with its obligations: -// 26167 nodes here, fib's definitions at fuel 4 included. -// RUN: %cpp-verify --jobs=1 --max-query-nodes=26167 %s -- -DDEFINITIONS 2>&1 \ +// 2637 nodes here, fib's definitions at fuel 4 included. +// RUN: %cpp-verify --jobs=1 --max-query-nodes=2637 %s -- -DDEFINITIONS 2>&1 \ // RUN: | FileCheck %s --check-prefix=DEFINITIONS-AT -// RUN: not %cpp-verify --jobs=1 --max-query-nodes=26166 %s -- -DDEFINITIONS \ +// RUN: not %cpp-verify --jobs=1 --max-query-nodes=2636 %s -- -DDEFINITIONS \ // RUN: 2>&1 | FileCheck %s --check-prefix=DEFINITIONS -// Each check repeats every assumption before it, so the obligations of a -// function grow with its checks times the statements before them. +// Each check restates every assumption before it, sharing its terms, so the +// obligations of a function grow with its checks times the statements before +// them. int steps(int x) cppverify::pre(0 <= x && x <= 100) cppverify::post(cppverify::result == x + 8) @@ -47,11 +57,13 @@ int steps(int x) cppverify::check(y == x + 8); return y; } -// LIMIT: obligation_size_limit.cpp:[[@LINE-22]]:5: Unresolved: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 24417 expression nodes, more than the limit of 3000 (--max-query-nodes): each check repeats every assumption before it, so split the function or raise the limit) -// JSON: {"backend":"z3","function":"steps","message":"steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 24417 expression nodes, more than the limit of 3000 (--max-query-nodes): each check repeats every assumption before it, so split the function or raise the limit)","reason":"query.size-limit","schema":"cppverify.diagnostic/1","severity":"error","source":{"column":5,"end_column":5,"end_line":[[@LINE-23]],"file":"{{.*}}obligation_size_limit.cpp","line":[[@LINE-23]]},"status":"unresolved"} -// LOWER: obligation_size_limit.cpp:[[@LINE-24]]:5: error: Z3 lowering failed: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 24417 expression nodes, more than the limit of 3000 +// LIMIT: obligation_size_limit.cpp:[[@LINE-22]]:5: Unresolved: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 747 expression nodes, more than the limit of 500 (--max-query-nodes): each check repeats every assumption before it, so split the function or raise the limit) +// JSON: {"backend":"z3","function":"steps","message":"steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 747 expression nodes, more than the limit of 500 (--max-query-nodes): each check repeats every assumption before it, so split the function or raise the limit)","reason":"query.size-limit","schema":"cppverify.diagnostic/1","severity":"error","source":{"column":5,"end_column":5,"end_line":[[@LINE-23]],"file":"{{.*}}obligation_size_limit.cpp","line":[[@LINE-23]]},"status":"unresolved"} +// LOWER: obligation_size_limit.cpp:[[@LINE-24]]:5: error: Z3 lowering failed: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 747 expression nodes, more than the limit of 500 // AT: Verified: steps [backend=z3] -// BELOW: Unresolved: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 24417 expression nodes, more than the limit of 24416 (--max-query-nodes) +// SHARED: Verified: steps [backend=z3] +// ARCHIVE: error: cannot serialize obligation: steps (its record would state more than 3000 expression nodes, the limit (--max-query-nodes)) +// BELOW: Unresolved: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 1939 expression nodes, more than the limit of 1938 (--max-query-nodes) // Its verdict relies on the contract of steps, which nothing establishes. int caller(int x) @@ -130,4 +142,4 @@ int defined(int x) } #endif // DEFINITIONS-AT: Verified: defined [backend=z3] -// DEFINITIONS: Unresolved: defined [backend=z3] [reason=query.size-limit] (the proof obligations with the definitions of the specs they apply would take at least 26167 expression nodes, more than the limit of 26166 (--max-query-nodes): lower the fuel cppverify::reveal_with_fuel gives, split the function, or raise the limit) +// DEFINITIONS: Unresolved: defined [backend=z3] [reason=query.size-limit] (the proof obligations with the definitions of the specs they apply would take at least 2637 expression nodes, more than the limit of 2636 (--max-query-nodes): lower the fuel cppverify::reveal_with_fuel gives, split the function, or raise the limit) From 20ed93147b53d35f04e8cf413c5a0cbf59c36473 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:18 +0530 Subject: [PATCH 45/52] test: Stop 1200 checks at 200000 nodes within 3 GB. --- clang/test/Verify/suite/memory_bounded.test | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/clang/test/Verify/suite/memory_bounded.test b/clang/test/Verify/suite/memory_bounded.test index a7bf787ca8..5ce3d43db0 100644 --- a/clang/test/Verify/suite/memory_bounded.test +++ b/clang/test/Verify/suite/memory_bounded.test @@ -4,15 +4,15 @@ # Within a 3 GB address space, functions whose obligations, or whose specs # unfolded as deep as their fuel, would take far more end with a verdict # instead of failing an allocation: what is built is counted as it is built -# (or before, for the obligations) and stops at --max-query-nodes. +# and stops at --max-query-nodes. 1200 checks would take about 30 GB. # RUN: rm -rf %t && mkdir -p %t -# RUN: %python %S/Inputs/many_checks.py 400 %t/many.cpp +# RUN: %python %S/Inputs/many_checks.py 1200 %t/many.cpp # RUN: ulimit -v 3000000 -# RUN: not %cpp-verify --jobs=1 --max-query-nodes=2000000 %t/many.cpp -- 2>&1 \ +# RUN: not %cpp-verify --jobs=1 --max-query-nodes=200000 %t/many.cpp -- 2>&1 \ # RUN: | FileCheck %s --check-prefix=MANY # RUN: not %cpp-verify --jobs=1 --max-query-nodes=2000000 \ # RUN: %S/obligation_size_limit.cpp -- -DFUEL 2>&1 | FileCheck %s --check-prefix=FUEL -MANY: Unresolved: many_checks [backend=z3] [reason=query.size-limit] (the proof obligations would take at least {{[0-9]+}} expression nodes, more than the limit of 2000000 (--max-query-nodes) +MANY: Unresolved: many_checks [backend=z3] [reason=query.size-limit] (the proof obligations would take at least {{[0-9]+}} expression nodes, more than the limit of 200000 (--max-query-nodes) FUEL: Verified: small [backend=z3] FUEL: Unresolved: unfolds [backend=z3] [reason=query.size-limit] (the facts about the specs it applies From 6bb02171d61388d61a30b05cc10b227d2e7e2c89 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:18 +0530 Subject: [PATCH 46/52] test: A cvc5 script is refused when it would state more nodes than the limit. --- clang/test/Verify/suite/cvc5_script_size.test | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 clang/test/Verify/suite/cvc5_script_size.test diff --git a/clang/test/Verify/suite/cvc5_script_size.test b/clang/test/Verify/suite/cvc5_script_size.test new file mode 100644 index 0000000000..1492b3a8de --- /dev/null +++ b/clang/test/Verify/suite/cvc5_script_size.test @@ -0,0 +1,8 @@ +# REQUIRES: cvc5 +# An SMT-LIB script states each term in full, a subterm that goals share at +# each of its places, so cvc5 refuses at 3000 nodes a module that Z3, which +# shares terms as the verifier does, proves (obligation_size_limit.cpp). +# RUN: not %cpp-verify --jobs=1 --backend=cvc5 --max-query-nodes=3000 \ +# RUN: %S/obligation_size_limit.cpp -- 2>&1 | FileCheck %s +# CHECK: Unresolved: steps [backend=cvc5] [reason=query.size-limit] (its SMT-LIB script would state more than 3000 expression nodes, the limit (--max-query-nodes): a script states a subterm that goals share at each of its places) +# CHECK: Verified: small [backend=cvc5] From 8979fb6e18e66c20bf54f2892bf43e304bd39802 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:18 +0530 Subject: [PATCH 47/52] docs: Describe the node limit as distinct nodes built, and the scripts and records checked as trees. --- website/source/language/tooling.rst | 63 ++++++++++++++++++----------- 1 file changed, 40 insertions(+), 23 deletions(-) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index e789ef2c32..e851eb11d8 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -464,10 +464,12 @@ Backends Not accepted with ``--backend=lean``, which runs no solver. * - ``--max-query-nodes=N`` - The expression nodes the verifier may build for one function (default - 32000000; ``0`` disables): its proof obligations, counted before they - are built, and the facts about the specs they apply, counted as they - are built. A function over it is ``Unresolved`` with reason - ``query.size-limit``, under every backend. See `Memory limits`_. + 4000000; ``0`` disables): its proof obligations and the facts about the + specs they apply, counted as they are built, a shared node once. A + function over it is ``Unresolved`` with reason ``query.size-limit``, + under every backend; cvc5's scripts and archive records, which state + shared terms in full, are checked against it too. See + `Memory limits`_. * - ``--memory-limit=MB`` - The megabytes the solvers may use (default 8192; ``0`` disables): Z3's queries together, and each cvc5 process. A query that reaches it is @@ -608,10 +610,10 @@ Memory limits Two limits bound the memory verification takes: - ``--max-query-nodes`` bounds what the verifier builds for **one** function - (default 32,000,000 expression nodes): its proof obligations, and the facts - about the specs they apply. The obligations are counted before they are - built, so a function over the limit is refused before it takes the memory; - the facts are counted as they are built and stop at the limit. + (default 4,000,000 expression nodes): its proof obligations, and the facts + about the specs they apply. Both are counted as they are built and stop at + the limit, so a function over it ends before it takes the memory. A node + that several terms share is counted once, as it takes memory once. - ``--memory-limit`` bounds the solvers (default 8192 MB): Z3's queries together, since Z3 runs inside cpp-verify, and each cvc5 process on its own. @@ -622,12 +624,13 @@ counterexample, and every function whose proof relies on its contract is The proof obligations of a function grow faster than its code. Each check is proved from everything before it (the preconditions, the statements, and the -earlier checks), and its obligation repeats all of it, so a function whose -checks follow many statements takes about their product. With two, four, and -eight checks like the four below, the obligations take 3,405, 8,505, and -25,425 nodes. With a limit of 2,000: +earlier checks): its obligation states each as an assumption, sharing its +terms with the other obligations, so a function whose checks follow many +statements takes about their number times its checks' (not times their +sizes). With two, four, and eight checks like the four below, the +obligations take 259, 523, and 1,375 nodes. With a limit of 400: -.. cppverify-example: flags --max-query-nodes=2000 +.. cppverify-example: flags --max-query-nodes=400 .. cppverify-example: unresolved steps .. code-block:: cpp @@ -649,19 +652,33 @@ eight checks like the four below, the obligations take 3,405, 8,505, and .. code-block:: text - steps.cpp:1:5: Unresolved: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 8505 expression nodes, more than the limit of 2000 (--max-query-nodes): each check repeats every assumption before it, so split the function or raise the limit) + steps.cpp:1:5: Unresolved: steps [backend=z3] [reason=query.size-limit] (the proof obligations would take at least 427 expression nodes, more than the limit of 400 (--max-query-nodes): each check repeats every assumption before it, so split the function or raise the limit) -The count is exact: with ``--max-query-nodes=8505`` the function verifies. -Under ``--lower-only`` the same is an error, ``Z3 lowering failed: steps``, -since no obligations were built. A function split into functions with +The count is where building stopped, so the function needs at least that +many. Its obligations take 523 nodes, and the checks that a proof is not +vacuous build programs of their own, the largest with 901: with +``--max-query-nodes=901`` the function verifies. Under ``--lower-only`` the +same is an error, ``Z3 lowering failed: steps``, since no obligations were +built. A function split into functions with contracts keeps each one's obligations small: a call repeats the callee's contract, not its body. -The default admits the largest function of the test suite, in the ULEB128 -case study (:doc:`../case-studies/llvm-uleb128`), whose obligations have 22.6 -million nodes. While obligations are built and checked, a node takes about -400 bytes, so the default lets one function take up to about 13 GB; with more -than one job, each job builds the obligations of its own function at once. +The default admits the largest function of the test suite, +``iterative_fibonacci`` in ``safe_fib.cpp`` (375,000 nodes, with the +definitions of the specs it applies), ten times over; the ULEB128 case study +(:doc:`../case-studies/llvm-uleb128`) takes under 200,000 a function. A node +takes about 600 bytes, and Z3's encoding of it about five times that, so the +default lets one function take up to about 12 GB; with more than one job, +each job builds the obligations of its own function at once. + +An SMT-LIB script, which the cvc5 backend writes, and an archive record +(``--obligation-out``) state each term in full: a subterm that several +obligations share is written at each of its places, so they are larger than +what is built. Each is checked against the same limit, as the nodes it +would state: a module whose script would be larger is ``Unresolved`` with +``query.size-limit`` under cvc5 (``its SMT-LIB script would state more than +N expression nodes``), and one whose record would be larger is an error with +``--obligation-out``. The facts about the specs a function applies include each spec's definition, unfolded as deep as its fuel. A spec that applies itself twice doubles with @@ -753,7 +770,7 @@ Choosing the limits: builds one function's obligations at once, then the two limits. - Continuous integration with a memory allowance: give ``--memory-limit`` the solvers' share, and ``--max-query-nodes`` the rest divided by - ``--jobs`` and by 400 bytes. + ``--jobs`` and by 3,000 bytes. Parallel solving and proof caching ---------------------------------- From 541d0e847c51de7f14350da24d8e7c412a54aee6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:19 +0530 Subject: [PATCH 48/52] docs: Give --max-query-nodes' new default in the book. --- website/source/book/part-ii/ch15-toolchain-and-flags.rst | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/website/source/book/part-ii/ch15-toolchain-and-flags.rst b/website/source/book/part-ii/ch15-toolchain-and-flags.rst index fce6a27042..ec39e37805 100644 --- a/website/source/book/part-ii/ch15-toolchain-and-flags.rst +++ b/website/source/book/part-ii/ch15-toolchain-and-flags.rst @@ -68,7 +68,8 @@ Other flags for Z3 and cvc5 (``0`` disables) - ``cpp-verify --max-query-nodes=N`` — the expression nodes the verifier may build for one function: its proof obligations, and the facts about the - specs they apply (default 32000000; ``0`` disables; ``query.size-limit``) + specs they apply, a shared node once (default 4000000; ``0`` disables; + ``query.size-limit``) - ``cpp-verify --memory-limit=MB`` — the megabytes the solvers may use, Z3's queries together and each cvc5 process (default 8192; ``0`` disables; ``solver.memory-limit``) From 36070bc20149e4c634cf96a97565923c0b7c8edc Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:19 +0530 Subject: [PATCH 49/52] docs: Give the node limit's new default in the limitations. --- website/source/language/limitations.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 2c47233033..8bd94ec764 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -174,8 +174,8 @@ C++ feature boundaries recursion through a function that allocates or frees storage, and general link-time summaries. A function whose proof obligations would take more than - ``--max-query-nodes`` expression nodes (32 million by default) is - ``Unresolved`` with reason ``query.size-limit``: each check repeats + ``--max-query-nodes`` expression nodes (4 million by default) is + ``Unresolved`` with reason ``query.size-limit``: each check restates every assumption before it, so a long function with many checks grows fastest. See the memory limits of :doc:`tooling`. * - Storage From cd5aba71de021b5367e1b1e991b88f949052078d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:20 +0530 Subject: [PATCH 50/52] docs: Note the node limit's new default and meaning in the 0.2.0 release notes. --- website/source/release-notes.rst | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 04aec6a4cf..9ea03edccf 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -500,9 +500,11 @@ report something unrelated. The query now ends ``Unresolved`` with reason proof obligations, which repeat every assumption before each check, came to hundreds of millions of nodes, or ``cppverify::reveal_with_fuel(fibo, 24)``, took tens of gigabytes until the system stopped the run. ``--max-query-nodes`` -now has a default, 32 million expression nodes, and bounds what is built for -one function before it is built; a function over it is ``Unresolved`` with -reason ``query.size-limit``, which names what was too large. The new +now has a default, 4 million expression nodes, and bounds what is built for +one function as it is built, a node shared by several terms once; a function +over it is ``Unresolved`` with reason ``query.size-limit``, which names what +was too large. cvc5's scripts and archive records, which state shared terms +in full, are checked against it too. The new ``--memory-limit`` (default 8192 MB) bounds Z3's queries together and each cvc5 process; a query that reaches it is ``Unresolved`` with reason ``solver.memory-limit`` (:doc:`language/tooling`). From f7b480e94288fc1b0d04a705d5ec0a33cec9b02d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:20 +0530 Subject: [PATCH 51/52] docs: Design the node limit as distinct nodes built. --- docs/DESIGN.md | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index e3383bc663..11a52662f3 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -2239,13 +2239,15 @@ canonical source order, so concurrency cannot choose which failure is public. of one function together, in wall-clock time; once it is spent no further query starts and the function is `Unresolved` (`solver.timeout`). AST/VCR lowering and Lean emission remain serial. `--solver-rlimit` adds a deterministic per-query Z3 budget. -`--max-query-nodes` (default 32,000,000) bounds the expression nodes built -for one function: the size of its obligations, each of which repeats every -assumption before it, is known exactly before they are built, so a function -over the limit is refused before it takes the memory, and the facts about -the specs it applies (definitions unfolded as deep as their fuel, -postconditions at each application) are counted as they are built and stop -at the limit. `--memory-limit` (default 8192 MB) bounds Z3's queries +`--max-query-nodes` (default 4,000,000) bounds the distinct expression +nodes built for one function, which is what it takes in memory: its +obligations, each of which restates every assumption before it and shares +its terms, and the facts about the specs it applies (definitions unfolded as +deep as their fuel, postconditions at each application) are counted as they +are built and stop at the limit, so a function over it ends before it takes +the memory. What states each term in full, an SMT-LIB script for cvc5 and an +archive record, is checked against the same limit as the tree it would +state. `--memory-limit` (default 8192 MB) bounds Z3's queries together, which a check's watchdog stops once Z3's allocations pass it, and each cvc5 process, whose allocations past it fail. Neither limit can become success: a function over the first is `Unresolved` with `query.size-limit`, From 35326f98c71ff15f5bf656319a666355167d92e7 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Tue, 27 Oct 2026 20:09:21 +0530 Subject: [PATCH 52/52] docs: Describe how a module's size is counted as it is built. --- docs/ARCHITECTURE.md | 44 +++++++++++++++++++++++++++----------------- 1 file changed, 27 insertions(+), 17 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 5c4a882c3a..5850113c3a 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -928,24 +928,34 @@ traversal that does not memoize (validation, hashing, serialization) still takes time quadratic in a function's length; hash-consing the terms and memoizing those traversals would make it linear. -**Size.** Each obligation's goal is its condition under a negated copy of -every assumption before it, so a module grows with its obligations times -the assumptions before them. Its node count, as `obligationModuleNodeCount` -counts it, is computed from the lowered statements before any goal is built -(four times the goals' nodes, for the goals, their queries, the complete -goal, and its query, plus three per obligation less one; an assertion -checks the count against the built module); over `--max-query-nodes` the -build returns `ObligationSizeError`. Constructions whose size the program -does not bound are counted as they go: `NodeBudget` (`IR/NodeBudget.h`) -counts the `VExpr` and `LogicExpr` nodes built on its thread against the -limit the driver sets for the function, and the spec inliner unfolds -nothing more once it is spent. The definitions `SpecAxioms` materializes, -each spec unfolded as deep as its fuel, are counted level by level into the -module's count; the facts the passivizer adds at each spec application are -counted in a budget, and a spent one leaves `PassiveProgram::TooLarge`, which -makes the build an `ObligationSizeError`; so does a spent budget while specs -are inlined for BMC. The driver reports the error as the function's verdict, +**Size.** Each obligation's goal is its condition under every assumption +before it, sharing their terms (above): a goal adds, for each assumption, a +negation, a disjunction, and a copy of the assumption's root, so a module's +distinct nodes grow with its obligations times the assumptions before them, +not times their sizes. `obligationModuleNodeCount` counts the distinct nodes, +a shared one once, which is what the module takes in memory. `NodeBudget` +(`IR/NodeBudget.h`) counts the `VExpr` and `LogicExpr` nodes built on its +thread against the limit the driver sets for the function +(`--max-query-nodes`): the goals are built in one, starting from the distinct +nodes of the lowered statements, and stop with `ObligationSizeError` once +they pass the limit; the spec inliner unfolds nothing more once its budget is +spent. The definitions `SpecAxioms` materializes, each spec unfolded as deep +as its fuel, are counted, each by its distinct nodes, from the module's +count; the facts the passivizer adds at each spec application are counted in +a budget, and a spent one leaves `PassiveProgram::TooLarge`, which makes the +build an `ObligationSizeError`; so does a spent budget while specs are +inlined for BMC. The driver reports the error as the function's verdict, `Unresolved` with `query.size-limit`, and never uses the partial result. +What states each term in full is larger than what is built: the cvc5 +adapter's SMT-LIB script and an archive record write a shared subterm at +each of its places. Each counts the module's complete query and definitions +as trees, stopping once past the limit (`obligationModuleTreeNodesUpTo`): +over it, cvc5's verdict is `Unresolved` with `query.size-limit`, and the +record is an error. Z3 and the Lean printer share terms (Z3 by hash-consing, +Lean by naming a shared subterm with a `let`), so the distinct count bounds +them. Before 0.2 the size was predicted, as trees, before any goal was +built; with shared terms that counted far more than a module takes (a +function of 400 checks: 45 million predicted, under 2 million built). Every source-built or replayed module then passes through one fail-closed canonicalization step before hashing or backend dispatch. The pass folds only