Peephole finished for now

1 files changed, 211 insertions, 86 deletions

diff --git a/aarch64/PeepholeOracle.ml b/aarch64/PeepholeOracle.ml
index 8d30d803..94efc75e 100644
--- a/aarch64/PeepholeOracle.ml
+++ b/aarch64/PeepholeOracle.ml
@@ -16,7 +16,7 @@ open Asm
 open Int64
 open Printf
 
-let debug = true
+let debug = false
 
 (* Functions to verify the immediate offset range for ldp/stp *)
 let is_valid_immofs_32 z =
@@ -64,153 +64,181 @@ let is_valid_strx b1 b2 n1 n2 =
 
 let dreg_of_ireg r = IR (RR1 r)
 
+(* Return true if an intermediate
+ * affectation eliminates the potential
+ * candidate *)
+let verify_load_affect reg rd b rev =
+  let b = (IR b) in
+  let rd = dreg_of_ireg rd in
+  if not rev then
+    dreg_eq reg b
+  else
+    (dreg_eq reg b) || (dreg_eq reg rd)
+
+(* Return true if an intermediate
+ * read eliminates the potential
+ * candidate *)
+let verify_load_read reg rd b rev =
+  let rd = dreg_of_ireg rd in
+  dreg_eq reg rd
+
+(* Return true if an intermediate
+ * affectation eliminates the potential
+ * candidate *)
+let verify_store_affect reg rs b rev =
+  let b = (IR b) in
+  let rs = dreg_of_ireg rs in
+  (dreg_eq reg b) || (dreg_eq reg rs)
+
 (* Affect a symbolic memory list of potential replacements
  * for a given write in reg *)
-let rec affect_symb_mem reg insta pot_rep stype =
+let rec affect_symb_mem reg insta pot_rep stype rev =
   match pot_rep with
   | [] -> []
   | h0 :: t0 -> (
       match (insta.(h0), stype) with
       | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd), ADimm (b, n))), "ldrw" ->
-          if dreg_eq reg (IR b) then affect_symb_mem reg insta t0 stype
-          else h0 :: affect_symb_mem reg insta t0 stype
+          if verify_load_affect reg rd b rev then affect_symb_mem reg insta t0 stype rev
+          else h0 :: affect_symb_mem reg insta t0 stype rev
       | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd), ADimm (b, n))), "ldrx" ->
-          if dreg_eq reg (IR b) then affect_symb_mem reg insta t0 stype
-          else h0 :: affect_symb_mem reg insta t0 stype
+          if verify_load_affect reg rd b rev then affect_symb_mem reg insta t0 stype rev
+          else h0 :: affect_symb_mem reg insta t0 stype rev
       | PStore (PSt_rs_a (Pstrw, IR (RR1 rs), ADimm (b, n))), "strw" ->
-          if dreg_eq reg (IR b) || dreg_eq reg (dreg_of_ireg rs) then
-            affect_symb_mem reg insta t0 stype
-          else h0 :: affect_symb_mem reg insta t0 stype
+          if verify_store_affect reg rs b rev then
+            affect_symb_mem reg insta t0 stype rev
+          else h0 :: affect_symb_mem reg insta t0 stype rev
       | PStore (PSt_rs_a (Pstrx, IR (RR1 rs), ADimm (b, n))), "strx" ->
-          if dreg_eq reg (IR b) || dreg_eq reg (dreg_of_ireg rs) then
-            affect_symb_mem reg insta t0 stype
-          else h0 :: affect_symb_mem reg insta t0 stype
+          if verify_store_affect reg rs b rev then
+            affect_symb_mem reg insta t0 stype rev
+          else h0 :: affect_symb_mem reg insta t0 stype rev
       | _, _ ->
           failwith "affect_symb_mem: Found an inconsistent inst in pot_rep")
 
 (* Affect a symbolic memory list of potential replacements
  * for a given read in reg *)
-let rec read_symb_mem reg insta pot_rep stype =
+let rec read_symb_mem reg insta pot_rep stype rev =
   match pot_rep with
   | [] -> []
   | h0 :: t0 -> (
       match (insta.(h0), stype) with
       | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd), ADimm (b, n))), "ldrw" ->
-          if dreg_eq reg (IR (RR1 rd)) then read_symb_mem reg insta t0 stype
-          else h0 :: read_symb_mem reg insta t0 stype
+          if verify_load_read reg rd b rev then read_symb_mem reg insta t0 stype rev
+          else h0 :: read_symb_mem reg insta t0 stype rev
       | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd), ADimm (b, n))), "ldrx" ->
-          if dreg_eq reg (IR (RR1 rd)) then read_symb_mem reg insta t0 stype
-          else h0 :: read_symb_mem reg insta t0 stype
+          if verify_load_read reg rd b rev then read_symb_mem reg insta t0 stype rev
+          else h0 :: read_symb_mem reg insta t0 stype rev
       | PStore (PSt_rs_a (Pstrw, IR (RR1 rs), ADimm (b, n))), "strw" ->
-          h0 :: affect_symb_mem reg insta t0 stype
+          h0 :: affect_symb_mem reg insta t0 stype rev
       | PStore (PSt_rs_a (Pstrx, IR (RR1 rs), ADimm (b, n))), "strx" ->
-          h0 :: affect_symb_mem reg insta t0 stype
+          h0 :: affect_symb_mem reg insta t0 stype rev
       | _, _ -> failwith "read_symb_mem: Found an inconsistent inst in pot_rep")
 
-let update_pot_rep_addressing a insta pot_rep stype =
+(* Update a symbolic memory list of potential replacements
+ * for any addressing *)
+let update_pot_rep_addressing a insta pot_rep stype rev =
   match a with
-  | ADimm (base, _) -> pot_rep := read_symb_mem (IR base) insta !pot_rep stype
+  | ADimm (base, _) -> pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev
   | ADreg (base, r) ->
-      pot_rep := read_symb_mem (IR base) insta !pot_rep stype;
-      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype
+      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev;
+      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype rev
   | ADlsl (base, r, _) ->
-      pot_rep := read_symb_mem (IR base) insta !pot_rep stype;
-      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype
+      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev;
+      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype rev
   | ADsxt (base, r, _) ->
-      pot_rep := read_symb_mem (IR base) insta !pot_rep stype;
-      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype
+      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev;
+      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype rev
   | ADuxt (base, r, _) ->
-      pot_rep := read_symb_mem (IR base) insta !pot_rep stype;
-      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype
+      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev;
+      pot_rep := read_symb_mem (dreg_of_ireg r) insta !pot_rep stype rev
   | ADadr (base, _, _) ->
-      pot_rep := read_symb_mem (IR base) insta !pot_rep stype
+      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev
   | ADpostincr (base, _) ->
-      pot_rep := read_symb_mem (IR base) insta !pot_rep stype
+      pot_rep := read_symb_mem (IR base) insta !pot_rep stype rev
 
 (* Update a symbolic memory list of potential replacements
  * for any basic instruction *)
