Refactor MetaSMTSolver and MetaSMTSolverImpl out of Solver.cpp into

their own file ``MetaSMTSolver.cpp``. Whilst I'm here also clang-format
the modified code.

This might not be a NFC (non functional change) as there's a good chance this
has broken the MetaSMT build of KLEE. I don't have a build of MetaSMT to hand
and there is no TravisCI build.  At this point because there is no maintainer
for this code I think we should consider removing it as it is going bitrot.

1 files changed, 0 insertions, 462 deletions

diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index a391ada4..bb4bef69 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -10,7 +10,6 @@
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
 
-#include "MetaSMTBuilder.h"
 
 #include "klee/Constraints.h"
 #include "klee/Expr.h"
@@ -29,34 +28,11 @@
 #include <map>
 #include <vector>
 
-#include <errno.h>
-#include <unistd.h>
-#include <signal.h>
-#include <sys/wait.h>
-#include <sys/ipc.h>
-#include <sys/shm.h>
-
 #include "llvm/Support/ErrorHandling.h"
 
 
 using namespace klee;
 
-
-#ifdef SUPPORT_METASMT
-
-#include <metaSMT/DirectSolver_Context.hpp>
-#include <metaSMT/backend/Z3_Backend.hpp>
-#include <metaSMT/backend/Boolector.hpp>
-#include <metaSMT/backend/MiniSAT.hpp>
-#include <metaSMT/support/run_algorithm.hpp>
-#include <metaSMT/API/Stack.hpp>
-#include <metaSMT/API/Group.hpp>
-
-using namespace metaSMT;
-using namespace metaSMT::solver;
-
-#endif /* SUPPORT_METASMT */
-
 const char *Solver::validity_to_str(Validity v) {
   switch (v) {
   default:    return "Unknown";
@@ -264,444 +240,6 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
                         ConstantExpr::create(max, width));
 }
 
