diff options
| -rw-r--r-- | include/klee/Solver.h | 5 | ||||
| -rw-r--r-- | lib/Solver/SMTLIBLoggingSolver.cpp | 167 |
2 files changed, 172 insertions, 0 deletions
diff --git a/include/klee/Solver.h b/include/klee/Solver.h index b87b6dc3..4cedf47d 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -215,6 +215,11 @@ namespace klee { /// after writing them to the given path in .pc format. Solver *createPCLoggingSolver(Solver *s, std::string path); + /// 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); + + /// createDummySolver - Create a dummy solver implementation which always /// fails. Solver *createDummySolver(); diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp new file mode 100644 index 00000000..0fb09424 --- /dev/null +++ b/lib/Solver/SMTLIBLoggingSolver.cpp @@ -0,0 +1,167 @@ +//===-- SMTLIBLoggingSolver.cpp -----------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "klee/Solver.h" + +#include "klee/Expr.h" +#include "klee/SolverImpl.h" +#include "klee/Statistics.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 +{ + 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"; + } + + public: + SMTLIBLoggingSolver(Solver *_solver, std::string path) + : solver(_solver), + os(path.c_str(), std::ios::trunc), + printer(), + queryCount(0), + startTime(0) + { + //Setup the printer + printer = createSMTLIBPrinter(); + printer->setOutput(os); + } + + ~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; + } +}; + + +Solver* klee::createSMTLIBLoggingSolver(Solver *_solver, std::string path) +{ + return new Solver(new SMTLIBLoggingSolver(_solver, path)); +} |