diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Core/AddressSpace.cpp | 126 | ||||
| -rw-r--r-- | lib/Core/AddressSpace.h | 30 |
2 files changed, 79 insertions, 77 deletions
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp index 32bcdcc5..78dab30a 100644 --- a/lib/Core/AddressSpace.cpp +++ b/lib/Core/AddressSpace.cpp @@ -160,12 +160,43 @@ bool AddressSpace::resolveOne(ExecutionState &state, } } -bool AddressSpace::resolve(ExecutionState &state, - TimingSolver *solver, - ref<Expr> p, - ResolutionList &rl, - unsigned maxResolutions, - double timeout) { +int AddressSpace::checkPointerInObject(ExecutionState &state, + TimingSolver *solver, ref<Expr> p, + const ObjectPair &op, ResolutionList &rl, + unsigned maxResolutions) const { + // XXX in the common case we can save one query if we ask + // mustBeTrue before mayBeTrue for the first result. easy + // to add I just want to have a nice symbolic test case first. + const MemoryObject *mo = op.first; + ref<Expr> inBounds = mo->getBoundsCheckPointer(p); + bool mayBeTrue; + if (!solver->mayBeTrue(state, inBounds, mayBeTrue)) { + return 1; + } + + if (mayBeTrue) { + rl.push_back(op); + + // fast path check + auto size = rl.size(); + if (size == 1) { + bool mustBeTrue; + if (!solver->mustBeTrue(state, inBounds, mustBeTrue)) + return 1; + if (mustBeTrue) + return 0; + } + else + if (size == maxResolutions) + return 1; + } + + return 2; +} + +bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver, + ref<Expr> p, ResolutionList &rl, + unsigned maxResolutions, double timeout) { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(p)) { ObjectPair res; if (resolveOne(CE, res)) @@ -173,112 +204,73 @@ bool AddressSpace::resolve(ExecutionState &state, return false; } else { TimerStatIncrementer timer(stats::resolveTime); - uint64_t timeout_us = (uint64_t) (timeout*1000000.); + uint64_t timeout_us = (uint64_t) (timeout * 1000000.); // XXX in general this isn't exactly what we want... for // a multiple resolution case (or for example, a \in {b,c,0}) // we want to find the first object, find a cex assuming // not the first, find a cex assuming not the second... // etc. - + // XXX how do we smartly amortize the cost of checking to // see if we need to keep searching up/down, in bad cases? // maybe we don't care? - + // XXX we really just need a smart place to start (although // if its a known solution then the code below is guaranteed // to hit the fast path with exactly 2 queries). we could also // just get this by inspection of the expr. - + ref<ConstantExpr> cex; if (!solver->getValue(state, p, cex)) return true; uint64_t example = cex->getZExtValue(); MemoryObject hack(example); - + MemoryMap::iterator oi = objects.upper_bound(&hack); MemoryMap::iterator begin = objects.begin(); MemoryMap::iterator end = objects.end(); - + MemoryMap::iterator start = oi; - - // XXX in the common case we can save one query if we ask - // mustBeTrue before mayBeTrue for the first result. easy - // to add I just want to have a nice symbolic test case first. - // search backwards, start with one minus because this // is the object that p *should* be within, which means we - // get write off the end with 4 queries (XXX can be better, - // no?) - while (oi!=begin) { + // get write off the end with 4 queries + while (oi != begin) { --oi; const MemoryObject *mo = oi->first; if (timeout_us && timeout_us < timer.check()) return true; - // XXX I think there is some query wasteage here? - ref<Expr> inBounds = mo->getBoundsCheckPointer(p); - bool mayBeTrue; - if (!solver->mayBeTrue(state, inBounds, mayBeTrue)) - return true; - if (mayBeTrue) { - rl.push_back(*oi); - - // fast path check - unsigned size = rl.size(); - if (size==1) { - bool mustBeTrue; - if (!solver->mustBeTrue(state, inBounds, mustBeTrue)) - return true; - if (mustBeTrue) - return false; - } else if (size==maxResolutions) { - return true; - } - } - + int incomplete = + checkPointerInObject(state, solver, p, *oi, rl, maxResolutions); + if (incomplete != 2) + return incomplete ? true : false; + bool mustBeTrue; - if (!solver->mustBeTrue(state, - UgeExpr::create(p, mo->getBaseExpr()), + if (!solver->mustBeTrue(state, UgeExpr::create(p, mo->getBaseExpr()), mustBeTrue)) return true; if (mustBeTrue) break; } + // search forwards - for (oi=start; oi!=end; ++oi) { + for (oi = start; oi != end; ++oi) { const MemoryObject *mo = oi->first; if (timeout_us && timeout_us < timer.check()) return true; bool mustBeTrue; - if (!solver->mustBeTrue(state, - UltExpr::create(p, mo->getBaseExpr()), + if (!solver->mustBeTrue(state, UltExpr::create(p, mo->getBaseExpr()), mustBeTrue)) return true; if (mustBeTrue) break; - - // XXX I think there is some query wasteage here? - ref<Expr> inBounds = mo->getBoundsCheckPointer(p); - bool mayBeTrue; - if (!solver->mayBeTrue(state, inBounds, mayBeTrue)) - return true; - if (mayBeTrue) { - rl.push_back(*oi); - - // fast path check - unsigned size = rl.size(); - if (size==1) { - bool mustBeTrue; - if (!solver->mustBeTrue(state, inBounds, mustBeTrue)) - return true; - if (mustBeTrue) - return false; - } else if (size==maxResolutions) { - return true; - } - } + + int incomplete = + checkPointerInObject(state, solver, p, *oi, rl, maxResolutions); + if (incomplete != 2) + return incomplete ? true : false; } } diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h index 10549e7a..fa814950 100644 --- a/lib/Core/AddressSpace.h +++ b/lib/Core/AddressSpace.h @@ -32,15 +32,26 @@ namespace klee { }; typedef ImmutableMap<const MemoryObject*, ObjectHolder, MemoryObjectLT> MemoryMap; - + class AddressSpace { private: /// Epoch counter used to control ownership of objects. mutable unsigned cowKey; /// Unsupported, use copy constructor - AddressSpace &operator=(const AddressSpace&); - + AddressSpace &operator=(const AddressSpace &); + + /// Check if pointer `p` can point to the memory object in the + /// given object pair. If so, add it to the given resolution list. + /// + /// \return 1 iff the resolution is incomplete (`maxResolutions` + /// is non-zero and it was reached, or a query timed out), 0 iff + /// the resolution is complete (`p` can only point to the given + /// memory object), and 2 otherwise. + int checkPointerInObject(ExecutionState &state, TimingSolver *solver, + ref<Expr> p, const ObjectPair &op, + ResolutionList &rl, unsigned maxResolutions) const; + public: /// The MemoryObject -> ObjectState map that constitutes the /// address space. @@ -51,7 +62,6 @@ namespace klee { /// \invariant forall o in objects, o->copyOnWriteOwner <= cowKey MemoryMap objects; - public: AddressSpace() : cowKey(1) {} AddressSpace(const AddressSpace &b) : cowKey(++b.cowKey), objects(b.objects) { } ~AddressSpace() {} @@ -76,15 +86,15 @@ namespace klee { ObjectPair &result, bool &success); - /// Resolve address to a list of ObjectPairs it can point to. If - /// maxResolutions is non-zero then no more than that many pairs - /// will be returned. + /// Resolve pointer `p` to a list of `ObjectPairs` it can point + /// to. If `maxResolutions` is non-zero then no more than that many + /// pairs will be returned. /// - /// \return true iff the resolution is incomplete (maxResolutions - /// is non-zero and the search terminated early, or a query timed out). + /// \return true iff the resolution is incomplete (`maxResolutions` + /// is non-zero and it was reached, or a query timed out). bool resolve(ExecutionState &state, TimingSolver *solver, - ref<Expr> address, + ref<Expr> p, ResolutionList &rl, unsigned maxResolutions=0, double timeout=0.); |