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
13using namespace clang;
14using namespace ento;
15
16using Z3Result = Z3CrosscheckVisitor::Z3Result;
17using Z3Decision = Z3CrosscheckOracle::Z3Decision;
18
19static constexpr Z3Decision AcceptReport = Z3Decision::AcceptReport;
20static constexpr Z3Decision RejectReport = Z3Decision::RejectReport;
21static constexpr Z3Decision RejectEQClass = Z3Decision::RejectEQClass;
22
23static constexpr std::optional<bool> SAT = true;
24static constexpr std::optional<bool> UNSAT = false;
25static constexpr std::optional<bool> UNDEF = std::nullopt;
26
27static unsigned operator""_ms(unsigned long long ms) { return ms; }
28static unsigned operator""_step(unsigned long long rlimit) { return rlimit; }
29
30static 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
50static 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
58namespace {
59
60template <const AnalyzerOptions &Opts>
61class Z3CrosscheckOracleTest : public testing::Test {
62public:
63 Z3Decision interpretQueryResult(const Z3Result &Result) {
64 return Oracle.interpretQueryResult(Meta: Result);
65 }
66
67private:
68 Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(Opts);
69};
70
71using DefaultZ3CrosscheckOracleTest = Z3CrosscheckOracleTest<DefaultOpts>;
72using LimitedZ3CrosscheckOracleTest = Z3CrosscheckOracleTest<LimitedOpts>;
73
74TEST_F(DefaultZ3CrosscheckOracleTest, AcceptsFirstSAT) {
75 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
76}
77TEST_F(LimitedZ3CrosscheckOracleTest, AcceptsFirstSAT) {
78 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
79}
80
81TEST_F(DefaultZ3CrosscheckOracleTest, AcceptsSAT) {
82 ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
83 ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
84}
85TEST_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
90TEST_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}
94TEST_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
99TEST_F(DefaultZ3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
100 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 15'010_ms, 1000_step}));
101}
102TEST_F(LimitedZ3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
103 ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step}));
104}
105
106TEST_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}
111TEST_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
117TEST_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}
123TEST_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
133TEST_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}
139TEST_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
146TEST_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}
152TEST_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.
161TEST_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.
173TEST_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.
186TEST_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.
194TEST_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
203TEST_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

source code of clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp