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.

4 files changed, 144 insertions, 3 deletions

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 <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.
  */
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() {