diff options
| -rw-r--r-- | include/klee/Solver.h | 3 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 6 | ||||
| -rw-r--r-- | lib/Solver/PCLoggingSolver.cpp | 211 | ||||
| -rw-r--r-- | lib/Solver/SMTLIBLoggingSolver.cpp | 181 | ||||
| -rw-r--r-- | test/Feature/ExprLogging.c | 4 |
5 files changed, 84 insertions, 321 deletions
diff --git a/include/klee/Solver.h b/include/klee/Solver.h index db14f003..94e7d477 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -218,7 +218,8 @@ namespace klee { /// createSMTLIBLoggingSolver - Create a solver which will forward all queries /// after writing them to the given path in .smt2 format. - Solver *createSMTLIBLoggingSolver(Solver *s, std::string path); + Solver *createSMTLIBLoggingSolver(Solver *s, std::string path, + int minQueryTimeToLog); /// createDummySolver - Create a dummy solver implementation which always diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index b8db18fe..5803e6ff 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -317,7 +317,8 @@ Solver *constructSolverChain(STPSolver *stpSolver, if (optionIsSet(queryLoggingOptions,SOLVER_SMTLIB)) { - solver = createSMTLIBLoggingSolver(solver,baseSolverQuerySMT2LogPath); + solver = createSMTLIBLoggingSolver(solver,baseSolverQuerySMT2LogPath, + MinQueryTimeToLog); klee_message("Logging queries that reach solver in .smt2 format to %s",baseSolverQuerySMT2LogPath.c_str()); } @@ -346,7 +347,8 @@ Solver *constructSolverChain(STPSolver *stpSolver, if (optionIsSet(queryLoggingOptions,ALL_SMTLIB)) { - solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath); + solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath, + MinQueryTimeToLog); klee_message("Logging all queries in .smt2 format to %s",querySMT2LogPath.c_str()); } diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/PCLoggingSolver.cpp index 0b31182e..67e9be45 100644 --- a/lib/Solver/PCLoggingSolver.cpp +++ b/lib/Solver/PCLoggingSolver.cpp @@ -7,192 +7,57 @@ // //===----------------------------------------------------------------------===// -#include "klee/Solver.h" +#include "QueryLoggingSolver.h" #include "klee/Expr.h" -#include "klee/SolverImpl.h" -#include "klee/Statistics.h" #include "klee/util/ExprPPrinter.h" #include "klee/Internal/Support/QueryLog.h" -#include "klee/Internal/System/Time.h" -#include "llvm/Support/CommandLine.h" - -#include <fstream> -#include <sstream> -#include <iostream> using namespace klee; -using namespace llvm; -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, - const ref<Expr> *evalExprsEnd = 0, - const Array * const* evalArraysBegin = 0, - const Array * const* evalArraysEnd = 0) { - Statistic *S = theStatisticManager->getStatisticByName("Instructions"); - uint64_t instructions = S ? S->getValue() : 0; - - 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) { - lastQueryTime = getWallTime() - startTime; - logBuffer << "# " << (success ? "OK" : "FAIL") << " -- " - << "Elapsed: " << lastQueryTime << "\n"; - - if (true == solver->impl->hasTimeoutOccurred()) { - logBuffer << "\nSolver TIMEOUT detected\n"; +class PCLoggingSolver : public QueryLoggingSolver { + +private : + ExprPPrinter *printer; + + virtual void printQuery(const Query& query, + const Query* falseQuery = 0, + const std::vector<const Array*>* objects = 0) { + + const ref<Expr>* evalExprsBegin = 0; + const ref<Expr>* evalExprsEnd = 0; + + if (0 != falseQuery) { + evalExprsBegin = &query.expr; + evalExprsEnd = &query.expr + 1; + } + + const Array* const *evalArraysBegin = 0; + const Array* const *evalArraysEnd = 0; + + if ((0 != objects) && (false == objects->empty())) { + evalArraysBegin = &((*objects)[0]); + evalArraysEnd = &((*objects)[0]) + objects->size(); + } + + const Query* q = (0 == falseQuery) ? &query : falseQuery; + + printer->printQuery(logBuffer, q->constraints, q->expr, + evalExprsBegin, evalExprsEnd, + evalArraysBegin, evalArraysEnd); } - } - - /// 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, int queryTimeToLog) - : solver(_solver), - os(path.c_str(), std::ios::trunc), - logBuffer(""), - printer(ExprPPrinter::create(logBuffer)), - queryCount(0), - minQueryTimeToLog(queryTimeToLog), - startTime(0.0f), - lastQueryTime(0.0f) { - } - ~PCLoggingSolver() { - delete printer; - delete solver; - } - - bool computeTruth(const Query& query, bool &isValid) { - startQuery(query, "Truth"); - bool success = solver->impl->computeTruth(query, isValid); - finishQuery(success); - if (success) - logBuffer << "# Is Valid: " << (isValid ? "true" : "false") << "\n"; - logBuffer << "\n"; - - flushBuffer(); + PCLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog) + : QueryLoggingSolver(_solver, path, "#", queryTimeToLog), + printer(ExprPPrinter::create(logBuffer)) { + } - return success; - } - - bool computeValidity(const Query& query, Solver::Validity &result) { - startQuery(query, "Validity"); - bool success = solver->impl->computeValidity(query, result); - finishQuery(success); - if (success) - logBuffer << "# Validity: " << result << "\n"; - logBuffer << "\n"; - - flushBuffer(); - - return success; - } - - bool computeValue(const Query& query, ref<Expr> &result) { - startQuery(query.withFalse(), "Value", - &query.expr, &query.expr + 1); - bool success = solver->impl->computeValue(query, result); - finishQuery(success); - if (success) - logBuffer << "# Result: " << result << "\n"; - logBuffer << "\n"; - - flushBuffer(); - - return success; - } - - bool computeInitialValues(const Query& query, - const std::vector<const Array*> &objects, - std::vector< std::vector<unsigned char> > &values, - bool &hasSolution) { - if (objects.empty()) { - startQuery(query, "InitialValues", - 0, 0); - } else { - startQuery(query, "InitialValues", - 0, 0, - &objects[0], &objects[0] + objects.size()); - } - bool success = solver->impl->computeInitialValues(query, objects, - values, hasSolution); - finishQuery(success); - if (success) { - logBuffer << "# Solvable: " << (hasSolution ? "true" : "false") << "\n"; - if (hasSolution) { - std::vector< std::vector<unsigned char> >::iterator - values_it = values.begin(); - for (std::vector<const Array*>::const_iterator i = objects.begin(), - e = objects.end(); i != e; ++i, ++values_it) { - const Array *array = *i; - std::vector<unsigned char> &data = *values_it; - logBuffer << "# " << array->name << " = ["; - for (unsigned j = 0; j < array->size; j++) { - logBuffer << (int) data[j]; - if (j+1 < array->size) - logBuffer << ","; - } - logBuffer << "]\n"; - } - } - } - logBuffer << "\n"; - - flushBuffer(); - - return success; - } - - bool hasTimeoutOccurred() { - return solver->impl->hasTimeoutOccurred(); - } + virtual ~PCLoggingSolver() { + delete printer; + } }; /// diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp index b3f7eb3b..f64e11e0 100644 --- a/lib/Solver/SMTLIBLoggingSolver.cpp +++ b/lib/Solver/SMTLIBLoggingSolver.cpp @@ -1,4 +1,4 @@ -//===-- SMTLIBLoggingSolver.cpp -----------------------------------------------===// +//===-- SMTLIBLoggingSolver.cpp -------------------------------------------===// // // The KLEE Symbolic Virtual Machine // @@ -7,166 +7,61 @@ // //===----------------------------------------------------------------------===// -#include "klee/Solver.h" - -#include "klee/Expr.h" -#include "klee/SolverImpl.h" -#include "klee/Statistics.h" - +#include "QueryLoggingSolver.h" #include "klee/util/ExprSMTLIBLetPrinter.h" -#include "klee/Internal/Support/QueryLog.h" -#include "klee/Internal/System/Time.h" - -#include "llvm/Support/CommandLine.h" - -#include <fstream> - using namespace klee; -using namespace llvm; -using namespace klee::util; -///This SolverImpl will log queries to a file in the SMTLIBv2 format -///and pass the query down to the underlying solver. -/// -///This is basically just a "copy" of PCLoggingSolver with a few modifications. -class SMTLIBLoggingSolver : public SolverImpl +/// This QueryLoggingSolver will log queries to a file in the SMTLIBv2 format +/// and pass the query down to the underlying solver. +class SMTLIBLoggingSolver : public QueryLoggingSolver { - Solver *solver; - std::ofstream os; - ExprSMTLIBPrinter* printer; - unsigned queryCount; - double startTime; - - void startQuery(const Query& query, const char *typeName, const std::vector<const Array*>* objects=NULL) - { - Statistic *S = theStatisticManager->getStatisticByName("Instructions"); - uint64_t instructions = S ? S->getValue() : 0; - os << ";SMTLIBv2 Query " << queryCount++ << " -- " - << "Type: " << typeName << ", " - << "Instructions: " << instructions << "\n"; - printer->setQuery(query); - - if(objects!=NULL) - printer->setArrayValuesToGet(*objects); - - printer->generateOutput(); - os << "\n"; - - startTime = getWallTime(); - } - - void finishQuery(bool success) - { - double delta = getWallTime() - startTime; - os << "; " << (success ? "OK" : "FAIL") << " -- " - << "Elapsed: " << delta << "\n"; - } + private: + + ExprSMTLIBPrinter* printer; + virtual void printQuery(const Query& query, + const Query* falseQuery = 0, + const std::vector<const Array*>* objects = 0) + { + if (0 == falseQuery) + { + printer->setQuery(query); + } + else + { + printer->setQuery(*falseQuery); + } + + if (0 != objects) + { + printer->setArrayValuesToGet(*objects); + } + + printer->generateOutput(); + } + public: - SMTLIBLoggingSolver(Solver *_solver, std::string path) - : solver(_solver), - os(path.c_str(), std::ios::trunc), - printer(), - queryCount(0), - startTime(0) + SMTLIBLoggingSolver(Solver *_solver, + std::string path, + int queryTimeToLog) + : QueryLoggingSolver(_solver, path, ";", queryTimeToLog), + printer() { //Setup the printer printer = createSMTLIBPrinter(); - printer->setOutput(os); + printer->setOutput(logBuffer); } ~SMTLIBLoggingSolver() { delete printer; - delete solver; - } - - bool computeTruth(const Query& query, bool &isValid) - { - startQuery(query, "Truth"); - bool success = solver->impl->computeTruth(query, isValid); - finishQuery(success); - if (success) - os << "; Is Valid: " << (isValid ? "true" : "false") << "\n"; - os << "\n"; - return success; - } - - bool computeValidity(const Query& query, Solver::Validity &result) - { - startQuery(query, "Validity"); - bool success = solver->impl->computeValidity(query, result); - finishQuery(success); - if (success) - os << "; Validity: " << result << "\n"; - os << "\n"; - return success; - } - - bool computeValue(const Query& query, ref<Expr> &result) - { - startQuery(query.withFalse(), "Value"); - - bool success = solver->impl->computeValue(query, result); - finishQuery(success); - if (success) - os << "; Result: " << result << "\n"; - os << "\n"; - return success; - } - - bool computeInitialValues(const Query& query, - const std::vector<const Array*> &objects, - std::vector< std::vector<unsigned char> > &values, - bool &hasSolution) - { - - startQuery(query, "InitialValues", &objects); - - - bool success = solver->impl->computeInitialValues(query, objects, - values, hasSolution); - finishQuery(success); - if (success) - { - os << "; Solvable: " << (hasSolution ? "true" : "false") << "\n"; - - if (hasSolution) - { - std::vector< std::vector<unsigned char> >::iterator - values_it = values.begin(); - for (std::vector<const Array*>::const_iterator i = objects.begin(), - e = objects.end(); i != e; ++i, ++values_it) - { - const Array *array = *i; - std::vector<unsigned char> &data = *values_it; - os << "; " << array->name << " = ["; - - for (unsigned j = 0; j < array->size; j++) - { - os << (int) data[j]; - if (j+1 < array->size) - os << ","; - } - - os << "]\n"; - } - } - } - - os << "\n"; - return success; } - - bool hasTimeoutOccurred() - { - return solver->impl->hasTimeoutOccurred(); - } }; -Solver* klee::createSMTLIBLoggingSolver(Solver *_solver, std::string path) +Solver* klee::createSMTLIBLoggingSolver(Solver *_solver, std::string path, + int minQueryTimeToLog) { - return new Solver(new SMTLIBLoggingSolver(_solver, path)); + return new Solver(new SMTLIBLoggingSolver(_solver, path, minQueryTimeToLog)); } diff --git a/test/Feature/ExprLogging.c b/test/Feature/ExprLogging.c index d8dfe4b4..ad671a5e 100644 --- a/test/Feature/ExprLogging.c +++ b/test/Feature/ExprLogging.c @@ -6,8 +6,8 @@ // RUN: %kleaver -print-ast klee-last/solver-queries.pc > %t3.log // RUN: %kleaver -print-ast %t3.log > %t4.log // RUN: diff %t3.log %t4.log -// RUN: grep "^;SMTLIBv2 Query" klee-last/all-queries.smt2 | wc -l | grep -q 17 -// RUN: grep "^;SMTLIBv2 Query" klee-last/solver-queries.smt2 | wc -l | grep -q 10 +// RUN: grep "^; Query" klee-last/all-queries.smt2 | wc -l | grep -q 17 +// RUN: grep "^; Query" klee-last/solver-queries.smt2 | wc -l | grep -q 10 #include <assert.h> |