about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorMartin Nowack <martin@se.inf.tu-dresden.de>2014-04-22 08:46:36 +0200
committerMartin Nowack <martin@se.inf.tu-dresden.de>2014-04-24 13:51:41 +0200
commit45ec4161781755dedc926341f98da2b8fa33695a (patch)
tree499b7eb4177038342f330333a16e9ff4657be929 /lib
parent292e8cc794f01df94ca02279f5833d7a460a62f9 (diff)
downloadklee-45ec4161781755dedc926341f98da2b8fa33695a.tar.gz
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.
Diffstat (limited to 'lib')
-rw-r--r--lib/Core/Executor.cpp7
-rw-r--r--lib/Support/MemoryUsage.cpp19
2 files changed, 21 insertions, 5 deletions
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;
+}