From 23c01485970efa11a7207ac2124f5922a011b0d4 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Jul 2021 20:01:12 +0200 Subject: new expansion oracle for BTL --- riscV/ExpansionOracle.ml | 330 ++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 328 insertions(+), 2 deletions(-) (limited to 'riscV') 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 -- cgit