steakhal updated this revision to Diff 259532.
steakhal added a comment.
- keep the visitor
- fix the bug
- add test demonstrating the bug and the fix
Repository:
rG LLVM Github Monorepo
CHANGES SINCE LAST ACTION
https://reviews.llvm.org/D78457/new/
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
clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
Index: clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
===================================================================
--- clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
+++ clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp
@@ -166,6 +166,53 @@
"test.FalsePositiveGenerator:ZERO_STATE_SHOULD_NOT_EXIST\n");
}
+TEST(FalsePositiveRefutationBRVisitor,
+ UnSatAtErrorNodeDueToRefinedConstraintNoReport) {
+ SKIP_WITHOUT_Z3;
+ std::string Diags;
+ constexpr auto Code = R"(
+ void reportIfCanBeZero(int);
+ 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 '($x+$n)' with the constraint [1, MAX] in the
+ // true branch.
+ if (y > 0) {
+ // Since the x: [0,2] and n: [1,2] the ($x+$n) is indeed greater than
+ // zero. If we emit a warning here, the constraints on the bugpath is
+ // SAT. Therefore that bugreport is NOT invalidated.
+ reachedWithNoContradiction(); // ($x+$n) can be grater than zero. OK
+
+ // If we ask the analyzer whether the 'y-5' can be zero. It won't know,
+ // therefore the state will be created where the 'y-5' expression is 0.
+ // This assumption is false!
+ // 'y' can not be 5 if the maximal value of both x and y is 2.
+ // This bugreport must be caught by the visitor, since the constraints
+ // of the bugpath are UnSAT.
+ reportIfCanBeZero(y - 5);
+ }
+ }
+ })";
+
+ // Only the first diagnostic is visible.
+ EXPECT_TRUE(runFalsePositiveGeneratorOnCode(Code, Diags, CrossCheckArgs));
+ EXPECT_EQ(Diags,
+ "test.FalsePositiveGenerator:REACHED_WITH_NO_CONTRADICTION\n");
+
+ // Without enabling the crosscheck-with-z3 the BugPath is not invalidated.
+ // Both diagnostics are visible.
+ std::string Diags2;
+ EXPECT_TRUE(runFalsePositiveGeneratorOnCode(Code, Diags2));
+ EXPECT_EQ(Diags2,
+ "test.FalsePositiveGenerator:REACHED_WITH_NO_CONTRADICTION\n"
+ "test.FalsePositiveGenerator:ZERO_STATE_SHOULD_NOT_EXIST\n");
+}
+
} // namespace
} // namespace ento
} // namespace clang
Index: clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
===================================================================
--- clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
+++ clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
@@ -2820,7 +2820,7 @@
BugReporterContext &BRC, const ExplodedNode *EndPathNode,
PathSensitiveBugReport &BR) {
// Collect new constraints
- VisitNode(EndPathNode, BRC, BR);
+ addConstraints(EndPathNode, /*OnlyForNewSymbols=*/false);
// Create a refutation manager
llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();
@@ -2831,30 +2831,30 @@
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 OnlyForNewSymbols) {
// Collect new constraints
const ConstraintRangeTy &NewCs = N->getState()->get<ConstraintRange>();
ConstraintRangeTy::Factory &CF =
@@ -2864,10 +2864,19 @@
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 (!OnlyForNewSymbols) {
+ // 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, /*OnlyForNewSymbols=*/true);
return nullptr;
}
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) {
@@ -2782,7 +2812,7 @@
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);
}
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
@@ -386,6 +386,8 @@
void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,
PathSensitiveBugReport &BR) override;
+
+ void addConstraints(const ExplodedNode *N, bool OnlyForNewSymbols);
};
_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
