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

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

================
@@ -17,43 +18,126 @@ using Z3Decision = Z3CrosscheckOracle::Z3Decision;
 
 static constexpr Z3Decision AcceptReport = Z3Decision::AcceptReport;
 static constexpr Z3Decision RejectReport = Z3Decision::RejectReport;
+static constexpr Z3Decision RejectEQClass = Z3Decision::RejectEQClass;
 
 static constexpr std::optional<bool> SAT = true;
 static constexpr std::optional<bool> UNSAT = false;
 static constexpr std::optional<bool> UNDEF = std::nullopt;
 
+static unsigned operator""_ms(unsigned long long ms) { return ms; }
+static unsigned operator""_step(unsigned long long rlimit) { return rlimit; }
+
+static const AnalyzerOptions DefaultOpts = [] {
+  AnalyzerOptions Config;
+#define ANALYZER_OPTION_DEPENDS_ON_USER_MODE(TYPE, NAME, CMDFLAG, DESC,        \
+                                             SHALLOW_VAL, DEEP_VAL)            \
+  ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEEP_VAL)
+#define ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEFAULT_VAL)                \
+  Config.NAME = DEFAULT_VAL;
+#include "clang/StaticAnalyzer/Core/AnalyzerOptions.def"
+
+  // Remember to update the tests in this file when these values change.
+  // Also update the doc comment of `interpretQueryResult`.
+  assert(Config.Z3CrosscheckRLimitThreshold == 400'000);
+  assert(Config.Z3CrosscheckTimeoutThreshold == 300 /*ms*/);
+  // Usually, when the timeout/rlimit threshold is reached, Z3 only slightly
+  // overshoots until it realizes that it overshoot and needs to back off.
+  // Consequently, the measured timeout should be fairly close to the threshold.
+  // Same reasoning applies to the rlimit too.
+  return Config;
+}();
+
 namespace {
 
-struct Z3CrosscheckOracleTest : public testing::Test {
-  Z3Decision interpretQueryResult(const Z3Result &Result) const {
-    return Z3CrosscheckOracle::interpretQueryResult(Result);
+class Z3CrosscheckOracleTest : public testing::Test {
+public:
+  Z3Decision interpretQueryResult(const Z3Result &Result) {
+    return Oracle.interpretQueryResult(Result);
   }
+
+private:
+  Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(DefaultOpts);
 };
 
 TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) {
-  ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));
+  ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
 }
 
 TEST_F(Z3CrosscheckOracleTest, AcceptsSAT) {
-  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
-  ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+  ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
+}
+
+TEST_F(Z3CrosscheckOracleTest, SATWhenItGoesOverTime) {
+  // Even if it times out, if it is SAT, we should accept it.
+  ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 310_ms, 1000_step}));
 }
 
-TEST_F(Z3CrosscheckOracleTest, AcceptsFirstTimeout) {
-  ASSERT_EQ(AcceptReport, interpretQueryResult({UNDEF}));
+TEST_F(Z3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
+  ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step}));
 }
 
-TEST_F(Z3CrosscheckOracleTest, AcceptsTimeout) {
-  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
-  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
-  ASSERT_EQ(AcceptReport, interpretQueryResult({UNDEF}));
+TEST_F(Z3CrosscheckOracleTest, RejectsTimeout) {
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+  ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 310_ms, 1000_step}));
 }
 
 TEST_F(Z3CrosscheckOracleTest, RejectsUNSATs) {
-  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
-  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
-  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
-  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+}
+
+// Testing cut heuristics:
+// =======================
+
+TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfSpendsTooMuchTotalTime) {
+  // Simulate long queries, that barely doesn't trigger the timeout.
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
+  ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
+}
+
+TEST_F(Z3CrosscheckOracleTest, SATWhenItSpendsTooMuchTotalTime) {
+  // Simulate long queries, that barely doesn't trigger the timeout.
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
+  ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 290_ms, 1000_step}));
+}
+
+TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfAttemptsManySmallQueries) {
+  // Simulate quick, but many queries: 35 quick UNSAT queries.
+  // 35*20ms = 700ms, which is equal to the 700ms threshold.
+  for (int i = 0; i < 35; ++i) {
+    ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step}));
+  }
+  // Do one more to trigger the heuristic.
+  ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 1_ms, 1000_step}));
+}
+
+TEST_F(Z3CrosscheckOracleTest, SATWhenIfAttemptsManySmallQueries) {
+  // Simulate quick, but many queries: 35 quick UNSAT queries.
+  // 35*20ms = 700ms, which is equal to the 700ms threshold.
+  for (int i = 0; i < 35; ++i) {
+    ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step}));
+  }
+  // Do one more to trigger the heuristic, but given this was SAT, we still
+  // accept the query.
+  ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 200_ms, 1000_step}));
+}
+
+TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfHitsRLimitTooManyTimes) {
----------------
NagyDonat wrote:

The name `"HitsRLimitTooManyTimes"` is a leftover from the earlier plan where one `rlimit` overrun wasn't enough to discard the eqclass. (This also applies for the next TC.)

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