diff options
author | Balazs Benics <benicsbalazs@gmail.com> | 2024-06-18 09:42:29 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2024-06-18 09:42:29 +0200 |
commit | 89c26f6c7b0a6dfa257ec090fcf5b6e6e0c89aab (patch) | |
tree | 602de62aa296796fb16700ead87642594f9edd77 /clang/include | |
parent | 7dd7d5749f7d9d98fec50ee88e633e8b85c6502a (diff) | |
download | llvm-89c26f6c7b0a6dfa257ec090fcf5b6e6e0c89aab.zip llvm-89c26f6c7b0a6dfa257ec090fcf5b6e6e0c89aab.tar.gz llvm-89c26f6c7b0a6dfa257ec090fcf5b6e6e0c89aab.tar.bz2 |
[analyzer][NFC] Reorganize Z3 report refutation
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
Reviewers: NagyDonat, haoNoQ, Xazax-hun, mikhailramalho, Szelethus
Reviewed By: NagyDonat
Pull Request: https://github.com/llvm/llvm-project/pull/95128
Diffstat (limited to 'clang/include')
3 files changed, 70 insertions, 24 deletions
diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h index cc3d93a..f975149 100644 --- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h +++ b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h @@ -597,29 +597,6 @@ public: 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 new file mode 100644 index 0000000..9413fd7 --- /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<bool> 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 diff --git a/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h b/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h index 5116a4c..bf18c353 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; //===------------------------------------------------------------------===// |