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

Description

Execution path.

An execution path points to a node in the execution tree which serves as the last node of this path. The functions defined in this interface operate on paths as a whole instead of single nodes.

Definition at line 21 of file Path.h.

#include <Path.h>

Public Types

using Ptr = PathPtr
 

Public Member Functions

bool isEmpty () const
 Test for empty path. More...
 
size_t nNodes () const
 Length of path in nodes. More...
 
size_t nSteps () const
 Length of path in steps. More...
 
double processingTime () const
 Total time to process path. More...
 
bool executionFailed () const
 Property: Whether execution has failed. More...
 
std::vector< SymbolicExpr::Ptrassertions () const
 All SMT assertions along the path. More...
 
PathNodePtr lastNode () const
 Last node of the path. More...
 
std::vector< PathNodePtr > nodes () const
 Nodes composing path. More...
 
std::string printableName () const
 Short name suitable for printing in diagnostics. More...
 
void print (const SettingsPtr &, std::ostream &, const std::string &prefix, size_t maxSteps) const
 Multi-line output of path. More...
 
void toYaml (const SettingsPtr &, std::ostream &, const std::string &prefix, size_t maxSteps) const
 Multi-line output of path. More...
 
uint64_t hash () const
 Path hash. More...
 
void hash (Combinatorics::Hasher &) const
 Path hash. More...
 

Static Public Member Functions

static Ptr instance (const ExecutionUnitPtr &)
 Construct a path that is one vertex in length. More...
 
static Ptr instance (const PathPtr &prefix, const ExecutionUnitPtr &, const SymbolicExpr::Ptr &assertion, const SmtSolver::Evidence &, const InstructionSemantics2::BaseSemantics::StatePtr &parentOutgoingState)
 Construct a path by extending some other path. More...
 

Protected Member Functions

 Path (const PathNodePtr &end)
 

Member Function Documentation

static Ptr Rose::BinaryAnalysis::ModelChecker::Path::instance ( const ExecutionUnitPtr &  )
static

Construct a path that is one vertex in length.

This constructs a root path that contains only one execution unit.

Thread safety: This constructor is thread safe.

static Ptr Rose::BinaryAnalysis::ModelChecker::Path::instance ( const PathPtr &  prefix,
const ExecutionUnitPtr &  ,
const SymbolicExpr::Ptr assertion,
const SmtSolver::Evidence ,
const InstructionSemantics2::BaseSemantics::StatePtr parentOutgoingState 
)
static

Construct a path by extending some other path.

The new path will extend the prefix path by adding the specified execution unit. An assertion must be provided that is already known to be true for the extended path (but it will not be checked by this method).

Thread safety: This constructor is thread safe.

bool Rose::BinaryAnalysis::ModelChecker::Path::isEmpty ( ) const

Test for empty path.

Returns true if the path is empty, false otherwise.

Thread safety: This method is thread safe.

size_t Rose::BinaryAnalysis::ModelChecker::Path::nNodes ( ) const

Length of path in nodes.

Returns the length of the path in nodes.

Thread safety: This method is thread safe.

size_t Rose::BinaryAnalysis::ModelChecker::Path::nSteps ( ) const

Length of path in steps.

Returns the length of the path in steps, .

Thread safety: This method is thread safe.

double Rose::BinaryAnalysis::ModelChecker::Path::processingTime ( ) const

Total time to process path.

Returns the total elapsed time to process this path by summing the elapsed times for each of this path's nodes. The returned time is measured in seconds. It excludes nodes for which no timing information is available, such as nodes that have not been executed yet.

Thread safety: This method is thread safe.

uint64_t Rose::BinaryAnalysis::ModelChecker::Path::hash ( ) const

Path hash.

Hashes a path by hashing the address of each node. This results in a useful identification number for a path that's stable across different runs of a tool.

Thread safety: This method is thread safe.

void Rose::BinaryAnalysis::ModelChecker::Path::hash ( Combinatorics::Hasher ) const

Path hash.

Hashes a path by hashing the address of each node. This results in a useful identification number for a path that's stable across different runs of a tool.

Thread safety: This method is thread safe.

bool Rose::BinaryAnalysis::ModelChecker::Path::executionFailed ( ) const

Property: Whether execution has failed.

This property is true if there has been a previous attempt to execute this path and that attempt has failed.

Thread safety: This method is thread safe.

std::vector<SymbolicExpr::Ptr> Rose::BinaryAnalysis::ModelChecker::Path::assertions ( ) const

All SMT assertions along the path.

Returns the list of all assertions that are required along the specified path.

Thread safety: This method is thread safe.

PathNodePtr Rose::BinaryAnalysis::ModelChecker::Path::lastNode ( ) const

Last node of the path.

Returns the last node of the path if the path is not empty. Returns null if the path is empty.

Thread safety: This method is thread safe.

std::vector<PathNodePtr> Rose::BinaryAnalysis::ModelChecker::Path::nodes ( ) const

Nodes composing path.

Returns a vector of the nodes that make up the path in the order they were executed.

Note: If you're able to process the path from its end toward its beginning, then it's more efficient to use each node's parent pointer instead of creating a vector of all the pointers.

Thread safety: This method is thread safe.

std::string Rose::BinaryAnalysis::ModelChecker::Path::printableName ( ) const

Short name suitable for printing in diagnostics.

Thread safety: This method is thread safe.

void Rose::BinaryAnalysis::ModelChecker::Path::print ( const SettingsPtr &  ,
std::ostream &  ,
const std::string &  prefix,
size_t  maxSteps 
) const

Multi-line output of path.

Prints details about a path in a multi-line text format. Up to maxSteps steps are printed.

Thread safety: This method is thread safe although the output from this thread may interleave with output from other threads.

void Rose::BinaryAnalysis::ModelChecker::Path::toYaml ( const SettingsPtr &  ,
std::ostream &  ,
const std::string &  prefix,
size_t  maxSteps 
) const

Multi-line output of path.

Prints details about a path in YAML format. Up to maxSteps steps are printed.

Thread safety: This method is thread safe although the output from this thread may interleave with output from other threads.


The documentation for this class was generated from the following file: