[analyzer] Harden safeguards for Z3 query times

clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def

@@ -184,6 +184,19 @@ ANALYZER_OPTION(bool, ShouldCrosscheckWithZ3, "crosscheck-with-z3",
                 "constraint manager backend.",
                 false)
 
+ANALYZER_OPTION(
+    unsigned, Z3CrosscheckTimeoutThreshold,
+    "crosscheck-with-z3-timeout-threshold",
+    "Set a timeout for individual Z3 queries in milliseconds. "
+    "Set 0 for no timeout.", 300)
+
+ANALYZER_OPTION(
+    unsigned, Z3CrosscheckRLimitThreshold,
+    "crosscheck-with-z3-rlimit-threshold",
+    "Set the Z3 resource limit threshold. This sets a deterministic cutoff "
+    "point for Z3 queries, as longer queries usually consume more resources. "
+    "Set 0 for unlimited.", 400'000)
+
 ANALYZER_OPTION(bool, ShouldReportIssuesInMainSourceFile,
                 "report-in-main-source-file",
                 "Whether or not the diagnostic report should be always "

clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h

@@ -597,29 +597,6 @@ class SuppressInlineDefensiveChecksVisitor final : public BugReporterVisitor {
                                    PathSensitiveBugReport &BR) override;
 };
 
-/// The bug visitor will walk all the nodes in a path and collect all the
-/// constraints. When it reaches the root node, will create a refutation
-/// manager and check if the constraints are satisfiable
-class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor {
-private:
-  /// Holds the constraints in a given path
-  ConstraintMap Constraints;
-
-public:
-  FalsePositiveRefutationBRVisitor();
-
-  void Profile(llvm::FoldingSetNodeID &ID) const override;
-
-  PathDiagnosticPieceRef VisitNode(const ExplodedNode *N,
-                                   BugReporterContext &BRC,
-                                   PathSensitiveBugReport &BR) override;
-
-  void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,
-                       PathSensitiveBugReport &BR) override;
-  void addConstraints(const ExplodedNode *N,
-                      bool OverwriteConstraintsOnExistingSyms);
-};
-
 /// The visitor detects NoteTags and displays the event notes they contain.
 class TagVisitor : public BugReporterVisitor {
 public:

clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h

@@ -0,0 +1,91 @@
+//===- Z3CrosscheckVisitor.h - Crosscheck reports with Z3 -------*- C++ -*-===//
+//
+// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
+// See https://llvm.org/LICENSE.txt for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+//
+//===----------------------------------------------------------------------===//
+//
+//  This file defines the visitor and utilities around it for Z3 report
+//  refutation.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H
+#define LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H
+
+#include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h"
+
+namespace clang::ento {
+
+/// The bug visitor will walk all the nodes in a path and collect all the
+/// constraints. When it reaches the root node, will create a refutation
+/// manager and check if the constraints are satisfiable.
+class Z3CrosscheckVisitor final : public BugReporterVisitor {
+public:
+  struct Z3Result {
+    std::optional<bool> IsSAT = std::nullopt;
+    unsigned Z3QueryTimeMilliseconds = 0;
+    unsigned UsedRLimit = 0;
+  };
+  Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,
+                      const AnalyzerOptions &Opts);
+
+  void Profile(llvm::FoldingSetNodeID &ID) const override;
+
+  PathDiagnosticPieceRef VisitNode(const ExplodedNode *N,
+                                   BugReporterContext &BRC,
+                                   PathSensitiveBugReport &BR) override;
+
+  void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,
+                       PathSensitiveBugReport &BR) override;
+
+private:
+  void addConstraints(const ExplodedNode *N,
+                      bool OverwriteConstraintsOnExistingSyms);
+
+  /// Holds the constraints in a given path.
+  ConstraintMap Constraints;
+  Z3Result &Result;
+  const AnalyzerOptions &Opts;
+};
+
+/// The oracle will decide if a report should be accepted or rejected based on
+/// the results of the Z3 solver and the statistics of the queries of a report
+/// equivalenece class.
+class Z3CrosscheckOracle {
+public:
+  explicit Z3CrosscheckOracle(const AnalyzerOptions &Opts) : Opts(Opts) {}
+
+  enum Z3Decision {
+    AcceptReport,  // The report was SAT.
+    RejectReport,  // The report was UNSAT or UNDEF.
+    RejectEQClass, // The heuristic suggests to skip the current eqclass.
+  };
+
+  /// Updates the internal state with the new Z3Result and makes a decision how
+  /// to proceed:
+  /// - Accept the report if the Z3Result was SAT.
+  /// - Suggest dropping the report equvalence class based on the accumulated
+  ///   statistics.
+  /// - Otherwise, reject the report if the Z3Result was UNSAT or UNDEF.
+  ///
+  /// Conditions for dropping the equivalence class:
+  /// - Accumulative time spent in Z3 checks is more than 700ms in the eqclass.
+  /// - Hit the 300ms query timeout in the report eqclass.
+  /// - Hit the 400'000 rlimit in the report eqclass.
+  ///
+  /// Refer to
+  /// https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520 to
+  /// see why this heuristic was chosen.
+  Z3Decision interpretQueryResult(const Z3CrosscheckVisitor::Z3Result &Meta);
+
+private:
+  const AnalyzerOptions &Opts;
+  unsigned NumZ3QueriesDoneInEqClass = 0;
+  unsigned AccumulatedZ3QueryTimeInEqClass = 0; // ms
+};
+
+} // namespace clang::ento
+
+#endif // LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H

clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h

@@ -34,7 +34,10 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager {
 public:
   SMTConstraintManager(clang::ento::ExprEngine *EE,
                        clang::ento::SValBuilder &SB)
-      : SimpleConstraintManager(EE, SB) {}
+      : SimpleConstraintManager(EE, SB) {
+    Solver->setBoolParam("model", true); // Enable model finding
+    Solver->setUnsignedParam("timeout", 15000 /*milliseconds*/);
+  }
   virtual ~SMTConstraintManager() = default;
 
   //===------------------------------------------------------------------===//

clang/lib/StaticAnalyzer/Core/BugReporter.cpp

@@ -35,6 +35,7 @@
 #include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
 #include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h"
 #include "clang/StaticAnalyzer/Core/BugReporter/BugType.h"
+#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
 #include "clang/StaticAnalyzer/Core/Checker.h"
 #include "clang/StaticAnalyzer/Core/CheckerManager.h"
 #include "clang/StaticAnalyzer/Core/CheckerRegistryData.h"
@@ -86,6 +87,14 @@ STATISTIC(MaxValidBugClassSize,
           "The maximum number of bug reports in the same equivalence class "
           "where at least one report is valid (not suppressed)");
 
+STATISTIC(NumTimesReportPassesZ3, "Number of reports passed Z3");
+STATISTIC(NumTimesReportRefuted, "Number of reports refuted by Z3");
+STATISTIC(NumTimesReportEQClassAborted,
+          "Number of times a report equivalence class was aborted by the Z3 "
+          "oracle heuristic");
+STATISTIC(NumTimesReportEQClassWasExhausted,
+          "Number of times all reports of an equivalence class was refuted");
+
 BugReporterVisitor::~BugReporterVisitor() = default;
 
 void BugReporterContext::anchor() {}
@@ -2834,6 +2843,7 @@ generateVisitorsDiagnostics(PathSensitiveBugReport *R,
 std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
     ArrayRef<PathSensitiveBugReport *> &bugReports,
     PathSensitiveBugReporter &Reporter) {
+  Z3CrosscheckOracle Z3Oracle(Reporter.getAnalyzerOptions());
 
   BugPathGetter BugGraph(&Reporter.getGraph(), bugReports);
 
@@ -2864,21 +2874,35 @@ std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
         // If crosscheck is enabled, remove all visitors, add the refutation
         // visitor and check again
         R->clearVisitors();
-        R->addVisitor<FalsePositiveRefutationBRVisitor>();
+        Z3CrosscheckVisitor::Z3Result CrosscheckResult;
+        R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult,
+                                           Reporter.getAnalyzerOptions());
 
         // We don't overwrite the notes inserted by other visitors because the
         // refutation manager does not add any new note to the path
         generateVisitorsDiagnostics(R, BugPath->ErrorNode, BRC);
+        switch (Z3Oracle.interpretQueryResult(CrosscheckResult)) {
+        case Z3CrosscheckOracle::RejectReport:
+          ++NumTimesReportRefuted;
+          R->markInvalid("Infeasible constraints", /*Data=*/nullptr);
+          continue;
+        case Z3CrosscheckOracle::RejectEQClass:
+          ++NumTimesReportEQClassAborted;
+          return {};
+        case Z3CrosscheckOracle::AcceptReport:
+          ++NumTimesReportPassesZ3;
+          break;
+        }
       }
 
