[analyzer] Replace the vector of ConstraintSets by a single ConstraintSet and a funct...
authorMikhail R. Gadelha <mikhail.ramalho@gmail.com>
Fri, 29 Jun 2018 18:11:43 +0000 (18:11 +0000)
committerMikhail R. Gadelha <mikhail.ramalho@gmail.com>
Fri, 29 Jun 2018 18:11:43 +0000 (18:11 +0000)
Now, instead of adding the constraints when they are removed, this patch adds them when they first appear and, since we walk the bug report backward, it should be the last set of ranges generated by the CSA for a given symbol.

These are the number before and after the patch:
```
Project    |  current |   patch  |
tmux       |  283.222 |  123.052 |
redis      |  614.858 |  400.347 |
openssl    |  308.292 |  307.149 |
twin       |  274.478 |  245.411 |
git        |  547.687 |  477.335 |
postgresql | 2927.495 | 2002.526 |
sqlite3    | 3264.305 | 1028.416 |
```

Major speedups in tmux and sqlite (less than half of the time), redis and postgresql were about 25% faster while the rest are basically the same.

Reviewers: NoQ, george.karpenkov

Reviewed By: george.karpenkov

Subscribers: rnkovacs, xazax.hun, szepet, a.sidorin

Differential Revision: https://reviews.llvm.org/D48565

llvm-svn: 336002

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

index 031a76c..92118b0 100644 (file)
@@ -336,11 +336,10 @@ public:
 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;
 
@@ -348,6 +347,9 @@ public:
                                                  const ExplodedNode *PrevN,
                                                  BugReporterContext &BRC,
                                                  BugReport &BR) override;
+
+  void finalizeVisitor(BugReporterContext &BRC, const ExplodedNode *EndPathNode,
+                       BugReport &BR) override;
 };
 
 namespace bugreporter {
index 468f218..025c289 100644 (file)
@@ -2349,9 +2349,8 @@ TaintBugVisitor::VisitNode(const ExplodedNode *N, const ExplodedNode *PrevN,
   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());
@@ -2360,28 +2359,45 @@ areConstraintsUnfeasible(BugReporterContext &BRC,
       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;
 }