Changing weights system at asmblock level instead of asm

1 files changed, 71 insertions, 240 deletions

diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml
index 9263babc..fbcdb55d 100644
--- a/aarch64/PostpassSchedulingOracle.ml
+++ b/aarch64/PostpassSchedulingOracle.ml
@@ -23,12 +23,10 @@ let debug = false
  * Extracting infos from Asm instructions
  *)
 
-type instruction = PBasic of basic | PControl of control
-
 type location = Reg of Asm.preg | Mem | IREG0_XZR
 
 type ab_inst_rec = {
-  inst : real_instruction;
+  inst : instruction;
   write_locs : location list;
   read_locs : location list;
   is_control : bool;
@@ -38,173 +36,6 @@ type ab_inst_rec = {
 
 exception OpaqueInstruction
 
-let arith_p_real = function
-  | Padrp (_, _) -> Adrp
-  | Pmovz (_, _, _) -> Movz
-  | Pmovn (_, _, _) -> Movn
-  | Pfmovimms _ ->
-      Fmov
-      (* XXX We could also use load, but Fmov may be more convenient for tuning *)
-  | Pfmovimmd _ -> Fmov
-
-let arith_pp_real = function
-  | Pmov -> Mov
-  | Pmovk (_, _, _) -> Movk
-  | Paddadr (_, _) -> Add
-  | Psbfiz (_, _, _) -> Sbfiz
-  | Psbfx (_, _, _) -> Sbfx
-  | Pubfiz (_, _, _) -> Ubfiz
-  | Pubfx (_, _, _) -> Ubfx
-  | Pfmov -> Fmov
-  | Pfcvtds -> Fcvt
-  | Pfcvtsd -> Fcvt
-  | Pfabs _ -> Fabs
-  | Pfneg _ -> Fneg
-  | Pscvtf (_, _) -> Scvtf
-  | Pucvtf (_, _) -> Ucvtf
-  | Pfcvtzs (_, _) -> Fcvtzs
-  | Pfcvtzu (_, _) -> Fcvtzu
-  | Paddimm (_, _) -> Add
-  | Psubimm (_, _) -> Sub
-
-let arith_ppp_real = function
-  | Pasrv _ -> Asr
-  | Plslv _ -> Lsl
-  | Plsrv _ -> Lsr
-  | Prorv _ -> Ror
-  | Psmulh -> Smulh
-  | Pumulh -> Umulh
-  | Psdiv _ -> Sdiv
-  | Pudiv _ -> Udiv
-  | Paddext _ -> Add
-  | Psubext _ -> Sub
-  | Pfadd _ -> Fadd
-  | Pfdiv _ -> Fdiv
-  | Pfmul _ -> Fmul
-  | Pfsub _ -> Fsub
-
-let arith_rr0r_real = function
-  | Padd (_, _) -> Add
-  | Psub (_, _) -> Sub
-  | Pand (_, _) -> And
-  | Pbic (_, _) -> Bic
-  | Peon (_, _) -> Eon
-  | Peor (_, _) -> Eor
-  | Porr (_, _) -> Orr
-  | Porn (_, _) -> Orn
-
-let arith_rr0_real = function
-  | Pandimm (_, _) -> And
-  | Peorimm (_, _) -> Eor
-  | Porrimm (_, _) -> Orr
-
-let arith_arrrr0_real = function Pmadd _ -> Madd | Pmsub _ -> Msub
-
-let arith_comparison_p_real = function
-  | Pfcmp0 _ -> Fcmp
-  | Pcmpimm (_, _) -> Cmp
-  | Pcmnimm (_, _) -> Cmn
-  | Ptstimm (_, _) -> Tst
-
-let arith_comparison_pp_real = function
-  | Pcmpext _ -> Cmp
-  | Pcmnext _ -> Cmn
-  | Pfcmp _ -> Fcmp
-
-let arith_comparison_r0r_real = function
-  | Pcmp (_, _) -> Cmp
-  | Pcmn (_, _) -> Cmn
-  | Ptst (_, _) -> Tst
-
-let arith_comparison_rr0r_real = function
-  | Padd (_, _) -> Add
-  | Psub (_, _) -> Sub
-  | Pand (_, _) -> And
-  | Pbic (_, _) -> Bic
-  | Peon (_, _) -> Eon
-  | Peor (_, _) -> Eor
-  | Porr (_, _) -> Orr
-  | Porn (_, _) -> Orn
-
-let arith_comparison_rr0_real = function
-  | Pandimm (_, _) -> And
-  | Peorimm (_, _) -> Eor
-  | Porrimm (_, _) -> Orr
-
-let arith_comparison_arrrr0_real = function Pmadd _ -> Madd | Pmsub _ -> Msub
-
-let store_rs_a_real = function
-  | Pstrw -> Str
-  | Pstrw_a -> Str
-  | Pstrx -> Str
-  | Pstrx_a -> Str
-  | Pstrb -> Strb
-  | Pstrh -> Strh
-  | Pstrs -> Str
-  | Pstrd -> Str
-  | Pstrd_a -> Str
-
-let load_rd_a_real = function
-  | Pldrw -> Ldr
-  | Pldrw_a -> Ldr
-  | Pldrx -> Ldr
-  | Pldrx_a -> Ldr
-  | Pldrb _ -> Ldrb
-  | Pldrsb _ -> Ldrsb
-  | Pldrh _ -> Ldrh
-  | Pldrsh _ -> Ldrsh
-  | Pldrzw -> Ldr
-  | Pldrsw -> Ldrsw
-  | Pldrs -> Ldr
-  | Pldrd -> Ldr
-  | Pldrd_a -> Ldr
-
-let loadsymbol_real = Ldr
-
-let cvtsw2x_real = Sxtw
-
-let cvtuw2x_real = Uxtw
-
-let cset_real = Cset
-
-let csel_real = Csel
-
-let fmovi_real = Fmov
-
-let fnmul_real = Fnmul
-
-let b_real = B
-
-let bc_real = B
-
-let bl_real = Bl
-
-let bs_real = B
-
-let blr_real = Blr
-
-let br_real = Br
-
-let ret_real = Ret
-
-let cbnz_real = Cbnz
-
-let cbz_real = Cbz
-
-let tbnz_real = Tbnz
-
-let tbz_real = Tbz
-
-let btbl_real = Btbl
-
-let allocframe_real = Allocframe
-
-let freeframe_real = Freeframe
-
-let builtin_real = Builtin
-
-let cvtx2w_real = Cvtx2w
-
 let is_XZR = function IREG0_XZR -> true | _ -> false
 
 let reg_of_pc = Reg Asm.PC
@@ -232,17 +63,17 @@ let get_arith_p_wlocs = function
   | Pfmovimmd _ -> [ reg_of_ireg Asm.X16 ]
   | _ -> []
 
-let arith_p_rec i rd =
+let arith_p_rec i i' rd =
   {
-    inst = arith_p_real i;
-    write_locs = [ rd ] @ get_arith_p_wlocs i;
+    inst = i;
+    write_locs = [ rd ] @ get_arith_p_wlocs i';
     read_locs = [];
     is_control = false;
   }
 
 let arith_pp_rec i rd rs =
   {
-    inst = arith_pp_real i;
+    inst = i;
     write_locs = [ rd ];
     read_locs = [ rs ];
     is_control = false;
@@ -250,7 +81,7 @@ let arith_pp_rec i rd rs =
 
 let arith_ppp_rec i rd r1 r2 =
   {
-    inst = arith_ppp_real i;
+    inst = i;
     write_locs = [ rd ];
     read_locs = [ r1; r2 ];
     is_control = false;
@@ -259,7 +90,7 @@ let arith_ppp_rec i rd r1 r2 =
 let arith_rr0r_rec i rd r1 r2 =
   let rlocs = if is_XZR r1 then [ r2 ] else [ r1; r2 ] in
   {
-    inst = arith_rr0r_real i;
+    inst = i;
     write_locs = [ rd ];
     read_locs = rlocs;
     is_control = false;
@@ -268,7 +99,7 @@ let arith_rr0r_rec i rd r1 r2 =
 let arith_rr0_rec i rd r1 =
   let rlocs = if is_XZR r1 then [] else [ r1 ] in
   {
-    inst = arith_rr0_real i;
+    inst = i;
     write_locs = [ rd ];
     read_locs = rlocs;
     is_control = false;
@@ -277,7 +108,7 @@ let arith_rr0_rec i rd r1 =
 let arith_arrrr0_rec i rd r1 r2 r3 =
   let rlocs = if is_XZR r3 then [ r1; r2 ] else [ r1; r2; r3 ] in
   {
-    inst = arith_arrrr0_real i;
+    inst = i;
     write_locs = [ rd ];
     read_locs = rlocs;
     is_control = false;
@@ -285,7 +116,7 @@ let arith_arrrr0_rec i rd r1 r2 r3 =
 
 let arith_comparison_pp_rec i r1 r2 =
   {
-    inst = arith_comparison_pp_real i;
+    inst = i;
     write_locs = flags_wlocs;
     read_locs = [ r1; r2 ];
     is_control = false;
@@ -294,7 +125,7 @@ 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 = arith_comparison_r0r_real i;
+    inst = i;
     write_locs = flags_wlocs;
     read_locs = rlocs;
     is_control = false;
@@ -302,7 +133,7 @@ let arith_comparison_r0r_rec i r1 r2 =
 
 let arith_comparison_p_rec i r1 =
   {
-    inst = arith_comparison_p_real i;
+    inst = i;
     write_locs = flags_wlocs;
     read_locs = [ r1 ];
     is_control = false;
@@ -320,7 +151,7 @@ let get_eval_addressing_rlocs a =
 
 let load_rec ld rd a =
   {
-    inst = load_rd_a_real ld;
+    inst = ld;
     write_locs = [ rd ];
     read_locs = [ Mem ] @ get_eval_addressing_rlocs a;
     is_control = false;
@@ -328,39 +159,39 @@ let load_rec ld rd a =
 
 let store_rec st r a =
   {
-    inst = store_rs_a_real st;
+    inst = st;
     write_locs = [ Mem ];
     read_locs = [ r; Mem ] @ get_eval_addressing_rlocs a;
     is_control = false;
   }
 
-let loadsymbol_rec rd id =
+let loadsymbol_rec i rd id =
   {
-    inst = loadsymbol_real;
+    inst = i;
     write_locs = [ rd ];
     read_locs = [ Mem ];
     is_control = false;
   }
 
-let cvtsw2x_rec rd r1 =
+let cvtsw2x_rec i rd r1 =
   {
-    inst = cvtsw2x_real;
+    inst = i;
     write_locs = [ rd ];
     read_locs = [ r1 ];
     is_control = false;
   }
 
-let cvtuw2x_rec rd r1 =
+let cvtuw2x_rec i rd r1 =
   {
-    inst = cvtuw2x_real;
+    inst = i;
     write_locs = [ rd ];
     read_locs = [ r1 ];
     is_control = false;
   }
 
-let cvtx2w_rec rd =
+let cvtx2w_rec i rd =
   {
-    inst = cvtx2w_real;
+    inst = i;
     write_locs = [ rd ];
     read_locs = [ rd ];
     is_control = false;
@@ -381,50 +212,50 @@ let get_testcond_rlocs c =
   | Asm.TCgt -> [ reg_of_cr Asm.CN; reg_of_cr Asm.CZ; reg_of_cr Asm.CV ]
   | Asm.TCle -> [ reg_of_cr Asm.CN; reg_of_cr Asm.CZ; reg_of_cr Asm.CV ]
 
-let cset_rec rd c =
+let cset_rec i rd c =
   {
-    inst = cset_real;
+    inst = i;
     write_locs = [ rd ];
     read_locs = get_testcond_rlocs c;
     is_control = false;
   }
 
-let csel_rec rd r1 r2 c =
+let csel_rec i rd r1 r2 c =
   {
-    inst = csel_real;
+    inst = i;
     write_locs = [ rd ];
     read_locs = [ r1; r2 ] @ get_testcond_rlocs c;
     is_control = false;
   }
 
-let fmovi_rec fsz rd r1 =
+let fmovi_rec i fsz rd r1 =
   let rlocs = if is_XZR r1 then [] else [ r1 ] in
   {
-    inst = fmovi_real;
+    inst = i;
     write_locs = [ rd ];
     read_locs = rlocs;
     is_control = false;
   }
 
-let fnmul_rec fsz rd r1 r2 =
+let fnmul_rec i fsz rd r1 r2 =
   {
-    inst = fnmul_real;
+    inst = i;
     write_locs = [ rd ];
     read_locs = [ r1; r2 ];
     is_control = false;
   }
 
-let allocframe_rec sz linkofs =
+let allocframe_rec i sz linkofs =
   {
-    inst = allocframe_real;
+    inst = i;
     write_locs = [ Mem; regXSP; reg_of_ireg Asm.X16; reg_of_ireg Asm.X29 ];
     read_locs = [ regXSP; Mem ];
     is_control = false;
   }
 
-let freeframe_rec sz linkofs =
+let freeframe_rec i sz linkofs =
   {
-    inst = freeframe_real;
+    inst = i;
     write_locs = [ Mem; regXSP; reg_of_ireg Asm.X16 ];
     read_locs = [ regXSP; Mem ];
     is_control = false;
@@ -432,44 +263,44 @@ let freeframe_rec sz linkofs =
 
 let arith_rec i =
   match i with
-  | PArithP (i', rd) -> arith_p_rec i' (reg_of_dreg rd)
-  | PArithPP (i', rd, rs) -> arith_pp_rec i' (reg_of_dreg rd) (reg_of_dreg rs)
+  | 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)
   | PArithPPP (i', rd, r1, r2) ->
-      arith_ppp_rec 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 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 i' (reg_of_ireg rd) (reg_of_ireg0 r1)
+      arith_rr0_rec (PBasic (PArith i)) (reg_of_ireg rd) (reg_of_ireg0 r1)
   | PArithARRRR0 (i', rd, r1, r2, r3) ->
-      arith_arrrr0_rec i' (reg_of_ireg rd) (reg_of_ireg r1) (reg_of_ireg r2)
+      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 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 i' (reg_of_ireg0 r1) (reg_of_ireg r2)
-  | PArithComparisonP (i', r1) -> arith_comparison_p_rec i' (reg_of_dreg r1)
-  | Pcset (rd, c) -> cset_rec (reg_of_ireg rd) c
-  | Pfmovi (fsz, rd, r1) -> fmovi_rec fsz (reg_of_freg rd) (reg_of_ireg0 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)
   | Pcsel (rd, r1, r2, c) ->
-      csel_rec (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 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
   | PArith i' -> arith_rec i'
-  | PLoad (ld, rd, a) -> load_rec ld (reg_of_dreg rd) a
-  | PStore (st, r, a) -> store_rec st (reg_of_dreg r) a
-  | Pallocframe (sz, linkofs) -> allocframe_rec sz linkofs
-  | Pfreeframe (sz, linkofs) -> freeframe_rec sz linkofs
-  | Ploadsymbol (rd, id) -> loadsymbol_rec (reg_of_ireg rd) id
-  | Pcvtsw2x (rd, r1) -> cvtsw2x_rec (reg_of_ireg rd) (reg_of_ireg r1)
-  | Pcvtuw2x (rd, r1) -> cvtuw2x_rec (reg_of_ireg rd) (reg_of_ireg r1)
-  | Pcvtx2w rd -> cvtx2w_rec (reg_of_ireg rd)
-
-let builtin_rec ef args res =
+  | PLoad (ld, rd, a) -> load_rec (PBasic i) (reg_of_dreg rd) a
+  | PStore (st, r, a) -> store_rec (PBasic i) (reg_of_dreg r) a
+  | 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)
+  | Pcvtx2w rd -> cvtx2w_rec (PBasic i) (reg_of_ireg rd)
+
+let builtin_rec i ef args res =
   {
-    inst = builtin_real;
+    inst = i;
     write_locs = [ Mem ];
     read_locs = [ Mem ];
     is_control = true;
@@ -479,84 +310,84 @@ let ctl_flow_rec i =
   match i with
   | Pb lbl ->
       {
-        inst = b_real;
+        inst = (PControl (PCtlFlow i));
         write_locs = [ reg_of_pc ];
         read_locs = [ reg_of_pc ];
         is_control = true;
       }
   | Pbc (c, lbl) ->
       {
-        inst = bc_real;
+        inst = (PControl (PCtlFlow i));
         write_locs = [ reg_of_pc ];
         read_locs = [ reg_of_pc ];
         is_control = true;
       }
   | Pbl (id, sg) ->
       {
-        inst = bl_real;
+        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 = bs_real;
+        inst = (PControl (PCtlFlow i));
         write_locs = [ reg_of_pc ];
         read_locs = [];
         is_control = true;
       }
   | Pblr (r, sg) ->
       {
-        inst = blr_real;
+        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 = br_real;
+        inst = (PControl (PCtlFlow i));
         write_locs = [ reg_of_pc ];
         read_locs = [ reg_of_ireg r ];
         is_control = true;
       }
   | Pret r ->
       {
-        inst = ret_real;
+        inst = (PControl (PCtlFlow i));
         write_locs = [ reg_of_pc ];
         read_locs = [ reg_of_ireg r ];
         is_control = true;
       }
   | Pcbnz (sz, r, lbl) ->
       {
-        inst = cbnz_real;
+        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 = cbz_real;
+        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 = tbnz_real;
+        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 = tbz_real;
+        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 = btbl_real;
+        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;
@@ -564,7 +395,7 @@ let ctl_flow_rec i =
 
 let control_rec i =
   match i with
-  | Pbuiltin (ef, args, res) -> builtin_rec ef args res
+  | Pbuiltin (ef, args, res) -> builtin_rec (PControl i) ef args res
   | PCtlFlow i' -> ctl_flow_rec i'
 
 let rec basic_recs body =