diff options
| -rw-r--r-- | lib/Solver/QueryLoggingSolver.cpp | 186 | ||||
| -rw-r--r-- | lib/Solver/QueryLoggingSolver.h | 77 |
2 files changed, 263 insertions, 0 deletions
diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp new file mode 100644 index 00000000..245ad3bf --- /dev/null +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -0,0 +1,186 @@ +//===-- QueryLoggingSolver.cpp --------------------------------------------===// + +#include "QueryLoggingSolver.h" +#include "klee/Internal/System/Time.h" +#include "klee/Statistics.h" + +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +using namespace klee::util; + +QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, + std::string path, + const std::string& commentSign, + int queryTimeToLog) + : solver(_solver), + os(path.c_str(), std::ios::trunc), + logBuffer(""), + queryCount(0), + minQueryTimeToLog(queryTimeToLog), + startTime(0.0f), + lastQueryTime(0.0f), + queryCommentSign(commentSign) { + assert(0 != solver); +} + +QueryLoggingSolver::~QueryLoggingSolver() { + delete solver; +} + +void QueryLoggingSolver::startQuery(const Query& query, const char* typeName, + const Query* falseQuery, + const std::vector<const Array*> *objects) { + Statistic *S = theStatisticManager->getStatisticByName("Instructions"); + uint64_t instructions = S ? S->getValue() : 0; + + logBuffer << queryCommentSign << " Query " << queryCount++ << " -- " + << "Type: " << typeName << ", " + << "Instructions: " << instructions << "\n"; + + printQuery(query, falseQuery, objects); + + startTime = getWallTime(); + +} + +void QueryLoggingSolver::finishQuery(bool success) { + lastQueryTime = getWallTime() - startTime; + logBuffer << queryCommentSign << " " << (success ? "OK" : "FAIL") << " -- " + << "Elapsed: " << lastQueryTime << "\n"; + + if (false == success) { + logBuffer << queryCommentSign << " Failure reason: " + << SolverImpl::getOperationStatusString(solver->impl->getOperationStatusCode()) + << "\n"; + } +} + +void QueryLoggingSolver::flushBuffer() { + 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) || + (SOLVER_RUN_STATUS_TIMEOUT == (solver->impl->getOperationStatusCode()))) { + // 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(""); +} + +bool QueryLoggingSolver::computeTruth(const Query& query, bool& isValid) { + startQuery(query, "Truth"); + + bool success = solver->impl->computeTruth(query, isValid); + + finishQuery(success); + + if (success) { + logBuffer << queryCommentSign << " Is Valid: " + << (isValid ? "true" : "false") << "\n"; + } + logBuffer << "\n"; + + flushBuffer(); + + return success; +} + +bool QueryLoggingSolver::computeValidity(const Query& query, + Solver::Validity& result) { + startQuery(query, "Validity"); + + bool success = solver->impl->computeValidity(query, result); + + finishQuery(success); + + if (success) { + logBuffer << queryCommentSign << " Validity: " + << result << "\n"; + } + logBuffer << "\n"; + + flushBuffer(); + + return success; +} + +bool QueryLoggingSolver::computeValue(const Query& query, ref<Expr>& result) { + Query withFalse = query.withFalse(); + startQuery(query, "Value", &withFalse); + + bool success = solver->impl->computeValue(query, result); + + finishQuery(success); + + if (success) { + logBuffer << queryCommentSign << " Result: " << result << "\n"; + } + logBuffer << "\n"; + + flushBuffer(); + + return success; +} + +bool QueryLoggingSolver::computeInitialValues(const Query& query, + const std::vector<const Array*>& objects, + std::vector<std::vector<unsigned char> >& values, + bool& hasSolution) { + startQuery(query, "InitialValues", 0, &objects); + + bool success = solver->impl->computeInitialValues(query, objects, + values, hasSolution); + + finishQuery(success); + + if (success) { + logBuffer << queryCommentSign << " 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 << queryCommentSign << " " << 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; +} + +SolverImpl::SolverRunStatus QueryLoggingSolver::getOperationStatusCode() { + return solver->impl->getOperationStatusCode(); +} + + diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h new file mode 100644 index 00000000..527d075b --- /dev/null +++ b/lib/Solver/QueryLoggingSolver.h @@ -0,0 +1,77 @@ +//===-- QueryLoggingSolver.h ---------------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_QUERYLOGGINGSOLVER_H +#define KLEE_QUERYLOGGINGSOLVER_H + +#include "klee/Solver.h" +#include "klee/SolverImpl.h" +#include <fstream> +#include <sstream> + +using namespace klee; + +/// This abstract class represents a solver that is capable of logging +/// queries to a file. +/// Derived classes might specialize this one by providing different formats +/// for the query output. +class QueryLoggingSolver : public SolverImpl { + +protected: + Solver *solver; + std::ofstream os; + std::ostringstream logBuffer; // buffer to store logs before flushing to + // file + unsigned queryCount; + int minQueryTimeToLog; // we log to file only those queries + // which take longer than the specified time (ms); + // if this param is negative, log only those queries + // on which the solver has timed out + + double startTime; + double lastQueryTime; + const std::string queryCommentSign; // sign representing commented lines + // in given a query format + + virtual void startQuery(const Query& query, const char* typeName, + const Query* falseQuery = 0, + const std::vector<const Array*>* objects = 0); + + virtual void finishQuery(bool success); + + /// 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); + + virtual void printQuery(const Query& query, + const Query* falseQuery = 0, + const std::vector<const Array*>* objects = 0) = 0; + +public: + QueryLoggingSolver(Solver *_solver, + std::string path, + const std::string& commentSign, + int queryTimeToLog); + + virtual ~QueryLoggingSolver(); + + /// implementation of the SolverImpl interface + bool computeTruth(const Query& query, bool &isValid); + bool computeValidity(const Query& query, Solver::Validity &result); + bool computeValue(const Query& query, ref<Expr> &result); + bool computeInitialValues(const Query& query, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution); + SolverRunStatus getOperationStatusCode(); + +}; + +#endif /* KLEE_QUERYLOGGINGSOLVER_H */ + |