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
24STATISTIC(NumZ3QueriesDone, "Number of Z3 queries done");
25STATISTIC(NumTimesZ3TimedOut, "Number of times Z3 query timed out");
26STATISTIC(NumTimesZ3ExhaustedRLimit,
27 "Number of times Z3 query exhausted the rlimit");
28STATISTIC(NumTimesZ3SpendsTooMuchTimeOnASingleEQClass,
29 "Number of times report equivalenece class was cut because it spent "
30 "too much time in Z3");
31
32STATISTIC(NumTimesZ3QueryAcceptsReport,
33 "Number of Z3 queries accepting a report");
34STATISTIC(NumTimesZ3QueryRejectReport,
35 "Number of Z3 queries rejecting a report");
36STATISTIC(NumTimesZ3QueryRejectEQClass,
37 "Number of times rejecting an report equivalenece class");
38
39using namespace clang;
40using namespace ento;
41
42Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,
43 const AnalyzerOptions &Opts)
44 : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result),
45 Opts(Opts) {}
46
47void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
48 const ExplodedNode *EndPathNode,
49 PathSensitiveBugReport &BR) {
50 // Collect new constraints
51 addConstraints(N: EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
52
53 // Create a refutation manager
54 llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
55 if (Opts.Z3CrosscheckRLimitThreshold)
56 RefutationSolver->setUnsignedParam(Key: "rlimit",
57 Value: Opts.Z3CrosscheckRLimitThreshold);
58 if (Opts.Z3CrosscheckTimeoutThreshold)
59 RefutationSolver->setUnsignedParam(Key: "timeout",
60 Value: 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 Solver&: RefutationSolver, Ctx, Sym, From: RangeIt->From(), To: RangeIt->To(),
70 /*InRange=*/true);
71 while ((++RangeIt) != Range.end()) {
72 SMTConstraints = RefutationSolver->mkOr(
73 LHS: SMTConstraints, RHS: SMTConv::getRangeExpr(Solver&: RefutationSolver, Ctx, Sym,
74 From: RangeIt->From(), To: RangeIt->To(),
75 /*InRange=*/true));
76 }
77 RefutationSolver->addConstraint(Exp: 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: IsSAT,
87 .Z3QueryTimeMilliseconds: static_cast<unsigned>(Diff.getWallTime() * 1000),
88 .UsedRLimit: RefutationSolver->getStatistics()->getUnsigned("rlimit count"),
89 };
90}
91
92void Z3CrosscheckVisitor::addConstraints(
93 const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
94 // Collect new constraints
95 ConstraintMap NewCs = getConstraintMap(State: 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(K: Sym)) {
101 // This symbol is new, just add the constraint.
102 Constraints = CF.add(Old: Constraints, K: Sym, D: Range);
103 } else if (OverwriteConstraintsOnExistingSyms) {
104 // Overwrite the associated constraint of the Symbol.
105 Constraints = CF.remove(Old: Constraints, K: Sym);
106 Constraints = CF.add(Old: Constraints, K: Sym, D: Range);
107 }
108 }
109}
110
111PathDiagnosticPieceRef
112Z3CrosscheckVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &,
113 PathSensitiveBugReport &) {
114 addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false);
115 return nullptr;
116}
117
118void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const {
119 static int Tag = 0;
120 ID.AddPointer(Ptr: &Tag);
121}
122
123Z3CrosscheckOracle::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