diff options
author | Julian Büning <julian.buening@rwth-aachen.de> | 2020-02-09 15:21:11 +0100 |
---|---|---|
committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2020-06-25 16:30:10 +0100 |
commit | 316886f1379290346c7e9734e1b3e1e299ea1391 (patch) | |
tree | fee27742c42c1b56d1c4d69e5958fb5652323872 | |
parent | c0fba136e40cd632adc863451189f0c77afc917b (diff) | |
download | klee-316886f1379290346c7e9734e1b3e1e299ea1391.tar.gz |
Executor: split initializeGlobals
-rw-r--r-- | lib/Core/Executor.cpp | 28 | ||||
-rw-r--r-- | lib/Core/Executor.h | 3 |
2 files changed, 26 insertions, 5 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index af714c2c..9c5054c0 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -636,6 +636,20 @@ MemoryObject * Executor::addExternalObject(ExecutionState &state, extern void *__dso_handle __attribute__ ((__weak__)); void Executor::initializeGlobals(ExecutionState &state) { + // allocate and initialize globals, done in two passes since we may + // need address of a global in order to initialize some other one. + + // allocate memory objects for all globals + allocateGlobalObjects(state); + + // initialize aliases first, may be needed for global objects + initializeGlobalAliases(); + + // finally, do the actual initialization + initializeGlobalObjects(state); +} + +void Executor::allocateGlobalObjects(ExecutionState &state) { Module *m = kmodule->module.get(); if (m->getModuleInlineAsm() != "") @@ -696,10 +710,7 @@ void Executor::initializeGlobals(ExecutionState &state) { #endif #endif - // allocate and initialize globals, done in two passes since we may - // need address of a global in order to initialize some other one. - // allocate memory objects for all globals for (Module::const_global_iterator i = m->global_begin(), e = m->global_end(); i != e; ++i) { @@ -775,7 +786,11 @@ void Executor::initializeGlobals(ExecutionState &state) { os->initializeToRandom(); } } - +} + +void Executor::initializeGlobalAliases() { + const Module *m = kmodule->module.get(); + // link aliases to their definitions (if bound) for (auto i = m->alias_begin(), ie = m->alias_end(); i != ie; ++i) { // Map the alias to its aliasee's address. This works because we have @@ -791,8 +806,11 @@ void Executor::initializeGlobals(ExecutionState &state) { globalAddresses.insert(std::make_pair(&*i, evalConstant(alias->getAliasee()))); } +} + +void Executor::initializeGlobalObjects(ExecutionState &state) { + const Module *m = kmodule->module.get(); - // once all objects are allocated, do the actual initialization // remember constant objects to initialise their counter part for external // calls std::vector<ObjectState *> constantObjects; diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 4ddbc98e..61664193 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -230,6 +230,9 @@ private: const llvm::Constant *c, unsigned offset); void initializeGlobals(ExecutionState &state); + void allocateGlobalObjects(ExecutionState &state); + void initializeGlobalAliases(); + void initializeGlobalObjects(ExecutionState &state); void stepInstruction(ExecutionState &state); void updateStates(ExecutionState *current); |