forked from llvm/llvm-project
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[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: llvm#95128
- Loading branch information
Showing
12 changed files
with
419 additions
and
126 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
66 changes: 66 additions & 0 deletions
66
clang/include/clang/StaticAnalyzer/Core/BugReporter/Z3CrosscheckVisitor.h
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -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 |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,118 @@ | ||
| //===- 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/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, | ||
| "Number of Z3 queries accepting a report"); | ||
| STATISTIC(NumTimesZ3QueryRejectReport, | ||
| "Number of Z3 queries rejecting a report"); | ||
|
|
||
| using namespace clang; | ||
| using namespace ento; | ||
|
|
||
| Z3CrosscheckVisitor::Z3CrosscheckVisitor(Z3CrosscheckVisitor::Z3Result &Result) | ||
| : Constraints(ConstraintMap::Factory().getEmptyMap()), Result(Result) {} | ||
|
|
||
| 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(); | ||
| RefutationSolver->setBoolParam("model", true); // Enable model finding | ||
| RefutationSolver->setUnsignedParam("timeout", 15000); // 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 | ||
| std::optional<bool> IsSAT = RefutationSolver->check(); | ||
| Result = Z3Result{IsSAT}; | ||
| } | ||
|
|
||
| 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; | ||
|
|
||
| if (!Query.IsSAT.has_value()) { | ||
| // For backward compatibility, let's accept the first timeout. | ||
| ++NumTimesZ3TimedOut; | ||
| return AcceptReport; | ||
| } | ||
|
|
||
| if (Query.IsSAT.value()) { | ||
| ++NumTimesZ3QueryAcceptsReport; | ||
| return AcceptReport; // sat | ||
| } | ||
|
|
||
| ++NumTimesZ3QueryRejectReport; | ||
| return RejectReport; // unsat | ||
| } |
Oops, something went wrong.