From 082e9d7bab796eda37624c026d8d006608625b90 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Wed, 23 Mar 2016 21:12:46 +0100 Subject: Fix comment + Clang Formatting --- lib/Solver/QueryLoggingSolver.h | 104 +++++++++++++++++++--------------------- 1 file changed, 50 insertions(+), 54 deletions(-) (limited to 'lib/Solver/QueryLoggingSolver.h') diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index ad1722ca..3068f2ab 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -1,4 +1,5 @@ -//===-- QueryLoggingSolver.h ---------------------------------------------------===// +//===-- QueryLoggingSolver.h +//---------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // @@ -8,75 +9,70 @@ //===----------------------------------------------------------------------===// #ifndef KLEE_QUERYLOGGINGSOLVER_H -#define KLEE_QUERYLOGGINGSOLVER_H +#define KLEE_QUERYLOGGINGSOLVER_H #include "klee/Solver.h" #include "klee/SolverImpl.h" #include "llvm/Support/raw_ostream.h" -#include -#include using namespace klee; -/// This abstract class represents a solver that is capable of logging +/// This abstract class represents a solver that is capable of logging /// queries to a file. /// Derived classes might specialize this one by providing different formats /// for the query output. class QueryLoggingSolver : public SolverImpl { protected: - Solver *solver; - std::string ErrorInfo; - llvm::raw_fd_ostream os; - // @brief Buffer used by logBuffer - std::string BufferString; - // @brief buffer to store logs before flushing to file - llvm::raw_string_ostream logBuffer; - unsigned queryCount; - int minQueryTimeToLog; // we log to file only those queries - // which take longer than the specified time (ms); - // if this param is negative, log only those queries - // on which the solver has timed out + Solver *solver; + std::string ErrorInfo; + llvm::raw_fd_ostream os; + // @brief Buffer used by logBuffer + std::string BufferString; + // @brief buffer to store logs before flushing to file + llvm::raw_string_ostream logBuffer; + unsigned queryCount; + int minQueryTimeToLog; // we log to file only those queries + // which take longer than the specified time (ms); + // if this param is negative, log only those queries + // on which the solver has timed out - double startTime; - double lastQueryTime; - const std::string queryCommentSign; // sign representing commented lines - // in given a query format + double startTime; + double lastQueryTime; + const std::string queryCommentSign; // sign representing commented lines + // in given a query format + + virtual void startQuery(const Query &query, const char *typeName, + const Query *falseQuery = 0, + const std::vector *objects = 0); + + virtual void finishQuery(bool success); + + /// flushBuffer - flushes the temporary logs buffer. Depending on threshold + /// settings, contents of the buffer are either discarded or written to a + /// file. + void flushBuffer(void); + + virtual void printQuery(const Query &query, const Query *falseQuery = 0, + const std::vector *objects = 0) = 0; - virtual void startQuery(const Query& query, const char* typeName, - const Query* falseQuery = 0, - const std::vector* objects = 0); - - virtual void finishQuery(bool success); - - /// flushBuffer - flushes the temporary logs buffer. Depending on threshold - /// settings, contents of the buffer are either discarded or written to a file. - void flushBuffer(void); - - virtual void printQuery(const Query& query, - const Query* falseQuery = 0, - const std::vector* objects = 0) = 0; - public: - QueryLoggingSolver(Solver *_solver, - std::string path, - const std::string& commentSign, - int queryTimeToLog); - - virtual ~QueryLoggingSolver(); + QueryLoggingSolver(Solver *_solver, std::string path, + const std::string &commentSign, int queryTimeToLog); - /// implementation of the SolverImpl interface - bool computeTruth(const Query& query, bool &isValid); - bool computeValidity(const Query& query, Solver::Validity &result); - bool computeValue(const Query& query, ref &result); - bool computeInitialValues(const Query& query, - const std::vector &objects, - std::vector< std::vector > &values, - bool &hasSolution); - SolverRunStatus getOperationStatusCode(); - char *getConstraintLog(const Query&); - void setCoreSolverTimeout(double timeout); -}; + virtual ~QueryLoggingSolver(); -#endif /* KLEE_QUERYLOGGINGSOLVER_H */ + /// implementation of the SolverImpl interface + bool computeTruth(const Query &query, bool &isValid); + bool computeValidity(const Query &query, Solver::Validity &result); + bool computeValue(const Query &query, ref &result); + bool computeInitialValues(const Query &query, + const std::vector &objects, + std::vector > &values, + bool &hasSolution); + SolverRunStatus getOperationStatusCode(); + char *getConstraintLog(const Query &); + void setCoreSolverTimeout(double timeout); +}; +#endif /* KLEE_QUERYLOGGINGSOLVER_H */ -- cgit 1.4.1 From 20eb0485850073fafdac07a630cededf8b99c536 Mon Sep 17 00:00:00 2001 From: Martin Nowack Date: Wed, 23 Mar 2016 21:48:12 +0100 Subject: Refactoring of conditional flush into own function. @delcypher: Thanks a lot Dan! --- lib/Solver/QueryLoggingSolver.cpp | 24 ++++++++++++++---------- lib/Solver/QueryLoggingSolver.h | 1 + 2 files changed, 15 insertions(+), 10 deletions(-) (limited to 'lib/Solver/QueryLoggingSolver.h') diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index 6084e2e1..f93bec3c 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -39,6 +39,16 @@ QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, QueryLoggingSolver::~QueryLoggingSolver() { delete solver; } +void QueryLoggingSolver::flushBufferConditionally(bool writeToFile) { + logBuffer.flush(); + if (writeToFile) { + os << logBuffer.str(); + os.flush(); + } + // prepare the buffer for reuse + BufferString = ""; +} + void QueryLoggingSolver::startQuery(const Query &query, const char *typeName, const Query *falseQuery, const std::vector *objects) { @@ -52,11 +62,7 @@ void QueryLoggingSolver::startQuery(const Query &query, const char *typeName, printQuery(query, falseQuery, objects); if (DumpPartialQueryiesEarly) { - logBuffer.flush(); - os << logBuffer.str(); - os.flush(); - // prepare the buffer for reuse - BufferString = ""; + flushBufferConditionally(true); } startTime = getWallTime(); } @@ -74,7 +80,7 @@ void QueryLoggingSolver::finishQuery(bool success) { } void QueryLoggingSolver::flushBuffer() { - logBuffer.flush(); + bool writeToFile = false; if ((0 == minQueryTimeToLog) || (static_cast(lastQueryTime * 1000) > minQueryTimeToLog)) { @@ -86,13 +92,11 @@ void QueryLoggingSolver::flushBuffer() { (solver->impl->getOperationStatusCode()))) { // we do additional check here to log only timeouts in case // user specified negative value for minQueryTimeToLog param - os << logBuffer.str(); - os.flush(); + writeToFile = true; } } - // prepare the buffer for reuse - BufferString = ""; + flushBufferConditionally(writeToFile); } bool QueryLoggingSolver::computeTruth(const Query &query, bool &isValid) { diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h index 3068f2ab..bb266c67 100644 --- a/lib/Solver/QueryLoggingSolver.h +++ b/lib/Solver/QueryLoggingSolver.h @@ -55,6 +55,7 @@ protected: virtual void printQuery(const Query &query, const Query *falseQuery = 0, const std::vector *objects = 0) = 0; + void flushBufferConditionally(bool writeToFile); public: QueryLoggingSolver(Solver *_solver, std::string path, -- cgit 1.4.1