Revert "[analyzer] Harden safeguards for Z3 query times" #95914
Closed
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
This reverts commit eacc3b3.
llvmbot
added
clang
|
@llvm/pr-subscribers-clang-static-analyzer-1 Author: Balazs Benics (steakhal) ChangesReverts llvm/llvm-project#95129 Reverting this patch as requested in this comment. Full diff: https://github.com/llvm/llvm-project/pull/95914.diff 6 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/Z3CrosscheckVisitor.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
index 439f37fa8604f..9413fd739f607 100644
--- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
+++ b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
@@ -25,11 +25,8 @@ 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);
+ explicit Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result);
void Profile(llvm::FoldingSetNodeID &ID) const override;
@@ -47,44 +44,21 @@ class Z3CrosscheckVisitor final : public BugReporterVisitor {
/// 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.
+/// the results of the Z3 solver.
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.
+ AcceptReport, // The report was SAT.
+ RejectReport, // The report was UNSAT or UNDEF.
};
- /// 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
+ /// 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
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
index e2002bfbe594a..c9a7fd0e035c2 100644
--- a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
+++ b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -89,9 +89,6 @@ STATISTIC(MaxValidBugClassSize,
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");
@@ -2843,7 +2840,6 @@ generateVisitorsDiagnostics(PathSensitiveBugReport *R,
std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
ArrayRef<PathSensitiveBugReport *> &bugReports,
PathSensitiveBugReporter &Reporter) {
- Z3CrosscheckOracle Z3Oracle(Reporter.getAnalyzerOptions());
BugPathGetter BugGraph(&Reporter.getGraph(), bugReports);
@@ -2875,20 +2871,16 @@ std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
// visitor and check again
R->clearVisitors();
Z3CrosscheckVisitor::Z3Result CrosscheckResult;
- R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult,
- Reporter.getAnalyzerOptions());
+ 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 (Z3Oracle.interpretQueryResult(CrosscheckResult)) {
+ switch (Z3CrosscheckOracle::interpretQueryResult(CrosscheckResult)) {
case Z3CrosscheckOracle::RejectReport:
++NumTimesReportRefuted;
R->markInvalid("Infeasible constraints", /*Data=*/nullptr);
continue;
- case Z3CrosscheckOracle::RejectEQClass:
- ++NumTimesReportEQClassAborted;
- return {};
case Z3CrosscheckOracle::AcceptReport:
++NumTimesReportPassesZ3;
break;
diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
index 739db951b3e18..a7db44ef8ea30 100644
--- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
+++ b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
@@ -12,37 +12,26 @@
//===----------------------------------------------------------------------===//
#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) {}
+Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result)
+ : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result) {}
void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
const ExplodedNode *EndPathNode,
@@ -52,12 +41,8 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
// 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
+ RefutationSolver->setBoolParam("model", true); // Enable model finding
+ RefutationSolver->setUnsignedParam("timeout", 15000); // ms
ASTContext &Ctx = BRC.getASTContext();
@@ -78,15 +63,8 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
}
// 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"),
- };
+ Result = Z3Result{IsSAT};
}
void Z3CrosscheckVisitor::addConstraints(
@@ -123,38 +101,18 @@ void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const {
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) {
+ if (!Query.IsSAT.has_value()) {
+ // For backward compatibility, let's accept the first timeout.
++NumTimesZ3TimedOut;
- ++NumTimesZ3QueryRejectEQClass;
- return RejectEQClass;
- }
-
- if (Opts.Z3CrosscheckRLimitThreshold &&
- Query.UsedRLimit >= Opts.Z3CrosscheckRLimitThreshold) {
- ++NumTimesZ3ExhaustedRLimit;
- ++NumTimesZ3QueryRejectEQClass;
- return RejectEQClass;
+ return AcceptReport;
}
- if (Opts.Z3CrosscheckEQClassTimeoutThreshold &&
- AccumulatedZ3QueryTimeInEqClass >
- Opts.Z3CrosscheckEQClassTimeoutThreshold) {
- ++NumTimesZ3SpendsTooMuchTimeOnASingleEQClass;
- ++NumTimesZ3QueryRejectEQClass;
- return RejectEQClass;
+ if (Query.IsSAT.value()) {
+ ++NumTimesZ3QueryAcceptsReport;
+ return AcceptReport; // sat
}
- // If no cutoff heuristics trigger, and the report is "unsat" or "undef",
- // then reject the report.
++NumTimesZ3QueryRejectReport;
- return RejectReport;
+ return RejectReport; // unsat
}
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/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
index ef07e47ee911b..efad4dd3f03b9 100644
--- a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
+++ b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
@@ -6,7 +6,6 @@
//
//===----------------------------------------------------------------------===//
-#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
#include "gtest/gtest.h"
@@ -18,126 +17,43 @@ 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);
+struct Z3CrosscheckOracleTest : public testing::Test {
+ Z3Decision interpretQueryResult(const Z3Result &Result) const {
+ return Z3CrosscheckOracle::interpretQueryResult(Result);
}
-
-private:
- Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(DefaultOpts);
};
TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) {
- ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
+ ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));
}
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}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));
}
-TEST_F(Z3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
- ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step}));
+TEST_F(Z3CrosscheckOracleTest, AcceptsFirstTimeout) {
+ ASSERT_EQ(AcceptReport, interpretQueryResult({UNDEF}));
}
-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, AcceptsTimeout) {
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(AcceptReport, interpretQueryResult({UNDEF}));
}
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}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
}
} // namespace
|
|
@llvm/pr-subscribers-clang Author: Balazs Benics (steakhal) ChangesReverts llvm/llvm-project#95129 Reverting this patch as requested in this comment. Full diff: https://github.com/llvm/llvm-project/pull/95914.diff 6 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/Z3CrosscheckVisitor.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
index 439f37fa8604f..9413fd739f607 100644
--- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
+++ b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
@@ -25,11 +25,8 @@ 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);
+ explicit Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result);
void Profile(llvm::FoldingSetNodeID &ID) const override;
@@ -47,44 +44,21 @@ class Z3CrosscheckVisitor final : public BugReporterVisitor {
/// 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.
+/// the results of the Z3 solver.
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.
+ AcceptReport, // The report was SAT.
+ RejectReport, // The report was UNSAT or UNDEF.
};
- /// 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
+ /// 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
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
index e2002bfbe594a..c9a7fd0e035c2 100644
--- a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
+++ b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -89,9 +89,6 @@ STATISTIC(MaxValidBugClassSize,
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");
@@ -2843,7 +2840,6 @@ generateVisitorsDiagnostics(PathSensitiveBugReport *R,
std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
ArrayRef<PathSensitiveBugReport *> &bugReports,
PathSensitiveBugReporter &Reporter) {
- Z3CrosscheckOracle Z3Oracle(Reporter.getAnalyzerOptions());
BugPathGetter BugGraph(&Reporter.getGraph(), bugReports);
@@ -2875,20 +2871,16 @@ std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
// visitor and check again
R->clearVisitors();
Z3CrosscheckVisitor::Z3Result CrosscheckResult;
- R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult,
- Reporter.getAnalyzerOptions());
+ 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 (Z3Oracle.interpretQueryResult(CrosscheckResult)) {
+ switch (Z3CrosscheckOracle::interpretQueryResult(CrosscheckResult)) {
case Z3CrosscheckOracle::RejectReport:
++NumTimesReportRefuted;
R->markInvalid("Infeasible constraints", /*Data=*/nullptr);
continue;
- case Z3CrosscheckOracle::RejectEQClass:
- ++NumTimesReportEQClassAborted;
- return {};
case Z3CrosscheckOracle::AcceptReport:
++NumTimesReportPassesZ3;
break;
diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
index 739db951b3e18..a7db44ef8ea30 100644
--- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
+++ b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp
@@ -12,37 +12,26 @@
//===----------------------------------------------------------------------===//
#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) {}
+Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result)
+ : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result) {}
void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
const ExplodedNode *EndPathNode,
@@ -52,12 +41,8 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
// 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
+ RefutationSolver->setBoolParam("model", true); // Enable model finding
+ RefutationSolver->setUnsignedParam("timeout", 15000); // ms
ASTContext &Ctx = BRC.getASTContext();
@@ -78,15 +63,8 @@ void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC,
}
// 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"),
- };
+ Result = Z3Result{IsSAT};
}
void Z3CrosscheckVisitor::addConstraints(
@@ -123,38 +101,18 @@ void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const {
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) {
+ if (!Query.IsSAT.has_value()) {
+ // For backward compatibility, let's accept the first timeout.
++NumTimesZ3TimedOut;
- ++NumTimesZ3QueryRejectEQClass;
- return RejectEQClass;
- }
-
- if (Opts.Z3CrosscheckRLimitThreshold &&
- Query.UsedRLimit >= Opts.Z3CrosscheckRLimitThreshold) {
- ++NumTimesZ3ExhaustedRLimit;
- ++NumTimesZ3QueryRejectEQClass;
- return RejectEQClass;
+ return AcceptReport;
}
- if (Opts.Z3CrosscheckEQClassTimeoutThreshold &&
- AccumulatedZ3QueryTimeInEqClass >
- Opts.Z3CrosscheckEQClassTimeoutThreshold) {
- ++NumTimesZ3SpendsTooMuchTimeOnASingleEQClass;
- ++NumTimesZ3QueryRejectEQClass;
- return RejectEQClass;
+ if (Query.IsSAT.value()) {
+ ++NumTimesZ3QueryAcceptsReport;
+ return AcceptReport; // sat
}
- // If no cutoff heuristics trigger, and the report is "unsat" or "undef",
- // then reject the report.
++NumTimesZ3QueryRejectReport;
- return RejectReport;
+ return RejectReport; // unsat
}
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/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
index ef07e47ee911b..efad4dd3f03b9 100644
--- a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
+++ b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp
@@ -6,7 +6,6 @@
//
//===----------------------------------------------------------------------===//
-#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h"
#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h"
#include "gtest/gtest.h"
@@ -18,126 +17,43 @@ 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);
+struct Z3CrosscheckOracleTest : public testing::Test {
+ Z3Decision interpretQueryResult(const Z3Result &Result) const {
+ return Z3CrosscheckOracle::interpretQueryResult(Result);
}
-
-private:
- Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(DefaultOpts);
};
TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) {
- ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step}));
+ ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));
}
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}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(AcceptReport, interpretQueryResult({SAT}));
}
-TEST_F(Z3CrosscheckOracleTest, UNSATWhenItGoesOverTime) {
- ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step}));
+TEST_F(Z3CrosscheckOracleTest, AcceptsFirstTimeout) {
+ ASSERT_EQ(AcceptReport, interpretQueryResult({UNDEF}));
}
-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, AcceptsTimeout) {
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(AcceptReport, interpretQueryResult({UNDEF}));
}
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}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
+ ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT}));
}
} // namespace
|
|
Superseded by a combined revert: #95916 |
steakhal
deleted the
revert-95129-users/steakhal/spr/analyzer-harden-safeguards-for-z3-query-times
branch
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.
Reverts #95129
Reverting this patch as requested in this comment.