-let update_pot_rep_basic inst insta pot_rep stype =
+let update_pot_rep_basic inst insta pot_rep stype rev =
   match inst with
   | PArith i -> (
       match i with
-      | PArithP (_, rd) -> pot_rep := affect_symb_mem rd insta !pot_rep stype
+      | PArithP (_, rd) -> pot_rep := affect_symb_mem rd insta !pot_rep stype rev
       | PArithPP (_, rd, rs) ->
-          pot_rep := affect_symb_mem rd insta !pot_rep stype;
-          pot_rep := read_symb_mem rs insta !pot_rep stype
+          pot_rep := affect_symb_mem rd insta !pot_rep stype rev;
+          pot_rep := read_symb_mem rs insta !pot_rep stype rev
       | PArithPPP (_, rd, rs1, rs2) ->
-          pot_rep := affect_symb_mem rd insta !pot_rep stype;
-          pot_rep := read_symb_mem rs1 insta !pot_rep stype;
-          pot_rep := read_symb_mem rs2 insta !pot_rep stype
+          pot_rep := affect_symb_mem rd insta !pot_rep stype rev;
+          pot_rep := read_symb_mem rs1 insta !pot_rep stype rev;
+          pot_rep := read_symb_mem rs2 insta !pot_rep stype rev
       | PArithRR0R (_, rd, rs1, rs2) ->
-          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype;
+          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
           (match rs1 with
           | RR0 rs1 ->
-              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype
+              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev
           | _ -> ());
-          pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype
+          pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype rev
       | PArithRR0 (_, rd, rs) -> (
-          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype;
+          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
           match rs with
           | RR0 rs1 ->
-              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype
+              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev
           | _ -> ())
       | PArithARRRR0 (_, rd, rs1, rs2, rs3) -> (
-          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype;
-          pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype;
-          pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype;
+          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
+          pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev;
+          pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype rev;
           match rs3 with
           | RR0 rs1 ->
-              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype
+              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev
           | _ -> ())
       | PArithComparisonPP (_, rs1, rs2) ->
-          pot_rep := read_symb_mem rs1 insta !pot_rep stype;
-          pot_rep := read_symb_mem rs2 insta !pot_rep stype
+          pot_rep := read_symb_mem rs1 insta !pot_rep stype rev;
+          pot_rep := read_symb_mem rs2 insta !pot_rep stype rev
       | PArithComparisonR0R (_, rs1, rs2) ->
           (match rs1 with
           | RR0 rs1 ->
-              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype
+              pot_rep := read_symb_mem (dreg_of_ireg rs1) insta !pot_rep stype rev
           | _ -> ());
-          pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype
+          pot_rep := read_symb_mem (dreg_of_ireg rs2) insta !pot_rep stype rev
       | PArithComparisonP (_, rs1) ->
-          pot_rep := read_symb_mem rs1 insta !pot_rep stype
+          pot_rep := read_symb_mem rs1 insta !pot_rep stype rev
       | Pcset (rd, _) ->
-          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype
+          pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev
       | Pfmovi (_, _, rs) -> (
           match rs with
           | RR0 rs ->
-              pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype
+              pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype rev
           | _ -> ())
       | Pcsel (rd, rs1, rs2, _) ->
-          pot_rep := affect_symb_mem rd insta !pot_rep stype;
-          pot_rep := read_symb_mem rs1 insta !pot_rep stype;
-          pot_rep := read_symb_mem rs2 insta !pot_rep stype
+          pot_rep := affect_symb_mem rd insta !pot_rep stype rev;
+          pot_rep := read_symb_mem rs1 insta !pot_rep stype rev;
+          pot_rep := read_symb_mem rs2 insta !pot_rep stype rev
       | Pfnmul (_, rd, rs1, rs2) -> ())
   | PLoad i -> (
       match stype with
       | "ldrw" | "ldrx" -> (
           match i with
           | PLd_rd_a (_, rd, a) ->
-              pot_rep := affect_symb_mem rd insta !pot_rep stype;
-              update_pot_rep_addressing a insta pot_rep stype
+              pot_rep := affect_symb_mem rd insta !pot_rep stype rev;
+              update_pot_rep_addressing a insta pot_rep stype rev
           | Pldp (_, rd1, rd2, a) ->
-              pot_rep := affect_symb_mem (dreg_of_ireg rd1) insta !pot_rep stype;
-              pot_rep := affect_symb_mem (dreg_of_ireg rd2) insta !pot_rep stype;
-              update_pot_rep_addressing a insta pot_rep stype)
+              pot_rep := affect_symb_mem (dreg_of_ireg rd1) insta !pot_rep stype rev;
+              pot_rep := affect_symb_mem (dreg_of_ireg rd2) insta !pot_rep stype rev;
+              update_pot_rep_addressing a insta pot_rep stype rev)
       | _ -> pot_rep := [])
   | PStore _ -> pot_rep := []
   | Pallocframe (_, _) -> pot_rep := []
   | Pfreeframe (_, _) -> pot_rep := []
   | Ploadsymbol (rd, _) ->
