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 42 Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result, 43 const AnalyzerOptions &Opts) 44 : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result), 45 Opts(Opts) {} 46 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 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 112 Z3CrosscheckVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &, 113 PathSensitiveBugReport &) { 114 addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false); 115 return nullptr; 116 } 117 118 void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const { 119 static int Tag = 0; 120 ID.AddPointer(&Tag); 121 } 122 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