Add support for tcmalloc

Beside improving performance of KLEE,
tcmalloc allows to track used memory correctly.

If available, tcmalloc is automatically used during compile time.

This can be forced to be:
 - disabled using --without-tcmalloc
 - enabled using --with-tcmalloc
In the second case, configure will fail if tcmalloc
is not found or usable.

Both versions of tcmalloc a minimal and normal version.

7 files changed, 177 insertions, 1 deletions

diff --git a/Makefile.config.in b/Makefile.config.in
index f92f453f..7d3c05f6 100644
--- a/Makefile.config.in
+++ b/Makefile.config.in
@@ -47,6 +47,9 @@ KLEE_UCLIBC_BCA := @KLEE_UCLIBC_BCA@
 
 HAVE_SELINUX := @HAVE_SELINUX@
 
+HAVE_TCMALLOC := @HAVE_TCMALLOC@
+TCMALLOC_LIB := @TCMALLOC_LIB@
+
 RUNTIME_ENABLE_OPTIMIZED := @RUNTIME_ENABLE_OPTIMIZED@
 RUNTIME_DISABLE_ASSERTIONS := @RUNTIME_DISABLE_ASSERTIONS@
 RUNTIME_DEBUG_SYMBOLS := @RUNTIME_DEBUG_SYMBOLS@
diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 617469e6..bb391329 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -550,6 +550,41 @@ AC_SEARCH_LIBS(mallinfo,malloc,
                AC_DEFINE([HAVE_MALLINFO],[1],[Define if mallinfo() is available on this platform.]))
 
 dnl **************************************************************************
+dnl Test for tcmalloc
+dnl **************************************************************************
+
+AC_ARG_WITH([tcmalloc],
+	    AS_HELP_STRING([--without-tcmalloc], [Ignore presence of tcmalloc and disable it (default=detect)]))
+
+AS_IF([test "x$with_tcmalloc" != "xno"],
+      AC_CHECK_HEADERS([gperftools/malloc_extension.h],
+		       [have_tcmalloc=yes], [have_tcmalloc=no]),
+      [have_tcmalloc=no])
+
+AS_IF([test "x$have_tcmalloc" = "xyes"],
+      [
+	AC_SEARCH_LIBS(tc_malloc,tcmalloc_minimal,
+		     [
+		      AC_SUBST(HAVE_TCMALLOC, 1)
+		      if test "${ac_cv_search_tc_malloc}" != "none required"; then
+			 TCMALLOC_LIB=${ac_cv_search_tc_malloc}
+			 AC_SUBST(TCMALLOC_LIB)
+		      fi
+		     ],
+		     [
+		      AC_MSG_WARN([Could not link with tcmalloc])
+		      AC_SUBST(HAVE_TCMALLOC, 0)
+		     ],)
+
+       ],
+      [AS_IF([test "x$with_tcmalloc" = "xyes"],
+	     [AC_MSG_ERROR([tcmalloc requested but not found])],
+	     [
+	      AC_SUBST(HAVE_TCMALLOC, 0)
+	      ])
+])
+
+dnl **************************************************************************
 dnl Find an install of STP
 dnl **************************************************************************
 
diff --git a/configure b/configure
index 4da72718..d4ef1048 100755
--- a/configure
+++ b/configure
@@ -632,6 +632,8 @@ ENABLE_Z3
 STP_LDFLAGS
 STP_CFLAGS
 ENABLE_STP
+TCMALLOC_LIB
+HAVE_TCMALLOC
 CXXCPP
 HAVE_SELINUX
 EGREP
@@ -733,6 +735,7 @@ with_llvmcxx
 with_uclibc
 enable_posix_runtime
 with_runtime
+with_tcmalloc
 with_stp
 with_z3
 with_metasmt
