From 5f55b5a492bfdccd7c149a301eb2fdaf834a6432 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:45 +0530 Subject: [PATCH 01/80] verify: Let a certified counterexample carry the values of its goal's variables. --- clang/lib/Verify/Backend/VerifyBackend.h | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/clang/lib/Verify/Backend/VerifyBackend.h b/clang/lib/Verify/Backend/VerifyBackend.h index 6e3a71e715..f006f4a5dc 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.h +++ b/clang/lib/Verify/Backend/VerifyBackend.h @@ -128,6 +128,8 @@ struct QuantifierProfileEntry { unsigned MaxGeneration = 0; }; +struct CounterexampleAssignment; + struct VerifyResult { VerifyStatus Status = VerifyStatus::Unresolved; VerifyReason Reason = VerifyReason::None; @@ -138,6 +140,9 @@ struct VerifyResult { std::vector Trace; std::string ObligationId; std::optional ObligationType; + /// For a certified counterexample: the value of every free variable of the + /// goal of the obligation it fails, when the model gives each one. + std::shared_ptr Assignment; SourceLocation Location; ObligationSource Source; uint64_t CacheHits = 0; From 742e6c7a2a8d21fbd24f9a5eb0aff35ec17d3c7e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:45 +0530 Subject: [PATCH 02/80] verify: Declare the assignment of a certified counterexample. --- clang/lib/Verify/Backend/Certify.h | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/clang/lib/Verify/Backend/Certify.h b/clang/lib/Verify/Backend/Certify.h index f9df4c387e..9c8a95c665 100644 --- a/clang/lib/Verify/Backend/Certify.h +++ b/clang/lib/Verify/Backend/Certify.h @@ -232,6 +232,18 @@ std::optional evaluateTerm(const ObligationModule &Module, const CertifyLimits &Limits = {}, std::string *Failure = nullptr); +/// The values a certified counterexample gives the free variables of the goal +/// of the obligation it fails, by name: what a refutation of that goal +/// applies it to. +struct CounterexampleAssignment { + std::map Values; +}; + +/// The assignment \p Model gives the free variables of \p Item's goal, or +/// null when it gives one no value. +std::shared_ptr +counterexampleAssignment(const Obligation &Item, CandidateModel &Model); + /// The source variables of \p Query with the values \p Model gives them, as /// a counterexample shows them; no value where the model gives none. std::vector candidateValues(const ObligationModule &Module, From 288e9a4df53fc49fbce416456e409689c6a7eda1 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:46 +0530 Subject: [PATCH 03/80] verify: Read the assignment of a certified counterexample from its candidate model. --- clang/lib/Verify/Backend/Certify.cpp | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) diff --git a/clang/lib/Verify/Backend/Certify.cpp b/clang/lib/Verify/Backend/Certify.cpp index 55df72c841..9562568603 100644 --- a/clang/lib/Verify/Backend/Certify.cpp +++ b/clang/lib/Verify/Backend/Certify.cpp @@ -4150,6 +4150,22 @@ void sourceVariables(const LogicExpr *Expr, std::set &Bound, } } // namespace +std::shared_ptr +verify::counterexampleAssignment(const Obligation &Item, + CandidateModel &Model) { + std::vector> Variables; + std::set Bound; + sourceVariables(Item.Goal.get(), Bound, Variables); + auto Assignment = std::make_shared(); + for (const auto &[Name, Sort] : Variables) { + std::optional Given = Model.constant(Name, Sort); + if (!Given) + return nullptr; + Assignment->Values.emplace(Name, std::move(*Given)); + } + return Assignment; +} + std::vector verify::candidateValues(const ObligationModule &Module, const LogicExpr &Query, CandidateModel &Model) { From aeb21829f22619d55380f94bacde8f15fc562a6b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:46 +0530 Subject: [PATCH 04/80] verify: Keep the assignment of each counterexample the Z3 adapter certifies. --- clang/lib/Verify/Backend/Z3Encode.cpp | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/clang/lib/Verify/Backend/Z3Encode.cpp b/clang/lib/Verify/Backend/Z3Encode.cpp index d1c13b6fc1..93cc05b0f5 100644 --- a/clang/lib/Verify/Backend/Z3Encode.cpp +++ b/clang/lib/Verify/Backend/Z3Encode.cpp @@ -3322,6 +3322,12 @@ VerifyResult Z3Encoder::decideModule(const ObligationModule &Module, EncodingError = std::move(SavedError); return sourceValue(Evaluated, Expr->Sort); }; + // Completing a model adds the values it chooses to it, and the model + // reported keeps the solver's alone: an assignment reads a copy. + auto assignment = [&](const Obligation &Item) { + Z3CandidateModel Copy(*this, z3::model(Mod, Ctx, z3::model::translate())); + return counterexampleAssignment(Item, Copy); + }; if (IsCompleteQuery && !TraceEventCount) { // The certified model is the completed one; the certifier evaluates // what the solver's evaluator leaves open, such as quantifiers. @@ -3346,9 +3352,18 @@ VerifyResult Z3Encoder::decideModule(const ObligationModule &Module, Out.ObligationType = Item.Kind; Out.Location = Item.Loc; Out.Source = Item.Source; + Out.Assignment = assignment(Item); TraceEventCount = Item.TraceEventCount; break; } + } else { + // A refutation of the goal of the obligation this query is the + // counterexample of applies the goal to the model's values. + for (const Obligation &Item : Module.Obligations) + if (Item.CounterexampleQuery.get() == Query) { + Out.Assignment = assignment(Item); + break; + } } for (const auto &[Name, Sort] : ModelVariables) { auto Metadata = Module.DiagnosticVariables.find(Name); From ce3dc2b408a13cf25880f9d2543ca313925904d0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:47 +0530 Subject: [PATCH 05/80] verify: Declare the Lean refutation of a counterexample. --- clang/lib/Verify/Backend/LeanBackend.h | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/clang/lib/Verify/Backend/LeanBackend.h b/clang/lib/Verify/Backend/LeanBackend.h index 94f82a6edd..c2cc672246 100644 --- a/clang/lib/Verify/Backend/LeanBackend.h +++ b/clang/lib/Verify/Backend/LeanBackend.h @@ -81,6 +81,26 @@ VerifyResult exportLeanScratchPad( const std::set *Selection = nullptr, std::map *Specs = nullptr); +/// A certified counterexample shown in Lean: a module of the project's +/// group directory, Refutations//.lean, that states the goal as +/// the project would and proves `_refuted : ¬ ` at the values. +struct LeanRefutation { + std::string Group; + std::string Goal; + std::string StableId; + std::string Text; +}; + +/// The refutation of Item's goal at Assignment, the values a certified +/// counterexample gives its variables. Specs receives the specs it applies, +/// as a project's export does. None, with Why, when a value has no Lean +/// form. +std::optional +exportLeanRefutation(const ObligationModule &Module, const Obligation &Item, + const CounterexampleAssignment &Assignment, + std::map &Specs, + std::string &Why); + class LeanVerifyBackend : public VerifyBackend { llvm::raw_ostream *Out = nullptr; LeanProjectModules *Modules = nullptr; From 34415e8e42602999dd8ef9e4be553aaa4e12a21c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:47 +0530 Subject: [PATCH 06/80] verify: Export a counterexample as a Lean refutation, and decide bounded integer quantifiers in the prelude. --- clang/lib/Verify/Backend/LeanBackend.cpp | 155 +++++++++++++++++++++++ 1 file changed, 155 insertions(+) diff --git a/clang/lib/Verify/Backend/LeanBackend.cpp b/clang/lib/Verify/Backend/LeanBackend.cpp index 944369ecfd..5ea0ce0786 100644 --- a/clang/lib/Verify/Backend/LeanBackend.cpp +++ b/clang/lib/Verify/Backend/LeanBackend.cpp @@ -1,5 +1,6 @@ //===--- LeanBackend.cpp --------------------------------------------------===// #include "LeanBackend.h" +#include "Certify.h" #include "ObligationSerialization.h" #include "llvm/ADT/STLExtras.h" #include "llvm/ADT/SmallString.h" @@ -1293,6 +1294,32 @@ static std::string leanSpecDefinition(const ObligationModule &Module, return Failed ? "" : Text; } +// A quantifier over a range of integers, as a goal states one, is decided by +// trying each integer of the range, as core Lean decides one over a range of +// naturals. +static constexpr llvm::StringLiteral LeanBoundedQuantifierPrelude = + R"lean(instance cppIntBallDecidable (lo hi : Int) (p : Int → Prop) [DecidablePred p] : + Decidable (∀ x : Int, lo ≤ x ∧ x < hi → p x) := + decidable_of_iff (∀ k : Nat, k < (hi - lo).toNat → p (lo + k)) (by + constructor + · intro h x hx + have := h (x - lo).toNat (by omega) + rwa [show lo + ((x - lo).toNat : Int) = x by omega] at this + · intro h k hk + exact h _ ⟨by omega, by omega⟩) + +instance cppIntBexDecidable (lo hi : Int) (p : Int → Prop) [DecidablePred p] : + Decidable (∃ x : Int, lo ≤ x ∧ x < hi ∧ p x) := + decidable_of_iff (∃ k : Nat, k < (hi - lo).toNat ∧ p (lo + k)) (by + constructor + · rintro ⟨k, hk, hp⟩ + exact ⟨lo + k, by omega, by omega, hp⟩ + · rintro ⟨x, h1, h2, hp⟩ + refine ⟨(x - lo).toNat, by omega, ?_⟩ + rwa [show lo + ((x - lo).toNat : Int) = x by omega]) + +)lean"; + static void emitLeanFunctionDeclarations( const ObligationModule &Module, llvm::raw_ostream &OS, std::set &EmittedFunctions, @@ -1680,6 +1707,7 @@ void verify::emitLeanPrelude(llvm::raw_ostream &OS, bool Project) { OS << " if (x < 0) ≠ (y < 0) then -q else q\n"; OS << "def cppIntRem (x y : Int) : Int :=\n"; OS << " if y = 0 then x else x - cppIntDiv x y * y\n\n"; + OS << LeanBoundedQuantifierPrelude; OS << LeanCollectionPrelude; OS << "/- Proves that an application in a spec's definition lowers its " "measure. -/\n"; @@ -1704,6 +1732,77 @@ void verify::emitLeanPrelude(llvm::raw_ostream &OS, bool Project) { } } +// A piecewise-constant function of the integers as a Lean term: the cell +// of each address, from the run it lies in. +static void printLeanRuns(const HeapValue &Runs, llvm::StringRef Before, + llvm::StringRef After, llvm::raw_ostream &OS) { + OS << "(fun (a : Int) => "; + for (auto It = Runs.Breaks.rbegin(); It != Runs.Breaks.rend(); ++It) + OS << "if a ≥ (" << It->first.toDecimal() << " : Int) then " << Before + << It->second.toDecimal() << After << " else "; + OS << Before << Runs.Default.toDecimal() << After << ")"; +} + +// A model's value as a Lean term of its sort; false when it has none. +static bool printLeanValue(const LogicValue &Value, const LogicSort &Sort, + llvm::raw_ostream &OS) { + switch (Sort.Kind) { + case LogicSortKind::Bool: + if (Value.K != LogicValue::Kind::Bool) + return false; + OS << (Value.Truth ? "True" : "False"); + return true; + case LogicSortKind::MathematicalInteger: + case LogicSortKind::Pointer: + if (Value.K != LogicValue::Kind::Integer) + return false; + OS << "(" << Value.Integer.toDecimal() << " : Int)"; + return true; + case LogicSortKind::BitVector: + if (Value.K != LogicValue::Kind::Integer) + return false; + OS << "(BitVec.ofInt " << Sort.BitWidth << " (" << Value.Integer.toDecimal() + << "))"; + return true; + case LogicSortKind::Heap: + if (Value.K != LogicValue::Kind::Heap || !Value.Heap) + return false; + printLeanRuns(*Value.Heap, "(", " : Int)", OS); + return true; + case LogicSortKind::Seq: + if (Value.K != LogicValue::Kind::Seq || !Value.Elements) + return false; + OS << "(["; + for (size_t I = 0; I != Value.Elements->size(); ++I) + OS << (I ? ", " : "") << "(" << (*Value.Elements)[I].toDecimal() + << " : Int)"; + OS << "] : List Int)"; + return true; + case LogicSortKind::Set: + if (Value.K != LogicValue::Kind::Set || !Value.Heap) + return false; + printLeanRuns(*Value.Heap, "decide ((", " : Int) ≠ 0)", OS); + return true; + case LogicSortKind::Multiset: + if (Value.K != LogicValue::Kind::Multiset || !Value.Heap) + return false; + printLeanRuns(*Value.Heap, "((", " : Int).toNat)", OS); + return true; + case LogicSortKind::Map: + if (Value.K != LogicValue::Kind::Map || !Value.Heap || !Value.Values) + return false; + OS << "(fun (k : Int) => if "; + printLeanRuns(*Value.Heap, "(", " : Int)", OS); + OS << " k ≠ 0 then some ("; + printLeanRuns(*Value.Values, "(", " : Int)", OS); + OS << " k) else none)"; + return true; + case LogicSortKind::Invalid: + return false; + } + return false; +} + VerifyResult verify::exportLeanScratchPad( const ObligationModule &Module, llvm::raw_ostream &OS, bool EmitPreamble, std::set &EmittedFunctions, @@ -1854,4 +1953,60 @@ VerifyResult verify::exportLeanScratchPad( Result.Message = ProjectGoals ? "editable Lean project obligation export" : "unchecked Lean obligation export"; return Result; +} + +std::optional verify::exportLeanRefutation( + const ObligationModule &Module, const Obligation &Item, + const CounterexampleAssignment &Assignment, + std::map &Specs, std::string &Why) { + // The goal, its bodies, and its specs as its project states them. + std::string Goals; + llvm::raw_string_ostream GoalsOS(Goals); + std::set Functions, Theorems; + std::vector Stated; + const std::set Selection = {Item.Id}; + VerifyResult Exported = exportLeanScratchPad( + Module, GoalsOS, /*EmitPreamble=*/false, Functions, Theorems, + /*ModuleIndex=*/1, &Stated, &Selection, &Specs); + auto Goal = llvm::find_if( + Stated, [](const LeanProjectGoal &Goal) { return Goal.Exported; }); + if (Exported.Status != VerifyStatus::Exported || Goal == Stated.end()) { + Why = Exported.Message.empty() ? "the goal has no Lean statement" + : Exported.Message; + return std::nullopt; + } + + // The goal applied to the values of its variables, in the order it binds + // them; the definition instances it states then hold by evaluation. + std::string Application; + llvm::raw_string_ostream ApplicationOS(Application); + std::map Variables; + collectLeanVariables(Item.Goal.get(), {}, Variables); + for (const auto &[Name, Sort] : Variables) { + auto Value = Assignment.Values.find(Name); + ApplicationOS << "\n "; + if (Value == Assignment.Values.end() || + !printLeanValue(Value->second, Sort, ApplicationOS)) { + Why = "the counterexample gives " + Name + " no value Lean can state"; + return std::nullopt; + } + } + + LeanRefutation Refutation; + Refutation.Group = Goal->Group; + Refutation.Goal = Goal->Name; + Refutation.StableId = Goal->StableId; + llvm::raw_string_ostream OS(Refutation.Text); + OS << "import CppVerify.Specs\nimport CppVerify.Auto\n\n" + << "noncomputable section\n\nset_option maxRecDepth 100000\n" + << "set_option linter.unusedVariables false\n\n" + << "section Goal\n\nset_option maxHeartbeats 0\n\n" + << "attribute [local instance] cppVerifyPropDecidable\n\n" + << Goals << "end Goal\n\n" + << "/- The goal is false at the counterexample of " + << (Item.StableId.empty() ? Item.Id : Item.StableId) << ". -/\n" + << "theorem " << Goal->Name << "_refuted : ¬ " << Goal->Name + << " := by\n intro h\n have h₁ := h" << Application + << "\n cppverify_refute h₁\n"; + return Refutation; } \ No newline at end of file From 0ce103143c3ac93d36767dc87371029d3c909f11 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:47 +0530 Subject: [PATCH 07/80] verify: Add the cppverify_refute tactic. --- clang/lib/Verify/Driver/LeanAutomation.h | 61 ++++++++++++++++++++++++ 1 file changed, 61 insertions(+) diff --git a/clang/lib/Verify/Driver/LeanAutomation.h b/clang/lib/Verify/Driver/LeanAutomation.h index fa807cf23c..8166156719 100644 --- a/clang/lib/Verify/Driver/LeanAutomation.h +++ b/clang/lib/Verify/Driver/LeanAutomation.h @@ -213,6 +213,67 @@ macro "cppverify_auto_div" : tactic => `(tactic| ( cppverify_norm all_goals grind [cppIntDiv, cppIntRem])) +/-- Memory reads and machine comparisons by their definitions, so that a +closed instance decides. -/ +macro "cppverify_reads" : tactic => `(tactic| (try simp only [heapSelectInt, + heapSelectBv, cppBvSle, cppBvSlt, cppBvUle, cppBvUlt])) + +/-- An instance of a goal at known values, evaluated: the bodies it names, +the spec definitions of `CppVerify.Specs` by their equations (which proves +the definition instances it states), memory reads and machine comparisons +by their definitions; then decided, or shown by `grind`, since a store +relates two heaps at every address. -/ +macro "cppverify_evaluate" : tactic => `(tactic| ( + cppverify_unfold_bodies + try cppverify_eval_specs + all_goals cppverify_reads + all_goals first + | decide + | grind [heapSelectInt, heapSelectBv, heapStoreInt, heapStoreBool, + heapStoreBv])) + +open Lean Elab Tactic in +/-- Whether a tactic closes every goal within `cppverify.autoBudget` +heartbeats of its own, as each step of cppverify_auto; running out of them +is a no, as any other error is. -/ +def CppVerify.Auto.withinBudget (tactic : TacticM Unit) : TacticM Bool := do + let budget := cppverify.autoBudget.get (← getOptions) + let saved ← saveState + tryCatchRuntimeEx + (do + let heartbeats ← IO.getNumHeartbeats + withTheReader Core.Context + (fun ctx => { ctx with initHeartbeats := heartbeats, + maxHeartbeats := budget * 1000 }) tactic + return (← getUnsolvedGoals).isEmpty) + fun _ => do saved.restore; return false + +open Lean Elab Tactic Meta in +/-- Shows that the instance of a goal that `h` states is false, or fails +saying why not: that Lean decides it true, which contradicts the +counterexample, or that it cannot decide it. Each attempt has the heartbeats +of a step of cppverify_auto. -/ +elab "cppverify_refute " h:ident : tactic => withMainContext do + let saved ← saveState + let attempts : List Syntax.Tactic := [ + ← `(tactic| (revert $h:ident; decide)), + ← `(tactic| (revert $h:ident; cppverify_evaluate))] + for attempt in attempts do + if ← CppVerify.Auto.withinBudget (evalTactic attempt) then return + saved.restore + let some decl := (← getLCtx).findFromUserName? h.getId + | throwError "cppverify: no hypothesis {h.getId}" + -- Whether the instance holds of itself: in a context without the goal, + -- which would prove any instance. + let probe ← mkFreshExprMVarAt {} {} decl.type + setGoals [probe.mvarId!] + let holds ← CppVerify.Auto.withinBudget + (evalTactic (← `(tactic| first | decide | cppverify_evaluate))) + saved.restore + if holds then + throwError "cppverify: Lean decides the goal true at the counterexample" + throwError "cppverify: Lean cannot decide the goal at the counterexample" + open Lean Elab Tactic in /-- Tries each step on the goal, each with `cppverify.autoBudget` heartbeats of its own, and keeps the first that proves it. A step that runs out of From 0a057fff7de7d039e06bef4ac8c97d98c7649a1e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:48 +0530 Subject: [PATCH 08/80] verify: Check refutation entries against the negation of their goals. --- clang/lib/Verify/Driver/LeanCertifier.h | 52 +++++++++++++++---------- 1 file changed, 32 insertions(+), 20 deletions(-) diff --git a/clang/lib/Verify/Driver/LeanCertifier.h b/clang/lib/Verify/Driver/LeanCertifier.h index 4286533013..da062f8322 100644 --- a/clang/lib/Verify/Driver/LeanCertifier.h +++ b/clang/lib/Verify/Driver/LeanCertifier.h @@ -130,11 +130,13 @@ unsafe def replayProject (closure : Closure) : IO Replayed := do return { env, rejected, owner } /-- Whether the proof of a goal states exactly the goal its generated module -defines and depends on no axiom outside the allowed ones. -/ +defines, or a refutation exactly its negation, and depends on no axiom +outside the allowed ones. -/ def checkStatement (project : Replayed) (goal module generated : Name) - (allowed : NameSet) : Option String := Id.run do + (refutes : Bool) (allowed : NameSet) : Option String := Id.run do let env := project.env - let proof := goal.appendAfter "_proof" + let proof := goal.appendAfter (if refutes then "_refuted" else "_proof") + let stated := if refutes then mkApp (mkConst ``Not) (mkConst goal) else mkConst goal match env.find? goal with | some (.defnInfo _) => if project.owner[goal]? != some generated then @@ -144,8 +146,8 @@ def checkStatement (project : Replayed) (goal module generated : Name) | some (.thmInfo v) => if project.owner[proof]? != some module then return some s!"{proof} is not declared in {module}" - if v.type != .const goal [] then - return some s!"{proof} proves {v.type}, not {goal}" + if v.type != stated then + return some s!"{proof} proves {v.type}, not {stated}" match axiomsOf env proof with | .error e => return some e | .ok axioms => @@ -169,35 +171,45 @@ def userSorry (closure : Closure) (project : Replayed) : Option String := Id.run return some s!"{name} of CppVerify.User uses sorry" return none +/-- What a check reports: the goal, or the theorem that refutes it. -/ +def shown (goal : Name) (refutes : Bool) : Name := + if refutes then goal.appendAfter "_refuted" else goal + /-- Usage: Certify GOALS ALLOWED, where each line of GOALS is a goal, its -proof module, and the module that defines it, separated by tabs, and ALLOWED -lists the axioms a proof may use, separated by commas. Prints one line per -goal: `ok` or `fail`, the goal, and why it failed. A goal is proved when its -proof module and its generated module pass the kernel, with every module of -the project they import, and its proof states exactly the goal and uses only -the allowed axioms. The generated modules are replayed first, so that a -proof file that declares a name one declares is the one left out. -/ +proof module, and the module that defines it, separated by tabs, then +`refutation` for a module that refutes the goal it defines, and ALLOWED lists +the axioms a proof may use, separated by commas. Prints one line per goal: +`ok` or `fail`, the goal (a refutation's theorem for a refutation), and why it +failed. A goal is proved when its proof module and its generated module pass +the kernel, with every module of the project they import, and its proof +states exactly the goal (a refutation, its negation) and uses only the +allowed axioms. The generated modules are replayed first, so that a proof +file that declares a name one declares is the one left out. -/ unsafe def main (args : List String) : IO UInt32 := do let [goals, allowed] := args | throw <| IO.userError "usage: Certify GOALS ALLOWED" let sysroot ← findSysroot initSearchPath sysroot let toolchain := (sysroot / "lib" / "lean").toString let allowed := (allowed.splitOn ",").foldl (fun s a => s.insert a.toName) ({} : NameSet) - let mut entries : Array (Name × Name × Name) := #[] + let mut entries : Array (Name × Name × Name × Bool) := #[] for line in ← IO.FS.lines goals do - let [goal, module, generated] := line.splitOn "\t" | continue - entries := entries.push (goal.toName, module.toName, generated.toName) - let roots := entries.map (·.2.2) ++ entries.map (·.2.1) + match line.splitOn "\t" with + | [goal, module, generated] => + entries := entries.push (goal.toName, module.toName, generated.toName, false) + | [goal, module, generated, "refutation"] => + entries := entries.push (goal.toName, module.toName, generated.toName, true) + | _ => continue + let roots := entries.map (·.2.2.1) ++ entries.map (·.2.1) let (_, closure) ← (roots.forM (Closure.visit toolchain)).run {} let project ← replayProject closure let user := userSorry closure project - for (goal, module, generated) in entries do + for (goal, module, generated, refutes) in entries do let why := (project.rejected[module]?).orElse fun _ => (project.rejected[generated]?).orElse fun _ => user.orElse fun _ => - checkStatement project goal module generated allowed + checkStatement project goal module generated refutes allowed match why with - | none => IO.println s!"ok\t{goal}" - | some why => IO.println s!"fail\t{goal}\t{why.replace "\n" " "}" + | none => IO.println s!"ok\t{shown goal refutes}" + | some why => IO.println s!"fail\t{shown goal refutes}\t{why.replace "\n" " "}" return 0 )lean"; From e31d6454a65bba4e618f481639bda3d12b7c3644 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:48 +0530 Subject: [PATCH 09/80] verify: Confirm the counterexamples of a fallback project in Lean. --- clang/lib/Verify/Driver/Verifier.cpp | 197 ++++++++++++++++++++++++--- 1 file changed, 176 insertions(+), 21 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index afecdfcb86..6854f53d33 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -1063,6 +1063,8 @@ struct VerifyDiagnostic { /// For an export to a Lean project: of its goals, how many cppverify_auto /// proves. unsigned LeanAutomatic = 0; + /// A certified failure that its refutation shows in Lean too. + bool LeanRefuted = false; /// A proof by a solver, by Lean, or by both, which establishes what it /// proves. bool isProof() const { @@ -1678,6 +1680,41 @@ class LeanProject { return llvm::Error::success(); } + // The refutation of each certified failure of the run, + // Refutations//.lean. Any other is removed: its failure is + // gone, or its program is not this one. + llvm::Error + writeLeanRefutations(const std::vector &Refutations) { + const std::string Dir = + leanProjectPath(leanProjectRoot(), {"CppVerify", "Refutations"}); + std::set Written; + for (const LeanRefutation &Refutation : Refutations) { + const std::string Path = + leanProjectPath(Dir, {Refutation.Group, Refutation.Goal + ".lean"}); + if (std::error_code EC = llvm::sys::fs::create_directories( + llvm::sys::path::parent_path(Path))) + return llvm::createStringError(EC, "cannot create %s", Path.c_str()); + if (llvm::Error Error = writeTextFileIfChanged( + Path, std::string(LeanGeneratedNote) + "\n" + Refutation.Text)) + return Error; + Written.insert(Path); + } + std::error_code EC; + std::vector Gone; + for (llvm::sys::fs::recursive_directory_iterator It(Dir, EC), End; + It != End && !EC; It.increment(EC)) + if (llvm::sys::path::extension(It->path()) == ".lean" && + !Written.count(It->path())) + Gone.push_back(It->path()); + for (const std::string &Path : Gone) { + llvm::sys::fs::remove(Path); + llvm::sys::fs::remove(llvm::sys::path::parent_path(Path)); + } + if (Written.empty()) + llvm::sys::fs::remove(Dir); + return llvm::Error::success(); + } + static std::vector leanProofComponents(const LeanProjectGoal &Goal, std::string &File) { File = Goal.Name + ".lean"; @@ -2289,8 +2326,9 @@ class LeanProject { } llvm::Expected> - certifyLeanProject(const std::vector &ProjectGoals) { - if (ProjectGoals.empty()) + certifyLeanProject(const std::vector &ProjectGoals, + const std::vector &Refutations = {}) { + if (ProjectGoals.empty() && Refutations.empty()) return llvm::createStringError(llvm::inconvertibleErrorCode(), "the project has no proof obligations"); auto Launcher = leanLauncher(".cppverify-certification"); @@ -2317,11 +2355,37 @@ class LeanProject { std::map UniqueGoals; for (const LeanProjectGoal &Goal : ProjectGoals) UniqueGoals.emplace(Goal.Name, &Goal); - std::vector> Proofs( - UniqueGoals.begin(), UniqueGoals.end()); - for (const auto &[Name, Goal] : Proofs) + // What is built: each goal's proof, and each refutation, which is its + // goal's module too; with the certifier's line for each, and the name + // it reports. + struct Build { + std::string Name, Source, Object, Entry; + }; + std::vector Proofs; + for (const auto &[Name, Goal] : UniqueGoals) { + std::string File; + Proofs.push_back( + {Name, leanProjectPath(Root, leanProofComponents(*Goal, File)), + leanProjectPath(leanProjectPath(ProofBuildDir, {Goal->Group}), + {Name + ".olean"}), + Name + "\tCppVerify.Proofs." + Goal->Group + "." + Name + + "\tCppVerify.Goals." + Goal->Group + "\n"}); + } + for (const LeanRefutation &Refutation : Refutations) { + const std::string Module = + "CppVerify.Refutations." + Refutation.Group + "." + Refutation.Goal; + Proofs.push_back( + {Refutation.Goal + "_refuted", + leanProjectPath(Root, {"CppVerify", "Refutations", Refutation.Group, + Refutation.Goal + ".lean"}), + leanProjectPath(Root, {".lake", "build", "lib", "lean", "CppVerify", + "Refutations", Refutation.Group, + Refutation.Goal + ".olean"}), + Refutation.Goal + "\t" + Module + "\t" + Module + "\trefutation\n"}); + } + for (const Build &Proof : Proofs) if (std::error_code EC = llvm::sys::fs::create_directories( - leanProjectPath(ProofBuildDir, {Goal->Group}))) + llvm::sys::path::parent_path(Proof.Object))) return llvm::createStringError( EC, "cannot create Lean proof build directory"); // Each proof builds by itself, several at once, unless nothing it is @@ -2336,12 +2400,9 @@ class LeanProject { std::atomic NextProof{0}; auto buildProofs = [&] { for (size_t I; (I = NextProof++) < Proofs.size();) { - const auto &[Name, Goal] = Proofs[I]; - std::string File; - const std::string ProofSource = - leanProjectPath(Root, leanProofComponents(*Goal, File)); - const std::string ProofObject = leanProjectPath( - leanProjectPath(ProofBuildDir, {Goal->Group}), {Name + ".olean"}); + const std::string &Name = Proofs[I].Name; + const std::string &ProofSource = Proofs[I].Source; + const std::string &ProofObject = Proofs[I].Object; const std::string KeyFile = leanProjectPath(KeyDir, {Name}); const std::optional Key = leanProofKey(ProofSource); if (Key && llvm::sys::fs::exists(ProofObject)) @@ -2370,13 +2431,11 @@ class LeanProject { std::map Failures; std::string Built; for (size_t I = 0; I != Proofs.size(); ++I) { - const auto &[Name, Goal] = Proofs[I]; if (BuildErrors[I]) { - Failures[Name] = *BuildErrors[I]; + Failures[Proofs[I].Name] = *BuildErrors[I]; continue; } - Built += Name + "\tCppVerify.Proofs." + Goal->Group + "." + Name + - "\tCppVerify.Goals." + Goal->Group + "\n"; + Built += Proofs[I].Entry; } if (Built.empty()) return Failures; @@ -2409,9 +2468,9 @@ class LeanProject { Failures[Fields[1].str()] = Fields.size() == 3 ? Fields[2].str() : "the certifier failed"; } - for (const auto &[Name, Goal] : UniqueGoals) - if (!Failures.count(Name) && !Checks.count(Name)) - Failures[Name] = "the certifier did not check it"; + for (const Build &Proof : Proofs) + if (!Failures.count(Proof.Name) && !Checks.count(Proof.Name)) + Failures[Proof.Name] = "the certifier did not check it"; return Failures; } @@ -3258,6 +3317,14 @@ class Verifier { BackendKind Kind; }; std::vector Confirmations; + /// Certified failures a fallback project shows in Lean: each one's + /// place in Diags and its refutation, or why it has none. + struct Refutation { + size_t Index; + std::optional Lean; + std::string Why; + }; + std::vector Refutations; /// For a verified proof function: what its verification proves. std::shared_ptr Contract; /// The verdict on the definedness of the function's contract, when it @@ -4475,6 +4542,21 @@ class Verifier { AnyFailed = true; if (!Fn->IsProof) FailedCallers.insert(Fn->Identity); + // A fallback project shows a certified counterexample in Lean too. + if (LeanFallbackBackend && R.Reason == VerifyReason::Counterexample) { + FunctionRun::Refutation Pending{Diags.size(), std::nullopt, + "the solver's model gives the " + "goal's variables no values"}; + auto Item = + llvm::find_if(Module.Obligations, [&](const Obligation &Item) { + return (Item.StableId.empty() ? Item.Id : Item.StableId) == + R.ObligationId; + }); + if (R.Assignment && Item != Module.Obligations.end()) + Pending.Lean = exportLeanRefutation( + Module, *Item, *R.Assignment, LeanModules.Specs, Pending.Why); + Run.Refutations.push_back(std::move(Pending)); + } std::string Msg = "verification failed: " + Fn->Name; if (!R.ObligationId.empty()) Msg += " [" + R.ObligationId + "]"; @@ -4521,6 +4603,7 @@ class Verifier { D.Hidden = true; Run.AllOk = false; Run.Confirmations.clear(); + Run.Refutations.clear(); VerifyResult Result; Result.Status = VerifyStatus::Unresolved; Result.Reason = VerifyReason::Interrupted; @@ -4528,6 +4611,10 @@ class Verifier { Fn.Name, std::move(Result)}); }; std::vector Confirmations; + std::vector Refutations; + // What certification found of the refutations, or why it checked none. + std::optional> RefutationChecks; + std::string RefutationsUnchecked; for (size_t I = 0; I != Runs.size(); ++I) { FunctionRun &Run = Runs[I]; if (Run.Interrupted) @@ -4558,6 +4645,10 @@ class Verifier { Pending.Index += Base; Confirmations.push_back(std::move(Pending)); } + for (FunctionRun::Refutation &Pending : Run.Refutations) { + Pending.Index += Base; + Refutations.push_back(std::move(Pending)); + } if (Run.ContractCheck) ContractChecks[Functions[I]->Identity] = Base + *Run.ContractCheck; if (DumpOS) @@ -4575,9 +4666,15 @@ class Verifier { [](const LeanProjectGoal &Goal) { return Goal.Exported; }); const std::set *RunGroups = LeanFallbackBackend ? &LeanRunGroups : nullptr; + std::vector LeanRefutations; + for (const FunctionRun::Refutation &Pending : Refutations) + if (Pending.Lean) + LeanRefutations.push_back(*Pending.Lean); llvm::Error Finalized = Lean->writeLeanProjectModules(LeanModules); if (!Finalized) Finalized = Lean->finalizeLeanProject(LeanProjectGoals, RunGroups); + if (!Finalized && LeanFallbackBackend) + Finalized = Lean->writeLeanRefutations(LeanRefutations); if (!Finalized && Opts.LeanAuto) Lean->automateLeanProject(LeanProjectGoals); reportLeanWarnings(); @@ -4599,7 +4696,7 @@ class Verifier { "cannot finalize Lean project (" + llvm::toString(std::move(Finalized)) + ")"}); } else if (Opts.LeanCertify && !interruptRequested() && - (!ExportedGoals.empty() || + (!ExportedGoals.empty() || !Refutations.empty() || Opts.LeanFallbackProjectPath.empty())) { // A verdict certification does not make a proof is reported, and // what its vacuity checks found is not. @@ -4624,12 +4721,15 @@ class Verifier { Diagnostic.Result->Message = Reason; } }; - auto Certified = Lean->certifyLeanProject(ExportedGoals); + auto Certified = + Lean->certifyLeanProject(ExportedGoals, LeanRefutations); std::map GoalsByName; for (const LeanProjectGoal &Goal : ExportedGoals) GoalsByName.emplace(Goal.Name, &Goal); + std::string NotCertified; if (!Certified) { const std::string Reason = llvm::toString(Certified.takeError()); + NotCertified = Reason; for (size_t Index = 0; Index != Diags.size(); ++Index) if (Diags[Index].K == VerifyDiagnostic::Exported) failed(Index, Reason); @@ -4696,6 +4796,11 @@ class Verifier { Diagnostic.Message += " [vacuous]"; } } + + if (Certified) + RefutationChecks = *Certified; + else + RefutationsUnchecked = NotCertified; } } for (const SpecReliance &Check : ProofDependencies) @@ -5224,6 +5329,54 @@ class Verifier { if (!Trusted.empty()) Diagnostic.Message += " [trusts=" + Trusted + "]"; } + // A certified failure stands on the certifier's evaluation. Its + // refutation shows it in Lean too; one Lean decides the other way is a + // disagreement between two evaluators of one goal, never a failure. Only + // the failures that stand once the verdicts settle are reported. + for (const FunctionRun::Refutation &Pending : Refutations) { + if ((!RefutationChecks && RefutationsUnchecked.empty()) || + Diags[Pending.Index].K != VerifyDiagnostic::Error) + continue; + const std::string Function = Diags[Pending.Index].FunctionName; + std::string Why = Pending.Why; + if (Pending.Lean && !RefutationChecks) { + Why = RefutationsUnchecked; + } else if (Pending.Lean) { + auto Outcome = RefutationChecks->find(Pending.Lean->Goal + "_refuted"); + if (Outcome == RefutationChecks->end()) { + Diags[Pending.Index].Message += " (confirmed in Lean)"; + Diags[Pending.Index].LeanRefuted = true; + continue; + } + Why = Outcome->second; + if (llvm::StringRef(Why).contains( + "Lean decides the goal true at the counterexample")) { + VerifyDiagnostic &Failure = Diags[Pending.Index]; + const std::string Detail = + "Lean decides the goal of " + Pending.Lean->StableId + + " true at the solver's counterexample, which the certifier " + "found false"; + Failure.K = VerifyDiagnostic::Unresolved; + Failure.Message = Function + " (" + Detail + ")"; + if (Failure.Result) { + Failure.Result->Status = VerifyStatus::Unresolved; + Failure.Result->Reason = VerifyReason::InconsistentBackendResults; + Failure.Result->Message = Detail; + Failure.Message += backendSuffix(*Failure.Result); + } + continue; + } + } + // What the refutation tactic says, else the first line. + llvm::StringRef Said = Why; + if (size_t At = Said.find("cppverify: "); At != llvm::StringRef::npos) + Said = Said.substr(At + std::strlen("cppverify: ")); + Said = Said.take_until([](char C) { return C == '\n'; }); + Diags.push_back({VerifyDiagnostic::Warning, + "the counterexample of " + Function + + " is not confirmed in Lean: " + Said.str()}); + } + // Calls from code that is not verified rely on the precondition without // checking it, so the proof holds only where they establish it. for (const auto &[Index, Identity, Callees] : CallDependencies) { @@ -5373,6 +5526,8 @@ class Verifier { } if (D.K == VerifyDiagnostic::Exported && D.LeanAutomatic) Record["lean_automatic"] = static_cast(D.LeanAutomatic); + if (D.LeanRefuted) + Record["lean_refuted"] = true; if (D.Result) { const VerifyResult &Result = *D.Result; if (!Result.BackendName.empty()) From 2706a6eb95b92f8cc472a1784ac1f95036ad314d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:49 +0530 Subject: [PATCH 10/80] test: Add the program of the Lean refutation test. --- .../Verify/suite/Inputs/lean_refutation.cpp | 39 +++++++++++++++++++ 1 file changed, 39 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_refutation.cpp diff --git a/clang/test/Verify/suite/Inputs/lean_refutation.cpp b/clang/test/Verify/suite/Inputs/lean_refutation.cpp new file mode 100644 index 0000000000..bc715e344f --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_refutation.cpp @@ -0,0 +1,39 @@ +// Certified failures shown in Lean, for lean_refutation.test. + +int add_one(int x) + cppverify::pre(x < 100) + cppverify::post(cppverify::result == x + 1) +{ + return x + 2; +} + +int below_three() + cppverify::post(cppverify::forall(i, 0, 4, i < 3)) +{ + return 0; +} + +void zero_first(int *p) + cppverify::pre(cppverify::valid(p, 2)) + cppverify::modifies(*p) + cppverify::post(p[0] == 1) +{ + p[0] = 0; +} + +cppverify::spec int tri(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : tri(n - 1) + n; +} + +cppverify::proof void tri_three() + cppverify::post(tri(3) == 7) +{ +} + +// A choice is opaque in Lean, so its counterexample is not decided there. +cppverify::proof void pick_one() + cppverify::post(cppverify::choose(k, 0, 2, k == 1) == 0) +{ +} From 481b3c8f390fed19a0bbb42b4f038e0c647654b3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 02:02:48 +0530 Subject: [PATCH 11/80] test: Add the refutations of the Lean refutation test that are bounded or not reported. --- .../suite/Inputs/lean_refutation_budget.cpp | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_refutation_budget.cpp diff --git a/clang/test/Verify/suite/Inputs/lean_refutation_budget.cpp b/clang/test/Verify/suite/Inputs/lean_refutation_budget.cpp new file mode 100644 index 0000000000..1d75a803eb --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_refutation_budget.cpp @@ -0,0 +1,24 @@ +// Refutations that are bounded, and refutations that are not reported, for +// lean_refutation.test. + +// Lean would decide this one by trying each of a billion integers: each +// attempt of the refutation stops at the heartbeats of a step of +// cppverify_auto, and the counterexample is not decided there. +cppverify::proof void below_a_billion() + cppverify::post(cppverify::forall(i, 0, 1000000000, i < 999999999)) +{ +} + +// A counterexample checked with a postcondition that is not established is +// not a failure (spec.post), so nothing is reported of its refutation. +cppverify::spec bool ge(int n) + cppverify::inductive + cppverify::post(!cppverify::result || n > -1000) +{ + return n == 20 || ge(n + 1); +} + +cppverify::proof void far() + cppverify::post(ge(-5000)) +{ +} From 8143117a7b40f46496670e0c3a6be7f874805a64 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:49 +0530 Subject: [PATCH 12/80] test: Add the instances the refutation tactic must not refute. --- .../suite/Inputs/lean_refutation_tactic.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/lean_refutation_tactic.lean diff --git a/clang/test/Verify/suite/Inputs/lean_refutation_tactic.lean b/clang/test/Verify/suite/Inputs/lean_refutation_tactic.lean new file mode 100644 index 0000000000..02f2844211 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_refutation_tactic.lean @@ -0,0 +1,16 @@ +import CppVerify.Auto + +-- An instance that holds: the refutation says Lean decides it true. +example : ¬ (∀ x : Int, x = 1 → x > 0) := by + intro h + have h₁ := h 1 + cppverify_refute h₁ + +opaque cppverify_unknown : Int + +-- An instance about a constant Lean has no value for: the refutation says +-- Lean cannot decide it. +example : ¬ (∀ x : Int, x = 0 → x = cppverify_unknown) := by + intro h + have h₁ := h 0 + cppverify_refute h₁ From feac3c452728b522c07bcf96011a22f4c118e443 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:49 +0530 Subject: [PATCH 13/80] test: Check that counterexamples are confirmed in Lean, or left with a reason. --- clang/test/Verify/suite/lean_refutation.test | 88 ++++++++++++++++++++ 1 file changed, 88 insertions(+) create mode 100644 clang/test/Verify/suite/lean_refutation.test diff --git a/clang/test/Verify/suite/lean_refutation.test b/clang/test/Verify/suite/lean_refutation.test new file mode 100644 index 0000000000..55ddb8a3a4 --- /dev/null +++ b/clang/test/Verify/suite/lean_refutation.test @@ -0,0 +1,88 @@ +# REQUIRES: lean +# +# A fallback project shows each certified counterexample in Lean too: its +# refutation states the failing goal as the project would and proves it false +# at the model's values, and certification checks it like a proof. A +# counterexample Lean cannot decide stays a failure, with a warning; Lean +# deciding the goal true would be a disagreement, never a failure. +# +# RUN: rm -rf %t && mkdir -p %t && cp %S/Inputs/lean_refutation.cpp %t/r.cpp +# RUN: not %cpp-verify --lean-fallback=%t/p %t/r.cpp -- 2>&1 | FileCheck %s --check-prefix=EXPORT +# RUN: FileCheck %s --input-file=%t/p/CppVerify/Refutations/cppverify_add_one_fc20c3/cppverify_add_one_fc20c3_postcondition_1b36ffe1.lean --check-prefix=REFUTATION +# RUN: not %cpp-verify --lean-fallback=%t/p --lean-certify %t/r.cpp -- 2>&1 | FileCheck %s --check-prefix=CERTIFY +# RUN: not %cpp-verify --lean-fallback=%t/p --lean-certify --diagnostics-format=json %t/r.cpp -- 2>&1 | FileCheck %s --check-prefix=JSON +# +# The checker takes a refutation only when its theorem states the negation +# of the goal its module defines. +# RUN: mkdir -p %t/p/CppVerify/Refutations/cppverify_fake_000000 %t/p/.lake/build/lib/lean/CppVerify/Refutations/cppverify_fake_000000 +# RUN: printf 'def cppverify_fake_000000_goal : Prop := True\ntheorem cppverify_fake_000000_goal_refuted : True := trivial\n' > %t/p/CppVerify/Refutations/cppverify_fake_000000/cppverify_fake_000000_goal.lean +# RUN: cd %t/p && lake env lean -R %t/p -o .lake/build/lib/lean/CppVerify/Refutations/cppverify_fake_000000/cppverify_fake_000000_goal.olean CppVerify/Refutations/cppverify_fake_000000/cppverify_fake_000000_goal.lean +# RUN: printf 'cppverify_fake_000000_goal\tCppVerify.Refutations.cppverify_fake_000000.cppverify_fake_000000_goal\tCppVerify.Refutations.cppverify_fake_000000.cppverify_fake_000000_goal\trefutation\n' > %t/goals +# RUN: cd %t/p && lake env lean --run .cppverify/Certify.lean %t/goals propext,Quot.sound,Classical.choice | FileCheck %s --check-prefix=CHECKER +# +# A failure that is gone takes its refutation with it, as does a module of +# no failure. +# RUN: sed -i 's/return x + 2;/return x + 1;/' %t/r.cpp +# RUN: not %cpp-verify --lean-fallback=%t/p %t/r.cpp -- 2>&1 | FileCheck %s --check-prefix=FIXED +# RUN: not test -e %t/p/CppVerify/Refutations/cppverify_add_one_fc20c3 +# RUN: not test -e %t/p/CppVerify/Refutations/cppverify_fake_000000 +# RUN: test -f %t/p/CppVerify/Refutations/cppverify_tri_three_55daf7/cppverify_tri_three_55daf7_postcondition_ffa2cd20.lean +# +# The tactic says why it cannot refute: Lean decides the instance true, or +# cannot decide it. +# +# Each attempt of the tactic has the heartbeats of a step of cppverify_auto, +# so a refutation Lean could only decide by trying a billion integers ends; +# and a counterexample that is not a failure once the verdicts settle reports +# nothing of its refutation. +# RUN: cd %t/p && not lake env lean %S/Inputs/lean_refutation_tactic.lean 2>&1 | FileCheck %s --check-prefix=TACTIC +# RUN: not %cpp-verify --lean-fallback=%t/b --lean-certify %S/Inputs/lean_refutation_budget.cpp -- 2>&1 | FileCheck %s --check-prefix=BUDGET + +# EXPORT: error: verification failed: add_one +# EXPORT-NOT: confirmed in Lean + +# The goal's definitions are elaborated without a heartbeat limit; the +# theorem keeps Lean's, which also bounds the kernel's check of its proof. +# REFUTATION: {{^}}import CppVerify.Specs{{$}} +# REFUTATION-NOT: maxHeartbeats +# REFUTATION: {{^}}section Goal{{$}} +# REFUTATION-EMPTY: +# REFUTATION-NEXT: {{^}}set_option maxHeartbeats 0{{$}} +# REFUTATION-NOT: maxHeartbeats +# REFUTATION: {{^}}def cppverify_add_one_fc20c3_postcondition_1b36ffe1 : Prop :={{$}} +# REFUTATION-NOT: maxHeartbeats +# REFUTATION: {{^}}end Goal{{$}} +# REFUTATION-NOT: maxHeartbeats +# REFUTATION: {{^}}theorem cppverify_add_one_fc20c3_postcondition_1b36ffe1_refuted : ¬ cppverify_add_one_fc20c3_postcondition_1b36ffe1 := by{{$}} +# REFUTATION-NEXT: {{^}} intro h{{$}} +# REFUTATION-NEXT: {{^}} have h₁ := h{{$}} +# REFUTATION-NEXT: {{^}} (fun (a : Int) => (0 : Int)){{$}} +# REFUTATION-NEXT: {{^}} (fun (a : Int) => (0 : Int)){{$}} +# REFUTATION-NEXT: {{^}} (BitVec.ofInt 32 ({{-?[0-9]+}})){{$}} +# REFUTATION-NEXT: {{^}} (BitVec.ofInt 32 ({{-?[0-9]+}})){{$}} +# REFUTATION-NEXT: {{^}} cppverify_refute h₁{{$}} + +# A contract, a bounded quantifier, a store to memory, and a spec Lean +# defines; the choice is opaque in Lean. +# CERTIFY: error: verification failed: add_one {{.*}}[reason=counterexample] (confirmed in Lean) +# CERTIFY-NEXT: error: verification failed: below_three {{.*}}[reason=counterexample] (confirmed in Lean) +# CERTIFY-NEXT: error: verification failed: zero_first {{.*}}[reason=counterexample] (confirmed in Lean) +# CERTIFY-NEXT: Verified: spec decreases: tri +# CERTIFY-NEXT: error: verification failed: tri_three {{.*}}[reason=counterexample] (confirmed in Lean) +# CERTIFY-NEXT: error: verification failed: pick_one {{.*}}[reason=counterexample]{{$}} +# CERTIFY-NEXT: warning: the counterexample of pick_one is not confirmed in Lean: Lean cannot decide the goal at the counterexample + +# JSON: {"backend":"z3","function":"add_one","lean_refuted":true, +# JSON: {"message":"the counterexample of pick_one is not confirmed in Lean: Lean cannot decide the goal at the counterexample","schema":"cppverify.diagnostic/1","severity":"warning","status":"warning"} + +# CHECKER: fail cppverify_fake_000000_goal_refuted cppverify_fake_000000_goal_refuted proves True, not Not cppverify_fake_000000_goal + +# FIXED: Verified: add_one [backend=z3] + +# TACTIC: lean_refutation_tactic.lean:7:2: error: cppverify: Lean decides the goal true at the counterexample +# TACTIC: lean_refutation_tactic.lean:16:2: error: cppverify: Lean cannot decide the goal at the counterexample + +# BUDGET: error: verification failed: below_a_billion {{.*}}[reason=counterexample]{{$}} +# BUDGET: Unresolved: verification unresolved: far {{.*}}[reason=spec.post] (its counterexample is checked with the postcondition of ge, which is not established){{$}} +# BUDGET: warning: the counterexample of below_a_billion is not confirmed in Lean: Lean cannot decide the goal at the counterexample +# BUDGET-NOT: the counterexample of far From e6cc4dadfc4b6cb2d3201dd7f34f4b617241b354 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:50 +0530 Subject: [PATCH 14/80] test: Add the proof of the one fidelity matrix goal cppverify_auto leaves open. --- ...heap_spec_read_2c60ae_postcondition_af8523f4.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/backend_fidelity_proofs/cppverify_heap_spec_read_2c60ae_postcondition_af8523f4.lean diff --git a/clang/test/Verify/suite/Inputs/backend_fidelity_proofs/cppverify_heap_spec_read_2c60ae_postcondition_af8523f4.lean b/clang/test/Verify/suite/Inputs/backend_fidelity_proofs/cppverify_heap_spec_read_2c60ae_postcondition_af8523f4.lean new file mode 100644 index 0000000000..9ee9a7538e --- /dev/null +++ b/clang/test/Verify/suite/Inputs/backend_fidelity_proofs/cppverify_heap_spec_read_2c60ae_postcondition_af8523f4.lean @@ -0,0 +1,12 @@ +import CppVerify.Goals.cppverify_heap_spec_read_2c60ae +import CppVerify.User +import CppVerify.Auto + +theorem cppverify_heap_spec_read_2c60ae_postcondition_af8523f4_proof : cppverify_heap_spec_read_2c60ae_postcondition_af8523f4 := by + apply cppverify_heap_spec_read_2c60ae_postcondition_af8523f4.of_readable + intro __heap_0 __heap_1 __heap_alloc_0 __heap_live_0 pointer_0 cppverify_spec_axiom_1_1 cppverify_spec_axiom_1_2 cppverify_spec_axiom_1_3 cppverify_spec_axiom_2_1 cppverify_spec_axiom_2_2 cppverify_spec_axiom_2_3 h_pre_1 h_pre_2 h_entry_1 h_null_1 h_null_2 h_object_1 h_store_1 + rw [cppverify_spec_axiom_1_2, cppverify_spec_axiom_2_2] + cppverify_unfold_bodies + cppverify_heap + simp + grind From 97c7129f3e8a10d9bc062dd962f510b0c0bb7418 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:50 +0530 Subject: [PATCH 15/80] test: Require decisive Lean verdicts in the backend fidelity gate. --- .../suite/Inputs/run_backend_fidelity.py | 69 ++++++++++++++++++- 1 file changed, 68 insertions(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/Inputs/run_backend_fidelity.py b/clang/test/Verify/suite/Inputs/run_backend_fidelity.py index d8734e15cc..cbbbdf3871 100644 --- a/clang/test/Verify/suite/Inputs/run_backend_fidelity.py +++ b/clang/test/Verify/suite/Inputs/run_backend_fidelity.py @@ -4,6 +4,7 @@ import json import pathlib import re +import shutil import subprocess import sys @@ -528,6 +529,64 @@ def check_lean_identity(cpp_verify, source, canonical, work): run(["lake", "--dir={}".format(project), "build", "CppVerify.Generated"], {0}) +def check_lean_verdicts(cpp_verify, source, proofs, work): + # Lean decides every case: a project certifies each valid one, with the + # proof by hand of the one goal cppverify_auto does not prove, and the + # one only a hidden definition proves, which Lean sees; a fallback + # project confirms the counterexample of each invalid one in Lean. + project = work / "lean-verdicts" + command = [ + str(cpp_verify), + "--backend=lean", + "--lean-project={}".format(project), + "--diagnostics-format=json", + str(source), + "--", + ] + run(command, {0, 1}) + for proof in proofs.glob("*.lean"): + group = re.match(r"(cppverify_.+?_[0-9a-f]{6})_", proof.name).group(1) + shutil.copy(proof, project / "CppVerify" / "Proofs" / group / proof.name) + # Every verdict on a function: its obligations, and the check of its + # contract when it has one. + certified = {} + for record in parse_json_lines( + run(command[:4] + ["--lean-certify"] + command[4:], {0, 1}) + ): + certified.setdefault(record.get("function"), []).append(record) + for name in sorted(VALID_FUNCTIONS | set(UNRESOLVED_REASONS)): + for record in certified.get(name) or [{}]: + if record.get("status") != "certified": + fail( + "Lean returned {} ({}) instead of certified for {}".format( + record.get("status"), record.get("message"), name + ) + ) + refuted = function_records( + parse_json_lines( + run( + [ + str(cpp_verify), + "--lean-fallback={}".format(work / "lean-refutations"), + "--lean-certify", + "--diagnostics-format=json", + str(source), + "--", + ], + {1}, + ) + ) + ) + for name in sorted(INVALID_FUNCTIONS): + record = refuted[name] + if record.get("status") != "failed" or record.get("lean_refuted") is not True: + fail( + "Lean did not confirm the counterexample of {} ({}, {})".format( + name, record.get("status"), record.get("message") + ) + ) + + def warning_messages(records): return [ record.get("message", "") @@ -617,10 +676,12 @@ def main(): parser.add_argument("--cpp-verify", required=True, type=pathlib.Path) parser.add_argument("--source", required=True, type=pathlib.Path) parser.add_argument("--recommends", required=True, type=pathlib.Path) + parser.add_argument("--lean-proofs", required=True, type=pathlib.Path) parser.add_argument("--work-dir", required=True, type=pathlib.Path) arguments = parser.parse_args() - for path in (arguments.cpp_verify, arguments.source, arguments.recommends): + for path in (arguments.cpp_verify, arguments.source, arguments.recommends, + arguments.lean_proofs): if not path.exists(): fail("required path does not exist: {}".format(path)) arguments.work_dir.mkdir(parents=True, exist_ok=False) @@ -642,6 +703,12 @@ def main(): ) print("PASS: Lean theorem, hash, replay, and kernel-export identity") + check_lean_verdicts( + arguments.cpp_verify, arguments.source, arguments.lean_proofs, + arguments.work_dir + ) + print("PASS: decisive Lean verdicts: valid cases certified, counterexamples refuted") + check_recommends_exclusion( arguments.cpp_verify, arguments.recommends, arguments.work_dir ) From bda0be4e62e020243eed678dc1e0e59e801bccb1 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:51 +0530 Subject: [PATCH 16/80] test: Check the decisive Lean row of the backend fidelity gate. --- clang/test/Verify/suite/backend_fidelity_gate.test | 2 ++ 1 file changed, 2 insertions(+) diff --git a/clang/test/Verify/suite/backend_fidelity_gate.test b/clang/test/Verify/suite/backend_fidelity_gate.test index 4af1f028b2..93dc370831 100644 --- a/clang/test/Verify/suite/backend_fidelity_gate.test +++ b/clang/test/Verify/suite/backend_fidelity_gate.test @@ -5,6 +5,7 @@ # RUN: --cpp-verify=%cpp-verify \ # RUN: --source=%S/Inputs/backend_fidelity_matrix.cpp \ # RUN: --recommends=%S/Inputs/backend_fidelity_recommends.cpp \ +# RUN: --lean-proofs=%S/Inputs/backend_fidelity_proofs \ # RUN: --work-dir=%t | FileCheck %s # # CHECK: PASS: canonical feature and operator matrix @@ -12,4 +13,5 @@ # CHECK-NEXT: PASS: source diagnostic identity and parallel determinism # CHECK-NEXT: PASS: canonical and incremental-BMC archive replay # CHECK-NEXT: PASS: Lean theorem, hash, replay, and kernel-export identity +# CHECK-NEXT: PASS: decisive Lean verdicts: valid cases certified, counterexamples refuted # CHECK-NEXT: PASS: recommends exclusion from BMC and Lean replay artifacts From 4e72ac8a906ae05c1c2cbe508e4e42e7ec5db3c4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:51 +0530 Subject: [PATCH 17/80] docs: Lower a documentation example without its Lean output options. --- website/scripts/check-doc-examples.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/website/scripts/check-doc-examples.py b/website/scripts/check-doc-examples.py index 2d7fa3122d..ae116befc1 100644 --- a/website/scripts/check-doc-examples.py +++ b/website/scripts/check-doc-examples.py @@ -209,8 +209,10 @@ def check(cpp_verify, job): f"\nactual output:\n{output.strip()[:2500]}"), False return None # A Lean export compiles the example itself; it has no lowering of its own. + # Lowering takes no Lean output. if "--backend=lean" not in arguments: - code, output = run(cpp_verify, source, ["--lower-only", *arguments], 300) + lowering = [a for a in arguments if not a.startswith("--lean-")] + code, output = run(cpp_verify, source, ["--lower-only", *lowering], 300) if code is None or code != 0 or "error:" in output: return f"{where}: the example does not compile:\n{output.strip()[:1500]}", False code, output = run(cpp_verify, source, From 7ae367156d72f4efc4f98e020617aef84d8a4397 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:51 +0530 Subject: [PATCH 18/80] docs: Explain counterexamples in Lean in chapter 17. --- .../part-ii/ch17-backends-modular-calls.rst | 66 ++++++++++++++++++- 1 file changed, 64 insertions(+), 2 deletions(-) diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst index 84198725c5..b007f3583c 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -279,8 +279,9 @@ proof. When every exported goal kernel-checks the function is ``Proved (z3+lean)``, or ``Proved (portfolio+lean)``, and JSON reports ``"status":"mixed-proof"`` with the per-obligation split. When Lean checked every obligation, because ``--lean-fallback-scope=all`` exported them all or -the solver proved none on its own, the function is ``Certified``. SAT counterexamples are failures, not -fallback candidates. A fallback run examines in Lean only what its solver +the solver proved none on its own, the function is ``Certified``. A certified +counterexample stays a failure, and the project shows it false in Lean too +(`Counterexamples in Lean`_). A fallback run examines in Lean only what its solver leaves unresolved, so the proofs of the obligations and functions the solver settles stay where they are until Lean needs them again. @@ -319,6 +320,67 @@ one does (``[trusts=f]``, ``[partial]``). It also gets the same vacuity checks, run with Z3: a goal that holds only because no execution reaches it is ``Certified: f [backend=Lean] [vacuous]``, with a warning. +Counterexamples in Lean +~~~~~~~~~~~~~~~~~~~~~~~ + +A counterexample the solver finds is a failure once the certifier has +evaluated the program's goal at it, with every spec at its true definition. A +fallback project shows each such failure false in Lean as well: its +refutation, ``CppVerify/Refutations//.lean``, states the +failing goal as the project would and proves it false at the values the +model gives its variables, machine integers as bit-vectors, memory as a +function of its runs of equal cells. ``--lean-certify`` checks it as it +checks a proof, with the kernel and Lean's foundations alone, and says so: + +.. cppverify-example: flags --lean-fallback={dir}/proof --lean-certify + +.. code-block:: cpp + + int add_one(int x) + cppverify::pre(x == 4) + cppverify::post(cppverify::result == x + 1) + { + return x + 2; + } + +.. code-block:: text + + error: verification failed: add_one [fn_5f5a376164645f6f6e6569::postcondition@3:37] (counterexample: result [ssa=__result_1] [type=i32] = 6, x [ssa=x_0] [type=i32] = 4; trace: return.return@5:3 value=6) [backend=z3] [reason=counterexample] (confirmed in Lean) + +The refutation applies the goal to the model's values and decides what is +left false, the definition instances the goal states with it, since they hold +of the spec functions Lean defines: + +.. code-block:: lean4 + + theorem cppverify_add_one_fc20c3_postcondition_8876761e_refuted : ¬ cppverify_add_one_fc20c3_postcondition_8876761e := by + intro h + have h₁ := h + (fun (a : Int) => (0 : Int)) + (fun (a : Int) => (0 : Int)) + (BitVec.ofInt 32 (6)) + (BitVec.ofInt 32 (4)) + cppverify_refute h₁ + +``cppverify_refute`` decides the instance, or evaluates it first, the spec +functions that are Lean definitions (`Spec functions in Lean`_) by their +equations, a store to memory with ``grind``, since it relates two heaps at +every address, and a quantifier over a range of integers by trying each one. +A goal that applies a spec Lean leaves opaque, such as a ``cppverify::choose``, +cannot be decided there: the failure stands, and a warning says so (``the +counterexample of pick_one is not confirmed in Lean: Lean cannot decide the +goal at the counterexample``). Should Lean decide the goal true at the +values, the solver's counterexample and Lean would disagree about one goal; +the function is then ``Unresolved`` with reason +``backend.inconsistent-results``, as when two solvers disagree, never +``Failed``. Each attempt of ``cppverify_refute`` has the heartbeats of a step +of ``cppverify_auto``, so a goal Lean could decide only by trying a billion +integers is not decided rather than tried for hours. Only failures that stand +once every verdict is settled report their refutations: a counterexample +checked with a spec's postcondition that is not established is no failure +(``spec.post``), and nothing is said of its refutation. A refutation is the +project's, rewritten by every run and removed with its failure. + Goals as hypotheses ~~~~~~~~~~~~~~~~~~~ From 823ae1f0b3293adbc991bcf1f137638fb82f9ad7 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:52 +0530 Subject: [PATCH 19/80] docs: Say that a fallback project refutes certified counterexamples. --- website/source/language/tooling.rst | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index bc8a7b150f..e26a16a7d9 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -347,6 +347,12 @@ Backends function whose exported goals all kernel-check reports ``Proved (z3+lean)`` (JSON ``"status":"mixed-proof"`` with an ``evidence`` record), or ``Certified`` when Lean checked every goal. + A certified counterexample stays a failure, and the project gets its + refutation, ``CppVerify/Refutations//.lean``; with + ``--lean-certify`` a refutation that checks adds ``(confirmed in + Lean)`` to the failure (JSON ``"lean_refuted": true``), one Lean + cannot decide a warning, and one Lean decides the other way makes the + function ``Unresolved`` (``backend.inconsistent-results``). * - ``--lean-fallback-scope=unproved|all`` - ``unproved`` (default) exports only the obligations the solver did not prove individually; each keeps the goal name it has in a complete From 88cd63aded47f0fa455d45f594f42a903fa6a4a5 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:52 +0530 Subject: [PATCH 20/80] docs: Note counterexamples confirmed in Lean in the release notes. --- website/source/release-notes.rst | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index b116cdb75a..c615fa3d1e 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -444,6 +444,19 @@ which a project needs to define the spec and to name the goal's hypotheses; a module keeps the specs its specs' measures apply (:doc:`book/part-ii/ch17-backends-modular-calls`). +**Counterexamples confirmed in Lean.** A counterexample the solver found was +checked by cpp-verify's own evaluator only. A fallback project now holds the +refutation of each certified failure, the failing goal stated as the project +states it and proved false at the model's values; ``--lean-certify`` checks it +with the kernel, and a failure it shows reads ``(confirmed in Lean)``. A +counterexample Lean cannot decide, as one that applies a ``cppverify::choose``, +stays a failure with a warning, and one Lean decides the other way would be +``Unresolved``, a disagreement, never a failure. Lean decides a quantifier +over a range of integers by trying each one, within the heartbeats of a step +of ``cppverify_auto``. The release gate's Lean row now +decides every case of its matrix: each valid one certified, each invalid one +refuted (:doc:`book/part-ii/ch17-backends-modular-calls`). + **Lean 4.35.0.** Lean projects pin ``leanprover/lean4:v4.35.0``. A project 0.1 generated, pinned to ``v4.32.2``, moves to the new pin the next time cpp-verify writes it, with a warning; a proof that no longer builds needs updating for that From a957a73f4ec820766abc705b436fb8ded70dd9e0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:52 +0530 Subject: [PATCH 21/80] docs: Describe Lean refutations in the design. --- docs/DESIGN.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 712f4e18a6..cc5524ed61 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -2028,6 +2028,18 @@ A result proved in Lean, alone or with the solver, rests on the callee contracts and spec facts its module uses, as a solver's does: certification runs before those are settled, whatever else failed, and a Lean result gets the same qualifiers and vacuity checks as a verified one. +A certified counterexample is shown false in Lean too: the fallback project +gets its refutation, the failing goal stated as the project states it and a +theorem `¬ goal` proved at the values the model gives its variables +(`cppverify_refute`: decided, or evaluated by the spec definitions, a store +by `grind`, a quantifier over a range of integers by trying each one, each +attempt within the heartbeats of a step of `cppverify_auto`), which +`--lean-certify` checks as it checks a proof. Of the failures that stand once +the verdicts settle, a refutation that checks marks +the failure `(confirmed in Lean)`; one Lean cannot decide leaves it a failure +with a warning; one Lean decides true is a disagreement between two +evaluators of one goal and makes the function `Unresolved` +(`backend.inconsistent-results`), never `Failed`. ## MVP Acceptance Programs From 90189a8f19f232accd6ac59da12aeecfc43abb38 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Fri, 23 Oct 2026 21:49:53 +0530 Subject: [PATCH 22/80] docs: Describe Lean refutations and the gate's Lean row in the architecture. --- docs/ARCHITECTURE.md | 44 +++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 41 insertions(+), 3 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 44d83331bf..5002ca77de 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1772,6 +1772,43 @@ replay both drive it. termination module it gives the solver (`LeanRunGroups`); a record whose group is among them but has no goal this run, or whose goal the run knows but does not export, is left where it is and never moved. +- **Refutations.** Where the adapter attributes a certified counterexample + to an obligation, it keeps the model's value of every free variable of + that obligation's goal (`counterexampleAssignment`, read through the + certifier's `CandidateModel::constant`, so the values are the ones it + evaluated; `VerifyResult::Assignment`). A fallback run turns each such + failure into `exportLeanRefutation`'s module, which states the goal and + the bodies it unfolds as the project would (its specs added to `Specs`, + so the trial may define them), then `theorem _refuted : ¬ `: + the goal applied to the values in the order it binds its variables + (machine integers as `BitVec.ofInt`, a heap or collection by its runs of + equal cells as nested `if`s), and closed by `cppverify_refute`, an + `Auto.lean` tactic that tries `decide`, then evaluation by the bodies, + the spec equations (which prove the definition instances the goal states), + memory reads, and machine comparisons, closed by `decide` or, for a store + relation, which quantifies over every address, `grind`. When both fail it + tries to show the instance true, in a context without the goal (which + would prove any instance of itself): Lean deciding it true fails with + `Lean decides the goal true at the counterexample`, else with `Lean cannot + decide the goal`. Each attempt, and that probe, has `cppverify.autoBudget` + heartbeats of its own (`withinBudget`, as a step of `cppverify_auto`), and + the module lifts the heartbeat limit for the goal's definitions only, so + the theorem keeps Lean's limit, which bounds the kernel's check of it too: + with no limit, the refutation of an inductive predicate applied at -5000 + ran for over an hour. The prelude decides a quantifier over a + range of integers by trying each one (`cppIntBallDecidable`, + `cppIntBexDecidable`, through core's `Nat` ones). `writeLeanRefutations` + writes `Refutations//.lean` and removes every other, and + certification builds them beside the proofs and gives the checker each as + a `refutation` entry, whose theorem must state exactly `Not ` of the + goal its module defines, with Lean's foundations alone. Once the verdicts + settle (a failure checked with a spec postcondition that is not + established is `spec.post`), the driver marks each failure that stands and + was confirmed (`LeanRefuted`, JSON `lean_refuted`), warns of one Lean + cannot decide, and makes one Lean decides true `Unresolved` + (`InconsistentBackendResults`): two evaluators of one goal disagree, so + the failure is not a fact. On the gate's matrix every certified failure is + refuted; a goal applying an opaque function (a choice, `validPtr`) is not. - **Readable goals.** `makeGoal` (`Obligation.cpp`) marks each `Or` it builds, `!A || rest`, with where `A` comes from (`LogicExpr::Premise`, @@ -2091,8 +2128,9 @@ prove individually, and by default only those are exported, under their complete-export goal names (`--lean-fallback-scope=all` exports every obligation). Once they kernel-check, the result is `MixedProof` (`Proved (z3+lean)`, JSON `mixed-proof`) with `ProofEvidence` recording the -split; `Certified` still means Lean checked every obligation. SAT -counterexamples are never fallback successes. +split; `Certified` still means Lean checked every obligation. A certified +counterexample is never a fallback success; its refutation shows it in +Lean. A verdict left to Lean (a Lean-backend export, or a fallback export under `--lean-certify`) rests on what its module uses, as a solver's does. At export @@ -2519,7 +2557,7 @@ an unchecked support table: | Quantifiers and finite-fuel specs | Both quantifier kinds, recursive spec calls, and conservative `unknown` rather than false proof | | Frontend-derived semantics | Type invariants and complete-loop Z3/BMC parity | | Portable artifacts | Source-stable obligation IDs, canonical/BMC archive replay, and deterministic parallel results | -| Lean | Source/archive obligation identity, one proof file per project goal recording its statement hash, generated-file kernel build, and bounds instrumentation | +| Lean | Source/archive obligation identity, one proof file per project goal recording its statement hash, generated-file kernel build, bounds instrumentation, and decisive verdicts: every valid case certified (one with a proof by hand, `Inputs/backend_fidelity_proofs`), every counterexample refuted | | Advisory checks | `cppverify::recommends` warnings stay source-only and never enter BMC or Lean replay artifacts | An approved valid quantified or inductive query may remain From b41eba8cfa6f8ed603088bd46b54925edd7ec5d7 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:28 +0530 Subject: [PATCH 23/80] verify: Mark a function that uses a construct the verifier does not represent. --- clang/lib/Verify/IR/VStmt.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/clang/lib/Verify/IR/VStmt.h b/clang/lib/Verify/IR/VStmt.h index b5c84ce10d..6db19ef883 100644 --- a/clang/lib/Verify/IR/VStmt.h +++ b/clang/lib/Verify/IR/VStmt.h @@ -374,6 +374,10 @@ struct VFunction { std::unique_ptr Domain; /// A spec without a definition: the value of another outside its domain. bool Uninterpreted = false; + /// Its body or contract uses a construct the verifier does not represent, + /// so the function is not verified: an executable or proof function keeps + /// its contract for its callers, a spec only its declaration. + bool UnsupportedConstruct = false; /// A choose(...) lifted to a function of what its body mentions: its post /// is the defining axiom (a witness when one exists), assumed, not proved. bool IsChoice = false; From 8966deb569bde36f01050766e4a2a58ec9333c90 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:28 +0530 Subject: [PATCH 24/80] verify: Copy the unsupported-construct mark with a function. --- clang/lib/Verify/IR/VStmt.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/lib/Verify/IR/VStmt.cpp b/clang/lib/Verify/IR/VStmt.cpp index 2d7a0a134d..687197e9ff 100644 --- a/clang/lib/Verify/IR/VStmt.cpp +++ b/clang/lib/Verify/IR/VStmt.cpp @@ -188,6 +188,7 @@ VFunction verify::cloneVFunction(const VFunction &Fn) { {cloneVExpr(R.Base.get()), cloneVExpr(R.Count.get()), R.ElementSize}); Out.Domain = cloneVExpr(Fn.Domain.get()); Out.Uninterpreted = Fn.Uninterpreted; + Out.UnsupportedConstruct = Fn.UnsupportedConstruct; Out.IsChoice = Fn.IsChoice; Out.UsesDynamicStorage = Fn.UsesDynamicStorage; Out.FreshOwnedReturn = Fn.FreshOwnedReturn; From d2c2979642bb0a29743c7fee98c2fb00402bf9ed Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:28 +0530 Subject: [PATCH 25/80] verify: Keep the unsupported-construct mark through loop unrolling. --- clang/lib/Verify/Transform/LoopUnroll.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/lib/Verify/Transform/LoopUnroll.cpp b/clang/lib/Verify/Transform/LoopUnroll.cpp index e6fe44f6a2..1f6bd7d3a3 100644 --- a/clang/lib/Verify/Transform/LoopUnroll.cpp +++ b/clang/lib/Verify/Transform/LoopUnroll.cpp @@ -231,6 +231,7 @@ VFunction LoopUnroller::unroll(const VFunction &Fn, unsigned K) { {cloneVExpr(R.Base.get()), cloneVExpr(R.Count.get()), R.ElementSize}); Out.Domain = cloneVExpr(Fn.Domain.get()); Out.Uninterpreted = Fn.Uninterpreted; + Out.UnsupportedConstruct = Fn.UnsupportedConstruct; Out.IsChoice = Fn.IsChoice; Out.IsExternalContract = Fn.IsExternalContract; Out.IsTrusted = Fn.IsTrusted; From 7a445598e5f36ea85b4bd04e1b5a2fcfc7182559 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:29 +0530 Subject: [PATCH 26/80] verify: Report a malformed inductive predicate with the predicate. --- clang/lib/Verify/Transform/Inductive.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/clang/lib/Verify/Transform/Inductive.h b/clang/lib/Verify/Transform/Inductive.h index a128132d4e..c68e0d22bf 100644 --- a/clang/lib/Verify/Transform/Inductive.h +++ b/clang/lib/Verify/Transform/Inductive.h @@ -21,10 +21,11 @@ namespace verify { /// Defines every predicate marked inductive in \p Functions as the least /// fixpoint of its body, and appends the specs and proof functions that /// establish its rules. A malformed predicate is reported through \p Report, -/// at its inductive marker, and left as it is. +/// with the predicate and at its inductive marker, and left as it is. void expandInductivePredicates( std::vector> &Functions, - llvm::function_ref Report); + llvm::function_ref + Report); } // namespace verify } // namespace clang From 219e43588ba20ab97f08a7580a9b4497f16e139d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:29 +0530 Subject: [PATCH 27/80] verify: Name the predicate of each inductive predicate error. --- clang/lib/Verify/Transform/Inductive.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/clang/lib/Verify/Transform/Inductive.cpp b/clang/lib/Verify/Transform/Inductive.cpp index 4e686f60e9..8c9ca9b15f 100644 --- a/clang/lib/Verify/Transform/Inductive.cpp +++ b/clang/lib/Verify/Transform/Inductive.cpp @@ -1055,7 +1055,8 @@ class GroupExpander { void verify::expandInductivePredicates( std::vector> &Functions, - llvm::function_ref Report) { + llvm::function_ref + Report) { std::map Inductive; for (auto &Fn : Functions) if (Fn->InductiveLoc.isValid()) @@ -1067,7 +1068,7 @@ void verify::expandInductivePredicates( std::map Unfoldings; for (auto &[Identity, Fn] : Inductive) { auto reject = [&, &Identity = Identity, Fn = Fn](const std::string &Why) { - Report(Fn->InductiveLoc, Fn->Name + ": " + Why); + Report(*Fn, Fn->InductiveLoc, Fn->Name + ": " + Why); Rejected.insert(Identity); }; if (!Fn->IsSpec || Fn->ReturnType.Kind != VTypeKind::Bool) { @@ -1142,7 +1143,7 @@ void verify::expandInductivePredicates( nonPositiveOccurrence(Unfoldings.at(Member).get(), Group); !Where.empty()) { Report( - Fn.InductiveLoc, + Fn, Fn.InductiveLoc, Fn.Name + ": " + (Group.size() == 1 ? Fn.Name : std::string("a predicate it is " From 036a3762894e1171d8b67192b92790a96def71f0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:29 +0530 Subject: [PATCH 28/80] verify: Record the function and part of it each conversion error belongs to. --- clang/lib/Verify/Frontend/ASTConverter.h | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index abf66a2105..152d0d48c4 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -16,6 +16,13 @@ namespace verify { struct ConversionError { SourceRange Range; std::string Message; + /// The function it is written in (its identity and name), whose verdict it + /// decides; empty for an error of the translation unit. + std::string Function; + std::string FunctionName; + /// In the function's signature or contract, rather than its body: then + /// its callers cannot use the contract either. + bool InContract = false; }; class ASTConverter { @@ -37,9 +44,20 @@ class ASTConverter { /// The innermost declaration, statement, or expression being converted, /// where an error is reported unless it names a place of its own. SourceRange CurrentRange; + /// The function whose conversion an error belongs to, and whether the + /// converter is in its signature and contract or in its body. + std::string ErrorFunction; + std::string ErrorFunctionName; + bool ErrorInContract = false; void error(std::string Message) { error(CurrentRange, std::move(Message)); } void error(SourceRange Range, std::string Message) { - Errors.push_back({Range, std::move(Message)}); + Errors.push_back({Range, std::move(Message), ErrorFunction, + ErrorFunctionName, ErrorInContract}); + } + /// An error about \p Fn found once every function is converted. + void errorOf(const VFunction &Fn, SourceLocation Loc, std::string Message) { + Errors.push_back( + {SourceRange(Loc), std::move(Message), Fn.Identity, Fn.Name, false}); } std::vector> Warnings; /// Maps unqualified field name -> "param." for type_invariant lowering. From a027243f186b666203a0735d5a5a925f47192ee6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:30 +0530 Subject: [PATCH 29/80] verify: Keep what others may rely on of a function the verifier cannot represent. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 152 +++++++++++++++------ 1 file changed, 108 insertions(+), 44 deletions(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index 6b2d271bd9..e04ac734fa 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -1903,6 +1903,28 @@ static void collectFunctionCandidates(const DeclContext *DC, ASTContext &Ctx, } } +/// What remains of a function that uses a construct the verifier does not +/// represent: an executable or proof function becomes the contract its +/// callers assume, not verified; a spec, a declaration without the +/// definition, postconditions, and reads that its body would establish. +static void markUnsupported(VFunction &Fn) { + Fn.UnsupportedConstruct = true; + Fn.Body.clear(); + Fn.ClauseProofs.clear(); + if (!Fn.IsSpec) { + Fn.IsExternalContract = true; + return; + } + Fn.Uninterpreted = true; + Fn.Postconditions.clear(); + Fn.Decreases.clear(); + Fn.Recommends.clear(); + Fn.Reads.clear(); + Fn.Domain.reset(); + Fn.Unfolding.reset(); + Fn.InductiveLoc = SourceLocation(); +} + std::vector> ASTConverter::convertTranslationUnit() { std::vector> Out; llvm::StringSet<> Identities; @@ -1910,16 +1932,19 @@ std::vector> ASTConverter::convertTranslationUnit() { collectFunctionCandidates(Ctx.getTranslationUnitDecl(), Ctx, Definitions); UsedConstexprSpecs.clear(); for (const FunctionDecl *FD : Definitions) { - if (isa(FD)) { - if (functionContract(FD) || hasContractStatements(FD, Ctx)) - error(FD->getLocation(), - FD->getNameAsString() + - ": member function verification is unsupported"); - continue; - } - // Only a template with contracts is reported here: one without matters - // where verified code calls it, which reports the call. - if (FD->isTemplated()) { + if (isa(FD) || FD->isTemplated()) { + llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); + llvm::SaveAndRestore OwnerName(ErrorFunctionName, FD->getNameAsString()); + llvm::SaveAndRestore InContract(ErrorInContract, true); + if (isa(FD)) { + if (functionContract(FD) || hasContractStatements(FD, Ctx)) + error(FD->getLocation(), + FD->getNameAsString() + + ": member function verification is unsupported"); + continue; + } + // Only a template with contracts is reported here: one without + // matters where verified code calls it, which reports the call. if (!FD->isInStdNamespace() && Ctx.getSourceManager().isWrittenInMainFile(FD->getLocation()) && (functionContract(FD) || hasContractStatements(FD, Ctx))) @@ -1930,12 +1955,24 @@ std::vector> ASTConverter::convertTranslationUnit() { } if (FD->isInStdNamespace()) continue; + const size_t ErrorsBefore = Errors.size(); auto Fn = convertFunction(FD); - if (Fn) { + if (Fn && Errors.size() == ErrorsBefore) { Identities.insert(Fn->Identity); Out.push_back(std::move(Fn)); continue; } + // A construct the verifier does not represent costs its function alone. + // What remains is what others may rely on: the contract, when it + // converted, of an executable or proof function; a spec's declaration. + if (Fn && + (Fn->IsSpec || + std::none_of(Errors.begin() + ErrorsBefore, Errors.end(), + [](const ConversionError &E) { return E.InContract; }))) { + markUnsupported(*Fn); + Identities.insert(Fn->Identity); + Out.push_back(std::move(Fn)); + } // A body the verifier does not verify still calls contracted functions, // whose preconditions it then assumes without checking (Frama-C reports // such properties as valid under hypotheses). @@ -1979,7 +2016,10 @@ std::vector> ASTConverter::convertTranslationUnit() { Changed = true; if (Identities.contains(functionIdentity(FD))) continue; + const size_t ErrorsBefore = Errors.size(); if (auto Fn = convertConstexprSpec(FD)) { + if (Errors.size() != ErrorsBefore) + markUnsupported(*Fn); Identities.insert(Fn->Identity); Lifted.push_back({I, std::move(Fn)}); } @@ -2039,9 +2079,10 @@ std::vector> ASTConverter::convertTranslationUnit() { } for (auto &Fn : Unspecified) Out.push_back(std::move(Fn)); - expandInductivePredicates(Out, [&](SourceLocation Loc, std::string Message) { - error(Loc, std::move(Message)); - }); + expandInductivePredicates( + Out, [&](const VFunction &Fn, SourceLocation Loc, std::string Message) { + errorOf(Fn, Loc, std::move(Message)); + }); for (auto &Fn : ChoiceFunctions) Out.push_back(std::move(Fn)); ChoiceFunctions.clear(); @@ -2132,14 +2173,14 @@ std::vector> ASTConverter::convertTranslationUnit() { llvm::any_of(Reach[Fn->Identity], [&](const std::string &Id) { return ChoiceIdentities.count(Id) && Reach[Id].count(Fn->Identity); }); - error(Fn->DeclLoc, - Fn->Name + - (InChoice - ? ": an inductive predicate occurs in the bodies of its " - "group only positively, never inside cppverify::choose" - : ": an inductive predicate applies itself only in its " - "body or through inductive predicates, not through " - "another spec")); + errorOf(*Fn, Fn->DeclLoc, + Fn->Name + + (InChoice + ? ": an inductive predicate occurs in the bodies of its " + "group only positively, never inside cppverify::choose" + : ": an inductive predicate applies itself only in its " + "body or through inductive predicates, not through " + "another spec")); for (const std::string &Other : Reach[Fn->Identity]) if (Reach[Other].count(Fn->Identity)) InductiveCycles.insert(Other); @@ -2200,9 +2241,9 @@ std::vector> ASTConverter::convertTranslationUnit() { return kindOf(*ByIdentity[Id]) == kindOf(*Fn); }); if (!SameKind) { - error(Fn->DeclLoc, - Fn->Name + ": mutual recursion is supported only among " - "functions of one kind: spec, proof, or executable"); + errorOf(*Fn, Fn->DeclLoc, + Fn->Name + ": mutual recursion is supported only among " + "functions of one kind: spec, proof, or executable"); continue; } const bool AllDiverge = @@ -2222,16 +2263,16 @@ std::vector> ASTConverter::convertTranslationUnit() { !ByIdentity[Id]->DivergenceDeclared; }); if (!SameMeasure) { - error(Fn->DeclLoc, - Fn->Name + ": mutually recursive " + - (Fn->IsSpec ? "spec" - : Fn->IsProof ? "proof" - : "executable") + - " functions require decreases clauses, all of the " - "same length" + - (Fn->IsSpec || Fn->IsProof - ? "" - : ", or all cppverify::decreases(*)")); + errorOf(*Fn, Fn->DeclLoc, + Fn->Name + ": mutually recursive " + + (Fn->IsSpec ? "spec" + : Fn->IsProof ? "proof" + : "executable") + + " functions require decreases clauses, all of the " + "same length" + + (Fn->IsSpec || Fn->IsProof + ? "" + : ", or all cppverify::decreases(*)")); continue; } Fn->RecursionGroup = std::move(Group); @@ -2242,12 +2283,13 @@ std::vector> ASTConverter::convertTranslationUnit() { if (Recursive && Fn->Decreases.empty() && Fn->DivergenceDeclared) continue; if (Recursive && Fn->Decreases.empty()) { - error(Fn->DeclLoc, - Fn->Name + - (Fn->IsSpec || Fn->IsProof - ? ": recursive spec and proof functions require decreases" - : ": recursive executable functions require decreases, or " - "cppverify::decreases(*) to allow divergence")); + errorOf( + *Fn, Fn->DeclLoc, + Fn->Name + + (Fn->IsSpec || Fn->IsProof + ? ": recursive spec and proof functions require decreases" + : ": recursive executable functions require decreases, or " + "cppverify::decreases(*) to allow divergence")); continue; } Fn->NeedsDecreasesCheck = Recursive; @@ -2307,6 +2349,15 @@ std::vector> ASTConverter::convertTranslationUnit() { Fn->SpecFuel.erase(Identity); } } + // A function an error after conversion is about (a recursion without a + // measure, a malformed inductive predicate) costs its function alone, as + // an error in its body does. + std::set Faulty; + for (const ConversionError &Err : Errors) + Faulty.insert(Err.Function); + for (auto &Fn : Out) + if (Faulty.count(Fn->Identity) && !Fn->UnsupportedConstruct) + markUnsupported(*Fn); return Out; } @@ -2554,6 +2605,10 @@ bool ASTConverter::exceedsNestingLimit(const FunctionDecl *FD, std::unique_ptr ASTConverter::convertFunction(const FunctionDecl *FD) { llvm::SaveAndRestore At(CurrentRange, SourceRange(FD->getLocation())); + llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); + llvm::SaveAndRestore OwnerName(ErrorFunctionName, FD->getNameAsString()); + llvm::SaveAndRestore InContract(ErrorInContract, true); + const size_t ErrorsAtStart = Errors.size(); const FunctionContractInfo *FCI = functionContract(FD); if (!FCI) { // Assertions and ghost code are obligations even without a contract @@ -2948,6 +3003,7 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { Fn->Body.push_back(std::make_unique( std::move(Condition), Check->getExprLoc())); } + ErrorInContract = false; for (auto &S : convertStmt(Body)) Fn->Body.push_back(std::move(S)); TrackInitialization = false; @@ -2983,11 +3039,13 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { CurrentFn = nullptr; return nullptr; } + // A spec whose body the verifier does not represent remains a + // declaration (markUnsupported), which its users apply. if (Fn->IsSpec && !specBodyCanBeAxiomatized(Fn->Body)) { error(Fn->Name + ": spec function body is unsupported by axiomatic " "lowering"); CurrentFn = nullptr; - return nullptr; + return Fn; } if (!Fn->IsSpec && Fn->Body.empty() && Fn->Postconditions.empty() && !functionContract(FD)) { @@ -3010,7 +3068,8 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { InPost = SavedPost; Fn->ClauseProofs.push_back(std::move(Converted)); } - if (Fn->IsSpec && Fn->Body.empty() && Fn->Decreases.empty()) { + if (Fn->IsSpec && Fn->Body.empty() && Fn->Decreases.empty() && + Errors.size() == ErrorsAtStart) { CurrentFn = nullptr; return nullptr; } @@ -3157,6 +3216,10 @@ bool ASTConverter::checkLoopTermination(const Stmt *Loop, bool HasMeasure) { std::unique_ptr ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { + llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); + llvm::SaveAndRestore OwnerName(ErrorFunctionName, FD->getNameAsString()); + llvm::SaveAndRestore InContract(ErrorInContract, true); + const size_t ErrorsAtStart = Errors.size(); ParameterNames.clear(); if (exceedsNestingLimit(FD, functionContract(FD)) || hasIndirectMemoryAccess(FD)) @@ -3203,10 +3266,11 @@ ASTConverter::convertConstexprSpec(const FunctionDecl *FD) { if (const Stmt *Body = FD->getBody()) { beginInitializationTracking(FD); + ErrorInContract = false; Fn->Body = convertStmt(Body); TrackInitialization = false; } - if (Fn->Body.empty()) { + if (Fn->Body.empty() && Errors.size() == ErrorsAtStart) { CurrentFn = nullptr; return nullptr; } From 5de19af5037441c0c13bd7b1728cc7f9453da631 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:30 +0530 Subject: [PATCH 30/80] verify: Verify every function but those using a construct the verifier does not represent. --- clang/lib/Verify/Driver/Verifier.cpp | 65 +++++++++++++++++++++++++--- 1 file changed, 59 insertions(+), 6 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 6854f53d33..d9f0ad5f33 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -3081,13 +3081,33 @@ class Verifier { Converter.getUnverifiedCallers(); for (const auto &[Loc, Message] : Converter.getWarnings()) Diags.push_back({VerifyDiagnostic::Warning, Message, Loc}); + // A construct the verifier does not represent costs its function alone: + // the function is Unresolved, its first error carrying the verdict, and + // the rest of the translation unit is verified. An error outside every + // function stops the run. + bool OutsideFunctions = false; + std::map UnsupportedConstructs; for (const ConversionError &Err : Converter.getErrors()) { VerifyDiagnostic D{VerifyDiagnostic::Error, Err.Message, Err.Range.getBegin()}; D.Span = Err.Range; + if (Err.Function.empty()) + OutsideFunctions = true; + else + D.FunctionName = Err.FunctionName; + if (!Err.Function.empty() && + UnsupportedConstructs.emplace(Err.Function, Err.Message).second) { + VerifyResult R; + R.Status = VerifyStatus::Unresolved; + R.Reason = VerifyReason::UnsupportedConstruct; + R.Message = Err.Message; + D.Result = std::move(R); + } Diags.push_back(std::move(D)); } - if (!Converter.getErrors().empty()) + if (OutsideFunctions) + return false; + if (Functions.empty() && !UnsupportedConstructs.empty()) return false; if (Functions.empty()) { if (Opts.LeanCertify) { @@ -3213,7 +3233,7 @@ class Verifier { }; const unsigned DumpLayers = Opts.DumpIRLayers; const bool MultiLayerDump = llvm::popcount(DumpLayers) > 1; - bool AllOk = true; + bool AllOk = UnsupportedConstructs.empty(); bool AnyFailed = false; std::set FailedCallers; // A spec whose termination is not established has no definition, so a @@ -3562,12 +3582,35 @@ class Verifier { // which is reported only if it fails. if (Fn->Uninterpreted || (Fn->IsBuiltin && !Fn->NeedsDecreasesCheck)) continue; + // What a function says depends on the definitions of the specs it + // reaches, so one that reaches a spec the verifier does not + // represent is not verified. + std::string ReliesOn; + for (const std::string &Spec : Fn->SpecDependencies) + if (auto It = FnMap.find(Spec); + It != FnMap.end() && It->second->UnsupportedConstruct) + ReliesOn += (ReliesOn.empty() ? "" : ", ") + It->second->Name; + if (!ReliesOn.empty()) { + AllOk = false; + VerifyResult R; + R.Status = VerifyStatus::Unresolved; + R.Reason = VerifyReason::UnsupportedConstruct; + R.Message = "relies on " + ReliesOn + + ", which uses a construct the verifier does not support"; + VerifyDiagnostic D{VerifyDiagnostic::Unresolved, + Fn->Name + " [reason=construct.unsupported] (" + + R.Message + ")", + Fn->DeclLoc, Fn->Name}; + D.Result = std::move(R); + Diags.push_back(std::move(D)); + continue; + } if (Fn->IsExternalContract) { if (Fn->IsTrusted) Diags.push_back({VerifyDiagnostic::Trusted, Fn->Name + " (contract assumed, not verified)", Fn->DeclLoc, Fn->Name}); - else + else if (!Fn->UnsupportedConstruct) Diags.push_back( {VerifyDiagnostic::Warning, Fn->Name + " has a contract but no definition, so its callers " @@ -4921,6 +4964,8 @@ class Verifier { auto Check = ContractChecks.find(Callee); if (Check != ContractChecks.end() && !settled(Check->second)) Names += " (its clauses are not shown to be defined)"; + else if (It != FnMap.end() && It->second->UnsupportedConstruct) + Names += " (it uses a construct the verifier does not support)"; else if (It != FnMap.end() && It->second->IsExternalContract && !It->second->IsTrusted) Names += " (no definition; mark it [[cppverify::trusted]] to " @@ -4955,9 +5000,12 @@ class Verifier { continue; // Definitions and frames of what the proof may reach; // postconditions and unfoldings where its module assumes them. - std::string Undefined, Unframed, Unproven, Unruled; + std::string Unsupported, Undefined, Unframed, Unproven, Unruled; for (const std::string &Identity : Reliance.Specs) { - if (UndefinedSpecs.count(Identity)) + if (auto It = FnMap.find(Identity); + It != FnMap.end() && It->second->UnsupportedConstruct) + list(Unsupported, nameOf(Identity)); + else if (UndefinedSpecs.count(Identity)) list(Undefined, nameOf(Identity)); else if (UnframedSpecs.count(Identity)) list(Unframed, nameOf(Identity)); @@ -4974,7 +5022,12 @@ class Verifier { for (const std::string &Identity : Reliance.AssumedUnfoldings) if (Unproved.count(Identity) && !Reliance.Withheld.count(Identity)) list(Unruled, nameOf(Identity)); - if (!Undefined.empty()) + if (!Unsupported.empty()) + demote(Reliance.Index, VerifyReason::UnsupportedConstruct, + "relies on " + Unsupported + + ", which uses a construct the verifier does not " + "support"); + else if (!Undefined.empty()) demote(Reliance.Index, VerifyReason::SpecTermination, "relies on the definition of " + Undefined + ", whose termination is not established"); From f96eed0228fc4d10c9ced22d46b2733d6ec63cb7 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:30 +0530 Subject: [PATCH 31/80] test: Check the verdict that an unsupported construct's record carries. --- clang/test/Verify/located_errors.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/clang/test/Verify/located_errors.cpp b/clang/test/Verify/located_errors.cpp index 9f8a43b940..0db71d256a 100644 --- a/clang/test/Verify/located_errors.cpp +++ b/clang/test/Verify/located_errors.cpp @@ -4,7 +4,7 @@ // // An error about source the verifier cannot represent points at that source, // with its line and a caret, as a compiler error does, and its JSON record -// carries the range. +// carries the range and the verdict of the function it is in. namespace cv = cppverify; @@ -16,7 +16,7 @@ int pick(int x) // CHECK: {{.*}}located_errors.cpp:[[@LINE-2]]:3: error: pick: unsupported statement: SwitchStmt // CHECK-NEXT: {{^ +}}[[@LINE-3]] | switch (x) { case 1: return 1; default: return 0; } // CHECK-NEXT: {{^ +}}| ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -// JSON: {"message":"pick: unsupported statement: SwitchStmt","schema":"cppverify.diagnostic/1","severity":"error","source":{"column":3,"end_column":53,"end_line":[[#@LINE-5]],"file":"{{.*}}located_errors.cpp","line":[[#@LINE-5]]},"status":"error"} +// JSON: {"function":"pick","message":"pick: unsupported statement: SwitchStmt","reason":"construct.unsupported","schema":"cppverify.diagnostic/1","severity":"error","source":{"column":3,"end_column":53,"end_line":[[#@LINE-5]],"file":"{{.*}}located_errors.cpp","line":[[#@LINE-5]]},"status":"unresolved"} struct Counter { int get(int x) { cv::check(x >= 0 || x < 0); return x; } @@ -50,3 +50,4 @@ int down(int n) // CHECK: {{.*}}located_errors.cpp:[[@LINE-8]]:5: error: down: recursive executable functions require decreases, or cppverify::decreases(*) to allow divergence // CHECK-NEXT: {{^ +}}[[@LINE-9]] | int down(int n) // CHECK-NEXT: {{^ +}}| ^~~~ +// JSON: {"function":"down","message":"down: recursive executable functions require decreases, or cppverify::decreases(*) to allow divergence","reason":"construct.unsupported",{{.*}}"status":"unresolved"} From 80eb0e4efa61a6b8ab7e7898f8edf489cc7ec02c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:31 +0530 Subject: [PATCH 32/80] test: Add the program of the per-function errors test. --- .../suite/Inputs/per_function_errors.cpp | 108 ++++++++++++++++++ 1 file changed, 108 insertions(+) create mode 100644 clang/test/Verify/suite/Inputs/per_function_errors.cpp diff --git a/clang/test/Verify/suite/Inputs/per_function_errors.cpp b/clang/test/Verify/suite/Inputs/per_function_errors.cpp new file mode 100644 index 0000000000..97a1f30df2 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/per_function_errors.cpp @@ -0,0 +1,108 @@ +// Functions the verifier cannot represent, beside ones it can, for +// per_function_errors.test. + +int table[4] = {1, 2, 3, 4}; + +// A statement the verifier does not represent: pick is not verified, and its +// caller relies on its contract. +int pick(int x) + cppverify::post(cppverify::result >= 1) +{ + switch (x) { + case 0: + return 1; + default: + return 2; + } +} + +int uses_pick(int x) + cppverify::post(cppverify::result >= 1) +{ + return pick(x); +} + +// A contract the verifier does not represent leaves no contract to rely on. +int lookup(int i) + cppverify::pre(0 <= i && i < 4 && table[i] > 0) + cppverify::post(cppverify::result >= 0) +{ + return 1; +} + +int uses_lookup() + cppverify::post(cppverify::result >= 0) +{ + return lookup(1); +} + +// A spec the verifier does not represent: what reaches it is not verified. +cppverify::spec int choice(int x) { + switch (x) { + case 0: + return 1; + default: + return 2; + } +} + +int uses_choice(int x) + cppverify::post(cppverify::result == x || choice(x) > 0) +{ + return x; +} + +cppverify::proof void choice_lemma(int x) + cppverify::post(choice(x) == choice(x)) +{ +} + +// A lemma whose body the verifier does not represent. +cppverify::proof void zero_lemma(int x) + cppverify::post(x * 0 == 0) +{ + switch (x) { + default: + break; + } +} + +int uses_zero_lemma(int x) + cppverify::post(cppverify::result == 0) +{ + cppverify::ghost { zero_lemma(x); } + return 0; +} + +// An uncontracted constexpr helper, lifted for its caller. +constexpr int step(int x) { + switch (x) { + case 0: + return 1; + default: + return 2; + } +} + +int uses_step(int x) + cppverify::post(cppverify::result >= 1) +{ + return step(x); +} + +// The functions the verifier represents are verified as before. +int inc(int x) + cppverify::pre(x < 100) + cppverify::post(cppverify::result == x + 1) +{ + return x + 1; +} + +cppverify::spec int twice(int x) { return x + x; } + +int uses_twice(int x) + cppverify::pre(0 <= x && x < 100) + cppverify::post(cppverify::result == twice(x)) +{ + return x + x; +} From 10dba84ad4ee556d5a69368ef77d993f31015b43 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:31 +0530 Subject: [PATCH 33/80] test: Check that an unsupported construct costs its function alone. --- .../Verify/suite/per_function_errors.test | 51 +++++++++++++++++++ 1 file changed, 51 insertions(+) create mode 100644 clang/test/Verify/suite/per_function_errors.test diff --git a/clang/test/Verify/suite/per_function_errors.test b/clang/test/Verify/suite/per_function_errors.test new file mode 100644 index 0000000000..eb04759f06 --- /dev/null +++ b/clang/test/Verify/suite/per_function_errors.test @@ -0,0 +1,51 @@ +# A construct the verifier does not represent costs its function alone. The +# function is reported where the construct is, and its JSON record carries its +# verdict, Unresolved with construct.unsupported; every other function is +# verified. A caller relies on the function's contract, which nothing +# establishes (callee.contract); a call of a function whose contract did not +# convert is unsupported where it is; a function that reaches a spec the +# verifier does not represent is not verified. +# +# RUN: not %cpp-verify %S/Inputs/per_function_errors.cpp -- 2>&1 \ +# RUN: | FileCheck %s --check-prefix=TEXT +# RUN: not %cpp-verify --diagnostics-format=json %S/Inputs/per_function_errors.cpp -- 2>/dev/null \ +# RUN: | FileCheck %s --check-prefix=JSON +# +# The same with BMC, and in a Lean export, which exports what it can. +# RUN: not %cpp-verify --backend=bmc --unroll=1 %S/Inputs/per_function_errors.cpp -- 2>&1 \ +# RUN: | FileCheck %s --check-prefix=BMC +# RUN: not %cpp-verify --backend=lean --lean-out=%t.lean %S/Inputs/per_function_errors.cpp -- 2>&1 \ +# RUN: | FileCheck %s --check-prefix=LEAN + +TEXT: per_function_errors.cpp:11:3: error: pick: unsupported statement: SwitchStmt +TEXT: per_function_errors.cpp:27:37: error: lookup: the global array 'table' is unsupported +TEXT: per_function_errors.cpp:41:3: error: choice: unsupported statement: SwitchStmt +TEXT: per_function_errors.cpp:64:3: error: zero_lemma: unsupported statement: SwitchStmt +TEXT: per_function_errors.cpp:79:3: error: step: unsupported statement: SwitchStmt +TEXT-NOT: {{(Verified|Unresolved): (spec [a-z]+: )?(pick|lookup|choice|zero_lemma|step) }} +TEXT: Unresolved: uses_pick [backend=z3] [reason=callee.contract] (relies on the contract of pick (it uses a construct the verifier does not support), which is not established) +TEXT-NEXT: per_function_errors.cpp:36:3: Unresolved: uses_lookup [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: a call of lookup, whose contract is not available) +TEXT-NEXT: per_function_errors.cpp:49:5: Unresolved: uses_choice [reason=construct.unsupported] (relies on choice, which uses a construct the verifier does not support) +TEXT-NEXT: per_function_errors.cpp:55:23: Unresolved: choice_lemma [reason=construct.unsupported] (relies on choice, which uses a construct the verifier does not support) +TEXT-NEXT: Unresolved: uses_zero_lemma [backend=z3] [reason=callee.contract] (relies on the contract of zero_lemma (it uses a construct the verifier does not support), which is not established) +TEXT-NEXT: per_function_errors.cpp:87:5: Unresolved: uses_step [reason=construct.unsupported] (relies on step, which uses a construct the verifier does not support) +TEXT-NEXT: Verified: inc [backend=z3] +TEXT-NEXT: Verified: spec axiom: twice +TEXT-NEXT: Verified: uses_twice [backend=z3] +TEXT-NOT: {{.}} + +JSON: {"function":"pick","message":"pick: unsupported statement: SwitchStmt","reason":"construct.unsupported",{{.*}}"line":11},"status":"unresolved"} +JSON: {"function":"lookup","message":"lookup: the global array 'table' is unsupported","reason":"construct.unsupported",{{.*}}"status":"unresolved"} +JSON-NEXT: {"function":"lookup","message":"lookup: unsupported expression in pre",{{.*}}"status":"error"} +JSON: {"backend":"z3","function":"uses_pick",{{.*}}"reason":"callee.contract",{{.*}}"status":"unresolved"} +JSON: {"backend":"z3","function":"inc",{{.*}}"status":"verified"} + +BMC: Unresolved: uses_pick [backend=bmc, bound=0] [reason=callee.contract] +BMC: Verified: inc [backend=bmc, bound=0] +BMC: Verified: uses_twice [backend=bmc, bound=0] + +LEAN: per_function_errors.cpp:11:3: error: pick: unsupported statement: SwitchStmt +LEAN: Exported: lean obligation: uses_pick +LEAN: per_function_errors.cpp:49:5: Unresolved: uses_choice [reason=construct.unsupported] +LEAN: Exported: lean obligation: inc +LEAN: Exported: lean obligation: uses_twice From a24894dbb035dee5f4d7192c46ec1d94dae4ded8 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:32 +0530 Subject: [PATCH 34/80] docs: Say that an unsupported construct costs its function alone. --- website/source/language/tooling.rst | 48 +++++++++++++++++++++++++---- 1 file changed, 42 insertions(+), 6 deletions(-) diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index e26a16a7d9..d5a127198f 100644 --- a/website/source/language/tooling.rst +++ b/website/source/language/tooling.rst @@ -72,8 +72,10 @@ printed ``error: invalid argument '-std=c++17' not allowed with 'C'``. A construct that cpp-verify does not represent yet, in a function it verifies, is an error at that construct, shown with its line and a caret as a -compiler error is. Like a compiler error it stops the file: no function of -the file gets a verdict (:doc:`limitations` lists what is not represented). +compiler error is. It costs that function alone: the function is +``Unresolved`` with reason ``construct.unsupported``, every other function of +the file is verified, and ``cpp-verify`` exits with status 1 +(:doc:`limitations` lists what is not represented). .. cppverify-example: rejects @@ -85,17 +87,51 @@ the file gets a verdict (:doc:`limitations` lists what is not represented). switch (x) { case 1: return 1; default: return 0; } } + int bump(int x) + cv::pre(x < 100) + cv::post(cv::result == x + 1) + { + return x + 1; + } + + int picked(int x) + cv::post(cv::result >= 0) + { + int r = pick(x); + return r; + } + .. code-block:: text pick.cpp:4:3: error: pick: unsupported statement: SwitchStmt 4 | switch (x) { case 1: return 1; default: return 0; } | ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + Verified: bump [backend=z3] + Unresolved: picked [backend=z3] [reason=callee.contract] (relies on the contract of pick (it uses a construct the verifier does not support), which is not established) + +What others may rely on stays: + +- a caller of an executable or proof function whose body is not represented + is verified against its contract, which nothing establishes, so it is + ``Unresolved`` with reason ``callee.contract``, as ``picked`` above; +- a function whose contract is not represented leaves nothing to rely on: a + call of it is ``construct.unsupported`` where it is (``a call of lookup, + whose contract is not available``); +- a spec whose body or contract is not represented has no definition, and a + function that reaches it, through its body, its contract, or a callee's + contract, is not verified: ``Unresolved`` with reason + ``construct.unsupported`` (``relies on choice, which uses a construct the + verifier does not support``). An uncontracted ``constexpr`` helper that + verified code calls is such a spec. An error about the function as a whole, such as a recursion without a -measure, points at its name. With ``--diagnostics-format=json`` the record -carries the range, here ``"source":{"column":3,"end_column":53,"end_line":4, -"file":"pick.cpp","line":4}``. Before 0.2 such an error named only the -function: ``error: pick: unsupported statement: SwitchStmt``. +measure, points at its name. With ``--diagnostics-format=json`` the record of +a function's first error carries its verdict and the range, here +``"function":"pick"``, ``"status":"unresolved"``, +``"reason":"construct.unsupported"``, and ``"source":{"column":3, +"end_column":53,"end_line":4,"file":"pick.cpp","line":4}``. Before 0.2 such an +error stopped the file, so that no function of it got a verdict, and named +only the function: ``error: pick: unsupported statement: SwitchStmt``. Stopping a run with Ctrl-C ~~~~~~~~~~~~~~~~~~~~~~~~~~ From 94c24f4873c9809e325df1c23bb96c46746dd44a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:32 +0530 Subject: [PATCH 35/80] docs: Describe failing closed per function in the limitations. --- website/source/language/limitations.rst | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 383e32a315..3b58f00f81 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -29,11 +29,15 @@ This page separates four different situations: return ``unknown``. Outside the supported subset the verifier *fails closed*: it never reports a -proof for what it does not model. Depending on the construct, the run stops -with an error that names it, and no function of the file gets a verdict, or -the function is ``Unresolved`` with reason ``construct.unsupported``. A -counterexample is never a way of failing closed: ``Failed`` always means a -checked counterexample. +proof for what it does not model. A construct it does not represent is an +error at the construct, and its function is ``Unresolved`` with reason +``construct.unsupported`` while every other function of the file is verified +(callers that rely on its contract are ``callee.contract``, and functions +that reach a spec it cannot represent are ``construct.unsupported`` too); one +it represents but does not model, such as a pointer difference between two +parameters' objects, makes the obligation that stands for it unsupported, and +the function is ``Unresolved`` with the same reason. A counterexample is never +a way of failing closed: ``Failed`` always means a checked counterexample. Meaning of a result ------------------- From 6898ea4fb859e820b835e3eb72110ffb08cf5d2a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:32 +0530 Subject: [PATCH 36/80] docs: Extend construct.unsupported to whole functions in chapter 16. --- .../book/part-ii/ch16-when-verification-fails.rst | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 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 40b383dfaa..e349049fa1 100644 --- a/website/source/book/part-ii/ch16-when-verification-fails.rst +++ b/website/source/book/part-ii/ch16-when-verification-fails.rst @@ -146,8 +146,10 @@ Every result that is not a proof carries one stable reason code (text - A loop has no termination measure. Add ``cppverify::decreases``, or ``cppverify::decreases(*)``. * - ``construct.unsupported`` - - The failed obligation stands for a construct the verifier does not - model; the message names it. + - The function uses a construct the verifier does not represent (an + error points at it), relies on a spec that does, or the failed + obligation stands for a construct it does not model; the message + names it. * - ``solver.timeout`` - A query, or the function's whole budget, ran out of time. Raise ``--timeout`` or ``--function-timeout``, or help the proof. @@ -214,7 +216,12 @@ Other results that are not counterexamples: - ``construct.unsupported``: the failed obligation stands for a construct the verifier does not model, so it says nothing about the program. The message names the construct, such as a pointer difference between two parameters' - objects or a call that keeps a pointer to local storage. + objects or a call that keeps a pointer to local storage. A function whose + body or contract the verifier does not represent at all gets this reason + too, with an error at the construct, and so does a function that relies on + a spec it does not represent (``relies on choice, which uses a construct + the verifier does not support``); the other functions of the file are + verified (see :doc:`../../language/tooling`). - ``[trusts=f]`` on a verified result: the proof relies on the contract of ``f``, marked ``[[cppverify::trusted]]`` (see :doc:`ch17-backends-modular-calls`). From e176567787a303d52e22794cba06c36a1717af95 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:33 +0530 Subject: [PATCH 37/80] docs: Note that an unsupported construct costs its function alone in the release notes. --- website/source/release-notes.rst | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index c615fa3d1e..c79f4204f3 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -308,6 +308,16 @@ SwitchStmt``. It now gives the file, line, and column, and shows the line with a caret under the construct, as a compiler error does; its JSON record carries the range (:doc:`language/tooling`). +**An unsupported construct costs its function alone.** One construct the +verifier does not represent, such as a ``switch``, stopped the file: no +function of it was verified. Now that function is ``Unresolved`` with reason +``construct.unsupported``, its first error's JSON record carrying the verdict, +and every other function is verified. A caller that relies on its contract is +``callee.contract``; a function whose contract is not represented leaves a +call of it ``construct.unsupported``; a function that reaches a spec the +verifier does not represent is ``construct.unsupported``. The exit status is 1 +as before (:doc:`language/tooling`). + **Z3 errors.** A Z3 call that failed went unnoticed, and a later step could report something unrelated. The query now ends ``Unresolved`` with reason ``encoding.failed`` and Z3's message (:doc:`language/tooling`). From 74951722cf9de65bb1815fa6f39d932b98f26f08 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:33 +0530 Subject: [PATCH 38/80] docs: Describe per-function unsupported constructs in the design. --- docs/DESIGN.md | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index cc5524ed61..3ebdc07ef9 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1497,7 +1497,16 @@ int safe_fib(int n) cppverify::pre(...) cppverify::post(cppverify::result == fib the verifier does not model, so its counterexample says nothing about the program; the message names the construct (for example "the operands of this pointer difference may address the objects of different parameters - or globals, which may be one caller array"). + or globals, which may be one caller array"). A function whose body or + contract uses a construct the verifier does not represent at all has this + verdict too, with the error at the construct, and costs that function + alone, as Prusti reports an unsupported feature and Kani a construct it + does not translate: every other function is verified. What others may + rely on stays: a caller verifies against the function's contract, which + nothing establishes (`callee.contract`); a call of a function whose + contract is not represented is unsupported where it is; a function that + reaches a spec the verifier does not represent, which keeps only its + declaration, is not verified (`construct.unsupported`). - Qualifiers: `[partial]` (proved for terminating executions only, after `cppverify::decreases(*)`), `[trusts=f]` (relies on the contract of `f`, marked `[[cppverify::trusted]]`), `[vacuous]` (no execution reaches the claim). From faa6c01fdf72250a48eb46c0896a0017b322a56a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 06:52:33 +0530 Subject: [PATCH 39/80] docs: Describe per-function conversion errors in the architecture. --- docs/ARCHITECTURE.md | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 5002ca77de..1389282dcf 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -2015,7 +2015,22 @@ caret included, as a compiler error is, and its JSON record carries the range. ## Modular Verification Protocol -1. Build VFunction for each function in source order. +1. Build VFunction for each function in source order. An error of the + converter belongs to the function it is raised in (`ConversionError:: + Function`), and to its signature or contract (`InContract`) or its body; + the errors that passes after conversion find about a function (a recursion + without a measure, a malformed inductive predicate) belong to it too + (`errorOf`). Such a function keeps what others may rely on + (`markUnsupported`, `VFunction::UnsupportedConstruct`): an executable or + proof function whose contract converted becomes an external contract, its + body not verified, and one whose contract did not is left out, so a call + of it is an `unsupported` obligation; a spec becomes a declaration without + definition, postconditions, reads, or domain. The driver prints every + error, gives the first of each function its verdict (`Unresolved`, + `construct.unsupported`), reports a function whose `SpecDependencies` + reach an unsupported spec the same way without verifying it, and verifies + the rest; the fixpoint demotes callers of the external contracts + (`callee.contract`). Only an error of no function stops the run. 2. For each VFunction: a. Build Layer 1 IR. b. Passivize to Layer 2 (SSA + havoc/assume/assert + heap versioning). From e6bf536ced124d7a6f31127d639fd9e0776bbbd4 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 07:59:45 +0530 Subject: [PATCH 40/80] verify: Keep only scalar reference parameters as footprints of one cell. --- clang/lib/Verify/IR/VStmt.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/clang/lib/Verify/IR/VStmt.h b/clang/lib/Verify/IR/VStmt.h index 6db19ef883..816f9f6910 100644 --- a/clang/lib/Verify/IR/VStmt.h +++ b/clang/lib/Verify/IR/VStmt.h @@ -419,7 +419,10 @@ struct VFunction { std::set RevealedSpecs; std::vector> Params; std::map SourceVariables; - std::set ReferenceParams; + /// Reference parameters to a scalar, whose `modifies(r)` is the one cell + /// they bind (perhaps a field of a larger object). A reference to a record + /// is a pointer to it, and `modifies(r)` its object. + std::set ScalarReferenceParams; /// Pointer and reference parameters to const objects: the function /// writes nothing through them. std::set ConstAddressParams; From 69c1fcc4cfe5b2b2b312281ca19fac417f2d9e93 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 07:59:45 +0530 Subject: [PATCH 41/80] verify: Clone a function's scalar reference parameters. --- clang/lib/Verify/IR/VStmt.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang/lib/Verify/IR/VStmt.cpp b/clang/lib/Verify/IR/VStmt.cpp index 687197e9ff..88f5970470 100644 --- a/clang/lib/Verify/IR/VStmt.cpp +++ b/clang/lib/Verify/IR/VStmt.cpp @@ -197,7 +197,7 @@ VFunction verify::cloneVFunction(const VFunction &Fn) { Out.RevealedSpecs = Fn.RevealedSpecs; Out.Params = Fn.Params; Out.SourceVariables = Fn.SourceVariables; - Out.ReferenceParams = Fn.ReferenceParams; + Out.ScalarReferenceParams = Fn.ScalarReferenceParams; Out.ConstAddressParams = Fn.ConstAddressParams; Out.BoundedPointers = Fn.BoundedPointers; Out.ReturnFields = Fn.ReturnFields; From b504ed449ba7638ba400510997215ccea6200709 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 07:59:46 +0530 Subject: [PATCH 42/80] verify: Keep a function's scalar reference parameters through loop unrolling. --- clang/lib/Verify/Transform/LoopUnroll.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/clang/lib/Verify/Transform/LoopUnroll.cpp b/clang/lib/Verify/Transform/LoopUnroll.cpp index 1f6bd7d3a3..80c2dc5254 100644 --- a/clang/lib/Verify/Transform/LoopUnroll.cpp +++ b/clang/lib/Verify/Transform/LoopUnroll.cpp @@ -255,7 +255,7 @@ VFunction LoopUnroller::unroll(const VFunction &Fn, unsigned K) { Out.FreshOwnedReturn = Fn.FreshOwnedReturn; Out.Params = Fn.Params; Out.SourceVariables = Fn.SourceVariables; - Out.ReferenceParams = Fn.ReferenceParams; + Out.ScalarReferenceParams = Fn.ScalarReferenceParams; Out.ConstAddressParams = Fn.ConstAddressParams; Out.BoundedPointers = Fn.BoundedPointers; Out.ReturnFields = Fn.ReturnFields; From 49ecde6d45f0ca89ebc9d4a6b7a773caa8dec9d5 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 07:59:46 +0530 Subject: [PATCH 43/80] verify: Frame a record reference's footprint as its object, and name the address passed to a callee. --- clang/lib/Verify/Transform/Passivize.cpp | 30 +++++++++++++----------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp index b416922e30..e41db3316c 100644 --- a/clang/lib/Verify/Transform/Passivize.cpp +++ b/clang/lib/Verify/Transform/Passivize.cpp @@ -1680,8 +1680,9 @@ samePointerDifferenceOrigin(const VExpr *L, const VExpr *R, /// Whether a footprint is the whole object its pointer addresses, rather /// than one cell or a range of cells. -static bool isRegionFootprint(const VFootprint &F, - const std::set &ReferenceParams) { +static bool +isRegionFootprint(const VFootprint &F, + const std::set &ScalarReferenceParams) { if (F.Count) return false; const VExpr *E = F.Target.get(); @@ -1691,7 +1692,7 @@ static bool isRegionFootprint(const VFootprint &F, while (Ptr && Ptr->K == VExpr::Cast) Ptr = static_cast(Ptr)->Inner.get(); if (Ptr && Ptr->K == VExpr::Var && - ReferenceParams.count(static_cast(Ptr)->Name)) + ScalarReferenceParams.count(static_cast(Ptr)->Name)) return false; return !Ptr || Ptr->K == VExpr::Var; } @@ -1700,7 +1701,7 @@ static bool hasUnboundedExtentWrite(const VFunction &Fn, const std::string &Base) { for (const VFootprint &Modify : Fn.Modifies) { if (!Modify.Target || Modify.Target->K != VExpr::Load || - !isRegionFootprint(Modify, Fn.ReferenceParams)) + !isRegionFootprint(Modify, Fn.ScalarReferenceParams)) continue; const VExpr *Ptr = pointerBase( static_cast(Modify.Target.get())->Ptr.get()); @@ -3548,7 +3549,7 @@ class PassivizerImpl { std::vector Out; for (const VFootprint &F : W.Modifies) { const auto *Load = static_cast(F.Target.get()); - if (isRegionFootprint(F, Fn.ReferenceParams)) { + if (isRegionFootprint(F, Fn.ScalarReferenceParams)) { auto R = rootRegion(addressRoot(Load->Ptr.get()), Renames, Load->Loc); if (!R) return std::nullopt; @@ -3648,7 +3649,7 @@ class PassivizerImpl { Out.push_back(rangeBytes(Ptr.get(), Count.get(), M.ElementSize, Loc)); continue; } - if (isRegionFootprint(M, Fn.ReferenceParams)) { + if (isRegionFootprint(M, Fn.ScalarReferenceParams)) { auto R = rootRegion(addressRoot(Load->Ptr.get()), Renames, Loc); if (!R) return false; @@ -3715,7 +3716,7 @@ class PassivizerImpl { TargetPtr = static_cast(TargetPtr)->Inner.get(); const bool OneCell = !M.Count && TargetPtr == CalleeRoot && - (!isRegionFootprint(M, Callee->ReferenceParams) || + (!isRegionFootprint(M, Callee->ScalarReferenceParams) || (Callee->ObjectModel && (Target->Ty.isInt() || Target->Ty.Kind == VTypeKind::Bool || Target->Ty.Kind == VTypeKind::Ptr) && @@ -4904,7 +4905,7 @@ class PassivizerImpl { const VFootprint &Declared = Callee.Modifies[I]; if (Count) return rangeBytes(Actual->Ptr.get(), Count, Declared.ElementSize, Loc); - if (!isRegionFootprint(Declared, Callee.ReferenceParams)) + if (!isRegionFootprint(Declared, Callee.ScalarReferenceParams)) return cellRegion(Actual->Ptr.get(), Actual->Ty, Loc); if (!Callee.ObjectModel) return std::nullopt; @@ -4949,7 +4950,8 @@ class PassivizerImpl { for (size_t I = 0; I < ActualModifies.size(); ++I) if (!ActualModifies[I] || ActualModifies[I]->K != VExpr::Load || ActualCounts[I] || - (isRegionFootprint(Callee.Modifies[I], Callee.ReferenceParams) && + (isRegionFootprint(Callee.Modifies[I], + Callee.ScalarReferenceParams) && !hasPointerProvenance( static_cast(ActualModifies[I].get()) ->Ptr.get()))) @@ -5055,7 +5057,7 @@ class PassivizerImpl { ActiveScans)) { emitPassive(P, PassiveStmt::Assert, makeBoolLiteral(false, C.Loc), nullptr, C.Loc, ProofObligationKind::Unsupported, - "a pointer to local or dynamic storage is passed to " + + "the address of local or dynamic storage is passed to " + C.Callee + ", which may keep, offset, or free it, or has no " "verified body"); @@ -5344,8 +5346,8 @@ class PassivizerImpl { ? static_cast(M.get()) : nullptr; if (ActualLoad) { - const bool ActualIsRegion = - isRegionFootprint(Callee->Modifies[I], Callee->ReferenceParams); + const bool ActualIsRegion = isRegionFootprint( + Callee->Modifies[I], Callee->ScalarReferenceParams); if (auto Provenance = pointerProvenance(ActualLoad->Ptr.get())) for (const std::string &Identity : OwnedAllocationIdentities) Allowed = makeOr(std::move(Allowed), @@ -5375,7 +5377,7 @@ class PassivizerImpl { OuterBytes = rangeBytes(CallerLoad->Ptr.get(), CallerCounts[J].get(), Fn.Modifies[J].ElementSize, C.Loc); const bool OuterIsRegion = - isRegionFootprint(Fn.Modifies[J], Fn.ReferenceParams); + isRegionFootprint(Fn.Modifies[J], Fn.ScalarReferenceParams); Allowed = makeOr( std::move(Allowed), footprintWithin(CallerLoad->Ptr.get(), OuterIsRegion, OuterBytes, @@ -5624,7 +5626,7 @@ class PassivizerImpl { St.Loc); } auto EffectivePtr = resolveReferenceAddress(Ptr.get()); - const bool Region = isRegionFootprint(M, Fn.ReferenceParams); + const bool Region = isRegionFootprint(M, Fn.ScalarReferenceParams); Allowed = makeOr( std::move(Allowed), footprintWithin(DeclaredPtr.get(), Region, Bytes, From 7825fcb13b5af802dc217ff94a11d8aaf1929d82 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 07:59:47 +0530 Subject: [PATCH 44/80] verify: Declare the places and pointers reached through references to records. --- clang/lib/Verify/Frontend/ASTConverter.h | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index 152d0d48c4..e1eb288972 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.h +++ b/clang/lib/Verify/Frontend/ASTConverter.h @@ -150,7 +150,8 @@ class ASTConverter { const Expr *Cond); bool isTriggerMarked(const Expr *E) const; void markTrigger(std::unique_ptr &Result, const Expr *E); - /// A modifies footprint: an lvalue, or the cells p[lo : n]. + /// A modifies footprint: an lvalue, the cells p[lo : n], or the bytes of a + /// record or array inside an object. std::optional convertFootprint(const Expr *E); /// A loop's declared footprints, each naming memory. std::vector convertLoopFootprints(const LoopContractInfo &LCI); @@ -188,6 +189,16 @@ class ASTConverter { /// object. Returns the root only when it was promoted to one automatic /// byte-addressed object. const VarDecl *promotedRootLocal(const Expr *E) const; + /// The reference parameter or local whose record \p E selects a field or + /// element of (or is), if any. + const VarDecl *recordReferenceRoot(const Expr *E) const; + /// Whether \p E is a place in an object reached through a pointer or a + /// reference, rather than a value of the function's own. + bool inPointeeObject(const Expr *E) const; + /// Whether a pointer may be formed into the place \p E (its address, or a + /// decayed member array): a place in an object that outlives the function, + /// reached through a pointer or a reference to a record. + bool subobjectPointerRoot(const Expr *E) const; /// The pointer whose pointee a chain of field and fixed-array element /// selections starts at (p in *p, p->m, p[k], (*p).a.b[i]); null when the /// chain does not start at a pointee. From 959018e1a0cb31b993c86fc101a904fe910bb64a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 07:59:48 +0530 Subject: [PATCH 45/80] verify: Verify records through references, as pointers never null or reseated, and members named whole in modifies as their bytes. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 97 ++++++++++++++++++---- 1 file changed, 79 insertions(+), 18 deletions(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index e04ac734fa..795f625d8f 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -609,6 +609,16 @@ static bool isSupportedScalarLValueReference(QualType Ty) { Referent->isEnumeralType(); } +/// A reference to a record is a pointer that is never null and never +/// reseated, so it is supported where a pointer to the record is (not to a +/// volatile one): its fields and elements are places in the object it names. +static bool isSupportedRecordLValueReference(QualType Ty, ASTContext &Ctx) { + return !Ty.isNull() && Ty->isLValueReferenceType() && + Ty.getNonReferenceType()->isRecordType() && + isSupportedVerificationType( + Ctx.getPointerType(Ty.getNonReferenceType())); +} + static std::optional findUnsupportedType(const FunctionDecl *FD, bool AllowScalarReferences) { // By-value records keep their flattened SSA representation, so only records @@ -624,7 +634,9 @@ findUnsupportedType(const FunctionDecl *FD, bool AllowScalarReferences) { for (const ParmVarDecl *Param : FD->parameters()) { QualType Ty = Param->getType(); if (Ty->isReferenceType()) { - if (!AllowScalarReferences || !isSupportedScalarLValueReference(Ty)) + if (!AllowScalarReferences || + !(isSupportedScalarLValueReference(Ty) || + isSupportedRecordLValueReference(Ty, FD->getASTContext()))) return Ty.getAsString(); } else if (UnsupportedValueType(Ty)) { return Param->getType().getAsString(); @@ -653,7 +665,8 @@ findUnsupportedType(const FunctionDecl *FD, bool AllowScalarReferences) { return false; QualType Ty = D->getType(); if (Ty->isReferenceType() && AllowScalarReferences && - isSupportedScalarLValueReference(Ty) && + (isSupportedScalarLValueReference(Ty) || + isSupportedRecordLValueReference(Ty, D->getASTContext())) && (isa(D) || D->hasLocalStorage())) return true; if (!isSupportedVerificationType(Ty)) @@ -1003,11 +1016,12 @@ static bool exprReferencesSpecCall(const VExpr *E, const std::string &Name) { } static const RecordDecl *getRecordFromType(QualType T) { - // See through references: a `C&`/`const C&` parameter's field access lowers - // to the same "param.field" variable as a by-value `C`, so type_invariant - // injection applies. Pointers are intentionally excluded: `p->field` lowers - // to a heap Load, which the "param.field" substitution does not model. - T = T.getNonReferenceType().getUnqualifiedType(); + // A record by value, whose fields are values of its own ("param.field"). + // A reference to a record is an address, as a pointer is: its fields are + // places in the object it names. + if (T->isReferenceType()) + return nullptr; + T = T.getUnqualifiedType(); // A cppverify collection is one mathematical value, not a record of fields. if (VType::collectionKind(T)) return nullptr; @@ -1170,10 +1184,10 @@ ASTConverter::convertPointerDifferenceOperand(const Expr *E, const Expr *Peeled = E->IgnoreParens(); if (const auto *Decay = dyn_cast(Peeled); Decay && Decay->getCastKind() == CK_ArrayToPointerDecay && - pointeeRootPointer(Decay->getSubExpr())) + subobjectPointerRoot(Decay->getSubExpr())) return convertExpr(Peeled); if (const auto *U = dyn_cast(Peeled); - U && U->getOpcode() == UO_AddrOf && pointeeRootPointer(U->getSubExpr())) + U && U->getOpcode() == UO_AddrOf && subobjectPointerRoot(U->getSubExpr())) return convertExpr(Peeled); E = E->IgnoreParenImpCasts(); if (const auto *DRE = dyn_cast(E)) @@ -2716,8 +2730,8 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { SmallVector AddressParams; for (const ParmVarDecl *P : FD->parameters()) { - if (P->getType()->isReferenceType()) - Fn->ReferenceParams.insert(valueName(P)); + if (isSupportedScalarLValueReference(P->getType())) + Fn->ScalarReferenceParams.insert(valueName(P)); if ((P->getType()->isPointerType() || P->getType()->isReferenceType()) && !isMutableAddressParam(P)) Fn->ConstAddressParams.insert(valueName(P)); @@ -3141,6 +3155,24 @@ std::optional ASTConverter::convertFootprint(const Expr *E) { if (!Out.Count) Out.Target.reset(); } + } else if (const Expr *Inner = E->IgnoreParens(); + (isa(Inner) || isa(Inner)) && + (Inner->getType()->isRecordType() || + Inner->getType()->isConstantArrayType()) && + inPointeeObject(Inner)) { + // A record or array inside an object (p->inner, r.buf, p[k]) is its + // bytes, a range of one element of its size; *p and a reference to a + // record name their whole object. + if (auto Place = objectPlace(Inner)) { + Out.Target = std::make_unique( + Place->takeAddress(), + VType::fromQualType(Inner->getType(), IntMode, Ctx), + Inner->getExprLoc(), "", Place->takeAccessCondition()); + Out.Count = std::make_unique( + 1, VType::fromQualType(Ctx.IntTy, IntMode, Ctx), Inner->getExprLoc()); + Out.ElementSize = static_cast( + Ctx.getTypeSizeInChars(Inner->getType()).getQuantity()); + } } else { Out.Target = convertExpr(E); } @@ -3382,7 +3414,7 @@ ASTConverter::subscriptPlace(const ArraySubscriptExpr *AS) { return std::nullopt; // An element of a fixed array inside a represented object: a promoted // local, or the object a pointer addresses (r->buf[i], p[k].grid[i][j]). - if (promotedRootLocal(AS) || pointeeRootPointer(AS->getBase())) + if (promotedRootLocal(AS) || inPointeeObject(AS->getBase())) return objectPlace(AS); return pointerElementPlace(AS); } @@ -3498,6 +3530,28 @@ const VarDecl *ASTConverter::promotedRootLocal(const Expr *E) const { return VD && AddressableLocals.count(VD) ? VD : nullptr; } +const VarDecl *ASTConverter::recordReferenceRoot(const Expr *E) const { + const VarDecl *VD = selectionRootVar(E); + return VD && (isa(VD) || VD->hasLocalStorage()) && + VD->getType()->isLValueReferenceType() && + VD->getType().getNonReferenceType()->isRecordType() + ? VD + : nullptr; +} + +bool ASTConverter::inPointeeObject(const Expr *E) const { + return pointeeRootPointer(E) || recordReferenceRoot(E); +} + +bool ASTConverter::subobjectPointerRoot(const Expr *E) const { + if (pointeeRootPointer(E)) + return true; + // A local reference bound to local or dynamic storage names an object + // whose lifetime a pointer formed from it would not carry. + const VarDecl *VD = recordReferenceRoot(E); + return VD && !LocalReferenceProvenanceVariables.count(VD); +} + std::string ASTConverter::arrayDecayError(const Expr *Array) const { const auto *M = dyn_cast_or_null(peelObjectExpr(Array)); const std::string Member = @@ -3662,6 +3716,9 @@ std::optional ASTConverter::objectPlace(const Expr *E) { if (const auto *DRE = dyn_cast(E)) { const auto *VD = dyn_cast(DRE->getDecl()); + // The object a reference to a record names, as *p for a pointer. + if (VD && recordReferenceRoot(E)) + return lvaluePlace(E); if (!VD || !AddressableLocals.count(VD)) return std::nullopt; return automaticLocalPlace(VD, E->getExprLoc()); @@ -3947,6 +4004,9 @@ std::optional ASTConverter::lvaluePlace(const Expr *E) { // rooted in it is an exact byte offset from its single automatic object. if (promotedRootLocal(E)) return objectPlace(E); + // A subobject of the record a reference names: c.f, c.buf[i]. + if (recordReferenceRoot(E) && !isa(E)) + return objectPlace(E); if (const auto *DRE = dyn_cast(E)) { const auto *VD = dyn_cast(DRE->getDecl()); @@ -4713,7 +4773,7 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { return convertExpr(MTE->getSubExpr()); if (const auto *Decay = dyn_cast(E); Decay && Decay->getCastKind() == CK_ArrayToPointerDecay) { - if (pointeeRootPointer(Decay->getSubExpr())) + if (subobjectPointerRoot(Decay->getSubExpr())) return subobjectPointer(E, Decay->getSubExpr(), /*AddressOf=*/false); error(CurrentFn->Name + ": " + arrayDecayError(Decay->getSubExpr())); return nullptr; @@ -4893,7 +4953,7 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { } if (const auto *U = dyn_cast(E)) { if (U->getOpcode() == UO_AddrOf) { - if (pointeeRootPointer(U->getSubExpr())) + if (subobjectPointerRoot(U->getSubExpr())) return subobjectPointer(E, U->getSubExpr(), /*AddressOf=*/true); error(CurrentFn->Name + ": raw address-of is unsupported until lexical lifetime and escape " @@ -5192,7 +5252,7 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { return std::make_unique(std::move(Address), Ty, E->getExprLoc()); } - if (!M->isArrow() && (promotedRootLocal(M) || pointeeRootPointer(M))) { + if (!M->isArrow() && (promotedRootLocal(M) || inPointeeObject(M))) { VType Ty = VType::fromQualType(E->getType(), IntMode, Ctx); if (Ty.isAggregate() || Ty.Kind == VTypeKind::Unsupported) { error(CurrentFn->Name + @@ -5200,7 +5260,8 @@ std::unique_ptr ASTConverter::convertExprImpl(const Expr *E) { ? ": aggregate value use of an automatic object " "subobject is unsupported" : ": a record or array read as a whole through a " - "pointer is unsupported; read its fields")); + "pointer or reference is unsupported; read its " + "fields")); return nullptr; } auto Place = objectPlace(M); @@ -5815,7 +5876,7 @@ void ASTConverter::appendAssignment(const Expr *LHS, return; } // A field inside the object a pointer addresses: p->inner.x, p[k].f. - if (!ME->isArrow() && pointeeRootPointer(ME)) { + if (!ME->isArrow() && inPointeeObject(ME)) { appendPointeeStore(LHS, std::move(Value), Loc, Out); return; } @@ -5869,7 +5930,7 @@ void ASTConverter::appendAssignment(const Expr *LHS, ": proof functions cannot modify executable memory"); return; } - if (pointeeRootPointer(AS->getBase())) { + if (inPointeeObject(AS->getBase())) { appendPointeeStore(LHS, std::move(Value), Loc, Out); return; } From 6b05b739408591b54ce426a148f65f1af08cd757 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 07:59:48 +0530 Subject: [PATCH 46/80] test: Check records through references and members named whole in modifies. --- clang/test/Verify/suite/record_references.cpp | 420 ++++++++++++++++++ 1 file changed, 420 insertions(+) create mode 100644 clang/test/Verify/suite/record_references.cpp diff --git a/clang/test/Verify/suite/record_references.cpp b/clang/test/Verify/suite/record_references.cpp new file mode 100644 index 0000000000..87e778efcd --- /dev/null +++ b/clang/test/Verify/suite/record_references.cpp @@ -0,0 +1,420 @@ +// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s +// RUN: %cpp-verify --lower-only --dump-ir=1 %s -- -DLOWER 2>&1 \ +// RUN: | FileCheck %s --check-prefix=VCR +// RUN: not %cpp-verify --jobs=1 --backend=bmc --unroll=1 %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=BMC +// +// A reference to a record is a pointer to it that is never null and never +// reseated: its fields and elements are places in the object it names, as +// p->f is for a pointer, and modifies(c) is that object, as modifies(*p) is. + +struct Counter { + int n; + int limit; +}; + +struct Pair { + Counter left; + Counter right; +}; + +struct Ring { + int buf[4]; + int head; +}; + +void reset(Counter &c) + cppverify::modifies(c) + cppverify::post(c.n == 0 && c.limit == 10) +{ + c.n = 0; + c.limit = 10; +} +// CHECK-DAG: Verified: reset [backend=z3] +// BMC-DAG: Verified: reset [backend=bmc, bound=0] +// VCR-LABEL: fn reset +// VCR: modifies +// VCR-NEXT: load +// VCR-NEXT: c +// VCR-NEXT: body + +// A record inside an object, through a reference or a pointer, is its bytes. +void left_only(Pair &p) + cppverify::modifies(p.left) + cppverify::post(p.left.n == 0 && p.right.n == cppverify::old(p.right.n)) +{ + reset(p.left); +} +// CHECK-DAG: Verified: left_only [backend=z3] +// VCR-LABEL: fn left_only +// VCR: modifies +// VCR-NEXT: load +// VCR-NEXT: + +// VCR-NEXT: p +// VCR-NEXT: 0 +// VCR-NEXT: range 8 +// VCR-NEXT: 1 +// VCR-NEXT: body + +void right_only(Pair *p) + cppverify::pre(p != nullptr) + cppverify::modifies(p->right) + cppverify::post(p->right.limit == 10 && p->left.n == cppverify::old(p->left.n)) +{ + reset(p->right); +} +// CHECK-DAG: Verified: right_only [backend=z3] + +#ifndef LOWER +void bump(Counter &c) + cppverify::pre(c.n < c.limit) + cppverify::modifies(c.n) + cppverify::post(c.n == cppverify::old(c.n) + 1) + cppverify::post(c.limit == cppverify::old(c.limit)) +{ + c.n = c.n + 1; +} +// CHECK-DAG: Verified: bump [backend=z3] +// BMC-DAG: Verified: bump [backend=bmc, bound=0] + +int read(const Counter &c) + cppverify::post(cppverify::result == c.n) +{ + return c.n; +} +// CHECK-DAG: Verified: read [backend=z3] + +// A reference passed on, from a reference, a pointer, and a field. +void twice(Counter &c) + cppverify::pre(c.n + 1 < c.limit) + cppverify::modifies(c.n) + cppverify::post(c.n == cppverify::old(c.n) + 2) +{ + bump(c); + bump(c); +} +// CHECK-DAG: Verified: twice [backend=z3] + +void via_pointer(Counter *p) + cppverify::pre(p != nullptr && p->n < p->limit) + cppverify::modifies(p->n) + cppverify::post(p->n == cppverify::old(p->n) + 1) +{ + bump(*p); +} +// CHECK-DAG: Verified: via_pointer [backend=z3] + +void via_field(Pair &p) + cppverify::pre(p.left.n < p.left.limit) + cppverify::modifies(p.left.n) + cppverify::post(p.left.n == cppverify::old(p.left.n) + 1) + cppverify::post(p.right.n == cppverify::old(p.right.n)) +{ + bump(p.left); +} +// CHECK-DAG: Verified: via_field [backend=z3] + +// Two mutable references name distinct objects unless aliases says so. +void frame(Counter &a, Counter &b) + cppverify::modifies(a) + cppverify::post(a.n == 0 && b.n == cppverify::old(b.n)) +{ + reset(a); +} +// CHECK-DAG: Verified: frame [backend=z3] + +void self_frame(Counter &c) + cppverify::modifies(c) +{ + frame(c, c); +} +// CHECK-DAG: error: verification failed: self_frame [{{.*}}::aliasing@[[@LINE-2]]:3] (counterexample: c [ssa=c_0] [type=pointer] = + +void may_alias(Counter &a, Counter &b) + cppverify::aliases(a, b) + cppverify::modifies(a.n) + cppverify::post(b.n == 5) +{ + a.n = 5; +} +// CHECK-DAG: error: verification failed: may_alias [{{.*}}::postcondition@[[@LINE-4]]:23] + +int sum(const Counter &a, const Counter &b) + cppverify::pre(-1000 < a.n && a.n < 1000 && -1000 < b.n && b.n < 1000) + cppverify::post(cppverify::result == a.n + b.n) +{ + return a.n + b.n; +} + +int sum_same(Counter &c) + cppverify::pre(-1000 < c.n && c.n < 1000) + cppverify::post(cppverify::result == 2 * c.n) +{ + return sum(c, c); +} +// CHECK-DAG: Verified: sum_same [backend=z3] + +// Each store lies in a footprint, and a callee's footprints in the caller's. +void bad_frame(Counter &c) + cppverify::modifies(c.n) +{ + c.limit = 3; +} +// CHECK-DAG: error: verification failed: bad_frame [{{.*}}::frame@[[@LINE-2]]:11] + +void narrow_caller(Counter &c) + cppverify::modifies(c.n) +{ + reset(c); +} +// CHECK-DAG: error: verification failed: narrow_caller [{{.*}}::frame@[[@LINE-2]]:3] + +void narrow_member(Pair &p) + cppverify::modifies(p.left.n) +{ + reset(p.left); +} +// CHECK-DAG: error: verification failed: narrow_member [{{.*}}::frame@[[@LINE-2]]:3] + +// A callee's whole record is every byte of it, which only a footprint naming +// the record, or an object around it, contains; its fields one by one do not. +void fields_one_by_one(Pair &p) + cppverify::modifies(p.left.n, p.left.limit) +{ + reset(p.left); +} +// CHECK-DAG: error: verification failed: fields_one_by_one [{{.*}}::frame@[[@LINE-2]]:3] + +// Array members: indices bounded by their array, and pointers into them +// bounded by it. +void put(Ring &r, int v) + cppverify::pre(0 <= r.head && r.head < 4) + cppverify::modifies(r.buf[r.head]) + cppverify::post(r.buf[r.head] == v && r.head == cppverify::old(r.head)) +{ + r.buf[r.head] = v; +} +// CHECK-DAG: Verified: put [backend=z3] + +void put_at(Ring &r, int i, int v) + cppverify::pre(0 <= i && i <= 4) + cppverify::modifies(r.buf[0 : 4]) +{ + r.buf[i] = v; +} +// CHECK-DAG: error: verification failed: put_at [{{.*}}::bounds@[[@LINE-2]]:12] + +void set_first(int *q, int v) + cppverify::pre(cppverify::valid(q, 4)) + cppverify::modifies(q[0]) + cppverify::post(q[0] == v) +{ + q[0] = v; +} + +void set_through_decay(Ring &r) + cppverify::modifies(r.buf[0]) + cppverify::post(r.buf[0] == 7 && r.head == cppverify::old(r.head)) +{ + set_first(r.buf, 7); +} +// CHECK-DAG: Verified: set_through_decay [backend=z3] + +int head_through_pointer(const Ring &r) + cppverify::post(cppverify::result == r.head) +{ + const int *h = &r.head; + return *h; +} +// CHECK-DAG: Verified: head_through_pointer [backend=z3] + +int read_object(const Counter *p) + cppverify::pre(p != nullptr) + cppverify::post(cppverify::result == p->n) +{ + return p->n; +} + +int through_address(const Counter &c) + cppverify::post(cppverify::result == c.n) +{ + return read_object(&c); +} +// CHECK-DAG: Verified: through_address [backend=z3] + +int past_head(const Ring &r) +{ + const int *h = &r.head; + cppverify::check(h[1] == 0); + return 0; +} +// CHECK-DAG: error: verification failed: past_head [{{.*}}::bounds@[[@LINE-3]]:3] + +// Local references to records bind a place as a parameter does. +void local_deref(Counter *p) + cppverify::pre(p != nullptr) + cppverify::modifies(*p) + cppverify::post(p->n == 0) +{ + Counter &r = *p; + r.n = 0; +} +// CHECK-DAG: Verified: local_deref [backend=z3] + +void local_member(Pair *p) + cppverify::pre(p != nullptr && p->left.n < p->left.limit) + cppverify::modifies(p->left.n) + cppverify::post(p->left.n == cppverify::old(p->left.n) + 1) +{ + Counter &r = p->left; + Counter &s = r; + bump(s); +} +// CHECK-DAG: Verified: local_member [backend=z3] + +void local_wrong_member(Pair *p) + cppverify::pre(p != nullptr) + cppverify::modifies(p->left) +{ + Counter &r = p->right; + r.n = 0; +} +// CHECK-DAG: error: verification failed: local_wrong_member [{{.*}}::frame@[[@LINE-2]]:7] + +void local_elements(Counter *a, int n) + cppverify::pre(cppverify::valid(a, n) && n >= 0) + cppverify::modifies(a[0 : n]) + cppverify::post(cppverify::forall(k, 0, n, a[k].n == 0)) +{ + for (int i = 0; i < n; i = i + 1) + cppverify::invariant(0 <= i && i <= n) + cppverify::invariant(cppverify::forall(k, 0, i, a[k].n == 0)) + cppverify::decreases(n - i) + { + Counter &r = a[i]; + r.n = 0; + } +} +// CHECK-DAG: Verified: local_elements [backend=z3] + +void local_past(Counter *a, int i) + cppverify::pre(cppverify::valid(a, 4) && 0 <= i && i <= 4) + cppverify::modifies(a[0 : 4]) +{ + Counter &r = a[i]; + r.n = 3; +} +// CHECK-DAG: error: verification failed: local_past [{{.*}}::dereference@[[@LINE-3]]:3] (counterexample: a [ssa=a_0] [type=pointer] = {{[0-9]+}}, i [ssa=i_0] [type=i32] = 4) + +// A local record bound to a reference is one object in memory. +int local_object() + cppverify::post(cppverify::result == 1) +{ + Counter c; + c.n = 0; + Counter &r = c; + r.n = 1; + return c.n; +} +// CHECK-DAG: Verified: local_object [backend=z3] + +int local_object_uninitialized() + cppverify::post(cppverify::result == 0) +{ + Counter c; + c.n = 0; + Counter &r = c; + return r.limit; +} +// CHECK-DAG: error: verification failed: local_object_uninitialized [{{.*}}::initialization@[[@LINE-2]]:3] + +// A type invariant is a fact about records by value; one a reference names is +// an object whose fields the function reads from memory. +struct Bounded { + int v; + cppverify::type_invariant(v >= 0); +}; + +int by_value(Bounded b) + cppverify::post(cppverify::result >= 0) +{ + return b.v; +} +// CHECK-DAG: Verified: by_value [backend=z3] + +int by_reference(const Bounded &b) + cppverify::post(cppverify::result >= 0) +{ + return b.v; +} +// CHECK-DAG: error: verification failed: by_reference [{{.*}}::postcondition@[[@LINE-4]]:37] + +// Not yet: a local passed to a callee by reference, whose non-escape is not +// established for records (B3a-4), a pointer formed from a local through a +// reference, a whole record read through one, a proof function's reference, +// and rvalue and volatile references. +int local_to_callee() + cppverify::post(cppverify::result == 1) +{ + Counter c; + c.n = 0; + c.limit = 5; + bump(c); + return c.n; +} +// CHECK-DAG: [[@LINE-3]]:3: Unresolved: local_to_callee [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: the address of local or dynamic storage is passed to bump, which may keep, offset, or free it, or has no verified body) + +int local_address() + cppverify::post(cppverify::result == 0) +{ + Ring local; + Ring &r = local; + int *q = &r.head; + return 0; +} +// CHECK-DAG: error: local_address: raw address-of is unsupported until lexical lifetime and escape effects are modeled + +int local_decay() + cppverify::post(cppverify::result == 0) +{ + Ring local; + local.buf[0] = 1; + Ring &r = local; + int *q = r.buf; + return 0; +} +// CHECK-DAG: error: local_decay: array-to-pointer decay of automatic storage is unsupported until lexical lifetime and escape effects are modeled + +int by_copy(Counter c) + cppverify::post(cppverify::result == c.n) +{ + return c.n; +} + +int whole_read(const Pair &p) + cppverify::post(cppverify::result == p.left.n) +{ + return by_copy(p.left); +} +// CHECK-DAG: error: whole_read: a record or array read as a whole through a pointer or reference is unsupported; read its fields + +cppverify::proof void proof_reference(Counter &c) + cppverify::post(true) +{ +} +// CHECK-DAG: error: proof_reference: unsupported C++ type in verification: Counter & + +int rvalue_reference(Counter &&c) + cppverify::post(cppverify::result == c.n) +{ + return c.n; +} +// CHECK-DAG: error: rvalue_reference: unsupported C++ type in verification: Counter && + +int volatile_reference(volatile Counter &c) + cppverify::post(cppverify::result == c.n) +{ + return c.n; +} +// CHECK-DAG: error: volatile_reference: unsupported C++ type in verification: volatile Counter & +#endif From 1f3fedf077e6d51911b49a34b4efc8f55e0c869a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 07:59:49 +0530 Subject: [PATCH 47/80] test: Stop expecting a reference to a record to be rejected. --- clang/test/Verify/suite/references_unsupported.cpp | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/clang/test/Verify/suite/references_unsupported.cpp b/clang/test/Verify/suite/references_unsupported.cpp index c72a17a1ef..412371b3e5 100644 --- a/clang/test/Verify/suite/references_unsupported.cpp +++ b/clang/test/Verify/suite/references_unsupported.cpp @@ -14,11 +14,6 @@ int read_value(const int &value) return value; } -struct Pair { - int first; - int second; -}; - struct WithReference { int &value; }; @@ -48,12 +43,6 @@ int &reference_return(int &value) cppverify::pre(true) { return value; } -int record_reference(Pair &value) - cppverify::post(cppverify::result == value.first) -{ - return value.first; -} - int rvalue_reference(int &&value) cppverify::post(cppverify::result == value) { @@ -140,7 +129,6 @@ void conditional_reference_actual(bool choose, int *value) // VERIFY-DAG: error: temporary_actual: reference arguments require a supported reference, addressable local, or direct pointer dereference // VERIFY-DAG: error: reference_return: unsupported C++ type in verification: int & -// VERIFY-DAG: error: record_reference: unsupported C++ type in verification: Pair & // VERIFY-DAG: error: rvalue_reference: unsupported C++ type in verification: int && // VERIFY-DAG: error: volatile_reference: unsupported C++ type in verification: volatile int & // VERIFY-DAG: error: pointer_reference: unsupported C++ type in verification: int *& From d906f9940ec075cc7c31406e2b4a91d2a4239c3e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 07:59:49 +0530 Subject: [PATCH 48/80] docs: Describe records through references, with a checked example. --- website/source/language/structs.rst | 107 ++++++++++++++++++++++++++-- 1 file changed, 103 insertions(+), 4 deletions(-) diff --git a/website/source/language/structs.rst b/website/source/language/structs.rst index 4b33605a57..6f82ceea6c 100644 --- a/website/source/language/structs.rst +++ b/website/source/language/structs.rst @@ -175,6 +175,103 @@ would be lost there: returning it, or storing it in memory, is an error. 10 | return &r->buf[i]; | ^~~~~~ +Records through references +-------------------------- + +A reference to a record (``Counter &``, ``const Counter &``) is a pointer to +it that is never null and never reseated, so everything above holds of it: +``c.n``, ``c.buf[i]``, and ``c.inner.x`` are cells of the object ``c`` names, +and ``&c.n`` and ``c.buf`` are pointers into it. The verifier requires the +object to be live and initialized at entry, as for a scalar reference, and +two references of which one is mutable name distinct objects unless +``cppverify::aliases`` allows them to name one. ``cppverify::modifies(c)`` is the +whole object, as ``cppverify::modifies(*p)`` is for a pointer, and a record +or array member named whole, ``cppverify::modifies(p.left)`` or +``cppverify::modifies(r.buf)``, is the bytes of that member. A reference +parameter may be bound to a reference, to ``*p``, to a field such as +``p->left``, or to an element ``a[i]``, and so may a local reference: + +.. cppverify-example: fails reset_count + +.. code-block:: cpp + + struct Counter { + int n; + int limit; + }; + + struct Pair { + Counter left; + Counter right; + }; + + void bump(Counter &c) + cv::pre(c.n < c.limit) + cv::modifies(c.n) + cv::post(c.n == cv::old(c.n) + 1) + { + c.n = c.n + 1; + } + + void reset(Counter &c) + cv::modifies(c) + cv::post(c.n == 0 && c.limit == 10) + { + c.n = 0; + c.limit = 10; + } + + void reset_left(Pair &p) + cv::modifies(p.left) + cv::post(p.left.n == 0 && p.right.n == cv::old(p.right.n)) + { + reset(p.left); + } + + void bump_left(Pair *p) + cv::pre(p != nullptr && p->left.n < p->left.limit) + cv::modifies(p->left.n) + cv::post(p->left.n == cv::old(p->left.n) + 1) + { + Counter &c = p->left; + bump(c); + } + + void reset_count(Pair &p) + cv::modifies(p.left.n) + { + reset(p.left); + } + +.. code-block:: text + + Verified: bump [backend=z3] + Verified: reset [backend=z3] + Verified: reset_left [backend=z3] + Verified: bump_left [backend=z3] + pair.cpp:46:3: error: verification failed: reset_count [...::frame@46:3] (counterexample: p [ssa=p_0] [type=pointer] = 1; trace: call.reset@46:3 arg0=1) [backend=z3] [reason=counterexample] + +``reset_left`` may write ``p.left``, which holds the whole object ``reset`` +may write, so ``p.right`` keeps its value. ``reset_count`` may write only +``p.left.n``, and ``reset`` writes ``p.left.limit`` too: the call fails its +``frame`` check. A caller that may write both fields one by one, +``cppverify::modifies(p.left.n, p.left.limit)``, still fails it: the callee's +footprint is every byte of the record, which only a footprint naming the +record, or an object around it, contains. + +Not yet supported: + +- a local record passed to a reference or pointer parameter (``bump(c)`` with + ``Counter c;``): the verifier does not yet show that the callee keeps no + pointer to it, and the call is ``Unresolved`` with reason + ``construct.unsupported``. A local reference may bind a local record, and + reads and writes through it are checked against that object's lifetime and + initialization, but forming a pointer through such a reference (``&r.n``, + ``r.buf``) is an error; +- reading a whole record through a reference, as through a pointer; +- reference returns, rvalue and ``volatile`` references, and references in + spec and proof functions. + ``cppverify::type_invariant`` ----------------------------- @@ -198,7 +295,8 @@ Semantics: - The invariant is injected as a **precondition** at the first use of an invariant field for by-value parameters. Because it is a precondition, callers must establish it when they pass such a value. -- It is **not** injected for raw pointer-to-struct parameters (their fields are heap loads). +- It is **not** injected for pointer-to-struct or reference-to-struct + parameters: their fields are heap loads of an object in memory. - **Returns are checked**: when a function returns a struct value of an invariant-bearing type, the verifier asserts the invariant holds for the returned value. Building and returning a struct whose fields violate the invariant is a verification error. @@ -232,8 +330,9 @@ returned by value must be trivial, standard-layout, and flat, with scalar fields. A local object whose address is needed (it holds a fixed array, or a reference binds to one of its members) is promoted to an automatic object and may also have nested record, pointer, and fixed-array members. A record -reached through a pointer may have the same members, and its scalar fields and -elements are reached one at a time (see `Records through pointers`_), or -through a pointer into it (see `Pointers into a record`_). Reference +reached through a pointer or a reference may have the same members, and its +scalar fields and elements are reached one at a time (see `Records through +pointers`_ and `Records through references`_), or through a pointer into it +(see `Pointers into a record`_). Reference members, unions, bases, virtual dispatch, and non-trivial construction/destruction are rejected rather than approximated. From a8b47d558bffb6573b247b92f01f3b879e3a807f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 07:59:50 +0530 Subject: [PATCH 49/80] docs: Extend records and frames to references to records in chapter 14. --- .../part-ii/ch14-pointers-frames-modifies.rst | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/website/source/book/part-ii/ch14-pointers-frames-modifies.rst b/website/source/book/part-ii/ch14-pointers-frames-modifies.rst index c5cd6bbc02..e0c0cd1e5f 100644 --- a/website/source/book/part-ii/ch14-pointers-frames-modifies.rst +++ b/website/source/book/part-ii/ch14-pointers-frames-modifies.rst @@ -77,8 +77,10 @@ liveness, initialization, and a non-escaping lifetime identity. A local binding snapshots its address, so changing a source pointer later does not rebind the reference. -Conditional bindings, temporaries, reference returns, address-taking, rvalue -references, and non-scalar referents remain rejected. +Conditional bindings, temporaries, reference returns, the address of a +scalar reference, and rvalue references remain rejected. A reference to a +record names an object in memory, as a pointer to it does (see `Records +through pointers`_ below). Addressable declarations inside loops and ``cppverify::old`` of automatic locals or local bindings are also fail-closed; outer automatic locals and loop-local reference aliases are supported. @@ -101,7 +103,10 @@ There are three frame granularities: - a **range**, ``cppverify::modifies(p[lo : n])``, names the ``n`` elements from ``p[lo]``, half-open ``[lo, lo + n)`` (Clang's array-section syntax); - a **region**, ``cppverify::modifies(*p)``, names the object ``p`` addresses: its - ``valid(p, n)`` extent, or one object. + ``valid(p, n)`` extent, or one object. ``cppverify::modifies(c)`` for a + reference ``c`` to a record names the object ``c`` names, and a record or + array member named whole (``cppverify::modifies(s->inner)``, + ``cppverify::modifies(s->items)``) names the bytes of that member. Inside the function, every store must lie in a footprint read in the entry state. At a modular call, the caller's heap changes only inside the callee's @@ -328,6 +333,12 @@ pointer stepped through the array stays a whole number of elements from its start, as a generated invariant it proves, so the walk never lands between elements. :doc:`../../language/structs` lists the forms that are supported. +All of this holds through a reference to a record too, which is a pointer +that is never null and never reseated: ``void push(Stack &s, int v)`` reads +and writes ``s.items[s.size]`` and ``s.size`` as the version above does +through ``s->``, ``cppverify::modifies(s)`` is the whole stack, and +``&s.size`` and ``s.items`` are pointers into it. + Declaring a checked extent -------------------------- From a430f47dd92a3cc4e259501b7a4a50b407b5981a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 07:59:51 +0530 Subject: [PATCH 50/80] docs: List references to records as supported in the limitations. --- website/source/language/limitations.rst | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 3b58f00f81..70d3943bfa 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -124,10 +124,14 @@ C++ feature boundaries boolean, integral, and enum referents, and bindings to a field or fixed array element of a promoted local object, or to a field or element of a parameter's buffer or of a record a pointer addresses - (``int &alias = p->second;``, ``p[i]``, ``p->buf[i]``). - - Conditional bindings, reference returns, non-scalar referents, rvalue - references, temporaries/lifetime extension, reference members, and - forwarding. + (``int &alias = p->second;``, ``p[i]``, ``p->buf[i]``). References to + records (``Counter &``, ``const Counter &``) as parameters and locals: + a pointer never null or reseated, whose fields and elements are cells + of the object it names (:doc:`structs`). + - Conditional bindings, reference returns, rvalue references, + temporaries/lifetime extension, reference members, and forwarding; a + local record passed to a reference parameter (``construct.unsupported``) + and a pointer formed through a local reference to a local record. * - Arrays - Pointer-parameter indexing, quantified abstract buffers, fixed local arrays (including arrays of records and multidimensional arrays) @@ -287,9 +291,10 @@ the lexical closing brace or on each early return, in reverse construction order; heap-reading return values are materialized before teardown. Scalar references may bind supported fields and fixed-array elements of these -promoted objects. Conditional bindings, temporaries, reference returns, general -raw address-taking/array decay, rvalue references, and non-scalar referents -remain fail-closed. Addressable declarations inside loops and ``cppverify::old`` of local +promoted objects, and a local reference to a record may bind a promoted +record. Conditional bindings, temporaries, reference returns, general raw +address-taking/array decay (through such a reference too), rvalue references, +and passing a promoted record to a callee by reference remain fail-closed. Addressable declarations inside loops and ``cppverify::old`` of local objects/bindings are also rejected; outer automatic locals and loop-local aliases are supported. Pointer leaves may retain abstract pointer values, but storing a provenance-bearing local dynamic pointer fails closed until pointer provenance is From af65377c2ea4ea3daa8222f35670847377b65985 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 07:59:51 +0530 Subject: [PATCH 51/80] docs: Mention references to records on the front page. --- website/source/index.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/website/source/index.rst b/website/source/index.rst index 7865a9bb98..783fb1bea7 100644 --- a/website/source/index.rst +++ b/website/source/index.rst @@ -189,8 +189,8 @@ Reference values lower to heap loads, writes lower to stores, and ``cppverify::o the entry heap. The bounded scalar slice supports direct forwarding, direct ``*p`` bindings, fields and elements of local objects and of parameter buffers, ordinary initialized scalar local actuals, and chained local reference aliases. -Conditional bindings, temporaries, reference returns, and non-scalar referents -remain fail-closed. See +A reference to a record is a pointer to it that is never null or reseated. +Conditional bindings, temporaries, and reference returns remain fail-closed. See :doc:`language/pointers`. Backends and modular calls From 34b3eceb9effcc96bf3d95a2316e4c27e72c9040 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 07:59:52 +0530 Subject: [PATCH 52/80] docs: Note records through references and members named whole in the release notes. --- website/source/release-notes.rst | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index c79f4204f3..42d5c4bbb1 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -212,6 +212,14 @@ although the callee writes only cells the caller may write, in two cases: The callee's footprint is now compared with the caller's frame cell by cell (:doc:`language/pointers`). +**A record member named whole in** ``cppverify::modifies``. +``cppverify::modifies(p->left)``, for a member that is a record or an array, +was taken for one cell holding the whole member. A call ``reset(&p->left)`` +of a function that may write its object failed its ``frame`` check, and a +call of the function itself could not be verified (``obligation lowering +failed: ... (invalid sort in obligation IR)``). The footprint is now the +bytes of the member (:doc:`language/structs`). + **Lean goals that could not be proved.** In a Lean goal a quantifier took everything after it into its body, which made a goal with a quantified fact before its conclusion say more than its obligation: the goal of a call that @@ -262,6 +270,17 @@ accesses, steps, pointer differences, and call arguments through it are checked against that subobject, so ``q[8]`` past ``r->buf`` is an error, though it lies in ``*r`` (:doc:`language/structs`). +**Records through references.** A reference to a record (``Counter &c``, +``const Counter &c``), as a parameter or a local, was an error +(``unsupported C++ type in verification: Counter &``), so the free function +form of a method on an object, ``bump(Counter &c)``, could not be verified. +A reference to a record is now a pointer to it that is never null and never +reseated: ``c.n`` and ``c.buf[i]`` are cells of the object, ``&c.n`` and +``c.buf`` point into it, ``cppverify::modifies(c)`` is the whole object, and +a reference can be bound to ``*p``, ``p->left``, ``a[i]``, or another +reference. Passing a local record to a reference parameter is still +``construct.unsupported`` (:doc:`language/structs`). + Running cpp-verify ~~~~~~~~~~~~~~~~~~ From 02e7fa7a250c41ef05252f261dab5c1e35ccda1a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 07:59:52 +0530 Subject: [PATCH 53/80] docs: Describe records through references in the design. --- docs/DESIGN.md | 71 +++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 64 insertions(+), 7 deletions(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 3ebdc07ef9..ef70dc2988 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1109,7 +1109,8 @@ identity. Addressable local declarations inside loops, `cppverify::old(local)`, `cppverify::old(local_ref)`, conditional bindings, temporaries, reference returns, -address-taking, rvalue references, and non-scalar referents remain fail-closed. +address-taking, and rvalue references remain fail-closed. A reference to a +record is the address of an object (3c). An outer automatic local and a local reference declaration may be used inside a loop. Recursive executable bodies may store through pointer and reference parameters and use automatic objects; recursion through a function that @@ -1159,6 +1160,56 @@ void put(Ring *r, int v) Returning such a pointer or storing it in memory would lose the bounds and is rejected. +### 3c. Records through references + +```cpp +struct Counter { int n; int limit; }; +struct Pair { Counter left; Counter right; }; + +void reset(Counter &c) + cppverify::modifies(c) + cppverify::post(c.n == 0 && c.limit == 10) +{ + c.n = 0; + c.limit = 10; +} + +void reset_left(Pair &p) + cppverify::modifies(p.left) + cppverify::post(p.left.n == 0 && p.right.n == cppverify::old(p.right.n)) +{ + reset(p.left); +} +``` + +- A reference to a record (`T &`, `const T &`, a parameter or a local) is a + pointer to it that is never null and never reseated, so everything 3b + says holds of it: `c.f`, `c.buf[i]`, and `c.inner.x` are cells of the + object `c` names, with the same two checks, and `&c.f` and `c.buf` are + pointers into it with subobject bounds. A record by value stays its + fields; only a reference or a pointer names an object. +- A reference parameter gets the generated preconditions of a scalar + reference: its object is non-null, live, and initialized, and it takes + part in the default non-aliasing of address parameters over its whole + object (`cppverify::aliases` opts out). A record's type invariant is not + injected for it, as for a pointer: its fields are read from memory. +- `cppverify::modifies(c)` is the object, as `cppverify::modifies(*p)` is, + and as Dafny's `modifies c` is every field of the object `c` references; + `cppverify::modifies(c.n)` is one cell, as Dafny's ``modifies c`n``. A + scalar reference's `modifies(r)` stays one cell, since it may bind a field + of a larger object. +- A reference argument or a local reference binds a place: another + reference, `*p`, a field (`p->left`), an element (`a[i]`), checked where it + is bound. A local reference may also bind a promoted local record; reads + and writes through it carry that object's lifetime and initialization + checks, but a pointer formed through it would not, and is rejected (as + `&local` is). +- Not yet: a local record passed to a reference or pointer parameter. The + non-escape scan that admits a local scalar actual does not cover records, + so the call is `Unresolved` (`construct.unsupported`). Also rejected: a + whole record read through a reference, reference returns, rvalue and + `volatile` references, and references in spec and proof functions. + ### 4. `cppverify::modifies(...)` frame condition ```cpp @@ -1191,14 +1242,20 @@ void incr_first(int* a, int* b) `p->buf[lo : n]` for an array member; - a region `*p`: the object `p` addresses, which is its `valid(p, n)` extent when it has one and otherwise one object. A region of a single - scalar object is one cell. + scalar object is one cell. `c` for a reference to a record is the object + it names; + - the bytes of a record or array inside an object, named whole + (`p->inner`, `c.buf`, `p[k]` of a record extent): a range of one element + of its size. - Inside the callee every store must lie in a footprint, read in the entry state, so reassigning a pointer cannot widen the frame; a footprint of a callee must lie within the caller's own frame, cell by cell: a region of one scalar object is one cell, ranges and extents compare by their cells, and a footprint reached through another pointer than a caller region's (a copy of a pointer into the object) lies in that region when its cells - lie in the region's object, as a store does. + lie in the region's object, as a store does. A region or range lies in + one footprint of the caller: the heap holds a cell at every address, so + footprints of a record's fields one by one do not contain the record. - At a call, the caller's heap changes only inside the callee's footprints instantiated with the arguments: a cell or range is exactly those cells, a region is the argument's extent (or one object). Every other cell keeps its @@ -1209,8 +1266,7 @@ void incr_first(int* a, int* b) forgets the whole heap. - Preconditions and `cppverify::old(parameter)` use entry actual arguments, and so does a parameter named in a postcondition. -- General reference binding and member-function effects are not yet in the - verified subset. +- Member-function effects are not yet in the verified subset. ### Worked example @@ -1267,7 +1323,8 @@ int dist_sq(Coordinate p, Coordinate q) ``` - `cppverify::type_invariant(expr)`: holds at function boundaries for by-value - records of the type; pointer-to-record parameters get no injection. + records of the type; pointer-to-record and reference-to-record parameters + get no injection. - `expr` may reference any field of the enclosing type by name. - Must be contextually convertible to bool. @@ -2087,5 +2144,5 @@ fixed arrays, scalar subobject references, the fields and fixed-array elements of a record a pointer addresses, modular slices, and general same-array pointer difference under `valid(p, n)` are also supported. Provenance across ownership-taking or recursive interfaces, pointer -reinterpretation/cross-object arithmetic, aggregate/rvalue references, +reinterpretation/cross-object arithmetic, rvalue references, by-value pointer-bearing records, and general arrays remains unsupported. From 63b2b98481bfcaa986b1ec1b0e3a0b96e6ed5a4f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 07:59:53 +0530 Subject: [PATCH 54/80] docs: Describe records through references in the architecture. --- docs/ARCHITECTURE.md | 39 ++++++++++++++++++++++++++++++++++----- 1 file changed, 34 insertions(+), 5 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 1389282dcf..3a0b6377b6 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -176,6 +176,31 @@ whose own access UB instrumentation checks against the pointer's extent or object as before. `p->buf[i]` therefore has both checks, and the array's is what rejects `p->buf[8]`, the address of the next field. +**Records through references:** a reference to a record, a parameter or a +local, is a pointer-typed VCR variable holding the object's address +(`VType::Ptr` of the record's size), never flattened: `getRecordFromType` +stops at references, so only a record by value becomes `param.field` +values, and so do source variables, type-invariant injection, and call +arguments. `recordReferenceRoot` finds the reference a selection chain +starts at (`c.f`, `c.buf[i]`), and `inPointeeObject` (it, or +`pointeeRootPointer`) admits the place wherever a place through a pointer is +admitted: loads, stores, subscripts, reference bindings, footprints. +`objectPlace` of the bare reference is the place at its address, as `*p`. +Pointers into the object (`&c.f`, `c.buf`) are formed only where +`subobjectPointerRoot` holds: through a pointer, or a reference whose object +outlives the function (a parameter, or a local not bound to represented +storage, which `LocalReferenceProvenanceVariables` records), since a +subobject pointer does not carry a promoted object's lifetime. +`VFunction::ScalarReferenceParams` holds only scalar references, whose +`modifies(r)` is the one cell they bind; a record reference's is a region, +its parameter's entry object (`entryObjectRegion`), as for `*p`. +`convertFootprint` lowers a record or array named whole inside an object +(`p->inner`, `c.buf`, `p[k]`) to a range of one element of its size, so +every frame path (own stores, call havoc, containment, loop frames) treats it +as its bytes; before, it was a cell holding the record, which held no +callee's footprint inside the member and whose havoc at a call had no logic +sort. + **Pointers into objects:** `ASTConverter::subobjectPointer` lowers a decayed member array of a pointee and the address of a pointee's element, field, or nested record. In a statement (`SubobjectSink`) it asserts the place's access @@ -300,8 +325,10 @@ VFunction = source spelling remain distinct through modular calls and SMT symbols. - `cppverify::aliases` empty means the implicit non-aliasing precondition applies to every pair of distinct pointer/reference parameters of which at least one is mutable. - A `VFootprint` is a target lvalue with an optional element count and - element size: a cell (`p[i]`, `p->f`, a reference), a range `p[lo : n]` - (target `p[lo]`, count `n`), or a region `*p` (the object `p` addresses). + element size: a cell (`p[i]`, `p->f`, a scalar reference), a range + `p[lo : n]` (target `p[lo]`, count `n`; a record or array named whole + inside an object, `p->inner`, is a range of one element of its size), or a + region `*p` (the object `p` addresses, or a reference to a record names). - Behaviors are desugared in the frontend: each scoped `cppverify::pre` becomes `!assumes || pre`, each scoped `cppverify::post` `!old(assumes) || post`, and `cppverify::complete_behaviors`/`cppverify::disjoint_behaviors` become assertions at body entry. @@ -2381,9 +2408,11 @@ disjoint from incoming address parameters, complete declared extents, stored pointer cells, and every live represented object. Their lifetimes end at the lexical closing brace and on each supported early return in reverse construction order, after materializing any heap-reading return value. Scalar references may -bind fields and fixed-array elements with access-local nested bounds. General -escape, raw array decay/address-taking, aggregate references, and addressable -declarations inside loops remain fail-closed; so does the decay of an array +bind fields and fixed-array elements with access-local nested bounds, and a +local reference to a record may bind a promoted record, its provenance +companion carried like a scalar reference's. General escape, raw array +decay/address-taking (through such a reference too), passing a promoted record +to a callee, and addressable declarations inside loops remain fail-closed; so does the decay of an array member through a pointer (`ASTConverter::arrayDecayError` names which). Automatic metadata transitions are private and a modular caller may frame them away. From 17b3c6892812bd31aa013ec69dc24aa8b3a87956 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 08:26:59 +0530 Subject: [PATCH 55/80] verify: Decide a quantifier over a range of integers in Lean only for at most 4096 integers. --- clang/lib/Verify/Backend/LeanBackend.cpp | 39 +++++++++++++++--------- 1 file changed, 24 insertions(+), 15 deletions(-) diff --git a/clang/lib/Verify/Backend/LeanBackend.cpp b/clang/lib/Verify/Backend/LeanBackend.cpp index 5ea0ce0786..e58cd24d6c 100644 --- a/clang/lib/Verify/Backend/LeanBackend.cpp +++ b/clang/lib/Verify/Backend/LeanBackend.cpp @@ -1296,27 +1296,36 @@ static std::string leanSpecDefinition(const ObligationModule &Module, // A quantifier over a range of integers, as a goal states one, is decided by // trying each integer of the range, as core Lean decides one over a range of -// naturals. +// naturals, when the range has at most 4096 integers, as many as the +// certifier expands (CertifyLimits::DirectExpansion). Each integer is a level +// of recursion whose memory heartbeats do not count: under the generated +// files' recursion depth a range of 64000 took 58 GB before failing, and one +// of 4000 already spent a step's heartbeats. A larger range has the classical +// instance, which decide cannot evaluate. static constexpr llvm::StringLiteral LeanBoundedQuantifierPrelude = R"lean(instance cppIntBallDecidable (lo hi : Int) (p : Int → Prop) [DecidablePred p] : Decidable (∀ x : Int, lo ≤ x ∧ x < hi → p x) := - decidable_of_iff (∀ k : Nat, k < (hi - lo).toNat → p (lo + k)) (by - constructor - · intro h x hx - have := h (x - lo).toNat (by omega) - rwa [show lo + ((x - lo).toNat : Int) = x by omega] at this - · intro h k hk - exact h _ ⟨by omega, by omega⟩) + if (hi - lo).toNat ≤ 4096 then + decidable_of_iff (∀ k : Nat, k < (hi - lo).toNat → p (lo + k)) (by + constructor + · intro h x hx + have := h (x - lo).toNat (by omega) + rwa [show lo + ((x - lo).toNat : Int) = x by omega] at this + · intro h k hk + exact h _ ⟨by omega, by omega⟩) + else Classical.propDecidable _ instance cppIntBexDecidable (lo hi : Int) (p : Int → Prop) [DecidablePred p] : Decidable (∃ x : Int, lo ≤ x ∧ x < hi ∧ p x) := - decidable_of_iff (∃ k : Nat, k < (hi - lo).toNat ∧ p (lo + k)) (by - constructor - · rintro ⟨k, hk, hp⟩ - exact ⟨lo + k, by omega, by omega, hp⟩ - · rintro ⟨x, h1, h2, hp⟩ - refine ⟨(x - lo).toNat, by omega, ?_⟩ - rwa [show lo + ((x - lo).toNat : Int) = x by omega]) + if (hi - lo).toNat ≤ 4096 then + decidable_of_iff (∃ k : Nat, k < (hi - lo).toNat ∧ p (lo + k)) (by + constructor + · rintro ⟨k, hk, hp⟩ + exact ⟨lo + k, by omega, by omega, hp⟩ + · rintro ⟨x, h1, h2, hp⟩ + refine ⟨(x - lo).toNat, by omega, ?_⟩ + rwa [show lo + ((x - lo).toNat : Int) = x by omega]) + else Classical.propDecidable _ )lean"; From 0776e1d156ab91ff079eba0cf6f25d8d04277517 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 08:27:00 +0530 Subject: [PATCH 56/80] test: Add a refutation over a thousand integers to the budget input. --- .../Verify/suite/Inputs/lean_refutation_budget.cpp | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/clang/test/Verify/suite/Inputs/lean_refutation_budget.cpp b/clang/test/Verify/suite/Inputs/lean_refutation_budget.cpp index 1d75a803eb..6b38456856 100644 --- a/clang/test/Verify/suite/Inputs/lean_refutation_budget.cpp +++ b/clang/test/Verify/suite/Inputs/lean_refutation_budget.cpp @@ -1,9 +1,16 @@ // Refutations that are bounded, and refutations that are not reported, for // lean_refutation.test. -// Lean would decide this one by trying each of a billion integers: each -// attempt of the refutation stops at the heartbeats of a step of -// cppverify_auto, and the counterexample is not decided there. +// Lean decides a quantifier over a thousand integers by trying each one. +cppverify::proof void below_a_thousand() + cppverify::post(cppverify::forall(i, 0, 1000, i < 999)) +{ +} + +// It would decide this one by trying each of a billion integers, which the +// prelude does only for ranges of at most 4096: each integer is a level of +// recursion, whose memory heartbeats do not bound. The counterexample is not +// decided. cppverify::proof void below_a_billion() cppverify::post(cppverify::forall(i, 0, 1000000000, i < 999999999)) { From 9f63ff77dd13e988d394a5d71d765b0293be6229 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 08:27:00 +0530 Subject: [PATCH 57/80] test: Check that a quantifier over a thousand integers is refuted in Lean. --- clang/test/Verify/suite/lean_refutation.test | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/test/Verify/suite/lean_refutation.test b/clang/test/Verify/suite/lean_refutation.test index 55ddb8a3a4..9d98556ddd 100644 --- a/clang/test/Verify/suite/lean_refutation.test +++ b/clang/test/Verify/suite/lean_refutation.test @@ -82,6 +82,7 @@ # TACTIC: lean_refutation_tactic.lean:7:2: error: cppverify: Lean decides the goal true at the counterexample # TACTIC: lean_refutation_tactic.lean:16:2: error: cppverify: Lean cannot decide the goal at the counterexample +# BUDGET: error: verification failed: below_a_thousand {{.*}}[reason=counterexample] (confirmed in Lean) # BUDGET: error: verification failed: below_a_billion {{.*}}[reason=counterexample]{{$}} # BUDGET: Unresolved: verification unresolved: far {{.*}}[reason=spec.post] (its counterexample is checked with the postcondition of ge, which is not established){{$}} # BUDGET: warning: the counterexample of below_a_billion is not confirmed in Lean: Lean cannot decide the goal at the counterexample From d5d21db3a10ddfa00a2888bbe4c0c7d5f766acbc Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 08:27:01 +0530 Subject: [PATCH 58/80] test: Check that refuting a quantifier over a billion integers stays below 4 GB. --- clang/test/Verify/suite/lean_refutation_memory.test | 13 +++++++++++++ 1 file changed, 13 insertions(+) create mode 100644 clang/test/Verify/suite/lean_refutation_memory.test diff --git a/clang/test/Verify/suite/lean_refutation_memory.test b/clang/test/Verify/suite/lean_refutation_memory.test new file mode 100644 index 0000000000..f29653a6d5 --- /dev/null +++ b/clang/test/Verify/suite/lean_refutation_memory.test @@ -0,0 +1,13 @@ +# REQUIRES: lean, system-linux +# +# Lean decides a quantifier over a range of integers by trying each one, and +# each integer is a level of recursion whose memory heartbeats do not bound: +# refuting below_a_billion took 58 GB before Lean gave up. The prelude tries +# each integer only for a range of at most 4096, so Lean gives up at once. +# +# RUN: rm -rf %t && mkdir -p %t +# RUN: not %python %S/Inputs/peak_memory.py 4096 %cpp-verify --lean-fallback=%t/b --lean-certify %S/Inputs/lean_refutation_budget.cpp -- 2>&1 | FileCheck %s + +# CHECK: error: verification failed: below_a_thousand {{.*}}[reason=counterexample] (confirmed in Lean) +# CHECK: warning: the counterexample of below_a_billion is not confirmed in Lean: Lean cannot decide the goal at the counterexample +# CHECK: peak memory below 4096 MB From 824cbf92498e576130988a9d99c10cb6ff043ff1 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 08:27:02 +0530 Subject: [PATCH 59/80] docs: Describe the range bound of the Lean prelude's quantifiers in the architecture. --- docs/ARCHITECTURE.md | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 5002ca77de..894d010973 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1796,8 +1796,16 @@ replay both drive it. the theorem keeps Lean's limit, which bounds the kernel's check of it too: with no limit, the refutation of an inductive predicate applied at -5000 ran for over an hour. The prelude decides a quantifier over a - range of integers by trying each one (`cppIntBallDecidable`, - `cppIntBexDecidable`, through core's `Nat` ones). `writeLeanRefutations` + range of at most 4096 integers, as many as the certifier expands + (`CertifyLimits::DirectExpansion`), by trying each one + (`cppIntBallDecidable`, `cppIntBexDecidable`, through core's `Nat` ones), + and a larger range has the classical instance, which `decide` cannot + evaluate. Each integer is a level of recursion whose memory heartbeats do + not count, and the generated files allow a depth of 100000: before the + bound, refuting `forall(i, 0, 1000000000, i < 999999999)` took one Lean + process 58 GB (16 GB for a range of 16000, which also spent the step's + heartbeats; 1.9 GB for one of 1000), and CI's 16 GB runners were shut down + (`lean_refutation_memory.test`, Linux, keeps it below 4 GB). `writeLeanRefutations` writes `Refutations//.lean` and removes every other, and certification builds them beside the proofs and gives the checker each as a `refutation` entry, whose theorem must state exactly `Not ` of the From b8fec4f77f679501eaeccebcc6352ce77c23238f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 08:27:02 +0530 Subject: [PATCH 60/80] docs: Bound the Lean prelude's quantifiers to 4096 integers in the design. --- docs/DESIGN.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index cc5524ed61..d2aeb8b810 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -2032,7 +2032,8 @@ A certified counterexample is shown false in Lean too: the fallback project gets its refutation, the failing goal stated as the project states it and a theorem `¬ goal` proved at the values the model gives its variables (`cppverify_refute`: decided, or evaluated by the spec definitions, a store -by `grind`, a quantifier over a range of integers by trying each one, each +by `grind`, a quantifier over a range of at most 4096 integers by trying +each one, each attempt within the heartbeats of a step of `cppverify_auto`), which `--lean-certify` checks as it checks a proof. Of the failures that stand once the verdicts settle, a refutation that checks marks From 30fae896d274c53c3d84619cc38bc6f533b683b6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 08:27:03 +0530 Subject: [PATCH 61/80] docs: Bound the Lean prelude's quantifiers to 4096 integers in chapter 17. --- website/source/book/part-ii/ch17-backends-modular-calls.rst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/website/source/book/part-ii/ch17-backends-modular-calls.rst b/website/source/book/part-ii/ch17-backends-modular-calls.rst index b007f3583c..04fb031093 100644 --- a/website/source/book/part-ii/ch17-backends-modular-calls.rst +++ b/website/source/book/part-ii/ch17-backends-modular-calls.rst @@ -365,7 +365,9 @@ of the spec functions Lean defines: ``cppverify_refute`` decides the instance, or evaluates it first, the spec functions that are Lean definitions (`Spec functions in Lean`_) by their equations, a store to memory with ``grind``, since it relates two heaps at -every address, and a quantifier over a range of integers by trying each one. +every address, and a quantifier over a range of at most 4096 integers by +trying each one (a larger range is not decided: each integer is a level of +recursion, and a billion of them took Lean 58 GB). A goal that applies a spec Lean leaves opaque, such as a ``cppverify::choose``, cannot be decided there: the failure stands, and a warning says so (``the counterexample of pick_one is not confirmed in Lean: Lean cannot decide the From c26a4edd5f75d61de2f7a5e1bfb429d071d1576c Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 08:27:03 +0530 Subject: [PATCH 62/80] docs: Bound the Lean prelude's quantifiers to 4096 integers in the release notes. --- website/source/release-notes.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index c615fa3d1e..2b6a54f7a3 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -452,8 +452,8 @@ with the kernel, and a failure it shows reads ``(confirmed in Lean)``. A counterexample Lean cannot decide, as one that applies a ``cppverify::choose``, stays a failure with a warning, and one Lean decides the other way would be ``Unresolved``, a disagreement, never a failure. Lean decides a quantifier -over a range of integers by trying each one, within the heartbeats of a step -of ``cppverify_auto``. The release gate's Lean row now +over a range of at most 4096 integers by trying each one, within the +heartbeats of a step of ``cppverify_auto``. The release gate's Lean row now decides every case of its matrix: each valid one certified, each invalid one refuted (:doc:`book/part-ii/ch17-backends-modular-calls`). From 61f543b538655851d1711036bf4fd7b9520cf46e Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 09:25:15 +0530 Subject: [PATCH 63/80] verify: Record the pointer and reference parameters that address a record. --- clang/lib/Verify/IR/VStmt.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/clang/lib/Verify/IR/VStmt.h b/clang/lib/Verify/IR/VStmt.h index 816f9f6910..3164896888 100644 --- a/clang/lib/Verify/IR/VStmt.h +++ b/clang/lib/Verify/IR/VStmt.h @@ -423,6 +423,10 @@ struct VFunction { /// they bind (perhaps a field of a larger object). A reference to a record /// is a pointer to it, and `modifies(r)` its object. std::set ScalarReferenceParams; + /// Pointer and reference parameters to a record, with the identity of the + /// record's entry in Layouts: an object whose leaves lie at offsets inside + /// it. + std::map RecordParams; /// Pointer and reference parameters to const objects: the function /// writes nothing through them. std::set ConstAddressParams; From c132d065e5a234cfdb79aeeb0efcfab1f9121d1a Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 09:25:16 +0530 Subject: [PATCH 64/80] verify: Clone a function's record parameters. --- clang/lib/Verify/IR/VStmt.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/lib/Verify/IR/VStmt.cpp b/clang/lib/Verify/IR/VStmt.cpp index 88f5970470..90348d6bc9 100644 --- a/clang/lib/Verify/IR/VStmt.cpp +++ b/clang/lib/Verify/IR/VStmt.cpp @@ -198,6 +198,7 @@ VFunction verify::cloneVFunction(const VFunction &Fn) { Out.Params = Fn.Params; Out.SourceVariables = Fn.SourceVariables; Out.ScalarReferenceParams = Fn.ScalarReferenceParams; + Out.RecordParams = Fn.RecordParams; Out.ConstAddressParams = Fn.ConstAddressParams; Out.BoundedPointers = Fn.BoundedPointers; Out.ReturnFields = Fn.ReturnFields; From 98aced80939783ed99e5904835d59d12d60b6d64 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 09:25:16 +0530 Subject: [PATCH 65/80] verify: Keep a function's record parameters through loop unrolling. --- clang/lib/Verify/Transform/LoopUnroll.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/clang/lib/Verify/Transform/LoopUnroll.cpp b/clang/lib/Verify/Transform/LoopUnroll.cpp index 80c2dc5254..c22a67864d 100644 --- a/clang/lib/Verify/Transform/LoopUnroll.cpp +++ b/clang/lib/Verify/Transform/LoopUnroll.cpp @@ -256,6 +256,7 @@ VFunction LoopUnroller::unroll(const VFunction &Fn, unsigned K) { Out.Params = Fn.Params; Out.SourceVariables = Fn.SourceVariables; Out.ScalarReferenceParams = Fn.ScalarReferenceParams; + Out.RecordParams = Fn.RecordParams; Out.ConstAddressParams = Fn.ConstAddressParams; Out.BoundedPointers = Fn.BoundedPointers; Out.ReturnFields = Fn.ReturnFields; From 9ff5f65e2986f3e1b5867d11499e9c741fe40f77 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 09:25:17 +0530 Subject: [PATCH 66/80] verify: Pass the address of a local to a pointer parameter, and record the parameters that address a record. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 32 ++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index 795f625d8f..ba762b436a 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -3088,6 +3088,19 @@ ASTConverter::convertFunction(const FunctionDecl *FD) { return nullptr; } collectLayouts(FD, *Fn); + for (const ParmVarDecl *P : FD->parameters()) { + QualType Ty = P->getType(); + if (!Ty->isPointerType() && !Ty->isReferenceType()) + continue; + const std::string Identity = canonicalTypeIdentity( + Ty->getPointeeType().getCanonicalType().getUnqualifiedType(), Ctx); + if (Ty->getPointeeType()->isRecordType() && + llvm::any_of(Fn->Layouts, [&](const VObjectLayout &Layout) { + return Layout.Kind == VObjectKind::Record && + Layout.TypeIdentity == Identity; + })) + Fn->RecordParams[valueName(P)] = Identity; + } CurrentFn = nullptr; return Fn; } @@ -5495,6 +5508,25 @@ void ASTConverter::convertExecCallArg( "local, or direct pointer dereference"); return; } + // The address of a local object, or of a field or element of one, binds a + // pointer parameter as a reference argument binds a reference: the call + // checks that the callee keeps no pointer into it. + if (Formal && Formal->getType()->isPointerType()) + if (const auto *U = dyn_cast(E->IgnoreParenImpCasts()); + U && U->getOpcode() == UO_AddrOf && + !U->getSubExpr()->getType()->isArrayType() && + promotedRootLocal(U->getSubExpr())) { + std::unique_ptr AccessCondition; + Out = convertLValueAddress(U->getSubExpr(), &AccessCondition); + if (AccessCondition) + Prelude.push_back(std::make_unique( + std::move(AccessCondition), E->getExprLoc(), + ProofObligationKind::Bounds)); + if (Out) + appendReferenceBindingCheck(U->getSubExpr(), Out.get(), E->getExprLoc(), + Prelude); + return; + } const VarDecl *Source = directDynamicPointer(E); if (Source || isDynamicAddress(E)) { if (!Source || !Formal || !Formal->getType()->isPointerType() || From ced3b16bef173e585cde55024ea6949aa9f28e04 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 09:25:17 +0530 Subject: [PATCH 67/80] verify: Lend a local record to a callee that keeps no address of it, checking the whole record and its fields at the call. --- clang/lib/Verify/Transform/Passivize.cpp | 272 +++++++++++++++++++++-- 1 file changed, 259 insertions(+), 13 deletions(-) diff --git a/clang/lib/Verify/Transform/Passivize.cpp b/clang/lib/Verify/Transform/Passivize.cpp index e41db3316c..e5851c138b 100644 --- a/clang/lib/Verify/Transform/Passivize.cpp +++ b/clang/lib/Verify/Transform/Passivize.cpp @@ -1487,6 +1487,159 @@ static bool scalarDynamicCalleeSafe( return Safe; } +/// Whether a pointer-typed expression may hold an address derived from one +/// of the aliases. +static bool pointerFromAliases(const VExpr *E, + const std::set &Aliases) { + return E && E->Ty.Kind == VTypeKind::Ptr && referencesAnyAlias(E, Aliases); +} + +/// The pointer variables of a body that may hold an address derived from +/// the aliases: those assigned one, to a fixpoint. +static void +collectRecordAliases(const std::vector> &Body, + std::set &Aliases, bool &Changed) { + for (const auto &S : Body) { + switch (S->K) { + case VStmt::Assign: { + const auto &A = static_cast(*S); + if (pointerFromAliases(A.Value.get(), Aliases) && + Aliases.insert(A.Target).second) + Changed = true; + break; + } + case VStmt::If: { + const auto &I = static_cast(*S); + collectRecordAliases(I.Then, Aliases, Changed); + collectRecordAliases(I.Else, Aliases, Changed); + break; + } + case VStmt::While: + collectRecordAliases(static_cast(*S).Body, Aliases, + Changed); + break; + case VStmt::Seq: + collectRecordAliases(static_cast(*S).Stmts, Aliases, + Changed); + break; + case VStmt::GhostBlock: + collectRecordAliases(static_cast(*S).Body, + Aliases, Changed); + break; + default: + break; + } + } +} + +static bool +keepsNoAddress(const VFunction &Fn, const std::string &Param, bool AllowExtent, + const FunctionMap &FnMap, + std::set> &ActiveScans); + +/// Whether a statement keeps no address derived from the aliases beyond the +/// call: none is stored in memory, returned, freed, or passed to a callee +/// that keeps it. An address converted to an integer is no escape, since no +/// integer becomes a pointer again (the frontend rejects those casts). +static bool +recordStmtSafe(const VStmt &S, const std::set &Aliases, + const FunctionMap &FnMap, + std::set> &ActiveScans) { + auto Each = [&](const std::vector> &Body) { + return llvm::all_of(Body, [&](const std::unique_ptr &Nested) { + return recordStmtSafe(*Nested, Aliases, FnMap, ActiveScans); + }); + }; + switch (S.K) { + case VStmt::Store: + return !pointerFromAliases(static_cast(S).Value.get(), + Aliases); + case VStmt::Allocate: + case VStmt::Free: + // A function that allocates or frees is UsesDynamicStorage, which + // keepsNoAddress rejects before it looks at a statement. + return false; + case VStmt::If: { + const auto &I = static_cast(S); + return Each(I.Then) && Each(I.Else); + } + case VStmt::While: + return Each(static_cast(S).Body); + case VStmt::Call: { + const auto &C = static_cast(S); + auto CalleeIt = FnMap.find(C.CalleeIdentity); + if (CalleeIt == FnMap.end()) + return false; + const VFunction &Callee = *CalleeIt->second; + // The function passing an address proved that the callee's object or + // extent lies in its own, so the callee need only keep none, returning + // one included. + for (unsigned I = 0; I < C.Args.size(); ++I) + if (pointerFromAliases(C.Args[I].get(), Aliases) && + (I >= Callee.Params.size() || + Callee.Params[I].second.Kind != VTypeKind::Ptr || + !keepsNoAddress(Callee, Callee.Params[I].first, + /*AllowExtent=*/true, FnMap, ActiveScans))) + return false; + return true; + } + case VStmt::Return: + return !pointerFromAliases(static_cast(S).Value.get(), + Aliases); + case VStmt::Seq: + return Each(static_cast(S).Stmts); + case VStmt::GhostBlock: + return Each(static_cast(S).Body); + case VStmt::Assign: + case VStmt::Assert: + case VStmt::Assume: + case VStmt::ContractAssert: + case VStmt::EndLifetime: + case VStmt::Havoc: + case VStmt::RevealWithFuel: + case VStmt::HideSpec: + case VStmt::RevealSpec: + case VStmt::Break: + case VStmt::Continue: + return true; + } + return false; +} + +/// Whether Fn keeps no pointer into the object its parameter Param addresses +/// beyond the call. Fn is verified in the object model, so every access +/// through Param, at whatever field or element, is proved to lie in its +/// object (or its extent, which only a caller that proved the extent inside +/// its own object may give, AllowExtent); what remains is that no address +/// derived from it escapes. +static bool +keepsNoAddress(const VFunction &Fn, const std::string &Param, bool AllowExtent, + const FunctionMap &FnMap, + std::set> &ActiveScans) { + if (Fn.IsSpec || Fn.IsProof || Fn.IsExternalContract || + Fn.UsesDynamicStorage || !Fn.ObjectModel || + (!AllowExtent && + llvm::any_of(Fn.ValidExtents, [&](const VValidExtent &Extent) { + return Extent.Base == Param; + }))) + return false; + // An escape is a finite path to a statement that keeps an address, so a + // scan that reaches itself again, through recursion, may assume none. + const auto Key = std::make_pair(Fn.Identity, Param); + if (!ActiveScans.insert(Key).second) + return true; + std::set Aliases = {Param}; + for (bool Changed = true; Changed;) { + Changed = false; + collectRecordAliases(Fn.Body, Aliases, Changed); + } + bool Safe = true; + for (const auto &S : Fn.Body) + Safe = Safe && recordStmtSafe(*S, Aliases, FnMap, ActiveScans); + ActiveScans.erase(Key); + return Safe; +} + static bool pointerResultComesFrom(const VExpr *E, const std::set &Params) { if (!E) @@ -4932,6 +5085,72 @@ class PassivizerImpl { Loc)}; } + /// A record in local or dynamic storage passed to a parameter that + /// addresses one: the generated validity clause names its first byte, and + /// the callee reads every leaf as valid and initialized storage. Each byte + /// up to its last belongs to the live allocation of its first when the + /// last does (an allocation's bytes are contiguous), and each leaf must be + /// initialized, which C++ does not require of an out-parameter. + void emitRecordActualChecks( + PassiveProgram &P, const VFunction &Callee, + const std::set &DynamicParams, + const std::map> &ParamMap, + const CloneCtx &Ctx, SourceLocation Loc) { + if (!Fn.ObjectModel) + return; + for (const auto &[Name, Identity] : Callee.RecordParams) { + auto Actual = ParamMap.find(Name); + if (!DynamicParams.count(Name) || Actual == ParamMap.end()) + continue; + const auto Layout = + llvm::find_if(Callee.Layouts, [&](const VObjectLayout &L) { + return L.TypeIdentity == Identity; + }); + if (Layout == Callee.Layouts.end() || Layout->SizeBytes == 0) + continue; + auto Offset = [&](uint64_t Bytes) { + return addBytes(cloneVExpr(Actual->second.get()), + std::make_unique( + std::to_string(Bytes), pointerOffsetType(), Loc), + Loc); + }; + emitPassive(P, PassiveStmt::Assert, + std::make_unique( + VUnaryOp::ValidPtr, Offset(Layout->SizeBytes - 1), + VType::makeBool(), Loc, + stateHeapName(Ctx, VAllocationHeapName, ""), + stateHeapName(Ctx, VLivenessHeapName, "")), + nullptr, Loc, ProofObligationKind::PointerValidity); + std::vector Leaves; + for (const VObjectLeaf &Leaf : Layout->Leaves) { + std::vector Offsets = {Leaf.OffsetBytes}; + for (const VObjectRepeat &Repeat : Leaf.Repeats) { + std::vector Next; + for (uint64_t Base : Offsets) + for (uint64_t K = 0; K < Repeat.Count && Next.size() <= 4096; ++K) + Next.push_back(Base + K * Repeat.StrideBytes); + Offsets = std::move(Next); + } + Leaves.insert(Leaves.end(), Offsets.begin(), Offsets.end()); + } + std::unique_ptr Initialized; + if (Leaves.size() <= 4096) + for (uint64_t Leaf : Leaves) { + auto One = std::make_unique( + VUnaryOp::InitializedPtr, Offset(Leaf), VType::makeBool(), Loc, + "", "", stateHeapName(Ctx, VInitializationHeapName, "")); + Initialized = + Initialized ? makeAnd(std::move(Initialized), std::move(One), Loc) + : std::move(One); + } + emitPassive(P, PassiveStmt::Assert, + Initialized ? std::move(Initialized) + : makeBoolLiteral(Leaves.empty(), Loc), + nullptr, Loc, ProofObligationKind::Unsupported, + OutParameterNote); + } + } + /// The heap after a call of Callee whose footprints are ActualModifies /// (with ActualCounts) in the caller's state: each one it may write gets /// unknown contents, as a chain of stores when all are cells, and every @@ -4946,15 +5165,28 @@ class PassivizerImpl { const std::map> &ParamMap, const CloneCtx &Ctx, const std::string &EntryHeap, bool HasImplicitHeapEffect, SourceLocation Loc) { + // A footprint in a record that a parameter addresses is its bytes there, + // in local or dynamic storage too, and never the one cell at its start. + auto InRecordParam = [&](size_t I) { + const VExpr *Target = Callee.Modifies[I].Target.get(); + const VExpr *Root = + Target && Target->K == VExpr::Load + ? addressRoot(static_cast(Target)->Ptr.get()) + : nullptr; + return Root && Root->K == VExpr::Var && + Callee.RecordParams.count( + static_cast(Root)->Name); + }; bool CanFrameExactly = !ActualModifies.empty(); for (size_t I = 0; I < ActualModifies.size(); ++I) if (!ActualModifies[I] || ActualModifies[I]->K != VExpr::Load || ActualCounts[I] || (isRegionFootprint(Callee.Modifies[I], Callee.ScalarReferenceParams) && - !hasPointerProvenance( - static_cast(ActualModifies[I].get()) - ->Ptr.get()))) + (!hasPointerProvenance( + static_cast(ActualModifies[I].get()) + ->Ptr.get()) || + InRecordParam(I)))) CanFrameExactly = false; // A region footprint is its actual's object: the callee's extent, or one // object; in the object model the callee writes nowhere else. @@ -4965,9 +5197,10 @@ class PassivizerImpl { for (size_t I = 0; CanFrameRegions && I < ActualModifies.size(); ++I) { std::optional Bytes; if (ActualModifies[I] && ActualModifies[I]->K == VExpr::Load && - !hasPointerProvenance( - static_cast(ActualModifies[I].get()) - ->Ptr.get())) + (!hasPointerProvenance( + static_cast(ActualModifies[I].get()) + ->Ptr.get()) || + InRecordParam(I))) Bytes = footprintBytes(Callee, I, ActualModifies[I].get(), ActualCounts[I].get(), ParamMap, Ctx, EntryHeap, Loc); @@ -5052,15 +5285,24 @@ class PassivizerImpl { if (auto It = ParamMap.find(Param.first); It != ParamMap.end() && hasPointerProvenance(It->second.get())) { DynamicParams.insert(Param.first); + // A record a function in the object model reaches through the + // parameter is accessed only inside it, at any field or element. + const bool RecordObject = + Fn.ObjectModel && Callee->RecordParams.count(Param.first); if (Callee->IsProof || Callee->IsExternalContract || - !scalarDynamicCalleeSafe(*Callee, Param.first, FnMap, - ActiveScans)) { + !(RecordObject + ? keepsNoAddress(*Callee, Param.first, /*AllowExtent=*/false, + FnMap, ActiveScans) + : scalarDynamicCalleeSafe(*Callee, Param.first, FnMap, + ActiveScans))) { emitPassive(P, PassiveStmt::Assert, makeBoolLiteral(false, C.Loc), nullptr, C.Loc, ProofObligationKind::Unsupported, "the address of local or dynamic storage is passed to " + C.Callee + - ", which may keep, offset, or free it, or has no " - "verified body"); + (RecordObject + ? ", which may keep or free it" + : ", which may keep, offset, or free it") + + ", or has no verified body"); return; } } @@ -5300,6 +5542,7 @@ class PassivizerImpl { emitPassive(P, PassiveStmt::Assert, std::move(Part), nullptr, C.Loc, Kind, std::move(Note)); } + emitRecordActualChecks(P, *Callee, DynamicParams, ParamMap, Ctx, C.Loc); // A call within the caller's recursion cycle lowers the measure below its // value at the caller's entry, so assuming the callee's contract there is @@ -5361,9 +5604,12 @@ class PassivizerImpl { InnerBytes = calleeFootprintBytes(I); // An empty range writes nothing. if (ActualCounts[I] && InnerBytes) - Allowed = std::make_unique( - VBinOp::Le, cloneVExpr(InnerBytes->Hi.get()), - cloneVExpr(InnerBytes->Lo.get()), VType::makeBool(), C.Loc); + Allowed = makeOr(std::move(Allowed), + std::make_unique( + VBinOp::Le, cloneVExpr(InnerBytes->Hi.get()), + cloneVExpr(InnerBytes->Lo.get()), + VType::makeBool(), C.Loc), + C.Loc); for (size_t J = 0; J < CallerModifies.size(); ++J) { const auto &CallerM = CallerModifies[J]; const auto *CallerLoad = From 64bd1d2b78f5662d3879e01a737672a3c04b4a41 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 09:25:18 +0530 Subject: [PATCH 68/80] test: Check local records and addresses passed to callees. --- .../Verify/suite/local_record_arguments.cpp | 524 ++++++++++++++++++ 1 file changed, 524 insertions(+) create mode 100644 clang/test/Verify/suite/local_record_arguments.cpp diff --git a/clang/test/Verify/suite/local_record_arguments.cpp b/clang/test/Verify/suite/local_record_arguments.cpp new file mode 100644 index 0000000000..e43baefa16 --- /dev/null +++ b/clang/test/Verify/suite/local_record_arguments.cpp @@ -0,0 +1,524 @@ +// RUN: not %cpp-verify --jobs=1 %s -- 2>&1 | FileCheck %s +// RUN: not %cpp-verify --jobs=1 --backend=bmc --unroll=5 %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=BMC +// RUN: not %cpp-verify --jobs=1 --no-check-ub %s -- 2>&1 \ +// RUN: | FileCheck %s --check-prefix=NOUB +// RUN: %cpp-verify --lower-only --dump-ir=2 %s -- -DLOWER 2>&1 \ +// RUN: | FileCheck %s --check-prefix=PASSIVE +// +// A local record passed to a callee by reference, or by its address, keeps +// its lifetime and frame across the call. The callee is verified in the +// object model, so every access through its parameter, at any field or +// element, lies in the object; the call checks that the callee keeps no +// address of it (stores none, returns none, frees none, and passes it only to +// callees that keep none), that the whole record lies in the live object, and +// that every field is initialized. The callee then writes only its footprints +// in the record, by their bytes. + +struct Counter { + int n; + int limit; +}; + +struct Pair { + Counter left; + Counter right; +}; + +struct Ring { + int buf[4]; + int head; +}; + +void bump(Counter &c) + cppverify::pre(c.n < c.limit) + cppverify::modifies(c.n) + cppverify::post(c.n == cppverify::old(c.n) + 1) + cppverify::post(c.limit == cppverify::old(c.limit)) +{ + c.n = c.n + 1; +} +// CHECK-DAG: Verified: bump [backend=z3] + +void reset(Counter *c) + cppverify::pre(c != nullptr) + cppverify::modifies(*c) + cppverify::post(c->n == 0 && c->limit == 10) +{ + c->n = 0; + c->limit = 10; +} + +int by_reference() + cppverify::post(cppverify::result == 1) +{ + Counter c; + c.n = 0; + c.limit = 5; + bump(c); + return c.n; +} +// CHECK-DAG: Verified: by_reference [backend=z3] +// BMC-DAG: Verified: by_reference [backend=bmc, bound=0] +// NOUB-DAG: Unresolved: by_reference [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: the address of local or dynamic storage is passed to bump, which may keep, offset, or free it, or has no verified body) +// The generated clauses name the first byte; the call checks the last byte +// and every field. +// PASSIVE-LABEL: passive by_reference +// PASSIVE: assert precondition +// PASSIVE: assert pointer-validity +// PASSIVE: assert unsupported +// PASSIVE: assert pointer-validity +// PASSIVE-NEXT: || +// PASSIVE-NEXT: ! +// PASSIVE-NEXT: true +// PASSIVE-NEXT: valid_ptr +// PASSIVE-NEXT: + +// PASSIVE-NEXT: c_{{[0-9]+}} +// PASSIVE-NEXT: 7 +// PASSIVE-NEXT: assert unsupported +// PASSIVE-NEXT: || +// PASSIVE-NEXT: ! +// PASSIVE-NEXT: true +// PASSIVE-NEXT: && +// PASSIVE-NEXT: initialized_ptr +// PASSIVE-NEXT: + +// PASSIVE-NEXT: c_{{[0-9]+}} +// PASSIVE-NEXT: 0 +// PASSIVE-NEXT: initialized_ptr +// PASSIVE-NEXT: + +// PASSIVE-NEXT: c_{{[0-9]+}} +// PASSIVE-NEXT: 4 + +#ifndef LOWER +int keeps_limit() + cppverify::post(cppverify::result == 5) +{ + Counter c; + c.n = 0; + c.limit = 5; + bump(c); + return c.limit; +} +// CHECK-DAG: Verified: keeps_limit [backend=z3] + +int by_address() + cppverify::post(cppverify::result == 10) +{ + Counter c; + c.n = 3; + c.limit = 4; + reset(&c); + return c.limit; +} +// CHECK-DAG: Verified: by_address [backend=z3] + +int other_local() + cppverify::post(cppverify::result == 4) +{ + Counter c; + c.n = 0; + c.limit = 5; + int k = 4; + bump(c); + return k; +} +// CHECK-DAG: Verified: other_local [backend=z3] + +int wrong() + cppverify::post(cppverify::result == 5) +{ + Counter c; + c.n = 0; + c.limit = 5; + bump(c); + return c.n; +} +// CHECK-DAG: error: verification failed: wrong [{{.*}}::postcondition@[[@LINE-8]]:37] (counterexample: result [ssa=__result_1] [type=i32] = 1; + +// A member and an element of a local, and the address of a field. +int member() + cppverify::post(cppverify::result == 7) +{ + Pair p; + p.left.n = 0; + p.left.limit = 5; + p.right.n = 7; + p.right.limit = 9; + bump(p.left); + return p.right.n; +} +// CHECK-DAG: Verified: member [backend=z3] + +int element() + cppverify::post(cppverify::result == 1) +{ + Counter a[2]; + a[0].n = 0; + a[0].limit = 3; + a[1].n = 0; + a[1].limit = 3; + bump(a[1]); + return a[1].n - a[0].n; +} +// CHECK-DAG: Verified: element [backend=z3] + +void inc(int *p) + cppverify::pre(p != nullptr && *p < 100) + cppverify::modifies(*p) + cppverify::post(*p == cppverify::old(*p) + 1) +{ + *p = *p + 1; +} + +int field_address() + cppverify::post(cppverify::result == 1) +{ + Counter c; + c.n = 0; + c.limit = 1; + inc(&c.n); + return c.n; +} +// CHECK-DAG: Verified: field_address [backend=z3] + +int scalar_address() + cppverify::post(cppverify::result == 2) +{ + int x = 1; + inc(&x); + return x; +} +// CHECK-DAG: Verified: scalar_address [backend=z3] + +// The callee may reach the record through copies of the address, forward it +// to callees that keep none, and recurse. +void twice(Counter &c) + cppverify::pre(c.n + 1 < c.limit) + cppverify::modifies(c.n) + cppverify::post(c.n == cppverify::old(c.n) + 2) +{ + bump(c); + bump(c); +} + +int nested_calls() + cppverify::post(cppverify::result == 2) +{ + Counter c; + c.n = 0; + c.limit = 5; + twice(c); + return c.n; +} +// CHECK-DAG: Verified: nested_calls [backend=z3] + +void walk(Ring &r) + cppverify::modifies(r.buf[0 : 4]) + cppverify::post(cppverify::forall(k, 0, 4, r.buf[k] == 0)) +{ + for (int *q = r.buf; q != r.buf + 4; q = q + 1) + cppverify::invariant(r.buf <= q && q <= r.buf + 4) + cppverify::invariant(cppverify::forall(k, 0, q - r.buf, r.buf[k] == 0)) + cppverify::decreases(r.buf + 4 - q) + { + *q = 0; + } +} + +int walked() + cppverify::post(cppverify::result == 5) +{ + Ring r; + r.buf[0] = 1; + r.buf[1] = 2; + r.buf[2] = 3; + r.buf[3] = 4; + r.head = 5; + walk(r); + return r.buf[3] + r.head; +} +// CHECK-DAG: Verified: walked [backend=z3] + +void first_to(int *q, int v) + cppverify::pre(cppverify::valid(q, 4)) + cppverify::modifies(q[0]) + cppverify::post(q[0] == v) +{ + q[0] = v; +} + +void through_decay(Ring &r) + cppverify::modifies(r.buf[0]) + cppverify::post(r.buf[0] == 7) +{ + first_to(r.buf, 7); +} + +int decayed() + cppverify::post(cppverify::result == 7) +{ + Ring r; + r.buf[0] = 1; + r.buf[1] = 2; + r.buf[2] = 3; + r.buf[3] = 4; + r.head = 2; + through_decay(r); + return r.buf[0]; +} +// CHECK-DAG: Verified: decayed [backend=z3] + +void down(Counter &c, int k) + cppverify::pre(k >= 0) + cppverify::modifies(c.n) + cppverify::decreases(k) +{ + c.n = k; + if (k > 0) + down(c, k - 1); +} + +int recursive() + cppverify::post(cppverify::result == 9) +{ + Counter c; + c.n = 3; + c.limit = 9; + down(c, 3); + return c.limit; +} +// CHECK-DAG: Verified: recursive [backend=z3] + +// A range footprint in the caller's own object: before, the range's check +// that it may be empty replaced the check that the object is the caller's. +void clear(Ring &r) + cppverify::modifies(r.buf[0 : 4], r.head) + cppverify::post(r.head == 0 && cppverify::forall(k, 0, 4, r.buf[k] == 0)) +{ + for (int i = 0; i < 4; i = i + 1) + cppverify::invariant(0 <= i && i <= 4) + cppverify::invariant(cppverify::forall(k, 0, i, r.buf[k] == 0)) + cppverify::modifies(r.buf[0 : 4]) + cppverify::decreases(4 - i) + { + r.buf[i] = 0; + } + r.head = 0; +} + +int cleared() + cppverify::post(cppverify::result == 0) +{ + Ring r; + r.buf[0] = 1; + r.buf[1] = 2; + r.buf[2] = 3; + r.buf[3] = 4; + r.head = 2; + clear(r); + return r.buf[2] + r.head; +} +// CHECK-DAG: Verified: cleared [backend=z3] + +// The caller's own frame need not name its local. +void into_out(int *out) + cppverify::pre(out != nullptr) + cppverify::modifies(*out) + cppverify::post(*out == 1) +{ + Counter c; + c.n = 0; + c.limit = 5; + bump(c); + *out = c.n; +} +// CHECK-DAG: Verified: into_out [backend=z3] + +// Two locals are distinct objects; one passed twice is not. +void pair_bump(Counter &a, Counter &b) + cppverify::pre(a.n < 10 && b.n < 10) + cppverify::modifies(a.n, b.n) + cppverify::post(a.n == cppverify::old(a.n) + 1) + cppverify::post(b.n == cppverify::old(b.n) + 1) +{ + a.n = a.n + 1; + b.n = b.n + 1; +} + +int two_locals() + cppverify::post(cppverify::result == 2) +{ + Counter a; + a.n = 0; + a.limit = 0; + Counter b; + b.n = 0; + b.limit = 0; + pair_bump(a, b); + return a.n + b.n; +} +// CHECK-DAG: Verified: two_locals [backend=z3] + +int same_local() + cppverify::post(cppverify::result == 2) +{ + Counter a; + a.n = 0; + a.limit = 0; + pair_bump(a, a); + return a.n; +} +// CHECK-DAG: error: verification failed: same_local [{{.*}}::aliasing@[[@LINE-3]]:3] + +// Every field must be initialized: the callee reads its record as +// initialized storage, which C++ does not require of an out-parameter. +void set_n(Counter &c) + cppverify::modifies(c.n) + cppverify::post(c.n == 1) +{ + c.n = 1; +} + +int out_parameter() + cppverify::post(cppverify::result == 1) +{ + Counter c; + c.n = 0; + set_n(c); + return c.n; +} +// CHECK-DAG: [[@LINE-3]]:3: Unresolved: out_parameter [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: binding a reference or pointer parameter to storage that is not initialized, since the callee is verified as reading initialized storage) + +// A callee that keeps the address: in memory, or by returning it. +struct Node { + Node *self; + int v; +}; + +void selfref(Node &n) + cppverify::modifies(n.self) +{ + n.self = &n; +} + +int keeps_self() + cppverify::post(cppverify::result == 0) +{ + Node n; + n.self = nullptr; + n.v = 0; + selfref(n); + return 0; +} +// CHECK-DAG: [[@LINE-3]]:3: Unresolved: keeps_self [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: the address of local or dynamic storage is passed to selfref, which may keep or free it, or has no verified body) + +Counter *same(Counter *p) + cppverify::post(cppverify::result == p) +{ + return p; +} + +int returned() + cppverify::post(cppverify::result == 0) +{ + Counter c; + c.n = 0; + c.limit = 1; + Counter *q = same(&c); + return 0; +} +// CHECK-DAG: [[@LINE-3]]:3: Unresolved: returned [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: the address of local or dynamic storage is passed to same, which may keep or free it, or has no verified body) + +// A copy of the address is the address, and so is one passed on. +void keeps_copy(Node &n) + cppverify::modifies(n.self) +{ + Node *q = &n; + n.self = q; +} + +int copied() + cppverify::post(cppverify::result == 0) +{ + Node n; + n.self = nullptr; + n.v = 0; + keeps_copy(n); + return 0; +} +// CHECK-DAG: [[@LINE-3]]:3: Unresolved: copied [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: the address of local or dynamic storage is passed to keeps_copy, which may keep or free it, or has no verified body) + +void forwards(Node &n) + cppverify::modifies(n.self) +{ + selfref(n); +} + +int forwarded() + cppverify::post(cppverify::result == 0) +{ + Node n; + n.self = nullptr; + n.v = 0; + forwards(n); + return 0; +} +// CHECK-DAG: [[@LINE-3]]:3: Unresolved: forwarded [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: the address of local or dynamic storage is passed to forwards, which may keep or free it, or has no verified body) + +// An extent is not offered to a local: zero_two may write c and the record +// after it. +void zero_two(Counter *a, int n) + cppverify::pre(cppverify::valid(a, n) && 0 <= n && n <= 2) + cppverify::modifies(*a) +{ + for (int i = 0; i < n; i = i + 1) + cppverify::invariant(0 <= i && i <= n) + cppverify::decreases(n - i) + { + a[i].n = 0; + } +} + +int extent_two() + cppverify::post(cppverify::result == 0) +{ + Counter c; + c.n = 0; + c.limit = 1; + zero_two(&c, 2); + return 0; +} +// CHECK-DAG: [[@LINE-3]]:3: Unresolved: extent_two [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: the address of local or dynamic storage is passed to zero_two, which may keep or free it, or has no verified body) + +// A callee without a verified body, called directly or through another. +void opaque(Counter &c) + cppverify::modifies(c.n); + +void through_opaque(Counter &c) + cppverify::modifies(c.n) +{ + opaque(c); +} + +int nested_opaque() + cppverify::post(cppverify::result == 0) +{ + Counter c; + c.n = 0; + c.limit = 1; + through_opaque(c); + return 0; +} +// CHECK-DAG: [[@LINE-3]]:3: Unresolved: nested_opaque [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: the address of local or dynamic storage is passed to through_opaque, which may keep or free it, or has no verified body) + +int to_opaque() + cppverify::post(cppverify::result == 0) +{ + Counter c; + c.n = 0; + c.limit = 1; + opaque(c); + return 0; +} +// CHECK-DAG: [[@LINE-3]]:3: Unresolved: to_opaque [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: the address of local or dynamic storage is passed to opaque, which may keep or free it, or has no verified body) +#endif From fbf6564336c0e407ff910c3d8c4e810d3a164e9f Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 09:25:19 +0530 Subject: [PATCH 69/80] test: Expect a local record passed by reference to verify. --- clang/test/Verify/suite/record_references.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/clang/test/Verify/suite/record_references.cpp b/clang/test/Verify/suite/record_references.cpp index 87e778efcd..793013fc11 100644 --- a/clang/test/Verify/suite/record_references.cpp +++ b/clang/test/Verify/suite/record_references.cpp @@ -349,10 +349,10 @@ int by_reference(const Bounded &b) } // CHECK-DAG: error: verification failed: by_reference [{{.*}}::postcondition@[[@LINE-4]]:37] -// Not yet: a local passed to a callee by reference, whose non-escape is not -// established for records (B3a-4), a pointer formed from a local through a -// reference, a whole record read through one, a proof function's reference, -// and rvalue and volatile references. +// A local passed to a callee by reference is checked at the call (see +// local_record_arguments.cpp). Not yet: a pointer formed from a local through +// a reference, a whole record read through one, a proof function's +// reference, and rvalue and volatile references. int local_to_callee() cppverify::post(cppverify::result == 1) { @@ -362,7 +362,7 @@ int local_to_callee() bump(c); return c.n; } -// CHECK-DAG: [[@LINE-3]]:3: Unresolved: local_to_callee [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: the address of local or dynamic storage is passed to bump, which may keep, offset, or free it, or has no verified body) +// CHECK-DAG: Verified: local_to_callee [backend=z3] int local_address() cppverify::post(cppverify::result == 0) From 2e87fff8fb0f5a8a30e766d2c577ab0627e560f0 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 09:25:19 +0530 Subject: [PATCH 70/80] docs: Describe local records passed to callees, with a checked example. --- website/source/language/structs.rst | 105 ++++++++++++++++++++++++++-- 1 file changed, 98 insertions(+), 7 deletions(-) diff --git a/website/source/language/structs.rst b/website/source/language/structs.rst index 6f82ceea6c..c3fdc86c43 100644 --- a/website/source/language/structs.rst +++ b/website/source/language/structs.rst @@ -259,15 +259,106 @@ may write, so ``p.right`` keeps its value. ``reset_count`` may write only footprint is every byte of the record, which only a footprint naming the record, or an object around it, contains. +Local records passed to callees +------------------------------- + +A local record may be passed to a reference parameter (``bump(c)``), and +the address of a local, of one of its fields, or of an element of a local +array (``&c``, ``&c.n``, ``&a[1]``) to a pointer parameter. The callee is +verified for an object it does not own, so every access it makes through +the parameter, at whatever field or element, is proved to lie in that +object. The call checks the rest: + +- the callee keeps no address of the local: it stores none in memory, + returns none, frees none, and passes one only to callees that keep none + themselves (recursion included). A callee without a verified body, or one + that may keep the address, makes the call ``Unresolved`` with reason + ``construct.unsupported`` (``the address of local or dynamic storage is + passed to f, which may keep or free it, or has no verified body``); +- the whole record lies in the live local; +- every field is initialized, since the callee reads its parameter's object + as initialized storage. C++ allows an out-parameter that is only written, + but the verifier does not model one yet: the call is ``Unresolved`` with + reason ``construct.unsupported``. + +The callee then writes only its footprints inside the local, by their bytes, +and every other local keeps its value. The caller's own +``cppverify::modifies`` need not name its locals. + +.. cppverify-example: unresolved half_initialized + +.. code-block:: cpp + + struct Counter { + int n; + int limit; + }; + + void bump(Counter &c) + cv::pre(c.n < c.limit) + cv::modifies(c.n) + cv::post(c.n == cv::old(c.n) + 1) + cv::post(c.limit == cv::old(c.limit)) + { + c.n = c.n + 1; + } + + void reset(Counter *c) + cv::pre(c != nullptr) + cv::modifies(*c) + cv::post(c->n == 0 && c->limit == 10) + { + c->n = 0; + c->limit = 10; + } + + void set_n(Counter &c) + cv::modifies(c.n) + cv::post(c.n == 1) + { + c.n = 1; + } + + int counted() + cv::post(cv::result == 11) + { + Counter c; + c.n = 0; + c.limit = 5; + bump(c); + int k = c.n; + reset(&c); + return k + c.limit; + } + + int half_initialized() + cv::post(cv::result == 1) + { + Counter c; + c.n = 0; + set_n(c); + return c.n; + } + +.. code-block:: text + + Verified: bump [backend=z3] + Verified: reset [backend=z3] + Verified: set_n [backend=z3] + Verified: counted [backend=z3] + counter.cpp:48:3: Unresolved: half_initialized [backend=z3] [reason=construct.unsupported] (the verifier cannot model a construct here: binding a reference or pointer parameter to storage that is not initialized, since the callee is verified as reading initialized storage) + +``half_initialized`` leaves ``c.limit`` uninitialized, and ``set_n`` would +read it as initialized. + +The address of a local is supported as a call argument only. Stored in a +pointer variable (``Counter *q = &c;``), or formed through a local reference +to a local (``&r.n``, ``r.buf``), it is still an error. Under +``--no-check-ub`` the callee's accesses are not proved to lie in its object, +so a call that passes a local record is ``construct.unsupported``. + Not yet supported: -- a local record passed to a reference or pointer parameter (``bump(c)`` with - ``Counter c;``): the verifier does not yet show that the callee keeps no - pointer to it, and the call is ``Unresolved`` with reason - ``construct.unsupported``. A local reference may bind a local record, and - reads and writes through it are checked against that object's lifetime and - initialization, but forming a pointer through such a reference (``&r.n``, - ``r.buf``) is an error; - reading a whole record through a reference, as through a pointer; - reference returns, rvalue and ``volatile`` references, and references in spec and proof functions. From d9595bbb1edaccaab7ee8900d77c05f7335028ec Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 09:25:20 +0530 Subject: [PATCH 71/80] docs: Extend reference arguments to local records and addresses in chapter 14. --- website/source/book/part-ii/ch14-pointers-frames-modifies.rst | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/website/source/book/part-ii/ch14-pointers-frames-modifies.rst b/website/source/book/part-ii/ch14-pointers-frames-modifies.rst index e0c0cd1e5f..308aeffd70 100644 --- a/website/source/book/part-ii/ch14-pointers-frames-modifies.rst +++ b/website/source/book/part-ii/ch14-pointers-frames-modifies.rst @@ -54,7 +54,9 @@ is present. Reference formals can be forwarded from another reference, bound to a direct dereference such as ``set_value(*p, value)``, bound to a field or element of a local object or of a parameter's buffer (``set_value(pt.x, 7)``, -``set_value(a[1], 9)``), or passed an initialized ordinary scalar local. Local +``set_value(a[1], 9)``), or passed an initialized local, scalar or record, +as can the address of one to a pointer parameter (``inc(&x)``), when the +callee keeps no address of it (see :doc:`../../language/structs`). Local references may bind those same forms and chain: .. cppverify-example: with swap From 4f6c7e13c4ebf28f5527c36117455edb20f08a8d Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 09:25:20 +0530 Subject: [PATCH 72/80] docs: List local objects passed to callees as supported in the limitations. --- website/source/language/limitations.rst | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 70d3943bfa..7b2fb7dcc7 100644 --- a/website/source/language/limitations.rst +++ b/website/source/language/limitations.rst @@ -120,7 +120,9 @@ C++ feature boundaries reinterpretation. * - References - Scalar ``T&``/``const T&`` parameters on contracted executable free - functions, initialized ordinary scalar local actuals, local aliases for + functions, initialized local actuals (scalars and records, and + ``&x`` of one passed to a pointer parameter, when the callee keeps no + address of it), local aliases for boolean, integral, and enum referents, and bindings to a field or fixed array element of a promoted local object, or to a field or element of a parameter's buffer or of a record a pointer addresses @@ -130,8 +132,10 @@ C++ feature boundaries of the object it names (:doc:`structs`). - Conditional bindings, reference returns, rvalue references, temporaries/lifetime extension, reference members, and forwarding; a - local record passed to a reference parameter (``construct.unsupported``) - and a pointer formed through a local reference to a local record. + local not fully initialized passed to a callee + (``construct.unsupported``), the address of a local stored in a + variable, and a pointer formed through a local reference to a local + record. * - Arrays - Pointer-parameter indexing, quantified abstract buffers, fixed local arrays (including arrays of records and multidimensional arrays) @@ -293,8 +297,10 @@ order; heap-reading return values are materialized before teardown. Scalar references may bind supported fields and fixed-array elements of these promoted objects, and a local reference to a record may bind a promoted record. Conditional bindings, temporaries, reference returns, general raw -address-taking/array decay (through such a reference too), rvalue references, -and passing a promoted record to a callee by reference remain fail-closed. Addressable declarations inside loops and ``cppverify::old`` of local +address-taking/array decay (through such a reference too, and ``&x`` but as +a call argument), and rvalue references remain fail-closed. A promoted object +passed to a callee, by reference or ``&x``, keeps its lifetime: the callee +must keep no address of it, and every field must be initialized. Addressable declarations inside loops and ``cppverify::old`` of local objects/bindings are also rejected; outer automatic locals and loop-local aliases are supported. Pointer leaves may retain abstract pointer values, but storing a provenance-bearing local dynamic pointer fails closed until pointer provenance is From efa9ef16a5d9776d17611ff279fba4376bc3b123 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 09:25:21 +0530 Subject: [PATCH 73/80] docs: Note local objects passed to callees in the release notes. --- website/source/release-notes.rst | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index b731d2b6f0..507b9f1dd0 100644 --- a/website/source/release-notes.rst +++ b/website/source/release-notes.rst @@ -278,8 +278,18 @@ A reference to a record is now a pointer to it that is never null and never reseated: ``c.n`` and ``c.buf[i]`` are cells of the object, ``&c.n`` and ``c.buf`` point into it, ``cppverify::modifies(c)`` is the whole object, and a reference can be bound to ``*p``, ``p->left``, ``a[i]``, or another -reference. Passing a local record to a reference parameter is still -``construct.unsupported`` (:doc:`language/structs`). +reference (:doc:`language/structs`). + +**Local objects passed to callees.** A local record passed to a reference +parameter (``bump(c)``), and the address of any local passed to a pointer +parameter (``reset(&c)``, ``inc(&x)``, ``inc(&c.n)``), were +``construct.unsupported`` or errors (``raw address-of is unsupported until +lexical lifetime and escape effects are modeled``). They are verified now +when the callee keeps no address of the local, which the call checks: it +stores none in memory, returns none, frees none, and passes one only to +callees that keep none. The callee writes only its footprints in the local, +and every field of a record must be initialized, since the callee reads it as +initialized (:doc:`language/structs`). Running cpp-verify ~~~~~~~~~~~~~~~~~~ From 3b4e989e2c95c1468a71c82e00e1dfc5a867c5bf Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 09:25:22 +0530 Subject: [PATCH 74/80] docs: Describe local objects passed to callees in the design. --- docs/DESIGN.md | 49 +++++++++++++++++++++++++++++++++++++++++-------- 1 file changed, 41 insertions(+), 8 deletions(-) diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 17b800de43..1ee4485b3e 100644 --- a/docs/DESIGN.md +++ b/docs/DESIGN.md @@ -1204,11 +1204,43 @@ void reset_left(Pair &p) and writes through it carry that object's lifetime and initialization checks, but a pointer formed through it would not, and is rejected (as `&local` is). -- Not yet: a local record passed to a reference or pointer parameter. The - non-escape scan that admits a local scalar actual does not cover records, - so the call is `Unresolved` (`construct.unsupported`). Also rejected: a - whole record read through a reference, reference returns, rvalue and - `volatile` references, and references in spec and proof functions. +- A local record may be passed to a reference parameter, and the address + of a local, a field, or an element (`&c`, `&c.n`, `&a[1]`) to a pointer + parameter: see 3d. Rejected: a whole record read through a reference, + reference returns, rvalue and `volatile` references, and references in + spec and proof functions. + +### 3d. Local objects passed to callees + +- A callee verified in the object model proves that every access through + its parameter, at any field or element, lies in the parameter's object (its + one object; its `valid` extent is not offered to a local). So a local can + be lent to it as long as no address of the local outlives the call, which + is a property of the callee's body: the call checks (`keepsNoAddress`) that + it stores no address derived from the parameter in memory, returns none, + frees none, and passes one only to callees that keep none, with a verified + body (not an external contract, a proof, or a function that allocates). + The addresses derived from the parameter are the variables assigned one, + closed to a fixpoint (copies, steps, subobject pointers, local references). + A scan that reaches itself again through recursion assumes the callee keeps + none, since an escape is a finite path to a statement that keeps one. An + address converted to an integer is no escape: no integer becomes a pointer + again. +- The generated validity clause of a reference or pointer parameter names + its first byte; for a record the call also checks that its last byte lies + in the same live allocation (an allocation's bytes are contiguous) and that + every leaf is initialized, since the callee reads it as initialized storage. + An out-parameter, which C++ allows uninitialized, is + `construct.unsupported`, as for a scalar. +- The callee's footprints inside the record are framed by their bytes + (`HeapFrame`), a region as the whole record and never only its first cell; + its writes need no footprint of the caller's, since the local is the + caller's own. A scalar local keeps the exact one-cell rule and its + stricter scan (direct accesses only), since its region is one cell. +- `&x` is admitted only as a call argument; stored in a variable it is still + rejected, as is a pointer formed through a local reference to a local. In + `--no-check-ub` nothing proves the callee's accesses inside its object, so + a record local passed to a callee is `construct.unsupported`. ### 4. `cppverify::modifies(...)` frame condition @@ -1296,9 +1328,10 @@ int compute() { ``` `swap(x, x)` from a verified function fails the call's `aliasing` check. -Binding a reference to a local is supported; taking a local's raw address -(`&x`) is not yet: lexical lifetimes are modeled, but where a pointer to a -local goes is not. +Binding a reference to a local is supported, and so is passing a local's +address to a callee that keeps none (3d); storing a local's raw address +(`int *q = &x;`) is not yet: lexical lifetimes are modeled, but where a +pointer variable holding it goes is not. ## Type Invariants From 90d335e2fc0f164924284a7b66d8ddb7738d62f3 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 09:25:22 +0530 Subject: [PATCH 75/80] docs: Describe the record scan and the call's checks in the architecture. --- docs/ARCHITECTURE.md | 31 +++++++++++++++++++++++++++++-- 1 file changed, 29 insertions(+), 2 deletions(-) diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 73a24a0946..87386d58f5 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -2375,6 +2375,32 @@ rejects offset/subscript access, pointer copies/rebinding, recursive scan cycles, borrowed pointer-result intermediates without an owned summary, ghost access, proof/external contracts, and deallocation. +A record in local or dynamic storage takes a second scan, for a parameter in +`VFunction::RecordParams` (a pointer or reference to a record, with its +layout's identity) of a callee in the object model, whose own checks prove +that every access through the parameter lies in its object. +`keepsNoAddress` (`Transform/Passivize.cpp`) closes the parameter's aliases +over the pointer variables assigned an address derived from one, to a +fixpoint, and rejects a store of such an address, a return of one, a free, a +call that passes one to a callee that keeps one (scanned the same way, its +extent allowed, since the function passing it proved the extent inside its +own object) or that returns a pointer, and any callee without a verified +body; re-entering a scan through recursion assumes it holds. Offsets, steps, +comparisons, conversions to integers, spec arguments, and ghost reads are +admitted. At the call `emitRecordActualChecks` asserts the validity of the +record's last byte (with the generated clause's first, the record lies in +one live allocation) and the initialization of every leaf of the callee's +layout, enumerated (an automatic object has at most 256 bytes), as an +`unsupported` obligation with the out-parameter note. `havocFootprints` +frames a footprint rooted at such a parameter by its bytes through +`footprintBytes`, never as the exact first cell the scalar rule uses. The +frame check of the caller accepts the callee's footprints in its own +allocations; its empty-range alternative was joined to them (it replaced +them before, so a range in the caller's own object failed `frame`). +`ASTConverter::convertExecCallArg` lowers `&place` rooted at a promoted local +(not an array) passed to a pointer parameter as a reference binding: the +address with its provenance, the access condition, and the binding check. + A pointer-returning callee may return a direct dynamic formal, null, or a conditional selection of direct dynamic formals. `VCallStmt` carries a `ResultProvenanceTarget` alongside `ResultTarget`; passivization freshens both @@ -2419,8 +2445,9 @@ order, after materializing any heap-reading return value. Scalar references may bind fields and fixed-array elements with access-local nested bounds, and a local reference to a record may bind a promoted record, its provenance companion carried like a scalar reference's. General escape, raw array -decay/address-taking (through such a reference too), passing a promoted record -to a callee, and addressable declarations inside loops remain fail-closed; so does the decay of an array +decay/address-taking (through such a reference too, and `&x` other than as a +call argument, above), and addressable declarations inside loops remain +fail-closed; so does the decay of an array member through a pointer (`ASTConverter::arrayDecayError` names which). Automatic metadata transitions are private and a modular caller may frame them away. From 51cde57b4a375ddf50382a0bb03a14ccbc7fa5d5 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 09:40:29 +0530 Subject: [PATCH 76/80] verify: Test the result of Lean certification once, so a failure is a verdict and not an abort. --- clang/lib/Verify/Driver/Verifier.cpp | 25 ++++++++++++++++--------- 1 file changed, 16 insertions(+), 9 deletions(-) diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 6854f53d33..2833bf10a0 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -4721,18 +4721,22 @@ class Verifier { Diagnostic.Result->Message = Reason; } }; - auto Certified = - Lean->certifyLeanProject(ExportedGoals, LeanRefutations); + // The goals that failed, by name, once; testing an Expected that + // holds an error again would leave it unchecked. + std::optional> Certified; + std::string NotCertified; + if (auto Checked = + Lean->certifyLeanProject(ExportedGoals, LeanRefutations)) + Certified = std::move(*Checked); + else + NotCertified = llvm::toString(Checked.takeError()); std::map GoalsByName; for (const LeanProjectGoal &Goal : ExportedGoals) GoalsByName.emplace(Goal.Name, &Goal); - std::string NotCertified; if (!Certified) { - const std::string Reason = llvm::toString(Certified.takeError()); - NotCertified = Reason; for (size_t Index = 0; Index != Diags.size(); ++Index) if (Diags[Index].K == VerifyDiagnostic::Exported) - failed(Index, Reason); + failed(Index, NotCertified); } else { for (size_t Index = 0; Index != Diags.size(); ++Index) { VerifyDiagnostic &Diagnostic = Diags[Index]; @@ -5806,10 +5810,13 @@ verify::replayLeanProject(const std::vector &Modules, // A module is proved when each of its goals is certified. A bounded one // whose unwinding goals alone are not is safe within its bound: Lean // proves goals, and never refutes one. - auto Certified = Project.certifyLeanProject(Goals); + // As for source certification: the Expected is tested once. + std::optional> Certified; std::string Failed; - if (!Certified) - Failed = llvm::toString(Certified.takeError()); + if (auto Checked = Project.certifyLeanProject(Goals)) + Certified = std::move(*Checked); + else + Failed = llvm::toString(Checked.takeError()); std::map GoalsByName; for (const LeanProjectGoal &Goal : Goals) GoalsByName.emplace(Goal.Name, &Goal); From a3fa00e39a9e74db6efe7d4c903226724d8d4c2b Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 09:40:30 +0530 Subject: [PATCH 77/80] test: Check that replaying an archive reports a failed Lean certification. --- clang/test/Verify/suite/lean_toolchain.test | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/clang/test/Verify/suite/lean_toolchain.test b/clang/test/Verify/suite/lean_toolchain.test index 03b229fd70..8973e1f6a2 100644 --- a/clang/test/Verify/suite/lean_toolchain.test +++ b/clang/test/Verify/suite/lean_toolchain.test @@ -3,7 +3,7 @@ # outside elan must report the pinned Lean. # # UNSUPPORTED: system-windows -# RUN: rm -rf %t %t.project && mkdir -p %t/elan %t/plain +# RUN: rm -rf %t %t.project %t.replay && mkdir -p %t/elan %t/plain # Without automation at export, the goal is new to cppverify_auto whether or # not Lean is installed, so the certification run below tries it first. # RUN: %cpp-verify --backend=lean --no-lean-auto --lean-project=%t.project %S/Inputs/lean_toolchain.cpp -- @@ -14,11 +14,18 @@ # RUN: not env PATH=%t/elan %cpp-verify --backend=lean --lean-project=%t.project --lean-certify %S/Inputs/lean_toolchain.cpp -- 2>&1 | FileCheck %s --check-prefix=ELAN # RUN: FileCheck %s --input-file=%t/elan.log --check-prefix=ELAN-LOG # +# Replaying an archive certifies with the same steps; the failure is a +# verdict, which an assertions build once turned into an abort (an Expected +# tested again after its error was taken). +# RUN: %cpp-verify --obligation-out=%t/a.cpv %S/Inputs/lean_toolchain.cpp -- > /dev/null +# RUN: not env PATH=%t/elan %cpp-verify --obligation-in=%t/a.cpv --lean-project=%t.replay --lean-certify 2>&1 | FileCheck %s --check-prefix=REPLAY +# # RUN: printf '#!/bin/sh\necho "Lake version 5.0.0 (Lean version 4.1.0)"\n' > %t/plain/lake # RUN: chmod +x %t/plain/lake # RUN: not env PATH=%t/plain %cpp-verify --backend=lean --lean-project=%t.project --lean-certify %S/Inputs/lean_toolchain.cpp -- 2>&1 | FileCheck %s --check-prefix=PLAIN -DDIR=%t/plain # ELAN: Unresolved: lean obligation: trivial (Lean certification failed: command failed with exit code 1 +# REPLAY: Unresolved: trivial (Lean certification failed: command failed with exit code 1 # The trial of cppverify_auto, then certification, each with the pin. # ELAN-LOG: {{^}}+leanprover/lean4:v4.35.0 --version{{$}} From 76aa3b920d1204f8b5839f6743f65c80c9d5a001 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 11:16:54 +0530 Subject: [PATCH 78/80] verify: Mangle a constructor or destructor as its complete-object variant. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index e04ac734fa..68221e7583 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -845,9 +845,15 @@ std::string ASTConverter::functionIdentity(const FunctionDecl *FD) { std::string Mangled; llvm::raw_string_ostream OS(Mangled); std::unique_ptr MC(Ctx.createMangleContext()); - if (MC->shouldMangleDeclName(FD)) - MC->mangleName(GlobalDecl(FD), OS); - else + // A constructor or destructor is mangled as its complete-object variant. + if (MC->shouldMangleDeclName(FD)) { + if (const auto *Ctor = dyn_cast(FD)) + MC->mangleName(GlobalDecl(Ctor, Ctor_Complete), OS); + else if (const auto *Dtor = dyn_cast(FD)) + MC->mangleName(GlobalDecl(Dtor, Dtor_Complete), OS); + else + MC->mangleName(GlobalDecl(FD), OS); + } else OS << FD->getQualifiedNameAsString() << '\0' << FD->getType().getCanonicalType().getAsString(); OS.flush(); From 6e1b3f89df41ee3695d2920794de7ba41924d0a6 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 13:02:00 +0530 Subject: [PATCH 79/80] verify: Name a template or member function only when it has contracts to report, so no header's is mangled. --- clang/lib/Verify/Frontend/ASTConverter.cpp | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index 68221e7583..de8609aa69 100644 --- a/clang/lib/Verify/Frontend/ASTConverter.cpp +++ b/clang/lib/Verify/Frontend/ASTConverter.cpp @@ -1939,21 +1939,21 @@ std::vector> ASTConverter::convertTranslationUnit() { UsedConstexprSpecs.clear(); for (const FunctionDecl *FD : Definitions) { if (isa(FD) || FD->isTemplated()) { + // Only one with contracts is reported here: one without matters where + // verified code calls it, which reports the call. + if (!functionContract(FD) && !hasContractStatements(FD, Ctx)) + continue; llvm::SaveAndRestore Owner(ErrorFunction, functionIdentity(FD)); llvm::SaveAndRestore OwnerName(ErrorFunctionName, FD->getNameAsString()); llvm::SaveAndRestore InContract(ErrorInContract, true); if (isa(FD)) { - if (functionContract(FD) || hasContractStatements(FD, Ctx)) - error(FD->getLocation(), - FD->getNameAsString() + - ": member function verification is unsupported"); + error(FD->getLocation(), + FD->getNameAsString() + + ": member function verification is unsupported"); continue; } - // Only a template with contracts is reported here: one without - // matters where verified code calls it, which reports the call. if (!FD->isInStdNamespace() && - Ctx.getSourceManager().isWrittenInMainFile(FD->getLocation()) && - (functionContract(FD) || hasContractStatements(FD, Ctx))) + Ctx.getSourceManager().isWrittenInMainFile(FD->getLocation())) error(FD->getLocation(), FD->getNameAsString() + ": function template verification is unsupported"); From 7412ac91a3f5a400648aa93faccec40dad43f385 Mon Sep 17 00:00:00 2001 From: SwayamInSync Date: Sat, 24 Oct 2026 13:02:00 +0530 Subject: [PATCH 80/80] test: Check that a run under the Microsoft ABI mangles no template. --- clang/test/Verify/microsoft_identity.cpp | 29 ++++++++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 clang/test/Verify/microsoft_identity.cpp diff --git a/clang/test/Verify/microsoft_identity.cpp b/clang/test/Verify/microsoft_identity.cpp new file mode 100644 index 0000000000..feb8c18b5b --- /dev/null +++ b/clang/test/Verify/microsoft_identity.cpp @@ -0,0 +1,29 @@ +// RUN: %cpp-verify --jobs=1 %s -- --target=x86_64-pc-windows-msvc 2>&1 \ +// RUN: | FileCheck %s +// +// Only the functions the verifier converts or reports are named. A template +// or member function without contracts is neither, so it is never mangled; +// under the Microsoft ABI, whose mangler cannot mangle a dependent type, the +// templates of the standard headers made every run fail. + +template int length(const char (&s)[N]) { return N; } + +template struct Box { + T get() const { return v; } + T v; +}; + +struct Plain { + int get() const { return 0; } +}; + +int abs_value(int x) + cppverify::pre(x > -2147483647 - 1) + cppverify::post(cppverify::result >= 0) +{ + return x < 0 ? -x : x; +} + +// CHECK-NOT: error +// CHECK: Verified: abs_value [backend=z3] +// CHECK-NOT: error