diff options
| -rw-r--r-- | lib/Solver/IndependentSolver.cpp | 77 |
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; |