diff options
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/Executor.cpp | 4 | ||||
-rw-r--r-- | lib/Core/Memory.cpp | 84 | ||||
-rw-r--r-- | lib/Core/Memory.h | 8 |
3 files changed, 81 insertions, 15 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 30c30928..39c6d78a 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2952,8 +2952,8 @@ void Executor::executeMakeSymbolic(ExecutionState &state, 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); + bindObjectInState(state, mo, false, array); + state.addSymbolic(mo, array); std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = seedMap.find(&state); diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index 04f68737..9a79abfd 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -21,6 +21,7 @@ #include <llvm/Function.h> #include <llvm/Instruction.h> #include <llvm/Value.h> +#include "llvm/Support/CommandLine.h" #include <iostream> #include <cassert> @@ -29,6 +30,12 @@ using namespace llvm; using namespace klee; +namespace { + cl::opt<bool> + UseConstantArrays("use-constant-arrays", + cl::init(true)); +} + /***/ ObjectHolder::ObjectHolder(const ObjectHolder &b) : os(b.os) { @@ -91,14 +98,15 @@ ObjectState::ObjectState(const MemoryObject *mo) concreteMask(0), flushMask(0), knownSymbolics(0), - size(mo->size), updates(0, 0), + size(mo->size), readOnly(false) { - // FIXME: Leaked. - static unsigned id = 0; - const Array *array = new Array("tmp_arr" + llvm::utostr(++id), - size); - updates = UpdateList(array, 0); + if (!UseConstantArrays) { + // FIXME: Leaked. + static unsigned id = 0; + const Array *array = new Array("tmp_arr" + llvm::utostr(++id), size); + updates = UpdateList(array, 0); + } } @@ -110,8 +118,8 @@ ObjectState::ObjectState(const MemoryObject *mo, const Array *array) concreteMask(0), flushMask(0), knownSymbolics(0), - size(mo->size), updates(array, 0), + size(mo->size), readOnly(false) { makeSymbolic(); } @@ -124,8 +132,8 @@ ObjectState::ObjectState(const ObjectState &os) concreteMask(os.concreteMask ? new BitArray(*os.concreteMask, os.size) : 0), flushMask(os.flushMask ? new BitArray(*os.flushMask, os.size) : 0), knownSymbolics(0), - size(os.size), updates(os.updates), + size(os.size), readOnly(false) { assert(!os.readOnly && "no need to copy read only object?"); @@ -147,6 +155,62 @@ ObjectState::~ObjectState() { /***/ +const UpdateList &ObjectState::getUpdates() const { + // Constant arrays are created lazily. + if (!updates.root) { + // Collect the list of writes, with the oldest writes first. + + // FIXME: We should be able to do this more efficiently, we just need to be + // careful to get the interaction with the cache right. In particular we + // should avoid creating UpdateNode instances we never use. + unsigned NumWrites = updates.head ? updates.head->getSize() : 0; + std::vector< std::pair< ref<Expr>, ref<Expr> > > Writes(NumWrites); + const UpdateNode *un = updates.head; + for (unsigned i = NumWrites; i != 0; un = un->next) { + --i; + Writes[i] = std::make_pair(un->index, un->value); + } + + std::vector< ref<ConstantExpr> > Contents(size); + + // Initialize to zeros. + for (unsigned i = 0, e = size; i != e; ++i) + Contents[i] = ConstantExpr::create(0, Expr::Int8); + + // Pull off as many concrete writes as we can. + unsigned Begin = 0, End = Writes.size(); + for (; Begin != End; ++Begin) { + // Push concrete writes into the constant array. + ConstantExpr *Index = dyn_cast<ConstantExpr>(Writes[Begin].first); + if (!Index) + break; + + ConstantExpr *Value = dyn_cast<ConstantExpr>(Writes[Begin].second); + if (!Value) + break; + + Contents[Index->getConstantValue()] = Value; + } + + // FIXME: We should unique these, there is no good reason to create multiple + // ones. + + // Start a new update list. + // FIXME: Leaked. + static unsigned id = 0; + const Array *array = new Array("const_arr" + llvm::utostr(++id), size, + &Contents[0], + &Contents[0] + Contents.size()); + updates = UpdateList(array, 0); + + // Apply the remaining (non-constant) writes. + for (; Begin != End; ++Begin) + updates.extend(Writes[Begin].first, Writes[Begin].second); + } + + return updates; +} + void ObjectState::makeConcrete() { if (concreteMask) delete concreteMask; if (flushMask) delete flushMask; @@ -304,7 +368,7 @@ ref<Expr> ObjectState::read8(unsigned offset) const { } else { assert(isByteFlushed(offset) && "unflushed byte without cache value"); - return ReadExpr::create(updates, + return ReadExpr::create(getUpdates(), ConstantExpr::create(offset, kMachinePointerType)); } } @@ -323,7 +387,7 @@ ref<Expr> ObjectState::read8(ref<Expr> offset) const { allocInfo.c_str()); } - return ReadExpr::create(updates, offset); + return ReadExpr::create(getUpdates(), offset); } void ObjectState::write8(unsigned offset, uint8_t value) { diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index 85f83ee1..d9849d2e 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -151,12 +151,12 @@ private: ref<Expr> *knownSymbolics; -public: - unsigned size; - // mutable because we may need flush during read of const mutable UpdateList updates; +public: + unsigned size; + bool readOnly; public: @@ -199,6 +199,8 @@ public: void write64(unsigned offset, uint64_t value); private: + const UpdateList &getUpdates() const; + void makeConcrete(); void makeSymbolic(); |