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 98eda10f5b..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" @@ -25,6 +26,10 @@ static thread_local std::map LeanTemporaryNames; static thread_local const LogicExpr *LeanTemporaryRoot = nullptr; static thread_local const LogicFunctionDecl *LeanActiveDefinition = nullptr; static thread_local unsigned LeanActiveDefinitionDepth = 0; +// Printing a spec's own definition for Lean to accept by well-founded +// recursion: every condition that reaches an application is a hypothesis +// there (`if _h : c`), so that the decrease can be proved from it. +static thread_local bool LeanDefinitionMode = false; static bool needsLeanNameEncoding(llvm::StringRef Name) { static const std::set Keywords = { @@ -108,6 +113,8 @@ static void printLeanCommentText(llvm::StringRef Text, llvm::raw_ostream &OS) { } } +// A sequence is a list, a set its membership test, a multiset its counts, +// and a map the value at each key it holds (CppVerify/Prelude.lean). static void printLeanSort(const LogicSort &Sort, llvm::raw_ostream &OS) { switch (Sort.Kind) { case LogicSortKind::Bool: @@ -123,17 +130,83 @@ static void printLeanSort(const LogicSort &Sort, llvm::raw_ostream &OS) { case LogicSortKind::Heap: OS << "CppHeap"; return; - case LogicSortKind::Invalid: case LogicSortKind::Seq: + OS << "List Int"; + return; case LogicSortKind::Set: + OS << "(Int → Bool)"; + return; case LogicSortKind::Multiset: + OS << "(Int → Nat)"; + return; case LogicSortKind::Map: + OS << "(Int → Option Int)"; + return; + case LogicSortKind::Invalid: LeanEmissionFailed = true; OS << "False"; return; } } +// The prelude's function for each collection operation. +static const char *leanCollectionName(LogicCollectionOp Operation) { + using Op = LogicCollectionOp; + switch (Operation) { + case Op::SeqEmpty: + return "cppSeqEmpty"; + case Op::SeqUnit: + return "cppSeqUnit"; + case Op::SeqLength: + return "cppSeqLength"; + case Op::SeqIndex: + return "cppSeqAt"; + case Op::SeqPush: + return "cppSeqPush"; + case Op::SeqSubrange: + return "cppSeqSubrange"; + case Op::SeqConcat: + return "cppSeqConcat"; + case Op::SeqContains: + return "cppSeqContains"; + case Op::SetEmpty: + return "cppSetEmpty"; + case Op::SetInsert: + return "cppSetInsert"; + case Op::SetRemove: + return "cppSetRemove"; + case Op::SetContains: + return "cppSetContains"; + case Op::SetUnion: + return "cppSetUnion"; + case Op::SetIntersect: + return "cppSetIntersect"; + case Op::SetDifference: + return "cppSetDifference"; + case Op::SetSubset: + return "cppSetSubset"; + case Op::MultisetEmpty: + return "cppMultisetEmpty"; + case Op::MultisetInsert: + return "cppMultisetInsert"; + case Op::MultisetRemove: + return "cppMultisetRemove"; + case Op::MultisetCount: + return "cppMultisetCount"; + case Op::MapEmpty: + return "cppMapEmpty"; + case Op::MapInsert: + return "cppMapInsert"; + case Op::MapRemove: + return "cppMapRemove"; + case Op::MapContains: + return "cppMapContains"; + case Op::MapGet: + return "cppMapGet"; + } + return nullptr; +} + static void collectLeanVariables(const LogicExpr *E, std::set Bound, std::map &Variables) { @@ -237,6 +310,16 @@ static const LogicFunctionDecl *findLeanFunction(llvm::StringRef Identity) { return It == LeanLogicFunctions->end() ? nullptr : &It->second; } +static bool leanAppliesSpec(const LogicExpr *E) { + if (!E) + return false; + if (E->K == VCExpr::SpecCall) + return true; + return llvm::any_of(E->Children, [](const auto &Child) { + return leanAppliesSpec(Child.get()); + }); +} + static void printLeanNativeSpecCall(const LogicExpr *Call, const LogicFunctionDecl &Function, llvm::raw_ostream &OS) { @@ -309,8 +392,33 @@ static void printVCExprLean(const VCExpr *E, llvm::raw_ostream &OS, printVCExprLean(E->Children[0].get(), OS, LeanArgument); }); break; - // Right-associative: only the last operand may be of the same level. + // Right-associative: only the last operand may be of the same level. In a + // definition, the operands before an application are its condition: + // `a ∧ b` is `if _h : a then b else False`. case VCExpr::And: + if (LeanDefinitionMode) + for (unsigned I = 1; I < E->Children.size(); ++I) + if (leanAppliesSpec(E->Children[I].get())) { + paren(LeanTop, [&] { + OS << "if _h : "; + for (unsigned J = 0; J < I; ++J) { + if (J) + OS << " ∧ "; + printVCExprLean(E->Children[J].get(), OS, + J + 1 == I ? LeanAnd : LeanAnd + 1); + } + OS << " then "; + for (unsigned J = I; J < E->Children.size(); ++J) { + if (J != I) + OS << " ∧ "; + printVCExprLean(E->Children[J].get(), OS, + J + 1 == E->Children.size() ? LeanAnd + : LeanAnd + 1); + } + OS << " else False"; + }); + return; + } paren(LeanAnd, [&] { for (unsigned I = 0; I < E->Children.size(); ++I) { if (I) @@ -320,7 +428,31 @@ static void printVCExprLean(const VCExpr *E, llvm::raw_ostream &OS, } }); break; + // `a ∨ b` is `if _h : a then True else b`, and `¬a ∨ b` is `if _h : a then b + // else True`. case VCExpr::Or: + if (LeanDefinitionMode && E->Children.size() > 1 && + llvm::any_of(llvm::drop_begin(E->Children), [](const auto &Child) { + return leanAppliesSpec(Child.get()); + })) { + paren(LeanTop, [&] { + const LogicExpr *First = E->Children[0].get(); + const bool Negated = First->K == VCExpr::Not; + OS << "if _h : "; + printVCExprLean(Negated ? First->Children[0].get() : First, OS, + LeanTop); + OS << (Negated ? " then " : " then True else "); + for (unsigned J = 1; J < E->Children.size(); ++J) { + if (J != 1) + OS << " ∨ "; + printVCExprLean(E->Children[J].get(), OS, + J + 1 == E->Children.size() ? LeanOr : LeanOr + 1); + } + if (Negated) + OS << " else True"; + }); + break; + } paren(LeanOr, [&] { for (unsigned I = 0; I < E->Children.size(); ++I) { if (I) @@ -332,7 +464,7 @@ static void printVCExprLean(const VCExpr *E, llvm::raw_ostream &OS, break; case VCExpr::Ite: paren(LeanTop, [&] { - OS << "if "; + OS << (LeanDefinitionMode ? "if _h : " : "if "); printVCExprLean(E->Children[0].get(), OS, LeanTop); OS << " then "; printVCExprLean(E->Children[1].get(), OS, LeanTop); @@ -535,10 +667,25 @@ static void printVCExprLean(const VCExpr *E, llvm::raw_ostream &OS, printVCExprLean(E->Children[3].get(), OS, LeanArgument); OS << ")"; break; - case VCExpr::Collection: - LeanEmissionFailed = true; - OS << "False"; + case VCExpr::Collection: { + const char *Name = leanCollectionName(E->CollectionOp); + if (!Name) { + LeanEmissionFailed = true; + OS << "False"; + break; + } + if (E->Children.empty()) { + OS << Name; + break; + } + OS << "(" << Name; + for (const auto &Child : E->Children) { + OS << " "; + printVCExprLean(Child.get(), OS, LeanArgument); + } + OS << ")"; break; + } case VCExpr::HeapFrame: OS << "(∀ ("; printLeanName("__frame_address", OS); @@ -575,6 +722,12 @@ static void printVCExprLean(const VCExpr *E, llvm::raw_ostream &OS, printVCExprLean(E->Children[0].get(), OS, LeanTop); return; } + // In a definition, the range of an existential that applies a spec + // is its condition, as a universal's is its antecedent. + const bool Guarded = E->K == VCExpr::Exists && LeanDefinitionMode && + leanAppliesSpec(E->Children[2].get()); + if (Guarded) + OS << "if _h : "; printVCExprLean(E->Children[0].get(), OS, LeanCompare + 1); OS << " ≤ "; printLeanName(E->Binder, OS); @@ -582,6 +735,12 @@ static void printVCExprLean(const VCExpr *E, llvm::raw_ostream &OS, printLeanName(E->Binder, OS); OS << " < "; printVCExprLean(E->Children[1].get(), OS, LeanCompare + 1); + if (Guarded) { + OS << " then "; + printVCExprLean(E->Children[2].get(), OS, LeanTop); + OS << " else False"; + return; + } OS << (E->K == VCExpr::Forall ? " → " : " ∧ "); printVCExprLean(E->Children[2].get(), OS, E->K == VCExpr::Forall ? LeanArrow : LeanAnd); @@ -1033,25 +1192,165 @@ static void emitLeanGoalDefinition(llvm::StringRef Name, const LogicExpr *Goal, emitLeanReadableGoal(Name, Goal, Variables, HasSpecAxioms, *Intros, OS); } -static void -emitLeanFunctionDeclarations(const ObligationModule &Module, - llvm::raw_ostream &OS, - std::set &EmittedFunctions) { - for (const auto &[Identity, Function] : Module.LogicFunctions) { - if (!EmittedFunctions.insert(Identity).second) +static void collectLeanApplied(const LogicExpr *E, + std::set &Applied) { + if (!E) + return; + if (E->K == VCExpr::SpecCall) + Applied.insert(E->SpecCallee); + for (const auto &Child : E->Children) + collectLeanApplied(Child.get(), Applied); +} + +static std::string leanOpaqueSpec(const LogicFunctionDecl &Function) { + std::string Text; + llvm::raw_string_ostream OS(Text); + OS << "/- spec function: "; + printLeanCommentText(Function.DisplayName, OS); + OS << " -/\n"; + OS << "opaque "; + printLeanSpecName(Function.Identity, OS); + OS << " : "; + for (const LogicFunctionParameter &Parameter : Function.Parameters) { + printLeanSort(Parameter.Sort, OS); + OS << " -> "; + } + printLeanSort(Function.ResultSort, OS); + OS << "\n\n"; + return Text; +} + +// A spec's own definition, for Lean to accept by well-founded recursion: its +// step definition, applying its recursion group by name, every condition +// that reaches an application a hypothesis there, and its termination +// measures, each m as `(m + 1).toNat`: for a caller's m at least 0 and a +// call's below it (it may be -1), the call's is below the caller's, the +// relation the termination check proves, lexicographic over a tuple. None +// for a choice, a function without a definition, or a recursive one without +// measures (an archive's). +static std::string leanSpecDefinition(const ObligationModule &Module, + const LogicFunctionDecl &Function) { + if (Function.Choice || !Function.StepDefinition) + return ""; + std::set Reached, Pending; + collectLeanApplied(Function.StepDefinition.get(), Pending); + while (!Pending.empty()) { + std::string Next = *Pending.begin(); + Pending.erase(Pending.begin()); + if (!Reached.insert(Next).second) continue; - OS << "/- spec function: "; - printLeanCommentText(Function.DisplayName, OS); - OS << " -/\n"; - OS << "opaque "; - printLeanSpecName(Identity, OS); + auto It = Module.LogicFunctions.find(Next); + if (It != Module.LogicFunctions.end() && It->second.StepDefinition) + collectLeanApplied(It->second.StepDefinition.get(), Pending); + } + const bool Recursive = Reached.count(Function.Identity); + if (Recursive && Function.Decreases.empty()) + return ""; + + const bool FailedBefore = LeanEmissionFailed; + LeanEmissionFailed = false; + auto Temporaries = std::move(LeanTemporaryNames); + LeanTemporaryNames.clear(); + LeanDefinitionMode = true; + LeanEmitBudget = 1000000; + std::string Text; + llvm::raw_string_ostream OS(Text); + OS << "/- spec function: "; + printLeanCommentText(Function.DisplayName, OS); + OS << " -/\n"; + OS << "def "; + printLeanSpecName(Function.Identity, OS); + for (const LogicFunctionParameter &Parameter : Function.Parameters) { + OS << " ("; + printLeanName(Parameter.Name, OS); OS << " : "; - for (const LogicFunctionParameter &Parameter : Function.Parameters) { - printLeanSort(Parameter.Sort, OS); - OS << " -> "; + printLeanSort(Parameter.Sort, OS); + OS << ")"; + } + OS << " : "; + printLeanSort(Function.ResultSort, OS); + OS << " :=\n "; + printVCExprLean(Function.StepDefinition.get(), OS, LeanTop); + if (Recursive) { + OS << "\ntermination_by "; + if (Function.Decreases.size() > 1) + OS << "("; + for (unsigned I = 0; I < Function.Decreases.size(); ++I) { + if (I) + OS << ", "; + OS << "(("; + printVCExprLean(Function.Decreases[I].get(), OS, LeanTop); + OS << ") + 1).toNat"; } - printLeanSort(Function.ResultSort, OS); - OS << "\n\n"; + if (Function.Decreases.size() > 1) + OS << ")"; + OS << "\ndecreasing_by all_goals cppverify_decreasing"; + } + OS << "\n\n"; + LeanDefinitionMode = false; + LeanTemporaryNames = std::move(Temporaries); + const bool Failed = LeanEmissionFailed; + LeanEmissionFailed = FailedBefore; + 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, + std::map *Specs) { + for (const auto &[Identity, Function] : Module.LogicFunctions) { + if (Specs) { + auto [It, Inserted] = Specs->try_emplace(Identity); + LeanSpecDeclaration &Declaration = It->second; + if (Inserted) { + llvm::raw_string_ostream Name(Declaration.Name); + printLeanSpecName(Identity, Name); + Declaration.Opaque = leanOpaqueSpec(Function); + } + if (Declaration.Definition.empty()) { + Declaration.Definition = leanSpecDefinition(Module, Function); + Declaration.Applies.clear(); + collectLeanApplied(Function.StepDefinition.get(), Declaration.Applies); + } + continue; + } + if (EmittedFunctions.insert(Identity).second) + OS << leanOpaqueSpec(Function); } } @@ -1087,12 +1386,439 @@ static void emitLeanFunctionBodies(const ObligationModule &Module, } } +// Collections of mathematical integers, with the total meaning +// gives each operation, and lemmas that state it for simp, grind, and proofs +// by hand. Checking a goal never needs them: they are theorems of the +// definitions. +static constexpr llvm::StringLiteral LeanCollectionPrelude = + R"lean(/- Collections of mathematical integers, total as defines + them: a sequence is a list, a set its membership test, a multiset its + counts, and a map the value at each key it holds. -/ + +def cppSeqEmpty : List Int := [] +def cppSeqUnit (x : Int) : List Int := [x] +def cppSeqLength (s : List Int) : Int := s.length +def cppSeqAt (s : List Int) (i : Int) : Int := + if i < 0 then 0 else s[i.toNat]?.getD 0 +def cppSeqPush (s : List Int) (x : Int) : List Int := s ++ [x] +def cppSeqConcat (s t : List Int) : List Int := s ++ t +def cppSeqSubrange (s : List Int) (lo hi : Int) : List Int := + (s.drop (max 0 (min lo s.length)).toNat).take + (max (max 0 (min lo s.length)) (min hi s.length) - + max 0 (min lo s.length)).toNat +def cppSeqContains (s : List Int) (x : Int) : Prop := x ∈ s +instance (s : List Int) (x : Int) : Decidable (cppSeqContains s x) := + inferInstanceAs (Decidable (x ∈ s)) + +def cppSetEmpty : Int → Bool := fun _ => false +def cppSetInsert (s : Int → Bool) (x : Int) : Int → Bool := + fun y => y == x || s y +def cppSetRemove (s : Int → Bool) (x : Int) : Int → Bool := + fun y => y != x && s y +def cppSetContains (s : Int → Bool) (x : Int) : Prop := s x = true +instance (s : Int → Bool) (x : Int) : Decidable (cppSetContains s x) := + inferInstanceAs (Decidable (s x = true)) +def cppSetUnion (s t : Int → Bool) : Int → Bool := fun y => s y || t y +def cppSetIntersect (s t : Int → Bool) : Int → Bool := fun y => s y && t y +def cppSetDifference (s t : Int → Bool) : Int → Bool := + fun y => s y && !t y +def cppSetSubset (s t : Int → Bool) : Prop := ∀ y, s y = true → t y = true + +def cppMultisetEmpty : Int → Nat := fun _ => 0 +def cppMultisetInsert (m : Int → Nat) (x : Int) : Int → Nat := + fun y => if y = x then m y + 1 else m y +def cppMultisetRemove (m : Int → Nat) (x : Int) : Int → Nat := + fun y => if y = x then m y - 1 else m y +def cppMultisetCount (m : Int → Nat) (x : Int) : Int := m x + +def cppMapEmpty : Int → Option Int := fun _ => none +def cppMapInsert (m : Int → Option Int) (k v : Int) : Int → Option Int := + fun y => if y = k then some v else m y +def cppMapRemove (m : Int → Option Int) (k : Int) : Int → Option Int := + fun y => if y = k then none else m y +def cppMapContains (m : Int → Option Int) (k : Int) : Prop := + (m k).isSome = true +instance (m : Int → Option Int) (k : Int) : Decidable (cppMapContains m k) := + inferInstanceAs (Decidable ((m k).isSome = true)) +def cppMapGet (m : Int → Option Int) (k : Int) : Int := (m k).getD 0 + +/- What each operation means, for simp, grind, and proofs by hand. -/ + +private theorem cppverify_ite_pos {c : Prop} [Decidable c] {α : Sort _} + {a b : α} (h : c) : (if c then a else b) = a := by simp [h] +private theorem cppverify_ite_neg {c : Prop} [Decidable c] {α : Sort _} + {a b : α} (h : ¬c) : (if c then a else b) = b := by simp [h] + +@[simp, grind =] theorem cppSeqLength_empty : cppSeqLength cppSeqEmpty = 0 := rfl +@[simp, grind =] theorem cppSeqLength_unit (x : Int) : + cppSeqLength (cppSeqUnit x) = 1 := rfl +@[simp, grind =] theorem cppSeqLength_push (s : List Int) (x : Int) : + cppSeqLength (cppSeqPush s x) = cppSeqLength s + 1 := by + simp [cppSeqLength, cppSeqPush] +@[simp, grind =] theorem cppSeqLength_concat (s t : List Int) : + cppSeqLength (cppSeqConcat s t) = cppSeqLength s + cppSeqLength t := by + simp [cppSeqLength, cppSeqConcat] +theorem cppSeqLength_nonneg (s : List Int) : 0 ≤ cppSeqLength s := by + simp [cppSeqLength] +grind_pattern cppSeqLength_nonneg => cppSeqLength s +@[simp, grind =] theorem cppSeqLength_subrange (s : List Int) (lo hi : Int) : + cppSeqLength (cppSeqSubrange s lo hi) = + max (max 0 (min lo (cppSeqLength s))) (min hi (cppSeqLength s)) - + max 0 (min lo (cppSeqLength s)) := by + simp only [cppSeqLength, cppSeqSubrange, List.length_take, List.length_drop] + omega + +theorem cppSeqAt_out (s : List Int) (i : Int) + (h : i < 0 ∨ cppSeqLength s ≤ i) : cppSeqAt s i = 0 := by + unfold cppSeqAt cppSeqLength at * + split + · rfl + · rw [List.getElem?_eq_none (by omega)]; rfl +@[simp, grind =] theorem cppSeqAt_empty (i : Int) : cppSeqAt cppSeqEmpty i = 0 := + cppSeqAt_out [] i (by simp [cppSeqLength]; omega) +@[simp, grind =] theorem cppSeqAt_push (s : List Int) (x i : Int) : + cppSeqAt (cppSeqPush s x) i = + if i = cppSeqLength s then x else cppSeqAt s i := by + unfold cppSeqAt cppSeqPush cppSeqLength + by_cases h0 : i < 0 + · simp only [h0, ↓reduceIte, show ¬ i = (s.length : Int) by omega] + · by_cases he : i = s.length + · subst he; simp only [h0, ↓reduceIte]; simp + · simp only [h0, he, ↓reduceIte] + by_cases hl : i.toNat < s.length + · rw [List.getElem?_append_left hl] + · rw [List.getElem?_append_right (by omega), + List.getElem?_eq_none (show s.length ≤ i.toNat by omega), + List.getElem?_eq_none (by simp; omega)] +@[simp, grind =] theorem cppSeqAt_concat (s t : List Int) (i : Int) : + cppSeqAt (cppSeqConcat s t) i = + if i < cppSeqLength s then cppSeqAt s i + else cppSeqAt t (i - cppSeqLength s) := by + unfold cppSeqAt cppSeqLength cppSeqConcat + by_cases h0 : i < 0 + · simp only [h0, ↓reduceIte, show i < (s.length : Int) by omega] + · by_cases hl : i < s.length + · simp only [h0, hl, ↓reduceIte] + rw [List.getElem?_append_left (by omega)] + · simp only [h0, hl, ↓reduceIte, show ¬ (i - s.length < 0) by omega] + rw [List.getElem?_append_right (by omega)] + congr 3; omega +@[simp, grind =] theorem cppSeqAt_unit (x i : Int) : + cppSeqAt (cppSeqUnit x) i = if i = 0 then x else 0 := by + unfold cppSeqAt cppSeqUnit + by_cases h0 : i < 0 + · simp only [h0, ↓reduceIte, show ¬ i = 0 by omega] + · by_cases h : i = 0 + · subst h; simp + · simp only [h0, h, ↓reduceIte] + rw [List.getElem?_eq_none (by simp; omega)]; rfl +@[simp, grind =] theorem cppSeqAt_subrange (s : List Int) (lo hi i : Int) : + cppSeqAt (cppSeqSubrange s lo hi) i = + if 0 ≤ i ∧ i < cppSeqLength (cppSeqSubrange s lo hi) + then cppSeqAt s (max 0 (min lo (cppSeqLength s)) + i) else 0 := by + rw [cppSeqLength_subrange] + unfold cppSeqAt cppSeqSubrange cppSeqLength + by_cases h0 : i < 0 + · simp only [h0, ↓reduceIte, show ¬ (0 ≤ i) by omega, false_and] + · simp only [h0, ↓reduceIte] + split + · rw [List.getElem?_take, cppverify_ite_pos (by omega), List.getElem?_drop, + cppverify_ite_neg (show ¬ (max 0 (min lo (s.length : Int)) + i < 0) by omega)] + congr 3; omega + · rw [List.getElem?_take, cppverify_ite_neg (by omega)]; rfl +@[simp, grind =] theorem cppSeqContains_empty (x : Int) : + cppSeqContains cppSeqEmpty x ↔ False := by + simp [cppSeqContains, cppSeqEmpty] +@[simp, grind =] theorem cppSeqContains_unit (y x : Int) : + cppSeqContains (cppSeqUnit y) x ↔ x = y := by + simp [cppSeqContains, cppSeqUnit] +@[simp, grind =] theorem cppSeqContains_push (s : List Int) (y x : Int) : + cppSeqContains (cppSeqPush s y) x ↔ cppSeqContains s x ∨ x = y := by + simp [cppSeqContains, cppSeqPush] +@[simp, grind =] theorem cppSeqContains_concat (s t : List Int) (x : Int) : + cppSeqContains (cppSeqConcat s t) x ↔ + cppSeqContains s x ∨ cppSeqContains t x := by + simp [cppSeqContains, cppSeqConcat] +@[simp, grind =] theorem cppSeqSubrange_all (s : List Int) : + cppSeqSubrange s 0 (cppSeqLength s) = s := by + unfold cppSeqSubrange cppSeqLength + rw [show (max 0 (min (0 : Int) (s.length : Int))).toNat = 0 by omega, + show (max (max 0 (min (0 : Int) (s.length : Int))) + (min (s.length : Int) (s.length : Int)) - + max 0 (min (0 : Int) (s.length : Int))).toNat = s.length by omega] + simp +@[simp, grind =] theorem cppSeqSubrange_concat_left (s t : List Int) : + cppSeqSubrange (cppSeqConcat s t) 0 (cppSeqLength s) = s := by + unfold cppSeqSubrange cppSeqConcat cppSeqLength + have hl : (s ++ t).length = s.length + t.length := List.length_append + rw [show (max 0 (min (0 : Int) ((s ++ t).length : Int))).toNat = 0 by omega, + show (max (max 0 (min (0 : Int) ((s ++ t).length : Int))) + (min (s.length : Int) ((s ++ t).length : Int)) - + max 0 (min (0 : Int) ((s ++ t).length : Int))).toNat = s.length by + omega] + simp +@[simp, grind =] theorem cppSeqSubrange_concat_right (s t : List Int) : + cppSeqSubrange (cppSeqConcat s t) (cppSeqLength s) + (cppSeqLength s + cppSeqLength t) = t := by + unfold cppSeqSubrange cppSeqConcat cppSeqLength + have hl : (s ++ t).length = s.length + t.length := List.length_append + rw [show (max 0 (min (s.length : Int) ((s ++ t).length : Int))).toNat = + s.length by omega, + show (max (max 0 (min (s.length : Int) ((s ++ t).length : Int))) + (min ((s.length : Int) + (t.length : Int)) ((s ++ t).length : Int)) - + max 0 (min (s.length : Int) ((s ++ t).length : Int))).toNat = + t.length by omega] + simp +@[simp, grind =] theorem cppSeqSubrange_push (s : List Int) (x : Int) : + cppSeqSubrange (cppSeqPush s x) 0 (cppSeqLength s) = s := + cppSeqSubrange_concat_left s [x] +theorem cppSeqContains_iff (s : List Int) (x : Int) : + cppSeqContains s x ↔ + ∃ i, 0 ≤ i ∧ i < cppSeqLength s ∧ cppSeqAt s i = x := by + unfold cppSeqContains cppSeqLength cppSeqAt + rw [List.mem_iff_getElem] + constructor + · rintro ⟨i, hi, he⟩ + refine ⟨i, by omega, by omega, ?_⟩ + rw [cppverify_ite_neg (by omega), Int.toNat_natCast, List.getElem?_eq_getElem hi] + simpa using he + · rintro ⟨i, h0, hl, he⟩ + refine ⟨i.toNat, by omega, ?_⟩ + rw [cppverify_ite_neg (by omega), List.getElem?_eq_getElem (by omega)] at he + simpa using he +theorem cppSeq_ext (s t : List Int) (hl : cppSeqLength s = cppSeqLength t) + (h : ∀ i, 0 ≤ i → i < cppSeqLength s → cppSeqAt s i = cppSeqAt t i) : + s = t := by + unfold cppSeqLength at hl + apply List.ext_getElem (by omega) + intro i h1 h2 + have := h i (by omega) (by unfold cppSeqLength; omega) + unfold cppSeqAt at this + simp only [show ¬ ((i : Int) < 0) by omega, ↓reduceIte, Int.toNat_natCast, + List.getElem?_eq_getElem h1, List.getElem?_eq_getElem h2, + Option.getD_some] at this + exact this + +@[simp, grind =] theorem cppSetContains_empty (x : Int) : + cppSetContains cppSetEmpty x ↔ False := by simp [cppSetContains, cppSetEmpty] +@[simp, grind =] theorem cppSetContains_insert (s : Int → Bool) (x y : Int) : + cppSetContains (cppSetInsert s x) y ↔ y = x ∨ cppSetContains s y := by + simp [cppSetContains, cppSetInsert] +@[simp, grind =] theorem cppSetContains_remove (s : Int → Bool) (x y : Int) : + cppSetContains (cppSetRemove s x) y ↔ y ≠ x ∧ cppSetContains s y := by + simp [cppSetContains, cppSetRemove] +@[simp, grind =] theorem cppSetContains_union (s t : Int → Bool) (y : Int) : + cppSetContains (cppSetUnion s t) y ↔ + cppSetContains s y ∨ cppSetContains t y := by + simp [cppSetContains, cppSetUnion] +@[simp, grind =] theorem cppSetContains_intersect (s t : Int → Bool) (y : Int) : + cppSetContains (cppSetIntersect s t) y ↔ + cppSetContains s y ∧ cppSetContains t y := by + simp [cppSetContains, cppSetIntersect] +@[simp, grind =] theorem cppSetContains_difference (s t : Int → Bool) (y : Int) : + cppSetContains (cppSetDifference s t) y ↔ + cppSetContains s y ∧ ¬ cppSetContains t y := by + simp [cppSetContains, cppSetDifference] +@[simp, grind =] theorem cppSetSubset_iff (s t : Int → Bool) : + cppSetSubset s t ↔ ∀ y, cppSetContains s y → cppSetContains t y := Iff.rfl +theorem cppSet_ext (s t : Int → Bool) + (h : ∀ y, cppSetContains s y ↔ cppSetContains t y) : s = t := by + funext y + have := h y + unfold cppSetContains at this + cases hs : s y <;> cases ht : t y <;> simp_all + +@[simp, grind =] theorem cppMultisetCount_empty (x : Int) : + cppMultisetCount cppMultisetEmpty x = 0 := rfl +@[simp, grind =] theorem cppMultisetCount_insert (m : Int → Nat) (x y : Int) : + cppMultisetCount (cppMultisetInsert m x) y = + if y = x then cppMultisetCount m y + 1 else cppMultisetCount m y := by + unfold cppMultisetCount cppMultisetInsert; split <;> simp +@[simp, grind =] theorem cppMultisetCount_remove (m : Int → Nat) (x y : Int) : + cppMultisetCount (cppMultisetRemove m x) y = + if y = x then max 0 (cppMultisetCount m y - 1) + else cppMultisetCount m y := by + unfold cppMultisetCount cppMultisetRemove; split <;> omega +theorem cppMultisetCount_nonneg (m : Int → Nat) (x : Int) : + 0 ≤ cppMultisetCount m x := by simp [cppMultisetCount] +grind_pattern cppMultisetCount_nonneg => cppMultisetCount m x +theorem cppMultiset_ext (m n : Int → Nat) + (h : ∀ y, cppMultisetCount m y = cppMultisetCount n y) : m = n := by + funext y; have := h y; unfold cppMultisetCount at this; omega + +@[simp, grind =] theorem cppMapContains_empty (k : Int) : + cppMapContains cppMapEmpty k ↔ False := by simp [cppMapContains, cppMapEmpty] +@[simp, grind =] theorem cppMapContains_insert (m : Int → Option Int) (k v y : Int) : + cppMapContains (cppMapInsert m k v) y ↔ y = k ∨ cppMapContains m y := by + unfold cppMapContains cppMapInsert; by_cases h : y = k <;> simp [h] +@[simp, grind =] theorem cppMapContains_remove (m : Int → Option Int) (k y : Int) : + cppMapContains (cppMapRemove m k) y ↔ y ≠ k ∧ cppMapContains m y := by + unfold cppMapContains cppMapRemove; by_cases h : y = k <;> simp [h] +@[simp, grind =] theorem cppMapGet_empty (k : Int) : cppMapGet cppMapEmpty k = 0 := rfl +@[simp, grind =] theorem cppMapGet_insert (m : Int → Option Int) (k v y : Int) : + cppMapGet (cppMapInsert m k v) y = if y = k then v else cppMapGet m y := by + unfold cppMapGet cppMapInsert; split <;> simp +@[simp, grind =] theorem cppMapGet_remove (m : Int → Option Int) (k y : Int) : + cppMapGet (cppMapRemove m k) y = if y = k then 0 else cppMapGet m y := by + unfold cppMapGet cppMapRemove; split <;> simp +theorem cppMapGet_out (m : Int → Option Int) (k : Int) + (h : ¬ cppMapContains m k) : cppMapGet m k = 0 := by + unfold cppMapGet; unfold cppMapContains at h; cases hm : m k <;> simp_all +theorem cppMap_ext (m n : Int → Option Int) + (hc : ∀ y, cppMapContains m y ↔ cppMapContains n y) + (hg : ∀ y, cppMapGet m y = cppMapGet n y) : m = n := by + funext y + have c := hc y; have g := hg y + unfold cppMapGet at g + unfold cppMapContains at c + cases hm : m y <;> cases hn : n y <;> simp_all + +)lean"; + +// The definitions every exported goal is stated with: the heap model, the +// machine comparisons, C++ division, and the collections; a project's goals +// also have the lemmas their readable forms' bridges use. +void verify::emitLeanPrelude(llvm::raw_ostream &OS, bool Project) { + OS << "noncomputable section\n\n"; + OS << "set_option maxRecDepth 100000\n"; + OS << "set_option maxHeartbeats 0\n\n"; + OS << "local instance cppVerifyPropDecidable (p : Prop) : Decidable p :=\n"; + OS << " Classical.propDecidable p\n\n"; + OS << "abbrev CppHeap := Int -> Int\n\n"; + OS << "def heapSelectInt (h : CppHeap) (p : Int) : Int := h p\n"; + OS << "abbrev heapSelectBool (h : CppHeap) (p : Int) : Prop := h p ≠ 0\n"; + OS << "def heapSelectBv (w : Nat) (h : CppHeap) (p : Int) : BitVec w :=\n"; + OS << " BitVec.ofInt w (h p)\n\n"; + OS << "def heapStoreInt (h : CppHeap) (p v : Int) (h' : CppHeap) : " + "Prop :=\n"; + OS << " h' = fun q => if q = p then v else h q\n"; + OS << "def heapStoreBool (h : CppHeap) (p : Int) (v : Prop)\n"; + OS << " (h' : CppHeap) : Prop :=\n"; + OS << " h' = fun q => if q = p then\n"; + OS << " @ite Int v (Classical.propDecidable v) 1 0 else h q\n"; + OS << "def heapStoreBv {w : Nat} (h : CppHeap) (p : Int) (v : BitVec w)\n"; + OS << " (h' : CppHeap) : Prop :=\n"; + OS << " h' = fun q => if q = p then Int.ofNat v.toNat else h q\n\n"; + OS << "opaque validPtr : Int -> Prop\n\n"; + // Reducible, so instance search sees the Bool comparison and decides it. + OS << "abbrev cppBvUlt {w : Nat} (x y : BitVec w) : Prop := x.ult y = " + "true\n"; + OS << "abbrev cppBvUle {w : Nat} (x y : BitVec w) : Prop := x.ule y = " + "true\n"; + OS << "abbrev cppBvSlt {w : Nat} (x y : BitVec w) : Prop := x.slt y = " + "true\n"; + OS << "abbrev cppBvSle {w : Nat} (x y : BitVec w) : Prop := x.sle y = " + "true\n\n"; + OS << "def cppIntDiv (x y : Int) : Int :=\n"; + OS << " if y = 0 then 0 else\n"; + OS << " let q := (if x < 0 then -x else x) / " + "(if y < 0 then -y else y)\n"; + 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"; + OS << "macro \"cppverify_decreasing\" : tactic => `(tactic| first\n"; + OS << " | (simp_wf; omega)\n"; + OS << " | (simp_wf; simp only [cppSeqLength, cppMultisetCount, cppBvSlt, " + "cppBvSle,\n"; + OS << " cppBvUlt, cppBvUle] at *; omega)\n"; + // C++ division and remainder by a constant, which omega reads once the + // signs are split. + OS << " | (simp_wf; simp only [cppIntDiv, cppIntRem] at *;\n"; + OS << " (repeat' split) <;> simp_all <;> omega)\n"; + OS << " | (simp_wf; simp_all; omega)\n"; + OS << " | decreasing_tactic)\n\n"; + if (Project) { + // What the bridges from readable goals use. + OS << "theorem cppverify_imp_or {a b : Prop} (h : a → b) : ¬a ∨ b :=\n"; + OS << " (Classical.em a).elim (fun ha => Or.inr (h ha)) Or.inl\n"; + OS << "theorem cppverify_not_imp_or {a b : Prop} (h : ¬a → b) : a ∨ b " + ":=\n"; + OS << " (Classical.em a).elim Or.inl (fun ha => Or.inr (h ha))\n\n"; + } +} + +// 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, std::set &EmittedTheorems, unsigned ModuleIndex, std::vector *ProjectGoals, - const std::set *Selection) { + const std::set *Selection, + std::map *Specs) { VerifyResult Result; if (!Module.CorrectnessGoal || !Module.CounterexampleQuery) { Result.Status = VerifyStatus::Unresolved; @@ -1130,60 +1856,22 @@ VerifyResult verify::exportLeanScratchPad( OS << " This file exports canonical obligations but does not certify " "them. -/\n\n"; } - OS << "noncomputable section\n\n"; - OS << "set_option maxRecDepth 100000\n"; - OS << "set_option maxHeartbeats 0\n\n"; - OS << "local instance cppVerifyPropDecidable (p : Prop) : Decidable p :=\n"; - OS << " Classical.propDecidable p\n\n"; - OS << "abbrev CppHeap := Int -> Int\n\n"; - OS << "def heapSelectInt (h : CppHeap) (p : Int) : Int := h p\n"; - OS << "abbrev heapSelectBool (h : CppHeap) (p : Int) : Prop := h p ≠ 0\n"; - OS << "def heapSelectBv (w : Nat) (h : CppHeap) (p : Int) : BitVec w :=\n"; - OS << " BitVec.ofInt w (h p)\n\n"; - OS << "def heapStoreInt (h : CppHeap) (p v : Int) (h' : CppHeap) : " - "Prop :=\n"; - OS << " h' = fun q => if q = p then v else h q\n"; - OS << "def heapStoreBool (h : CppHeap) (p : Int) (v : Prop)\n"; - OS << " (h' : CppHeap) : Prop :=\n"; - OS << " h' = fun q => if q = p then\n"; - OS << " @ite Int v (Classical.propDecidable v) 1 0 else h q\n"; - OS << "def heapStoreBv {w : Nat} (h : CppHeap) (p : Int) (v : BitVec w)\n"; - OS << " (h' : CppHeap) : Prop :=\n"; - OS << " h' = fun q => if q = p then Int.ofNat v.toNat else h q\n\n"; - OS << "opaque validPtr : Int -> Prop\n\n"; - // Reducible, so instance search sees the Bool comparison and decides it. - OS << "abbrev cppBvUlt {w : Nat} (x y : BitVec w) : Prop := x.ult y = " - "true\n"; - OS << "abbrev cppBvUle {w : Nat} (x y : BitVec w) : Prop := x.ule y = " - "true\n"; - OS << "abbrev cppBvSlt {w : Nat} (x y : BitVec w) : Prop := x.slt y = " - "true\n"; - OS << "abbrev cppBvSle {w : Nat} (x y : BitVec w) : Prop := x.sle y = " - "true\n\n"; - OS << "def cppIntDiv (x y : Int) : Int :=\n"; - OS << " if y = 0 then 0 else\n"; - OS << " let q := (if x < 0 then -x else x) / " - "(if y < 0 then -y else y)\n"; - 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"; - if (ProjectGoals) { - // What the bridges from readable goals use. - OS << "theorem cppverify_imp_or {a b : Prop} (h : a → b) : ¬a ∨ b :=\n"; - OS << " (Classical.em a).elim (fun ha => Or.inr (h ha)) Or.inl\n"; - OS << "theorem cppverify_not_imp_or {a b : Prop} (h : ¬a → b) : a ∨ b " - ":=\n"; - OS << " (Classical.em a).elim Or.inl (fun ha => Or.inr (h ha))\n\n"; - } + emitLeanPrelude(OS, ProjectGoals != nullptr); } - emitLeanFunctionDeclarations(Module, OS, EmittedFunctions); + emitLeanFunctionDeclarations(Module, OS, EmittedFunctions, Specs); emitLeanFunctionBodies(Module, OS); OS << "/- function: "; 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_" + @@ -1231,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; @@ -1273,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 7145e8596c..c2cc672246 100644 --- a/clang/lib/Verify/Backend/LeanBackend.h +++ b/clang/lib/Verify/Backend/LeanBackend.h @@ -4,8 +4,10 @@ #include "VerifyBackend.h" #include "llvm/Support/raw_ostream.h" +#include #include #include +#include #include namespace clang { @@ -33,26 +35,75 @@ 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. std::string leanProjectGroup(const ObligationModule &Module); +/// A logical function of a Lean project: its opaque declaration and, when it +/// has a definition Lean may accept, that definition, recursion measured by +/// its termination measures, with the functions it applies. +struct LeanSpecDeclaration { + /// Its Lean constant. + std::string Name; + std::string Opaque; + std::string Definition; + std::set Applies; +}; + +/// The generated modules of a Lean project: the specs its goals apply, by +/// identity, which every goal module imports, and each group's spec +/// definitions and goals. +struct LeanProjectModules { + std::map Specs; + std::map Goals; + /// The groups in the order their functions were exported: the source's. + std::vector Order; +}; + +/// The definitions every exported goal is stated with. +void emitLeanPrelude(llvm::raw_ostream &OS, bool Project); + /// Selection names the internal IDs to export; a project goal is named by /// its function and semantic hash, so it keeps its name whatever else is /// exported, and a scratch-pad goal keeps the positional name it has when /// every obligation is exported. A project records every goal of the module, -/// the ones left out as not exported. -VerifyResult -exportLeanScratchPad(const ObligationModule &Module, llvm::raw_ostream &OS, - bool EmitPreamble, std::set &EmittedFunctions, - std::set &EmittedTheorems, - unsigned ModuleIndex, - std::vector *ProjectGoals, - const std::set *Selection = nullptr); +/// the ones left out as not exported. Specs, when given, receives each spec +/// once, as its project declares it, instead of OS. +VerifyResult exportLeanScratchPad( + const ObligationModule &Module, llvm::raw_ostream &OS, bool EmitPreamble, + std::set &EmittedFunctions, + std::set &EmittedTheorems, unsigned ModuleIndex, + std::vector *ProjectGoals, + 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; + llvm::raw_ostream *Out = nullptr; + LeanProjectModules *Modules = nullptr; bool PreambleEmitted = false; std::set EmittedFunctions; std::set EmittedTheorems; @@ -64,12 +115,13 @@ class LeanVerifyBackend : public VerifyBackend { LeanVerifyBackend(llvm::raw_ostream *OS, std::vector *ProjectGoals) : Out(OS), ProjectGoals(ProjectGoals) {} + /// A project's export, into its modules. + LeanVerifyBackend(LeanProjectModules *Modules, + std::vector *ProjectGoals) + : Modules(Modules), ProjectGoals(ProjectGoals) {} llvm::StringRef getName() const override { return "lean"; } BackendCapabilities getCapabilities() const override { - // Collections have no Lean semantics yet. - return {allLogicFeatures() & ~logicFeature(LogicFeature::Sequences) & - ~logicFeature(LogicFeature::Collections), - false}; + return {allLogicFeatures(), false}; } /// Restrict later exports to these internal obligation IDs. void selectObligations(std::optional> Ids) { 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.cpp b/clang/lib/Verify/Backend/VerifyBackend.cpp index 134495fe9a..fac014a9f8 100644 --- a/clang/lib/Verify/Backend/VerifyBackend.cpp +++ b/clang/lib/Verify/Backend/VerifyBackend.cpp @@ -15,17 +15,31 @@ using namespace verify; VerifyResult LeanVerifyBackend::verifyModule(const ObligationModule &Module) { VerifyResult R; - if (!Out) { + if (!Out && !Modules) { R.Status = VerifyStatus::Unresolved; R.Reason = VerifyReason::LeanExportFailure; R.Message = "no lean output stream"; return R; } const size_t Before = ProjectGoals ? ProjectGoals->size() : 0; - VerifyResult Result = exportLeanScratchPad( - Module, *Out, !PreambleEmitted, EmittedFunctions, EmittedTheorems, - ++ModuleIndex, ProjectGoals, Selection ? &*Selection : nullptr); - PreambleEmitted = true; + VerifyResult Result; + if (Modules) { + // A project's goals go to their function's module, and the specs they + // apply are declared once, in the module every goal module imports. + const std::string Group = leanProjectGroup(Module); + if (!Modules->Goals.count(Group)) + Modules->Order.push_back(Group); + llvm::raw_string_ostream Goals(Modules->Goals[Group]); + Result = exportLeanScratchPad( + Module, Goals, /*EmitPreamble=*/false, EmittedFunctions, + EmittedTheorems, ++ModuleIndex, ProjectGoals, + Selection ? &*Selection : nullptr, &Modules->Specs); + } else { + Result = exportLeanScratchPad( + Module, *Out, !PreambleEmitted, EmittedFunctions, EmittedTheorems, + ++ModuleIndex, ProjectGoals, Selection ? &*Selection : nullptr); + PreambleEmitted = true; + } if (ProjectGoals) for (size_t I = Before; I < ProjectGoals->size(); ++I) if ((*ProjectGoals)[I].Exported) @@ -754,11 +768,14 @@ std::unique_ptr verify::createVerifyBackend(BackendKind K, llvm::raw_ostream *LeanOut, unsigned BMCUnroll, const BackendExecutionOptions &Execution, - std::vector *LeanProjectGoals) { + std::vector *LeanProjectGoals, + LeanProjectModules *LeanModules) { switch (K) { case BackendKind::Z3: return std::make_unique(Execution, "z3"); case BackendKind::Lean: + if (LeanModules) + return std::make_unique(LeanModules, LeanProjectGoals); return std::make_unique(LeanOut, LeanProjectGoals); case BackendKind::BMC: return std::make_unique(BMCUnroll, Execution); diff --git a/clang/lib/Verify/Backend/VerifyBackend.h b/clang/lib/Verify/Backend/VerifyBackend.h index 6159936740..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; @@ -307,12 +312,14 @@ inline unsigned moduleTimeoutMs(const ObligationModule &Module, } struct LeanProjectGoal; +struct LeanProjectModules; std::unique_ptr createVerifyBackend(BackendKind K, llvm::raw_ostream *LeanOut = nullptr, unsigned BMCUnroll = 10, const BackendExecutionOptions &Execution = {}, - std::vector *LeanProjectGoals = nullptr); + std::vector *LeanProjectGoals = nullptr, + LeanProjectModules *LeanModules = nullptr); VerifyResult lowerObligationModule(const ObligationModule &Module, 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 0db32bac01..8166156719 100644 --- a/clang/lib/Verify/Driver/LeanAutomation.h +++ b/clang/lib/Verify/Driver/LeanAutomation.h @@ -9,23 +9,32 @@ namespace verify { /// Names this module's tactics: a stub or automatic proof that an earlier /// revision wrote is tried again. -inline constexpr llvm::StringLiteral LeanAutomationRevision = "1"; +inline constexpr llvm::StringLiteral LeanAutomationRevision = "3"; /// The steps of cppverify_auto, each the whole proof of a goal it proves. inline constexpr llvm::StringLiteral LeanAutomationSteps[] = { - "cppverify_auto_grind", "cppverify_auto_heap", "cppverify_auto_bv", - "cppverify_auto_decide", "cppverify_auto_simp"}; + "cppverify_auto_grind", "cppverify_auto_heap", "cppverify_auto_bv", + "cppverify_auto_decide", "cppverify_auto_simp", "cppverify_auto_bveq", + "cppverify_auto_ext", "cppverify_auto_unfold", "cppverify_auto_eval", + "cppverify_auto_div"}; /// CppVerify/Auto.lean, written with every export. Its steps were chosen by /// what proves the goals of the test suite (heap stores as the functions /// they define, machine arithmetic as integers, then grind; stating toInt /// ranges and removing Int.bmod first proved nothing more, the latter less), /// each with a heartbeat budget of its own, as Vermilion's discharger ladder. +/// Revision 2 adds the last three, after the others, so that every goal an +/// earlier step proves keeps its proof: machine equalities and sign +/// extensions as integer facts, collection equality element by element, and +/// the definition instances a goal states, by the bodies they name. +/// Revision 3 adds the last two: the spec functions with Lean definitions +/// evaluated by their equations, and C++ division and remainder by their +/// definitions. inline constexpr llvm::StringLiteral LeanAutomationSource = R"lean(/- Generated by CppVerify: the tactics of its automatic proofs, which proof files may use too. Regeneration replaces this file. -/ import Lean -import CppVerify.Generated +import CppVerify.Prelude register_option cppverify.autoBudget : Nat := { defValue := 50000 @@ -82,6 +91,51 @@ elab "cppverify_unfold_readable" : tactic => withMainContext do let unfolded ← deltaExpand target (· == name) replaceMainGoal [← (← getMainGoal).change unfolded] +open Lean Elab Tactic Meta in +/-- Unfolds the definitions of spec bodies that a goal and its hypotheses +name, so that each definition instance a goal states says what the body +does. A body names only lower levels of its definition, so this ends. -/ +elab "cppverify_unfold_bodies" : tactic => withMainContext do + let isBody : Name → Bool := fun + | .str _ s => s.startsWith "cppSpecBody_" + | _ => false + let rec expand (e : Expr) : Nat → MetaM Expr + | 0 => return e + | fuel + 1 => do + let e' ← deltaExpand e isBody + if e' == e then return e else expand e' fuel + let mut goal ← getMainGoal + goal ← goal.change (← expand (← instantiateMVars (← goal.getType)) 64) + for d in ← goal.withContext getLCtx do + if d.isImplementationDetail then continue + let t ← instantiateMVars d.type + let t' ← expand t 64 + if t' != t then + goal ← goal.changeLocalDecl d.fvarId t' + replaceMainGoal [goal] + +open Lean Elab Tactic Meta in +/-- Rewrites with the equations of every spec function that Specs.lean +defines, and C++ division and remainder, so that applications at known +arguments become values. On unknown arguments it unfolds until its budget +is spent. -/ +elab "cppverify_eval_specs" : tactic => withMainContext do + let env ← getEnv + let mut lemmas : Array (TSyntax `Lean.Parser.Tactic.simpLemma) := #[] + let some idx := env.getModuleIdx? `CppVerify.Specs + | throwError "no spec function has a Lean definition" + let some data := env.header.moduleData[idx.toNat]? + | throwError "no spec function has a Lean definition" + for name in data.constNames do + if let .str .anonymous s := name then + if s.startsWith "cppSpec_" then + if let some (.defnInfo _) := env.find? name then + lemmas := lemmas.push + (← `(Lean.Parser.Tactic.simpLemma| $(mkIdent name):ident)) + if lemmas.isEmpty then + throwError "no spec function has a Lean definition" + evalTactic (← `(tactic| simp [$lemmas,*, cppIntDiv, cppIntRem])) + /-- Machine comparisons, constants, and overflow conditions as facts about integers. -/ macro "cppverify_norm" : tactic => `(tactic| (try simp only [cppBvSlt, cppBvSle, @@ -118,6 +172,108 @@ macro "cppverify_auto_decide" : tactic => macro "cppverify_auto_simp" : tactic => `(tactic| (cppverify_unfold_readable; simp_all)) +/-- Machine equalities, as of `x ≠ y` for distinct keys, and sign extensions +as facts about integers. -/ +macro "cppverify_bveq" : tactic => `(tactic| (try simp (disch := omega) only + [ne_eq, ← BitVec.toInt_inj, BitVec.toInt_signExtend_of_le] at *)) +macro "cppverify_auto_bveq" : tactic => `(tactic| ( + cppverify_unfold_readable + intros + cppverify_bveq + cppverify_norm + all_goals grind)) +/-- Two collections are equal when they agree at every element: equal +lengths and reads for sequences, membership for sets, counts for +multisets, and keys and values for maps. -/ +macro "cppverify_auto_ext" : tactic => `(tactic| ( + cppverify_unfold_readable + intros + (first | apply cppSeq_ext | apply cppSet_ext | apply cppMultiset_ext + | apply cppMap_ext) + all_goals (intros; cppverify_norm; all_goals grind))) +macro "cppverify_auto_unfold" : tactic => `(tactic| ( + cppverify_unfold_readable + intros + cppverify_unfold_bodies + cppverify_bveq + cppverify_norm + all_goals grind)) +macro "cppverify_auto_eval" : tactic => `(tactic| ( + cppverify_unfold_readable + intros + cppverify_bveq + cppverify_eval_specs + all_goals grind)) +/-- C++ division and remainder by their definitions, which grind reads by +constant divisors once the signs are split. -/ +macro "cppverify_auto_div" : tactic => `(tactic| ( + cppverify_unfold_readable + intros + cppverify_bveq + 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 @@ -132,7 +288,12 @@ elab "cppverify_auto" : tactic => do ("cppverify_auto_heap", ← `(tactic| cppverify_auto_heap)), ("cppverify_auto_bv", ← `(tactic| cppverify_auto_bv)), ("cppverify_auto_decide", ← `(tactic| cppverify_auto_decide)), - ("cppverify_auto_simp", ← `(tactic| cppverify_auto_simp))] + ("cppverify_auto_simp", ← `(tactic| cppverify_auto_simp)), + ("cppverify_auto_bveq", ← `(tactic| cppverify_auto_bveq)), + ("cppverify_auto_ext", ← `(tactic| cppverify_auto_ext)), + ("cppverify_auto_unfold", ← `(tactic| cppverify_auto_unfold)), + ("cppverify_auto_eval", ← `(tactic| cppverify_auto_eval)), + ("cppverify_auto_div", ← `(tactic| cppverify_auto_div))] for (name, step) in steps do let attempt : TacticM Unit := do let heartbeats ← IO.getNumHeartbeats diff --git a/clang/lib/Verify/Driver/LeanCertifier.h b/clang/lib/Verify/Driver/LeanCertifier.h index dc62393db9..da062f8322 100644 --- a/clang/lib/Verify/Driver/LeanCertifier.h +++ b/clang/lib/Verify/Driver/LeanCertifier.h @@ -16,7 +16,7 @@ open Lean /-- The axioms a constant depends on, through the statements and values of the constants it uses, read from the kernel's constants. -/ -def axiomsOf (env : Environment) (root : Name) : Except String NameSet := Id.run do +def axiomsOf (env : Kernel.Environment) (root : Name) : Except String NameSet := Id.run do let mut seen : NameSet := {} let mut axioms : NameSet := {} let mut work := #[root] @@ -38,9 +38,10 @@ def axiomsOf (env : Environment) (root : Name) : Except String NameSet := Id.run | none => return .error s!"{c} is not in the environment" return .ok axioms -/-- A module's imports and its own constants, read from its compiled files. -/ +/-- A module's imports and its own constants, in the order it declares them, +read from its compiled files. -/ unsafe def moduleConstants (module : Name) : - IO (Array Import × Std.HashMap Name ConstantInfo) := do + IO (Array Import × Array Name × Std.HashMap Name ConstantInfo) := do let file ← findOLean module let mut files := #[file] let server := OLeanLevel.server.adjustFileName file @@ -54,40 +55,99 @@ unsafe def moduleConstants (module : Name) : let mut constants := {} for name in parts[parts.size - 1].1.constNames, info in parts[parts.size - 1].1.constants do constants := constants.insert name info - return (parts[0].1.imports, constants) - -/-- Replays constants with the kernel into the environment of imports, as -leanchecker does: nothing in them escaped the kernel. -/ -unsafe def replayInto (imports : Array Import) - (constants : Std.HashMap Name ConstantInfo) : IO Unit := do - let (_, s) ← importModulesCore imports |>.run - let env ← finalizeImport s imports {} 0 false false (isModule := true) - discard <| env.toKernelEnv.replay constants - -/-- Replays a module's own constants into the environment of its imports. -/ -unsafe def replayModule (module : Name) : IO Unit := do - let (imports, constants) ← moduleConstants module - replayInto imports constants - -/-- Whether the proof of a goal states exactly the goal the generated module -defines and depends on no axiom outside the allowed ones. -/ -def checkStatement (env : Environment) (goal module : Name) (allowed : NameSet) : - Option String := Id.run do - let generated := `CppVerify.Generated - let moduleOf (c : Name) : Option Name := - (env.getModuleIdxFor? c).bind fun i => env.header.moduleNames[i.toNat]? - let proof := goal.appendAfter "_proof" + return (parts[0].1.imports, parts[parts.size - 1].1.constNames, constants) + +/-- A module of the project, read from its compiled files. -/ +structure ProjectModule where + name : Name + imports : Array Import + declared : Array Name + constants : Std.HashMap Name ConstantInfo + +/-- The modules of the project some modules import, each after the modules it +imports, and the toolchain's modules they import. -/ +structure Closure where + modules : Array ProjectModule := #[] + toolchain : Array Import := #[] + seen : NameSet := {} + +unsafe def Closure.visit (toolchain : String) (module : Name) : StateT Closure IO Unit := do + if (← get).seen.contains module then return + modify fun c => { c with seen := c.seen.insert module } + if (← findOLean module).toString.startsWith toolchain then + modify fun c => { c with toolchain := c.toolchain.push { module } } + return + let (imports, declared, constants) ← moduleConstants module + for i in imports do + Closure.visit toolchain i.module + modify fun c => { c with modules := c.modules.push { name := module, imports, declared, constants } } + +/-- The kernel's environment of the project: the toolchain's modules the +project imports, imported once, then every module of the project replayed +with the kernel, each after the modules it imports, as leanchecker does. A +module the kernel rejects, one that imports it, and one that declares a +constant an earlier module or the toolchain declares otherwise are left out, +each with why; the constant each other module declares is recorded with it. -/ +structure Replayed where + env : Kernel.Environment + rejected : Std.HashMap Name String + owner : Std.HashMap Name Name + +unsafe def replayProject (closure : Closure) : IO Replayed := do + let (_, s) ← importModulesCore closure.toolchain |>.run + let imported ← finalizeImport s closure.toolchain {} 0 false false (isModule := true) + let mut env := imported.toKernelEnv + let mut rejected : Std.HashMap Name String := {} + let mut owner : Std.HashMap Name Name := {} + for m in closure.modules do + if let some i := m.imports.find? (rejected.contains ·.module) then + rejected := rejected.insert m.name rejected[i.module]! + continue + let mut fresh : Std.HashMap Name ConstantInfo := {} + let mut clash : Option String := none + for (name, info) in m.constants do + match env.find? name with + | none => fresh := fresh.insert name info + | some known => + -- Lean derives an equation lemma in each module that unfolds a + -- definition, the same constant every time, and the kernel takes a + -- theorem twice when it states the same. + let same := known.type == info.type && known.levelParams == info.levelParams && + (known.isTheorem || known.value? == info.value?) + unless same do + let other := (owner[name]?).map toString |>.getD "the toolchain" + clash := some s!"{m.name} declares {name}, which {other} declares" + break + if let some why := clash then + rejected := rejected.insert m.name why + continue + try env ← env.replay fresh + catch e => + rejected := rejected.insert m.name s!"the kernel rejects {m.name}: {e}" + continue + for (name, _) in fresh do + owner := owner.insert name m.name + return { env, rejected, owner } + +/-- Whether the proof of a goal states exactly the goal its generated module +defines, or a refutation exactly its negation, and depends on no axiom +outside the allowed ones. -/ +def checkStatement (project : Replayed) (goal module generated : Name) + (refutes : Bool) (allowed : NameSet) : Option String := Id.run do + let env := project.env + 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 moduleOf goal != some generated then + if project.owner[goal]? != some generated then return some s!"{goal} is not the goal {generated} defines" | _ => return some s!"{generated} defines no goal {goal}" match env.find? proof with | some (.thmInfo v) => - if moduleOf proof != some module then + 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 => @@ -100,80 +160,56 @@ def checkStatement (env : Environment) (goal module : Name) (allowed : NameSet) | some _ => return some s!"{proof} is not a theorem" | none => return some s!"{module} declares no {proof}" -/-- A goal is proved when every module of the project its proof imports passes -the kernel (each replayed once in a run), and its proof states exactly the -goal and uses only the allowed axioms. Imported data is never freed: a later -import in the process reads it. -/ -unsafe def checkGoal (goal module : Name) (allowed : NameSet) (toolchain : String) - (replayed : IO.Ref NameSet) : IO (Option String) := do - let env ← importModules #[{ module }] {} - let project ← env.header.moduleNames.filterM fun m => - return !(← findOLean m).toString.startsWith toolchain - let why := checkStatement env goal module allowed - for m in project do - if (← replayed.get).contains m then continue - try replayModule m - catch e => return some s!"the kernel rejects {m}: {e}" - replayed.modify (·.insert m) - return why - -/-- Every goal checked in one environment: each proof module imported once, -and every module of the project replayed together into the environment of the -toolchain's modules they import. A check reads only kernel constants, each -in the module that declares it, so proofs imported together cannot change -each other's checks; but one bad module would stop the replay of all, and a -proof file that declares a goal's name stops the import, so then none is -reported (`none`) and each goal is checked by itself. A proof file of -cppverify_auto imports `Lean`, whose import each goal would repeat. -/ -unsafe def checkTogether (entries : Array (Name × Name)) (allowed : NameSet) - (toolchain : String) : IO (Option (Array (Option String))) := do - let modules := entries.foldl (fun ms (_, m) => if ms.contains m then ms else ms.push m) #[] - let some env ← (try some <$> importModules (modules.map ({ module := · })) {} - catch _ => pure none) | return none - let project ← env.header.moduleNames.filterM fun m => - return !(← findOLean m).toString.startsWith toolchain - let mut imports : Array Import := #[] - let mut constants : Std.HashMap Name ConstantInfo := {} - for m in project do - let (own, declared) ← moduleConstants m - for i in own do - unless project.contains i.module || imports.any (·.module == i.module) do - imports := imports.push i - -- Lean derives an equation lemma in each module that unfolds the - -- definition, the same constant every time. - for (name, info) in declared do - if let some known := constants[name]? then - unless known.type == info.type && known.value? == info.value? do - return none - continue - constants := constants.insert name info - try replayInto imports constants catch _ => return none - return some (entries.map fun (goal, module) => checkStatement env goal module allowed) - -/-- Usage: Certify GOALS ALLOWED, where each line of GOALS is a goal and its -proof module, separated by a tab, 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. -/ +/-- The declaration of the user's lemmas that uses `sorry`, if one does: an +admitted lemma fails every goal, as when the module was compiled with `sorry` +an error. -/ +def userSorry (closure : Closure) (project : Replayed) : Option String := Id.run do + let some user := closure.modules.find? (·.name == `CppVerify.User) | return none + for name in user.declared do + if let .ok axioms := axiomsOf project.env name then + if axioms.contains ``sorryAx then + 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, 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) := #[] + let mut entries : Array (Name × Name × Name × Bool) := #[] for line in ← IO.FS.lines goals do - let [goal, module] := line.splitOn "\t" | continue - entries := entries.push (goal.toName, module.toName) - let report (goal : Name) : Option String → IO Unit - | none => IO.println s!"ok\t{goal}" - | some why => IO.println s!"fail\t{goal}\t{why.replace "\n" " "}" - if let some results ← checkTogether entries allowed toolchain then - for (goal, _) in entries, why in results do - report goal why - return 0 - let replayed ← IO.mkRef ({} : NameSet) - for (goal, module) in entries do - report goal (← checkGoal goal module allowed toolchain replayed) + 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, refutes) in entries do + let why := (project.rejected[module]?).orElse fun _ => + (project.rejected[generated]?).orElse fun _ => user.orElse fun _ => + checkStatement project goal module generated refutes allowed + match why with + | 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 f317e60815..2833bf10a0 100644 --- a/clang/lib/Verify/Driver/Verifier.cpp +++ b/clang/lib/Verify/Driver/Verifier.cpp @@ -32,6 +32,7 @@ #include "llvm/ADT/ScopeExit.h" #include "llvm/ADT/SmallString.h" #include "llvm/ADT/SmallVector.h" +#include "llvm/ADT/StringExtras.h" #include "llvm/Support/Error.h" #include "llvm/Support/FileSystem.h" #include "llvm/Support/FormatVariadic.h" @@ -41,6 +42,7 @@ #include "llvm/Support/MemoryBuffer.h" #include "llvm/Support/Path.h" #include "llvm/Support/Program.h" +#include "llvm/Support/SHA256.h" #include "llvm/Support/ThreadPool.h" #include "llvm/Support/Threading.h" #include "llvm/Support/raw_ostream.h" @@ -1061,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 { @@ -1255,6 +1259,28 @@ static llvm::Error writeTextFile(llvm::StringRef Path, return llvm::Error::success(); } +// A generated file is rewritten only when it changes, so that a rerun of the +// same source leaves every file as it was. +static llvm::Error writeTextFileIfChanged(llvm::StringRef Path, + llvm::StringRef Contents) { + if (auto Buffer = llvm::MemoryBuffer::getFile(Path, /*IsText=*/true)) + if ((*Buffer)->getBuffer() == Contents) + return llvm::Error::success(); + return writeTextFile(Path, Contents); +} + +static constexpr llvm::StringLiteral LeanGeneratedNote = + "/- Generated by CppVerify. Regeneration replaces this file, never a " + "proof. -/"; + +// What each module of goals starts with: options and the instance attribute +// of the prelude's classical decidability are local to a file. +static constexpr llvm::StringLiteral LeanGoalModulePreamble = + "noncomputable section\n\n" + "set_option maxRecDepth 100000\n" + "set_option maxHeartbeats 0\n\n" + "attribute [local instance] cppVerifyPropDecidable\n\n"; + static llvm::Error writeTextFileIfMissing(llvm::StringRef Path, llvm::StringRef Contents) { if (llvm::sys::fs::exists(Path)) @@ -1314,18 +1340,28 @@ struct LeanProofRecord { std::string Automation; }; -// A proof starts from the goal's readable form, its names introduced. Stubs -// before cppverify_auto did not import it. -static std::string leanProofHead(llvm::StringRef Goal, bool Automation = true) { - return "import CppVerify.User\n" + - std::string(Automation ? "import CppVerify.Auto\n" : "") + - "\ntheorem " + Goal.str() + "_proof : " + Goal.str() + +// The imports a proof file starts with: its function's goals, the user's +// lemmas, and the automation. Before 0.2's modules a proof imported only +// User (which imported every goal), and before cppverify_auto, not Auto. +enum class LeanProofImports { Modules, Automation, User }; + +// A proof starts from the goal's readable form, its names introduced. +static std::string +leanProofHead(llvm::StringRef Goal, llvm::StringRef Group, + LeanProofImports Imports = LeanProofImports::Modules) { + std::string Head; + if (Imports == LeanProofImports::Modules) + Head += "import CppVerify.Goals." + Group.str() + "\n"; + Head += "import CppVerify.User\n"; + if (Imports != LeanProofImports::User) + Head += "import CppVerify.Auto\n"; + return Head + "\ntheorem " + Goal.str() + "_proof : " + Goal.str() + " := by\n apply " + Goal.str() + ".of_readable\n"; } -static std::string leanProof(llvm::StringRef Goal, llvm::StringRef Intros, - llvm::StringRef Last) { - std::string Proof = leanProofHead(Goal); +static std::string leanProof(llvm::StringRef Goal, llvm::StringRef Group, + llvm::StringRef Intros, llvm::StringRef Last) { + std::string Proof = leanProofHead(Goal, Group); if (!Intros.empty()) Proof += " intro " + Intros.str() + "\n"; return Proof + " " + Last.str() + "\n"; @@ -1335,9 +1371,15 @@ static std::string leanProof(llvm::StringRef Goal, llvm::StringRef Intros, // whether cppverify_auto proves it: its last line is a stub's `sorry` or a // step of cppverify_auto. static std::optional leanGeneratedProof(llvm::StringRef Body, - llvm::StringRef Goal) { - if (!Body.consume_front(leanProofHead(Goal)) && - !Body.consume_front(leanProofHead(Goal, /*Automation=*/false))) + llvm::StringRef Goal, + llvm::StringRef Group) { + if (!llvm::any_of( + std::initializer_list{LeanProofImports::Modules, + LeanProofImports::Automation, + LeanProofImports::User}, + [&](LeanProofImports Imports) { + return Body.consume_front(leanProofHead(Goal, Group, Imports)); + })) return std::nullopt; if (Body.consume_front(" intro ")) { const size_t End = Body.find('\n'); @@ -1354,6 +1396,10 @@ static std::optional leanGeneratedProof(llvm::StringRef Body, } // The revision of cppverify_auto that an automation note was written by. +// Names the printing of spec definitions and the prelude's tactic for their +// measures: a verdict an earlier revision kept is not used. +static constexpr llvm::StringLiteral LeanSpecRevision = "1"; + static std::string leanAutomationTag() { return ("cppverify_auto " + LeanAutomationRevision + " ").str(); } @@ -1407,8 +1453,9 @@ static std::optional readLeanProof(llvm::StringRef Path) { return std::nullopt; const size_t End = Text.find("-/\n"); if (End != llvm::StringRef::npos) - if (std::optional Automatic = - leanGeneratedProof(Text.substr(End + 3), Record.Goal)) { + if (std::optional Automatic = leanGeneratedProof( + Text.substr(End + 3), Record.Goal, + llvm::sys::path::filename(llvm::sys::path::parent_path(Path)))) { Record.Pristine = true; Record.Automatic = *Automatic; } @@ -1428,7 +1475,8 @@ static void replaceAllIn(std::string &Text, llvm::StringRef From, static llvm::Error moveLeanProof(llvm::StringRef From, llvm::StringRef To, const LeanProjectGoal &Goal, llvm::StringRef OldGoal, - llvm::StringRef OldBodies) { + llvm::StringRef OldBodies, + llvm::StringRef OldGroup = "") { auto Buffer = llvm::MemoryBuffer::getFile(From); if (!Buffer) return llvm::createStringError( @@ -1449,6 +1497,9 @@ static llvm::Error moveLeanProof(llvm::StringRef From, llvm::StringRef To, } replaceAllIn(Body, OldGoal, Goal.Name); replaceAllIn(Body, OldBodies, Goal.BodyPrefix); + if (!OldGroup.empty()) + replaceAllIn(Body, ("import CppVerify.Goals." + OldGroup + "\n").str(), + "import CppVerify.Goals." + Goal.Group + "\n"); if (std::error_code EC = llvm::sys::fs::create_directories(llvm::sys::path::parent_path(To))) return llvm::createStringError(EC, "cannot create %s", To.str().c_str()); @@ -1499,131 +1550,25 @@ 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::Expected initializeLeanProject() { + llvm::Error initializeLeanProject() { const std::string &Root = leanProjectRoot(); std::error_code EC = llvm::sys::fs::create_directories( leanProjectPath(Root, {"CppVerify", "Proofs"})); @@ -1649,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); @@ -1672,18 +1615,104 @@ class Verifier { leanProjectPath(Root, {"lakefile.toml"}), Lakefile)) return std::move(Error); + // A project of an earlier release imports CppVerify.Generated here, + // which still imports every goal. constexpr llvm::StringLiteral UserFile = - "import CppVerify.Generated\n\n" + "import CppVerify.Specs\n\n" "/- Add reusable lemmas here. This file is never regenerated. -/\n"; if (llvm::Error Error = writeTextFileIfMissing( leanProjectPath(Root, {"CppVerify", "User.lean"}), UserFile)) - return std::move(Error); - if (llvm::Error Error = - writeTextFile(leanProjectPath(Root, {"CppVerify", "Auto.lean"}), - LeanAutomationSource)) - return std::move(Error); + return Error; + + std::string Prelude = std::string(LeanGeneratedNote) + "\n\n"; + llvm::raw_string_ostream PreludeOS(Prelude); + emitLeanPrelude(PreludeOS, /*Project=*/true); + for (const auto &[File, Contents] : + {std::pair{"Prelude.lean", Prelude}, + {"Auto.lean", LeanAutomationSource}}) + if (llvm::Error Error = writeTextFileIfChanged( + leanProjectPath(Root, {"CppVerify", File}), Contents)) + return Error; + // The root of the library, so that `lake build` builds every proof. + return writeTextFileIfChanged(leanProjectPath(Root, {"CppVerify.lean"}), + "import CppVerify.Check\n"); + } + + // The generated modules of a run: Specs, a goal module for each function + // the run exported, and Generated, which imports them all. Any other goal + // module is removed, so that every module of the project builds: one an + // earlier run wrote may apply a spec Specs no longer declares, as after a + // fallback run whose solver settled the functions that applied it. The + // proofs of a function the run did not export stay as they are. + llvm::Error writeLeanProjectModules(const LeanProjectModules &Modules) { + const std::string &Root = leanProjectRoot(); + const std::string Header = std::string(LeanGeneratedNote) + "\n"; + if (llvm::Error Error = writeTextFileIfChanged( + leanProjectPath(Root, {"CppVerify", "Specs.lean"}), + Header + + "import CppVerify.Prelude\n\nnoncomputable section\n\n" + "attribute [local instance] cppVerifyPropDecidable\n\n" + + leanSpecsText(Modules))) + return Error; + const std::string GoalsDir = leanProjectPath(Root, {"CppVerify", "Goals"}); + if (std::error_code EC = llvm::sys::fs::create_directories(GoalsDir)) + return llvm::createStringError(EC, "cannot create %s", GoalsDir.c_str()); + std::string Generated = Header + "import CppVerify.Prelude\n" + "import CppVerify.Specs\n"; + for (const std::string &Group : Modules.Order) { + if (llvm::Error Error = writeTextFileIfChanged( + leanProjectPath(GoalsDir, {Group + ".lean"}), + Header + "import CppVerify.Specs\n\n" + + LeanGoalModulePreamble.str() + Modules.Goals.at(Group))) + return Error; + Generated += "import CppVerify.Goals." + Group + "\n"; + } + if (llvm::Error Error = writeTextFileIfChanged( + leanProjectPath(Root, {"CppVerify", "Generated.lean"}), Generated)) + return Error; + + std::error_code EC; + for (llvm::sys::fs::directory_iterator It(GoalsDir, EC), End; + It != End && !EC; It.increment(EC)) + if (llvm::sys::path::extension(It->path()) == ".lean" && + !Modules.Goals.count(llvm::sys::path::stem(It->path()).str())) + llvm::sys::fs::remove(It->path()); + return llvm::Error::success(); + } - return leanProjectPath(Root, {"CppVerify", "Generated.lean"}); + // 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 @@ -1802,15 +1831,15 @@ class Verifier { (Moving->Path != ProofPath || !Taken.count(ProofPath))) { const bool WasKept = llvm::StringRef(Moving->Path).starts_with(StaleDir); - if (llvm::Error Error = moveLeanProof(Moving->Path, ProofPath, *Goal, - Moving->Goal, Moving->BodyPrefix)) + if (llvm::Error Error = + 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()); @@ -1821,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)) { @@ -1841,9 +1868,10 @@ class Verifier { llvm::sys::path::parent_path(ProofPath))) return llvm::createStringError(EC, "cannot create %s", ProofPath.c_str()); - if (llvm::Error Error = writeTextFile( - ProofPath, leanProofHeader(*Goal) + - leanProof(Goal->Name, Goal->Intros, "sorry"))) + if (llvm::Error Error = + writeTextFile(ProofPath, leanProofHeader(*Goal) + + leanProof(Goal->Name, Goal->Group, + Goal->Intros, "sorry"))) return Error; Taken.insert(ProofPath); } @@ -1870,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) { @@ -1918,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"; @@ -1931,8 +1957,8 @@ class Verifier { CheckFile += "example : " + Name + " := " + Name + "_proof\n"; CheckFile += "#print axioms " + Name + "_proof\n"; } - return writeTextFile(leanProjectPath(Root, {"CppVerify", "Check.lean"}), - CheckFile); + return writeTextFileIfChanged( + leanProjectPath(Root, {"CppVerify", "Check.lean"}), CheckFile); } // Certifies each goal's proof: an error fails every goal; otherwise the @@ -2008,9 +2034,301 @@ class Verifier { return Launcher; } + // The specs of a project as Specs.lean declares them: each recursion group + // by its real definitions where Lean accepts them, callees first, and + // opaque where it does not, where a member has no definition, or where no + // Lean is installed to try them. Lean's verdict on a group's text, with + // what its callees are, is kept in .cppverify/specs, so that the file is + // the same on every run. A group is tried with its undecided callees real + // and keeps its verdict only if they are; else it is tried again with the + // rejected callees opaque. + std::string leanSpecsText(const LeanProjectModules &Modules) { + const auto &Specs = Modules.Specs; + // Strongly connected components of the calls, callees first (Tarjan). + std::vector> Groups; + std::map GroupOf; + { + std::map Index, Low; + std::set OnStack; + std::vector Stack; + unsigned Counter = 0; + std::function visit = + [&](const std::string &V) { + Index[V] = Low[V] = Counter++; + Stack.push_back(V); + OnStack.insert(V); + for (const std::string &W : Specs.at(V).Applies) { + if (!Specs.count(W)) + continue; + if (!Index.count(W)) { + visit(W); + Low[V] = std::min(Low[V], Low[W]); + } else if (OnStack.count(W)) { + Low[V] = std::min(Low[V], Index[W]); + } + } + if (Low[V] != Index[V]) + return; + std::vector Group; + std::string W; + do { + W = Stack.back(); + Stack.pop_back(); + OnStack.erase(W); + Group.push_back(W); + GroupOf[W] = Groups.size(); + } while (W != V); + std::sort(Group.begin(), Group.end()); + Groups.push_back(std::move(Group)); + }; + for (const auto &[Identity, Declaration] : Specs) + if (!Index.count(Identity)) + visit(Identity); + } + std::vector> Callees(Groups.size()); + std::vector Definition(Groups.size()); + // 1 real, 0 opaque, -1 undecided. + std::vector Verdict(Groups.size(), -1); + for (size_t G = 0; G != Groups.size(); ++G) { + for (const std::string &Member : Groups[G]) { + const LeanSpecDeclaration &Declaration = Specs.at(Member); + if (Declaration.Definition.empty()) + Verdict[G] = 0; + Definition[G] += Declaration.Definition; + for (const std::string &Callee : Declaration.Applies) + if (Specs.count(Callee) && GroupOf.at(Callee) != G) + Callees[G].insert(GroupOf.at(Callee)); + } + if (Groups[G].size() > 1) + Definition[G] = "mutual\n" + Definition[G] + "end\n\n"; + } + auto opaque = [&](size_t G) { + std::string Text; + for (const std::string &Member : Groups[G]) + Text += Specs.at(Member).Opaque; + return Text; + }; + // What a group's verdict rests on: the toolchain, this revision of the + // printer and the prelude's tactic, its text, and what its callees are. + auto keyOf = [&](size_t G, const std::set &Assumed) { + llvm::SHA256 Hasher; + Hasher.update(LeanToolchain); + Hasher.update(LeanSpecRevision); + Hasher.update(Definition[G]); + for (size_t C : Callees[G]) + Hasher.update(Groups[C].front() + (Verdict[C] == 1 || Assumed.count(C) + ? "=real" + : "=opaque")); + return llvm::toHex(Hasher.final()); + }; + const std::string &Root = leanProjectRoot(); + const std::string Dir = leanProjectPath(Root, {".cppverify", "specs"}); + std::optional Launcher; + bool LeanUnavailable = false; + for (size_t Round = 0; Round <= Groups.size(); ++Round) { + std::set Trying; + std::map Keys; + for (size_t G = 0; G != Groups.size(); ++G) { + if (Verdict[G] >= 0) + continue; + const bool CalleesDecided = + llvm::all_of(Callees[G], [&](size_t C) { return Verdict[C] >= 0; }); + const std::string Key = keyOf(G, Trying); + if (CalleesDecided) + if (auto Kept = + llvm::MemoryBuffer::getFile(leanProjectPath(Dir, {Key}))) { + Verdict[G] = (*Kept)->getBuffer().trim() == "real" ? 1 : 0; + continue; + } + if (LeanUnavailable) { + Verdict[G] = 0; + continue; + } + Trying.insert(G); + Keys[G] = Key; + } + if (Trying.empty()) + break; + std::map Axioms; + if (!tryLeanSpecs(Specs, Groups, Definition, Verdict, Trying, Launcher, + opaque, Axioms)) { + LeanUnavailable = true; + for (size_t G : Trying) + Verdict[G] = 0; + break; + } + std::map Accepted; + for (size_t G : Trying) + Accepted[G] = llvm::all_of(Groups[G], [&](const std::string &Member) { + auto It = Axioms.find(Specs.at(Member).Name); + if (It == Axioms.end() || It->second == "missing") + return false; + llvm::SmallVector Used; + llvm::StringRef(It->second).split(Used, ',', -1, false); + return llvm::all_of(Used, [](llvm::StringRef Axiom) { + return Axiom == "propext" || Axiom == "Quot.sound" || + Axiom == "Classical.choice"; + }); + }); + // A callee decided before this round was what the trial assumed; one + // tried in it was assumed real. + for (size_t G : Trying) { + if (!llvm::all_of(Callees[G], [&](size_t C) { + return !Trying.count(C) || Accepted[C]; + })) + continue; + Verdict[G] = Accepted[G] ? 1 : 0; + if (!llvm::sys::fs::create_directories(Dir)) + llvm::consumeError( + writeTextFile(leanProjectPath(Dir, {Keys[G]}), + Accepted[G] ? "real\n" : "opaque\n")); + } + } + std::string Text; + for (size_t G = 0; G != Groups.size(); ++G) + Text += Verdict[G] == 1 ? Definition[G] : opaque(G); + return Text; + } + + // Elaborates the spec groups of Trying with the others as decided, in a + // file of their own, and reports the axioms of each member of Trying: a + // definition Lean rejects is added with sorryAx, or not at all. False when + // no pinned Lean can run it. + bool tryLeanSpecs(const std::map &Specs, + const std::vector> &Groups, + const std::vector &Definition, + const std::vector &Verdict, + const std::set &Trying, + std::optional &Launcher, + llvm::function_ref Opaque, + std::map &Axioms) { + const std::string &Root = leanProjectRoot(); + if (!Launcher) { + auto Found = leanLauncher(".cppverify-specs"); + if (!Found) { + llvm::consumeError(Found.takeError()); + return false; + } + if (auto Build = Found->run({"build", "CppVerify.Auto"}, "build", Root); + !Build) { + llvm::consumeError(Build.takeError()); + return false; + } + Launcher = std::move(*Found); + } + const std::string Dir = leanProjectPath(Root, {".cppverify", "specs"}); + if (llvm::sys::fs::create_directories(Dir)) + return false; + const std::string Source = leanProjectPath(Dir, {"trial.lean"}); + const std::string Report = leanProjectPath(Dir, {"trial.report"}); + std::string Quoted = "\""; + for (char C : Report) { + if (C == '\\' || C == '"') + Quoted += '\\'; + Quoted += C; + } + Quoted += "\""; + std::string Text = "import CppVerify.Auto\n\n#eval CppVerify.Auto.report " + + Quoted + + " \"ready\"\n\nnoncomputable section\n\n" + "attribute [local instance] cppVerifyPropDecidable\n\n"; + for (size_t G = 0; G != Groups.size(); ++G) { + if (Verdict[G] == 1 || Trying.count(G)) + Text += Definition[G]; + else + Text += Opaque(G); + if (Trying.count(G)) + for (const std::string &Member : Groups[G]) + Text += "#cppverify_axioms " + Quoted + " " + Specs.at(Member).Name + + "\n\n"; + } + llvm::sys::fs::remove(Report); + if (llvm::Error Error = writeTextFile(Source, Text)) { + llvm::consumeError(std::move(Error)); + return false; + } + // Lean exits with an error status when a definition fails; the report + // says which. + if (auto Run = Launcher->run({"env", "lean", "-DmaxErrors=1000000", Source}, + "specs", Root); + !Run) + llvm::consumeError(Run.takeError()); + auto Buffer = llvm::MemoryBuffer::getFile(Report); + if (!Buffer) + return false; + bool Ready = false; + for (llvm::StringRef Rest = (*Buffer)->getBuffer(); !Rest.empty();) { + auto [Line, Next] = Rest.split('\n'); + Rest = Next; + Line = Line.rtrim("\r"); + if (Line == "ready") { + Ready = true; + continue; + } + llvm::SmallVector Fields; + Line.split(Fields, '\t', 2); + if (Fields.size() == 3 && Fields[0] == "axioms") + Axioms[Fields[1].str()] = Fields[2].str(); + } + return Ready; + } + + // What a proof is built from: the pinned toolchain, its source, and the + // compiled modules of the project in its import closure, read from the + // import lines of their sources. None when a module of the closure has no + // compiled module. + std::optional leanProofKey(llvm::StringRef ProofSource) { + const std::string &Root = leanProjectRoot(); + auto importsOf = [](llvm::StringRef Source) { + std::vector Imports; + if (auto Buffer = llvm::MemoryBuffer::getFile(Source)) + for (llvm::StringRef Rest = (*Buffer)->getBuffer(); !Rest.empty();) { + auto [Line, Next] = Rest.split('\n'); + Rest = Next; + if (Line.consume_front("import ")) + Imports.push_back(Line.trim().str()); + } + return Imports; + }; + llvm::SHA256 Hasher; + Hasher.update(LeanToolchain); + auto Source = llvm::MemoryBuffer::getFile(ProofSource); + if (!Source) + return std::nullopt; + Hasher.update((*Source)->getBuffer()); + std::map Compiled; + std::vector Work = importsOf(ProofSource); + while (!Work.empty()) { + const std::string Module = Work.back(); + Work.pop_back(); + if (Compiled.count(Module)) + continue; + std::string Relative = Module; + std::replace(Relative.begin(), Relative.end(), '.', '/'); + const std::string ModuleSource = + leanProjectPath(Root, {Relative + ".lean"}); + if (!llvm::sys::fs::exists(ModuleSource)) + continue; + auto Object = llvm::MemoryBuffer::getFile(leanProjectPath( + Root, {".lake", "build", "lib", "lean", Relative + ".olean"})); + if (!Object) + return std::nullopt; + Compiled[Module] = llvm::toHex(llvm::SHA256::hash( + llvm::arrayRefFromStringRef((*Object)->getBuffer()))); + for (std::string &Import : importsOf(ModuleSource)) + Work.push_back(std::move(Import)); + } + for (const auto &[Module, Hash] : Compiled) { + Hasher.update(Module); + Hasher.update(Hash); + } + return llvm::toHex(Hasher.final()); + } + 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"); @@ -2028,15 +2346,6 @@ class Verifier { !Build) return Build.takeError(); - const std::string UserObject = leanProjectPath( - Root, {".lake", "build", "lib", "lean", "CppVerify", "User.olean"}); - if (auto User = - runLake({"env", "lean", "-EhasSorry", "-R", Root, "-o", UserObject, - leanProjectPath(Root, {"CppVerify", "User.lean"})}, - "user"); - !User) - return User.takeError(); - const std::string ProofBuildDir = leanProjectPath( Root, {".lake", "build", "lib", "lean", "CppVerify", "Proofs"}); if (std::error_code EC = llvm::sys::fs::create_directories(ProofBuildDir)) @@ -2046,31 +2355,70 @@ 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. + // Each proof builds by itself, several at once, unless nothing it is + // built from changed since it last built: its source and the compiled + // modules of the project it imports (which Lake has just built). Lake + // cannot say this itself: a module whose import failed is not built and + // not named, and its .olean of an earlier build would stay. + const std::string KeyDir = leanProjectPath(Root, {".cppverify", "built"}); + if (std::error_code EC = llvm::sys::fs::create_directories(KeyDir)) + return llvm::createStringError(EC, "cannot create %s", KeyDir.c_str()); std::vector> BuildErrors(Proofs.size()); 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)) + if (auto Kept = llvm::MemoryBuffer::getFile(KeyFile)) + if ((*Kept)->getBuffer() == *Key) + continue; llvm::sys::fs::remove(ProofObject); + llvm::sys::fs::remove(KeyFile); if (auto Proof = runLake({"env", "lean", "-EhasSorry", "-R", Root, "-o", ProofObject, ProofSource}, Name); !Proof) BuildErrors[I] = llvm::StringRef(llvm::toString(Proof.takeError())).rtrim().str(); + else if (Key) + llvm::consumeError(writeTextFile(KeyFile, *Key)); } }; { @@ -2083,12 +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 + "\n"; + Built += Proofs[I].Entry; } if (Built.empty()) return Failures; @@ -2121,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; } @@ -2179,7 +2526,8 @@ class Verifier { : ""; for (size_t Next = 0; Next < Goals.size() && !interruptRequested();) { - std::string Text = "import CppVerify.User\nimport CppVerify.Auto\n\n" + std::string Text = "import CppVerify.Generated\nimport CppVerify.User\n" + "import CppVerify.Auto\n\n" "set_option cppverify.autoReport " + ReportName + "\n#eval CppVerify.Auto.report " + ReportName + " \"ready\"\n"; @@ -2318,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; @@ -2331,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 @@ -2369,12 +2712,12 @@ 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.User", "CppVerify.Auto"}, "build", Root); + if (auto Build = Launcher->run({"build", "CppVerify.Generated", + "CppVerify.User", "CppVerify.Auto"}, + "build", Root); !Build) return skipped( "the project does not build (" + @@ -2425,20 +2768,145 @@ class Verifier { const std::string Text = Trial.Step.empty() ? leanProofHeader(Goal, Tag + Trial.Why) + - leanProof(Goal.Name, Goal.Intros, "sorry") + leanProof(Goal.Name, Goal.Group, Goal.Intros, "sorry") : leanProofHeader(Goal, Tag + "proves it with " + Trial.Step, /*Automatic=*/true) + - leanProof(Goal.Name, Goal.Intros, Trial.Step); + leanProof(Goal.Name, Goal.Group, Goal.Intros, Trial.Step); if (llvm::Error Error = writeTextFile(pathOf(Goal), Text)) Failures.push_back(llvm::toString(std::move(Error))); } 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, @@ -2664,19 +3132,19 @@ class Verifier { std::string LeanOutputPath = Opts.LeanOutPath; const bool HasLeanProject = !Opts.LeanProjectPath.empty() || !Opts.LeanFallbackProjectPath.empty(); + // A project's goals go to modules, one per function. + LeanProjectModules LeanModules; if (HasLeanProject) { - auto GeneratedPath = initializeLeanProject(); - if (!GeneratedPath) { + Lean.emplace(Opts); + llvm::Error Error = Lean->initializeLeanProject(); + reportLeanWarnings(); + if (Error) { Diags.push_back({VerifyDiagnostic::Error, "cannot initialize Lean project (" + - llvm::toString(GeneratedPath.takeError()) + ")"}); + llvm::toString(std::move(Error)) + ")"}); return false; } - LeanOutputPath = std::move(*GeneratedPath); - } - if ((Opts.Backend == BackendKind::Lean || - !Opts.LeanFallbackProjectPath.empty()) && - !LeanOutputPath.empty()) { + } else if (Opts.Backend == BackendKind::Lean && !LeanOutputPath.empty()) { std::error_code EC; LeanFile = std::make_unique(LeanOutputPath, EC, llvm::sys::fs::OF_Text); @@ -2720,11 +3188,12 @@ class Verifier { if (!Parallel) SharedBackend = createVerifyBackend( Opts.Backend, LeanOut, Opts.BMCUnroll, Execution, - Opts.LeanProjectPath.empty() ? nullptr : &LeanProjectGoals); + Opts.LeanProjectPath.empty() ? nullptr : &LeanProjectGoals, + Opts.LeanProjectPath.empty() ? nullptr : &LeanModules); std::unique_ptr LeanFallbackBackend; if (!Opts.LeanFallbackProjectPath.empty()) - LeanFallbackBackend = std::make_unique( - LeanFile.get(), &LeanProjectGoals); + LeanFallbackBackend = + std::make_unique(&LeanModules, &LeanProjectGoals); // Vacuity checks: whether a verified function's end is reachable at all. // A vacuous path is refuted quickly; a satisfiable one is not worth // searching long, since an unsettled check only omits a warning. @@ -2848,6 +3317,14 @@ class Verifier { BackendKind Kind; }; std::vector Confirmations; + /// Certified failures a fallback project shows in Lean: each one's + /// place in Diags and its refutation, or why it has none. + struct Refutation { + size_t Index; + std::optional Lean; + std::string Why; + }; + std::vector Refutations; /// For a verified proof function: what its verification proves. std::shared_ptr Contract; /// The verdict on the definedness of the function's contract, when it @@ -4065,6 +4542,21 @@ class Verifier { AnyFailed = true; if (!Fn->IsProof) FailedCallers.insert(Fn->Identity); + // A fallback project shows a certified counterexample in Lean too. + if (LeanFallbackBackend && R.Reason == VerifyReason::Counterexample) { + FunctionRun::Refutation Pending{Diags.size(), std::nullopt, + "the solver's model gives the " + "goal's variables no values"}; + auto Item = + llvm::find_if(Module.Obligations, [&](const Obligation &Item) { + return (Item.StableId.empty() ? Item.Id : Item.StableId) == + R.ObligationId; + }); + if (R.Assignment && Item != Module.Obligations.end()) + Pending.Lean = exportLeanRefutation( + Module, *Item, *R.Assignment, LeanModules.Specs, Pending.Why); + Run.Refutations.push_back(std::move(Pending)); + } std::string Msg = "verification failed: " + Fn->Name; if (!R.ObligationId.empty()) Msg += " [" + R.ObligationId + "]"; @@ -4111,6 +4603,7 @@ class Verifier { D.Hidden = true; Run.AllOk = false; Run.Confirmations.clear(); + Run.Refutations.clear(); VerifyResult Result; Result.Status = VerifyStatus::Unresolved; Result.Reason = VerifyReason::Interrupted; @@ -4118,6 +4611,10 @@ class Verifier { Fn.Name, std::move(Result)}); }; std::vector Confirmations; + std::vector Refutations; + // What certification found of the refutations, or why it checked none. + std::optional> RefutationChecks; + std::string RefutationsUnchecked; for (size_t I = 0; I != Runs.size(); ++I) { FunctionRun &Run = Runs[I]; if (Run.Interrupted) @@ -4148,6 +4645,10 @@ class Verifier { Pending.Index += Base; Confirmations.push_back(std::move(Pending)); } + for (FunctionRun::Refutation &Pending : Run.Refutations) { + Pending.Index += Base; + Refutations.push_back(std::move(Pending)); + } if (Run.ContractCheck) ContractChecks[Functions[I]->Identity] = Base + *Run.ContractCheck; if (DumpOS) @@ -4160,19 +4661,34 @@ class Verifier { // certified one is a proof like a solver's, and one that fails, or that // certification does not check, establishes nothing. if (HasLeanProject) { - if (LeanFile) { - LeanFile->flush(); - LeanFile.reset(); - } std::vector ExportedGoals; llvm::copy_if(LeanProjectGoals, std::back_inserter(ExportedGoals), [](const LeanProjectGoal &Goal) { return Goal.Exported; }); - llvm::Error Finalized = finalizeLeanProject( - LeanProjectGoals, LeanFallbackBackend ? &LeanRunGroups : nullptr); - if (!Finalized && Opts.LeanAuto) - automateLeanProject(LeanProjectGoals); + const std::set *RunGroups = + LeanFallbackBackend ? &LeanRunGroups : nullptr; + std::vector LeanRefutations; + for (const FunctionRun::Refutation &Pending : Refutations) + if (Pending.Lean) + LeanRefutations.push_back(*Pending.Lean); + llvm::Error Finalized = Lean->writeLeanProjectModules(LeanModules); if (!Finalized) - countLeanAutomation(LeanProjectGoals); + Finalized = Lean->finalizeLeanProject(LeanProjectGoals, RunGroups); + if (!Finalized && LeanFallbackBackend) + Finalized = Lean->writeLeanRefutations(LeanRefutations); + if (!Finalized && Opts.LeanAuto) + 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; @@ -4180,7 +4696,7 @@ class Verifier { "cannot finalize Lean project (" + llvm::toString(std::move(Finalized)) + ")"}); } else if (Opts.LeanCertify && !interruptRequested() && - (!ExportedGoals.empty() || + (!ExportedGoals.empty() || !Refutations.empty() || Opts.LeanFallbackProjectPath.empty())) { // A verdict certification does not make a proof is reported, and // what its vacuity checks found is not. @@ -4205,15 +4721,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]; @@ -4277,6 +4800,11 @@ class Verifier { Diagnostic.Message += " [vacuous]"; } } + + if (Certified) + RefutationChecks = *Certified; + else + RefutationsUnchecked = NotCertified; } } for (const SpecReliance &Check : ProofDependencies) @@ -4805,6 +5333,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) { @@ -4954,6 +5530,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()) @@ -5180,4 +5758,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/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_certifier_first.cpp b/clang/test/Verify/suite/Inputs/lean_certifier_first.cpp new file mode 100644 index 0000000000..29404fc469 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_first.cpp @@ -0,0 +1,11 @@ +int early() + cppverify::post(cppverify::result == 2) +{ + return 1; +} + +int fine() + cppverify::post(cppverify::result == 1) +{ + return 1; +} diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean index 24d917ca90..53b4aee615 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fine_52006a import CppVerify.User theorem cppverify_fine_52006a_missing_return_54ae7c80_proof : cppverify_fine_52006a_missing_return_54ae7c80 := by diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean index 2d440f8a0e..415249b275 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_fine_52006a_postcondition_cd6bdfcd.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fine_52006a import CppVerify.User theorem cppverify_fine_52006a_postcondition_cd6bdfcd_proof : cppverify_fine_52006a_postcondition_cd6bdfcd := by diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean index f7d3d1a1a7..c6061d122c 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_missing_return_54ae7c80_proof : cppverify_one_99bcee_missing_return_54ae7c80 := by diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/first/cppverify_early_103f65_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/first/cppverify_early_103f65_postcondition_646d2761.lean new file mode 100644 index 0000000000..cc38fc4238 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/first/cppverify_early_103f65_postcondition_646d2761.lean @@ -0,0 +1,5 @@ +/- A goal of the same name of its own, true, in the proof of the goal that + comes first, which imports nothing of the project. -/ +def cppverify_early_103f65_postcondition_646d2761 : Prop := True + +theorem cppverify_early_103f65_postcondition_646d2761_proof : cppverify_early_103f65_postcondition_646d2761 := trivial diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean index 823511abad..3ed1c6e593 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/hidden/cppverify_one_99bcee_postcondition_646d2761.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User /- An axiom behind a lemma. -/ diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean index 0897c5c20f..71e1a1f4ad 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/imported/Lemmas.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User import Lean diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean index f5ce026671..ed060924ed 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/rewritten/cppverify_one_99bcee_postcondition_646d2761.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_postcondition_646d2761_proof : True := trivial diff --git a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean index 296d7e4797..0c477a9fa8 100644 --- a/clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean +++ b/clang/test/Verify/suite/Inputs/lean_certifier_proofs/unchecked/cppverify_one_99bcee_postcondition_646d2761.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User import Lean diff --git a/clang/test/Verify/suite/Inputs/lean_collections.cpp b/clang/test/Verify/suite/Inputs/lean_collections.cpp new file mode 100644 index 0000000000..333d61d940 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_collections.cpp @@ -0,0 +1,60 @@ +// Sequences, sets, multisets, and maps in a Lean project, for +// lean_collections.test. +using cppverify::map; +using cppverify::multiset; +using cppverify::seq; +using cppverify::set; + +cppverify::spec int total(seq s) + cppverify::decreases(s.len()) +{ + return s.len() <= 0 ? 0 : total(s.subrange(0, s.len() - 1)) + s[s.len() - 1]; +} + +cppverify::proof void sequences(seq s, int x) +{ + cppverify::check(s.push(x).len() == s.len() + 1); + cppverify::check(s.push(x)[s.len()] == x); + cppverify::check((s + cppverify::seq_of(x)).contains(x)); + cppverify::check(s.subrange(0, s.len()) == s); +} + +cppverify::proof void sets(set a, int x, int y) + cppverify::pre(x != y) +{ + cppverify::check(a.insert(x).remove(y).contains(x)); + cppverify::check(a.subset_of(a.unite(cppverify::set_empty().insert(y)))); +} + +cppverify::proof void multisets(multiset m, int x) +{ + cppverify::check(m.insert(x).count(x) == m.count(x) + 1); + cppverify::check(m.insert(x).remove(x) == m); +} + +cppverify::proof void maps(map m, int k, int v) +{ + cppverify::check(m.insert(k, v)[k] == v); + cppverify::check(!m.remove(k).contains(k)); +} + +cppverify::proof void total_push(seq s, int x) + cppverify::post(total(s.push(x)) == total(s) + x) +{ +} + +cppverify::proof void wrong(set a, int x) +{ + cppverify::check(a.remove(x).contains(x) == a.contains(x)); +} + +cppverify::spec int members(set a, int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : members(a, n - 1) + (a.contains(n) ? 1 : 0); +} + +cppverify::proof void no_members(set a) + cppverify::post(members(a, 0) == 0) +{ +} diff --git a/clang/test/Verify/suite/Inputs/lean_collections_total_push.lean b/clang/test/Verify/suite/Inputs/lean_collections_total_push.lean new file mode 100644 index 0000000000..ee5b58fee6 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_collections_total_push.lean @@ -0,0 +1,13 @@ +import CppVerify.Goals.cppverify_total_push_cdfd2d +import CppVerify.User +import CppVerify.Auto + +theorem cppverify_total_push_cdfd2d_postcondition_3a9fac6f_proof : + cppverify_total_push_cdfd2d_postcondition_3a9fac6f := by + apply cppverify_total_push_cdfd2d_postcondition_3a9fac6f.of_readable + intro _ _ s x pushed _ _ _ + rw [pushed] + unfold cppSpecBody_cdfd2da1_fn_5f5a35746f74616c4e396370707665726966793373657145_1 + have := cppSeqLength_nonneg s + simp [BitVec.toInt_signExtend_of_le] + omega diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean index daf2ade742..6002daa66b 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_division_by_zero_df06c970.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_reading_8d7035 import CppVerify.User theorem cppverify_reading_8d7035_division_by_zero_df06c970_proof : cppverify_reading_8d7035_division_by_zero_df06c970 := by diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean index 7bb7dd4b6b..8a10f2476c 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_reading_8d7035 import CppVerify.User theorem cppverify_reading_8d7035_missing_return_54ae7c80_proof : cppverify_reading_8d7035_missing_return_54ae7c80 := by diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean index 97d154cc3c..b99f29c9e1 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_postcondition_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_reading_8d7035 import CppVerify.User theorem cppverify_reading_8d7035_postcondition_54ae7c80_proof : cppverify_reading_8d7035_postcondition_54ae7c80 := by diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean index d8692c5599..df12dae878 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_155ffe95.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_reading_8d7035 import CppVerify.User theorem cppverify_reading_8d7035_precondition_155ffe95_proof : cppverify_reading_8d7035_precondition_155ffe95 := by diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean index 5779536cb6..589c770d90 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_reading_8d7035_precondition_814bc5b2.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_reading_8d7035 import CppVerify.User theorem cppverify_reading_8d7035_precondition_814bc5b2_proof : cppverify_reading_8d7035_precondition_814bc5b2 := by diff --git a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean index 8e3effb2e7..8d4ca35013 100644 --- a/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean +++ b/clang/test/Verify/suite/Inputs/lean_contract_certify_proofs/cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_sensor_contract_eb6f5c import CppVerify.User theorem cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d_proof : cppverify_sensor_contract_eb6f5c_division_by_zero_d81a153d := by diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean index 391927a090..c2cb31fbe6 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_impossible.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_impossible_9d6c7c import CppVerify.User theorem cppverify_impossible_9d6c7c_postcondition_1cd35301_proof : cppverify_impossible_9d6c7c_postcondition_1cd35301 := by diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean index b07ce3c20e..4a74afae54 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_looping.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_looping_3f4bd4 import CppVerify.User theorem cppverify_looping_3f4bd4_postcondition_d06fccd0_proof : cppverify_looping_3f4bd4_postcondition_d06fccd0 := by diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean index 9df085a719..b6bbaa9d98 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_mixed.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_product_4751c3 import CppVerify.User theorem cppverify_product_4751c3_postcondition_c4d4674b_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean index 4a3c213156..5fd5c25e71 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_positive.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_positive_fb6abf import CppVerify.User theorem cppverify_positive_fb6abf_postcondition_78bdd643_proof : cppverify_positive_fb6abf_postcondition_78bdd643 := by diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean index 5a8320c770..a663e3e6a1 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_same.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_same_9601c2 import CppVerify.User theorem cppverify_same_9601c2_postcondition_ce92acf8_proof : cppverify_same_9601c2_postcondition_ce92acf8 := by diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean index ae71525385..741439d952 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_seven.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_seven_634ea3 import CppVerify.User theorem cppverify_seven_634ea3_postcondition_f0d135e6_proof : cppverify_seven_634ea3_postcondition_f0d135e6 := by diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean index 86ffa0028e..ef58ba38cf 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_termination.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_scaled_decreases_52d363 import CppVerify.User theorem cppverify_scaled_decreases_52d363_termination_3164b050_proof : cppverify_scaled_decreases_52d363_termination_3164b050 := by diff --git a/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean b/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean index 3fd338653d..d075683fb3 100644 --- a/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean +++ b/clang/test/Verify/suite/Inputs/lean_dependencies_trusting.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_trusting_b6301a import CppVerify.User theorem cppverify_trusting_b6301a_postcondition_bafafdfb_proof : cppverify_trusting_b6301a_postcondition_bafafdfb := by diff --git a/clang/test/Verify/suite/Inputs/lean_division.cpp b/clang/test/Verify/suite/Inputs/lean_division.cpp new file mode 100644 index 0000000000..99b3672250 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_division.cpp @@ -0,0 +1,13 @@ +// C++ division and remainder in contracts, for lean_division.test. + +cppverify::proof void half_bound(int a) + cppverify::pre(a >= 4) + cppverify::post(a / 2 >= 2 && a % 2 >= 0) +{ +} + +cppverify::proof void negative_division(int a) + cppverify::pre(a < 0 && a > -100) + cppverify::post(a / 2 <= 0 && a % 3 <= 0) +{ +} diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean index 8ba810ff34..1db8715a34 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_1.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fibo_step_624f01 import CppVerify.User theorem cppverify_fibo_step_624f01_missing_return_ba8abb90_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean index df65b45915..86bfafa577 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_2.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fibo_step_624f01 import CppVerify.User theorem cppverify_fibo_step_624f01_postcondition_559cb60a_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean index 55b9772bad..6ec932841d 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_3.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fibo_six_ec829a import CppVerify.User theorem cppverify_fibo_six_ec829a_missing_return_ba8abb90_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean b/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean index 8ebf102ec4..df78e0c7ec 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_goal_4.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_fibo_six_ec829a import CppVerify.User theorem cppverify_fibo_six_ec829a_postcondition_30cd1b97_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean index aa658e5ebc..9e7048ae1a 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_1.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_bump_ce87d1 import CppVerify.User theorem cppverify_bump_ce87d1_overflow_f5ee4d20_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean index 8d12720c5a..0218241f17 100644 --- a/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean +++ b/clang/test/Verify/suite/Inputs/lean_fallback_partial_goal_2.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_bump_ce87d1 import CppVerify.User theorem cppverify_bump_ce87d1_assertion_06404a7a_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean index 145a149822..acb538820c 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_bump_ce87d1_missing_return_ba8abb90.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_bump_ce87d1 import CppVerify.User theorem cppverify_bump_ce87d1_missing_return_ba8abb90_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean index f9024c9662..9bece241a3 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_missing_return_54ae7c80_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean index eee644659e..58448ce153 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_postcondition_cd6bdfcd_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean index 7f4b99e6d4..1f724407fa 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_cd6bdfcd_2.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_postcondition_cd6bdfcd_2_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean index 5b4dde2b95..b09560a383 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_one_99bcee_postcondition_ebbe6a6a.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_one_99bcee import CppVerify.User theorem cppverify_one_99bcee_postcondition_ebbe6a6a_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean index f3ca2db1f1..8fdce88ad3 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_six_6a2cf3 import CppVerify.User theorem cppverify_six_6a2cf3_missing_return_54ae7c80_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean index 3dae61ac78..0d1c2b271c 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_six_6a2cf3_postcondition_198bc076.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_six_6a2cf3 import CppVerify.User theorem cppverify_six_6a2cf3_postcondition_198bc076_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean index 9f5bed9a7f..05952c73c6 100644 --- a/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean +++ b/clang/test/Verify/suite/Inputs/lean_identity_proofs/cppverify_tri_decreases_f55d4c_termination_3c6bb93f.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_tri_decreases_f55d4c import CppVerify.User theorem cppverify_tri_decreases_f55d4c_termination_3c6bb93f_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_modules.cpp b/clang/test/Verify/suite/Inputs/lean_modules.cpp new file mode 100644 index 0000000000..953d77f17a --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_modules.cpp @@ -0,0 +1,36 @@ +// Five functions for lean_modules.test: inc and dbl, and two that apply the +// recursive spec tri, whose postconditions Inputs/lean_modules_*.lean also +// prove by hand. + +cppverify::spec int tri(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : tri(n - 1) + n; +} + +int inc(int x) + cppverify::pre(0 <= x && x < 1000) + cppverify::post(cppverify::result == x + 1) +{ + return x + 1; +} + +int dbl(int x) + cppverify::pre(0 <= x && x < 1000) + cppverify::post(cppverify::result == 2 * x) +{ + return x + x; +} + +int tri_zero() + cppverify::post(cppverify::result == tri(0)) +{ + return 0; +} + +int plus_tri_zero(int x) + cppverify::pre(0 <= x && x < 1000) + cppverify::post(cppverify::result == x + tri(0)) +{ + return x; +} diff --git a/clang/test/Verify/suite/Inputs/lean_modules_plus_tri_zero.lean b/clang/test/Verify/suite/Inputs/lean_modules_plus_tri_zero.lean new file mode 100644 index 0000000000..2af3414bc0 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_modules_plus_tri_zero.lean @@ -0,0 +1,11 @@ +import CppVerify.Goals.cppverify_plus_tri_zero_10bb8a +import CppVerify.User +import CppVerify.Auto + +theorem cppverify_plus_tri_zero_10bb8a_postcondition_8b45419c_proof : + cppverify_plus_tri_zero_10bb8a_postcondition_8b45419c := by + apply cppverify_plus_tri_zero_10bb8a_postcondition_8b45419c.of_readable + intro __heap_alloc_0 __heap_live_0 __result_1 x_0 tri_0 _ _ h_pre_1 h_null_1 h_null_2 h_result_1 + rw [tri_0] at * + simp only [cppSpecBody_10bb8a86_fn_5f5a3374726969_1] at * + cppverify_auto diff --git a/clang/test/Verify/suite/Inputs/lean_modules_tri_zero.lean b/clang/test/Verify/suite/Inputs/lean_modules_tri_zero.lean new file mode 100644 index 0000000000..03445c1a79 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_modules_tri_zero.lean @@ -0,0 +1,11 @@ +import CppVerify.Goals.cppverify_tri_zero_e086e9 +import CppVerify.User +import CppVerify.Auto + +theorem cppverify_tri_zero_e086e9_postcondition_44e49d34_proof : + cppverify_tri_zero_e086e9_postcondition_44e49d34 := by + apply cppverify_tri_zero_e086e9_postcondition_44e49d34.of_readable + intro __heap_alloc_0 __heap_live_0 __result_1 tri_0 _ _ h_null_1 h_null_2 h_result_1 + rw [tri_0] at * + simp only [cppSpecBody_e086e9ab_fn_5f5a3374726969_1] at * + cppverify_auto diff --git a/clang/test/Verify/suite/Inputs/lean_project_text.py b/clang/test/Verify/suite/Inputs/lean_project_text.py new file mode 100644 index 0000000000..a090df2bd5 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_project_text.py @@ -0,0 +1,11 @@ +"""Prints the generated text of a Lean project: its prelude, its specs, and +each goal module in the order its Generated module imports them, the +functions' source order.""" +import pathlib, sys + +root = pathlib.Path(sys.argv[1]) / "CppVerify" +parts = [root / "Prelude.lean", root / "Specs.lean"] +for line in (root / "Generated.lean").read_text().splitlines(): + if line.startswith("import CppVerify.Goals."): + parts.append(root / "Goals" / (line[len("import CppVerify.Goals."):] + ".lean")) +sys.stdout.write("".join(part.read_text() for part in parts)) diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean index d450f13548..18f468999d 100644 --- a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_missing_return_54ae7c80.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_twice_edf933 import CppVerify.User theorem cppverify_twice_edf933_missing_return_54ae7c80_proof : cppverify_twice_edf933_missing_return_54ae7c80 := by diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean index e1080ebc94..11440c7bf0 100644 --- a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_postcondition_28de726e.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_twice_edf933 import CppVerify.User theorem cppverify_twice_edf933_postcondition_28de726e_proof : cppverify_twice_edf933_postcondition_28de726e := by diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean index 5c6b0e43e4..30d1e5cc82 100644 --- a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_51b3c1f0.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_twice_edf933 import CppVerify.User theorem cppverify_twice_edf933_precondition_51b3c1f0_proof : cppverify_twice_edf933_precondition_51b3c1f0 := by diff --git a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean index 2607fff7eb..9b2059d45a 100644 --- a/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean +++ b/clang/test/Verify/suite/Inputs/lean_readable_proofs/cppverify_twice_edf933_precondition_f0a3d715.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_twice_edf933 import CppVerify.User theorem cppverify_twice_edf933_precondition_f0a3d715_proof : cppverify_twice_edf933_precondition_f0a3d715 := by 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/lean_semantics_call.lean b/clang/test/Verify/suite/Inputs/lean_semantics_call.lean index 8dc0f46fa3..5df905de2c 100644 --- a/clang/test/Verify/suite/Inputs/lean_semantics_call.lean +++ b/clang/test/Verify/suite/Inputs/lean_semantics_call.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_small_74ff94 import CppVerify.User theorem cppverify_small_74ff94_precondition_4e324fa2_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean b/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean index 4c46c601c2..623902f5cf 100644 --- a/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean +++ b/clang/test/Verify/suite/Inputs/lean_semantics_mix.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_mix_b839ab import CppVerify.User theorem cppverify_mix_b839ab_assertion_255467f3_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean b/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean index 5142c33706..96e97fd298 100644 --- a/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean +++ b/clang/test/Verify/suite/Inputs/lean_semantics_numerals.lean @@ -1,3 +1,4 @@ +import CppVerify.Goals.cppverify_difference_465d5b import CppVerify.User theorem cppverify_difference_465d5b_assertion_d7e0e821_proof : diff --git a/clang/test/Verify/suite/Inputs/lean_spec_definitions.cpp b/clang/test/Verify/suite/Inputs/lean_spec_definitions.cpp new file mode 100644 index 0000000000..bf9fbec303 --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_spec_definitions.cpp @@ -0,0 +1,110 @@ +// Spec functions as Lean definitions, for lean_spec_definitions.test. + +cppverify::spec int tri(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : tri(n - 1) + n; +} + +cppverify::spec bool odd(int n); + +cppverify::spec bool even(int n) + cppverify::decreases(n, 1) +{ + return n <= 0 || odd(n - 1); +} + +cppverify::spec bool odd(int n) + cppverify::decreases(n, 0) +{ + return n > 0 && even(n - 1); +} + +cppverify::spec int ack(int m, int n) + cppverify::decreases(m, n) +{ + return m <= 0 ? n + 1 : (n <= 0 ? ack(m - 1, 1) : ack(m - 1, ack(m, n - 1))); +} + +cppverify::spec int half(int n) + cppverify::decreases(n) + cppverify::post(cppverify::result >= 0 && (n <= 1 || cppverify::result < n)) +{ + return n <= 1 ? 0 : half(n - 2) + 1; +} + +// Its measure falls by C++ division. +cppverify::spec int log2(int n) + cppverify::decreases(n) +{ + return n <= 1 ? 0 : log2(n / 2) + 1; +} + +// Its termination rests on the postcondition of half, which Lean does not +// know: it stays opaque. +cppverify::spec int steps(int n) + cppverify::decreases(n) +{ + return n <= 1 ? 0 : steps(half(n)) + 1; +} + +cppverify::proof void tri_nonneg(int n) + cppverify::post(tri(n) >= 0) +{ +} + +cppverify::proof void tri_four() + cppverify::post(tri(4) == 10) +{ +} + +cppverify::proof void even_four() + cppverify::post(even(4) && !odd(4)) +{ +} + +cppverify::proof void small_ack() + cppverify::post(ack(1, 1) == 3) +{ +} + +cppverify::proof void log2_eight() + cppverify::post(log2(8) == 3) +{ +} + +cppverify::proof void steps_one() + cppverify::post(steps(1) == 0) +{ +} + +// Its call may have the measure -1 where the caller's is 0. +cppverify::spec int down(int n) + cppverify::decreases(n) +{ + return n < 0 ? 0 : down(n - 1) + 1; +} + +// It calls steps, which stays opaque: Lean accepts it once steps is. +cppverify::spec int count_steps(int n) + cppverify::decreases(n) +{ + return n <= 0 ? 0 : count_steps(n - 1) + steps(n); +} + +cppverify::proof void down_zero() + cppverify::post(down(0) == 1 && count_steps(0) == 0) +{ +} + +// A call under an existential sees its range. +cppverify::spec bool reaches(int n) + cppverify::decreases(n) +{ + return n <= 0 || cppverify::exists(k, 0, n, reaches(k)); +} + +cppverify::proof void reaches_zero() + cppverify::post(reaches(0)) +{ +} diff --git a/clang/test/Verify/suite/Inputs/lean_spec_definitions_tri_nonneg.lean b/clang/test/Verify/suite/Inputs/lean_spec_definitions_tri_nonneg.lean new file mode 100644 index 0000000000..3e20c0085f --- /dev/null +++ b/clang/test/Verify/suite/Inputs/lean_spec_definitions_tri_nonneg.lean @@ -0,0 +1,15 @@ +import CppVerify.Goals.cppverify_tri_nonneg_42a030 +import CppVerify.User +import CppVerify.Auto + +/-- tri is never negative, by induction over its own recursion. -/ +theorem tri_nonneg (m : Int) : 0 ≤ cppSpec_fn_5f5a3374726969 m := by + induction m using cppSpec_fn_5f5a3374726969.induct with + | case1 x h => rw [cppSpec_fn_5f5a3374726969]; simp [h] + | case2 x h ih => rw [cppSpec_fn_5f5a3374726969]; simp [h]; omega + +theorem cppverify_tri_nonneg_42a030_postcondition_053b1980_proof : + cppverify_tri_nonneg_42a030_postcondition_053b1980 := by + apply cppverify_tri_nonneg_42a030_postcondition_053b1980.of_readable + intro _ _ n _ _ _ + exact tri_nonneg _ 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("