Revert "[analyzer] Harden safeguards for Z3 query times"

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

@@ -184,26 +184,6 @@ 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,11 +25,8 @@ class Z3CrosscheckVisitor final : public BugReporterVisitor {
 public:
   struct Z3Result {
     std::optional<bool> IsSAT = std::nullopt;
-    unsigned Z3QueryTimeMilliseconds = 0;
-    unsigned UsedRLimit = 0;
   };
-  Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,
-                      const AnalyzerOptions &Opts);
+  explicit Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result);
 
   void Profile(llvm::FoldingSetNodeID &ID) const override;
 
@@ -47,44 +44,21 @@ 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 and the statistics of the queries of a report
-/// equivalenece class.
+/// the results of the Z3 solver.
 class Z3CrosscheckOracle {
 public:
-  explicit Z3CrosscheckOracle(const AnalyzerOptions &Opts) : Opts(Opts) {}
-
   enum Z3Decision {
-    AcceptReport,  // The report was SAT.
-    RejectReport,  // The report was UNSAT or UNDEF.
-    RejectEQClass, // The heuristic suggests to skip the current eqclass.
+    AcceptReport, // The report was SAT.
+    RejectReport, // The report was UNSAT or UNDEF.
   };
 
-  /// 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
+  /// 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);
 };
 
 } // namespace clang::ento

clang/lib/StaticAnalyzer/Core/BugReporter.cpp

@@ -89,9 +89,6 @@ 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");
 
@@ -2843,7 +2840,6 @@ generateVisitorsDiagnostics(PathSensitiveBugReport *R,
 std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
     ArrayRef<PathSensitiveBugReport *> &bugReports,
     PathSensitiveBugReporter &Reporter) {
-  Z3CrosscheckOracle Z3Oracle(Reporter.getAnalyzerOptions());
 
   BugPathGetter BugGraph(&Reporter.getGraph(), bugReports);
 
@@ -2875,20 +2871,16 @@ std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
         // visitor and check again
         R->clearVisitors();
         Z3CrosscheckVisitor::Z3Result CrosscheckResult;
-        R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult,
-                                           Reporter.getAnalyzerOptions());
+        R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult);
 
         // 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 (Z3Oracle.interpretQueryResult(CrosscheckResult)) {
+        switch (Z3CrosscheckOracle::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,37 +12,26 @@
 //===----------------------------------------------------------------------===//
 
 #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,
-                                         const AnalyzerOptions &Opts)
-    : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result),
-      Opts(Opts) {}
+Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result)
+    : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result) {}
 
 void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
                                           const ExplodedNode *EndPathNode,
@@ -52,12 +41,8 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
 
   // Create a refutation manager
   llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
-  if (Opts.Z3CrosscheckRLimitThreshold)
-    RefutationSolver->setUnsignedParam("rlimit",
-                                       Opts.Z3CrosscheckRLimitThreshold);
-  if (Opts.Z3CrosscheckTimeoutThreshold)
-    RefutationSolver->setUnsignedParam("timeout",
-                                       Opts.Z3CrosscheckTimeoutThreshold); // ms
+  RefutationSolver->setBoolParam("model", true);        // Enable model finding
+  RefutationSolver->setUnsignedParam("timeout", 15000); // ms
 
   ASTContext &Ctx = BRC.getASTContext();
 
@@ -78,15 +63,8 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
   }
 
   // And check for satisfiability
-  llvm::TimeRecord Start = llvm::TimeRecord::getCurrentTime(/*Start=*/true);
   std::optional<bool> IsSAT = RefutationSolver->check();
-  llvm::TimeRecord Diff = llvm::TimeRecord::getCurrentTime(/*Start=*/false);
-  Diff -= Start;
-  Result = Z3Result{
-      IsSAT,
-      static_cast<unsigned>(Diff.getWallTime() * 1000),
-      RefutationSolver->getStatistics()->getUnsigned("rlimit count"),
-  };
+  Result = Z3Result{IsSAT};
 }
 
 void Z3CrosscheckVisitor::addConstraints(
@@ -123,38 +101,18 @@ void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const {
 Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
     const Z3CrosscheckVisitor::Z3Result &Query) {
   ++NumZ3QueriesDone;
-  AccumulatedZ3QueryTimeInEqClass += Query.Z3QueryTimeMilliseconds;
 
-  if (Query.IsSAT && Query.IsSAT.value()) {
-    ++NumTimesZ3QueryAcceptsReport;
-    return AcceptReport;
-  }
-
-  // Suggest cutting the EQClass if certain heuristics trigger.
-  if (Opts.Z3CrosscheckTimeoutThreshold &&
-      Query.Z3QueryTimeMilliseconds >= Opts.Z3CrosscheckTimeoutThreshold) {
+  if (!Query.IsSAT.has_value()) {
+    // For backward compatibility, let's accept the first timeout.
     ++NumTimesZ3TimedOut;
-    ++NumTimesZ3QueryRejectEQClass;
-    return RejectEQClass;
-  }
-
-  if (Opts.Z3CrosscheckRLimitThreshold &&
-      Query.UsedRLimit >= Opts.Z3CrosscheckRLimitThreshold) {
-    ++NumTimesZ3ExhaustedRLimit;
-    ++NumTimesZ3QueryRejectEQClass;
-    return RejectEQClass;
+    return AcceptReport;
   }
 
-  if (Opts.Z3CrosscheckEQClassTimeoutThreshold &&
-      AccumulatedZ3QueryTimeInEqClass >
-          Opts.Z3CrosscheckEQClassTimeoutThreshold) {
-    ++NumTimesZ3SpendsTooMuchTimeOnASingleEQClass;
-    ++NumTimesZ3QueryRejectEQClass;
-    return RejectEQClass;
+  if (Query.IsSAT.value()) {
+    ++NumTimesZ3QueryAcceptsReport;
+    return AcceptReport; // sat
   }
 
-  // If no cutoff heuristics trigger, and the report is "unsat" or "undef",
-  // then reject the report.
   ++NumTimesZ3QueryRejectReport;
-  return RejectReport;
+  return RejectReport; // unsat
 }

clang/test/Analysis/analyzer-config.c

@@ -43,9 +43,6 @@
 // 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