[analyzer] Harden safeguards for Z3 query times · llvm/llvm-project@eacc3b3 (original) (raw)
`@@ -12,26 +12,37 @@
`
12
12
`//===----------------------------------------------------------------------===//
`
13
13
``
14
14
`#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
`
``
15
`+
#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
`
15
16
`#include "clang/StaticAnalyzer/Core/BugReporter/BugReporter.h"
`
16
17
`#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
`
17
18
`#include "llvm/ADT/Statistic.h"
`
18
19
`#include "llvm/Support/SMTAPI.h"
`
``
20
`+
#include "llvm/Support/Timer.h"
`
19
21
``
20
22
`#define DEBUG_TYPE "Z3CrosscheckOracle"
`
21
23
``
22
24
`STATISTIC(NumZ3QueriesDone, "Number of Z3 queries done");
`
23
25
`STATISTIC(NumTimesZ3TimedOut, "Number of times Z3 query timed out");
`
``
26
`+
STATISTIC(NumTimesZ3ExhaustedRLimit,
`
``
27
`+
"Number of times Z3 query exhausted the rlimit");
`
``
28
`+
STATISTIC(NumTimesZ3SpendsTooMuchTimeOnASingleEQClass,
`
``
29
`+
"Number of times report equivalenece class was cut because it spent "
`
``
30
`+
"too much time in Z3");
`
24
31
``
25
32
`STATISTIC(NumTimesZ3QueryAcceptsReport,
`
26
33
`"Number of Z3 queries accepting a report");
`
27
34
`STATISTIC(NumTimesZ3QueryRejectReport,
`
28
35
`"Number of Z3 queries rejecting a report");
`
``
36
`+
STATISTIC(NumTimesZ3QueryRejectEQClass,
`
``
37
`+
"Number of times rejecting an report equivalenece class");
`
29
38
``
30
39
`using namespace clang;
`
31
40
`using namespace ento;
`
32
41
``
33
``
`-
Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result)
`
34
``
`-
: Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result) {}
`
``
42
`+
Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,
`
``
43
`+
const AnalyzerOptions &Opts)
`
``
44
`+
: Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result),
`
``
45
`+
Opts(Opts) {}
`
35
46
``
36
47
`void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
`
37
48
`const ExplodedNode *EndPathNode,
`
`@@ -41,8 +52,12 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
`
41
52
``
42
53
`// Create a refutation manager
`
43
54
` llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
`
44
``
`-
RefutationSolver->setBoolParam("model", true); // Enable model finding
`
45
``
`-
RefutationSolver->setUnsignedParam("timeout", 15000); // ms
`
``
55
`+
if (Opts.Z3CrosscheckRLimitThreshold)
`
``
56
`+
RefutationSolver->setUnsignedParam("rlimit",
`
``
57
`+
Opts.Z3CrosscheckRLimitThreshold);
`
``
58
`+
if (Opts.Z3CrosscheckTimeoutThreshold)
`
``
59
`+
RefutationSolver->setUnsignedParam("timeout",
`
``
60
`+
Opts.Z3CrosscheckTimeoutThreshold); // ms
`
46
61
``
47
62
` ASTContext &Ctx = BRC.getASTContext();
`
48
63
``
`@@ -63,8 +78,15 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
`
63
78
` }
`
64
79
``
65
80
`// And check for satisfiability
`
``
81
`+
llvm::TimeRecord Start = llvm::TimeRecord::getCurrentTime(/Start=/true);
`
66
82
` std::optional IsSAT = RefutationSolver->check();
`
67
``
`-
Result = Z3Result{IsSAT};
`
``
83
`+
llvm::TimeRecord Diff = llvm::TimeRecord::getCurrentTime(/Start=/false);
`
``
84
`+
Diff -= Start;
`
``
85
`+
Result = Z3Result{
`
``
86
`+
IsSAT,
`
``
87
`+
static_cast(Diff.getWallTime() * 1000),
`
``
88
`+
RefutationSolver->getStatistics()->getUnsigned("rlimit count"),
`
``
89
`+
};
`
68
90
`}
`
69
91
``
70
92
`void Z3CrosscheckVisitor::addConstraints(
`
`@@ -101,18 +123,38 @@ void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const {
`
101
123
`Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
`
102
124
`const Z3CrosscheckVisitor::Z3Result &Query) {
`
103
125
` ++NumZ3QueriesDone;
`
``
126
`+
AccumulatedZ3QueryTimeInEqClass += Query.Z3QueryTimeMilliseconds;
`
104
127
``
105
``
`-
if (!Query.IsSAT.has_value()) {
`
106
``
`-
// For backward compatibility, let's accept the first timeout.
`
107
``
`-
++NumTimesZ3TimedOut;
`
``
128
`+
if (Query.IsSAT && Query.IsSAT.value()) {
`
``
129
`+
++NumTimesZ3QueryAcceptsReport;
`
108
130
`return AcceptReport;
`
109
131
` }
`
110
132
``
111
``
`-
if (Query.IsSAT.value()) {
`
112
``
`-
++NumTimesZ3QueryAcceptsReport;
`
113
``
`-
return AcceptReport; // sat
`
``
133
`+
// Suggest cutting the EQClass if certain heuristics trigger.
`
``
134
`+
if (Opts.Z3CrosscheckTimeoutThreshold &&
`
``
135
`+
Query.Z3QueryTimeMilliseconds >= Opts.Z3CrosscheckTimeoutThreshold) {
`
``
136
`+
++NumTimesZ3TimedOut;
`
``
137
`+
++NumTimesZ3QueryRejectEQClass;
`
``
138
`+
return RejectEQClass;
`
``
139
`+
}
`
``
140
+
``
141
`+
if (Opts.Z3CrosscheckRLimitThreshold &&
`
``
142
`+
Query.UsedRLimit >= Opts.Z3CrosscheckRLimitThreshold) {
`
``
143
`+
++NumTimesZ3ExhaustedRLimit;
`
``
144
`+
++NumTimesZ3QueryRejectEQClass;
`
``
145
`+
return RejectEQClass;
`
``
146
`+
}
`
``
147
+
``
148
`+
if (Opts.Z3CrosscheckEQClassTimeoutThreshold &&
`
``
149
`+
AccumulatedZ3QueryTimeInEqClass >
`
``
150
`+
Opts.Z3CrosscheckEQClassTimeoutThreshold) {
`
``
151
`+
++NumTimesZ3SpendsTooMuchTimeOnASingleEQClass;
`
``
152
`+
++NumTimesZ3QueryRejectEQClass;
`
``
153
`+
return RejectEQClass;
`
114
154
` }
`
115
155
``
``
156
`+
// If no cutoff heuristics trigger, and the report is "unsat" or "undef",
`
``
157
`+
// then reject the report.
`
116
158
` ++NumTimesZ3QueryRejectReport;
`
117
``
`-
return RejectReport; // unsat
`
``
159
`+
return RejectReport;
`
118
160
`}
`