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

[Donát Nagy via llvm-branch-commits]

================
@@ -101,18 +123,37 @@ void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const {
 Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
     const Z3CrosscheckVisitor::Z3Result &Query) {
   ++NumZ3QueriesDone;
+  ++NumZ3QueriesDoneInEqClass;
+  AccumulatedZ3QueryTimeInEqClass += Query.Z3QueryTimeMilliseconds;
 
-  if (!Query.IsSAT.has_value()) {
-    // For backward compatibility, let's accept the first timeout.
+  if (Query.IsSAT && Query.IsSAT.value()) {
+    ++NumTimesZ3QueryAcceptsReport;
+    return AcceptReport; // sat
+  }
+
+  // Suggest cutting the EQClass if certain heuristics trigger.
+  if (Opts.Z3CrosscheckTimeoutThreshold &&
+      Query.Z3QueryTimeMilliseconds >= Opts.Z3CrosscheckTimeoutThreshold) {
     ++NumTimesZ3TimedOut;
-    return AcceptReport;
+    ++NumTimesZ3QueryRejectEQClass;
+    return RejectEQClass;
   }
 
-  if (Query.IsSAT.value()) {
-    ++NumTimesZ3QueryAcceptsReport;
-    return AcceptReport; // sat
+  if (Opts.Z3CrosscheckRLimitThreshold &&
+      Query.UsedRLimit >= Opts.Z3CrosscheckRLimitThreshold) {
+    ++NumTimesZ3ExhaustedRLimit;
+    ++NumTimesZ3QueryRejectEQClass;
+    return RejectEQClass;
+  }
+
+  if (AccumulatedZ3QueryTimeInEqClass > 700 /*ms*/) {
----------------
NagyDonat wrote:

It's counter-intuitive that this limit is hardcoded, while the others are not -- e.g. this will silently override timeout thresholds above 700 ms.

Obviously this is bikeshedding, because practically nobody will use these config options, but if we want to make this configurable, then we should make the config clear and user-friendly. Either introduce this limit as a third configurable value, or e.g. say that it's always twice the individual timeout (which would yield 600 ms instead of 700 ms). 

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