about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--include/klee/Internal/System/MemoryUsage.h21
-rw-r--r--lib/Core/Executor.cpp7
-rw-r--r--lib/Support/MemoryUsage.cpp19
3 files changed, 42 insertions, 5 deletions
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 <cstddef>
+
+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 <malloc.h>
+
+using namespace klee;
+
+size_t util::GetTotalMemoryUsage() {
+  // This is linux platform specific
+  struct mallinfo mi = ::mallinfo();
+  return mi.uordblks + mi.hblkhd;
+}