diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2017-11-30 19:00:23 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-11-30 19:00:23 -0800 |
commit | 6d740ab8167fe0f48ea78306d65e2cb8a4de2d09 (patch) | |
tree | 55af24ca0024a7a5327b936213c055eca96107cf /src/context/context_mm.cpp | |
parent | 4c1f1cad720a94226f7834874cf59478de35b74a (diff) |
Add debugging tools for ContextMemoryManager (#1407)
This commit adds two configuration options that help debugging memory
issues with allocations in the ContextMemoryManager:
--enable/disable-valgrind: This flag enables/disables Valgrind
instrumentation of the ContextMemoryManager. Enabled by default for
debug builds if the Valgrind headers are available.
--enable/disable-context-memory-manager: This flag enables/disables the
use of the ContextMemoryManager. If the flag is disableda dummy
ContextMemoryManager is used that does single allocations instead of
chunks. The flag is enabled by default.
Diffstat (limited to 'src/context/context_mm.cpp')
-rw-r--r-- | src/context/context_mm.cpp | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp index f0f6ebc42..39af8bd9e 100644 --- a/src/context/context_mm.cpp +++ b/src/context/context_mm.cpp @@ -20,6 +20,10 @@ #include <deque> #include <new> +#ifdef CVC4_VALGRIND +#include <valgrind/memcheck.h> +#endif /* CVC4_VALGRIND */ + #include "base/cvc4_assert.h" #include "base/output.h" #include "context/context_mm.h" @@ -27,6 +31,8 @@ namespace CVC4 { namespace context { +#ifdef CVC4_CONTEXT_MEMORY_MANAGER + void ContextMemoryManager::newChunk() { // Increment index to chunk list @@ -40,6 +46,10 @@ void ContextMemoryManager::newChunk() { if(d_chunkList.back() == NULL) { throw std::bad_alloc(); } + +#ifdef CVC4_VALGRIND + VALGRIND_MAKE_MEM_NOACCESS(d_chunkList.back(), chunkSizeBytes); +#endif /* CVC4_VALGRIND */ } // If there is a free chunk, use that else { @@ -60,10 +70,20 @@ ContextMemoryManager::ContextMemoryManager() : d_indexChunkList(0) { throw std::bad_alloc(); } d_endChunk = d_nextFree + chunkSizeBytes; + +#ifdef CVC4_VALGRIND + VALGRIND_CREATE_MEMPOOL(this, 0, false); + VALGRIND_MAKE_MEM_NOACCESS(d_nextFree, chunkSizeBytes); + d_allocations.push_back(std::vector<void*>()); +#endif /* CVC4_VALGRIND */ } ContextMemoryManager::~ContextMemoryManager() { +#ifdef CVC4_VALGRIND + VALGRIND_DESTROY_MEMPOOL(this); +#endif /* CVC4_VALGRIND */ + // Delete all chunks while(!d_chunkList.empty()) { free(d_chunkList.back()); @@ -91,11 +111,21 @@ void* ContextMemoryManager::newData(size_t size) { Debug("context") << "ContextMemoryManager::newData(" << size << ") returning " << res << " at level " << d_chunkList.size() << std::endl; + +#ifdef CVC4_VALGRIND + VALGRIND_MEMPOOL_ALLOC(this, static_cast<char*>(res), size); + d_allocations.back().push_back(static_cast<char*>(res)); +#endif /* CVC4_VALGRIND */ + return res; } void ContextMemoryManager::push() { +#ifdef CVC4_VALGRIND + d_allocations.push_back(std::vector<char*>()); +#endif /* CVC4_VALGRIND */ + // Store current state on the stack d_nextFreeStack.push_back(d_nextFree); d_endChunkStack.push_back(d_endChunk); @@ -104,6 +134,14 @@ void ContextMemoryManager::push() { void ContextMemoryManager::pop() { +#ifdef CVC4_VALGRIND + for (auto allocation : d_allocations.back()) + { + VALGRIND_MEMPOOL_FREE(this, allocation); + } + d_allocations.pop_back(); +#endif /* CVC4_VALGRIND */ + Assert(d_nextFreeStack.size() > 0 && d_endChunkStack.size() > 0); // Restore state from stack @@ -115,6 +153,9 @@ void ContextMemoryManager::pop() { // Free all the new chunks since the last push while(d_indexChunkList > d_indexChunkListStack.back()) { d_freeChunks.push_back(d_chunkList.back()); +#ifdef CVC4_VALGRIND + VALGRIND_MAKE_MEM_NOACCESS(d_chunkList.back(), chunkSizeBytes); +#endif /* CVC4_VALGRIND */ d_chunkList.pop_back(); --d_indexChunkList; } @@ -127,6 +168,7 @@ void ContextMemoryManager::pop() { } } +#endif /* CVC4_CONTEXT_MEMORY_MANAGER */ } /* CVC4::context namespace */ } /* CVC4 namespace */ |