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

Description

Definition at line 24 of file PathNode.h.

Classes

class  BorrowedOutgoingState
 

Public Types

using Ptr = PathNodePtr
 Shared-ownership pointer. More...
 

Public Member Functions

uint32_t id () const
 Property: Identifier. More...
 
Ptr parent () const
 Property: Parent node. More...
 
ExecutionUnitPtr executionUnit () const
 Property: Unit of execution. More...
 
size_t nSteps () const
 Length of node in steps. More...
 
void assertion (const SymbolicExpression::Ptr &)
 Insert an assertion for the SMT solver. More...
 
std::vector< SymbolicExpression::Ptrassertions () const
 Returns all the assersions for this node. More...
 
SmtSolver::Evidence evidence () const
 Returns the SMT solver evidence for path feasibility. More...
 
void execute (const SettingsPtr &, const SemanticCallbacksPtr &, const InstructionSemantics::BaseSemantics::RiscOperatorsPtr &, const SmtSolver::Ptr &)
 Execute this node. More...
 
bool executionFailed () const
 Property: Whether execution has failed. More...
 
InstructionSemantics::BaseSemantics::StatePtr copyOutgoingState () const
 Returns a copy of the outgoing state. More...
 
BorrowedOutgoingState borrowOutgoingState ()
 Borrow the state from a node. More...
 
void releaseOutgoingState ()
 Release the outgoing state. More...
 
size_t nTags () const
 Number of tags attached to this node. More...
 
std::vector< TagPtr > tags () const
 All tags for this node. More...
 
double processingTime () const
 Time spent processing this node. More...
 
void incrementProcessingTime (double seconds)
 Add additional time to the processing time. More...
 
Sawyer::Optional< rose_addr_t > address () const
 Address of execution unit. More...
 
std::string printableName () const
 Printable name for this node. More...
 
void toYamlHeader (const SettingsPtr &, std::ostream &, const std::string &prefix) const
 Output path node header as YAML. More...
 
void toYamlSteps (const SettingsPtr &, std::ostream &, const std::string &prefix, size_t stepOrigin, size_t maxSteps) const
 Output the steps as YAML. More...
 
double sortKey () const
 Property: Key for user-defined sorting. More...
 
void sortKey (double)
 Property: Key for user-defined sorting. More...
 
void appendTag (const TagPtr &)
 Append tags. More...
 
void appendTags (const std::vector< TagPtr > &)
 Append tags. More...
 

Static Public Member Functions

static Ptr instance (const ExecutionUnitPtr &)
 Construct a root node. More...
 
static Ptr instance (const Ptr &parent, const ExecutionUnitPtr &, const SymbolicExpression::Ptr &assertion, const SmtSolver::Evidence &, const InstructionSemantics::BaseSemantics::StatePtr &parentOutgoingState)
 Construct a child node. More...
 

Protected Member Functions

 PathNode (const ExecutionUnitPtr &)
 Allocating constructor. More...
 
 PathNode (const Ptr &parent, const ExecutionUnitPtr &, const SymbolicExpression::Ptr &assertion, const SmtSolver::Evidence &, const InstructionSemantics::BaseSemantics::StatePtr &parentOutgoingState)
 Allocating constructor. More...
 

Member Typedef Documentation

Shared-ownership pointer.

Definition at line 27 of file PathNode.h.

Constructor & Destructor Documentation

Rose::BinaryAnalysis::ModelChecker::PathNode::PathNode ( const ExecutionUnitPtr &  )
protected

Allocating constructor.

Create an initial path node. This node has no parent. See instance.

Rose::BinaryAnalysis::ModelChecker::PathNode::PathNode ( const Ptr parent,
const ExecutionUnitPtr &  ,
const SymbolicExpression::Ptr assertion,
const SmtSolver::Evidence ,
const InstructionSemantics::BaseSemantics::StatePtr parentOutgoingState 
)
protected

Allocating constructor.

Create a non-initial path node. This node is a continuation of the path ending at parent. See instance.

Member Function Documentation

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

Construct a root node.

