Merge pull request #116 from MartinNowack/fix_malloc

Fix handling of memory usage in KLEE.

6 files changed, 121 insertions, 5 deletions

diff --git a/autoconf/configure.ac b/autoconf/configure.ac
index 7d4ff994..c1b1d2b8 100644
--- a/autoconf/configure.ac
+++ b/autoconf/configure.ac
@@ -496,6 +496,14 @@ AC_CHECK_HEADERS([selinux/selinux.h],
         AC_SUBST(HAVE_SELINUX, 0))
 
 dnl **************************************************************************
+dnl Test for features
+dnl **************************************************************************
+AC_SEARCH_LIBS(mallinfo,malloc,
+               AC_DEFINE([HAVE_MALLINFO],[1],[Define if mallinfo() is available on this platform.]),
+               AC_MSG_ERROR([mallinfo() must be supported by your malloc implementation])
+              )
+
+dnl **************************************************************************
 dnl Find an install of STP
 dnl **************************************************************************
 
diff --git a/configure b/configure
index 55497c3a..78e6ac69 100755
--- a/configure
+++ b/configure
@@ -4834,6 +4834,68 @@ fi
 done
 
 
+{ $as_echo "$as_me:${as_lineno-$LINENO}: checking for library containing mallinfo" >&5
+$as_echo_n "checking for library containing mallinfo... " >&6; }
+if ${ac_cv_search_mallinfo+:} 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 mallinfo ();
+int
+main ()
+{
+return mallinfo ();
+  ;
+  return 0;
+}
+_ACEOF
+for ac_lib in '' malloc; 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_mallinfo=$ac_res
+fi
+rm -f core conftest.err conftest.$ac_objext \
+    conftest$ac_exeext
+  if ${ac_cv_search_mallinfo+:} false; then :
+  break
+fi
+done
+if ${ac_cv_search_mallinfo+:} false; then :
+
+else
+  ac_cv_search_mallinfo=no
+fi
+rm conftest.$ac_ext
+LIBS=$ac_func_search_save_LIBS
+fi
+{ $as_echo "$as_me:${as_lineno-$LINENO}: result: $ac_cv_search_mallinfo" >&5
+$as_echo "$ac_cv_search_mallinfo" >&6; }
+ac_res=$ac_cv_search_mallinfo
+if test "$ac_res" != no; then :
+  test "$ac_res" = "none required" || LIBS="$ac_res $LIBS"
+
+$as_echo "#define HAVE_MALLINFO 1" >>confdefs.h
+
+else
+  as_fn_error $? "mallinfo() must be supported by your malloc implementation" "$LINENO" 5
+
+fi
+
+
 
 
 # Check whether --with-stp was given.
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in
index 3f6da802..5e49e35d 100644
--- a/include/klee/Config/config.h.in
+++ b/include/klee/Config/config.h.in
@@ -12,6 +12,9 @@
 /* Define to 1 if you have the `stp' library (-lstp). */
 #undef HAVE_LIBSTP
 
+/* Define if mallinfo() is available on this platform. */
+#undef HAVE_MALLINFO
+
 /* Define to 1 if you have the <memory.h> header file. */
 #undef HAVE_MEMORY_H
 
diff --git a/include/klee/Internal/System/MemoryUsage.h b/include/klee/Internal/System/MemoryUsage.h
new file mode 100644
index 00000000..e8e5d769
--- /dev/null
+++ b/include/klee/Internal/System/MemoryUsage.h
@@ -0,0 +1,21 @@
+//===-- MemoryUsage.h -------------------------------------------*- C++ -*-===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#ifndef KLEE_UTIL_MEMORYUSAGE_H
+#define KLEE_UTIL_MEMORYUSAGE_H
+
+#include <cstddef>
+
+namespace klee {
+  namespace util {
+    size_t GetTotalMallocUsage();
+  }
+}
+
+#endif
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 070f825e..abb023eb 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -47,6 +47,7 @@
 #include "klee/Internal/Module/KModule.h"
 #include "klee/Internal/Support/FloatEvaluation.h"
 #include "klee/Internal/System/Time.h"
+#include "klee/Internal/System/MemoryUsage.h"
 
 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
 #include "llvm/IR/Function.h"
@@ -2584,11 +2585,7 @@ void Executor::run(ExecutionState &initialState) {
         // We need to avoid calling GetMallocUsage() often because it
         // is O(elts on freelist). This is really bad since we start
         // to pummel the freelist once we hit the memory cap.
-#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 3)
-        unsigned mbs = sys::Process::GetMallocUsage() >> 20;
-#else
-        unsigned mbs = sys::Process::GetTotalMemoryUsage() >> 20;
-#endif
+        unsigned mbs = util::GetTotalMallocUsage() >> 20;
         if (mbs > MaxMemory) {
           if (mbs > MaxMemory + 100) {
             // just guess at how many to kill
diff --git a/lib/Support/MemoryUsage.cpp b/lib/Support/MemoryUsage.cpp
new file mode 100644
index 00000000..676ce307
--- /dev/null
+++ b/lib/Support/MemoryUsage.cpp
@@ -0,0 +1,25 @@
+//===-- MemoryUsage.cpp ---------------------------------------------------===//
+//
+//                     The KLEE Symbolic Virtual Machine
+//
+// This file is distributed under the University of Illinois Open Source
+// License. See LICENSE.TXT for details.
+//
+//===----------------------------------------------------------------------===//
+
+#include "klee/Internal/System/MemoryUsage.h"
+#include <malloc.h>
+
+using namespace klee;
+
+size_t util::GetTotalMallocUsage() {
+  struct mallinfo mi = ::mallinfo();
+  // The malloc implementation in glibc (pmalloc2)
+  // does not include mmap()'ed memory in mi.uordblks
+  // but other implementations (e.g. tcmalloc) do.
+#if defined(__GLIBC__)
+  return mi.uordblks + mi.hblkhd;
+#else
+  return mi.uordblks;
+#endif
+}