From 6517b3a69deac9faacb5139efa44511e5d2a197f Mon Sep 17 00:00:00 2001 From: Daniel Dunbar Date: Wed, 10 Jun 2009 06:03:26 +0000 Subject: Use Arrays instead of MemoryObject where possible. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@73160 91177308-0d34-0410-b5e6-96231b3b80d8 --- lib/Core/Executor.cpp | 19 +++++++++---------- 1 file changed, 9 insertions(+), 10 deletions(-) (limited to 'lib/Core/Executor.cpp') diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index e47dcfc0..4c5f9511 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -50,6 +50,7 @@ #include "llvm/Instructions.h" #include "llvm/IntrinsicInst.h" #include "llvm/Module.h" +#include "llvm/ADT/StringExtras.h" #include "llvm/Support/CallSite.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/GetElementPtrTypeIterator.h" @@ -2606,11 +2607,10 @@ ref Executor::replaceReadWithSymbolic(ExecutionState &state, // create a new fresh location, assert it is equal to concrete value in e // and return it. - const MemoryObject *mo = - memory->allocate(Expr::getMinBytesForWidth(e->getWidth()), false, false, - state.prevPC->inst); - assert(mo && "out of memory"); - ref res = Expr::createTempRead(mo->array, e->getWidth()); + static unsigned id; + const Array *array = new Array("rrws_arr" + llvm::utostr(++id), + Expr::getMinBytesForWidth(e->getWidth())); + ref res = Expr::createTempRead(array, e->getWidth()); ref eq = NotOptimizedExpr::create(EqExpr::create(e, res)); llvm::cerr << "Making symbolic: " << eq << "\n"; state.addConstraint(eq); @@ -2943,6 +2943,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state, os->makeSymbolic(); state.addSymbolic(mo); + const Array *array = os->updates.root; std::map< ExecutionState*, std::vector >::iterator it = seedMap.find(&state); if (it!=seedMap.end()) { // In seed mode we need to add this as a @@ -2955,8 +2956,7 @@ void Executor::executeMakeSymbolic(ExecutionState &state, if (!obj) { if (ZeroSeedExtension) { - std::vector &values = - si.assignment.bindings[mo->array]; + std::vector &values = si.assignment.bindings[array]; values = std::vector(mo->size, '\0'); } else if (!AllowSeedExtension) { terminateStateOnError(state, @@ -2980,10 +2980,9 @@ void Executor::executeMakeSymbolic(ExecutionState &state, "user.err"); break; } else { - std::vector &values = - si.assignment.bindings[mo->array]; + std::vector &values = si.assignment.bindings[array]; values.insert(values.begin(), obj->bytes, - obj->bytes + std::min(obj->numBytes, mo->size)); + obj->bytes + std::min(obj->numBytes, mo->size)); if (ZeroSeedExtension) { for (unsigned i=obj->numBytes; isize; ++i) values.push_back('\0'); -- cgit 1.4.1