diff --git a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def index 737bc8e86cfb6..efed65e6c986d 100644 --- a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def +++ b/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", diff --git a/clang/test/Analysis/analyzer-config.c b/clang/test/Analysis/analyzer-config.c index 8eb869bac46f8..0f1314aae9db5 100644 --- a/clang/test/Analysis/analyzer-config.c +++ b/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 diff --git a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp index ef07e47ee911b..626f5c163d17d 100644 --- a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp +++ b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp @@ -38,8 +38,8 @@ 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. @@ -47,8 +47,17 @@ static const AnalyzerOptions DefaultOpts = [] { 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 class Z3CrosscheckOracleTest : public testing::Test { public: Z3Decision interpretQueryResult(const Z3Result &Result) { @@ -56,58 +65,100 @@ class Z3CrosscheckOracleTest : public testing::Test { } private: - Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(DefaultOpts); + Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(Opts); }; -TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) { +using DefaultZ3CrosscheckOracleTest = Z3CrosscheckOracleTest; +using LimitedZ3CrosscheckOracleTest = Z3CrosscheckOracleTest; + +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