source: extracted/untrusted/untrusted_interference.mli @ 2740

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

Graph colouring terminated up to Uses that will be implemented
in Matita.

File size: 7.4 KB
Line 
1type pseudoregister = Registers.register
2type hwregister = I8051.register
3module HwRegisterSet : Set.S with type elt = hwregister
4
5val 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
27type 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
39module 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
54end
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
63val 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
70val 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
79val 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
84val 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
89val 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
99val 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
105val coalesceh: graph -> Vertex.t -> I8051.register -> graph
106
107(* [remove graph v] is a new graph where vertex [v] is removed. *)
108
109val 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
114val 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
119val 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
124val 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
133val lookup: graph -> pseudoregister -> Vertex.t
134
135(* Conversely, [registers graph v] returns the set of pseudo-registers
136   associated with vertex [v]. *)
137
138val 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
143val 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
148val 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
155val 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
162val minimum: (Vertex.t -> 'a) -> graph -> Vertex.t option
163
164(* [fold f graph accu] folds over all vertices. *)
165
166val 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
171val 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
176val 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
181val 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
186val 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
191type ppedge =
192    Vertex.t * Vertex.t
193
194val 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
199type phedge =
200    Vertex.t * I8051.register
201
202val 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
212val 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
219val print: out_channel -> graph -> unit
220*)
Note: See TracBrowser for help on using the repository browser.