use rlimit to enforce memory limits rather than global allocators

Lib/Allocator.cpp

@@ -16,79 +16,23 @@
  * @since 24/07/2023, mostly replaced by a small-object allocator
  */
 
-#include <cstdlib>
-#include <limits>
-
 #include "Allocator.hpp"
 
-#include <cstdlib>
-#include <limits>
-
 #ifndef INDIVIDUAL_ALLOCATIONS
 Lib::SmallObjectAllocator Lib::GLOBAL_SMALL_OBJECT_ALLOCATOR;
 #endif
 
-static size_t ALLOCATED = 0;
-// set by main very soon after launch
-static size_t LIMIT = std::numeric_limits<size_t>::max();
-
-size_t Lib::getUsedMemory() { return ALLOCATED; }
-size_t Lib::getMemoryLimit() { return LIMIT; }
-void Lib::setMemoryLimit(size_t limit) { LIMIT = limit; }
-
-// override global allocators to keep track of allocated memory, doing very little else
-// TODO does not support get_new_handler/set_new_handler as we don't use it, but we could
-void *operator new(size_t size, std::align_val_t align_val) {
-  size_t align = static_cast<size_t>(align_val);
-  // standard says `size` must be an integer multiple of `align`
-  ASS_EQ(size % align, 0)
-
-  if(ALLOCATED + size > LIMIT)
-    throw std::bad_alloc();
-  ALLOCATED += size;
-  {
-    if(void *ptr = std::aligned_alloc(align, size))
-      return ptr;
-
-    // we might be here because `aligned_alloc` is finicky (Apple, looking at you)
-    // so try again with `malloc` and hope for good alignment
-    if(void *ptr = std::malloc(size))
-      return ptr;
-
-  }
-  // no, we're actually out of memory
-  throw std::bad_alloc();
-}
-
-// a version of the above operator-new without alignment information
-void *operator new(size_t size) {
-  if(ALLOCATED + size > LIMIT)
-    throw std::bad_alloc();
-  ALLOCATED += size;
-  {
-    if(void *ptr = std::malloc(size))
-      return ptr;
-  }
-  throw std::bad_alloc();
-}
-
-// normal delete, just decrements `ALLOCATED` and calls free()
-void operator delete(void *ptr, size_t size) noexcept {
-  ASS_GE(ALLOCATED, size)
-  ALLOCATED -= size;
-  std::free(ptr);
-}
-
-// aligned-and-sized delete
-// forwards to the sized delete as we don't use the alignment information
-void operator delete(void *ptr, size_t size, std::align_val_t align) noexcept {
-  operator delete(ptr, size);
-}
+#if __has_include(<sys/resource.h>)
+#include <sys/resource.h>
+#define HAVE_RLIMIT
+#endif
 
-// unsized (and unaligned) delete
-// called if we don't know the size of the deallocated object somehow,
-// occurs very rarely and usually from deep in the bowels of the standard library
-// TODO does cause us to slightly over-report allocated memory
-void operator delete(void *ptr) noexcept {
-  std::free(ptr);
+void Lib::setMemoryLimit(size_t limit) {
+#ifdef HAVE_RLIMIT
+  struct rlimit rlimit;
+  rlimit.rlim_cur = rlimit.rlim_max = limit;
+  ASS_EQ(setrlimit(RLIMIT_DATA, &rlimit), 0)
+#else
+  // TODO should we warn here?
+#endif
 }

Lib/Allocator.hpp

@@ -24,7 +24,6 @@
 #include <new>
 
 #include "Debug/Assertion.hpp"
-#include "Portability.hpp"
 
 /*
  * uncomment the following to use Valgrind more profitably
@@ -34,15 +33,8 @@
 // #define INDIVIDUAL_ALLOCATIONS
 
 namespace Lib {
-
-// get the amount of memory used by global operator new so far
-size_t getUsedMemory();
-
-// get the memory limit for global operator new
-size_t getMemoryLimit();
-// set the memory limit for global operator new
+// attempt to set a memory limit for this process by system call
 void setMemoryLimit(size_t bytes);
-
 }
 
 #ifdef INDIVIDUAL_ALLOCATIONS

Saturation/ProvingHelper.cpp

@@ -57,9 +57,6 @@ using namespace Shell;
   catch(const std::bad_alloc &) {
     env.statistics->terminationReason=Statistics::MEMORY_LIMIT;
     env.statistics->refutation=0;
-    size_t limit=Lib::getMemoryLimit();
-    //add extra 1 MB to allow proper termination
-    Lib::setMemoryLimit(limit+1000000);
   }
   catch(TimeLimitExceededException&) {
     env.statistics->terminationReason=Statistics::TIME_LIMIT;
@@ -107,9 +104,6 @@ void ProvingHelper::runVampire(Problem& prb, const Options& opt)
   catch(const std::bad_alloc &) {
     env.statistics->terminationReason=Statistics::MEMORY_LIMIT;
     env.statistics->refutation=0;
-    size_t limit=Lib::getMemoryLimit();
-    //add extra 1 MB to allow proper termination
-    Lib::setMemoryLimit(limit+1000000);
   }
   catch(TimeLimitExceededException&) {
     env.statistics->terminationReason=Statistics::TIME_LIMIT;

Shell/Statistics.cpp

@@ -18,7 +18,6 @@
 
 #include "Debug/RuntimeStatistics.hpp"
 
-#include "Lib/Allocator.hpp"
 #include "Lib/Environment.hpp"
 #include "Lib/Timer.hpp"
 #include "SAT/Z3Interfacing.hpp"
@@ -469,21 +468,19 @@ void Statistics::print(ostream& out)
 
   }
 
-  COND_OUT("Memory used [KB]", Lib::getUsedMemory()/1024);
-
   addCommentSignForSZS(out);
   out << "Time elapsed: ";
   Timer::printMSString(out,Timer::elapsedMilliseconds());
   out << endl;
-  
+
   Timer::updateInstructionCount();
   unsigned instr = Timer::elapsedMegaInstructions();
   if (instr) {
     addCommentSignForSZS(out);
     out << "Instructions burned: " << instr << " (million)";
     out << endl;
   }
-  
+
   addCommentSignForSZS(out);
   out << "------------------------------\n";
 

Shell/UIHelper.cpp

@@ -106,7 +106,6 @@ void reportSpiderStatus(char status)
     << (problemName.length() == 0 ? "unknown" : problemName) << " "
     << Timer::elapsedDeciseconds() << " "
     << Timer::elapsedMegaInstructions() << " "
-    << Lib::getUsedMemory()/1048576 << " "
     << (Lib::env.options ? Lib::env.options->testId() : "unknown") << " "
     << commitNumber << ':' << z3Version << endl;
 #endif