From 7fa96f70cf52b0f3112046962487e95eab0d88fe Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 5 Sep 2019 16:58:21 +0100 Subject: Mark all constant global memory objects as constant Fixes #264. We first aggregate all constant memory objects initialise them and initialise their counter parts in the concrete memory. After that, we mark memory objects as constant such that they can't be modified (i.e. this includes marking them symbolic). --- lib/Core/Executor.cpp | 16 +++++++++++++++- 1 file changed, 15 insertions(+), 1 deletion(-) (limited to 'lib/Core') diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index bc889f25..4ac848b0 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -788,6 +788,9 @@ void Executor::initializeGlobals(ExecutionState &state) { } // once all objects are allocated, do the actual initialization + // remember constant objects to initialise their counter part for external + // calls + std::vector constantObjects; for (Module::const_global_iterator i = m->global_begin(), e = m->global_end(); i != e; ++i) { @@ -799,9 +802,20 @@ void Executor::initializeGlobals(ExecutionState &state) { ObjectState *wos = state.addressSpace.getWriteable(mo, os); initializeGlobalObject(state, wos, i->getInitializer(), 0); - // if(i->isConstant()) os->setReadOnly(true); + if (i->isConstant()) + constantObjects.emplace_back(wos); } } + + // initialise constant memory that is potentially used with external calls + if (!constantObjects.empty()) { + // initialise the actual memory with constant values + state.addressSpace.copyOutConcretes(); + + // mark constant objects as read-only + for (auto obj : constantObjects) + obj->setReadOnly(true); + } } void Executor::branch(ExecutionState &state, -- cgit 1.4.1