Commit aa66e021 authored by Léo Gourdin's avatar Léo Gourdin
Browse files

Non conseq loads in peephole

parent 0c5bf1fd
......@@ -18,20 +18,22 @@ open Printf
let debug = true
(* Functions to verify the immediate offset range for ldp/stp *)
let is_valid_immofs_32 z =
if z <= 252 && z >= -256 && z mod 4 == 0 then true else false
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
if z <= 504 && z >= -512 && z mod 8 = 0 then true else false
(* Functions to check if a ldp/stp replacement is valid according to args *)
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
&& (not (iregsp_eq (RR1 rd1) b2))
&& ((z2 = z1 + 4) || (z2 = z1 - 4))
&& is_valid_immofs_32 z1
then true
else false
......@@ -42,8 +44,8 @@ let is_valid_ldrx rd1 rd2 b1 b2 n1 n2 =
if
(not (ireg_eq rd1 rd2))
&& iregsp_eq b1 b2
&& (not (iregsp_eq (RR1 rd1) b1))
&& z2 == z1 + 8
&& (not (iregsp_eq (RR1 rd1) b2))
&& ((z2 = z1 + 8) || (z2 = z1 - 8))
&& is_valid_immofs_64 z1
then true
else false
......@@ -51,118 +53,187 @@ let is_valid_ldrx rd1 rd2 b1 b2 n1 n2 =
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
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
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 =
(* 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 =
match inst with
| PArith i -> (
match i with
| PArithP (_, rd) -> pot_rep := affect_symb_mem rd !pot_rep stype
| PArithP (_, rd) -> pot_rep := affect_symb_mem rd insta !pot_rep stype
| PArithPP (_, rd, rs) ->
pot_rep := affect_symb_mem rd !pot_rep stype;
pot_rep := read_symb_mem rs !pot_rep stype
pot_rep := affect_symb_mem rd insta !pot_rep stype;
pot_rep := read_symb_mem rs insta !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
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
| PArithRR0R (_, rd, rs1, rs2) ->
pot_rep := affect_symb_mem (dreg_of_ireg rd) !pot_rep stype;
pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !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 rs1) insta !pot_rep stype
| _ -> ());
pot_rep := read_symb_mem (dreg_of_ireg rs2) !pot_rep stype
pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype
| PArithRR0 (_, rd, rs) -> (
pot_rep := affect_symb_mem (dreg_of_ireg rd) !pot_rep stype;
pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype;
match rs with
| RR0 rs1 ->
pot_rep := read_symb_mem (dreg_of_ireg rs1) !pot_rep stype
pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !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;
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;
match rs3 with
| RR0 rs1 ->
pot_rep := read_symb_mem (dreg_of_ireg rs1) !pot_rep stype
pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype
| _ -> ())
| PArithComparisonPP (_, rs1, rs2) ->
pot_rep := read_symb_mem rs1 !pot_rep stype;
pot_rep := read_symb_mem rs2 !pot_rep stype
pot_rep := read_symb_mem rs1 insta !pot_rep stype;
pot_rep := read_symb_mem rs2 insta !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 rs1) insta !pot_rep stype
| _ -> ());
pot_rep := read_symb_mem (dreg_of_ireg rs2) !pot_rep stype
pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype
| PArithComparisonP (_, rs1) ->
pot_rep := read_symb_mem rs1 !pot_rep stype
pot_rep := read_symb_mem rs1 insta !pot_rep stype
| Pcset (rd, _) ->
pot_rep := affect_symb_mem (dreg_of_ireg rd) !pot_rep stype
pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype
| Pfmovi (_, _, rs) -> (
match rs with
| RR0 rs -> pot_rep := read_symb_mem (dreg_of_ireg rs) !pot_rep stype
| RR0 rs ->
pot_rep := read_symb_mem (dreg_of_ireg rs) insta !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
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
| 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)
| 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)
| PStore _ -> pot_rep := []
(* TODO *)
| _ -> ()
| 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 -> ()
(*let update_symb_mem inst = update_pot_rep inst pot_ldrw_rep "ldrw"*)
(* 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")
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
(* 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
(* Main peephole function *)
let pair_rep 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". *)
let pot_ldrw_rep = ref [] in
let pot_ldrx_rep = ref [] in
for i = 0 to Array.length insta - 2 do
let h0 = insta.(i) in
let h1 = insta.(i + 1) in
match (h0, h1) with
(* Consecutive ldrw *)
| ( 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. *)
......@@ -172,8 +243,12 @@ let pair_rep insta =
(* 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)));
(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))));
insta.(i + 1) <- Pnop)
(* Consecutive ldrx *)
| ( 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 (
......@@ -181,13 +256,42 @@ let pair_rep insta =
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) -> *))
(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 *)
| ( 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. *)
......@@ -199,6 +303,7 @@ let pair_rep insta =
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. *))
(* Consecutive strx *)
| ( 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
......@@ -208,17 +313,22 @@ let pair_rep insta =
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*)
(* 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"
done
(* Calling peephole if flag is set *)
let optimize_bdy (bdy : basic list) : basic list =
if !Clflags.option_fcoalesce_mem then
if !Clflags.option_fcoalesce_mem then (
let insta = Array.of_list bdy in
(pair_rep insta; Array.to_list insta)
pair_rep insta;
Array.to_list insta)
else bdy
(** Called peephole function from Coq *)
(* Called peephole function from Coq *)
let peephole_opt bdy =
Timing.time_coq
[
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment