[analyzer][NFC] Reorganize Z3 report refutation by steakhal · Pull Request #95128 · llvm/llvm-project (original) (raw)

@llvm/pr-subscribers-llvm-support
@llvm/pr-subscribers-clang-static-analyzer-1

@llvm/pr-subscribers-clang

Author: Balazs Benics (steakhal)

Changes

This change keeps existing behavior, namely that if we hit a Z3 timeout
we will accept the report as "satisfiable".

This prepares for the commit "Harden safeguards for Z3 query times".
https://discourse.llvm.org/t/analyzer-rfc-taming-z3-query-times/79520

Patch is 27.25 KiB, truncated to 20.00 KiB below, full version: https://github.com/llvm/llvm-project/pull/95128.diff

12 Files Affected:

diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h index cc3d93aabafda..f97514955a591 100644 --- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h +++ b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h @@ -597,29 +597,6 @@ 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();

-};

/// 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 new file mode 100644 index 0000000000000..3ec59e3037363 --- /dev/null +++ b/clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h @@ -0,0 +1,66 @@ +//===- 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 IsSAT = std::nullopt; + }; + explicit Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result); + + 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; +}; + +/// The oracle will decide if a report should be accepted or rejected based on +/// the results of the Z3 solver. +class Z3CrosscheckOracle { +public: + enum Z3Decision { + AcceptReport, // The report was SAT. + RejectReport, // The report was UNSAT or UNDEF. + }; + + /// 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 + +#endif // LLVM_CLANG_STATICANALYZER_CORE_BUGREPORTER_Z3CROSSCHECKVISITOR_H \ No newline at end of file diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index 5116a4c06850d..bf18c353b8508 100644 --- a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h +++ b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h @@ -34,7 +34,10 @@ class SMTConstraintManager : public clang::ento::SimpleConstraintManager { public: SMTConstraintManager(clang::ento::ExprEngine *EE, clang::ento::SValBuilder &SB) - : SimpleConstraintManager(EE, SB) {} + : SimpleConstraintManager(EE, SB) { + Solver->setBoolParam("model", true); // Enable model finding + Solver->setUnsignedParam("timeout", 15000 /milliseconds/); + } virtual SMTConstraintManager() = default; //===------------------------------------------------------------------===// diff --git a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp index 14ca507a16d55..c9a7fd0e035c2 100644 --- a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp +++ b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp @@ -35,6 +35,7 @@ #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" @@ -86,6 +87,11 @@ 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(NumTimesReportEQClassWasExhausted, + "Number of times all reports of an equivalence class was refuted"); + BugReporterVisitor::BugReporterVisitor() = default; void BugReporterContext::anchor() {} @@ -2864,21 +2870,31 @@ std::optional PathDiagnosticBuilder::findValidReport( // If crosscheck is enabled, remove all visitors, add the refutation // visitor and check again R->clearVisitors(); - R->addVisitor(); + Z3CrosscheckVisitor::Z3Result CrosscheckResult; + R->addVisitor(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 (Z3CrosscheckOracle::interpretQueryResult(CrosscheckResult)) { + case Z3CrosscheckOracle::RejectReport: + ++NumTimesReportRefuted; + R->markInvalid("Infeasible constraints", /Data=/nullptr); + continue; + case Z3CrosscheckOracle::AcceptReport: + ++NumTimesReportPassesZ3; + break; + } } - // 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)); + assert(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 487a3bd16b674..68dac65949117 100644 --- a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp +++ b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp @@ -3446,82 +3446,6 @@ 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);

-}

-void FalsePositiveRefutationBRVisitor::addConstraints( - const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) { - // Collect new constraints - ConstraintMap NewCs = getConstraintMap(N->getState()); - ConstraintMap::Factory &CF = N->getState()->get_context();

diff --git a/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp new file mode 100644 index 0000000000000..20cd8434cbdc6 --- /dev/null +++ b/clang/lib/StaticAnalyzer/Core/Z3CrosscheckVisitor.cpp @@ -0,0 +1,118 @@ +//===- 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 declares the visitor and utilities around it for Z3 report +// refutation. +// +//===----------------------------------------------------------------------===// + +#include "clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.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" + +#define DEBUG_TYPE "Z3CrosscheckOracle" + +STATISTIC(NumZ3QueriesDone, "Number of Z3 queries done"); +STATISTIC(NumTimesZ3TimedOut, "Number of times Z3 query timed out"); + +STATISTIC(NumTimesZ3QueryAcceptsReport,

+STATISTIC(NumTimesZ3QueryRejectReport,

clang_target_link_libraries(StaticAnalysisTests diff --git a/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp new file mode 100644 index 0000000000000..efad4dd3f03b9 --- /dev/null +++ b/clang/unittests/StaticAnalyzer/Z3CrosscheckOracleTest.cpp @@ -0,0 +1,59 @@ +//===- 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/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 std::optional SAT = true; +static constexpr std::optional UNSAT = false; +static constexpr std::optional UNDEF = std::nullopt; + +namespace { + +struct Z3CrosscheckOracleTest : public testing::Test {