ROSE  0.11.51.0
Public Types | Public Member Functions | List of all members
Rose::BinaryAnalysis::ModelChecker::ExecutionUnit Class Referenceabstract

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 <ExecutionUnit.h>

Inheritance diagram for Rose::BinaryAnalysis::ModelChecker::ExecutionUnit:
Inheritance graph
[legend]

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 InstructionSemantics2::BaseSemantics::RiscOperatorsPtr &)=0
 Execute the unit to create a new state. 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...
 

Member Typedef Documentation

Shared ownership pointer for an execution unit.

Definition at line 22 of file ExecutionUnit.h.

Member Function Documentation

virtual std::string Rose::BinaryAnalysis::ModelChecker::ExecutionUnit::printableName ( ) const
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.

virtual void Rose::BinaryAnalysis::ModelChecker::ExecutionUnit::printSteps ( const SettingsPtr &  ,
std::ostream &  ,
const std::string &  prefix,
size_t  stepOrigin,
size_t  maxSteps 
) const
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.

virtual void Rose::BinaryAnalysis::ModelChecker::ExecutionUnit::toYamlHeader ( const SettingsPtr &  ,
std::ostream &  ,
const std::string &  prefix 
) const
pure virtual
virtual void Rose::BinaryAnalysis::ModelChecker::ExecutionUnit::toYamlSteps ( const SettingsPtr &  ,
std::ostream &  ,
const std::string &  prefix,
size_t  stepOrigin,
size_t  maxSteps 
) const
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.

virtual size_t Rose::BinaryAnalysis::ModelChecker::ExecutionUnit::nSteps ( ) const
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 Sawyer::Optional<rose_addr_t> Rose::BinaryAnalysis::ModelChecker::ExecutionUnit::address ( ) const
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 bool Rose::BinaryAnalysis::ModelChecker::ExecutionUnit::containsUnknownInsn ( ) const
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.

virtual std::vector<TagPtr> Rose::BinaryAnalysis::ModelChecker::ExecutionUnit::execute ( const SettingsPtr &  ,
const SemanticCallbacksPtr &  ,
const InstructionSemantics2::BaseSemantics::RiscOperatorsPtr  
)
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 InstructionSemantics2::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 Tag::Ptr directly–these are std::shared_ptr that 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: