
   0 | ||| This module contains a representation of a control-flow graph that aims to
   1 | ||| enforce the correctness of jumps between vertices of graphs, i.e., blocks
   2 | ||| of code.
   3 | ||| The graph model permits both graphs and vertices that are incomplete and
   4 | ||| facilitates easy composition of such graphs when they are compatible.
   5 | |||
   6 | ||| A graph / vertex is incomplete when vertices / insrtuctions need to be
   7 | ||| added to it in order for it to be a valid function body / basic block.
   8 | ||| For example a graph that contains only the following pseudo-code block:
   9 | ||| ```
  10 | ||| L0: x = call func ()
  11 | |||     jump L1
  12 | ||| ```
  13 | ||| is incomplete because the code block ends with a jump to the block `L1` but
  14 | ||| `L1` is not in the graph.
  15 | ||| An example of an incomplete vertex is the following:
  16 | ||| ```
  17 | ||| L0: x = call func ()
  18 | ||| ```
  19 | ||| because it does not end with a jump nor with a return instruction.
  20 | |||
  21 | ||| In this model, vertices and graphs can be incomplete at the beginning or at
  22 | ||| the end (or both). In other words, graphs / vertices can be completed only
  23 | ||| by prepending or appending vertices / instructions to them.
  24 | module ControlFlow.CFG
  25 | 
  26 | import public ControlFlow.Edge
  27 | 
  28 | {-
  29 | TODO:
  30 | Consider singling out `Just []` / `Defined []` and use `List1` instead of `List`
  31 | -}
  32 | 
  33 | ||| Neighbors of a vertex
  34 | ||| * `Just l` represents neighbors of a vertex that is complete at the
  35 | |||    relevant end (beginning or end)
  36 | ||| * `Nothing` is used to mark that a vertex is incomplete at a given end
  37 | ||| @ a the type of vertex identifiers
  38 | public export
  39 | Neighbors : Type -> Type
  40 | Neighbors a = Maybe (List a)
  41 | 
  42 | ||| A constructor of verteices of a directed graph
  43 | ||| @ a    the type of vertex identifiers
  44 | ||| @ v    the identifier              of the vertex
  45 | ||| @ ins  the inputs  (in-neighbors)  of the vertex
  46 | ||| @ outs the outputs (out-neighbors) of the vertex
  47 | public export
  48 | Vertex : Type -> Type
  49 | Vertex a = (v : a) -> (ins : Neighbors a) -> (outs : Neighbors a) -> Type
  50 | 
  51 | ||| Types of vertices that allow merging undefined vertices
  52 | public export
  53 | interface Connectable (0 vertex : Vertex a) where
  54 |   ||| Merge two vertices undefined on opposite ends
  55 |   cnct : {0 v : a}
  56 |       -> {0 ins, outs : Neighbors a}
  57 |       -> vertex v ins Nothing
  58 |       -> vertex v Nothing outs
  59 |       -> vertex v ins outs
  60 | 
  61 | ||| Input or output edges of an incomplete graph
  62 | ||| @ a the type of vertex identifiers
  63 | public export
  64 | data Edges a
  65 |   = ||| `Undefined v` is used to mark that a graph has, at the a given end,
  66 |     ||| one incomplete vertex labeled `v`.
  67 |     Undefined a
  68 |   | ||| `Defined edges` represents the input or output edges of a graph in a
  69 |     ||| case when it has no incomplete vertices at the relevant end.
  70 |     |||
  71 |     ||| `edges` is then the list of edges whose destinations (origins) are in
  72 |     ||| the graph but their origins (destinations) are not.
  73 |     Defined (List (Edge a))
  74 | 
  75 | namespace Vertex
  76 | 
  77 |   public export
  78 |   Closed : Neighbors a
  79 |   Closed = Just []
  80 | 
  81 |   public export
  82 |   Single : a -> Neighbors a
  83 |   Single x = Just [x]
  84 | 
  85 | namespace Graph
  86 | 
  87 |   public export
  88 |   Closed : Edges a
  89 |   Closed = Defined []
  90 | 
  91 |   public export
  92 |   Single : a -> a -> Edges a
  93 |   Single from to = Defined [from ~> to]
  94 | 
  95 | ||| Given an identifier of a vertex and its out-neighbors return the output
  96 | ||| edges of that vertex
  97 | ||| @ v    the vertex identifier
  98 | ||| @ outs the out-neighbors of the vertex
  99 | public export
 100 | fromVOut : (v : a) -> (outs : Neighbors a) -> Edges a
 101 | fromVOut v Nothing      = Undefined v
 102 | fromVOut v (Just outs)  = Defined (v ~>> outs)
 103 | 
 104 | ||| Given an identifier of a vertex and its in-neighbors return the input
 105 | ||| edges of that vertex
 106 | ||| @ v   the vertex identifier
 107 | ||| @ ins the in-neighbors of the vertex
 108 | public export
 109 | fromVIn : (ins : Neighbors a) -> (v : a) -> Edges a
 110 | fromVIn Nothing     v = Undefined v
 111 | fromVIn (Just ins)  v = Defined (ins ~~> v)
 112 | 
 113 | export
 114 | infix 8 ~>>?, ?~~>
 115 | 
 116 | ||| Alias for `fromVOut`
 117 | public export
 118 | (~>>?) : (v : a) -> (outs : Neighbors a) -> Edges a
 119 | v ~>>? vs = fromVOut v vs
 120 | 
 121 | ||| Alias for `fromVIn`
 122 | public export
 123 | (?~~>) : (ins : Neighbors a) -> (v : a) -> Edges a
 124 | vs ?~~> v = fromVIn vs v
 125 | 
 126 | {-
 127 | TODO: Consider adding an `data` parameter to `CFG` that would be the type of
 128 | data that would be stored alongside vertices.
 129 | 
 130 | The `data` could be:
 131 |   - the values of variables
 132 |   - variables that were changed
 133 |   - variables that are live
 134 | -}
 135 | 
 136 | ||| A potentially incomplete control flow graph.
 137 | ||| @ ins    edges from "to be defined" vertices to vertices in the graph
 138 | ||| @ outs   edges from vertices in the graph to "to be defined" vertices
 139 | ||| @ vertex constructor of vertex types.
 140 | public export
 141 | data CFG : (vertex : Vertex a) -> (ins : Edges a) -> (outs : Edges a) -> Type where
 142 | 
 143 |   ||| An empty graph
 144 |   Empty : CFG vertex (Defined edges) (Defined edges)
 145 | 
 146 |   ||| A singleton graph - a graph containing a single vertex
 147 |   SingleVertex
 148 |      : {0 vertex : Vertex a}
 149 |     -> {vins, vouts : Neighbors a}
 150 |     -> vertex v vins vouts
 151 |     -> CFG vertex (vins ?~~> v) (v ~>>? vouts)
 152 | 
 153 |   -- TODO consider `CFG (ins ++ edges) (outs ++ edges) -> CFG ins outs` instead of this
 154 |   ||| A graph that represents a while loop
 155 |   ||| @ node the graph in which the while condition is computed
 156 |   ||| @ loop the body of the loop
 157 |   Cycle
 158 |      : {ins, outs, loopIns, loopOuts : List (Edge a)}
 159 |     -> (node : CFG vertex (Defined $ ins ++ loopOuts) (Defined $ loopIns ++ outs))
 160 |     -> (loop : CFG vertex (Defined loopIns) (Defined loopOuts))
 161 |     -> CFG vertex (Defined ins) (Defined outs)
 162 | 
 163 |   ||| A sequential connection of two graphs
 164 |   ||| The output vertices of one (`pre`) are being connected to the input
 165 |   ||| vertices of the other (`post`)
 166 |   ||| @ pre  the predecessor of `post`
 167 |   ||| @ post the successor   of `pre`
 168 |   Series
 169 |      : (pre  : CFG vertex ins (Defined edges))
 170 |     -> (post : CFG vertex (Defined edges) outs)
 171 |     -> CFG vertex ins outs
 172 | 
 173 |   ||| A parallel connection of graphs
 174 |   ||| Two graphs are combined into one without any connections beetween them
 175 |   ||| The result has the inputs and outputs of both
 176 |   ||| @ left  the left sub-graph
 177 |   ||| @ right the right sub-graph
 178 |   Parallel
 179 |      : (left  : CFG vertex (Defined ins)  (Defined outs))
 180 |     -> (right : CFG vertex (Defined ins') (Defined outs'))
 181 |     -> CFG vertex (Defined $ ins ++ ins') (Defined $ outs ++ outs')
 182 | 
 183 |   -- TODO: consider removing these constructors
 184 |   ||| Used to flip the inputs of a graph to make it connectable with another
 185 |   IFlip
 186 |      : {ins, ins' : List (Edge a)}
 187 |     -> CFG vertex (Defined $ ins ++ ins') outs
 188 |     -> CFG vertex (Defined $ ins' ++ ins) outs
 189 | 
 190 |   ||| Used to flip the outputs of a graph to make it connectable with another
 191 |   OFlip
 192 |      : {outs, outs' : List (Edge a)}
 193 |     -> CFG vertex ins (Defined $ outs ++ outs')
 194 |     -> CFG vertex ins (Defined $ outs' ++ outs)
 195 | 
 196 | export infixr 4 |-|
 197 | ||| Alias for `Parallel`
 198 | public export
 199 | (|-|)
 200 |    : CFG vertex (Defined ins)           (Defined outs)
 201 |   -> CFG vertex (Defined ins')          (Defined outs')
 202 |   -> CFG vertex (Defined $ ins ++ ins') (Defined $ outs ++ outs')
 203 | (|-|) = Parallel
 204 | 
 205 | export infixr 5 *->
 206 | ||| Alias for `Series`
 207 | public export
 208 | (*->)
 209 |    : CFG vertex ins (Defined edges)
 210 |   -> CFG vertex (Defined edges) outs
 211 |   -> CFG vertex ins outs
 212 | (*->) = Series
 213 | 
 214 | public export
 215 | prepend
 216 |    : {0 vertex : Vertex a}
 217 |   -> {vins : Neighbors a}
 218 |   -> {vouts : List a}
 219 |   -> vertex v vins (Just vouts)
 220 |   -> CFG vertex (Defined $ v ~>> vouts) gouts
 221 |   -> CFG vertex (vins ?~~> v) gouts
 222 | prepend v g = (SingleVertex v) *-> g
 223 | 
 224 | public export
 225 | append
 226 |    : {vins : List a}
 227 |   -> {vouts : Neighbors a}
 228 | 
 229 |   -> CFG vertex gins (Defined $ vins ~~> v)
 230 |   -> vertex v (Just vins) vouts
 231 |   -> CFG vertex gins (v ~>>? vouts)
 232 | append g v = g *-> (SingleVertex v)
 233 | 
 234 | branch
 235 |    : {0 vertex : Vertex a}
 236 |   -> {vins : Neighbors a}
 237 |   -> {w, w' : a}
 238 | 
 239 |   -> (pre   : vertex v vins (Just [w, w']))
 240 |   -> (left  : CFG vertex (Single v w)  (Defined louts))
 241 |   -> (right : CFG vertex (Single v w') (Defined routs))
 242 |   -> CFG vertex (vins ?~~> v) (Defined $ louts ++ routs)
 243 | branch pre left right = pre `prepend` (left |-| right)
 244 | 
 245 | fullBranch
 246 |    : {0 vertex : Vertex a}
 247 |   -> {vins, vouts : Neighbors a}
 248 |   -> {w, w', u, u' : a}
 249 | 
 250 |   -> (pre    : vertex v vins (Just [w, w']))
 251 |   -> (left   : CFG vertex (Single v w)  (Single u t))
 252 |   -> (right  : CFG vertex (Single v w') (Single u' t))
 253 |   -> (post   : vertex t (Just [u, u']) vouts)
 254 |   -> CFG vertex (vins ?~~> v) (t ~>>? vouts)
 255 | fullBranch pre left right post = (branch pre left right) `append` post
 256 | 
 257 | ||| A partial sequential connection of two graphs
 258 | ||| The left outputs of the predecessor are connected with all inputs of
 259 | ||| the successor
 260 | ||| @ node   the           predecessor of `branch`
 261 | ||| @ branch the (partial) successor   of `node`
 262 | ||| @ ls     the left  outputs of `node` / the inputs of `branch`
 263 | ||| @ rs     the right outputs of `node`
 264 | public export
 265 | lbranch
 266 |    : {ls, rs : List (Edge a)}
 267 |   -> (node   : CFG vertex ins (Defined $ ls ++ rs))
 268 |   -> (branch : CFG vertex (Defined ls) (Defined ls'))
 269 |   ->           CFG vertex ins (Defined $ ls' ++ rs)
 270 | lbranch node branch = node *-> (branch |-| Empty)
 271 | 
 272 | ||| A partial sequential connection of two graphs
 273 | ||| The right outputs of the predecessor are connected with all inputs of
 274 | ||| the successor
 275 | ||| @ node   the           predecessor of `branch`
 276 | ||| @ branch the (partial) successor   of `node`
 277 | ||| @ ls     the left  outputs of `node`
 278 | ||| @ rs     the right outputs of `node` / the inputs of `branch`
 279 | public export
 280 | rbranch
 281 |    : {ls, rs : List (Edge a)}
 282 |   -> (node   : CFG vertex ins (Defined $ ls ++ rs))
 283 |   -> (branch : CFG vertex (Defined rs) (Defined rs'))
 284 |   ->           CFG vertex ins (Defined $ ls ++ rs')
 285 | rbranch node branch = node *-> (Empty |-| branch)
 286 | 
 287 | ||| A partial sequential connection of two graphs
 288 | ||| All outputs of the predecessor are connected with the left inputs of
 289 | ||| the successor
 290 | ||| @ branch the           predecessor of `node`
 291 | ||| @ node   the (partial) successor   of `branch`
 292 | ||| @ ls'    the left  inputs of `node` / the outputs of `branch`
 293 | ||| @ rs     the right inputs of `node`
 294 | public export
 295 | lmerge
 296 |    : {ls, rs  : List (Edge a)}
 297 |   -> (branch  : CFG vertex (Defined ls) (Defined ls'))
 298 |   -> (node    : CFG vertex (Defined $ ls' ++ rs) outs)
 299 |   ->            CFG vertex (Defined $ ls  ++ rs) outs
 300 | lmerge branch node = (branch |-| Empty) *-> node
 301 | 
 302 | ||| A partial sequential connection of two graphs
 303 | ||| All outputs of the predecessor are connected with the right inputs of
 304 | ||| the successor
 305 | ||| @ branch the           predecessor of `node`
 306 | ||| @ node   the (partial) successor   of `branch`
 307 | ||| @ ls     the left  inputs of `node`
 308 | ||| @ rs'    the right inputs of `node` / the outputs of `branch`
 309 | public export
 310 | rmerge
 311 |    : {ls, rs  : List (Edge a)}
 312 |   -> (branch  : CFG vertex (Defined rs) (Defined rs'))
 313 |   -> (node    : CFG vertex (Defined $ ls ++ rs') outs)
 314 |   ->            CFG vertex (Defined $ ls ++ rs) outs
 315 | rmerge branch node = (Empty |-| branch) *-> node
 316 | 
 317 | ||| Apply a function to the undefined input vertex
 318 | export
 319 | imap
 320 |    : {0 vertex : Vertex a}
 321 |   -> {ins : Neighbors a}
 322 | 
 323 |   -> ({outs : Neighbors a} -> vertex v Nothing outs -> vertex v ins outs)
 324 |   -> CFG vertex (Undefined v) gouts
 325 |   -> CFG vertex (ins ?~~> v) gouts
 326 | 
 327 | imap f (SingleVertex {vins = Nothing} v)  = SingleVertex (f v)
 328 | imap f (Series g g')                      = Series (imap f g) g'
 329 | imap f (OFlip g)                          = OFlip (imap f g)
 330 | 
 331 | imap f Empty                              impossible
 332 | imap f (SingleVertex {vins = Just ins} v) impossible
 333 | imap f (Cycle node loop)                  impossible
 334 | imap f (Parallel g g')                    impossible
 335 | imap f (IFlip g)                          impossible
 336 | 
 337 | ||| Apply a function to the undefined output vertex
 338 | export
 339 | omap
 340 |    : {0 vertex : Vertex a}
 341 |   -> {outs : Neighbors a}
 342 | 
 343 |   -> ({ins : Neighbors a} -> vertex v ins Nothing -> vertex v ins outs)
 344 |   -> CFG vertex gins (Undefined v)
 345 |   -> CFG vertex gins (v ~>>? outs)
 346 | 
 347 | omap f (SingleVertex {vouts = Nothing} v)   = SingleVertex (f v)
 348 | omap f (Series g g')                        = Series g (omap f g')
 349 | omap f (IFlip g)                            = IFlip (omap f g)
 350 | 
 351 | omap f Empty                                impossible
 352 | omap f (SingleVertex {vouts = Just outs} v) impossible
 353 | omap f (Cycle node loop)                    impossible
 354 | omap f (Parallel g g')                      impossible
 355 | omap f (OFlip g)                            impossible
 356 | 
 357 | ||| Connect sequentialy two graphs that end and begin with an undefined vertex
 358 | |||
 359 | ||| Connects the two grapgs by merges the output vertex of the predecessor
 360 | ||| with the input vertex of the successor
 361 | export
 362 | connect
 363 |    : (impl : Connectable vertex)
 364 |   => CFG vertex ins (Undefined v)
 365 |   -> CFG vertex (Undefined v) outs
 366 |   -> CFG vertex ins outs
 367 | 
 368 | connect (SingleVertex {vouts = Nothing} v)  g   = imap (cnct @{impl} v) g
 369 | connect (Series g g')                       g'' = Series g (connect g' g'')
 370 | connect (IFlip g)                           g'  = IFlip (connect g g')
 371 | 
 372 | connect Empty                                 g' impossible
 373 | connect (SingleVertex {vouts = Just outs} v)  g' impossible
 374 | connect (Cycle node loop)                     g' impossible
 375 | connect (Parallel g g')                       g' impossible
 376 | connect (OFlip g)                             g' impossible
 377 | 
 378 | export infixr 5 *~>
 379 | ||| Alias for `connect`
 380 | export
 381 | (*~>)
 382 |    : (impl : Connectable vertex)
 383 |   => CFG vertex ins (Undefined v)
 384 |   -> CFG vertex (Undefined v) outs
 385 |   -> CFG vertex ins outs
 386 | (*~>) = connect
 387 | 
 388 | export
 389 | initGraph
 390 |    : {0 vertex : Vertex a}
 391 |   -> vertex v Nothing Nothing
 392 |   -> CFG vertex (Undefined v) (Undefined v)
 393 | initGraph v = SingleVertex v
 394 | 
 395 | ||| Get data from the undefined input vertex
 396 | export
 397 | iget
 398 |    : {0 vertex : Vertex a}
 399 |   -> ({outs : Neighbors a} -> vertex v Nothing outs -> b)
 400 |   -> CFG vertex (Undefined v) gouts
 401 |   -> b
 402 | iget f (SingleVertex {vins = Nothing} v)  = f v
 403 | iget f (Series g g')                      = iget f g
 404 | iget f (OFlip g)                          = iget f g
 405 | 
 406 | iget f Empty                              impossible
 407 | iget f (SingleVertex {vins = Just ins} v) impossible
 408 | iget f (Cycle node loop)                  impossible
 409 | iget f (Parallel g g')                    impossible
 410 | iget f (IFlip g)                          impossible
 411 | 
 412 | ||| Get data from the undefined output vertex
 413 | export
 414 | oget
 415 |    : {0 vertex : Vertex a}
 416 |   -> ({ins : Neighbors a} -> vertex v ins Nothing -> b)
 417 |   -> CFG vertex gins (Undefined v)
 418 |   -> b
 419 | 
 420 | oget f (SingleVertex {vouts = Nothing} v)   = f v
 421 | oget f (Series g g')                        = oget f g'
 422 | oget f (IFlip g)                            = oget f g
 423 | 
 424 | oget f Empty                                impossible
 425 | oget f (SingleVertex {vouts = Just outs} v) impossible
 426 | oget f (Cycle node loop)                    impossible
 427 | oget f (Parallel g g')                      impossible
 428 | oget f (OFlip g)                            impossible
 429 | 
 430 | ||| Apply a function to all vertices in a grpaph
 431 | export
 432 | vmap
 433 |    : {0 a : Type}
 434 |   -> {0 vertex, vertex' : Vertex a}
 435 |   -> {0 ins, outs : Edges a}
 436 |   -> ( {0 v : a}
 437 |     -> {vins, vouts : Neighbors a}
 438 |     -> vertex v vins vouts
 439 |     -> vertex' v vins vouts
 440 |      )
 441 |   -> CFG vertex ins outs
 442 |   -> CFG vertex' ins outs
 443 | 
 444 | vmap f Empty              = Empty
 445 | vmap f (SingleVertex v)   = SingleVertex (f v)
 446 | vmap f (Cycle node loop)  = Cycle (vmap f node) (vmap f loop)
 447 | vmap f (Series g g')      = Series (vmap f g) (vmap f g')
 448 | vmap f (Parallel g g')    = Parallel (vmap f g) (vmap f g')
 449 | vmap f (IFlip g)          = IFlip (vmap f g)
 450 | vmap f (OFlip g)          = OFlip (vmap f g)
 451 | 
 452 | ||| Apply a function to all vertices in a fully defined graph
 453 | |||
 454 | ||| Like `vmap` but all vertices in the graph are defined an thus the applied
 455 | ||| function works only for defined vertices
 456 | export
 457 | vmap'
 458 |    : {0 a : Type}
 459 |   -> {0 vertex, vertex' : Vertex a}
 460 |   -> {0 ins, outs : List (Edge a)}
 461 |   -> ( {0 v : a}
 462 |     -> {vins, vouts : List a}
 463 |     -> vertex v (Just vins) (Just vouts)
 464 |     -> vertex' v (Just vins) (Just vouts)
 465 |      )
 466 |   -> CFG vertex (Defined ins) (Defined outs)
 467 |   -> CFG vertex' (Defined ins) (Defined outs)
 468 | 
 469 | vmap' f (SingleVertex {vins = Just ins, vouts = Just outs} v) = SingleVertex (f v)
 470 | vmap' f Empty             = Empty
 471 | vmap' f (Cycle node loop) = Cycle (vmap' f node) (vmap' f loop)
 472 | vmap' f (Series g g')     = Series (vmap' f g) (vmap' f g')
 473 | vmap' f (Parallel g g')   = Parallel (vmap' f g) (vmap' f g')
 474 | vmap' f (IFlip g)         = IFlip (vmap' f g)
 475 | vmap' f (OFlip g)         = OFlip (vmap' f g)
 476 | 
 477 | vmap' f (SingleVertex {vins  = Nothing} v) impossible
 478 | vmap' f (SingleVertex {vouts = Nothing} v) impossible
 479 |