diff options
Diffstat (limited to 'lib/Solver')
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 466 | ||||
| -rw-r--r-- | lib/Solver/Solver.cpp | 462 |
2 files changed, 466 insertions, 462 deletions
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp new file mode 100644 index 00000000..8394bbf3 --- /dev/null +++ b/lib/Solver/MetaSMTSolver.cpp @@ -0,0 +1,466 @@ +//===-- MetaSMTSolver.cpp -------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifdef SUPPORT_METASMT + +#include "MetaSMTBuilder.h" +#include "klee/Constraints.h" +#include "klee/Solver.h" +#include "klee/SolverImpl.h" +#include "klee/util/Assignment.h" +#include "klee/util/ExprUtil.h" + +#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> + +#include <errno.h> +#include <unistd.h> +#include <signal.h> +#include <sys/wait.h> +#include <sys/ipc.h> +#include <sys/shm.h> + + +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 + +namespace klee { + +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); }; +}; + +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> >; + +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); +} +} +#endif // SUPPORT_METASMT 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(); |