diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/Executor.cpp | 23 | ||||
-rw-r--r-- | lib/Core/Executor.h | 3 | ||||
-rw-r--r-- | lib/Core/Memory.cpp | 29 | ||||
-rw-r--r-- | lib/Core/Memory.h | 25 |
4 files changed, 53 insertions, 27 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 63d21c6e..30c30928 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2627,9 +2627,11 @@ ref<Expr> Executor::replaceReadWithSymbolic(ExecutionState &state, return res; } -ObjectState *Executor::bindObjectInState(ExecutionState &state, const MemoryObject *mo, - bool isLocal) { - ObjectState *os = new ObjectState(mo, mo->size); +ObjectState *Executor::bindObjectInState(ExecutionState &state, + const MemoryObject *mo, + bool isLocal, + const Array *array) { + ObjectState *os = array ? new ObjectState(mo, array) : new ObjectState(mo); state.addressSpace.bindObject(mo, os); // Its possible that multiple bindings of the same mo in the state @@ -2945,15 +2947,14 @@ void Executor::executeMemoryOperation(ExecutionState &state, void Executor::executeMakeSymbolic(ExecutionState &state, const MemoryObject *mo) { - // make a new one and rebind, we use bind here because we want to - // create a flat out new state, not a copy. although I'm not really - // sure it matters. - ObjectState *os = bindObjectInState(state, mo, false); + // Create a new object state for the memory object (instead of a copy). if (!replayOut) { - os->makeSymbolic(); + static unsigned id = 0; + const Array *array = new Array("arr" + llvm::utostr(++id), + mo->size); + ObjectState *os = bindObjectInState(state, mo, false, array); state.addSymbolic(mo, os->updates.root); - const Array *array = os->updates.root; std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = seedMap.find(&state); if (it!=seedMap.end()) { // In seed mode we need to add this as a @@ -2961,8 +2962,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state, for (std::vector<SeedInfo>::iterator siit = it->second.begin(), siie = it->second.end(); siit != siie; ++siit) { SeedInfo &si = *siit; - KTestObject *obj = si.getNextInput(mo, - NamedSeedMatching); + KTestObject *obj = si.getNextInput(mo, NamedSeedMatching); if (!obj) { if (ZeroSeedExtension) { @@ -3002,6 +3002,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state, } } } else { + ObjectState *os = bindObjectInState(state, mo, false); if (replayPosition >= replayOut->numObjects) { terminateStateOnError(state, "replay count mismatch", "user.err"); } else { diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 013d3bb8..4dd89f2a 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -42,6 +42,7 @@ namespace llvm { } namespace klee { + class Array; class Cell; class ExecutionState; class ExternalDispatcher; @@ -198,7 +199,7 @@ private: std::vector< ref<Expr> > &arguments); ObjectState *bindObjectInState(ExecutionState &state, const MemoryObject *mo, - bool isLocal); + bool isLocal, const Array *array = 0); /// Resolve a pointer to the memory objects it could point to the /// start of, forking execution when necessary and generating errors diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index 513c2177..04f68737 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -83,18 +83,37 @@ void MemoryObject::getAllocInfo(std::string &result) const { /***/ -ObjectState::ObjectState(const MemoryObject *mo, unsigned _size) +ObjectState::ObjectState(const MemoryObject *mo) : copyOnWriteOwner(0), refCount(0), object(mo), - concreteStore(new uint8_t[_size]), + concreteStore(new uint8_t[mo->size]), concreteMask(0), flushMask(0), knownSymbolics(0), - size(_size), - // FIXME: Leaked! - updates(new Array("arr" + llvm::utostr(mo->id), _size), 0), + size(mo->size), + updates(0, 0), readOnly(false) { + // FIXME: Leaked. + static unsigned id = 0; + const Array *array = new Array("tmp_arr" + llvm::utostr(++id), + size); + updates = UpdateList(array, 0); +} + + +ObjectState::ObjectState(const MemoryObject *mo, const Array *array) + : copyOnWriteOwner(0), + refCount(0), + object(mo), + concreteStore(new uint8_t[mo->size]), + concreteMask(0), + flushMask(0), + knownSymbolics(0), + size(mo->size), + updates(array, 0), + readOnly(false) { + makeSymbolic(); } ObjectState::ObjectState(const ObjectState &os) diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index 565572be..85f83ee1 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -160,9 +160,15 @@ public: bool readOnly; public: - // initial contents are undefined but concrete, it is the creators - // responsibility to initialize the object contents appropriate - ObjectState(const MemoryObject *mo, unsigned size); + /// Create a new object state for the given memory object with concrete + /// contents. The initial contents are undefined, it is the callers + /// responsibility to initialize the object contents appropriately. + ObjectState(const MemoryObject *mo); + + /// Create a new object state for the given memory object with symbolic + /// contents. + ObjectState(const MemoryObject *mo, const Array *array); + ObjectState(const ObjectState &os); ~ObjectState(); @@ -170,11 +176,6 @@ public: void setReadOnly(bool ro) { readOnly = ro; } - // make all bytes are concrete with undefined values - void makeConcrete(); - - void makeSymbolic(); - // make contents all concrete and zero void initializeToZero(); // make contents all concrete and random @@ -198,6 +199,10 @@ public: void write64(unsigned offset, uint64_t value); private: + void makeConcrete(); + + void makeSymbolic(); + ref<Expr> read1(ref<Expr> offset) const; ref<Expr> read8(ref<Expr> offset) const; ref<Expr> read16(ref<Expr> offset) const; @@ -215,8 +220,8 @@ private: void write64(unsigned offset, ref<Expr> value); void write64(ref<Expr> offset, ref<Expr> value); - - void fastRangeCheckOffset(ref<Expr> offset, unsigned *base_r, unsigned *size_r) const; + void fastRangeCheckOffset(ref<Expr> offset, unsigned *base_r, + unsigned *size_r) const; void flushRangeForRead(unsigned rangeBase, unsigned rangeSize) const; void flushRangeForWrite(unsigned rangeBase, unsigned rangeSize); |