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 = SMTConv::getRangeExpr(
79 Solver&: RefutationSolver, Ctx, Sym, From: RangeIt->From(), To: RangeIt->To(),
80 /*InRange=*/true);
81 while ((++RangeIt) != Range.end()) {
82 SMTConstraints = RefutationSolver->mkOr(
83 LHS: SMTConstraints, RHS: SMTConv::getRangeExpr(Solver&: RefutationSolver, Ctx, Sym,
84 From: RangeIt->From(), To: RangeIt->To(),
85 /*InRange=*/true));
86 }
87 RefutationSolver->addConstraint(Exp: 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: IsSAT,
102 .Z3QueryTimeMilliseconds: static_cast<unsigned>((End - Start) * 1000),
103 .UsedRLimit: 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(a: MinQueryTimeAcrossAttempts, b: Result.Z3QueryTimeMilliseconds);
113 if (Result.IsSAT.has_value())
114 return;
115 }
116}
117
118void Z3CrosscheckVisitor::addConstraints(
119 const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
120 // Collect new constraints
121 ConstraintMap NewCs = getConstraintMap(State: 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(K: Sym)) {
127 // This symbol is new, just add the constraint.
128 Constraints = CF.add(Old: Constraints, K: Sym, D: Range);
129 } else if (OverwriteConstraintsOnExistingSyms) {
130 // Overwrite the associated constraint of the Symbol.
131 Constraints = CF.remove(Old: Constraints, K: Sym);
132 Constraints = CF.add(Old: Constraints, K: Sym, D: Range);
133 }
134 }
135}
136
137PathDiagnosticPieceRef
138Z3CrosscheckVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &,
139 PathSensitiveBugReport &) {
140 addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false);
141 return nullptr;
142}
143
144void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const {
145 static int Tag = 0;
146 ID.AddPointer(Ptr: &Tag);
147}
148
149Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
150 const Z3CrosscheckVisitor::Z3Result &Query) {
151 ++NumZ3QueriesDone;
152 AccumulatedZ3QueryTimeInEqClass += Query.Z3QueryTimeMilliseconds;
153 TimeSpentSolvingZ3Queries += Query.Z3QueryTimeMilliseconds;
154 MaxTimeSpentSolvingZ3Queries.updateMax(Value: 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