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

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>

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

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 Ptr Rose::BinaryAnalysis::ModelChecker::ExternalFunctionUnit::instance ( const Partitioner2::FunctionPtr ,
const SourceLocation  
)
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.

virtual std::string Rose::BinaryAnalysis::ModelChecker::ExternalFunctionUnit::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::ExternalFunctionUnit::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::ExternalFunctionUnit::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::ExternalFunctionUnit::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::ExternalFunctionUnit::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::ExternalFunctionUnit::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 std::vector<TagPtr> Rose::BinaryAnalysis::ModelChecker::ExternalFunctionUnit::execute ( const SettingsPtr &  ,
const SemanticCallbacksPtr &  ,
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr riscOperators 
)
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: