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.

1 files changed, 45 insertions, 0 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],