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