diff options
Diffstat (limited to 'lib/Solver/IndependentSolver.cpp')
| -rw-r--r-- | lib/Solver/IndependentSolver.cpp | 211 |
1 files changed, 203 insertions, 8 deletions
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index dcaecb05..cfe1bb16 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; @@ -62,6 +64,14 @@ public: return false; } + std::set<unsigned>::iterator begin(){ + return s.begin(); + } + + std::set<unsigned>::iterator end(){ + return s.end(); + } + void print(llvm::raw_ostream &os) const { bool first = true; os << "{"; @@ -86,13 +96,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 +126,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 +141,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 +184,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 +195,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 +210,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 +240,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; } @@ -223,6 +256,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) { @@ -244,6 +331,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); } @@ -270,6 +359,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; @@ -285,10 +395,7 @@ public: bool computeInitialValues(const Query& query, const std::vector<const Array*> &objects, std::vector< std::vector<unsigned char> > &values, - bool &hasSolution) { - return solver->impl->computeInitialValues(query, objects, values, - hasSolution); - } + bool &hasSolution); SolverRunStatus getOperationStatusCode(); char *getConstraintLog(const Query&); void setCoreSolverTimeout(double timeout); @@ -321,6 +428,94 @@ bool IndependentSolver::computeValue(const Query& query, ref<Expr> &result) { return solver->impl->computeValue(Query(tmp, query.expr), result); } + +// Helper function used only for assertions to make sure point created +// during computeInitialValues is in fact correct. +bool assertCreatedPointEvaluatesToTrue(const Query &query, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values){ + Assignment assign = Assignment(objects, values); + for(ConstraintManager::constraint_iterator it = query.constraints.begin(); + it != query.constraints.end(); ++it){ + ref<Expr> ret = assign.evaluate(*it); + if(! isa<ConstantExpr>(ret) || ! cast<ConstantExpr>(ret)->isTrue()){ + return false; + } + } + ref<Expr> neg = Expr::createIsZero(query.expr); + ref<Expr> q = assign.evaluate(neg); + + assert(isa<ConstantExpr>(q) && "assignment evaluation did not result in constant"); + return cast<ConstantExpr>(q)->isTrue(); +} + +bool IndependentSolver::computeInitialValues(const Query& query, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution){ + std::list<IndependentElementSet> * factors = new std::list<IndependentElementSet>; + getAllIndependentConstraintsSets(query, factors); + //Used to rearrange all of the answers into the correct order + std::map<const Array*, std::vector<unsigned char> > retMap; + for (std::list<IndependentElementSet>::iterator it = factors->begin(); + it != factors->end(); ++it) { + std::vector<const Array*> arraysInFactor; + calculateArrayReferences(*it, arraysInFactor); + // Going to use this as the "fresh" expression for the Query() invocation below + assert(it->exprs.size() >= 1 && "No null/empty factors"); + if (arraysInFactor.size() == 0){ + continue; + } + ConstraintManager tmp(it->exprs); + std::vector<std::vector<unsigned char> > tempValues; + if (!solver->impl->computeInitialValues(Query(tmp, ConstantExpr::alloc(0, Expr::Bool)), + arraysInFactor, tempValues, hasSolution)){ + values.clear(); + return false; + } else if (!hasSolution){ + values.clear(); + return true; + } else { + assert(tempValues.size() == arraysInFactor.size() && + "Should be equal number arrays and answers"); + for (unsigned i = 0; i < tempValues.size(); i++){ + if (retMap.count(arraysInFactor[i])){ + // We already have an array with some partially correct answers, + // so we need to place the answers to the new query into the right + // spot while avoiding the undetermined values also in the array + std::vector<unsigned char> * tempPtr = &retMap[arraysInFactor[i]]; + assert(tempPtr->size() == tempValues[i].size() && + "we're talking about the same array here"); + ::DenseSet<unsigned> * ds = &(it->elements[arraysInFactor[i]]); + for (std::set<unsigned>::iterator it2 = ds->begin(); it2 != ds->end(); it2++){ + unsigned index = * it2; + (* tempPtr)[index] = tempValues[i][index]; + } + } else { + // Dump all the new values into the array + retMap[arraysInFactor[i]] = tempValues[i]; + } + } + } + } + for (std::vector<const Array *>::const_iterator it = objects.begin(); + it != objects.end(); it++){ + const Array * arr = * it; + if (!retMap.count(arr)){ + // this means we have an array that is somehow related to the + // constraint, but whose values aren't actually required to + // satisfy the query. + std::vector<unsigned char> ret(arr->size); + values.push_back(ret); + } else { + values.push_back(retMap[arr]); + } + } + assert(assertCreatedPointEvaluatesToTrue(query, objects, values) && "should satisfy the equation"); + delete factors; + return true; +} + SolverImpl::SolverRunStatus IndependentSolver::getOperationStatusCode() { return solver->impl->getOperationStatusCode(); } |