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

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

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

Léo Gourdin's avatar
Léo Gourdin committed
28
(* Functions to check if a ldp/stp replacement is valid according to args *)
29
30
31
32
33
34
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
Léo Gourdin's avatar
Léo Gourdin committed
35
36
    && (not (iregsp_eq (RR1 rd1) b2))
    && ((z2 = z1 + 4) || (z2 = z1 - 4))
37
38
39
40
41
42
43
44
45
46
    && 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
Léo Gourdin's avatar
Léo Gourdin committed
47
48
    && (not (iregsp_eq (RR1 rd1) b2))
    && ((z2 = z1 + 8) || (z2 = z1 - 8))
49
50
51
52
53
54
55
    && 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
Léo Gourdin's avatar
Léo Gourdin committed
56
  if iregsp_eq b1 b2 && z2 = z1 + 4 && is_valid_immofs_32 z1 then true
57
58
59
60
61
  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
Léo Gourdin's avatar
Léo Gourdin committed
62
  if iregsp_eq b1 b2 && z2 = z1 + 8 && is_valid_immofs_64 z1 then true
63
64
65
66
  else false

let dreg_of_ireg r = IR (RR1 r)

Léo Gourdin's avatar
Léo Gourdin committed
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
(* Affect a symbolic memory list of potential replacements
 * for a given write in reg *)
let rec affect_symb_mem reg insta pot_rep stype =
  match pot_rep with
  | [] -> []
  | h0 :: t0 -> (
      match (insta.(h0), stype) with
      | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd), ADimm (b, n))), "ldrw" ->
          if dreg_eq reg (IR b) then affect_symb_mem reg insta t0 stype
          else h0 :: affect_symb_mem reg insta t0 stype
      | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd), ADimm (b, n))), "ldrx" ->
          if dreg_eq reg (IR b) then affect_symb_mem reg insta t0 stype
          else h0 :: affect_symb_mem reg insta t0 stype
      | _, _ ->
          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 *)
let rec read_symb_mem reg insta pot_rep stype =
  match pot_rep with
  | [] -> []
  | h0 :: t0 -> (
      match (insta.(h0), stype) with
      | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd), ADimm (b, n))), "ldrw" ->
          if dreg_eq reg (IR (RR1 rd)) then read_symb_mem reg insta t0 stype
          else h0 :: read_symb_mem reg insta t0 stype
      | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd), ADimm (b, n))), "ldrx" ->
          if dreg_eq reg (IR (RR1 rd)) then read_symb_mem reg insta t0 stype
          else h0 :: read_symb_mem reg insta t0 stype
      | _, _ -> failwith "read_symb_mem: Found an inconsistent inst in pot_rep")

let update_pot_rep_addressing a insta pot_rep stype =
  match a with
  | ADimm (base, _) ->
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype
  | ADreg (base, r) ->
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype;
      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype
  | ADlsl (base, r, _) ->
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype;
      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype
  | ADsxt (base, r, _) ->
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype;
      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype
  | ADuxt (base, r, _) ->
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype;
      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype
  | ADadr (base, _, _) ->
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype
  | ADpostincr (base, _) ->
      pot_rep := read_symb_mem (IR base) insta !pot_rep stype

(* Update a symbolic memory list of potential replacements
 * for any basic instruction *)
