[analyzer][NFC] Reorganize Z3 report refutation

This change keeps existing behavior, namely that if we hit a Z3 timeout
we will accept the report as "satisfiable".

This prepares for the commit "Harden safeguards for Z3 query times".
https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520

Reviewers: NagyDonat, haoNoQ, Xazax-hun, mikhailramalho, Szelethus

Reviewed By: NagyDonat

Pull Request: #95128

Author: steakhal

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,66 @@
+//===- 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;
+  };
+  explicit Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result);
+
+  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;
+};
+
+/// The oracle will decide if a report should be accepted or rejected based on
+/// the results of the Z3 solver.
+class Z3CrosscheckOracle {
+public:
+  enum Z3Decision {
+    AcceptReport, // The report was SAT.
+    RejectReport, // The report was UNSAT or UNDEF.
+  };
+
+  /// Makes a decision for accepting or rejecting the report based on the
+  /// result of the corresponding Z3 query.
+  static Z3Decision
+  interpretQueryResult(const Z3CrosscheckVisitor::Z3Result &Query);
+};
+
+} // 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,11 @@ 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(NumTimesReportEQClassWasExhausted,
+          "Number of times all reports of an equivalence class was refuted");
+
 BugReporterVisitor::~BugReporterVisitor() = default;
 
 void BugReporterContext::anchor() {}
@@ -2864,21 +2870,31 @@ 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);
 
         // 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 (Z3CrosscheckOracle::interpretQueryResult(CrosscheckResult)) {
+        case Z3CrosscheckOracle::RejectReport:
+          ++NumTimesReportRefuted;
+          R->markInvalid("Infeasible constraints", /*Data=*/nullptr);
+          continue;
+        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

clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp

@@ -0,0 +1,118 @@
+//===- Z3CrosscheckVisitor.cpp - 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 declares the visitor and utilities around it for Z3 report
+//  refutation.
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
+#include "clang/StaticAnalyzer/Core/BugReporter/BugReporter.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
+#include "llvm/ADT/Statistic.h"
+#include "llvm/Support/SMTAPI.h"
+
+#define DEBUG_TYPE "Z3CrosscheckOracle"
+
+STATISTIC(NumZ3QueriesDone, "Number of Z3 queries done");
+STATISTIC(NumTimesZ3TimedOut, "Number of times Z3 query timed out");
+
+STATISTIC(NumTimesZ3QueryAcceptsReport,
+          "Number of Z3 queries accepting a report");
+STATISTIC(NumTimesZ3QueryRejectReport,
+          "Number of Z3 queries rejecting a report");
+
+using namespace clang;
+using namespace ento;
+
+Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result)
+    : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result) {}
+
+void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
+                                          const ExplodedNode *EndPathNode,
+                                          PathSensitiveBugReport &BR) {
+  // Collect new constraints
+  addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
+
+  // Create a refutation manager
+  llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
+  RefutationSolver->setBoolParam("model", true);        // Enable model finding
+  RefutationSolver->setUnsignedParam("timeout", 15000); // ms
+
+  ASTContext &Ctx = BRC.getASTContext();
+
+  // Add constraints to the solver
+  for (const auto &[Sym, Range] : Constraints) {
+    auto RangeIt = Range.begin();
+
+    llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr(
+        RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
+        /*InRange=*/true);
+    while ((++RangeIt) != Range.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();
+  Result = Z3Result{IsSAT};
+}
+
+void Z3CrosscheckVisitor::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 &[Sym, Range] : NewCs) {
+    if (!Constraints.contains(Sym)) {
+      // This symbol is new, just add the constraint.
+      Constraints = CF.add(Constraints, Sym, Range);
+    } else if (OverwriteConstraintsOnExistingSyms) {
+      // Overwrite the associated constraint of the Symbol.
+      Constraints = CF.remove(Constraints, Sym);
+      Constraints = CF.add(Constraints, Sym, Range);
+    }
+  }
+}
+
+PathDiagnosticPieceRef
+Z3CrosscheckVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &,
+                               PathSensitiveBugReport &) {
+  addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false);
+  return nullptr;
+}
+
+void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const {
+  static int Tag = 0;
+  ID.AddPointer(&Tag);
+}
+
+Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult(
+    const Z3CrosscheckVisitor::Z3Result &Query) {
+  ++NumZ3QueriesDone;
+
+  if (!Query.IsSAT.has_value()) {
+    // For backward compatibility, let's accept the first timeout.
+    ++NumTimesZ3TimedOut;
+    return AcceptReport;
+  }
+
+  if (Query.IsSAT.value()) {
+    ++NumTimesZ3QueryAcceptsReport;
+    return AcceptReport; // sat
+  }
+
+  ++NumTimesZ3QueryRejectReport;
+  return RejectReport; // unsat
+}