From 64868646eed7384c38db41aff5002215b92c1601 Mon Sep 17 00:00:00 2001 From: Hristina Palikareva Date: Fri, 4 Oct 2013 18:32:55 +0100 Subject: MetaSMT builder, solver and command-line options. --- lib/Solver/Solver.cpp | 440 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 440 insertions(+) (limited to 'lib/Solver/Solver.cpp') diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 3414cda2..4df691f2 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -12,6 +12,7 @@ #include "SolverStats.h" #include "STPBuilder.h" +#include "MetaSMTBuilder.h" #include "klee/Constraints.h" #include "klee/Expr.h" @@ -20,6 +21,7 @@ #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprUtil.h" #include "klee/Internal/Support/Timer.h" +#include "klee/CommandLine.h" #define vc_bvBoolExtract IAMTHESPAWNOFSATAN @@ -45,6 +47,24 @@ IgnoreSolverFailures("ignore-solver-failures", using namespace klee; + +#ifdef SUPPORT_METASMT + +#include +#include +#include +#include +#include +#include +#include + +using namespace metaSMT; +using namespace metaSMT::solver; + +#endif /* SUPPORT_METASMT */ + + + /***/ SolverImpl::~SolverImpl() { @@ -809,3 +829,423 @@ STPSolverImpl::computeInitialValues(const Query &query, SolverImpl::SolverRunStatus STPSolverImpl::getOperationStatusCode() { return runStatusCode; } + +#ifdef SUPPORT_METASMT + +// ------------------------------------- MetaSMTSolverImpl class declaration ------------------------------ + +template +class MetaSMTSolverImpl : public SolverImpl { +private: + + SolverContext _meta_solver; + MetaSMTSolver *_solver; + MetaSMTBuilder *_builder; + double _timeout; + bool _useForked; + SolverRunStatus _runStatusCode; + +public: + MetaSMTSolverImpl(MetaSMTSolver *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 &result); + + bool computeInitialValues(const Query &query, + const std::vector &objects, + std::vector< std::vector > &values, + bool &hasSolution); + + SolverImpl::SolverRunStatus runAndGetCex(ref query_expr, + const std::vector &objects, + std::vector< std::vector > &values, + bool &hasSolution); + + SolverImpl::SolverRunStatus runAndGetCexForked(const Query &query, + const std::vector &objects, + std::vector< std::vector > &values, + bool &hasSolution, + double timeout); + + SolverRunStatus getOperationStatusCode(); + + SolverContext& get_meta_solver() { return(_meta_solver); }; + +}; + + +// ------------------------------------- MetaSMTSolver methods -------------------------------------------- + + +template +MetaSMTSolver::MetaSMTSolver(bool useForked, bool optimizeDivides) + : Solver(new MetaSMTSolverImpl(this, useForked, optimizeDivides)) +{ + +} + +template +MetaSMTSolver::~MetaSMTSolver() +{ + +} + +template +char *MetaSMTSolver::getConstraintLog(const Query& query) { + return(impl->getConstraintLog(query)); +} + +template +void MetaSMTSolver::setCoreSolverTimeout(double timeout) { + impl->setCoreSolverTimeout(timeout); +} + + +// ------------------------------------- MetaSMTSolverImpl methods ---------------------------------------- + + + +template +MetaSMTSolverImpl::MetaSMTSolverImpl(MetaSMTSolver *solver, bool useForked, bool optimizeDivides) + : _solver(solver), + _builder(new MetaSMTBuilder(_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 +MetaSMTSolverImpl::~MetaSMTSolverImpl() { + +} + +template +char *MetaSMTSolverImpl::getConstraintLog(const Query&) { + // ToDo +} + +template +bool MetaSMTSolverImpl::computeTruth(const Query& query, bool &isValid) { + + bool success = false; + std::vector objects; + std::vector< std::vector > 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 +bool MetaSMTSolverImpl::computeValue(const Query& query, ref &result) { + + bool success = false; + std::vector objects; + std::vector< std::vector > 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 +bool MetaSMTSolverImpl::computeInitialValues(const Query &query, + const std::vector &objects, + std::vector< std::vector > &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 +SolverImpl::SolverRunStatus MetaSMTSolverImpl::runAndGetCex(ref query_expr, + const std::vector &objects, + std::vector< std::vector > &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_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 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 +SolverImpl::SolverRunStatus MetaSMTSolverImpl::runAndGetCexForked(const Query &query, + const std::vector &objects, + std::vector< std::vector > &values, + bool &hasSolution, + double timeout) +{ + unsigned char *pos = shared_memory_ptr; + unsigned sum = 0; + for (std::vector::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 > aux_arr_exprs; + if (UseMetaSMT == METASMT_BACKEND_BOOLECTOR) { + for (std::vector::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + + std::vector 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_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 >::const_iterator eit = aux_arr_exprs.begin(), eie = aux_arr_exprs.end(); + for (std::vector::const_iterator it = objects.begin(), ie = objects.end(); it != ie, eit != eie; ++it, ++eit) { + const Array *array = *it; + const std::vector& 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 >(objects.size()); + unsigned i = 0; + for (std::vector::const_iterator it = objects.begin(), ie = objects.end(); it != ie; ++it) { + const Array *array = *it; + assert(array); + std::vector &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 +SolverImpl::SolverRunStatus MetaSMTSolverImpl::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 */ + -- cgit 1.4.1 From f53b2ebc74acd9d31b54f21434e1b21eed7f5787 Mon Sep 17 00:00:00 2001 From: Hristina Palikareva Date: Thu, 10 Oct 2013 12:23:20 +0100 Subject: getConstraintLog() of MetaSMTSolver explicitly states that this feature is not supported; a test case modified to not fail because of this. --- lib/Solver/Solver.cpp | 5 ++++- test/Feature/ExprLogging.c | 3 ++- 2 files changed, 6 insertions(+), 2 deletions(-) (limited to 'lib/Solver/Solver.cpp') diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 4df691f2..22b1545f 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -935,7 +935,10 @@ MetaSMTSolverImpl::~MetaSMTSolverImpl() { template char *MetaSMTSolverImpl::getConstraintLog(const Query&) { - // ToDo + const char* msg = "Not supported"; + char *buf = new char[strlen(msg) + 1]; + strcpy(buf, msg); + return(buf); } template diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c index ad671a5e..73623af0 100644 --- a/test/Feature/ExprLogging.c +++ b/test/Feature/ExprLogging.c @@ -1,5 +1,6 @@ // RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc -// RUN: %klee --use-query-log=all:pc,all:smt2,solver:pc,solver:smt2 --write-pcs --write-cvcs --write-smt2s %t1.bc 2> %t2.log +// RUN: %klee --use-query-log=all:pc,all:smt2,solver:pc,solver:smt2 --use-metasmt=none --write-pcs --write-cvcs --write-smt2s %t1.bc 2> %t2.log +// RUN: %klee --use-query-log=all:pc,all:smt2,solver:pc,solver:smt2 --write-pcs --write-smt2s %t1.bc 2> %t2.log // RUN: %kleaver -print-ast klee-last/all-queries.pc > %t3.log // RUN: %kleaver -print-ast %t3.log > %t4.log // RUN: diff %t3.log %t4.log -- cgit 1.4.1