klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
QueryLoggingSolver Class Referenceabstract

#include <QueryLoggingSolver.h>

Inheritance diagram for QueryLoggingSolver:
Collaboration diagram for QueryLoggingSolver:

Public Member Functions

 QueryLoggingSolver (Solver *_solver, std::string path, const std::string &commentSign, int queryTimeToLog)
 
virtual ~QueryLoggingSolver ()
 
bool computeTruth (const Query &query, bool &isValid)
 implementation of the SolverImpl interface More...
 
bool computeValidity (const Query &query, Solver::Validity &result)
 
bool computeValue (const Query &query, ref< Expr > &result)
 
bool computeInitialValues (const Query &query, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)
 
SolverRunStatus getOperationStatusCode ()
 getOperationStatusCode - get the status of the last solver operation More...
 
char * getConstraintLog (const Query &)
 
void setCoreSolverTimeout (double timeout)
 
- Public Member Functions inherited from klee::SolverImpl
 SolverImpl ()
 
virtual ~SolverImpl ()
 

Protected Member Functions

virtual void startQuery (const Query &query, const char *typeName, const Query *falseQuery=0, const std::vector< const Array * > *objects=0)
 
virtual void finishQuery (bool success)
 
void flushBuffer (void)
 
virtual void printQuery (const Query &query, const Query *falseQuery=0, const std::vector< const Array * > *objects=0)=0
 

Protected Attributes

Solversolver
 
std::string ErrorInfo
 
llvm::raw_fd_ostream os
 
std::string BufferString
 
llvm::raw_string_ostream logBuffer
 
unsigned queryCount
 
int minQueryTimeToLog
 
double startTime
 
double lastQueryTime
 
const std::string queryCommentSign
 

Additional Inherited Members

- Public Types inherited from klee::SolverImpl
enum  SolverRunStatus {
  SOLVER_RUN_STATUS_SUCCESS_SOLVABLE, SOLVER_RUN_STATUS_SUCCESS_UNSOLVABLE, SOLVER_RUN_STATUS_FAILURE, SOLVER_RUN_STATUS_TIMEOUT,
  SOLVER_RUN_STATUS_FORK_FAILED, SOLVER_RUN_STATUS_INTERRUPTED, SOLVER_RUN_STATUS_UNEXPECTED_EXIT_CODE, SOLVER_RUN_STATUS_WAITPID_FAILED
}
 
- Static Public Member Functions inherited from klee::SolverImpl
static const char * getOperationStatusString (SolverRunStatus statusCode)
 

Detailed Description

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.

Definition at line 25 of file QueryLoggingSolver.h.

Constructor & Destructor Documentation

QueryLoggingSolver::QueryLoggingSolver ( Solver _solver,
std::string  path,
const std::string &  commentSign,
int  queryTimeToLog 
)

Definition at line 17 of file QueryLoggingSolver.cpp.

References solver.

QueryLoggingSolver::~QueryLoggingSolver ( )
virtual

Definition at line 33 of file QueryLoggingSolver.cpp.

References solver.

Member Function Documentation

bool QueryLoggingSolver::computeInitialValues ( const Query query,
const std::vector< const Array * > &  objects,
std::vector< std::vector< unsigned char > > &  values,
bool &  hasSolution 
)
virtual
See also
Solver::getInitialValues()

Implements klee::SolverImpl.

Definition at line 141 of file QueryLoggingSolver.cpp.

References klee::SolverImpl::computeInitialValues(), finishQuery(), flushBuffer(), klee::Solver::impl, logBuffer, klee::Array::name, queryCommentSign, klee::Array::size, solver, and startQuery().

Here is the call graph for this function:

bool QueryLoggingSolver::computeTruth ( const Query query,
bool &  isValid 
)
virtual

implementation of the SolverImpl interface

Implements klee::SolverImpl.

Definition at line 86 of file QueryLoggingSolver.cpp.

References klee::SolverImpl::computeTruth(), finishQuery(), flushBuffer(), klee::Solver::impl, logBuffer, queryCommentSign, solver, and startQuery().

Here is the call graph for this function:

bool QueryLoggingSolver::computeValidity ( const Query query,
Solver::Validity result 
)
virtual

computeValidity - Compute a full validity result for the query.

The query expression is guaranteed to be non-constant and have bool type.

SolverImpl provides a default implementation which uses computeTruth. Clients should override this if a more efficient implementation is available.

Parameters
[out]result- if

\[ \forall X constraints(X) \to query(X) \]

then Solver::True, else if

\[ \forall X constraints(X) \to \lnot query(X) \]

then Solver::False, else Solver::Unknown
Returns
True on success

Reimplemented from klee::SolverImpl.

Definition at line 104 of file QueryLoggingSolver.cpp.