-      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype
+      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev
   | Pcvtsw2x (rd, rs) ->
-      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype;
-      pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype
+      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
+      pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype rev
   | Pcvtuw2x (rd, rs) ->
-      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype;
-      pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype
+      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
+      pot_rep := read_symb_mem (dreg_of_ireg rs) insta !pot_rep stype rev
   | Pcvtx2w rd ->
-      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype;
-      pot_rep := read_symb_mem (dreg_of_ireg rd) insta !pot_rep stype
+      pot_rep := affect_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev;
+      pot_rep := read_symb_mem (dreg_of_ireg rd) insta !pot_rep stype rev
   | Pnop -> ()
 
 (* Try to find the index of the first previous compatible
@@ -235,6 +263,28 @@ let rec search_compat_rep r2 b2 n2 insta pot_rep stype =
       | _, _ ->
           failwith "search_compat_rep: Found an inconsistent inst in pot_rep")
 
+(* Try to find the index of the first previous compatible
+ * replacement in a given symbolic memory (when iterating in the reversed list) *)
+let rec search_compat_rep_inv r2 b2 n2 insta pot_rep stype =
+  match pot_rep with
+  | [] -> None
+  | h0 :: t0 -> (
+      match (insta.(h0), stype) with
+      | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))), "ldrw" ->
+          if is_valid_ldrw r2 rd1 b2 b1 n2 n1 then Some (h0, rd1, b1, n1)
+          else search_compat_rep_inv r2 b2 n2 insta t0 stype
+      | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd1), ADimm (b1, n1))), "ldrx" ->
+          if is_valid_ldrx r2 rd1 b2 b1 n2 n1 then Some (h0, rd1, b1, n1)
+          else search_compat_rep_inv r2 b2 n2 insta t0 stype
+      | PStore (PSt_rs_a (Pstrw, IR (RR1 rs1), ADimm (b1, n1))), "strw" ->
+          if is_valid_strw b2 b1 n2 n1 then Some (h0, rs1, b1, n1)
+          else search_compat_rep_inv r2 b2 n2 insta t0 stype
+      | PStore (PSt_rs_a (Pstrx, IR (RR1 rs1), ADimm (b1, n1))), "strx" ->
+          if is_valid_strx b2 b1 n2 n1 then Some (h0, rs1, b1, n1)
+          else search_compat_rep_inv r2 b2 n2 insta t0 stype
+      | _, _ ->
+          failwith "search_compat_rep_inv: Found an inconsistent inst in pot_rep")
+
 (* This is useful to manage the case were the immofs
  * of the first ldr/str is greater than the second one *)
 let min_is_rev n1 n2 =
@@ -242,7 +292,81 @@ let min_is_rev n1 n2 =
   let z2 = to_int (camlint64_of_coqint n2) in
   if z1 < z2 then true else false
 
