Allowing non-consec store, and cleaning

1 files changed, 41 insertions, 8 deletions

diff --git a/aarch64/PeepholeOracle.ml b/aarch64/PeepholeOracle.ml
index 65c820ac..a6945b9f 100644
--- a/aarch64/PeepholeOracle.ml
+++ b/aarch64/PeepholeOracle.ml
@@ -16,6 +16,7 @@ open Asm
 open Int64
 open Printf
 
+(* If true, the oracle will print a msg for each applied peephole *)
 let debug = false
 
 (* Functions to verify the immediate offset range for ldp/stp *)
@@ -208,6 +209,8 @@ let update_pot_rep_basic inst insta pot_rep stype rev =
           pot_rep := read_symb_mem rs2 insta !pot_rep stype rev
       | Pfnmul (_, rd, rs1, rs2) -> ())
   | 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" -> (
           match i with
@@ -221,7 +224,11 @@ let update_pot_rep_basic inst insta pot_rep stype rev =
                 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 := []
+  | 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 := [] | _ -> ())
   | Pallocframe (_, _) -> pot_rep := []
   | Pfreeframe (_, _) -> pot_rep := []
   | Ploadsymbol (rd, _) ->
@@ -297,6 +304,8 @@ let min_is_rev n1 n2 =
   let z2 = to_int (camlint64_of_coqint n2) in
   if z1 < z2 then true else false
 
+(* Below functions were added to merge pattern matching cases in peephole,
+ * thanks to this, we can make the chunk difference (int/any) compatible. *)
 let trans_ldi (ldi : load_rd_a) : load_rd1_rd2_a =
   match ldi with
   | Pldrw | Pldrw_a -> Pldpw
@@ -409,8 +418,11 @@ let pair_rep_inv insta =
             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
+          (* 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_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 *)
@@ -420,9 +432,16 @@ let pair_rep_inv insta =
               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)))
+                  (Pstp
+                     (trans_sti sti, rd1, r, chunk_store sti, c, ADimm (b, n1)))
           (* Any other inst *))
-    | _, _ -> ()
+    | i, _ -> (
+        (* Clear list of candidates if there is a non supported store *)
+        match i with
+        | PStore _ ->
+            pot_strw_rep := [];
+            pot_strx_rep := []
+        | _ -> ())
   done
 
 (* Main peephole function in forward style *)
@@ -505,6 +524,11 @@ let pair_rep insta =
     (* Consecutive str *)
     | ( PStore (PSt_rs_a (sti1, IR (RR1 rd1), ADimm (b1, n1))),
         PStore (PSt_rs_a (sti2, IR (RR1 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 := [];
         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";
@@ -528,8 +552,11 @@ let pair_rep insta =
           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
+          (* 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_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 *)
@@ -542,7 +569,13 @@ let pair_rep insta =
                   (Pstp (trans_sti sti, r, rd1, c, chunk_store sti, ADimm (b, n)))
         )
     (* Any other inst *)
-    | _, _ -> ()
+    | i, _ -> (
+        (* Clear list of candidates if there is a non supported store *)
+        match i with
+        | PStore _ ->
+            pot_strw_rep := [];
+            pot_strx_rep := []
+        | _ -> ())
   done
 
 (* Calling peephole if flag is set *)