diff options
author | Martin Nowack <m.nowack@imperial.ac.uk> | 2023-05-16 15:23:11 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2023-05-26 21:01:54 +0100 |
commit | 7667c5c71748f319f2b8b2e7fb0cbc884bde04d4 (patch) | |
tree | 4a9a6ebe782689b7fb8842fd9c68284fa7546a66 /lib | |
parent | 8500a8190fe61dd9240d91baf849cba0cc859b82 (diff) | |
download | klee-7667c5c71748f319f2b8b2e7fb0cbc884bde04d4.tar.gz |
Use unique_ptr for MemoryManager and avoid re-creating it in the first place
No need to re-create and re-alloc all the memory again after execution.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/Executor.cpp | 9 | ||||
-rw-r--r-- | lib/Core/Executor.h | 2 | ||||
-rw-r--r-- | lib/Core/MemoryManager.h | 2 |
3 files changed, 6 insertions, 7 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 0b28d608..5194aff2 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -494,7 +494,7 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, interpreterHandler->getOutputFilename(SOLVER_QUERIES_KQUERY_FILE_NAME)); this->solver = std::make_unique<TimingSolver>(std::move(solver), EqualitySubstitution); - memory = new MemoryManager(&arrayCache); + memory = std::make_unique<MemoryManager>(&arrayCache); initializeSearchOptions(); @@ -589,7 +589,6 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &modules, } Executor::~Executor() { - delete memory; delete externalDispatcher; delete specialFunctionHandler; delete statsTracker; @@ -4548,7 +4547,8 @@ void Executor::runFunctionAsMain(Function *f, } } - ExecutionState *state = new ExecutionState(kmodule->functionMap[f], memory); + ExecutionState *state = + new ExecutionState(kmodule->functionMap[f], memory.get()); if (pathWriter) state->pathOS = pathWriter->open(); @@ -4597,8 +4597,7 @@ void Executor::runFunctionAsMain(Function *f, processTree = nullptr; // hack to clear memory objects - delete memory; - memory = new MemoryManager(NULL); + memory = nullptr; globalObjects.clear(); globalAddresses.clear(); diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 40111af9..204638e8 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -111,7 +111,7 @@ private: ExternalDispatcher *externalDispatcher; std::unique_ptr<TimingSolver> solver; - MemoryManager *memory; + std::unique_ptr<MemoryManager> memory; std::set<ExecutionState*, ExecutionStateIDCompare> states; StatsTracker *statsTracker; TreeStreamWriter *pathWriter, *symPathWriter; diff --git a/lib/Core/MemoryManager.h b/lib/Core/MemoryManager.h index 71a70183..c8ef8016 100644 --- a/lib/Core/MemoryManager.h +++ b/lib/Core/MemoryManager.h @@ -38,7 +38,7 @@ private: kdalloc::Allocator constantsAllocator; public: - MemoryManager(ArrayCache *arrayCache); + explicit MemoryManager(ArrayCache *arrayCache); ~MemoryManager(); kdalloc::AllocatorFactory heapFactory; |