Core/BugReporter/Z3CrosscheckVisitor.h

0001 //===- Z3CrosscheckVisitor.h - Crosscheck reports with Z3 -------*- C++ -*-===//
0002 //
0003 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
0004 // See https://llvm.org/LICENSE.txt for license information.
0005 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
0006 //
0007 //===----------------------------------------------------------------------===//
0008 //
0009 //  This file defines the visitor and utilities around it for Z3 report
0010 //  refutation.
0011 //
0012 //===----------------------------------------------------------------------===//
0013
0014 #ifndef LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H
0015 #define LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H
0016
0017 #include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h"
0018
0019 namespace clang::ento {
0020
0021 /// The bug visitor will walk all the nodes in a path and collect all the
0022 /// constraints. When it reaches the root node, will create a refutation
0023 /// manager and check if the constraints are satisfiable.
0024 class Z3CrosscheckVisitor final : public BugReporterVisitor {
0025 public:
0026   struct Z3Result {
0027     std::optional<bool> IsSAT = std::nullopt;
0028     unsigned Z3QueryTimeMilliseconds = 0;
0029     unsigned UsedRLimit = 0;
0030   };
0031   Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,
0032                       const AnalyzerOptions &Opts);
0033
0034   void Profile(llvm::FoldingSetNodeID &ID) const override;
0035
0036   PathDiagnosticPieceRef VisitNode(const ExplodedNode *N,
0037                                    BugReporterContext &BRC,
0038                                    PathSensitiveBugReport &BR) override;
0039
0040   void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,
0041                        PathSensitiveBugReport &BR) override;
0042
0043 private:
0044   void addConstraints(const ExplodedNode *N,
0045                       bool OverwriteConstraintsOnExistingSyms);
0046
0047   /// Holds the constraints in a given path.
0048   ConstraintMap Constraints;
0049   Z3Result &Result;
0050   const AnalyzerOptions &Opts;
0051 };
0052
0053 /// The oracle will decide if a report should be accepted or rejected based on
0054 /// the results of the Z3 solver and the statistics of the queries of a report
0055 /// equivalenece class.
0056 class Z3CrosscheckOracle {
0057 public:
0058   explicit Z3CrosscheckOracle(const AnalyzerOptions &Opts) : Opts(Opts) {}
0059
0060   enum Z3Decision {
0061     AcceptReport,  // The report was SAT.
0062     RejectReport,  // The report was UNSAT or UNDEF.
0063     RejectEQClass, // The heuristic suggests to skip the current eqclass.
0064   };
0065
0066   /// Updates the internal state with the new Z3Result and makes a decision how
0067   /// to proceed:
0068   /// - Accept the report if the Z3Result was SAT.
0069   /// - Suggest dropping the report equvalence class based on the accumulated
0070   ///   statistics.
0071   /// - Otherwise, reject the report if the Z3Result was UNSAT or UNDEF.
0072   ///
0073   /// Conditions for dropping the equivalence class:
0074   /// - Accumulative time spent in Z3 checks is more than 700ms in the eqclass.
0075   /// - Hit the 300ms query timeout in the report eqclass.
0076   /// - Hit the 400'000 rlimit in the report eqclass.
0077   ///
0078   /// All these thresholds are configurable via the analyzer options.
0079   ///
0080   /// Refer to
0081   /// https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520 to
0082   /// see why this heuristic was chosen.
0083   Z3Decision interpretQueryResult(const Z3CrosscheckVisitor::Z3Result &Meta);
0084
0085 private:
0086   const AnalyzerOptions &Opts;
0087   unsigned AccumulatedZ3QueryTimeInEqClass = 0; // ms
0088 };
0089
0090 } // namespace clang::ento
0091
0092 #endif // LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H