source: extracted/untrusted/untrusted_interference.mli @ 2738

Last change on this file since 2738 was 2738, checked in by sacerdot, 7 years ago

Porting the graph colouring stuff from the untrusted prototype to the extracted
code.

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