diff options
author | Cristian Cadar <cristic@cs.stanford.edu> | 2013-01-02 14:33:58 +0000 |
---|---|---|
committer | Cristian Cadar <cristic@cs.stanford.edu> | 2013-01-02 14:33:58 +0000 |
commit | c7db4230beef3b81542edb5d7ae6ca606d0567dd (patch) | |
tree | f3913e6ea23e0bffbbeff0fc8f5810159c1517f9 | |
parent | 26bf73bf80369a24467fcf1f53165824cbcd5679 (diff) | |
download | klee-c7db4230beef3b81542edb5d7ae6ca606d0567dd.tar.gz |
Patch by Tomasz Kuchta adding a new option (min-query-time-to-log) that enables KLEE to log only the queries exceeding a certain duration, or only those that time out.
git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171385 91177308-0d34-0410-b5e6-96231b3b80d8
-rw-r--r-- | include/klee/IncompleteSolver.h | 1 | ||||
-rw-r--r-- | include/klee/Solver.h | 10 | ||||
-rw-r--r-- | include/klee/SolverImpl.h | 5 | ||||
-rw-r--r-- | lib/Core/Executor.cpp | 15 | ||||
-rw-r--r-- | lib/Solver/CachingSolver.cpp | 5 | ||||
-rw-r--r-- | lib/Solver/CexCachingSolver.cpp | 5 | ||||
-rw-r--r-- | lib/Solver/IncompleteSolver.cpp | 4 | ||||
-rw-r--r-- | lib/Solver/IndependentSolver.cpp | 5 | ||||
-rw-r--r-- | lib/Solver/PCLoggingSolver.cpp | 112 | ||||
-rw-r--r-- | lib/Solver/SMTLIBLoggingSolver.cpp | 5 | ||||
-rw-r--r-- | lib/Solver/Solver.cpp | 57 | ||||
-rw-r--r-- | tools/kleaver/main.cpp | 13 |
12 files changed, 187 insertions, 50 deletions
diff --git a/include/klee/IncompleteSolver.h b/include/klee/IncompleteSolver.h index 9c05ad21..38ee4e28 100644 --- a/include/klee/IncompleteSolver.h +++ b/include/klee/IncompleteSolver.h @@ -101,6 +101,7 @@ public: const std::vector<const Array*> &objects, std::vector< std::vector<unsigned char> > &values, bool &hasSolution); + bool hasTimeoutOccurred(); }; } diff --git a/include/klee/Solver.h b/include/klee/Solver.h index 4cedf47d..db14f003 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -213,7 +213,8 @@ namespace klee { /// createPCLoggingSolver - Create a solver which will forward all queries /// after writing them to the given path in .pc format. - Solver *createPCLoggingSolver(Solver *s, std::string path); + Solver *createPCLoggingSolver(Solver *s, std::string path, + int minQueryTimeToLog); /// createSMTLIBLoggingSolver - Create a solver which will forward all queries /// after writing them to the given path in .smt2 format. @@ -223,6 +224,13 @@ namespace klee { /// createDummySolver - Create a dummy solver implementation which always /// 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 29c356be..080dfc54 100644 --- a/include/klee/SolverImpl.h +++ b/include/klee/SolverImpl.h @@ -55,7 +55,10 @@ namespace klee { &objects, std::vector< std::vector<unsigned char> > &values, - bool &hasSolution) = 0; + bool &hasSolution) = 0; + + /// haveTimeOutOccurred - retrieve timeout status for the last query. + virtual bool hasTimeoutOccurred() = 0; }; } diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 968283b7..b8db18fe 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -164,6 +164,15 @@ namespace { cl::init(true), cl::desc("Use counterexample caching (default=on)")); + // FIXME: Command line argument duplicated in main.cpp of Kleaver + cl::opt<int> + MinQueryTimeToLog("min-query-time-to-log", + cl::init(0), + cl::value_desc("milliseconds"), + cl::desc("Set time threshold (in ms) for queries logged in files. " + "Only queries longer than threshold will be logged. (default=0). " + "Set this param to a negative value to log timeouts only.")); + cl::opt<bool> NoExternals("no-externals", cl::desc("Do not allow external function calls (default=off)")); @@ -301,7 +310,8 @@ Solver *constructSolverChain(STPSolver *stpSolver, if (optionIsSet(queryLoggingOptions,SOLVER_PC)) { solver = createPCLoggingSolver(solver, - baseSolverQueryPCLogPath); + baseSolverQueryPCLogPath, + MinQueryTimeToLog); klee_message("Logging queries that reach solver in .pc format to %s",baseSolverQueryPCLogPath.c_str()); } @@ -329,7 +339,8 @@ Solver *constructSolverChain(STPSolver *stpSolver, if (optionIsSet(queryLoggingOptions,ALL_PC)) { solver = createPCLoggingSolver(solver, - queryPCLogPath); + queryPCLogPath, + MinQueryTimeToLog); klee_message("Logging all queries in .pc format to %s",queryPCLogPath.c_str()); } diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index c0b77429..f7b88855 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -82,6 +82,7 @@ public: return solver->impl->computeInitialValues(query, objects, values, hasSolution); } + bool hasTimeoutOccurred(); }; /** @returns the canonical version of the given query. The reference @@ -234,6 +235,10 @@ bool CachingSolver::computeTruth(const Query& query, return true; } +bool CachingSolver::hasTimeoutOccurred() { + return solver->impl->hasTimeoutOccurred(); +} + /// Solver *klee::createCachingSolver(Solver *_solver) { diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index 19f16821..c84ae409 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -82,6 +82,7 @@ public: const std::vector<const Array*> &objects, std::vector< std::vector<unsigned char> > &values, bool &hasSolution); + bool hasTimeoutOccurred(); }; /// @@ -339,6 +340,10 @@ CexCachingSolver::computeInitialValues(const Query& query, return true; } +bool CexCachingSolver::hasTimeoutOccurred() { + return solver->impl->hasTimeoutOccurred(); +} + /// Solver *klee::createCexCachingSolver(Solver *_solver) { diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp index a565bab2..45e2ea9b 100644 --- a/lib/Solver/IncompleteSolver.cpp +++ b/lib/Solver/IncompleteSolver.cpp @@ -134,3 +134,7 @@ StagedSolverImpl::computeInitialValues(const Query& query, return secondary->impl->computeInitialValues(query, objects, values, hasSolution); } + +bool StagedSolverImpl::hasTimeoutOccurred() { + return secondary->impl->hasTimeoutOccurred(); +} diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 70f3cab2..0eb86720 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -284,6 +284,7 @@ public: return solver->impl->computeInitialValues(query, objects, values, hasSolution); } + bool hasTimeoutOccurred(); }; bool IndependentSolver::computeValidity(const Query& query, @@ -313,6 +314,10 @@ 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(); +} + Solver *klee::createIndependentSolver(Solver *s) { return new Solver(new IndependentSolver(s)); } diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/PCLoggingSolver.cpp index e7128982..0b31182e 100644 --- a/lib/Solver/PCLoggingSolver.cpp +++ b/lib/Solver/PCLoggingSolver.cpp @@ -19,7 +19,8 @@ #include "llvm/Support/CommandLine.h" #include <fstream> - +#include <sstream> +#include <iostream> using namespace klee; using namespace llvm; using namespace klee::util; @@ -29,9 +30,17 @@ using namespace klee::util; class PCLoggingSolver : public SolverImpl { Solver *solver; std::ofstream os; + std::ostringstream logBuffer; // buffer to store logs before flushing to + // file ExprPPrinter *printer; unsigned queryCount; + int minQueryTimeToLog; // we log to file only those queries + // which take longer than specified time (ms); + // if this param is negative, log only those queries + // on which solver's timed out + double startTime; + double lastQueryTime; void startQuery(const Query& query, const char *typeName, const ref<Expr> *evalExprsBegin = 0, @@ -40,30 +49,62 @@ class PCLoggingSolver : public SolverImpl { const Array * const* evalArraysEnd = 0) { Statistic *S = theStatisticManager->getStatisticByName("Instructions"); uint64_t instructions = S ? S->getValue() : 0; - os << "# Query " << queryCount++ << " -- " - << "Type: " << typeName << ", " - << "Instructions: " << instructions << "\n"; - printer->printQuery(os, query.constraints, query.expr, + + logBuffer << "# Query " << queryCount++ << " -- " + << "Type: " << typeName << ", " + << "Instructions: " << instructions << "\n"; + printer->printQuery(logBuffer, query.constraints, query.expr, evalExprsBegin, evalExprsEnd, evalArraysBegin, evalArraysEnd); - + startTime = getWallTime(); } void finishQuery(bool success) { - double delta = getWallTime() - startTime; - os << "# " << (success ? "OK" : "FAIL") << " -- " - << "Elapsed: " << delta << "\n"; + lastQueryTime = getWallTime() - startTime; + logBuffer << "# " << (success ? "OK" : "FAIL") << " -- " + << "Elapsed: " << lastQueryTime << "\n"; + + if (true == solver->impl->hasTimeoutOccurred()) { + logBuffer << "\nSolver TIMEOUT detected\n"; + } + } + + /// flushBuffer - flushes the temporary logs buffer. Depending on threshold + /// settings, contents of the buffer are either discarded or written to a file. + void flushBuffer(void) { + logBuffer.flush(); + + if ((0 == minQueryTimeToLog) || + (static_cast<int>(lastQueryTime * 1000) > minQueryTimeToLog)) { + // we either do not limit logging queries or the query time + // is larger than threshold (in ms) + + if ((minQueryTimeToLog >= 0) || + (true == (solver->impl->hasTimeoutOccurred()))) { + // we do additional check here to log only timeouts in case + // user specified negative value for minQueryTimeToLog param + os << logBuffer.str(); + } + } + + // prepare the buffer for reuse + logBuffer.clear(); + logBuffer.str(""); } public: - PCLoggingSolver(Solver *_solver, std::string path) + PCLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog) : solver(_solver), os(path.c_str(), std::ios::trunc), - printer(ExprPPrinter::create(os)), - queryCount(0) { + logBuffer(""), + printer(ExprPPrinter::create(logBuffer)), + queryCount(0), + minQueryTimeToLog(queryTimeToLog), + startTime(0.0f), + lastQueryTime(0.0f) { } - ~PCLoggingSolver() { + ~PCLoggingSolver() { delete printer; delete solver; } @@ -73,8 +114,11 @@ public: bool success = solver->impl->computeTruth(query, isValid); finishQuery(success); if (success) - os << "# Is Valid: " << (isValid ? "true" : "false") << "\n"; - os << "\n"; + logBuffer << "# Is Valid: " << (isValid ? "true" : "false") << "\n"; + logBuffer << "\n"; + + flushBuffer(); + return success; } @@ -83,8 +127,11 @@ public: bool success = solver->impl->computeValidity(query, result); finishQuery(success); if (success) - os << "# Validity: " << result << "\n"; - os << "\n"; + logBuffer << "# Validity: " << result << "\n"; + logBuffer << "\n"; + + flushBuffer(); + return success; } @@ -94,8 +141,11 @@ public: bool success = solver->impl->computeValue(query, result); finishQuery(success); if (success) - os << "# Result: " << result << "\n"; - os << "\n"; + logBuffer << "# Result: " << result << "\n"; + logBuffer << "\n"; + + flushBuffer(); + return success; } @@ -115,7 +165,7 @@ public: values, hasSolution); finishQuery(success); if (success) { - os << "# Solvable: " << (hasSolution ? "true" : "false") << "\n"; + logBuffer << "# Solvable: " << (hasSolution ? "true" : "false") << "\n"; if (hasSolution) { std::vector< std::vector<unsigned char> >::iterator values_it = values.begin(); @@ -123,23 +173,31 @@ public: e = objects.end(); i != e; ++i, ++values_it) { const Array *array = *i; std::vector<unsigned char> &data = *values_it; - os << "# " << array->name << " = ["; + logBuffer << "# " << array->name << " = ["; for (unsigned j = 0; j < array->size; j++) { - os << (int) data[j]; + logBuffer << (int) data[j]; if (j+1 < array->size) - os << ","; + logBuffer << ","; } - os << "]\n"; + logBuffer << "]\n"; } } } - os << "\n"; + logBuffer << "\n"; + + flushBuffer(); + return success; } + + bool hasTimeoutOccurred() { + return solver->impl->hasTimeoutOccurred(); + } }; /// -Solver *klee::createPCLoggingSolver(Solver *_solver, std::string path) { - return new Solver(new PCLoggingSolver(_solver, path)); +Solver *klee::createPCLoggingSolver(Solver *_solver, std::string path, + int minQueryTimeToLog) { + return new Solver(new PCLoggingSolver(_solver, path, minQueryTimeToLog)); } diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp index 0fb09424..b3f7eb3b 100644 --- a/lib/Solver/SMTLIBLoggingSolver.cpp +++ b/lib/Solver/SMTLIBLoggingSolver.cpp @@ -158,6 +158,11 @@ class SMTLIBLoggingSolver : public SolverImpl os << "\n"; return success; } + + bool hasTimeoutOccurred() + { + return solver->impl->hasTimeoutOccurred(); + } }; diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 7430a58b..366a7b05 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -273,6 +273,7 @@ public: const std::vector<const Array*> &objects, std::vector< std::vector<unsigned char> > &values, bool &hasSolution); + bool hasTimeoutOccurred(); }; bool ValidatingSolver::computeTruth(const Query& query, @@ -370,6 +371,10 @@ ValidatingSolver::computeInitialValues(const Query& query, return true; } +bool ValidatingSolver::hasTimeoutOccurred() { + return solver->impl->hasTimeoutOccurred(); +} + Solver *klee::createValidatingSolver(Solver *s, Solver *oracle) { return new Solver(new ValidatingSolver(s, oracle)); } @@ -403,6 +408,10 @@ public: ++stats::queryCounterexamples; return false; } + bool hasTimeoutOccurred() { + return false; + } + }; Solver *klee::createDummySolver() { @@ -419,6 +428,7 @@ private: STPBuilder *builder; double timeout; bool useForkedSTP; + bool timeoutOccurred; public: STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optimizeDivides = true); @@ -433,6 +443,7 @@ public: const std::vector<const Array*> &objects, std::vector< std::vector<unsigned char> > &values, bool &hasSolution); + bool hasTimeoutOccurred(); }; static unsigned char *shared_memory_ptr; @@ -449,7 +460,8 @@ STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optim vc(vc_createValidityChecker()), builder(new STPBuilder(vc, _optimizeDivides)), timeout(0.0), - useForkedSTP(_useForkedSTP) + useForkedSTP(_useForkedSTP), + timeoutOccurred(false) { assert(vc && "unable to create validity checker"); assert(builder && "unable to create STPBuilder"); @@ -577,14 +589,14 @@ static void stpTimeoutHandler(int x) { _exit(52); } -static bool 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 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 @@ -597,11 +609,11 @@ static bool runAndGetCexForked(::VC vc, int pid = fork(); if (pid==-1) { fprintf(stderr, "error: fork failed (for STP)"); - return false; + return SOLVER_RUN_STATUS_FORK_FAILED; } if (pid == 0) { - if (timeout) { + if (timeout) { ::alarm(0); /* Turn off alarm so we can safely set signal handler */ ::signal(SIGALRM, stpTimeoutHandler); ::alarm(std::max(1, (int)timeout)); @@ -629,7 +641,7 @@ static bool runAndGetCexForked(::VC vc, if (res < 0) { fprintf(stderr, "error: waitpid() for STP failed"); - return false; + return SOLVER_RUN_STATUS_WAITPID_FAILED; } // From timed_run.py: It appears that linux at least will on @@ -637,7 +649,7 @@ static bool runAndGetCexForked(::VC vc, // signal, so test signal first. if (WIFSIGNALED(status) || !WIFEXITED(status)) { fprintf(stderr, "error: STP did not return successfully"); - return false; + return SOLVER_RUN_STATUS_INTERRUPTED; } int exitcode = WEXITSTATUS(status); @@ -647,10 +659,11 @@ static bool runAndGetCexForked(::VC vc, hasSolution = false; } else if (exitcode==52) { fprintf(stderr, "error: STP timed out"); - return false; + // mark that a timeout occurred + return SOLVER_RUN_STATUS_TIMEOUT; } else { fprintf(stderr, "error: STP did not return a recognized code"); - return false; + return SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE; } if (hasSolution) { @@ -665,7 +678,7 @@ static bool runAndGetCexForked(::VC vc, } } - return true; + return SOLVER_RUN_STATUS_SUCCESS; } } @@ -676,6 +689,8 @@ STPSolverImpl::computeInitialValues(const Query &query, std::vector< std::vector<unsigned char> > &values, bool &hasSolution) { + timeoutOccurred = false; + TimerStatIncrementer t(stats::queryTime); vc_push(vc); @@ -698,8 +713,10 @@ STPSolverImpl::computeInitialValues(const Query &query, bool success; if (useForkedSTP) { - success = runAndGetCexForked(vc, builder, stp_e, objects, values, - hasSolution, timeout); + SolverRunStatus runStatus = runAndGetCexForked(vc, builder, stp_e, objects, values, + hasSolution, timeout); + success = (SOLVER_RUN_STATUS_SUCCESS == runStatus); + timeoutOccurred = (SOLVER_RUN_STATUS_TIMEOUT == runStatus); } else { runAndGetCex(vc, builder, stp_e, objects, values, hasSolution); success = true; @@ -716,3 +733,7 @@ STPSolverImpl::computeInitialValues(const Query &query, return success; } + +bool STPSolverImpl::hasTimeoutOccurred() { + return timeoutOccurred; +} diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 077de3ed..16a0ea42 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -93,9 +93,20 @@ namespace { UseFastCexSolver("use-fast-cex-solver", cl::init(false)); + // FIXME: Command line argument duplicated in Executor.cpp of Klee. Different + // output file name used. cl::opt<bool> UseSTPQueryPCLog("use-stp-query-pc-log", cl::init(false)); + + // FIXME: Command line argument duplicated in Executor.cpp of Klee + cl::opt<unsigned int> + MinQueryTimeToLog("min-query-time-to-log", + cl::init(0), + cl::value_desc("milliseconds"), + cl::desc("Set time threshold (in ms) for queries logged in files. " + "Only queries longer than threshold will be logged. (default=0)")); + } static std::string escapedString(const char *start, unsigned length) { @@ -186,7 +197,7 @@ static bool EvaluateInputAST(const char *Filename, Solver *S, *STP = S = UseDummySolver ? createDummySolver() : new STPSolver(true); if (UseSTPQueryPCLog) - S = createPCLoggingSolver(S, "stp-queries.pc"); + S = createPCLoggingSolver(S, "stp-queries.pc", MinQueryTimeToLog); if (UseFastCexSolver) S = createFastCexSolver(S); S = createCexCachingSolver(S); |