diff options
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. */ |