aboutsummaryrefslogtreecommitdiffstats
path: root/aarch64/PeepholeOracle.ml
diff options
context:
space:
mode:
Diffstat (limited to 'aarch64/PeepholeOracle.ml')
-rw-r--r--aarch64/PeepholeOracle.ml315
1 files changed, 191 insertions, 124 deletions
diff --git a/aarch64/PeepholeOracle.ml b/aarch64/PeepholeOracle.ml
index a6945b9f..83e454e7 100644
--- a/aarch64/PeepholeOracle.ml
+++ b/aarch64/PeepholeOracle.ml
@@ -27,57 +27,56 @@ 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
else false
let dreg_of_ireg r = IR (RR1 r)
+let dreg_of_freg r = FR 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
@@ -85,9 +84,30 @@ 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
+type ph_type =
+ | P32
+ | P32f
+ | P64
+ | P64f
+
+type inst_type =
+ | Ldr of ph_type
+ | Str of ph_type
+
+let ph_ty_to_string = function
+ | Ldr P32 -> "ldr32"
+ | Ldr P32f -> "ldr32f"
+ | Ldr P64 -> "ldr64"
+ | Ldr P64f -> "ldr64f"
+ | Str P32 -> "str32"
+ | Str P32f -> "str32f"
+ | Str P64 -> "str64"
+ | Str P64f -> "str64f"
+
+let print_ph_ty chan v = output_string chan (ph_ty_to_string v)
+
(* Affect a symbolic memory list of potential replacements
* for a given write in reg *)
let rec affect_symb_mem reg insta pot_rep stype rev =
@@ -95,11 +115,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 +133,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")
@@ -197,7 +217,8 @@ let update_pot_rep_basic inst insta pot_rep stype rev =
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 rev
- | Pfmovi (_, _, rs) -> (
+ | Pfmovi (_, rd, rs) -> (
+ pot_rep := affect_symb_mem (dreg_of_freg rd) insta !pot_rep stype rev;
match rs with
| RR0 rs ->
pot_rep :=
@@ -207,28 +228,31 @@ let update_pot_rep_basic inst insta pot_rep stype rev =
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) -> ())
+ | Pfnmul (_, rd, rs1, rs2) ->
+ pot_rep := affect_symb_mem (dreg_of_freg rd) insta !pot_rep stype rev;
+ pot_rep := read_symb_mem (dreg_of_freg rs1) insta !pot_rep stype rev;
+ pot_rep := read_symb_mem (dreg_of_freg rs2) insta !pot_rep stype rev)
| PLoad i -> (
(* Here, we consider a different behavior for load and store potential candidates:
* a load does not obviously cancel the ldp candidates, but it does for any stp candidate. *)
match stype with
- | "ldr" -> (
+ | 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;
+ 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 _ -> (
(* Here, we consider that a store cancel all ldp candidates, but it is far more complicated for stp ones :
* if we cancel stp candidates here, we would prevent ourselves to apply the non-consec store peephole.
* To solve this issue, the store candidates cleaning is managed directly in the peephole function below. *)
- match stype with "ldr" -> pot_rep := [] | _ -> ())
+ match stype with Ldr _ -> pot_rep := [] | _ -> ())
| Pallocframe (_, _) -> pot_rep := []
| Pfreeframe (_, _) -> pot_rep := []
| Ploadsymbol (rd, _) ->
@@ -244,59 +268,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,53 +281,102 @@ 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 =
match sti with
| Pstrw | Pstrw_a -> Pstpw
| Pstrx | Pstrx_a -> Pstpx
+ | Pstrs -> Pstps
+ | Pstrd | Pstrd_a -> Pstpd
| _ -> 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) =
- match sti with Pstrw | Pstrw_a | Pstrx | Pstrx_a -> true | _ -> false
+ match sti with Pstrw | Pstrw_a | Pstrx | Pstrx_a | Pstrs | Pstrd | Pstrd_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)
+ | Pstrs -> (match sti2 with Pstrs -> true | _ -> false)
+ | Pstrd | Pstrd_a -> ( match sti2 with Pstrd | Pstrd_a -> true | _ -> false)
| _ -> false
-let get_load_string (ldi : load_rd_a) =
+let get_load_pht (ldi : load_rd_a) =
match ldi with
- | Pldrw | Pldrw_a -> "ldrw"
- | Pldrx | Pldrx_a -> "ldrx"
+ | Pldrw | Pldrw_a -> Ldr P32
+ | Pldrs -> Ldr P32f
+ | Pldrx | Pldrx_a -> Ldr P64
+ | Pldrd | Pldrd_a -> Ldr P64f
| _ -> failwith "get_load_string: Found a non compatible load to translate"
-let get_store_string (sti : store_rs_a) =
+let get_store_pht (sti : store_rs_a) =
match sti with
- | Pstrw | Pstrw_a -> "strw"
- | Pstrx | Pstrx_a -> "strx"
+ | Pstrw | Pstrw_a -> Str P32
+ | Pstrs -> Str P32f
+ | Pstrx | Pstrx_a -> Str P64
+ | Pstrd | Pstrd_a -> Str P64f
| _ -> 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
+ | Ldr P32 | Ldr P32f -> 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
+ | Str P32 | Str P32f -> 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,26 +385,39 @@ 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
+ let pot_strs_rep = ref [] in
+ let pot_strd_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 "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;
+ update_pot_rep_basic h0 insta pot_ldrw_rep (Ldr P32) true;
+ update_pot_rep_basic h0 insta pot_ldrx_rep (Ldr P64) true;
+ update_pot_rep_basic h0 insta pot_ldrs_rep (Ldr P32f) true;
+ update_pot_rep_basic h0 insta pot_ldrd_rep (Ldr P64f) true;
+ update_pot_rep_basic h0 insta pot_strw_rep (Str P32) true;
+ update_pot_rep_basic h0 insta pot_strx_rep (Str P64) true;
+ update_pot_rep_basic h0 insta pot_strs_rep (Str P32f) true;
+ update_pot_rep_basic h0 insta pot_strd_rep (Str P64f) 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_t = get_load_pht 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_t
with
(* If we can't find a candidate, add the current load as a potential future one *)
| None -> pot_rep := i :: !pot_rep
@@ -395,33 +428,39 @@ 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_%a\n" print_ph_ty ld_t;
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_%a\n" print_ph_ty ld_t;
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
+ match sti with
+ | Pstrw | Pstrw_a -> pot_strw_rep
+ | Pstrx | Pstrx_a -> pot_strx_rep
+ | Pstrs -> pot_strs_rep
+ | _ -> pot_strd_rep
in
(* Search a previous compatible store *)
+ let st_t = get_store_pht sti in
match
- search_compat_rep_inv rd1 b1 n1 insta !pot_rep
- (get_store_string sti)
+ search_compat_rep_inv rd1 b1 n1 insta !pot_rep st_t
with
(* If we can't find a candidate, clean and add the current store as a potential future one *)
| None ->
pot_strw_rep := [];
pot_strx_rep := [];
+ pot_strs_rep := [];
+ pot_strd_rep := [];
pot_rep := i :: !pot_rep
(* Else, perform the peephole *)
| Some (rep, c, r, b, n) ->
@@ -429,7 +468,7 @@ let pair_rep_inv insta =
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";
+ if debug then eprintf "STP_BACK_SPACED_PEEP_IMM_INC_%a\n" print_ph_ty st_t;
insta.(i) <-
PStore
(Pstp
@@ -440,7 +479,9 @@ let pair_rep_inv insta =
match i with
| PStore _ ->
pot_strw_rep := [];
- pot_strx_rep := []
+ pot_strx_rep := [];
+ pot_strs_rep := [];
+ pot_strd_rep := []
| _ -> ())
done
@@ -451,24 +492,33 @@ 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
+ let pot_strs_rep = ref [] in
+ let pot_strd_rep = ref [] in
for i = 0 to Array.length insta - 2 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 "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;
+ update_pot_rep_basic h0 insta pot_ldrw_rep (Ldr P32) true;
+ update_pot_rep_basic h0 insta pot_ldrx_rep (Ldr P64) true;
+ update_pot_rep_basic h0 insta pot_ldrs_rep (Ldr P32f) true;
+ update_pot_rep_basic h0 insta pot_ldrd_rep (Ldr P64f) true;
+ update_pot_rep_basic h0 insta pot_strw_rep (Str P32) true;
+ update_pot_rep_basic h0 insta pot_strx_rep (Str P64) true;
+ update_pot_rep_basic h0 insta pot_strs_rep (Str P32f) true;
+ update_pot_rep_basic h0 insta pot_strd_rep (Str P64f) true;
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_t = get_load_pht ldi1 in
+ if is_valid_ldr rd1 rd2 b1 b2 n1 n2 ld_t 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_%a\n" print_ph_ty ld_t;
insta.(i) <-
PLoad
(Pldp
@@ -479,7 +529,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_%a\n" print_ph_ty ld_t;
insta.(i) <-
PLoad
(Pldp
@@ -491,14 +541,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_t = get_load_pht 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_t
with
(* If we can't find a candidate, add the current load as a potential future one *)
| None -> pot_rep := i :: !pot_rep
@@ -509,29 +564,32 @@ 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_%a\n" print_ph_ty ld_t;
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_%a\n" print_ph_ty ld_t;
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. *)
pot_strw_rep := [];
pot_strx_rep := [];
+ pot_strs_rep := [];
+ pot_strd_rep := [];
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";
+ let st_t = get_store_pht sti1 in
+ if is_valid_str b1 b2 n1 n2 st_t then (
+ if debug then eprintf "STP_CONSEC_PEEP_IMM_INC_%a\n" print_ph_ty st_t;
insta.(i) <-
PStore
(Pstp
@@ -543,19 +601,26 @@ 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
+ match sti with
+ | Pstrw | Pstrw_a -> pot_strw_rep
+ | Pstrx | Pstrx_a -> pot_strx_rep
+ | Pstrs -> pot_strs_rep
+ | _ -> pot_strd_rep
in
(* Search a previous compatible store *)
+ let st_t = get_store_pht sti in
match
- search_compat_rep rd1 b1 n1 insta !pot_rep (get_store_string sti)
+ search_compat_rep rd1 b1 n1 insta !pot_rep st_t
with
(* If we can't find a candidate, clean and add the current store as a potential future one *)
| None ->
pot_strw_rep := [];
pot_strx_rep := [];
+ pot_strs_rep := [];
+ pot_strd_rep := [];
pot_rep := i :: !pot_rep
(* Else, perform the peephole *)
| Some (rep, c, r, b, n) ->
@@ -563,7 +628,7 @@ let pair_rep insta =
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";
+ if debug then eprintf "STP_FORW_SPACED_PEEP_IMM_INC_%a\n" print_ph_ty st_t;
insta.(i) <-
PStore
(Pstp (trans_sti sti, r, rd1, c, chunk_store sti, ADimm (b, n)))
@@ -574,7 +639,9 @@ let pair_rep insta =
match i with
| PStore _ ->
pot_strw_rep := [];
- pot_strx_rep := []
+ pot_strx_rep := [];
+ pot_strs_rep := [];
+ pot_strd_rep := []
| _ -> ())
done