new expansion oracle for BTL

1 files changed, 328 insertions, 2 deletions

diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml
index 0869007c..7950cb6a 100644
--- a/riscV/ExpansionOracle.ml
+++ b/riscV/ExpansionOracle.ml
@@ -10,6 +10,332 @@
 (*                                                             *)
 (* *************************************************************)
 
-let expanse n ibf btl = btl
+open BTL
+open Op
+open! Integers
+open Camlcoq
+open DebugPrint
+open RTLcommonaux
+open BTLcommonaux
+open AST
+open Datatypes
+open Maps
 
-let find_last_node_reg c = ()
+(** Tools *)
+
+(** TODO gourdinl move to BTLcommonaux *)
+let rec iblock_to_list ib =
+  match ib with
+  | Bseq (ib1, ib2) -> iblock_to_list ib1 @ iblock_to_list ib2
+  | _ -> [ ib ]
+
+let rec list_to_iblock lib =
+  match lib with
+  | i1 :: k ->
+      if List.length lib > 1 then
+        Bseq (i1, list_to_iblock k)
+      else i1
+  | [] -> failwith "list_to_iblock: called on empty list"
+
+(** Mini CSE (a dynamic numbering is applied during expansion. 
+    The CSE algorithm is inspired by the "static" one used in backend/CSE.v *)
+
+(** Managing virtual registers and node index *)
+
+let reg = ref 1
+
+let r2p () = P.of_int !reg
+
+let r2pi () =
+  reg := !reg + 1;
+  r2p ()
+
+(** Below are the types for rhs and equations *)
+
+type rhs = Sop of operation * int list | Smove
+
+type seq = Seq of int * rhs
+
+(** This is a mini abstraction to have a simpler representation during expansion
+    - (Sr r) is inserted if the value was found in register r
+    - (Sexp dest rhs args iinfo) represent an instruction
+    - (Scond cond args ib1 ib2 iinfo) represents a condition
+*)
+
+type expl =
+  | Sr of P.t
+  | Sexp of P.t * rhs * P.t list * inst_info
+  | Scond of condition * P.t list * iblock * iblock * inst_info
+
+(** Record used during the "dynamic" value numbering *)
+
+type numb = {
+  mutable nnext : int;  (** Next unusued value number *)
+  mutable seqs : seq list;  (** equations *)
+  mutable nreg : (P.t, int) Hashtbl.t;  (** mapping registers to values *)
+  mutable nval : (int, P.t list) Hashtbl.t;
+      (** reverse mapping values to registers containing it *)
+}
+
+let print_list_pos l =
+  debug "[";
+  List.iter (fun i -> debug "%d;" (p2i i)) l;
+  debug "]\n"
+
+let empty_numbering () =
+  { nnext = 1; seqs = []; nreg = Hashtbl.create 100; nval = Hashtbl.create 100 }
+
+let rec get_nvalues vn = function
+  | [] -> []
+  | r :: rs ->
+      let v =
+        match Hashtbl.find_opt !vn.nreg r with
+        | Some v ->
+            debug "getnval r=%d |-> v=%d\n" (p2i r) v;
+            v
+        | None ->
+            let n = !vn.nnext in
+            debug "getnval r=%d |-> v=%d\n" (p2i r) n;
+            !vn.nnext <- !vn.nnext + 1;
+            Hashtbl.replace !vn.nreg r n;
+            Hashtbl.replace !vn.nval n [ r ];
+            n
+      in
+      let vs = get_nvalues vn rs in
+      v :: vs
+
+let get_nval_ornil vn v =
+  match Hashtbl.find_opt !vn.nval v with None -> [] | Some l -> l
+
+let forget_reg vn rd =
+  match Hashtbl.find_opt !vn.nreg rd with
+  | Some v ->
+      debug "forget_reg: r=%d |-> v=%d\n" (p2i rd) v;
+      let old_regs = get_nval_ornil vn v in
+      debug "forget_reg: old_regs are:\n";
+      print_list_pos old_regs;
+      Hashtbl.replace !vn.nval v
+        (List.filter (fun n -> not (P.eq n rd)) old_regs)
+  | None -> debug "forget_reg: no mapping for r=%d\n" (p2i rd)
+
+let update_reg vn rd v =
+  debug "update_reg: update v=%d with r=%d\n" v (p2i rd);
+  forget_reg vn rd;
+  let old_regs = get_nval_ornil vn v in
+  Hashtbl.replace !vn.nval v (rd :: old_regs)
+
+let rec find_valnum_rhs rh = function
+  | [] -> None
+  | Seq (v, rh') :: tl -> if rh = rh' then Some v else find_valnum_rhs rh tl
+
+let set_unknown vn rd =
+  debug "set_unknown: rd=%d\n" (p2i rd);
+  forget_reg vn rd;
+  Hashtbl.remove !vn.nreg rd
+
+let set_res_unknown vn res = match res with BR r -> set_unknown vn r | _ -> ()
+
+let addrhs vn rd rh =
+  match find_valnum_rhs rh !vn.seqs with
+  | Some vres ->
+      debug "addrhs: Some v=%d\n" vres;
+      Hashtbl.replace !vn.nreg rd vres;
+      update_reg vn rd vres
+  | None ->
+      let n = !vn.nnext in
+      debug "addrhs: None v=%d\n" n;
+      !vn.nnext <- !vn.nnext + 1;
+      !vn.seqs <- Seq (n, rh) :: !vn.seqs;
+      update_reg vn rd n;
+      Hashtbl.replace !vn.nreg rd n
+
+let addsop vn v op rd =
+  debug "addsop\n";
+  if op = Omove then (
+    update_reg vn rd (List.hd v);
+    Hashtbl.replace !vn.nreg rd (List.hd v))
+  else addrhs vn rd (Sop (op, v))
+
+let rec kill_mem_operations = function
+  | (Seq (v, Sop (op, vl)) as eq) :: tl ->
+      if op_depends_on_memory op then kill_mem_operations tl
+      else eq :: kill_mem_operations tl
+  | [] -> []
+  | eq :: tl -> eq :: kill_mem_operations tl
+
+let reg_valnum vn v =
+  debug "reg_valnum: trying to find a mapping for v=%d\n" v;
+  match Hashtbl.find !vn.nval v with
+  | [] -> None
+  | r :: rs ->
+      debug "reg_valnum: found a mapping r=%d\n" (p2i r);
+      Some r
+
+let rec reg_valnums vn = function
+  | [] -> Some []
+  | v :: vs -> (
+      match (reg_valnum vn v, reg_valnums vn vs) with
+      | Some r, Some rs -> Some (r :: rs)
+      | _, _ -> None)
+
+let find_rhs vn rh =
+  match find_valnum_rhs rh !vn.seqs with
+  | None -> None
+  | Some vres -> reg_valnum vn vres
+
+(** Functions to perform the dynamic reduction during CSE *)
+
+let extract_arg l =
+  if List.length l > 0 then
+    match List.hd l with
+    | Sr r -> (r, List.tl l)
+    | Sexp (rd, _, _, _) -> (rd, l)
+    | _ -> failwith "extract_arg: final instruction arg can not be extracted"
+  else failwith "extract_arg: trying to extract on an empty list"
+
+let extract_final vn fl fdest =
+  if List.length fl > 0 then
+    match List.hd fl with
+    | Sr r ->
+        if not (P.eq r fdest) then (
+          let v = get_nvalues vn [ r ] in
+          addsop vn v Omove fdest;
+          Sexp (fdest, Smove, [ r ], def_iinfo ()) :: List.tl fl)
+        else List.tl fl
+    | _ -> fl
+  else failwith "extract_final: trying to extract on an empty list"
+
+let addinst vn op args rd iinfo =
+  let v = get_nvalues vn args in
+  let rh = Sop (op, v) in
+  match find_rhs vn rh with
+  | Some r ->
+      debug "addinst: rhs found with r=%d\n" (p2i r);
+      Sr r
+  | None ->
+      addsop vn v op rd;
+      Sexp (rd, rh, args, iinfo)
+
+(** Expansion functions *)
+
+let is_inv_cmp = function Cle | Cgt -> true | _ -> false
+
+let make_optR is_x0 is_inv =
+  if is_x0 then if is_inv then Some X0_L else Some X0_R else None
+
+let cond_int32s vn is_x0 cmp a1 a2 dest iinfo =
+  let optR = make_optR is_x0 (is_inv_cmp cmp) in
+  match cmp with
+  | Ceq -> [ addinst vn (OEseqw optR) [ a1; a2 ] dest iinfo ]
+  | Cne -> [ addinst vn (OEsnew optR) [ a1; a2 ] dest iinfo ]
+  | Clt -> [ addinst vn (OEsltw optR) [ a1; a2 ] dest iinfo ]
+  | Cle ->
+      let r = r2pi () in
+      let op = OEsltw optR in
+      let i1 = addinst vn op [ a2; a1 ] r iinfo in
+      let r', l = extract_arg [ i1 ] in
+      addinst vn (OExoriw Int.one) [ r' ] dest iinfo :: l
+  | Cgt -> [ addinst vn (OEsltw optR) [ a2; a1 ] dest iinfo ]
+  | Cge ->
+      let r = r2pi () in
+      let op = OEsltw optR in
+      let i1 = addinst vn op [ a1; a2 ] r iinfo in
+      let r', l = extract_arg [ i1 ] in
+      addinst vn (OExoriw Int.one) [ r' ] dest iinfo :: l
+
+(** Return olds args if the CSE numbering is empty *)
+
+let get_arguments vn vals args =
+  match reg_valnums vn vals with Some args' -> args' | None -> args
+
+let rec gen_btl_list vn exp =
+  match exp with
+  | Sr r :: _ ->
+      failwith "write_tree: there are still some symbolic values in the list"
+  | Sexp (rd, Sop (op, vals), args, iinfo) :: k ->
+      let args = get_arguments vn vals args in
+      let inst = Bop (op, args, rd, iinfo) in
+      inst :: gen_btl_list vn k
+  | [ Sexp (rd, Smove, args, iinfo) ] ->
+      [ Bop (Omove, args, rd, iinfo) ]
+  | [ Scond (cond, args, succ1, succ2, iinfo) ] ->
+      [ Bcond (cond, args, succ1, succ2, iinfo) ]
+  | [] -> []
+  | _ -> failwith "write_tree: invalid list"
+
+let expanse_list li =
+  debug "#### New block for expansion oracle\n";
+  let exp = ref [] in
+  let was_exp = ref false in
+  let vn = ref (empty_numbering ()) in
+  let rec expanse_list_rec li =
+    match li with
+    | [] -> li
+    | i :: li' ->
+        was_exp := false;
+        (if !Clflags.option_fexpanse_rtlcond then
+         match i with
+         | Bop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, iinfo) ->
+             debug "Bop/Ccomp\n";
+             exp := cond_int32s vn false c a1 a2 dest iinfo;
+             exp := extract_final vn !exp dest;
+             was_exp := true
+         | _ -> ());
+        if not !was_exp then (
+          (match i with
+          | Bop (op, args, dest, iinfo) ->
+              let v = get_nvalues vn args in
+              addsop vn v op dest
+          | Bload (_, _, _, _, dst, _) -> set_unknown vn dst
+          | Bstore (_, _, _, _, _) ->
+              !vn.seqs <- kill_mem_operations !vn.seqs
+              (* TODO gourdinl empty numb BF? vn := empty_numbering ()*)
+          | _ -> ());
+          i :: expanse_list_rec li')
+        else
+          gen_btl_list vn !exp @ expanse_list_rec li'
+  in
+  expanse_list_rec li
+
+let expanse n ibf btl =
+  debug_flag := true;
+  let lib = iblock_to_list ibf.entry in
+  let new_lib = expanse_list lib in
+  let ibf' = { entry = list_to_iblock new_lib;
+               input_regs = ibf.input_regs;
+               binfo = ibf.binfo } in
+  debug_flag := false;
+  PTree.set n ibf' btl
+
+(** Form a list containing both sources and destination regs of a block *)
+let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ]
+
+let rec get_regs_ib = function
+  | Bnop _ -> []
+  | Bop (_, args, dest, _) -> dest :: args
+  | Bload (_, _, _, args, dest, _) -> dest :: args
+  | Bstore (_, _, args, src, _) -> src :: args
+  | Bcond (_, args, ib1, ib2, _) -> 
+      get_regs_ib ib1 @ get_regs_ib ib2 @ args
+  | Bseq (ib1, ib2) ->
+      get_regs_ib ib1 @ get_regs_ib ib2
+  | BF (Breturn (Some r), _) -> [r]
+  | BF (Bcall (_, t, args, dest, _), _) -> dest :: (get_regindent t @ args)
+  | BF (Btailcall (_, t, args), _) -> (get_regindent t @ args)
+  | BF (Bbuiltin (_, args, dest, _), _) -> 
+      AST.params_of_builtin_res dest @ AST.params_of_builtin_args args
+  | BF (Bjumptable (arg, _), _) -> [arg]
+  | _ -> []
+
+let rec find_last_reg = function
+  | [] -> ()
+  | (pc, ibf) :: k ->
+      let rec traverse_list var = function
+        | [] -> ()
+        | e :: t ->
+            let e' = p2i e in
+            if e' > !var then var := e';
+            traverse_list var t
+      in
+      traverse_list reg (get_regs_ib ibf.entry);
+      find_last_reg k