extracted/untrusted/untrusted_interference.mli

   1 type pseudoregister = Registers.register
   2 type hwregister = I8051.register
   3 module HwRegisterSet : Set.S with type elt = hwregister
   4
   5 val hwregisterset_of_list : hwregister List.list -> HwRegisterSet.t
   6
   7 (* Pasted from Pottier's PP compiler *)
   8
   9 (** This module implements a data structure for interference graphs.
  10     It provides functions that help construct, transform and inspect
  11     interference graphs. *)
  12
  13 (* Interference graphs record two kinds of edges: interference edges
  14    (``these two vertices cannot receive the same color'') and
  15    preference edges (``these two vertices should preferably receive
  16    the same color''). Furthermore, each kind of edge can relate either
  17    two pseudo-registers or one pseudo-register and one hardware
  18    register. Thus, an interference graph keeps track of four kinds of
  19    relationships.
  20
  21    This module automatically maintains the invariant that two vertices
  22    [x] and [y] cannot be related by both an interference edge and a
  23    preference edge. When such a situation appears (for instance,
  24    because of coalescing), the preference edge is automatically
  25    removed. *)
  26
  27 type graph
  28
  29 (* The vertices of an interference graph initially correspond to
  30    pseudo-registers. However, interference graphs support coalescing,
  31    which means that a new graph can be constructed by coalescing two
  32    vertices in an existing graph. As a result, in general, the vertices
  33    of an interference graph correspond to sets of pseudo-registers. *)
  34
  35 (* ------------------------------------------------------------------------- *)
  36
  37 (* Operations over vertices: sets of vertices, maps over vertices. *)
  38
  39 module Vertex : sig
  40
  41   type t
  42
  43   (* The usual operations on sets, see [Set.S] in Objective Caml's
  44      documentation. *)
  45
  46   module Set : Set.S with type elt = t
  47
  48   (* The usual operations on maps, see [Map.S] in Objective Caml's
  49      documentation. One slight difference is that [find] expects
  50      the key to be present in the map -- it will fail otherwise. *)
  51
  52   module Map : MyMap.S with type key = t
  53
  54 end
  55
  56 (* ------------------------------------------------------------------------- *)
  57
  58 (* Building interference graphs. *)
  59
  60 (* [create regs] creates an interference graph whose vertices are
  61    the pseudo-registers [regs] and that does not have any edges. *)
  62
  63 val create: pseudoregister Pset.set -> graph
  64
  65 (* [mki graph regs1 regs2] adds interference edges between all pairs
  66    of (pseudo- or hardware) registers [r1] and [r2], where [r1] ranges
  67    over [regs1], [r2] ranges over [regs2], and [r1] and [r2] are
  68    distinct. *)
  69
  70 val mki: graph ->
  71          pseudoregister Pset.set * HwRegisterSet.t ->
  72          pseudoregister Pset.set * HwRegisterSet.t ->
  73          graph
  74
  75 (* [mkiph graph regs hwregs] adds interference edges between all pairs
  76    of a pseudo-register [r] and a hardware register [hwr], where [r]
  77    ranges over [regs] and [hwr] ranges over [hwregs]. *)
  78
  79 val mkiph: graph -> pseudoregister Pset.set -> HwRegisterSet.t -> graph
  80
  81 (* [mkppp graph r1 r2] adds a preference edge between the
  82     pseudo-registers [r1] and [r2]. *)
  83
  84 val mkppp: graph -> pseudoregister -> pseudoregister -> graph
  85
  86 (* [mkpph graph r h] adds a preference edge between the
  87     pseudo-register [r] and the hardware register [h]. *)
  88
  89 val mkpph: graph -> pseudoregister -> hwregister -> graph
  90
  91 (* ------------------------------------------------------------------------- *)
  92
  93 (* Transforming interference graphs. *)
  94
  95 (* [coalesce graph v1 v2] is a new graph where the vertices [v1] and
  96    [v2] are coalesced. [v1] and [v2] must not interfere. The new
  97    coalesced vertex is known under the name [v2]. *)
  98
  99 val coalesce: graph -> Vertex.t -> Vertex.t -> graph
 100
 101 (* [coalesceh graph v h] coalesces the vertex [v] with the hardware register
 102    [h]. This produces a new graph where [v] no longer exists and all edges
 103    leading to [v] are replaced with edges leading to [h]. *)
 104
 105 val coalesceh: graph -> Vertex.t -> I8051.register -> graph
 106
 107 (* [remove graph v] is a new graph where vertex [v] is removed. *)
 108
 109 val remove: graph -> Vertex.t -> graph
 110
 111 (* [freeze graph x] is a new graph where all preference edges carried
 112    by [x] are removed. *)
 113
 114 val freeze: graph -> Vertex.t -> graph
 115
 116 (* [restrict graph p] is a new graph where only those vertices that
 117    satisfy predicate [p] are kept. *)
 118
 119 val restrict: graph -> (Vertex.t -> bool) -> graph
 120
 121 (* [droph graph] is a new graph where all information concerning hardware
 122    registers has been dropped. *)
 123
 124 val droph: graph -> graph
 125
 126 (* ------------------------------------------------------------------------- *)
 127
 128 (* Inspecting interference graphs. *)
 129
 130 (* [lookup graph r] returns the graph vertex associated with
 131    pseudo-register [r]. *)
 132
 133 val lookup: graph -> pseudoregister -> Vertex.t
 134
 135 (* Conversely, [registers graph v] returns the set of pseudo-registers
 136    associated with vertex [v]. *)
 137
 138 val registers: graph -> Vertex.t -> pseudoregister Pset.set
 139
 140 (* [degree graph v] is the degree of the vertex [v], that is, the number
 141    of vertices and hardware registers that [v] interferes with. *)
 142
 143 val degree: graph -> Vertex.t -> int
 144
 145 (* [lowest graph] returns [Some (v, d)], where the vertex [v] has
 146    minimum degree [d], or returns [None] if the graph is empty. *)
 147
 148 val lowest: graph -> (Vertex.t * int) option
 149
 150 (* [lowest_non_move_related graph] returns [Some (v, d)], where the
 151    vertex [v] has minimum degree [d] among the vertices that are not
 152    move-related, or returns [None] if all vertices are move-related. A
 153    vertex is move-related if it carries a preference edge. *)
 154
 155 val lowest_non_move_related: graph -> (Vertex.t * int) option
 156
 157 (* [minimum f graph] returns a vertex [v] such that the value of [f x]
 158    is minimal. The values returned by [f] are compared using Objective
 159    Caml's generic comparison operator [<]. If the graph is empty,
 160    [None] is returned. *)
 161
 162 val minimum: (Vertex.t -> 'a) -> graph -> Vertex.t option
 163
 164 (* [fold f graph accu] folds over all vertices. *)
 165
 166 val fold: (Vertex.t -> 'a -> 'a) -> graph -> 'a -> 'a
 167
 168 (* [ipp graph v] is the set of vertices that the vertex [v] interferes
 169    with. *)
 170
 171 val ipp: graph -> Vertex.t -> Vertex.Set.t
 172
 173 (* [iph graph v] is the set of hardware registers that the vertex [v]
 174    interferes with. *)
 175
 176 val iph: graph -> Vertex.t -> HwRegisterSet.t
 177
 178 (* [ppp graph v] is the set of vertices that should preferably be
 179    assigned the same color as the vertex [v]. *)
 180
 181 val ppp: graph -> Vertex.t -> Vertex.Set.t
 182
 183 (* [pph graph v] is the set of hardware registers that [v] should
 184    preferably be assigned. *)
 185
 186 val pph: graph -> Vertex.t -> HwRegisterSet.t
 187
 188 (* [pppick graph p] returns an arbitrary preference edge that
 189    satisfies the predicate [p], if the graph contains one. *)
 190
 191 type ppedge =
 192     Vertex.t * Vertex.t
 193
 194 val pppick: graph -> (ppedge -> bool) -> ppedge option
 195
 196 (* [phpick graph p] returns an arbitrary preference edge that
 197    satisfies the predicate [p], if the graph contains one. *)
 198
 199 type phedge =
 200     Vertex.t * I8051.register
 201
 202 val phpick: graph -> (phedge -> bool) -> phedge option
 203
 204 (*
 205 (* ------------------------------------------------------------------------- *)
 206
 207 (* Displaying interference graphs. *)
 208
 209 (* [print_vertex graph v] produces a string representation of the
 210    vertex [v]. *)
 211
 212 val print_vertex: graph -> Vertex.t -> string
 213
 214 (* [print f graph] prints a representation of the interference graph
 215    [graph] in [dot] format to the output channel [f]. Interference
 216    edges are drawn as plain lines; preference edges are drawn as
 217    dotted lines. *)
 218
 219 val print: out_channel -> graph -> unit
 220 *)