Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

PeepholeOracle.ml 25.1 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
(* *************************************************************)
(*                                                             *)
(*             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

19
(* If true, the oracle will print a msg for each applied peephole *)
Léo Gourdin's avatar
Léo Gourdin committed
20
let debug = false
21

Léo Gourdin's avatar
Léo Gourdin committed
22
(* Functions to verify the immediate offset range for ldp/stp *)
23
let is_valid_immofs_32 z =
Léo Gourdin's avatar
Léo Gourdin committed
24
  if z <= 252 && z >= -256 && z mod 4 = 0 then true else false
25
26

let is_valid_immofs_64 z =
Léo Gourdin's avatar
Léo Gourdin committed
27
  if z <= 504 && z >= -512 && z mod 8 = 0 then true else false
28

Léo Gourdin's avatar
Léo Gourdin committed
29
(* Functions to check if a ldp/stp replacement is valid according to args *)
Léo Gourdin's avatar
Léo Gourdin committed
30
let is_valid_ldr32 rd1 rd2 b1 b2 n1 n2 =
31
32
33
  let z1 = to_int (camlint64_of_coqint n1) in
  let z2 = to_int (camlint64_of_coqint n2) in
  if
Léo Gourdin's avatar
Léo Gourdin committed
34
    (not (dreg_eq rd1 rd2))
35
    && iregsp_eq b1 b2
Léo Gourdin's avatar
Léo Gourdin committed
36
    && (not (dreg_eq rd1 (IR b2)))
Léo Gourdin's avatar
Léo Gourdin committed
37
    && (z2 = z1 + 4 || z2 = z1 - 4)
38
39
40
41
    && is_valid_immofs_32 z1
  then true
  else false

Léo Gourdin's avatar
Léo Gourdin committed
42
let is_valid_ldr64 rd1 rd2 b1 b2 n1 n2 =
43
44
45
  let z1 = to_int (camlint64_of_coqint n1) in
  let z2 = to_int (camlint64_of_coqint n2) in
  if
Léo Gourdin's avatar
Léo Gourdin committed
46
    (not (dreg_eq rd1 rd2))
47
    && iregsp_eq b1 b2
Léo Gourdin's avatar
Léo Gourdin committed
48
    && (not (dreg_eq rd1 (IR b2)))
Léo Gourdin's avatar
Léo Gourdin committed
49
    && (z2 = z1 + 8 || z2 = z1 - 8)
50
51
52
53
    && is_valid_immofs_64 z1
  then true
  else false

Léo Gourdin's avatar
Léo Gourdin committed
54
let is_valid_str32 b1 b2 n1 n2 =
55
56
  let z1 = to_int (camlint64_of_coqint n1) in
  let z2 = to_int (camlint64_of_coqint n2) in
Léo Gourdin's avatar
Léo Gourdin committed
57
  if iregsp_eq b1 b2 && z2 = z1 + 4 && is_valid_immofs_32 z1 then true
58
59
  else false

Léo Gourdin's avatar
Léo Gourdin committed
60
let is_valid_str64 b1 b2 n1 n2 =
61
62
  let z1 = to_int (camlint64_of_coqint n1) in
  let z2 = to_int (camlint64_of_coqint n2) in
Léo Gourdin's avatar
Léo Gourdin committed
63
  if iregsp_eq b1 b2 && z2 = z1 + 8 && is_valid_immofs_64 z1 then true
64
65
66
  else false

let dreg_of_ireg r = IR (RR1 r)
Léo Gourdin's avatar
Léo Gourdin committed
67

Léo Gourdin's avatar
Léo Gourdin committed
68
let dreg_of_freg r = FR r
69

Léo Gourdin's avatar
Léo Gourdin committed
70
71
72
73
(* Return true if an intermediate
 * affectation eliminates the potential
 * candidate *)
let verify_load_affect reg rd b rev =
74
75
  let b = IR b in
  if not rev then dreg_eq reg b else dreg_eq reg b || dreg_eq reg rd
Léo Gourdin's avatar
Léo Gourdin committed
76
77
78
79

(* Return true if an intermediate
 * read eliminates the potential
 * candidate *)
Léo Gourdin's avatar
Léo Gourdin committed
80
let verify_load_read reg rd b rev = dreg_eq reg rd
Léo Gourdin's avatar
Léo Gourdin committed
81
82
83
84
85

(* Return true if an intermediate
 * affectation eliminates the potential
 * candidate *)
let verify_store_affect reg rs b rev =
86
87
  let b = IR b in
  dreg_eq reg b || dreg_eq reg rs
Léo Gourdin's avatar
Léo Gourdin committed
88

Léo Gourdin's avatar
Léo Gourdin committed
89
type ph_type = P32 | P32f | P64 | P64f
Léo Gourdin's avatar
Léo Gourdin committed
90

Léo Gourdin's avatar
Léo Gourdin committed
91
type inst_type = Ldr of ph_type | Str of ph_type
Léo Gourdin's avatar
Léo Gourdin committed
92
93
94
95
96
97
98
99
100
101
102
103
104

let ph_ty_to_string = function
  | Ldr P32 -> "ldr32"
  | Ldr P32f -> "ldr32f"
  | Ldr P64 -> "ldr64"
  | Ldr P64f -> "ldr64f"
  | Str P32 -> "str32"
  | Str P32f -> "str32f"
  | Str P64 -> "str64"
  | Str P64f -> "str64f"

let print_ph_ty chan v = output_string chan (ph_ty_to_string v)

Léo Gourdin's avatar
Léo Gourdin committed
105
106
let symb_mem = Hashtbl.create 9

Léo Gourdin's avatar
Léo Gourdin committed
107
108
(* Affect a symbolic memory list of potential replacements
 * for a given write in reg *)
Léo Gourdin's avatar
Léo Gourdin committed
109
let rec affect_symb_mem reg insta pot_rep stype rev =
Léo Gourdin's avatar
Léo Gourdin committed
110
111
112
113
  match pot_rep with
  | [] -> []
  | h0 :: t0 -> (
      match (insta.(h0), stype) with
Léo Gourdin's avatar
Léo Gourdin committed
114
      | PLoad (PLd_rd_a (_, rd, ADimm (b, n))), Ldr _ ->
115
          if verify_load_affect reg rd b rev then
Léo Gourdin's avatar
Léo Gourdin committed
116
117
            affect_symb_mem reg insta t0 stype rev
          else h0 :: affect_symb_mem reg insta t0 stype rev
Léo Gourdin's avatar
Léo Gourdin committed
118
      | PStore (PSt_rs_a (_, rs, ADimm (b, n))), Str _ ->
Léo Gourdin's avatar
Léo Gourdin committed
119
120
121
          if verify_store_affect reg rs b rev then
            affect_symb_mem reg insta t0 stype rev
          else h0 :: affect_symb_mem reg insta t0 stype rev
Léo Gourdin's avatar
Léo Gourdin committed
122
123
124
125
126
      | _, _ ->
          failwith "affect_symb_mem: Found an inconsistent inst in pot_rep")

(* Affect a symbolic memory list of potential replacements
 * for a given read in reg *)
Léo Gourdin's avatar
Léo Gourdin committed
127
let rec read_symb_mem reg insta pot_rep stype rev =
Léo Gourdin's avatar
Léo Gourdin committed
128
129
130
131
  match pot_rep with
  | [] -> []
  | h0 :: t0 -> (
      match (insta.(h0), stype) with
Léo Gourdin's avatar
Léo Gourdin committed
132
      | PLoad (PLd_rd_a (_, rd, ADimm (b, n))), Ldr _ ->
133
134
          if verify_load_read reg rd b rev then
            read_symb_mem reg insta t0 stype rev
Léo Gourdin's avatar
Léo Gourdin committed
135
          else h0 :: read_symb_mem reg insta t0 stype rev
Léo Gourdin's avatar
Léo Gourdin committed
136
      | PStore (PSt_rs_a (_, rs, ADimm (b, n))), Str _ ->
137
          h0 :: read_symb_mem reg insta t0 stype rev
Léo Gourdin's avatar
Léo Gourdin committed
138
139
      | _, _ -> failwith "read_symb_mem: Found an inconsistent inst in pot_rep")

Léo Gourdin's avatar
Léo Gourdin committed
140
141
142
(* Update a symbolic memory list of potential replacements
 * for any addressing *)
let update_pot_rep_addressing a insta pot_rep stype rev =
Léo Gourdin's avatar
Léo Gourdin committed
143
  match a with
144
145
  | ADimm (base, _) ->
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev
Léo Gourdin's avatar
Léo Gourdin committed
146
  | ADreg (base, r) ->
Léo Gourdin's avatar
Léo Gourdin committed
147
148
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev;
      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype rev
Léo Gourdin's avatar
Léo Gourdin committed
149
  | ADlsl (base, r, _) ->
Léo Gourdin's avatar
Léo Gourdin committed
150
151
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev;
      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype rev
Léo Gourdin's avatar
Léo Gourdin committed
152
  | ADsxt (base, r, _) ->
Léo Gourdin's avatar
Léo Gourdin committed
153
154
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev;
      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype rev
Léo Gourdin's avatar
Léo Gourdin committed
155
  | ADuxt (base, r, _) ->
Léo Gourdin's avatar
Léo Gourdin committed
156
157
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev;
      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype rev
Léo Gourdin's avatar
Léo Gourdin committed
158
  | ADadr (base, _, _) ->
Léo Gourdin's avatar
Léo Gourdin committed
159
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev
Léo Gourdin's avatar
Léo Gourdin committed
160
  | ADpostincr (base, _) ->
Léo Gourdin's avatar
Léo Gourdin committed
161
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev
Léo Gourdin's avatar
Léo Gourdin committed
162
163
164

(* Update a symbolic memory list of potential replacements
 * for any basic instruction *)
Léo Gourdin's avatar
Léo Gourdin committed
165
166
167
let update_pot_rep_basic inst insta stype rev =
  let pot_rep = Hashtbl.find symb_mem stype in
  (match inst with
168
169
  | PArith i -> (
      match i with
170
171
      | PArithP (_, rd) ->
          pot_rep := affect_symb_mem rd insta !pot_rep stype rev
172
      | PArithPP (_, rd, rs) ->
Léo Gourdin's avatar
Léo Gourdin committed
173
174
          pot_rep := affect_symb_mem rd insta !pot_rep stype rev;
          pot_rep := read_symb_mem rs insta !pot_rep stype rev
175
      | PArithPPP (_, rd, rs1, rs2) ->
Léo Gourdin's avatar
Léo Gourdin committed
176
177
178
          pot_rep := affect_symb_mem rd insta !pot_rep stype rev;
          pot_rep := read_symb_mem rs1 insta !pot_rep stype rev;
          pot_rep := read_symb_mem rs2 insta !pot_rep stype rev
179
      | PArithRR0R (_, rd, rs1, rs2) ->
Léo Gourdin's avatar
Léo Gourdin committed
180
          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
181
182
          (match rs1 with
          | RR0 rs1 ->
183
184
              pot_rep :=
                read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev
185
          | _ -> ());
Léo Gourdin's avatar
Léo Gourdin committed
186
          pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype rev
187
      | PArithRR0 (_, rd, rs) -> (
Léo Gourdin's avatar
Léo Gourdin committed
188
          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
189
190
          match rs with
          | RR0 rs1 ->
191
192
              pot_rep :=
                read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev
193
194
          | _ -> ())
      | PArithARRRR0 (_, rd, rs1, rs2, rs3) -> (
Léo Gourdin's avatar
Léo Gourdin committed
195
196
197
          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
          pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev;
          pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype rev;
198
199
          match rs3 with
          | RR0 rs1 ->
200
201
              pot_rep :=
                read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev
202
203
          | _ -> ())
      | PArithComparisonPP (_, rs1, rs2) ->
Léo Gourdin's avatar
Léo Gourdin committed
204
205
          pot_rep := read_symb_mem rs1 insta !pot_rep stype rev;
          pot_rep := read_symb_mem rs2 insta !pot_rep stype rev
206
207
208
      | PArithComparisonR0R (_, rs1, rs2) ->
          (match rs1 with
          | RR0 rs1 ->
209
210
              pot_rep :=
                read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev
211
          | _ -> ());
Léo Gourdin's avatar
Léo Gourdin committed
212
          pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype rev
213
      | PArithComparisonP (_, rs1) ->
Léo Gourdin's avatar
Léo Gourdin committed
214
          pot_rep := read_symb_mem rs1 insta !pot_rep stype rev
215
      | Pcset (rd, _) ->
Léo Gourdin's avatar
Léo Gourdin committed
216
          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev
Léo Gourdin's avatar
Léo Gourdin committed
217
      | Pfmovi (_, rd, rs) -> (
Léo Gourdin's avatar
Léo Gourdin committed
218
          pot_rep := affect_symb_mem (dreg_of_freg rd) insta !pot_rep stype rev;
219
          match rs with
Léo Gourdin's avatar
Léo Gourdin committed
220
          | RR0 rs ->
221
222
              pot_rep :=
                read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype rev
223
224
          | _ -> ())
      | Pcsel (rd, rs1, rs2, _) ->
Léo Gourdin's avatar
Léo Gourdin committed
225
226
227
          pot_rep := affect_symb_mem rd insta !pot_rep stype rev;
          pot_rep := read_symb_mem rs1 insta !pot_rep stype rev;
          pot_rep := read_symb_mem rs2 insta !pot_rep stype rev
Léo Gourdin's avatar
Léo Gourdin committed
228
      | Pfnmul (_, rd, rs1, rs2) ->
Léo Gourdin's avatar
Léo Gourdin committed
229
230
231
          pot_rep := affect_symb_mem (dreg_of_freg rd) insta !pot_rep stype rev;
          pot_rep := read_symb_mem (dreg_of_freg rs1) insta !pot_rep stype rev;
          pot_rep := read_symb_mem (dreg_of_freg rs2) insta !pot_rep stype rev)
232
  | PLoad i -> (
233
234
      (* Here, we consider a different behavior for load and store potential candidates:
         * a load does not obviously cancel the ldp candidates, but it does for any stp candidate. *)
Léo Gourdin's avatar
Léo Gourdin committed
235
      match stype with
Léo Gourdin's avatar
Léo Gourdin committed
236
      | Ldr _ -> (
Léo Gourdin's avatar
Léo Gourdin committed
237
238
          match i with
          | PLd_rd_a (_, rd, a) ->
Léo Gourdin's avatar
Léo Gourdin committed
239
240
              pot_rep := affect_symb_mem rd insta !pot_rep stype rev;
              update_pot_rep_addressing a insta pot_rep stype rev
241
          | Pldp (_, rd1, rd2, _, _, a) ->
Léo Gourdin's avatar
Léo Gourdin committed
242
243
              pot_rep := affect_symb_mem rd1 insta !pot_rep stype rev;
              pot_rep := affect_symb_mem rd2 insta !pot_rep stype rev;
Léo Gourdin's avatar
Léo Gourdin committed
244
              update_pot_rep_addressing a insta pot_rep stype rev)
Léo Gourdin's avatar
Léo Gourdin committed
245
      | _ -> pot_rep := [])
246
247
248
249
  | PStore _ -> (
      (* Here, we consider that a store cancel all ldp candidates, but it is far more complicated for stp ones :
         * if we cancel stp candidates here, we would prevent ourselves to apply the non-consec store peephole.
         * To solve this issue, the store candidates cleaning is managed directly in the peephole function below. *)
Léo Gourdin's avatar
Léo Gourdin committed
250
      match stype with Ldr _ -> pot_rep := [] | _ -> ())
Léo Gourdin's avatar
Léo Gourdin committed
251
252
253
  | Pallocframe (_, _) -> pot_rep := []
  | Pfreeframe (_, _) -> pot_rep := []
  | Ploadsymbol (rd, _) ->
Léo Gourdin's avatar
Léo Gourdin committed
254
      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev
Léo Gourdin's avatar
Léo Gourdin committed
255
  | Pcvtsw2x (rd, rs) ->
Léo Gourdin's avatar
Léo Gourdin committed
256
257
      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
      pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype rev
Léo Gourdin's avatar
Léo Gourdin committed
258
  | Pcvtuw2x (rd, rs) ->
Léo Gourdin's avatar
Léo Gourdin committed
259
260
      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
      pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype rev
Léo Gourdin's avatar
Léo Gourdin committed
261
  | Pcvtx2w rd ->
Léo Gourdin's avatar
Léo Gourdin committed
262
263
      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
      pot_rep := read_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev
Léo Gourdin's avatar
Léo Gourdin committed
264
265
  | Pnop -> ());
  Hashtbl.replace symb_mem stype pot_rep
266

Léo Gourdin's avatar
Léo Gourdin committed
267
268
269
270
271
272
(* This is useful to manage the case were the immofs
 * of the first ldr/str is greater than the second one *)
let min_is_rev n1 n2 =
  let z1 = to_int (camlint64_of_coqint n1) in
  let z2 = to_int (camlint64_of_coqint n2) in
  if z1 < z2 then true else false
273

274
275
(* Below functions were added to merge pattern matching cases in peephole,
 * thanks to this, we can make the chunk difference (int/any) compatible. *)
276
277
278
279
let trans_ldi (ldi : load_rd_a) : load_rd1_rd2_a =
  match ldi with
  | Pldrw | Pldrw_a -> Pldpw
  | Pldrx | Pldrx_a -> Pldpx
Léo Gourdin's avatar
Léo Gourdin committed
280
281
  | Pldrs -> Pldps
  | Pldrd | Pldrd_a -> Pldpd
282
283
284
285
286
287
  | _ -> failwith "trans_ldi: Found a non compatible load to translate"

let trans_sti (sti : store_rs_a) : store_rs1_rs2_a =
  match sti with
  | Pstrw | Pstrw_a -> Pstpw
  | Pstrx | Pstrx_a -> Pstpx
Léo Gourdin's avatar
Léo Gourdin committed
288
289
  | Pstrs -> Pstps
  | Pstrd | Pstrd_a -> Pstpd
290
291
292
  | _ -> failwith "trans_sti: Found a non compatible store to translate"

let is_compat_load (ldi : load_rd_a) =
Léo Gourdin's avatar
Léo Gourdin committed
293
294
295
  match ldi with
  | Pldrw | Pldrw_a | Pldrx | Pldrx_a | Pldrs | Pldrd | Pldrd_a -> true
  | _ -> false
296
297
298
299
300

let are_compat_load (ldi1 : load_rd_a) (ldi2 : load_rd_a) =
  match ldi1 with
  | Pldrw | Pldrw_a -> ( match ldi2 with Pldrw | Pldrw_a -> true | _ -> false)
  | Pldrx | Pldrx_a -> ( match ldi2 with Pldrx | Pldrx_a -> true | _ -> false)
Léo Gourdin's avatar
Léo Gourdin committed
301
  | Pldrs -> ( match ldi2 with Pldrs -> true | _ -> false)
Léo Gourdin's avatar
Léo Gourdin committed
302
  | Pldrd | Pldrd_a -> ( match ldi2 with Pldrd | Pldrd_a -> true | _ -> false)
303
304
305
  | _ -> false

let is_compat_store (sti : store_rs_a) =
Léo Gourdin's avatar
Léo Gourdin committed
306
307
308
  match sti with
  | Pstrw | Pstrw_a | Pstrx | Pstrx_a | Pstrs | Pstrd | Pstrd_a -> true
  | _ -> false
309
310
311
312
313

let are_compat_store (sti1 : store_rs_a) (sti2 : store_rs_a) =
  match sti1 with
  | Pstrw | Pstrw_a -> ( match sti2 with Pstrw | Pstrw_a -> true | _ -> false)
  | Pstrx | Pstrx_a -> ( match sti2 with Pstrx | Pstrx_a -> true | _ -> false)
Léo Gourdin's avatar
Léo Gourdin committed
314
  | Pstrs -> ( match sti2 with Pstrs -> true | _ -> false)
Léo Gourdin's avatar
Léo Gourdin committed
315
  | Pstrd | Pstrd_a -> ( match sti2 with Pstrd | Pstrd_a -> true | _ -> false)
316
317
  | _ -> false

Léo Gourdin's avatar
Léo Gourdin committed
318
let get_load_pht (ldi : load_rd_a) =
319
  match ldi with
Léo Gourdin's avatar
Léo Gourdin committed
320
321
322
323
  | Pldrw | Pldrw_a -> Ldr P32
  | Pldrs -> Ldr P32f
  | Pldrx | Pldrx_a -> Ldr P64
  | Pldrd | Pldrd_a -> Ldr P64f
324
325
  | _ -> failwith "get_load_string: Found a non compatible load to translate"

Léo Gourdin's avatar
Léo Gourdin committed
326
let get_store_pht (sti : store_rs_a) =
327
  match sti with
Léo Gourdin's avatar
Léo Gourdin committed
328
329
330
331
  | Pstrw | Pstrw_a -> Str P32
  | Pstrs -> Str P32f
  | Pstrx | Pstrx_a -> Str P64
  | Pstrd | Pstrd_a -> Str P64f
332
333
334
335
  | _ -> failwith "get_store_string: Found a non compatible store to translate"

let is_valid_ldr rd1 rd2 b1 b2 n1 n2 stype =
  match stype with
Léo Gourdin's avatar
Léo Gourdin committed
336
  | Ldr P32 | Ldr P32f -> is_valid_ldr32 rd1 rd2 b1 b2 n1 n2
Léo Gourdin's avatar
Léo Gourdin committed
337
  | _ -> is_valid_ldr64 rd1 rd2 b1 b2 n1 n2
338
339
340

let is_valid_str b1 b2 n1 n2 stype =
  match stype with
Léo Gourdin's avatar
Léo Gourdin committed
341
  | Str P32 | Str P32f -> is_valid_str32 b1 b2 n1 n2
Léo Gourdin's avatar
Léo Gourdin committed
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
  | _ -> is_valid_str64 b1 b2 n1 n2

(* Try to find the index of the first previous compatible
 * replacement in a given symbolic memory *)
let rec search_compat_rep r2 b2 n2 insta pot_rep stype =
  match pot_rep with
  | [] -> None
  | h0 :: t0 -> (
      match insta.(h0) with
      | PLoad (PLd_rd_a (ld1, rd1, ADimm (b1, n1))) ->
          if is_valid_ldr rd1 r2 b1 b2 n1 n2 stype then
            Some (h0, chunk_load ld1, rd1, b1, n1)
          else search_compat_rep r2 b2 n2 insta t0 stype
      | PStore (PSt_rs_a (st1, rs1, ADimm (b1, n1))) ->
          if is_valid_str b1 b2 n1 n2 stype then
            Some (h0, chunk_store st1, rs1, b1, n1)
          else search_compat_rep r2 b2 n2 insta t0 stype
Léo Gourdin's avatar
Léo Gourdin committed
359
360
      | _ -> failwith "search_compat_rep: Found an inconsistent inst in pot_rep"
      )
Léo Gourdin's avatar
Léo Gourdin committed
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378

(* Try to find the index of the first previous compatible
 * replacement in a given symbolic memory (when iterating in the reversed list) *)
let rec search_compat_rep_inv r2 b2 n2 insta pot_rep stype =
  match pot_rep with
  | [] -> None
  | h0 :: t0 -> (
      match insta.(h0) with
      | PLoad (PLd_rd_a (ld1, rd1, ADimm (b1, n1))) ->
          if is_valid_ldr r2 rd1 b2 b1 n2 n1 stype then
            Some (h0, chunk_load ld1, rd1, b1, n1)
          else search_compat_rep_inv r2 b2 n2 insta t0 stype
      | PStore (PSt_rs_a (st1, rs1, ADimm (b1, n1))) ->
          if is_valid_str b2 b1 n2 n1 stype then
            Some (h0, chunk_store st1, rs1, b1, n1)
          else search_compat_rep_inv r2 b2 n2 insta t0 stype
      | _ ->
          failwith
Léo Gourdin's avatar
Léo Gourdin committed
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
            "search_compat_rep_ldst_inv: Found an inconsistent inst in pot_rep")

let init_symb_mem () =
  Hashtbl.clear symb_mem;
  Hashtbl.add symb_mem (Ldr P32) (ref []);
  Hashtbl.add symb_mem (Ldr P64) (ref []);
  Hashtbl.add symb_mem (Ldr P32f) (ref []);
  Hashtbl.add symb_mem (Ldr P64f) (ref []);
  Hashtbl.add symb_mem (Str P32) (ref []);
  Hashtbl.add symb_mem (Str P64) (ref []);
  Hashtbl.add symb_mem (Str P32f) (ref []);
  Hashtbl.add symb_mem (Str P64f) (ref [])

let reset_str_symb_mem () =
  Hashtbl.replace symb_mem (Str P32) (ref []);
  Hashtbl.replace symb_mem (Str P64) (ref []);
  Hashtbl.replace symb_mem (Str P32f) (ref []);
  Hashtbl.replace symb_mem (Str P64f) (ref [])
397

Léo Gourdin's avatar
Léo Gourdin committed
398
399
400
401
402
(* Main peephole function in backward style *)
let pair_rep_inv insta =
  (* Each list below is a symbolic mem representation
   * for one type of inst. Lists contains integers which
   * are the indices of insts in the main array "insta". *)
Léo Gourdin's avatar
Léo Gourdin committed
403
  init_symb_mem ();
404
  for i = Array.length insta - 1 downto 0 do
Léo Gourdin's avatar
Léo Gourdin committed
405
406
    let h0 = insta.(i) in
    (* Here we need to update every symbolic memory according to the matched inst *)
Léo Gourdin's avatar
Léo Gourdin committed
407
408
409
410
411
412
413
414
    update_pot_rep_basic h0 insta (Ldr P32) true;
    update_pot_rep_basic h0 insta (Ldr P64) true;
    update_pot_rep_basic h0 insta (Ldr P32f) true;
    update_pot_rep_basic h0 insta (Ldr P64f) true;
    update_pot_rep_basic h0 insta (Str P32) true;
    update_pot_rep_basic h0 insta (Str P64) true;
    update_pot_rep_basic h0 insta (Str P32f) true;
    update_pot_rep_basic h0 insta (Str P64f) true;
415
    match h0 with
416
    (* Non-consecutive ldr *)
417
    | PLoad (PLd_rd_a (ldi, rd1, ADimm (b1, n1))) ->
Léo Gourdin's avatar
Léo Gourdin committed
418
        if is_compat_load ldi then (
419
          (* Search a previous compatible load *)
Léo Gourdin's avatar
Léo Gourdin committed
420
          let ld_t = get_load_pht ldi in
Léo Gourdin's avatar
Léo Gourdin committed
421
422
          let pot_rep = Hashtbl.find symb_mem ld_t in
          (match search_compat_rep_inv rd1 b1 n1 insta !pot_rep ld_t with
423
424
425
426
427
428
429
430
431
          (* If we can't find a candidate, add the current load as a potential future one *)
          | None -> pot_rep := i :: !pot_rep
          (* Else, perform the peephole *)
          | Some (rep, c, r, b, n) ->
              (* The two lines below are used to filter the elected candidate *)
              let filt x = x != rep in
              pot_rep := List.filter filt !pot_rep;
              insta.(rep) <- Pnop;
              if min_is_rev n n1 then (
Léo Gourdin's avatar
Léo Gourdin committed
432
433
                if debug then
                  eprintf "LDP_BACK_SPACED_PEEP_IMM_INC_%a\n" print_ph_ty ld_t;
434
435
436
437
438
                insta.(i) <-
                  PLoad
                    (Pldp
                       (trans_ldi ldi, r, rd1, c, chunk_load ldi, ADimm (b, n))))
              else (
Léo Gourdin's avatar
Léo Gourdin committed
439
440
                if debug then
                  eprintf "LDP_BACK_SPACED_PEEP_IMM_DEC_%a\n" print_ph_ty ld_t;
441
442
443
                insta.(i) <-
                  PLoad
                    (Pldp
Léo Gourdin's avatar
Léo Gourdin committed
444
445
                       (trans_ldi ldi, rd1, r, chunk_load ldi, c, ADimm (b, n1)))));
          Hashtbl.replace symb_mem ld_t pot_rep)
446
    (* Non-consecutive str *)
447
    | PStore (PSt_rs_a (sti, rd1, ADimm (b1, n1))) ->
Léo Gourdin's avatar
Léo Gourdin committed
448
        if is_compat_store sti then (
449
          (* Search a previous compatible store *)
Léo Gourdin's avatar
Léo Gourdin committed
450
          let st_t = get_store_pht sti in
Léo Gourdin's avatar
Léo Gourdin committed
451
452
          let pot_rep = Hashtbl.find symb_mem st_t in
          (match search_compat_rep_inv rd1 b1 n1 insta !pot_rep st_t with
453
454
          (* If we can't find a candidate, clean and add the current store as a potential future one *)
          | None ->
Léo Gourdin's avatar
Léo Gourdin committed
455
456
              reset_str_symb_mem ();
              pot_rep := [ i ]
457
458
459
460
461
462
          (* Else, perform the peephole *)
          | Some (rep, c, r, b, n) ->
              (* The two lines below are used to filter the elected candidate *)
              let filt x = x != rep in
              pot_rep := List.filter filt !pot_rep;
              insta.(rep) <- Pnop;
Léo Gourdin's avatar
Léo Gourdin committed
463
464
              if debug then
                eprintf "STP_BACK_SPACED_PEEP_IMM_INC_%a\n" print_ph_ty st_t;
465
466
              insta.(i) <-
                PStore
467
                  (Pstp
Léo Gourdin's avatar
Léo Gourdin committed
468
469
                     (trans_sti sti, rd1, r, chunk_store sti, c, ADimm (b, n1))));
          Hashtbl.replace symb_mem st_t pot_rep
470
          (* Any other inst *))
471
    | i -> (
472
        (* Clear list of candidates if there is a non supported store *)
Léo Gourdin's avatar
Léo Gourdin committed
473
        match i with PStore _ -> reset_str_symb_mem () | _ -> ())
Léo Gourdin's avatar
Léo Gourdin committed
474
475
476
  done

(* Main peephole function in forward style *)
477
let pair_rep insta =
Léo Gourdin's avatar
Léo Gourdin committed
478
479
480
  (* Each list below is a symbolic mem representation
   * for one type of inst. Lists contains integers which
   * are the indices of insts in the main array "insta". *)
Léo Gourdin's avatar
Léo Gourdin committed
481
  init_symb_mem ();
482
483
484
  for i = 0 to Array.length insta - 2 do
    let h0 = insta.(i) in
    let h1 = insta.(i + 1) in
Léo Gourdin's avatar
Léo Gourdin committed
485
    (* Here we need to update every symbolic memory according to the matched inst *)
Léo Gourdin's avatar
Léo Gourdin committed
486
487
488
489
490
491
492
493
    update_pot_rep_basic h0 insta (Ldr P32) false;
    update_pot_rep_basic h0 insta (Ldr P64) false;
    update_pot_rep_basic h0 insta (Ldr P32f) false;
    update_pot_rep_basic h0 insta (Ldr P64f) false;
    update_pot_rep_basic h0 insta (Str P32) false;
    update_pot_rep_basic h0 insta (Str P64) false;
    update_pot_rep_basic h0 insta (Str P32f) false;
    update_pot_rep_basic h0 insta (Str P64f) false;
494
    match (h0, h1) with
495
    (* Consecutive ldr *)
Léo Gourdin's avatar
Léo Gourdin committed
496
497
    | ( PLoad (PLd_rd_a (ldi1, rd1, ADimm (b1, n1))),
        PLoad (PLd_rd_a (ldi2, rd2, ADimm (b2, n2))) ) ->
498
        if are_compat_load ldi1 ldi2 then
Léo Gourdin's avatar
Léo Gourdin committed
499
500
          let ld_t = get_load_pht ldi1 in
          if is_valid_ldr rd1 rd2 b1 b2 n1 n2 ld_t then (
501
            if min_is_rev n1 n2 then (
Léo Gourdin's avatar
Léo Gourdin committed
502
503
              if debug then
                eprintf "LDP_CONSEC_PEEP_IMM_INC_%a\n" print_ph_ty ld_t;
504
505
506
507
508
509
510
511
512
              insta.(i) <-
                PLoad
                  (Pldp
                     ( trans_ldi ldi1,
                       rd1,
                       rd2,
                       chunk_load ldi1,
                       chunk_load ldi2,
                       ADimm (b1, n1) )))
Léo Gourdin's avatar
Léo Gourdin committed
513
            else (
Léo Gourdin's avatar
Léo Gourdin committed
514
515
              if debug then
                eprintf "LDP_CONSEC_PEEP_IMM_DEC_%a\n" print_ph_ty ld_t;
516
517
518
519
520
521
522
523
524
525
526
              insta.(i) <-
                PLoad
                  (Pldp
                     ( trans_ldi ldi1,
                       rd2,
                       rd1,
                       chunk_load ldi2,
                       chunk_load ldi1,
                       ADimm (b1, n2) )));
            insta.(i + 1) <- Pnop)
    (* Non-consecutive ldr *)
Léo Gourdin's avatar
Léo Gourdin committed
527
528
    | PLoad (PLd_rd_a (ldi, rd1, ADimm (b1, n1))), _ ->
        if is_compat_load ldi then (
529
          (* Search a previous compatible load *)
Léo Gourdin's avatar
Léo Gourdin committed
530
          let ld_t = get_load_pht ldi in
Léo Gourdin's avatar
Léo Gourdin committed
531
532
          let pot_rep = Hashtbl.find symb_mem ld_t in
          (match search_compat_rep rd1 b1 n1 insta !pot_rep ld_t with
533
534
535
536
537
538
539
540
541
          (* If we can't find a candidate, add the current load as a potential future one *)
          | None -> pot_rep := i :: !pot_rep
          (* Else, perform the peephole *)
          | Some (rep, c, r, b, n) ->
              (* The two lines below are used to filter the elected candidate *)
              let filt x = x != rep in
              pot_rep := List.filter filt !pot_rep;
              insta.(rep) <- Pnop;
              if min_is_rev n n1 then (
Léo Gourdin's avatar
Léo Gourdin committed
542
543
                if debug then
                  eprintf "LDP_FORW_SPACED_PEEP_IMM_INC_%a\n" print_ph_ty ld_t;
544
545
546
547
548
                insta.(i) <-
                  PLoad
                    (Pldp
                       (trans_ldi ldi, r, rd1, c, chunk_load ldi, ADimm (b, n))))
              else (
Léo Gourdin's avatar
Léo Gourdin committed
549
550
                if debug then
                  eprintf "LDP_FORW_SPACED_PEEP_IMM_DEC_%a\n" print_ph_ty ld_t;
551
552
553
                insta.(i) <-
                  PLoad
                    (Pldp
Léo Gourdin's avatar
Léo Gourdin committed
554
555
                       (trans_ldi ldi, rd1, r, chunk_load ldi, c, ADimm (b, n1)))));
          Hashtbl.replace symb_mem ld_t pot_rep)
556
    (* Consecutive str *)
Léo Gourdin's avatar
Léo Gourdin committed
557
558
    | ( PStore (PSt_rs_a (sti1, rd1, ADimm (b1, n1))),
        PStore (PSt_rs_a (sti2, rd2, ADimm (b2, n2))) ) ->
559
560
561
        (* Regardless of whether we can perform the peephole or not,
         * we have to clean the potential candidates for stp now as we are
         * looking at two new store instructions. *)
Léo Gourdin's avatar
Léo Gourdin committed
562
        reset_str_symb_mem ();
563
        if are_compat_store sti1 sti2 then
Léo Gourdin's avatar
Léo Gourdin committed
564
565
          let st_t = get_store_pht sti1 in
          if is_valid_str b1 b2 n1 n2 st_t then (
Léo Gourdin's avatar
Léo Gourdin committed
566
567
            if debug then
              eprintf "STP_CONSEC_PEEP_IMM_INC_%a\n" print_ph_ty st_t;
568
569
570
571
572
573
574
575
576
577
578
            insta.(i) <-
              PStore
                (Pstp
                   ( trans_sti sti1,
                     rd1,
                     rd2,
                     chunk_store sti1,
                     chunk_store sti2,
                     ADimm (b1, n1) ));
            insta.(i + 1) <- Pnop)
    (* Non-consecutive str *)
Léo Gourdin's avatar
Léo Gourdin committed
579
580
    | PStore (PSt_rs_a (sti, rd1, ADimm (b1, n1))), _ ->
        if is_compat_store sti then (
581
          (* Search a previous compatible store *)
Léo Gourdin's avatar
Léo Gourdin committed
582
          let st_t = get_store_pht sti in
Léo Gourdin's avatar
Léo Gourdin committed
583
584
          let pot_rep = Hashtbl.find symb_mem st_t in
          (match search_compat_rep rd1 b1 n1 insta !pot_rep st_t with
585
586
          (* If we can't find a candidate, clean and add the current store as a potential future one *)
          | None ->
Léo Gourdin's avatar
Léo Gourdin committed
587
588
              reset_str_symb_mem ();
              pot_rep := [ i ]
589
590
591
592
593
594
          (* Else, perform the peephole *)
          | Some (rep, c, r, b, n) ->
              (* The two lines below are used to filter the elected candidate *)
              let filt x = x != rep in
              pot_rep := List.filter filt !pot_rep;
              insta.(rep) <- Pnop;
Léo Gourdin's avatar
Léo Gourdin committed
595
596
              if debug then
                eprintf "STP_FORW_SPACED_PEEP_IMM_INC_%a\n" print_ph_ty st_t;
597
598
              insta.(i) <-
                PStore
Léo Gourdin's avatar
Léo Gourdin committed
599
600
                  (Pstp (trans_sti sti, r, rd1, c, chunk_store sti, ADimm (b, n))));
          Hashtbl.replace symb_mem st_t pot_rep)
Léo Gourdin's avatar
Léo Gourdin committed
601
    (* Any other inst *)
602
603
    | i, _ -> (
        (* Clear list of candidates if there is a non supported store *)
Léo Gourdin's avatar
Léo Gourdin committed
604
        match i with PStore _ -> reset_str_symb_mem () | _ -> ())
605
606
  done

Léo Gourdin's avatar
Léo Gourdin committed
607
(* Calling peephole if flag is set *)
608
let optimize_bdy (bdy : basic list) : basic list =
Léo Gourdin's avatar
Léo Gourdin committed
609
  if !Clflags.option_fcoalesce_mem then (
610
    let insta = Array.of_list bdy in
Léo Gourdin's avatar
Léo Gourdin committed
611
    pair_rep insta;
Léo Gourdin's avatar
Léo Gourdin committed
612
    pair_rep_inv insta;
Léo Gourdin's avatar
Léo Gourdin committed
613
    Array.to_list insta)
614
615
  else bdy

Léo Gourdin's avatar
Léo Gourdin committed
616
(* Called peephole function from Coq *)
617
618
619
620
621
622
let peephole_opt bdy =
  Timing.time_coq
    [
      'P'; 'e'; 'e'; 'p'; 'h'; 'o'; 'l'; 'e'; ' '; 'o'; 'r'; 'a'; 'c'; 'l'; 'e';
    ]
    optimize_bdy bdy