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) { 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, diff --git a/clang/lib/Verify/Backend/LeanBackend.cpp b/clang/lib/Verify/Backend/LeanBackend.cpp index 25c590fa63..e58cd24d6c 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,41 @@ 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, 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) := + 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) := + 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"; + static void emitLeanFunctionDeclarations( const ObligationModule &Module, llvm::raw_ostream &OS, std::set &EmittedFunctions, @@ -1680,6 +1716,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 +1741,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, @@ -1757,7 +1865,13 @@ VerifyResult verify::exportLeanScratchPad( printLeanCommentText(Module.FunctionName, OS); OS << " -/\n"; OS << "/- required logic: " << formatLogicFeatures(Module.RequiredFeatures) - << " -/\n\n"; + << " -/\n"; + if (Module.BMCTransform) + OS << "/- bound: " << Module.BMCTransform->UnrollBound + << " loop iterations, by unrolling: these goals speak only of the\n" + " executions within them, and an unwinding goal says that every " + "loop\n ends within them -/\n"; + OS << "\n"; std::string TheoremName = "cppverify_" + @@ -1805,6 +1919,7 @@ VerifyResult verify::exportLeanScratchPad( Goal.LegacyName = encodeLeanName(ObligationName + "_goal"); Goal.LegacyBodyPrefix = LegacyBodyPrefix; Goal.Exported = Selected; + Goal.Unwinding = Item.Kind == ObligationKind::Unwinding; if (!Selected) { ProjectGoals->push_back(std::move(Goal)); continue; @@ -1847,4 +1962,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 diff --git a/clang/lib/Verify/Backend/LeanBackend.h b/clang/lib/Verify/Backend/LeanBackend.h index 176d58923d..c2cc672246 100644 --- a/clang/lib/Verify/Backend/LeanBackend.h +++ b/clang/lib/Verify/Backend/LeanBackend.h @@ -35,6 +35,9 @@ struct LeanProjectGoal { /// False for an obligation of an exported function that a selection left /// to the solver: its goal is known, but has no definition or proof file. bool Exported = true; + /// An unwinding goal of a bounded module: that its loops end within the + /// bound. + bool Unwinding = false; }; /// The group of a module's goals in a project: its function's directory. @@ -78,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; diff --git a/clang/lib/Verify/Backend/Obligation.cpp b/clang/lib/Verify/Backend/Obligation.cpp index 07524b070f..fa36569e16 100644 --- a/clang/lib/Verify/Backend/Obligation.cpp +++ b/clang/lib/Verify/Backend/Obligation.cpp @@ -2578,6 +2578,26 @@ verify::validateObligationModule(const ObligationModule &M) { ValidationError.c_str()); collectRequiredFeatures(Definition.get(), RequiredFeatures); } + // A measure only chooses an induction or Lean's termination argument, + // so it adds no feature; it must still be an integer over the + // parameters. + for (const auto &Measure : Declaration.Decreases) { + if (!validateLogicExpr(Measure.get(), ValidationError)) + return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", + ValidationError.c_str()); + if (Measure->Sort.Kind != LogicSortKind::MathematicalInteger && + Measure->Sort.Kind != LogicSortKind::BitVector) + return llvm::createStringError( + llvm::inconvertibleErrorCode(), + "logical function termination measure is not an integer"); + if (!validateLogicCalls(Measure.get(), M.LogicFunctions, + ValidationError) || + !validateVariableScopes(Measure.get(), ValidationError) || + !validateDefinitionVariables(Measure.get(), Parameters, {}, + ValidationError)) + return llvm::createStringError(llvm::inconvertibleErrorCode(), "%s", + ValidationError.c_str()); + } } return RequiredFeatures; } diff --git a/clang/lib/Verify/Backend/Obligation.h b/clang/lib/Verify/Backend/Obligation.h index a3281d8f53..e93984883f 100644 --- a/clang/lib/Verify/Backend/Obligation.h +++ b/clang/lib/Verify/Backend/Obligation.h @@ -230,7 +230,8 @@ class LogicExpr : public llvm::ThreadSafeRefCountedBase { std::vector Patterns; /// For an Or that states one assumption of a goal (`!A || rest`): where A /// comes from (`pre`, `call:f`, `def:x_1`), so a goal can be shown as - /// named hypotheses. Outside the term's meaning, identity, and archives. + /// named hypotheses. Outside the term's meaning and identity; archives + /// keep it with their source metadata. std::string Premise; explicit LogicExpr(Kind K) : K(K) {} @@ -355,7 +356,8 @@ struct LogicFunctionDecl { /// value; a verdict that does rests on them. Not archived. std::vector> Postconditions; /// A recursive function's termination measure over the parameters, by - /// which an induction over its applications descends. Not archived. + /// which an induction over its applications descends and Lean proves its + /// definition terminates. Archived, never hashed. std::vector> Decreases; static constexpr const char *ResultVariable = "cppverify.result"; }; diff --git a/clang/lib/Verify/Backend/ObligationSerialization.cpp b/clang/lib/Verify/Backend/ObligationSerialization.cpp index 547b55818f..6b20cf5979 100644 --- a/clang/lib/Verify/Backend/ObligationSerialization.cpp +++ b/clang/lib/Verify/Backend/ObligationSerialization.cpp @@ -501,17 +501,24 @@ class ArchiveWriter { writeU8(collectionTag(Expr->CollectionOp)); writeString(Expr->SpecCallee); writeSource(Expr->Source); + // Where an assumption comes from names its hypothesis in a readable + // Lean goal, as source points name a diagnostic's place. + if (IncludeSource && Expr->K == LogicExpr::Or) + writeString(Expr->Premise); writeU64(Expr->Children.size()); for (const auto &Child : Expr->Children) writeExpr(Child.get()); } + // A record keeps what a hash leaves out: the display name, and the + // termination measures, which change no meaning (Lean checks termination + // itself, and an induction descends by a well-founded relation whatever + // the measure). void writeFunction(const std::string &MapIdentity, - const LogicFunctionDecl &Function, - bool IncludeDisplayName) { + const LogicFunctionDecl &Function, bool Archived) { writeString(MapIdentity); writeString(Function.Identity); - writeString(IncludeDisplayName ? Function.DisplayName : ""); + writeString(Archived ? Function.DisplayName : ""); writeU64(Function.Parameters.size()); for (const LogicFunctionParameter &Parameter : Function.Parameters) { writeString(Parameter.Name); @@ -523,6 +530,11 @@ class ArchiveWriter { writeU64(Function.DefinitionLevels.size()); for (const auto &Definition : Function.DefinitionLevels) writeExpr(Definition.get()); + if (!Archived) + return; + writeU64(Function.Decreases.size()); + for (const auto &Measure : Function.Decreases) + writeExpr(Measure.get()); } void writeFunctionSignature(const std::string &MapIdentity, @@ -536,10 +548,10 @@ class ArchiveWriter { } void writeFunctions(const std::map &Functions, - bool IncludeDisplayNames) { + bool Archived) { writeU64(Functions.size()); for (const auto &[Identity, Function] : Functions) - writeFunction(Identity, Function, IncludeDisplayNames); + writeFunction(Identity, Function, Archived); } void writeModule(const ObligationModule &Module, @@ -804,6 +816,8 @@ class ArchiveReader { } Expr->SpecCallee = readString(); Expr->Source = readSource(IncludeSource); + if (Version >= 3 && IncludeSource && Expr->K == LogicExpr::Or) + Expr->Premise = readString(); uint64_t Children = readCount(); if (!Failure.empty()) @@ -839,6 +853,12 @@ class ArchiveReader { Function.DefinitionLevels.reserve(Levels); for (uint64_t I = 0; I != Levels && Failure.empty(); ++I) Function.DefinitionLevels.push_back(readExpr()); + if (Version >= 3) { + uint64_t Measures = readCount(); + Function.Decreases.reserve(Measures); + for (uint64_t I = 0; I != Measures && Failure.empty(); ++I) + Function.Decreases.push_back(readExpr()); + } return Function; } diff --git a/clang/lib/Verify/Backend/ObligationSerialization.h b/clang/lib/Verify/Backend/ObligationSerialization.h index 3eb10da883..944dcd85e8 100644 --- a/clang/lib/Verify/Backend/ObligationSerialization.h +++ b/clang/lib/Verify/Backend/ObligationSerialization.h @@ -12,7 +12,10 @@ namespace clang { namespace verify { -inline constexpr uint32_t ObligationSerializationVersion = 2; +/// Version 2 adds the precise obligation kinds; version 3 each logical +/// function's termination measures and, with source metadata, where each +/// assumption of a goal comes from. Readers read every earlier version. +inline constexpr uint32_t ObligationSerializationVersion = 3; inline constexpr uint32_t ObligationSemanticHashVersion = 4; /// Serialize one module as a deterministic, versioned binary record. Records diff --git a/clang/lib/Verify/Backend/ObligationSimplify.cpp b/clang/lib/Verify/Backend/ObligationSimplify.cpp index 3fc0f03d45..66154f06fe 100644 --- a/clang/lib/Verify/Backend/ObligationSimplify.cpp +++ b/clang/lib/Verify/Backend/ObligationSimplify.cpp @@ -363,10 +363,14 @@ void simplifyFunctions(ObligationModule &Module, auto Function = Module.LogicFunctions.find(Pending[I]); if (Function == Module.LogicFunctions.end()) continue; + // A function's declaration depends on what its definition and its + // measures apply. std::set Dependencies; collectCalledFunctions(Function->second.StepDefinition.get(), Dependencies); for (const auto &Definition : Function->second.DefinitionLevels) collectCalledFunctions(Definition.get(), Dependencies); + for (const auto &Measure : Function->second.Decreases) + collectCalledFunctions(Measure.get(), Dependencies); for (const std::string &Dependency : Dependencies) if (Reachable.insert(Dependency).second) Pending.push_back(Dependency); 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; 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); 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 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"; diff --git a/clang/lib/Verify/Driver/Verifier.cpp b/clang/lib/Verify/Driver/Verifier.cpp index 841c52b63f..00ff4c3233 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 { @@ -1548,129 +1550,23 @@ executeWithLogs(llvm::StringRef Program, return Stdout; } -class Verifier { - ASTContext &Ctx; - VerifyOptions Opts; - llvm::raw_ostream *DumpOS = nullptr; - std::vector Diags; +// A Lean project: its generated modules, the proof file of each goal, the +// trial of cppverify_auto, and certification. Source verification and +// archive replay both write one through it; what it warns of is kept for +// the caller to report. +class LeanProject { + const VerifyOptions &Opts; + std::vector Warnings; const std::string &leanProjectRoot() const { return Opts.LeanProjectPath.empty() ? Opts.LeanFallbackProjectPath : Opts.LeanProjectPath; } - /// The archive record of Module, empty without --obligation-out. - llvm::Expected archiveRecord(const ObligationModule &Module) { - if (!Opts.ObligationOut) - return std::string(); - - std::string Serialized = serializeObligationModule(Module); - auto RoundTrip = deserializeObligationModules(Serialized); - if (!RoundTrip) - return RoundTrip.takeError(); - if (RoundTrip->size() != 1 || - serializeObligationModule(RoundTrip->front()) != Serialized || - obligationSemanticHash(RoundTrip->front()) != - obligationSemanticHash(Module)) - return llvm::createStringError( - llvm::inconvertibleErrorCode(), - "canonical obligation serialization did not round-trip"); - return Serialized; - } - - llvm::Error emitObligationArchive(const ObligationModule &Module) { - llvm::Expected Record = archiveRecord(Module); - if (!Record) - return Record.takeError(); - if (Opts.ObligationOut) - *Opts.ObligationOut << *Record; - return llvm::Error::success(); - } - - void annotateObligationSources(ObligationModule &Module) { - const SourceManager &SourceMgr = Ctx.getSourceManager(); - auto annotateSource = [&](SourceLocation Loc, SourceLocation EndLoc, - ObligationSource &Source) { - if (!Loc.isValid()) - return; - PresumedLoc Location = SourceMgr.getPresumedLoc(Loc); - if (!Location.isValid()) - return; - ObligationSource Found; - Found.File = Location.getFilename(); - Found.Line = Location.getLine(); - Found.Column = Location.getColumn(); - PresumedLoc End = - SourceMgr.getPresumedLoc(EndLoc.isValid() ? EndLoc : Loc); - if (End.isValid() && Found.File == End.getFilename() && - (End.getLine() > Found.Line || - (End.getLine() == Found.Line && End.getColumn() >= Found.Column))) { - Found.EndLine = End.getLine(); - Found.EndColumn = End.getColumn(); - } else { - Found.EndLine = Found.Line; - Found.EndColumn = Found.Column; - } - // A term shared with a module annotated before, which other threads - // may be reading, is read and not written. - if (Source.File != Found.File || Source.Line != Found.Line || - Source.Column != Found.Column || Source.EndLine != Found.EndLine || - Source.EndColumn != Found.EndColumn) - Source = std::move(Found); - }; - // Terms share subterms: each node once. - llvm::DenseSet Annotated; - auto annotateExpr = [&](const LogicExpr *Root) { - if (!Root) - return; - std::vector Pending = {Root}; - while (!Pending.empty()) { - const LogicExpr *Expr = Pending.back(); - Pending.pop_back(); - if (!Annotated.insert(Expr).second) - continue; - annotateSource(Expr->Loc, Expr->EndLoc, Expr->Source); - for (const auto &Child : Expr->Children) - if (Child) - Pending.push_back(Child.get()); - } - }; +public: + explicit LeanProject(const VerifyOptions &Opts) : Opts(Opts) {} - annotateExpr(Module.CorrectnessGoal.get()); - annotateExpr(Module.CounterexampleQuery.get()); - std::map StableIdCounts; - for (Obligation &Item : Module.Obligations) { - annotateSource(Item.Loc, Item.EndLoc, Item.Source); - std::string StableId = - Module.FunctionIdentity + "::" + obligationKindName(Item.Kind) + "@"; - StableId += Item.Source.isValid() - ? std::to_string(Item.Source.Line) + ":" + - std::to_string(Item.Source.Column) - : "synthetic"; - unsigned &Count = StableIdCounts[StableId]; - if (++Count > 1) - StableId += "#" + std::to_string(Count); - Item.StableId = std::move(StableId); - annotateExpr(Item.Goal.get()); - annotateExpr(Item.CounterexampleQuery.get()); - } - for (auto &[InternalName, Variable] : Module.DiagnosticVariables) { - (void)InternalName; - annotateSource(Variable.Loc, Variable.EndLoc, Variable.Source); - } - for (DiagnosticTraceEvent &Event : Module.TraceEvents) { - annotateSource(Event.Loc, Event.EndLoc, Event.Source); - annotateExpr(Event.Guard.get()); - for (DiagnosticTraceValue &Value : Event.Values) - annotateExpr(Value.Value.get()); - } - for (auto &[Identity, Function] : Module.LogicFunctions) { - (void)Identity; - annotateExpr(Function.StepDefinition.get()); - for (auto &Definition : Function.DefinitionLevels) - annotateExpr(Definition.get()); - } - } + std::vector takeWarnings() { return std::move(Warnings); } llvm::Error initializeLeanProject() { const std::string &Root = leanProjectRoot(); @@ -1698,14 +1594,12 @@ class Verifier { LeanToolchain.str().c_str()); if (llvm::Error Error = writeTextFile(ToolchainPath, Toolchain)) return std::move(Error); - Diags.push_back( - {VerifyDiagnostic::Warning, - "the Lean project " + Root + " pinned " + Pin + - ", which an earlier release of cpp-verify wrote; it now " - "pins " + - LeanToolchain.str() + - ", so a proof that no longer builds needs updating for " - "that Lean"}); + Warnings.push_back("the Lean project " + Root + " pinned " + Pin + + ", which an earlier release of cpp-verify wrote; " + "it now pins " + + LeanToolchain.str() + + ", so a proof that no longer builds needs " + "updating for that Lean"); } } else if (llvm::Error Error = writeTextFile(ToolchainPath, Toolchain)) { return std::move(Error); @@ -1786,6 +1680,41 @@ class Verifier { 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"; @@ -1906,12 +1835,11 @@ class Verifier { moveLeanProof(Moving->Path, ProofPath, *Goal, Moving->Goal, Moving->BodyPrefix, groupOf(*Moving))) return Error; - Diags.push_back({VerifyDiagnostic::Warning, - "the Lean proof of " + Goal->StableId + - (WasKept ? " came back from " : " moved from ") + - relative(Moving->Path) + " to " + - relative(ProofPath) + - ", the file of the goal with its statement"}); + Warnings.push_back("the Lean proof of " + Goal->StableId + + (WasKept ? " came back from " : " moved from ") + + relative(Moving->Path) + " to " + + relative(ProofPath) + + ", the file of the goal with its statement"); Taken.insert(Moving->Path); Taken.insert(ProofPath); Emptied.insert(llvm::sys::path::parent_path(Moving->Path).str()); @@ -1922,11 +1850,9 @@ class Verifier { Goal->LegacyBodyPrefix)) return Error; if (!Stub) - Diags.push_back({VerifyDiagnostic::Warning, - "the Lean proof " + relative(LegacyPath) + - " that cpp-verify 0.1 wrote for " + - Goal->StableId + " is now " + - relative(ProofPath)}); + Warnings.push_back("the Lean proof " + relative(LegacyPath) + + " that cpp-verify 0.1 wrote for " + + Goal->StableId + " is now " + relative(ProofPath)); Legacy.erase(LegacyPath); Taken.insert(ProofPath); } else if (llvm::sys::fs::exists(ProofPath)) { @@ -1972,9 +1898,8 @@ class Verifier { llvm::raw_fd_ostream Note(Target, EC, llvm::sys::fs::OF_Append); if (!EC) Note << "\n" << LeanQuarantineNote << Why << "\n"; - Diags.push_back({VerifyDiagnostic::Warning, - "the Lean proof " + relative(Path) + " is kept in " + - relative(Target) + ": " + Why}); + Warnings.push_back("the Lean proof " + relative(Path) + " is kept in " + + relative(Target) + ": " + Why); return llvm::Error::success(); }; for (const LeanProofRecord &Record : Records) { @@ -2020,12 +1945,11 @@ class Verifier { if (std::error_code EC = llvm::sys::fs::remove_directories(StaleDir)) return llvm::createStringError(EC, "cannot remove %s", StaleDir.c_str()); - Diags.push_back({VerifyDiagnostic::Warning, - "removed " + - (Pruned == 1 ? std::string("the Lean proof") - : "the " + std::to_string(Pruned) + - " Lean proofs") + - " kept in Stale/, as --lean-prune-stale asks"}); + Warnings.push_back( + "removed " + + (Pruned == 1 ? std::string("the Lean proof") + : "the " + std::to_string(Pruned) + " Lean proofs") + + " kept in Stale/, as --lean-prune-stale asks"); } CheckFile += "\n"; @@ -2402,8 +2326,9 @@ class Verifier { } 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"); @@ -2430,11 +2355,37 @@ class Verifier { 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 @@ -2449,12 +2400,9 @@ class Verifier { 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)) @@ -2483,13 +2431,11 @@ class Verifier { 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; @@ -2522,9 +2468,9 @@ class Verifier { 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; } @@ -2720,9 +2666,9 @@ class Verifier { return Trials; } - // Each export's count of the goals cppverify_auto proves, from the proof - // files as they are now. - void countLeanAutomation(const std::vector &ProjectGoals) { + // The goals cppverify_auto proves, from the proof files as they are now. + std::set + automaticLeanGoals(const std::vector &ProjectGoals) const { std::set Automatic; for (const LeanProjectGoal &Goal : ProjectGoals) { std::string File; @@ -2733,12 +2679,7 @@ class Verifier { if (Record->Automatic) Automatic.insert(Goal.Name); } - for (VerifyDiagnostic &Diagnostic : Diags) - if (Diagnostic.K == VerifyDiagnostic::Exported && Diagnostic.Result) - Diagnostic.LeanAutomatic = llvm::count_if( - std::set(Diagnostic.Result->LeanGoals.begin(), - Diagnostic.Result->LeanGoals.end()), - [&](const std::string &Goal) { return Automatic.count(Goal); }); + return Automatic; } // Tries cppverify_auto on each goal whose proof file is still the one @@ -2771,9 +2712,8 @@ class Verifier { return; } auto skipped = [&](const std::string &Why) { - Diags.push_back( - {VerifyDiagnostic::Warning, - "cppverify_auto was not tried on the new Lean goals: " + Why}); + Warnings.push_back( + "cppverify_auto was not tried on the new Lean goals: " + Why); }; if (auto Build = Launcher->run({"build", "CppVerify.Generated", "CppVerify.User", "CppVerify.Auto"}, @@ -2838,10 +2778,135 @@ class Verifier { std::set Reported; for (const std::string &Failure : Failures) if (!Failure.empty() && Reported.insert(Failure).second) - Diags.push_back({VerifyDiagnostic::Warning, - "cppverify_auto stopped before every new Lean goal " - "was tried: " + - Failure}); + Warnings.push_back("cppverify_auto stopped before every new Lean goal " + "was tried: " + + Failure); + } +}; + +class Verifier { + ASTContext &Ctx; + VerifyOptions Opts; + llvm::raw_ostream *DumpOS = nullptr; + std::vector Diags; + std::optional Lean; + + void reportLeanWarnings() { + for (std::string &Warning : Lean->takeWarnings()) + Diags.push_back({VerifyDiagnostic::Warning, std::move(Warning)}); + } + + /// The archive record of Module, empty without --obligation-out. + llvm::Expected archiveRecord(const ObligationModule &Module) { + if (!Opts.ObligationOut) + return std::string(); + + std::string Serialized = serializeObligationModule(Module); + auto RoundTrip = deserializeObligationModules(Serialized); + if (!RoundTrip) + return RoundTrip.takeError(); + if (RoundTrip->size() != 1 || + serializeObligationModule(RoundTrip->front()) != Serialized || + obligationSemanticHash(RoundTrip->front()) != + obligationSemanticHash(Module)) + return llvm::createStringError( + llvm::inconvertibleErrorCode(), + "canonical obligation serialization did not round-trip"); + return Serialized; + } + + llvm::Error emitObligationArchive(const ObligationModule &Module) { + llvm::Expected Record = archiveRecord(Module); + if (!Record) + return Record.takeError(); + if (Opts.ObligationOut) + *Opts.ObligationOut << *Record; + return llvm::Error::success(); + } + + void annotateObligationSources(ObligationModule &Module) { + const SourceManager &SourceMgr = Ctx.getSourceManager(); + auto annotateSource = [&](SourceLocation Loc, SourceLocation EndLoc, + ObligationSource &Source) { + if (!Loc.isValid()) + return; + PresumedLoc Location = SourceMgr.getPresumedLoc(Loc); + if (!Location.isValid()) + return; + ObligationSource Found; + Found.File = Location.getFilename(); + Found.Line = Location.getLine(); + Found.Column = Location.getColumn(); + PresumedLoc End = + SourceMgr.getPresumedLoc(EndLoc.isValid() ? EndLoc : Loc); + if (End.isValid() && Found.File == End.getFilename() && + (End.getLine() > Found.Line || + (End.getLine() == Found.Line && End.getColumn() >= Found.Column))) { + Found.EndLine = End.getLine(); + Found.EndColumn = End.getColumn(); + } else { + Found.EndLine = Found.Line; + Found.EndColumn = Found.Column; + } + // A term shared with a module annotated before, which other threads + // may be reading, is read and not written. + if (Source.File != Found.File || Source.Line != Found.Line || + Source.Column != Found.Column || Source.EndLine != Found.EndLine || + Source.EndColumn != Found.EndColumn) + Source = std::move(Found); + }; + // Terms share subterms: each node once. + llvm::DenseSet Annotated; + auto annotateExpr = [&](const LogicExpr *Root) { + if (!Root) + return; + std::vector Pending = {Root}; + while (!Pending.empty()) { + const LogicExpr *Expr = Pending.back(); + Pending.pop_back(); + if (!Annotated.insert(Expr).second) + continue; + annotateSource(Expr->Loc, Expr->EndLoc, Expr->Source); + for (const auto &Child : Expr->Children) + if (Child) + Pending.push_back(Child.get()); + } + }; + + annotateExpr(Module.CorrectnessGoal.get()); + annotateExpr(Module.CounterexampleQuery.get()); + std::map StableIdCounts; + for (Obligation &Item : Module.Obligations) { + annotateSource(Item.Loc, Item.EndLoc, Item.Source); + std::string StableId = + Module.FunctionIdentity + "::" + obligationKindName(Item.Kind) + "@"; + StableId += Item.Source.isValid() + ? std::to_string(Item.Source.Line) + ":" + + std::to_string(Item.Source.Column) + : "synthetic"; + unsigned &Count = StableIdCounts[StableId]; + if (++Count > 1) + StableId += "#" + std::to_string(Count); + Item.StableId = std::move(StableId); + annotateExpr(Item.Goal.get()); + annotateExpr(Item.CounterexampleQuery.get()); + } + for (auto &[InternalName, Variable] : Module.DiagnosticVariables) { + (void)InternalName; + annotateSource(Variable.Loc, Variable.EndLoc, Variable.Source); + } + for (DiagnosticTraceEvent &Event : Module.TraceEvents) { + annotateSource(Event.Loc, Event.EndLoc, Event.Source); + annotateExpr(Event.Guard.get()); + for (DiagnosticTraceValue &Value : Event.Values) + annotateExpr(Value.Value.get()); + } + for (auto &[Identity, Function] : Module.LogicFunctions) { + (void)Identity; + annotateExpr(Function.StepDefinition.get()); + for (auto &Definition : Function.DefinitionLevels) + annotateExpr(Definition.get()); + } } void checkCalleeRecommendsOnFailure(const VFunction &Caller, @@ -3016,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) { @@ -3070,7 +3155,10 @@ class Verifier { // A project's goals go to modules, one per function. LeanProjectModules LeanModules; if (HasLeanProject) { - if (llvm::Error Error = initializeLeanProject()) { + Lean.emplace(Opts); + llvm::Error Error = Lean->initializeLeanProject(); + reportLeanWarnings(); + if (Error) { Diags.push_back({VerifyDiagnostic::Error, "cannot initialize Lean project (" + llvm::toString(std::move(Error)) + ")"}); @@ -3145,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 @@ -3249,6 +3337,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 @@ -3486,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 " @@ -4466,6 +4585,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 + "]"; @@ -4512,6 +4646,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; @@ -4519,6 +4654,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) @@ -4549,6 +4688,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) @@ -4566,13 +4709,29 @@ class Verifier { [](const LeanProjectGoal &Goal) { return Goal.Exported; }); const std::set *RunGroups = LeanFallbackBackend ? &LeanRunGroups : nullptr; - llvm::Error Finalized = writeLeanProjectModules(LeanModules); + 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 = finalizeLeanProject(LeanProjectGoals, RunGroups); + Finalized = Lean->finalizeLeanProject(LeanProjectGoals, RunGroups); + if (!Finalized && LeanFallbackBackend) + Finalized = Lean->writeLeanRefutations(LeanRefutations); if (!Finalized && Opts.LeanAuto) - automateLeanProject(LeanProjectGoals); - if (!Finalized) - countLeanAutomation(LeanProjectGoals); + Lean->automateLeanProject(LeanProjectGoals); + reportLeanWarnings(); + if (!Finalized) { + // Each export's count of the goals cppverify_auto proves. + const std::set Automatic = + Lean->automaticLeanGoals(LeanProjectGoals); + for (VerifyDiagnostic &Diagnostic : Diags) + if (Diagnostic.K == VerifyDiagnostic::Exported && Diagnostic.Result) + Diagnostic.LeanAutomatic = llvm::count_if( + std::set(Diagnostic.Result->LeanGoals.begin(), + Diagnostic.Result->LeanGoals.end()), + [&](const std::string &Goal) { return Automatic.count(Goal); }); + } if (Finalized) { AllOk = false; AnyFailed = true; @@ -4580,7 +4739,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. @@ -4605,15 +4764,22 @@ class Verifier { Diagnostic.Result->Message = Reason; } }; - auto Certified = certifyLeanProject(ExportedGoals); + // 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); if (!Certified) { - const std::string Reason = llvm::toString(Certified.takeError()); 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]; @@ -4677,6 +4843,11 @@ class Verifier { Diagnostic.Message += " [vacuous]"; } } + + if (Certified) + RefutationChecks = *Certified; + else + RefutationsUnchecked = NotCertified; } } for (const SpecReliance &Check : ProofDependencies) @@ -4797,6 +4968,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 " @@ -4831,9 +5004,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)); @@ -4850,7 +5026,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"); @@ -5205,6 +5386,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) { @@ -5354,6 +5583,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()) @@ -5580,4 +5811,101 @@ bool verify::verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS, bool Ok = V.run(); V.printDiagnostics(OS); return Ok; +} + +LeanProjectReplay +verify::replayLeanProject(const std::vector &Modules, + const VerifyOptions &Opts) { + LeanProjectReplay Replay; + LeanProject Project(Opts); + auto report = [&] { + for (std::string &Warning : Project.takeWarnings()) + Replay.Warnings.push_back(std::move(Warning)); + }; + llvm::Error Error = Project.initializeLeanProject(); + report(); + if (Error) { + Replay.Error = "cannot initialize Lean project (" + + llvm::toString(std::move(Error)) + ")"; + return Replay; + } + + // The goals have the names, files, and proofs a source run gives the + // same obligations, since both name them by their statements. + std::vector Goals; + LeanProjectModules Generated; + LeanVerifyBackend Backend(&Generated, &Goals); + for (const ObligationModule &Module : Modules) { + VerifyResult Result = Backend.verify(Module); + if (Module.BMCTransform) + Result.Bound = Module.BMCTransform->UnrollBound; + Replay.Results.push_back(std::move(Result)); + } + Error = Project.writeLeanProjectModules(Generated); + if (!Error) + Error = Project.finalizeLeanProject(Goals, nullptr); + if (!Error && Opts.LeanAuto) + Project.automateLeanProject(Goals); + report(); + if (Error) { + Replay.Error = "cannot finalize Lean project (" + + llvm::toString(std::move(Error)) + ")"; + return Replay; + } + const std::set Automatic = Project.automaticLeanGoals(Goals); + for (const VerifyResult &Result : Replay.Results) + Replay.Automatic.push_back(llvm::count_if( + std::set(Result.LeanGoals.begin(), Result.LeanGoals.end()), + [&](const std::string &Goal) { return Automatic.count(Goal); })); + if (!Opts.LeanCertify || interruptRequested()) + return Replay; + + // 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. + // As for source certification: the Expected is tested once. + std::optional> Certified; + std::string Failed; + 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); + for (VerifyResult &Result : Replay.Results) { + if (Result.Status != VerifyStatus::Exported) + continue; + std::string Reason = Failed; + bool OnlyUnwinding = Failed.empty(); + if (Certified) + for (const std::string &Goal : std::set( + Result.LeanGoals.begin(), Result.LeanGoals.end())) + if (auto Failure = Certified->find(Goal); Failure != Certified->end()) { + const LeanProjectGoal *Known = GoalsByName.at(Goal); + OnlyUnwinding = OnlyUnwinding && Known->Unwinding; + if (Result.ObligationId.empty()) + Result.ObligationId = Known->StableId; + Reason += (Reason.empty() ? "" : "; ") + + std::string("the proof of ") + Known->StableId + ": " + + Failure->second; + } + if (Reason.empty()) { + Result.Status = VerifyStatus::Verified; + Result.Reason = VerifyReason::None; + Result.Message.clear(); + } else if (Result.Bound && OnlyUnwinding) { + Result.Status = VerifyStatus::BoundedSafe; + Result.Reason = VerifyReason::IncompleteBound; + Result.Message = "every goal is certified but the unwinding: no " + "execution within " + + std::to_string(*Result.Bound) + + " loop iterations fails (" + Reason + ")"; + } else { + Result.Status = VerifyStatus::Unresolved; + Result.Reason = VerifyReason::LeanExportFailure; + Result.Message = "Lean certification failed: " + Reason; + } + } + return Replay; } \ No newline at end of file diff --git a/clang/lib/Verify/Driver/Verifier.h b/clang/lib/Verify/Driver/Verifier.h index 887f375853..2407637712 100644 --- a/clang/lib/Verify/Driver/Verifier.h +++ b/clang/lib/Verify/Driver/Verifier.h @@ -91,6 +91,25 @@ struct VerifyOptions { bool verifyTranslationUnit(ASTContext &Ctx, llvm::raw_ostream &OS, const VerifyOptions &Opts = VerifyOptions()); + +/// What exporting the modules of an archive to a Lean project gives: a +/// result for each module, in order, with the goals cppverify_auto proves of +/// it, and what the project warns of; or why the project was not written. +struct LeanProjectReplay { + std::vector Results; + std::vector Automatic; + std::vector Warnings; + std::string Error; +}; + +/// Exports Modules to the Lean project of Opts as a source run exports its +/// functions, with their proofs and cppverify_auto, and with LeanCertify +/// certifies them. A module alone is all that is checked: one whose goals +/// all certify is Verified, its obligations proved; a bounded one is +/// BoundedSafe when only unwinding goals do not. +LeanProjectReplay +replayLeanProject(const std::vector &Modules, + const VerifyOptions &Opts); } // namespace verify } // namespace clang diff --git a/clang/lib/Verify/Frontend/ASTConverter.cpp b/clang/lib/Verify/Frontend/ASTConverter.cpp index 6b2d271bd9..a276c8f47c 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)) @@ -845,9 +858,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(); @@ -1003,11 +1022,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 +1190,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)) @@ -1903,6 +1923,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,19 +1952,22 @@ 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)) + 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)) { 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()) { + continue; + } 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"); @@ -1930,12 +1975,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 +2036,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 +2099,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 +2193,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 +2261,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 +2283,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 +2303,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 +2369,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 +2625,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 @@ -2661,8 +2736,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)); @@ -2948,6 +3023,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 +3059,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 +3088,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; } @@ -3082,6 +3161,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); } @@ -3157,6 +3254,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 +3304,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; } @@ -3318,7 +3420,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); } @@ -3434,6 +3536,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 = @@ -3598,6 +3722,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()); @@ -3883,6 +4010,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()); @@ -4649,7 +4779,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; @@ -4829,7 +4959,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 " @@ -5128,7 +5258,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 + @@ -5136,7 +5266,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); @@ -5751,7 +5882,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; } @@ -5805,7 +5936,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; } diff --git a/clang/lib/Verify/Frontend/ASTConverter.h b/clang/lib/Verify/Frontend/ASTConverter.h index abf66a2105..e1eb288972 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. @@ -132,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); @@ -170,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. diff --git a/clang/lib/Verify/IR/VStmt.cpp b/clang/lib/Verify/IR/VStmt.cpp index 2d7a0a134d..88f5970470 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; @@ -196,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; diff --git a/clang/lib/Verify/IR/VStmt.h b/clang/lib/Verify/IR/VStmt.h index b5c84ce10d..816f9f6910 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; @@ -415,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; 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 " 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 diff --git a/clang/lib/Verify/Transform/LoopUnroll.cpp b/clang/lib/Verify/Transform/LoopUnroll.cpp index e6fe44f6a2..80c2dc5254 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; @@ -254,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; 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, 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"} 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 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 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) +{ +} 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..6b38456856 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_refutation_budget.cpp @@ -0,0 +1,31 @@ +// Refutations that are bounded, and refutations that are not reported, for +// lean_refutation.test. + +// 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)) +{ +} + +// 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)) +{ +} 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₁ diff --git a/clang/test/Verify/suite/Inputs/lean_replay.cpp b/clang/test/Verify/suite/Inputs/lean_replay.cpp new file mode 100644 index 0000000000..f2f232d87b --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_replay.cpp @@ -0,0 +1,33 @@ +// A program whose archive replays into a Lean project, for lean_replay.test. + +cppverify::spec int tri(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : tri(n - 1) + n; +} + +cppverify::proof void tri_nonneg(int n) + cppverify::post(tri(n) >= 0) +{ +} + +// A measure that applies a spec: its module keeps the spec it applies. +cppverify::spec int size(int n) { return n; } + +cppverify::spec int down(int n) + cppverify::decreases(size(n)) +{ + return n <= 0 ? 0 : down(n - 1); +} + +cppverify::proof void down_zero() + cppverify::post(down(0) == 0) +{ +} + +int inc(int x) + cppverify::pre(x < 100) + cppverify::post(cppverify::result == x + 1) +{ + return x + 1; +} diff --git a/clang/test/Verify/suite/Inputs/lean_replay_loops.cpp b/clang/test/Verify/suite/Inputs/lean_replay_loops.cpp new file mode 100644 index 0000000000..80232d4525 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_replay_loops.cpp @@ -0,0 +1,22 @@ +// Loops for a bounded archive, for lean_replay.test: one ends within the +// bound, one need not. + +int sum_small(int n) + cppverify::pre(0 <= n && n <= 2) + cppverify::post(cppverify::result >= 0) +{ + int s = 0; + for (int i = 0; i < n; i = i + 1) + s = s + i; + return s; +} + +int count_up(int n) + cppverify::pre(0 <= n && n <= 1000) + cppverify::post(cppverify::result == n) +{ + int c = 0; + while (c < n) + c = c + 1; + return c; +} diff --git a/clang/test/Verify/suite/Inputs/mutate_obligation_archive.py b/clang/test/Verify/suite/Inputs/mutate_obligation_archive.py index a057a36fe5..64dfac1893 100644 --- a/clang/test/Verify/suite/Inputs/mutate_obligation_archive.py +++ b/clang/test/Verify/suite/Inputs/mutate_obligation_archive.py @@ -18,6 +18,11 @@ def __init__(self, data): self.obligation_ids = [] self.obligation_kind_offsets = [] self.version_offsets = [] + self.version = 0 + # What schema 3 adds: measures and premises, which a record of an + # earlier schema has not. + self.measure_spans = [] + self.measures = [] self.modules = [] def u8(self): @@ -99,6 +104,11 @@ def expression(self, track=True): self.offset += 1 self.string() source = self.source() + if self.version >= 3 and self.flags & 1 and kind == 26: + # Schema 3 adds where an assumption comes from. + start = self.offset + self.string() + self.measure_spans.append((start, self.offset)) children_count_offset = self.offset children = [self.expression(track=track) for _ in range(self.u64())] return { @@ -124,12 +134,18 @@ def function(self): self.offset += 4 expressions = [self.expression()] expressions.extend(self.expression() for _ in range(self.u64())) + if self.version >= 3: + # Schema 3 adds the termination measures. + start = self.offset + for _ in range(self.u64()): + self.measures.append(self.expression()) + self.measure_spans.append((start, self.offset)) return expressions, identity def module(self): self.offset += 8 self.version_offsets.append(self.offset) - self.offset += 4 + self.version = self.u32() self.flags = self.u32() function_name = self.string() self.string() @@ -351,6 +367,8 @@ def invalidate_quantifier_binder_sort(self, node): "invalid-utf8", "schema-v1", "schema-v1-kinds", + "schema-v2", + "measure-free-variable", "truncated", ], ) @@ -364,14 +382,41 @@ def invalidate_quantifier_binder_sort(self, node): if args.mode == "invalid-kind": archive.data[archive.expression_kind_offsets[0]] = 255 -elif args.mode in ("schema-v1", "schema-v1-kinds"): +elif args.mode in ("schema-v1", "schema-v1-kinds", "schema-v2"): for offset in archive.version_offsets: - struct.pack_into(" 3: archive.data[offset] = 1 + # Records before schema 3 have no measures or premises; a premise + # inside a measure goes with it. + spans = sorted(archive.measure_spans) + outer = [ + span + for span in spans + if not any(o != span and o[0] <= span[0] and span[1] <= o[1] for o in spans) + ] + for start, end in reversed(outer): + del archive.data[start:end] +elif args.mode == "measure-free-variable": + def first_variable(node): + if node is None: + return None + if node["kind"] == 5 and node["name"][1] > 0: + return node + return next( + (found for child in node["children"] if (found := first_variable(child))), + None, + ) + variable = next( + (found for measure in archive.measures if (found := first_variable(measure))), + None, + ) + if variable is None: + raise ValueError("archive has no measure that reads a variable") + archive.data[variable["name"][0]] = ord("z") elif args.mode == "feature-mismatch": struct.pack_into("= 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; +} 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 ) 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 diff --git a/clang/test/Verify/suite/lean_refutation.test b/clang/test/Verify/suite/lean_refutation.test new file mode 100644 index 0000000000..9d98556ddd --- /dev/null +++ b/clang/test/Verify/suite/lean_refutation.test @@ -0,0 +1,89 @@ +# 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_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 +# BUDGET-NOT: the counterexample of far 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 diff --git a/clang/test/Verify/suite/lean_replay.test b/clang/test/Verify/suite/lean_replay.test new file mode 100644 index 0000000000..6b3b9484c1 --- /dev/null +++ b/clang/test/Verify/suite/lean_replay.test @@ -0,0 +1,99 @@ +# REQUIRES: lean +# +# An archive replays into a Lean project as its source exports: the same +# goals, specs, and proof files, so a proof written for the source certifies +# the archive's goal. Replay checks each module alone, as with a solver. +# +# RUN: rm -rf %t && mkdir -p %t +# RUN: %cpp-verify --lower-only --obligation-out=%t/a.cpv %S/Inputs/lean_replay.cpp -- +# RUN: %cpp-verify --backend=lean --lean-project=%t/src %S/Inputs/lean_replay.cpp -- 2>&1 | FileCheck %s --check-prefix=SOURCE +# RUN: %cpp-verify --obligation-in=%t/a.cpv --lean-project=%t/rep 2>&1 | FileCheck %s --check-prefix=REPLAY +# RUN: diff -r %t/src/CppVerify/Goals %t/rep/CppVerify/Goals +# RUN: diff %t/src/CppVerify/Specs.lean %t/rep/CppVerify/Specs.lean +# RUN: diff -r %t/src/CppVerify/Proofs %t/rep/CppVerify/Proofs +# RUN: FileCheck %s --input-file=%t/rep/CppVerify/Specs.lean --check-prefix=SPECS +# RUN: FileCheck %s --input-file=%t/rep/CppVerify/Goals/cppverify_inc_c0810e.lean --check-prefix=READABLE +# +# RUN: cp %S/Inputs/lean_spec_definitions_tri_nonneg.lean %t/rep/CppVerify/Proofs/cppverify_tri_nonneg_42a030/cppverify_tri_nonneg_42a030_postcondition_053b1980.lean +# RUN: %cpp-verify --obligation-in=%t/a.cpv --lean-project=%t/rep --lean-certify 2>&1 | FileCheck %s --check-prefix=CERTIFY +# RUN: %cpp-verify --obligation-in=%t/a.cpv --lean-project=%t/rep --diagnostics-format=json | FileCheck %s --check-prefix=JSON +# +# A record of schema 2 has no measures, and no names for a goal's +# assumptions: tri is opaque, and a readable goal names no hypothesis. +# RUN: %python %S/Inputs/mutate_obligation_archive.py schema-v2 %t/a.cpv %t/v2.cpv +# RUN: %cpp-verify --obligation-in=%t/v2.cpv --lean-project=%t/v2 2>&1 | FileCheck %s --check-prefix=REPLAY +# RUN: FileCheck %s --input-file=%t/v2/CppVerify/Specs.lean --check-prefix=SPECS-V2 +# RUN: FileCheck %s --input-file=%t/v2/CppVerify/Goals/cppverify_inc_c0810e.lean --check-prefix=READABLE-V2 +# +# A bounded module states its bound with its goals. Every goal of sum_small +# certifies, its unwinding included; count_up's unwinding does not, since +# its loop may run longer, and the rest shows it safe within the bound. +# RUN: not %cpp-verify --backend=bmc --unroll=3 --obligation-out=%t/b.cpv %S/Inputs/lean_replay_loops.cpp -- +# RUN: %cpp-verify --obligation-in=%t/b.cpv --backend=lean --lean-out=%t/b.lean 2>&1 | FileCheck %s --check-prefix=BOUNDED-EXPORT +# RUN: FileCheck %s --input-file=%t/b.lean --check-prefix=BOUND +# RUN: not %cpp-verify --obligation-in=%t/b.cpv --lean-project=%t/b --lean-certify 2>&1 | FileCheck %s --check-prefix=BOUNDED +# +# A replay moves and keeps proofs as a source run does: the proof of +# tri_nonneg, which no goal of the bounded archive has, is kept in Stale/. +# RUN: %cpp-verify --obligation-in=%t/b.cpv --lean-project=%t/rep 2>&1 | FileCheck %s --check-prefix=STALE +# RUN: test -f %t/rep/Stale/Proofs/cppverify_tri_nonneg_42a030/cppverify_tri_nonneg_42a030_postcondition_053b1980.lean +# Its goal back, it takes the proof back, which a JSON run says as JSON. +# RUN: %cpp-verify --obligation-in=%t/a.cpv --lean-project=%t/rep --diagnostics-format=json | FileCheck %s --check-prefix=BACK +# +# RUN: not %cpp-verify --obligation-in=%t/a.cpv --lean-certify 2>&1 | FileCheck %s --check-prefix=NO-PROJECT +# RUN: not %cpp-verify --obligation-in=%t/a.cpv --lean-fallback=%t/f 2>&1 | FileCheck %s --check-prefix=NO-FALLBACK +# RUN: not %cpp-verify --obligation-in=%t/a.cpv --lean-project=%t/x --lean-out=%t/x.lean 2>&1 | FileCheck %s --check-prefix=BOTH +# RUN: not %cpp-verify --obligation-in=%t/a.cpv --backend=z3 --lean-project=%t/x 2>&1 | FileCheck %s --check-prefix=Z3 + +# SOURCE: Exported: decreases: tri (cppverify_auto proved 1 of 1 goals) +# SOURCE-NEXT: Exported: lean obligation: tri_nonneg (cppverify_auto proved 1 of 2 goals) +# SOURCE: Exported: decreases: down (cppverify_auto proved 1 of 1 goals) +# SOURCE-NEXT: Exported: lean obligation: down_zero (cppverify_auto proved 2 of 2 goals) +# SOURCE-NEXT: Exported: lean obligation: inc (cppverify_auto proved 3 of 3 goals) + +# REPLAY: Exported: lean obligation: tri.decreases (cppverify_auto proved 1 of 1 goals) [backend=lean] [semantic-hash=sha256:{{[0-9a-f]+}}] +# REPLAY-NEXT: Exported: lean obligation: tri_nonneg (cppverify_auto proved 1 of 2 goals) [backend=lean] +# REPLAY-NEXT: Exported: lean obligation: down.decreases (cppverify_auto proved 1 of 1 goals) [backend=lean] +# REPLAY-NEXT: Exported: lean obligation: down_zero (cppverify_auto proved 2 of 2 goals) [backend=lean] +# REPLAY-NEXT: Exported: lean obligation: inc (cppverify_auto proved 3 of 3 goals) [backend=lean] + +# The archive keeps tri's measure, and, for down's, the spec it applies. +# SPECS: {{^}}def cppSpec_fn_5f5a3374726969 (n : Int) : Int :={{$}} +# SPECS: {{^}}termination_by ((n) + 1).toNat{{$}} +# SPECS: {{^}}def cppSpec_fn_5f5a3473697a6569 (n : Int) : Int :={{$}} + +# READABLE: (h_pre_1 : (cppBvSlt x_0 (BitVec.ofInt 32 (100)))) → + +# CERTIFY: Proved obligations: tri.decreases (dependencies not checked in replay) [backend=lean] +# CERTIFY-NEXT: Proved obligations: tri_nonneg (dependencies not checked in replay) [backend=lean] +# CERTIFY-NEXT: Proved obligations: down.decreases (dependencies not checked in replay) [backend=lean] +# CERTIFY-NEXT: Proved obligations: down_zero (dependencies not checked in replay) [backend=lean] +# CERTIFY-NEXT: Proved obligations: inc (dependencies not checked in replay) [backend=lean] + +# JSON: {"backend":"lean","function":"tri.decreases","lean_automatic":1,{{.*}}"status":"exported"} + +# SPECS-V2: {{^}}opaque cppSpec_fn_5f5a3374726969 : Int -> Int{{$}} +# READABLE-V2-NOT: h_pre + +# BOUNDED-EXPORT: Exported: lean obligation: sum_small [backend=lean, bound=2] +# BOUNDED-EXPORT-NEXT: Exported: lean obligation: count_up [backend=lean, bound=3] + +# BOUND: /- function: sum_small -/ +# BOUND: /- bound: 2 loop iterations, by unrolling: these goals speak only of the +# BOUND: kind: unwinding +# BOUND: /- function: count_up -/ +# BOUND: /- bound: 3 loop iterations, by unrolling: these goals speak only of the + +# BOUNDED: Proved obligations: sum_small (dependencies not checked in replay) [backend=lean, bound=2] +# BOUNDED-NEXT: lean_replay_loops.cpp:19:3: BoundedSafe: count_up (every goal is certified but the unwinding: no execution within 3 loop iterations fails (the proof of fn_5f5a38636f756e745f757069::unwinding@19:3: {{.*}}) [backend=lean, bound=3] [reason=bmc.incomplete-bound] + +# STALE: warning: the Lean proof CppVerify/Proofs/cppverify_tri_nonneg_42a030/cppverify_tri_nonneg_42a030_postcondition_053b1980.lean is kept in Stale/Proofs/cppverify_tri_nonneg_42a030/cppverify_tri_nonneg_42a030_postcondition_053b1980.lean: its function is gone, and no goal has its statement +# STALE-NEXT: Exported: lean obligation: sum_small (cppverify_auto proved 7 of 7 goals) [backend=lean, bound=2] + +# BACK: {"message":"the Lean proof of fn_5f5a31307472695f6e6f6e6e656769::postcondition@{{[0-9]+}}:{{[0-9]+}} came back from Stale/Proofs/cppverify_tri_nonneg_42a030/cppverify_tri_nonneg_42a030_postcondition_053b1980.lean to CppVerify/Proofs/cppverify_tri_nonneg_42a030/cppverify_tri_nonneg_42a030_postcondition_053b1980.lean, the file of the goal with its statement","schema":"cppverify.diagnostic/1","severity":"warning","status":"warning"} +# BACK-NEXT: {"backend":"lean","function":"tri.decreases",{{.*}}"status":"exported"} + +# NO-PROJECT: error: --lean-certify, --lean-prune-stale, and --no-lean-auto require --lean-project +# NO-FALLBACK: error: --lean-fallback applies to source verification; archive replay writes a Lean project with --lean-project +# BOTH: error: --lean-project cannot be combined with --lean-out +# Z3: error: --lean-project requires --backend=lean 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{{$}} diff --git a/clang/test/Verify/suite/obligation_archive.test b/clang/test/Verify/suite/obligation_archive.test index 9939b4d523..61e78e97d0 100644 --- a/clang/test/Verify/suite/obligation_archive.test +++ b/clang/test/Verify/suite/obligation_archive.test @@ -15,12 +15,18 @@ # RUN: %python %S/Inputs/mutate_obligation_archive.py truncated %t.one %t.truncated # RUN: not %cpp-verify --obligation-in=%t.truncated 2>&1 | FileCheck %s --check-prefix=TRUNCATED # RUN: cp %t.one %t.version -# RUN: printf '\003\000\000\000' | dd of=%t.version bs=1 seek=8 conv=notrunc 2>/dev/null +# RUN: printf '\004\000\000\000' | dd of=%t.version bs=1 seek=8 conv=notrunc 2>/dev/null # RUN: not %cpp-verify --obligation-in=%t.version 2>&1 | FileCheck %s --check-prefix=VERSION # RUN: %python %S/Inputs/mutate_obligation_archive.py schema-v1 %t.one %t.schema-v1 # RUN: not %cpp-verify --obligation-in=%t.schema-v1 2>&1 | FileCheck %s --check-prefix=SCHEMA-V1 # RUN: %python %S/Inputs/mutate_obligation_archive.py schema-v1-kinds %t.one %t.schema-v1-kinds # RUN: %cpp-verify --obligation-in=%t.schema-v1-kinds --backend=z3 | FileCheck %s --check-prefix=SCHEMA-V1-KINDS +# RUN: %python %S/Inputs/mutate_obligation_archive.py schema-v2 %t.one %t.schema-v2 +# RUN: %cpp-verify --obligation-in=%t.schema-v2 --backend=z3 | FileCheck %s --check-prefix=SCHEMA-V2 +# A measure is read like a definition, over the function's parameters. +# RUN: %cpp-verify --lower-only --obligation-out=%t.measures %S/Inputs/lean_replay.cpp -- +# RUN: %python %S/Inputs/mutate_obligation_archive.py measure-free-variable %t.measures %t.measure-variable +# RUN: not %cpp-verify --obligation-in=%t.measure-variable 2>&1 | FileCheck %s --check-prefix=MEASURE # RUN: %python %S/Inputs/mutate_obligation_archive.py invalid-kind %t.one %t.invalid-kind # RUN: not %cpp-verify --obligation-in=%t.invalid-kind 2>&1 | FileCheck %s --check-prefix=KIND # RUN: %python %S/Inputs/mutate_obligation_archive.py feature-mismatch %t.one %t.features @@ -93,7 +99,7 @@ # REPLAY: Proved obligations: canonical_obligations (dependencies not checked in replay) [backend=z3] [semantic-hash=sha256:{{[0-9a-f]+}}] # LOWER: vc canonical_obligations -# LOWER: schema cppverify.obligation/2 +# LOWER: schema cppverify.obligation/3 # LOWER: (let # LOWER: Lowered: canonical_obligations [backend=z3] [semantic-hash=sha256:{{[0-9a-f]+}}] # LEAN: Exported: lean obligation: canonical_obligations [backend=lean] @@ -104,6 +110,8 @@ # VERSION: error: invalid obligation archive: unsupported obligation archive version # SCHEMA-V1: error: invalid obligation archive: invalid obligation kind in obligation archive # SCHEMA-V1-KINDS: Proved obligations: canonical_obligations (dependencies not checked in replay) [backend=z3] +# SCHEMA-V2: Proved obligations: canonical_obligations (dependencies not checked in replay) [backend=z3] +# MEASURE: error: invalid obligation archive: logical function definition has a free variable: z # KIND: error: invalid obligation archive: invalid expression kind in obligation archive # FEATURES: error: invalid obligation archive: obligation archive feature declaration does not match contents # DUPLICATE-ID: error: invalid obligation archive: obligation module has an empty or duplicate obligation identity diff --git a/clang/test/Verify/suite/obligation_ir.cpp b/clang/test/Verify/suite/obligation_ir.cpp index 1545435386..f8f2fddeab 100644 --- a/clang/test/Verify/suite/obligation_ir.cpp +++ b/clang/test/Verify/suite/obligation_ir.cpp @@ -26,7 +26,7 @@ int canonical_obligations(int x) } // OBLIGATION-LABEL: vc canonical_obligations -// OBLIGATION-NEXT: schema cppverify.obligation/2 +// OBLIGATION-NEXT: schema cppverify.obligation/3 // OBLIGATION-NEXT: simplification nodes {{[1-9][0-9]*}} -> {{[1-9][0-9]*}}, rewrites {{[1-9][0-9]*}}, functions-removed 0 // OBLIGATION-NEXT: semantic-hash sha256:f6d09cd4e2ac5c541fa8e0e443f4c2981e5763ce9b4d94d69f9856eaa1e95f2e // OBLIGATION-NEXT: identity [[IDENTITY:fn_[0-9a-f]+]] 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 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 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 *& diff --git a/clang/tools/cpp-verify/Main.cpp b/clang/tools/cpp-verify/Main.cpp index 7c27e2f10d..4b99460ea2 100644 --- a/clang/tools/cpp-verify/Main.cpp +++ b/clang/tools/cpp-verify/Main.cpp @@ -325,6 +325,20 @@ lowerForBackend(const verify::ObligationModule &Module, return verify::lowerObligationModule(Module, Z3Out, Execution); } +// The options of Lean output and Lean projects, which source verification +// and archive replay share. +static void setLeanOptions(verify::VerifyOptions &VOpts) { + VOpts.LeanOutPath = LeanOut.getValue(); + VOpts.LeanProjectPath = LeanProject.getValue(); + VOpts.LeanFallbackProjectPath = LeanFallback.getValue(); + VOpts.LeanScope = LeanFallbackScope.getValue(); + VOpts.LeanCertify = LeanCertify.getValue(); + VOpts.LeanPruneStale = LeanPruneStale.getValue(); + VOpts.LeanAuto = !NoLeanAuto.getValue(); + VOpts.LeanAutoTimeoutMs = LeanAutoTimeout.getValue(); + VOpts.LeanJobs = Jobs.getNumOccurrences() ? Jobs.getValue() : 0; +} + class VerifyConsumer : public ASTConsumer { public: void HandleTranslationUnit(ASTContext &Ctx) override { @@ -346,15 +360,7 @@ class VerifyConsumer : public ASTConsumer { VOpts.Backend = verify::BackendKind::Race; else VOpts.Backend = verify::BackendKind::Z3; - VOpts.LeanOutPath = LeanOut.getValue(); - VOpts.LeanProjectPath = LeanProject.getValue(); - VOpts.LeanFallbackProjectPath = LeanFallback.getValue(); - VOpts.LeanScope = LeanFallbackScope.getValue(); - VOpts.LeanCertify = LeanCertify.getValue(); - VOpts.LeanPruneStale = LeanPruneStale.getValue(); - VOpts.LeanAuto = !NoLeanAuto.getValue(); - VOpts.LeanAutoTimeoutMs = LeanAutoTimeout.getValue(); - VOpts.LeanJobs = Jobs.getNumOccurrences() ? Jobs.getValue() : 0; + setLeanOptions(VOpts); VOpts.BMCUnroll = BMCUnroll.getValue(); VOpts.SolverTimeoutMs = SolverTimeout.getValue(); VOpts.CollectionTimeoutMs = collectionTimeoutMs(); @@ -465,7 +471,8 @@ replaySourceJSON(const verify::ObligationSource &Source) { static void printReplayJSON(const verify::ObligationModule &Module, const verify::VerifyResult &Result, - llvm::StringRef SemanticHash) { + llvm::StringRef SemanticHash, + unsigned LeanAutomatic) { llvm::json::Object Record; Record["schema"] = "cppverify.diagnostic/1"; Record["status"] = replayStatusCode(Result.Status); @@ -486,6 +493,8 @@ static void printReplayJSON(const verify::ObligationModule &Module, Record["reason"] = verify::verifyReasonCode(Result.Reason); if (Result.Bound) Record["bound"] = static_cast(*Result.Bound); + if (Result.Status == verify::VerifyStatus::Exported && LeanAutomatic) + Record["lean_automatic"] = static_cast(LeanAutomatic); if (!Result.ExploredBounds.empty()) { llvm::json::Array Bounds; for (unsigned Bound : Result.ExploredBounds) @@ -632,16 +641,31 @@ static int replayObligationArchive() { "exclusive\n"; return 1; } - if (!LeanProject.empty() || !LeanFallback.empty() || LeanCertify || - LeanPruneStale || NoLeanAuto || LeanAutoTimeout.getNumOccurrences()) { - llvm::errs() << "error: archive replay supports Lean scratch-pad export " - "with --lean-out, not Lean project generation or " - "certification\n"; + if (!LeanFallback.empty()) { + llvm::errs() << "error: --lean-fallback applies to source verification; " + "archive replay writes a Lean project with " + "--lean-project\n"; return 1; } - if (BackendOpt == "lean" && (jobs() != 1 || !ProofCache.empty())) { - llvm::errs() - << "error: --jobs and --proof-cache are not supported by Lean replay\n"; + if (LeanProject.empty() && (LeanCertify || LeanPruneStale || NoLeanAuto)) { + llvm::errs() << "error: --lean-certify, --lean-prune-stale, and " + "--no-lean-auto require --lean-project\n"; + return 1; + } + if (!LeanProject.empty() && BackendOpt != "lean") { + llvm::errs() << "error: --lean-project requires --backend=lean\n"; + return 1; + } + if (!LeanProject.empty() && (!LeanOut.empty() || LowerOnly)) { + llvm::errs() << "error: --lean-project cannot be combined with " + << (LowerOnly ? "--lower-only" : "--lean-out") << "\n"; + return 1; + } + // A project's Lean processes run at once; the scratch-pad is one file. + if (BackendOpt == "lean" && + ((LeanProject.empty() && jobs() != 1) || !ProofCache.empty())) { + llvm::errs() << "error: --proof-cache is not supported by Lean replay, " + "nor --jobs by its scratch-pad\n"; return 1; } if (BackendOpt == "cvc5" && !ProofCache.empty()) { @@ -691,11 +715,6 @@ static int replayObligationArchive() { "before obligation lowering\n"; return 1; } - if (BackendOpt == "lean" && Module.BMCTransform) { - llvm::errs() << "error: Lean scratch export cannot replay a " - "BMC-transformed obligation archive\n"; - return 1; - } if ((BackendOpt == "cvc5" || BackendOpt == "portfolio" || BackendOpt == "race") && Module.BMCTransform) { @@ -718,10 +737,10 @@ static int replayObligationArchive() { std::unique_ptr LeanFile; llvm::raw_ostream *LeanStream = nullptr; - if (BackendOpt == "lean") { + if (BackendOpt == "lean" && LeanProject.empty()) { if (LeanOut.empty()) { - llvm::errs() - << "error: --backend=lean archive replay requires --lean-out\n"; + llvm::errs() << "error: --backend=lean archive replay requires " + "--lean-out or --lean-project\n"; return 1; } std::error_code EC; @@ -750,17 +769,47 @@ static int replayObligationArchive() { const unsigned DumpLayers = DumpIR.getNumOccurrences() > 0 ? verify::parseDumpIRLayers(DumpIR.getValue()) : 0; + // A Lean project takes every module before any is certified. + std::optional Project; + if (!LeanProject.empty() && !verify::interruptRequested()) { + verify::VerifyOptions VOpts; + VOpts.Backend = verify::BackendKind::Lean; + setLeanOptions(VOpts); + Project = verify::replayLeanProject(Modules, VOpts); + for (const std::string &Warning : Project->Warnings) { + if (DiagnosticsFormat != verify::DiagnosticFormat::Json) { + llvm::outs() << "warning: " << Warning << "\n"; + continue; + } + llvm::json::Object Record; + Record["schema"] = "cppverify.diagnostic/1"; + Record["status"] = "warning"; + Record["severity"] = "warning"; + Record["message"] = jsonText(Warning); + llvm::outs() << llvm::formatv("{0}\n", + llvm::json::Value(std::move(Record))); + } + if (!Project->Error.empty()) { + llvm::errs() << "error: " << Project->Error << "\n"; + return 1; + } + } bool AllOk = true; - for (const verify::ObligationModule &Module : Modules) { + for (size_t Index = 0; Index != Modules.size(); ++Index) { + const verify::ObligationModule &Module = Modules[Index]; if (DumpLayers & verify::LayerVC) verify::dumpVC(Module, llvm::outs()); verify::VerifyResult Result; - if (LowerOnly) { + const unsigned LeanAutomatic = Project ? Project->Automatic[Index] : 0; + if (Project) { + Result = Project->Results[Index]; + } else if (LowerOnly) { Result = lowerForBackend( Module, Kind, DumpLayers & verify::LayerZ3 ? &llvm::outs() : nullptr); } else if (!verify::interruptRequested()) { - if (Module.BMCTransform) { + // Lean exports a bounded module, its bound stated with its goals. + if (Module.BMCTransform && Kind != verify::BackendKind::Lean) { std::unique_ptr BMCBackend = verify::createVerifyBackend(verify::BackendKind::BMC, nullptr, Module.BMCTransform->UnrollBound, @@ -768,6 +817,8 @@ static int replayObligationArchive() { Result = BMCBackend->verify(Module); } else { Result = Backend->verify(Module); + if (Module.BMCTransform) + Result.Bound = Module.BMCTransform->UnrollBound; } } // After Ctrl-C no result is final, whatever the queries returned. @@ -779,7 +830,7 @@ static int replayObligationArchive() { const std::string Hash = verify::obligationSemanticHash(Module); if (DiagnosticsFormat == verify::DiagnosticFormat::Json) { - printReplayJSON(Module, Result, Hash); + printReplayJSON(Module, Result, Hash, LeanAutomatic); if (Result.Status != verify::VerifyStatus::Lowered && Result.Status != verify::VerifyStatus::Verified && Result.Status != verify::VerifyStatus::Exported) @@ -833,8 +884,14 @@ static int replayObligationArchive() { << ReplayProofNote << ")" << Suffix << "\n"; break; case verify::VerifyStatus::Exported: - llvm::outs() << "Exported: lean obligation: " << Module.FunctionName - << Suffix << "\n"; + llvm::outs() << "Exported: lean obligation: " << Module.FunctionName; + if (LeanAutomatic) + llvm::outs() << " (cppverify_auto proved " << LeanAutomatic << " of " + << std::set(Result.LeanGoals.begin(), + Result.LeanGoals.end()) + .size() + << " goals)"; + llvm::outs() << Suffix << "\n"; break; case verify::VerifyStatus::Failed: AllOk = false; diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index e2603cfe67..73a24a0946 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. @@ -609,7 +636,8 @@ canonicalization step before hashing or backend dispatch. The pass folds only sort-preserving Boolean constants, double negation, constant conditionals, and reflexive equality/inequality. It simplifies owned finite-fuel definitions and removes logical declarations unreachable transitively from every ordered -obligation. It then rebuilds each exact counterexample negation, the complete +obligation, a declaration reaching what its definition and its termination +measures apply. It then rebuilds each exact counterexample negation, the complete ordered goal/query, and required feature set before revalidation. Arithmetic, quantifiers, pointer/heap terms, and assumptions are not rewritten. Layer 3 reports before/after node counts, rewrite count, and removed declarations for @@ -678,7 +706,7 @@ and obligation kinds. ### Canonical archives and semantic identity `--obligation-out=FILE` writes one or more deterministic -`cppverify.obligation/2` records after source attribution. The binary format has +`cppverify.obligation/3` records after source attribution. The binary format has the `CPVOBL\r\n` magic, an explicit schema version, little-endian fixed-width integers, length-delimited strings/collections, and stable hand-assigned wire tags rather than C++ enum ordinals. The reader bounds strings, collections, @@ -691,10 +719,20 @@ which tag 6, the former sequence update, is reserved); the collection sorts `seq`, `set`, `multiset`, and `map` have sort tags 6 to 9. Trigger patterns and the `Choice` marker of a logical function are not archived, so a replayed module instantiates quantifiers by the solver's own patterns and -treats a choice as an ordinary uninterpreted function. - -Schema v2 adds the precise obligation kinds and still reads schema v1, whose -records name only assertions, postconditions, and unwinding checks. Records +treats a choice as an ordinary uninterpreted function. A logical function's +`Decreases` follow its definition levels, and with source metadata the +`Premise` of each `Or` follows its source point; neither is hashed. A +measure is validated like a definition (an integer over the parameters, +every call resolved): it changes no meaning, since Lean proves a +definition's termination itself and an induction descends by a +well-founded relation whatever the measure, and canonicalization keeps the +functions a measure applies, so a module never names one it does not +declare. Before, a spec only a measure applied was removed, and the +measure could not be printed. + +Schema v2 adds the precise obligation kinds, and schema v3 the measures and +premises; readers still read schema v2 and schema v1, whose records name +only assertions, postconditions, and unwinding checks. Records limit strings to 64 MiB, collections and expression nodes/edges to 100,000 per record, expression nesting to 4096, canonical integer numerals to 4096 decimal characters, and integer sorts to 4096 bits. @@ -706,8 +744,9 @@ that are not the conjunction of their ordered obligations. Every module and individual obligation has a SHA-256 semantic hash. Semantic hashes omit source paths, display-only function names, internal positional -or public source-anchored obligation IDs, and every obligation kind except -`unwinding` (the only kind that changes result semantics), so moving identical +or public source-anchored obligation IDs, measures, premises, and every +obligation kind except `unwinding` (the only kind that changes result +semantics), so moving identical C++ source or inserting an unrelated earlier obligation does not invalidate an individual goal's proof identity. Per-obligation hashes include only the transitive @@ -728,6 +767,7 @@ cpp-verify --obligation-in=goals.cpv --backend=z3 cpp-verify --obligation-in=goals.cpv --backend=portfolio cpp-verify --obligation-in=goals.cpv --lower-only --dump-ir=3,4 cpp-verify --obligation-in=goals.cpv --backend=lean --lean-out=goals.lean +cpp-verify --obligation-in=goals.cpv --lean-project=proof --lean-certify ``` Replay treats decoded records as untrusted input: validation happens before @@ -743,13 +783,33 @@ f (dependencies not checked in replay)` (JSON status `proved-obligations`), never `Verified`. A counterexample is still a failure: postconditions are not archived either, so replay certifies it by the definitions alone. +With `--lean-project`, `replayLeanProject` (`Verifier.h`) exports every +module through the project adapter and drives the same `LeanProject` a +source run does: the modules and the spec trial, regeneration with moves +and quarantine, automation, and with `--lean-certify` certification. The +goals have the names, files, and proofs the same obligations have from +source (both name a goal by its statement), and `Specs.lean` the same +definitions, since the measures are archived; a readable goal names the +same hypotheses, since the premises are. A module whose goals all certify +is `Verified` there, printed `Proved obligations ... [backend=lean]`, never +`Certified`, which claims the dependency fixpoint. + BMC-produced modules retain the unroll bound as semantic transform provenance. Replay aggregates those modules with BMC unwinding semantics even when Z3 is the selected solver, so an exhausted frontier remains `BoundedSafe(N)` rather than becoming an ordinary program failure or an unbounded proof. Applying BMC to an untransformed archive is rejected because loop unrolling must precede -obligation construction. Lean scratch export of a bounded archive is also -rejected until bounded theorem provenance is represented in generated Lean. +obligation construction. Lean exports a bounded module, to the scratch-pad +or a project, with its bound stated over its goals (`/- bound: N loop +iterations, by unrolling: ... -/`), and `LeanProjectGoal::Unwinding` marks +its unwinding goals: every goal certified is `Verified` (`Proved +obligations`, `bound=N`), every goal but some unwinding goal certified is +`BoundedSafe` (`bmc.incomplete-bound`), else `Unresolved`. Lean proves and +never refutes, so its `BoundedSafe` says that the unwinding goals are not +certified, where BMC's says that they fail; both claim what the safety +goals state, no failure in an execution within the bound, and reporting +the unproved unwinding unresolved would leave Lean no bounded verdict for +a module whose unwinding fails, the case BMC is for. Failure-triggered `cppverify::recommends` diagnostics are excluded from archives, keeping archive contents independent of solver outcomes. @@ -1640,7 +1700,10 @@ SMT-LIB, and Lean's own operators differ. ### Project goals and their proofs A project names nothing by position, so that a proof keeps every name it -uses when the source around it changes. +uses when the source around it changes. `LeanProject` (`Verifier.cpp`) owns +a project: its modules, its proof files, automation, and certification, +reporting what it warns of to its caller; a source run and an archive's +replay both drive it. - **Names.** A module's goals form a group, `cppverify__
` (`leanProjectGroup`), `h6` from the MD5 of the function identity, which @@ -1736,11 +1799,57 @@ uses when the source around it changes. 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 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 + 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`, - like `Patterns` outside the term's meaning, its hash, and archives, and - kept by the clones and the in-place simplifier). The passivizer records + like `Patterns` outside the term's meaning and its hash, kept by the + clones, the in-place simplifier, and archives of schema 3, so a replayed + goal names the same hypotheses). The passivizer records the origin of every assumption it emits (`PassiveStmt::Origin`, from a current origin each statement kind sets and its parts refine: `def`, `call:f`, `inv`, `cond`, `exit`, `keep`, `exact`, `check`, @@ -1941,7 +2050,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). @@ -2054,8 +2178,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 @@ -2291,9 +2416,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. @@ -2482,7 +2609,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 diff --git a/docs/DESIGN.md b/docs/DESIGN.md index 3f51623778..17b800de43 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. @@ -1497,7 +1554,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). @@ -1775,15 +1841,18 @@ Before publication or dispatch, a shared fail-closed canonicalizer applies a deliberately narrow set of semantics-preserving rewrites: Boolean constants, double negation, constant conditionals, and reflexive equality/inequality. It simplifies logical definitions, removes declarations unreachable transitively -from the ordered goals, rebuilds exact per-obligation and complete +from the ordered goals (through definitions and termination measures, since +a declaration depends on what both apply), rebuilds exact per-obligation and complete goal/counterexample pairs, recomputes features, and revalidates. The same step runs after archive decoding, so adapters never depend on producer-specific dead declarations or trivial Boolean structure. It does not rewrite arithmetic, quantifiers, pointer/heap expressions, or assumptions. `--obligation-out=FILE` publishes deterministic, concatenable -`cppverify.obligation/2` binary records with stable wire tags and portable -source attribution; schema v1 records remain readable. Publication includes an +`cppverify.obligation/3` binary records with stable wire tags and portable +source attribution; schema v3 adds each logical function's termination +measures and, with source attribution, where each assumption of a goal comes +from, neither hashed, and records of schemas v1 and v2 remain readable. Publication includes an exact serialize/deserialize/validate/reserialize check. SHA-256 module and per-obligation semantic hashes exclude source paths, display-only names, both positional and source-anchored obligation IDs, and every obligation kind except @@ -1793,14 +1862,21 @@ wire version. Canonicalization introduced semantic-hash format v2, excluding diagnostic identities advanced it to v3, and excluding diagnostic kinds advances it to v4. `--obligation-in=FILE` validates and replays the records through Z3, cvc5, -strict Z3+cvc5 portfolio, lower-only/Layer 3-4 dumps, or Lean scratch export -without reparsing C++. Each module is replayed alone, without the contracts, +strict Z3+cvc5 portfolio, lower-only/Layer 3-4 dumps, Lean scratch export, or +a Lean project (`--lean-project`, with certification) without reparsing C++. +A project gets the goals, specs, and proof files a source run gives the same +obligations, which are named by their statements, so a proof certifies from +either. Each module is replayed alone, without the contracts, spec facts, partiality, and vacuity checks its source verdict rests on, so a module whose obligations hold reports `Proved obligations` (JSON `proved-obligations`), never `Verified`. BMC-produced records carry their unroll bound in semantics and replay through the BMC result aggregator; untransformed records cannot acquire BMC semantics -after this boundary. Lean scratch replay of bounded records is rejected. +after this boundary. In Lean the goals of a bounded module state its bound, +and its result aggregates the same way: every goal certified proves its +obligations, and every goal but some unwinding goal certified is +`BoundedSafe`, which in Lean says that the unwinding is not certified (Lean +never refutes a goal). Failure-only `cppverify::recommends` diagnostics do not alter archive contents. Imported records are untrusted input: bounded parsing precedes structural, scope, sort, signature, feature, canonical-payload, exact-negation, and @@ -2018,6 +2094,19 @@ 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 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 +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 @@ -2056,5 +2145,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. 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, 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 -------------------------- 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`). 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 7ed662d840..04fb031093 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,69 @@ 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 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 +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 ~~~~~~~~~~~~~~~~~~~ @@ -956,8 +1020,9 @@ The canonical backend boundary can be persisted and replayed: cpp-verify --obligation-in=goals.cpv --backend=portfolio cpp-verify --obligation-in=goals.cpv --lower-only --dump-ir=3,4 cpp-verify --obligation-in=goals.cpv --backend=lean --lean-out=goals.lean + cpp-verify --obligation-in=goals.cpv --lean-project=proof --lean-certify -Each ``cppverify.obligation/2`` record uses stable wire tags, defensive bounds, +Each ``cppverify.obligation/3`` record uses stable wire tags, defensive bounds, portable source points, and path-independent SHA-256 semantic hashes. Replay revalidates every sort, expression, logical declaration, call signature, feature declaration, and identity before backend dispatch. Multiple records may @@ -979,27 +1044,119 @@ and its replay side by side. Source-built and replayed records pass through the same conservative canonicalizer before hashing and dispatch. It folds only trivial Boolean structure and reflexive equality/inequality, removes transitively unreachable -logical declarations, rebuilds exact ordered and complete queries plus feature +logical declarations (a declaration reaches what its definition and its +termination measures apply), rebuilds exact ordered and complete queries plus feature metadata, and revalidates. It does not rewrite arithmetic, quantifiers, pointers, heaps, or assumptions. Canonicalization introduced semantic-hash format v2; format v3 removed diagnostic obligation identities from the preimage, and format v4 removes every obligation kind except ``unwinding``. -Schema v2 adds precise obligation kinds; schema v1 records remain readable. +Schema v2 adds precise obligation kinds, and schema v3 each spec function's +termination measures and where each assumption of a goal comes from (what a +Lean project needs to define a spec and to name a goal's hypotheses); none +of these is hashed, and records of schemas v1 and v2 remain readable. BMC source verification archives only the terminal module for each function. Those records retain their exact explored unroll bound. Replay is fixed-bound and uses BMC unwinding aggregation, so an incomplete frontier remains ``BoundedSafe(N)`` rather than rerunning the incremental source strategy. BMC cannot be applied to an untransformed record because loop unrolling is a VCR -transformation that occurs before canonical obligation construction. Lean -scratch replay of bounded records is rejected until the generated theorem -format carries the same transform provenance. +transformation that occurs before canonical obligation construction. Failure-only ``cppverify::recommends`` checks are not archived, so bytes do not depend on whether a prior solver run succeeded or failed. The dependency-scoped proof cache is shared by direct verification and replay, so identical canonical goals reuse proofs without trusting source paths or diagnostic identities. +Archives in a Lean project +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +``--lean-project`` with ``--obligation-in`` writes the archive's modules to a +Lean project as a source run writes its functions: each goal has the name, +module, and proof file the same obligation has from source, since both name +it by its statement, and the specs are the same Lean definitions. A proof +written for the source certifies the archive's goal. For the specs of +`Spec functions in Lean`_, + +.. code-block:: bash + + cpp-verify --lower-only --obligation-out=goals.cpv file.cpp + cpp-verify --obligation-in=goals.cpv --lean-project=replay + +prints + +.. code-block:: text + + Exported: lean obligation: tri.decreases (cppverify_auto proved 1 of 1 goals) [backend=lean] [semantic-hash=sha256:...] + Exported: lean obligation: tri_nonneg (cppverify_auto proved 1 of 2 goals) [backend=lean] [semantic-hash=sha256:...] + +and ``replay`` has the goals, ``Specs.lean``, and proof files of +``cpp-verify --backend=lean --lean-project=proof file.cpp``. With the proof of +``tri_nonneg`` by induction in its file, ``--lean-certify`` prints + +.. code-block:: text + + Proved obligations: tri.decreases (dependencies not checked in replay) [backend=lean] [semantic-hash=sha256:...] + Proved obligations: tri_nonneg (dependencies not checked in replay) [backend=lean] [semantic-hash=sha256:...] + +As with a solver, replay checks each module alone, so a module whose goals +all certify has its obligations proved, never ``Certified``, which would +also say that what the verdict rests on is established. Automation, moving +and keeping proofs in ``Stale/``, ``--lean-prune-stale``, and ``--jobs`` work +as for a source project; ``--lean-fallback`` is for source verification +only. + +A bounded record of BMC exports too, to a project or to the scratch-pad. +The goals of each bounded module say its bound: + +.. code-block:: lean4 + + /- function: count_up -/ + /- required logic: mathematical-integers, bit-vectors, pointers, heap-arrays -/ + /- bound: 3 loop iterations, by unrolling: these goals speak only of the + executions within them, and an unwinding goal says that every loop + ends within them -/ + +Its result is read as BMC reads one: every goal certified, its unwinding +goals included, proves the obligations, and every goal but some unwinding +goal certified is ``BoundedSafe``: no execution within the bound fails. Lean +proves goals and never refutes one, so a Lean ``BoundedSafe`` says that the +unwinding goals are not certified, not that they fail. For two loops +archived by ``cpp-verify --backend=bmc --unroll=3``, + +.. cppverify-example: flags --backend=bmc --unroll=3 + +.. code-block:: cpp + + int sum_small(int n) + cppverify::pre(0 <= n && n <= 2) + cppverify::post(cppverify::result >= 0) + { + int s = 0; + for (int i = 0; i < n; i = i + 1) + s = s + i; + return s; + } + + int count_up(int n) + cppverify::pre(0 <= n && n <= 1000) + cppverify::post(cppverify::result == n) + { + int c = 0; + while (c < n) + c = c + 1; + return c; + } + +``--lean-certify`` prints + +.. code-block:: text + + Proved obligations: sum_small (dependencies not checked in replay) [backend=lean, bound=2] [semantic-hash=sha256:...] + loops.cpp:16:3: BoundedSafe: count_up (every goal is certified but the unwinding: no execution within 3 loop iterations fails (the proof of fn_5f5a38636f756e745f757069::unwinding@16:3: ...)) [backend=lean, bound=3] [reason=bmc.incomplete-bound] [semantic-hash=sha256:...] + +``count_up`` loops up to 1000 times, so its unwinding goal at the bound 3 is +false, as BMC finds (``BoundedSafe: count_up [backend=bmc, bound=3]``). + Modular function calls ---------------------- 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 diff --git a/website/source/language/limitations.rst b/website/source/language/limitations.rst index 383e32a315..70d3943bfa 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 ------------------- @@ -120,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) @@ -283,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 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. diff --git a/website/source/language/tooling.rst b/website/source/language/tooling.rst index 9b46373167..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 ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -347,6 +383,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 @@ -467,11 +509,13 @@ Backends concatenated in one archive. * - ``--obligation-in=FILE`` - Validate and replay an archive without reparsing C++. Supports Z3, cvc5, - strict portfolio, ``--lower-only``/Layer 3-4 dumps, and Lean scratch - export. Archives + strict portfolio, ``--lower-only``/Layer 3-4 dumps, Lean scratch + export, and Lean projects (``--lean-project``, with certification). + Archives produced after BMC unrolling retain their bound and replay with BMC - unwinding semantics; applying BMC to an untransformed archive is - rejected because unrolling must run before obligation lowering. + unwinding semantics, in Lean too; applying BMC to an untransformed + archive is rejected because unrolling must run before obligation + lowering. Each module is replayed on its own, without the callee and trusted contracts, spec facts, partiality, and vacuity its source verdict rests on: a module whose obligations all hold reports ``Proved @@ -783,13 +827,26 @@ against the definitions the archive carries. Before 0.2, replay printed run did not verify the function, for example when a callee's verification failed. -``--obligation-out`` writes ``cppverify.obligation/2`` records only after exact +An archive replays into a Lean project with ``--lean-project``, optionally +with ``--lean-certify``, ``--lean-prune-stale``, ``--no-lean-auto``, +``--lean-auto-timeout``, and ``--jobs``: the project gets the goals, specs, +and proof files a source run of the same program gives, and a module whose +goals all certify is ``Proved obligations`` ``[backend=lean]``. A bounded +record of BMC goes to Lean too, its bound stated with its goals; its +module is ``BoundedSafe`` when every goal but some unwinding goal +certifies (:doc:`../book/part-ii/ch17-backends-modular-calls`). +``--lean-fallback`` applies to source verification only. + +``--obligation-out`` writes ``cppverify.obligation/3`` records only after exact serialize/deserialize/validate/reserialize checks. Stable wire tags make the format independent of C++ enum ordinals. The reader rejects malformed magic, unsupported versions, truncation, invalid tags, inconsistent feature declarations, duplicate identities, and oversized/deep expressions. -Schema v2 adds the precise obligation kinds; schema v1 records, which name -only assertions, postconditions, and unwinding checks, are still read. +Schema v2 adds the precise obligation kinds; schema v3 each spec function's +termination measures, read like its definition, and, with source metadata, +where each assumption of a goal comes from, which names a hypothesis of a +readable Lean goal. Records of schema v2, and of schema v1, which name only +assertions, postconditions, and unwinding checks, are still read. Records cap integer widths at 4096 bits, expression depth at 4096, and collections plus expression nodes/edges at 100,000 per record. It also rejects embedded NULs, non-canonical numerals, inactive payload fields, ill-scoped @@ -799,7 +856,8 @@ backend dispatch. Module and per-obligation SHA-256 hashes omit source paths and display-only names, source ranges, internal positional and public source-anchored IDs, -obligation kinds other than ``unwinding``, and traces, so moving unchanged +obligation kinds other than ``unwinding``, traces, measures, and where +assumptions come from, so moving unchanged source, inserting an unrelated earlier obligation, or changing display metadata preserves an individual goal's semantic identity. Archives still diff --git a/website/source/release-notes.rst b/website/source/release-notes.rst index 7f0115d48a..b731d2b6f0 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 ~~~~~~~~~~~~~~~~~~ @@ -308,6 +327,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`). @@ -429,6 +458,34 @@ proves goals such as ``a / 2 >= 2`` for ``a >= 4``. Lean's verdict on each spec is kept in the project, so a later export tries nothing (:doc:`book/part-ii/ch17-backends-modular-calls`). +**Lean projects from archives.** An obligation archive could reach Lean only +as the unchecked scratch-pad, and a bounded archive of BMC not at all. +``--obligation-in`` with ``--lean-project`` now writes a Lean project as a +source run of the same program does, with the same goals, specs, and proof +files, so a proof written for the source certifies the archive's goal; +``--lean-certify`` reports each module whose goals all certify as ``Proved +obligations`` ``[backend=lean]``, since replay checks a module alone. A +bounded module states its bound with its goals, in a project and in the +scratch-pad, and its result is read as BMC reads one: it is ``BoundedSafe`` +when every goal but some unwinding goal certifies. Archives record each spec +function's termination measures and the source of each assumption of a goal, +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 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`). + **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 @@ -443,8 +500,11 @@ refuses a ``lake`` outside elan that reports another Lean Data formats ~~~~~~~~~~~~ -Archives stay ``cppverify.obligation/2`` and JSON diagnostics -``cppverify.diagnostic/1``. JSON records may carry the status +Archives are ``cppverify.obligation/3``, which adds measures and the +sources of assumptions and reads ``/2`` and ``/1``; JSON diagnostics stay +``cppverify.diagnostic/1``. A module whose specs' measures apply other specs +keeps them, so its module hash changes; per-obligation hashes, and the proof +cache keyed by them, do not. JSON records may carry the status ``proved-obligations`` (archive replay) and the reason ``interrupted`` (Ctrl-C). Lean projects pin ``leanprover/lean4:v4.35.0``, and each proof file records the hash of its goal's statement (``cppverify-obligation-statement``