diff options
Diffstat (limited to 'riscV/ExpansionOracle.ml')
-rw-r--r-- | riscV/ExpansionOracle.ml | 1019 |
1 files changed, 1019 insertions, 0 deletions
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml new file mode 100644 index 00000000..49ca7e96 --- /dev/null +++ b/riscV/ExpansionOracle.ml @@ -0,0 +1,1019 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Léo Gourdin UGA, VERIMAG *) +(* *) +(* Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) + +open BTL +open Op +open! Integers +open Camlcoq +open DebugPrint +open RTLcommonaux +open BTLcommonaux +open AST +open Datatypes +open Maps +open Asmgen + +(** Tools *) + +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 = + 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, def_iinfo ()) + +(** 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 iinfo succ1 succ2 k = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Scond (CEbeqw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cne -> Scond (CEbnew optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Clt -> Scond (CEbltw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cle -> Scond (CEbgew optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cgt -> Scond (CEbltw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cge -> Scond (CEbgew optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + +let cbranch_int32u is_x0 cmp a1 a2 iinfo succ1 succ2 k = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Scond (CEbequw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cne -> Scond (CEbneuw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Clt -> Scond (CEbltuw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cle -> Scond (CEbgeuw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cgt -> Scond (CEbltuw optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cge -> Scond (CEbgeuw optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + +let cbranch_int64s is_x0 cmp a1 a2 iinfo succ1 succ2 k = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Scond (CEbeql optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cne -> Scond (CEbnel optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Clt -> Scond (CEbltl optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cle -> Scond (CEbgel optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cgt -> Scond (CEbltl optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cge -> Scond (CEbgel optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + +let cbranch_int64u is_x0 cmp a1 a2 iinfo succ1 succ2 k = + let optR = make_optR is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Scond (CEbequl optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cne -> Scond (CEbneul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Clt -> Scond (CEbltul optR, [ a1; a2 ], succ1, succ2, iinfo) :: k + | Cle -> Scond (CEbgeul optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cgt -> Scond (CEbltul optR, [ a2; a1 ], succ1, succ2, iinfo) :: k + | Cge -> Scond (CEbgeul optR, [ a1; a2 ], succ1, succ2, iinfo) :: 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 iinfo succ1 succ2 = + if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 iinfo 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' iinfo succ1 succ2 l' + +let expanse_cbranchimm_int32u vn cmp a1 n iinfo succ1 succ2 = + if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 iinfo 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' iinfo succ1 succ2 l' + +let expanse_cbranchimm_int64s vn cmp a1 n iinfo succ1 succ2 = + if Int64.eq n Int64.zero then + cbranch_int64s true cmp a1 a1 iinfo 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' iinfo succ1 succ2 l' + +let expanse_cbranchimm_int64u vn cmp a1 n iinfo succ1 succ2 = + if Int64.eq n Int64.zero then + cbranch_int64u true cmp a1 a1 iinfo 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' iinfo 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 iinfo 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 + Scond (CEbnew (Some X0_R), [ r'; r' ], succ1, succ2, iinfo) :: l + else Scond (CEbeqw (Some X0_R), [ r'; r' ], succ1, succ2, 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) ] -> + let ib = Bcond (cond, args, succ1, succ2, iinfo) in + [ ib ] + | [] -> [] + | _ -> failwith "write_tree: invalid list" + +let expanse_list li = + debug "#### New block for expansion oracle\n"; + let exp = ref [] in + let was_branch = ref false 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_branch := false; + was_exp := false; + (if !Clflags.option_fexpanse_rtlcond then + match i with + (* Expansion of conditions - Ocmp *) + | Bop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, iinfo) -> + debug "Bop/Ccomp\n"; + exp := cond_int32s vn false c a1 a2 dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, iinfo) -> + debug "Bop/Ccompu\n"; + exp := cond_int32u vn false c a1 a2 dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, iinfo) -> + debug "Bop/Ccompimm\n"; + exp := expanse_condimm_int32s vn c a1 imm dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, iinfo) -> + debug "Bop/Ccompuimm\n"; + exp := expanse_condimm_int32u vn c a1 imm dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, iinfo) -> + debug "Bop/Ccompl\n"; + exp := cond_int64s vn false c a1 a2 dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, iinfo) -> + debug "Bop/Ccomplu\n"; + exp := cond_int64u vn false c a1 a2 dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, iinfo) -> + debug "Bop/Ccomplimm\n"; + exp := expanse_condimm_int64s vn c a1 imm dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, iinfo) -> + debug "Bop/Ccompluimm\n"; + exp := expanse_condimm_int64u vn c a1 imm dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, iinfo) -> + debug "Bop/Ccompf\n"; + exp := expanse_cond_fp vn false cond_float c f1 f2 dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, iinfo) -> + debug "Bop/Cnotcompf\n"; + exp := expanse_cond_fp vn true cond_float c f1 f2 dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, iinfo) -> + debug "Bop/Ccompfs\n"; + exp := expanse_cond_fp vn false cond_single c f1 f2 dest; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, iinfo) -> + debug "Bop/Cnotcompfs\n"; + exp := expanse_cond_fp vn true cond_single c f1 f2 dest; + exp := extract_final vn !exp dest; + was_exp := true + (* Expansion of branches - Ccomp *) + | Bcond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccomp\n"; + exp := cbranch_int32s false c a1 a2 iinfo succ1 succ2 []; + was_branch := true; + was_exp := true + | Bcond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompu\n"; + exp := cbranch_int32u false c a1 a2 iinfo succ1 succ2 []; + was_branch := true; + was_exp := true + | Bcond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompimm\n"; + exp := expanse_cbranchimm_int32s vn c a1 imm iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Ccompuimm (c, imm), a1 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompuimm\n"; + exp := expanse_cbranchimm_int32u vn c a1 imm iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Ccompl c, a1 :: a2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompl\n"; + exp := cbranch_int64s false c a1 a2 iinfo succ1 succ2 []; + was_branch := true; + was_exp := true + | Bcond (Ccomplu c, a1 :: a2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccomplu\n"; + exp := cbranch_int64u false c a1 a2 iinfo succ1 succ2 []; + was_branch := true; + was_exp := true + | Bcond (Ccomplimm (c, imm), a1 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccomplimm\n"; + exp := expanse_cbranchimm_int64s vn c a1 imm iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Ccompluimm (c, imm), a1 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompluimm\n"; + exp := expanse_cbranchimm_int64u vn c a1 imm iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompf\n"; + exp := + expanse_cbranch_fp vn false cond_float c f1 f2 iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Cnotcompf\n"; + exp := + expanse_cbranch_fp vn true cond_float c f1 f2 iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Ccompfs\n"; + exp := + expanse_cbranch_fp vn false cond_single c f1 f2 iinfo succ1 succ2; + was_branch := true; + was_exp := true + | Bcond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, iinfo) -> + debug "Bcond/Cnotcompfs\n"; + exp := + expanse_cbranch_fp vn true cond_single c f1 f2 iinfo succ1 succ2; + was_branch := true; + was_exp := true + | _ -> ()); + (if !Clflags.option_fexpanse_others && not !was_exp then + match i with + (* Others expansions *) + | Bop (Ofloatconst f, nil, dest, iinfo) -> ( + match make_immed64 (Floats.Float.to_bits f) with + | Imm64_single _ | Imm64_large _ -> () + | Imm64_pair (hi, lo) -> + debug "Bop/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; + was_exp := true) + | Bop (Osingleconst f, nil, dest, iinfo) -> ( + match make_immed32 (Floats.Float32.to_bits f) with + | Imm32_single imm -> () + | Imm32_pair (hi, lo) -> + debug "Bop/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; + was_exp := true) + | Bop (Ointconst n, nil, dest, iinfo) -> + debug "Bop/Ointconst\n"; + exp := loadimm32 vn dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Olongconst n, nil, dest, iinfo) -> + debug "Bop/Olongconst\n"; + exp := loadimm64 vn dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oaddimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oaddimm\n"; + exp := addimm32 vn a1 dest n None; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oaddlimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oaddlimm\n"; + exp := addimm64 vn a1 dest n None; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oandimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oandimm\n"; + exp := andimm32 vn a1 dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oandlimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oandlimm\n"; + exp := andimm64 vn a1 dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oorimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oorimm\n"; + exp := orimm32 vn a1 dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oorlimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oorlimm\n"; + exp := orimm64 vn a1 dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oxorimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oxorimm\n"; + exp := xorimm32 vn a1 dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Oxorlimm n, a1 :: nil, dest, iinfo) -> + debug "Bop/Oxorlimm\n"; + exp := xorimm64 vn a1 dest n; + exp := extract_final vn !exp dest; + was_exp := true + | Bop (Ocast8signed, a1 :: nil, dest, iinfo) -> + debug "Bop/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; + was_exp := true + | Bop (Ocast16signed, a1 :: nil, dest, iinfo) -> + debug "Bop/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; + was_exp := true + | Bop (Ocast32unsigned, a1 :: nil, dest, iinfo) -> + debug "Bop/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; + was_exp := true + | Bop (Oshrximm n, a1 :: nil, dest, iinfo) -> + if Int.eq n Int.zero then ( + debug "Bop/Oshrximm1\n"; + exp := [ addinst vn (OEmayundef (MUshrx n)) [ a1; a1 ] dest ]) + else if Int.eq n Int.one then ( + debug "Bop/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 "Bop/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; + was_exp := true + | Bop (Oshrxlimm n, a1 :: nil, dest, iinfo) -> + if Int.eq n Int.zero then ( + debug "Bop/Oshrxlimm1\n"; + exp := [ addinst vn (OEmayundef (MUshrxl n)) [ a1; a1 ] dest ]) + else if Int.eq n Int.one then ( + debug "Bop/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 "Bop/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; + 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 + let hd = gen_btl_list vn (List.rev !exp) in + hd @ 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 |