E4b: --max-failures, each failure past the failing checks before it

clang/lib/Verify/Backend/VerifyBackend.cpp

@@ -614,6 +614,9 @@ VerifyResult VerifyBackend::verifyDirect(const ObligationModule &Module) {
   VerifyResult Result = verifyModule(Module);
   if (Result.BackendName.empty())
     Result.BackendName = getName().str();
+  for (VerifyResult &More : Result.MoreFailures)
+    if (More.BackendName.empty())
+      More.BackendName = Result.BackendName;
   if (!Capabilities.ProducesVerificationVerdict &&
       Result.Status != VerifyStatus::Exported &&
       Result.Status != VerifyStatus::Unresolved) {

clang/lib/Verify/Backend/VerifyBackend.h

@@ -146,6 +146,9 @@ struct VerifyResult {
   std::string Message;
   std::vector<VerifyModelValue> Model;
   std::vector<VerifyTraceEvent> Trace;
+  /// The failing obligations after this one, in order, each with its own
+  /// counterexample, as many as the run's MaxFailures allows.
+  std::vector<VerifyResult> MoreFailures;
   std::string ObligationId;
   std::optional<ObligationKind> ObligationType;
   /// For a certified counterexample: the value of every free variable of the
@@ -287,6 +290,9 @@ struct BackendExecutionOptions {
   /// unresolved. Interactive fallback backends can consume those unresolved
   /// obligations without spending a second whole-module timeout budget.
   bool SkipWholeModuleRetry = false;
+  /// How many failing obligations of a module are reported, each with its
+  /// own counterexample; 0 reports every one.
+  unsigned MaxFailures = 1;
   /// Solve the whole-module query once, at the full budget, and report it:
   /// no per-obligation queries, refinement fallback, or induction. For small
   /// auxiliary questions such as the vacuity checks.

clang/lib/Verify/Backend/Z3Encode.cpp

@@ -3595,8 +3595,8 @@ static VerifyResult finishZ3Result(VerifyResult Result) {
 
 std::vector<VerifyResult>
 Z3VerifyBackend::verifyObligations(const ObligationModule &Module,
-                                   bool StopAtFailure, Race *Racing,
-                                   unsigned TimeoutCapMs) {
+                                   std::optional<unsigned> ReportedFailures,
+                                   Race *Racing, unsigned TimeoutCapMs) {
   TimeoutMs =
       budget(moduleTimeoutMs(Module, SolverTimeoutMs, CollectionTimeoutMs));
   if (TimeoutCapMs != 0)
@@ -3626,13 +3626,31 @@ Z3VerifyBackend::verifyObligations(const ObligationModule &Module,
   auto IsReused = [&](size_t I) {
     return ReuseVerifiedQueries && VerifiedQueries.count(QueryHashes[I]) != 0;
   };
+  // When failures are reported, each obligation after the first failure is
+  // solved in the executions that pass every earlier one that fails, as
+  // Boogie assumes an assertion after checking it: alone, its counterexample
+  // could start where an earlier check already fails, and fixing that one
+  // would remove it. A check not settled is not assumed, so a proof past
+  // the failures rests on no check that may not hold.
+  const unsigned StopAfterFailures = ReportedFailures.value_or(0);
+  std::vector<size_t> Failing;
+  std::vector<bool> PastEarlier(Module.Obligations.size());
   if (Jobs == 1 || Module.Obligations.size() < 2) {
+    unsigned Failures = 0;
     for (size_t I = 0; I != Module.Obligations.size(); ++I) {
-      Results.push_back(verifyObligation(
-          Module, Module.Obligations[I],
-          Cache ? llvm::StringRef(CacheHashes[I]) : llvm::StringRef(),
-          Cache ? &CacheLookups[I] : nullptr, IsReused(I), Racing));
-      if (StopAtFailure && Results.back().Status == VerifyStatus::Failed)
+      PastEarlier[I] = ReportedFailures && Failures != 0;
+      Results.push_back(
+          PastEarlier[I]
+              ? verifyPastEarlier(Module, I, Failing, Racing)
+              : verifyObligation(Module, Module.Obligations[I],
+                                 Cache ? llvm::StringRef(CacheHashes[I])
+                                       : llvm::StringRef(),
+                                 Cache ? &CacheLookups[I] : nullptr,
+                                 IsReused(I), Racing));
+      if (Results.back().Status != VerifyStatus::Failed)
+        continue;
+      Failing.push_back(I);
+      if (++Failures == StopAfterFailures)
         break;
     }
   } else {
@@ -3656,10 +3674,26 @@ Z3VerifyBackend::verifyObligations(const ObligationModule &Module,
     Group.wait();
     for (std::shared_future<VerifyResult> &Future : Futures)
       Results.push_back(Future.get());
+    // A failure after the first is solved again past the earlier checks; a
+    // proof or an unresolved result stays one there.
+    unsigned Failures = 0;
+    for (size_t I = 0;
+         ReportedFailures && I != Results.size() &&
+         (StopAfterFailures == 0 || Failures < StopAfterFailures);
+         ++I) {
+      if (Failures != 0 && Results[I].Status == VerifyStatus::Failed) {
+        PastEarlier[I] = true;
+        Results[I] = verifyPastEarlier(Module, I, Failing, Racing);
+      }
+      if (Results[I].Status == VerifyStatus::Failed) {
+        Failing.push_back(I);
+        ++Failures;
+      }
+    }
   }
   if (ReuseVerifiedQueries)
     for (size_t I = 0; I != Results.size(); ++I)
-      if (Results[I].Status == VerifyStatus::Verified)
+      if (Results[I].Status == VerifyStatus::Verified && !PastEarlier[I])
         VerifiedQueries.insert(QueryHashes[I]);
   return Results;
 }
@@ -3671,7 +3705,8 @@ Z3VerifyBackend::Z3VerifyBackend(const BackendExecutionOptions &Execution,
       SolverTimeoutMs(Execution.SolverTimeoutMs),
       CollectionTimeoutMs(Execution.CollectionTimeoutMs),
       ResourceLimit(Execution.SolverResourceLimit), Jobs(Execution.Jobs),
-      Pool(Execution.Pool), MaxQueryNodes(Execution.MaxQueryNodes),
+      MaxFailures(Execution.MaxFailures), Pool(Execution.Pool),
+      MaxQueryNodes(Execution.MaxQueryNodes),
       IntegerEncoding(Execution.IntegerEncoding),
       SkipWholeModuleRetry(Execution.SkipWholeModuleRetry),
       SingleQuery(Execution.SingleQuery),
@@ -3789,6 +3824,18 @@ VerifyResult Z3VerifyBackend::solveQuery(
   return WithFacts;
 }
 
+/// \p Result as the result of obligation \p Item.
+static VerifyResult attributed(VerifyResult Result, const Obligation &Item) {
+  Result.ObligationId = Item.StableId.empty() ? Item.Id : Item.StableId;
+  Result.ObligationType = Item.Kind;
+  Result.Location = Item.Loc;
+  Result.Source = Item.Source;
+  if (Result.Status == VerifyStatus::Unresolved)
+    Result.Message = "proof obligation " + Result.ObligationId +
+                     (Result.Message.empty() ? "" : ": " + Result.Message);
+  return finishZ3Result(std::move(Result));
+}
+
 VerifyResult Z3VerifyBackend::verifyObligation(const ObligationModule &Module,
                                                const Obligation &Item,
                                                llvm::StringRef SemanticHash,
@@ -3836,14 +3883,31 @@ VerifyResult Z3VerifyBackend::verifyObligation(const ObligationModule &Module,
     }
   }
 
-  Result.ObligationId = Item.StableId.empty() ? Item.Id : Item.StableId;
-  Result.ObligationType = Item.Kind;
-  Result.Location = Item.Loc;
-  Result.Source = Item.Source;
-  if (Result.Status == VerifyStatus::Unresolved)
-    Result.Message = "proof obligation " + Result.ObligationId +
-                     (Result.Message.empty() ? "" : ": " + Result.Message);
-  return finishZ3Result(std::move(Result));
+  return attributed(std::move(Result), Item);
+}
+
+VerifyResult
+Z3VerifyBackend::verifyPastEarlier(const ObligationModule &Module, size_t I,
+                                   const std::vector<size_t> &Earlier,
+                                   Race *Racing) {
+  const Obligation &Item = Module.Obligations[I];
+  auto Query = cloneLogicExpr(Item.CounterexampleQuery.get());
+  for (size_t J : Earlier) {
+    auto Conjunction = std::make_unique<LogicExpr>(LogicExpr::And);
+    Conjunction->Sort = LogicSort::boolSort();
+    Conjunction->Loc = Query->Loc;
+    Conjunction->EndLoc = Query->EndLoc;
+    Conjunction->Source = Query->Source;
+    Conjunction->Children.push_back(std::move(Query));
+    Conjunction->Children.push_back(
+        cloneLogicExpr(Module.Obligations[J].Goal.get()));
+    Query = std::move(Conjunction);
+  }
+  return attributed(spent() ? timeSpent()
+                            : solveQuery(Module, Query.get(),
+                                         Item.TraceEventCount,
+                                         budget(TimeoutMs), Racing),
+                    Item);
 }
 
 /// Internal IDs of the obligations that one-to-one Results did not prove.
@@ -3859,6 +3923,17 @@ unprovedObligations(const ObligationModule &Module,
   return Unproved;
 }
 
+VerifyResult
+Z3VerifyBackend::withMoreFailures(std::vector<VerifyResult> &Results,
+                                  size_t First) {
+  VerifyResult Reported = std::move(Results[First]);
+  for (size_t I = First + 1; I != Results.size(); ++I)
+    if (Results[I].Status == VerifyStatus::Failed &&
+        (MaxFailures == 0 || Reported.MoreFailures.size() + 1 < MaxFailures))
+      Reported.MoreFailures.push_back(std::move(Results[I]));
+  return Reported;
+}
+
 VerifyResult Z3VerifyBackend::verifyModule(const ObligationModule &Module) {
   TimeoutMs =
       budget(moduleTimeoutMs(Module, SolverTimeoutMs, CollectionTimeoutMs));
@@ -4014,7 +4089,7 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) {
     Group.emplace(*Pool);
     Ordered = Group->async([this, &Module, &Rivals, &WholeRace] {
       std::vector<VerifyResult> Results =
-          verifyObligations(Module, /*StopAtFailure=*/true, &Rivals);
+          verifyObligations(Module, MaxFailures, &Rivals);
       // The obligations settle the module when they prove all of it or one
       // fails, and the whole query, or its retry, is then stopped.
       if (llvm::any_of(Results,
@@ -4070,8 +4145,7 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) {
   if (Whole.Status == VerifyStatus::Verified)
     return finishZ3Result(std::move(Whole));
   auto orderedResults = [&] {
-    return Racing ? Ordered.get()
-                  : verifyObligations(Module, /*StopAtFailure=*/true);
+    return Racing ? Ordered.get() : verifyObligations(Module, MaxFailures);
   };
 
   if (Whole.Status == VerifyStatus::Failed) {
@@ -4084,18 +4158,18 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) {
       TimeoutMs = FullTimeout;
       UnitsCap = 0;
     });
-    std::vector<VerifyResult> Results = verifyObligations(
-        Module, /*StopAtFailure=*/true, nullptr, WholeTimeout);
+    std::vector<VerifyResult> Results =
+        verifyObligations(Module, MaxFailures, nullptr, WholeTimeout);
     bool SawUnresolved = false;
-    for (VerifyResult &Result : Results) {
-      if (Result.Status == VerifyStatus::Verified)
+    for (size_t I = 0; I != Results.size(); ++I) {
+      if (Results[I].Status == VerifyStatus::Verified)
         continue;
-      if (Result.Status == VerifyStatus::Unresolved) {
+      if (Results[I].Status == VerifyStatus::Unresolved) {
         SawUnresolved = true;
         continue;
       }
-      if (Result.Status == VerifyStatus::Failed)
-        return std::move(Result);
+      if (Results[I].Status == VerifyStatus::Failed)
+        return withMoreFailures(Results, I);
     }
     if (SawUnresolved)
       return finishZ3Result(std::move(Whole));
@@ -4122,13 +4196,16 @@ Z3VerifyBackend::verifyModuleDirect(const ObligationModule &Module) {
   std::optional<std::vector<std::string>> Unproved =
       unprovedObligations(Module, Results);
   std::optional<VerifyResult> FirstUnresolved;
-  for (VerifyResult &Result : Results) {
+  for (size_t I = 0; I != Results.size(); ++I) {
+    VerifyResult &Result = Results[I];
     if (Result.Status != VerifyStatus::Verified) {
       if (Result.Status == VerifyStatus::Unresolved) {
         if (!FirstUnresolved)
           FirstUnresolved = std::move(Result);
         continue;
       }
+      if (Result.Status == VerifyStatus::Failed)
+        return withMoreFailures(Results, I);
       return std::move(Result);
     }
   }

clang/lib/Verify/Backend/Z3Encode.h

@@ -333,6 +333,8 @@ class Z3VerifyBackend : public VerifyBackend {
   /// of their queries may do: the work the complete query's probe had, or 0.
   unsigned UnitsCap = 0;
   unsigned Jobs;
+  /// How many failing obligations a module reports; 0: every one.
+  unsigned MaxFailures;
   llvm::StdThreadPool *Pool;
   uint64_t MaxQueryNodes;
   MachineIntegerEncoding IntegerEncoding;
@@ -345,6 +347,10 @@ class Z3VerifyBackend : public VerifyBackend {
 
   std::optional<std::chrono::steady_clock::time_point> Deadline;
   unsigned budget(unsigned Ms) const { return withinDeadline(Ms, Deadline); }
+  /// The failure at First of the results of verifyObligations, carrying the
+  /// failures after it, as many as MaxFailures allows.
+  VerifyResult withMoreFailures(std::vector<VerifyResult> &Results,
+                                size_t First);
   /// The function's time is spent, so no further query starts.
   bool spent() const {
     return Cancellation.Cancelled ||
@@ -381,6 +387,12 @@ class Z3VerifyBackend : public VerifyBackend {
                                 llvm::StringRef SemanticHash = {},
                                 const ProofCacheLookup *Lookup = nullptr,
                                 bool Reused = false, Race *Racing = nullptr);
+  /// Obligation \p I of \p Module in the executions that pass every one of
+  /// \p Earlier, failing obligations before it. No cache holds it, since it
+  /// asks less than the obligation.
+  VerifyResult verifyPastEarlier(const ObligationModule &Module, size_t I,
+                                 const std::vector<size_t> &Earlier,
+                                 Race *Racing);
 
 public:
   explicit Z3VerifyBackend(const BackendExecutionOptions &Execution = {},
@@ -390,13 +402,15 @@ class Z3VerifyBackend : public VerifyBackend {
   BackendCapabilities getCapabilities() const override {
     return {allLogicFeatures(), true};
   }
-  /// One result per obligation in order. With StopAtFailure a serial run ends
-  /// after the first failure, since later results cannot change it. A nonzero
-  /// TimeoutCapMs bounds every query's timeout.
-  std::vector<VerifyResult> verifyObligations(const ObligationModule &Module,
-                                              bool StopAtFailure = false,
-                                              Race *Racing = nullptr,
-                                              unsigned TimeoutCapMs = 0);
+  /// One result per obligation in order, each solved alone. With
+  /// ReportedFailures, a serial run ends after that many failures (0: never),
+  /// since later results are not reported, and each obligation after the
+  /// first failure is solved in the executions that pass every earlier one
+  /// that fails. A nonzero TimeoutCapMs bounds every query's timeout.
+  std::vector<VerifyResult>
+  verifyObligations(const ObligationModule &Module,
+                    std::optional<unsigned> ReportedFailures = std::nullopt,
+                    Race *Racing = nullptr, unsigned TimeoutCapMs = 0);
   void cancel() override { Cancellation.cancel(); }
   void resume() override { Cancellation.reset(); }
   std::optional<unsigned>