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 == 400'000); 42 assert(Config.Z3CrosscheckTimeoutThreshold == 300_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 namespace { 51 52 class Z3CrosscheckOracleTest : public testing::Test { 53 public: 54 Z3Decision interpretQueryResult(const Z3Result &Result) { 55 return Oracle.interpretQueryResult(Result); 56 } 57 58 private: 59 Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(DefaultOpts); 60 }; 61 62 TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) { 63 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step})); 64 } 65 66 TEST_F(Z3CrosscheckOracleTest, AcceptsSAT) { 67 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 68 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step})); 69 } 70 71 TEST_F(Z3CrosscheckOracleTest, SATWhenItGoesOverTime) { 72 // Even if it times out, if it is SAT, we should accept it. 73 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 310_ms, 1000_step})); 74 } 75 76 TEST_F(Z3CrosscheckOracleTest, UNSATWhenItGoesOverTime) { 77 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step})); 78 } 79 80 TEST_F(Z3CrosscheckOracleTest, RejectsTimeout) { 81 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 82 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 83 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 310_ms, 1000_step})); 84 } 85 86 TEST_F(Z3CrosscheckOracleTest, RejectsUNSATs) { 87 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 88 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 89 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 90 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 91 } 92 93 // Testing cut heuristics: 94 // ======================= 95 96 TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfSpendsTooMuchTotalTime) { 97 // Simulate long queries, that barely doesn't trigger the timeout. 98 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step})); 99 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step})); 100 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 290_ms, 1000_step})); 101 } 102 103 TEST_F(Z3CrosscheckOracleTest, SATWhenItSpendsTooMuchTotalTime) { 104 // Simulate long queries, that barely doesn't trigger the timeout. 105 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step})); 106 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step})); 107 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 290_ms, 1000_step})); 108 } 109 110 TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfAttemptsManySmallQueries) { 111 // Simulate quick, but many queries: 35 quick UNSAT queries. 112 // 35*20ms = 700ms, which is equal to the 700ms threshold. 113 for (int i = 0; i < 35; ++i) { 114 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step})); 115 } 116 // Do one more to trigger the heuristic. 117 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 1_ms, 1000_step})); 118 } 119 120 TEST_F(Z3CrosscheckOracleTest, SATWhenIfAttemptsManySmallQueries) { 121 // Simulate quick, but many queries: 35 quick UNSAT queries. 122 // 35*20ms = 700ms, which is equal to the 700ms threshold. 123 for (int i = 0; i < 35; ++i) { 124 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step})); 125 } 126 // Do one more to trigger the heuristic, but given this was SAT, we still 127 // accept the query. 128 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 200_ms, 1000_step})); 129 } 130 131 TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfExhaustsRLimit) { 132 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 133 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 134 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 25_ms, 405'000_step})); 135 } 136 137 TEST_F(Z3CrosscheckOracleTest, SATWhenItExhaustsRLimit) { 138 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 139 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); 140 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 405'000_step})); 141 } 142 143 } // namespace 144