@@ -1385,6 +1388,8 @@ Optional Packages:
                           (klee-uclibc root directory or libc.a file
   --with-runtime          Select build configuration for runtime libraries
                           (default [Release+Asserts])
+  --without-tcmalloc      Ignore presence of tcmalloc and disable it
+                          (default=detect)
   --with-stp              Location of STP installation directory
   --with-z3               Location of Z3 installation directory
   --with-metasmt          Location of metaSMT installation directory
@@ -4871,6 +4876,119 @@ fi
 
 
 
+
+# Check whether --with-tcmalloc was given.
+if test "${with_tcmalloc+set}" = set; then :
+  withval=$with_tcmalloc;
+fi
+
+
+if test "x$with_tcmalloc" != "xno"; then :
+  for ac_header in gperftools/malloc_extension.h
+do :
+  ac_fn_cxx_check_header_mongrel "$LINENO" "gperftools/malloc_extension.h" "ac_cv_header_gperftools_malloc_extension_h" "$ac_includes_default"
+if test "x$ac_cv_header_gperftools_malloc_extension_h" = xyes; then :
+  cat >>confdefs.h <<_ACEOF
+#define HAVE_GPERFTOOLS_MALLOC_EXTENSION_H 1
+_ACEOF
+ have_tcmalloc=yes
+else
+  have_tcmalloc=no
+fi
+
+done
+
+else
+  have_tcmalloc=no
+fi
+
+if test "x$have_tcmalloc" = "xyes"; then :
+
+	{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for library containing tc_malloc" >&5
+$as_echo_n "checking for library containing tc_malloc... " >&6; }
+if ${ac_cv_search_tc_malloc+:} false; then :
+  $as_echo_n "(cached) " >&6
+else
+  ac_func_search_save_LIBS=$LIBS
+cat confdefs.h - <<_ACEOF >conftest.$ac_ext
+/* end confdefs.h.  */
+
+/* Override any GCC internal prototype to avoid an error.
+   Use char because int might match the return type of a GCC
+   builtin and then its argument prototype would still apply.  */
+#ifdef __cplusplus
+extern "C"
+#endif
+char tc_malloc ();
+int
+main ()
+{
+return tc_malloc ();
+  ;
+  return 0;
+}
+_ACEOF
+for ac_lib in '' tcmalloc_minimal; do
+  if test -z "$ac_lib"; then
+    ac_res="none required"
+  else
+    ac_res=-l$ac_lib
+    LIBS="-l$ac_lib  $ac_func_search_save_LIBS"
+  fi
+  if ac_fn_cxx_try_link "$LINENO"; then :
+  ac_cv_search_tc_malloc=$ac_res
+fi
+rm -f core conftest.err conftest.$ac_objext \
+    conftest$ac_exeext
+  if ${ac_cv_search_tc_malloc+:} false; then :
+  break
+fi
+done
+if ${ac_cv_search_tc_malloc+:} false; then :
+
+else
+  ac_cv_search_tc_malloc=no
+fi
+rm conftest.$ac_ext
+LIBS=$ac_func_search_save_LIBS
+fi
+{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_search_tc_malloc" >&5
+$as_echo "$ac_cv_search_tc_malloc" >&6; }
+ac_res=$ac_cv_search_tc_malloc
+if test "$ac_res" != no; then :
+  test "$ac_res" = "none required" || LIBS="$ac_res $LIBS"
+
+		      HAVE_TCMALLOC=1
+
+		      if test "${ac_cv_search_tc_malloc}" != "none required"; then
+			 TCMALLOC_LIB=${ac_cv_search_tc_malloc}
+
+		      fi
+
+else
+
+		      { $as_echo "$as_me:${as_lineno-$LINENO}: WARNING: Could not link with tcmalloc" >&5
+$as_echo "$as_me: WARNING: Could not link with tcmalloc" >&2;}
+		      HAVE_TCMALLOC=0
+
+
+fi
+
+
+
+else
+  if test "x$with_tcmalloc" = "xyes"; then :
+  as_fn_error $? "tcmalloc requested but not found" "$LINENO" 5
+else
+
+	      HAVE_TCMALLOC=0
+
+
+fi
+
+fi
+
+
 ENABLE_STP=0
 
 # Check whether --with-stp was given.
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 66bf31cb..9adf7306 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -18,6 +18,9 @@
 /* Does the platform use __ctype_b_loc, etc. */
 #undef HAVE_CTYPE_EXTERNALS
 
+/* Define to 1 if you have the <gperftools/malloc_extension.h> header file. */
+#undef HAVE_GPERFTOOLS_MALLOC_EXTENSION_H
+
 /* Define to 1 if you have the <inttypes.h> header file. */
 #undef HAVE_INTTYPES_H
 
diff --git a/lib/Support/MemoryUsage.cpp b/lib/Support/MemoryUsage.cpp
index 32a7eb3b..a9f4026d 100644
--- a/lib/Support/MemoryUsage.cpp
+++ b/lib/Support/MemoryUsage.cpp
@@ -11,6 +11,10 @@
 
 #include "klee/Config/config.h"
 
+#ifdef HAVE_GPERFTOOLS_MALLOC_EXTENSION_H
+#include "gperftools/malloc_extension.h"
+#endif
+
 #ifdef HAVE_MALLINFO
 #include <malloc.h>
 #endif
@@ -21,7 +25,12 @@
 using namespace klee;
 
 size_t util::GetTotalMallocUsage() {
-#ifdef HAVE_MALLINFO
+#ifdef HAVE_GPERFTOOLS_MALLOC_EXTENSION_H
+  uint64_t value;
+  MallocExtension::instance()->GetNumericProperty(
+      "generic.current_allocated_bytes", &value);
+  return value;
+#elif HAVE_MALLINFO
   struct mallinfo mi = ::mallinfo();
   // The malloc implementation in glibc (pmalloc2)
   // does not include mmap()'ed memory in mi.uordblks
diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile
index 08249444..1631dda6 100644
--- a/tools/kleaver/Makefile
+++ b/tools/kleaver/Makefile
@@ -28,3 +28,7 @@ ifneq ($(ENABLE_Z3),0)
 endif
 
 include $(PROJ_SRC_ROOT)/MetaSMT.mk
+
+ifeq ($(HAVE_TCMALLOC),1)
+  LIBS += $(TCMALLOC_LIB)
+endif
diff --git a/tools/klee/Makefile b/tools/klee/Makefile
index e3364e77..676507e0 100644
--- a/tools/klee/Makefile
+++ b/tools/klee/Makefile
@@ -29,3 +29,7 @@ ifneq ($(ENABLE_Z3),0)
 endif
 
 include $(PROJ_SRC_ROOT)/MetaSMT.mk
+
+ifeq ($(HAVE_TCMALLOC),1)
+  LIBS += $(TCMALLOC_LIB)
+endif