From f27cf86466d75c71a302abe5e0a3ffcad1670373 Mon Sep 17 00:00:00 2001 From: Eric Rizzi Date: Mon, 14 Sep 2015 14:32:37 -0400 Subject: Renamed .pc to .kquery (kleaver query) --- lib/Basic/CmdLineOptions.cpp | 4 +-- lib/Basic/ConstructSolverChain.cpp | 24 +++++++------ lib/Core/Executor.cpp | 5 +-- lib/SMT/SMTParser.cpp | 6 ++-- lib/Solver/CMakeLists.txt | 2 +- lib/Solver/KQueryLoggingSolver.cpp | 69 ++++++++++++++++++++++++++++++++++++++ lib/Solver/PCLoggingSolver.cpp | 68 ------------------------------------- 7 files changed, 91 insertions(+), 87 deletions(-) create mode 100644 lib/Solver/KQueryLoggingSolver.cpp delete mode 100644 lib/Solver/PCLoggingSolver.cpp (limited to 'lib') diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp index 399c27a2..e55c4550 100644 --- a/lib/Basic/CmdLineOptions.cpp +++ b/lib/Basic/CmdLineOptions.cpp @@ -73,9 +73,9 @@ llvm::cl::list queryLoggingOptions( "use-query-log", llvm::cl::desc("Log queries to a file. Multiple options can be specified separated by a comma. By default nothing is logged."), llvm::cl::values( - clEnumValN(ALL_PC,"all:pc","All queries in .pc (KQuery) format"), + clEnumValN(ALL_KQUERY,"all:kquery","All queries in .kquery (KQuery) format"), clEnumValN(ALL_SMTLIB,"all:smt2","All queries in .smt2 (SMT-LIBv2) format"), - clEnumValN(SOLVER_PC,"solver:pc","All queries reaching the solver in .pc (KQuery) format"), + clEnumValN(SOLVER_KQUERY,"solver:kquery","All queries reaching the solver in .kquery (KQuery) format"), clEnumValN(SOLVER_SMTLIB,"solver:smt2","All queries reaching the solver in .smt2 (SMT-LIBv2) format"), clEnumValEnd ), diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp index debb1e9e..68e1b08b 100644 --- a/lib/Basic/ConstructSolverChain.cpp +++ b/lib/Basic/ConstructSolverChain.cpp @@ -16,17 +16,18 @@ #include "llvm/Support/raw_ostream.h" namespace klee { -Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath, +Solver *constructSolverChain(Solver *coreSolver, + std::string querySMT2LogPath, std::string baseSolverQuerySMT2LogPath, - std::string queryPCLogPath, - std::string baseSolverQueryPCLogPath) { + std::string queryKQueryLogPath, + std::string baseSolverQueryKQueryLogPath) { Solver *solver = coreSolver; - if (optionIsSet(queryLoggingOptions, SOLVER_PC)) { - solver = createPCLoggingSolver(solver, baseSolverQueryPCLogPath, + if (optionIsSet(queryLoggingOptions, SOLVER_KQUERY)) { + solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath, MinQueryTimeToLog); - klee_message("Logging queries that reach solver in .pc format to %s\n", - baseSolverQueryPCLogPath.c_str()); + klee_message("Logging queries that reach solver in .kquery format to %s\n", + baseSolverQueryKQueryLogPath.c_str()); } if (optionIsSet(queryLoggingOptions, SOLVER_SMTLIB)) { @@ -51,10 +52,11 @@ Solver *constructSolverChain(Solver *coreSolver, std::string querySMT2LogPath, if (DebugValidateSolver) solver = createValidatingSolver(solver, coreSolver); - if (optionIsSet(queryLoggingOptions, ALL_PC)) { - solver = createPCLoggingSolver(solver, queryPCLogPath, MinQueryTimeToLog); - klee_message("Logging all queries in .pc format to %s\n", - queryPCLogPath.c_str()); + if (optionIsSet(queryLoggingOptions, ALL_KQUERY)) { + solver = createKQueryLoggingSolver(solver, queryKQueryLogPath, + MinQueryTimeToLog); + klee_message("Logging all queries in .kquery format to %s\n", + queryKQueryLogPath.c_str()); } if (optionIsSet(queryLoggingOptions, ALL_SMTLIB)) { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 0981b8f4..1f3c1939 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -353,12 +353,13 @@ Executor::Executor(const InterpreterOptions &opts, InterpreterHandler *ih) if (!coreSolver) { klee_error("Failed to create core solver\n"); } + Solver *solver = constructSolverChain( coreSolver, interpreterHandler->getOutputFilename(ALL_QUERIES_SMT2_FILE_NAME), interpreterHandler->getOutputFilename(SOLVER_QUERIES_SMT2_FILE_NAME), - interpreterHandler->getOutputFilename(ALL_QUERIES_PC_FILE_NAME), - interpreterHandler->getOutputFilename(SOLVER_QUERIES_PC_FILE_NAME)); + interpreterHandler->getOutputFilename(ALL_QUERIES_KQUERY_FILE_NAME), + interpreterHandler->getOutputFilename(SOLVER_QUERIES_KQUERY_FILE_NAME)); this->solver = new TimingSolver(solver, EqualitySubstitution); memory = new MemoryManager(&arrayCache); diff --git a/lib/SMT/SMTParser.cpp b/lib/SMT/SMTParser.cpp index eefe443a..19ce5af7 100644 --- a/lib/SMT/SMTParser.cpp +++ b/lib/SMT/SMTParser.cpp @@ -67,11 +67,11 @@ Decl* SMTParser::ParseTopLevelDecl() { bool SMTParser::Solve() { // FIXME: Support choice of solver. - bool UseDummySolver = false, UseFastCexSolver = true, UseSTPQueryPCLog = true; + bool UseDummySolver = false, UseFastCexSolver = true, UseSTPQueryKQueryLog = true; Solver *S, *STP = S = UseDummySolver ? createDummySolver() : new STPSolver(true); - if (UseSTPQueryPCLog) - S = createPCLoggingSolver(S, "stp-queries.pc"); + if (UseSTPQueryKQueryLog) + S = createKQueryLoggingSolver(S, "stp-queries.kquery"); if (UseFastCexSolver) S = createFastCexSolver(S); S = createCexCachingSolver(S); diff --git a/lib/Solver/CMakeLists.txt b/lib/Solver/CMakeLists.txt index 20da74da..1302db38 100644 --- a/lib/Solver/CMakeLists.txt +++ b/lib/Solver/CMakeLists.txt @@ -16,7 +16,7 @@ klee_add_component(kleaverSolver IncompleteSolver.cpp IndependentSolver.cpp MetaSMTSolver.cpp - PCLoggingSolver.cpp + KQueryLoggingSolver.cpp QueryLoggingSolver.cpp SMTLIBLoggingSolver.cpp Solver.cpp diff --git a/lib/Solver/KQueryLoggingSolver.cpp b/lib/Solver/KQueryLoggingSolver.cpp new file mode 100644 index 00000000..a0ac950c --- /dev/null +++ b/lib/Solver/KQueryLoggingSolver.cpp @@ -0,0 +1,69 @@ +//===-- KQueryLoggingSolver.cpp -----------------------------------------------===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "QueryLoggingSolver.h" + +#include "klee/Expr.h" +#include "klee/util/ExprPPrinter.h" +#include "klee/Internal/Support/QueryLog.h" + +using namespace klee; + +/// + +class KQueryLoggingSolver : 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); + } + +public: + KQueryLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog) + : QueryLoggingSolver(_solver, path, "#", queryTimeToLog), + printer(ExprPPrinter::create(logBuffer)) { + } + + virtual ~KQueryLoggingSolver() { + delete printer; + } +}; + +/// + +Solver *klee::createKQueryLoggingSolver(Solver *_solver, std::string path, + int minQueryTimeToLog) { + return new Solver(new KQueryLoggingSolver(_solver, path, minQueryTimeToLog)); +} + diff --git a/lib/Solver/PCLoggingSolver.cpp b/lib/Solver/PCLoggingSolver.cpp deleted file mode 100644 index 67e9be45..00000000 --- a/lib/Solver/PCLoggingSolver.cpp +++ /dev/null @@ -1,68 +0,0 @@ -//===-- PCLoggingSolver.cpp -----------------------------------------------===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#include "QueryLoggingSolver.h" - -#include "klee/Expr.h" -#include "klee/util/ExprPPrinter.h" -#include "klee/Internal/Support/QueryLog.h" - -using namespace klee; - -/// - -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); - } - -public: - PCLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog) - : QueryLoggingSolver(_solver, path, "#", queryTimeToLog), - printer(ExprPPrinter::create(logBuffer)) { - } - - virtual ~PCLoggingSolver() { - delete printer; - } -}; - -/// - -Solver *klee::createPCLoggingSolver(Solver *_solver, std::string path, - int minQueryTimeToLog) { - return new Solver(new PCLoggingSolver(_solver, path, minQueryTimeToLog)); -} -- cgit 1.4.1