diff options
author | MartinNowack <martin.nowack@gmail.com> | 2016-02-29 14:14:43 +0100 |
---|---|---|
committer | MartinNowack <martin.nowack@gmail.com> | 2016-02-29 14:14:43 +0100 |
commit | ce1dd5a7f3de7b536a9ff266a9231b44a053fe95 (patch) | |
tree | 47dd5e214efaa3a28333a071c30a35895a03b5ed | |
parent | 0fc86ca9e28cc411cb5e00afa22c32e77aca7e57 (diff) | |
parent | 18f01e9f6d5471d176091f24671bef3eac0293ac (diff) | |
download | klee-ce1dd5a7f3de7b536a9ff266a9231b44a053fe95.tar.gz |
Merge pull request #344 from MartinNowack/feat_malloc
Add support for tcmalloc
-rw-r--r-- | .travis.yml | 6 | ||||
-rwxr-xr-x | .travis/install-llvm-and-runtime-compiler.sh | 4 | ||||
-rwxr-xr-x | .travis/install-tcmalloc.sh | 12 | ||||
-rwxr-xr-x | .travis/klee.sh | 8 | ||||
-rw-r--r-- | Makefile.config.in | 3 | ||||
-rw-r--r-- | autoconf/configure.ac | 35 | ||||
-rwxr-xr-x | configure | 118 | ||||
-rw-r--r-- | include/klee/Config/config.h.in | 3 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 67 | ||||
-rw-r--r-- | lib/Core/Executor.h | 3 | ||||
-rw-r--r-- | lib/Core/StatsTracker.cpp | 7 | ||||
-rw-r--r-- | lib/Support/MemoryUsage.cpp | 11 | ||||
-rw-r--r-- | tools/kleaver/Makefile | 4 | ||||
-rw-r--r-- | tools/klee/Makefile | 4 |
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 |