-(* Main peephole function *)
+(* Main peephole function in backward style *)
+let pair_rep_inv insta =
+  (* Each list below is a symbolic mem representation
+   * for one type of inst. Lists contains integers which
+   * are the indices of insts in the main array "insta". *)
+  let pot_ldrw_rep = ref [] in
+  let pot_ldrx_rep = ref [] in
+  let pot_strw_rep = ref [] in
+  let pot_strx_rep = ref [] in
+  for i = Array.length insta - 1 downto 1 do
+    let h0 = insta.(i) in
+    let h1 = insta.(i - 1) in
+    (* Here we need to update every symbolic memory according to the matched inst *)
+    update_pot_rep_basic h0 insta pot_ldrw_rep "ldrw" true;
+    update_pot_rep_basic h0 insta pot_ldrx_rep "ldrx" true;
+    update_pot_rep_basic h0 insta pot_strw_rep "strw" true;
+    update_pot_rep_basic h0 insta pot_strx_rep "strx" true;
+    match (h0, h1) with
+    (* Non-consecutive ldrw *)
+    | PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))), _ -> (
+        (* Search a previous compatible load *)
+        match search_compat_rep_inv rd1 b1 n1 insta !pot_ldrw_rep "ldrw" with
+        (* If we can't find a candidate, add the current load as a potential future one *)
+        | None -> pot_ldrw_rep := i :: !pot_ldrw_rep
+        (* Else, perform the peephole *)
+        | Some (rep, r, b, n) ->
+            (* The two lines below are used to filter the elected candidate *)
+            let filt x = x != rep in
+            pot_ldrw_rep := List.filter filt !pot_ldrw_rep;
+            insta.(rep) <- Pnop;
+            if min_is_rev n n1 then (
+              if debug then eprintf "LDP_W_BACK_SPACED_PEEP_IMM_INC\n";
+              insta.(i) <- PLoad (Pldp (Pldpw, r, rd1, ADimm (b, n))))
+            else (
+              if debug then eprintf "LDP_W_BACK_SPACED_PEEP_IMM_DEC\n";
+              insta.(i) <- PLoad (Pldp (Pldpw, rd1, r, ADimm (b, n1)))))
+    (* Non-consecutive ldrx *)
+    | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd1), ADimm (b1, n1))), _ -> (
+        match search_compat_rep_inv rd1 b1 n1 insta !pot_ldrx_rep "ldrx" with
+        | None -> pot_ldrx_rep := i :: !pot_ldrx_rep
+        | Some (rep, r, b, n) ->
+            let filt x = x != rep in
+            pot_ldrx_rep := List.filter filt !pot_ldrx_rep;
+            insta.(rep) <- Pnop;
+            if min_is_rev n n1 then (
+              if debug then eprintf "LDP_X_BACK_SPACED_PEEP_IMM_INC\n";
+              insta.(i) <- PLoad (Pldp (Pldpx, r, rd1, ADimm (b, n))))
+            else (
+              if debug then eprintf "LDP_X_BACK_SPACED_PEEP_IMM_DEC\n";
+              insta.(i) <- PLoad (Pldp (Pldpx, rd1, r, ADimm (b, n1)))))
+    (* Non-consecutive stpw *)
+    | PStore (PSt_rs_a (Pstrw, IR (RR1 rs1), ADimm (b1, n1))), _ -> (
+        match search_compat_rep_inv rs1 b1 n1 insta !pot_strw_rep "strw" with
+        | None -> pot_strw_rep := i :: !pot_strw_rep
+        | Some (rep, r, b, n) ->
+            let filt x = x != rep in
+            pot_strw_rep := List.filter filt !pot_strw_rep;
+            insta.(rep) <- Pnop;
+            if debug then eprintf "STP_W_BACK_SPACED_PEEP_IMM_INC\n";
+            insta.(i) <- PStore (Pstp (Pstpw, r, rs1, ADimm (b, n))))
+    (* Non-consecutive stpx *)
+    | PStore (PSt_rs_a (Pstrx, IR (RR1 rs1), ADimm (b1, n1))), _ -> (
+        match search_compat_rep_inv rs1 b1 n1 insta !pot_strx_rep "strx" with
+        | None -> pot_strx_rep := i :: !pot_strx_rep
+        | Some (rep, r, b, n) ->
+            let filt x = x != rep in
+            pot_strx_rep := List.filter filt !pot_strx_rep;
+            insta.(rep) <- Pnop;
+            if debug then eprintf "STP_X_BACK_SPACED_PEEP_IMM_INC\n";
+            insta.(i) <- PStore (Pstp (Pstpx, r, rs1, ADimm (b, n))))
+    (* Any other inst *)
+    | _, _ -> ()
+  done
+
+(* Main peephole function in forward style *)
 let pair_rep insta =
   (* Each list below is a symbolic mem representation
    * for one type of inst. Lists contains integers which
@@ -255,10 +379,10 @@ let pair_rep insta =
     let h0 = insta.(i) in
     let h1 = insta.(i + 1) in
     (* Here we need to update every symbolic memory according to the matched inst *)
-    update_pot_rep_basic h0 insta pot_ldrw_rep "ldrw";
-    update_pot_rep_basic h0 insta pot_ldrx_rep "ldrx";
-    update_pot_rep_basic h0 insta pot_strw_rep "strw";
-    update_pot_rep_basic h0 insta pot_strx_rep "strx";
+    update_pot_rep_basic h0 insta pot_ldrw_rep "ldrw" false;
+    update_pot_rep_basic h0 insta pot_ldrx_rep "ldrx" false;
+    update_pot_rep_basic h0 insta pot_strw_rep "strw" false;
+    update_pot_rep_basic h0 insta pot_strx_rep "strx" false;
     match (h0, h1) with
     (* Consecutive ldrw *)
     | ( PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))),
