diff options
-rw-r--r-- | include/klee/IncompleteSolver.h | 2 | ||||
-rw-r--r-- | include/klee/Solver.h | 6 | ||||
-rw-r--r-- | include/klee/SolverImpl.h | 17 | ||||
-rw-r--r-- | lib/Solver/CachingSolver.cpp | 6 | ||||
-rw-r--r-- | lib/Solver/CexCachingSolver.cpp | 6 | ||||
-rw-r--r-- | lib/Solver/IncompleteSolver.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/IndependentSolver.cpp | 6 | ||||
-rw-r--r-- | lib/Solver/Solver.cpp | 143 | ||||
-rw-r--r-- | tools/kleaver/main.cpp | 15 |
9 files changed, 128 insertions, 77 deletions
diff --git a/include/klee/IncompleteSolver.h b/include/klee/IncompleteSolver.h index 38ee4e28..9a122c74 100644 --- a/include/klee/IncompleteSolver.h +++ b/include/klee/IncompleteSolver.h @@ -101,7 +101,7 @@ public: const std::vector<const Array*> &objects, std::vector< std::vector<unsigned char> > &values, bool &hasSolution); - bool hasTimeoutOccurred(); + SolverRunStatus getOperationStatusCode(); }; } diff --git a/include/klee/Solver.h b/include/klee/Solver.h index 94e7d477..9e05967d 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -226,12 +226,6 @@ namespace klee { /// fails. Solver *createDummySolver(); - enum SolverRunStatus { SOLVER_RUN_STATUS_SUCCESS, - SOLVER_RUN_STATUS_TIMEOUT, - SOLVER_RUN_STATUS_FORK_FAILED, - SOLVER_RUN_STATUS_INTERRUPTED, - SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE, - SOLVER_RUN_STATUS_WAITPID_FAILED }; } #endif diff --git a/include/klee/SolverImpl.h b/include/klee/SolverImpl.h index 080dfc54..09be849b 100644 --- a/include/klee/SolverImpl.h +++ b/include/klee/SolverImpl.h @@ -28,6 +28,15 @@ namespace klee { SolverImpl() {} virtual ~SolverImpl(); + enum SolverRunStatus { SOLVER_RUN_STATUS_SUCCESS_SOLVABLE, + SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE, + SOLVER_RUN_STATUS_FAILURE, + SOLVER_RUN_STATUS_TIMEOUT, + SOLVER_RUN_STATUS_FORK_FAILED, + SOLVER_RUN_STATUS_INTERRUPTED, + SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE, + SOLVER_RUN_STATUS_WAITPID_FAILED }; + /// computeValidity - Compute a full validity result for the /// query. /// @@ -57,8 +66,12 @@ namespace klee { &values, bool &hasSolution) = 0; - /// haveTimeOutOccurred - retrieve timeout status for the last query. - virtual bool hasTimeoutOccurred() = 0; + /// getOperationStatusCode - get the status of the last solver operation + virtual SolverRunStatus getOperationStatusCode() = 0; + + /// getOperationStatusString - get string representation of the operation + /// status code + static const char* getOperationStatusString(SolverRunStatus statusCode); }; } diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index f7b88855..b6a93c7b 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -82,7 +82,7 @@ public: return solver->impl->computeInitialValues(query, objects, values, hasSolution); } - bool hasTimeoutOccurred(); + SolverRunStatus getOperationStatusCode(); }; /** @returns the canonical version of the given query. The reference @@ -235,8 +235,8 @@ bool CachingSolver::computeTruth(const Query& query, return true; } -bool CachingSolver::hasTimeoutOccurred() { - return solver->impl->hasTimeoutOccurred(); +SolverImpl::SolverRunStatus CachingSolver::getOperationStatusCode() { + return solver->impl->getOperationStatusCode(); } /// diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index c84ae409..3d7a754c 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -82,7 +82,7 @@ public: const std::vector<const Array*> &objects, std::vector< std::vector<unsigned char> > &values, bool &hasSolution); - bool hasTimeoutOccurred(); + SolverRunStatus getOperationStatusCode(); }; /// @@ -340,8 +340,8 @@ CexCachingSolver::computeInitialValues(const Query& query, return true; } -bool CexCachingSolver::hasTimeoutOccurred() { - return solver->impl->hasTimeoutOccurred(); +SolverImpl::SolverRunStatus CexCachingSolver::getOperationStatusCode() { + return solver->impl->getOperationStatusCode(); } /// diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp index 45e2ea9b..7bc8058d 100644 --- a/lib/Solver/IncompleteSolver.cpp +++ b/lib/Solver/IncompleteSolver.cpp @@ -135,6 +135,6 @@ StagedSolverImpl::computeInitialValues(const Query& query, hasSolution); } -bool StagedSolverImpl::hasTimeoutOccurred() { - return secondary->impl->hasTimeoutOccurred(); +SolverImpl::SolverRunStatus StagedSolverImpl::getOperationStatusCode() { + return secondary->impl->getOperationStatusCode(); } diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 0eb86720..b3ef1e57 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -284,7 +284,7 @@ public: return solver->impl->computeInitialValues(query, objects, values, hasSolution); } - bool hasTimeoutOccurred(); + SolverRunStatus getOperationStatusCode(); }; bool IndependentSolver::computeValidity(const Query& query, @@ -314,8 +314,8 @@ bool IndependentSolver::computeValue(const Query& query, ref<Expr> &result) { return solver->impl->computeValue(Query(tmp, query.expr), result); } -bool IndependentSolver::hasTimeoutOccurred() { - return solver->impl->hasTimeoutOccurred(); +SolverImpl::SolverRunStatus IndependentSolver::getOperationStatusCode() { + return solver->impl->getOperationStatusCode(); } Solver *klee::createIndependentSolver(Solver *s) { diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 366a7b05..abb70770 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -39,6 +39,48 @@ using namespace klee; /***/ +SolverImpl::~SolverImpl() { +} + +bool SolverImpl::computeValidity(const Query& query, Solver::Validity &result) { + bool isTrue, isFalse; + if (!computeTruth(query, isTrue)) + return false; + if (isTrue) { + result = Solver::True; + } else { + if (!computeTruth(query.negateExpr(), isFalse)) + return false; + result = isFalse ? Solver::False : Solver::Unknown; + } + return true; +} + +const char* SolverImpl::getOperationStatusString(SolverRunStatus statusCode) +{ + switch (statusCode) + { + case SOLVER_RUN_STATUS_SUCCESS_SOLVABLE: + return "OPERATION SUCCESSFUL, QUERY IS SOLVABLE"; + case SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE: + return "OPERATION SUCCESSFUL, QUERY IS UNSOLVABLE"; + case SOLVER_RUN_STATUS_FAILURE: + return "OPERATION FAILED"; + case SOLVER_RUN_STATUS_TIMEOUT: + return "SOLVER TIMEOUT"; + case SOLVER_RUN_STATUS_FORK_FAILED: + return "FORK FAILED"; + case SOLVER_RUN_STATUS_INTERRUPTED: + return "SOLVER PROCESS INTERRUPTED"; + case SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE: + return "UNEXPECTED SOLVER PROCESS EXIT CODE"; + case SOLVER_RUN_STATUS_WAITPID_FAILED: + return "WAITPID FAILED FOR SOLVER PROCESS"; + default: + return "UNRECOGNIZED OPERATION STATUS"; + } +} + const char *Solver::validity_to_str(Validity v) { switch (v) { default: return "Unknown"; @@ -51,9 +93,6 @@ Solver::~Solver() { delete impl; } -SolverImpl::~SolverImpl() { -} - bool Solver::evaluate(const Query& query, Validity &result) { assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!"); @@ -66,20 +105,6 @@ bool Solver::evaluate(const Query& query, Validity &result) { return impl->computeValidity(query, result); } -bool SolverImpl::computeValidity(const Query& query, Solver::Validity &result) { - bool isTrue, isFalse; - if (!computeTruth(query, isTrue)) - return false; - if (isTrue) { - result = Solver::True; - } else { - if (!computeTruth(query.negateExpr(), isFalse)) - return false; - result = isFalse ? Solver::False : Solver::Unknown; - } - return true; -} - bool Solver::mustBeTrue(const Query& query, bool &result) { assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!"); @@ -273,7 +298,7 @@ public: const std::vector<const Array*> &objects, std::vector< std::vector<unsigned char> > &values, bool &hasSolution); - bool hasTimeoutOccurred(); + SolverRunStatus getOperationStatusCode(); }; bool ValidatingSolver::computeTruth(const Query& query, @@ -371,8 +396,8 @@ ValidatingSolver::computeInitialValues(const Query& query, return true; } -bool ValidatingSolver::hasTimeoutOccurred() { - return solver->impl->hasTimeoutOccurred(); +SolverImpl::SolverRunStatus ValidatingSolver::getOperationStatusCode() { + return solver->impl->getOperationStatusCode(); } Solver *klee::createValidatingSolver(Solver *s, Solver *oracle) { @@ -408,8 +433,8 @@ public: ++stats::queryCounterexamples; return false; } - bool hasTimeoutOccurred() { - return false; + SolverRunStatus getOperationStatusCode() { + return SOLVER_RUN_STATUS_FAILURE; } }; @@ -428,7 +453,7 @@ private: STPBuilder *builder; double timeout; bool useForkedSTP; - bool timeoutOccurred; + SolverRunStatus runStatusCode; public: STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true); @@ -443,7 +468,7 @@ public: const std::vector<const Array*> &objects, std::vector< std::vector<unsigned char> > &values, bool &hasSolution); - bool hasTimeoutOccurred(); + SolverRunStatus getOperationStatusCode(); }; static unsigned char *shared_memory_ptr; @@ -461,7 +486,7 @@ STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optim builder(new STPBuilder(vc, _optimizeDivides)), timeout(0.0), useForkedSTP(_useForkedSTP), - timeoutOccurred(false) + runStatusCode(SOLVER_RUN_STATUS_FAILURE) { assert(vc && "unable to create validity checker"); assert(builder && "unable to create STPBuilder"); @@ -558,10 +583,10 @@ bool STPSolverImpl::computeValue(const Query& query, return true; } -static void runAndGetCex(::VC vc, STPBuilder *builder, ::VCExpr q, - const std::vector<const Array*> &objects, - std::vector< std::vector<unsigned char> > &values, - bool &hasSolution) { +static SolverImpl::SolverRunStatus runAndGetCex(::VC vc, STPBuilder *builder, ::VCExpr q, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution) { // XXX I want to be able to timeout here, safely hasSolution = !vc_query(vc, q); @@ -583,20 +608,27 @@ static void runAndGetCex(::VC vc, STPBuilder *builder, ::VCExpr q, values.push_back(data); } } + + if (true == hasSolution) { + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; + } + else { + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE; + } } static void stpTimeoutHandler(int x) { _exit(52); } -static SolverRunStatus runAndGetCexForked(::VC vc, - STPBuilder *builder, - ::VCExpr q, - const std::vector<const Array*> &objects, - std::vector< std::vector<unsigned char> > - &values, - bool &hasSolution, - double timeout) { +static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc, + STPBuilder *builder, + ::VCExpr q, + 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 @@ -609,7 +641,7 @@ static SolverRunStatus runAndGetCexForked(::VC vc, int pid = fork(); if (pid==-1) { fprintf(stderr, "error: fork failed (for STP)"); - return SOLVER_RUN_STATUS_FORK_FAILED; + return SolverImpl::SOLVER_RUN_STATUS_FORK_FAILED; } if (pid == 0) { @@ -641,7 +673,7 @@ static SolverRunStatus runAndGetCexForked(::VC vc, if (res < 0) { fprintf(stderr, "error: waitpid() for STP failed"); - return SOLVER_RUN_STATUS_WAITPID_FAILED; + return SolverImpl::SOLVER_RUN_STATUS_WAITPID_FAILED; } // From timed_run.py: It appears that linux at least will on @@ -649,7 +681,7 @@ static SolverRunStatus runAndGetCexForked(::VC vc, // signal, so test signal first. if (WIFSIGNALED(status) || !WIFEXITED(status)) { fprintf(stderr, "error: STP did not return successfully"); - return SOLVER_RUN_STATUS_INTERRUPTED; + return SolverImpl::SOLVER_RUN_STATUS_INTERRUPTED; } int exitcode = WEXITSTATUS(status); @@ -660,10 +692,10 @@ static SolverRunStatus runAndGetCexForked(::VC vc, } else if (exitcode==52) { fprintf(stderr, "error: STP timed out"); // mark that a timeout occurred - return SOLVER_RUN_STATUS_TIMEOUT; + return SolverImpl::SOLVER_RUN_STATUS_TIMEOUT; } else { fprintf(stderr, "error: STP did not return a recognized code"); - return SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE; + return SolverImpl::SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE; } if (hasSolution) { @@ -677,11 +709,16 @@ static SolverRunStatus runAndGetCexForked(::VC vc, pos += array->size; } } - - return SOLVER_RUN_STATUS_SUCCESS; + + if (true == hasSolution) { + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_SOLVABLE; + } + else { + return SolverImpl::SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE; + } } } - +#include <iostream> bool STPSolverImpl::computeInitialValues(const Query &query, const std::vector<const Array*> @@ -689,7 +726,7 @@ STPSolverImpl::computeInitialValues(const Query &query, std::vector< std::vector<unsigned char> > &values, bool &hasSolution) { - timeoutOccurred = false; + runStatusCode = SOLVER_RUN_STATUS_FAILURE; TimerStatIncrementer t(stats::queryTime); @@ -713,12 +750,12 @@ STPSolverImpl::computeInitialValues(const Query &query, bool success; if (useForkedSTP) { - SolverRunStatus runStatus = runAndGetCexForked(vc, builder, stp_e, objects, values, - hasSolution, timeout); - success = (SOLVER_RUN_STATUS_SUCCESS == runStatus); - timeoutOccurred = (SOLVER_RUN_STATUS_TIMEOUT == runStatus); + runStatusCode = runAndGetCexForked(vc, builder, stp_e, objects, values, + hasSolution, timeout); + success = ((SOLVER_RUN_STATUS_SUCCESS_SOLVABLE == runStatusCode) || + (SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE == runStatusCode)); } else { - runAndGetCex(vc, builder, stp_e, objects, values, hasSolution); + runStatusCode = runAndGetCex(vc, builder, stp_e, objects, values, hasSolution); success = true; } @@ -734,6 +771,6 @@ STPSolverImpl::computeInitialValues(const Query &query, return success; } -bool STPSolverImpl::hasTimeoutOccurred() { - return timeoutOccurred; +SolverImpl::SolverRunStatus STPSolverImpl::getOperationStatusCode() { + return runStatusCode; } diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 16a0ea42..1a4663a1 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -8,6 +8,7 @@ #include "klee/Expr.h" #include "klee/ExprBuilder.h" #include "klee/Solver.h" +#include "klee/SolverImpl.h" #include "klee/Statistics.h" #include "klee/util/ExprPPrinter.h" #include "klee/util/ExprVisitor.h" @@ -93,7 +94,7 @@ namespace { UseFastCexSolver("use-fast-cex-solver", cl::init(false)); - // FIXME: Command line argument duplicated in Executor.cpp of Klee. Different + // FIXME: Command line argument modified in Executor.cpp of Klee. Different // output file name used. cl::opt<bool> UseSTPQueryPCLog("use-stp-query-pc-log", @@ -220,7 +221,9 @@ static bool EvaluateInputAST(const char *Filename, result)) { std::cout << (result ? "VALID" : "INVALID"); } else { - std::cout << "FAIL"; + std::cout << "FAIL (reason: " + << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode()) + << ")"; } } else if (!QC->Values.empty()) { assert(QC->Objects.empty() && @@ -236,7 +239,9 @@ static bool EvaluateInputAST(const char *Filename, std::cout << "INVALID\n"; std::cout << "\tExpr 0:\t" << result; } else { - std::cout << "FAIL"; + std::cout << "FAIL (reason: " + << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode()) + << ")"; } } else { std::vector< std::vector<unsigned char> > result; @@ -260,7 +265,9 @@ static bool EvaluateInputAST(const char *Filename, std::cout << "\n"; } } else { - std::cout << "FAIL"; + std::cout << "FAIL (reason: " + << SolverImpl::getOperationStatusString(S->impl->getOperationStatusCode()) + << ")"; } } |