Author: Balazs Benics Date: 2024-06-18T14:50:00+02:00 New Revision: bbcee744465c72b8000321defd85ed3daa290502
URL: https://github.com/llvm/llvm-project/commit/bbcee744465c72b8000321defd85ed3daa290502 DIFF: https://github.com/llvm/llvm-project/commit/bbcee744465c72b8000321defd85ed3daa290502.diff LOG: Revert "[analyzer] Harden safeguards for Z3 query times" This reverts commit eacc3b3504be061f7334410dd0eb599688ba103a. Added: Modified: clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h clang/lib/StaticAnalyzer/Core/BugReporter.cpp clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp clang/test/Analysis/analyzer-config.c clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp Removed: ################################################################################ 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-branch-commits mailing list llvm-branch-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-branch-commits
