Skip to content

Commit ea8e328

Browse files
Szelethussteakhal
andauthored
[analyzer][Z3] Restore the original timeout of 15s (#118291)
Discussion here: https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520/15?u=szelethus The original patch, #97298 introduced new timeouts backed by thorough testing and measurements to keep the running time of Z3 within reasonable limits. The measurements also showed that only certain reports and certain TUs were responsible for the poor performance of Z3 refutation. Unfortunately, it seems like that on machines with different characteristics (slower machines) the current timeouts don't just axe 0.01% of reports, but many more as well. Considering that timeouts are inherently nondeterministic as a cutoff point, this lead reports sets being vastly different on the same projects with the same configuration. The discussion link shows that all configurations introduced in the patch with their default values lead to severa nondeterminism of the analyzer. As we, and others use the analyzer as a gating tool for PRs, we should revert to the original defaults. We should respect that * There are still parts of the analyzer that are either proven or suspected to contain nondeterministic code (like pointer sets), * A 15s timeout is more likely to hit the same reports every time on a wider range of machines, but is still inherently nondeterministic, but an infinite timeout leads to the tool hanging, * If you measure the performance of the analyzer on your machines, you can and should achieve some speedup with little or no observable nondeterminism. --------- Co-authored-by: Balazs Benics <[email protected]>
1 parent fb8df8c commit ea8e328

File tree

3 files changed

+105
-25
lines changed

3 files changed

+105
-25
lines changed

clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def

Lines changed: 14 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -189,20 +189,29 @@ ANALYZER_OPTION(
189189
"crosscheck-with-z3-eqclass-timeout-threshold",
190190
"Set a timeout for bug report equivalence classes in milliseconds. "
191191
"If we exhaust this threshold, we will drop the bug report eqclass "
192-
"instead of doing more Z3 queries. Set 0 for no timeout.", 700)
192+
"instead of doing more Z3 queries. Setting this to 700 ms in conjunction "
193+
"with \"crosscheck-with-z3-timeout-threshold\" of 300 ms, would nicely "
194+
"guarantee that no bug report equivalence class can take longer than "
195+
"1 second, effectively mitigating Z3 hangs during refutation. "
196+
"Set 0 for no timeout.", 0)
193197

194198
ANALYZER_OPTION(
195199
unsigned, Z3CrosscheckTimeoutThreshold,
196200
"crosscheck-with-z3-timeout-threshold",
197201
"Set a timeout for individual Z3 queries in milliseconds. "
198-
"Set 0 for no timeout.", 300)
202+
"On fast machines, 300 worked well in some cases. "
203+
"The lower it is, the higher the chances of having flaky issues. "
204+
"Having no timeout may hang the analyzer indefinitely. "
205+
"Set 0 for no timeout.", 15'000)
199206

200207
ANALYZER_OPTION(
201208
unsigned, Z3CrosscheckRLimitThreshold,
202209
"crosscheck-with-z3-rlimit-threshold",
203-
"Set the Z3 resource limit threshold. This sets a deterministic cutoff "
204-
"point for Z3 queries, as longer queries usually consume more resources. "
205-
"Set 0 for unlimited.", 400'000)
210+
"Set the Z3 resource limit threshold. This sets a supposedly deterministic "
211+
"cutoff point for Z3 queries, as longer queries usually consume more "
212+
"resources. "
213+
"400'000 should on average make Z3 queries run for up to 100ms on modern "
214+
"hardware. Set 0 for unlimited.", 0)
206215

207216
ANALYZER_OPTION(bool, ShouldReportIssuesInMainSourceFile,
208217
"report-in-main-source-file",

clang/test/Analysis/analyzer-config.c

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -40,9 +40,9 @@
4040
// CHECK-NEXT: cplusplus.Move:WarnOn = KnownsAndLocals
4141
// CHECK-NEXT: cplusplus.SmartPtrModeling:ModelSmartPtrDereference = false
4242
// CHECK-NEXT: crosscheck-with-z3 = false
43-
// CHECK-NEXT: crosscheck-with-z3-eqclass-timeout-threshold = 700
44-
// CHECK-NEXT: crosscheck-with-z3-rlimit-threshold = 400000
45-
// CHECK-NEXT: crosscheck-with-z3-timeout-threshold = 300
43+
// CHECK-NEXT: crosscheck-with-z3-eqclass-timeout-threshold = 0
44+
// CHECK-NEXT: crosscheck-with-z3-rlimit-threshold = 0
45+
// CHECK-NEXT: crosscheck-with-z3-timeout-threshold = 15000
4646
// CHECK-NEXT: ctu-dir = ""
4747
// CHECK-NEXT: ctu-import-cpp-threshold = 8
4848
// CHECK-NEXT: ctu-import-threshold = 24

clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp

Lines changed: 88 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -38,76 +38,127 @@ static const AnalyzerOptions DefaultOpts = [] {
3838

3939
// Remember to update the tests in this file when these values change.
4040
// Also update the doc comment of `interpretQueryResult`.
41-
assert(Config.Z3CrosscheckRLimitThreshold == 400'000);
42-
assert(Config.Z3CrosscheckTimeoutThreshold == 300_ms);
41+
assert(Config.Z3CrosscheckRLimitThreshold == 0);
42+
assert(Config.Z3CrosscheckTimeoutThreshold == 15'000_ms);
4343
// Usually, when the timeout/rlimit threshold is reached, Z3 only slightly
4444
// overshoots until it realizes that it overshoot and needs to back off.
4545
// Consequently, the measured timeout should be fairly close to the threshold.
4646
// Same reasoning applies to the rlimit too.
4747
return Config;
4848
}();
4949

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+
5058
namespace {
5159

60+
template <const AnalyzerOptions &Opts>
5261
class Z3CrosscheckOracleTest : public testing::Test {
5362
public:
5463
Z3Decision interpretQueryResult(const Z3Result &Result) {
5564
return Oracle.interpretQueryResult(Result);
5665
}
5766

5867
private:
59-
Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(DefaultOpts);
68+
Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(Opts);
6069
};
6170

62-
TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) {
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) {
6378
ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
6479
}
6580

66-
TEST_F(Z3CrosscheckOracleTest, AcceptsSAT) {
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) {
6786
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
6887
ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
6988
}
7089

71-
TEST_F(Z3CrosscheckOracleTest, SATWhenItGoesOverTime) {
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) {
7295
// Even if it times out, if it is SAT, we should accept it.
7396
ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 310_ms, 1000_step}));
7497
}
7598

