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
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** Redundant Reloads Elimination *)
Require Import Coqlib.
Require Import AST.
Require Import Op.
Require Import Locations.
Require Import Conventions.
Require Import Linear.
(** * Equations between slots and machine registers *)
(** The RRE pass keeps track of which register holds the value of which
stack slot, using sets of equations like the following. *)
Record equation := mkeq { e_reg: mreg; e_slot: slot }.
Definition equations : Type := list equation.
Fixpoint find_reg_containing (s: slot) (eqs: equations) : option mreg :=
match eqs with
| nil => None
| e :: eqs' => if slot_eq (e_slot e) s then Some (e_reg e) else find_reg_containing s eqs'
end.
Definition eq_equation (eq1 eq2: equation) : {eq1=eq2} + {eq1<>eq2}.
Proof.
generalize slot_eq mreg_eq. decide equality.
Defined.
Definition contains_equation (s: slot) (r: mreg) (eqs: equations) : bool :=
In_dec eq_equation (mkeq r s) eqs.
(** Remove equations that are invalidated by an assignment to location [l]. *)
Fixpoint kill_loc (l: loc) (eqs: equations) : equations :=
match eqs with
| nil => nil
| e :: eqs' =>
if Loc.diff_dec (S (e_slot e)) l && Loc.diff_dec (R (e_reg e)) l
then e :: kill_loc l eqs'
else kill_loc l eqs'
end.
(** Same, for a list of locations [ll]. *)
Definition kill_locs (ll: list loc) (eqs: equations) : equations :=
List.fold_left (fun eqs l => kill_loc l eqs) ll eqs.
Definition kill_temps (eqs: equations) : equations :=
kill_locs temporaries eqs.
Definition kill_at_move (eqs: equations) : equations :=
kill_locs destroyed_at_move eqs.
Definition kill_op (op: operation) (eqs: equations) : equations :=
match op with Omove => kill_at_move eqs | _ => kill_temps eqs end.
(** * Safety criterion *)
Definition is_incoming (s: slot) : bool :=
match s with
| Incoming _ _ => true
| _ => false
end.
(** Turning a [Lgetstack] into a register-to-register move is not always
safe: at least on x86, the move destroys some registers
(those from [destroyed_at_move] list) while the [Lgetstack] does not.
Therefore, we perform this transformation only if the destroyed
registers are not used before being destroyed by a later
[Lop], [Lload], [Lstore], [Lbuiltin], [Lcond] or [Ljumptable] operation. *)
Fixpoint safe_move_insertion (c: code) : bool :=
match c with
| Lgetstack s r :: c' =>
negb(In_dec mreg_eq r destroyed_at_move_regs) && safe_move_insertion c'
| Lsetstack r s :: c' =>
negb(In_dec mreg_eq r destroyed_at_move_regs)
| Lop op args res :: c' =>
list_disjoint_dec mreg_eq args destroyed_at_move_regs
| Lload chunk addr args res :: c' =>
list_disjoint_dec mreg_eq args destroyed_at_move_regs
| Lstore chunk addr args src :: c' =>
list_disjoint_dec mreg_eq (src :: args) destroyed_at_move_regs
| Lbuiltin ef args res :: c' =>
list_disjoint_dec mreg_eq args destroyed_at_move_regs
| Lcond cond args lbl :: c' =>
list_disjoint_dec mreg_eq args destroyed_at_move_regs
| Ljumptable arg tbl :: c' =>
negb(In_dec mreg_eq arg destroyed_at_move_regs)
| _ => false
end.
(** * Code transformation *)
(** The following function eliminates [Lgetstack] instructions or turn them
into register-to-register move whenever possible. Simultaneously,
it propagates valid (register, slot) equations across basic blocks. *)
(** [transf_code] is written in accumulator-passing style so that it runs
in constant stack space. The [k] parameter accumulates the instructions
to be generated, in reverse order, and is then reversed at the end *)
Fixpoint transf_code (eqs: equations) (c: code) (k: code) : code :=
match c with
| nil => List.rev' k
| Lgetstack s r :: c =>
if is_incoming s then
transf_code (kill_loc (R r) (kill_loc (R IT1) eqs)) c (Lgetstack s r :: k)
else if contains_equation s r eqs then
transf_code eqs c k
else
match find_reg_containing s eqs with
| Some r' =>
if safe_move_insertion c then
transf_code (kill_at_move (mkeq r s :: kill_loc (R r) eqs)) c (Lop Omove (r' :: nil) r :: k)
else
transf_code (mkeq r s :: kill_loc (R r) eqs) c (Lgetstack s r :: k)
| None =>
transf_code (mkeq r s :: kill_loc (R r) eqs) c (Lgetstack s r :: k)
end
| Lsetstack r s :: c =>
transf_code (kill_at_move (mkeq r s :: kill_loc (S s) eqs)) c (Lsetstack r s :: k)
| Lop op args res :: c =>
transf_code (kill_loc (R res) (kill_op op eqs)) c (Lop op args res :: k)
| Lload chunk addr args res :: c =>
transf_code (kill_loc (R res) (kill_temps eqs)) c (Lload chunk addr args res :: k)
| Lstore chunk addr args src :: c =>
transf_code (kill_temps eqs) c (Lstore chunk addr args src :: k)
| Lcall sg ros :: c =>
transf_code nil c (Lcall sg ros :: k)
| Ltailcall sg ros :: c =>
transf_code nil c (Ltailcall sg ros :: k)
| Lbuiltin ef args res :: c =>
transf_code (kill_loc (R res) (kill_temps eqs)) c (Lbuiltin ef args res :: k)
| Lannot ef args :: c =>
transf_code eqs c (Lannot ef args :: k)
| Llabel lbl :: c =>
transf_code nil c (Llabel lbl :: k)
| Lgoto lbl :: c =>
transf_code nil c (Lgoto lbl :: k)
| Lcond cond args lbl :: c =>
transf_code (kill_temps eqs) c (Lcond cond args lbl :: k)
| Ljumptable arg lbls :: c =>
transf_code nil c (Ljumptable arg lbls :: k)
| Lreturn :: c =>
transf_code nil c (Lreturn :: k)
end.
Definition transf_function (f: function) : function :=
mkfunction
(fn_sig f)
(fn_stacksize f)
(transf_code nil (fn_code f) nil).
Definition transf_fundef (fd: fundef) : fundef :=
transf_fundef transf_function fd.
Definition transf_program (p: program) : program :=
transform_program transf_fundef p.
|
