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