From: Andres Noetzli Date: Fri, 1 Dec 2017 03:00:23 +0000 (-0800) Subject: Add debugging tools for ContextMemoryManager (#1407) X-Git-Tag: cvc5-1.0.0~5439 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6d740ab8167fe0f48ea78306d65e2cb8a4de2d09;p=cvc5.git 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. --- diff --git a/configure.ac b/configure.ac index cb36c7a9d..319b8d79f 100644 --- a/configure.ac +++ b/configure.ac @@ -500,6 +500,7 @@ case "$with_build" in if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi + if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi ;; debug) # unoptimized, debug symbols, assertions, tracing, dumping CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG" @@ -516,6 +517,7 @@ case "$with_build" in if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi + if test -z "${enable_valgrind+set}" ; then enable_valgrind=optional ; fi ;; default) # moderately optimized, assertions, tracing, dumping CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }" @@ -533,6 +535,7 @@ case "$with_build" in if test -z "${enable_tracing+set}" ; then enable_tracing=yes ; fi if test -z "${enable_dumping+set}" ; then enable_dumping=yes ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=no ; fi + if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi ;; competition) # maximally optimized, no assertions, no tracing, no dumping, muzzled CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_COMPETITION_MODE" @@ -550,6 +553,7 @@ case "$with_build" in if test -z "${enable_tracing+set}" ; then enable_tracing=no ; fi if test -z "${enable_dumping+set}" ; then enable_dumping=no ; fi if test -z "${enable_muzzle+set}" ; then enable_muzzle=yes ; fi + if test -z "${enable_valgrind+set}" ; then enable_valgrind=no ; fi if test -z "${user_specified_enable_or_disable_shared}"; then enable_shared=no; fi if test -z "${user_specified_enable_or_disable_static}"; then enable_static=yes; fi if test -z "${enable_static_binary+set}"; then enable_static_binary=yes ; fi @@ -645,6 +649,47 @@ if test "$enable_debug_symbols" = yes; then CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3" fi +AC_MSG_CHECKING([whether to enable Valgrind instrumentation]) + +AC_ARG_ENABLE([valgrind], + [AS_HELP_STRING([--enable-valgrind], + [enable Valgrind instrumentation])]) + +if test -z "${enable_valgrind+set}"; then + enable_valgrind=no +fi + +AC_MSG_RESULT([$enable_valgrind]) + +if test "$enable_valgrind" != no; then + # Valgrind instrumentation is either explicitly enabled (enable_valgrind=yes) + # or enabled if available (enable_valgrind=optional) + AC_CHECK_HEADER([valgrind/memcheck.h], + [CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_VALGRIND"], + [if test "$enable_valgrind" = yes; then + AC_MSG_ERROR([Need valgrind/memcheck.h to enable Valgrind instrumentation]) + else + AC_MSG_NOTICE([valgrind/memcheck.h missing, Valgrind instrumentation disabled]) + fi + ]) +fi + +AC_MSG_CHECKING([whether to use the context memory manager]) + +AC_ARG_ENABLE([context-memory-manager], + [AS_HELP_STRING([--disable-context-memory-manager], + [do not use the context memory manager])]) + +if test -z "${enable_context_memory_manager+set}"; then + enable_context_memory_manager=yes +fi + +AC_MSG_RESULT([$enable_context_memory_manager]) + +if test "$enable_context_memory_manager" = yes; then + CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_CONTEXT_MEMORY_MANAGER" +fi + AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4]) AC_ARG_ENABLE([statistics], 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 #include +#ifdef CVC4_VALGRIND +#include +#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()); +#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(res), size); + d_allocations.back().push_back(static_cast(res)); +#endif /* CVC4_VALGRIND */ + return res; } void ContextMemoryManager::push() { +#ifdef CVC4_VALGRIND + d_allocations.push_back(std::vector()); +#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 #include +#include +#include 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> 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::max(); + } + + ContextMemoryManager() { d_allocations.push_back(std::vector()); } + + void* newData(size_t size) + { + void* alloc = malloc(size); + d_allocations.back().push_back(static_cast(alloc)); + return alloc; + } + + void push() { d_allocations.push_back(std::vector()); } + + void pop() + { + for (auto alloc : d_allocations.back()) + { + free(alloc); + } + d_allocations.pop_back(); + } + + private: + std::vector> d_allocations; +}; /* ContextMemoryManager */ + +#endif /* CVC4_CONTEXT_MEMORY_MANAGER */ + /** * An STL-like allocator class for allocating from context memory. */ diff --git a/test/unit/context/context_mm_black.h b/test/unit/context/context_mm_black.h index 2fcc30e7b..c789702f5 100644 --- a/test/unit/context/context_mm_black.h +++ b/test/unit/context/context_mm_black.h @@ -40,7 +40,7 @@ public: } void testPushPop() { - +#ifdef CVC4_CONTEXT_MEMORY_MANAGER // Push, then allocate, then pop // We make sure that we don't allocate too much so that all the regions // should be reclaimed @@ -91,6 +91,9 @@ public: // Try popping out of scope TS_ASSERT_THROWS(d_cmm->pop(), CVC4::AssertionException); +#else /* CVC4_CONTEXT_MEMORY_MANAGER */ +#warning "Context memory manager disabled, omitting unit tests" +#endif /* __CVC4__CONTEXT__CONTEXT_MM_H */ } void tearDown() {