1 //===- unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp ----------------===// 2 // 3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. 4 // See https://llvm.org/LICENSE.txt for license information. 5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception 6 // 7 //===----------------------------------------------------------------------===// 8 9 #include "clang/StaticAnalyzer/Core/AnalyzerOptions.h" 10 #include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h" 11 #include "gtest/gtest.h" 12 13 using namespace clang; 14 using namespace ento; 15 16 using Z3Result = Z3CrosscheckVisitor::Z3Result; 17 using Z3Decision = Z3CrosscheckOracle::Z3Decision; 18 19 static constexpr Z3Decision AcceptReport = Z3Decision::AcceptReport; 20 static constexpr Z3Decision RejectReport = Z3Decision::RejectReport; 21 static constexpr Z3Decision RejectEQClass = Z3Decision::RejectEQClass; 22 23 static constexpr std::optional<bool> SAT = true; 24 static constexpr std::optional<bool> UNSAT = false; 25 static constexpr std::optional<bool> UNDEF = std::nullopt; 26 27 static unsigned operator""_ms(unsigned long long ms) { return ms; } 28 static unsigned operator""_step(unsigned long long rlimit) { return rlimit; } 29 30 static const AnalyzerOptions DefaultOpts = [] { 31 AnalyzerOptions Config; 32 #define ANALYZER_OPTION_DEPENDS_ON_USER_MODE(TYPE, NAME, CMDFLAG, DESC, \ 33 SHALLOW_VAL, DEEP_VAL) \ 34 ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEEP_VAL) 35 #define ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEFAULT_VAL) \ 36 Config.NAME = DEFAULT_VAL; 37 #include "clang/StaticAnalyzer/Core/AnalyzerOptions.def" 38 39 // Remember to update the tests in this file when these values change. 40 // Also update the doc comment of `interpretQueryResult`. 41 assert(Config.Z3CrosscheckRLimitThreshold == 0); 42 assert(Config.Z3CrosscheckTimeoutThreshold == 15'000_ms); 43 // Usually, when the timeout/rlimit threshold is reached, Z3 only slightly 44 // overshoots until it realizes that it overshoot and needs to back off. 45 // Consequently, the measured timeout should be fairly close to the threshold. 46 // Same reasoning applies to the rlimit too. 47 return Config; 48 }(); 49 50 static const AnalyzerOptions LimitedOpts = [] { 51 AnalyzerOptions Config = DefaultOpts; 52 Config.Z3CrosscheckEQClassTimeoutThreshold = 700_ms; 53 Config.Z3CrosscheckTimeoutThreshold = 300_step; 54 Config.Z3CrosscheckRLimitThreshold = 400'000_step; 55 return Config; 56 }(); 57 58 namespace { 59 60 template <const AnalyzerOptions &Opts> 61 class Z3CrosscheckOracleTest : public testing::Test { 62 public: 63 Z3Decision interpretQueryResult(const Z3Result &Result) { 64 return Oracle.interpretQueryResult(Result); 65 } 66 67 private: 68 Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(Opts); 69 }; 70 71 using DefaultZ3CrosscheckOracleTest = Z3CrosscheckOracleTest<DefaultOpts>; 72 using LimitedZ3CrosscheckOracleTest = Z3CrosscheckOracleTest<LimitedOpts>; 73 74 TEST_F(DefaultZ3CrosscheckOracleTest, AcceptsFirstSAT) { 75 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step})); 76 } 77 TEST_F(LimitedZ3CrosscheckOracleTest, AcceptsFirstSAT) { 78 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step})); 79 } 80 81 TEST_F(DefaultZ3CrosscheckOracleTest, AcceptsSAT) { 82 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 83 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step})); 84 } 85 TEST_F(LimitedZ3CrosscheckOracleTest, AcceptsSAT) { 86 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 87 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step})); 88 } 89 90 TEST_F(DefaultZ3CrosscheckOracleTest, SATWhenItGoesOverTime) { 91 // Even if it times out, if it is SAT, we should accept it. 92 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 15'010_ms, 1000_step})); 93 } 94 TEST_F(LimitedZ3CrosscheckOracleTest, SATWhenItGoesOverTime) { 95 // Even if it times out, if it is SAT, we should accept it. 96 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 310_ms, 1000_step})); 97 } 98 99 TEST_F(DefaultZ3CrosscheckOracleTest, UNSATWhenItGoesOverTime) { 100 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 15'010_ms, 1000_step})); 101 } 102 TEST_F(LimitedZ3CrosscheckOracleTest, UNSATWhenItGoesOverTime) { 103 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step})); 104 } 105 106 TEST_F(DefaultZ3CrosscheckOracleTest, RejectsTimeout) { 107 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 108 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 109 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 15'010_ms, 1000_step})); 110 } 111 TEST_F(LimitedZ3CrosscheckOracleTest, RejectsTimeout) { 112 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 113 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 114 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 310_ms, 1000_step})); 115 } 116 117 TEST_F(DefaultZ3CrosscheckOracleTest, RejectsUNSATs) { 118 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 119 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 120 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 121 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 122 } 123 TEST_F(LimitedZ3CrosscheckOracleTest, RejectsUNSATs) { 124 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 125 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 126 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 127 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 128 } 129 130 // Testing cut heuristics of the two configurations: 131 // ================================================= 132 133 TEST_F(DefaultZ3CrosscheckOracleTest, RejectEQClassIfSpendsTooMuchTotalTime) { 134 // Simulate long queries, that barely doesn't trigger the timeout. 135 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step})); 136 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step})); 137 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step})); 138 } 139 TEST_F(LimitedZ3CrosscheckOracleTest, RejectEQClassIfSpendsTooMuchTotalTime) { 140 // Simulate long queries, that barely doesn't trigger the timeout. 141 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step})); 142 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step})); 143 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 290_ms, 1000_step})); 144 } 145 146 TEST_F(DefaultZ3CrosscheckOracleTest, SATWhenItSpendsTooMuchTotalTime) { 147 // Simulate long queries, that barely doesn't trigger the timeout. 148 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step})); 149 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 14'990_ms, 1000_step})); 150 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 14'990_ms, 1000_step})); 151 } 152 TEST_F(LimitedZ3CrosscheckOracleTest, SATWhenItSpendsTooMuchTotalTime) { 153 // Simulate long queries, that barely doesn't trigger the timeout. 154 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step})); 155 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step})); 156 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 290_ms, 1000_step})); 157 } 158 159 // Z3CrosscheckEQClassTimeoutThreshold is disabled in default configuration, so 160 // it doesn't make sense to test that. 161 TEST_F(LimitedZ3CrosscheckOracleTest, RejectEQClassIfAttemptsManySmallQueries) { 162 // Simulate quick, but many queries: 35 quick UNSAT queries. 163 // 35*20ms = 700ms, which is equal to the 700ms threshold. 164 for (int i = 0; i < 35; ++i) { 165 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step})); 166 } 167 // Do one more to trigger the heuristic. 168 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 1_ms, 1000_step})); 169 } 170 171 // Z3CrosscheckEQClassTimeoutThreshold is disabled in default configuration, so 172 // it doesn't make sense to test that. 173 TEST_F(LimitedZ3CrosscheckOracleTest, SATWhenItAttemptsManySmallQueries) { 174 // Simulate quick, but many queries: 35 quick UNSAT queries. 175 // 35*20ms = 700ms, which is equal to the 700ms threshold. 176 for (int i = 0; i < 35; ++i) { 177 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step})); 178 } 179 // Do one more to trigger the heuristic, but given this was SAT, we still 180 // accept the query. 181 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 200_ms, 1000_step})); 182 } 183 184 // Z3CrosscheckRLimitThreshold is disabled in default configuration, so it 185 // doesn't make sense to test that. 186 TEST_F(LimitedZ3CrosscheckOracleTest, RejectEQClassIfExhaustsRLimit) { 187 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 188 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 189 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 25_ms, 405'000_step})); 190 } 191 192 // Z3CrosscheckRLimitThreshold is disabled in default configuration, so it 193 // doesn't make sense to test that. 194 TEST_F(LimitedZ3CrosscheckOracleTest, SATWhenItExhaustsRLimit) { 195 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 196 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 197 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 405'000_step})); 198 } 199 200 // Demonstrate the weaknesses of the default configuration: 201 // ======================================================== 202 203 TEST_F(DefaultZ3CrosscheckOracleTest, ManySlowQueriesHangTheAnalyzer) { 204 // Simulate many slow queries: 250 slow UNSAT queries. 205 // 250*14000ms = 3500s, ~1 hour. Since we disabled the total time limitation, 206 // this eqclass would take roughly 1 hour to process. 207 // It doesn't matter what rlimit the queries consume. 208 for (int i = 0; i < 250; ++i) { 209 ASSERT_EQ(RejectReport, 210 interpretQueryResult({UNSAT, 14'000_ms, 1'000'000_step})); 211 } 212 } 213 214 } // namespace 215