[analyzer] Revert Z3 changes

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

@@ -184,26 +184,6 @@ ANALYZER_OPTION(bool, ShouldCrosscheckWithZ3, "crosscheck-with-z3",
                 "constraint manager backend.",
                 false)
 
-ANALYZER_OPTION(
-    unsigned, Z3CrosscheckEQClassTimeoutThreshold,
-    "crosscheck-with-z3-eqclass-timeout-threshold",
-    "Set a timeout for bug report equivalence classes in milliseconds. "
-    "If we exhaust this threshold, we will drop the bug report eqclass "
-    "instead of doing more Z3 queries. Set 0 for no timeout.", 700)
-
-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,6 +597,29 @@ 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/PathSensitive/SMTConstraintManager.h

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

clang/lib/StaticAnalyzer/Core/BugReporter.cpp

@@ -35,7 +35,6 @@
 #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"
@@ -87,14 +86,6 @@ 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() {}
@@ -2843,7 +2834,6 @@ generateVisitorsDiagnostics(PathSensitiveBugReport *R,
 std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
     ArrayRef<PathSensitiveBugReport *> &bugReports,
     PathSensitiveBugReporter &Reporter) {
-  Z3CrosscheckOracle Z3Oracle(Reporter.getAnalyzerOptions());
 
   BugPathGetter BugGraph(&Reporter.getGraph(), bugReports);
 
@@ -2874,35 +2864,21 @@ std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
         // If crosscheck is enabled, remove all visitors, add the refutation
         // visitor and check again
         R->clearVisitors();
-        Z3CrosscheckVisitor::Z3Result CrosscheckResult;
-        R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult,
-                                           Reporter.getAnalyzerOptions());
+        R->addVisitor<FalsePositiveRefutationBRVisitor>();
 
         // 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;
-        }
       }
 
-      assert(R->isValid());
-      return PathDiagnosticBuilder(std::move(BRC), std::move(BugPath->BugPath),
-                                   BugPath->Report, BugPath->ErrorNode,
-                                   std::move(visitorNotes));
+      // 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));
     }
   }
 
-  ++NumTimesReportEQClassWasExhausted;
   return {};
 }
 

clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp

@@ -3446,6 +3446,82 @@ 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,7 +51,6 @@ add_clang_library(clangStaticAnalyzerCore
   SymbolManager.cpp
   TextDiagnostics.cpp
   WorkList.cpp
-  Z3CrosscheckVisitor.cpp
 
   LINK_LIBS
   clangAST