References klee::SolverImpl::computeValidity(), finishQuery(), flushBuffer(), klee::Solver::impl, logBuffer, queryCommentSign, solver, and startQuery().

Here is the call graph for this function:

bool QueryLoggingSolver::computeValue ( const Query query,
ref< Expr > &  result 
)
virtual

computeValue - Compute a feasible value for the expression.

The query expression is guaranteed to be non-constant.

Returns
True on success

Implements klee::SolverImpl.

Definition at line 123 of file QueryLoggingSolver.cpp.

References klee::SolverImpl::computeValue(), finishQuery(), flushBuffer(), klee::Solver::impl, logBuffer, queryCommentSign, solver, startQuery(), and klee::Query::withFalse().

Here is the call graph for this function:

void QueryLoggingSolver::finishQuery ( bool  success)
protectedvirtual

Definition at line 53 of file QueryLoggingSolver.cpp.

References klee::SolverImpl::getOperationStatusCode(), klee::util::getWallTime(), klee::Solver::impl, lastQueryTime, logBuffer, queryCommentSign, solver, and startTime.

Referenced by computeInitialValues(), computeTruth(), computeValidity(), and computeValue().

Here is the call graph for this function:

Here is the caller graph for this function:

void QueryLoggingSolver::flushBuffer ( void  )
protected

flushBuffer - flushes the temporary logs buffer. Depending on threshold settings, contents of the buffer are either discarded or written to a file.

Definition at line 65 of file QueryLoggingSolver.cpp.

References BufferString, klee::SolverImpl::getOperationStatusCode(), klee::Solver::impl, lastQueryTime, logBuffer, minQueryTimeToLog, os, solver, and klee::SolverImpl::SOLVER_RUN_STATUS_TIMEOUT.

Referenced by computeInitialValues(), computeTruth(), computeValidity(), and computeValue().

Here is the call graph for this function:

Here is the caller graph for this function:

char * QueryLoggingSolver::getConstraintLog ( const Query query)
virtual

Reimplemented from klee::SolverImpl.

Definition at line 187 of file QueryLoggingSolver.cpp.

References klee::SolverImpl::getConstraintLog(), klee::Solver::impl, and solver.

Here is the call graph for this function:

SolverImpl::SolverRunStatus QueryLoggingSolver::getOperationStatusCode ( )
virtual

getOperationStatusCode - get the status of the last solver operation

Implements klee::SolverImpl.

Definition at line 183 of file QueryLoggingSolver.cpp.

References klee::SolverImpl::getOperationStatusCode(), klee::Solver::impl, and solver.

Here is the call graph for this function:

virtual void QueryLoggingSolver::printQuery ( const Query query,
const Query falseQuery = 0,
const std::vector< const Array * > *  objects = 0 
)
protectedpure virtual

Implemented in PCLoggingSolver, and SMTLIBLoggingSolver.

Referenced by startQuery().

Here is the caller graph for this function:

void QueryLoggingSolver::setCoreSolverTimeout ( double  timeout)
virtual

Reimplemented from klee::SolverImpl.

Definition at line 191 of file QueryLoggingSolver.cpp.

References klee::Solver::impl, klee::SolverImpl::setCoreSolverTimeout(), and solver.

Here is the call graph for this function:

void QueryLoggingSolver::startQuery ( const Query query,
const char *  typeName,
const Query falseQuery = 0,
const std::vector< const Array * > *  objects = 0 
)
protectedvirtual

Member Data Documentation

std::string QueryLoggingSolver::BufferString
protected

Definition at line 32 of file QueryLoggingSolver.h.

Referenced by flushBuffer().

std::string QueryLoggingSolver::ErrorInfo
protected

Definition at line 29 of file QueryLoggingSolver.h.

double QueryLoggingSolver::lastQueryTime
protected

Definition at line 42 of file QueryLoggingSolver.h.

Referenced by finishQuery(), and flushBuffer().

llvm::raw_string_ostream QueryLoggingSolver::logBuffer
protected
int QueryLoggingSolver::minQueryTimeToLog
protected

Definition at line 36 of file QueryLoggingSolver.h.

Referenced by flushBuffer().

llvm::raw_fd_ostream QueryLoggingSolver::os
protected

Definition at line 30 of file QueryLoggingSolver.h.

Referenced by flushBuffer().

const std::string QueryLoggingSolver::queryCommentSign
protected
unsigned QueryLoggingSolver::queryCount
protected

Definition at line 35 of file QueryLoggingSolver.h.

Referenced by startQuery().

double QueryLoggingSolver::startTime
protected

Definition at line 41 of file QueryLoggingSolver.h.

Referenced by finishQuery(), and startQuery().


The documentation for this class was generated from the following files: