[analyzer][Z3] Restore the original timeout of 15s

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

@@ -189,20 +189,29 @@ ANALYZER_OPTION(
     "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)
+    "instead of doing more Z3 queries. Setting this to 700 ms in conjunction "
+    "with \"crosscheck-with-z3-timeout-threshold\" of 300 ms, would nicely "
+    "guarantee that no bug report equivalence class can take longer than "
+    "1 second, effectively mitigating Z3 hangs during refutation. "
+    "Set 0 for no timeout.", 0)
 
 ANALYZER_OPTION(
     unsigned, Z3CrosscheckTimeoutThreshold,
     "crosscheck-with-z3-timeout-threshold",
     "Set a timeout for individual Z3 queries in milliseconds. "
-    "Set 0 for no timeout.", 300)
+    "On fast machines, 300 worked well in some cases. "
+    "The lower it is, the higher the chances of having flaky issues. "
+    "Having no timeout may hang the analyzer indefinitely. "
+    "Set 0 for no timeout.", 15'000)
 
 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)
+    "Set the Z3 resource limit threshold. This sets a supposedly deterministic "
+    "cutoff point for Z3 queries, as longer queries usually consume more "
+    "resources. "
+    "400'000 should on average make Z3 queries run for up to 100ms on modern "
+    "hardware. Set 0 for unlimited.", 0)
 
 ANALYZER_OPTION(bool, ShouldReportIssuesInMainSourceFile,
                 "report-in-main-source-file",

clang/test/Analysis/analyzer-config.c

@@ -41,9 +41,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: crosscheck-with-z3-eqclass-timeout-threshold = 0
+// CHECK-NEXT: crosscheck-with-z3-rlimit-threshold = 0
+// CHECK-NEXT: crosscheck-with-z3-timeout-threshold = 15000
 // CHECK-NEXT: ctu-dir = ""
 // CHECK-NEXT: ctu-import-cpp-threshold = 8
 // CHECK-NEXT: ctu-import-threshold = 24

clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp

@@ -38,76 +38,127 @@ static const AnalyzerOptions DefaultOpts = [] {
 
   // 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);
+  assert(Config.Z3CrosscheckRLimitThreshold == 0);
+  assert(Config.Z3CrosscheckTimeoutThreshold == 15'000_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;
 }();
 
+static const AnalyzerOptions LimitedOpts = [] {
+  AnalyzerOptions Config = DefaultOpts;
+  Config.Z3CrosscheckEQClassTimeoutThreshold = 700_ms;
+  Config.Z3CrosscheckTimeoutThreshold = 300_step;
+  Config.Z3CrosscheckRLimitThreshold = 400'000_step;
+  return Config;
+}();
+
 namespace {
 
+template <const AnalyzerOptions &Opts>
 class Z3CrosscheckOracleTest : public testing::Test {
 public:
   Z3Decision interpretQueryResult(const Z3Result &Result) {
     return Oracle.interpretQueryResult(Result);
   }
 
 private:
-  Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(DefaultOpts);
+  Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(Opts);
 };
 
-TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) {
+using DefaultZ3CrosscheckOracleTest = Z3CrosscheckOracleTest<DefaultOpts>;
+using LimitedZ3CrosscheckOracleTest = Z3CrosscheckOracleTest<LimitedOpts>;
+
+TEST_F(DefaultZ3CrosscheckOracleTest, AcceptsFirstSAT) {
+  ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
+}
+TEST_F(LimitedZ3CrosscheckOracleTest, AcceptsFirstSAT) {
   ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
 }
 
-TEST_F(Z3CrosscheckOracleTest, AcceptsSAT) {
+TEST_F(DefaultZ3CrosscheckOracleTest, AcceptsSAT) {
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+  ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
+}
+TEST_F(LimitedZ3CrosscheckOracleTest, AcceptsSAT) {
   ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
   ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
 }
 
-TEST_F(Z3CrosscheckOracleTest, SATWhenItGoesOverTime) {
+TEST_F(DefaultZ3CrosscheckOracleTest, SATWhenItGoesOverTime) {
+  // Even if it times out, if it is SAT, we should accept it.
+  ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 15'010_ms, 1000_step}));
+}
+TEST_F(LimitedZ3CrosscheckOracleTest, 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, UNSATWhenItGoesOverTime) {
+TEST_F(DefaultZ3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
+  ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 15'010_ms, 1000_step}));
+}
+TEST_F(LimitedZ3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
   ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step}));
 }
 
-TEST_F(Z3CrosscheckOracleTest, RejectsTimeout) {
+TEST_F(DefaultZ3CrosscheckOracleTest, RejectsTimeout) {
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
+  ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 15'010_ms, 1000_step}));
+}
+TEST_F(LimitedZ3CrosscheckOracleTest, 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) {
+TEST_F(DefaultZ3CrosscheckOracleTest, RejectsUNSATs) {
+  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}));
+}
+TEST_F(LimitedZ3CrosscheckOracleTest, RejectsUNSATs) {
   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:
-// =======================
+// Testing cut heuristics of the two configurations:
+// =================================================
 
-TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfSpendsTooMuchTotalTime) {
+TEST_F(DefaultZ3CrosscheckOracleTest, RejectEQClassIfSpendsTooMuchTotalTime) {
+  // Simulate long queries, that barely doesn't trigger the timeout.
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step}));
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step}));
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step}));
+}
+TEST_F(LimitedZ3CrosscheckOracleTest, 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) {
+TEST_F(DefaultZ3CrosscheckOracleTest, SATWhenItSpendsTooMuchTotalTime) {
+  // Simulate long queries, that barely doesn't trigger the timeout.
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step}));
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step}));
+  ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 14'990_ms, 1000_step}));
+}
+TEST_F(LimitedZ3CrosscheckOracleTest, 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) {
+// Z3CrosscheckEQClassTimeoutThreshold is disabled in default configuration, so
+// it doesn't make sense to test that.
+TEST_F(LimitedZ3CrosscheckOracleTest, 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) {
@@ -117,7 +168,9 @@ TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfAttemptsManySmallQueries) {
   ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 1_ms, 1000_step}));
 }
 
-TEST_F(Z3CrosscheckOracleTest, SATWhenIfAttemptsManySmallQueries) {
+// Z3CrosscheckEQClassTimeoutThreshold is disabled in default configuration, so
+// it doesn't make sense to test that.
+TEST_F(LimitedZ3CrosscheckOracleTest, SATWhenItAttemptsManySmallQueries) {
   // 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) {
@@ -128,16 +181,34 @@ TEST_F(Z3CrosscheckOracleTest, SATWhenIfAttemptsManySmallQueries) {
   ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 200_ms, 1000_step}));
 }
 
-TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfExhaustsRLimit) {
+// Z3CrosscheckRLimitThreshold is disabled in default configuration, so it
+// doesn't make sense to test that.
+TEST_F(LimitedZ3CrosscheckOracleTest, RejectEQClassIfExhaustsRLimit) {
   ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
   ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
   ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 25_ms, 405'000_step}));
 }
 
-TEST_F(Z3CrosscheckOracleTest, SATWhenItExhaustsRLimit) {
+// Z3CrosscheckRLimitThreshold is disabled in default configuration, so it
+// doesn't make sense to test that.
+TEST_F(LimitedZ3CrosscheckOracleTest, SATWhenItExhaustsRLimit) {
   ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
   ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
   ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 405'000_step}));
 }
 
+// Demonstrate the weaknesses of the default configuration:
+// ========================================================
+
+TEST_F(DefaultZ3CrosscheckOracleTest, ManySlowQueriesHangTheAnalyzer) {
+  // Simulate many slow queries: 250 slow UNSAT queries.
+  // 250*14000ms = 3500s, ~1 hour. Since we disabled the total time limitation,
+  // this eqclass would take roughly 1 hour to process.
+  // It doesn't matter what rlimit the queries consume.
+  for (int i = 0; i < 250; ++i) {
+    ASSERT_EQ(RejectReport,
+              interpretQueryResult({UNSAT, 14'000_ms, 1'000'000_step}));
+  }
+}
+
 } // namespace