Postpass scheduling OK

- Modifying Asmblockdeps to adapt to Pfmovimm new specification
- Changing the Asmgenproof to adapt PArith in consequence
- Modifying the oracle to specify correct wlocs
- Cleaning everywhere

1 files changed, 13 insertions, 146 deletions

diff --git a/aarch64/PostpassSchedulingOracle.ml b/aarch64/PostpassSchedulingOracle.ml
index 821a1d53..463d65b5 100644
--- a/aarch64/PostpassSchedulingOracle.ml
+++ b/aarch64/PostpassSchedulingOracle.ml
@@ -17,7 +17,7 @@ open Asmblock
 open OpWeightsAsm
 open InstructionScheduler
 
-let debug = true
+let debug = false
 
 (**
  * Extracting infos from Asm instructions
@@ -40,7 +40,7 @@ let arith_p_real = function
   | Padrp (_, _) -> Adrp
   | Pmovz (_, _, _) -> Movz
   | Pmovn (_, _, _) -> Movn
-  | Pfmovimms _ -> Fmov (* TODO not sure about this and below too *)
+  | Pfmovimms _ -> Fmov (* XXX We could also use load, but Fmov may be more convenient for tuning *)
   | Pfmovimmd _ -> Fmov
 
 let arith_pp_real = function
@@ -223,10 +223,15 @@ let regXSP = Reg (Asm.DR (Asm.IR Asm.XSP))
 let flags_wlocs =
   [ reg_of_cr Asm.CN; reg_of_cr Asm.CZ; reg_of_cr Asm.CC; reg_of_cr Asm.CV ]
 
+let get_arith_p_wlocs = function
+  | Pfmovimms _ -> [ reg_of_ireg Asm.X16 ]
+  | Pfmovimmd _ -> [ reg_of_ireg Asm.X16 ]
+  | _ -> []
+
 let arith_p_rec i rd =
   {
     inst = arith_p_real i;
-    write_locs = [ rd ];
+    write_locs = [ rd ] @ get_arith_p_wlocs i;
     read_locs = [];
     is_control = false;
   }
@@ -459,7 +464,6 @@ let basic_rec i =
   | Pcvtx2w rd -> cvtx2w_rec (reg_of_ireg rd)
 
 let builtin_rec ef args res =
-  (* XXX verify this *)
   {
     inst = builtin_real;
     write_locs = [ Mem ];
@@ -490,7 +494,6 @@ let ctl_flow_rec i =
         read_locs = [ reg_of_pc ];
         is_control = true;
       }
-      (* XXX not sure about X30 *)
   | Pbs (id, sg) ->
       {
         inst = bs_real;
@@ -555,8 +558,6 @@ let ctl_flow_rec i =
         is_control = true;
       }
 
-(* XXX Verify this (Pbtbl) *)
-
 let control_rec i =
   match i with
   | Pbuiltin (ef, args, res) -> builtin_rec ef args res
@@ -577,30 +578,12 @@ type inst_info = {
   write_locs : location list;
   read_locs : location list;
   is_control : bool;
-  usage : int array;
   (* resources consumed by the instruction *)
+  usage : int array;
   latency : int;
 }
-(** Abstraction providing all the necessary informations for solving the scheduling problem *)
-
-(*(** Resources *)*)
-(*type rname = Rissue | Rtiny | Rlite | Rfull | Rlsu | Rmau | Rbcu | Rtca | Rauxr | Rauxw | Rcrrp | Rcrwl | Rcrwh | Rnop*)
-
-(*let resource_names = [Rissue; Rtiny; Rlite; Rfull; Rlsu; Rmau; Rbcu; Rtca; Rauxr; Rauxw; Rcrrp; Rcrwl; Rcrwh; Rnop]*)
-
-(*let rec find_index elt l =*)
-(*match l with*)
-(*| [] -> raise Not_found*)
-(*| e::l -> if (e == elt) then 0*)
-(*else 1 + find_index elt l*)
 
-(*let resource_id resource : int = find_index resource resource_names*)
-
-(*let resource_bounds : int array = Array.of_list (List.map resource_bound resource_names)*)
-
-(*let rec empty_inter la = function*)
-(*| [] -> true*)
-(*| b::lb -> if (List.mem b la) then false else empty_inter la lb*)
+(** Abstraction providing all the necessary informations for solving the scheduling problem *)
 
 let rec_to_info (r : ab_inst_rec) : inst_info =
   let opweights = OpWeightsAsm.get_opweights () in
@@ -616,8 +599,6 @@ let rec_to_info (r : ab_inst_rec) : inst_info =
 
 let instruction_infos bb = List.map rec_to_info (instruction_recs bb)
 
-(*let instruction_infos bb = instruction_recs bb*)
-
 let instruction_usages bb =
   let usages = List.map (fun info -> info.usage) (instruction_infos bb) in
   Array.of_list usages
@@ -626,25 +607,9 @@ let instruction_usages bb =
  * Latency constraints building
  *)
 
