about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
authorDaniel Dunbar <daniel@zuster.org>2014-09-13 18:22:45 -0700
committerDaniel Dunbar <daniel@zuster.org>2014-09-13 18:22:45 -0700
commit35723ae8eec286d357e6def1c2adec3638b4af2d (patch)
treef3adca8ee335176c8dd86ff03cd2a934d4f0e2d2 /lib/Solver
parentf11c0b1039bcadf5420e1d9139200ef1ea93e37a (diff)
downloadklee-35723ae8eec286d357e6def1c2adec3638b4af2d.tar.gz
[Solver] Ensure shared memory allocation failures are reported as errors, not asserts.
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/Solver.cpp18
1 files changed, 14 insertions, 4 deletions
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 229fa234..d4e572cf 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -38,6 +38,7 @@
 #include <sys/shm.h>
 
 #include "llvm/Support/CommandLine.h"
+#include "llvm/Support/ErrorHandling.h"
 
 llvm::cl::opt<bool>
 IgnoreSolverFailures("ignore-solver-failures",
@@ -518,7 +519,7 @@ public:
 
 static unsigned char *shared_memory_ptr;
 static const unsigned shared_memory_size = 1<<20;
-static int shared_memory_id;
+static int shared_memory_id = 0;
 
 static void stp_error_handler(const char* err_msg) {
   fprintf(stderr, "error: STP Error: %s\n", err_msg);
@@ -546,15 +547,23 @@ STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides)
   vc_registerErrorHandler(::stp_error_handler);
 
   if (useForkedSTP) {
+    assert(shared_memory_id == 0 && "shared memory id already allocated");
     shared_memory_id = shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700);
-    assert(shared_memory_id>=0 && "shmget failed");
+    if (shared_memory_id < 0)
+      llvm::report_fatal_error("unable to allocate shared memory region");
     shared_memory_ptr = (unsigned char*) shmat(shared_memory_id, NULL, 0);
-    assert(shared_memory_ptr!=(void*)-1 && "shmat failed");
+    if (shared_memory_ptr == (void*)-1)
+      llvm::report_fatal_error("unable to attach shared memory region");
     shmctl(shared_memory_id, IPC_RMID, NULL);
   }
 }
 
 STPSolverImpl::~STPSolverImpl() {
+  // Detach the memory region.
+  shmdt(shared_memory_ptr);
+  shared_memory_ptr = 0;
+  shared_memory_id = 0;
+
   delete builder;
 
   vc_Destroy(vc);
@@ -678,7 +687,8 @@ static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc,
   for (std::vector<const Array*>::const_iterator
          it = objects.begin(), ie = objects.end(); it != ie; ++it)
     sum += (*it)->size;
-  assert(sum<shared_memory_size && "not enough shared memory for counterexample");
+  if (sum >= shared_memory_size)
+    llvm::report_fatal_error("not enough shared memory for counterexample");
 
   fflush(stdout);
   fflush(stderr);