diff --git a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h b/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h --- a/clang/include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h +++ b/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); }; diff --git a/clang/lib/StaticAnalyzer/Core/BugReporter.cpp b/clang/lib/StaticAnalyzer/Core/BugReporter.cpp --- 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" @@ -2747,6 +2748,35 @@ return Notes; } +Optional hasContradictionUsingZ3(BugReporterContext &BRC, + const ExplodedNode *EndPathNode) { + // Create a refutation manager + llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver(); + ASTContext &Ctx = BRC.getASTContext(); + ConstraintRangeTy Constraints = + EndPathNode->getState()->get(); + + // 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::findValidReport( ArrayRef &bugReports, PathSensitiveBugReporter &Reporter) { @@ -2782,7 +2812,7 @@ R->clearVisitors(); R->addVisitor(std::make_unique()); - // 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 --- a/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp +++ b/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 isSat = RefutationSolver->check(); - if (!isSat.hasValue()) + Optional 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(); 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; } diff --git a/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp b/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp --- a/clang/unittests/StaticAnalyzer/FalsePositiveRefutationBRVisitorTest.cpp +++ b/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