Reland "[analyzer][NFC] Reorganize Z3 report refutation" #97265

steakhal · 2024-07-01T08:53:40Z

This is exactly as originally landed in #95128,
but now the minimal Z3 version was increased to meet this change in #96682.
https://discourse.llvm.org/t/bump-minimal-z3-requirements-from-4-7-1-to-4-8-9/79664/4

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

(cherry picked from commit 89c26f6)

This is exactly as originally landed in llvm#95128, but now the minimal Z3 version was increased to meet this change in llvm#96682. https://discourse.llvm.org/t/bump-minimal-z3-requirements-from-4-7-1-to-4-8-9/79664/4 --- 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 (cherry picked from commit 89c26f6)

llvmbot · 2024-07-01T08:54:00Z

@llvm/pr-subscribers-llvm-support
@llvm/pr-subscribers-clang

@llvm/pr-subscribers-clang-static-analyzer-1

Author: Balazs Benics (steakhal)

Changes

This is exactly as originally landed in #95128,
but now the minimal Z3 version was increased to meet this change in #96682.
https://discourse.llvm.org/t/bump-minimal-z3-requirements-from-4-7-1-to-4-8-9/79664/4

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

(cherry picked from commit 89c26f6)

Patch is 27.63 KiB, truncated to 20.00 KiB below, full version: https://github.com/llvm/llvm-project/pull/97265.diff

12 Files Affected:

(modified) clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h (-23)
(added) clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h (+66)
(modified) clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (+4-1)
(modified) clang/lib/StaticAnalyzer/Core/BugReporter.cpp (+22-6)
(modified) clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp (-76)
(modified) clang/lib/StaticAnalyzer/Core/CMakeLists.txt (+1)
(added) clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp (+118)
(added) clang/test/Analysis/z3/crosscheck-statistics.c (+33)
(modified) clang/unittests/StaticAnalyzer/CMakeLists.txt (+1)
(added) clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp (+59)
(modified) llvm/include/llvm/Support/SMTAPI.h (+19)
(modified) llvm/lib/Support/Z3Solver.cpp (+96-20)

diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
index cc3d93aabafda..f97514955a591 100644
--- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
+++ b/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:
diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
new file mode 100644
index 0000000000000..9413fd739f607
--- /dev/null
+++ b/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
diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
index 5116a4c06850d..bf18c353b8508 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/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;
 
   //===------------------------------------------------------------------===//
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
index 14ca507a16d55..c9a7fd0e035c2 100644
--- a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
+++ b/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 {};
 }
 
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
index 4ff4f7de425ca..7102bf51a57e8 100644
--- a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -3447,82 +3447,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.
 //===----------------------------------------------------------------------===//
diff --git a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt b/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
index 8672876c0608d..fb9394a519eb7 100644
--- a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
+++ b/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
diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
new file mode 100644
index 0000000000000..a7db44ef8ea30
--- /dev/null
+++ b/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
+}
diff --git a/clang/test/Analysis/z3/crosscheck-statistics.c b/clang/test/Analysis/z3/crosscheck-statistics.c
new file mode 100644
index 0000000000000..7192824c5be31
--- /dev/null
+++ b/clang/test/Analysis/z3/crosscheck-statistics.c
@@ -0,0 +1,33 @@
+// RUN: %clang_analyze_cc1 -analyzer-checker=core -verify %s  \
+// RUN:   -analyzer-config crosscheck-with-z3=true \
+// RUN:   -analyzer-stats 2>&1 | FileCheck %s
+
+// REQUIRES: z3
+
+// expected-error@1 {{Z3 refutation rate:1/2}}
+
+int accepting(int n) {
+  if (n == 4) {
+    n = n / (n-4); // expected-warning {{Division by zero}}
+  }
+  return n;
+}
+
+int rejecting(int n, int x) {
+  // Let's make the path infeasible.
+  if (2 < x && x < 5 && x*x == x*x*x) {
+    // Have the same condition as in 'accepting'.
+    if (n == 4) {
+      n = x / (n-4); // no-warning: refuted
+    }
+  }
+  return n;
+}
+
+// CHECK:       1 BugReporter         - Number of times all reports of an equivalence class was refuted
+// CHECK-NEXT:  1 BugReporter         - Number of reports passed Z3
+// CHECK-NEXT:  1 BugReporter         - Number of reports refuted by Z3
+
+// CHECK:       1 Z3CrosscheckVisitor - Number of Z3 queries accepting a report
+// CHECK-NEXT:  1 Z3CrosscheckVisitor - Number of Z3 queries rejecting a report
+// CHECK-NEXT:  2 Z3CrosscheckVisitor - Number of Z3 queries done
diff --git a/clang/unittests/StaticAnalyzer/CMakeLists.txt b/clang/unittests/StaticAnalyzer/CMakeLists.txt
index ff34d5747cc81..dcc557b44fb31 100644
--- a/clang/unittests/StaticAnalyzer/CMakeLists.txt
+++ b/clang/unittests/StaticAnalyzer/CMakeLists.txt
@@ -21,6 +21,7 @@ add_clang_unittest(StaticAnalysisTests
   SymbolReaperTest.cpp
   SValTest.cpp
   TestReturnValueUnderConstruction.cpp
+  Z3CrosscheckOracleTest.cpp
   )
 
 clang_target_link_libraries(StaticAnalysisTests
diff --git a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
new file mode 100644
index 0000000000000..efad4dd3f03b9
--- /dev/null
+++ b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
@@ -0,0 +1,59 @@
+//===- unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp ----------------===//
+//
+// 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
+//
+//===----------------------------------------------------------------------===//
+
+#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
+#include "gtest/gtest.h"
+
+using namespace clang;
+using namespace ento;
+
+using Z3Result = Z3CrosscheckVisitor::Z3Result;
+using Z3Decision = Z3CrosscheckOracle::Z3Decision;
+
+static constexpr Z3Decision AcceptReport = Z3Decision::AcceptReport;
+static constexpr Z3Decision RejectReport = Z3Decision::RejectReport;
+
+static constexpr std::optional<bool> SAT = true;
+static constexpr std::optional<bool> UNSAT = false;
+static constexpr std::optional<bool> UNDEF = std::nullopt;
+
+namespace {
+
+struct Z3CrosscheckOracleTest : public testing::Test {
+  Z3Decision interpretQueryResult(const Z3Result &Result) const {
+    return Z3CrosscheckOracle::interpretQueryResult(Result);
+  }
+};
+
+TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) {
+  ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));
+}
+
+TEST_F(Z3CrosscheckOracleTest, AcceptsSAT) {
+  ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+  ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));
+}
+
+TEST_F(Z3CrosscheckOracleTest, AcceptsFirstTimeout) {
+  ASSERT_EQ(AcceptReport, interpretQueryResult({UNDEF}));
+}
+
+TEST_F(Z3CrosscheckOracleTest, Accept...
[truncated]

steakhal · 2024-07-01T08:54:09Z

This was already reviewed and approved in the past. The content is identical to that one.

NagyDonat

Let's merge this again, after the Z3 required version bump there shouldn't be any additional problems.

This is exactly as originally landed in llvm#95128, but now the minimal Z3 version was increased to meet this change in llvm#96682. https://discourse.llvm.org/t/bump-minimal-z3-requirements-from-4-7-1-to-4-8-9/79664/4 --- 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 (cherry picked from commit 89c26f6)

In my patch there, I left a test expectation stale. Tests with `REQUIRES: Z3` never run because no bots check such configurations. Here I'm adjusting the test expectations to meet reality.

steakhal added clang Clang issues not falling into any other category clang:static analyzer labels Jul 1, 2024

steakhal requested review from Xazax-hun, mikhailramalho, haoNoQ, Szelethus, NagyDonat, mikaelholmen and vabridgers July 1, 2024 08:53

llvmbot added the llvm:support label Jul 1, 2024

NagyDonat approved these changes Jul 1, 2024

View reviewed changes

steakhal merged commit b3b0d09 into llvm:main Jul 1, 2024
9 of 11 checks passed

steakhal deleted the bb/reland-z3-nfc branch July 1, 2024 14:03

steakhal mentioned this pull request Jul 1, 2024

Reland "[analyzer] Harden safeguards for Z3 query times" #97298

Merged

lukeshingles mentioned this pull request Aug 29, 2024

[analyzer] Add missing include <unordered_map> to llvm/lib/Support/Z3Solver.cpp #106410

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Reland "[analyzer][NFC] Reorganize Z3 report refutation" #97265

Reland "[analyzer][NFC] Reorganize Z3 report refutation" #97265

steakhal commented Jul 1, 2024

llvmbot commented Jul 1, 2024 •

edited

Loading

steakhal commented Jul 1, 2024

NagyDonat left a comment •

edited

Loading

Reland "[analyzer][NFC] Reorganize Z3 report refutation" #97265

Reland "[analyzer][NFC] Reorganize Z3 report refutation" #97265

Conversation

steakhal commented Jul 1, 2024

llvmbot commented Jul 1, 2024 • edited Loading

steakhal commented Jul 1, 2024

NagyDonat left a comment • edited Loading

Choose a reason for hiding this comment

llvmbot commented Jul 1, 2024 •

edited

Loading

NagyDonat left a comment •

edited

Loading