189 lines · cpp
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-exception6//7//===----------------------------------------------------------------------===//8//9// This file declares the visitor and utilities around it for Z3 report10// 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 previous26// attempts of the same query resulted in UNSAT for any reason. Each query is27// 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 constraints61 addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);62 63 // Create a refutation manager64 llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();65 if (Opts.Z3CrosscheckRLimitThreshold)66 RefutationSolver->setUnsignedParam("rlimit",67 Opts.Z3CrosscheckRLimitThreshold);68 if (Opts.Z3CrosscheckTimeoutThreshold)69 RefutationSolver->setUnsignedParam("timeout",70 Opts.Z3CrosscheckTimeoutThreshold); // ms71 72 ASTContext &Ctx = BRC.getASTContext();73 74 // Add constraints to the solver75 for (const auto &[Sym, Range] : Constraints) {76 auto RangeIt = Range.begin();77 78 llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(79 RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),80 /*InRange=*/true);81 while ((++RangeIt) != Range.end()) {82 SMTConstraints = RefutationSolver->mkOr(83 SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,84 RangeIt->From(), RangeIt->To(),85 /*InRange=*/true));86 }87 RefutationSolver->addConstraint(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,102 static_cast<unsigned>((End - Start) * 1000),103 GetUsedRLimit(Solver) - InitialRLimit,104 };105 };106 107 // And check for satisfiability108 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(MinQueryTimeAcrossAttempts, 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 constraints121 ConstraintMap NewCs = getConstraintMap(N->getState());122 ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>();123 124 // Add constraints if we don't have them yet125 for (auto const &[Sym, Range] : NewCs) {126 if (!Constraints.contains(Sym)) {127 // This symbol is new, just add the constraint.128 Constraints = CF.add(Constraints, Sym, Range);129 } else if (OverwriteConstraintsOnExistingSyms) {130 // Overwrite the associated constraint of the Symbol.131 Constraints = CF.remove(Constraints, Sym);132 Constraints = CF.add(Constraints, Sym, Range);133 }134 }135}136 137PathDiagnosticPieceRef138Z3CrosscheckVisitor::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(&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(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