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.

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