[analyzer] Revert Z3 changes #95916
Merged
[analyzer] Revert Z3 changes #95916
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Requested in: #95128 (comment) Revert "[analyzer] Harden safeguards for Z3 query times" Revert "[analyzer][NFC] Reorganize Z3 report refutation" This reverts commit eacc3b3. This reverts commit 89c26f6.
llvmbot
added
clang
|
@llvm/pr-subscribers-clang @llvm/pr-subscribers-clang-static-analyzer-1 Author: Balazs Benics (steakhal) ChangesRequested in: Revert "[analyzer] Harden safeguards for Z3 query times" Revert "[analyzer][NFC] Reorganize Z3 report refutation" This reverts commit eacc3b3. This reverts commit 89c26f6. Patch is 37.47 KiB, truncated to 20.00 KiB below, full version: https://github.com/llvm/llvm-project/pull/95916.diff 14 Files Affected:
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 &,
- ...
[truncated]
|
|
@llvm/pr-subscribers-llvm-support Author: Balazs Benics (steakhal) ChangesRequested in: Revert "[analyzer] Harden safeguards for Z3 query times" Revert "[analyzer][NFC] Reorganize Z3 report refutation" This reverts commit eacc3b3. This reverts commit 89c26f6. Patch is 37.47 KiB, truncated to 20.00 KiB below, full version: https://github.com/llvm/llvm-project/pull/95916.diff 14 Files Affected:
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 &,
- ...
[truncated]
|
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Requested in: #95128 (comment)
Revert "[analyzer] Harden safeguards for Z3 query times"
Revert "[analyzer][NFC] Reorganize Z3 report refutation"
This reverts commit eacc3b3.
This reverts commit 89c26f6.