Replace CMM flag with debug CMM flag, fix leak in debug CMM (#1586)

Previously, we had -DCVC4_CONTEXT_MEMORY_MANAGER that needed to be added as a compile flag
to use the context memory manager (which we want by default). This makes compiling with
other build systems cumbersome because you have to know about the flag.

This commit replaces the -DCVC4_CONTEXT_MEMORY_MANAGER flag with a -DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER
flag that does the opposite (in absence of the flag, we use the context memory manager).
Additionally, the commit fixes a memory leak in the debug context memory manager (the
destructor did not clean up the allocations).

diff --git a/configure.ac b/configure.ac
index 319b8d79f7b380ca4df3058bd83a586530f2b05c..ef12e4825c74cb20490d00bf43a7b5b07f451ddd 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -674,20 +674,20 @@ if test "$enable_valgrind" != no; then
                   ])
 fi
 
-AC_MSG_CHECKING([whether to use the context memory manager])
+AC_MSG_CHECKING([whether to use the debug context memory manager])
 
-AC_ARG_ENABLE([context-memory-manager],
-  [AS_HELP_STRING([--disable-context-memory-manager],
-     [do not use the context memory manager])])
+AC_ARG_ENABLE([debug-context-memory-manager],
+  [AS_HELP_STRING([--enable-debug-context-memory-manager],
+     [use the debug context memory manager])])
 
-if test -z "${enable_context_memory_manager+set}"; then
-  enable_context_memory_manager=yes
+if test -z "${enable_debug_context_memory_manager+set}"; then
+  enable_debug_context_memory_manager=no
 fi
 
-AC_MSG_RESULT([$enable_context_memory_manager])
+AC_MSG_RESULT([$enable_debug_context_memory_manager])
 
-if test "$enable_context_memory_manager" = yes; then
-  CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_CONTEXT_MEMORY_MANAGER"
+if test "$enable_debug_context_memory_manager" = yes; then
+  CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER"
 fi
 
 AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4])

diff --git a/src/context/context_mm.cpp b/src/context/context_mm.cpp
index a36d523f7595d0bcfe6aa8fc50d89506df8d3abb..bbaf606eccf95957e74bd4381f561eb9006bded8 100644 (file)
--- a/src/context/context_mm.cpp
+++ b/src/context/context_mm.cpp
@@ -31,7 +31,7 @@
 namespace CVC4 {
 namespace context {
 
-#ifdef CVC4_CONTEXT_MEMORY_MANAGER
+#ifndef CVC4_DEBUG_CONTEXT_MEMORY_MANAGER
 
 void ContextMemoryManager::newChunk() {
 
@@ -168,7 +168,7 @@ void ContextMemoryManager::pop() {
   }
 }
 
-#endif /* CVC4_CONTEXT_MEMORY_MANAGER */
+#endif /* CVC4_DEBUG_CONTEXT_MEMORY_MANAGER */
 
 } /* CVC4::context namespace */
 } /* CVC4 namespace */

diff --git a/src/context/context_mm.h b/src/context/context_mm.h
index b7e5ec119ee936232b49be8f2498bef550e8625e..3607d97c336613b55c95aff34671eab6e9ee328f 100644 (file)
--- a/src/context/context_mm.h
+++ b/src/context/context_mm.h
@@ -27,7 +27,7 @@
 namespace CVC4 {
 namespace context {
 
-#ifdef CVC4_CONTEXT_MEMORY_MANAGER
+#ifndef CVC4_DEBUG_CONTEXT_MEMORY_MANAGER
 
 /**
  * Region-based memory manager for contexts.  Calls to newData provide memory
@@ -148,11 +148,14 @@ class ContextMemoryManager {
 
 };/* class ContextMemoryManager */
 
-#else /* CVC4_CONTEXT_MEMORY_MANAGER */
+#else /* CVC4_DEBUG_CONTEXT_MEMORY_MANAGER */
+
+#warning \
+    "Using the debug version of ContextMemoryManager, expect performance degradation"
 
 /**
  * Dummy implementation of the ContextMemoryManager for debugging purposes. Use
- * the configure flag "--disable-context-memory-manager" to use this
+ * the configure flag "--enable-debug-context-memory-manager" to use this
  * implementation.
  */
 class ContextMemoryManager
@@ -164,6 +167,16 @@ class ContextMemoryManager
   }
 
   ContextMemoryManager() { d_allocations.push_back(std::vector<char*>()); }
+  ~ContextMemoryManager()
+  {
+    for (const auto& levelAllocs : d_allocations)
+    {
+      for (auto alloc : levelAllocs)
+      {
+        free(alloc);
+      }
+    }
+  }
 
   void* newData(size_t size)
   {
@@ -187,7 +200,7 @@ class ContextMemoryManager
   std::vector<std::vector<char*>> d_allocations;
 }; /* ContextMemoryManager */
 
-#endif /* CVC4_CONTEXT_MEMORY_MANAGER */
+#endif /* CVC4_DEBUG_CONTEXT_MEMORY_MANAGER */
 
 /**
  * An STL-like allocator class for allocating from context memory.