From c813f1464ce8ad98d45a6a132499247251e15d96 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 23 Feb 2016 15:29:58 +0100 Subject: 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. --- Makefile.config.in | 3 + autoconf/configure.ac | 35 ++++++++++++ configure | 118 ++++++++++++++++++++++++++++++++++++++++ include/klee/Config/config.h.in | 3 + lib/Support/MemoryUsage.cpp | 11 +++- tools/kleaver/Makefile | 4 ++ tools/klee/Makefile | 4 ++ 7 files changed, 177 insertions(+), 1 deletion(-) 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 @@ -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 ************************************************************************** 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 header file. */ +#undef HAVE_GPERFTOOLS_MALLOC_EXTENSION_H + /* Define to 1 if you have the 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 #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 -- cgit 1.4.1 From b9b40354336dfac0847041119f64c8d11db8b5e3 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 23 Feb 2016 15:30:39 +0100 Subject: Refactoring: Extract checking memory limit into own function --- lib/Core/Executor.cpp | 67 ++++++++++++++++++++++++++------------------------- lib/Core/Executor.h | 3 ++- 2 files changed, 36 insertions(+), 34 deletions(-) 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 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 arr(states.begin(), states.end()); - for (unsigned i=0,N=arr.size(); N && icoveredNew) - 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(); -- cgit 1.4.1 From 4d082d995e5404de0058f6db2b008a3f830c627d Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Sun, 21 Feb 2016 10:15:08 +0000 Subject: Use klee-provided GetMallocUsage for consistency --- lib/Core/StatsTracker.cpp | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) 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 -- cgit 1.4.1 From a6a5c148b63f811a6df1e5a3eb6edd43148df510 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 23 Feb 2016 14:17:20 +0000 Subject: Update travis configuration to use tcmalloc We have to build our own tcmalloc, as the version provided with Ubtuntu 12.04 is too old. --- .travis.yml | 1 + .travis/install-llvm-and-runtime-compiler.sh | 4 ++-- .travis/install-tcmalloc.sh | 10 ++++++++++ .travis/klee.sh | 4 ++-- 4 files changed, 15 insertions(+), 4 deletions(-) create mode 100755 .travis/install-tcmalloc.sh diff --git a/.travis.yml b/.travis.yml index 9a17f968..db6a27ac 100644 --- a/.travis.yml +++ b/.travis.yml @@ -92,6 +92,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..8d60a997 --- /dev/null +++ b/.travis/install-tcmalloc.sh @@ -0,0 +1,10 @@ +#!/bin/bash -x +set -ev + +# 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 diff --git a/.travis/klee.sh b/.travis/klee.sh index 0f855b46..acb2a8d1 100755 --- a/.travis/klee.sh +++ b/.travis/klee.sh @@ -141,11 +141,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 -- cgit 1.4.1 From 18f01e9f6d5471d176091f24671bef3eac0293ac Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Sat, 27 Feb 2016 15:13:07 +0100 Subject: Travis: Run TCMalloc runs explicitly --- .travis.yml | 5 +++++ .travis/install-tcmalloc.sh | 16 +++++++++------- .travis/klee.sh | 4 ++++ 3 files changed, 18 insertions(+), 7 deletions(-) diff --git a/.travis.yml b/.travis.yml index db6a27ac..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= diff --git a/.travis/install-tcmalloc.sh b/.travis/install-tcmalloc.sh index 8d60a997..5a86380b 100755 --- a/.travis/install-tcmalloc.sh +++ b/.travis/install-tcmalloc.sh @@ -1,10 +1,12 @@ #!/bin/bash -x set -ev -# 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 +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 acb2a8d1..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} \ -- cgit 1.4.1