-/***/
-
-#ifdef SUPPORT_METASMT
-
-static unsigned char *shared_memory_ptr;
-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
-// parallel. For now, we work around this by just requesting a smaller size --
-// in practice users hitting this limit on counterexample sizes probably already
-// are hitting more serious scalability issues.
-#ifdef __APPLE__
-static const unsigned shared_memory_size = 1<<16;
-#else
-static const unsigned shared_memory_size = 1<<20;
-#endif
-
-// ------------------------------------- MetaSMTSolverImpl class declaration ------------------------------
-
-template<typename SolverContext>
-class MetaSMTSolverImpl : public SolverImpl {
-private:
-
-  SolverContext _meta_solver;
-  MetaSMTSolver<SolverContext>  *_solver;  
-  MetaSMTBuilder<SolverContext> *_builder;
-  double _timeout;
-  bool   _useForked;
-  SolverRunStatus _runStatusCode;
-
-public:
-  MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides);  
-  virtual ~MetaSMTSolverImpl();
-  
-  char *getConstraintLog(const Query&);
-  void setCoreSolverTimeout(double timeout) { _timeout = timeout; }
-
-  bool computeTruth(const Query&, bool &isValid);
-  bool computeValue(const Query&, ref<Expr> &result);
-    
-  bool computeInitialValues(const Query &query,
-                            const std::vector<const Array*> &objects,
-                            std::vector< std::vector<unsigned char> > &values,
-                            bool &hasSolution);
-    
-  SolverImpl::SolverRunStatus runAndGetCex(ref<Expr> query_expr,
-                                           const std::vector<const Array*> &objects,
-                                           std::vector< std::vector<unsigned char> > &values,
-                                           bool &hasSolution);
-  
-  SolverImpl::SolverRunStatus runAndGetCexForked(const Query &query,
-                                                 const std::vector<const Array*> &objects,
-                                                 std::vector< std::vector<unsigned char> > &values,
-                                                 bool &hasSolution,
-                                                 double timeout);
-  
-  SolverRunStatus getOperationStatusCode();
-  
-  SolverContext& get_meta_solver() { return(_meta_solver); };
-  
-};
-
-
-// ------------------------------------- MetaSMTSolver methods --------------------------------------------
-
-
-template<typename SolverContext>
-MetaSMTSolver<SolverContext>::MetaSMTSolver(bool useForked, bool optimizeDivides) 
-  : Solver(new MetaSMTSolverImpl<SolverContext>(this, useForked, optimizeDivides))
-{
-   
-}
-
-template<typename SolverContext>
-MetaSMTSolver<SolverContext>::~MetaSMTSolver()
-{
-  
-}
-
-template<typename SolverContext>
-char *MetaSMTSolver<SolverContext>::getConstraintLog(const Query& query) {
-  return(impl->getConstraintLog(query));
-}
-
-template<typename SolverContext>
-void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) {
-  impl->setCoreSolverTimeout(timeout);
-}
-
-
-// ------------------------------------- MetaSMTSolverImpl methods ----------------------------------------
-
-
-
-template<typename SolverContext>
-MetaSMTSolverImpl<SolverContext>::MetaSMTSolverImpl(MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides)
-  : _solver(solver),    
-    _builder(new MetaSMTBuilder<SolverContext>(_meta_solver, optimizeDivides)),
-    _timeout(0.0),
-    _useForked(useForked)
-{  
-  assert(_solver && "unable to create MetaSMTSolver");
-  assert(_builder && "unable to create MetaSMTBuilder");
-  
-  if (_useForked) {
-      shared_memory_id = shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700);
-      assert(shared_memory_id >= 0 && "shmget failed");
-      shared_memory_ptr = (unsigned char*) shmat(shared_memory_id, NULL, 0);
-      assert(shared_memory_ptr != (void*) -1 && "shmat failed");
-      shmctl(shared_memory_id, IPC_RMID, NULL);
-  }
-}
-
-template<typename SolverContext>
-MetaSMTSolverImpl<SolverContext>::~MetaSMTSolverImpl() {
-
-}
-
-template<typename SolverContext>
-char *MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query&) {
-  const char* msg = "Not supported";
-  char *buf = new char[strlen(msg) + 1];
-  strcpy(buf, msg);
-  return(buf);
-}
-
-template<typename SolverContext>
-bool MetaSMTSolverImpl<SolverContext>::computeTruth(const Query& query, bool &isValid) {  
-
-  bool success = false;
-  std::vector<const Array*> objects;
-  std::vector< std::vector<unsigned char> > values;
-  bool hasSolution;
-
-  if (computeInitialValues(query, objects, values, hasSolution)) {
-      // query.expr is valid iff !query.expr is not satisfiable
-      isValid = !hasSolution;
-      success = true;
-  }
-
-  return(success);
-}
-
-template<typename SolverContext>
-bool MetaSMTSolverImpl<SolverContext>::computeValue(const Query& query, ref<Expr> &result) {
-  
-  bool success = false;
-  std::vector<const Array*> objects;
-  std::vector< std::vector<unsigned char> > values;
-  bool hasSolution;
-
-  // Find the object used in the expression, and compute an assignment for them.
-  findSymbolicObjects(query.expr, objects);  
-  if (computeInitialValues(query.withFalse(), objects, values, hasSolution)) {  
-      assert(hasSolution && "state has invalid constraint set");
-      // Evaluate the expression with the computed assignment.
-      Assignment a(objects, values);
-      result = a.evaluate(query.expr);
-      success = true;
-  }
-
-  return(success);
-}
-
-
-template<typename SolverContext>
-bool MetaSMTSolverImpl<SolverContext>::computeInitialValues(const Query &query,
-                                             const std::vector<const Array*> &objects,
-                                             std::vector< std::vector<unsigned char> > &values,
-                                             bool &hasSolution) {  
-
-  _runStatusCode =  SOLVER_RUN_STATUS_FAILURE;
-
-  TimerStatIncrementer t(stats::queryTime);
-  assert(_builder);
-
-  /*
-   * FIXME push() and pop() work for Z3 but not for Boolector.
-   * If using Z3, use push() and pop() and assert constraints.
-   * If using Boolector, assume constrainsts instead of asserting them.
-   */
-  //push(_meta_solver);
-
-  if (!_useForked) {
-      for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) {
-          //assertion(_meta_solver, _builder->construct(*it));
-          assumption(_meta_solver, _builder->construct(*it));  
-      }  
-  }  
-    
-  ++stats::queries;
-  ++stats::queryCounterexamples;  
- 
-  bool success = true;
-  if (_useForked) {
-      _runStatusCode = runAndGetCexForked(query, objects, values, hasSolution, _timeout);
-      success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == _runStatusCode) || (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == _runStatusCode));
-  }
-  else {
-      _runStatusCode = runAndGetCex(query.expr, objects, values, hasSolution);
-      success = true;
-  } 
-    
-  if (success) {
-      if (hasSolution) {
-          ++stats::queriesInvalid;
-      }
-      else {
-          ++stats::queriesValid;
-      }
-  }  
-   
-  //pop(_meta_solver); 
-  
-  return(success);
-}
-
-template<typename SolverContext>
-SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCex(ref<Expr> query_expr,
-                                             const std::vector<const Array*> &objects,
-                                             std::vector< std::vector<unsigned char> > &values,
-                                             bool &hasSolution)
-{
-
-  // assume the negation of the query  
-  assumption(_meta_solver, _builder->construct(Expr::createIsZero(query_expr)));  
-  hasSolution = solve(_meta_solver);  
-  
-  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;
-          assert(array);
-          typename SolverContext::result_type array_exp = _builder->getInitialArray(array);
-           
-          std::vector<unsigned char> data;      
-          data.reserve(array->size);       
-           
-          for (unsigned offset = 0; offset < array->size; offset++) {
-              typename SolverContext::result_type elem_exp = evaluate(
-                       _meta_solver,
-                       metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain())));
-              unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp);
-              data.push_back(elem_value);
-          }
-                   
-          values.push_back(data);
-      }
-  }
-  
-  if (true == hasSolution) {
-      return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE);
-  }
-  else {
-      return(SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE);  
-  }
-}
-
-static void metaSMTTimeoutHandler(int x) {
-  _exit(52);
-}
-
-template<typename SolverContext>
-SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCexForked(const Query &query,
-                                                          const std::vector<const Array*> &objects,
-                                                          std::vector< std::vector<unsigned char> > &values,
-                                                          bool &hasSolution,
-                                                          double 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;    
-  }
-  // sum += sizeof(uint64_t);
-  sum += sizeof(stats::queryConstructs);
-  assert(sum < shared_memory_size && "not enough shared memory for counterexample");
-
-  fflush(stdout);
-  fflush(stderr);
-  int pid = fork();
-  if (pid == -1) {
-      fprintf(stderr, "error: fork failed (for metaSMT)");
-      return(SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED);
-  }
-  
-  if (pid == 0) {
-      if (timeout) {
-          ::alarm(0); /* Turn off alarm so we can safely set signal handler */
-          ::signal(SIGALRM, metaSMTTimeoutHandler);
-          ::alarm(std::max(1, (int) timeout));
-      }     
-      
-      for (ConstraintManager::const_iterator it = query.constraints.begin(), ie = query.constraints.end(); it != ie; ++it) {      
-          assertion(_meta_solver, _builder->construct(*it));
-          //assumption(_meta_solver, _builder->construct(*it));  
-      } 
-      
-      
-      std::vector< std::vector<typename SolverContext::result_type> > aux_arr_exprs;
-      if (UseMetaSMT == METASMT_BACKEND_BOOLECTOR) {
-          for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
-            
-              std::vector<typename SolverContext::result_type> aux_arr;          
-              const Array *array = *it;
-              assert(array);
-              typename SolverContext::result_type array_exp = _builder->getInitialArray(array);
-              
-              for (unsigned offset = 0; offset < array->size; offset++) {
-                  typename SolverContext::result_type elem_exp = evaluate(
-                      _meta_solver,
-                      metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain())));
-                  aux_arr.push_back(elem_exp);
-              }
-              aux_arr_exprs.push_back(aux_arr);
-          }
-          assert(aux_arr_exprs.size() == objects.size());
-      }
-      
-           
-      // assume the negation of the query
-      // can be also asserted instead of assumed as we are in a child process
-      assumption(_meta_solver, _builder->construct(Expr::createIsZero(query.expr)));        
-      unsigned res = solve(_meta_solver);
-
-      if (res) {
-
-          if (UseMetaSMT != METASMT_BACKEND_BOOLECTOR) {
-
-              for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) {
-
-                  const Array *array = *it;
-                  assert(array);
-                  typename SolverContext::result_type array_exp = _builder->getInitialArray(array);      
-
-                  for (unsigned offset = 0; offset < array->size; offset++) {
-
-                      typename SolverContext::result_type elem_exp = evaluate(
-                          _meta_solver,
-                          metaSMT::logic::Array::select(array_exp, bvuint(offset, array->getDomain())));
-                      unsigned char elem_value = metaSMT::read_value(_meta_solver, elem_exp);
-                      *pos++ = elem_value;
-                  }
-              }
-          }
-          else {
-              typename std::vector< std::vector<typename SolverContext::result_type> >::const_iterator eit = aux_arr_exprs.begin(), eie = aux_arr_exprs.end();
-              for (std::vector<const Array*>::const_iterator it = objects.begin(), ie = objects.end(); it != ie, eit != eie; ++it, ++eit) {
-                  const Array *array = *it;
-                  const std::vector<typename SolverContext::result_type>& arr_exp = *eit;
-                  assert(array);
-                  assert(array->size == arr_exp.size());
-
-                  for (unsigned offset = 0; offset < array->size; offset++) {
-                      unsigned char elem_value = metaSMT::read_value(_meta_solver, arr_exp[offset]);
-                       *pos++ = elem_value;
-                  }
-              }
-          }
-      }
-      assert((uint64_t*) pos);
-      *((uint64_t*) pos) = stats::queryConstructs;      
-      
-      _exit(!res);
-  }
-  else {
-      int status;
-      pid_t res;
-
-      do {
-          res = waitpid(pid, &status, 0);
-      } 
-      while (res < 0 && errno == EINTR);
-    
-      if (res < 0) {
-          fprintf(stderr, "error: waitpid() for metaSMT failed");
-          return(SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED);
-      }
-      
-      // From timed_run.py: It appears that linux at least will on
-      // "occasion" return a status when the process was terminated by a
-      // signal, so test signal first.
-      if (WIFSIGNALED(status) || !WIFEXITED(status)) {
-           fprintf(stderr, "error: metaSMT did not return successfully (status = %d) \n", WTERMSIG(status));
-           return(SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED);
-      }
-
-      int exitcode = WEXITSTATUS(status);
-      if (exitcode == 0) {
-          hasSolution = true;
-      } 
-      else if (exitcode == 1) {
-          hasSolution = false;
-      }
-      else if (exitcode == 52) {
-          fprintf(stderr, "error: metaSMT timed out");
-          return(SolverImpl::SOLVER_RUN_STATUS_TIMEOUT);
-      }
-      else {
-          fprintf(stderr, "error: metaSMT did not return a recognized code");
-          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;
-              assert(array);
-              std::vector<unsigned char> &data = values[i++];
-              data.insert(data.begin(), pos, pos + array->size);
-              pos += array->size;
-          }
-      }
-      stats::queryConstructs += (*((uint64_t*) pos) - stats::queryConstructs);      
-
-      if (true == hasSolution) {
-          return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE;
-      }
-      else {
-          return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE;
-      }
-  }
-}
-
-template<typename SolverContext>
-SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::getOperationStatusCode() {
-   return _runStatusCode;
-}
-
-template class MetaSMTSolver< DirectSolver_Context < Boolector> >;
-template class MetaSMTSolver< DirectSolver_Context < Z3_Backend> >;
-template class MetaSMTSolver< DirectSolver_Context < STP_Backend> >;
-
-#endif /* SUPPORT_METASMT */
-///
-
 void Query::dump() const {
   llvm::errs() << "Constraints [\n";
   for (ConstraintManager::const_iterator i = constraints.begin();