|
ROSE
0.11.102.0
|
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.
#include <Rose/BinaryAnalysis/ModelChecker/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< SymbolicExpression::Ptr > | assertions () 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 SymbolicExpression::Ptr &assertion, const SmtSolver::Evidence &, const InstructionSemantics::BaseSemantics::StatePtr &parentOutgoingState) |
| Construct a path by extending some other path. More... | |
Protected Member Functions | |
| Path (const PathNodePtr &end) | |
|
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 |
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<SymbolicExpression::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.
1.8.10