Commit c6f16dd3 authored by Cristian Cadar's avatar Cristian Cadar Committed by Daniel Liew
Browse files

Patch by Dan Liew which improves the logging options: "Removed

-use-query-pc-log and -use-stp-query-pc-log and replaced with better
command line option -use-query-log=option.  Multiple comma seperated
options can be specified after -use-query-log=.  In addition queries
can now be logged in SMT-LIBv2 format as well as KQuery format. The
names of logging files has changed and also KLEE now informs users
which files are being written to.

Because of the changes the test/Feature/ExprLogging.c test broke so it
was necessary to fix it."

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166565 91177308-0d34-0410-b5e6-96231b3b80d8

Conflicts:

	lib/Core/Executor.cpp
parent bee97262
......@@ -168,14 +168,6 @@ namespace {
cl::init(true),
cl::desc("Use counterexample caching"));
cl::opt<bool>
UseQueryPCLog("use-query-pc-log",
cl::init(false));
cl::opt<bool>
UseSTPQueryPCLog("use-stp-query-pc-log",
cl::init(false));
cl::opt<bool>
UseFPRewriter("use-fp-rewriter",
cl::init(false));
......@@ -280,27 +272,63 @@ namespace {
cl::desc("fork when various schedules are possible (defaul=disabled)"),
cl::init(false));
/* Using cl::list<> instead of cl::bits<> results in quite a bit of ugliness when it comes to checking
* if an option is set. Unfortunately with gcc4.7 cl::bits<> is broken with LLVM2.9 and I doubt everyone
* wants to patch their copy of LLVM just for these options.
*/
cl::list<klee::QueryLoggingSolver> queryLoggingOptions("use-query-log",
cl::desc("Log queries to a file. Multiple options can be specified seperate by a comma. By default nothing is logged."),
cl::values(
clEnumValN(klee::ALL_PC,"all:pc","All queries in .pc (KQuery) format"),
clEnumValN(klee::ALL_SMTLIB,"all:smt2","All queries in .smt2 (SMT-LIBv2) format"),
clEnumValN(klee::SOLVER_PC,"solver:pc","All queries reaching the solver in .pc (KQuery) format"),
clEnumValN(klee::SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .pc (SMT-LIBv2) format"),
clEnumValEnd
), cl::CommaSeparated
);
}
namespace klee {
RNG theRNG;
//A bit of ugliness so we can use cl::list<> like cl::bits<>, see queryLoggingOptions
template <typename T>
static bool optionIsSet(cl::list<T> list, T option)
{
return std::find(list.begin(), list.end(), option) != list.end();
}
}
Solver *constructSolverChain(STPSolver *stpSolver,
std::string queryLogPath,
std::string stpQueryLogPath,
std::string querySMT2LogPath,
std::string baseSolverQuerySMT2LogPath,
std::string queryPCLogPath,
std::string stpQueryPCLogPath) {
std::string baseSolverQueryPCLogPath) {
Solver *solver = stpSolver;
if (UseFPRewriter)
solver = createFPRewritingSolver(solver);
if (UseSTPQueryPCLog)
if (optionIsSet(queryLoggingOptions,SOLVER_PC))
{
solver = createPCLoggingSolver(solver,
stpQueryLogPath);
baseSolverQueryPCLogPath);
klee_message("Logging queries that reach solver in .pc format to %s",baseSolverQueryPCLogPath.c_str());
}
if (optionIsSet(queryLoggingOptions,SOLVER_SMTLIB))
{
solver = createSMTLIBLoggingSolver(solver,baseSolverQuerySMT2LogPath);
klee_message("Logging queries that reach solver in .smt2 format to %s",baseSolverQuerySMT2LogPath.c_str());
}
if (UseFPRewriter)
solver = createFPRewritingSolver(solver);
if (UseFastCexSolver)
solver = createFastCexSolver(solver);
......@@ -316,10 +344,19 @@ Solver *constructSolverChain(STPSolver *stpSolver,
if (DebugValidateSolver)
solver = createValidatingSolver(solver, stpSolver);
if (UseQueryPCLog)
if (optionIsSet(queryLoggingOptions,ALL_PC))
{
solver = createPCLoggingSolver(solver,
queryPCLogPath);
klee_message("Logging all queries in .pc format to %s",queryPCLogPath.c_str());
}
if (optionIsSet(queryLoggingOptions,ALL_SMTLIB))
{
solver = createSMTLIBLoggingSolver(solver,querySMT2LogPath);
klee_message("Logging all queries in .smt2 format to %s",querySMT2LogPath.c_str());
}
return solver;
}
......@@ -484,10 +521,10 @@ Executor::Executor(const InterpreterOptions &opts,
STPSolver *stpSolver = new STPSolver(UseForkedSTP, STPOptimizeDivides);
Solver *solver =
constructSolverChain(stpSolver,
interpreterHandler->getOutputFilename("queries.qlog"),
interpreterHandler->getOutputFilename("stp-queries.qlog"),
interpreterHandler->getOutputFilename("queries.pc"),
interpreterHandler->getOutputFilename("stp-queries.pc"));
interpreterHandler->getOutputFilename("all-queries.smt2"),
interpreterHandler->getOutputFilename("solver-queries.smt2"),
interpreterHandler->getOutputFilename("all-queries.pc"),
interpreterHandler->getOutputFilename("solver-queries.pc"));
this->solver = new TimingSolver(solver, stpSolver);
......
......@@ -82,6 +82,16 @@ namespace klee {
enum ESD_LOCK_TYPE {LOCK, UNLOCK};
///The different query logging solvers that can switched on/off
enum QueryLoggingSolver
{
ALL_PC, ///< Log all queries (un-optimised) in .pc (KQuery) format
ALL_SMTLIB, ///< Log all queries (un-optimised) .smt2 (SMT-LIBv2) format
SOLVER_PC, ///< Log queries passed to solver (optimised) in .pc (KQuery) format
SOLVER_SMTLIB ///< Log queries passed to solver (optimised) in .smt2 (SMT-LIBv2) format
};
/// \todo Add a context object to keep track of data only live
/// during an instruction step. Should contain addedStates,
/// removedStates, and haltExecution, among others.
......
// RUN: %llvmgcc %s -emit-llvm -g -O0 -c -o %t1.bc
// RUN: %klee --use-query-pc-log --write-pcs --write-cvcs %t1.bc 2> %t2.log
// RUN: %kleaver -print-ast klee-last/queries.pc > %t3.log
// RUN: %klee --use-query-log=all:pc --write-pcs --write-cvcs %t1.bc 2> %t2.log
// RUN: %kleaver -print-ast klee-last/all-queries.pc > %t3.log
// RUN: %kleaver -print-ast %t3.log > %t4.log
// RUN: diff %t3.log %t4.log
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment