Non conseq stores

1 files changed, 87 insertions, 39 deletions

diff --git a/aarch64/PeepholeOracle.ml b/aarch64/PeepholeOracle.ml
index 5e473049..8d30d803 100644
--- a/aarch64/PeepholeOracle.ml
+++ b/aarch64/PeepholeOracle.ml
@@ -33,7 +33,7 @@ let is_valid_ldrw rd1 rd2 b1 b2 n1 n2 =
     (not (ireg_eq rd1 rd2))
     && iregsp_eq b1 b2
     && (not (iregsp_eq (RR1 rd1) b2))
-    && ((z2 = z1 + 4) || (z2 = z1 - 4))
+    && (z2 = z1 + 4 || z2 = z1 - 4)
     && is_valid_immofs_32 z1
   then true
   else false
@@ -45,7 +45,7 @@ let is_valid_ldrx rd1 rd2 b1 b2 n1 n2 =
     (not (ireg_eq rd1 rd2))
     && iregsp_eq b1 b2
     && (not (iregsp_eq (RR1 rd1) b2))
-    && ((z2 = z1 + 8) || (z2 = z1 - 8))
+    && (z2 = z1 + 8 || z2 = z1 - 8)
     && is_valid_immofs_64 z1
   then true
   else false
@@ -77,6 +77,14 @@ let rec affect_symb_mem reg insta pot_rep stype =
       | 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
+      | 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
+      | 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
       | _, _ ->
           failwith "affect_symb_mem: Found an inconsistent inst in pot_rep")
 
@@ -93,12 +101,15 @@ let rec read_symb_mem reg insta pot_rep stype =
       | 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
+      | PStore (PSt_rs_a (Pstrw, IR (RR1 rs), ADimm (b, n))), "strw" ->
+          h0 :: affect_symb_mem reg insta t0 stype
+      | PStore (PSt_rs_a (Pstrx, IR (RR1 rs), ADimm (b, n))), "strx" ->
+          h0 :: affect_symb_mem reg insta t0 stype
       | _, _ -> failwith "read_symb_mem: Found an inconsistent inst in pot_rep")
 
 let update_pot_rep_addressing a insta pot_rep stype =
   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
   | 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
@@ -175,14 +186,17 @@ let update_pot_rep_basic inst insta pot_rep stype =
           pot_rep := read_symb_mem rs2 insta !pot_rep stype
       | Pfnmul (_, rd, rs1, rs2) -> ())
   | PLoad i -> (
-      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
-      | 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)
+      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
+          | 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 := [])
   | PStore _ -> pot_rep := []
   | Pallocframe (_, _) -> pot_rep := []
   | Pfreeframe (_, _) -> pot_rep := []
@@ -201,17 +215,23 @@ let update_pot_rep_basic inst insta pot_rep stype =
 
 (* Try to find the index of the first previous compatible
  * replacement in a given symbolic memory *)
-let rec search_compat_rep rd2 b2 n2 insta pot_rep stype =
+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 (Pldrw, IR (RR1 rd1), ADimm (b1, n1))), "ldrw" ->
-          if is_valid_ldrw rd1 rd2 b1 b2 n1 n2 then Some (h0, rd1, b1, n1)
-          else search_compat_rep rd2 b2 n2 insta t0 stype
+          if is_valid_ldrw rd1 r2 b1 b2 n1 n2 then Some (h0, 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 rd2 b1 b2 n1 n2 then Some (h0, rd1, b1, n1)
-          else search_compat_rep rd2 b2 n2 insta t0 stype
+          if is_valid_ldrx rd1 r2 b1 b2 n1 n2 then Some (h0, 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)
+          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)
+          else search_compat_rep r2 b2 n2 insta t0 stype
       | _, _ ->
           failwith "search_compat_rep: Found an inconsistent inst in pot_rep")
 
