steakhal created this revision.
steakhal added reviewers: mikhail.ramalho, NoQ, Szelethus, baloghadamsoftware,
xazax.hun.
Herald added subscribers: cfe-commits, ASDenysPetrov, martong, Charusso,
dkrupp, donat.nagy, a.sidorin, rnkovacs, szepet, whisperity.
Herald added a project: clang.
`FalsePositiveRefutationBRVisitor` had a bug(*) where the constraints were not
properly collected thus crosschecked with Z3.
This patch fixes that bug by eliminating the `FalsePositiveRefutationBRVisitor`
completely.
As turned out we don't even need a `BugReporterVisitor` for doing the
crosscheck.
We should simply use the constraints of the `ErrorNode` since that has all the
necessary information.
Bug(*):
The visitor collected all the constraints on a `BugPath`.
Since it is a visitor, it visited the node before the `ErrorNode`, and so on
until the `RootNode`.
At the end visited the ErrorNode explicitly, but that visit had no effect.
Since the constraints were collected into a map, mapping each symbol to its
`RangeSet`.
If the map already had a mapping with the symbol, then it was skipped.
Consider the following case:
We already had a constraint on a symbol, but az the end in the ErrorNode we
have a stricter constraint on that.
This visitor would not utilize that stricter constraint in the crosschecking.
Repository:
rG LLVM Github Monorepo
https://reviews.llvm.org/D78457
Files:
clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
clang/lib/StaticAnalyzer/Core/BugReporter.cpp
clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
Index: clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -2809,74 +2809,6 @@
return nullptr;
}
-//===----------------------------------------------------------------------===//
-// Implementation of FalsePositiveRefutationBRVisitor.
-//===----------------------------------------------------------------------===//
-
-FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor()
- : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {}
-
-void FalsePositiveRefutationBRVisitor::finalizeVisitor(
- BugReporterContext &BRC, const ExplodedNode *EndPathNode,
- PathSensitiveBugReport &BR) {
- // Collect new constraints
- VisitNode(EndPathNode, BRC, BR);
-
- // 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 Constraints = SMTConv::getRangeExpr(
- RefutationSolver, Ctx, Sym, RangeIt->From(), RangeIt->To(),
- /*InRange=*/true);
- while ((++RangeIt) != I.second.end()) {
- Constraints = RefutationSolver->mkOr(
- Constraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
- RangeIt->From(), RangeIt->To(),
- /*InRange=*/true));
- }
-
- RefutationSolver->addConstraint(Constraints);
- }
-
- // And check for satisfiability
- Optional<bool> isSat = RefutationSolver->check();
- if (!isSat.hasValue())
- return;
-
- if (!isSat.getValue())
- BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
-}
-
-PathDiagnosticPieceRef FalsePositiveRefutationBRVisitor::VisitNode(
- const ExplodedNode *N, BugReporterContext &, PathSensitiveBugReport &) {
- // Collect new constraints
- const ConstraintRangeTy &NewCs = N->getState()->get<ConstraintRange>();
- ConstraintRangeTy::Factory &CF =
- N->getState()->get_context<ConstraintRange>();
-
- // Add constraints if we don't have them yet
- for (auto const &C : NewCs) {
- const SymbolRef &Sym = C.first;
- if (!Constraints.contains(Sym)) {
- Constraints = CF.add(Constraints, Sym, C.second);
- }
- }
-
- return nullptr;
-}
-
-void FalsePositiveRefutationBRVisitor::Profile(
- llvm::FoldingSetNodeID &ID) const {
- static int Tag = 0;
- ID.AddPointer(&Tag);
-}
-
//===----------------------------------------------------------------------===//
// Implementation of TagVisitor.
//===----------------------------------------------------------------------===//
Index: clang/lib/StaticAnalyzer/Core/BugReporter.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/BugReporter.cpp
+++ clang/lib/StaticAnalyzer/Core/BugReporter.cpp
@@ -38,6 +38,7 @@
#include "clang/StaticAnalyzer/Core/PathSensitive/ExprEngine.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/MemRegion.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/ProgramState.h"
+#include "clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SVals.h"
#include "clang/StaticAnalyzer/Core/PathSensitive/SymbolManager.h"
#include "llvm/ADT/ArrayRef.h"
@@ -2747,6 +2748,35 @@
return Notes;
}
+Optional<bool> hasContradictionUsingZ3(BugReporterContext &BRC,
+ const ExplodedNode *EndPathNode) {
+ // Create a refutation manager
+ llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
+ ASTContext &Ctx = BRC.getASTContext();
+ ConstraintRangeTy Constraints =
+ EndPathNode->getState()->get<ConstraintRange>();
+
+ // 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);
+ }
+
+ return RefutationSolver->check();
+}
+
Optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
ArrayRef<PathSensitiveBugReport *> &bugReports,
PathSensitiveBugReporter &Reporter) {
@@ -2777,14 +2807,10 @@
if (R->isValid()) {
if (Reporter.getAnalyzerOptions().ShouldCrosscheckWithZ3) {
- // If crosscheck is enabled, remove all visitors, add the refutation
- // visitor and check again
- R->clearVisitors();
- R->addVisitor(std::make_unique<FalsePositiveRefutationBRVisitor>());
-
- // We don't overrite the notes inserted by other visitors because the
- // refutation manager does not add any new note to the path
- generateVisitorsDiagnostics(R, BugPath->ErrorNode, BRC);
+ Optional<bool> IsSAT = hasContradictionUsingZ3(BRC, ErrorNode);
+ if (IsSAT.hasValue() && !IsSAT.getValue())
+ R->markInvalid("Infeasible constraints",
+ ErrorNode->getLocationContext());
}
// Check if the bug is still valid
Index: clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
===================================================================
--- clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
+++ clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
@@ -367,28 +367,6 @@
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
- ConstraintRangeTy 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;
-};
-
-
/// The visitor detects NoteTags and displays the event notes they contain.
class TagVisitor : public BugReporterVisitor {
public:
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