@@ -270,10 +394,10 @@ let pair_rep insta =
           (* When two consec mem addr are loading two different dest. *))
         else if is_valid_ldrw rd1 rd2 b1 b2 n1 n2 then (
           if min_is_rev n1 n2 then (
-            if debug then eprintf "LDP_W_CONSEC_PEEP_FORWARD\n";
+            if debug then eprintf "LDP_W_CONSEC_PEEP_IMM_INC\n";
             insta.(i) <- PLoad (Pldp (Pldpw, rd1, rd2, ADimm (b1, n1))))
           else (
-            if debug then eprintf "LDP_W_CONSEC_PEEP_BACKWARD\n";
+            if debug then eprintf "LDP_W_CONSEC_PEEP_IMM_DEC\n";
             insta.(i) <- PLoad (Pldp (Pldpw, rd2, rd1, ADimm (b1, n2))));
           insta.(i + 1) <- Pnop)
     (* Consecutive ldrx *)
@@ -284,10 +408,10 @@ let pair_rep insta =
           insta.(i) <- Pnop)
         else if is_valid_ldrx rd1 rd2 b1 b2 n1 n2 then (
           if min_is_rev n1 n2 then (
-            if debug then eprintf "LDP_X_CONSEC_PEEP_FORWARD\n";
+            if debug then eprintf "LDP_X_CONSEC_PEEP_IMM_INC\n";
             insta.(i) <- PLoad (Pldp (Pldpx, rd1, rd2, ADimm (b1, n1))))
           else (
-            if debug then eprintf "LDP_X_CONSEC_PEEP_BACKWARD\n";
+            if debug then eprintf "LDP_X_CONSEC_PEEP_IMM_DEC\n";
             insta.(i) <- PLoad (Pldp (Pldpx, rd2, rd1, ADimm (b1, n2))));
           insta.(i + 1) <- Pnop)
     (* Non-consecutive ldrw *)
