Big improvment in peephole, changing LDP/STP semantics

1 files changed, 69 insertions, 124 deletions

diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml
index e233f77d..d7fab1de 100644
--- a/aarch64/PostpassSchedulingOracle.ml
+++ b/aarch64/PostpassSchedulingOracle.ml
@@ -18,6 +18,7 @@ open OpWeightsAsm
 open InstructionScheduler
 
 let debug = false
+
 let stats = false
 
 (**
@@ -73,47 +74,22 @@ let arith_p_rec i i' rd =
   }
 
 let arith_pp_rec i rd rs =
-  {
-    inst = i;
-    write_locs = [ rd ];
-    read_locs = [ rs ];
-    is_control = false;
-  }
+  { inst = i; write_locs = [ rd ]; read_locs = [ rs ]; is_control = false }
 
 let arith_ppp_rec i rd r1 r2 =
-  {
-    inst = i;
-    write_locs = [ rd ];
-    read_locs = [ r1; r2 ];
-    is_control = false;
-  }
+  { inst = i; write_locs = [ rd ]; read_locs = [ r1; r2 ]; is_control = false }
 
 let arith_rr0r_rec i rd r1 r2 =
   let rlocs = if is_XZR r1 then [ r2 ] else [ r1; r2 ] in
-  {
-    inst = i;
-    write_locs = [ rd ];
-    read_locs = rlocs;
-    is_control = false;
-  }
+  { inst = i; write_locs = [ rd ]; read_locs = rlocs; is_control = false }
 
 let arith_rr0_rec i rd r1 =
   let rlocs = if is_XZR r1 then [] else [ r1 ] in
-  {
-    inst = i;
-    write_locs = [ rd ];
-    read_locs = rlocs;
-    is_control = false;
-  }
+  { inst = i; write_locs = [ rd ]; read_locs = rlocs; is_control = false }
 
 let arith_arrrr0_rec i rd r1 r2 r3 =
   let rlocs = if is_XZR r3 then [ r1; r2 ] else [ r1; r2; r3 ] in
