Description
One unit of execution.
A unit of execution can be a basic block, a single instruction, a function summary, or any other user-defined item. Users are expected to subclass this as necessary.
Definition at line 19 of file ExecutionUnit.h.
#include <Rose/BinaryAnalysis/ModelChecker/ExecutionUnit.h>
Public Types | |
| using | Ptr = ExecutionUnitPtr |
| Shared ownership pointer for an execution unit. More... | |
Public Member Functions | |
| ExecutionUnit (const SourceLocation &) | |
| virtual std::string | printableName () const =0 |
| Property: Printable name. More... | |
| virtual void | printSteps (const SettingsPtr &, std::ostream &, const std::string &prefix, size_t stepOrigin, size_t maxSteps) const =0 |
| Print the steps for this execution unit. More... | |
| virtual void | toYamlHeader (const SettingsPtr &, std::ostream &, const std::string &prefix) const =0 |
| 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 =0 |
| Print the steps for this execution unit in YAML format. More... | |
| virtual size_t | nSteps () const =0 |
| Property: Number of steps required to execute this unit. More... | |
| virtual Sawyer::Optional< rose_addr_t > | address () const |
| Property: Address if it has one. More... | |
| SourceLocation | sourceLocation () const |
| Property: Location in source code. More... | |
| virtual bool | containsUnknownInsn () const |
| Predicate to test for unknown instructions. More... | |
| virtual std::vector< TagPtr > | execute (const SettingsPtr &, const SemanticCallbacksPtr &, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &riscOperators)=0 |
| Execute the unit to create a new state. 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... | |
Member Typedef Documentation
| using Rose::BinaryAnalysis::ModelChecker::ExecutionUnit::Ptr = ExecutionUnitPtr |
Shared ownership pointer for an execution unit.
Definition at line 22 of file ExecutionUnit.h.
Member Function Documentation
|
pure virtual |
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.
Implemented in Rose::BinaryAnalysis::ModelChecker::FailureUnit, Rose::BinaryAnalysis::ModelChecker::ExternalFunctionUnit, Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit, and Rose::BinaryAnalysis::ModelChecker::InstructionUnit.
|
pure virtual |
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.
Implemented in Rose::BinaryAnalysis::ModelChecker::FailureUnit, Rose::BinaryAnalysis::ModelChecker::ExternalFunctionUnit, Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit, and Rose::BinaryAnalysis::ModelChecker::InstructionUnit.
|
pure virtual |
Print the header information in YAML format.
Implemented in Rose::BinaryAnalysis::ModelChecker::FailureUnit, Rose::BinaryAnalysis::ModelChecker::ExternalFunctionUnit, Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit, and Rose::BinaryAnalysis::ModelChecker::InstructionUnit.
|
pure virtual |
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.
Implemented in Rose::BinaryAnalysis::ModelChecker::FailureUnit, Rose::BinaryAnalysis::ModelChecker::ExternalFunctionUnit, Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit, and Rose::BinaryAnalysis::ModelChecker::InstructionUnit.
| void Rose::BinaryAnalysis::ModelChecker::ExecutionUnit::printSource | ( | const SettingsPtr & | , |
| std::ostream & | , | ||
| const std::string & | prefix | ||
| ) | const |
List source location.
List some source lines if we can find them. If a source location is specified, use it, otherwise use the source location associated with this execution unit. If the source location is empty, then nothing is printed.
Thread safety: This method is thread safe.
| void Rose::BinaryAnalysis::ModelChecker::ExecutionUnit::printSource | ( | const SettingsPtr & | , |
| std::ostream & | , | ||
| const std::string & | prefix, | ||
| const SourceLocation & | |||
| ) | const |
List source location.
List some source lines if we can find them. If a source location is specified, use it, otherwise use the source location associated with this execution unit. If the source location is empty, then nothing is printed.
Thread safety: This method is thread safe.
|
pure virtual |
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.
Implemented in Rose::BinaryAnalysis::ModelChecker::FailureUnit, Rose::BinaryAnalysis::ModelChecker::ExternalFunctionUnit, Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit, and Rose::BinaryAnalysis::ModelChecker::InstructionUnit.
|
virtual |
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 in Rose::BinaryAnalysis::ModelChecker::FailureUnit, Rose::BinaryAnalysis::ModelChecker::ExternalFunctionUnit, Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit, and Rose::BinaryAnalysis::ModelChecker::InstructionUnit.
| SourceLocation Rose::BinaryAnalysis::ModelChecker::ExecutionUnit::sourceLocation | ( | ) | const |
Property: Location in source code.
This property holds an optional source location record.
Thread safety: This property accessor is thread safe.
|
virtual |
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 in Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit.
|
pure virtual |
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.
Implemented in Rose::BinaryAnalysis::ModelChecker::FailureUnit, Rose::BinaryAnalysis::ModelChecker::BasicBlockUnit, Rose::BinaryAnalysis::ModelChecker::ExternalFunctionUnit, and Rose::BinaryAnalysis::ModelChecker::InstructionUnit.
| TagPtr Rose::BinaryAnalysis::ModelChecker::ExecutionUnit::executeInstruction | ( | const SettingsPtr & | , |
| SgAsmInstruction * | , | ||
| const InstructionSemantics::BaseSemantics::DispatcherPtr & | , | ||
| size_t | nodeStep | ||
| ) |
Execute a single instruction semantically.
This is a support function for executing a single instruction semantically. Doing this consistently is a little hard because of the different kinds of exceptions that can be thrown by the semantics layers, and the need to indicate to the caller whether the execution failed or succeeded independently of returning tags and without any particular specialized support in the semantics layers.
The low level semantic execution can indicate a failure in different ways:
- It can set the current state of the RISC operators to null. Since this doesn't involve exceptions, it's sometimes the fastest way to indicate the failure, but it doesn't say why the failure occurred.
- It can throw a Rose::Exception which will be caught by this function and emitted in the diagnostic output. This function will then make sure the current state of the RISC operators is null before returning.
- It can throw a Tag wrapped in a ThrownTag object, which this function catches and returns. The tag is printed in the diagnostic output and the current state of the RISC operators is set to null before returning. Do not throw a ModelChecker::Tag::Ptr directly–these are
std::shared_ptrthat don't interact well with C++ try/catch.
Limitations of this design:
- It is currently possible to return only one tag by throwing it. If this is a problem, the natural solution is to extend the ThrownTag to hold more than one pointer.
- It is not currently possible to return a tag and have the execution succeed. This is because Dispatcher::processInstruction doesn't catch exceptions and therefore does not perform any final operations on the semantic state.
Thread safety: This method is NOT thread safe.
The documentation for this class was generated from the following file:
