From d101b22997470c78b94e183db0b451c95878a999 Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Sun, 14 Jan 2018 00:04:29 +0000
Subject: [PATCH] Set memory limit utility

---
 src/util/Makefile         |  1 +
 src/util/memory_limit.cpp | 48 +++++++++++++++++++++++++++++++++++++++
 src/util/memory_limit.h   | 18 +++++++++++++++
 3 files changed, 67 insertions(+)
 create mode 100644 src/util/memory_limit.cpp
 create mode 100644 src/util/memory_limit.h

diff --git a/src/util/Makefile b/src/util/Makefile
index 4592c896966..0b1f8aa67a8 100644
--- a/src/util/Makefile
+++ b/src/util/Makefile
@@ -40,6 +40,7 @@ SRC = arith_tools.cpp \
       lispexpr.cpp \
       lispirep.cpp \
       memory_info.cpp \
+      memory_limit.cpp \
       merge_irep.cpp \
       message.cpp \
       mp_arith.cpp \
diff --git a/src/util/memory_limit.cpp b/src/util/memory_limit.cpp
new file mode 100644
index 00000000000..c312b6bea08
--- /dev/null
+++ b/src/util/memory_limit.cpp
@@ -0,0 +1,48 @@
+/*******************************************************************\
+
+Module:
+
+Author: Peter Schrammel, peter.schrammel@diffblue.com
+
+\*******************************************************************/
+
+#include "memory_limit.h"
+
+#ifdef __linux__
+#include <sys/resource.h>
+#endif
+
+#include <ostream>
+
+/// Outputs the memory limits to the given output stream
+/// \param out: output stream
+void memory_limits(std::ostream &out)
+{
+#ifdef __linux__
+  struct rlimit mem_limit;
+  getrlimit(RLIMIT_AS, &mem_limit);
+
+  out << "  soft limit: " << mem_limit.rlim_cur << '\n';
+  out << "  hard limit: " << mem_limit.rlim_max;
+#else
+  out << "  not supported";
+#endif
+}
+
+/// Sets the soft memory limit of the current process
+/// \param soft_limit: the soft limit in bytes
+/// \return: true if setting the limit succeeded
+bool set_memory_limit(std::size_t soft_limit)
+{
+#ifdef __linux__
+  struct rlimit mem_limit;
+  getrlimit(RLIMIT_AS, &mem_limit);
+  mem_limit.rlim_cur = soft_limit;
+  setrlimit(RLIMIT_AS, &mem_limit);
+  getrlimit(RLIMIT_AS, &mem_limit);
+  return mem_limit.rlim_cur == soft_limit;
+#else
+  // not supported
+  return false;
+#endif
+}
diff --git a/src/util/memory_limit.h b/src/util/memory_limit.h
new file mode 100644
index 00000000000..53aaef125e9
--- /dev/null
+++ b/src/util/memory_limit.h
@@ -0,0 +1,18 @@
+/*******************************************************************\
+
+Module:
+
+Author: Peter Schrammel, peter.schrammel@diffblue.com
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_MEMORY_LIMIT_H
+#define CPROVER_UTIL_MEMORY_LIMIT_H
+
+#include <cstddef> // size_t
+#include <iosfwd>
+
+void memory_limits(std::ostream &);
+bool set_memory_limit(std::size_t soft_limit);
+
+#endif // CPROVER_UTIL_MEMORY_LIMIT_H