|
ROSE 0.11.145.147
|
Data-flow engine.
The data-flow engine traverses the supplied control flow graph, runs the transfer function at each vertex, and merges data state objects as necessary.
The template arguments are:
CFG is the type for the control flow graph. It must implement the Sawyer::Container::Graph API and have vertex ID numbers of type size_t. The data-flow will follow the edges of this graph, invoking a transfer function (see below) at each vertex. The vertices are usually basic blocks or instructions, although they can be anything that the transfer function can understand. For instance, its possible for a called function to be represented by a special vertex that encapsulates the entire effect of the function, either encoded in the vertex itself or as a special case in the transfer function. Although a normal CFG can be used, one often passes either a subgraph of the CFG or an entirely different kind of control flow graph. Subgraphs are useful for solving data-flow for a single function, and different types are useful for passing additional/different information to the transfer function.State is an object that stores (or points to) an analysis state: the values that the data flow is manipulating. A state object is attached to each vertex of the CFG to represent the data-flow state at that vertex. For instance, the state might be a map of abstract locations (e.g., variables) and their current values, such as an instruction semantics State object. If the State type is a pointer to a state, then since the engine doesn't implement any particular ownership paradigm, the State type should be some kind of shared-ownership pointer so that the objects are properly freed. See the description of the MergeFunction below for more info about the values stored in state object.TransferFunction is a functor that is invoked at each CFG vertex to create a new vertex output state from its input state. The functor is called with three arguments: a const reference to the control flow graph, the CFG vertex ID for the vertex being processed, and the incoming state for that vertex. The call should return a new outgoing state. For instance, if the CFG vertices contain SgAsmInstruction nodes and the State is a pointer to an instruction semantics state, then the transfer function would most likely perform these operations: create a new state by cloning the incoming state, attach the new state to an instruction semantics dispatcher (virtual CPU), call the dispatcher's processInstruction, return the new state. The transfer functor should also have a toString method that returns an optional string containing one or more lines, which is used for debugging (this method often just delegates to a similar method in the state, but that's not always possible, which is why we define it here).MergeFunction is a functor that takes two State objects and merges the second state into the first state. Therefore, the first argument should be a reference. The MergeFunction returns true if the first state changed, false if there was no change. In order for a data-flow to reach a fixed point the values must form a lattice and a merge operation should return a value which is the greatest lower bound. This implies that the lattice has a bottom element that is a descendent of all other vertices. However, the data-flow engine is designed to also operate in cases where a fixed point cannot be reached.PathFeasibility is a predicate that returns true if the data-flow should traverse the specified CFG edge. It's called with the following arguments: (1) the CFG, which it should accept as a const reference argument for efficiency's sake; (2) the edge that should be tested by this predicate; (3) the incoming state for the edge, i.e., the outgoing state for the edge's source vertex; and (4) the outgoing state for the edge, i.e., the incoming state for the edge's target vertex.A common configuration for an engine is to use a control-flow graph whose vertices are basic blocks, whose State is a pointer to an instruction semantics state, whose TransferFunction calls Dispatcher::processInstruction, and whose MergeFunction calls the state's merge method.
The control flow graph and transfer function are specified in the engine's constructor. The starting CFG vertex and its initial state are supplied when the engine starts to run.
Definition at line 315 of file DataFlow.h.
#include <Rose/BinaryAnalysis/DataFlow.h>
Public Types | |
| using | Cfg = Cfg_ |
| Type of the data-flow control flow graph. | |
| using | State = State_ |
| Type of the states stored at each CFG vertex. | |
| using | TransferFunction = TransferFunction_ |
| Type of the transfer function that creates new states. | |
| using | MergeFunction = MergeFunction_ |
| Type of the function that merges two states into a single state. | |
| using | PathFeasibility = PathFeasibility_ |
| Predicate testing whether certain CFG edges should be followed. | |
| using | VertexStates = std::vector< State > |
| Vector of states per vertex. | |
| using | CFG = Cfg_ |
Public Member Functions | |
| Engine (const Cfg &cfg, TransferFunction &xfer, MergeFunction merge=MergeFunction(), PathFeasibility isFeasible=PathFeasibility()) | |
| Constructor. | |
| const Cfg & | cfg () const |
| Data-flow control flow graph. | |
| void | reset (State initialState=State()) |
| Reset engine to initial state. | |
| std::string | prefix () const |
| Line prefix for debugging. | |
| size_t | nIterations () const |
| Number of iterations run. | |
| bool | runOneIteration () |
| Runs one iteration. | |
| void | insertStartingVertex (size_t startVertexId, const State &initialState) |
| Add a starting vertex. | |
| void | runToFixedPoint () |
| Run data-flow until it reaches a fixed point. | |
| void | runToFixedPoint (size_t startVertexId, const State &initialState) |
| Add starting point and run to fixed point. | |
| State | getInitialState (size_t cfgVertexId) const |
| Return the incoming state for the specified CFG vertex. | |
| void | setInitialState (size_t cfgVertexId, State state) |
| Set the initial state for the specified CFG vertex. | |
| State | getFinalState (size_t cfgVertexId) const |
| Return the outgoing state for the specified CFG vertex. | |
| const VertexStates & | getInitialStates () const |
| All incoming states. | |
| const VertexStates & | getFinalStates () const |
| All outgoing states. | |
| const std::string & | name () const |
| Property: Name for debugging. | |
| void | name (const std::string &s) |
| Property: Name for debugging. | |
| size_t | maxIterations () const |
| Max number of iterations to allow. | |
| void | maxIterations (size_t n) |
| Max number of iterations to allow. | |
| using Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::Cfg = Cfg_ |
Type of the data-flow control flow graph.
Definition at line 317 of file DataFlow.h.
| using Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::State = State_ |
Type of the states stored at each CFG vertex.
Definition at line 318 of file DataFlow.h.
| using Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::TransferFunction = TransferFunction_ |
Type of the transfer function that creates new states.
Definition at line 319 of file DataFlow.h.
| using Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::MergeFunction = MergeFunction_ |
Type of the function that merges two states into a single state.
Definition at line 320 of file DataFlow.h.
| using Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::PathFeasibility = PathFeasibility_ |
Predicate testing whether certain CFG edges should be followed.
Definition at line 321 of file DataFlow.h.
| using Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::VertexStates = std::vector<State> |
Vector of states per vertex.
Definition at line 322 of file DataFlow.h.
| using Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::CFG = Cfg_ |
Definition at line 324 of file DataFlow.h.
|
inline |
Constructor.
Constructs a new data-flow engine that will operate over the specified control flow graph using the specified transfer function. The control flow graph is incorporated into the engine by reference; the transfer functor is copied.
Definition at line 345 of file DataFlow.h.
|
inline |
Data-flow control flow graph.
Returns a reference to the control flow graph that's being used for the data-flow analysis. The return value is the same control flow graph as which was supplied to the constructor.
Definition at line 355 of file DataFlow.h.
|
inline |
Reset engine to initial state.
Definition at line 360 of file DataFlow.h.
References Sawyer::Container::DistinctList< T, Cmp >::clear().
Referenced by Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::Engine(), and Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::runToFixedPoint().
|
inline |
Property: Name for debugging.
This optional name will show up in debugging output.
Definition at line 375 of file DataFlow.h.
Referenced by Rose::BinaryAnalysis::TaintedFlow::runToFixedPoint().
|
inline |
Property: Name for debugging.
This optional name will show up in debugging output.
Definition at line 376 of file DataFlow.h.
|
inline |
Line prefix for debugging.
Definition at line 380 of file DataFlow.h.
Referenced by Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::runOneIteration().
|
inline |
Max number of iterations to allow.
Allow N number of calls to runOneIteration. When the limit is exceeded a NotConverging exception is thrown.
Definition at line 394 of file DataFlow.h.
|
inline |
Max number of iterations to allow.
Allow N number of calls to runOneIteration. When the limit is exceeded a NotConverging exception is thrown.
Definition at line 395 of file DataFlow.h.
|
inline |
Number of iterations run.
The number of times runOneIteration was called since the last reset.
Definition at line 401 of file DataFlow.h.
|
inline |
Runs one iteration.
Runs one step of data-flow analysis by consuming the first item on the work list. Returns false if the work list is empty (before of after the iteration).
Definition at line 407 of file DataFlow.h.
References Sawyer::Container::DistinctList< T, Cmp >::isEmpty(), Sawyer::Container::DistinctList< T, Cmp >::items(), Rose::StringUtility::numberToString(), Rose::StringUtility::plural(), Sawyer::Container::DistinctList< T, Cmp >::popFront(), Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::prefix(), Rose::StringUtility::prefixLines(), and Sawyer::Container::DistinctList< T, Cmp >::pushBack().
Referenced by Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::runToFixedPoint(), and Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::runToFixedPoint().
|
inline |
Add a starting vertex.
Definition at line 464 of file DataFlow.h.
References Sawyer::Container::DistinctList< T, Cmp >::pushBack().
Referenced by Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::runToFixedPoint().
|
inline |
Run data-flow until it reaches a fixed point.
Run data-flow starting at the specified control flow vertex with the specified initial state until the state converges to a fixed point or the maximum number of iterations is reached (in which case a NotConverging exception is thrown).
Definition at line 474 of file DataFlow.h.
Referenced by Rose::BinaryAnalysis::TaintedFlow::runToFixedPoint().
|
inline |
Add starting point and run to fixed point.
This is a combination of reset, insertStartingVertex, and runToFixedPoint.
Definition at line 481 of file DataFlow.h.
References Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::insertStartingVertex(), Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::reset(), and Rose::BinaryAnalysis::DataFlow::Engine< Cfg_, State_, TransferFunction_, MergeFunction_, PathFeasibility_ >::runOneIteration().
|
inline |
Return the incoming state for the specified CFG vertex.
This is a pointer to the incoming state for the vertex as of the latest data-flow iteration. If the data-flow has not reached this vertex then it is likely to be a null pointer.
Definition at line 491 of file DataFlow.h.
|
inline |
Set the initial state for the specified CFG vertex.
Definition at line 496 of file DataFlow.h.
|
inline |
Return the outgoing state for the specified CFG vertex.
This is a pointer to the outgoing state for the vertex as of the latest data-flow iteration. If the data-flow has not processed this vertex then it is likely to be a null pointer.
Definition at line 504 of file DataFlow.h.
|
inline |
All incoming states.
Returns a vector indexed by vertex ID for the incoming state of each vertex as of the latest data-flow iteration. States for vertices that have not yet been reached are null pointers.
Definition at line 512 of file DataFlow.h.
|
inline |
All outgoing states.
Returns a vector indexed by vertex ID for the outgoing state of each vertex as of the latest data-flow iteration. States for vertices that have not yet been processed are null pointers.
Definition at line 520 of file DataFlow.h.
Referenced by Rose::BinaryAnalysis::TaintedFlow::runToFixedPoint().
1.9.8