-(*(* type access = { inst: int; loc: location } *)*)
-
-(*let preg2int pr = Camlcoq.P.to_int @@ Asmblockdeps.ppos pr*)
-
-(*let loc2int = function*)
-(*| Mem -> 1*)
-(*| Reg pr -> preg2int pr*)
-
-(*(* module HashedLoc = struct*)
-  (*type t = { loc: location; key: int }*)
-  (*let equal l1 l2 = (l1.key = l2.key)*)
-  (*let hash l = l.key*)
-  (*let create (l:location) : t = { loc=l; key = loc2int l }*)
-(*end *)*)
-
-(*(* module LocHash = Hashtbl.Make(HashedLoc) *)*)
 module LocHash = Hashtbl
 
-(*(* Hash table : location => list of instruction ids *)*)
+(* Hash table : location => list of instruction ids *)
 
 let rec intlist n =
   if n < 0 then failwith "intlist: n < 0"
@@ -662,10 +627,6 @@ let rec get_accesses hashloc (ll : location list) =
 
 let compute_latency (ifrom : inst_info) = ifrom.latency
 
-(*let dlat = inst_info_to_dlatency ito*)
-(*in let lat = ifrom.latency + dlat*)
-(*in assert (lat >= 0); if (lat == 0) then 1 else lat*)
-
 let latency_constraints bb =
   let written = LocHash.create 70
   and read = LocHash.create 70
@@ -726,8 +687,6 @@ let latency_constraints bb =
  * Using the InstructionScheduler
  *)
 
-(* TODO RESUME HERE *)
-
 let opweights = OpWeightsAsm.get_opweights ()
 
 let build_problem bb =
@@ -738,32 +697,11 @@ let build_problem bb =
     latency_constraints = latency_constraints bb;
   }
 
-(*let rec find_min_opt (l: int option list) =*)
-(*match l with*)
-(*| [] -> None *)
-(*| e :: l ->*)
-(*begin match find_min_opt l with*)
-(*| None -> e*)
-(*| Some m ->*)
-(*begin match e with*)
-(*| None -> Some m*)
-(*| Some n -> if n < m then Some n else Some m*)
-(*end*)
-(*end*)
-
-(*let rec filter_indexes predicate = function*)
-(*| [] -> []*)
-(*| e :: l -> if (predicate e) then e :: (filter_indexes predicate l) else filter_indexes predicate l*)
-
 let get_from_indexes indexes l = List.map (List.nth l) indexes
 
 (*let is_basic = function PBasic _ -> true | _ -> false*)
 let is_control = function PControl _ -> true | _ -> false
 
-(*let to_basic = function*)
-(*| PBasic i -> i*)
-(*| _ -> failwith "to_basic: control instruction found"*)
-
 let to_control = function
   | PControl i -> i
   | _ -> failwith "to_control: basic instruction found"
@@ -786,35 +724,11 @@ let repack li hd =
     { header = hd; body = instrs_to_bdy cut_li; exit = Some (to_control last) }
   else { header = hd; body = instrs_to_bdy li; exit = None }
 
-(*let extract_some o = match o with Some e -> e | None -> failwith "extract_some: None found"*)
-
-(*let rec find_min = function*)
-(*| [] -> None*)
-(*| e :: l ->*)
-(*match find_min l with*)
-(*| None -> Some e*)
-(*| Some m -> if (e < m) then Some e else Some m*)
-
-(*let rec remove_all m = function*)
-(*| [] -> []*)
-(*| e :: l -> if m=e then remove_all m l*)
-(*else e :: (remove_all m l)*)
-
-(*let rec find_mins l = match find_min l with*)
-(*| None -> []*)
-(*| Some m -> m :: find_mins (remove_all m l)*)
-
-(*let find_all_indices m l = *)
-(*let rec find m off = function*)
-(*| [] -> []*)
-(*| e :: l -> if m=e then off :: find m (off+1) l*)
-(*else find m (off+1) l*)
-(*in find m 0 l*)
-
 module TimeHash = Hashtbl
 
 (*Hash table : time => list of instruction ids *)
 
+(* Flattening the minpack result *)
 let hashtbl2flatarray h maxint =
   let rec f i =
     match TimeHash.find_opt h i with
@@ -833,6 +747,7 @@ let find_max l =
   in
   match f l with None -> raise Not_found | Some m -> m
 
+(* We still use the minpack algorithm even without bundles, but the result is then flattened *)
 (*(* [0, 2, 3, 1, 1, 2, 4, 5] -> [[0], [3, 4], [1, 5], [2], [6], [7]] *)*)
 let minpack_list (l : int list) =
   let timehash = TimeHash.create (List.length l) in
@@ -847,10 +762,6 @@ let minpack_list (l : int list) =
   f 0 l;
   hashtbl2flatarray timehash (find_max l)
 
-(*let minpack_list l =*)
-(*let mins = find_mins l*)
-(*in List.map (fun m -> find_all_indices m l) mins*)
-
 let bb_to_instrs bb =
   body_to_instrs bb.body
   @ match bb.exit with None -> [] | Some e -> [ PControl e ]
@@ -861,21 +772,6 @@ let build_solution bb sol =
   let pack = minpack_list tmp and instrs = bb_to_instrs bb in
   repack (get_from_indexes pack instrs) bb.header
 
-(*in let rec bund hd = function*)
-(*| [] -> []*)
-(*| pack :: packs -> repack (get_from_indexes pack instrs) hd :: (bund [] packs)*)
-(*in bund bb.header packs*)
-
-(*let print_inst oc = function i -> TargetPrinter.Target.print_instructions oc i*)
-(*| Asm.Pallocframe(sz, ofs) -> Printf.fprintf oc "	Pallocframe\n"*)
-(*| Asm.Pfreeframe(sz, ofs) -> Printf.fprintf oc "	Pfreeframe\n"*)
-(*| Asm.Pbuiltin(ef, args, res) -> Printf.fprintf oc "	Pbuiltin\n"*)
-
-(*let print_bb oc bb =*)
-(*match Asmgen.Asmblock_TRANSF.unfold_bblock bb with*)
-(*| Errors.OK instructions -> List.iter (print_inst oc) instructions*)
-(*| Errors.Error _ -> Printf.eprintf "Error in print_bb"*)
-
 let print_schedule sched =
   print_string "[ ";
   Array.iter (fun x -> Printf.printf "%d; " x) sched;
@@ -898,35 +794,6 @@ let do_schedule bb =
 (* Pack result *)
 let pack_result (bb : bblock) = (bb.body, bb.exit)
 
-(**
- * Separates the opaque instructions such as Pfreeframe and Pallocframe
- *)
-
-(*let is_opaque = function*)
-(*| Pallocframe _ | Pfreeframe _ -> true*)
-(*| _ -> false*)
-
-(*(* Returns : (accumulated instructions, remaining instructions, opaque instruction if found) *)*)
-(*let rec biggest_wo_opaque = function
-  | [] -> ([], [], None)
-  | i :: li -> if is_opaque i then ([], li, Some i)
-               else let big, rem, opaque = biggest_wo_opaque li in (i :: big, rem, opaque);;
-
-let separate_opaque bb =
-  let instrs = bb_to_instrs bb
-  in let rec f hd li =
-    match li with
-    | [] -> []
-    | li -> let big, rem, opaque = biggest_wo_opaque li in
-            match opaque with
-            | Some i ->
-                (match big with
-                | [] -> (repack [i] hd) :: (f [] rem)
-                | big -> (repack big hd) :: (bundlize [i] []) :: (f [] rem)
-                )
-            | None -> (bundlize big hd) :: (f [] rem)
-  in f bb.header instrs*)
-
 let smart_schedule bb =
   let bb' =
     try do_schedule bb with