Theory Traversal

subsection ‹Control-flow Graph Traversal›

theory
  Traversal
imports
  IRGraph
begin

type_synonym Seen = "ID set"


text ‹
nextEdge helps determine which node to traverse next by returning the first successor
edge that isn't in the set of already visited nodes.
If there is not an appropriate successor, None is returned instead.
›
fun nextEdge :: "Seen ⇒ ID ⇒ IRGraph ⇒ ID option" where
  "nextEdge seen nid g = 
    (let nids = (filter (λnid'. nid' ∉ seen) (successors_of (kind g nid))) in 
     (if length nids > 0 then Some (hd nids) else None))"

text ‹
pred determines which node, if any, acts as the predecessor of another.

Merge nodes represent a special case where-in the predecessor exists as
an input edge of the merge node, to simplify the traversal we treat only
the first input end node as the predecessor, ignoring that multiple nodes
may act as a successor.

For all other nodes, the predecessor is the first element of the predecessors set.
Note that in a well-formed graph there should only be one element in the predecessor set.›
fun pred :: "IRGraph ⇒ ID ⇒ ID option" where
  "pred g nid = (case kind g nid of
    (MergeNode ends _ _) ⇒ Some (hd ends) |
    _ ⇒ 
      (if IRGraph.predecessors g nid = {} 
        then None else
        Some (hd (sorted_list_of_set (IRGraph.predecessors g nid)))
      )
  )"


text ‹
Here we try to implement a generic fork of the control-flow traversal algorithm
that was initially implemented for the ConditionalElimination phase
›
type_synonym 'a TraversalState = "(ID × Seen × 'a)"

inductive Step 
  :: "('a TraversalState ⇒ 'a) ⇒ IRGraph ⇒ 'a TraversalState ⇒ 'a TraversalState option ⇒ bool"
  for sa g where
  ― ‹
  Hit a BeginNode with an IfNode predecessor which represents
  the start of a basic block for the IfNode.
     1. nid' will be the successor of the begin node.
     2. Find the first and only predecessor.
     3. Extract condition from the preceding IfNode.
     4. Negate condition if the begin node is second branch
        (we've taken the else branch of the condition)
     5. Add the condition or the negated condition to stack
     6. Perform any stamp updates based on the condition using
        the registerNewCondition function and place them on the
        top of the stack of stamp information
  ›
  "⟦kind g nid = BeginNode nid';

    nid ∉ seen;
    seen' = {nid} ∪ seen;

    Some ifcond = pred g nid;
    kind g ifcond = IfNode cond t f;

    analysis' = sa (nid, seen, analysis)⟧
   ⟹ Step sa g (nid, seen, analysis) (Some (nid', seen', analysis'))" |

  ― ‹
  Hit an EndNode
     1. nid' will be the usage of EndNode
     2. pop the conditions and stamp stack
  ›
  "⟦kind g nid = EndNode;

    nid ∉ seen;
    seen' = {nid} ∪ seen;

    nid' = any_usage g nid;

    analysis' = sa (nid, seen, analysis)⟧
   ⟹ Step sa g (nid, seen, analysis) (Some (nid', seen', analysis'))" |

  ― ‹We can find a successor edge that is not in seen, go there›
  "⟦¬(is_EndNode (kind g nid));
    ¬(is_BeginNode (kind g nid));

    nid ∉ seen;
    seen' = {nid} ∪ seen;

    Some nid' = nextEdge seen' nid g;

    analysis' = sa (nid, seen, analysis)⟧
   ⟹ Step sa g (nid, seen, analysis) (Some (nid', seen', analysis'))" |

  ― ‹We can cannot find a successor edge that is not in seen, give back None›
  "⟦¬(is_EndNode (kind g nid));
    ¬(is_BeginNode (kind g nid));

    nid ∉ seen;
    seen' = {nid} ∪ seen;

    None = nextEdge seen' nid g⟧
    ⟹ Step sa g (nid, seen, analysis) None" |

  ― ‹We've already seen this node, give back None›
  "⟦nid ∈ seen⟧ ⟹ Step sa g (nid, seen, analysis) None"

code_pred (modes: i ⇒ i ⇒ i ⇒ o ⇒ bool) Step .

end