[clang] de361df - [analyzer][Z3-refutation] Fix a refutation BugReporterVisitor bug
Balazs Benics via cfe-commits
cfe-commits at lists.llvm.org
Mon Jun 29 09:51:45 PDT 2020
Author: Balazs Benics
Date: 2020-06-29T18:51:24+02:00
New Revision: de361df3f6d0f20bf16a8deb9e6219556d028b81
URL: https://github.com/llvm/llvm-project/commit/de361df3f6d0f20bf16a8deb9e6219556d028b81
DIFF: https://github.com/llvm/llvm-project/commit/de361df3f6d0f20bf16a8deb9e6219556d028b81.diff
LOG: [analyzer][Z3-refutation] Fix a refutation BugReporterVisitor bug
FalsePositiveRefutationBRVisitor had a bug where the constraints were not
properly collected thus crosschecked with Z3.
This patch demonstratest and fixes that bug.
Bug:
The visitor wanted to collect all the constraints on a BugPath.
Since it is a visitor, it stated the visitation of the BugPath with the node
before the ErrorNode. As a final step, it visited the ErrorNode explicitly,
before it processed the collected constraints.
In principle, the ErrorNode should have visited before every other node.
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.
This behavior was flawed if:
We already had a constraint on a symbol, but at the end in the ErrorNode we have
a tighter constraint on that. Therefore, this visitor would not utilize that
tighter constraint during the crosscheck validation.
Differential Revision: https://reviews.llvm.org/D78457
Added:
Modified:
clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
clang/lib/StaticAnalyzer/Core/BugReporter.cpp
clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
Removed:
################################################################################
diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
index de0ee5de81b5..365b1ff1bfe3 100644
--- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
+++ b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
@@ -386,6 +386,8 @@ class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor {
void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,
PathSensitiveBugReport &BR) override;
+ void addConstraints(const ExplodedNode *N,
+ bool OverwriteConstraintsOnExistingSyms);
};
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
index efae511da83b..f4fd495956aa 100644
--- a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp
+++ b/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"
@@ -2783,7 +2784,7 @@ Optional<PathDiagnosticBuilder> PathDiagnosticBuilder::findValidReport(
R->clearVisitors();
R->addVisitor(std::make_unique<FalsePositiveRefutationBRVisitor>());
- // We don't overrite the notes inserted by other visitors because the
+ // 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);
}
diff --git a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
index ad79f7cb9359..ef4d38ff498f 100644
--- a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ b/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -2819,7 +2819,7 @@ void FalsePositiveRefutationBRVisitor::finalizeVisitor(
BugReporterContext &BRC, const ExplodedNode *EndPathNode,
PathSensitiveBugReport &BR) {
// Collect new constraints
- VisitNode(EndPathNode, BRC, BR);
+ addConstraints(EndPathNode, /*OverwriteConstraintsOnExistingSyms=*/true);
// Create a refutation manager
llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
@@ -2830,30 +2830,30 @@ void FalsePositiveRefutationBRVisitor::finalizeVisitor(
const SymbolRef Sym = I.first;
auto RangeIt = I.second.begin();
- llvm::SMTExprRef Constraints = SMTConv::getRangeExpr(
+ llvm::SMTExprRef SMTConstraints = 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));
+ SMTConstraints = RefutationSolver->mkOr(
+ SMTConstraints, SMTConv::getRangeExpr(RefutationSolver, Ctx, Sym,
+ RangeIt->From(), RangeIt->To(),
+ /*InRange=*/true));
}
- RefutationSolver->addConstraint(Constraints);
+ RefutationSolver->addConstraint(SMTConstraints);
}
// And check for satisfiability
- Optional<bool> isSat = RefutationSolver->check();
- if (!isSat.hasValue())
+ Optional<bool> IsSAT = RefutationSolver->check();
+ if (!IsSAT.hasValue())
return;
- if (!isSat.getValue())
+ if (!IsSAT.getValue())
BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
}
-PathDiagnosticPieceRef FalsePositiveRefutationBRVisitor::VisitNode(
- const ExplodedNode *N, BugReporterContext &, PathSensitiveBugReport &) {
+void FalsePositiveRefutationBRVisitor::addConstraints(
+ const ExplodedNode *N, bool OverwriteConstraintsOnExistingSyms) {
// Collect new constraints
const ConstraintRangeTy &NewCs = N->getState()->get<ConstraintRange>();
ConstraintRangeTy::Factory &CF =
@@ -2863,10 +2863,19 @@ PathDiagnosticPieceRef FalsePositiveRefutationBRVisitor::VisitNode(
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;
}
diff --git a/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp b/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
index ad202f844597..7c151c182113 100644
--- a/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
+++ b/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
@@ -170,6 +170,54 @@ TEST(FalsePositiveRefutationBRVisitor, UnSatAtErrorNodeWithNewSymbolNoReport) {
"test.FalsePositiveGenerator:CAN_BE_TRUE\n");
}
+TEST(FalsePositiveRefutationBRVisitor,
+ UnSatAtErrorNodeDueToRefinedConstraintNoReport) {
+ SKIP_WITHOUT_Z3;
+ constexpr auto Code = R"(
+ void reportIfCanBeTrue(bool);
+ void reachedWithNoContradiction();
+ void test(unsigned x, unsigned n) {
+ if (n >= 1 && n <= 2) {
+ if (x >= 3)
+ return;
+ // x: [0,2] and n: [1,2]
+ int y = x + n; // y: '(x+n)' Which is in approximately between 1 and 4.
+
+ // Registers the symbol 'y' with the constraint [1, MAX] in the true
+ // branch.
+ if (y > 0) {
+ // Since the x: [0,2] and n: [1,2], the 'y' is indeed greater than
+ // zero. If we emit a warning here, the constraints on the BugPath is
+ // SAT. Therefore that report is NOT invalidated.
+ reachedWithNoContradiction(); // 'y' can be greater than zero. OK
+
+ // If we ask the analyzer whether the 'y' can be 5. It won't know,
+ // therefore, the state will be created where the 'y' expression is 5.
+ // Although, this assumption is false!
+ // 'y' can not be 5 if the maximal value of both x and n is 2.
+ // The BugPath which become UnSAT in the ErrorNode with a refined
+ // constraint, should be invalidated.
+ reportIfCanBeTrue(y == 5);
+ }
+ }
+ })";
+
+ std::string Diags;
+ EXPECT_TRUE(runCheckerOnCodeWithArgs<addFalsePositiveGenerator>(
+ Code, LazyAssumeAndCrossCheckArgs, Diags));
+ EXPECT_EQ(Diags,
+ "test.FalsePositiveGenerator:REACHED_WITH_NO_CONTRADICTION\n");
+ // Single warning. The second report was invalidated by the visitor.
+
+ // Without enabling the crosscheck-with-z3 both reports are displayed.
+ std::string Diags2;
+ EXPECT_TRUE(runCheckerOnCodeWithArgs<addFalsePositiveGenerator>(
+ Code, LazyAssumeArgs, Diags2));
+ EXPECT_EQ(Diags2,
+ "test.FalsePositiveGenerator:REACHED_WITH_NO_CONTRADICTION\n"
+ "test.FalsePositiveGenerator:CAN_BE_TRUE\n");
+}
+
} // namespace
} // namespace ento
} // namespace clang
More information about the cfe-commits
mailing list