diff options
| -rw-r--r-- | include/klee/Interpreter.h | 9 | ||||
| -rw-r--r-- | lib/Core/Executor.cpp | 50 | ||||
| -rw-r--r-- | lib/Core/Executor.h | 2 | ||||
| -rw-r--r-- | tools/klee/main.cpp | 16 |
4 files changed, 63 insertions, 14 deletions
diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h index 8640869a..e29db411 100644 --- a/include/klee/Interpreter.h +++ b/include/klee/Interpreter.h @@ -58,6 +58,13 @@ public: CheckDivZero(_CheckDivZero) {} }; + enum LogType + { + STP, //.CVC (STP's native language) + KQUERY, //.PC files (kQuery native language) + SMTLIB2 //.SMT2 files (SMTLIB version 2 files) + }; + /// InterpreterOptions - Options varying the runtime behavior during /// interpretation. struct InterpreterOptions { @@ -132,7 +139,7 @@ public: virtual void getConstraintLog(const ExecutionState &state, std::string &res, - bool asCVC = false) = 0; + LogType logFormat = STP) = 0; virtual bool getSymbolicSolution(const ExecutionState &state, std::vector< diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 74769aa1..968283b7 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -32,6 +32,7 @@ #include "klee/TimerStatIncrementer.h" #include "klee/util/Assignment.h" #include "klee/util/ExprPPrinter.h" +#include "klee/util/ExprSMTLIBLetPrinter.h" #include "klee/util/ExprUtil.h" #include "klee/util/GetElementPtrTypeIterator.h" #include "klee/Config/Version.h" @@ -3373,17 +3374,46 @@ unsigned Executor::getSymbolicPathStreamID(const ExecutionState &state) { void Executor::getConstraintLog(const ExecutionState &state, std::string &res, - bool asCVC) { - if (asCVC) { - Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); - char *log = solver->stpSolver->getConstraintLog(query); - res = std::string(log); - free(log); - } else { - std::ostringstream info; - ExprPPrinter::printConstraints(info, state.constraints); - res = info.str(); + Interpreter::LogType logFormat) { + + std::ostringstream info; + + switch(logFormat) + { + case STP: + { + Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); + char *log = solver->stpSolver->getConstraintLog(query); + res = std::string(log); + free(log); + } + break; + + case KQUERY: + { + std::ostringstream info; + ExprPPrinter::printConstraints(info, state.constraints); + res = info.str(); + } + break; + + case SMTLIB2: + { + std::ostringstream info; + ExprSMTLIBPrinter* printer = createSMTLIBPrinter(); + printer->setOutput(info); + Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); + printer->setQuery(query); + printer->generateOutput(); + res = info.str(); + delete printer; } + break; + + default: + klee_warning("Executor::getConstraintLog() : Log format not supported!"); + } + } bool Executor::getSymbolicSolution(const ExecutionState &state, diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index f0c9f576..c86fe6ab 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -456,7 +456,7 @@ public: virtual void getConstraintLog(const ExecutionState &state, std::string &res, - bool asCVC = false); + Interpreter::LogType logFormat = Interpreter::STP); virtual bool getSymbolicSolution(const ExecutionState &state, std::vector< diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index dc335cd0..d28356bd 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -96,6 +96,10 @@ namespace { cl::desc("Write .pc files for each test case")); cl::opt<bool> + WriteSMT2s("write-smt2s", + cl::desc("Write .smt2 (SMT-LIBv2) files for each test case")); + + cl::opt<bool> WriteCov("write-cov", cl::desc("Write coverage information for each test case")); @@ -448,7 +452,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, if (errorMessage || WritePCs) { std::string constraints; - m_interpreter->getConstraintLog(state, constraints); + m_interpreter->getConstraintLog(state, constraints,Interpreter::KQUERY); std::ostream *f = openTestFile("pc", id); *f << constraints; delete f; @@ -456,12 +460,20 @@ void KleeHandler::processTestCase(const ExecutionState &state, if (WriteCVCs) { std::string constraints; - m_interpreter->getConstraintLog(state, constraints, true); + m_interpreter->getConstraintLog(state, constraints, Interpreter::STP); std::ostream *f = openTestFile("cvc", id); *f << constraints; delete f; } + if(WriteSMT2s) { + std::string constraints; + m_interpreter->getConstraintLog(state, constraints, Interpreter::SMTLIB2); + std::ostream *f = openTestFile("smt2", id); + *f << constraints; + delete f; + } + if (m_symPathWriter) { std::vector<unsigned char> symbolicBranches; m_symPathWriter->readStream(m_interpreter->getSymbolicPathStreamID(state), |