Added the ability to solve for all factors in a particular query.

This functionality is necessary in order to more effectively handle
calls to IndependentSolver::getInitialValues.  An incoming query will
be broken down into its smaller parts, and each piece will be solved
for. At the end, the pieces will be recombined into a larger solution.
The IndependentElementSet::getAllFactors() method takes a query and
breaks it down into all of it's non-interacting factors.  The
IndependentElementSet::calculateArrays() method calculates which
arrays are involved in a particular factor.

1 files changed, 77 insertions, 0 deletions

diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 59a357b3..c02a3bd6 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -16,11 +16,13 @@
 #include "klee/Internal/Support/Debug.h"
 
 #include "klee/util/ExprUtil.h"
+#include "klee/util/Assignment.h"
 
 #include "llvm/Support/raw_ostream.h"
 #include <map>
 #include <vector>
 #include <ostream>
+#include <list>
 
 using namespace klee;
 using namespace llvm;
@@ -246,6 +248,60 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os,
   return os;
 }
 
+// Breaks down a constraint into all of it's individual pieces, returning a
+// list of IndependentElementSets or the independent factors.
+static
+void getAllIndependentConstraintsSets(const Query& query,
+                                      std::list<IndependentElementSet> * &factors){
+  ConstantExpr *CE = dyn_cast<ConstantExpr>(query.expr);
+  if (CE){
+    assert(CE && CE->isFalse() &&
+           "the expr should always be false and therefore not included in factors");
+  } else {
+    ref<Expr> neg = Expr::createIsZero(query.expr);
+    factors->push_back(IndependentElementSet(neg));
+  }
+
+  for (ConstraintManager::const_iterator it = query.constraints.begin(),
+       ie = query.constraints.end(); it != ie; ++it)
+    // iterate through all the previously separated constraints.  Until we
+    // actually return, factors is treated as a queue of expressions to be
+    // evaluated.  If the queue property isn't maintained, then the exprs
+    // could be returned in an order different from how they came it, negatively
+    // affecting later stages.
+    factors->push_back(IndependentElementSet(*it));
+    bool doneLoop = false;
+    do {
+      doneLoop = true;
+      std::list<IndependentElementSet> * done = new std::list<IndependentElementSet>;
+      while (factors->size() > 0){
+        IndependentElementSet current = factors->front();
+        factors->pop_front();
+        // This list represents the set of factors that are separate from current.
+        // Those that are not inserted into this list (queue) intersect with current.
+	std::list<IndependentElementSet> *keep = new std::list<IndependentElementSet>;
+	while (factors->size() > 0){
+          IndependentElementSet compare = factors->front();
+          factors->pop_front();
+          if (current.intersects(compare)){
+            if (current.add(compare)){
+	      // Means that we have added (z=y)added to (x=y)
+	      // Now need to see if there are any (z=?)'s
+	      doneLoop = false;
+	    }
+	  } else {
+            keep->push_back(compare);
+	  }
+	}
+	done->push_back(current);
+	delete factors;
+	factors = keep;
+      }
+    delete factors;
+    factors = done;
+  } while (!doneLoop);
+}
+
 static 
 IndependentElementSet getIndependentConstraints(const Query& query,
                                                 std::vector< ref<Expr> > &result) {
@@ -295,6 +351,27 @@ IndependentElementSet getIndependentConstraints(const Query& query,
   return eltsClosure;
 }
 
+
+// Extracts which arrays are referenced from a particular independent set.  Examines both
+// the actual known array accesses arr[1] plus the undetermined accesses arr[x].
+static
+void calculateArrayReferences(const IndependentElementSet & ie,
+                              std::vector<const Array *> &returnVector){
+  std::set<const Array*> thisSeen;
+  for(std::map<const Array*, ::DenseSet<unsigned> >::const_iterator it = ie.elements.begin();
+      it != ie.elements.end(); it ++){
+    thisSeen.insert(it->first);
+  }
+  for(std::set<const Array *>::iterator it = ie.wholeObjects.begin();
+      it != ie.wholeObjects.end(); it ++){
+    thisSeen.insert(*it);
+  }
+  for(std::set<const Array *>::iterator it = thisSeen.begin(); it != thisSeen.end();
+      it ++){
+    returnVector.push_back(*it);
+  }
+}
+
 class IndependentSolver : public SolverImpl {
 private:
   Solver *solver;