diff options
Diffstat (limited to 'lib/Solver/Solver.cpp')
| -rw-r--r-- | lib/Solver/Solver.cpp | 462 |
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(); |