verify: Verify records through references, as pointers never null or reseated

clang/lib/Verify/Backend/Certify.cpp

@@ -4150,6 +4150,22 @@ void sourceVariables(const LogicExpr *Expr, std::set<std::string> &Bound,
 }
 } // namespace
 
+std::shared_ptr<const CounterexampleAssignment>
+verify::counterexampleAssignment(const Obligation &Item,
+                                 CandidateModel &Model) {
+  std::vector<std::pair<std::string, LogicSort>> Variables;
+  std::set<std::string> Bound;
+  sourceVariables(Item.Goal.get(), Bound, Variables);
+  auto Assignment = std::make_shared<CounterexampleAssignment>();
+  for (const auto &[Name, Sort] : Variables) {
+    std::optional<LogicValue> Given = Model.constant(Name, Sort);
+    if (!Given)
+      return nullptr;
+    Assignment->Values.emplace(Name, std::move(*Given));
+  }
+  return Assignment;
+}
+
 std::vector<VerifyModelValue>
 verify::candidateValues(const ObligationModule &Module, const LogicExpr &Query,
                         CandidateModel &Model) {

clang/lib/Verify/Backend/Certify.h

@@ -232,6 +232,18 @@ std::optional<LogicValue> 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<std::string, LogicValue> 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<const CounterexampleAssignment>
+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<VerifyModelValue> candidateValues(const ObligationModule &Module,

clang/lib/Verify/Backend/LeanBackend.cpp

@@ -1,5 +1,6 @@
 //===--- LeanBackend.cpp --------------------------------------------------===//
 #include "LeanBackend.h"
+#include "Certify.h"
 #include "ObligationSerialization.h"
 #include "llvm/ADT/STLExtras.h"
 #include "llvm/ADT/SmallString.h"
@@ -1293,6 +1294,41 @@ static std::string leanSpecDefinition(const ObligationModule &Module,
   return Failed ? "" : Text;
 }
 
+// A quantifier over a range of integers, as a goal states one, is decided by
+// trying each integer of the range, as core Lean decides one over a range of
+// naturals, when the range has at most 4096 integers, as many as the
+// certifier expands (CertifyLimits::DirectExpansion). Each integer is a level
+// of recursion whose memory heartbeats do not count: under the generated
+// files' recursion depth a range of 64000 took 58 GB before failing, and one
+// of 4000 already spent a step's heartbeats. A larger range has the classical
+// instance, which decide cannot evaluate.
+static constexpr llvm::StringLiteral LeanBoundedQuantifierPrelude =
+    R"lean(instance cppIntBallDecidable (lo hi : Int) (p : Int → Prop) [DecidablePred p] :
+    Decidable (∀ x : Int, lo ≤ x ∧ x < hi → p x) :=
+  if (hi - lo).toNat ≤ 4096 then
+    decidable_of_iff (∀ k : Nat, k < (hi - lo).toNat → p (lo + k)) (by
+      constructor
+      · intro h x hx
+        have := h (x - lo).toNat (by omega)
+        rwa [show lo + ((x - lo).toNat : Int) = x by omega] at this
+      · intro h k hk
+        exact h _ ⟨by omega, by omega⟩)
+  else Classical.propDecidable _
+
+instance cppIntBexDecidable (lo hi : Int) (p : Int → Prop) [DecidablePred p] :
+    Decidable (∃ x : Int, lo ≤ x ∧ x < hi ∧ p x) :=
+  if (hi - lo).toNat ≤ 4096 then
+    decidable_of_iff (∃ k : Nat, k < (hi - lo).toNat ∧ p (lo + k)) (by
+      constructor
+      · rintro ⟨k, hk, hp⟩
+        exact ⟨lo + k, by omega, by omega, hp⟩
+      · rintro ⟨x, h1, h2, hp⟩
+        refine ⟨(x - lo).toNat, by omega, ?_⟩
+        rwa [show lo + ((x - lo).toNat : Int) = x by omega])
+  else Classical.propDecidable _
+
+)lean";
+
 static void emitLeanFunctionDeclarations(
     const ObligationModule &Module, llvm::raw_ostream &OS,
     std::set<std::string> &EmittedFunctions,
@@ -1680,6 +1716,7 @@ void verify::emitLeanPrelude(llvm::raw_ostream &OS, bool Project) {
   OS << "    if (x < 0) ≠ (y < 0) then -q else q\n";
   OS << "def cppIntRem (x y : Int) : Int :=\n";
   OS << "  if y = 0 then x else x - cppIntDiv x y * y\n\n";
+  OS << LeanBoundedQuantifierPrelude;
   OS << LeanCollectionPrelude;
   OS << "/- Proves that an application in a spec's definition lowers its "
         "measure. -/\n";
@@ -1704,6 +1741,77 @@ void verify::emitLeanPrelude(llvm::raw_ostream &OS, bool Project) {
   }
 }
 
+// A piecewise-constant function of the integers as a Lean term: the cell
+// of each address, from the run it lies in.
+static void printLeanRuns(const HeapValue &Runs, llvm::StringRef Before,
+                          llvm::StringRef After, llvm::raw_ostream &OS) {
+  OS << "(fun (a : Int) => ";
+  for (auto It = Runs.Breaks.rbegin(); It != Runs.Breaks.rend(); ++It)
+    OS << "if a ≥ (" << It->first.toDecimal() << " : Int) then " << Before
+       << It->second.toDecimal() << After << " else ";
+  OS << Before << Runs.Default.toDecimal() << After << ")";
+}
+
+// A model's value as a Lean term of its sort; false when it has none.
+static bool printLeanValue(const LogicValue &Value, const LogicSort &Sort,
+                           llvm::raw_ostream &OS) {
+  switch (Sort.Kind) {
+  case LogicSortKind::Bool:
+    if (Value.K != LogicValue::Kind::Bool)
+      return false;
+    OS << (Value.Truth ? "True" : "False");
+    return true;
+  case LogicSortKind::MathematicalInteger:
+  case LogicSortKind::Pointer:
+    if (Value.K != LogicValue::Kind::Integer)
+      return false;
+    OS << "(" << Value.Integer.toDecimal() << " : Int)";
+    return true;
+  case LogicSortKind::BitVector:
+    if (Value.K != LogicValue::Kind::Integer)
+      return false;
+    OS << "(BitVec.ofInt " << Sort.BitWidth << " (" << Value.Integer.toDecimal()
+       << "))";
+    return true;
+  case LogicSortKind::Heap:
+    if (Value.K != LogicValue::Kind::Heap || !Value.Heap)
+      return false;
+    printLeanRuns(*Value.Heap, "(", " : Int)", OS);
+    return true;
+  case LogicSortKind::Seq:
+    if (Value.K != LogicValue::Kind::Seq || !Value.Elements)
+      return false;
+    OS << "([";
+    for (size_t I = 0; I != Value.Elements->size(); ++I)
+      OS << (I ? ", " : "") << "(" << (*Value.Elements)[I].toDecimal()
+         << " : Int)";
+    OS << "] : List Int)";
+    return true;
+  case LogicSortKind::Set:
+    if (Value.K != LogicValue::Kind::Set || !Value.Heap)
+      return false;
+    printLeanRuns(*Value.Heap, "decide ((", " : Int) ≠ 0)", OS);
+    return true;
+  case LogicSortKind::Multiset:
+    if (Value.K != LogicValue::Kind::Multiset || !Value.Heap)
+      return false;
+    printLeanRuns(*Value.Heap, "((", " : Int).toNat)", OS);
+    return true;
+  case LogicSortKind::Map:
+    if (Value.K != LogicValue::Kind::Map || !Value.Heap || !Value.Values)
+      return false;
+    OS << "(fun (k : Int) => if ";
+    printLeanRuns(*Value.Heap, "(", " : Int)", OS);
+    OS << " k ≠ 0 then some (";
+    printLeanRuns(*Value.Values, "(", " : Int)", OS);
+    OS << " k) else none)";
+    return true;
+  case LogicSortKind::Invalid:
+    return false;
+  }
+  return false;
+}
+
 VerifyResult verify::exportLeanScratchPad(
     const ObligationModule &Module, llvm::raw_ostream &OS, bool EmitPreamble,
     std::set<std::string> &EmittedFunctions,
@@ -1757,7 +1865,13 @@ VerifyResult verify::exportLeanScratchPad(
   printLeanCommentText(Module.FunctionName, OS);
   OS << " -/\n";
   OS << "/- required logic: " << formatLogicFeatures(Module.RequiredFeatures)
-     << " -/\n\n";
+     << " -/\n";
+  if (Module.BMCTransform)
+    OS << "/- bound: " << Module.BMCTransform->UnrollBound
+       << " loop iterations, by unrolling: these goals speak only of the\n"
+          "   executions within them, and an unwinding goal says that every "
+          "loop\n   ends within them -/\n";
+  OS << "\n";
 
   std::string TheoremName =
       "cppverify_" +
@@ -1805,6 +1919,7 @@ VerifyResult verify::exportLeanScratchPad(
       Goal.LegacyName = encodeLeanName(ObligationName + "_goal");
       Goal.LegacyBodyPrefix = LegacyBodyPrefix;
       Goal.Exported = Selected;
+      Goal.Unwinding = Item.Kind == ObligationKind::Unwinding;
       if (!Selected) {
         ProjectGoals->push_back(std::move(Goal));
         continue;
@@ -1847,4 +1962,60 @@ VerifyResult verify::exportLeanScratchPad(
   Result.Message = ProjectGoals ? "editable Lean project obligation export"
                                 : "unchecked Lean obligation export";
   return Result;
+}
+
+std::optional<LeanRefutation> verify::exportLeanRefutation(
+    const ObligationModule &Module, const Obligation &Item,
+    const CounterexampleAssignment &Assignment,
+    std::map<std::string, LeanSpecDeclaration> &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<std::string> Functions, Theorems;
+  std::vector<LeanProjectGoal> Stated;
+  const std::set<std::string> 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<std::string, LogicSort> 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;
 }

clang/lib/Verify/Backend/LeanBackend.h

@@ -35,6 +35,9 @@ struct LeanProjectGoal {
   /// False for an obligation of an exported function that a selection left
   /// to the solver: its goal is known, but has no definition or proof file.
   bool Exported = true;
+  /// An unwinding goal of a bounded module: that its loops end within the
+  /// bound.
+  bool Unwinding = false;
 };
 
 /// The group of a module's goals in a project: its function's directory.
@@ -78,6 +81,26 @@ VerifyResult exportLeanScratchPad(
     const std::set<std::string> *Selection = nullptr,
     std::map<std::string, LeanSpecDeclaration> *Specs = nullptr);
 
+/// A certified counterexample shown in Lean: a module of the project's
+/// group directory, Refutations/<Group>/<Goal>.lean, that states the goal as
+/// the project would and proves `<Goal>_refuted : ¬ <Goal>` 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<LeanRefutation>
+exportLeanRefutation(const ObligationModule &Module, const Obligation &Item,
+                     const CounterexampleAssignment &Assignment,
+                     std::map<std::string, LeanSpecDeclaration> &Specs,
+                     std::string &Why);
+
 class LeanVerifyBackend : public VerifyBackend {
   llvm::raw_ostream *Out = nullptr;
   LeanProjectModules *Modules = nullptr;

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;
 }

clang/lib/Verify/Backend/Obligation.h

@@ -230,7 +230,8 @@ class LogicExpr : public llvm::ThreadSafeRefCountedBase<LogicExpr> {
   std::vector<LogicExprRef> 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<std::unique_ptr<LogicExpr>> 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<std::unique_ptr<LogicExpr>> Decreases;
   static constexpr const char *ResultVariable = "cppverify.result";
 };