[clang] [llvm] [analyzer] Revert Z3 changes (PR #95916)
Balazs Benics via llvm-commits
llvm-commits at lists.llvm.org
Tue Jun 18 05:55:54 PDT 2024
https://github.com/steakhal created https://github.com/llvm/llvm-project/pull/95916
Requested in:
https://github.com/llvm/llvm-project/pull/95128#issuecomment-2176008007
Revert "[analyzer] Harden safeguards for Z3 query times" Revert "[analyzer][NFC] Reorganize Z3 report refutation"
This reverts commit eacc3b3504be061f7334410dd0eb599688ba103a. This reverts commit 89c26f6c7b0a6dfa257ec090fcf5b6e6e0c89aab.
>From 0a9434a872ea9a47a56c1c8fd74474aec52fea0d Mon Sep 17 00:00:00 2001
From: Balazs Benics <benicsbalazs at gmail.com>
Date: Tue, 18 Jun 2024 14:53:07 +0200
Subject: [PATCH] Revert Z3 changes
Requested in:
https://github.com/llvm/llvm-project/pull/95128#issuecomment-2176008007
Revert "[analyzer] Harden safeguards for Z3 query times"
Revert "[analyzer][NFC] Reorganize Z3 report refutation"
This reverts commit eacc3b3504be061f7334410dd0eb599688ba103a.
This reverts commit 89c26f6c7b0a6dfa257ec090fcf5b6e6e0c89aab.
---
.../StaticAnalyzer/Core/AnalyzerOptions.def | 20 ---
.../Core/BugReporter/BugReporterVisitors.h | 23 +++
.../Core/BugReporter/Z3CrosscheckVisitor.h | 92 ----------
.../Core/PathSensitive/SMTConstraintManager.h | 5 +-
clang/lib/StaticAnalyzer/Core/BugReporter.cpp | 36 +---
.../Core/BugReporterVisitors.cpp | 76 +++++++++
clang/lib/StaticAnalyzer/Core/CMakeLists.txt | 1 -
.../Core/Z3CrosscheckVisitor.cpp | 160 ------------------
clang/test/Analysis/analyzer-config.c | 3 -
.../test/Analysis/z3/crosscheck-statistics.c | 33 ----
clang/unittests/StaticAnalyzer/CMakeLists.txt | 1 -
.../StaticAnalyzer/Z3CrosscheckOracleTest.cpp | 143 ----------------
llvm/include/llvm/Support/SMTAPI.h | 19 ---
llvm/lib/Support/Z3Solver.cpp | 116 +++----------
14 files changed, 126 insertions(+), 602 deletions(-)
delete mode 100644 clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
delete mode 100644 clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
delete mode 100644 clang/test/Analysis/z3/crosscheck-statistics.c
delete mode 100644 clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
diff --git a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
index 29aa6a3b8a16e..f008c9c581d95 100644
--- a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def
+++ b/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 "
diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
index f97514955a591..cc3d93aabafda 100644
--- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
+++ b/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:
diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
deleted file mode 100644
index 439f37fa8604f..0000000000000
--- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
+++ /dev/null
@@ -1,92 +0,0 @@
-//===- 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.
- ///
- /// All these thresholds are configurable via the analyzer options.
- ///
- /// 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 AccumulatedZ3QueryTimeInEqClass = 0; // ms
-};
-
-} // 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 bf18c353b8508..5116a4c06850d 100644
--- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h
+++ b/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;
//===------------------------------------------------------------------===//
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
index e2002bfbe594a..14ca507a16d55 100644
--- a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
+++ b/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 {};
}
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
index 68dac65949117..487a3bd16b674 100644
--- a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ b/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.
//===----------------------------------------------------------------------===//
diff --git a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt b/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
index fb9394a519eb7..8672876c0608d 100644
--- a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt
+++ b/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
diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
deleted file mode 100644
index 739db951b3e18..0000000000000
--- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
+++ /dev/null
@@ -1,160 +0,0 @@
-//===- 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/AnalyzerOptions.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"
-#include "llvm/Support/Timer.h"
-
-#define DEBUG_TYPE "Z3CrosscheckOracle"
-
-STATISTIC(NumZ3QueriesDone, "Number of Z3 queries done");
-STATISTIC(NumTimesZ3TimedOut, "Number of times Z3 query timed out");
-STATISTIC(NumTimesZ3ExhaustedRLimit,
- "Number of times Z3 query exhausted the rlimit");
-STATISTIC(NumTimesZ3SpendsTooMuchTimeOnASingleEQClass,
- "Number of times report equivalenece class was cut because it spent "
- "too much time in Z3");
-
-STATISTIC(NumTimesZ3QueryAcceptsReport,
- "Number of Z3 queries accepting a report");
-STATISTIC(NumTimesZ3QueryRejectReport,
- "Number of Z3 queries rejecting a report");
-STATISTIC(NumTimesZ3QueryRejectEQClass,
- "Number of times rejecting an report equivalenece class");
-
-using namespace clang;
-using namespace ento;
-
-Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result,
- const AnalyzerOptions &Opts)
- : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result),
- Opts(Opts) {}
-
-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();
- if (Opts.Z3CrosscheckRLimitThreshold)
- RefutationSolver->setUnsignedParam("rlimit",
- Opts.Z3CrosscheckRLimitThreshold);
- if (Opts.Z3CrosscheckTimeoutThreshold)
- RefutationSolver->setUnsignedParam("timeout",
- Opts.Z3CrosscheckTimeoutThreshold); // 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
- llvm::TimeRecord Start = llvm::TimeRecord::getCurrentTime(/*Start=*/true);
- std::optional<bool> IsSAT = RefutationSolver->check();
- llvm::TimeRecord Diff = llvm::TimeRecord::getCurrentTime(/*Start=*/false);
- Diff -= Start;
- Result = Z3Result{
- IsSAT,
- static_cast<unsigned>(Diff.getWallTime() * 1000),
- RefutationSolver->getStatistics()->getUnsigned("rlimit count"),
- };
-}
-
-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;
- AccumulatedZ3QueryTimeInEqClass += Query.Z3QueryTimeMilliseconds;
-
- if (Query.IsSAT && Query.IsSAT.value()) {
- ++NumTimesZ3QueryAcceptsReport;
- return AcceptReport;
- }
-
- // Suggest cutting the EQClass if certain heuristics trigger.
- if (Opts.Z3CrosscheckTimeoutThreshold &&
- Query.Z3QueryTimeMilliseconds >= Opts.Z3CrosscheckTimeoutThreshold) {
- ++NumTimesZ3TimedOut;
- ++NumTimesZ3QueryRejectEQClass;
- return RejectEQClass;
- }
-
- if (Opts.Z3CrosscheckRLimitThreshold &&
- Query.UsedRLimit >= Opts.Z3CrosscheckRLimitThreshold) {
- ++NumTimesZ3ExhaustedRLimit;
- ++NumTimesZ3QueryRejectEQClass;
- return RejectEQClass;
- }
-
- if (Opts.Z3CrosscheckEQClassTimeoutThreshold &&
- AccumulatedZ3QueryTimeInEqClass >
- Opts.Z3CrosscheckEQClassTimeoutThreshold) {
- ++NumTimesZ3SpendsTooMuchTimeOnASingleEQClass;
- ++NumTimesZ3QueryRejectEQClass;
- return RejectEQClass;
- }
-
- // If no cutoff heuristics trigger, and the report is "unsat" or "undef",
- // then reject the report.
- ++NumTimesZ3QueryRejectReport;
- return RejectReport;
-}
diff --git a/clang/test/Analysis/analyzer-config.c b/clang/test/Analysis/analyzer-config.c
index 2a4c40005a4dc..fda920fa3951e 100644
--- a/clang/test/Analysis/analyzer-config.c
+++ b/clang/test/Analysis/analyzer-config.c
@@ -43,9 +43,6 @@
// CHECK-NEXT: cplusplus.Move:WarnOn = KnownsAndLocals
// CHECK-NEXT: cplusplus.SmartPtrModeling:ModelSmartPtrDereference = false
// CHECK-NEXT: crosscheck-with-z3 = false
-// CHECK-NEXT: crosscheck-with-z3-eqclass-timeout-threshold = 700
-// CHECK-NEXT: crosscheck-with-z3-rlimit-threshold = 400000
-// CHECK-NEXT: crosscheck-with-z3-timeout-threshold = 300
// CHECK-NEXT: ctu-dir = ""
// CHECK-NEXT: ctu-import-cpp-threshold = 8
// CHECK-NEXT: ctu-import-threshold = 24
diff --git a/clang/test/Analysis/z3/crosscheck-statistics.c b/clang/test/Analysis/z3/crosscheck-statistics.c
deleted file mode 100644
index 7192824c5be31..0000000000000
--- a/clang/test/Analysis/z3/crosscheck-statistics.c
+++ /dev/null
@@ -1,33 +0,0 @@
-// 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 dcc557b44fb31..ff34d5747cc81 100644
--- a/clang/unittests/StaticAnalyzer/CMakeLists.txt
+++ b/clang/unittests/StaticAnalyzer/CMakeLists.txt
@@ -21,7 +21,6 @@ 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
deleted file mode 100644
index ef07e47ee911b..0000000000000
--- a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
+++ /dev/null
@@ -1,143 +0,0 @@
-//===- 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/AnalyzerOptions.h"
-#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 Z3Decision RejectEQClass = Z3Decision::RejectEQClass;
-
-static constexpr std::optional<bool> SAT = true;
-static constexpr std::optional<bool> UNSAT = false;
-static constexpr std::optional<bool> UNDEF = std::nullopt;
-
-static unsigned operator""_ms(unsigned long long ms) { return ms; }
-static unsigned operator""_step(unsigned long long rlimit) { return rlimit; }
-
-static const AnalyzerOptions DefaultOpts = [] {
- AnalyzerOptions Config;
-#define ANALYZER_OPTION_DEPENDS_ON_USER_MODE(TYPE, NAME, CMDFLAG, DESC, \
- SHALLOW_VAL, DEEP_VAL) \
- ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEEP_VAL)
-#define ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEFAULT_VAL) \
- Config.NAME = DEFAULT_VAL;
-#include "clang/StaticAnalyzer/Core/AnalyzerOptions.def"
-
- // Remember to update the tests in this file when these values change.
- // Also update the doc comment of `interpretQueryResult`.
- assert(Config.Z3CrosscheckRLimitThreshold == 400'000);
- assert(Config.Z3CrosscheckTimeoutThreshold == 300_ms);
- // Usually, when the timeout/rlimit threshold is reached, Z3 only slightly
- // overshoots until it realizes that it overshoot and needs to back off.
- // Consequently, the measured timeout should be fairly close to the threshold.
- // Same reasoning applies to the rlimit too.
- return Config;
-}();
-
-namespace {
-
-class Z3CrosscheckOracleTest : public testing::Test {
-public:
- Z3Decision interpretQueryResult(const Z3Result &Result) {
- return Oracle.interpretQueryResult(Result);
- }
-
-private:
- Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(DefaultOpts);
-};
-
-TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) {
- ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
-}
-
-TEST_F(Z3CrosscheckOracleTest, AcceptsSAT) {
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
- ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
-}
-
-TEST_F(Z3CrosscheckOracleTest, SATWhenItGoesOverTime) {
- // Even if it times out, if it is SAT, we should accept it.
- ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 310_ms, 1000_step}));
-}
-
-TEST_F(Z3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
- ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step}));
-}
-
-TEST_F(Z3CrosscheckOracleTest, RejectsTimeout) {
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
- ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 310_ms, 1000_step}));
-}
-
-TEST_F(Z3CrosscheckOracleTest, RejectsUNSATs) {
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
-}
-
-// Testing cut heuristics:
-// =======================
-
-TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfSpendsTooMuchTotalTime) {
- // Simulate long queries, that barely doesn't trigger the timeout.
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
- ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
-}
-
-TEST_F(Z3CrosscheckOracleTest, SATWhenItSpendsTooMuchTotalTime) {
- // Simulate long queries, that barely doesn't trigger the timeout.
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step}));
- ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 290_ms, 1000_step}));
-}
-
-TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfAttemptsManySmallQueries) {
- // Simulate quick, but many queries: 35 quick UNSAT queries.
- // 35*20ms = 700ms, which is equal to the 700ms threshold.
- for (int i = 0; i < 35; ++i) {
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step}));
- }
- // Do one more to trigger the heuristic.
- ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 1_ms, 1000_step}));
-}
-
-TEST_F(Z3CrosscheckOracleTest, SATWhenIfAttemptsManySmallQueries) {
- // Simulate quick, but many queries: 35 quick UNSAT queries.
- // 35*20ms = 700ms, which is equal to the 700ms threshold.
- for (int i = 0; i < 35; ++i) {
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step}));
- }
- // Do one more to trigger the heuristic, but given this was SAT, we still
- // accept the query.
- ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 200_ms, 1000_step}));
-}
-
-TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfExhaustsRLimit) {
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
- ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 25_ms, 405'000_step}));
-}
-
-TEST_F(Z3CrosscheckOracleTest, SATWhenItExhaustsRLimit) {
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
- ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step}));
- ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 405'000_step}));
-}
-
-} // namespace
diff --git a/llvm/include/llvm/Support/SMTAPI.h b/llvm/include/llvm/Support/SMTAPI.h
index a2a89674414f4..9389c96956dd1 100644
--- a/llvm/include/llvm/Support/SMTAPI.h
+++ b/llvm/include/llvm/Support/SMTAPI.h
@@ -125,19 +125,6 @@ class SMTExpr {
virtual bool equal_to(SMTExpr const &other) const = 0;
};
-class SMTSolverStatistics {
-public:
- SMTSolverStatistics() = default;
- virtual ~SMTSolverStatistics() = default;
-
- virtual double getDouble(llvm::StringRef) const = 0;
- virtual unsigned getUnsigned(llvm::StringRef) const = 0;
-
- virtual void print(raw_ostream &OS) const = 0;
-
- LLVM_DUMP_METHOD void dump() const;
-};
-
/// Shared pointer for SMTExprs, used by SMTSolver API.
using SMTExprRef = const SMTExpr *;
@@ -447,12 +434,6 @@ class SMTSolver {
virtual bool isFPSupported() = 0;
virtual void print(raw_ostream &OS) const = 0;
-
- /// Sets the requested option.
- virtual void setBoolParam(StringRef Key, bool Value) = 0;
- virtual void setUnsignedParam(StringRef Key, unsigned Value) = 0;
-
- virtual std::unique_ptr<SMTSolverStatistics> getStatistics() const = 0;
};
/// Shared pointer for SMTSolvers.
diff --git a/llvm/lib/Support/Z3Solver.cpp b/llvm/lib/Support/Z3Solver.cpp
index 5a34ff160f6cf..eb671fe2596db 100644
--- a/llvm/lib/Support/Z3Solver.cpp
+++ b/llvm/lib/Support/Z3Solver.cpp
@@ -6,9 +6,7 @@
//
//===----------------------------------------------------------------------===//
-#include "llvm/ADT/ScopeExit.h"
#include "llvm/Config/config.h"
-#include "llvm/Support/NativeFormatting.h"
#include "llvm/Support/SMTAPI.h"
using namespace llvm;
@@ -28,14 +26,18 @@ namespace {
class Z3Config {
friend class Z3Context;
- Z3_config Config = Z3_mk_config();
+ Z3_config Config;
public:
- Z3Config() = default;
- Z3Config(const Z3Config &) = delete;
- Z3Config(Z3Config &&) = default;
- Z3Config &operator=(Z3Config &) = delete;
- Z3Config &operator=(Z3Config &&) = default;
+ Z3Config() : Config(Z3_mk_config()) {
+ // Enable model finding
+ Z3_set_param_value(Config, "model", "true");
+ // Disable proof generation
+ Z3_set_param_value(Config, "proof", "false");
+ // Set timeout to 15000ms = 15s
+ Z3_set_param_value(Config, "timeout", "15000");
+ }
+
~Z3Config() { Z3_del_config(Config); }
}; // end class Z3Config
@@ -48,22 +50,16 @@ void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
/// Wrapper for Z3 context
class Z3Context {
public:
- Z3Config Config;
Z3_context Context;
Z3Context() {
- Context = Z3_mk_context_rc(Config.Config);
+ Context = Z3_mk_context_rc(Z3Config().Config);
// The error function is set here because the context is the first object
// created by the backend
Z3_set_error_handler(Context, Z3ErrorHandler);
}
- Z3Context(const Z3Context &) = delete;
- Z3Context(Z3Context &&) = default;
- Z3Context &operator=(Z3Context &) = delete;
- Z3Context &operator=(Z3Context &&) = default;
-
- ~Z3Context() {
+ virtual ~Z3Context() {
Z3_del_context(Context);
Context = nullptr;
}
@@ -266,17 +262,7 @@ class Z3Solver : public SMTSolver {
Z3Context Context;
- Z3_solver Solver = [this] {
- Z3_solver S = Z3_mk_simple_solver(Context.Context);
- Z3_solver_inc_ref(Context.Context, S);
- return S;
- }();
-
- Z3_params Params = [this] {
- Z3_params P = Z3_mk_params(Context.Context);
- Z3_params_inc_ref(Context.Context, P);
- return P;
- }();
+ Z3_solver Solver;
// Cache Sorts
std::set<Z3Sort> CachedSorts;
@@ -285,15 +271,18 @@ class Z3Solver : public SMTSolver {
std::set<Z3Expr> CachedExprs;
public:
- Z3Solver() = default;
+ Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {
+ Z3_solver_inc_ref(Context.Context, Solver);
+ }
+
Z3Solver(const Z3Solver &Other) = delete;
Z3Solver(Z3Solver &&Other) = delete;
Z3Solver &operator=(Z3Solver &Other) = delete;
Z3Solver &operator=(Z3Solver &&Other) = delete;
- ~Z3Solver() override {
- Z3_params_dec_ref(Context.Context, Params);
- Z3_solver_dec_ref(Context.Context, Solver);
+ ~Z3Solver() {
+ if (Solver)
+ Z3_solver_dec_ref(Context.Context, Solver);
}
void addConstraint(const SMTExprRef &Exp) const override {
@@ -882,7 +871,6 @@ class Z3Solver : public SMTSolver {
}
std::optional<bool> check() const override {
- Z3_solver_set_params(Context.Context, Solver, Params);
Z3_lbool res = Z3_solver_check(Context.Context, Solver);
if (res == Z3_L_TRUE)
return true;
@@ -908,71 +896,8 @@ class Z3Solver : public SMTSolver {
void print(raw_ostream &OS) const override {
OS << Z3_solver_to_string(Context.Context, Solver);
}
-
- void setUnsignedParam(StringRef Key, unsigned Value) override {
- Z3_symbol Sym = Z3_mk_string_symbol(Context.Context, Key.str().c_str());
- Z3_params_set_uint(Context.Context, Params, Sym, Value);
- }
-
- void setBoolParam(StringRef Key, bool Value) override {
- Z3_symbol Sym = Z3_mk_string_symbol(Context.Context, Key.str().c_str());
- Z3_params_set_bool(Context.Context, Params, Sym, Value);
- }
-
- std::unique_ptr<SMTSolverStatistics> getStatistics() const override;
}; // end class Z3Solver
-class Z3Statistics final : public SMTSolverStatistics {
-public:
- double getDouble(StringRef Key) const override {
- auto It = DoubleValues.find(Key.str());
- assert(It != DoubleValues.end());
- return It->second;
- };
- unsigned getUnsigned(StringRef Key) const override {
- auto It = UnsignedValues.find(Key.str());
- assert(It != UnsignedValues.end());
- return It->second;
- };
-
- void print(raw_ostream &OS) const override {
- for (auto const &[K, V] : UnsignedValues) {
- OS << K << ": " << V << '\n';
- }
- for (auto const &[K, V] : DoubleValues) {
- write_double(OS << K << ": ", V, FloatStyle::Fixed);
- OS << '\n';
- }
- }
-
-private:
- friend class Z3Solver;
- std::unordered_map<std::string, unsigned> UnsignedValues;
- std::unordered_map<std::string, double> DoubleValues;
-};
-
-std::unique_ptr<SMTSolverStatistics> Z3Solver::getStatistics() const {
- auto const &C = Context.Context;
- Z3_stats S = Z3_solver_get_statistics(C, Solver);
- Z3_stats_inc_ref(C, S);
- auto StatsGuard = llvm::make_scope_exit([&C, &S] { Z3_stats_dec_ref(C, S); });
- Z3Statistics Result;
-
- unsigned NumKeys = Z3_stats_size(C, S);
- for (unsigned Idx = 0; Idx < NumKeys; ++Idx) {
- const char *Key = Z3_stats_get_key(C, S, Idx);
- if (Z3_stats_is_uint(C, S, Idx)) {
- auto Value = Z3_stats_get_uint_value(C, S, Idx);
- Result.UnsignedValues.try_emplace(Key, Value);
- } else {
- assert(Z3_stats_is_double(C, S, Idx));
- auto Value = Z3_stats_get_double_value(C, S, Idx);
- Result.DoubleValues.try_emplace(Key, Value);
- }
- }
- return std::make_unique<Z3Statistics>(std::move(Result));
-}
-
} // end anonymous namespace
#endif
@@ -991,4 +916,3 @@ llvm::SMTSolverRef llvm::CreateZ3Solver() {
LLVM_DUMP_METHOD void SMTSort::dump() const { print(llvm::errs()); }
LLVM_DUMP_METHOD void SMTExpr::dump() const { print(llvm::errs()); }
LLVM_DUMP_METHOD void SMTSolver::dump() const { print(llvm::errs()); }
-LLVM_DUMP_METHOD void SMTSolverStatistics::dump() const { print(llvm::errs()); }
More information about the llvm-commits
mailing list