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 <Rose/BinaryAnalysis/ModelChecker/BasicBlockUnit.h>
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 InstructionSemantics::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 InstructionSemantics::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 |
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.
|
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.
|
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.
|
overridevirtual |
Print the header information in YAML format.
Implements Rose::BinaryAnalysis::ModelChecker::ExecutionUnit.
|
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.
|
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.
|
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.
|
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.
|
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:
