From d369654e361782b3f4a52303114db11959a346f7 Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Wed, 2 Jan 2013 14:49:59 +0000 Subject: Patch by Tomasz Kuchta that refactors the logging code, by introducing a new logging class hierarchy. git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@171387 91177308-0d34-0410-b5e6-96231b3b80d8 --- lib/Solver/PCLoggingSolver.cpp | 211 +++++++------------------------------ lib/Solver/SMTLIBLoggingSolver.cpp | 181 +++++++------------------------ 2 files changed, 76 insertions(+), 316 deletions(-) (limited to 'lib/Solver') 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 -#include -#include 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 *evalExprsBegin = 0, - const ref *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* objects = 0) { + + const ref* evalExprsBegin = 0; + const ref* 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(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 &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 &objects, - std::vector< std::vector > &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 >::iterator - values_it = values.begin(); - for (std::vector::const_iterator i = objects.begin(), - e = objects.end(); i != e; ++i, ++values_it) { - const Array *array = *i; - std::vector &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 - 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* 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* 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 &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 &objects, - std::vector< std::vector > &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 >::iterator - values_it = values.begin(); - for (std::vector::const_iterator i = objects.begin(), - e = objects.end(); i != e; ++i, ++values_it) - { - const Array *array = *i; - std::vector &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)); } -- cgit 1.4.1