1 //===- Z3CrosscheckVisitor.h - 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 defines the visitor and utilities around it for Z3 report 10 // refutation. 11 // 12 //===----------------------------------------------------------------------===// 13 14 #ifndef LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H 15 #define LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H 16 17 #include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h" 18 19 namespace clang::ento { 20 21 /// The bug visitor will walk all the nodes in a path and collect all the 22 /// constraints. When it reaches the root node, will create a refutation 23 /// manager and check if the constraints are satisfiable. 24 class Z3CrosscheckVisitor final : public BugReporterVisitor { 25 public: 26 struct Z3Result { 27 std::optional<bool> IsSAT = std::nullopt; 28 unsigned Z3QueryTimeMilliseconds = 0; 29 unsigned UsedRLimit = 0; 30 }; 31 Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result, 32 const AnalyzerOptions &Opts); 33 34 void Profile(llvm::FoldingSetNodeID &ID) const override; 35 36 PathDiagnosticPieceRef VisitNode(const ExplodedNode *N, 37 BugReporterContext &BRC, 38 PathSensitiveBugReport &BR) override; 39 40 void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode, 41 PathSensitiveBugReport &BR) override; 42 43 private: 44 void addConstraints(const ExplodedNode *N, 45 bool OverwriteConstraintsOnExistingSyms); 46 47 /// Holds the constraints in a given path. 48 ConstraintMap Constraints; 49 Z3Result &Result; 50 const AnalyzerOptions &Opts; 51 }; 52 53 /// The oracle will decide if a report should be accepted or rejected based on 54 /// the results of the Z3 solver and the statistics of the queries of a report 55 /// equivalenece class. 56 class Z3CrosscheckOracle { 57 public: Z3CrosscheckOracle(const AnalyzerOptions & Opts)58 explicit Z3CrosscheckOracle(const AnalyzerOptions &Opts) : Opts(Opts) {} 59 60 enum Z3Decision { 61 AcceptReport, // The report was SAT. 62 RejectReport, // The report was UNSAT or UNDEF. 63 RejectEQClass, // The heuristic suggests to skip the current eqclass. 64 }; 65 66 /// Updates the internal state with the new Z3Result and makes a decision how 67 /// to proceed: 68 /// - Accept the report if the Z3Result was SAT. 69 /// - Suggest dropping the report equvalence class based on the accumulated 70 /// statistics. 71 /// - Otherwise, reject the report if the Z3Result was UNSAT or UNDEF. 72 /// 73 /// Conditions for dropping the equivalence class: 74 /// - Accumulative time spent in Z3 checks is more than 700ms in the eqclass. 75 /// - Hit the 300ms query timeout in the report eqclass. 76 /// - Hit the 400'000 rlimit in the report eqclass. 77 /// 78 /// All these thresholds are configurable via the analyzer options. 79 /// 80 /// Refer to 81 /// https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520 to 82 /// see why this heuristic was chosen. 83 Z3Decision interpretQueryResult(const Z3CrosscheckVisitor::Z3Result &Meta); 84 85 private: 86 const AnalyzerOptions &Opts; 87 unsigned AccumulatedZ3QueryTimeInEqClass = 0; // ms 88 }; 89 90 } // namespace clang::ento 91 92 #endif // LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H 93