#include <QueryLoggingSolver.h>

Inheritance diagram for QueryLoggingSolver:

[legend]

Collaboration diagram for QueryLoggingSolver:

[legend]

Public Member Functions
	QueryLoggingSolver (Solver *_solver, std::string path, const std::string &commentSign, time::Span queryTimeToLog, bool logTimedOut)

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 (time::Span timeout)

Public Member Functions inherited from klee::SolverImpl
	SolverImpl ()

virtual	~SolverImpl ()

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

virtual bool	computeTruth (const Query &query, bool &isValid)=0

virtual bool	computeValue (const Query &query, ref< Expr > &result)=0

virtual bool	computeInitialValues (const Query &query, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &values, bool &hasSolution)=0

virtual SolverRunStatus	getOperationStatusCode ()=0
	getOperationStatusCode - get the status of the last solver operation More...

virtual char *	getConstraintLog (const Query &query)

virtual void	setCoreSolverTimeout (time::Span timeout)

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

void	flushBufferConditionally (bool writeToFile)

Protected Attributes
Solver *	solver

std::unique_ptr< llvm::raw_ostream >	os

std::string	BufferString

llvm::raw_string_ostream	logBuffer

unsigned	queryCount

time::Span	minQueryTimeToLog

bool	logTimedOutQueries = false

time::Point	startTime

time::Span	lastQueryDuration

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 26 of file QueryLoggingSolver.h.

Constructor & Destructor Documentation

◆ QueryLoggingSolver()

QueryLoggingSolver::QueryLoggingSolver	(	Solver *	_solver,
		std::string	path,
		const std::string &	commentSign,
		time::Span	queryTimeToLog,
		bool	logTimedOut
	)

Definition at line 32 of file QueryLoggingSolver.cpp.

References klee::klee_error(), klee::klee_open_output_file(), os, and solver.

Here is the call graph for this function:

◆ ~QueryLoggingSolver()

QueryLoggingSolver::~QueryLoggingSolver ( )

virtual

Definition at line 56 of file QueryLoggingSolver.cpp.

References solver.

Member Function Documentation

◆ computeInitialValues()

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 166 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:

◆ computeTruth()

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

virtual

implementation of the SolverImpl interface

Implements klee::SolverImpl.

Definition at line 112 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:

◆ computeValidity()

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 130 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:

◆ computeValue()

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 148 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:

◆ finishQuery()

void QueryLoggingSolver::finishQuery ( bool success )

protectedvirtual

Definition at line 88 of file QueryLoggingSolver.cpp.

References klee::SolverImpl::getOperationStatusCode(), klee::time::getWallTime(), klee::Solver::impl, lastQueryDuration, 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:

◆ flushBuffer()

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 100 of file QueryLoggingSolver.cpp.

References flushBufferConditionally(), klee::SolverImpl::getOperationStatusCode(), klee::Solver::impl, lastQueryDuration, logTimedOutQueries, minQueryTimeToLog, 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:

◆ flushBufferConditionally()

void QueryLoggingSolver::flushBufferConditionally ( bool writeToFile )

protected

Definition at line 60 of file QueryLoggingSolver.cpp.

References BufferString, logBuffer, and os.

Referenced by flushBuffer(), and startQuery().

Here is the caller graph for this function:

◆ getConstraintLog()

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

virtual

Reimplemented from klee::SolverImpl.

Definition at line 212 of file QueryLoggingSolver.cpp.

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

Here is the call graph for this function:

◆ getOperationStatusCode()

SolverImpl::SolverRunStatus QueryLoggingSolver::getOperationStatusCode ( )

virtual

getOperationStatusCode - get the status of the last solver operation

Implements klee::SolverImpl.

Definition at line 208 of file QueryLoggingSolver.cpp.

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

Here is the call graph for this function:

◆ printQuery()

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

protectedpure virtual

Implemented in KQueryLoggingSolver, and SMTLIBLoggingSolver.

Referenced by startQuery().

Here is the caller graph for this function:

◆ setCoreSolverTimeout()

