diff options
Diffstat (limited to 'lib/Core')
-rw-r--r-- | lib/Core/Executor.cpp | 6 | ||||
-rw-r--r-- | lib/Core/Memory.cpp | 16 | ||||
-rw-r--r-- | lib/Core/Memory.h | 9 |
3 files changed, 30 insertions, 1 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 4fd94dd4..1e1a142b 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -3024,6 +3024,12 @@ void Executor::callExternalFunction(ExecutionState &state, assert(success && "FIXME: Unhandled solver failure"); (void) success; ce->toMemory(&args[wordIndex]); + ObjectPair op; + // Checking to see if the argument is a pointer to something + if (ce->getWidth() == Context::get().getPointerWidth() && + state.addressSpace.resolveOne(ce, op)) { + op.second->flushToConcreteStore(solver, state); + } wordIndex += (ce->getWidth()+63)/64; } else { ref<Expr> arg = toUnique(state, *ai); diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index cd13eada..5c855fb8 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -229,6 +229,22 @@ const UpdateList &ObjectState::getUpdates() const { return updates; } +void ObjectState::flushToConcreteStore(TimingSolver *solver, + const ExecutionState &state) const { + for (unsigned i = 0; i < size; i++) { + if (isByteKnownSymbolic(i)) { + ref<ConstantExpr> ce; + bool success = solver->getValue(state, read8(i), ce); + if (!success) + klee_warning("Solver timed out when getting a value for external call, " + "byte %p+%u will have random value", + (void *)object->address, i); + else + ce->toMemory(concreteStore + i); + } + } +} + void ObjectState::makeConcrete() { delete concreteMask; delete flushMask; diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index e854502c..47dd892a 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -11,6 +11,7 @@ #define KLEE_MEMORY_H #include "Context.h" +#include "TimingSolver.h" #include "klee/Expr.h" #include "llvm/ADT/StringExtras.h" @@ -205,9 +206,15 @@ public: void write16(unsigned offset, uint16_t value); void write32(unsigned offset, uint32_t value); void write64(unsigned offset, uint64_t value); - void print() const; + /* + Looks at all the symbolic bytes of this object, gets a value for them + from the solver and puts them in the concreteStore. + */ + void flushToConcreteStore(TimingSolver *solver, + const ExecutionState &state) const; + private: const UpdateList &getUpdates() const; |