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
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
|
(* *************************************************************)
(* *)
(* 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. *)
(* *)
(* *************************************************************)
open Camlcoq
open Asmblock
open Asm
open Int64
open Printf
let debug = true
let is_valid_immofs_32 z =
if z <= 252 && z >= -256 && z mod 4 == 0 then true else false
let is_valid_immofs_64 z =
if z <= 504 && z >= -512 && z mod 8 == 0 then true else false
let is_valid_ldrw rd1 rd2 b1 b2 n1 n2 =
let z1 = to_int (camlint64_of_coqint n1) in
let z2 = to_int (camlint64_of_coqint n2) in
if
(not (ireg_eq rd1 rd2))
&& iregsp_eq b1 b2
&& (not (iregsp_eq (RR1 rd1) b1))
&& z2 == z1 + 4
&& is_valid_immofs_32 z1
then true
else false
let is_valid_ldrx rd1 rd2 b1 b2 n1 n2 =
let z1 = to_int (camlint64_of_coqint n1) in
let z2 = to_int (camlint64_of_coqint n2) in
if
(not (ireg_eq rd1 rd2))
&& iregsp_eq b1 b2
&& (not (iregsp_eq (RR1 rd1) b1))
&& z2 == z1 + 8
&& is_valid_immofs_64 z1
then true
else false
let is_valid_strw b1 b2 n1 n2 =
let z1 = to_int (camlint64_of_coqint n1) in
let z2 = to_int (camlint64_of_coqint n2) in
if iregsp_eq b1 b2 && z2 == z1 + 4 && is_valid_immofs_32 z1 then true
else false
let is_valid_strx b1 b2 n1 n2 =
let z1 = to_int (camlint64_of_coqint n1) in
let z2 = to_int (camlint64_of_coqint n2) in
if iregsp_eq b1 b2 && z2 == z1 + 8 && is_valid_immofs_64 z1 then true
else false
let dreg_of_ireg r = IR (RR1 r)
(*let pot_ldrw_rep = ref []*)
let rec affect_symb_mem reg pot_rep stype =
match (pot_rep, stype) with
| [], _ -> []
| ( ((PLoad (PLd_rd_a (Pldrw, IR (RR1 rd), ADimm (b, n))), _) as h0) :: t0,
"ldrw" ) ->
if dreg_eq reg (IR b) then affect_symb_mem reg t0 stype
else h0 :: affect_symb_mem reg t0 stype
| _, _ -> failwith "Found an inconsistent inst in pot_rep"
let rec read_symb_mem reg pot_rep stype =
match (pot_rep, stype) with
| [], _ -> []
| ( ((PLoad (PLd_rd_a (Pldrw, IR (RR1 rd), ADimm (b, n))), _) as h0) :: t0,
"ldrw" ) ->
if dreg_eq reg (IR (RR1 rd)) then read_symb_mem reg t0 stype
else h0 :: read_symb_mem reg t0 stype
| _, _ -> failwith "Found an inconsistent inst in pot_rep"
let update_pot_rep inst pot_rep stype =
match inst with
| PArith i -> (
match i with
| PArithP (_, rd) -> pot_rep := affect_symb_mem rd !pot_rep stype
| PArithPP (_, rd, rs) ->
pot_rep := affect_symb_mem rd !pot_rep stype;
pot_rep := read_symb_mem rs !pot_rep stype
| PArithPPP (_, rd, rs1, rs2) ->
pot_rep := affect_symb_mem rd !pot_rep stype;
pot_rep := read_symb_mem rs1 !pot_rep stype;
pot_rep := read_symb_mem rs2 !pot_rep stype
| PArithRR0R (_, rd, rs1, rs2) ->
pot_rep := affect_symb_mem (dreg_of_ireg rd) !pot_rep stype;
(match rs1 with
| RR0 rs1 ->
pot_rep := read_symb_mem (dreg_of_ireg rs1) !pot_rep stype
| _ -> ());
pot_rep := read_symb_mem (dreg_of_ireg rs2) !pot_rep stype
| PArithRR0 (_, rd, rs) -> (
pot_rep := affect_symb_mem (dreg_of_ireg rd) !pot_rep stype;
match rs with
| RR0 rs1 ->
pot_rep := read_symb_mem (dreg_of_ireg rs1) !pot_rep stype
| _ -> ())
| PArithARRRR0 (_, rd, rs1, rs2, rs3) -> (
pot_rep := affect_symb_mem (dreg_of_ireg rd) !pot_rep stype;
pot_rep := read_symb_mem (dreg_of_ireg rs1) !pot_rep stype;
pot_rep := read_symb_mem (dreg_of_ireg rs2) !pot_rep stype;
match rs3 with
| RR0 rs1 ->
pot_rep := read_symb_mem (dreg_of_ireg rs1) !pot_rep stype
| _ -> ())
| PArithComparisonPP (_, rs1, rs2) ->
pot_rep := read_symb_mem rs1 !pot_rep stype;
pot_rep := read_symb_mem rs2 !pot_rep stype
| PArithComparisonR0R (_, rs1, rs2) ->
(match rs1 with
| RR0 rs1 ->
pot_rep := read_symb_mem (dreg_of_ireg rs1) !pot_rep stype
| _ -> ());
pot_rep := read_symb_mem (dreg_of_ireg rs2) !pot_rep stype
| PArithComparisonP (_, rs1) ->
pot_rep := read_symb_mem rs1 !pot_rep stype
| Pcset (rd, _) ->
pot_rep := affect_symb_mem (dreg_of_ireg rd) !pot_rep stype
| Pfmovi (_, _, rs) -> (
match rs with
| RR0 rs -> pot_rep := read_symb_mem (dreg_of_ireg rs) !pot_rep stype
| _ -> ())
| Pcsel (rd, rs1, rs2, _) ->
pot_rep := affect_symb_mem rd !pot_rep stype;
pot_rep := read_symb_mem rs1 !pot_rep stype;
pot_rep := read_symb_mem rs2 !pot_rep stype
| Pfnmul (_, rd, rs1, rs2) -> ())
| PLoad i -> (
match i with
| PLd_rd_a (_, rd, _) -> pot_rep := affect_symb_mem rd !pot_rep stype
| Pldp (_, rd1, rd2, _) ->
pot_rep := affect_symb_mem (dreg_of_ireg rd1) !pot_rep stype;
pot_rep := affect_symb_mem (dreg_of_ireg rd2) !pot_rep stype)
| PStore _ -> pot_rep := []
(* TODO *)
| _ -> ()
(*let update_symb_mem inst = update_pot_rep inst pot_ldrw_rep "ldrw"*)
let rec search_compat_rep rd b n pot_rep stype =
match (pot_rep, stype) with
| [], _ -> None
| ( ((PLoad (PLd_rd_a (Pldrx, IR (RR1 rd'), ADimm (b', n'))), c) as h0) :: t0,
"ldrw" ) ->
if is_valid_ldrw rd rd' b b' n n' then Some h0
else search_compat_rep rd b n t0 stype
| _, _ -> None
let pair_rep insta =
for i = 0 to Array.length insta - 2 do
let h0 = insta.(i) in
let h1 = insta.(i + 1) in
match (h0, h1) with
| ( PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))),
PLoad (PLd_rd_a (Pldrw, IR (RR1 rd2), ADimm (b2, n2))) ) ->
(* When both load the same dest, and with no reuse of ld1 in ld2. *)
if ireg_eq rd1 rd2 && not (iregsp_eq b2 (RR1 rd1)) then (
if debug then eprintf "LDP_WOPT\n";
insta.(i) <- Pnop
(* When two consec mem addr are loading two different dest. *))
else if is_valid_ldrw rd1 rd2 b1 b2 n1 n2 then (
if debug then eprintf "LDP_WPEEP\n";
insta.(i) <- PLoad (Pldp (Pldpw, rd1, rd2, ADimm (b1, n1)));
insta.(i + 1) <- Pnop)
| ( PLoad (PLd_rd_a (Pldrx, IR (RR1 rd1), ADimm (b1, n1))),
PLoad (PLd_rd_a (Pldrx, IR (RR1 rd2), ADimm (b2, n2))) ) ->
if ireg_eq rd1 rd2 && not (iregsp_eq b2 (RR1 rd1)) then (
if debug then eprintf "LDP_XOPT\n";
insta.(i) <- Pnop)
else if is_valid_ldrx rd1 rd2 b1 b2 n1 n2 then (
if debug then eprintf "LDP_XPEEP\n";
insta.(i) <- PLoad (Pldp (Pldpx, rd1, rd2, ADimm (b1, n1)));
insta.(i + 1) <- Pnop
(* When there are some insts between loads/stores *)
(*| PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))), _ ->*)
(*(match search_compat_rep h0 pot_ldrw_rep with*)
(*| None -> (pot_ldrw_rep := (h0, count) :: !pot_ldrw_rep; h0 :: pair_rep insta t0)*)
(*| Some (l, c) -> *))
| ( PStore (PSt_rs_a (Pstrw, IR (RR1 rs1), ADimm (b1, n1))),
PStore (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 insta t0)
(* When two consec mem addr are targeted by two store. *)
else*)
if is_valid_strw b1 b2 n1 n2 then (
if debug then eprintf "STP_WPEEP\n";
insta.(i) <- PStore (Pstp (Pstpw, rs1, rs2, ADimm (b1, n1)));
insta.(i + 1) <- Pnop (* When nothing can be optimized. *))
| ( PStore (PSt_rs_a (Pstrx, IR (RR1 rs1), ADimm (b1, n1))),
PStore (PSt_rs_a (Pstrx, IR (RR1 rs2), ADimm (b2, n2))) ) ->
(*if (iregsp_eq b1 b2) && (z2 =? z1) then
Pnop :: (pair_rep insta t0)
else*)
if is_valid_strx b1 b2 n1 n2 then (
if debug then eprintf "STP_XPEEP\n";
insta.(i) <- PStore (Pstp (Pstpx, rs1, rs2, ADimm (b1, n1)));
insta.(i + 1) <- Pnop)
| h0, _ -> () (*update_symb_mem h0*)
done
let optimize_bdy (bdy : basic list) : basic list =
if !Clflags.option_fcoalesce_mem then
let insta = Array.of_list bdy in
(pair_rep insta; Array.to_list insta)
else bdy
(** Called peephole function from Coq *)
let peephole_opt bdy =
Timing.time_coq
[
'P'; 'e'; 'e'; 'p'; 'h'; 'o'; 'l'; 'e'; ' '; 'o'; 'r'; 'a'; 'c'; 'l'; 'e';
]
optimize_bdy bdy
|
