1 //===- Z3CrosscheckVisitor.cpp - Crosscheck reports with Z3 -----*- C++ -*-===//
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 // This file declares the visitor and utilities around it for Z3 report
10 // refutation.
11 //
12 //===----------------------------------------------------------------------===//
13
14 #include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
15 #include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
16 #include "clang/StaticAnalyzer/Core/BugReporter/BugReporter.h"
17 #include "clang/StaticAnalyzer/Core/PathSensitive/EntryPointStats.h"
18 #include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
19 #include "llvm/Support/SMTAPI.h"
20 #include "llvm/Support/Timer.h"
21
22 #define DEBUG_TYPE "Z3CrosscheckOracle"
23
24 // Queries attempted at most `Z3CrosscheckMaxAttemptsPerQuery` number of times.
25 // Multiple `check()` calls might be called on the same query if previous
26 // attempts of the same query resulted in UNSAT for any reason. Each query is
27 // only counted once for these statistics, the retries are not accounted for.
28 STAT_COUNTER(NumZ3QueriesDone, "Number of Z3 queries done");
29 STAT_COUNTER(NumTimesZ3TimedOut, "Number of times Z3 query timed out");
30 STAT_COUNTER(NumTimesZ3ExhaustedRLimit,
31 "Number of times Z3 query exhausted the rlimit");
32 STAT_COUNTER(
33 NumTimesZ3SpendsTooMuchTimeOnASingleEQClass,
34 "Number of times report equivalenece class was cut because it spent "
35 "too much time in Z3");
36
37 STAT_COUNTER(NumTimesZ3QueryAcceptsReport,
38 "Number of Z3 queries accepting a report");
39 STAT_COUNTER(NumTimesZ3QueryRejectReport,
40 "Number of Z3 queries rejecting a report");
41 STAT_COUNTER(NumTimesZ3QueryRejectEQClass,
42 "Number of times rejecting an report equivalenece class");
43
44 STAT_COUNTER(TimeSpentSolvingZ3Queries,
45 "Total time spent solving Z3 queries excluding retries");
46 STAT_MAX(MaxTimeSpentSolvingZ3Queries,
47 "Max time spent solving a Z3 query excluding retries");
48
49 using namespace clang;
50 using namespace ento;
51
Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result & Result,const AnalyzerOptions & Opts)52 Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,
53 const AnalyzerOptions &Opts)
54 : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result),
55 Opts(Opts) {}
56
finalizeVisitor(BugReporterContext & BRC,const ExplodedNode * EndPathNode,PathSensitiveBugReport & BR)57 void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
58 const ExplodedNode *EndPathNode,
59 PathSensitiveBugReport &BR) {
60 // Collect new constraints
61 addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
62
63 // Create a refutation manager
64 llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
65 if (Opts.Z3CrosscheckRLimitThreshold)
66 RefutationSolver->setUnsignedParam("rlimit",
67 Opts.Z3CrosscheckRLimitThreshold);
68 if (Opts.Z3CrosscheckTimeoutThreshold)
69 RefutationSolver->setUnsignedParam("timeout",
70 Opts.Z3CrosscheckTimeoutThreshold); // ms
71
72 ASTContext &Ctx = BRC.getASTContext();
73
74 // Add constraints to the solver
75 for (const auto &[Sym, Range] : Constraints) {
76 auto RangeIt = Range.begin();
77
78 llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(
79 RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
80 /*InRange=*/true);
81 while ((++RangeIt) != Range.end()) {
82 SMTConstraints = RefutationSolver->mkOr(
83 SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
84 RangeIt->From(), RangeIt->To(),
85 /*InRange=*/true));
86 }
87 RefutationSolver->addConstraint(SMTConstraints);
88 }
89
90 auto GetUsedRLimit = [](const llvm::SMTSolverRef &Solver) {
91 return Solver->getStatistics()->getUnsigned("rlimit count");
92 };
93
94 auto AttemptOnce = [&](const llvm::SMTSolverRef &Solver) -> Z3Result {
95 auto getCurrentTime = llvm::TimeRecord::getCurrentTime;
96 unsigned InitialRLimit = GetUsedRLimit(Solver);
97 double Start = getCurrentTime(/*Start=*/true).getWallTime();
98 std::optional<bool> IsSAT = Solver->check();
99 double End = getCurrentTime(/*Start=*/false).getWallTime();
100 return {
101 IsSAT,
102 static_cast<unsigned>((End - Start) * 1000),
103 GetUsedRLimit(Solver) - InitialRLimit,
104 };
105 };
106
107 // And check for satisfiability
108 unsigned MinQueryTimeAcrossAttempts = std::numeric_limits<unsigned>::max();
109 for (unsigned I = 0; I < Opts.Z3CrosscheckMaxAttemptsPerQuery; ++I) {
110 Result = AttemptOnce(RefutationSolver);
111 Result.Z3QueryTimeMilliseconds =
112 std::min(MinQueryTimeAcrossAttempts, Result.Z3QueryTimeMilliseconds);
113 if (Result.IsSAT.has_value())
114 return;
115 }
116 }
117
addConstraints(const ExplodedNode * N,bool OverwriteConstraintsOnExistingSyms)118 void Z3CrosscheckVisitor::addConstraints(
119 const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
120 // Collect new constraints
121 ConstraintMap NewCs = getConstraintMap(N->getState());
122 ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>();
123
124 // Add constraints if we don't have them yet
125 for (auto const &[Sym, Range] : NewCs) {
126 if (!Constraints.contains(Sym)) {
127 // This symbol is new, just add the constraint.
128 Constraints = CF.add(Constraints, Sym, Range);
129 } else if (OverwriteConstraintsOnExistingSyms) {
130 // Overwrite the associated constraint of the Symbol.
131 Constraints = CF.remove(Constraints, Sym);
132 Constraints = CF.add(Constraints, Sym, Range);
133 }
134 }
135 }
136
137 PathDiagnosticPieceRef
VisitNode(const ExplodedNode * N,BugReporterContext &,PathSensitiveBugReport &)138 Z3CrosscheckVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &,
139 PathSensitiveBugReport &) {
140 addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false);
141 return nullptr;
142 }
143
Profile(llvm::FoldingSetNodeID & ID) const144 void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const {
145 static int Tag = 0;
146 ID.AddPointer(&Tag);
147 }
148
interpretQueryResult(const Z3CrosscheckVisitor::Z3Result & Query)149 Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
150 const Z3CrosscheckVisitor::Z3Result &Query) {
151 ++NumZ3QueriesDone;
152 AccumulatedZ3QueryTimeInEqClass += Query.Z3QueryTimeMilliseconds;
153 TimeSpentSolvingZ3Queries += Query.Z3QueryTimeMilliseconds;
154 MaxTimeSpentSolvingZ3Queries.updateMax(Query.Z3QueryTimeMilliseconds);
155
156 if (Query.IsSAT && Query.IsSAT.value()) {
157 ++NumTimesZ3QueryAcceptsReport;
158 return AcceptReport;
159 }
160
161 // Suggest cutting the EQClass if certain heuristics trigger.
162 if (Opts.Z3CrosscheckTimeoutThreshold &&
163 Query.Z3QueryTimeMilliseconds >= Opts.Z3CrosscheckTimeoutThreshold) {
164 ++NumTimesZ3TimedOut;
165 ++NumTimesZ3QueryRejectEQClass;
166 return RejectEQClass;
167 }
168
169 if (Opts.Z3CrosscheckRLimitThreshold &&
170 Query.UsedRLimit >= Opts.Z3CrosscheckRLimitThreshold) {
171 ++NumTimesZ3ExhaustedRLimit;
172 ++NumTimesZ3QueryRejectEQClass;
173 return RejectEQClass;
174 }
175
176 if (Opts.Z3CrosscheckEQClassTimeoutThreshold &&
177 AccumulatedZ3QueryTimeInEqClass >
178 Opts.Z3CrosscheckEQClassTimeoutThreshold) {
179 ++NumTimesZ3SpendsTooMuchTimeOnASingleEQClass;
180 ++NumTimesZ3QueryRejectEQClass;
181 return RejectEQClass;
182 }
183
184 // If no cutoff heuristics trigger, and the report is "unsat" or "undef",
185 // then reject the report.
186 ++NumTimesZ3QueryRejectReport;
187 return RejectReport;
188 }
189