ROSE  0.11.51.0
Public Types | Public Member Functions | Static Public Member Functions | Protected Member Functions | List of all members
Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks Class Reference

Description

Virtual definition of semantic operations for model checking.

Definition at line 504 of file P2Model.h.

#include <P2Model.h>

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

Public Types

using Ptr = SemanticCallbacksPtr
 
using UnitCounts = Sawyer::Container::Map< rose_addr_t, size_t >
 
- Public Types inherited from Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks
using Ptr = SemanticCallbacksPtr
 Shared-ownership pointer. More...
 

Public Member Functions

const Partitioner2::Partitionerpartitioner () const
 Property: Partitioner being used. More...
 
void followOnePath (const std::list< ExecutionUnitPtr > &)
 Cause this model to follow only one path through the specimen. More...
 
size_t nDuplicateStates () const
 Property: Number of duplicate states. More...
 
size_t nSolverFailures () const
 Property: Number of times the SMT solver failed. More...
 
size_t nUnitsReached () const
 Property: Number of execution units reached. More...
 
UnitCounts unitsReached () const
 Property: Execution units reached. More...
 
virtual bool filterNullDeref (const InstructionSemantics2::BaseSemantics::SValuePtr &addr, TestMode testMode, IoMode ioMode)
 Filter null dereferences. More...
 
virtual void reset () override
 Reset internal data. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr protoval () override
 Create a prototypical semantic value. More...
 
virtual InstructionSemantics2::BaseSemantics::RegisterStatePtr createInitialRegisters () override
 Create an initial register state. More...
 
virtual InstructionSemantics2::BaseSemantics::MemoryStatePtr createInitialMemory () override
 Create an initial memory state. More...
 
virtual InstructionSemantics2::BaseSemantics::StatePtr createInitialState () override
 Create an initial state. More...
 
virtual InstructionSemantics2::BaseSemantics::RiscOperatorsPtr createRiscOperators () override
 Create RISC operators. More...
 
