E5b: --function, with the verdicts of a whole run

clang/lib/Verify/Driver/Verifier.cpp

@@ -13,6 +13,7 @@
 #include "../Backend/ProofCache.h"
 #include "../Backend/SpecAxioms.h"
 #include "../Backend/TaskGroup.h"
+#include "../Backend/Z3Encode.h"
 #include "../Frontend/ASTConverter.h"
 #include "../IR/VStmt.h"
 #include "../Transform/LoopUnroll.h"
@@ -37,6 +38,7 @@
 #include "llvm/Support/Error.h"
 #include "llvm/Support/FileSystem.h"
 #include "llvm/Support/FormatVariadic.h"
+#include "llvm/Support/GlobPattern.h"
 #include "llvm/Support/JSON.h"
 #include "llvm/Support/MD5.h"
 #include "llvm/Support/MathExtras.h"
@@ -1101,6 +1103,8 @@ struct VerifyDiagnostic {
   SourceRange Span;
   /// A spec function that needs no check, listed with --verbose: no verdict.
   bool Axiom = false;
+  /// What else the verifier found about the verdict, each printed as a note.
+  std::vector<std::string> Notes;
 };
 
 /// The backend a lowering reports, as lower-only names it.
@@ -3133,6 +3137,24 @@ class Verifier {
     // the function is Unresolved, its first error carrying the verdict, and
     // the rest of the translation unit is verified. An error outside every
     // function stops the run.
+    // --function: the functions the run reports, by their names.
+    std::vector<llvm::GlobPattern> Patterns;
+    for (const std::string &Text : Opts.FunctionPatterns) {
+      auto Pattern = llvm::GlobPattern::create(Text);
+      if (!Pattern) {
+        Diags.push_back(
+            {VerifyDiagnostic::Error, "--function=" + Text + ": " +
+                                          llvm::toString(Pattern.takeError())});
+        return false;
+      }
+      Patterns.push_back(std::move(*Pattern));
+    }
+    auto selects = [&](llvm::StringRef Name) {
+      return Patterns.empty() ||
+             llvm::any_of(Patterns, [&](const llvm::GlobPattern &Pattern) {
+               return Pattern.match(Name);
+             });
+    };
     bool OutsideFunctions = false;
     std::map<std::string, std::string> UnsupportedConstructs;
     for (const ConversionError &Err : Converter.getErrors()) {
@@ -3143,6 +3165,7 @@ class Verifier {
         OutsideFunctions = true;
       else
         D.FunctionName = Err.FunctionName;
+      D.Hidden = !Err.Function.empty() && !selects(Err.FunctionName);
       if (!Err.Function.empty() &&
           UnsupportedConstructs.emplace(Err.Function, Err.Message).second) {
         VerifyResult R;
@@ -3168,10 +3191,37 @@ class Verifier {
           {VerifyDiagnostic::Warning, "no verifiable functions found"});
       return true;
     }
+    // A function is selected by the name its verdicts print, which for an
+    // inductive predicate's step is the predicate's; the predicate's rule
+    // proofs are reported with it.
+    std::vector<bool> Selected(Functions.size());
+    for (size_t I = 0; I != Functions.size(); ++I) {
+      const VFunction &Fn = *Functions[I];
+      Selected[I] =
+          selects(Fn.InductiveStepOf.empty() ? Fn.Name : Fn.InductiveStepOf);
+    }
+    std::set<std::string> SelectedIdentities;
+    for (size_t I = 0; I != Functions.size(); ++I)
+      if (Selected[I])
+        SelectedIdentities.insert(Functions[I]->Identity);
+    for (size_t I = 0; I != Functions.size(); ++I)
+      Selected[I] = Selected[I] ||
+                    SelectedIdentities.count(Functions[I]->InductiveRuleOf);
+    if (!Patterns.empty() &&
+        llvm::none_of(Selected, [](bool S) { return S; }) &&
+        llvm::none_of(Converter.getErrors(), [&](const ConversionError &Err) {
+          return !Err.Function.empty() && selects(Err.FunctionName);
+        })) {
+      Diags.push_back({VerifyDiagnostic::Error,
+                       "no function matches --function=" +
+                           llvm::join(Opts.FunctionPatterns, ", --function=")});
+      return false;
+    }
     if (Opts.ListFunctions) {
-      for (const auto &Fn : Functions) {
+      for (size_t I = 0; I != Functions.size(); ++I) {
+        const auto &Fn = Functions[I];
         if (Fn->IsBuiltin || Fn->IsChoice || !Fn->InductiveStepOf.empty() ||
-            !Fn->InductiveRuleOf.empty())
+            !Fn->InductiveRuleOf.empty() || !Selected[I])
           continue;
         const char *Kind = Fn->IsConstexprSpec ? "constexpr spec"
                            : Fn->IsSpec        ? "spec"
@@ -3502,6 +3552,132 @@ class Verifier {
       }
       auto SmokeBackend = createVerifyBackend(BackendKind::Z3, nullptr, 0,
                                               SmokeExecution, nullptr);
+      // What else a failure shows. A counterexample that passes through a
+      // loop starts from any state the loop's invariants allow, which no
+      // execution need reach; unrolling the loops looks for an execution
+      // that fails, or proves that none does.
+      auto failureNotes = [&](const VFunction &F, const VerifyResult &Failure) {
+        std::vector<std::string> Notes;
+        auto at = [&](SourceLocation Loc) {
+          const PresumedLoc Where = Ctx.getSourceManager().getPresumedLoc(Loc);
+          return Where.isValid() ? std::to_string(Where.getLine()) + ":" +
+                                       std::to_string(Where.getColumn())
+                                 : std::string("?");
+        };
+        if (F.UnmeasuredLoop.isValid())
+          Notes.push_back("the loop at " + at(F.UnmeasuredLoop) +
+                          " has no cppverify::decreases: a proof would be "
+                          "Unresolved (decreases.missing) until it has one");
+        const auto Loop = llvm::find_if(Failure.Trace, [](const auto &Event) {
+          return Event.Kind == DiagnosticTraceKind::Loop &&
+                 Event.Active.value_or(false);
+        });
+        if (Loop == Failure.Trace.end() || !isDeductiveBackend(Opts.Backend) ||
+            Failure.Reason != VerifyReason::Counterexample)
+          return Notes;
+        Notes.push_back(
+            "the counterexample's state at the loop at " +
+            (Loop->Source.isValid() ? std::to_string(Loop->Source.Line) + ":" +
+                                          std::to_string(Loop->Source.Column)
+                                    : std::string("?")) +
+            " is any state its invariants allow, not necessarily one an "
+            "execution reaches");
+        if (Opts.ConfirmBound == 0 || !Failure.ObligationType)
+          return Notes;
+        VFunction Bounded = cloneVFunction(F);
+        annotatePointerOrigins(Bounded);
+        if (Opts.CheckUB && !F.TotalExpressions && instrumentUBChecks(Bounded))
+          return Notes;
+        SpecInliner(FnMap, Bounded.SpecFuel).prepareFunction(Bounded);
+        // The search after a failure takes at most one query's time.
+        Z3VerifyBackend Unroller(Execution, "bmc");
+        std::optional<std::chrono::steady_clock::time_point> Until = Deadline;
+        if (Opts.SolverTimeoutMs != 0) {
+          const auto Slice = std::chrono::steady_clock::now() +
+                             std::chrono::milliseconds(Opts.SolverTimeoutMs);
+          if (!Until || Slice < *Until)
+            Until = Slice;
+        }
+        Unroller.setDeadline(Until);
+        auto iterations = [](unsigned Bound) {
+          return std::to_string(Bound) +
+                 (Bound == 1 ? " iteration" : " iterations");
+        };
+        // Unrolling keeps the function's checks, each copied into every
+        // iteration it is in, but not the loops' invariants and measures:
+        // the copies of the failed check are those of its kind at its place.
+        auto copyOfFailure = [&](const VerifyResult &Result) {
+          return Result.ObligationType == Failure.ObligationType &&
+                 Result.Source.Line == Failure.Source.Line &&
+                 Result.Source.Column == Failure.Source.Column &&
+                 Result.Source.File == Failure.Source.File;
+        };
+        bool Unrolled = false;
+        for (unsigned Bound = 0; Bound <= Opts.ConfirmBound; ++Bound) {
+          VFunction Copy = LoopUnroller::unroll(Bounded, Bound);
+          Passivizer Unrolling;
+          Unrolling.setFunctionMap(InterfaceMap);
+          auto Lowered = buildObligationModule(Unrolling.run(Copy));
+          if (!Lowered) {
+            llvm::consumeError(Lowered.takeError());
+            return Notes;
+          }
+          auto Simplified = simplifyObligationModule(std::move(*Lowered));
+          if (!Simplified) {
+            llvm::consumeError(Simplified.takeError());
+            return Notes;
+          }
+          ObligationModule Module = std::move(*Simplified);
+          Module.BMCTransform = BMCTransformProvenance{Bound};
+          annotateObligationSources(Module);
+          bool Copies = false;
+          bool CopiesHold = true;
+          bool Unwound = true;
+          for (VerifyResult &Result : Unroller.verifyObligations(Module)) {
+            if (Result.ObligationType == ObligationKind::Unwinding) {
+              Unwound &= Result.Status == VerifyStatus::Verified;
+              continue;
+            }
+            if (!copyOfFailure(Result))
+              continue;
+            Copies = true;
+            if (Result.Status == VerifyStatus::Failed &&
+                Result.Reason == VerifyReason::Counterexample) {
+              Notes.push_back(
+                  "an execution fails this check " +
+                  (Bound == 0
+                       ? std::string("with no iteration of any loop")
+                       : "within " + iterations(Bound) + " of each loop") +
+                  (Result.Message.empty()
+                       ? std::string()
+                       : " (counterexample: " + Result.Message + ")"));
+              return Notes;
+            }
+            CopiesHold &= Result.Status == VerifyStatus::Verified;
+          }
+          Unrolled |= Copies;
+          // Unrolled once, every loop body holds a copy of each of its
+          // checks, and a check after a loop has one from no iteration on;
+          // a failure without a copy by then is of an invariant or a
+          // measure, which unrolling drops at every bound.
+          if (Bound >= 1 && !Unrolled)
+            return Notes;
+          if (!CopiesHold)
+            return Notes;
+          if (Copies && Unwound) {
+            Notes.push_back(
+                "no execution fails this check: every loop ends within " +
+                iterations(Bound) +
+                ", and unrolling proves it there; the "
+                "loops' invariants are too weak for an unbounded proof");
+            return Notes;
+          }
+        }
+        if (Unrolled)
+          Notes.push_back("no execution fails this check within " +
+                          iterations(Opts.ConfirmBound) + " of each loop");
+        return Notes;
+      };
       Passivizer P;
       P.setFunctionMap(InterfaceMap);
       auto proves = [&](PassiveProgram Smoke) {
@@ -4720,6 +4896,7 @@ class Verifier {
           Msg += backendSuffix(R);
           Diags.push_back(
               {VerifyDiagnostic::Error, Msg, R.Location, Fn->Name, R});
+          Diags.back().Notes = failureNotes(*Fn, R);
         } else {
           const bool FallbackExported = R.Status == VerifyStatus::Unresolved &&
                                         exportLeanFallback(Module, Fn->Name, R);
@@ -4740,14 +4917,51 @@ class Verifier {
       }
       DumpStream.flush();
     };
-    if (Parallel) {
-      TaskGroup Group(*Pool);
-      for (size_t I = 0; I != Functions.size(); ++I)
-        Group.async([&verifyFunction, I] { verifyFunction(I); });
-      Group.wait();
-    } else {
+    // With --function, the executable functions run are the selected ones
+    // and, round by round, those whose contracts a verdict of the run relies
+    // on; specs, proof functions, and generated checks always run, since any
+    // verdict may rest on their facts. Every verdict reported is then the
+    // one a run of the whole file gives.
+    std::vector<bool> Scheduled(Functions.size(), true);
+    if (!Opts.FunctionPatterns.empty())
       for (size_t I = 0; I != Functions.size(); ++I)
-        verifyFunction(I);
+        Scheduled[I] =
+            Selected[I] || Functions[I]->IsSpec || Functions[I]->IsProof;
+    std::map<std::string, size_t> IndexOf;
+    for (size_t I = 0; I != Functions.size(); ++I)
+      IndexOf.emplace(Functions[I]->Identity, I);
+    std::vector<size_t> Batch;
+    for (size_t I = 0; I != Functions.size(); ++I)
+      if (Scheduled[I])
+        Batch.push_back(I);
+    while (!Batch.empty()) {
+      if (Parallel) {
+        TaskGroup Group(*Pool);
+        for (size_t I : Batch)
+          Group.async([&verifyFunction, I] { verifyFunction(I); });
+        Group.wait();
+      } else {
+        for (size_t I : Batch)
+          verifyFunction(I);
+      }
+      std::vector<size_t> Next;
+      auto need = [&](const std::string &Identity) {
+        auto It = IndexOf.find(Identity);
+        if (It != IndexOf.end() && !Scheduled[It->second]) {
+          Scheduled[It->second] = true;
+          Next.push_back(It->second);
+        }
+      };
+      for (size_t I : Batch) {
+        for (const auto &[Index, Identity, Callees] : Runs[I].CallDependencies)
+          for (const std::string &Callee : Callees)
+            need(Callee);
+        for (const SpecReliance &Reliance : Runs[I].ProofDependencies)
+          for (const std::string &Callee : Reliance.Callees)
+            need(Callee);
+      }
+      llvm::sort(Next);
+      Batch = std::move(Next);
     }
     // A function whose verification Ctrl-C cut short is reported by one
     // line. Its verdicts stay, hidden, for what they establish: a query the
@@ -4778,6 +4992,9 @@ class Verifier {
       for (VerifyDiagnostic &D : Run.Diags) {
         if (D.FindingOf)
           *D.FindingOf += Base;
+        // What a function --function leaves out reports stays, hidden, for
+        // what it establishes.
+        D.Hidden |= !Selected[I];
         Diags.push_back(std::move(D));
       }
       AllOk &= Run.AllOk;
@@ -5636,6 +5853,14 @@ class Verifier {
       }
     }
 
+    // A run --function narrows succeeds when what it reports does.
+    if (!Opts.FunctionPatterns.empty())
+      return llvm::none_of(Diags, [](const VerifyDiagnostic &D) {
+        return !D.Hidden && (D.K == VerifyDiagnostic::Error ||
+                             D.K == VerifyDiagnostic::Unresolved ||
+                             D.K == VerifyDiagnostic::Interrupted ||
+                             D.K == VerifyDiagnostic::BoundedSafe);
+      });
     return AllOk;
   }
 
@@ -5654,6 +5879,12 @@ class Verifier {
             ? "error"
             : "note";
     Record["message"] = jsonText(D.Message);
+    if (!D.Notes.empty()) {
+      llvm::json::Array Notes;
+      for (const std::string &Note : D.Notes)
+        Notes.push_back(jsonText(Note));
+      Record["notes"] = std::move(Notes);
+    }
     if (!D.FunctionName.empty())
       Record["function"] = jsonText(D.FunctionName);
 
@@ -6000,6 +6231,8 @@ class Verifier {
              << PLoc.getColumn() << ": ";
         OS << "note: " << InstantiationNote << "\n";
       }
+      for (const std::string &Note : D.Notes)
+        OS << "note: " << Note << "\n";
     }
   }
 };

clang/lib/Verify/Driver/Verifier.h

@@ -120,6 +120,13 @@ struct VerifyOptions {
   bool Verbose = false;
   /// List the functions the run would verify, and verify none.
   bool ListFunctions = false;
+  /// Glob patterns over function names: only the functions they match are
+  /// reported. Empty: every function.
+  std::vector<std::string> FunctionPatterns;
+  /// For a failure whose counterexample passes through a loop, the most
+  /// iterations of each loop that unrolling may try to find an execution
+  /// that fails (0: do not try).
+  unsigned ConfirmBound = 10;
   /// Where the run counts the verdicts it prints, if anywhere.
   VerifySummary *Summary = nullptr;
 };