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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
|
Require Import Coqlib.
Require Import FSets.
Require Import FSetAVL.
Require Import Maps.
Require Import Ordered.
Require Import Registers.
Require Import Locations.
Require Import AST.
Require Import Op.
Require Import RTLtyping.
Require Import RTL.
Require Import Conventions.
Require Import InterfGraph.
Definition add_interf_live
(filter: reg -> bool) (res: reg) (live: Regset.t) (g: graph): graph :=
Regset.fold
(fun r g => if filter r then add_interf r res g else g) live g.
Definition add_interf_op
(res: reg) (live: Regset.t) (g: graph): graph :=
add_interf_live
(fun r => if Reg.eq r res then false else true)
res live g.
Definition add_interf_move
(arg res: reg) (live: Regset.t) (g: graph): graph :=
add_interf_live
(fun r =>
if Reg.eq r res then false else
if Reg.eq r arg then false else true)
res live g.
Definition add_interf_destroyed
(live: Regset.t) (destroyed: list mreg) (g: graph): graph :=
List.fold_left
(fun g mr => Regset.fold (fun r g => add_interf_mreg r mr g) live g)
destroyed g.
Definition add_interfs_indirect_call
(rfun: reg) (locs: list loc) (g: graph): graph :=
List.fold_left
(fun g loc =>
match loc with R mr => add_interf_mreg rfun mr g | _ => g end)
locs g.
Definition add_interf_call
(ros: reg + ident) (locs: list loc) (g: graph): graph :=
match ros with
| inl rfun => add_interfs_indirect_call rfun locs g
| inr idfun => g
end.
Fixpoint add_prefs_call
(args: list reg) (locs: list loc) (g: graph) {struct args} : graph :=
match args, locs with
| a1 :: al, l1 :: ll =>
add_prefs_call al ll
(match l1 with R mr => add_pref_mreg a1 mr g | _ => g end)
| _, _ => g
end.
Definition add_interf_entry
(params: list reg) (live: Regset.t) (g: graph): graph :=
List.fold_left (fun g r => add_interf_op r live g) params g.
Fixpoint add_interf_params
(params: list reg) (g: graph) {struct params}: graph :=
match params with
| nil => g
| p1 :: pl =>
add_interf_params pl
(List.fold_left
(fun g r => if Reg.eq r p1 then g else add_interf r p1 g)
pl g)
end.
Definition add_edges_instr
(sig: signature) (i: instruction) (live: Regset.t) (g: graph) : graph :=
match i with
| Iop op args res s =>
if Regset.mem res live then
match is_move_operation op args with
| Some arg =>
add_pref arg res (add_interf_move arg res live g)
| None =>
add_interf_op res live g
end
else g
| Iload chunk addr args dst s =>
if Regset.mem dst live
then add_interf_op dst live g
else g
| Icall sig ros args res s =>
let largs := loc_arguments sig in
let lres := loc_result sig in
add_prefs_call args largs
(add_pref_mreg res lres
(add_interf_op res live
(add_interf_call ros largs
(add_interf_destroyed
(Regset.remove res live) destroyed_at_call_regs g))))
| Itailcall sig ros args =>
let largs := loc_arguments sig in
add_prefs_call args largs
(add_interf_call ros largs g)
| Ireturn (Some r) =>
add_pref_mreg r (loc_result sig) g
| _ => g
end.
Definition add_edges_instrs (f: function) (live: PMap.t Regset.t) : graph :=
PTree.fold
(fun g pc i => add_edges_instr f.(fn_sig) i live!!pc g)
f.(fn_code)
empty_graph.
Definition interf_graph (f: function) (live: PMap.t Regset.t) (live0: Regset.t) :=
add_prefs_call f.(fn_params) (loc_parameters f.(fn_sig))
(add_interf_params f.(fn_params)
(add_interf_entry f.(fn_params) live0
(add_edges_instrs f live))).
(** * Graph coloring *)
(** The actual coloring of the graph is performed by a function written
directly in Caml, and not proved correct in any way. This function
takes as argument the [RTL] function, the interference graph for
this function, an assignment of types to [RTL] pseudo-registers,
and the set of all [RTL] pseudo-registers mentioned in the
interference graph. It returns the coloring as a function from
pseudo-registers to locations. *)
(*
Parameter graph_coloring:
function -> graph -> regenv -> Regset.t -> (reg -> loc).
*)
(** To ensure that the result of [graph_coloring] is a correct coloring,
we check a posteriori its result using the following Coq functions.
Let [coloring] be the function [reg -> loc] returned by [graph_coloring].
The three properties checked are:
- [coloring r1 <> coloring r2] if there is a conflict edge between
[r1] and [r2] in the interference graph.
- [coloring r1 <> R m2] if there is a conflict edge between pseudo-register
[r1] and machine register [m2] in the interference graph.
- For all [r] mentioned in the interference graph,
the location [coloring r] is acceptable and has the same type as [r].
*)
Definition check_coloring_1 (g: graph) (coloring: reg -> loc) :=
SetRegReg.for_all
(fun r1r2 =>
if Loc.eq (coloring (fst r1r2)) (coloring (snd r1r2)) then false else true)
g.(interf_reg_reg).
Definition check_coloring_2 (g: graph) (coloring: reg -> loc) :=
SetRegMreg.for_all
(fun r1mr2 =>
if Loc.eq (coloring (fst r1mr2)) (R (snd r1mr2)) then false else true)
g.(interf_reg_mreg).
Definition same_typ (t1 t2: typ) :=
match t1, t2 with
| Tint, Tint => true
| Tfloat, Tfloat => true
| _, _ => false
end.
Definition loc_is_acceptable (l: loc) :=
match l with
| R r =>
if In_dec Loc.eq l temporaries then false else true
| S (Local ofs ty) =>
if zlt ofs 0 then false else true
| _ =>
false
end.
Definition check_coloring_3 (rs: Regset.t) (env: regenv) (coloring: reg -> loc) :=
Regset.for_all
(fun r =>
let l := coloring r in
andb (loc_is_acceptable l) (same_typ (env r) (Loc.type l)))
rs.
Definition check_coloring
(g: graph) (env: regenv) (rs: Regset.t) (coloring: reg -> loc) :=
andb (check_coloring_1 g coloring)
(andb (check_coloring_2 g coloring)
(check_coloring_3 rs env coloring)).
|