let update_pot_rep_basic inst insta pot_rep stype =
122
123
124
  match inst with
  | PArith i -> (
      match i with
Léo Gourdin's avatar
Léo Gourdin committed
125
      | PArithP (_, rd) -> pot_rep := affect_symb_mem rd insta !pot_rep stype
126
      | PArithPP (_, rd, rs) ->
Léo Gourdin's avatar
Léo Gourdin committed
127
128
          pot_rep := affect_symb_mem rd insta !pot_rep stype;
          pot_rep := read_symb_mem rs insta !pot_rep stype
129
      | PArithPPP (_, rd, rs1, rs2) ->
Léo Gourdin's avatar
Léo Gourdin committed
130
131
132
          pot_rep := affect_symb_mem rd insta !pot_rep stype;
          pot_rep := read_symb_mem rs1 insta !pot_rep stype;
          pot_rep := read_symb_mem rs2 insta !pot_rep stype
133
      | PArithRR0R (_, rd, rs1, rs2) ->
Léo Gourdin's avatar
Léo Gourdin committed
134
          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype;
135
136
          (match rs1 with
          | RR0 rs1 ->
Léo Gourdin's avatar
Léo Gourdin committed
137
              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype
138
          | _ -> ());
Léo Gourdin's avatar
Léo Gourdin committed
139
          pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype
140
      | PArithRR0 (_, rd, rs) -> (
Léo Gourdin's avatar
Léo Gourdin committed
141
          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype;
142
143
          match rs with
          | RR0 rs1 ->
Léo Gourdin's avatar
Léo Gourdin committed
144
              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype
145
146
          | _ -> ())
      | PArithARRRR0 (_, rd, rs1, rs2, rs3) -> (
Léo Gourdin's avatar
Léo Gourdin committed
147
148
149
          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype;
          pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype;
          pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype;
150
151
          match rs3 with
          | RR0 rs1 ->
Léo Gourdin's avatar
Léo Gourdin committed
152
              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype
153
154
          | _ -> ())
      | PArithComparisonPP (_, rs1, rs2) ->
Léo Gourdin's avatar
Léo Gourdin committed
155
156
          pot_rep := read_symb_mem rs1 insta !pot_rep stype;
          pot_rep := read_symb_mem rs2 insta !pot_rep stype
157
158
159
      | PArithComparisonR0R (_, rs1, rs2) ->
          (match rs1 with
          | RR0 rs1 ->
Léo Gourdin's avatar
Léo Gourdin committed
160
              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype
161
          | _ -> ());
Léo Gourdin's avatar
Léo Gourdin committed
162
          pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype
163
      | PArithComparisonP (_, rs1) ->
Léo Gourdin's avatar
Léo Gourdin committed
164
          pot_rep := read_symb_mem rs1 insta !pot_rep stype
165
      | Pcset (rd, _) ->
Léo Gourdin's avatar
Léo Gourdin committed
166
          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype
167
168
      | Pfmovi (_, _, rs) -> (
          match rs with
Léo Gourdin's avatar
Léo Gourdin committed
169
170
          | RR0 rs ->
              pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype
171
172
          | _ -> ())
      | Pcsel (rd, rs1, rs2, _) ->
Léo Gourdin's avatar
Léo Gourdin committed
173
174
175
          pot_rep := affect_symb_mem rd insta !pot_rep stype;
          pot_rep := read_symb_mem rs1 insta !pot_rep stype;
          pot_rep := read_symb_mem rs2 insta !pot_rep stype
176
177
178
      | Pfnmul (_, rd, rs1, rs2) -> ())
  | PLoad i -> (
      match i with
Léo Gourdin's avatar
Léo Gourdin committed
179
180
181
182
183
184
185
      | PLd_rd_a (_, rd, a) ->
          pot_rep := affect_symb_mem rd insta !pot_rep stype;
          update_pot_rep_addressing a insta pot_rep stype
      | Pldp (_, rd1, rd2, a) ->
          pot_rep := affect_symb_mem (dreg_of_ireg rd1) insta !pot_rep stype;
          pot_rep := affect_symb_mem (dreg_of_ireg rd2) insta !pot_rep stype;
          update_pot_rep_addressing a insta pot_rep stype)
186
  | PStore _ -> pot_rep := []
Léo Gourdin's avatar
Léo Gourdin committed
187
188
189
190
191
192
193
194
195
196
197
198
199
200
  | Pallocframe (_, _) -> pot_rep := []
  | Pfreeframe (_, _) -> pot_rep := []
  | Ploadsymbol (rd, _) ->
      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype
  | Pcvtsw2x (rd, rs) ->
      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype;
      pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype
  | Pcvtuw2x (rd, rs) ->
      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype;
      pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype
  | Pcvtx2w rd ->
      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype;
      pot_rep := read_symb_mem (dreg_of_ireg rd) insta !pot_rep stype
  | Pnop -> ()
201

Léo Gourdin's avatar
Léo Gourdin committed
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
(* Try to find the index of the first previous compatible
 * replacement in a given symbolic memory *)
let rec search_compat_rep rd2 b2 n2 insta pot_rep stype =
  match pot_rep with
  | [] -> None
  | h0 :: t0 -> (
      match (insta.(h0), stype) with
      | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))), "ldrw" ->
          if is_valid_ldrw rd1 rd2 b1 b2 n1 n2 then Some (h0, rd1, b1, n1)
          else search_compat_rep rd2 b2 n2 insta t0 stype
      | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd1), ADimm (b1, n1))), "ldrx" ->
          if is_valid_ldrx rd1 rd2 b1 b2 n1 n2 then Some (h0, rd1, b1, n1)
          else search_compat_rep rd2 b2 n2 insta t0 stype
      | _, _ ->
          failwith "search_compat_rep: Found an inconsistent inst in pot_rep")
217

Léo Gourdin's avatar
Léo Gourdin committed
218
219
220
221
222
223
(* 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
224

Léo Gourdin's avatar
Léo Gourdin committed
225
(* Main peephole function *)
226
let pair_rep insta =
Léo Gourdin's avatar
Léo Gourdin committed
227
228
229
230
231
  (* 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". *)
  let pot_ldrw_rep = ref [] in
  let pot_ldrx_rep = ref [] in
232
233
234
235
  for i = 0 to Array.length insta - 2 do
    let h0 = insta.(i) in
    let h1 = insta.(i + 1) in
    match (h0, h1) with
Léo Gourdin's avatar
Léo Gourdin committed
236
    (* Consecutive ldrw *)
237
238
239
240
241
242
243
244
245
    | ( 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";
Léo Gourdin's avatar
Léo Gourdin committed
246
247
248
249
          (if min_is_rev n1 n2 then
            insta.(i) <- PLoad (Pldp (Pldpw, rd1, rd2, ADimm (b1, n1)))
          else
            insta.(i) <- PLoad (Pldp (Pldpw, rd2, rd1, ADimm (b1, n2))));
250
          insta.(i + 1) <- Pnop)
Léo Gourdin's avatar
Léo Gourdin committed
251
    (* Consecutive ldrx *)
252
253
254
255
256
257
258
    | ( 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";
Léo Gourdin's avatar
Léo Gourdin committed
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
          (if min_is_rev n1 n2 then
            insta.(i) <- PLoad (Pldp (Pldpx, rd1, rd2, ADimm (b1, n1)))
          else
            insta.(i) <- PLoad (Pldp (Pldpx, rd2, rd1, ADimm (b1, n2))));
          insta.(i + 1) <- Pnop)
    (* Non-consecutive ldrw *)
    | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))), _ -> (
        (* Search a previous compatible load *)
        match search_compat_rep rd1 b1 n1 insta !pot_ldrw_rep "ldrw" with
        (* If we can't find a candidate, add the current load as a potential future one *)
        | None -> pot_ldrw_rep := i :: !pot_ldrw_rep
        (* Else, perform the peephole *)
        | Some (rep, r, b, n) ->
            eprintf "LDP_WCPEEP\n";
            (* The two lines below are used to filter the elected candidate *)
            let filt x = x != rep in
            pot_ldrw_rep := List.filter filt !pot_ldrw_rep;
            insta.(rep) <- Pnop;
            (if min_is_rev n n1 then
              insta.(i) <- PLoad (Pldp (Pldpw, r, rd1, ADimm (b, n)))
            else
              insta.(i) <- PLoad (Pldp (Pldpw, rd1, r, ADimm (b, n1)))))
    (* Non-consecutive ldrx *)
    | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd1), ADimm (b1, n1))), _ -> (
        match search_compat_rep rd1 b1 n1 insta !pot_ldrx_rep "ldrx" with
        | None -> pot_ldrx_rep := i :: !pot_ldrx_rep
        | Some (rep, r, b, n) ->
            eprintf "LDP_XCPEEP\n";
            let filt x = x != rep in
            pot_ldrx_rep := List.filter filt !pot_ldrx_rep;
            insta.(rep) <- Pnop;
            (if min_is_rev n n1 then
              insta.(i) <- PLoad (Pldp (Pldpx, r, rd1, ADimm (b, n)))
            else
              insta.(i) <- PLoad (Pldp (Pldpx, rd1, r, ADimm (b, n1)))))
    (* Consecutive strw *)
295
296
297
298
299
300
301
302
303
304
305
    | ( 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. *))
Léo Gourdin's avatar
Léo Gourdin committed
306
    (* Consecutive strx *)
307
308
309
310
311
312
313
314
315
    | ( 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)
Léo Gourdin's avatar
Léo Gourdin committed
316
317
318
319
320
    (* Any other inst *)
    | h0, _ ->
        (* Here we need to update every symbolic memory according to the matched inst *)
        update_pot_rep_basic h0 insta pot_ldrw_rep "ldrw";
        update_pot_rep_basic h0 insta pot_ldrx_rep "ldrx"
321
322
  done

Léo Gourdin's avatar
Léo Gourdin committed
323
(* Calling peephole if flag is set *)
324
let optimize_bdy (bdy : basic list) : basic list =
Léo Gourdin's avatar
Léo Gourdin committed
325
  if !Clflags.option_fcoalesce_mem then (
326
    let insta = Array.of_list bdy in
Léo Gourdin's avatar
Léo Gourdin committed
327
328
    pair_rep insta;
    Array.to_list insta)
329
330
  else bdy

Léo Gourdin's avatar
Léo Gourdin committed
331
(* Called peephole function from Coq *)
332
333
334
335
336
337
let peephole_opt bdy =
  Timing.time_coq
    [
      'P'; 'e'; 'e'; 'p'; 'h'; 'o'; 'l'; 'e'; ' '; 'o'; 'r'; 'a'; 'c'; 'l'; 'e';
    ]
    optimize_bdy bdy