https://github.com/steakhal created https://github.com/llvm/llvm-project/pull/95916
Requested in: https://github.com/llvm/llvm-project/pull/95128#issuecomment-2176008007 Revert "[analyzer] Harden safeguards for Z3 query times" Revert "[analyzer][NFC] Reorganize Z3 report refutation" This reverts commit eacc3b3504be061f7334410dd0eb599688ba103a. This reverts commit 89c26f6c7b0a6dfa257ec090fcf5b6e6e0c89aab. >From 0a9434a872ea9a47a56c1c8fd74474aec52fea0d Mon Sep 17 00:00:00 2001 From: Balazs Benics <benicsbal...@gmail.com> Date: Tue, 18 Jun 2024 14:53:07 +0200 Subject: [PATCH] Revert Z3 changes Requested in: https://github.com/llvm/llvm-project/pull/95128#issuecomment-2176008007 Revert "[analyzer] Harden safeguards for Z3 query times" Revert "[analyzer][NFC] Reorganize Z3 report refutation" This reverts commit eacc3b3504be061f7334410dd0eb599688ba103a. This reverts commit 89c26f6c7b0a6dfa257ec090fcf5b6e6e0c89aab. --- .../StaticAnalyzer/Core/AnalyzerOptions.def | 20 --- .../Core/BugReporter/BugReporterVisitors.h | 23 +++ .../Core/BugReporter/Z3CrosscheckVisitor.h | 92 ---------- .../Core/PathSensitive/SMTConstraintManager.h | 5 +- clang/lib/StaticAnalyzer/Core/BugReporter.cpp | 36 +--- .../Core/BugReporterVisitors.cpp | 76 +++++++++ clang/lib/StaticAnalyzer/Core/CMakeLists.txt | 1 - .../Core/Z3CrosscheckVisitor.cpp | 160 ------------------ clang/test/Analysis/analyzer-config.c | 3 - .../test/Analysis/z3/crosscheck-statistics.c | 33 ---- clang/unittests/StaticAnalyzer/CMakeLists.txt | 1 - .../StaticAnalyzer/Z3CrosscheckOracleTest.cpp | 143 ---------------- llvm/include/llvm/Support/SMTAPI.h | 19 --- llvm/lib/Support/Z3Solver.cpp | 116 +++---------- 14 files changed, 126 insertions(+), 602 deletions(-) delete mode 100644 clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h delete mode 100644 clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp delete mode 100644 clang/test/Analysis/z3/crosscheck-statistics.c delete mode 100644 clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp diff --git a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def index 29aa6a3b8a16e..f008c9c581d95 100644 --- a/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def +++ b/clang/include/clang/StaticAnalyzer/Core/AnalyzerOptions.def @@ -184,26 +184,6 @@ ANALYZER_OPTION(bool, ShouldCrosscheckWithZ3, "crosscheck-with-z3", "constraint manager backend.", false) -ANALYZER_OPTION( - unsigned, Z3CrosscheckEQClassTimeoutThreshold, - "crosscheck-with-z3-eqclass-timeout-threshold", - "Set a timeout for bug report equivalence classes in milliseconds. " - "If we exhaust this threshold, we will drop the bug report eqclass " - "instead of doing more Z3 queries. Set 0 for no timeout.", 700) - -ANALYZER_OPTION( - unsigned, Z3CrosscheckTimeoutThreshold, - "crosscheck-with-z3-timeout-threshold", - "Set a timeout for individual Z3 queries in milliseconds. " - "Set 0 for no timeout.", 300) - -ANALYZER_OPTION( - unsigned, Z3CrosscheckRLimitThreshold, - "crosscheck-with-z3-rlimit-threshold", - "Set the Z3 resource limit threshold. This sets a deterministic cutoff " - "point for Z3 queries, as longer queries usually consume more resources. " - "Set 0 for unlimited.", 400'000) - ANALYZER_OPTION(bool, ShouldReportIssuesInMainSourceFile, "report-in-main-source-file", "Whether or not the diagnostic report should be always " diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h index f97514955a591..cc3d93aabafda 100644 --- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h +++ b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h @@ -597,6 +597,29 @@ class SuppressInlineDefensiveChecksVisitor final : public BugReporterVisitor { PathSensitiveBugReport &BR) override; }; +/// The bug visitor will walk all the nodes in a path and collect all the +/// constraints. When it reaches the root node, will create a refutation +/// manager and check if the constraints are satisfiable +class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor { +private: + /// Holds the constraints in a given path + ConstraintMap Constraints; + +public: + FalsePositiveRefutationBRVisitor(); + + void Profile(llvm::FoldingSetNodeID &ID) const override; + + PathDiagnosticPieceRef VisitNode(const ExplodedNode *N, + BugReporterContext &BRC, + PathSensitiveBugReport &BR) override; + + void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode, + PathSensitiveBugReport &BR) override; + void addConstraints(const ExplodedNode *N, + bool OverwriteConstraintsOnExistingSyms); +}; + /// The visitor detects NoteTags and displays the event notes they contain. class TagVisitor : public BugReporterVisitor { public: diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h deleted file mode 100644 index 439f37fa8604f..0000000000000 --- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h +++ /dev/null @@ -1,92 +0,0 @@ -//===- Z3CrosscheckVisitor.h - Crosscheck reports with Z3 -------*- C++ -*-===// -// -// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. -// See https://llvm.org/LICENSE.txt for license information. -// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception -// -//===----------------------------------------------------------------------===// -// -// This file defines the visitor and utilities around it for Z3 report -// refutation. -// -//===----------------------------------------------------------------------===// - -#ifndef LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H -#define LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H - -#include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h" - -namespace clang::ento { - -/// The bug visitor will walk all the nodes in a path and collect all the -/// constraints. When it reaches the root node, will create a refutation -/// manager and check if the constraints are satisfiable. -class Z3CrosscheckVisitor final : public BugReporterVisitor { -public: - struct Z3Result { - std::optional<bool> IsSAT = std::nullopt; - unsigned Z3QueryTimeMilliseconds = 0; - unsigned UsedRLimit = 0; - }; - Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result, - const AnalyzerOptions &Opts); - - void Profile(llvm::FoldingSetNodeID &ID) const override; - - PathDiagnosticPieceRef VisitNode(const ExplodedNode *N, - BugReporterContext &BRC, - PathSensitiveBugReport &BR) override; - - void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode, - PathSensitiveBugReport &BR) override; - -private: - void addConstraints(const ExplodedNode *N, - bool OverwriteConstraintsOnExistingSyms); - - /// Holds the constraints in a given path. - ConstraintMap Constraints; - Z3Result &Result; - const AnalyzerOptions &Opts; -}; - -/// The oracle will decide if a report should be accepted or rejected based on -/// the results of the Z3 solver and the statistics of the queries of a report -/// equivalenece class. -class Z3CrosscheckOracle { -public: - explicit Z3CrosscheckOracle(const AnalyzerOptions &Opts) : Opts(Opts) {} - - enum Z3Decision { - AcceptReport, // The report was SAT. - RejectReport, // The report was UNSAT or UNDEF. - RejectEQClass, // The heuristic suggests to skip the current eqclass. - }; - - /// Updates the internal state with the new Z3Result and makes a decision how - /// to proceed: - /// - Accept the report if the Z3Result was SAT. - /// - Suggest dropping the report equvalence class based on the accumulated - /// statistics. - /// - Otherwise, reject the report if the Z3Result was UNSAT or UNDEF. - /// - /// Conditions for dropping the equivalence class: - /// - Accumulative time spent in Z3 checks is more than 700ms in the eqclass. - /// - Hit the 300ms query timeout in the report eqclass. - /// - Hit the 400'000 rlimit in the report eqclass. - /// - /// All these thresholds are configurable via the analyzer options. - /// - /// Refer to - /// https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520 to - /// see why this heuristic was chosen. - Z3Decision interpretQueryResult(const Z3CrosscheckVisitor::Z3Result &Meta); - -private: - const AnalyzerOptions &Opts; - unsigned AccumulatedZ3QueryTimeInEqClass = 0; // ms -}; - -} // namespace clang::ento - -#endif // LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index bf18c353b8508..5116a4c06850d 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -34,10 +34,7 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager { public: SMTConstraintManager(clang::ento::ExprEngine *EE, clang::ento::SValBuilder &SB) - : SimpleConstraintManager(EE, SB) { - Solver->setBoolParam("model", true); // Enable model finding - Solver->setUnsignedParam("timeout", 15000 /*milliseconds*/); - } + : SimpleConstraintManager(EE, SB) {} virtual ~SMTConstraintManager() = default; //===------------------------------------------------------------------===// diff --git a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp index e2002bfbe594a..14ca507a16d55 100644 --- a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp +++ b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp @@ -35,7 +35,6 @@ #include "clang/StaticAnalyzer/Core/AnalyzerOptions.h" #include "clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h" #include "clang/StaticAnalyzer/Core/BugReporter/BugType.h" -#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h" #include "clang/StaticAnalyzer/Core/Checker.h" #include "clang/StaticAnalyzer/Core/CheckerManager.h" #include "clang/StaticAnalyzer/Core/CheckerRegistryData.h" @@ -87,14 +86,6 @@ STATISTIC(MaxValidBugClassSize, "The maximum number of bug reports in the same equivalence class " "where at least one report is valid (not suppressed)"); -STATISTIC(NumTimesReportPassesZ3, "Number of reports passed Z3"); -STATISTIC(NumTimesReportRefuted, "Number of reports refuted by Z3"); -STATISTIC(NumTimesReportEQClassAborted, - "Number of times a report equivalence class was aborted by the Z3 " - "oracle heuristic"); -STATISTIC(NumTimesReportEQClassWasExhausted, - "Number of times all reports of an equivalence class was refuted"); - BugReporterVisitor::~BugReporterVisitor() = default; void BugReporterContext::anchor() {} @@ -2843,7 +2834,6 @@ generateVisitorsDiagnostics(PathSensitiveBugReport *R, std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport( ArrayRef<PathSensitiveBugReport *> &bugReports, PathSensitiveBugReporter &Reporter) { - Z3CrosscheckOracle Z3Oracle(Reporter.getAnalyzerOptions()); BugPathGetter BugGraph(&Reporter.getGraph(), bugReports); @@ -2874,35 +2864,21 @@ std::optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport( // If crosscheck is enabled, remove all visitors, add the refutation // visitor and check again R->clearVisitors(); - Z3CrosscheckVisitor::Z3Result CrosscheckResult; - R->addVisitor<Z3CrosscheckVisitor>(CrosscheckResult, - Reporter.getAnalyzerOptions()); + R->addVisitor<FalsePositiveRefutationBRVisitor>(); // We don't overwrite the notes inserted by other visitors because the // refutation manager does not add any new note to the path generateVisitorsDiagnostics(R, BugPath->ErrorNode, BRC); - switch (Z3Oracle.interpretQueryResult(CrosscheckResult)) { - case Z3CrosscheckOracle::RejectReport: - ++NumTimesReportRefuted; - R->markInvalid("Infeasible constraints", /*Data=*/nullptr); - continue; - case Z3CrosscheckOracle::RejectEQClass: - ++NumTimesReportEQClassAborted; - return {}; - case Z3CrosscheckOracle::AcceptReport: - ++NumTimesReportPassesZ3; - break; - } } - assert(R->isValid()); - return PathDiagnosticBuilder(std::move(BRC), std::move(BugPath->BugPath), - BugPath->Report, BugPath->ErrorNode, - std::move(visitorNotes)); + // Check if the bug is still valid + if (R->isValid()) + return PathDiagnosticBuilder( + std::move(BRC), std::move(BugPath->BugPath), BugPath->Report, + BugPath->ErrorNode, std::move(visitorNotes)); } } - ++NumTimesReportEQClassWasExhausted; return {}; } diff --git a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp index 68dac65949117..487a3bd16b674 100644 --- a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp +++ b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp @@ -3446,6 +3446,82 @@ UndefOrNullArgVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &BRC, return nullptr; } +//===----------------------------------------------------------------------===// +// Implementation of FalsePositiveRefutationBRVisitor. +//===----------------------------------------------------------------------===// + +FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor() + : Constraints(ConstraintMap::Factory().getEmptyMap()) {} + +void FalsePositiveRefutationBRVisitor::finalizeVisitor( + BugReporterContext &BRC, const ExplodedNode *EndPathNode, + PathSensitiveBugReport &BR) { + // Collect new constraints + addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true); + + // Create a refutation manager + llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver(); + ASTContext &Ctx = BRC.getASTContext(); + + // Add constraints to the solver + for (const auto &I : Constraints) { + const SymbolRef Sym = I.first; + auto RangeIt = I.second.begin(); + + llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr( + RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(), + /*InRange=*/true); + while ((++RangeIt) != I.second.end()) { + SMTConstraints = RefutationSolver->mkOr( + SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym, + RangeIt->From(), RangeIt->To(), + /*InRange=*/true)); + } + + RefutationSolver->addConstraint(SMTConstraints); + } + + // And check for satisfiability + std::optional<bool> IsSAT = RefutationSolver->check(); + if (!IsSAT) + return; + + if (!*IsSAT) + BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext()); +} + +void FalsePositiveRefutationBRVisitor::addConstraints( + const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) { + // Collect new constraints + ConstraintMap NewCs = getConstraintMap(N->getState()); + ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>(); + + // Add constraints if we don't have them yet + for (auto const &C : NewCs) { + const SymbolRef &Sym = C.first; + if (!Constraints.contains(Sym)) { + // This symbol is new, just add the constraint. + Constraints = CF.add(Constraints, Sym, C.second); + } else if (OverwriteConstraintsOnExistingSyms) { + // Overwrite the associated constraint of the Symbol. + Constraints = CF.remove(Constraints, Sym); + Constraints = CF.add(Constraints, Sym, C.second); + } + } +} + +PathDiagnosticPieceRef FalsePositiveRefutationBRVisitor::VisitNode( + const ExplodedNode *N, BugReporterContext &, PathSensitiveBugReport &) { + addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false); + return nullptr; +} + +void FalsePositiveRefutationBRVisitor::Profile( + llvm::FoldingSetNodeID &ID) const { + static int Tag = 0; + ID.AddPointer(&Tag); +} + //===----------------------------------------------------------------------===// // Implementation of TagVisitor. //===----------------------------------------------------------------------===// diff --git a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt b/clang/lib/StaticAnalyzer/Core/CMakeLists.txt index fb9394a519eb7..8672876c0608d 100644 --- a/clang/lib/StaticAnalyzer/Core/CMakeLists.txt +++ b/clang/lib/StaticAnalyzer/Core/CMakeLists.txt @@ -51,7 +51,6 @@ add_clang_library(clangStaticAnalyzerCore SymbolManager.cpp TextDiagnostics.cpp WorkList.cpp - Z3CrosscheckVisitor.cpp LINK_LIBS clangAST diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp deleted file mode 100644 index 739db951b3e18..0000000000000 --- a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp +++ /dev/null @@ -1,160 +0,0 @@ -//===- Z3CrosscheckVisitor.cpp - Crosscheck reports with Z3 -----*- C++ -*-===// -// -// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. -// See https://llvm.org/LICENSE.txt for license information. -// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception -// -//===----------------------------------------------------------------------===// -// -// This file declares the visitor and utilities around it for Z3 report -// refutation. -// -//===----------------------------------------------------------------------===// - -#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h" -#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h" -#include "clang/StaticAnalyzer/Core/BugReporter/BugReporter.h" -#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h" -#include "llvm/ADT/Statistic.h" -#include "llvm/Support/SMTAPI.h" -#include "llvm/Support/Timer.h" - -#define DEBUG_TYPE "Z3CrosscheckOracle" - -STATISTIC(NumZ3QueriesDone, "Number of Z3 queries done"); -STATISTIC(NumTimesZ3TimedOut, "Number of times Z3 query timed out"); -STATISTIC(NumTimesZ3ExhaustedRLimit, - "Number of times Z3 query exhausted the rlimit"); -STATISTIC(NumTimesZ3SpendsTooMuchTimeOnASingleEQClass, - "Number of times report equivalenece class was cut because it spent " - "too much time in Z3"); - -STATISTIC(NumTimesZ3QueryAcceptsReport, - "Number of Z3 queries accepting a report"); -STATISTIC(NumTimesZ3QueryRejectReport, - "Number of Z3 queries rejecting a report"); -STATISTIC(NumTimesZ3QueryRejectEQClass, - "Number of times rejecting an report equivalenece class"); - -using namespace clang; -using namespace ento; - -Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result, - const AnalyzerOptions &Opts) - : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result), - Opts(Opts) {} - -void Z3CrosscheckVisitor::finalizeVisitor(BugReporterContext &BRC, - const ExplodedNode *EndPathNode, - PathSensitiveBugReport &BR) { - // Collect new constraints - addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true); - - // Create a refutation manager - llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver(); - if (Opts.Z3CrosscheckRLimitThreshold) - RefutationSolver->setUnsignedParam("rlimit", - Opts.Z3CrosscheckRLimitThreshold); - if (Opts.Z3CrosscheckTimeoutThreshold) - RefutationSolver->setUnsignedParam("timeout", - Opts.Z3CrosscheckTimeoutThreshold); // ms - - ASTContext &Ctx = BRC.getASTContext(); - - // Add constraints to the solver - for (const auto &[Sym, Range] : Constraints) { - auto RangeIt = Range.begin(); - - llvm::SMTExprRef SMTConstraints = SMTConv::getRangeExpr( - RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(), - /*InRange=*/true); - while ((++RangeIt) != Range.end()) { - SMTConstraints = RefutationSolver->mkOr( - SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym, - RangeIt->From(), RangeIt->To(), - /*InRange=*/true)); - } - RefutationSolver->addConstraint(SMTConstraints); - } - - // And check for satisfiability - llvm::TimeRecord Start = llvm::TimeRecord::getCurrentTime(/*Start=*/true); - std::optional<bool> IsSAT = RefutationSolver->check(); - llvm::TimeRecord Diff = llvm::TimeRecord::getCurrentTime(/*Start=*/false); - Diff -= Start; - Result = Z3Result{ - IsSAT, - static_cast<unsigned>(Diff.getWallTime() * 1000), - RefutationSolver->getStatistics()->getUnsigned("rlimit count"), - }; -} - -void Z3CrosscheckVisitor::addConstraints( - const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) { - // Collect new constraints - ConstraintMap NewCs = getConstraintMap(N->getState()); - ConstraintMap::Factory &CF = N->getState()->get_context<ConstraintMap>(); - - // Add constraints if we don't have them yet - for (auto const &[Sym, Range] : NewCs) { - if (!Constraints.contains(Sym)) { - // This symbol is new, just add the constraint. - Constraints = CF.add(Constraints, Sym, Range); - } else if (OverwriteConstraintsOnExistingSyms) { - // Overwrite the associated constraint of the Symbol. - Constraints = CF.remove(Constraints, Sym); - Constraints = CF.add(Constraints, Sym, Range); - } - } -} - -PathDiagnosticPieceRef -Z3CrosscheckVisitor::VisitNode(const ExplodedNode *N, BugReporterContext &, - PathSensitiveBugReport &) { - addConstraints(N, /*OverwriteConstraintsOnExistingSyms=*/false); - return nullptr; -} - -void Z3CrosscheckVisitor::Profile(llvm::FoldingSetNodeID &ID) const { - static int Tag = 0; - ID.AddPointer(&Tag); -} - -Z3CrosscheckOracle::Z3Decision Z3CrosscheckOracle::interpretQueryResult( - const Z3CrosscheckVisitor::Z3Result &Query) { - ++NumZ3QueriesDone; - AccumulatedZ3QueryTimeInEqClass += Query.Z3QueryTimeMilliseconds; - - if (Query.IsSAT && Query.IsSAT.value()) { - ++NumTimesZ3QueryAcceptsReport; - return AcceptReport; - } - - // Suggest cutting the EQClass if certain heuristics trigger. - if (Opts.Z3CrosscheckTimeoutThreshold && - Query.Z3QueryTimeMilliseconds >= Opts.Z3CrosscheckTimeoutThreshold) { - ++NumTimesZ3TimedOut; - ++NumTimesZ3QueryRejectEQClass; - return RejectEQClass; - } - - if (Opts.Z3CrosscheckRLimitThreshold && - Query.UsedRLimit >= Opts.Z3CrosscheckRLimitThreshold) { - ++NumTimesZ3ExhaustedRLimit; - ++NumTimesZ3QueryRejectEQClass; - return RejectEQClass; - } - - if (Opts.Z3CrosscheckEQClassTimeoutThreshold && - AccumulatedZ3QueryTimeInEqClass > - Opts.Z3CrosscheckEQClassTimeoutThreshold) { - ++NumTimesZ3SpendsTooMuchTimeOnASingleEQClass; - ++NumTimesZ3QueryRejectEQClass; - return RejectEQClass; - } - - // If no cutoff heuristics trigger, and the report is "unsat" or "undef", - // then reject the report. - ++NumTimesZ3QueryRejectReport; - return RejectReport; -} diff --git a/clang/test/Analysis/analyzer-config.c b/clang/test/Analysis/analyzer-config.c index 2a4c40005a4dc..fda920fa3951e 100644 --- a/clang/test/Analysis/analyzer-config.c +++ b/clang/test/Analysis/analyzer-config.c @@ -43,9 +43,6 @@ // CHECK-NEXT: cplusplus.Move:WarnOn = KnownsAndLocals // CHECK-NEXT: cplusplus.SmartPtrModeling:ModelSmartPtrDereference = false // CHECK-NEXT: crosscheck-with-z3 = false -// CHECK-NEXT: crosscheck-with-z3-eqclass-timeout-threshold = 700 -// CHECK-NEXT: crosscheck-with-z3-rlimit-threshold = 400000 -// CHECK-NEXT: crosscheck-with-z3-timeout-threshold = 300 // CHECK-NEXT: ctu-dir = "" // CHECK-NEXT: ctu-import-cpp-threshold = 8 // CHECK-NEXT: ctu-import-threshold = 24 diff --git a/clang/test/Analysis/z3/crosscheck-statistics.c b/clang/test/Analysis/z3/crosscheck-statistics.c deleted file mode 100644 index 7192824c5be31..0000000000000 --- a/clang/test/Analysis/z3/crosscheck-statistics.c +++ /dev/null @@ -1,33 +0,0 @@ -// RUN: %clang_analyze_cc1 -analyzer-checker=core -verify %s \ -// RUN: -analyzer-config crosscheck-with-z3=true \ -// RUN: -analyzer-stats 2>&1 | FileCheck %s - -// REQUIRES: z3 - -// expected-error@1 {{Z3 refutation rate:1/2}} - -int accepting(int n) { - if (n == 4) { - n = n / (n-4); // expected-warning {{Division by zero}} - } - return n; -} - -int rejecting(int n, int x) { - // Let's make the path infeasible. - if (2 < x && x < 5 && x*x == x*x*x) { - // Have the same condition as in 'accepting'. - if (n == 4) { - n = x / (n-4); // no-warning: refuted - } - } - return n; -} - -// CHECK: 1 BugReporter - Number of times all reports of an equivalence class was refuted -// CHECK-NEXT: 1 BugReporter - Number of reports passed Z3 -// CHECK-NEXT: 1 BugReporter - Number of reports refuted by Z3 - -// CHECK: 1 Z3CrosscheckVisitor - Number of Z3 queries accepting a report -// CHECK-NEXT: 1 Z3CrosscheckVisitor - Number of Z3 queries rejecting a report -// CHECK-NEXT: 2 Z3CrosscheckVisitor - Number of Z3 queries done diff --git a/clang/unittests/StaticAnalyzer/CMakeLists.txt b/clang/unittests/StaticAnalyzer/CMakeLists.txt index dcc557b44fb31..ff34d5747cc81 100644 --- a/clang/unittests/StaticAnalyzer/CMakeLists.txt +++ b/clang/unittests/StaticAnalyzer/CMakeLists.txt @@ -21,7 +21,6 @@ add_clang_unittest(StaticAnalysisTests SymbolReaperTest.cpp SValTest.cpp TestReturnValueUnderConstruction.cpp - Z3CrosscheckOracleTest.cpp ) clang_target_link_libraries(StaticAnalysisTests diff --git a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp deleted file mode 100644 index ef07e47ee911b..0000000000000 --- a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp +++ /dev/null @@ -1,143 +0,0 @@ -//===- unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp ----------------===// -// -// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. -// See https://llvm.org/LICENSE.txt for license information. -// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception -// -//===----------------------------------------------------------------------===// - -#include "clang/StaticAnalyzer/Core/AnalyzerOptions.h" -#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h" -#include "gtest/gtest.h" - -using namespace clang; -using namespace ento; - -using Z3Result = Z3CrosscheckVisitor::Z3Result; -using Z3Decision = Z3CrosscheckOracle::Z3Decision; - -static constexpr Z3Decision AcceptReport = Z3Decision::AcceptReport; -static constexpr Z3Decision RejectReport = Z3Decision::RejectReport; -static constexpr Z3Decision RejectEQClass = Z3Decision::RejectEQClass; - -static constexpr std::optional<bool> SAT = true; -static constexpr std::optional<bool> UNSAT = false; -static constexpr std::optional<bool> UNDEF = std::nullopt; - -static unsigned operator""_ms(unsigned long long ms) { return ms; } -static unsigned operator""_step(unsigned long long rlimit) { return rlimit; } - -static const AnalyzerOptions DefaultOpts = [] { - AnalyzerOptions Config; -#define ANALYZER_OPTION_DEPENDS_ON_USER_MODE(TYPE, NAME, CMDFLAG, DESC, \ - SHALLOW_VAL, DEEP_VAL) \ - ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEEP_VAL) -#define ANALYZER_OPTION(TYPE, NAME, CMDFLAG, DESC, DEFAULT_VAL) \ - Config.NAME = DEFAULT_VAL; -#include "clang/StaticAnalyzer/Core/AnalyzerOptions.def" - - // Remember to update the tests in this file when these values change. - // Also update the doc comment of `interpretQueryResult`. - assert(Config.Z3CrosscheckRLimitThreshold == 400'000); - assert(Config.Z3CrosscheckTimeoutThreshold == 300_ms); - // Usually, when the timeout/rlimit threshold is reached, Z3 only slightly - // overshoots until it realizes that it overshoot and needs to back off. - // Consequently, the measured timeout should be fairly close to the threshold. - // Same reasoning applies to the rlimit too. - return Config; -}(); - -namespace { - -class Z3CrosscheckOracleTest : public testing::Test { -public: - Z3Decision interpretQueryResult(const Z3Result &Result) { - return Oracle.interpretQueryResult(Result); - } - -private: - Z3CrosscheckOracle Oracle = Z3CrosscheckOracle(DefaultOpts); -}; - -TEST_F(Z3CrosscheckOracleTest, AcceptsFirstSAT) { - ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step})); -} - -TEST_F(Z3CrosscheckOracleTest, AcceptsSAT) { - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); - ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 1000_step})); -} - -TEST_F(Z3CrosscheckOracleTest, SATWhenItGoesOverTime) { - // Even if it times out, if it is SAT, we should accept it. - ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 310_ms, 1000_step})); -} - -TEST_F(Z3CrosscheckOracleTest, UNSATWhenItGoesOverTime) { - ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 310_ms, 1000_step})); -} - -TEST_F(Z3CrosscheckOracleTest, RejectsTimeout) { - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); - ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 310_ms, 1000_step})); -} - -TEST_F(Z3CrosscheckOracleTest, RejectsUNSATs) { - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); -} - -// Testing cut heuristics: -// ======================= - -TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfSpendsTooMuchTotalTime) { - // Simulate long queries, that barely doesn't trigger the timeout. - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step})); - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step})); - ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 290_ms, 1000_step})); -} - -TEST_F(Z3CrosscheckOracleTest, SATWhenItSpendsTooMuchTotalTime) { - // Simulate long queries, that barely doesn't trigger the timeout. - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step})); - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 290_ms, 1000_step})); - ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 290_ms, 1000_step})); -} - -TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfAttemptsManySmallQueries) { - // Simulate quick, but many queries: 35 quick UNSAT queries. - // 35*20ms = 700ms, which is equal to the 700ms threshold. - for (int i = 0; i < 35; ++i) { - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step})); - } - // Do one more to trigger the heuristic. - ASSERT_EQ(RejectEQClass, interpretQueryResult({UNSAT, 1_ms, 1000_step})); -} - -TEST_F(Z3CrosscheckOracleTest, SATWhenIfAttemptsManySmallQueries) { - // Simulate quick, but many queries: 35 quick UNSAT queries. - // 35*20ms = 700ms, which is equal to the 700ms threshold. - for (int i = 0; i < 35; ++i) { - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 20_ms, 1000_step})); - } - // Do one more to trigger the heuristic, but given this was SAT, we still - // accept the query. - ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 200_ms, 1000_step})); -} - -TEST_F(Z3CrosscheckOracleTest, RejectEQClassIfExhaustsRLimit) { - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); - ASSERT_EQ(RejectEQClass, interpretQueryResult({UNDEF, 25_ms, 405'000_step})); -} - -TEST_F(Z3CrosscheckOracleTest, SATWhenItExhaustsRLimit) { - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); - ASSERT_EQ(RejectReport, interpretQueryResult({UNSAT, 25_ms, 1000_step})); - ASSERT_EQ(AcceptReport, interpretQueryResult({SAT, 25_ms, 405'000_step})); -} - -} // namespace diff --git a/llvm/include/llvm/Support/SMTAPI.h b/llvm/include/llvm/Support/SMTAPI.h index a2a89674414f4..9389c96956dd1 100644 --- a/llvm/include/llvm/Support/SMTAPI.h +++ b/llvm/include/llvm/Support/SMTAPI.h @@ -125,19 +125,6 @@ class SMTExpr { virtual bool equal_to(SMTExpr const &other) const = 0; }; -class SMTSolverStatistics { -public: - SMTSolverStatistics() = default; - virtual ~SMTSolverStatistics() = default; - - virtual double getDouble(llvm::StringRef) const = 0; - virtual unsigned getUnsigned(llvm::StringRef) const = 0; - - virtual void print(raw_ostream &OS) const = 0; - - LLVM_DUMP_METHOD void dump() const; -}; - /// Shared pointer for SMTExprs, used by SMTSolver API. using SMTExprRef = const SMTExpr *; @@ -447,12 +434,6 @@ class SMTSolver { virtual bool isFPSupported() = 0; virtual void print(raw_ostream &OS) const = 0; - - /// Sets the requested option. - virtual void setBoolParam(StringRef Key, bool Value) = 0; - virtual void setUnsignedParam(StringRef Key, unsigned Value) = 0; - - virtual std::unique_ptr<SMTSolverStatistics> getStatistics() const = 0; }; /// Shared pointer for SMTSolvers. diff --git a/llvm/lib/Support/Z3Solver.cpp b/llvm/lib/Support/Z3Solver.cpp index 5a34ff160f6cf..eb671fe2596db 100644 --- a/llvm/lib/Support/Z3Solver.cpp +++ b/llvm/lib/Support/Z3Solver.cpp @@ -6,9 +6,7 @@ // //===----------------------------------------------------------------------===// -#include "llvm/ADT/ScopeExit.h" #include "llvm/Config/config.h" -#include "llvm/Support/NativeFormatting.h" #include "llvm/Support/SMTAPI.h" using namespace llvm; @@ -28,14 +26,18 @@ namespace { class Z3Config { friend class Z3Context; - Z3_config Config = Z3_mk_config(); + Z3_config Config; public: - Z3Config() = default; - Z3Config(const Z3Config &) = delete; - Z3Config(Z3Config &&) = default; - Z3Config &operator=(Z3Config &) = delete; - Z3Config &operator=(Z3Config &&) = default; + Z3Config() : Config(Z3_mk_config()) { + // Enable model finding + Z3_set_param_value(Config, "model", "true"); + // Disable proof generation + Z3_set_param_value(Config, "proof", "false"); + // Set timeout to 15000ms = 15s + Z3_set_param_value(Config, "timeout", "15000"); + } + ~Z3Config() { Z3_del_config(Config); } }; // end class Z3Config @@ -48,22 +50,16 @@ void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) { /// Wrapper for Z3 context class Z3Context { public: - Z3Config Config; Z3_context Context; Z3Context() { - Context = Z3_mk_context_rc(Config.Config); + Context = Z3_mk_context_rc(Z3Config().Config); // The error function is set here because the context is the first object // created by the backend Z3_set_error_handler(Context, Z3ErrorHandler); } - Z3Context(const Z3Context &) = delete; - Z3Context(Z3Context &&) = default; - Z3Context &operator=(Z3Context &) = delete; - Z3Context &operator=(Z3Context &&) = default; - - ~Z3Context() { + virtual ~Z3Context() { Z3_del_context(Context); Context = nullptr; } @@ -266,17 +262,7 @@ class Z3Solver : public SMTSolver { Z3Context Context; - Z3_solver Solver = [this] { - Z3_solver S = Z3_mk_simple_solver(Context.Context); - Z3_solver_inc_ref(Context.Context, S); - return S; - }(); - - Z3_params Params = [this] { - Z3_params P = Z3_mk_params(Context.Context); - Z3_params_inc_ref(Context.Context, P); - return P; - }(); + Z3_solver Solver; // Cache Sorts std::set<Z3Sort> CachedSorts; @@ -285,15 +271,18 @@ class Z3Solver : public SMTSolver { std::set<Z3Expr> CachedExprs; public: - Z3Solver() = default; + Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) { + Z3_solver_inc_ref(Context.Context, Solver); + } + Z3Solver(const Z3Solver &Other) = delete; Z3Solver(Z3Solver &&Other) = delete; Z3Solver &operator=(Z3Solver &Other) = delete; Z3Solver &operator=(Z3Solver &&Other) = delete; - ~Z3Solver() override { - Z3_params_dec_ref(Context.Context, Params); - Z3_solver_dec_ref(Context.Context, Solver); + ~Z3Solver() { + if (Solver) + Z3_solver_dec_ref(Context.Context, Solver); } void addConstraint(const SMTExprRef &Exp) const override { @@ -882,7 +871,6 @@ class Z3Solver : public SMTSolver { } std::optional<bool> check() const override { - Z3_solver_set_params(Context.Context, Solver, Params); Z3_lbool res = Z3_solver_check(Context.Context, Solver); if (res == Z3_L_TRUE) return true; @@ -908,71 +896,8 @@ class Z3Solver : public SMTSolver { void print(raw_ostream &OS) const override { OS << Z3_solver_to_string(Context.Context, Solver); } - - void setUnsignedParam(StringRef Key, unsigned Value) override { - Z3_symbol Sym = Z3_mk_string_symbol(Context.Context, Key.str().c_str()); - Z3_params_set_uint(Context.Context, Params, Sym, Value); - } - - void setBoolParam(StringRef Key, bool Value) override { - Z3_symbol Sym = Z3_mk_string_symbol(Context.Context, Key.str().c_str()); - Z3_params_set_bool(Context.Context, Params, Sym, Value); - } - - std::unique_ptr<SMTSolverStatistics> getStatistics() const override; }; // end class Z3Solver -class Z3Statistics final : public SMTSolverStatistics { -public: - double getDouble(StringRef Key) const override { - auto It = DoubleValues.find(Key.str()); - assert(It != DoubleValues.end()); - return It->second; - }; - unsigned getUnsigned(StringRef Key) const override { - auto It = UnsignedValues.find(Key.str()); - assert(It != UnsignedValues.end()); - return It->second; - }; - - void print(raw_ostream &OS) const override { - for (auto const &[K, V] : UnsignedValues) { - OS << K << ": " << V << '\n'; - } - for (auto const &[K, V] : DoubleValues) { - write_double(OS << K << ": ", V, FloatStyle::Fixed); - OS << '\n'; - } - } - -private: - friend class Z3Solver; - std::unordered_map<std::string, unsigned> UnsignedValues; - std::unordered_map<std::string, double> DoubleValues; -}; - -std::unique_ptr<SMTSolverStatistics> Z3Solver::getStatistics() const { - auto const &C = Context.Context; - Z3_stats S = Z3_solver_get_statistics(C, Solver); - Z3_stats_inc_ref(C, S); - auto StatsGuard = llvm::make_scope_exit([&C, &S] { Z3_stats_dec_ref(C, S); }); - Z3Statistics Result; - - unsigned NumKeys = Z3_stats_size(C, S); - for (unsigned Idx = 0; Idx < NumKeys; ++Idx) { - const char *Key = Z3_stats_get_key(C, S, Idx); - if (Z3_stats_is_uint(C, S, Idx)) { - auto Value = Z3_stats_get_uint_value(C, S, Idx); - Result.UnsignedValues.try_emplace(Key, Value); - } else { - assert(Z3_stats_is_double(C, S, Idx)); - auto Value = Z3_stats_get_double_value(C, S, Idx); - Result.DoubleValues.try_emplace(Key, Value); - } - } - return std::make_unique<Z3Statistics>(std::move(Result)); -} - } // end anonymous namespace #endif @@ -991,4 +916,3 @@ llvm::SMTSolverRef llvm::CreateZ3Solver() { LLVM_DUMP_METHOD void SMTSort::dump() const { print(llvm::errs()); } LLVM_DUMP_METHOD void SMTExpr::dump() const { print(llvm::errs()); } LLVM_DUMP_METHOD void SMTSolver::dump() const { print(llvm::errs()); } -LLVM_DUMP_METHOD void SMTSolverStatistics::dump() const { print(llvm::errs()); } _______________________________________________ cfe-commits mailing list cfe-commits@lists.llvm.org https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
