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.
28STAT_COUNTER(NumZ3QueriesDone, "Number of Z3 queries done");
29STAT_COUNTER(NumTimesZ3TimedOut, "Number of times Z3 query timed out");
30STAT_COUNTER(NumTimesZ3ExhaustedRLimit,
31 "Number of times Z3 query exhausted the rlimit");
32STAT_COUNTER(
33 NumTimesZ3SpendsTooMuchTimeOnASingleEQClass,
34 "Number of times report equivalenece class was cut because it spent "
35 "too much time in Z3");
36
37STAT_COUNTER(NumTimesZ3QueryAcceptsReport,
38 "Number of Z3 queries accepting a report");
39STAT_COUNTER(NumTimesZ3QueryRejectReport,
40 "Number of Z3 queries rejecting a report");
41STAT_COUNTER(NumTimesZ3QueryRejectEQClass,
42 "Number of times rejecting an report equivalenece class");
43
44STAT_COUNTER(TimeSpentSolvingZ3Queries,
45 "Total time spent solving Z3 queries excluding retries");
46STAT_MAX(MaxTimeSpentSolvingZ3Queries,
47 "Max time spent solving a Z3 query excluding retries");
48
49using namespace clang;
50using namespace ento;
51
52Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,
53 const AnalyzerOptions &Opts)
54 : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result),
55 Opts(Opts) {}
56
57void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
58 const ExplodedNode *EndPathNode,
59 PathSensitiveBugReport &BR) {
60 // Collect new constraints
61 addConstraints(N: EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
62
63 // Create a refutation manager
64 llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
65 if (Opts.Z3CrosscheckRLimitThreshold)
66 RefutationSolver->setUnsignedParam(Key: "rlimit",
67 Value: Opts.Z3CrosscheckRLimitThreshold);
68 if (Opts.Z3CrosscheckTimeoutThreshold)
69 RefutationSolver->setUnsignedParam(Key: "timeout",
70 Value: 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 =
79 SMTConv::getRangeExpr(Solver&: RefutationSolver, Ctx, Sym, From: RangeIt->From(),
80 To: RangeIt->To(),
81 /*InRange=*/true)
82 .value();
83 while ((++RangeIt) != Range.end()) {
84 SMTConstraints = RefutationSolver->mkOr(
85 LHS: SMTConstraints, RHS: SMTConv::getRangeExpr(Solver&: RefutationSolver, Ctx, Sym,
86 From: RangeIt->From(), To: RangeIt->To(),
87 /*InRange=*/true)
88 .value());
89 }
90 RefutationSolver->addConstraint(Exp: SMTConstraints);
91 }
92
93 auto GetUsedRLimit = [](const llvm::SMTSolverRef &Solver) {
94 return Solver->getStatistics()->getUnsigned("rlimit count");
95 };
96
97 auto AttemptOnce = [&](const llvm::SMTSolverRef &Solver) -> Z3Result {
98 auto getCurrentTime = llvm::TimeRecord::getCurrentTime;
99 unsigned InitialRLimit = GetUsedRLimit(Solver);
100 double Start = getCurrentTime(/*Start=*/true).getWallTime();
101 std::optional<bool> IsSAT = Solver->check();
102 double End = getCurrentTime(/*Start=*/false).getWallTime();
103 return {
104 .IsSAT: IsSAT,
105 .Z3QueryTimeMilliseconds: static_cast<unsigned>((End - Start) * 1000),
106 .UsedRLimit: GetUsedRLimit(Solver) - InitialRLimit,
107 };
108 };
109
110 // And check for satisfiability
111 unsigned MinQueryTimeAcrossAttempts = std::numeric_limits<unsigned>::max();
112 for (unsigned I = 0; I < Opts.Z3CrosscheckMaxAttemptsPerQuery; ++I) {
113 Result = AttemptOnce(RefutationSolver);
114 Result.Z3QueryTimeMilliseconds =
115 std::min(a: MinQueryTimeAcrossAttempts, b: Result.Z3QueryTimeMilliseconds);
116 if (Result.IsSAT.has_value())
117 return;
118 }
119}
120
121void Z3CrosscheckVisitor::addConstraints(
122 const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
123 // Collect new constraints
124 ConstraintMap NewCs = getConstraintMap(State: N->getState());
125 ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>();
126
127 // Add constraints if we don't have them yet
128 for (auto const &[Sym, Range] : NewCs) {
129 if (!Constraints.contains(K: Sym)) {
130 // This symbol is new, just add the constraint.
131 Constraints = CF.add(Old: Constraints, K: Sym, D: Range);
132 } else if (OverwriteConstraintsOnExistingSyms) {
133 // Overwrite the associated constraint of the Symbol.
134 Constraints = CF.remove(Old: Constraints, K: Sym);
135 Constraints = CF.add(Old: Constraints, K: Sym, D: Range);
136 }
137 }
138}
139
140PathDiagnosticPieceRef
141Z3CrosscheckVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &,
142 PathSensitiveBugReport &) {
143 addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false);
144 return nullptr;
145}
146
147void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const {
148 static int Tag = 0;
149 ID.AddPointer(Ptr: &Tag);
150}
151
152Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
153 const Z3CrosscheckVisitor::Z3Result &Query) {
154 ++NumZ3QueriesDone;
155 AccumulatedZ3QueryTimeInEqClass += Query.Z3QueryTimeMilliseconds;
156 TimeSpentSolvingZ3Queries += Query.Z3QueryTimeMilliseconds;
157 MaxTimeSpentSolvingZ3Queries.updateMax(Value: Query.Z3QueryTimeMilliseconds);
158
159 if (Query.IsSAT && Query.IsSAT.value()) {
160 ++NumTimesZ3QueryAcceptsReport;
161 return AcceptReport;
162 }
163
164 // Suggest cutting the EQClass if certain heuristics trigger.
165 if (Opts.Z3CrosscheckTimeoutThreshold &&
166 Query.Z3QueryTimeMilliseconds >= Opts.Z3CrosscheckTimeoutThreshold) {
167 ++NumTimesZ3TimedOut;
168 ++NumTimesZ3QueryRejectEQClass;
169 return RejectEQClass;
170 }
171
172 if (Opts.Z3CrosscheckRLimitThreshold &&
173 Query.UsedRLimit >= Opts.Z3CrosscheckRLimitThreshold) {
174 ++NumTimesZ3ExhaustedRLimit;
175 ++NumTimesZ3QueryRejectEQClass;
176 return RejectEQClass;
177 }
178
179 if (Opts.Z3CrosscheckEQClassTimeoutThreshold &&
180 AccumulatedZ3QueryTimeInEqClass >
181 Opts.Z3CrosscheckEQClassTimeoutThreshold) {
182 ++NumTimesZ3SpendsTooMuchTimeOnASingleEQClass;
183 ++NumTimesZ3QueryRejectEQClass;
184 return RejectEQClass;
185 }
186
187 // If no cutoff heuristics trigger, and the report is "unsat" or "undef",
188 // then reject the report.
189 ++NumTimesZ3QueryRejectReport;
190 return RejectReport;
191}
192