diff options
| -rw-r--r-- | lib/Solver/IndependentSolver.cpp | 33 |
1 files changed, 29 insertions, 4 deletions
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index dcaecb05..59a357b3 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -86,13 +86,23 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, } class IndependentElementSet { +public: typedef std::map<const Array*, ::DenseSet<unsigned> > elements_ty; - elements_ty elements; - std::set<const Array*> wholeObjects; + elements_ty elements; // Represents individual elements of array accesses (arr[1]) + std::set<const Array*> wholeObjects; // Represents symbolically accessed arrays (arr[x]) + std::vector<ref<Expr> > exprs; // All expressions that are associated with this factor + // Although order doesn't matter, we use a vector to match + // the ConstraintManager constructor that will eventually + // be invoked. -public: IndependentElementSet() {} IndependentElementSet(ref<Expr> e) { + exprs.push_back(e); + // Track all reads in the program. Determines whether reads are + // concrete or symbolic. If they are symbolic, "collapses" array + // by adding it to wholeObjects. Otherwise, creates a mapping of + // the form Map<array, set<index>> which tracks which parts of the + // array are being accessed. std::vector< ref<ReadExpr> > reads; findReads(e, /* visitUpdates= */ true, reads); for (unsigned i = 0; i != reads.size(); ++i) { @@ -106,6 +116,8 @@ public: if (!wholeObjects.count(array)) { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(re->index)) { + // if index constant, then add to set of constraints operating + // on that array (actually, don't add constraint, just set index) ::DenseSet<unsigned> &dis = elements[array]; dis.add((unsigned) CE->getZExtValue(32)); } else { @@ -119,11 +131,13 @@ public: } IndependentElementSet(const IndependentElementSet &ies) : elements(ies.elements), - wholeObjects(ies.wholeObjects) {} + wholeObjects(ies.wholeObjects), + exprs(ies.exprs) {} IndependentElementSet &operator=(const IndependentElementSet &ies) { elements = ies.elements; wholeObjects = ies.wholeObjects; + exprs = ies.exprs; return *this; } @@ -160,6 +174,7 @@ public: // more efficient when this is the smaller set bool intersects(const IndependentElementSet &b) { + // If there are any symbolic arrays in our query that b accesses for (std::set<const Array*>::iterator it = wholeObjects.begin(), ie = wholeObjects.end(); it != ie; ++it) { const Array *array = *it; @@ -170,9 +185,11 @@ public: for (elements_ty::iterator it = elements.begin(), ie = elements.end(); it != ie; ++it) { const Array *array = it->first; + // if the array we access is symbolic in b if (b.wholeObjects.count(array)) return true; elements_ty::const_iterator it2 = b.elements.find(array); + // if any of the elements we access are also accessed by b if (it2 != b.elements.end()) { if (it->second.intersects(it2->second)) return true; @@ -183,6 +200,11 @@ public: // returns true iff set is changed by addition bool add(const IndependentElementSet &b) { + for(unsigned i = 0; i < b.exprs.size(); i ++){ + ref<Expr> expr = b.exprs[i]; + exprs.push_back(expr); + } + bool modified = false; for (std::set<const Array*>::const_iterator it = b.wholeObjects.begin(), ie = b.wholeObjects.end(); it != ie; ++it) { @@ -208,6 +230,7 @@ public: modified = true; elements.insert(*it); } else { + // Now need to see if there are any (z=?)'s if (it2->second.add(it->second)) modified = true; } @@ -244,6 +267,8 @@ IndependentElementSet getIndependentConstraints(const Query& query, if (eltsClosure.add(it->second)) done = false; result.push_back(it->first); + // Means that we have added (z=y)added to (x=y) + // Now need to see if there are any (z=?)'s } else { newWorklist.push_back(*it); } |