-      // Check if the bug is still valid
-      if (R->isValid())
-        return PathDiagnosticBuilder(
-            std::move(BRC), std::move(BugPath->BugPath), BugPath->Report,
-            BugPath->ErrorNode, std::move(visitorNotes));
+      assert(R->isValid());
+      return PathDiagnosticBuilder(std::move(BRC), std::move(BugPath->BugPath),
+                                   BugPath->Report, BugPath->ErrorNode,
+                                   std::move(visitorNotes));
     }
   }
 
+  ++NumTimesReportEQClassWasExhausted;
   return {};
 }
 

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

@@ -3446,82 +3446,6 @@ UndefOrNullArgVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &BRC,
   return nullptr;
 }
 
-//===----------------------------------------------------------------------===//
-// Implementation of FalsePositiveRefutationBRVisitor.
-//===----------------------------------------------------------------------===//
-
-FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
-    : Constraints(ConstraintMap::Factory().getEmptyMap()) {}
-
-void FalsePositiveRefutationBRVisitor::finalizeVisitor(
-    BugReporterContext &BRC, const ExplodedNode *EndPathNode,
-    PathSensitiveBugReport &BR) {
-  // Collect new constraints
-  addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
-
-  // Create a refutation manager
-  llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
-  ASTContext &Ctx = BRC.getASTContext();
-
-  // Add constraints to the solver
-  for (const auto &I : Constraints) {
-    const SymbolRef Sym = I.first;
-    auto RangeIt = I.second.begin();
-
-    llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(
-        RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
-        /*InRange=*/true);
-    while ((++RangeIt) != I.second.end()) {
-      SMTConstraints = RefutationSolver->mkOr(
-          SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
-                                                RangeIt->From(), RangeIt->To(),
-                                                /*InRange=*/true));
-    }
-
-    RefutationSolver->addConstraint(SMTConstraints);
-  }
-
-  // And check for satisfiability
-  std::optional<bool> IsSAT = RefutationSolver->check();
-  if (!IsSAT)
-    return;
-
-  if (!*IsSAT)
-    BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
-}
-
-void FalsePositiveRefutationBRVisitor::addConstraints(
-    const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
-  // Collect new constraints
-  ConstraintMap NewCs = getConstraintMap(N->getState());
-  ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>();
-
-  // Add constraints if we don't have them yet
-  for (auto const &C : NewCs) {
-    const SymbolRef &Sym = C.first;
-    if (!Constraints.contains(Sym)) {
-      // This symbol is new, just add the constraint.
-      Constraints = CF.add(Constraints, Sym, C.second);
-    } else if (OverwriteConstraintsOnExistingSyms) {
-      // Overwrite the associated constraint of the Symbol.
-      Constraints = CF.remove(Constraints, Sym);
-      Constraints = CF.add(Constraints, Sym, C.second);
-    }
-  }
-}
-
-PathDiagnosticPieceRef FalsePositiveRefutationBRVisitor::VisitNode(
-    const ExplodedNode *N, BugReporterContext &, PathSensitiveBugReport &) {
-  addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false);
-  return nullptr;
-}
-
-void FalsePositiveRefutationBRVisitor::Profile(
-    llvm::FoldingSetNodeID &ID) const {
-  static int Tag = 0;
-  ID.AddPointer(&Tag);
-}
-
 //===----------------------------------------------------------------------===//
 // Implementation of TagVisitor.
 //===----------------------------------------------------------------------===//

clang/lib/StaticAnalyzer/Core/CMakeLists.txt

@@ -51,6 +51,7 @@ add_clang_library(clangStaticAnalyzerCore
   SymbolManager.cpp
   TextDiagnostics.cpp
   WorkList.cpp
+  Z3CrosscheckVisitor.cpp
 
   LINK_LIBS
   clangAST