source: extracted/untrusted/untrusted_interference.ml @ 2755

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

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

File size: 25.1 KB
Line 
1type pseudoregister = Registers.register
2type hwregister = I8051.register
3module HwOrdReg = struct type t = hwregister let compare = compare end
4module HwRegisterSet = Set.Make (HwOrdReg)
5
6let hwregisterset_of_list =
7  List.foldr
8   (fun reg set -> HwRegisterSet.add reg set)
9   HwRegisterSet.empty
10
11(* Pasted from Pottier's PP compiler *)
12
13(* This module implements a data structure for interference graphs.
14   It provides functions that help construct, transform and inspect
15   interference graphs. *)
16
17(* ------------------------------------------------------------------------- *)
18
19(* Vertices are represented as integers. We need sets of vertices, maps over
20   vertices, maps of vertices to nonempty sets of vertices, maps of vertices
21   to nonempty sets of hardware registers, and priority sets over vertices. *)
22
23module Vertex = struct
24
25  module V = struct
26    type t = Positive.pos
27    let compare = compare
28  end
29
30  include V
31     
32  module Set = Set.Make(V)
33
34  module Map = MyMap.Make(V)
35
36end
37
38module VertexSetMap =
39  SetMap.MakeHomo(Vertex.Set)(Vertex.Map)
40
41module I8051RegisterSetMap =
42  SetMap.MakeHetero(HwRegisterSet)(Vertex.Map)
43
44module PrioritySet =
45  PrioritySet.Make(Vertex)
46
47(* ------------------------------------------------------------------------- *)
48
49(* Each vertex maps to a set of pseudo-registers, which initially is a
50   singleton set, but can grow due to coalescing. Conversely, each
51   pseudo-register maps to a single vertex. *)
52
53module RegMap : sig
54
55  type t
56
57  (* [empty] is the empty map. *)
58
59  val empty: t
60
61  (* [forward] maps a vertex to a set of pseudo-registers. *)
62
63  val forward: Vertex.t -> t -> pseudoregister Pset.set
64
65  (* [backward] maps a pseudo-register to a vertex. *)
66
67  val backward: pseudoregister -> t -> Vertex.t
68
69  (* [add r v m] adds a relation between pseudo-register [r] and
70     vertex [v], both of which are assumed fresh. *)
71
72  val add: pseudoregister -> Vertex.t -> t -> t
73
74  (* [fold f m accu] folds over all vertices. *)
75
76  val fold: (Vertex.t -> pseudoregister Pset.set -> 'a -> 'a) -> t -> 'a -> 'a
77
78  (* [coalesce x y m] coalesces vertices [x] and [y]. Vertex [x] is
79     removed and the pseudo-registers associated with it become
80     associated with [y] instead. *)
81
82  val coalesce: Vertex.t -> Vertex.t -> t -> t
83
84  (* [remove x m] removes vertex [x]. The pseudo-registers associated
85     with [x] disappear. *)
86
87  val remove: Vertex.t -> t -> t
88
89  (* [restrict] keeps only those vertices that satisfy predicate [p]. *)
90
91  val restrict: (Vertex.t -> bool) -> t -> t
92
93end = struct
94
95  type t = {
96      forward: pseudoregister Pset.set Vertex.Map.t;
97      backward: (pseudoregister,Vertex.t) Pmap.map
98    }
99
100  let empty = {
101    forward = Vertex.Map.empty;
102    backward = Pmap.empty
103  }
104
105  let forward v m =
106    Vertex.Map.find v m.forward
107
108  let backward r m =
109    try
110      Pmap.find r m.backward
111    with Not_found ->
112      assert false (* bad pseudo-register *)
113
114  let add r v m = {
115    forward = Vertex.Map.add v (Pset.singleton r) m.forward;
116    backward = Pmap.add r v m.backward
117  }
118
119  let fold f m accu =
120    Vertex.Map.fold f m.forward accu
121
122  let coalesce x y m =
123    let rx, forward = Vertex.Map.find_remove x m.forward in
124    let forward = Vertex.Map.update y (Pset.union rx) forward in
125    let backward =
126      Pset.fold (fun r backward ->
127        Pmap.add r y backward
128      ) rx m.backward
129    in
130    {
131      forward = forward;
132      backward = backward
133    }
134
135  let remove x m =
136    let rx, forward = Vertex.Map.find_remove x m.forward in
137    let backward = Pset.fold Pmap.remove rx m.backward in
138    {
139      forward = forward;
140      backward = backward
141    }
142
143  let restrict p m = {
144    forward = Vertex.Map.restrict p m.forward;
145    backward = Pmap.restrict (fun r -> p (backward r m)) m.backward
146  }
147
148end
149
150(* ------------------------------------------------------------------------- *)
151
152(* Graphs. *)
153
154type graph = {
155
156    (* A two-way correspondence between vertices and pseudo-registers.
157       This data structure is also used to keep a record of the set of
158       all vertices. *)
159
160    regmap: RegMap.t;
161
162    (* Interference edges between two vertices: ``these two vertices
163       cannot receive the same color''. *)
164
165    ivv: VertexSetMap.t;
166
167    (* Interference edges between a vertex and a hardware register:
168       ``this vertex cannot receive this color''. *)
169
170    ivh: I8051RegisterSetMap.t;
171
172    (* Preference edges between two vertices: ``these two vertices
173       should preferably receive the same color''. *)
174
175    pvv: VertexSetMap.t;
176
177    (* Preference edges between a vertex and a hardware register:
178       ``this vertex should preferably receive this color''. *)
179
180    pvh: I8051RegisterSetMap.t;
181
182    (* The degree of each vertex [v], that is, the number of vertices
183       and hardware registers that [v] interferes with, is recorded at
184       all times. We use a ``priority set'' so as to be able to
185       efficiently find a vertex of minimum degree. *)
186
187    degree: PrioritySet.t;
188
189    (* The degree of each *non-move-related* vertex [v]. This
190        information is partially redundant with the [degree] field
191        above. It is nevertheless required in order to be able to
192        efficiently find a *non-move-related* vertex of minimum
193        degree. *)
194
195    nmr: PrioritySet.t;
196
197  }
198
199(* ------------------------------------------------------------------------- *)
200
201(* Our graphs are made up of two subgraphs: the subgraph formed by the
202   interference edges alone and the one formed by the preference edges
203   alone.
204
205   In order to allow more code sharing, we define functions that allow
206   dealing with a single subgraph at a time. They provide operations
207   such as inspecting the neighbors of a vertex, adding edges,
208   removing edges, coalescing two vertices, removing a vertex, etc.
209
210   We first define functions that deal with a ``generic'' subgraph,
211   then (via inheritance) specialize them to deal with the
212   interference subgraph and the preference subgraph with their
213   specific features. *)
214
215class virtual subgraph = object (self)
216
217  (* These methods provide access to the fields of the [graph] data
218     structure that define the subgraph of interest. All data is
219     stored in the [graph] data structure. The object [self] has no
220     state and holds no data. *)
221
222  method virtual getvv: graph -> VertexSetMap.t
223  method virtual setvv: graph -> VertexSetMap.t -> graph
224  method virtual getvh: graph -> I8051RegisterSetMap.t
225  method virtual setvh: graph -> I8051RegisterSetMap.t -> graph
226
227  (* Accessing the neighbors of a vertex and testing whether edges
228     exist. *)
229
230  method neighborsv graph v =
231    VertexSetMap.find v (self#getvv graph)
232
233  method existsvv graph v1 v2 =
234    Vertex.Set.mem v1 (self#neighborsv graph v2)
235
236  method neighborsh graph v =
237    I8051RegisterSetMap.find v (self#getvh graph)
238
239  method existsvh graph v h =
240    HwRegisterSet.mem h (self#neighborsh graph v)
241
242  (* [degree graph v] is the degree of vertex [v] with respect to the
243     subgraph. *)
244
245  method degree graph v =
246    Vertex.Set.cardinal (self#neighborsv graph v) + HwRegisterSet.cardinal (self#neighborsh graph v)
247
248  (* [hwregs graph] is the set of all hardware registers mentioned in
249     the subgraph. *)
250
251  method hwregs graph =
252   let union _ = HwRegisterSet.union in
253   Vertex.Map.fold union (self#getvh graph) HwRegisterSet.empty
254
255  (* [iter graph fvv fvh] iterates over all edges in the subgraph.
256     Vertex-to-vertex edges are presented only once. *)
257
258  method iter graph fvv fvh =
259    Vertex.Map.iter (fun vertex neighbors ->
260      Vertex.Set.iter (fun neighbor ->
261        if vertex < neighbor then
262          fvv vertex neighbor
263      ) neighbors
264    ) (self#getvv graph);
265    Vertex.Map.iter (fun vertex neighbors ->
266      HwRegisterSet.iter (fun neighbor ->
267        fvh vertex neighbor
268      ) neighbors
269    ) (self#getvh graph)
270
271  (* [mkvv graph v1 v2] adds an edge between vertices [v1] and [v2]. *)
272
273  method mkvv graph v1 v2 =
274   if v1 = v2 then
275     graph (* avoid creating self-edge *)
276   else if self#existsvv graph v1 v2 then
277     graph (* avoid re-adding an existing edge *)
278   else
279     self#mkvvi graph v1 v2
280
281  method mkvvi graph v1 v2 =
282     self#setvv graph (VertexSetMap.mkbiedge v1 v2 (self#getvv graph))
283
284  (* [rmvv graph v1 v2] removes an edge between vertices [v1] and [v2].
285     [rmvvifx] removes an edge if it exists. *)
286
287  method rmvv graph v1 v2 =
288    assert (self#existsvv graph v1 v2);
289    self#setvv graph (VertexSetMap.rmbiedge v1 v2 (self#getvv graph))
290
291  method rmvvifx graph v1 v2 =
292    if self#existsvv graph v1 v2 then
293      self#rmvv graph v1 v2
294    else
295      graph
296
297  (* [mkvh graph v h] adds an edge between vertex [v] and hardware
298     register [h]. *)
299
300  method mkvh graph v h =
301    if self#existsvh graph v h then
302      graph (* avoid re-adding an existing edge *)
303    else
304      self#mkvhi graph v h
305
306  method mkvhi graph v h =
307     self#setvh graph (I8051RegisterSetMap.update v (HwRegisterSet.add h) (self#getvh graph))
308
309  (* [rmvh v h] removes an edge between vertex [v] and hardware
310     register [h]. [rmvhifx] removes an edge if it exists. *)
311
312  method rmvh graph v h =
313    assert (self#existsvh graph v h);
314    self#setvh graph (I8051RegisterSetMap.update v (HwRegisterSet.remove h) (self#getvh graph))
315
316  method rmvhifx graph v h =
317    if self#existsvh graph v h then
318      self#rmvh graph v h
319    else
320      graph
321
322  (* [coalesce graph x y] turns every neighbor [w] or [h] of [x] into
323      a neighbor of [y] instead. [w] ranges over both vertices and
324      hardware registers. *)
325
326  method coalesce graph x y =
327    let graph =
328      Vertex.Set.fold (fun w graph ->
329        self#mkvv (self#rmvv graph x w) y w
330      ) (self#neighborsv graph x) graph
331    in
332    let graph =
333      HwRegisterSet.fold (fun h graph ->
334        self#mkvh (self#rmvh graph x h) y h
335      ) (self#neighborsh graph x) graph
336    in
337    graph
338
339  (* [coalesceh graph x h] turns every neighbor [w] of [x] into a
340      neighbor of [h] instead. [w] ranges over both vertices and
341      hardware registers. Edges between two hardware registers are not
342      recorded. *)
343
344  method coalesceh graph x h =
345    let graph =
346      Vertex.Set.fold (fun w graph ->
347        self#mkvh (self#rmvv graph x w) w h
348      ) (self#neighborsv graph x) graph
349    in
350    let graph =
351      HwRegisterSet.fold (fun k graph ->
352        self#rmvh graph x k
353      ) (self#neighborsh graph x) graph
354    in
355    graph
356
357  (* [remove graph x] removes all edges carried by vertex [x]. *)
358
359  method remove graph x =
360    let graph =
361      Vertex.Set.fold (fun w graph ->
362        self#rmvv graph x w
363      ) (self#neighborsv graph x) graph
364    in
365    let graph =
366      HwRegisterSet.fold (fun h graph ->
367        self#rmvh graph x h
368      ) (self#neighborsh graph x) graph
369    in
370    graph
371
372end
373
374(* ------------------------------------------------------------------------- *)
375
376(* The interference subgraph.
377
378   This is a subgraph with the following specific features: (1) the
379   degree of every vertex is recorded in the [degree] field of the
380   [graph] data structure; (2) the degree of every non-move-related
381   vertex is recorded in the [nmr] field of the [graph] data
382   structure; (3) creating an edge in the interference subgraph
383   automatically destroys a corresponding edge in the preference
384   subgraph. *)
385
386class interference (preference : preference Lazy.t) = object (self)
387
388  inherit subgraph as super
389
390  method getvv graph = graph.ivv
391  method setvv graph m = { graph with ivv = m }
392  method getvh graph = graph.ivh
393  method setvh graph m = { graph with ivh = m }
394
395  (* Override the edge creation and destruction methods. *)
396
397  method mkvvi graph v1 v2 =
398    let graph = super#mkvvi graph v1 v2 in
399    let graph = (Lazy.force preference)#rmvvifx graph v1 v2 in (* do not constrain an existing preference edge *)
400    { graph with
401      degree = PrioritySet.increment v1 1 (PrioritySet.increment v2 1 graph.degree);
402      nmr = PrioritySet.incrementifx v1 1 (PrioritySet.incrementifx v2 1 graph.nmr);
403    }
404
405  method rmvv graph v1 v2 =
406    let graph = super#rmvv graph v1 v2 in
407    { graph with
408      degree = PrioritySet.increment v1 (-1) (PrioritySet.increment v2 (-1) graph.degree);
409      nmr = PrioritySet.incrementifx v1 (-1) (PrioritySet.incrementifx v2 (-1) graph.nmr);
410    }
411
412  method mkvhi graph v h =
413    let graph = super#mkvhi graph v h in
414    let graph = (Lazy.force preference)#rmvhifx graph v h in (* do not constrain an existing preference edge *)
415    { graph with
416      degree = PrioritySet.increment v 1 graph.degree;
417      nmr = PrioritySet.incrementifx v 1 graph.nmr;
418    }
419
420  method rmvh graph v h =
421    let graph = super#rmvh graph v h in
422    { graph with
423      degree = PrioritySet.increment v (-1) graph.degree;
424      nmr = PrioritySet.incrementifx v (-1) graph.nmr;
425    }
426
427end
428
429(* ------------------------------------------------------------------------- *)
430
431(* The preference subgraph.
432
433   This is a subgraph with the following specific features: (1) an
434   edge in the preference subgraph cannot be created if a
435   corresponding edge exists in the interference subgraph; (2) adding
436   an edge can make a vertex move-related, which requires taking that
437   vertex out of the [nmr] set; conversely, removing an edge can make
438   a vertex non-move-related, which requires adding that vertex to the
439   [nmr] set. *)
440
441and preference (interference : interference Lazy.t) = object (self)
442
443  inherit subgraph as super
444
445  method getvv graph = graph.pvv
446  method setvv graph m = { graph with pvv = m }
447  method getvh graph = graph.pvh
448  method setvh graph m = { graph with pvh = m }
449
450  (* [nmr graph v] tells whether vertex [v] is non-move-related. *)
451
452  method nmr graph v =
453    Vertex.Set.is_empty (self#neighborsv graph v) &&
454    HwRegisterSet.is_empty (self#neighborsh graph v)
455
456  (* [mkcheck graph v] moves [v] out of the [nmr] set if [v] is
457     non-move-related. *)
458
459  method mkcheck graph v =
460   if self#nmr graph v then
461     { graph with
462       nmr = PrioritySet.remove v graph.nmr }
463   else
464     graph
465
466  (* Override the edge creation methods. *)
467
468  method mkvvi graph v1 v2 =
469    if (Lazy.force interference)#existsvv graph v1 v2 then
470      graph (* avoid creating constrained preference edge *)
471    else 
472      let graph = self#mkcheck graph v1 in
473      let graph = self#mkcheck graph v2 in
474      super#mkvvi graph v1 v2
475
476  method mkvhi graph v h =
477    if (Lazy.force interference)#existsvh graph v h then
478      graph (* avoid creating constrained preference edge *)
479    else
480      let graph = self#mkcheck graph v in
481      super#mkvhi graph v h
482
483  (* [rmcheck graph v] moves [v] into the [nmr] set if [v] is
484     non-move-related. *)
485       
486  method rmcheck graph v =
487    if self#nmr graph v then
488      { graph with
489        nmr = PrioritySet.add v (PrioritySet.priority v graph.degree) graph.nmr
490      }
491    else
492      graph
493
494  (* Override the edge destruction methods. *)
495
496  method rmvv graph v1 v2 =
497    let graph = super#rmvv graph v1 v2 in
498    let graph = self#rmcheck graph v1 in
499    let graph = self#rmcheck graph v2 in
500    graph
501
502  method rmvh graph v h =
503    let graph = super#rmvh graph v h in
504    let graph = self#rmcheck graph v in
505    graph
506
507end
508
509(* ------------------------------------------------------------------------- *)
510
511(* Because the interference and preference subgraphs are mutually
512   referential, a recursive definition is required. It is made
513   somewhat inelegant by Objective Caml's insistence on using the
514   [Lazy] mechanism. *)
515
516let rec interference = lazy (new interference preference)
517    and preference   = lazy (new preference interference)
518let interference     = Lazy.force interference
519let preference       = Lazy.force preference
520
521(* ------------------------------------------------------------------------- *)
522
523(* Inspecting interference graphs. *)
524
525(* [ipp graph v] is the set of vertices that the vertex [v] interferes
526   with. *)
527
528let ipp graph v =
529  interference#neighborsv graph v
530
531(* [iph graph v] is the set of hardware registers that the vertex [v]
532   interferes with. *)
533
534let iph graph v =
535  interference#neighborsh graph v
536
537(* [ppp graph v] is the set of vertices that should preferably be
538   assigned the same color as the vertex [v]. *)
539
540let ppp graph v =
541  preference#neighborsv graph v
542
543(* [pph graph v] is the set of hardware registers that [v] should
544   preferably be assigned. *)
545
546let pph graph v =
547  preference#neighborsh graph v
548
549(* [degree graph v] is the degree of the vertex [v], that is, the number
550   of vertices and hardware registers that [v] interferes with. *)
551
552let degree graph v =
553  PrioritySet.priority v graph.degree
554
555(* [lowest graph] returns [Some (v, d)], where the vertex [v] has
556   minimum degree [d], or returns [None] if the graph is empty. *)
557
558let lowest graph =
559  PrioritySet.lowest graph.degree
560
561(* [lowest_non_move_related graph] returns [Some (v, d)], where the
562   vertex [v] has minimum degree [d] among the vertices that are not
563   move-related, or returns [None] if all vertices are move-related. A
564   vertex is move-related if it carries a preference edge. *)
565
566let lowest_non_move_related graph =
567  PrioritySet.lowest graph.nmr
568
569(* [fold f graph accu] folds over all vertices. *)
570
571let fold f graph accu =
572  RegMap.fold (fun v _ accu -> f v accu) graph.regmap accu
573
574(* [minimum f graph] returns a vertex [v] such that the value of [f x]
575   is minimal. The values returned by [f] are compared using Objective
576   Caml's generic comparison operator [<]. If the graph is empty,
577   [None] is returned. *)
578
579let minimum f graph =
580  match
581    fold (fun w accu ->
582      let dw = f w in
583      match accu with
584      | None ->
585          Some (dw, w)
586      | Some (dv, v) ->
587          if dw < dv then
588            Some (dw, w)
589          else
590            accu
591    ) graph None
592  with
593  | None ->
594      None
595  | Some (_, v) ->
596      Some v
597
598(* [pppick graph p] returns an arbitrary preference edge that
599   satisfies the predicate [p], if the graph contains one. *)
600
601type ppedge =
602    Vertex.t * Vertex.t
603
604let pppick graph p =
605  VertexSetMap.pick graph.pvv p
606
607(* [phpick graph p] returns an arbitrary preference edge that
608   satisfies the predicate [p], if the graph contains one. *)
609
610type phedge =
611    Vertex.t * I8051.register
612
613let phpick graph p =
614  I8051RegisterSetMap.pick graph.pvh p
615
616(* ------------------------------------------------------------------------- *)
617
618(* Constructing interference graphs. *)
619
620(* [create regs] creates an interference graph whose vertices are
621   the pseudo-registers [regs] and that does not have any edges. *)
622
623let create regs =
624  let _, regmap, degree =
625    Pset.fold (fun r (v, regmap, degree) ->
626      Positive.succ v,
627      RegMap.add r v regmap,
628      PrioritySet.add v 0 degree
629    ) regs (Positive.One, RegMap.empty, PrioritySet.empty)
630  in
631  {
632    regmap = regmap;
633    ivv = Vertex.Map.empty;
634    ivh = Vertex.Map.empty;
635    pvv = Vertex.Map.empty;
636    pvh = Vertex.Map.empty;
637    degree = degree;
638    nmr = degree
639  }
640
641(* [lookup graph r] returns the graph vertex associated with
642   pseudo-register [r]. *)
643
644let lookup graph r =
645  RegMap.backward r graph.regmap
646
647(* Conversely, [registers graph v] returns the set of pseudo-registers
648   associated with vertex [v]. *)
649
650let registers graph v =
651  RegMap.forward v graph.regmap
652
653(* [mkipp graph regs1 regs2] adds interference edges between all pairs
654   of pseudo-registers [r1] and [r2], where [r1] ranges over [regs1],
655   [r2] ranges over [regs2], and [r1] and [r2] are distinct. *)
656
657let mkipp graph regs1 regs2 =
658  Pset.fold (fun r1 graph ->
659    let v1 = lookup graph r1 in
660    Pset.fold (fun r2 graph ->
661      interference#mkvv graph v1 (lookup graph r2)
662    ) regs2 graph
663  ) regs1 graph
664
665(* [mkiph graph regs hwregs] adds interference edges between all pairs
666   of a pseudo-register [r] and a hardware register [hwr], where [r]
667   ranges over [regs] and [hwr] ranges over [hwregs]. *)
668
669let mkiph graph regs hwregs =
670  Pset.fold (fun r graph ->
671    let v = lookup graph r in
672    HwRegisterSet.fold (fun h graph ->
673      interference#mkvh graph v h
674    ) hwregs graph
675  ) regs graph
676
677(* [mki graph regs1 regs2] adds interference edges between all pairs
678   of (pseudo- or hardware) registers [r1] and [r2], where [r1] ranges
679   over [regs1], [r2] ranges over [regs2], and [r1] and [r2] are
680   distinct. *)
681
682let mki graph (regs1, hwregs1) (regs2, hwregs2) =
683  let graph = mkipp graph regs1 regs2 in
684  let graph = mkiph graph regs1 hwregs2 in
685  let graph = mkiph graph regs2 hwregs1 in
686  graph
687
688(* [mkppp graph r1 r2] adds a preference edge between the
689    pseudo-registers [r1] and [r2]. *)
690
691let mkppp graph r1 r2 =
692  let v1 = lookup graph r1
693  and v2 = lookup graph r2 in
694  let graph = preference#mkvv graph v1 v2 in
695  graph
696
697(* [mkpph graph r h] adds a preference edge between the
698    pseudo-register [r] and the hardware register [h]. *)
699
700let mkpph graph r h =
701  let v = lookup graph r in
702  let graph = preference#mkvh graph v h in
703  graph
704
705(* ------------------------------------------------------------------------- *)
706
707(*
708(* Displaying interference graphs. *)
709
710open Printf
711
712let hwregs graph =
713  HwRegisterSet.union (interference#hwregs graph) (preference#hwregs graph)
714
715let print_vertex graph v =
716  Pset.print (registers graph v)
717
718let print f graph =
719
720  fprintf f "graph G {\n";
721(*  fprintf f "size=\"6, 3\";\n"; (* in inches *)*)
722  fprintf f "orientation = landscape;\n";
723  fprintf f "rankdir = LR;\n";
724  fprintf f "ratio = compress;\n\n"; (* compress or fill or auto *)
725 
726  RegMap.fold (fun vertex regs () ->
727    fprintf f "r%d [ label=\"%s\" ] ;\n" vertex (Pset.print regs)
728  ) graph.regmap ();
729
730  HwRegisterSet.iter (fun hwr ->
731    let name = I8051.print_register hwr in
732    fprintf f "hwr%s [ label=\"$%s\" ] ;\n" name name
733  ) (hwregs graph);
734
735  interference#iter graph
736    (fun vertex neighbor ->
737      fprintf f "r%d -- r%d ;\n" vertex neighbor)
738    (fun vertex neighbor ->
739      fprintf f "r%d -- hwr%s ;\n" vertex (I8051.print_register neighbor));
740
741  preference#iter graph
742    (fun vertex neighbor ->
743      fprintf f "r%d -- r%d [ style = dashed ] ;\n" vertex neighbor)
744    (fun vertex neighbor ->
745      fprintf f "r%d -- hwr%s [ style = dashed ] ;\n" vertex (I8051.print_register neighbor));
746
747  fprintf f "\n}\n"
748*)
749
750(* ------------------------------------------------------------------------- *)
751
752(* Coalescing. *)
753
754(* [coalesce graph v1 v2] is a new graph where the vertices [v1] and [v2]
755   are coalesced. The new coalesced vertex is known under the name [v2]. *)
756
757let coalesce graph x y =
758
759  assert (x <> y); (* attempt to coalesce one vertex with itself *)
760  assert (not (interference#existsvv graph x y)); (* attempt to coalesce two interfering vertices *)
761
762  (* Perform coalescing in the two subgraphs. *)
763
764  let graph = interference#coalesce graph x y in
765  let graph = preference#coalesce graph x y in
766
767  (* Remove [x] from all tables. *)
768
769  {
770    graph with
771    regmap = RegMap.coalesce x y graph.regmap;
772    ivh = Vertex.Map.remove x graph.ivh;
773    pvh = Vertex.Map.remove x graph.pvh;
774    degree = PrioritySet.remove x graph.degree;
775    nmr = PrioritySet.remove x graph.nmr;
776  }
777
778(* [coalesceh graph v h] coalesces the vertex [v] with the hardware register
779   [h]. This produces a new graph where [v] no longer exists and all edges
780   leading to [v] are replaced with edges leading to [h]. *)
781
782let coalesceh graph x h =
783
784  assert (not (interference#existsvh graph x h)); (* attempt to coalesce interfering entities *)
785
786  (* Perform coalescing in the two subgraphs. *)
787
788  let graph = interference#coalesceh graph x h in
789  let graph = preference#coalesceh graph x h in
790
791  (* Remove [x] from all tables. *)
792
793  {
794    graph with
795    regmap = RegMap.remove x graph.regmap;
796    ivh = Vertex.Map.remove x graph.ivh;
797    pvh = Vertex.Map.remove x graph.pvh;
798    degree = PrioritySet.remove x graph.degree;
799    nmr = PrioritySet.remove x graph.nmr;
800  }
801
802(* ------------------------------------------------------------------------- *)
803
804(* [freeze graph x] is a new graph where all preference edges carried
805   by [x] are removed. *)
806
807let freeze graph x =
808  preference#remove graph x
809
810(* ------------------------------------------------------------------------- *)
811
812(* Removal. *)
813
814(* [remove graph v] is a new graph where vertex [v] is removed. *)
815
816let remove graph v =
817
818  (* Remove all edges carried by [v]. *)
819
820  let graph = interference#remove graph v in
821  let graph = preference#remove graph v in
822
823  (* Remove [v] from all tables. *)
824
825  {
826    graph with
827    regmap = RegMap.remove v graph.regmap;
828    degree = PrioritySet.remove v graph.degree;
829    nmr = PrioritySet.remove v graph.nmr;
830  }
831
832(* ------------------------------------------------------------------------- *)
833
834(* [mkdeg graph] recomputes degree information from scratch. *)
835
836let mkdeg graph =
837  let degree, nmr =
838    fold (fun v (degree, nmr) ->
839      let d = interference#degree graph v in
840      PrioritySet.add v d degree,
841      if preference#nmr graph v then PrioritySet.add v d nmr else nmr
842      ) graph (PrioritySet.empty, PrioritySet.empty)
843  in
844  { graph with
845    degree = degree;
846    nmr = nmr;
847  }
848
849(* [restrict graph p] is a new graph where only those vertices that
850   satisfy predicate [p] are kept. The same effect could be obtained
851   by repeated application of [remove], but [restrict] is likely to be
852   more efficient if many vertices are removed. *)
853
854let restrict graph p =
855  mkdeg {
856    graph with
857    regmap = RegMap.restrict p graph.regmap;
858    ivv = VertexSetMap.restrict p graph.ivv;
859    ivh = Vertex.Map.restrict p graph.ivh;
860    pvv = VertexSetMap.restrict p graph.pvv;
861    pvh = Vertex.Map.restrict p graph.pvh;
862  }
863
864(* [droph graph] is a new graph where all information concerning hardware
865   registers has been dropped. *)
866
867let droph graph =
868  mkdeg {
869    graph with
870    ivh = Vertex.Map.empty;
871    pvh = Vertex.Map.empty;
872  }
873
Note: See TracBrowser for help on using the repository browser.