From 45ec4161781755dedc926341f98da2b8fa33695a Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Tue, 22 Apr 2014 08:46:36 +0200 Subject: Fix handling of memory usage in KLEE. Memory usage API in LLVM since 3.3 is not working the way it is intended by KLEE. This ports the pre 3.3. version to KLEE. Fixes the malloc test case. --- include/klee/Internal/System/MemoryUsage.h | 21 +++++++++++++++++++++ lib/Core/Executor.cpp | 7 ++----- lib/Support/MemoryUsage.cpp | 19 +++++++++++++++++++ 3 files changed, 42 insertions(+), 5 deletions(-) create mode 100644 include/klee/Internal/System/MemoryUsage.h create mode 100644 lib/Support/MemoryUsage.cpp diff --git a/include/klee/Internal/System/MemoryUsage.h b/include/klee/Internal/System/MemoryUsage.h new file mode 100644 index 00000000..37c838fc --- /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 + +namespace klee { + namespace util { + size_t GetTotalMemoryUsage(); + } +} + +#endif diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 070f825e..c0baa88c 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::GetTotalMemoryUsage() >> 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..1bdff819 --- /dev/null +++ b/lib/Support/MemoryUsage.cpp @@ -0,0 +1,19 @@ +//===-- 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 + +using namespace klee; + +size_t util::GetTotalMemoryUsage() { + // This is linux platform specific + struct mallinfo mi = ::mallinfo(); + return mi.uordblks + mi.hblkhd; +} -- cgit 1.4.1 From d344b98751232ea79a22c6907175154f3fc9889d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 24 Apr 2014 11:30:34 +0100 Subject: Have configure check for presense of mallinfo for the newly added klee::util::GetTotalMemoryUsage() --- autoconf/configure.ac | 8 ++++++ configure | 62 +++++++++++++++++++++++++++++++++++++++++ include/klee/Config/config.h.in | 3 ++ 3 files changed, 73 insertions(+) diff --git a/autoconf/configure.ac b/autoconf/configure.ac index 7d4ff994..c1b1d2b8 100644 --- a/autoconf/configure.ac +++ b/autoconf/configure.ac @@ -495,6 +495,14 @@ AC_CHECK_HEADERS([selinux/selinux.h], AC_SUBST(HAVE_SELINUX, 1), 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 header file. */ #undef HAVE_MEMORY_H -- cgit 1.4.1 From e2799703b08cc1feb8a324bfb04edfeb2c296e57 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 24 Apr 2014 11:32:54 +0100 Subject: Modify klee::util::GetTotalMemoryUsage() so that if the system is not using glibc the malloc usage if computed differently. --- lib/Support/MemoryUsage.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/lib/Support/MemoryUsage.cpp b/lib/Support/MemoryUsage.cpp index 1bdff819..94cee79e 100644 --- a/lib/Support/MemoryUsage.cpp +++ b/lib/Support/MemoryUsage.cpp @@ -13,7 +13,13 @@ using namespace klee; size_t util::GetTotalMemoryUsage() { - // This is linux platform specific 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 } -- cgit 1.4.1 From 016120fd8a8a2cac8457b66b6d2a41e0b5093889 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Thu, 24 Apr 2014 13:58:03 +0200 Subject: Renamed GetTotalMemoryUsage to GetTotalMallocUsage --- include/klee/Internal/System/MemoryUsage.h | 2 +- lib/Core/Executor.cpp | 2 +- lib/Support/MemoryUsage.cpp | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/include/klee/Internal/System/MemoryUsage.h b/include/klee/Internal/System/MemoryUsage.h index 37c838fc..e8e5d769 100644 --- a/include/klee/Internal/System/MemoryUsage.h +++ b/include/klee/Internal/System/MemoryUsage.h @@ -14,7 +14,7 @@ namespace klee { namespace util { - size_t GetTotalMemoryUsage(); + size_t GetTotalMallocUsage(); } } diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index c0baa88c..abb023eb 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -2585,7 +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. - unsigned mbs = util::GetTotalMemoryUsage() >> 20; + 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 index 94cee79e..676ce307 100644 --- a/lib/Support/MemoryUsage.cpp +++ b/lib/Support/MemoryUsage.cpp @@ -12,7 +12,7 @@ using namespace klee; -size_t util::GetTotalMemoryUsage() { +size_t util::GetTotalMallocUsage() { struct mallinfo mi = ::mallinfo(); // The malloc implementation in glibc (pmalloc2) // does not include mmap()'ed memory in mi.uordblks -- cgit 1.4.1