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/SMTConv.h"
18 #include "llvm/ADT/Statistic.h"
19 #include "llvm/Support/SMTAPI.h"
20 #include "llvm/Support/Timer.h"
21
22 #define DEBUG_TYPE "Z3CrosscheckOracle"
23
24 STATISTIC(NumZ3QueriesDone, "Number of Z3 queries done");
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");
31
32 STATISTIC(NumTimesZ3QueryAcceptsReport,
33 "Number of Z3 queries accepting a report");
34 STATISTIC(NumTimesZ3QueryRejectReport,
35 "Number of Z3 queries rejecting a report");
36 STATISTIC(NumTimesZ3QueryRejectEQClass,
37 "Number of times rejecting an report equivalenece class");
38
39 using namespace clang;
40 using namespace ento;
41
Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result & Result,const AnalyzerOptions & Opts)42 Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,
43 const AnalyzerOptions &Opts)
44 : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result),
45 Opts(Opts) {}
46
finalizeVisitor(BugReporterContext & BRC,const ExplodedNode * EndPathNode,PathSensitiveBugReport & BR)47 void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
48 const ExplodedNode *EndPathNode,
49 PathSensitiveBugReport &BR) {
50 // Collect new constraints
51 addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
52
53 // Create a refutation manager
54 llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
55 if (Opts.Z3CrosscheckRLimitThreshold)
56 RefutationSolver->setUnsignedParam("rlimit",
57 Opts.Z3CrosscheckRLimitThreshold);
58 if (Opts.Z3CrosscheckTimeoutThreshold)
59 RefutationSolver->setUnsignedParam("timeout",
60 Opts.Z3CrosscheckTimeoutThreshold); // ms
61
62 ASTContext &Ctx = BRC.getASTContext();
63
64 // Add constraints to the solver
65 for (const auto &[Sym, Range] : Constraints) {
66 auto RangeIt = Range.begin();
67
68 llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(
69 RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
70 /*InRange=*/true);
71 while ((++RangeIt) != Range.end()) {
72 SMTConstraints = RefutationSolver->mkOr(
73 SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
74 RangeIt->From(), RangeIt->To(),
75 /*InRange=*/true));
76 }
77 RefutationSolver->addConstraint(SMTConstraints);
78 }
79
80 // And check for satisfiability
81 llvm::TimeRecord Start = llvm::TimeRecord::getCurrentTime(/*Start=*/true);
82 std::optional<bool> IsSAT = RefutationSolver->check();
83 llvm::TimeRecord Diff = llvm::TimeRecord::getCurrentTime(/*Start=*/false);
84 Diff -= Start;
85 Result = Z3Result{
86 IsSAT,
87 static_cast<unsigned>(Diff.getWallTime() * 1000),
88 RefutationSolver->getStatistics()->getUnsigned("rlimit count"),
89 };
90 }
91
addConstraints(const ExplodedNode * N,bool OverwriteConstraintsOnExistingSyms)92 void Z3CrosscheckVisitor::addConstraints(
93 const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
94 // Collect new constraints
95 ConstraintMap NewCs = getConstraintMap(N->getState());
96 ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>();
97
98 // Add constraints if we don't have them yet
99 for (auto const &[Sym, Range] : NewCs) {
100 if (!Constraints.contains(Sym)) {
101 // This symbol is new, just add the constraint.
102 Constraints = CF.add(Constraints, Sym, Range);
103 } else if (OverwriteConstraintsOnExistingSyms) {
104 // Overwrite the associated constraint of the Symbol.
105 Constraints = CF.remove(Constraints, Sym);
106 Constraints = CF.add(Constraints, Sym, Range);
107 }
108 }
109 }
110
111 PathDiagnosticPieceRef
VisitNode(const ExplodedNode * N,BugReporterContext &,PathSensitiveBugReport &)112 Z3CrosscheckVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &,
113 PathSensitiveBugReport &) {
114 addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false);
115 return nullptr;
116 }
117
Profile(llvm::FoldingSetNodeID & ID) const118 void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const {
119 static int Tag = 0;
120 ID.AddPointer(&Tag);
121 }
122
interpretQueryResult(const Z3CrosscheckVisitor::Z3Result & Query)123 Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
124 const Z3CrosscheckVisitor::Z3Result &Query) {
125 ++NumZ3QueriesDone;
126 AccumulatedZ3QueryTimeInEqClass += Query.Z3QueryTimeMilliseconds;
127
128 if (Query.IsSAT && Query.IsSAT.value()) {
129 ++NumTimesZ3QueryAcceptsReport;
130 return AcceptReport;
131 }
132
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;
154 }
155
156 // If no cutoff heuristics trigger, and the report is "unsat" or "undef",
157 // then reject the report.
158 ++NumTimesZ3QueryRejectReport;
159 return RejectReport;
160 }
161