STPSolver: C++11, add missing free, refactoring

1 files changed, 85 insertions, 97 deletions

diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp
index b058a9cb..e8b9222f 100644
--- a/lib/Solver/STPSolver.cpp
+++ b/lib/Solver/STPSolver.cpp
@@ -7,27 +7,25 @@
 //
 //===----------------------------------------------------------------------===//
 #include "klee/Config/config.h"
+
 #ifdef ENABLE_STP
-#include "STPSolver.h"
 #include "STPBuilder.h"
-#include "klee/Solver.h"
-#include "klee/SolverImpl.h"
+#include "STPSolver.h"
 #include "klee/Constraints.h"
-#include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/OptionCategories.h"
+#include "klee/SolverImpl.h"
+#include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/util/Assignment.h"
 #include "klee/util/ExprUtil.h"
 
 #include "llvm/Support/CommandLine.h"
 #include "llvm/Support/Errno.h"
-#include "llvm/Support/ErrorHandling.h"
 
-#include <errno.h>
+#include <csignal>
 #include <unistd.h>
-#include <signal.h>
-#include <sys/wait.h>
 #include <sys/ipc.h>
 #include <sys/shm.h>
+#include <sys/wait.h>
 
 namespace {
 
@@ -44,7 +42,7 @@ llvm::cl::opt<bool> IgnoreSolverFailures(
 
 #define vc_bvBoolExtract IAMTHESPAWNOFSATAN
 
-static unsigned char *shared_memory_ptr;
+static unsigned char *shared_memory_ptr = nullptr;
 static int shared_memory_id = 0;
 // Darwin by default has a very small limit on the maximum amount of shared
 // memory, which will quickly be exhausted by KLEE running its tests in
@@ -73,25 +71,25 @@ private:
   SolverRunStatus runStatusCode;
 
 public:
-  STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides = true);
-  ~STPSolverImpl();
+  explicit STPSolverImpl(bool useForkedSTP, bool optimizeDivides = true);
+  ~STPSolverImpl() override;
 
-  char *getConstraintLog(const Query &);
-  void setCoreSolverTimeout(time::Span timeout) { this->timeout = timeout; }
+  char *getConstraintLog(const Query &) override;
+  void setCoreSolverTimeout(time::Span timeout) override { this->timeout = timeout; }
 
-  bool computeTruth(const Query &, bool &isValid);
-  bool computeValue(const Query &, ref<Expr> &result);
+  bool computeTruth(const Query &, bool &isValid) override;
+  bool computeValue(const Query &, ref<Expr> &result) override;
   bool computeInitialValues(const Query &,
                             const std::vector<const Array *> &objects,
-                            std::vector<std::vector<unsigned char> > &values,
-                            bool &hasSolution);
-  SolverRunStatus getOperationStatusCode();
+                            std::vector<std::vector<unsigned char>> &values,
+                            bool &hasSolution) override;
+  SolverRunStatus getOperationStatusCode() override;
 };
 
-STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides)
+STPSolverImpl::STPSolverImpl(bool useForkedSTP, bool optimizeDivides)
     : vc(vc_createValidityChecker()),
-      builder(new STPBuilder(vc, _optimizeDivides)),
-      useForkedSTP(_useForkedSTP), runStatusCode(SOLVER_RUN_STATUS_FAILURE) {
+      builder(new STPBuilder(vc, optimizeDivides)),
+      useForkedSTP(useForkedSTP), runStatusCode(SOLVER_RUN_STATUS_FAILURE) {
   assert(vc && "unable to create validity checker");
   assert(builder && "unable to create STPBuilder");
 
@@ -113,17 +111,17 @@ STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides)
         shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700);
     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);
+    shared_memory_ptr = (unsigned char *)shmat(shared_memory_id, nullptr, 0);
     if (shared_memory_ptr == (void *)-1)
       llvm::report_fatal_error("unable to attach shared memory region");
-    shmctl(shared_memory_id, IPC_RMID, NULL);
+    shmctl(shared_memory_id, IPC_RMID, nullptr);
   }
 }
 
 STPSolverImpl::~STPSolverImpl() {
   // Detach the memory region.
   shmdt(shared_memory_ptr);
-  shared_memory_ptr = 0;
+  shared_memory_ptr = nullptr;
   shared_memory_id = 0;
 
   delete builder;
@@ -135,10 +133,9 @@ STPSolverImpl::~STPSolverImpl() {
 
 char *STPSolverImpl::getConstraintLog(const Query &query) {
   vc_push(vc);
-  for (std::vector<ref<Expr> >::const_iterator it = query.constraints.begin(),
-                                               ie = query.constraints.end();
-       it != ie; ++it)
-    vc_assertFormula(vc, builder->construct(*it));
+
+  for (const auto &constraint : query.constraints)
+    vc_assertFormula(vc, builder->construct(constraint));
   assert(query.expr == ConstantExpr::alloc(0, Expr::Bool) &&
          "Unexpected expression in query!");
 
@@ -152,7 +149,7 @@ char *STPSolverImpl::getConstraintLog(const Query &query) {
 
 bool STPSolverImpl::computeTruth(const Query &query, bool &isValid) {
   std::vector<const Array *> objects;
-  std::vector<std::vector<unsigned char> > values;
+  std::vector<std::vector<unsigned char>> values;
   bool hasSolution;
 
   if (!computeInitialValues(query, objects, values, hasSolution))
@@ -164,7 +161,7 @@ bool STPSolverImpl::computeTruth(const Query &query, bool &isValid) {
 
 bool STPSolverImpl::computeValue(const Query &query, ref<Expr> &result) {
   std::vector<const Array *> objects;
-  std::vector<std::vector<unsigned char> > values;
+  std::vector<std::vector<unsigned char>> values;
   bool hasSolution;
 
   // Find the object used in the expression, and compute an assignment
@@ -184,36 +181,28 @@ bool STPSolverImpl::computeValue(const Query &query, ref<Expr> &result) {
 static SolverImpl::SolverRunStatus
 runAndGetCex(::VC vc, STPBuilder *builder, ::VCExpr q,
              const std::vector<const Array *> &objects,
-             std::vector<std::vector<unsigned char> > &values,
+             std::vector<std::vector<unsigned char>> &values,
              bool &hasSolution) {
   // XXX I want to be able to timeout here, safely
   hasSolution = !vc_query(vc, q);
 
-  if (hasSolution) {
-    values.reserve(objects.size());
-    for (std::vector<const Array *>::const_iterator it = objects.begin(),
-                                                    ie = objects.end();
-         it != ie; ++it) {
-      const Array *array = *it;
-      std::vector<unsigned char> data;
-
-      data.reserve(array->size);
-      for (unsigned offset = 0; offset < array->size; offset++) {
-        ExprHandle counter =
-            vc_getCounterExample(vc, builder->getInitialRead(array, offset));
-        unsigned char val = getBVUnsigned(counter);
-        data.push_back(val);
-      }
+  if (!hasSolution)
+    return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;
+
+  values.reserve(objects.size());
+  unsigned i = 0; // FIXME C++17: use reference from emplace_back()
+  for (const auto object : objects) {
+    values.emplace_back(object->size);
 
-      values.push_back(data);
+    for (unsigned offset = 0; offset < object->size; offset++) {
+      ExprHandle counter =
+          vc_getCounterExample(vc, builder->getInitialRead(object, offset));
+      values[i][offset] = static_cast<unsigned char>(getBVUnsigned(counter));
     }
+    ++i;
   }
 
-  if (true == hasSolution) {
-    return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
-  } else {
-    return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;
-  }
+  return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
 }
 
 static void stpTimeoutHandler(int x) { _exit(52); }
@@ -221,47 +210,46 @@ static void stpTimeoutHandler(int x) { _exit(52); }
 static SolverImpl::SolverRunStatus
 runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q,
                    const std::vector<const Array *> &objects,
-                   std::vector<std::vector<unsigned char> > &values,
+                   std::vector<std::vector<unsigned char>> &values,
                    bool &hasSolution, time::Span timeout) {
   unsigned char *pos = shared_memory_ptr;
   unsigned sum = 0;
-  for (std::vector<const Array *>::const_iterator it = objects.begin(),
-                                                  ie = objects.end();
-       it != ie; ++it)
-    sum += (*it)->size;
+  for (const auto object : objects)
+    sum += object->size;
   if (sum >= shared_memory_size)
     llvm::report_fatal_error("not enough shared memory for counterexample");
 
   fflush(stdout);
   fflush(stderr);
+
+  // fork solver
   int pid = fork();
+  // - error
   if (pid == -1) {
     klee_warning("fork failed (for STP) - %s", llvm::sys::StrError(errno).c_str());
     if (!IgnoreSolverFailures)
       exit(1);
     return SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED;
   }
-
+  // - child (solver)
   if (pid == 0) {
     if (timeout) {
       ::alarm(0); /* Turn off alarm so we can safely set signal handler */
       ::signal(SIGALRM, stpTimeoutHandler);
       ::alarm(std::max(1u, static_cast<unsigned>(timeout.toSeconds())));
     }
-    unsigned res = vc_query(vc, q);
+    int res = vc_query(vc, q);
     if (!res) {
-      for (std::vector<const Array *>::const_iterator it = objects.begin(),
-                                                      ie = objects.end();
-           it != ie; ++it) {
-        const Array *array = *it;
-        for (unsigned offset = 0; offset < array->size; offset++) {
+      for (const auto object : objects) {
+        for (unsigned offset = 0; offset < object->size; offset++) {
           ExprHandle counter =
-              vc_getCounterExample(vc, builder->getInitialRead(array, offset));
-          *pos++ = getBVUnsigned(counter);
+              vc_getCounterExample(vc, builder->getInitialRead(object, offset));
+          *pos++ = static_cast<unsigned char>(getBVUnsigned(counter));
         }
       }
     }
     _exit(res);
+  // - parent
   } else {
     int status;
     pid_t res;
@@ -290,53 +278,51 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q,
     }
 
     int exitcode = WEXITSTATUS(status);
+
+    // solvable
     if (exitcode == 0) {
       hasSolution = true;
-    } else if (exitcode == 1) {
-      hasSolution = false;
-    } else if (exitcode == 52) {
-      klee_warning("STP timed out");
-      // mark that a timeout occurred
-      return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT;
-    } else {
-      klee_warning("STP did not return a recognized code");
-      if (!IgnoreSolverFailures)
-        exit(1);
-      return SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE;
-    }
 
-    if (hasSolution) {
-      values = std::vector<std::vector<unsigned char> >(objects.size());
-      unsigned i = 0;
-      for (std::vector<const Array *>::const_iterator it = objects.begin(),
-                                                      ie = objects.end();
-           it != ie; ++it) {
-        const Array *array = *it;
-        std::vector<unsigned char> &data = values[i++];
-        data.insert(data.begin(), pos, pos + array->size);
-        pos += array->size;
+      values.reserve(objects.size());
+      for (const auto object : objects) {
+        values.emplace_back(pos, pos + object->size);
+        pos += object->size;
       }
-    }
 
-    if (true == hasSolution) {
       return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
-    } else {
+    }
+
+    // unsolvable
+    if (exitcode == 1) {
+      hasSolution = false;
       return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;
     }
+
+    // timeout
+    if (exitcode == 52) {
+      klee_warning("STP timed out");
+      // mark that a timeout occurred
+      return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT;
+    }
+
+    // unknown return code
+    klee_warning("STP did not return a recognized code");
+    if (!IgnoreSolverFailures)
+      exit(1);
+    return SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE;
   }
 }
+
 bool STPSolverImpl::computeInitialValues(
     const Query &query, const std::vector<const Array *> &objects,
-    std::vector<std::vector<unsigned char> > &values, bool &hasSolution) {
+    std::vector<std::vector<unsigned char>> &values, bool &hasSolution) {
   runStatusCode = SOLVER_RUN_STATUS_FAILURE;
   TimerStatIncrementer t(stats::queryTime);
 
   vc_push(vc);
 
-  for (ConstraintManager::const_iterator it = query.constraints.begin(),
-                                         ie = query.constraints.end();
-       it != ie; ++it)
-    vc_assertFormula(vc, builder->construct(*it));
+  for (const auto &constraint : query.constraints)
+    vc_assertFormula(vc, builder->construct(constraint));
 
   ++stats::queries;
   ++stats::queryCounterexamples;
@@ -348,6 +334,7 @@ bool STPSolverImpl::computeInitialValues(
     unsigned long len;
     vc_printQueryStateToBuffer(vc, stp_e, &buf, &len, false);
     klee_warning("STP query:\n%.*s\n", (unsigned)len, buf);
+    free(buf);
   }
 
   bool success;
@@ -388,5 +375,6 @@ char *STPSolver::getConstraintLog(const Query &query) {
 void STPSolver::setCoreSolverTimeout(time::Span timeout) {
   impl->setCoreSolverTimeout(timeout);
 }
-}
+
+} // klee
 #endif // ENABLE_STP