virtual void initializeState (const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
 Initialize the initial state. More...
 
virtual InstructionSemantics2::BaseSemantics::DispatcherPtr createDispatcher (const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
 Create an instruction dispatcher. More...
 
virtual SmtSolver::Ptr createSolver () override
 Create model checker solver. More...
 
virtual void attachModelCheckerSolver (const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &, const SmtSolver::Ptr &) override
 Associate solver with semantics. More...
 
virtual CodeAddresses nextCodeAddresses (const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
 Possible next code addresses. More...
 
virtual std::vector< TagPtr > preExecute (const ExecutionUnitPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
 Called before execution starts. More...
 
virtual InstructionSemantics2::BaseSemantics::SValuePtr instructionPointer (const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
 Address of the next instruction. More...
 
virtual std::vector< NextUnitnextUnits (const PathPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &, const SmtSolver::Ptr &) override
 Discover next execution units. More...
 
bool followingOnePath () const
 Property: Whether we are in follow-one-path mode. More...
 
void followingOnePath (bool)
 Property: Whether we are in follow-one-path mode. More...
 
- Public Member Functions inherited from Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks
SettingsPtr mcSettings () const
 Property: Model checker settings. More...
 
virtual std::vector< TagPtr > postExecute (const ExecutionUnitPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &)
 Called after execution ends. More...
 

Static Public Member Functions

static Ptr instance (const ModelChecker::SettingsPtr &, const Settings &, const Partitioner2::Partitioner &)
 

Protected Member Functions

 SemanticCallbacks (const ModelChecker::SettingsPtr &, const Settings &, const Partitioner2::Partitioner &)
 
- Protected Member Functions inherited from Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks
 SemanticCallbacks (const SettingsPtr &)
 

Member Function Documentation

const Partitioner2::Partitioner& Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks::partitioner ( ) const

Property: Partitioner being used.

void Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks::followOnePath ( const std::list< ExecutionUnitPtr > &  )

Cause this model to follow only one path through the specimen.

The path is provided as an ordered list of execution units. The initial execution unit will not appear in this list since it should have been added to the model checker work list already, and it must be the only work on that list. In this mode of operation, the model checker is single threaded and will follow only this specified path until it reaches the end or some other condition causes the model checker to abandon the path earlier.

When the model checker runs, the nextCodeAddress method is overridden to return only the address of the next execution unit on this list, and the internal findUnit function returns the next unit, removing it from the list. When the list becomes empty, then no more code addresses or units are returned.

If this function is called when the model checker is already in followingOnePath mode, the behavior is as if followingOnePath was cleared first.

Thread safety: This function is thread safe.

bool Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks::followingOnePath ( ) const

Property: Whether we are in follow-one-path mode.

This property can be queried or modified at any time. The followOnePath function sets the property, which must then be cleared manually if you want to continue to use the model checker in its normal mode. Clearing this property will also discard any execution units that remain for the one path mode. Setting the property manually has no effect if the property was already set, but if it was clear then the model checker behaves as if it reached the end of the one path: it will stop exploring.

Thread safety: This property accessor is thread safe.

void Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks::followingOnePath ( bool  )

Property: Whether we are in follow-one-path mode.

This property can be queried or modified at any time. The followOnePath function sets the property, which must then be cleared manually if you want to continue to use the model checker in its normal mode. Clearing this property will also discard any execution units that remain for the one path mode. Setting the property manually has no effect if the property was already set, but if it was clear then the model checker behaves as if it reached the end of the one path: it will stop exploring.

Thread safety: This property accessor is thread safe.

size_t Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks::nDuplicateStates ( ) const

Property: Number of duplicate states.

This read-only property returns the number of times that a semantic state was encountered that had been encountered previously. Whenever a state is re-encountered, the corresponding path is not extended since extending it would also result in duplicate states (even though the paths to those states are different).

Thread safety: This property accessor is thread safe.

size_t Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks::nSolverFailures ( ) const

Property: Number of times the SMT solver failed.

This read-only property contains the number of times that an attempt was made to extend a path and the SMT solver returned an "unknown" answer (i.e., neither "satisfied" nor "unsatisfied"). An "unknown" result is usually caused only when a per-call solver timeout is enabled and the solver was unable to finish in the allotted time.

Thread safety: This property accessor is thread safe.

size_t Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks::nUnitsReached ( ) const

Property: Number of execution units reached.

This read-only property returns the number of unique execution unit addresses that were reached (i.e., semantically executed) during exploration. An execution unit is normally either a basic block or an externally defined function. However, if we attempt to execute an instruction that wasn't known to the partitioner, then each such instruction is counted separately without being part of a basic block.

Thread safety: This property accessor is thread safe.

UnitCounts Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks::unitsReached ( ) const

Property: Execution units reached.

Returns a mapping from execution unit address to the number of times that the address was semantically executed. The counts are returned by value rather than reference in order to achieve thread safety.

Thread safety: This property accessor is thread safe.

virtual bool Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks::filterNullDeref ( const InstructionSemantics2::BaseSemantics::SValuePtr addr,
TestMode  testMode,
IoMode  ioMode 
)
virtual

Filter null dereferences.

Returns true to accept the nullptr dereference, or false to say that it's not really a nullptr dereference.

The default implementation always returns true.

Thread safety: The implementation must be thread safe.

virtual void Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks::reset ( )
overridevirtual

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 from Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks.

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

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 from Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks.

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

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.

Implements Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks.

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

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.

Implements Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks.

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

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 from Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks.

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

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.

Implements Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks.

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

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 from Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks.

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

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.

Implements Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks.

virtual SmtSolver::Ptr Rose::BinaryAnalysis::ModelChecker::P2Model::SemanticCallbacks::createSolver ( )
overridevirtual

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.

Implements Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks.

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

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 from Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks.

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

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 from Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks.

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

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 from Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks.

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

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.

Implements Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks.

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

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.

Implements Rose::BinaryAnalysis::ModelChecker::SemanticCallbacks.


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