From b70e2d2e772748ac4e217881742ad55fcfb77096 Mon Sep 17 00:00:00 2001 From: Eric Rizzi Date: Mon, 16 Feb 2015 11:38:33 -0500 Subject: Altered DenseSet and IndependentElementSet to record ref involved This is important for future changes to IndependentSolver:: getInitialValues() so that an incoming constraint can be broken down into its smallest possible parts. Each of these individual parts may then be solved for and then the solutions to each piece combined to create a final answer. Finally, several fields which had previously been private are now public to facilitate the smaller solutions being combined into a larger solution. --- lib/Solver/IndependentSolver.cpp | 33 +++++++++++++++++++++++++++++---- 1 file 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 > elements_ty; - elements_ty elements; - std::set wholeObjects; + elements_ty elements; // Represents individual elements of array accesses (arr[1]) + std::set wholeObjects; // Represents symbolically accessed arrays (arr[x]) + std::vector > 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 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> which tracks which parts of the + // array are being accessed. std::vector< ref > 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(re->index)) { + // if index constant, then add to set of constraints operating + // on that array (actually, don't add constraint, just set index) ::DenseSet &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::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 = b.exprs[i]; + exprs.push_back(expr); + } + bool modified = false; for (std::set::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); } -- cgit 1.4.1 From d9bcbba2c94086039c11c86200670639ee2ec19f Mon Sep 17 00:00:00 2001 From: Eric Rizzi Date: Mon, 16 Feb 2015 11:42:08 -0500 Subject: 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. --- lib/Solver/IndependentSolver.cpp | 77 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 77 insertions(+) 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 #include #include +#include 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 * &factors){ + ConstantExpr *CE = dyn_cast(query.expr); + if (CE){ + assert(CE && CE->isFalse() && + "the expr should always be false and therefore not included in factors"); + } else { + ref 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 * done = new std::list; + 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 *keep = new std::list; + 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 > &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 &returnVector){ + std::set thisSeen; + for(std::map >::const_iterator it = ie.elements.begin(); + it != ie.elements.end(); it ++){ + thisSeen.insert(it->first); + } + for(std::set::iterator it = ie.wholeObjects.begin(); + it != ie.wholeObjects.end(); it ++){ + thisSeen.insert(*it); + } + for(std::set::iterator it = thisSeen.begin(); it != thisSeen.end(); + it ++){ + returnVector.push_back(*it); + } +} + class IndependentSolver : public SolverImpl { private: Solver *solver; -- cgit 1.4.1 From 76b6ae9a16dcb643456a98a845dc8d44df3aa049 Mon Sep 17 00:00:00 2001 From: Eric Rizzi Date: Mon, 16 Feb 2015 11:46:01 -0500 Subject: Commit of improved IndependentSolver::getIniitalValues(). Previous implementation simply passed the entire constraint forward without any factoring of the constraint at all. This is a problem since it is highly likely that there are cached solutions to pieces of the constraint. The new implementation breaks the entire constraint down into its requisite factors and passes each piece forward, one by one, down the solver chain. After an answer is returned, it is integrated into a larger solution. Since, by definition, no factor can affect another, we can safely create a solution to the larger constraint from the answers of its smaller pieces. The reconstruction of the solution is done by analyzing which parts of an array a factor touches. If the factor is the only one to reference a particular array, then all of the values calculated in the solution for that array are included in the final answer. If the factor references a particular element of the array (for example, arr[1]), then only the value in index 1 of array arr will be included in the solution. --- include/klee/util/Assignment.h | 4 +- lib/Solver/IndependentSolver.cpp | 79 ++++++++++++++++++++++++++++++++++++++-- 2 files changed, 77 insertions(+), 6 deletions(-) diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h index 63df4b65..6fee5cb1 100644 --- a/include/klee/util/Assignment.h +++ b/include/klee/util/Assignment.h @@ -29,13 +29,13 @@ namespace klee { public: Assignment(bool _allowFreeValues=false) : allowFreeValues(_allowFreeValues) {} - Assignment(std::vector &objects, + Assignment(const std::vector &objects, std::vector< std::vector > &values, bool _allowFreeValues=false) : allowFreeValues(_allowFreeValues){ std::vector< std::vector >::iterator valIt = values.begin(); - for (std::vector::iterator it = objects.begin(), + for (std::vector::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { const Array *os = *it; std::vector &arr = *valIt; diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index c02a3bd6..4d628a15 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -64,6 +64,14 @@ public: return false; } + std::set::iterator begin(){ + return s.begin(); + } + + std::set::iterator end(){ + return s.end(); + } + void print(llvm::raw_ostream &os) const { bool first = true; os << "{"; @@ -387,10 +395,7 @@ public: bool computeInitialValues(const Query& query, const std::vector &objects, std::vector< std::vector > &values, - bool &hasSolution) { - return solver->impl->computeInitialValues(query, objects, values, - hasSolution); - } + bool &hasSolution); SolverRunStatus getOperationStatusCode(); char *getConstraintLog(const Query&); void setCoreSolverTimeout(double timeout); @@ -423,6 +428,72 @@ bool IndependentSolver::computeValue(const Query& query, ref &result) { return solver->impl->computeValue(Query(tmp, query.expr), result); } +bool IndependentSolver::computeInitialValues(const Query& query, + const std::vector &objects, + std::vector< std::vector > &values, + bool &hasSolution){ + std::list * factors = new std::list; + getAllIndependentConstraintsSets(query, factors); + //Used to rearrange all of the answers into the correct order + std::map > retMap; + for (std::list::iterator it = factors->begin(); + it != factors->end(); ++it) { + std::vector 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 > 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 * tempPtr = &retMap[arraysInFactor[i]]; + assert(tempPtr->size() == tempValues[i].size() && + "we're talking about the same array here"); + ::DenseSet * ds = &(it->elements[arraysInFactor[i]]); + for (std::set::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_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 ret(arr->size); + values.push_back(ret); + } else { + values.push_back(retMap[arr]); + } + } + delete factors; + return true; +} + SolverImpl::SolverRunStatus IndependentSolver::getOperationStatusCode() { return solver->impl->getOperationStatusCode(); } -- cgit 1.4.1 From be37ac9605d380b7f36717338c2c520f375798c8 Mon Sep 17 00:00:00 2001 From: Eric Rizzi Date: Mon, 16 Feb 2015 12:17:00 -0500 Subject: Added the function IndependentSolver::createdPointEvaluatesToTrue This function should be used solely in assertion statements and is intended as a sanity check to make sure that the solution constructed by IndependentSolver::getInitialValues() produces and answer that in fact satisfies the the query. --- lib/Solver/IndependentSolver.cpp | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 4d628a15..cfe1bb16 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -428,6 +428,27 @@ bool IndependentSolver::computeValue(const Query& query, ref &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 &objects, + std::vector< std::vector > &values){ + Assignment assign = Assignment(objects, values); + for(ConstraintManager::constraint_iterator it = query.constraints.begin(); + it != query.constraints.end(); ++it){ + ref ret = assign.evaluate(*it); + if(! isa(ret) || ! cast(ret)->isTrue()){ + return false; + } + } + ref neg = Expr::createIsZero(query.expr); + ref q = assign.evaluate(neg); + + assert(isa(q) && "assignment evaluation did not result in constant"); + return cast(q)->isTrue(); +} + bool IndependentSolver::computeInitialValues(const Query& query, const std::vector &objects, std::vector< std::vector > &values, @@ -490,6 +511,7 @@ bool IndependentSolver::computeInitialValues(const Query& query, values.push_back(retMap[arr]); } } + assert(assertCreatedPointEvaluatesToTrue(query, objects, values) && "should satisfy the equation"); delete factors; return true; } -- cgit 1.4.1