[llvm-branch-commits] [analyzer] Harden safeguards for Z3 query times (PR #95129)

[Balazs Benics via llvm-branch-commits]

================
@@ -44,21 +47,43 @@ 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.
+  ///
+  /// 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 NumZ3QueriesDoneInEqClass = 0;
----------------
steakhal wrote:

Hmm, I dont think I use this anymore.

https://github.com/llvm/llvm-project/pull/95129