-  {
-    inst = i;
-    write_locs = [ rd ];
-    read_locs = rlocs;
-    is_control = false;
-  }
+  { inst = i; write_locs = [ rd ]; read_locs = rlocs; is_control = false }
 
 let arith_comparison_pp_rec i r1 r2 =
   {
@@ -125,20 +101,10 @@ let arith_comparison_pp_rec i r1 r2 =
 
 let arith_comparison_r0r_rec i r1 r2 =
   let rlocs = if is_XZR r1 then [ r2 ] else [ r1; r2 ] in
-  {
-    inst = i;
-    write_locs = flags_wlocs;
-    read_locs = rlocs;
-    is_control = false;
-  }
+  { inst = i; write_locs = flags_wlocs; read_locs = rlocs; is_control = false }
 
 let arith_comparison_p_rec i r1 =
-  {
-    inst = i;
-    write_locs = flags_wlocs;
-    read_locs = [ r1 ];
-    is_control = false;
-  }
+  { inst = i; write_locs = flags_wlocs; read_locs = [ r1 ]; is_control = false }
 
 let get_eval_addressing_rlocs a =
   match a with
@@ -168,8 +134,11 @@ let load_rd1_rd2_a_rec ld rd1 rd2 a =
 
 let load_rec ldi =
   match ldi with
-  | PLd_rd_a (ld, rd, a) -> load_rd_a_rec (PBasic (PLoad ldi)) (reg_of_dreg rd) a
-  | Pldp (ld, rd1, rd2, a) -> load_rd1_rd2_a_rec (PBasic (PLoad ldi)) (reg_of_ireg rd1) (reg_of_ireg rd2) a
+  | PLd_rd_a (ld, rd, a) ->
+      load_rd_a_rec (PBasic (PLoad ldi)) (reg_of_dreg rd) a
+  | Pldp (ld, rd1, rd2, _, _, a) ->
+      load_rd1_rd2_a_rec (PBasic (PLoad ldi)) (reg_of_ireg rd1)
+        (reg_of_ireg rd2) a
 
 let store_rs_a_rec st rs a =
   {
@@ -189,40 +158,23 @@ let store_rs1_rs2_a_rec st rs1 rs2 a =
 
 let store_rec sti =
   match sti with
-  | PSt_rs_a (st, rs, a) -> store_rs_a_rec (PBasic (PStore sti)) (reg_of_dreg rs) a
-  | Pstp (st, rs1, rs2, a) -> store_rs1_rs2_a_rec (PBasic (PStore sti)) (reg_of_ireg rs1) (reg_of_ireg rs2) a 
+  | PSt_rs_a (st, rs, a) ->
+      store_rs_a_rec (PBasic (PStore sti)) (reg_of_dreg rs) a
+  | Pstp (st, rs1, rs2, _, _, a) ->
+      store_rs1_rs2_a_rec (PBasic (PStore sti)) (reg_of_ireg rs1)
+        (reg_of_ireg rs2) a
 
 let loadsymbol_rec i rd id =
-  {
-    inst = i;
-    write_locs = [ rd ];
-    read_locs = [ Mem ];
-    is_control = false;
-  }
+  { inst = i; write_locs = [ rd ]; read_locs = [ Mem ]; is_control = false }
 
 let cvtsw2x_rec i rd r1 =
-  {
-    inst = i;
-    write_locs = [ rd ];
-    read_locs = [ r1 ];
-    is_control = false;
-  }
+  { inst = i; write_locs = [ rd ]; read_locs = [ r1 ]; is_control = false }
 
 let cvtuw2x_rec i rd r1 =
-  {
-    inst = i;
-    write_locs = [ rd ];
-    read_locs = [ r1 ];
-    is_control = false;
-  }
+  { inst = i; write_locs = [ rd ]; read_locs = [ r1 ]; is_control = false }
 
 let cvtx2w_rec i rd =
-  {
-    inst = i;
-    write_locs = [ rd ];
-    read_locs = [ rd ];
-    is_control = false;
-  }
+  { inst = i; write_locs = [ rd ]; read_locs = [ rd ]; is_control = false }
 
 let get_testcond_rlocs c =
   match c with
@@ -257,20 +209,10 @@ let csel_rec i rd r1 r2 c =
 
 let fmovi_rec i fsz rd r1 =
   let rlocs = if is_XZR r1 then [] else [ r1 ] in
-  {
-    inst = i;
-    write_locs = [ rd ];
-    read_locs = rlocs;
-    is_control = false;
-  }
+  { inst = i; write_locs = [ rd ]; read_locs = rlocs; is_control = false }
 
 let fnmul_rec i fsz rd r1 r2 =
-  {
-    inst = i;
-    write_locs = [ rd ];
-    read_locs = [ r1; r2 ];
-    is_control = false;
-  }
+  { inst = i; write_locs = [ rd ]; read_locs = [ r1; r2 ]; is_control = false }
 
 let allocframe_rec i sz linkofs =
   {
@@ -289,37 +231,41 @@ let freeframe_rec i sz linkofs =
   }
 
 let nop_rec i =
-  {
-    inst = i;
-    write_locs = [ ];
-    read_locs = [ ];
-    is_control = false;
-  }
+  { inst = i; write_locs = []; read_locs = []; is_control = false }
 
 let arith_rec i =
   match i with
   | PArithP (i', rd) -> arith_p_rec (PBasic (PArith i)) i' (reg_of_dreg rd)
-  | PArithPP (i', rd, rs) -> arith_pp_rec (PBasic (PArith i)) (reg_of_dreg rd) (reg_of_dreg rs)
+  | PArithPP (i', rd, rs) ->
+      arith_pp_rec (PBasic (PArith i)) (reg_of_dreg rd) (reg_of_dreg rs)
   | PArithPPP (i', rd, r1, r2) ->
-      arith_ppp_rec (PBasic (PArith i)) (reg_of_dreg rd) (reg_of_dreg r1) (reg_of_dreg r2)
+      arith_ppp_rec (PBasic (PArith i)) (reg_of_dreg rd) (reg_of_dreg r1)
+        (reg_of_dreg r2)
   | PArithRR0R (i', rd, r1, r2) ->
-      arith_rr0r_rec (PBasic (PArith i)) (reg_of_ireg rd) (reg_of_ireg0 r1) (reg_of_ireg r2)
+      arith_rr0r_rec (PBasic (PArith i)) (reg_of_ireg rd) (reg_of_ireg0 r1)
+        (reg_of_ireg r2)
   | PArithRR0 (i', rd, r1) ->
       arith_rr0_rec (PBasic (PArith i)) (reg_of_ireg rd) (reg_of_ireg0 r1)
   | PArithARRRR0 (i', rd, r1, r2, r3) ->
-      arith_arrrr0_rec (PBasic (PArith i)) (reg_of_ireg rd) (reg_of_ireg r1) (reg_of_ireg r2)
-        (reg_of_ireg0 r3)
+      arith_arrrr0_rec (PBasic (PArith i)) (reg_of_ireg rd) (reg_of_ireg r1)
+        (reg_of_ireg r2) (reg_of_ireg0 r3)
   | PArithComparisonPP (i', r1, r2) ->
-      arith_comparison_pp_rec (PBasic (PArith i)) (reg_of_dreg r1) (reg_of_dreg r2)
+      arith_comparison_pp_rec (PBasic (PArith i)) (reg_of_dreg r1)
+        (reg_of_dreg r2)
   | PArithComparisonR0R (i', r1, r2) ->
-      arith_comparison_r0r_rec (PBasic (PArith i)) (reg_of_ireg0 r1) (reg_of_ireg r2)
-  | PArithComparisonP (i', r1) -> arith_comparison_p_rec (PBasic (PArith i)) (reg_of_dreg r1)
+      arith_comparison_r0r_rec (PBasic (PArith i)) (reg_of_ireg0 r1)
+        (reg_of_ireg r2)
+  | PArithComparisonP (i', r1) ->
+      arith_comparison_p_rec (PBasic (PArith i)) (reg_of_dreg r1)
   | Pcset (rd, c) -> cset_rec (PBasic (PArith i)) (reg_of_ireg rd) c
-  | Pfmovi (fsz, rd, r1) -> fmovi_rec (PBasic (PArith i)) fsz (reg_of_freg rd) (reg_of_ireg0 r1)
+  | Pfmovi (fsz, rd, r1) ->
+      fmovi_rec (PBasic (PArith i)) fsz (reg_of_freg rd) (reg_of_ireg0 r1)
   | Pcsel (rd, r1, r2, c) ->
-      csel_rec (PBasic (PArith i)) (reg_of_dreg rd) (reg_of_dreg r1) (reg_of_dreg r2) c
+      csel_rec (PBasic (PArith i)) (reg_of_dreg rd) (reg_of_dreg r1)
+        (reg_of_dreg r2) c
   | Pfnmul (fsz, rd, r1, r2) ->
-      fnmul_rec (PBasic (PArith i)) fsz (reg_of_freg rd) (reg_of_freg r1) (reg_of_freg r2)
+      fnmul_rec (PBasic (PArith i)) fsz (reg_of_freg rd) (reg_of_freg r1)
+        (reg_of_freg r2)
 
 let basic_rec i =
   match i with
@@ -329,101 +275,98 @@ let basic_rec i =
   | Pallocframe (sz, linkofs) -> allocframe_rec (PBasic i) sz linkofs
   | Pfreeframe (sz, linkofs) -> freeframe_rec (PBasic i) sz linkofs
   | Ploadsymbol (rd, id) -> loadsymbol_rec (PBasic i) (reg_of_ireg rd) id
-  | Pcvtsw2x (rd, r1) -> cvtsw2x_rec (PBasic i) (reg_of_ireg rd) (reg_of_ireg r1)
-  | Pcvtuw2x (rd, r1) -> cvtuw2x_rec (PBasic i) (reg_of_ireg rd) (reg_of_ireg r1)
+  | Pcvtsw2x (rd, r1) ->
+      cvtsw2x_rec (PBasic i) (reg_of_ireg rd) (reg_of_ireg r1)
+  | Pcvtuw2x (rd, r1) ->
+      cvtuw2x_rec (PBasic i) (reg_of_ireg rd) (reg_of_ireg r1)
   | Pcvtx2w rd -> cvtx2w_rec (PBasic i) (reg_of_ireg rd)
   | Pnop -> nop_rec (PBasic i)
 
 let builtin_rec i ef args res =
-  {
-    inst = i;
-    write_locs = [ Mem ];
-    read_locs = [ Mem ];
-    is_control = true;
-  }
+  { inst = i; write_locs = [ Mem ]; read_locs = [ Mem ]; is_control = true }
 
 let ctl_flow_rec i =
   match i with
   | Pb lbl ->
       {
-        inst = (PControl (PCtlFlow i));
+        inst = PControl (PCtlFlow i);
         write_locs = [ reg_of_pc ];
         read_locs = [ reg_of_pc ];
         is_control = true;
       }
   | Pbc (c, lbl) ->
       {
-        inst = (PControl (PCtlFlow i));
+        inst = PControl (PCtlFlow i);
         write_locs = [ reg_of_pc ];
         read_locs = [ reg_of_pc ];
         is_control = true;
       }
   | Pbl (id, sg) ->
       {
-        inst = (PControl (PCtlFlow i));
+        inst = PControl (PCtlFlow i);
         write_locs = [ reg_of_ireg Asm.X30; reg_of_pc ];
         read_locs = [ reg_of_pc ];
         is_control = true;
       }
   | Pbs (id, sg) ->
       {
-        inst = (PControl (PCtlFlow i));
+        inst = PControl (PCtlFlow i);
         write_locs = [ reg_of_pc ];
         read_locs = [];
         is_control = true;
       }
   | Pblr (r, sg) ->
       {
-        inst = (PControl (PCtlFlow i));
+        inst = PControl (PCtlFlow i);
         write_locs = [ reg_of_ireg Asm.X30; reg_of_pc ];
         read_locs = [ reg_of_ireg r ];
         is_control = true;
       }
   | Pbr (r, sg) ->
       {
-        inst = (PControl (PCtlFlow i));
+        inst = PControl (PCtlFlow i);
         write_locs = [ reg_of_pc ];
         read_locs = [ reg_of_ireg r ];
         is_control = true;
       }
   | Pret r ->
       {
-        inst = (PControl (PCtlFlow i));
+        inst = PControl (PCtlFlow i);
         write_locs = [ reg_of_pc ];
         read_locs = [ reg_of_ireg r ];
         is_control = true;
       }
   | Pcbnz (sz, r, lbl) ->
       {
-        inst = (PControl (PCtlFlow i));
+        inst = PControl (PCtlFlow i);
         write_locs = [ reg_of_pc ];
         read_locs = [ reg_of_ireg r; reg_of_pc ];
         is_control = true;
       }
   | Pcbz (sz, r, lbl) ->
       {
-        inst = (PControl (PCtlFlow i));
+        inst = PControl (PCtlFlow i);
         write_locs = [ reg_of_pc ];
         read_locs = [ reg_of_ireg r; reg_of_pc ];
         is_control = true;
       }
   | Ptbnz (sz, r, n, lbl) ->
       {
-        inst = (PControl (PCtlFlow i));
+        inst = PControl (PCtlFlow i);
         write_locs = [ reg_of_pc ];
         read_locs = [ reg_of_ireg r; reg_of_pc ];
         is_control = true;
       }
   | Ptbz (sz, r, n, lbl) ->
       {
-        inst = (PControl (PCtlFlow i));
+        inst = PControl (PCtlFlow i);
         write_locs = [ reg_of_pc ];
         read_locs = [ reg_of_ireg r; reg_of_pc ];
         is_control = true;
       }
   | Pbtbl (r1, tbl) ->
       {
-        inst = (PControl (PCtlFlow i));
+        inst = PControl (PCtlFlow i);
         write_locs = [ reg_of_ireg Asm.X16; reg_of_ireg Asm.X17; reg_of_pc ];
         read_locs = [ reg_of_ireg r1; reg_of_pc ];
         is_control = true;
@@ -614,7 +557,7 @@ let find_max l =
     | e :: l -> (
         match f l with
         | None -> Some e
-        | Some m -> if e > m then Some e else Some m )
+        | Some m -> if e > m then Some e else Some m)
   in
   match f l with None -> raise Not_found | Some m -> m
 
@@ -625,9 +568,9 @@ let minpack_list (l : int list) =
   let rec f i = function
     | [] -> ()
     | t :: l ->
-        ( match TimeHash.find_opt timehash t with
+        (match TimeHash.find_opt timehash t with
         | None -> TimeHash.add timehash t [ i ]
-        | Some bund -> TimeHash.replace timehash t (bund @ [ i ]) );
+        | Some bund -> TimeHash.replace timehash t (bund @ [ i ]));
         f (i + 1) l
   in
   f 0 l;
@@ -684,9 +627,11 @@ let bblock_schedule bb =
   let identity_mode = not !Clflags.option_fpostpass in
   if debug && not identity_mode then (
     Printf.eprintf "###############################\n";
-    Printf.eprintf "SCHEDULING\n" );
+    Printf.eprintf "SCHEDULING\n");
   if stats then (
-    let oc = open_out_gen [Open_append; Open_creat] 0o666 "oracle_stats.csv" in
+    let oc =
+      open_out_gen [ Open_append; Open_creat ] 0o666 "oracle_stats.csv"
+    in
     Printf.fprintf oc "%d\n" (Camlcoq.Z.to_int (size bb));
     close_out oc);
   if identity_mode then pack_result bb else smart_schedule bb