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

Description

An execution unit for a basic block.

This is a model checker execution unit representing a complete basic block.

Definition at line 16 of file BasicBlockUnit.h.

#include <BasicBlockUnit.h>

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

Public Types

using Ptr = BasicBlockUnitPtr
 
- Public Types inherited from Rose::BinaryAnalysis::ModelChecker::ExecutionUnit
using Ptr = ExecutionUnitPtr
 Shared ownership pointer for an execution unit. More...
 

Public Member Functions

Partitioner2::BasicBlockPtr basicBlock () const
 Property: Basic block. More...
 
virtual std::string printableName () const override
 Property: Printable name. More...
 
virtual void printSteps (const SettingsPtr &, std::ostream &, const std::string &prefix, size_t stepOrigin, size_t maxSteps) const override
 Print the steps for this execution unit. More...
 
virtual void toYamlHeader (const SettingsPtr &, std::ostream &, const std::string &prefix) const override
 Print the header information in YAML format. More...
 
virtual void toYamlSteps (const SettingsPtr &, std::ostream &, const std::string &prefix, size_t stepOrigin, size_t maxSteps) const override
 Print the steps for this execution unit in YAML format. More...
 
virtual size_t nSteps () const override
 Property: Number of steps required to execute this unit. More...
 
virtual Sawyer::Optional< rose_addr_t > address () const override
 Property: Address if it has one. More...
 
virtual bool containsUnknownInsn () const override
 Predicate to test for unknown instructions. More...
 
virtual std::vector< TagPtr > execute (const SettingsPtr &, const SemanticCallbacksPtr &, const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &) override
 Execute the unit to create a new state. More...
 
- Public Member Functions inherited from Rose::BinaryAnalysis::ModelChecker::ExecutionUnit
 ExecutionUnit (const SourceLocation &)
 
SourceLocation sourceLocation () const
 Property: Location in source code. More...
 
TagPtr executeInstruction (const SettingsPtr &, SgAsmInstruction *, const InstructionSemantics2::BaseSemantics::DispatcherPtr &, size_t nodeStep)
 Execute a single instruction semantically. More...
 
void printSource (const SettingsPtr &, std::ostream &, const std::string &prefix) const
 List source location. More...
 
void printSource (const SettingsPtr &, std::ostream &, const std::string &prefix, const SourceLocation &) const
 List source location. More...
 

Static Public Member Functions

static Ptr instance (const Partitioner2::Partitioner &, const Partitioner2::BasicBlockPtr &)
 Allocating constructor. More...
 

Protected Member Functions

 BasicBlockUnit (const Partitioner2::Partitioner &partitioner, const Partitioner2::BasicBlockPtr &)
 

Member Function Documentation

static Ptr Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit::instance ( const Partitioner2::Partitioner ,
const Partitioner2::BasicBlockPtr  
)
static

Allocating constructor.

Constructs a new execution unit that holds the specified basic block, which must not be null.

Thread safety: This constructor is thread safe.

Partitioner2::BasicBlockPtr Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit::basicBlock ( ) const

Property: Basic block.

This is the basic block associated with this execution unit. This property is read-only and initialized when this execution unit is created.

Thread safety: This property accessor is thread safe.

virtual std::string Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit::printableName ( ) const
overridevirtual

Property: Printable name.

This returns the name of this unit as a single line that is suitable for terminal output.

Thread safety: The implementation must be thread safe.

Implements Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.

virtual void Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit::printSteps ( const SettingsPtr &  ,
std::ostream &  ,
const std::string &  prefix,
size_t  stepOrigin,
size_t  maxSteps 
) const
overridevirtual

Print the steps for this execution unit.

The output should show each step starting on its own line indented by the specified prefix. The steps should be numbered starting from stepOrigin. Additional details about the step should be on subsequent lines and indented in units of two spaces at a time.

Thread safety: The implementation must be thread safe but may allow other threads to output to the same stream concurrently.

Implements Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.

virtual void Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit::toYamlHeader ( const SettingsPtr &  ,
std::ostream &  ,
const std::string &  prefix 
) const
overridevirtual

Print the header information in YAML format.

Implements Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.

virtual void Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit::toYamlSteps ( const SettingsPtr &  ,
std::ostream &  ,
const std::string &  prefix,
size_t  stepOrigin,
size_t  maxSteps 
) const
overridevirtual

Print the steps for this execution unit in YAML format.

The output should show each step starting on its own line indented by the specified prefix. The steps should be numbered starting from stepOrigin. Additional details about the steps should be indented further.

Thread safety: The implementation must be thread safe but may allow other threads to output to the same stream concurrently.

Implements Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.

virtual size_t Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit::nSteps ( ) const
overridevirtual

Property: Number of steps required to execute this unit.

This is a user-defined measure of the approximate difficulty of executing this unit. For instance, it could be the number of instructions that are executed. The number of steps returned by this method should generally agree with the number of steps printed when displaying this unit.

Thread safety: The implementation must be thread safe. The easiest way to achieve this is to ensure that the information doesn't change during model checking.

Implements Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.

virtual Sawyer::Optional<rose_addr_t> Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit::address ( ) const
overridevirtual

Property: Address if it has one.

Returns the address of this execution unit if it has one.

The default implementation always returns nothing.

Thread safety: The implementation must be thread safe.

Reimplemented from Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.

virtual bool Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit::containsUnknownInsn ( ) const
overridevirtual

Predicate to test for unknown instructions.

Returns true if the execution unit contains any instructions whose machine bytes exist but could not be decoded. This typically indicates that we're trying to execute data or we've chosen the wrong instruction set architecture.

The default implementation always returns false.

Thread safety: The implementation must be thread safe.

Reimplemented from Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.

virtual std::vector<TagPtr> Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit::execute ( const SettingsPtr &  ,
const SemanticCallbacksPtr &  ,
const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr  
)
overridevirtual

Execute the unit to create a new state.

The supplied RiscOperators argument has an attached state that should be modified in place according to the semantics of the execution unit. It returns zero or more tags to be added to the path node.

This method is not responsible for adding new paths to the work queue–it only updates the state.

Thread safety: The implementation need not be thread safe.

Implements Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.


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