From 8781c27a16463fd8f83a9c6eaba7b76846bd296c Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 20 Jan 2021 16:46:52 +0100 Subject: Adding fp loads pair --- aarch64/PeepholeOracle.ml | 203 ++++++++++++++++++++++++---------------------- 1 file changed, 105 insertions(+), 98 deletions(-) (limited to 'aarch64/PeepholeOracle.ml') diff --git a/aarch64/PeepholeOracle.ml b/aarch64/PeepholeOracle.ml index a6945b9f..ecb529d0 100644 --- a/aarch64/PeepholeOracle.ml +++ b/aarch64/PeepholeOracle.ml @@ -27,37 +27,37 @@ let is_valid_immofs_64 z = 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 is_valid_ldr32 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)) + (not (dreg_eq rd1 rd2)) && iregsp_eq b1 b2 - && (not (iregsp_eq (RR1 rd1) b2)) + && (not (dreg_eq rd1 (IR b2))) && (z2 = z1 + 4 || z2 = z1 - 4) && is_valid_immofs_32 z1 then true else false -let is_valid_ldrx rd1 rd2 b1 b2 n1 n2 = +let is_valid_ldr64 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)) + (not (dreg_eq rd1 rd2)) && iregsp_eq b1 b2 - && (not (iregsp_eq (RR1 rd1) b2)) + && (not (dreg_eq rd1 (IR b2))) && (z2 = z1 + 8 || z2 = z1 - 8) && is_valid_immofs_64 z1 then true else false -let is_valid_strw b1 b2 n1 n2 = +let is_valid_str32 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 else false -let is_valid_strx b1 b2 n1 n2 = +let is_valid_str64 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 @@ -70,14 +70,12 @@ let dreg_of_ireg r = IR (RR1 r) * 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 @@ -85,7 +83,6 @@ let verify_load_read reg rd b rev = * 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 @@ -95,11 +92,11 @@ let rec affect_symb_mem reg insta pot_rep stype rev = | [] -> [] | h0 :: t0 -> ( match (insta.(h0), stype) with - | PLoad (PLd_rd_a (_, IR (RR1 rd), ADimm (b, n))), "ldr" -> + | PLoad (PLd_rd_a (_, 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 (_, IR (RR1 rs), ADimm (b, n))), "str" -> + | PStore (PSt_rs_a (_, 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 @@ -113,11 +110,11 @@ let rec read_symb_mem reg insta pot_rep stype rev = | [] -> [] | h0 :: t0 -> ( match (insta.(h0), stype) with - | PLoad (PLd_rd_a (_, IR (RR1 rd), ADimm (b, n))), "ldr" -> + | PLoad (PLd_rd_a (_, 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 - | PStore (PSt_rs_a (_, IR (RR1 rs), ADimm (b, n))), "str" -> + | PStore (PSt_rs_a (_, 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") @@ -219,9 +216,9 @@ let update_pot_rep_basic inst 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; + affect_symb_mem rd1 insta !pot_rep stype rev; pot_rep := - affect_symb_mem (dreg_of_ireg rd2) insta !pot_rep stype rev; + affect_symb_mem rd2 insta !pot_rep stype rev; update_pot_rep_addressing a insta pot_rep stype rev) | _ -> pot_rep := []) | PStore _ -> ( @@ -244,59 +241,6 @@ let update_pot_rep_basic inst 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 - * 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), stype) with - | 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 (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 (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 (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") - -(* 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 (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 (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 (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 (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") - (* 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 = @@ -310,6 +254,8 @@ let trans_ldi (ldi : load_rd_a) : load_rd1_rd2_a = match ldi with | Pldrw | Pldrw_a -> Pldpw | Pldrx | Pldrx_a -> Pldpx + | Pldrs -> Pldps + | Pldrd | Pldrd_a -> Pldpd | _ -> failwith "trans_ldi: Found a non compatible load to translate" let trans_sti (sti : store_rs_a) : store_rs1_rs2_a = @@ -319,12 +265,14 @@ let trans_sti (sti : store_rs_a) : store_rs1_rs2_a = | _ -> 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 + match ldi with Pldrw | Pldrw_a | Pldrx | Pldrx_a | Pldrs | Pldrd | Pldrd_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) + | Pldrs -> (match ldi2 with Pldrs -> true | _ -> false) + | Pldrd | Pldrd_a -> ( match ldi2 with Pldrd | Pldrd_a -> true | _ -> false) | _ -> false let is_compat_store (sti : store_rs_a) = @@ -338,25 +286,64 @@ let are_compat_store (sti1 : store_rs_a) (sti2 : store_rs_a) = let get_load_string (ldi : load_rd_a) = match ldi with - | Pldrw | Pldrw_a -> "ldrw" - | Pldrx | Pldrx_a -> "ldrx" + | Pldrw | Pldrw_a -> "ldr32" + | Pldrs -> "ldr32f" + | Pldrx | Pldrx_a -> "ldr64" + | Pldrd | Pldrd_a -> "ldr64f" | _ -> 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" + | Pstrw | Pstrw_a -> "str32" + | Pstrx | Pstrx_a -> "str64" | _ -> 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 + | "ldr32" | "ldr32f" -> is_valid_ldr32 rd1 rd2 b1 b2 n1 n2 + | _ -> is_valid_ldr64 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 + | "str32" -> is_valid_str32 b1 b2 n1 n2 + | _ -> 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 + | _ -> + 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) 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 + "search_compat_rep_inv: Found an inconsistent inst in pot_rep") (* Main peephole function in backward style *) let pair_rep_inv insta = @@ -365,6 +352,8 @@ let pair_rep_inv insta = * are the indices of insts in the main array "insta". *) let pot_ldrw_rep = ref [] in let pot_ldrx_rep = ref [] in + let pot_ldrs_rep = ref [] in + let pot_ldrd_rep = ref [] in let pot_strw_rep = ref [] in let pot_strx_rep = ref [] in for i = Array.length insta - 1 downto 1 do @@ -373,18 +362,25 @@ let pair_rep_inv insta = (* Here we need to update every symbolic memory according to the matched inst *) 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_ldrs_rep "ldr" true; + update_pot_rep_basic h0 insta pot_ldrd_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 ldr *) - | PLoad (PLd_rd_a (ldi, IR (RR1 rd1), ADimm (b1, n1))), _ -> ( + | PLoad (PLd_rd_a (ldi, 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 + match ldi with + | Pldrw | Pldrw_a -> pot_ldrw_rep + | Pldrx | Pldrx_a -> pot_ldrx_rep + | Pldrs -> pot_ldrs_rep + | _ -> pot_ldrd_rep in (* Search a previous compatible load *) + let ld_string = get_load_string ldi in match - search_compat_rep_inv rd1 b1 n1 insta !pot_rep (get_load_string ldi) + search_compat_rep_inv rd1 b1 n1 insta !pot_rep ld_string with (* If we can't find a candidate, add the current load as a potential future one *) | None -> pot_rep := i :: !pot_rep @@ -395,20 +391,20 @@ let pair_rep_inv insta = 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"; + if debug then eprintf "LDP_BACK_SPACED_PEEP_IMM_INC_%s\n" ld_string; 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"; + if debug then eprintf "LDP_BACK_SPACED_PEEP_IMM_DEC_%s\n" ld_string; 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))), _ -> ( + | PStore (PSt_rs_a (sti, 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 @@ -451,24 +447,30 @@ let pair_rep insta = * are the indices of insts in the main array "insta". *) let pot_ldrw_rep = ref [] in let pot_ldrx_rep = ref [] in + let pot_ldrs_rep = ref [] in + let pot_ldrd_rep = ref [] in let pot_strw_rep = ref [] in let pot_strx_rep = ref [] in for i = 0 to Array.length insta - 2 do + eprintf "DEBUG %d" (Array.length 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 "ldr" false; update_pot_rep_basic h0 insta pot_ldrx_rep "ldr" false; + update_pot_rep_basic h0 insta pot_ldrs_rep "ldr" true; + update_pot_rep_basic h0 insta pot_ldrd_rep "ldr" true; 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 ldr *) - | ( PLoad (PLd_rd_a (ldi1, IR (RR1 rd1), ADimm (b1, n1))), - PLoad (PLd_rd_a (ldi2, IR (RR1 rd2), ADimm (b2, n2))) ) -> + | ( PLoad (PLd_rd_a (ldi1, rd1, ADimm (b1, n1))), + PLoad (PLd_rd_a (ldi2, 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 ( + let ld_string = get_load_string ldi1 in + if is_valid_ldr rd1 rd2 b1 b2 n1 n2 ld_string then ( if min_is_rev n1 n2 then ( - if debug then eprintf "LDP_CONSEC_PEEP_IMM_INC\n"; + if debug then eprintf "LDP_CONSEC_PEEP_IMM_INC_%s\n" ld_string; insta.(i) <- PLoad (Pldp @@ -479,7 +481,7 @@ let pair_rep insta = chunk_load ldi2, ADimm (b1, n1) ))) else ( - if debug then eprintf "LDP_CONSEC_PEEP_IMM_DEC\n"; + if debug then eprintf "LDP_CONSEC_PEEP_IMM_DEC_%s\n" ld_string; insta.(i) <- PLoad (Pldp @@ -491,14 +493,19 @@ let pair_rep insta = ADimm (b1, n2) ))); insta.(i + 1) <- Pnop) (* Non-consecutive ldr *) - | PLoad (PLd_rd_a (ldi, IR (RR1 rd1), ADimm (b1, n1))), _ -> ( + | PLoad (PLd_rd_a (ldi, 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 + match ldi with + | Pldrw | Pldrw_a -> pot_ldrw_rep + | Pldrx | Pldrx_a -> pot_ldrx_rep + | Pldrs -> pot_ldrs_rep + | _ -> pot_ldrd_rep in (* Search a previous compatible load *) + let ld_string = get_load_string ldi in match - search_compat_rep rd1 b1 n1 insta !pot_rep (get_load_string ldi) + search_compat_rep rd1 b1 n1 insta !pot_rep ld_string with (* If we can't find a candidate, add the current load as a potential future one *) | None -> pot_rep := i :: !pot_rep @@ -509,21 +516,21 @@ let pair_rep insta = 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"; + if debug then eprintf "LDP_FORW_SPACED_PEEP_IMM_INC_%s\n" ld_string; 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"; + if debug then eprintf "LDP_FORW_SPACED_PEEP_IMM_DEC_%s\n" ld_string; 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))) ) -> + | ( PStore (PSt_rs_a (sti1, rd1, ADimm (b1, n1))), + PStore (PSt_rs_a (sti2, rd2, ADimm (b2, n2))) ) -> (* 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. *) @@ -543,7 +550,7 @@ let pair_rep insta = ADimm (b1, n1) )); insta.(i + 1) <- Pnop) (* Non-consecutive str *) - | PStore (PSt_rs_a (sti, IR (RR1 rd1), ADimm (b1, n1))), _ -> ( + | PStore (PSt_rs_a (sti, 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 -- cgit