llvmbot wrote:
<!--LLVM PR SUMMARY COMMENT--> @llvm/pr-subscribers-llvm-support Author: Balazs Benics (steakhal) <details> <summary>Changes</summary> Requested in: https://github.com/llvm/llvm-project/pull/95128#issuecomment-2176008007 Revert "[analyzer] Harden safeguards for Z3 query times" Revert "[analyzer][NFC] Reorganize Z3 report refutation" This reverts commit eacc3b3504be061f7334410dd0eb599688ba103a. This reverts commit 89c26f6c7b0a6dfa257ec090fcf5b6e6e0c89aab. --- 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: - (modified) clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def (-20) - (modified) clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h (+23) - (removed) clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h (-92) - (modified) clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h (+1-4) - (modified) clang/lib/StaticAnalyzer/Core/BugReporter.cpp (+6-30) - (modified) clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp (+76) - (modified) clang/lib/StaticAnalyzer/Core/CMakeLists.txt (-1) - (removed) clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp (-160) - (modified) clang/test/Analysis/analyzer-config.c (-3) - (removed) clang/test/Analysis/z3/crosscheck-statistics.c (-33) - (modified) clang/unittests/StaticAnalyzer/CMakeLists.txt (-1) - (removed) clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp (-143) - (modified) llvm/include/llvm/Support/SMTAPI.h (-19) - (modified) llvm/lib/Support/Z3Solver.cpp (+20-96) ``````````diff 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] `````````` </details> https://github.com/llvm/llvm-project/pull/95916 _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
