diff options
Diffstat (limited to 'lib/Solver/SMTLIBLoggingSolver.cpp')
| -rw-r--r-- | lib/Solver/SMTLIBLoggingSolver.cpp | 181 |
1 files changed, 38 insertions, 143 deletions
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)); } |