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.cpp | 303 ++++++++++++++++++-------------------- 1 file changed, 147 insertions(+), 156 deletions(-) (limited to 'lib/Solver/QueryLoggingSolver.cpp') diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index b6c25b55..6084e2e1 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -1,13 +1,4 @@ //===-- QueryLoggingSolver.cpp --------------------------------------------===// - -#include "QueryLoggingSolver.h" -#include "klee/Internal/System/Time.h" -#include "klee/Statistics.h" - -#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) -#include "llvm/Support/FileSystem.h" -#endif - // // The KLEE Symbolic Virtual Machine // @@ -15,6 +6,13 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// +#include "QueryLoggingSolver.h" +#include "klee/Internal/System/Time.h" +#include "klee/Statistics.h" + +#if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) +#include "llvm/Support/FileSystem.h" +#endif using namespace klee::util; @@ -24,187 +22,180 @@ llvm::cl::opt DumpPartialQueryiesEarly( llvm::cl::desc("Log queries before calling the solver (default=off)")); } -QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, - std::string path, - const std::string& commentSign, - int queryTimeToLog) +QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, + const std::string &commentSign, + int queryTimeToLog) : solver(_solver), #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 5) os(path.c_str(), ErrorInfo, llvm::sys::fs::OpenFlags::F_Text), #else os(path.c_str(), ErrorInfo), #endif - BufferString(""), - logBuffer(BufferString), - queryCount(0), - minQueryTimeToLog(queryTimeToLog), - startTime(0.0f), - lastQueryTime(0.0f), + BufferString(""), logBuffer(BufferString), queryCount(0), + minQueryTimeToLog(queryTimeToLog), startTime(0.0f), lastQueryTime(0.0f), queryCommentSign(commentSign) { - assert(0 != solver); + assert(0 != solver); } -QueryLoggingSolver::~QueryLoggingSolver() { - delete solver; -} +QueryLoggingSolver::~QueryLoggingSolver() { delete solver; } -void QueryLoggingSolver::startQuery(const Query& query, const char* typeName, - const Query* falseQuery, - const std::vector *objects) { - Statistic *S = theStatisticManager->getStatisticByName("Instructions"); - uint64_t instructions = S ? S->getValue() : 0; +void QueryLoggingSolver::startQuery(const Query &query, const char *typeName, + const Query *falseQuery, + const std::vector *objects) { + Statistic *S = theStatisticManager->getStatisticByName("Instructions"); + uint64_t instructions = S ? S->getValue() : 0; - logBuffer << queryCommentSign << " Query " << queryCount++ << " -- " - << "Type: " << typeName << ", " - << "Instructions: " << instructions << "\n"; - - printQuery(query, falseQuery, objects); + logBuffer << queryCommentSign << " Query " << queryCount++ << " -- " + << "Type: " << typeName << ", " + << "Instructions: " << instructions << "\n"; - if (DumpPartialQueryiesEarly) { - logBuffer.flush(); - os << logBuffer.str(); - os.flush(); - // prepare the buffer for reuse - BufferString = ""; - } - startTime = getWallTime(); + printQuery(query, falseQuery, objects); + + if (DumpPartialQueryiesEarly) { + logBuffer.flush(); + os << logBuffer.str(); + os.flush(); + // prepare the buffer for reuse + BufferString = ""; + } + startTime = getWallTime(); } void QueryLoggingSolver::finishQuery(bool success) { - lastQueryTime = getWallTime() - startTime; - logBuffer << queryCommentSign << " " << (success ? "OK" : "FAIL") << " -- " - << "Elapsed: " << lastQueryTime << "\n"; - - if (false == success) { - logBuffer << queryCommentSign << " Failure reason: " - << SolverImpl::getOperationStatusString(solver->impl->getOperationStatusCode()) - << "\n"; - } + lastQueryTime = getWallTime() - startTime; + logBuffer << queryCommentSign << " " << (success ? "OK" : "FAIL") << " -- " + << "Elapsed: " << lastQueryTime << "\n"; + + if (false == success) { + logBuffer << queryCommentSign << " Failure reason: " + << SolverImpl::getOperationStatusString( + solver->impl->getOperationStatusCode()) << "\n"; + } } void QueryLoggingSolver::flushBuffer() { - logBuffer.flush(); - - if ((0 == minQueryTimeToLog) || - (static_cast(lastQueryTime * 1000) > minQueryTimeToLog)) { - // we either do not limit logging queries or the query time - // is larger than threshold (in ms) - - if ((minQueryTimeToLog >= 0) || - (SOLVER_RUN_STATUS_TIMEOUT == (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(); - } - } - - // prepare the buffer for reuse - BufferString = ""; + logBuffer.flush(); + + if ((0 == minQueryTimeToLog) || + (static_cast(lastQueryTime * 1000) > minQueryTimeToLog)) { + // we either do not limit logging queries or the query time + // is larger than threshold (in ms) + + if ((minQueryTimeToLog >= 0) || + (SOLVER_RUN_STATUS_TIMEOUT == + (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(); + } + } + + // prepare the buffer for reuse + BufferString = ""; } -bool QueryLoggingSolver::computeTruth(const Query& query, bool& isValid) { - startQuery(query, "Truth"); - - bool success = solver->impl->computeTruth(query, isValid); - - finishQuery(success); - - if (success) { - logBuffer << queryCommentSign << " Is Valid: " - << (isValid ? "true" : "false") << "\n"; - } - logBuffer << "\n"; - - flushBuffer(); - - return success; +bool QueryLoggingSolver::computeTruth(const Query &query, bool &isValid) { + startQuery(query, "Truth"); + + bool success = solver->impl->computeTruth(query, isValid); + + finishQuery(success); + + if (success) { + logBuffer << queryCommentSign + << " Is Valid: " << (isValid ? "true" : "false") << "\n"; + } + logBuffer << "\n"; + + flushBuffer(); + + return success; } -bool QueryLoggingSolver::computeValidity(const Query& query, - Solver::Validity& result) { - startQuery(query, "Validity"); - - bool success = solver->impl->computeValidity(query, result); - - finishQuery(success); - - if (success) { - logBuffer << queryCommentSign << " Validity: " - << result << "\n"; - } - logBuffer << "\n"; - - flushBuffer(); - - return success; +bool QueryLoggingSolver::computeValidity(const Query &query, + Solver::Validity &result) { + startQuery(query, "Validity"); + + bool success = solver->impl->computeValidity(query, result); + + finishQuery(success); + + if (success) { + logBuffer << queryCommentSign << " Validity: " << result << "\n"; + } + logBuffer << "\n"; + + flushBuffer(); + + return success; } -bool QueryLoggingSolver::computeValue(const Query& query, ref& result) { - Query withFalse = query.withFalse(); - startQuery(query, "Value", &withFalse); +bool QueryLoggingSolver::computeValue(const Query &query, ref &result) { + Query withFalse = query.withFalse(); + startQuery(query, "Value", &withFalse); - bool success = solver->impl->computeValue(query, result); - - finishQuery(success); - - if (success) { - logBuffer << queryCommentSign << " Result: " << result << "\n"; - } - logBuffer << "\n"; - - flushBuffer(); - - return success; + bool success = solver->impl->computeValue(query, result); + + finishQuery(success); + + if (success) { + logBuffer << queryCommentSign << " Result: " << result << "\n"; + } + logBuffer << "\n"; + + flushBuffer(); + + return success; } -bool QueryLoggingSolver::computeInitialValues(const Query& query, - const std::vector& objects, - std::vector >& values, - bool& hasSolution) { - startQuery(query, "InitialValues", 0, &objects); - - bool success = solver->impl->computeInitialValues(query, objects, - values, hasSolution); - - finishQuery(success); - - if (success) { - logBuffer << queryCommentSign << " Solvable: " - << (hasSolution ? "true" : "false") << "\n"; - if (hasSolution) { - std::vector< std::vector >::iterator - values_it = values.begin(); - - for (std::vector::const_iterator i = objects.begin(), - e = objects.end(); i != e; ++i, ++values_it) { - const Array *array = *i; - std::vector &data = *values_it; - logBuffer << queryCommentSign << " " << array->name << " = ["; - - for (unsigned j = 0; j < array->size; j++) { - logBuffer << (int) data[j]; - - if (j+1 < array->size) { - logBuffer << ","; - } - } - logBuffer << "]\n"; - } +bool QueryLoggingSolver::computeInitialValues( + const Query &query, const std::vector &objects, + std::vector > &values, bool &hasSolution) { + startQuery(query, "InitialValues", 0, &objects); + + bool success = + solver->impl->computeInitialValues(query, objects, values, hasSolution); + + finishQuery(success); + + if (success) { + logBuffer << queryCommentSign + << " Solvable: " << (hasSolution ? "true" : "false") << "\n"; + if (hasSolution) { + std::vector >::iterator values_it = + values.begin(); + + for (std::vector::const_iterator i = objects.begin(), + e = objects.end(); + i != e; ++i, ++values_it) { + const Array *array = *i; + std::vector &data = *values_it; + logBuffer << queryCommentSign << " " << array->name << " = ["; + + for (unsigned j = 0; j < array->size; j++) { + logBuffer << (int)data[j]; + + if (j + 1 < array->size) { + logBuffer << ","; + } } + logBuffer << "]\n"; + } } - logBuffer << "\n"; - - flushBuffer(); - - return success; + } + logBuffer << "\n"; + + flushBuffer(); + + return success; } SolverImpl::SolverRunStatus QueryLoggingSolver::getOperationStatusCode() { - return solver->impl->getOperationStatusCode(); + return solver->impl->getOperationStatusCode(); } -char *QueryLoggingSolver::getConstraintLog(const Query& query) { +char *QueryLoggingSolver::getConstraintLog(const Query &query) { return solver->impl->getConstraintLog(query); } -- cgit 1.4.1