ControlFlow.CFG

(source)

This module contains a representation of a control-flow graph that aims to
enforce the correctness of jumps between vertices of graphs, i.e., blocks
of code.
The graph model permits both graphs and vertices that are incomplete and
facilitates easy composition of such graphs when they are compatible.

A graph / vertex is incomplete when vertices / insrtuctions need to be
added to it in order for it to be a valid function body / basic block.
For example a graph that contains only the following pseudo-code block:
```
L0: x = call func ()
    jump L1
```
is incomplete because the code block ends with a jump to the block `L1` but
`L1` is not in the graph.
An example of an incomplete vertex is the following:
```
L0: x = call func ()
```
because it does not end with a jump nor with a return instruction.

In this model, vertices and graphs can be incomplete at the beginning or at
the end (or both). In other words, graphs / vertices can be completed only
by prepending or appending vertices / instructions to them.

Reexports

import public ControlFlow.Edge

Definitions

Neighbors : Type -> Type

  Neighbors of a vertex
  * `Just l` represents neighbors of a vertex that is complete at the
     relevant end (beginning or end)
  * `Nothing` is used to mark that a vertex is incomplete at a given end
  @ a the type of vertex identifiers

Visibility: public export

Vertex : Type -> Type

  A constructor of verteices of a directed graph
  @ a    the type of vertex identifiers
  @ v    the identifier              of the vertex
  @ ins  the inputs  (in-neighbors)  of the vertex
  @ outs the outputs (out-neighbors) of the vertex

Visibility: public export

interface Connectable : Vertex a -> Type

  Types of vertices that allow merging undefined vertices

Parameters: vertex
Methods:

cnct : vertex v ins Nothing -> vertex v Nothing outs -> vertex v ins outs

  Merge two vertices undefined on opposite ends

cnct : Connectable vertex => vertex v ins Nothing -> vertex v Nothing outs -> vertex v ins outs

  Merge two vertices undefined on opposite ends

Visibility: public export

data Edges : Type -> Type

  Input or output edges of an incomplete graph
  @ a the type of vertex identifiers

Totality: total
Visibility: public export
Constructors:

Undefined : a -> Edges a

  `Undefined v` is used to mark that a graph has, at the a given end,
  one incomplete vertex labeled `v`.

Defined : List (Edge a) -> Edges a

  `Defined edges` represents the input or output edges of a graph in a
  case when it has no incomplete vertices at the relevant end.
  
  `edges` is then the list of edges whose destinations (origins) are in
  the graph but their origins (destinations) are not.

Closed : Neighbors a

Visibility: public export

Single : a -> Neighbors a

Visibility: public export

Closed : Edges a

Visibility: public export

Single : a -> a -> Edges a

Visibility: public export

fromVOut : a -> Neighbors a -> Edges a

  Given an identifier of a vertex and its out-neighbors return the output
  edges of that vertex
  @ v    the vertex identifier
  @ outs the out-neighbors of the vertex

Visibility: public export

fromVIn : Neighbors a -> a -> Edges a

  Given an identifier of a vertex and its in-neighbors return the input
  edges of that vertex
  @ v   the vertex identifier
  @ ins the in-neighbors of the vertex

Visibility: public export

(~>>?) : a -> Neighbors a -> Edges a

  Alias for `fromVOut`

Visibility: public export
Fixity Declaration: infix operator, level 8

(?~~>) : Neighbors a -> a -> Edges a

  Alias for `fromVIn`

Visibility: public export
Fixity Declaration: infix operator, level 8

data CFG : Vertex a -> Edges a -> Edges a -> Type

  A potentially incomplete control flow graph.
  @ ins    edges from "to be defined" vertices to vertices in the graph
  @ outs   edges from vertices in the graph to "to be defined" vertices
  @ vertex constructor of vertex types.

Totality: total
Visibility: public export
Constructors:

Empty : CFG vertex (Defined edges) (Defined edges)

  An empty graph

SingleVertex : vertex v vins vouts -> CFG vertex (vins ?~~> v) (v ~>>? vouts)

  A singleton graph - a graph containing a single vertex

Cycle : CFG vertex (Defined (ins ++ loopOuts)) (Defined (loopIns ++ outs)) -> CFG vertex (Defined loopIns) (Defined loopOuts) -> CFG vertex (Defined ins) (Defined outs)

  A graph that represents a while loop
  @ node the graph in which the while condition is computed
  @ loop the body of the loop

Series : CFG vertex ins (Defined edges) -> CFG vertex (Defined edges) outs -> CFG vertex ins outs

  A sequential connection of two graphs
  The output vertices of one (`pre`) are being connected to the input
  vertices of the other (`post`)
  @ pre  the predecessor of `post`
  @ post the successor   of `pre`

Parallel : CFG vertex (Defined ins) (Defined outs) -> CFG vertex (Defined ins') (Defined outs') -> CFG vertex (Defined (ins ++ ins')) (Defined (outs ++ outs'))

  A parallel connection of graphs
  Two graphs are combined into one without any connections beetween them
  The result has the inputs and outputs of both
  @ left  the left sub-graph
  @ right the right sub-graph

IFlip : CFG vertex (Defined (ins ++ ins')) outs -> CFG vertex (Defined (ins' ++ ins)) outs

  Used to flip the inputs of a graph to make it connectable with another

OFlip : CFG vertex ins (Defined (outs ++ outs')) -> CFG vertex ins (Defined (outs' ++ outs))

  Used to flip the outputs of a graph to make it connectable with another

(|-|) : CFG vertex (Defined ins) (Defined outs) -> CFG vertex (Defined ins') (Defined outs') -> CFG vertex (Defined (ins ++ ins')) (Defined (outs ++ outs'))

  Alias for `Parallel`

Visibility: public export
Fixity Declaration: infixr operator, level 4

(*->) : CFG vertex ins (Defined edges) -> CFG vertex (Defined edges) outs -> CFG vertex ins outs

  Alias for `Series`

Visibility: public export
Fixity Declaration: infixr operator, level 5

prepend : vertex v vins (Just vouts) -> CFG vertex (Defined (v ~>> vouts)) gouts -> CFG vertex (vins ?~~> v) gouts

Visibility: public export

append : CFG vertex gins (Defined (vins ~~> v)) -> vertex v (Just vins) vouts -> CFG vertex gins (v ~>>? vouts)

Visibility: public export

lbranch : CFG vertex ins (Defined (ls ++ rs)) -> CFG vertex (Defined ls) (Defined ls') -> CFG vertex ins (Defined (ls' ++ rs))

  A partial sequential connection of two graphs
  The left outputs of the predecessor are connected with all inputs of
  the successor
  @ node   the           predecessor of `branch`
  @ branch the (partial) successor   of `node`
  @ ls     the left  outputs of `node` / the inputs of `branch`
  @ rs     the right outputs of `node`

Visibility: public export

rbranch : CFG vertex ins (Defined (ls ++ rs)) -> CFG vertex (Defined rs) (Defined rs') -> CFG vertex ins (Defined (ls ++ rs'))

  A partial sequential connection of two graphs
  The right outputs of the predecessor are connected with all inputs of
  the successor
  @ node   the           predecessor of `branch`
  @ branch the (partial) successor   of `node`
  @ ls     the left  outputs of `node`
  @ rs     the right outputs of `node` / the inputs of `branch`

Visibility: public export

lmerge : CFG vertex (Defined ls) (Defined ls') -> CFG vertex (Defined (ls' ++ rs)) outs -> CFG vertex (Defined (ls ++ rs)) outs

  A partial sequential connection of two graphs
  All outputs of the predecessor are connected with the left inputs of
  the successor
  @ branch the           predecessor of `node`
  @ node   the (partial) successor   of `branch`
  @ ls'    the left  inputs of `node` / the outputs of `branch`
  @ rs     the right inputs of `node`

Visibility: public export

rmerge : CFG vertex (Defined rs) (Defined rs') -> CFG vertex (Defined (ls ++ rs')) outs -> CFG vertex (Defined (ls ++ rs)) outs

  A partial sequential connection of two graphs
  All outputs of the predecessor are connected with the right inputs of
  the successor
  @ branch the           predecessor of `node`
  @ node   the (partial) successor   of `branch`
  @ ls     the left  inputs of `node`
  @ rs'    the right inputs of `node` / the outputs of `branch`

Visibility: public export

imap : (vertex v Nothing outs -> vertex v ins outs) -> CFG vertex (Undefined v) gouts -> CFG vertex (ins ?~~> v) gouts

  Apply a function to the undefined input vertex

Visibility: export

omap : (vertex v ins Nothing -> vertex v ins outs) -> CFG vertex gins (Undefined v) -> CFG vertex gins (v ~>>? outs)

  Apply a function to the undefined output vertex

Visibility: export

connect : Connectable vertex => CFG vertex ins (Undefined v) -> CFG vertex (Undefined v) outs -> CFG vertex ins outs

  Connect sequentialy two graphs that end and begin with an undefined vertex
  
  Connects the two grapgs by merges the output vertex of the predecessor
  with the input vertex of the successor

Visibility: export

(*~>) : Connectable vertex => CFG vertex ins (Undefined v) -> CFG vertex (Undefined v) outs -> CFG vertex ins outs

  Alias for `connect`

Visibility: export
Fixity Declaration: infixr operator, level 5

initGraph : vertex v Nothing Nothing -> CFG vertex (Undefined v) (Undefined v)

Visibility: export

iget : (vertex v Nothing outs -> b) -> CFG vertex (Undefined v) gouts -> b

  Get data from the undefined input vertex

Visibility: export

oget : (vertex v ins Nothing -> b) -> CFG vertex gins (Undefined v) -> b

  Get data from the undefined output vertex

Visibility: export

vmap : (vertex v vins vouts -> vertex' v vins vouts) -> CFG vertex ins outs -> CFG vertex' ins outs

  Apply a function to all vertices in a grpaph

Visibility: export

vmap' : (vertex v (Just vins) (Just vouts) -> vertex' v (Just vins) (Just vouts)) -> CFG vertex (Defined ins) (Defined outs) -> CFG vertex' (Defined ins) (Defined outs)

  Apply a function to all vertices in a fully defined graph
  
  Like `vmap` but all vertices in the graph are defined an thus the applied
  function works only for defined vertices

Visibility: export