klee
Public Member Functions | Public Attributes | List of all members
klee::TimingSolver Class Reference

#include <TimingSolver.h>

Public Member Functions

 TimingSolver (Solver *_solver, bool _simplifyExprs=true)
 
void setTimeout (time::Span t)
 
char * getConstraintLog (const Query &query)
 
bool evaluate (const ConstraintSet &, ref< Expr >, Solver::Validity &result, SolverQueryMetaData &metaData)
 
bool mustBeTrue (const ConstraintSet &, ref< Expr >, bool &result, SolverQueryMetaData &metaData)
 
bool mustBeFalse (const ConstraintSet &, ref< Expr >, bool &result, SolverQueryMetaData &metaData)
 
bool mayBeTrue (const ConstraintSet &, ref< Expr >, bool &result, SolverQueryMetaData &metaData)
 
bool mayBeFalse (const ConstraintSet &, ref< Expr >, bool &result, SolverQueryMetaData &metaData)
 
bool getValue (const ConstraintSet &, ref< Expr > expr, ref< ConstantExpr > &result, SolverQueryMetaData &metaData)
 
bool getInitialValues (const ConstraintSet &, const std::vector< const Array * > &objects, std::vector< std::vector< unsigned char > > &result, SolverQueryMetaData &metaData)
 
std::pair< ref< Expr >, ref< Expr > > getRange (const ConstraintSet &, ref< Expr > query, SolverQueryMetaData &metaData)
 

Public Attributes

std::unique_ptr< Solver > solver
 
bool simplifyExprs
 

Detailed Description

TimingSolver - A simple class which wraps a solver and handles tracking the statistics that we care about.

Definition at line 27 of file TimingSolver.h.

Constructor & Destructor Documentation

◆ TimingSolver()

klee::TimingSolver::TimingSolver ( Solver *  _solver,
bool  _simplifyExprs = true 
)
inline

TimingSolver - Construct a new timing solver.

Parameters
_simplifyExprs- Whether expressions should be simplified (via the constraint manager interface) prior to querying.

Definition at line 38 of file TimingSolver.h.

Member Function Documentation

◆ evaluate()

bool TimingSolver::evaluate ( const ConstraintSet &  constraints,
ref< Expr >  expr,
Solver::Validity &  result,
SolverQueryMetaData &  metaData 
)

Definition at line 26 of file TimingSolver.cpp.

References klee::TimerStatIncrementer::delta(), klee::Solver::False, klee::SolverQueryMetaData::queryCost, klee::ConstraintManager::simplifyExpr(), simplifyExprs, solver, klee::stats::solverTime, and klee::Solver::True.

Referenced by klee::Executor::fork().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ getConstraintLog()

char * klee::TimingSolver::getConstraintLog ( const Query &  query)
inline

Definition at line 43 of file TimingSolver.h.

References solver.

Referenced by klee::Executor::getConstraintLog().

Here is the caller graph for this function:

◆ getInitialValues()

bool TimingSolver::getInitialValues ( const ConstraintSet &  constraints,
const std::vector< const Array * > &  objects,
std::vector< std::vector< unsigned char > > &  result,
SolverQueryMetaData &  metaData 
)

Definition at line 111 of file TimingSolver.cpp.

References klee::ConstantExpr::alloc(), klee::Expr::Bool, klee::TimerStatIncrementer::delta(), klee::SolverQueryMetaData::queryCost, solver, and klee::stats::solverTime.

Referenced by klee::Executor::getSymbolicSolution().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ getRange()

std::pair< ref< Expr >, ref< Expr > > TimingSolver::getRange ( const ConstraintSet &  constraints,
ref< Expr >  query,
SolverQueryMetaData &  metaData 
)

Definition at line 129 of file TimingSolver.cpp.

References klee::TimerStatIncrementer::delta(), klee::SolverQueryMetaData::queryCost, solver, and klee::stats::solverTime.

Referenced by klee::Executor::getAddressInfo().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ getValue()

bool TimingSolver::getValue ( const ConstraintSet &  constraints,
ref< Expr >  expr,
ref< ConstantExpr > &  result,
SolverQueryMetaData &  metaData 
)

Definition at line 90 of file TimingSolver.cpp.

References klee::TimerStatIncrementer::delta(), klee::SolverQueryMetaData::queryCost, klee::ConstraintManager::simplifyExpr(), simplifyExprs, solver, and klee::stats::solverTime.

Referenced by klee::Executor::branch(), klee::Executor::callExternalFunction(), klee::Executor::executeAlloc(), klee::Executor::executeGetValue(), klee::Executor::executeInstruction(), klee::ObjectState::flushToConcreteStore(), klee::Executor::fork(), klee::Executor::getAddressInfo(), klee::Executor::maxStaticPctChecks(), klee::SeedInfo::patchSeed(), klee::AddressSpace::resolve(), klee::AddressSpace::resolveOne(), klee::Executor::toConstant(), and klee::Executor::toUnique().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ mayBeFalse()

bool TimingSolver::mayBeFalse ( const ConstraintSet &  constraints,
ref< Expr >  expr,
bool &  result,
SolverQueryMetaData &  metaData 
)

Definition at line 81 of file TimingSolver.cpp.

References mustBeTrue().

Here is the call graph for this function:

◆ mayBeTrue()

bool TimingSolver::mayBeTrue ( const ConstraintSet &  constraints,
ref< Expr >  expr,
bool &  result,
SolverQueryMetaData &  metaData 
)

Definition at line 72 of file TimingSolver.cpp.

References mustBeFalse().

Referenced by klee::AddressSpace::checkPointerInObject(), klee::Executor::executeAlloc(), klee::Executor::executeInstruction(), klee::SeedInfo::patchSeed(), and klee::AddressSpace::resolveOne().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ mustBeFalse()

bool TimingSolver::mustBeFalse ( const ConstraintSet &  constraints,
ref< Expr >  expr,
bool &  result,
SolverQueryMetaData &  metaData 
)

Definition at line 67 of file TimingSolver.cpp.

References klee::Expr::createIsZero(), and mustBeTrue().

Referenced by klee::Executor::addConstraint(), mayBeTrue(), and klee::SeedInfo::patchSeed().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ mustBeTrue()

bool TimingSolver::mustBeTrue ( const ConstraintSet &  constraints,
ref< Expr >  expr,
bool &  result,
SolverQueryMetaData &  metaData 
)

Definition at line 47 of file TimingSolver.cpp.

References klee::TimerStatIncrementer::delta(), klee::SolverQueryMetaData::queryCost, klee::ConstraintManager::simplifyExpr(), simplifyExprs, solver, and klee::stats::solverTime.

Referenced by klee::AddressSpace::checkPointerInObject(), klee::Executor::executeAlloc(), klee::Executor::executeMemoryOperation(), klee::Executor::getSymbolicSolution(), mayBeFalse(), mustBeFalse(), klee::AddressSpace::resolve(), klee::AddressSpace::resolveOne(), and klee::Executor::toUnique().

Here is the call graph for this function:
Here is the caller graph for this function:

◆ setTimeout()

void klee::TimingSolver::setTimeout ( time::Span  t)
inline

Definition at line 41 of file TimingSolver.h.

References solver.

Referenced by klee::Executor::executeMemoryOperation(), klee::Executor::fork(), klee::Executor::getSymbolicSolution(), and klee::Executor::toUnique().

Here is the caller graph for this function:

Member Data Documentation

◆ simplifyExprs

bool klee::TimingSolver::simplifyExprs

Definition at line 30 of file TimingSolver.h.

Referenced by evaluate(), getValue(), and mustBeTrue().

◆ solver

std::unique_ptr<Solver> klee::TimingSolver::solver

Definition at line 29 of file TimingSolver.h.

Referenced by klee::Executor::doImpliedValueConcretization(), evaluate(), getConstraintLog(), getInitialValues(), getRange(), getValue(), mustBeTrue(), and setTimeout().

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