Reland "[analyzer] Harden safeguards for Z3 query times" (llvm#97298)

This is exactly as originally landed in llvm#95129,
but now the minimal Z3 version was increased to meet this change in llvm#96682.

https://discourse.llvm.org/t/bump-minimal-z3-requirements-from-4-7-1-to-4-8-9/79664/4

---

This patch is a functional change.
https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520

As a result of this patch, individual Z3 queries in refutation will be
bound by 300ms. Every report equivalence class will be processed in at
most 1 second.

The heuristic should have only really marginal observable impact -
except for the cases when we had big report eqclasses with long-running
(15s) Z3 queries, where previously CSA effectively halted. After this
patch, CSA will tackle such extreme cases as well.

(cherry picked from commit eacc3b3)

clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def

@@ -184,6 +184,26 @@ ANALYZER_OPTION(bool, ShouldCrosscheckWithZ3, "crosscheck-with-z3",
                 "constraint manager backend.",
                 false)
 
+ANALYZER_OPTION(
+    unsigned, Z3CrosscheckEQClassTimeoutThreshold,
+    "crosscheck-with-z3-eqclass-timeout-threshold",
+    "Set a timeout for bug report equivalence classes in milliseconds. "
+    "If we exhaust this threshold, we will drop the bug report eqclass "
+    "instead of doing more Z3 queries. Set 0 for no timeout.", 700)
+
+ANALYZER_OPTION(
+    unsigned, Z3CrosscheckTimeoutThreshold,
+    "crosscheck-with-z3-timeout-threshold",
+    "Set a timeout for individual Z3 queries in milliseconds. "
+    "Set 0 for no timeout.", 300)
+
+ANALYZER_OPTION(
+    unsigned, Z3CrosscheckRLimitThreshold,
+    "crosscheck-with-z3-rlimit-threshold",
+    "Set the Z3 resource limit threshold. This sets a deterministic cutoff "
+    "point for Z3 queries, as longer queries usually consume more resources. "
+    "Set 0 for unlimited.", 400'000)
+
 ANALYZER_OPTION(bool, ShouldReportIssuesInMainSourceFile,
                 "report-in-main-source-file",
                 "Whether or not the diagnostic report should be always "

clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h

@@ -25,8 +25,11 @@ class Z3CrosscheckVisitor final : public BugReporterVisitor {
 public:
   struct Z3Result {
     std::optional<bool> IsSAT = std::nullopt;
+    unsigned Z3QueryTimeMilliseconds = 0;
+    unsigned UsedRLimit = 0;
   };
-  explicit Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result);
+  Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,
+                      const AnalyzerOptions &Opts);
 
   void Profile(llvm::FoldingSetNodeID &ID) const override;
 
@@ -44,21 +47,44 @@ class Z3CrosscheckVisitor final : public BugReporterVisitor {
   /// Holds the constraints in a given path.
   ConstraintMap Constraints;
   Z3Result &Result;
+  const AnalyzerOptions &Opts;
 };
 
 /// The oracle will decide if a report should be accepted or rejected based on
-/// the results of the Z3 solver.
+/// the results of the Z3 solver and the statistics of the queries of a report
+/// equivalenece class.
 class Z3CrosscheckOracle {
 public:
+  explicit Z3CrosscheckOracle(const AnalyzerOptions &Opts) : Opts(Opts) {}
+
   enum Z3Decision {
-    AcceptReport, // The report was SAT.
-    RejectReport, // The report was UNSAT or UNDEF.
+    AcceptReport,  // The report was SAT.
+    RejectReport,  // The report was UNSAT or UNDEF.
+    RejectEQClass, // The heuristic suggests to skip the current eqclass.
   };
 
-  /// Makes a decision for accepting or rejecting the report based on the
-  /// result of the corresponding Z3 query.
-  static Z3Decision
-  interpretQueryResult(const Z3CrosscheckVisitor::Z3Result &Query);
+  /// Updates the internal state with the new Z3Result and makes a decision how
+  /// to proceed:
+  /// - Accept the report if the Z3Result was SAT.
+  /// - Suggest dropping the report equvalence class based on the accumulated
+  ///   statistics.
+  /// - Otherwise, reject the report if the Z3Result was UNSAT or UNDEF.
+  ///
+  /// Conditions for dropping the equivalence class:
+  /// - Accumulative time spent in Z3 checks is more than 700ms in the eqclass.
+  /// - Hit the 300ms query timeout in the report eqclass.
+  /// - Hit the 400'000 rlimit in the report eqclass.
+  ///
+  /// All these thresholds are configurable via the analyzer options.
+  ///
+  /// Refer to
+  /// https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520 to
+  /// see why this heuristic was chosen.
+  Z3Decision interpretQueryResult(const Z3CrosscheckVisitor::Z3Result &Meta);
+
+private:
+  const AnalyzerOptions &Opts;
+  unsigned AccumulatedZ3QueryTimeInEqClass = 0; // ms
 };
 
 } // namespace clang::ento

clang/lib/StaticAnalyzer/Core/BugReporter.cpp

@@ -89,6 +89,9 @@ STATISTIC(MaxValidBugClassSize,
 
 STATISTIC(NumTimesReportPassesZ3, "Number of reports passed Z3");
 STATISTIC(NumTimesReportRefuted, "Number of reports refuted by Z3");
+STATISTIC(NumTimesReportEQClassAborted,
+          "Number of times a report equivalence class was aborted by the Z3 "
+          "oracle heuristic");
 STATISTIC(NumTimesReportEQClassWasExhausted,
           "Number of times all reports of an equivalence class was refuted");
 
@@ -2840,6 +2843,7 @@ generateVisitorsDiagnostics(PathSensitiveBugReport *R,
 std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
     ArrayRef<PathSensitiveBugReport *> &bugReports,
     PathSensitiveBugReporter &Reporter) {
+  Z3CrosscheckOracle Z3Oracle(Reporter.getAnalyzerOptions());
 
   BugPathGetter BugGraph(&Reporter.getGraph(), bugReports);
 
@@ -2871,16 +2875,20 @@ std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
         // visitor and check again
         R->clearVisitors();
         Z3CrosscheckVisitor::Z3Result CrosscheckResult;
-        R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult);
+        R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult,
+                                           Reporter.getAnalyzerOptions());
 
         // We don't overwrite the notes inserted by other visitors because the
         // refutation manager does not add any new note to the path
         generateVisitorsDiagnostics(R, BugPath->ErrorNode, BRC);
-        switch (Z3CrosscheckOracle::interpretQueryResult(CrosscheckResult)) {
+        switch (Z3Oracle.interpretQueryResult(CrosscheckResult)) {
         case Z3CrosscheckOracle::RejectReport:
           ++NumTimesReportRefuted;
           R->markInvalid("Infeasible constraints", /*Data=*/nullptr);
           continue;
+        case Z3CrosscheckOracle::RejectEQClass:
+          ++NumTimesReportEQClassAborted;
+          return {};
         case Z3CrosscheckOracle::AcceptReport:
           ++NumTimesReportPassesZ3;
           break;

clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp

@@ -12,26 +12,37 @@
 //===----------------------------------------------------------------------===//
 
 #include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
+#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
 #include "clang/StaticAnalyzer/Core/BugReporter/BugReporter.h"
 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
 #include "llvm/ADT/Statistic.h"
 #include "llvm/Support/SMTAPI.h"
+#include "llvm/Support/Timer.h"
 
 #define DEBUG_TYPE "Z3CrosscheckOracle"
 
 STATISTIC(NumZ3QueriesDone, "Number of Z3 queries done");
 STATISTIC(NumTimesZ3TimedOut, "Number of times Z3 query timed out");
+STATISTIC(NumTimesZ3ExhaustedRLimit,
+          "Number of times Z3 query exhausted the rlimit");
+STATISTIC(NumTimesZ3SpendsTooMuchTimeOnASingleEQClass,
+          "Number of times report equivalenece class was cut because it spent "
+          "too much time in Z3");
 
 STATISTIC(NumTimesZ3QueryAcceptsReport,
           "Number of Z3 queries accepting a report");
 STATISTIC(NumTimesZ3QueryRejectReport,
           "Number of Z3 queries rejecting a report");
+STATISTIC(NumTimesZ3QueryRejectEQClass,
+          "Number of times rejecting an report equivalenece class");
 
 using namespace clang;
 using namespace ento;
 
-Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result)
-    : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result) {}
+Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,
+                                         const AnalyzerOptions &Opts)
+    : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result),
+      Opts(Opts) {}
 
 void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
                                           const ExplodedNode *EndPathNode,