76-
TEST_F(Z3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
99+
TEST_F(DefaultZ3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
100+
ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 15'010_ms, 1000_step}));
101+
}
102+
TEST_F(LimitedZ3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
77103
ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step}));
78104
}
79105

80-
TEST_F(Z3CrosscheckOracleTest, RejectsTimeout) {
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) {
81112
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
82113
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
83114
ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 310_ms, 1000_step}));
84115
}
85116

86-
TEST_F(Z3CrosscheckOracleTest, RejectsUNSATs) {
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) {
87124
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
88125
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
89126
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
90127
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
91128
}
92129

93-
// Testing cut heuristics:
94-
// =======================
130+
// Testing cut heuristics of the two configurations:
131+
// =================================================
95132

96-
TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfSpendsTooMuchTotalTime) {
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) {
97140
// Simulate long queries, that barely doesn't trigger the timeout.
98141
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
99142
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
100143
ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
101144
}
102145

103-
TEST_F(Z3CrosscheckOracleTest, SATWhenItSpendsTooMuchTotalTime) {
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) {
104153
// Simulate long queries, that barely doesn't trigger the timeout.
105154
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
106155
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
107156
ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 290_ms, 1000_step}));
108157
}
109158

110-
TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfAttemptsManySmallQueries) {
159+
// Z3CrosscheckEQClassTimeoutThreshold is disabled in default configuration, so
160+
// it doesn't make sense to test that.
161+
TEST_F(LimitedZ3CrosscheckOracleTest, RejectEQClassIfAttemptsManySmallQueries) {
111162
// Simulate quick, but many queries: 35 quick UNSAT queries.
112163
// 35*20ms = 700ms, which is equal to the 700ms threshold.
113164
for (int i = 0; i < 35; ++i) {
@@ -117,7 +168,9 @@ TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfAttemptsManySmallQueries) {
117168
ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 1_ms, 1000_step}));
118169
}
119170

120-
TEST_F(Z3CrosscheckOracleTest, SATWhenIfAttemptsManySmallQueries) {
171+
// Z3CrosscheckEQClassTimeoutThreshold is disabled in default configuration, so
172+
// it doesn't make sense to test that.
173+
TEST_F(LimitedZ3CrosscheckOracleTest, SATWhenItAttemptsManySmallQueries) {
121174
// Simulate quick, but many queries: 35 quick UNSAT queries.
122175
// 35*20ms = 700ms, which is equal to the 700ms threshold.
123176
for (int i = 0; i < 35; ++i) {
@@ -128,16 +181,34 @@ TEST_F(Z3CrosscheckOracleTest, SATWhenIfAttemptsManySmallQueries) {
128181
ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 200_ms, 1000_step}));
129182
}
130183

131-
TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfExhaustsRLimit) {
184+
// Z3CrosscheckRLimitThreshold is disabled in default configuration, so it
185+
// doesn't make sense to test that.
186+
TEST_F(LimitedZ3CrosscheckOracleTest, RejectEQClassIfExhaustsRLimit) {
132187
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
133188
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
134189
ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 25_ms, 405'000_step}));
135190
}
136191

137-
TEST_F(Z3CrosscheckOracleTest, SATWhenItExhaustsRLimit) {
192+
// Z3CrosscheckRLimitThreshold is disabled in default configuration, so it
193+
// doesn't make sense to test that.
194+
TEST_F(LimitedZ3CrosscheckOracleTest, SATWhenItExhaustsRLimit) {
138195
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
139196
ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
140197
ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 405'000_step}));
141198
}
142199

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+
143214
} // namespace

0 commit comments

Comments
 (0)