[clang] [llvm] Reland "[analyzer][NFC] Reorganize Z3 report refutation" (PR #97265)
via cfe-commits
cfe-commits at lists.llvm.org
Mon Jul 1 01:54:06 PDT 2024
llvmbot wrote:
<!--LLVM PR SUMMARY COMMENT-->
@llvm/pr-subscribers-clang-static-analyzer-1
Author: Balazs Benics (steakhal)
<details>
<summary>Changes</summary>
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 89c26f6c7b0a6dfa257ec090fcf5b6e6e0c89aab)
---
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
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 at 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]
``````````
</details>
https://github.com/llvm/llvm-project/pull/97265
More information about the cfe-commits
mailing list