Description
An execution unit for an externally linked function.
This execution unit represents a call to an external function which is not loaded as part of the memory image for the specimen under consideration. Executing such a call uses the calling conventions to set certain locations to undefined values. At some point in the future we might provide a more precise way of executing these functions, but this will do for now.
Definition at line 20 of file ExternalFunctionUnit.h.
#include <Rose/BinaryAnalysis/ModelChecker/ExternalFunctionUnit.h>
Public Types | |
| using | Ptr = ExternalFunctionUnitPtr |
 Public Types inherited from Rose::BinaryAnalysis::ModelChecker::ExecutionUnit | |
| using | Ptr = ExecutionUnitPtr |
| Shared ownership pointer for an execution unit. More... | |
Public Member Functions | |
| Partitioner2::FunctionPtr | function () const |
| Property: Function. 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 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... | |
| virtual bool | containsUnknownInsn () const |
| Predicate to test for unknown instructions. 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::FunctionPtr &, const SourceLocation &) |
| Allocating constructor. More... | |
Protected Member Functions | |
| ExternalFunctionUnit (const Partitioner2::FunctionPtr &, const SourceLocation &) | |
Member Function Documentation
|
static |
Allocating constructor.
Constructs a new execution unit that holds the specified function, which must not be null.
Thread safety: This constructor is thread safe.
| Partitioner2::FunctionPtr Rose::BinaryAnalysis::ModelChecker::ExternalFunctionUnit::function | ( | ) | const |
Property: Function.
This is the function associated with the execution unit. This property is read-only and initialized when this execution object 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 |
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:
