| Copyright | (c) Galois Inc 2015 |
|---|---|
| License | BSD3 |
| Maintainer | Rob Dockins <rdockins@galois.com> |
| Stability | provisional |
| Safe Haskell | Safe-Inferred |
| Language | Haskell2010 |
Lang.Crucible.Analysis.DFS
Description
This module defines a generic algorithm for depth-first search traversal of a control flow graph.
Synopsis
- data DFSEdgeType
- type DFSNodeFunc ext blocks a = forall ret ctx. Block ext blocks ret ctx -> a -> a
- type DFSEdgeFunc blocks a = DFSEdgeType -> SomeBlockID blocks -> SomeBlockID blocks -> a -> a
- dfs :: DFSNodeFunc ext blocks a -> DFSEdgeFunc blocks a -> a -> CFG ext blocks init ret -> a
- run_dfs :: forall ext blocks a ret cxt. DFSNodeFunc ext blocks a -> DFSEdgeFunc blocks a -> BlockMap ext blocks ret -> Set (SomeBlockID blocks) -> BlockID blocks cxt -> (a, Set (SomeBlockID blocks)) -> (a, Set (SomeBlockID blocks))
- dfs_backedge_targets :: CFG ext blocks init ret -> Set (SomeBlockID blocks)
- dfs_backedges :: CFG ext blocks init ret -> Seq (SomeBlockID blocks, SomeBlockID blocks)
- dfs_list :: CFG ext blocks init ret -> Seq (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks)
- dfs_preorder :: CFG ext blocks init ret -> Seq (SomeBlockID blocks)
- dfs_postorder :: CFG ext blocks init ret -> Seq (SomeBlockID blocks)
Basic DFS types and algorithms
data DFSEdgeType Source #
Constructors
| TreeEdge | This edge is on the spanning forrest computed by this DFS |
| ForwardOrCrossEdge | This edge is either a forward (to a direct decendent in the spanning tree) or a cross edge (to a cousin node) |
| BackEdge | This edge is a back edge (to an ancestor in the spanning tree). Every cycle in the graph must traverse at least one back edge. |
Instances
| Show DFSEdgeType Source # | |
Defined in Lang.Crucible.Analysis.DFS Methods showsPrec :: Int -> DFSEdgeType -> ShowS # show :: DFSEdgeType -> String # showList :: [DFSEdgeType] -> ShowS # | |
| Eq DFSEdgeType Source # | |
Defined in Lang.Crucible.Analysis.DFS | |
| Ord DFSEdgeType Source # | |
Defined in Lang.Crucible.Analysis.DFS Methods compare :: DFSEdgeType -> DFSEdgeType -> Ordering # (<) :: DFSEdgeType -> DFSEdgeType -> Bool # (<=) :: DFSEdgeType -> DFSEdgeType -> Bool # (>) :: DFSEdgeType -> DFSEdgeType -> Bool # (>=) :: DFSEdgeType -> DFSEdgeType -> Bool # max :: DFSEdgeType -> DFSEdgeType -> DFSEdgeType # min :: DFSEdgeType -> DFSEdgeType -> DFSEdgeType # | |
type DFSNodeFunc ext blocks a = forall ret ctx. Block ext blocks ret ctx -> a -> a Source #
Function to update the traversal state when we have finished visiting all of a nodes's reachable children.
type DFSEdgeFunc blocks a = DFSEdgeType -> SomeBlockID blocks -> SomeBlockID blocks -> a -> a Source #
Function to update the traversal state when traversing an edge.
dfs :: DFSNodeFunc ext blocks a -> DFSEdgeFunc blocks a -> a -> CFG ext blocks init ret -> a Source #
A depth-first search algorithm on a block map.
The DFSNodeFunc and DFSEdgeFunc define what we are computing. The DFSEdgeFunc is called on each edge. The edges are classified according to standard depth-first search terminology. A tree edge is an edge in the discovered spanning tree. A back edge goes from a child to an ancestor in the spanning tree. A ForwardOrCross edge travels either from an ancestor to a child (but not a tree edge), or between two unrelated nodes. The forward/cross case can be distinguished, if desired, by tracking the order in which nodes are found. A forward edge goes from a low numbered node to a high numbered node, but a cross edge goes from a high node to a low node.
The DFSNodeFunc is called on each block _after_ the DFS has processed all its fresh reachable children; that is, as the search is leaving the given node. In particular, using the DFSNodeFunc to put the blocks in a queue will give a postorder traversal of the discovered nodes. Contrarywise, using the DFSEdgeFunc to place blocks in a queue when they occur in a TreeEdge will give a preorder traversal of the discovered nodes.
We track the lifecycle of nodes by using two sets; an ancestor set and a black set. Nodes are added to the ancestor set as we pass down into recursive calls, and changes to this set are discarded upon return. The black set records black nodes (those whose visit is completed), and changes are threaded through the search.
In the standard parlance, a node is white if it has not yet been discovered; it is in neither the ancestor nor black set. A node is grey if it has been discovered, but not yet completed; such a node is in the ancestor set, but not the black set. A node is black if its visit has been completed; it is in the black set and not in the ancestor set. INVARIANT: at all times, the ancestor set and black set are disjoint. After a DFS is completed, all visited nodes will be in the black set; any nodes not in the black set are unreachable from the initial node.
Arguments
| :: forall ext blocks a ret cxt. DFSNodeFunc ext blocks a | action to take after a visit is finished |
| -> DFSEdgeFunc blocks a | action to take for each edge |
| -> BlockMap ext blocks ret | CFG blocks to search |
| -> Set (SomeBlockID blocks) | ancestor nodes |
| -> BlockID blocks cxt | a white node to visit |
| -> (a, Set (SomeBlockID blocks)) | Partially-computed value and initial black set |
| -> (a, Set (SomeBlockID blocks)) | Computed value and modified black set |
Low-level depth-first search function. This exposes more of the moving parts
than dfs for algorithms that need more access to the guts.
Some specific DFS traversals
dfs_backedge_targets :: CFG ext blocks init ret -> Set (SomeBlockID blocks) Source #
Use depth-first search to calculate a set of all the block IDs that are the target of some back-edge, i.e., a set of nodes through which every loop passes.
dfs_backedges :: CFG ext blocks init ret -> Seq (SomeBlockID blocks, SomeBlockID blocks) Source #
Compute a sequence of all the back edges found in a depth-first search of the given CFG.
dfs_list :: CFG ext blocks init ret -> Seq (DFSEdgeType, SomeBlockID blocks, SomeBlockID blocks) Source #
Compute a sequence of all the edges visited in a depth-first search of the given CFG.
dfs_preorder :: CFG ext blocks init ret -> Seq (SomeBlockID blocks) Source #
Compute a preorder traversal of all the reachable nodes in the CFG
dfs_postorder :: CFG ext blocks init ret -> Seq (SomeBlockID blocks) Source #
Compute a postorder traversal of all the reachable nodes in the CFG