Index: include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h =================================================================== --- include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h +++ include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h @@ -336,11 +336,10 @@ class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor { private: /// Holds the constraints in a given path - // TODO: should we use a set? - llvm::SmallVector Constraints; + ConstraintRangeTy Constraints; public: - FalsePositiveRefutationBRVisitor() = default; + FalsePositiveRefutationBRVisitor(); void Profile(llvm::FoldingSetNodeID &ID) const override; @@ -348,6 +347,9 @@ const ExplodedNode *PrevN, BugReporterContext &BRC, BugReport &BR) override; + + void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode, + BugReport &BR) override; }; namespace bugreporter { Index: lib/StaticAnalyzer/Core/BugReporterVisitors.cpp =================================================================== --- lib/StaticAnalyzer/Core/BugReporterVisitors.cpp +++ lib/StaticAnalyzer/Core/BugReporterVisitors.cpp @@ -2349,9 +2349,8 @@ return std::make_shared(L, "Taint originated here"); } -static bool -areConstraintsUnfeasible(BugReporterContext &BRC, - const llvm::SmallVector &Cs) { +static bool areConstraintsUnfeasible(BugReporterContext &BRC, + const ConstraintRangeTy &Cs) { // Create a refutation manager std::unique_ptr RefutationMgr = CreateZ3ConstraintManager( BRC.getStateManager(), BRC.getStateManager().getOwningEngine()); @@ -2359,29 +2358,48 @@ SMTConstraintManager *SMTRefutationMgr = static_cast(RefutationMgr.get()); - // Add constraints to the solver - for (const auto &C : Cs) - SMTRefutationMgr->addRangeConstraints(C); + SMTRefutationMgr->addRangeConstraints(Cs); // And check for satisfiability return SMTRefutationMgr->isModelFeasible().isConstrainedFalse(); } +static void addNewConstraints(ConstraintRangeTy &Cs, + const ConstraintRangeTy &NewCs, + ConstraintRangeTy::Factory &CF) { + // Add constraints if we don't have them yet + for (auto const &C : NewCs) { + const SymbolRef &Sym = C.first; + if (!Cs.contains(Sym)) { + Cs = CF.add(Cs, Sym, C.second); + } + } +} + +FalsePositiveRefutationBRVisitor::FalsePositiveRefutationBRVisitor() + : Constraints(ConstraintRangeTy::Factory().getEmptyMap()) {} + +void FalsePositiveRefutationBRVisitor::finalizeVisitor( + BugReporterContext &BRC, const ExplodedNode *EndPathNode, BugReport &BR) { + // Collect new constraints + addNewConstraints(Constraints, + EndPathNode->getState()->get(), + EndPathNode->getState()->get_context()); + + // Create a new refutation manager and check feasibility + if (areConstraintsUnfeasible(BRC, Constraints)) { + BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext()); + } +} + std::shared_ptr FalsePositiveRefutationBRVisitor::VisitNode(const ExplodedNode *N, const ExplodedNode *PrevN, BugReporterContext &BRC, BugReport &BR) { - // Collect the constraint for the current state - const ConstraintRangeTy &CR = N->getState()->get(); - Constraints.push_back(CR); - - // If there are no predecessor, we reached the root node. In this point, - // a new refutation manager will be created and the path will be checked - // for reachability - if (PrevN->pred_size() == 0 && areConstraintsUnfeasible(BRC, Constraints)) { - BR.markInvalid("Infeasible constraints", N->getLocationContext()); - } + // Collect new constraints + addNewConstraints(Constraints, N->getState()->get(), + N->getState()->get_context()); return nullptr; }