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