From a3319eb05543930844dedd9ac31ed1beaac3047e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Jul 2021 15:21:29 +0200 Subject: Fix compile on ARM/x86 backends --- riscV/ExpansionOracle.ml | 1056 +--------------------------------------------- 1 file changed, 2 insertions(+), 1054 deletions(-) (limited to 'riscV') diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index bbcc6807..0869007c 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -10,1058 +10,6 @@ (* *) (* *************************************************************) -open RTLpathLivegenaux -open RTLpathCommon -open Datatypes -open Maps -open RTL -open Op -open Asmgen -open RTLpath -open! Integers -open Camlcoq -open Option -open AST -open DebugPrint -open RTLcommonaux +let expanse n ibf btl = btl -(** 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 node = ref 1 - -let r2p () = P.of_int !reg - -let n2p () = P.of_int !node - -let r2pi () = - reg := !reg + 1; - r2p () - -let n2pi () = - node := !node + 1; - n2p () - -(** 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 - - Snop will be converted to Inop - - (Sr r) is inserted if the value was found in register r - - (Sexp dest rhs args succ) represent an instruction - (succesor may not be defined at this point, hence the use of type option) - - (Sfinalcond cond args succ1 succ2 info) represents a condition (which must - always be the last instruction in expansion list *) - -type expl = - | Snop of P.t - | Sr of P.t - | Sexp of P.t * rhs * P.t list * node option - | Sfinalcond of condition * P.t list * node * node * bool option - -(** 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 succ = - 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 ], Some succ) :: List.tl fl) - else Snop succ :: List.tl fl - | Sexp (rd, rh, args, None) -> - assert (rd = fdest); - Sexp (fdest, rh, args, Some succ) :: List.tl fl - | _ -> fl - else failwith "extract_final: trying to extract on an empty list" - -let addinst vn op args rd = - 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, None) - -(** Expansion functions *) - -type immt = - | Addiw - | Addil - | Andiw - | Andil - | Oriw - | Oril - | Xoriw - | Xoril - | Sltiw - | Sltiuw - | Sltil - | Sltiul - -let load_hilo32 vn dest hi lo = - let op1 = OEluiw hi in - if Int.eq lo Int.zero then [ addinst vn op1 [] dest ] - else - let r = r2pi () in - let op2 = OEaddiw (None, lo) in - let i1 = addinst vn op1 [] r in - let r', l = extract_arg [ i1 ] in - let i2 = addinst vn op2 [ r' ] dest in - i2 :: l - -let load_hilo64 vn dest hi lo = - let op1 = OEluil hi in - if Int64.eq lo Int64.zero then [ addinst vn op1 [] dest ] - else - let r = r2pi () in - let op2 = OEaddil (None, lo) in - let i1 = addinst vn op1 [] r in - let r', l = extract_arg [ i1 ] in - let i2 = addinst vn op2 [ r' ] dest in - i2 :: l - -let loadimm32 vn dest n = - match make_immed32 n with - | Imm32_single imm -> - let op1 = OEaddiw (Some X0_R, imm) in - [ addinst vn op1 [] dest ] - | Imm32_pair (hi, lo) -> load_hilo32 vn dest hi lo - -let loadimm64 vn dest n = - match make_immed64 n with - | Imm64_single imm -> - let op1 = OEaddil (Some X0_R, imm) in - [ addinst vn op1 [] dest ] - | Imm64_pair (hi, lo) -> load_hilo64 vn dest hi lo - | Imm64_large imm -> - let op1 = OEloadli imm in - [ addinst vn op1 [] dest ] - -let get_opimm optR imm = function - | Addiw -> OEaddiw (optR, imm) - | Andiw -> OEandiw imm - | Oriw -> OEoriw imm - | Xoriw -> OExoriw imm - | Sltiw -> OEsltiw imm - | Sltiuw -> OEsltiuw imm - | Addil -> OEaddil (optR, imm) - | Andil -> OEandil imm - | Oril -> OEoril imm - | Xoril -> OExoril imm - | Sltil -> OEsltil imm - | Sltiul -> OEsltiul imm - -let opimm32 vn a1 dest n optR op opimm = - match make_immed32 n with - | Imm32_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ] - | Imm32_pair (hi, lo) -> - let r = r2pi () in - let l = load_hilo32 vn r hi lo in - let r', l' = extract_arg l in - let i = addinst vn op [ a1; r' ] dest in - i :: l' - -let opimm64 vn a1 dest n optR op opimm = - match make_immed64 n with - | Imm64_single imm -> [ addinst vn (get_opimm optR imm opimm) [ a1 ] dest ] - | Imm64_pair (hi, lo) -> - let r = r2pi () in - let l = load_hilo64 vn r hi lo in - let r', l' = extract_arg l in - let i = addinst vn op [ a1; r' ] dest in - i :: l' - | Imm64_large imm -> - let r = r2pi () in - let op1 = OEloadli imm in - let i1 = addinst vn op1 [] r in - let r', l' = extract_arg [ i1 ] in - let i2 = addinst vn op [ a1; r' ] dest in - i2 :: l' - -let addimm32 vn a1 dest n optR = opimm32 vn a1 dest n optR Oadd Addiw - -let andimm32 vn a1 dest n = opimm32 vn a1 dest n None Oand Andiw - -let orimm32 vn a1 dest n = opimm32 vn a1 dest n None Oor Oriw - -let xorimm32 vn a1 dest n = opimm32 vn a1 dest n None Oxor Xoriw - -let sltimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltw None) Sltiw - -let sltuimm32 vn a1 dest n = opimm32 vn a1 dest n None (OEsltuw None) Sltiuw - -let addimm64 vn a1 dest n optR = opimm64 vn a1 dest n optR Oaddl Addil - -let andimm64 vn a1 dest n = opimm64 vn a1 dest n None Oandl Andil - -let orimm64 vn a1 dest n = opimm64 vn a1 dest n None Oorl Oril - -let xorimm64 vn a1 dest n = opimm64 vn a1 dest n None Oxorl Xoril - -let sltimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltl None) Sltil - -let sltuimm64 vn a1 dest n = opimm64 vn a1 dest n None (OEsltul None) Sltiul - -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 cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> Sfinalcond (CEbeqw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Sfinalcond (CEbnew optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Sfinalcond (CEbltw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Sfinalcond (CEbgew optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Sfinalcond (CEbltw optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Sfinalcond (CEbgew optR, [ a1; a2 ], succ1, succ2, info) :: k - -let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> Sfinalcond (CEbequw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Sfinalcond (CEbneuw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Sfinalcond (CEbltuw optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Sfinalcond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Sfinalcond (CEbltuw optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Sfinalcond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, info) :: k - -let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> Sfinalcond (CEbeql optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Sfinalcond (CEbnel optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Sfinalcond (CEbltl optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Sfinalcond (CEbgel optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Sfinalcond (CEbltl optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Sfinalcond (CEbgel optR, [ a1; a2 ], succ1, succ2, info) :: k - -let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> Sfinalcond (CEbequl optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cne -> Sfinalcond (CEbneul optR, [ a1; a2 ], succ1, succ2, info) :: k - | Clt -> Sfinalcond (CEbltul optR, [ a1; a2 ], succ1, succ2, info) :: k - | Cle -> Sfinalcond (CEbgeul optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cgt -> Sfinalcond (CEbltul optR, [ a2; a1 ], succ1, succ2, info) :: k - | Cge -> Sfinalcond (CEbgeul optR, [ a1; a2 ], succ1, succ2, info) :: k - -let cond_int32s vn is_x0 cmp a1 a2 dest = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> [ addinst vn (OEseqw optR) [ a1; a2 ] dest ] - | Cne -> [ addinst vn (OEsnew optR) [ a1; a2 ] dest ] - | Clt -> [ addinst vn (OEsltw optR) [ a1; a2 ] dest ] - | Cle -> - let r = r2pi () in - let op = OEsltw optR in - let i1 = addinst vn op [ a2; a1 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - | Cgt -> [ addinst vn (OEsltw optR) [ a2; a1 ] dest ] - | Cge -> - let r = r2pi () in - let op = OEsltw optR in - let i1 = addinst vn op [ a1; a2 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - -let cond_int32u vn is_x0 cmp a1 a2 dest = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> [ addinst vn (OEsequw optR) [ a1; a2 ] dest ] - | Cne -> [ addinst vn (OEsneuw optR) [ a1; a2 ] dest ] - | Clt -> [ addinst vn (OEsltuw optR) [ a1; a2 ] dest ] - | Cle -> - let r = r2pi () in - let op = OEsltuw optR in - let i1 = addinst vn op [ a2; a1 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - | Cgt -> [ addinst vn (OEsltuw optR) [ a2; a1 ] dest ] - | Cge -> - let r = r2pi () in - let op = OEsltuw optR in - let i1 = addinst vn op [ a1; a2 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - -let cond_int64s vn is_x0 cmp a1 a2 dest = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> [ addinst vn (OEseql optR) [ a1; a2 ] dest ] - | Cne -> [ addinst vn (OEsnel optR) [ a1; a2 ] dest ] - | Clt -> [ addinst vn (OEsltl optR) [ a1; a2 ] dest ] - | Cle -> - let r = r2pi () in - let op = OEsltl optR in - let i1 = addinst vn op [ a2; a1 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - | Cgt -> [ addinst vn (OEsltl optR) [ a2; a1 ] dest ] - | Cge -> - let r = r2pi () in - let op = OEsltl optR in - let i1 = addinst vn op [ a1; a2 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - -let cond_int64u vn is_x0 cmp a1 a2 dest = - let optR = make_optR is_x0 (is_inv_cmp cmp) in - match cmp with - | Ceq -> [ addinst vn (OEsequl optR) [ a1; a2 ] dest ] - | Cne -> [ addinst vn (OEsneul optR) [ a1; a2 ] dest ] - | Clt -> [ addinst vn (OEsltul optR) [ a1; a2 ] dest ] - | Cle -> - let r = r2pi () in - let op = OEsltul optR in - let i1 = addinst vn op [ a2; a1 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - | Cgt -> [ addinst vn (OEsltul optR) [ a2; a1 ] dest ] - | Cge -> - let r = r2pi () in - let op = OEsltul optR in - let i1 = addinst vn op [ a1; a2 ] r in - let r', l = extract_arg [ i1 ] in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - -let is_normal_cmp = function Cne -> false | _ -> true - -let cond_float vn cmp f1 f2 dest = - match cmp with - | Ceq -> [ addinst vn OEfeqd [ f1; f2 ] dest ] - | Cne -> [ addinst vn OEfeqd [ f1; f2 ] dest ] - | Clt -> [ addinst vn OEfltd [ f1; f2 ] dest ] - | Cle -> [ addinst vn OEfled [ f1; f2 ] dest ] - | Cgt -> [ addinst vn OEfltd [ f2; f1 ] dest ] - | Cge -> [ addinst vn OEfled [ f2; f1 ] dest ] - -let cond_single vn cmp f1 f2 dest = - match cmp with - | Ceq -> [ addinst vn OEfeqs [ f1; f2 ] dest ] - | Cne -> [ addinst vn OEfeqs [ f1; f2 ] dest ] - | Clt -> [ addinst vn OEflts [ f1; f2 ] dest ] - | Cle -> [ addinst vn OEfles [ f1; f2 ] dest ] - | Cgt -> [ addinst vn OEflts [ f2; f1 ] dest ] - | Cge -> [ addinst vn OEfles [ f2; f1 ] dest ] - -let expanse_cbranchimm_int32s vn cmp a1 n info succ1 succ2 = - if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 [] - else - let r = r2pi () in - let l = loadimm32 vn r n in - let r', l' = extract_arg l in - cbranch_int32s false cmp a1 r' info succ1 succ2 l' - -let expanse_cbranchimm_int32u vn cmp a1 n info succ1 succ2 = - if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 [] - else - let r = r2pi () in - let l = loadimm32 vn r n in - let r', l' = extract_arg l in - cbranch_int32u false cmp a1 r' info succ1 succ2 l' - -let expanse_cbranchimm_int64s vn cmp a1 n info succ1 succ2 = - if Int64.eq n Int64.zero then - cbranch_int64s true cmp a1 a1 info succ1 succ2 [] - else - let r = r2pi () in - let l = loadimm64 vn r n in - let r', l' = extract_arg l in - cbranch_int64s false cmp a1 r' info succ1 succ2 l' - -let expanse_cbranchimm_int64u vn cmp a1 n info succ1 succ2 = - if Int64.eq n Int64.zero then - cbranch_int64u true cmp a1 a1 info succ1 succ2 [] - else - let r = r2pi () in - let l = loadimm64 vn r n in - let r', l' = extract_arg l in - cbranch_int64u false cmp a1 r' info succ1 succ2 l' - -let expanse_condimm_int32s vn cmp a1 n dest = - if Int.eq n Int.zero then cond_int32s vn true cmp a1 a1 dest - else - match cmp with - | Ceq | Cne -> - let r = r2pi () in - let l = xorimm32 vn a1 r n in - let r', l' = extract_arg l in - cond_int32s vn true cmp r' r' dest @ l' - | Clt -> sltimm32 vn a1 dest n - | Cle -> - if Int.eq n (Int.repr Int.max_signed) then - let l = loadimm32 vn dest Int.one in - let r, l' = extract_arg l in - addinst vn (OEmayundef MUint) [ a1; r ] dest :: l' - else sltimm32 vn a1 dest (Int.add n Int.one) - | _ -> - let r = r2pi () in - let l = loadimm32 vn r n in - let r', l' = extract_arg l in - cond_int32s vn false cmp a1 r' dest @ l' - -let expanse_condimm_int32u vn cmp a1 n dest = - if Int.eq n Int.zero then cond_int32u vn true cmp a1 a1 dest - else - match cmp with - | Clt -> sltuimm32 vn a1 dest n - | _ -> - let r = r2pi () in - let l = loadimm32 vn r n in - let r', l' = extract_arg l in - cond_int32u vn false cmp a1 r' dest @ l' - -let expanse_condimm_int64s vn cmp a1 n dest = - if Int64.eq n Int64.zero then cond_int64s vn true cmp a1 a1 dest - else - match cmp with - | Ceq | Cne -> - let r = r2pi () in - let l = xorimm64 vn a1 r n in - let r', l' = extract_arg l in - cond_int64s vn true cmp r' r' dest @ l' - | Clt -> sltimm64 vn a1 dest n - | Cle -> - if Int64.eq n (Int64.repr Int64.max_signed) then - let l = loadimm32 vn dest Int.one in - let r, l' = extract_arg l in - addinst vn (OEmayundef MUlong) [ a1; r ] dest :: l' - else sltimm64 vn a1 dest (Int64.add n Int64.one) - | _ -> - let r = r2pi () in - let l = loadimm64 vn r n in - let r', l' = extract_arg l in - cond_int64s vn false cmp a1 r' dest @ l' - -let expanse_condimm_int64u vn cmp a1 n dest = - if Int64.eq n Int64.zero then cond_int64u vn true cmp a1 a1 dest - else - match cmp with - | Clt -> sltuimm64 vn a1 dest n - | _ -> - let r = r2pi () in - let l = loadimm64 vn r n in - let r', l' = extract_arg l in - cond_int64u vn false cmp a1 r' dest @ l' - -let expanse_cond_fp vn cnot fn_cond cmp f1 f2 dest = - let normal = is_normal_cmp cmp in - let normal' = if cnot then not normal else normal in - let insn = fn_cond vn cmp f1 f2 dest in - if normal' then insn - else - let r', l = extract_arg insn in - addinst vn (OExoriw Int.one) [ r' ] dest :: l - -let expanse_cbranch_fp vn cnot fn_cond cmp f1 f2 info succ1 succ2 = - let r = r2pi () in - let normal = is_normal_cmp cmp in - let normal' = if cnot then not normal else normal in - let insn = fn_cond vn cmp f1 f2 r in - let r', l = extract_arg insn in - if normal' then - Sfinalcond (CEbnew (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l - else Sfinalcond (CEbeqw (Some X0_R), [ r'; r' ], succ1, succ2, info) :: l - -(** Form a list containing both sources and destination regs of an instruction *) - -let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] - -let get_regs_inst = function - | Inop _ -> [] - | Iop (_, args, dest, _) -> dest :: args - | Iload (_, _, _, args, dest, _) -> dest :: args - | Istore (_, _, args, src, _) -> src :: args - | Icall (_, t, args, dest, _) -> dest :: (get_regindent t @ args) - | Itailcall (_, t, args) -> get_regindent t @ args - | Ibuiltin (_, args, dest, _) -> - AST.params_of_builtin_res dest @ AST.params_of_builtin_args args - | Icond (_, args, _, _, _) -> args - | Ijumptable (arg, _) -> [ arg ] - | Ireturn (Some r) -> [ r ] - | _ -> [] - -(** Modify pathmap according to the size of the expansion list *) - -let write_pathmap initial esize pm' = - debug "write_pathmap: initial=%d, esize=%d\n" (p2i initial) esize; - let path = get_some @@ PTree.get initial !pm' in - let npsize = Camlcoq.Nat.of_int (esize + Camlcoq.Nat.to_int path.psize) in - let path' = - { - psize = npsize; - input_regs = path.input_regs; - pre_output_regs = path.pre_output_regs; - output_regs = path.output_regs; - } - in - pm' := PTree.set initial path' !pm' - -(** Write a single instruction in the tree and update order *) - -let write_inst target_node inst code' new_order = - code' := PTree.set (P.of_int target_node) inst !code'; - new_order := P.of_int target_node :: !new_order - -(** 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 - -(** Update the code tree with the expansion list *) - -let rec write_tree vn exp initial current code' new_order fturn = - debug "wt: node is %d\n" !node; - let target_node, next_node = - if fturn then (P.to_int initial, current) else (current, current - 1) - in - match exp with - | Sr r :: _ -> - failwith "write_tree: there are still some symbolic values in the list" - | Sexp (rd, Sop (op, vals), args, None) :: k -> - let args = get_arguments vn vals args in - let inst = Iop (op, args, rd, P.of_int next_node) in - write_inst target_node inst code' new_order; - write_tree vn k initial next_node code' new_order false - | [ Snop succ ] -> - let inst = Inop succ in - write_inst target_node inst code' new_order - | [ Sexp (rd, Sop (op, vals), args, Some succ) ] -> - let args = get_arguments vn vals args in - let inst = Iop (op, args, rd, succ) in - write_inst target_node inst code' new_order - | [ Sexp (rd, Smove, args, Some succ) ] -> - let inst = Iop (Omove, args, rd, succ) in - write_inst target_node inst code' new_order - | [ Sfinalcond (cond, args, succ1, succ2, info) ] -> - let inst = Icond (cond, args, succ1, succ2, info) in - write_inst target_node inst code' new_order - | [] -> () - | _ -> failwith "write_tree: invalid list" - -(** Main expansion function - TODO gourdinl to split? *) -let expanse (sb : superblock) code pm = - debug "#### New superblock for expansion oracle\n"; - let new_order = ref [] in - let liveins = ref sb.liveins in - let exp = ref [] in - let was_branch = ref false in - let was_exp = ref false in - let code' = ref code in - let pm' = ref pm in - let vn = ref (empty_numbering ()) in - Array.iter - (fun n -> - was_branch := false; - was_exp := false; - let inst = get_some @@ PTree.get n code in - (if !Clflags.option_fexpanse_rtlcond then - match inst with - (* Expansion of conditions - Ocmp *) - | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> - debug "Iop/Ccomp\n"; - exp := cond_int32s vn false c a1 a2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> - debug "Iop/Ccompu\n"; - exp := cond_int32u vn false c a1 a2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> - debug "Iop/Ccompimm\n"; - exp := expanse_condimm_int32s vn c a1 imm dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> - debug "Iop/Ccompuimm\n"; - exp := expanse_condimm_int32u vn c a1 imm dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> - debug "Iop/Ccompl\n"; - exp := cond_int64s vn false c a1 a2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) -> - debug "Iop/Ccomplu\n"; - exp := cond_int64u vn false c a1 a2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> - debug "Iop/Ccomplimm\n"; - exp := expanse_condimm_int64s vn c a1 imm dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> - debug "Iop/Ccompluimm\n"; - exp := expanse_condimm_int64u vn c a1 imm dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) -> - debug "Iop/Ccompf\n"; - exp := expanse_cond_fp vn false cond_float c f1 f2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) -> - debug "Iop/Cnotcompf\n"; - exp := expanse_cond_fp vn true cond_float c f1 f2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) -> - debug "Iop/Ccompfs\n"; - exp := expanse_cond_fp vn false cond_single c f1 f2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) -> - debug "Iop/Cnotcompfs\n"; - exp := expanse_cond_fp vn true cond_single c f1 f2 dest; - exp := extract_final vn !exp dest succ; - was_exp := true - (* Expansion of branches - Ccomp *) - | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccomp\n"; - exp := cbranch_int32s false c a1 a2 info succ1 succ2 []; - was_branch := true; - was_exp := true - | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompu\n"; - exp := cbranch_int32u false c a1 a2 info succ1 succ2 []; - was_branch := true; - was_exp := true - | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompimm\n"; - exp := expanse_cbranchimm_int32s vn c a1 imm info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompuimm\n"; - exp := expanse_cbranchimm_int32u vn c a1 imm info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompl\n"; - exp := cbranch_int64s false c a1 a2 info succ1 succ2 []; - was_branch := true; - was_exp := true - | Icond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccomplu\n"; - exp := cbranch_int64u false c a1 a2 info succ1 succ2 []; - was_branch := true; - was_exp := true - | Icond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, info) -> - debug "Icond/Ccomplimm\n"; - exp := expanse_cbranchimm_int64s vn c a1 imm info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompluimm\n"; - exp := expanse_cbranchimm_int64u vn c a1 imm info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompf\n"; - exp := - expanse_cbranch_fp vn false cond_float c f1 f2 info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) -> - debug "Icond/Cnotcompf\n"; - exp := expanse_cbranch_fp vn true cond_float c f1 f2 info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompfs\n"; - exp := - expanse_cbranch_fp vn false cond_single c f1 f2 info succ1 succ2; - was_branch := true; - was_exp := true - | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> - debug "Icond/Cnotcompfs\n"; - exp := - expanse_cbranch_fp vn true cond_single c f1 f2 info succ1 succ2; - was_branch := true; - was_exp := true - | _ -> ()); - (if !Clflags.option_fexpanse_others && not !was_exp then - match inst with - | Iop (Ofloatconst f, nil, dest, succ) -> ( - match make_immed64 (Floats.Float.to_bits f) with - | Imm64_single _ | Imm64_large _ -> () - | Imm64_pair (hi, lo) -> - debug "Iop/Ofloatconst\n"; - let r = r2pi () in - let l = load_hilo64 vn r hi lo in - let r', l' = extract_arg l in - exp := addinst vn Ofloat_of_bits [ r' ] dest :: l'; - exp := extract_final vn !exp dest succ; - was_exp := true) - | Iop (Osingleconst f, nil, dest, succ) -> ( - match make_immed32 (Floats.Float32.to_bits f) with - | Imm32_single imm -> () - | Imm32_pair (hi, lo) -> - debug "Iop/Osingleconst\n"; - let r = r2pi () in - let l = load_hilo32 vn r hi lo in - let r', l' = extract_arg l in - exp := addinst vn Osingle_of_bits [ r' ] dest :: l'; - exp := extract_final vn !exp dest succ; - was_exp := true) - | Iop (Ointconst n, nil, dest, succ) -> - debug "Iop/Ointconst\n"; - exp := loadimm32 vn dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Olongconst n, nil, dest, succ) -> - debug "Iop/Olongconst\n"; - exp := loadimm64 vn dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oaddimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oaddimm\n"; - exp := addimm32 vn a1 dest n None; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oaddlimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oaddlimm\n"; - exp := addimm64 vn a1 dest n None; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oandimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oandimm\n"; - exp := andimm32 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oandlimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oandlimm\n"; - exp := andimm64 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oorimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oorimm\n"; - exp := orimm32 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oorlimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oorlimm\n"; - exp := orimm64 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oxorimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oxorimm\n"; - exp := xorimm32 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oxorlimm n, a1 :: nil, dest, succ) -> - debug "Iop/Oxorlimm\n"; - exp := xorimm64 vn a1 dest n; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocast8signed, a1 :: nil, dest, succ) -> - debug "Iop/cast8signed\n"; - let op = Oshlimm (Int.repr (Z.of_sint 24)) in - let r = r2pi () in - let i1 = addinst vn op [ a1 ] r in - let r', l = extract_arg [ i1 ] in - exp := - addinst vn (Oshrimm (Int.repr (Z.of_sint 24))) [ r' ] dest :: l; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocast16signed, a1 :: nil, dest, succ) -> - debug "Iop/cast16signed\n"; - let op = Oshlimm (Int.repr (Z.of_sint 16)) in - let r = r2pi () in - let i1 = addinst vn op [ a1 ] r in - let r', l = extract_arg [ i1 ] in - exp := - addinst vn (Oshrimm (Int.repr (Z.of_sint 16))) [ r' ] dest :: l; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Ocast32unsigned, a1 :: nil, dest, succ) -> - debug "Iop/Ocast32unsigned\n"; - let r1 = r2pi () in - let r2 = r2pi () in - let op1 = Ocast32signed in - let i1 = addinst vn op1 [ a1 ] r1 in - let r1', l1 = extract_arg [ i1 ] in - - let op2 = Oshllimm (Int.repr (Z.of_sint 32)) in - let i2 = addinst vn op2 [ r1' ] r2 in - let r2', l2 = extract_arg (i2 :: l1) in - - let op3 = Oshrluimm (Int.repr (Z.of_sint 32)) in - exp := addinst vn op3 [ r2' ] dest :: l2; - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oshrximm n, a1 :: nil, dest, succ) -> - if Int.eq n Int.zero then ( - debug "Iop/Oshrximm1\n"; - exp := [ addinst vn (OEmayundef (MUshrx n)) [ a1; a1 ] dest ]) - else if Int.eq n Int.one then ( - debug "Iop/Oshrximm2\n"; - let r1 = r2pi () in - let r2 = r2pi () in - let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in - let i1 = addinst vn op1 [ a1 ] r1 in - let r1', l1 = extract_arg [ i1 ] in - - let op2 = Oadd in - let i2 = addinst vn op2 [ a1; r1' ] r2 in - let r2', l2 = extract_arg (i2 :: l1) in - - let op3 = Oshrimm Int.one in - let i3 = addinst vn op3 [ r2' ] dest in - let r3, l3 = extract_arg (i3 :: l2) in - exp := addinst vn (OEmayundef (MUshrx n)) [ r3; r3 ] dest :: l3) - else ( - debug "Iop/Oshrximm3\n"; - let r1 = r2pi () in - let r2 = r2pi () in - let r3 = r2pi () in - let op1 = Oshrimm (Int.repr (Z.of_sint 31)) in - let i1 = addinst vn op1 [ a1 ] r1 in - let r1', l1 = extract_arg [ i1 ] in - - let op2 = Oshruimm (Int.sub Int.iwordsize n) in - let i2 = addinst vn op2 [ r1' ] r2 in - let r2', l2 = extract_arg (i2 :: l1) in - - let op3 = Oadd in - let i3 = addinst vn op3 [ a1; r2' ] r3 in - let r3', l3 = extract_arg (i3 :: l2) in - - let op4 = Oshrimm n in - let i4 = addinst vn op4 [ r3' ] dest in - let r4, l4 = extract_arg (i4 :: l3) in - exp := addinst vn (OEmayundef (MUshrx n)) [ r4; r4 ] dest :: l4); - exp := extract_final vn !exp dest succ; - was_exp := true - | Iop (Oshrxlimm n, a1 :: nil, dest, succ) -> - if Int.eq n Int.zero then ( - debug "Iop/Oshrxlimm1\n"; - exp := [ addinst vn (OEmayundef (MUshrxl n)) [ a1; a1 ] dest ]) - else if Int.eq n Int.one then ( - debug "Iop/Oshrxlimm2\n"; - let r1 = r2pi () in - let r2 = r2pi () in - let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in - let i1 = addinst vn op1 [ a1 ] r1 in - let r1', l1 = extract_arg [ i1 ] in - - let op2 = Oaddl in - let i2 = addinst vn op2 [ a1; r1' ] r2 in - let r2', l2 = extract_arg (i2 :: l1) in - - let op3 = Oshrlimm Int.one in - let i3 = addinst vn op3 [ r2' ] dest in - let r3, l3 = extract_arg (i3 :: l2) in - exp := addinst vn (OEmayundef (MUshrxl n)) [ r3; r3 ] dest :: l3) - else ( - debug "Iop/Oshrxlimm3\n"; - let r1 = r2pi () in - let r2 = r2pi () in - let r3 = r2pi () in - let op1 = Oshrlimm (Int.repr (Z.of_sint 63)) in - let i1 = addinst vn op1 [ a1 ] r1 in - let r1', l1 = extract_arg [ i1 ] in - - let op2 = Oshrluimm (Int.sub Int64.iwordsize' n) in - let i2 = addinst vn op2 [ r1' ] r2 in - let r2', l2 = extract_arg (i2 :: l1) in - - let op3 = Oaddl in - let i3 = addinst vn op3 [ a1; r2' ] r3 in - let r3', l3 = extract_arg (i3 :: l2) in - - let op4 = Oshrlimm n in - let i4 = addinst vn op4 [ r3' ] dest in - let r4, l4 = extract_arg (i4 :: l3) in - exp := addinst vn (OEmayundef (MUshrxl n)) [ r4; r4 ] dest :: l4); - exp := extract_final vn !exp dest succ; - was_exp := true - | _ -> ()); - (* Update the CSE numbering *) - (if not !was_exp then - match inst with - | Iop (op, args, dest, succ) -> - let v = get_nvalues vn args in - addsop vn v op dest - | Iload (_, _, _, _, dst, _) -> set_unknown vn dst - | Istore (chk, addr, args, src, s) -> - !vn.seqs <- kill_mem_operations !vn.seqs - | Icall (_, _, _, _, _) | Itailcall (_, _, _) | Ibuiltin (_, _, _, _) -> - vn := empty_numbering () - | _ -> ()); - (* Update code, liveins, pathmap, and order of the superblock for one expansion *) - if !was_exp then ( - (if !was_branch && List.length !exp > 1 then - let lives = PTree.get n !liveins in - match lives with - | Some lives -> - let new_branch_pc = P.of_int (!node + 1) in - liveins := PTree.set new_branch_pc lives !liveins; - liveins := PTree.remove n !liveins - | _ -> ()); - node := !node + List.length !exp - 1; - write_pathmap sb.instructions.(0) (List.length !exp - 1) pm'; - write_tree vn (List.rev !exp) n !node code' new_order true) - else new_order := n :: !new_order) - sb.instructions; - sb.instructions <- Array.of_list (List.rev !new_order); - sb.liveins <- !liveins; - (!code', !pm') - -(** Compute the last used node and reg indexs *) - -let rec find_last_node_reg = function - | [] -> () - | (pc, i) :: 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 node [ pc ]; - traverse_list reg (get_regs_inst i); - find_last_node_reg k +let find_last_node_reg c = () -- cgit