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 | |
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')
-rw-r--r-- | src/context/context_mm.cpp | 42 | ||||
-rw-r--r-- | src/context/context_mm.h | 55 |
2 files changed, 95 insertions, 2 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 */ diff --git a/src/context/context_mm.h b/src/context/context_mm.h index 974135e3e..8125fbd14 100644 --- a/src/context/context_mm.h +++ b/src/context/context_mm.h @@ -20,12 +20,15 @@ #ifndef __CVC4__CONTEXT__CONTEXT_MM_H #define __CVC4__CONTEXT__CONTEXT_MM_H -#include <vector> #include <deque> +#include <limits> +#include <vector> namespace CVC4 { namespace context { +#ifdef CVC4_CONTEXT_MEMORY_MANAGER + /** * Region-based memory manager for contexts. Calls to newData provide memory * from the current region. This memory will persist until the entire @@ -101,8 +104,15 @@ class ContextMemoryManager { */ void newChunk(); -public: +#ifdef CVC4_VALGRIND + /** + * Vector of allocations for each level. Used for accurately marking + * allocations as free'd in Valgrind. + */ + std::vector<std::vector<char*>> d_allocations; +#endif + public: /** * Get the maximum allocation size for this memory manager. */ @@ -138,6 +148,47 @@ public: };/* class ContextMemoryManager */ +#else /* CVC4_CONTEXT_MEMORY_MANAGER */ + +/** + * Dummy implementation of the ContextMemoryManager for debugging purposes. Use + * the configure flag "--disable-context-memory-manager" to use this + * implementation. + */ +class ContextMemoryManager +{ + public: + static unsigned getMaxAllocationSize() + { + return std::numeric_limits<unsigned>::max(); + } + + ContextMemoryManager() { d_allocations.push_back(std::vector<char*>()); } + + void* newData(size_t size) + { + void* alloc = malloc(size); + d_allocations.back().push_back(static_cast<char*>(alloc)); + return alloc; + } + + void push() { d_allocations.push_back(std::vector<char*>()); } + + void pop() + { + for (auto alloc : d_allocations.back()) + { + free(alloc); + } + d_allocations.pop_back(); + } + + private: + std::vector<std::vector<char*>> d_allocations; +}; /* ContextMemoryManager */ + +#endif /* CVC4_CONTEXT_MEMORY_MANAGER */ + /** * An STL-like allocator class for allocating from context memory. */ |