@@ -229,9 +249,16 @@ 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_strw_rep = ref [] in
+  let pot_strx_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 "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";
     match (h0, h1) with
     (* Consecutive ldrw *)
     | ( PLoad (PLd_rd_a (Pldrw, IR (RR1 rd1), ADimm (b1, n1))),
@@ -242,10 +269,11 @@ let pair_rep insta =
           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 debug then eprintf "LDP_WPEEP\n";
-          (if min_is_rev n1 n2 then
-            insta.(i) <- PLoad (Pldp (Pldpw, rd1, rd2, ADimm (b1, n1)))
-          else
+          if min_is_rev n1 n2 then (
+            if debug then eprintf "LDP_W_CONSEC_PEEP_FORWARD\n";
+            insta.(i) <- PLoad (Pldp (Pldpw, rd1, rd2, ADimm (b1, n1))))
+          else (
+            if debug then eprintf "LDP_W_CONSEC_PEEP_BACKWARD\n";
             insta.(i) <- PLoad (Pldp (Pldpw, rd2, rd1, ADimm (b1, n2))));
           insta.(i + 1) <- Pnop)
     (* Consecutive ldrx *)
@@ -255,10 +283,11 @@ let pair_rep insta =
           if debug then eprintf "LDP_XOPT\n";
           insta.(i) <- Pnop)
         else if is_valid_ldrx rd1 rd2 b1 b2 n1 n2 then (
-          if debug then eprintf "LDP_XPEEP\n";
-          (if min_is_rev n1 n2 then
-            insta.(i) <- PLoad (Pldp (Pldpx, rd1, rd2, ADimm (b1, n1)))
-          else
+          if min_is_rev n1 n2 then (
+            if debug then eprintf "LDP_X_CONSEC_PEEP_FORWARD\n";
+            insta.(i) <- PLoad (Pldp (Pldpx, rd1, rd2, ADimm (b1, n1))))
+          else (
+            if debug then eprintf "LDP_X_CONSEC_PEEP_BACKWARD\n";
             insta.(i) <- PLoad (Pldp (Pldpx, rd2, rd1, ADimm (b1, n2))));
           insta.(i + 1) <- Pnop)
     (* Non-consecutive ldrw *)
@@ -269,27 +298,29 @@ let pair_rep insta =
         | None -> pot_ldrw_rep := i :: !pot_ldrw_rep
         (* Else, perform the peephole *)
         | Some (rep, r, b, n) ->
-            eprintf "LDP_WCPEEP\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
-              insta.(i) <- PLoad (Pldp (Pldpw, r, rd1, ADimm (b, n)))
-            else
+            if min_is_rev n n1 then (
+              if debug then eprintf "LDP_W_SPACED_PEEP_FORWARD\n";
+              insta.(i) <- PLoad (Pldp (Pldpw, r, rd1, ADimm (b, n))))
+            else (
+              if debug then eprintf "LDP_W_SPACED_PEEP_BACKWARD\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) ->
-            eprintf "LDP_XCPEEP\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
-              insta.(i) <- PLoad (Pldp (Pldpx, r, rd1, ADimm (b, n)))
-            else
+            if min_is_rev n n1 then (
+              if debug then eprintf "LDP_X_SPACED_PEEP_FORWARD\n";
+              insta.(i) <- PLoad (Pldp (Pldpx, r, rd1, ADimm (b, n))))
+            else (
+              if debug then eprintf "LDP_X_SPACED_PEEP_BACKWARD\n";
               insta.(i) <- PLoad (Pldp (Pldpx, rd1, r, ADimm (b, n1)))))
     (* Consecutive strw *)
     | ( PStore (PSt_rs_a (Pstrw, IR (RR1 rs1), ADimm (b1, n1))),
@@ -300,7 +331,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_WPEEP\n";
+          if debug then eprintf "STP_W_CONSEC_PEEP_FORWARD\n";
           insta.(i) <- PStore (Pstp (Pstpw, rs1, rs2, ADimm (b1, n1)));
           insta.(i + 1) <- Pnop (* When nothing can be optimized. *))
     (* Consecutive strx *)
@@ -310,14 +341,31 @@ let pair_rep insta =
           Pnop :: (pair_rep insta t0)
            else*)
         if is_valid_strx b1 b2 n1 n2 then (
-          if debug then eprintf "STP_XPEEP\n";
+          if debug then eprintf "STP_X_CONSEC_PEEP_FORWARD\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_SPACED_PEEP_FORWARD\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_SPACED_PEEP_FORWARD\n";
+            insta.(i) <- PStore (Pstp (Pstpx, r, rs1, ADimm (b, n))))
     (* Any other inst *)
-    | h0, _ ->
-        (* 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"
+    | _, _ -> ()
   done
 
 (* Calling peephole if flag is set *)