diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Solver/STPSolver.cpp | 182 |
1 files changed, 85 insertions, 97 deletions
diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index b058a9cb..e8b9222f 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -7,27 +7,25 @@ // //===----------------------------------------------------------------------===// #include "klee/Config/config.h" + #ifdef ENABLE_STP -#include "STPSolver.h" #include "STPBuilder.h" -#include "klee/Solver.h" -#include "klee/SolverImpl.h" +#include "STPSolver.h" #include "klee/Constraints.h" -#include "klee/Internal/Support/ErrorHandling.h" #include "klee/OptionCategories.h" +#include "klee/SolverImpl.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "klee/util/Assignment.h" #include "klee/util/ExprUtil.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/Errno.h" -#include "llvm/Support/ErrorHandling.h" -#include <errno.h> +#include <csignal> #include <unistd.h> -#include <signal.h> -#include <sys/wait.h> #include <sys/ipc.h> #include <sys/shm.h> +#include <sys/wait.h> namespace { @@ -44,7 +42,7 @@ llvm::cl::opt<bool> IgnoreSolverFailures( #define vc_bvBoolExtract IAMTHESPAWNOFSATAN -static unsigned char *shared_memory_ptr; +static unsigned char *shared_memory_ptr = nullptr; 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 @@ -73,25 +71,25 @@ private: SolverRunStatus runStatusCode; public: - STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides = true); - ~STPSolverImpl(); + explicit STPSolverImpl(bool useForkedSTP, bool optimizeDivides = true); + ~STPSolverImpl() override; - char *getConstraintLog(const Query &); - void setCoreSolverTimeout(time::Span timeout) { this->timeout = timeout; } + char *getConstraintLog(const Query &) override; + void setCoreSolverTimeout(time::Span timeout) override { this->timeout = timeout; } - bool computeTruth(const Query &, bool &isValid); - bool computeValue(const Query &, ref<Expr> &result); + bool computeTruth(const Query &, bool &isValid) override; + bool computeValue(const Query &, ref<Expr> &result) override; bool computeInitialValues(const Query &, const std::vector<const Array *> &objects, - std::vector<std::vector<unsigned char> > &values, - bool &hasSolution); - SolverRunStatus getOperationStatusCode(); + std::vector<std::vector<unsigned char>> &values, + bool &hasSolution) override; + SolverRunStatus getOperationStatusCode() override; }; -STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides) +STPSolverImpl::STPSolverImpl(bool useForkedSTP, bool optimizeDivides) : vc(vc_createValidityChecker()), - builder(new STPBuilder(vc, _optimizeDivides)), - useForkedSTP(_useForkedSTP), runStatusCode(SOLVER_RUN_STATUS_FAILURE) { + builder(new STPBuilder(vc, optimizeDivides)), + useForkedSTP(useForkedSTP), runStatusCode(SOLVER_RUN_STATUS_FAILURE) { assert(vc && "unable to create validity checker"); assert(builder && "unable to create STPBuilder"); @@ -113,17 +111,17 @@ STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides) shmget(IPC_PRIVATE, shared_memory_size, IPC_CREAT | 0700); if (shared_memory_id < 0) llvm::report_fatal_error("unable to allocate shared memory region"); - shared_memory_ptr = (unsigned char *)shmat(shared_memory_id, NULL, 0); + shared_memory_ptr = (unsigned char *)shmat(shared_memory_id, nullptr, 0); if (shared_memory_ptr == (void *)-1) llvm::report_fatal_error("unable to attach shared memory region"); - shmctl(shared_memory_id, IPC_RMID, NULL); + shmctl(shared_memory_id, IPC_RMID, nullptr); } } STPSolverImpl::~STPSolverImpl() { // Detach the memory region. shmdt(shared_memory_ptr); - shared_memory_ptr = 0; + shared_memory_ptr = nullptr; shared_memory_id = 0; delete builder; @@ -135,10 +133,9 @@ STPSolverImpl::~STPSolverImpl() { char *STPSolverImpl::getConstraintLog(const Query &query) { vc_push(vc); - for (std::vector<ref<Expr> >::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); - it != ie; ++it) - vc_assertFormula(vc, builder->construct(*it)); + + for (const auto &constraint : query.constraints) + vc_assertFormula(vc, builder->construct(constraint)); assert(query.expr == ConstantExpr::alloc(0, Expr::Bool) && "Unexpected expression in query!"); @@ -152,7 +149,7 @@ char *STPSolverImpl::getConstraintLog(const Query &query) { bool STPSolverImpl::computeTruth(const Query &query, bool &isValid) { std::vector<const Array *> objects; - std::vector<std::vector<unsigned char> > values; + std::vector<std::vector<unsigned char>> values; bool hasSolution; if (!computeInitialValues(query, objects, values, hasSolution)) @@ -164,7 +161,7 @@ bool STPSolverImpl::computeTruth(const Query &query, bool &isValid) { bool STPSolverImpl::computeValue(const Query &query, ref<Expr> &result) { std::vector<const Array *> objects; - std::vector<std::vector<unsigned char> > values; + std::vector<std::vector<unsigned char>> values; bool hasSolution; // Find the object used in the expression, and compute an assignment @@ -184,36 +181,28 @@ bool STPSolverImpl::computeValue(const Query &query, ref<Expr> &result) { static SolverImpl::SolverRunStatus runAndGetCex(::VC vc, STPBuilder *builder, ::VCExpr q, const std::vector<const Array *> &objects, - std::vector<std::vector<unsigned char> > &values, + std::vector<std::vector<unsigned char>> &values, bool &hasSolution) { // XXX I want to be able to timeout here, safely hasSolution = !vc_query(vc, q); - 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; - std::vector<unsigned char> data; - - data.reserve(array->size); - for (unsigned offset = 0; offset < array->size; offset++) { - ExprHandle counter = - vc_getCounterExample(vc, builder->getInitialRead(array, offset)); - unsigned char val = getBVUnsigned(counter); - data.push_back(val); - } + if (!hasSolution) + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE; + + values.reserve(objects.size()); + unsigned i = 0; // FIXME C++17: use reference from emplace_back() + for (const auto object : objects) { + values.emplace_back(object->size); - values.push_back(data); + for (unsigned offset = 0; offset < object->size; offset++) { + ExprHandle counter = + vc_getCounterExample(vc, builder->getInitialRead(object, offset)); + values[i][offset] = static_cast<unsigned char>(getBVUnsigned(counter)); } + ++i; } - if (true == hasSolution) { - return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; - } else { - return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE; - } + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; } static void stpTimeoutHandler(int x) { _exit(52); } @@ -221,47 +210,46 @@ static void stpTimeoutHandler(int x) { _exit(52); } static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q, const std::vector<const Array *> &objects, - std::vector<std::vector<unsigned char> > &values, + std::vector<std::vector<unsigned char>> &values, bool &hasSolution, time::Span 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; + for (const auto object : objects) + sum += object->size; if (sum >= shared_memory_size) llvm::report_fatal_error("not enough shared memory for counterexample"); fflush(stdout); fflush(stderr); + + // fork solver int pid = fork(); + // - error if (pid == -1) { klee_warning("fork failed (for STP) - %s", llvm::sys::StrError(errno).c_str()); if (!IgnoreSolverFailures) exit(1); return SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED; } - + // - child (solver) if (pid == 0) { if (timeout) { ::alarm(0); /* Turn off alarm so we can safely set signal handler */ ::signal(SIGALRM, stpTimeoutHandler); ::alarm(std::max(1u, static_cast<unsigned>(timeout.toSeconds()))); } - unsigned res = vc_query(vc, q); + int res = vc_query(vc, q); if (!res) { - for (std::vector<const Array *>::const_iterator it = objects.begin(), - ie = objects.end(); - it != ie; ++it) { - const Array *array = *it; - for (unsigned offset = 0; offset < array->size; offset++) { + for (const auto object : objects) { + for (unsigned offset = 0; offset < object->size; offset++) { ExprHandle counter = - vc_getCounterExample(vc, builder->getInitialRead(array, offset)); - *pos++ = getBVUnsigned(counter); + vc_getCounterExample(vc, builder->getInitialRead(object, offset)); + *pos++ = static_cast<unsigned char>(getBVUnsigned(counter)); } } } _exit(res); + // - parent } else { int status; pid_t res; @@ -290,53 +278,51 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q, } int exitcode = WEXITSTATUS(status); + + // solvable if (exitcode == 0) { hasSolution = true; - } else if (exitcode == 1) { - hasSolution = false; - } else if (exitcode == 52) { - klee_warning("STP timed out"); - // mark that a timeout occurred - return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT; - } else { - klee_warning("STP did not return a recognized code"); - if (!IgnoreSolverFailures) - exit(1); - 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; - std::vector<unsigned char> &data = values[i++]; - data.insert(data.begin(), pos, pos + array->size); - pos += array->size; + values.reserve(objects.size()); + for (const auto object : objects) { + values.emplace_back(pos, pos + object->size); + pos += object->size; } - } - if (true == hasSolution) { return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; - } else { + } + + // unsolvable + if (exitcode == 1) { + hasSolution = false; return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE; } + + // timeout + if (exitcode == 52) { + klee_warning("STP timed out"); + // mark that a timeout occurred + return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT; + } + + // unknown return code + klee_warning("STP did not return a recognized code"); + if (!IgnoreSolverFailures) + exit(1); + return SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE; } } + bool STPSolverImpl::computeInitialValues( const Query &query, const std::vector<const Array *> &objects, - std::vector<std::vector<unsigned char> > &values, bool &hasSolution) { + std::vector<std::vector<unsigned char>> &values, bool &hasSolution) { runStatusCode = SOLVER_RUN_STATUS_FAILURE; TimerStatIncrementer t(stats::queryTime); vc_push(vc); - for (ConstraintManager::const_iterator it = query.constraints.begin(), - ie = query.constraints.end(); - it != ie; ++it) - vc_assertFormula(vc, builder->construct(*it)); + for (const auto &constraint : query.constraints) + vc_assertFormula(vc, builder->construct(constraint)); ++stats::queries; ++stats::queryCounterexamples; @@ -348,6 +334,7 @@ bool STPSolverImpl::computeInitialValues( unsigned long len; vc_printQueryStateToBuffer(vc, stp_e, &buf, &len, false); klee_warning("STP query:\n%.*s\n", (unsigned)len, buf); + free(buf); } bool success; @@ -388,5 +375,6 @@ char *STPSolver::getConstraintLog(const Query &query) { void STPSolver::setCoreSolverTimeout(time::Span timeout) { impl->setCoreSolverTimeout(timeout); } -} + +} // klee #endif // ENABLE_STP |