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
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
|
(* *************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Léo Gourdin UGA, VERIMAG *)
(* *)
(* Copyright VERIMAG. All rights reserved. *)
(* This file is distributed under the terms of the INRIA *)
(* Non-Commercial License Agreement. *)
(* *)
(* *************************************************************)
Require Import Coqlib.
Require Import Asmblock.
Require Import Values.
Require Import Integers.
Require Import AST.
Require Compopts.
Definition is_valid_immofs_32 (z: Z) : bool :=
if (zle z 252) && (zle (-256) z) && ((Z.modulo z 4) =? 0) then true else false.
Definition is_valid_immofs_64 (z: Z) : bool :=
if (zle z 504) && (zle (-512) z) && ((Z.modulo z 8) =? 0) then true else false.
Definition is_valid_ldrw (rd1 rd2: ireg) (b1 b2: iregsp) (n1 n2: int64) : bool :=
let z1 := Int64.signed n1 in
let z2 := Int64.signed n2 in
if (negb (ireg_eq rd1 rd2)) && (iregsp_eq b1 b2) && (negb (iregsp_eq (RR1 rd1) b1))
&& (z2 =? z1 + 4) && (is_valid_immofs_32 z1) then true else false.
Definition is_valid_ldrx (rd1 rd2: ireg) (b1 b2: iregsp) (n1 n2: int64) : bool :=
let z1 := Int64.signed n1 in
let z2 := Int64.signed n2 in
if (negb (ireg_eq rd1 rd2)) && (iregsp_eq b1 b2) && (negb (iregsp_eq (RR1 rd1) b1))
&& (z2 =? z1 + 8) && (is_valid_immofs_64 z1) then true else false.
Definition is_valid_strw (b1 b2: iregsp) (n1 n2: int64) : bool :=
let z1 := Int64.signed n1 in
let z2 := Int64.signed n2 in
if (iregsp_eq b1 b2) && (z2 =? z1 + 4) && (is_valid_immofs_32 z1)
then true else false.
Definition is_valid_strx (b1 b2: iregsp) (n1 n2: int64) : bool :=
let z1 := Int64.signed n1 in
let z2 := Int64.signed n2 in
if (iregsp_eq b1 b2) && (z2 =? z1 + 8) && (is_valid_immofs_64 z1)
then true else false.
(* Try to find arguments of the next compatible ldrw to replace. *)
Fixpoint get_next_comp_ldpw_args (ldb: basic) (rd1: ireg) (b1: iregsp) (n1: int64) (t1: list basic) : option (ireg * iregsp * int64) :=
match t1 with
| nil => None
| (PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) :: t2 =>
if (is_valid_ldrw rd1 rd2 b1 b2 n1 n2) then Some (rd2, b2, n2)
else None
| _ :: t2 => get_next_comp_ldpw_args ldb rd1 b1 n1 t2
end.
(*Fixpoint ldpw_follow (ldb h1: basic) (rd1: ireg) (b1: iregsp) (n1: int64) (t1: list basic) : list basic :=
match (get_next_comp_ldpw_args ldb rd1 b1 n1 t1) with
| None => ldb :: h1 :: t1
| Some (rd2, b2, n2) =>
match t1 with
| nil => ldb :: h1 :: nil
| h2 :: t2 =>
match h2 with
| (PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) =>
|
*)
Fixpoint pair_rep (insns : list basic) : list basic :=
match insns with
| nil => nil
| h0 :: t0 =>
match t0 with
| h1 :: t1 =>
match h0, h1 with
(* ########################## LDP *)
| (PLd_rd_a Pldrw (IR (RR1 rd1)) (ADimm b1 n1)),
(PLd_rd_a Pldrw (IR (RR1 rd2)) (ADimm b2 n2)) =>
(* TODO This could be insteresting to add if compatible with the checker
When both load the same dest, and with no reuse of ld1 in ld2. *)
(* if (ireg_eq rd1 rd2) && (negb (iregsp_eq b2 (RR1 rd1))) then
Pnop :: (pair_rep t0)
(* When two consec mem addr are loading two different dest. *)
else*)
if (is_valid_ldrw rd1 rd2 b1 b2 n1 n2) then
(PLoad (Pldp Pldpw rd1 rd2 (ADimm b1 n1))) :: Pnop :: (pair_rep t1)
(* When nothing can be optimized. *)
else
h0 :: (pair_rep t0)
| (PLd_rd_a Pldrx (IR (RR1 rd1)) (ADimm b1 n1)),
(PLd_rd_a Pldrx (IR (RR1 rd2)) (ADimm b2 n2)) =>
(*if (ireg_eq rd1 rd2) && (negb (iregsp_eq b2 (RR1 rd1))) then
Pnop :: (pair_rep t0)
else*)
if (is_valid_ldrx rd1 rd2 b1 b2 n1 n2) then
(PLoad (Pldp Pldpx rd1 rd2 (ADimm b1 n1))) :: Pnop :: (pair_rep t1)
else
h0 :: (pair_rep t0)
(* When there are some insts between loads/stores *)
(*| (PLd_rd_a Pldrw (IR (RR1 rd1)) (ADimm b1 n1)), h1 =>*)
(*pair_rep (ldpw_follow h0 h1 rd1 b1 n1 t1)*)
(*| (PLd_rd_a Pldrx rd1 (ADimm b1 n1)), h1 => ldpx_follow rd1 b1 n1*)
(* ########################## STP *)
| (PSt_rs_a Pstrw (IR (RR1 rs1)) (ADimm b1 n1)),
(PSt_rs_a Pstrw (IR (RR1 rs2)) (ADimm b2 n2)) =>
(* When both store at the same addr, same ofs. *)
(*if (iregsp_eq b1 b2) && (z2 =? z1) then
Pnop :: (pair_rep t0)
(* When two consec mem addr are targeted by two store. *)
else*)
if (is_valid_strw b1 b2 n1 n2) then
(PStore (Pstp Pstpw rs1 rs2 (ADimm b1 n1))) :: Pnop :: (pair_rep t1)
(* When nothing can be optimized. *)
else
h0 :: (pair_rep t0)
| (PSt_rs_a Pstrx (IR (RR1 rs1)) (ADimm b1 n1)),
(PSt_rs_a Pstrx (IR (RR1 rs2)) (ADimm b2 n2)) =>
(*if (iregsp_eq b1 b2) && (z2 =? z1) then
Pnop :: (pair_rep t0)
else*)
if (is_valid_strx b1 b2 n1 n2) then
(PStore (Pstp Pstpx rs1 rs2 (ADimm b1 n1))) :: Pnop :: (pair_rep t1)
else
h0 :: (pair_rep t0)
| _, _ => h0 :: (pair_rep t0)
end
| nil => h0 :: nil
end
end.
(*Fixpoint stp_rep (insns : list basic) : list basic :=
match insns with
| nil => nil
| h0 :: t0 =>
match t0 with
| h1 :: t1 =>
match h0, h1 with
| (PSt_rs_a Pstrw (IR (RR1 rs1)) (ADimm b1 n1)),
(PSt_rs_a Pstrw (IR (RR1 rs2)) (ADimm b2 n2)) =>
let z1 := Int64.signed n1 in
let z2 := Int64.signed n2 in
(* When both store at the same addr, same ofs. *)
(*if (iregsp_eq b1 b2) && (z2 =? z1) then
Pnop :: (stp_rep t0)
(* When two consec mem addr are targeted by two store. *)
else*)
if (iregsp_eq b1 b2) && (z2 =? z1 + 4) && (is_valid_immofs_32 z1) then
(PStore (Pstp Pstpw rs1 rs2 (ADimm b1 n1))) :: Pnop :: (stp_rep t1)
(* When nothing can be optimized. *)
else
h0 :: (stp_rep t0)
| (PSt_rs_a Pstrx (IR (RR1 rs1)) (ADimm b1 n1)),
(PSt_rs_a Pstrx (IR (RR1 rs2)) (ADimm b2 n2)) =>
let z1 := Int64.signed n1 in
let z2 := Int64.signed n2 in
(*if (iregsp_eq b1 b2) && (z2 =? z1) then
Pnop :: (stp_rep t0)
else*)
if (iregsp_eq b1 b2) && (z2 =? z1 + 8) && (is_valid_immofs_64 z1) then
(PStore (Pstp Pstpx rs1 rs2 (ADimm b1 n1))) :: Pnop :: (stp_rep t1)
else
h0 :: (stp_rep t0)
(*| (PLd_rd_a Pldrw rd1 (ADimm b1 n1)), h1 => ldpw_follow rd1 b1 n1*)
(*| (PLd_rd_a Pldrx rd1 (ADimm b1 n1)), h1 => ldpx_follow rd1 b1 n1*)
| _, _ => h0 :: (stp_rep t0)
end
| nil => h0 :: nil
end
end.
*)
Definition optimize_body (insns : list basic) :=
(* TODO ADD A FLAG TO ENABLE PEEPHOLE *)
if Compopts.optim_coalesce_mem tt
then (pair_rep insns)
else insns.
Program Definition optimize_bblock (bb : bblock) :=
let optimized := optimize_body (body bb) in
let wf_ok := non_empty_bblockb optimized (exit bb) in
{| header := header bb;
body := if wf_ok then optimized else (body bb);
exit := exit bb |}.
Next Obligation.
destruct (non_empty_bblockb (optimize_body (body bb))) eqn:Rwf.
- rewrite Rwf. cbn. trivial.
- exact (correct bb).
Qed.
|
