diff options
Diffstat (limited to 'lib/Solver/MetaSMTSolver.cpp')
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 466 |
1 files changed, 466 insertions, 0 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 |