blob: 7842a4bd931691dbd44a1de35490921577db886d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
|
Require Import Recdef.
Require Import FSetInterface.
Require Import InterfGraphMapImp.
Require Import OrderedOption.
Require Import FMapAVL.
Require Import IRC_termination.
Require Import IRC_graph.
Require Import IRC_Graph_Functions.
Require Import Edges.
Import Edge RegFacts Props OTFacts.
(* Definition of Register options *)
Module OptionReg := OrderedOpt Register.
(* Definition of the type of colorings *)
Definition Coloring := Register.t -> OptionReg.t.
(* Map used to build a coloring of the graph.
A coloring is a the function find applied to the map *)
Module ColorMap := FMapAVL.Make Register.
(* Function to complete a coloring by giving the
same color to coalesced vertices *)
Definition complete_coloring e col : ColorMap.t Register.t :=
let x := snd_ext e in let y := fst_ext e in
match ColorMap.find y col with
| None => col
| Some c => ColorMap.add x c col
end.
(* Function to compute forbidden colors when completing the coloring
for simplified or spilled registers (optimistic spilling) *)
Section add_monad.
Definition vertex_add_monad (o : option Register.t) (VS : VertexSet.t) :=
match o with
|Some v => VertexSet.add v VS
|None => VS
end.
Variable A : Type.
Lemma monad_fold : forall f a l s,
VertexSet.Equal (fold_left
(fun (x : VertexSet.t) (e : A) => vertex_add_monad (f e) x)
(a :: l) s)
(vertex_add_monad (f a)
(fold_left (fun (x : VertexSet.t) (e : A) => vertex_add_monad (f e) x) l s)).
Proof.
intros f a l s;apply fold_left_assoc.
intros y z e;unfold vertex_add_monad.
destruct (f y);destruct (f z);[apply add_add|intuition|intuition|intuition].
intros e1 e2 y H. unfold vertex_add_monad.
destruct (f y);intuition.
apply Dec.F.add_m; intuition.
Qed.
End add_monad.
Definition forbidden_colors x col g :=
VertexSet.fold (fun v => vertex_add_monad (ColorMap.find v col))
(interference_adj x g)
VertexSet.empty.
(* Function to complete the coloring for simplified or spilled vertices.
Calls forbidden_colors. Is choosing yet any available color *)
Definition available_coloring ircg x (col : ColorMap.t Register.t) :=
let g := (irc_g ircg) in let palette := (pal ircg) in
match (VertexSet.choose (VertexSet.diff palette (forbidden_colors x col g))) with
| None => col
| Some c => ColorMap.add x c col
end.
(* Definition of the empty coloring as the coloring where the only
colored vertices are the precolored ones *)
Definition precoloring_map g :=
VertexSet.fold (fun x => ColorMap.add x x) (precolored g) (ColorMap.empty Register.t).
Function IRC_map (g : irc_graph)
{measure irc_measure g} : ColorMap.t Register.t :=
match simplify g with
|Some rg' => let (r,g') := rg' in available_coloring g r (IRC_map g')
|None => match coalesce g with
|Some eg' => let (e,g') := eg' in complete_coloring e (IRC_map g')
|None => match freeze g with
|Some rg' => let (r,g') := rg' in IRC_map g'
|None => match spill g with
|Some rg' => let (r,g') := rg' in available_coloring g r (IRC_map g')
|None => precoloring_map (irc_g g)
end
end
end
end.
Proof.
intros. apply (simplify_dec g r g' teq).
intros. apply (coalesce_dec g e g' teq0).
intros. apply (freeze_dec g r g' teq1).
intros. apply (spill_dec g r g' teq2).
Qed.
(* Definition of the transformation from a map to a coloring,
simply by using find *)
Definition map_to_coloring (colmap : ColorMap.t Register.t) :=
fun x => ColorMap.find x colmap.
(* Final definition of iterated register coalescing *)
Definition IRC g palette :=
let g' := graph_to_IRC_graph g palette in map_to_coloring (IRC_map g').
Definition precoloring g := map_to_coloring (precoloring_map g).
|