A root node is the starting point for all paths within that virtual execution tree.

Thread safety: This constructor is thread safe.

static Ptr Rose::BinaryAnalysis::ModelChecker::PathNode::instance ( const Ptr parent,
const ExecutionUnitPtr &  ,
const SymbolicExpression::Ptr assertion,
const SmtSolver::Evidence ,
const InstructionSemantics::BaseSemantics::StatePtr parentOutgoingState 
)
static

Construct a child node.

A child node has the specified parent path as a prefix. The child node's incoming state will be the (eventually computed) outgoing state of the parent node, and a new outgoing state will eventually be computed for this node by "executing" this node in a worker thread. The assertion must be true but is not checked here.

Thread safety: This constructor is thread safe.

uint32_t Rose::BinaryAnalysis::ModelChecker::PathNode::id ( ) const

Property: Identifier.

Every node has a randomly generated identifier.

Thread safety: This property accessor is thread safe.

double Rose::BinaryAnalysis::ModelChecker::PathNode::sortKey ( ) const

Property: Key for user-defined sorting.

This property holds a user-defined value that can be used by the PathPrioritizer functions. The model checker framework itself does not use this property for anything and all new nodes initialize this property to NaN. If this is used for sorting, it generally shouldn't be changed once the node has been sorted into position. E.g., a priority queue will not automatically resort its members if any of their keys change.

Thread safety: This property accessor is thread safe.

void Rose::BinaryAnalysis::ModelChecker::PathNode::sortKey ( double  )

Property: Key for user-defined sorting.

This property holds a user-defined value that can be used by the PathPrioritizer functions. The model checker framework itself does not use this property for anything and all new nodes initialize this property to NaN. If this is used for sorting, it generally shouldn't be changed once the node has been sorted into position. E.g., a priority queue will not automatically resort its members if any of their keys change.

Thread safety: This property accessor is thread safe.

Ptr Rose::BinaryAnalysis::ModelChecker::PathNode::parent ( ) const

Property: Parent node.

The parent node is the execution path predecessor, the node that was executed prior to this current node. All nodes have a non-null predecessor except for the first node of an execution path, whose parent is null.

This property is read-only. The preceding node was specified when this object was created.

Thread safety: This method is thread safe.

ExecutionUnitPtr Rose::BinaryAnalysis::ModelChecker::PathNode::executionUnit ( ) const

Property: Unit of execution.

The unit of execution is the thing that's executed at this node of the path. It can be a single instruction, a basic block, a function summary, or anything else defined by the user by subclassing the ExecutionUnit type.

This property is read-only. The execution unit was specified when this object was created.

Thread safety: This method is thread safe.

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

Length of node in steps.

Returns the length of this node. The length is measured in terms of number of steps, which in turn is computed from the associated ExecutionUnit::nSteps properties.

Thread safety: This method is thread safe.

void Rose::BinaryAnalysis::ModelChecker::PathNode::assertion ( const SymbolicExpression::Ptr )

Insert an assertion for the SMT solver.

An assertion is a Boolean expression that can be true according to the model checker. The most common use for this during model checking is to indicate how the conditional branches in the path depend on other variables.

Thread safety: This method is thread safe.

std::vector<SymbolicExpression::Ptr> Rose::BinaryAnalysis::ModelChecker::PathNode::assertions ( ) const

Returns all the assersions for this node.

Thread safety: This method is thread safe.

SmtSolver::Evidence Rose::BinaryAnalysis::ModelChecker::PathNode::evidence ( ) const

Returns the SMT solver evidence for path feasibility.

Returns that evidence that shows that the path ending at this node is feasible.

Thread safety: This method is thread safe.

void Rose::BinaryAnalysis::ModelChecker::PathNode::execute ( const SettingsPtr &  ,
const SemanticCallbacksPtr &  ,
const InstructionSemantics::BaseSemantics::RiscOperatorsPtr ,
const SmtSolver::Ptr  
)

Execute this node.

If necessary, executes all predecessors recursively and then executes this node. Afterward, this node and all predecessors will store their outgoing states. Only nodes that have not bee previously executed are executed.

