Big improvment in peephole, changing LDP/STP semantics

1 files changed, 270 insertions, 217 deletions

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