[PATCH] D48565: [analyzer] Replace the vector of ConstraintSets by a single ConstraintSet and a function to merge ConstraintSets

[Phabricator via Phabricator via cfe-commits]

This revision was automatically updated to reflect the committed changes.
Closed by commit rC336002: [analyzer] Replace the vector of ConstraintSets by a 
single ConstraintSet and a… (authored by mramalho, committed by ).
Herald added a subscriber: cfe-commits.

Repository:
  rC Clang

https://reviews.llvm.org/D48565

Files:
  include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
  lib/StaticAnalyzer/Core/BugReporterVisitors.cpp


Index: include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
===================================================================
--- include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
+++ include/clang/StaticAnalyzer/Core/BugReporter/BugReporterVisitors.h
@@ -336,18 +336,20 @@
 class FalsePositiveRefutationBRVisitor final : public BugReporterVisitor {
 private:
   /// Holds the constraints in a given path
-  // TODO: should we use a set?
-  llvm::SmallVector<ConstraintRangeTy, 32> Constraints;
+  ConstraintRangeTy Constraints;
 
 public:
-  FalsePositiveRefutationBRVisitor() = default;
+  FalsePositiveRefutationBRVisitor();
 
   void Profile(llvm::FoldingSetNodeID &ID) const override;
 
   std::shared_ptr<PathDiagnosticPiece> VisitNode(const ExplodedNode *N,
                                                  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,39 +2349,55 @@
   return std::make_shared<PathDiagnosticEventPiece>(L, "Taint originated here");
 }
 
-static bool
-areConstraintsUnfeasible(BugReporterContext &BRC,
-                         const llvm::SmallVector<ConstraintRangeTy, 32> &Cs) {
+static bool areConstraintsUnfeasible(BugReporterContext &BRC,
+                                     const ConstraintRangeTy &Cs) {
   // Create a refutation manager
   std::unique_ptr<ConstraintManager> RefutationMgr = CreateZ3ConstraintManager(
       BRC.getStateManager(), BRC.getStateManager().getOwningEngine());
 
   SMTConstraintManager *SMTRefutationMgr =
       static_cast<SMTConstraintManager *>(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
+  VisitNode(EndPathNode, nullptr, BRC, BR);
+
+  // Create a new refutation manager and check feasibility
+  if (areConstraintsUnfeasible(BRC, Constraints))
+    BR.markInvalid("Infeasible constraints", EndPathNode->getLocationContext());
+}
+
 std::shared_ptr<PathDiagnosticPiece>
 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<ConstraintRange>();
-  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<ConstraintRange>(),
+                    N->getState()->get_context<ConstraintRange>());
 
   return nullptr;
 }

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
http://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits