ROSE  0.11.51.0
Classes | Public Types | Public Member Functions | Protected Member Functions | List of all members
Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks Class Referenceabstract

Description

User-defined functions for model checking semantics.

This class contains functions that are called by the model checker engine and which are meant to be overridden by users. This base class provides some reasonable defaults for some of the functions, but some of the others are pure virtual.

Definition at line 24 of file SemanticCallbacks.h.

#include <SemanticCallbacks.h>

Inheritance diagram for Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks:
Inheritance graph
[legend]

Classes

struct  CodeAddresses
 Addresses and completeness. More...
 
struct  NextUnit
 Return value for nextUnits. More...
 

Public Types

using Ptr = SemanticCallbacksPtr
 Shared-ownership pointer. More...
 

Public Member Functions

virtual void reset ()
 Reset internal data. More...
 
SettingsPtr mcSettings () const
 Property: Model checker settings. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr protoval ()
 Create a prototypical semantic value. More...
 
virtual InstructionSemantics2::BaseSemantics::RegisterStatePtr createInitialRegisters ()=0
 Create an initial register state. More...
 
virtual InstructionSemantics2::BaseSemantics::MemoryStatePtr createInitialMemory ()=0
 Create an initial memory state. More...
 
virtual InstructionSemantics2::BaseSemantics::StatePtr createInitialState ()
 Create an initial state. More...
 
virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr createRiscOperators ()=0
 Create RISC operators. More...
 
virtual SmtSolver::Ptr createSolver ()=0
 Create model checker solver. More...
 
virtual void attachModelCheckerSolver (const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &, const SmtSolver::Ptr &)
 Associate solver with semantics. More...
 
virtual void initializeState (const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &)
 Initialize the initial state. More...
 
virtual InstructionSemantics2::BaseSemantics::DispatcherPtr createDispatcher (const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &)=0
 Create an instruction dispatcher. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr instructionPointer (const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &)=0
 Address of the next instruction. More...
 
virtual CodeAddresses nextCodeAddresses (const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &)
 Possible next code addresses. More...
 
virtual std::vector< TagPtr > preExecute (const ExecutionUnitPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &)
 Called before execution starts. More...
 
virtual std::vector< TagPtr > postExecute (const ExecutionUnitPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &)
 Called after execution ends. More...
 
virtual std::vector< NextUnitnextUnits (const PathPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &, const SmtSolver::Ptr &)=0
 Discover next execution units. More...
 

Protected Member Functions

 SemanticCallbacks (const SettingsPtr &)
 

Member Typedef Documentation

Shared-ownership pointer.

Definition at line 27 of file SemanticCallbacks.h.

Member Function Documentation

virtual void Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::reset ( )
inlinevirtual

Reset internal data.

This is called when the model checker framework is reset. It should reset most internal data associated with the model checking process itself, but should not reset settings that control how the model checker works.

Thread safety: This method is not thread safe.

Reimplemented in Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks.

Definition at line 49 of file SemanticCallbacks.h.

SettingsPtr Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::mcSettings ( ) const

Property: Model checker settings.

Returns a pointer to the model checker settings.

Thread safety: This method is thread safe.

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::protoval ( )
virtual

Create a prototypical semantic value.

The prototypical value is used to instantiate other parts of the semantic framework and is what defines the semantic domain in conjunction with the RISCoperators". The default implementation returns a prototypical value of the @ref Rose::BinaryAnalysis::InstructionSemantics2::SymbolicSemantics "symbolic domain".

Thread safety: The implementation must be thread safe, but the object it returns does not need to have a thread safe API.

Reimplemented in Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks.

virtual InstructionSemantics2::BaseSemantics::RegisterStatePtr Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::createInitialRegisters ( )
pure virtual

Create an initial register state.

Creates the initial register state for paths. The registers can be initialize here or in initializeState.

Thread safety: The implementation must be thread safe, but the object it returns does not need to have a thread safe API.

Implemented in Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks.

virtual InstructionSemantics2::BaseSemantics::MemoryStatePtr Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::createInitialMemory ( )
pure virtual

Create an initial memory state.

Creates the initial memory state for paths. The memory can be initialized here or in initializeState.

Thread safety: The implementation must be thread safe, but the object it returns does not need to have a thread safe API.

Implemented in Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks.

virtual InstructionSemantics2::BaseSemantics::StatePtr Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::createInitialState ( )
virtual

Create an initial state.

Creates the initial state for paths beginning at the specified execution unit. The default implementation uses the base semantics state.

Thread safety: The implementation must be thread safe, but the object it returns does not need to have a thread safe API.

Reimplemented in Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks.

virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::createRiscOperators ( )
pure virtual

Create RISC operators.

Creates a new RISC operators object which, together with the protoval, defines the semantic domain.

The returned operators must have a null initial state and null current state. This is to prevent implementations of this function from accidentally thinking they can initialize the path's state this way – they can't. Instead, states are initialized either when they're created (createInitialRegisters, createInitialMemory, createInitialState) or when they're first associated with a path (initializeState). The latter is the easiest since it allows one to initialize the state through the RISC operators. The model checker framework will swap states into and out of the RISC operators object as necessary.

The RISC operators may refer to an SMT solver if desired. This solver will remain attached to the operators for the duration of its existence and will be used for operations but not for the model checking. The SMT solver for the model checker is created by the createSolver method.

Thread safety: The implementation must be thread safe, but the object it returns does not need to have a thread safe API.

Implemented in Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks.

virtual SmtSolver::Ptr Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::createSolver ( )
pure virtual

Create model checker solver.

This solver will be used for model checker operations, but not for RISC operations (see createRiscOperators). The The model checker will insert various path assertions when necessary. Whenever the model checker calls user code that might modify the solver, it will protect the call with a solver transaction. If user code needs to permanently add assertions, there are other mechanisms to do so. Namely, one needs to add the assertion through a model checker API so that the model checker knows about it.

Thread safety: The implementation must be thread safe, but the object it returns will be used only by the calling thread.

Implemented in Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks.

virtual void Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::attachModelCheckerSolver ( const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr ,
const SmtSolver::Ptr  
)
inlinevirtual

Associate solver with semantics.

Given the semantics RISC operators for a thread, and the SMT solver used by the model checking for that thread, associate the model checker solver with the operators. This only needs to do anything if the semantics need access to the solver. For instance, a null address checker would evaluate the address during memoryRead and memoryWrite RISC operations and would therefore benefit from being able to use the model checker's current solver state.

The model checker solver can be completely independent of the SMT solver that's sometimes associated with symbolic RISC operators, or they can be the same solver.

Thread safety: The implementation must be thread safe, but the provided RISC operators and solver will be thread local.

Reimplemented in Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks.

Definition at line 137 of file SemanticCallbacks.h.

virtual void Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::initializeState ( const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr )
virtual

Initialize the initial state.

This is useful if initializations were not done in createInitialRegisters, createInitialMemory, or createInitialState. The benefit of doing it here si that the same code can be used for different semantic domains, leaving the other functions to choose the domains. Doing the initialization here also allows you to use the RISC operators to initialize the states.

Thread safety: The implementation must be thread safe. However, the RISC operators object is thread-local.

Reimplemented in Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks.

virtual InstructionSemantics2::BaseSemantics::DispatcherPtr Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::createDispatcher ( const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr )
pure virtual

Create an instruction dispatcher.

The instruction dispatcher is used to transition from one state to another when "executing" an instruction.

Thread safety: The implementation must be thread safe, but the object it returns does not need to have a thread safe API.

Implemented in Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks.

virtual InstructionSemantics2::BaseSemantics::SValuePtr Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::instructionPointer ( const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr )
pure virtual

Address of the next instruction.

Given a state, return the address of the instruction that would be executed next. It should not modify the current state associated with the supplied RISC operators.

Thread safety: The implementation must be thread safe, but the provided state will be thread local.

Implemented in Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks.

virtual CodeAddresses Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::nextCodeAddresses ( const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr )
virtual

Possible next code addresses.

This method looks at the instruction pointer register (see instructionPointer) and returns whatever concrete addresses it can find. It should not modify the current state associated with the RISC operators.

Thread safety: The implementation must be thread safe, but the provided arguments are all thread local.

Reimplemented in Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks.

virtual std::vector<TagPtr> Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::preExecute ( const ExecutionUnitPtr &  ,
const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr  
)
virtual

Called before execution starts.

This method is called before the execution unit is executed. It is allowed to change the state prior to the execution. It is also a convenient place at which to create tags to be later attached to the node.

The default implementation does nothing.

Thread safety: The implementation must be thread safe, but the provided RISC operators will be thread local. The current state to which the RISC operators pointsw ill have been copied by this thread.

Reimplemented in Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks.

virtual std::vector<TagPtr> Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::postExecute ( const ExecutionUnitPtr &  ,
const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr  
)
virtual

Called after execution ends.

This method is called after the execution unit is executed. It is allowed to change the execution's resulting state. It is also a convenient place at which to create tags to be later attached to the node.

The default implementation does nothing.

Thread safety: The implementation must be thread safe, but the provided RISC operators will be thread local. The current state to which the RISC operators pointsw ill have been copied by this thread.

virtual std::vector<NextUnit> Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks::nextUnits ( const PathPtr &  ,
const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr ,
const SmtSolver::Ptr  
)
pure virtual

Discover next execution units.

Given a semantic state of an execution path, determine how the path should be extended by returning the list of next execution units. For instance, a conditional branch instruction would likely result in two new execution units: the target basic block for when the branch is taken, and the fall-through basic block for when the branch is not taken.

All returned execution units should be feasible. That is, this function should check that the address of a candidate execution unit satisfies the path constraints that are already represented in the supplied solver.

The order of the returned execution units is irrelevant because they will be sorted within the work list according to the work list priority function. However, since the user defines both the priority and the execution unit types, this method can communicate to the priority function via data it stores in the execution unit.

Thread safety: The implementation must be thread safe, but the provided RISC operators will be thread local. The current state to which the RISC operators points will have been copied by this thread.

Implemented in Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks.


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