void QueryLoggingSolver::setCoreSolverTimeout ( time::Span timeout )

virtual

Reimplemented from klee::SolverImpl.

Definition at line 216 of file QueryLoggingSolver.cpp.

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

Here is the call graph for this function:

◆ startQuery()

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

protectedvirtual

Definition at line 70 of file QueryLoggingSolver.cpp.

References flushBufferConditionally(), klee::StatisticManager::getStatisticByName(), klee::Statistic::getValue(), klee::time::getWallTime(), klee::stats::instructions, logBuffer, printQuery(), queryCommentSign, queryCount, startTime, and klee::theStatisticManager.

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

Here is the call graph for this function:

Here is the caller graph for this function:

Member Data Documentation

◆ BufferString

std::string QueryLoggingSolver::BufferString

protected

Definition at line 32 of file QueryLoggingSolver.h.

Referenced by flushBufferConditionally().

◆ lastQueryDuration

time::Span QueryLoggingSolver::lastQueryDuration

protected

Definition at line 39 of file QueryLoggingSolver.h.

Referenced by finishQuery(), and flushBuffer().

◆ logBuffer

llvm::raw_string_ostream QueryLoggingSolver::logBuffer

protected

Definition at line 34 of file QueryLoggingSolver.h.

Referenced by computeInitialValues(), computeTruth(), computeValidity(), computeValue(), finishQuery(), flushBufferConditionally(), KQueryLoggingSolver::printQuery(), SMTLIBLoggingSolver::SMTLIBLoggingSolver(), and startQuery().

◆ logTimedOutQueries

bool QueryLoggingSolver::logTimedOutQueries = false

protected

Definition at line 37 of file QueryLoggingSolver.h.

Referenced by flushBuffer().

◆ minQueryTimeToLog

time::Span QueryLoggingSolver::minQueryTimeToLog

protected

Definition at line 36 of file QueryLoggingSolver.h.

Referenced by flushBuffer().

◆ os

std::unique_ptr<llvm::raw_ostream> QueryLoggingSolver::os

protected

Definition at line 30 of file QueryLoggingSolver.h.

Referenced by flushBufferConditionally(), and QueryLoggingSolver().

◆ queryCommentSign

const std::string QueryLoggingSolver::queryCommentSign

protected

Definition at line 40 of file QueryLoggingSolver.h.

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

◆ queryCount

unsigned QueryLoggingSolver::queryCount

protected

Definition at line 35 of file QueryLoggingSolver.h.

Referenced by startQuery().

◆ solver

Solver* QueryLoggingSolver::solver

protected

Definition at line 29 of file QueryLoggingSolver.h.

Referenced by computeInitialValues(), computeTruth(), computeValidity(), computeValue(), finishQuery(), flushBuffer(), getConstraintLog(), getOperationStatusCode(), QueryLoggingSolver(), setCoreSolverTimeout(), and ~QueryLoggingSolver().

◆ startTime

time::Point QueryLoggingSolver::startTime

protected

Definition at line 38 of file QueryLoggingSolver.h.

Referenced by finishQuery(), and startQuery().

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

/Users/cristic/klee/lib/Solver/QueryLoggingSolver.h
/Users/cristic/klee/lib/Solver/QueryLoggingSolver.cpp

Public Member Functions

Protected Member Functions

Protected Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ QueryLoggingSolver()

◆ ~QueryLoggingSolver()

Member Function Documentation

◆ computeInitialValues()

◆ computeTruth()

◆ computeValidity()

◆ computeValue()

◆ finishQuery()

◆ flushBuffer()

◆ flushBufferConditionally()

◆ getConstraintLog()

◆ getOperationStatusCode()

◆ printQuery()

◆ setCoreSolverTimeout()

◆ startQuery()

Member Data Documentation

◆ BufferString

◆ lastQueryDuration

◆ logBuffer

◆ logTimedOutQueries

◆ minQueryTimeToLog

◆ os

◆ queryCommentSign

◆ queryCount

◆ solver

◆ startTime