From 9d5f379cd9e36def513357363308f1e0b0f4e082 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 10 Dec 2020 14:36:18 +0100 Subject: Peephole finished for now --- aarch64/PeepholeOracle.ml | 297 ++++++++++++++++++++++++++++++++-------------- 1 file changed, 211 insertions(+), 86 deletions(-) (limited to 'aarch64/PeepholeOracle.ml') diff --git a/aarch64/PeepholeOracle.ml b/aarch64/PeepholeOracle.ml index 8d30d803..94efc75e 100644 --- a/aarch64/PeepholeOracle.ml +++ b/aarch64/PeepholeOracle.ml @@ -16,7 +16,7 @@ open Asm open Int64 open Printf -let debug = true +let debug = false (* Functions to verify the immediate offset range for ldp/stp *) let is_valid_immofs_32 z = @@ -64,153 +64,181 @@ let is_valid_strx b1 b2 n1 n2 = let dreg_of_ireg r = IR (RR1 r) +(* Return true if an intermediate + * affectation eliminates the potential + * candidate *) +let verify_load_affect reg rd b rev = + let b = (IR b) in + let rd = dreg_of_ireg rd in + if not rev then + dreg_eq reg b + else + (dreg_eq reg b) || (dreg_eq reg rd) + +(* Return true if an intermediate + * read eliminates the potential + * candidate *) +let verify_load_read reg rd b rev = + let rd = dreg_of_ireg rd in + dreg_eq reg rd + +(* Return true if an intermediate + * affectation eliminates the potential + * candidate *) +let verify_store_affect reg rs b rev = + let b = (IR b) in + let rs = dreg_of_ireg rs in + (dreg_eq reg b) || (dreg_eq reg rs) + (* Affect a symbolic memory list of potential replacements * for a given write in reg *) -let rec affect_symb_mem reg insta pot_rep stype = +let rec affect_symb_mem reg insta pot_rep stype rev = 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 + if verify_load_affect reg rd b rev then affect_symb_mem reg insta t0 stype rev + else h0 :: affect_symb_mem reg insta t0 stype rev | 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 + if verify_load_affect reg rd b rev then affect_symb_mem reg insta t0 stype rev + else h0 :: affect_symb_mem reg insta t0 stype rev | PStore (PSt_rs_a (Pstrw, IR (RR1 rs), ADimm (b, n))), "strw" -> - if dreg_eq reg (IR b) || dreg_eq reg (dreg_of_ireg rs) then - affect_symb_mem reg insta t0 stype - else h0 :: affect_symb_mem reg insta t0 stype + 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 | PStore (PSt_rs_a (Pstrx, IR (RR1 rs), ADimm (b, n))), "strx" -> - if dreg_eq reg (IR b) || dreg_eq reg (dreg_of_ireg rs) then - affect_symb_mem reg insta t0 stype - else h0 :: affect_symb_mem reg insta t0 stype + 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 | _, _ -> 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 = +let rec read_symb_mem reg insta pot_rep stype rev = 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 + if verify_load_read reg rd b rev then read_symb_mem reg insta t0 stype rev + else h0 :: read_symb_mem reg insta t0 stype rev | 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 + if verify_load_read reg rd b rev then read_symb_mem reg insta t0 stype rev + else h0 :: read_symb_mem reg insta t0 stype rev | PStore (PSt_rs_a (Pstrw, IR (RR1 rs), ADimm (b, n))), "strw" -> - h0 :: affect_symb_mem reg insta t0 stype + h0 :: affect_symb_mem reg insta t0 stype rev | PStore (PSt_rs_a (Pstrx, IR (RR1 rs), ADimm (b, n))), "strx" -> - h0 :: affect_symb_mem reg insta t0 stype + h0 :: affect_symb_mem reg insta t0 stype rev | _, _ -> failwith "read_symb_mem: Found an inconsistent inst in pot_rep") -let update_pot_rep_addressing a insta pot_rep stype = +(* Update a symbolic memory list of potential replacements + * for any addressing *) +let update_pot_rep_addressing a insta pot_rep stype rev = match a with - | ADimm (base, _) -> pot_rep := read_symb_mem (IR base) insta !pot_rep stype + | ADimm (base, _) -> pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev | 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 + 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 | 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 + 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 | 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 + 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 | 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 + 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 | ADadr (base, _, _) -> - pot_rep := read_symb_mem (IR base) insta !pot_rep stype + pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev | ADpostincr (base, _) -> - pot_rep := read_symb_mem (IR base) insta !pot_rep stype + pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev (* Update a symbolic memory list of potential replacements * for any basic instruction *) -let update_pot_rep_basic inst insta pot_rep stype = +let update_pot_rep_basic inst insta pot_rep stype rev = match inst with | PArith i -> ( match i with - | PArithP (_, rd) -> pot_rep := affect_symb_mem rd insta !pot_rep stype + | PArithP (_, rd) -> pot_rep := affect_symb_mem rd insta !pot_rep stype rev | PArithPP (_, rd, rs) -> - pot_rep := affect_symb_mem rd insta !pot_rep stype; - pot_rep := read_symb_mem rs insta !pot_rep stype + pot_rep := affect_symb_mem rd insta !pot_rep stype rev; + pot_rep := read_symb_mem rs insta !pot_rep stype rev | PArithPPP (_, rd, rs1, rs2) -> - 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 + 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 | PArithRR0R (_, rd, rs1, rs2) -> - pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype; + pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev; (match rs1 with | RR0 rs1 -> - pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype + 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 + pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype rev | PArithRR0 (_, rd, rs) -> ( - pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype; + pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev; match rs with | RR0 rs1 -> - pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype + pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev | _ -> ()) | PArithARRRR0 (_, rd, rs1, rs2, rs3) -> ( - 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; + 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; match rs3 with | RR0 rs1 -> - pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype + pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev | _ -> ()) | PArithComparisonPP (_, rs1, rs2) -> - pot_rep := read_symb_mem rs1 insta !pot_rep stype; - pot_rep := read_symb_mem rs2 insta !pot_rep stype + pot_rep := read_symb_mem rs1 insta !pot_rep stype rev; + pot_rep := read_symb_mem rs2 insta !pot_rep stype rev | PArithComparisonR0R (_, rs1, rs2) -> (match rs1 with | RR0 rs1 -> - pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype + 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 + pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype rev | PArithComparisonP (_, rs1) -> - pot_rep := read_symb_mem rs1 insta !pot_rep stype + pot_rep := read_symb_mem rs1 insta !pot_rep stype rev | Pcset (rd, _) -> - pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype + pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev | Pfmovi (_, _, rs) -> ( match rs with | RR0 rs -> - pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype + pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype rev | _ -> ()) | Pcsel (rd, rs1, rs2, _) -> - 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 + 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 | Pfnmul (_, rd, rs1, rs2) -> ()) | PLoad i -> ( match stype with | "ldrw" | "ldrx" -> ( match i with | PLd_rd_a (_, rd, a) -> - pot_rep := affect_symb_mem rd insta !pot_rep stype; - update_pot_rep_addressing a insta pot_rep stype + pot_rep := affect_symb_mem rd insta !pot_rep stype rev; + update_pot_rep_addressing a insta pot_rep stype rev | 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) + pot_rep := affect_symb_mem (dreg_of_ireg rd1) insta !pot_rep stype rev; + pot_rep := affect_symb_mem (dreg_of_ireg rd2) insta !pot_rep stype rev; + update_pot_rep_addressing a insta pot_rep stype rev) | _ -> pot_rep := []) | PStore _ -> pot_rep := [] | Pallocframe (_, _) -> pot_rep := [] | Pfreeframe (_, _) -> pot_rep := [] | Ploadsymbol (rd, _) -> - pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype + pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev | 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 + 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 | 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 + 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 | 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 + 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 | Pnop -> () (* Try to find the index of the first previous compatible @@ -235,6 +263,28 @@ let rec search_compat_rep r2 b2 n2 insta pot_rep stype = | _, _ -> failwith "search_compat_rep: Found an inconsistent inst in pot_rep") +(* 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), stype) with + | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))), "ldrw" -> + if is_valid_ldrw r2 rd1 b2 b1 n2 n1 then Some (h0, rd1, b1, n1) + else search_compat_rep_inv r2 b2 n2 insta t0 stype + | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd1), ADimm (b1, n1))), "ldrx" -> + if is_valid_ldrx r2 rd1 b2 b1 n2 n1 then Some (h0, rd1, b1, n1) + else search_compat_rep_inv r2 b2 n2 insta t0 stype + | PStore (PSt_rs_a (Pstrw, IR (RR1 rs1), ADimm (b1, n1))), "strw" -> + if is_valid_strw b2 b1 n2 n1 then Some (h0, rs1, b1, n1) + else search_compat_rep_inv r2 b2 n2 insta t0 stype + | PStore (PSt_rs_a (Pstrx, IR (RR1 rs1), ADimm (b1, n1))), "strx" -> + if is_valid_strx b2 b1 n2 n1 then Some (h0, rs1, b1, n1) + else search_compat_rep_inv r2 b2 n2 insta t0 stype + | _, _ -> + failwith "search_compat_rep_inv: Found an inconsistent inst in pot_rep") + (* 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 = @@ -242,7 +292,81 @@ let min_is_rev n1 n2 = let z2 = to_int (camlint64_of_coqint n2) in if z1 < z2 then true else false -(* Main peephole function *) +(* 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". *) + let pot_ldrw_rep = ref [] in + let pot_ldrx_rep = ref [] in + let pot_strw_rep = ref [] in + let pot_strx_rep = ref [] in + for i = Array.length insta - 1 downto 1 do + let h0 = insta.(i) in + let h1 = insta.(i - 1) in + (* Here we need to update every symbolic memory according to the matched inst *) + update_pot_rep_basic h0 insta pot_ldrw_rep "ldrw" true; + update_pot_rep_basic h0 insta pot_ldrx_rep "ldrx" true; + update_pot_rep_basic h0 insta pot_strw_rep "strw" true; + update_pot_rep_basic h0 insta pot_strx_rep "strx" true; + match (h0, h1) with + (* Non-consecutive ldrw *) + | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))), _ -> ( + (* Search a previous compatible load *) + match search_compat_rep_inv 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) -> + (* 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 ( + if debug then eprintf "LDP_W_BACK_SPACED_PEEP_IMM_INC\n"; + insta.(i) <- PLoad (Pldp (Pldpw, r, rd1, ADimm (b, n)))) + else ( + if debug then eprintf "LDP_W_BACK_SPACED_PEEP_IMM_DEC\n"; + 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_inv rd1 b1 n1 insta !pot_ldrx_rep "ldrx" with + | None -> pot_ldrx_rep := i :: !pot_ldrx_rep + | Some (rep, r, b, 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 ( + if debug then eprintf "LDP_X_BACK_SPACED_PEEP_IMM_INC\n"; + insta.(i) <- PLoad (Pldp (Pldpx, r, rd1, ADimm (b, n)))) + else ( + if debug then eprintf "LDP_X_BACK_SPACED_PEEP_IMM_DEC\n"; + insta.(i) <- PLoad (Pldp (Pldpx, rd1, r, ADimm (b, n1))))) + (* Non-consecutive stpw *) + | PStore (PSt_rs_a (Pstrw, IR (RR1 rs1), ADimm (b1, n1))), _ -> ( + match search_compat_rep_inv rs1 b1 n1 insta !pot_strw_rep "strw" with + | None -> pot_strw_rep := i :: !pot_strw_rep + | Some (rep, r, b, n) -> + let filt x = x != rep in + pot_strw_rep := List.filter filt !pot_strw_rep; + insta.(rep) <- Pnop; + if debug then eprintf "STP_W_BACK_SPACED_PEEP_IMM_INC\n"; + insta.(i) <- PStore (Pstp (Pstpw, r, rs1, ADimm (b, n)))) + (* Non-consecutive stpx *) + | PStore (PSt_rs_a (Pstrx, IR (RR1 rs1), ADimm (b1, n1))), _ -> ( + match search_compat_rep_inv rs1 b1 n1 insta !pot_strx_rep "strx" with + | None -> pot_strx_rep := i :: !pot_strx_rep + | Some (rep, r, b, n) -> + let filt x = x != rep in + pot_strx_rep := List.filter filt !pot_strx_rep; + insta.(rep) <- Pnop; + if debug then eprintf "STP_X_BACK_SPACED_PEEP_IMM_INC\n"; + insta.(i) <- PStore (Pstp (Pstpx, r, rs1, ADimm (b, n)))) + (* Any other inst *) + | _, _ -> () + done + +(* Main peephole function in forward style *) let pair_rep insta = (* Each list below is a symbolic mem representation * for one type of inst. Lists contains integers which @@ -255,10 +379,10 @@ let pair_rep insta = let h0 = insta.(i) in let h1 = insta.(i + 1) in (* 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"; - update_pot_rep_basic h0 insta pot_strw_rep "strw"; - update_pot_rep_basic h0 insta pot_strx_rep "strx"; + update_pot_rep_basic h0 insta pot_ldrw_rep "ldrw" false; + update_pot_rep_basic h0 insta pot_ldrx_rep "ldrx" false; + update_pot_rep_basic h0 insta pot_strw_rep "strw" false; + update_pot_rep_basic h0 insta pot_strx_rep "strx" false; match (h0, h1) with (* Consecutive ldrw *) | ( PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))), @@ -270,10 +394,10 @@ 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 min_is_rev n1 n2 then ( - if debug then eprintf "LDP_W_CONSEC_PEEP_FORWARD\n"; + if debug then eprintf "LDP_W_CONSEC_PEEP_IMM_INC\n"; insta.(i) <- PLoad (Pldp (Pldpw, rd1, rd2, ADimm (b1, n1)))) else ( - if debug then eprintf "LDP_W_CONSEC_PEEP_BACKWARD\n"; + if debug then eprintf "LDP_W_CONSEC_PEEP_IMM_DEC\n"; insta.(i) <- PLoad (Pldp (Pldpw, rd2, rd1, ADimm (b1, n2)))); insta.(i + 1) <- Pnop) (* Consecutive ldrx *) @@ -284,10 +408,10 @@ let pair_rep insta = insta.(i) <- Pnop) else if is_valid_ldrx rd1 rd2 b1 b2 n1 n2 then ( if min_is_rev n1 n2 then ( - if debug then eprintf "LDP_X_CONSEC_PEEP_FORWARD\n"; + if debug then eprintf "LDP_X_CONSEC_PEEP_IMM_INC\n"; insta.(i) <- PLoad (Pldp (Pldpx, rd1, rd2, ADimm (b1, n1)))) else ( - if debug then eprintf "LDP_X_CONSEC_PEEP_BACKWARD\n"; + if debug then eprintf "LDP_X_CONSEC_PEEP_IMM_DEC\n"; insta.(i) <- PLoad (Pldp (Pldpx, rd2, rd1, ADimm (b1, n2)))); insta.(i + 1) <- Pnop) (* Non-consecutive ldrw *) @@ -303,10 +427,10 @@ let pair_rep insta = pot_ldrw_rep := List.filter filt !pot_ldrw_rep; insta.(rep) <- Pnop; if min_is_rev n n1 then ( - if debug then eprintf "LDP_W_SPACED_PEEP_FORWARD\n"; + if debug then eprintf "LDP_W_FORW_SPACED_PEEP_IMM_INC\n"; insta.(i) <- PLoad (Pldp (Pldpw, r, rd1, ADimm (b, n)))) else ( - if debug then eprintf "LDP_W_SPACED_PEEP_BACKWARD\n"; + if debug then eprintf "LDP_W_FORW_SPACED_PEEP_IMM_DEC\n"; insta.(i) <- PLoad (Pldp (Pldpw, rd1, r, ADimm (b, n1))))) (* Non-consecutive ldrx *) | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd1), ADimm (b1, n1))), _ -> ( @@ -317,10 +441,10 @@ let pair_rep insta = pot_ldrx_rep := List.filter filt !pot_ldrx_rep; insta.(rep) <- Pnop; if min_is_rev n n1 then ( - if debug then eprintf "LDP_X_SPACED_PEEP_FORWARD\n"; + if debug then eprintf "LDP_X_FORW_SPACED_PEEP_IMM_INC\n"; insta.(i) <- PLoad (Pldp (Pldpx, r, rd1, ADimm (b, n)))) else ( - if debug then eprintf "LDP_X_SPACED_PEEP_BACKWARD\n"; + if debug then eprintf "LDP_X_FORW_SPACED_PEEP_IMM_DEC\n"; insta.(i) <- PLoad (Pldp (Pldpx, rd1, r, ADimm (b, n1))))) (* Consecutive strw *) | ( PStore (PSt_rs_a (Pstrw, IR (RR1 rs1), ADimm (b1, n1))), @@ -331,7 +455,7 @@ let pair_rep insta = (* 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_W_CONSEC_PEEP_FORWARD\n"; + if debug then eprintf "STP_W_CONSEC_PEEP_IMM_INC\n"; insta.(i) <- PStore (Pstp (Pstpw, rs1, rs2, ADimm (b1, n1))); insta.(i + 1) <- Pnop (* When nothing can be optimized. *)) (* Consecutive strx *) @@ -341,7 +465,7 @@ let pair_rep insta = Pnop :: (pair_rep insta t0) else*) if is_valid_strx b1 b2 n1 n2 then ( - if debug then eprintf "STP_X_CONSEC_PEEP_FORWARD\n"; + if debug then eprintf "STP_X_CONSEC_PEEP_IMM_INC\n"; insta.(i) <- PStore (Pstp (Pstpx, rs1, rs2, ADimm (b1, n1))); insta.(i + 1) <- Pnop) (* Non-consecutive stpw *) @@ -352,7 +476,7 @@ let pair_rep insta = let filt x = x != rep in pot_strw_rep := List.filter filt !pot_strw_rep; insta.(rep) <- Pnop; - if debug then eprintf "STP_W_SPACED_PEEP_FORWARD\n"; + if debug then eprintf "STP_W_FORW_SPACED_PEEP_IMM_INC\n"; insta.(i) <- PStore (Pstp (Pstpw, r, rs1, ADimm (b, n)))) (* Non-consecutive stpx *) | PStore (PSt_rs_a (Pstrx, IR (RR1 rs1), ADimm (b1, n1))), _ -> ( @@ -362,7 +486,7 @@ let pair_rep insta = let filt x = x != rep in pot_strx_rep := List.filter filt !pot_strx_rep; insta.(rep) <- Pnop; - if debug then eprintf "STP_X_SPACED_PEEP_FORWARD\n"; + if debug then eprintf "STP_X_FORW_SPACED_PEEP_IMM_INC\n"; insta.(i) <- PStore (Pstp (Pstpx, r, rs1, ADimm (b, n)))) (* Any other inst *) | _, _ -> () @@ -373,6 +497,7 @@ let optimize_bdy (bdy : basic list) : basic list = if !Clflags.option_fcoalesce_mem then ( let insta = Array.of_list bdy in pair_rep insta; + pair_rep_inv insta; Array.to_list insta) else bdy -- cgit