@@ -41,8 +52,12 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
 
   // Create a refutation manager
   llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
-  RefutationSolver->setBoolParam("model", true);        // Enable model finding
-  RefutationSolver->setUnsignedParam("timeout", 15000); // ms
+  if (Opts.Z3CrosscheckRLimitThreshold)
+    RefutationSolver->setUnsignedParam("rlimit",
+                                       Opts.Z3CrosscheckRLimitThreshold);
+  if (Opts.Z3CrosscheckTimeoutThreshold)
+    RefutationSolver->setUnsignedParam("timeout",
+                                       Opts.Z3CrosscheckTimeoutThreshold); // ms
 
   ASTContext &Ctx = BRC.getASTContext();
 
@@ -63,8 +78,15 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
   }
 
   // And check for satisfiability
+  llvm::TimeRecord Start = llvm::TimeRecord::getCurrentTime(/*Start=*/true);
   std::optional<bool> IsSAT = RefutationSolver->check();
-  Result = Z3Result{IsSAT};
+  llvm::TimeRecord Diff = llvm::TimeRecord::getCurrentTime(/*Start=*/false);
+  Diff -= Start;
+  Result = Z3Result{
+      IsSAT,
+      static_cast<unsigned>(Diff.getWallTime() * 1000),
+      RefutationSolver->getStatistics()->getUnsigned("rlimit count"),
+  };
 }
 
 void Z3CrosscheckVisitor::addConstraints(
@@ -101,18 +123,38 @@ void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const {
 Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
     const Z3CrosscheckVisitor::Z3Result &Query) {
   ++NumZ3QueriesDone;
+  AccumulatedZ3QueryTimeInEqClass += Query.Z3QueryTimeMilliseconds;
 
-  if (!Query.IsSAT.has_value()) {
-    // For backward compatibility, let's accept the first timeout.
-    ++NumTimesZ3TimedOut;
+  if (Query.IsSAT && Query.IsSAT.value()) {
+    ++NumTimesZ3QueryAcceptsReport;
     return AcceptReport;
   }
 
-  if (Query.IsSAT.value()) {
-    ++NumTimesZ3QueryAcceptsReport;
-    return AcceptReport; // sat
+  // Suggest cutting the EQClass if certain heuristics trigger.
+  if (Opts.Z3CrosscheckTimeoutThreshold &&
+      Query.Z3QueryTimeMilliseconds >= Opts.Z3CrosscheckTimeoutThreshold) {
+    ++NumTimesZ3TimedOut;
+    ++NumTimesZ3QueryRejectEQClass;
+    return RejectEQClass;
+  }
+
+  if (Opts.Z3CrosscheckRLimitThreshold &&
+      Query.UsedRLimit >= Opts.Z3CrosscheckRLimitThreshold) {
+    ++NumTimesZ3ExhaustedRLimit;
+    ++NumTimesZ3QueryRejectEQClass;
+    return RejectEQClass;
+  }
+
+  if (Opts.Z3CrosscheckEQClassTimeoutThreshold &&
+      AccumulatedZ3QueryTimeInEqClass >
+          Opts.Z3CrosscheckEQClassTimeoutThreshold) {
+    ++NumTimesZ3SpendsTooMuchTimeOnASingleEQClass;
+    ++NumTimesZ3QueryRejectEQClass;
+    return RejectEQClass;
   }
 
+  // If no cutoff heuristics trigger, and the report is "unsat" or "undef",
+  // then reject the report.
   ++NumTimesZ3QueryRejectReport;
-  return RejectReport; // unsat
+  return RejectReport;
 }

clang/test/Analysis/analyzer-config.c

@@ -43,6 +43,9 @@
 // CHECK-NEXT: cplusplus.Move:WarnOn = KnownsAndLocals
 // CHECK-NEXT: cplusplus.SmartPtrModeling:ModelSmartPtrDereference = false
 // CHECK-NEXT: crosscheck-with-z3 = false
+// CHECK-NEXT: crosscheck-with-z3-eqclass-timeout-threshold = 700
+// CHECK-NEXT: crosscheck-with-z3-rlimit-threshold = 400000
+// CHECK-NEXT: crosscheck-with-z3-timeout-threshold = 300
 // CHECK-NEXT: ctu-dir = ""
 // CHECK-NEXT: ctu-import-cpp-threshold = 8
 // CHECK-NEXT: ctu-import-threshold = 24