@@ -303,10 +427,10 @@ let pair_rep insta =
             pot_ldrw_rep := List.filter filt !pot_ldrw_rep;
             insta.(rep) <- Pnop;
             if min_is_rev n n1 then (
-              if debug then eprintf "LDP_W_SPACED_PEEP_FORWARD\n";
+              if debug then eprintf "LDP_W_FORW_SPACED_PEEP_IMM_INC\n";
               insta.(i) <- PLoad (Pldp (Pldpw, r, rd1, ADimm (b, n))))
             else (
-              if debug then eprintf "LDP_W_SPACED_PEEP_BACKWARD\n";
+              if debug then eprintf "LDP_W_FORW_SPACED_PEEP_IMM_DEC\n";
               insta.(i) <- PLoad (Pldp (Pldpw, rd1, r, ADimm (b, n1)))))
     (* Non-consecutive ldrx *)
     | PLoad (PLd_rd_a (Pldrx, IR (RR1 rd1), ADimm (b1, n1))), _ -> (
@@ -317,10 +441,10 @@ let pair_rep insta =
             pot_ldrx_rep := List.filter filt !pot_ldrx_rep;
             insta.(rep) <- Pnop;
             if min_is_rev n n1 then (
-              if debug then eprintf "LDP_X_SPACED_PEEP_FORWARD\n";
+              if debug then eprintf "LDP_X_FORW_SPACED_PEEP_IMM_INC\n";
               insta.(i) <- PLoad (Pldp (Pldpx, r, rd1, ADimm (b, n))))
             else (
-              if debug then eprintf "LDP_X_SPACED_PEEP_BACKWARD\n";
+              if debug then eprintf "LDP_X_FORW_SPACED_PEEP_IMM_DEC\n";
               insta.(i) <- PLoad (Pldp (Pldpx, rd1, r, ADimm (b, n1)))))
     (* Consecutive strw *)
     | ( PStore (PSt_rs_a (Pstrw, IR (RR1 rs1), ADimm (b1, n1))),
@@ -331,7 +455,7 @@ let pair_rep insta =
           (* When two consec mem addr are targeted by two store. *)
              else*)
         if is_valid_strw b1 b2 n1 n2 then (
-          if debug then eprintf "STP_W_CONSEC_PEEP_FORWARD\n";
+          if debug then eprintf "STP_W_CONSEC_PEEP_IMM_INC\n";
           insta.(i) <- PStore (Pstp (Pstpw, rs1, rs2, ADimm (b1, n1)));
           insta.(i + 1) <- Pnop (* When nothing can be optimized. *))
     (* Consecutive strx *)
@@ -341,7 +465,7 @@ let pair_rep insta =
           Pnop :: (pair_rep insta t0)
            else*)
         if is_valid_strx b1 b2 n1 n2 then (
-          if debug then eprintf "STP_X_CONSEC_PEEP_FORWARD\n";
+          if debug then eprintf "STP_X_CONSEC_PEEP_IMM_INC\n";
           insta.(i) <- PStore (Pstp (Pstpx, rs1, rs2, ADimm (b1, n1)));
           insta.(i + 1) <- Pnop)
     (* Non-consecutive stpw *)
@@ -352,7 +476,7 @@ let pair_rep insta =
             let filt x = x != rep in
             pot_strw_rep := List.filter filt !pot_strw_rep;
             insta.(rep) <- Pnop;
-            if debug then eprintf "STP_W_SPACED_PEEP_FORWARD\n";
+            if debug then eprintf "STP_W_FORW_SPACED_PEEP_IMM_INC\n";
             insta.(i) <- PStore (Pstp (Pstpw, r, rs1, ADimm (b, n))))
     (* Non-consecutive stpx *)
     | PStore (PSt_rs_a (Pstrx, IR (RR1 rs1), ADimm (b1, n1))), _ -> (
@@ -362,7 +486,7 @@ let pair_rep insta =
             let filt x = x != rep in
             pot_strx_rep := List.filter filt !pot_strx_rep;
             insta.(rep) <- Pnop;
-            if debug then eprintf "STP_X_SPACED_PEEP_FORWARD\n";
+            if debug then eprintf "STP_X_FORW_SPACED_PEEP_IMM_INC\n";
             insta.(i) <- PStore (Pstp (Pstpx, r, rs1, ADimm (b, n))))
     (* Any other inst *)
     | _, _ -> ()
@@ -373,6 +497,7 @@ let optimize_bdy (bdy : basic list) : basic list =
   if !Clflags.option_fcoalesce_mem then (
     let insta = Array.of_list bdy in
     pair_rep insta;
+    pair_rep_inv insta;
     Array.to_list insta)
   else bdy