From ec1a33e664f3484772a06dcd7e3198aa80b5d993 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 10 Dec 2020 23:06:17 +0100 Subject: Big improvment in peephole, changing LDP/STP semantics --- aarch64/PeepholeOracle.ml | 487 +++++++++++++++++++++++++--------------------- 1 file changed, 270 insertions(+), 217 deletions(-) (limited to 'aarch64/PeepholeOracle.ml') diff --git a/aarch64/PeepholeOracle.ml b/aarch64/PeepholeOracle.ml index 94efc75e..65c820ac 100644 --- a/aarch64/PeepholeOracle.ml +++ b/aarch64/PeepholeOracle.ml @@ -68,12 +68,9 @@ let dreg_of_ireg r = IR (RR1 r) * affectation eliminates the potential * candidate *) let verify_load_affect reg rd b rev = - let b = (IR b) in + 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) + 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 @@ -86,9 +83,9 @@ let verify_load_read reg rd b rev = * affectation eliminates the potential * candidate *) let verify_store_affect reg rs b rev = - let b = (IR b) in + let b = IR b in let rs = dreg_of_ireg rs in - (dreg_eq reg b) || (dreg_eq reg rs) + dreg_eq reg b || dreg_eq reg rs (* Affect a symbolic memory list of potential replacements * for a given write in reg *) @@ -97,17 +94,11 @@ let rec affect_symb_mem reg insta pot_rep stype rev = | [] -> [] | h0 :: t0 -> ( match (insta.(h0), stype) with - | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd), ADimm (b, n))), "ldrw" -> - 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 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 verify_store_affect reg rs b rev then + | PLoad (PLd_rd_a (_, IR (RR1 rd), ADimm (b, n))), "ldr" -> + 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 (Pstrx, IR (RR1 rs), ADimm (b, n))), "strx" -> + | PStore (PSt_rs_a (_, IR (RR1 rs), ADimm (b, n))), "str" -> 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 @@ -121,23 +112,20 @@ let rec read_symb_mem reg insta pot_rep stype rev = | [] -> [] | h0 :: t0 -> ( match (insta.(h0), stype) with - | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd), ADimm (b, n))), "ldrw" -> - if verify_load_read reg rd b rev then read_symb_mem reg insta t0 stype rev + | PLoad (PLd_rd_a (_, IR (RR1 rd), ADimm (b, n))), "ldr" -> + 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 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 rev - | PStore (PSt_rs_a (Pstrx, IR (RR1 rs), ADimm (b, n))), "strx" -> - h0 :: affect_symb_mem reg insta t0 stype rev + | PStore (PSt_rs_a (_, IR (RR1 rs), ADimm (b, n))), "str" -> + h0 :: read_symb_mem reg insta t0 stype rev | _, _ -> failwith "read_symb_mem: Found an inconsistent inst in pot_rep") (* 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 rev + | 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 rev; pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype rev @@ -161,7 +149,8 @@ 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 rev + | 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 rev; pot_rep := read_symb_mem rs insta !pot_rep stype rev @@ -173,14 +162,16 @@ let update_pot_rep_basic inst insta pot_rep stype rev = 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 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 | PArithRR0 (_, rd, rs) -> ( 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 rev + 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 rev; @@ -188,7 +179,8 @@ let update_pot_rep_basic inst 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 rev + 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 rev; @@ -196,7 +188,8 @@ let update_pot_rep_basic inst 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 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 | PArithComparisonP (_, rs1) -> @@ -206,7 +199,8 @@ let update_pot_rep_basic inst 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 rev + 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 rev; @@ -215,14 +209,16 @@ let update_pot_rep_basic inst insta pot_rep stype rev = | Pfnmul (_, rd, rs1, rs2) -> ()) | PLoad i -> ( match stype with - | "ldrw" | "ldrx" -> ( + | "ldr" -> ( match i with | PLd_rd_a (_, rd, a) -> 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 rev; - pot_rep := affect_symb_mem (dreg_of_ireg rd2) insta !pot_rep stype rev; + | Pldp (_, rd1, rd2, _, _, a) -> + 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 := [] @@ -248,17 +244,21 @@ let rec search_compat_rep r2 b2 n2 insta pot_rep stype = | [] -> 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 r2 b1 b2 n1 n2 then Some (h0, rd1, b1, n1) + | PLoad (PLd_rd_a (ld1, IR (RR1 rd1), ADimm (b1, n1))), "ldrw" -> + if is_valid_ldrw rd1 r2 b1 b2 n1 n2 then + Some (h0, chunk_load ld1, rd1, b1, n1) else search_compat_rep r2 b2 n2 insta t0 stype - | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd1), ADimm (b1, n1))), "ldrx" -> - if is_valid_ldrx rd1 r2 b1 b2 n1 n2 then Some (h0, rd1, b1, n1) + | PLoad (PLd_rd_a (ld1, IR (RR1 rd1), ADimm (b1, n1))), "ldrx" -> + if is_valid_ldrx rd1 r2 b1 b2 n1 n2 then + Some (h0, chunk_load ld1, rd1, b1, n1) else search_compat_rep r2 b2 n2 insta t0 stype - | PStore (PSt_rs_a (Pstrw, IR (RR1 rs1), ADimm (b1, n1))), "strw" -> - if is_valid_strw b1 b2 n1 n2 then Some (h0, rs1, b1, n1) + | PStore (PSt_rs_a (st1, IR (RR1 rs1), ADimm (b1, n1))), "strw" -> + if is_valid_strw b1 b2 n1 n2 then + Some (h0, chunk_store st1, rs1, b1, n1) else search_compat_rep r2 b2 n2 insta t0 stype - | PStore (PSt_rs_a (Pstrx, IR (RR1 rs1), ADimm (b1, n1))), "strx" -> - if is_valid_strx b1 b2 n1 n2 then Some (h0, rs1, b1, n1) + | PStore (PSt_rs_a (st1, IR (RR1 rs1), ADimm (b1, n1))), "strx" -> + if is_valid_strx b1 b2 n1 n2 then + Some (h0, chunk_store st1, rs1, b1, n1) else search_compat_rep r2 b2 n2 insta t0 stype | _, _ -> failwith "search_compat_rep: Found an inconsistent inst in pot_rep") @@ -270,20 +270,25 @@ let rec search_compat_rep_inv r2 b2 n2 insta pot_rep stype = | [] -> 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) + | PLoad (PLd_rd_a (ld1, IR (RR1 rd1), ADimm (b1, n1))), "ldrw" -> + if is_valid_ldrw r2 rd1 b2 b1 n2 n1 then + Some (h0, chunk_load ld1, 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) + | PLoad (PLd_rd_a (ld1, IR (RR1 rd1), ADimm (b1, n1))), "ldrx" -> + if is_valid_ldrx r2 rd1 b2 b1 n2 n1 then + Some (h0, chunk_load ld1, 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) + | PStore (PSt_rs_a (st1, IR (RR1 rs1), ADimm (b1, n1))), "strw" -> + if is_valid_strw b2 b1 n2 n1 then + Some (h0, chunk_store st1, 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) + | PStore (PSt_rs_a (st1, IR (RR1 rs1), ADimm (b1, n1))), "strx" -> + if is_valid_strx b2 b1 n2 n1 then + Some (h0, chunk_store st1, 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") + 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 *) @@ -292,6 +297,58 @@ let min_is_rev n1 n2 = let z2 = to_int (camlint64_of_coqint n2) in if z1 < z2 then true else false +let trans_ldi (ldi : load_rd_a) : load_rd1_rd2_a = + match ldi with + | Pldrw | Pldrw_a -> Pldpw + | Pldrx | Pldrx_a -> Pldpx + | _ -> 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 + | _ -> failwith "trans_sti: Found a non compatible store to translate" + +let is_compat_load (ldi : load_rd_a) = + match ldi with Pldrw | Pldrw_a | Pldrx | Pldrx_a -> true | _ -> false + +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) + | _ -> false + +let is_compat_store (sti : store_rs_a) = + match sti with Pstrw | Pstrw_a | Pstrx | Pstrx_a -> true | _ -> false + +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) + | _ -> false + +let get_load_string (ldi : load_rd_a) = + match ldi with + | Pldrw | Pldrw_a -> "ldrw" + | Pldrx | Pldrx_a -> "ldrx" + | _ -> failwith "get_load_string: Found a non compatible load to translate" + +let get_store_string (sti : store_rs_a) = + match sti with + | Pstrw | Pstrw_a -> "strw" + | Pstrx | Pstrx_a -> "strx" + | _ -> 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 + | "ldrw" -> is_valid_ldrw rd1 rd2 b1 b2 n1 n2 + | _ -> is_valid_ldrx rd1 rd2 b1 b2 n1 n2 + +let is_valid_str b1 b2 n1 n2 stype = + match stype with + | "strw" -> is_valid_strw b1 b2 n1 n2 + | _ -> is_valid_strx b1 b2 n1 n2 + (* Main peephole function in backward style *) let pair_rep_inv insta = (* Each list below is a symbolic mem representation @@ -305,64 +362,66 @@ let pair_rep_inv 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" 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; + update_pot_rep_basic h0 insta pot_ldrw_rep "ldr" true; + update_pot_rep_basic h0 insta pot_ldrx_rep "ldr" true; + update_pot_rep_basic h0 insta pot_strw_rep "str" true; + update_pot_rep_basic h0 insta pot_strx_rep "str" 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 *) + (* Non-consecutive ldr *) + | PLoad (PLd_rd_a (ldi, IR (RR1 rd1), ADimm (b1, n1))), _ -> ( + if is_compat_load ldi then + let pot_rep = + match ldi with Pldrw | Pldrw_a -> pot_ldrw_rep | _ -> pot_ldrx_rep + in + (* Search a previous compatible load *) + match + search_compat_rep_inv rd1 b1 n1 insta !pot_rep (get_load_string ldi) + with + (* 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 ( + if debug then eprintf "LDP_BACK_SPACED_PEEP_IMM_INC\n"; + insta.(i) <- + PLoad + (Pldp + (trans_ldi ldi, r, rd1, c, chunk_load ldi, ADimm (b, n)))) + else ( + if debug then eprintf "LDP_BACK_SPACED_PEEP_IMM_DEC\n"; + insta.(i) <- + PLoad + (Pldp + (trans_ldi ldi, rd1, r, chunk_load ldi, c, ADimm (b, n1)))) + ) + (* Non-consecutive str *) + | PStore (PSt_rs_a (sti, IR (RR1 rd1), ADimm (b1, n1))), _ -> ( + if is_compat_store sti then + let pot_rep = + match sti with Pstrw | Pstrw_a -> pot_strw_rep | _ -> pot_strx_rep + in + (* Search a previous compatible store *) + match + search_compat_rep_inv rd1 b1 n1 insta !pot_rep + (get_store_string sti) + with + (* If we can't find a candidate, add the current store 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 debug then eprintf "STP_BACK_SPACED_PEEP_IMM_INC\n"; + insta.(i) <- + PStore + (Pstp (trans_sti sti, r, rd1, c, chunk_store sti, ADimm (b, n))) + (* Any other inst *)) | _, _ -> () done @@ -379,115 +438,109 @@ 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" 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; + update_pot_rep_basic h0 insta pot_ldrw_rep "ldr" false; + update_pot_rep_basic h0 insta pot_ldrx_rep "ldr" false; + update_pot_rep_basic h0 insta pot_strw_rep "str" false; + update_pot_rep_basic h0 insta pot_strx_rep "str" false; 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. *) - 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 min_is_rev n1 n2 then ( - 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_IMM_DEC\n"; - 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 ( - if debug then eprintf "LDP_XOPT\n"; - 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_IMM_INC\n"; - insta.(i) <- PLoad (Pldp (Pldpx, rd1, rd2, ADimm (b1, n1)))) - else ( - 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 *) - | 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) -> - (* 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_FORW_SPACED_PEEP_IMM_INC\n"; - insta.(i) <- PLoad (Pldp (Pldpw, r, rd1, ADimm (b, n)))) - else ( - 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))), _ -> ( - 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) -> - 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_FORW_SPACED_PEEP_IMM_INC\n"; - insta.(i) <- PLoad (Pldp (Pldpx, r, rd1, ADimm (b, n)))) + (* Consecutive ldr *) + | ( PLoad (PLd_rd_a (ldi1, IR (RR1 rd1), ADimm (b1, n1))), + PLoad (PLd_rd_a (ldi2, IR (RR1 rd2), ADimm (b2, n2))) ) -> + if are_compat_load ldi1 ldi2 then + if is_valid_ldr rd1 rd2 b1 b2 n1 n2 (get_load_string ldi1) then ( + if min_is_rev n1 n2 then ( + if debug then eprintf "LDP_CONSEC_PEEP_IMM_INC\n"; + insta.(i) <- + PLoad + (Pldp + ( trans_ldi ldi1, + rd1, + rd2, + chunk_load ldi1, + chunk_load ldi2, + ADimm (b1, n1) ))) else ( - 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))), - 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_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 *) - | ( 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_X_CONSEC_PEEP_IMM_INC\n"; - insta.(i) <- PStore (Pstp (Pstpx, rs1, rs2, ADimm (b1, n1))); - insta.(i + 1) <- Pnop) - (* Non-consecutive stpw *) - | PStore (PSt_rs_a (Pstrw, IR (RR1 rs1), ADimm (b1, n1))), _ -> ( - match search_compat_rep 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_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))), _ -> ( - match search_compat_rep 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_FORW_SPACED_PEEP_IMM_INC\n"; - insta.(i) <- PStore (Pstp (Pstpx, r, rs1, ADimm (b, n)))) + if debug then eprintf "LDP_CONSEC_PEEP_IMM_DEC\n"; + 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 *) + | PLoad (PLd_rd_a (ldi, IR (RR1 rd1), ADimm (b1, n1))), _ -> ( + if is_compat_load ldi then + let pot_rep = + match ldi with Pldrw | Pldrw_a -> pot_ldrw_rep | _ -> pot_ldrx_rep + in + (* Search a previous compatible load *) + match + search_compat_rep rd1 b1 n1 insta !pot_rep (get_load_string ldi) + with + (* 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 ( + if debug then eprintf "LDP_FORW_SPACED_PEEP_IMM_INC\n"; + insta.(i) <- + PLoad + (Pldp + (trans_ldi ldi, r, rd1, c, chunk_load ldi, ADimm (b, n)))) + else ( + if debug then eprintf "LDP_FORW_SPACED_PEEP_IMM_DEC\n"; + insta.(i) <- + PLoad + (Pldp + (trans_ldi ldi, rd1, r, chunk_load ldi, c, ADimm (b, n1)))) + ) + (* Consecutive str *) + | ( PStore (PSt_rs_a (sti1, IR (RR1 rd1), ADimm (b1, n1))), + PStore (PSt_rs_a (sti2, IR (RR1 rd2), ADimm (b2, n2))) ) -> + if are_compat_store sti1 sti2 then + if is_valid_str b1 b2 n1 n2 (get_store_string sti1) then ( + if debug then eprintf "STP_CONSEC_PEEP_IMM_INC\n"; + 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 *) + | PStore (PSt_rs_a (sti, IR (RR1 rd1), ADimm (b1, n1))), _ -> ( + if is_compat_store sti then + let pot_rep = + match sti with Pstrw | Pstrw_a -> pot_strw_rep | _ -> pot_strx_rep + in + (* Search a previous compatible store *) + match + search_compat_rep rd1 b1 n1 insta !pot_rep (get_store_string sti) + with + (* If we can't find a candidate, add the current store 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 debug then eprintf "STP_FORW_SPACED_PEEP_IMM_INC\n"; + insta.(i) <- + PStore + (Pstp (trans_sti sti, r, rd1, c, chunk_store sti, ADimm (b, n))) + ) (* Any other inst *) | _, _ -> () done -- cgit