diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Core/Executor.cpp | 45 | ||||
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.cpp | 27 | ||||
| -rw-r--r-- | lib/Core/SpecialFunctionHandler.h | 1 | ||||
| -rw-r--r-- | lib/Solver/CexCachingSolver.cpp | 15 | ||||
| -rw-r--r-- | lib/Solver/IndependentSolver.cpp | 211 |
5 files changed, 266 insertions, 33 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 45876659..49e526f5 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -140,10 +140,6 @@ namespace { cl::desc("Dump test cases for all active states on exit (default=on)")); cl::opt<bool> - NoPreferCex("no-prefer-cex", - cl::init(false)); - - cl::opt<bool> RandomizeFork("randomize-fork", cl::init(false), cl::desc("Randomly swap the true and false states on a fork (default=off)")); @@ -3482,20 +3478,33 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, solver->setTimeout(coreSolverTimeout); ExecutionState tmp(state); - if (!NoPreferCex) { - for (unsigned i = 0; i != state.symbolics.size(); ++i) { - const MemoryObject *mo = state.symbolics[i].first; - std::vector< ref<Expr> >::const_iterator pi = - mo->cexPreferences.begin(), pie = mo->cexPreferences.end(); - for (; pi != pie; ++pi) { - bool mustBeTrue; - bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi), - mustBeTrue); - if (!success) break; - if (!mustBeTrue) tmp.addConstraint(*pi); - } - if (pi!=pie) break; - } + + // Go through each byte in every test case and attempt to restrict + // it to the constraints contained in cexPreferences. (Note: + // usually this means trying to make it an ASCII character (0-127) + // and therefore human readable. It is also possible to customize + // the preferred constraints. See test/Features/PreferCex.c for + // an example) While this process can be very expensive, it can + // also make understanding individual test cases much easier. + for (unsigned i = 0; i != state.symbolics.size(); ++i) { + const MemoryObject *mo = state.symbolics[i].first; + std::vector< ref<Expr> >::const_iterator pi = + mo->cexPreferences.begin(), pie = mo->cexPreferences.end(); + for (; pi != pie; ++pi) { + bool mustBeTrue; + // Attempt to bound byte to constraints held in cexPreferences + bool success = solver->mustBeTrue(tmp, Expr::createIsZero(*pi), + mustBeTrue); + // If it isn't possible to constrain this particular byte in the desired + // way (normally this would mean that the byte can't be constrained to + // be between 0 and 127 without making the entire constraint list UNSAT) + // then just continue on to the next byte. + if (!success) break; + // If the particular constraint operated on in this iteration through + // the loop isn't implied then add it to the list of constraints. + if (!mustBeTrue) tmp.addConstraint(*pi); + } + if (pi!=pie) break; } std::vector< std::vector<unsigned char> > values; diff --git a/lib/Core/SpecialFunctionHandler.cpp b/lib/Core/SpecialFunctionHandler.cpp index f06ae4f5..52abff5f 100644 --- a/lib/Core/SpecialFunctionHandler.cpp +++ b/lib/Core/SpecialFunctionHandler.cpp @@ -22,6 +22,8 @@ #include "Executor.h" #include "MemoryManager.h" +#include "klee/CommandLine.h" + #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3) #include "llvm/IR/Module.h" #else @@ -34,6 +36,15 @@ using namespace llvm; using namespace klee; +namespace { + cl::opt<bool> + ReadablePosix("readable-posix-inputs", + cl::init(false), + cl::desc("Prefer creation of POSIX inputs (command-line arguments, files, etc.) with human readable bytes. " + "Note: option is expensive when creating lots of tests (default=false)")); +} + + /// \todo Almost all of the demands in this file should be replaced /// with terminateState calls. @@ -81,6 +92,7 @@ static SpecialFunctionHandler::HandlerInfo handlerInfo[] = { add("klee_mark_global", handleMarkGlobal, false), add("klee_merge", handleMerge, false), add("klee_prefer_cex", handlePreferCex, false), + add("klee_posix_prefer_cex", handlePosixPreferCex, false), add("klee_print_expr", handlePrintExpr, false), add("klee_print_range", handlePrintRange, false), add("klee_set_forking", handleSetForking, false), @@ -222,7 +234,7 @@ SpecialFunctionHandler::readStringAtAddress(ExecutionState &state, ref<ConstantExpr> address = cast<ConstantExpr>(addressExpr); if (!state.addressSpace.resolveOne(address, op)) assert(0 && "XXX out of bounds / multiple resolution unhandled"); - bool res; + bool res __attribute__ ((unused)); assert(executor.solver->mustBeTrue(state, EqExpr::create(address, op.first->getBaseExpr()), @@ -376,7 +388,7 @@ void SpecialFunctionHandler::handleAssume(ExecutionState &state, e = NeExpr::create(e, ConstantExpr::create(0, e->getWidth())); bool res; - bool success = executor.solver->mustBeFalse(state, e, res); + bool success __attribute__ ((unused)) = executor.solver->mustBeFalse(state, e, res); assert(success && "FIXME: Unhandled solver failure"); if (res) { executor.terminateStateOnError(state, @@ -416,6 +428,13 @@ void SpecialFunctionHandler::handlePreferCex(ExecutionState &state, rl[0].first.first->cexPreferences.push_back(cond); } +void SpecialFunctionHandler::handlePosixPreferCex(ExecutionState &state, + KInstruction *target, + std::vector<ref<Expr> > &arguments) { + if (ReadablePosix) + return handlePreferCex(state, target, arguments); +} + void SpecialFunctionHandler::handlePrintExpr(ExecutionState &state, KInstruction *target, std::vector<ref<Expr> > &arguments) { @@ -480,7 +499,7 @@ void SpecialFunctionHandler::handlePrintRange(ExecutionState &state, if (!isa<ConstantExpr>(arguments[1])) { // FIXME: Pull into a unique value method? ref<ConstantExpr> value; - bool success = executor.solver->getValue(state, arguments[1], value); + bool success __attribute__ ((unused)) = executor.solver->getValue(state, arguments[1], value); assert(success && "FIXME: Unhandled solver failure"); bool res; success = executor.solver->mustBeTrue(state, @@ -679,7 +698,7 @@ void SpecialFunctionHandler::handleMakeSymbolic(ExecutionState &state, // FIXME: Type coercion should be done consistently somewhere. bool res; - bool success = + bool success __attribute__ ((unused)) = executor.solver->mustBeTrue(*s, EqExpr::create(ZExtExpr::create(arguments[1], Context::get().getPointerWidth()), diff --git a/lib/Core/SpecialFunctionHandler.h b/lib/Core/SpecialFunctionHandler.h index d52b8fc5..2dfdde43 100644 --- a/lib/Core/SpecialFunctionHandler.h +++ b/lib/Core/SpecialFunctionHandler.h @@ -120,6 +120,7 @@ namespace klee { HANDLER(handleNew); HANDLER(handleNewArray); HANDLER(handlePreferCex); + HANDLER(handlePosixPreferCex); HANDLER(handlePrintExpr); HANDLER(handlePrintRange); HANDLER(handleRange); diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index df7fffc5..d51c1695 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -35,6 +35,11 @@ namespace { cl::init(false)); cl::opt<bool> + CexCacheSuperSet("cex-cache-superset", + cl::desc("try substituting SAT super-set counterexample before asking the SMT solver (default=false)"), + cl::init(false)); + + cl::opt<bool> CexCacheExperimental("cex-cache-exp", cl::init(false)); } @@ -124,8 +129,10 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) { if (CexCacheTryAll) { // Look for a satisfying assignment for a superset, which is trivially an // assignment for any subset. - Assignment **lookup = cache.findSuperset(key, NonNullAssignment()); - + Assignment **lookup = 0; + if (CexCacheSuperSet) + lookup = cache.findSuperset(key, NonNullAssignment()); + // Otherwise, look for a subset which is unsatisfiable, see below. if (!lookup) lookup = cache.findSubset(key, NullAssignment()); @@ -151,7 +158,9 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) { // Look for a satisfying assignment for a superset, which is trivially an // assignment for any subset. - Assignment **lookup = cache.findSuperset(key, NonNullAssignment()); + Assignment **lookup = 0; + if (CexCacheSuperSet) + lookup = cache.findSuperset(key, NonNullAssignment()); // Otherwise, look for a subset which is unsatisfiable -- if the subset is // unsatisfiable then no additional constraints can produce a valid 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(); } |