about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.travis.yml6
-rwxr-xr-x.travis/install-llvm-and-runtime-compiler.sh4
-rwxr-xr-x.travis/install-tcmalloc.sh12
-rwxr-xr-x.travis/klee.sh8
-rw-r--r--Makefile.config.in3
-rw-r--r--autoconf/configure.ac35
-rwxr-xr-xconfigure118
-rw-r--r--include/klee/Config/config.h.in3
-rw-r--r--lib/Core/Executor.cpp67
-rw-r--r--lib/Core/Executor.h3
-rw-r--r--lib/Core/StatsTracker.cpp7
-rw-r--r--lib/Support/MemoryUsage.cpp11
-rw-r--r--tools/kleaver/Makefile4
-rw-r--r--tools/klee/Makefile4
14 files changed, 241 insertions, 44 deletions
diff --git a/.travis.yml b/.travis.yml
index 9a17f968..b64754eb 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -48,6 +48,11 @@ env:
 
     # Check at least one Debug+Asserts build
     - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=master KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=0 COVERAGE=0
+
+    # Check with TCMALLOC
+    - LLVM_VERSION=3.4 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
+    - LLVM_VERSION=2.9 SOLVERS=STP STP_VERSION=2.1.0 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0 USE_TCMALLOC=1
+
     global:
     - secure: EF/WAc4BdIRUchF3mjATN3/UwtGWtGaRgb5oIIJHjKhgZFdPsgWsXFgaOB0jaK2hfO/svj/LvlasuRIGxeePVjeaiX8ZlVpuHiX67vdYLY+0kCDRwkusRjm60/GbPU9O/Xjgb/d4aWAEkoq5OnsprVTEvU8iY2JHtAqgwR+wW9I=
     - secure: Hrp1MRSxDUH2GTQg3QR/yUttY/3KmgbFb5e+zyy551dKpHjxJdsNe8bquY9oFoT7KmPQYl0HNNjEv4qWW8RK+HWHOCB55nL1KlGpOG7vAJcUEZg7ScbliGgiovMB6jIQVfeP9FhYngfc13vNZQ5PGlqzfSsHSAbvkwEogBToHVw=
@@ -92,6 +97,7 @@ before_install:
     - sudo update-alternatives --install /usr/bin/clang++ clang++ /usr/bin/clang++-3.4 20
     # Install LLVM and the LLVM bitcode compiler we require to build KLEE
     - ${KLEE_SRC}/.travis/install-llvm-and-runtime-compiler.sh
+    - ${KLEE_SRC}/.travis/install-tcmalloc.sh
     # Install lit (llvm-lit is not available)
     - sudo pip install lit
     # Get SMT solvers
diff --git a/.travis/install-llvm-and-runtime-compiler.sh b/.travis/install-llvm-and-runtime-compiler.sh
index 6fba5baf..13a7f140 100755
--- a/.travis/install-llvm-and-runtime-compiler.sh
+++ b/.travis/install-llvm-and-runtime-compiler.sh
@@ -1,10 +1,10 @@
 #!/bin/bash -x
 set -ev
 
-sudo apt-get install llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev
+sudo apt-get install -y llvm-${LLVM_VERSION} llvm-${LLVM_VERSION}-dev
 
 if [ "${LLVM_VERSION}" != "2.9" ]; then
-    sudo apt-get install llvm-${LLVM_VERSION}-tools clang-${LLVM_VERSION}
+    sudo apt-get install -y llvm-${LLVM_VERSION}-tools clang-${LLVM_VERSION}
 else
     # Get llvm-gcc. We don't bother installing it
     wget http://llvm.org/releases/2.9/llvm-gcc4.2-2.9-x86_64-linux.tar.bz2
diff --git a/.travis/install-tcmalloc.sh b/.travis/install-tcmalloc.sh
new file mode 100755
index 00000000..5a86380b
--- /dev/null
+++ b/.travis/install-tcmalloc.sh
@@ -0,0 +1,12 @@
+#!/bin/bash -x
+set -ev
+
+if [ ${USE_TCMALLOC:-0} -eq 1 ] ; then
+	# Get tcmalloc release
+	wget https://github.com/gperftools/gperftools/releases/download/gperftools-2.4/gperftools-2.4.tar.gz
+	tar xfz gperftools-2.4.tar.gz
+	cd gperftools-2.4
+	./configure --disable-dependency-tracking --disable-cpu-profiler --disable-heap-checker --disable-debugalloc  --enable-minimal --prefix=/usr
+	make
+	sudo make install
+fi
diff --git a/.travis/klee.sh b/.travis/klee.sh
index 0f855b46..296e1c83 100755
--- a/.travis/klee.sh
+++ b/.travis/klee.sh
@@ -68,6 +68,9 @@ for solver in ${SOLVER_LIST}; do
     exit 1
   esac
 done
+
+
+TCMALLOC_OPTION=$([ "${USE_TCMALLOC:-0}" == 1 ] && echo "--with-tcmalloc" || echo "--without-tcmalloc")
 ###############################################################################
 # KLEE
 ###############################################################################
@@ -85,6 +88,7 @@ ${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \
             ${KLEE_STP_CONFIGURE_OPTION} \
             ${KLEE_Z3_CONFIGURE_OPTION} \
             ${KLEE_UCLIBC_CONFIGURE_OPTION} \
+            ${TCMALLOC_OPTION} \
             CXXFLAGS="${COVERAGE_FLAGS}" \
             && make DISABLE_ASSERTIONS=${DISABLE_ASSERTIONS} \
                     ENABLE_OPTIMIZED=${ENABLE_OPTIMIZED} \
@@ -141,11 +145,11 @@ if [ ${COVERAGE} -eq 1 ]; then
     sudo cp style.css /usr/local/lib/python2.7/dist-packages/zcov-0.3.0.dev0-py2.7.egg/zcov/style.css
 
 #install zcov dependency
-    sudo apt-get install enscript
+    sudo apt-get install -y enscript
 
 #update gcov from v4.6 to v4.8. This is becauase gcda files are made for v4.8 and cause 
 #a segmentation fault in v4.6
-    sudo apt-get install ggcov
+    sudo apt-get install -y ggcov
     sudo rm /usr/bin/gcov
     sudo ln -s /usr/bin/gcov-4.8 /usr/bin/gcov
 
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/Core/Executor.cpp b/lib/Core/Executor.cpp
index 854754b0..33cee9f9 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -2437,6 +2437,39 @@ void Executor::bindModuleConstants() {
   }
 }
 
+void Executor::checkMemoryUsage() {
+  if (!MaxMemory)
+    return;
+  if ((stats::instructions & 0xFFFF) == 0) {
+    // We need to avoid calling GetTotalMallocUsage() 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.
+    unsigned mbs = util::GetTotalMallocUsage() >> 20;
+    if (mbs > MaxMemory) {
+      if (mbs > MaxMemory + 100) {
+        // just guess at how many to kill
+        unsigned numStates = states.size();
+        unsigned toKill = std::max(1U, numStates - numStates * MaxMemory / mbs);
+        klee_warning("killing %d states (over memory cap)", toKill);
+        std::vector<ExecutionState *> arr(states.begin(), states.end());
+        for (unsigned i = 0, N = arr.size(); N && i < toKill; ++i, --N) {
+          unsigned idx = rand() % N;
+          // Make two pulls to try and not hit a state that
+          // covered new code.
+          if (arr[idx]->coveredNew)
+            idx = rand() % N;
+
+          std::swap(arr[idx], arr[N - 1]);
+          terminateStateEarly(*arr[N - 1], "Memory limit exceeded.");
+        }
+      }
+      atMemoryLimit = true;
+    } else {
+      atMemoryLimit = false;
+    }
+  }
+}
+
 void Executor::run(ExecutionState &initialState) {
   bindModuleConstants();
 
@@ -2522,39 +2555,7 @@ void Executor::run(ExecutionState &initialState) {
     executeInstruction(state, ki);
     processTimers(&state, MaxInstructionTime);
 
-    if (MaxMemory) {
-      if ((stats::instructions & 0xFFFF) == 0) {
-        // 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.
-        unsigned mbs = util::GetTotalMallocUsage() >> 20;
-        if (mbs > MaxMemory) {
-          if (mbs > MaxMemory + 100) {
-            // just guess at how many to kill
-            unsigned numStates = states.size();
-            unsigned toKill = std::max(1U, numStates - numStates*MaxMemory/mbs);
-
-            klee_warning("killing %d states (over memory cap)", toKill);
-
-            std::vector<ExecutionState*> arr(states.begin(), states.end());
-            for (unsigned i=0,N=arr.size(); N && i<toKill; ++i,--N) {
-              unsigned idx = rand() % N;
-
-              // Make two pulls to try and not hit a state that
-              // covered new code.
-              if (arr[idx]->coveredNew)
-                idx = rand() % N;
-
-              std::swap(arr[idx], arr[N-1]);
-              terminateStateEarly(*arr[N-1], "Memory limit exceeded.");
-            }
-          }
-          atMemoryLimit = true;
-        } else {
-          atMemoryLimit = false;
-        }
-      }
-    }
+    checkMemoryUsage();
 
     updateStates(&state);
   }
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 919d2124..8bfa278a 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -399,7 +399,8 @@ private:
   void initTimers();
   void processTimers(ExecutionState *current,
                      double maxInstTime);
-                
+  void checkMemoryUsage();
+
 public:
   Executor(const InterpreterOptions &opts, InterpreterHandler *ie);
   virtual ~Executor();
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 2e107fb3..9995b7e2 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -16,6 +16,7 @@
 #include "klee/Internal/Module/KModule.h"
 #include "klee/Internal/Module/KInstruction.h"
 #include "klee/Internal/Support/ModuleUtil.h"
+#include "klee/Internal/System/MemoryUsage.h"
 #include "klee/Internal/System/Time.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/SolverStats.h"
@@ -404,11 +405,7 @@ void StatsTracker::writeStatsLine() {
              << "," << numBranches
              << "," << util::getUserTime()
              << "," << executor.states.size()
-#if LLVM_VERSION_CODE > LLVM_VERSION(3, 2)
-             << "," << sys::Process::GetMallocUsage()
-#else
-             << "," << sys::Process::GetTotalMemoryUsage()
-#endif
+             << "," << util::GetTotalMallocUsage()
              << "," << stats::queries
              << "," << stats::queryConstructs
              << "," << 0 // was numObjects
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
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-28 21:00:19 +0000