Merge pull request klee#344 from MartinNowack/feat_malloc

Add support for tcmalloc

.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

.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

.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

.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
 

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@

autoconf/configure.ac

@@ -549,6 +549,41 @@ AC_CHECK_FUNCS([malloc_zone_statistics])
 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 **************************************************************************

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.

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
 

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);
  }

lib/Core/Executor.h

@@ -399,7 +399,8 @@ class Executor : public Interpreter {
  void initTimers();
  void processTimers(ExecutionState *current,
  double maxInstTime);
-
+ void checkMemoryUsage();
+
 public:
  Executor(const InterpreterOptions &opts, InterpreterHandler *ie);
  virtual ~Executor();

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