Although the RiscOperators may point to a solver already, the solver supplied as an argument is the one that's being used by the model checker itself.

Thread safety: This method is thread safe, but the RISC operators must be thread local.

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

Property: Whether execution has failed.

This property is true if there was a previous attempt to execute this node and that attempt failed.

Thread safety: This method is thread safe.

InstructionSemantics::BaseSemantics::StatePtr Rose::BinaryAnalysis::ModelChecker::PathNode::copyOutgoingState ( ) const

Returns a copy of the outgoing state.

If this node has been successfully executed, then a copy of its outgoing state is returned, otherwise null is returned.

See also, execute, which creates the outgoing state if necessary.

Thread safety: This method is thread safe. The state is owned by only this node.

BorrowedOutgoingState Rose::BinaryAnalysis::ModelChecker::PathNode::borrowOutgoingState ( )

Borrow the state from a node.

The semantic states generally don't have thread-safe APIs because they're designed to be transformed by calling a sequence of state-modifying functions. The model checker logic should prevent two threads from ever accessing a node's state concurrently, but we want to be able to check it, which is what this function does. It operates by having the node relinguish its state, and then returning the state at the end of the scope (either normal scope exit or exception). The borrowing is not foolproof–nothing prevents the borrower from keeping a reference to the state and continuing to use it after the borrow is returned.

{
PathNode::Ptr node = ...; // Some node not accessible by other threads, but we're not absolutely sure
auto borrowed = node->borrowOutgoingState(); // I now have the state, and the node doesn't have it
doSomethingWith(borrowed.state); // I can access and even modify the state with no other threads interfering
throw x; // I can even throw an exception
} // the state is now returned to the node, with abort if some other thread managed to give it a new state

Thread safety: This method is thread safe.

void Rose::BinaryAnalysis::ModelChecker::PathNode::releaseOutgoingState ( )

Release the outgoing state.

The outgoing state for this node is set to null. This should only be done after this path has been extended in all the ways it will ever be extended and its outgoing state pointer has been copied into the incoming state of each path extension.

Thread safety: This method is thread safe.

void Rose::BinaryAnalysis::ModelChecker::PathNode::appendTag ( const TagPtr &  )

Append tags.

The specified tags are added to the end of the tag list for this node.

Thread safety: This method is thread safe.

void Rose::BinaryAnalysis::ModelChecker::PathNode::appendTags ( const std::vector< TagPtr > &  )

Append tags.

The specified tags are added to the end of the tag list for this node.

Thread safety: This method is thread safe.

size_t Rose::BinaryAnalysis::ModelChecker::PathNode::nTags ( ) const

Number of tags attached to this node.

Thread safety: This method is thread safe.

std::vector<TagPtr> Rose::BinaryAnalysis::ModelChecker::PathNode::tags ( ) const

All tags for this node.

Thread safety: This method is thread safe.

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

Time spent processing this node.

Returns the elapsed time to process this node, measured in seconds.

Thread safety: This method is thread safe.

void Rose::BinaryAnalysis::ModelChecker::PathNode::incrementProcessingTime ( double  seconds)

Add additional time to the processing time.

Updates this node's processingTime by added the specified time in seconds.

Thread safety: This method is thread safe.

Sawyer::Optional<rose_addr_t> Rose::BinaryAnalysis::ModelChecker::PathNode::address ( ) const

Address of execution unit.

Thread safety: This method is thread safe.

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

Printable name for this node.

The returned string is suitable for terminal output, used mostly for debugging.

Thread safety: This method is thread safe.

void Rose::BinaryAnalysis::ModelChecker::PathNode::toYamlHeader ( const SettingsPtr &  ,
std::ostream &  ,
const std::string &  prefix 
) const

Output path node header as YAML.

The output does not include the individual steps for the node.

void Rose::BinaryAnalysis::ModelChecker::PathNode::toYamlSteps ( const SettingsPtr &  ,
std::ostream &  ,
const std::string &  prefix,
size_t  stepOrigin,
size_t  maxSteps 
) const

Output the steps as YAML.


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