diff options
Diffstat (limited to 'riscV/ExpansionOracle.ml')
| -rw-r--r-- | riscV/ExpansionOracle.ml | 587 |
1 files changed, 414 insertions, 173 deletions
diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 27a36283..676b8da6 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -45,12 +45,26 @@ let n2pi () = node := !node + 1; n2p () -type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul - -let find_or_addnmove op args rd succ map_consts = +type immt = + | Addiw + | Addil + | Andiw + | Andil + | Oriw + | Oril + | Xoriw + | Xoril + | Sltiw + | Sltiuw + | Sltil + | Sltiul + +let find_or_addnmove op args rd succ map_consts node_dec = let sop = Sop (op, args) in match Hashtbl.find_opt map_consts sop with - | Some r -> Sr (P.of_int r) + | Some r -> + if node_dec then node := !node - 1; + Sr (P.of_int r) | None -> Hashtbl.add map_consts sop (p2i rd); Si (Iop (op, args, rd, succ)) @@ -58,93 +72,114 @@ let find_or_addnmove op args rd succ map_consts = let build_head_tuple head sv = match sv with Si i -> (head @ [ i ], None) | Sr r -> (head, Some r) -let load_hilo32 dest hi lo succ map_consts = +let unzip_head_tuple ht r = match ht with l, Some r' -> r' | l, None -> r + +let unzip_head_tuple_move ht r succ = + match ht with l, Some r' -> [ Iop (Omove, [ r' ], r, succ) ] | l, None -> l + +let build_full_ilist op args dest succ hd k map_consts = + let sv = find_or_addnmove op args dest succ map_consts false in + let ht = build_head_tuple hd sv in + unzip_head_tuple_move ht dest succ @ k + +let load_hilo32 dest hi lo succ map_consts node_dec = let op1 = OEluiw hi in if Int.eq lo Int.zero then - let sv = find_or_addnmove op1 [] dest succ map_consts in + let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in build_head_tuple [] sv else let r = r2pi () in - let op2 = Oaddimm lo in - match find_or_addnmove op1 [] r (n2pi ()) map_consts with - | Si i -> - let sv = find_or_addnmove op2 [ r ] dest succ map_consts in - build_head_tuple [ i ] sv - | Sr r' -> - let sv = find_or_addnmove op2 [ r' ] dest succ map_consts in - build_head_tuple [] sv - -let load_hilo64 dest hi lo succ map_consts = + let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts node_dec in + let ht1 = build_head_tuple [] sv1 in + let r' = unzip_head_tuple ht1 r in + let op2 = OEaddiw lo in + let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts node_dec in + build_head_tuple (fst ht1) sv2 + +let load_hilo64 dest hi lo succ map_consts node_dec = let op1 = OEluil hi in if Int64.eq lo Int64.zero then - let sv = find_or_addnmove op1 [] dest succ map_consts in + let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in build_head_tuple [] sv else let r = r2pi () in - let op2 = Oaddlimm lo in - match find_or_addnmove op1 [] r (n2pi ()) map_consts with - | Si i -> - let sv = find_or_addnmove op2 [ r ] dest succ map_consts in - build_head_tuple [ i ] sv - | Sr r' -> - let sv = find_or_addnmove op2 [ r' ] dest succ map_consts in - build_head_tuple [] sv - -let loadimm32 dest n succ map_consts = + let sv1 = find_or_addnmove op1 [] r (n2pi ()) map_consts node_dec in + let ht1 = build_head_tuple [] sv1 in + let r' = unzip_head_tuple ht1 r in + let op2 = OEaddil lo in + let sv2 = find_or_addnmove op2 [ r' ] dest succ map_consts node_dec in + build_head_tuple (fst ht1) sv2 + +let loadimm32 dest n succ map_consts node_dec = match make_immed32 n with | Imm32_single imm -> let op1 = OEaddiwr0 imm in - let sv = find_or_addnmove op1 [] dest succ map_consts in + let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in build_head_tuple [] sv - | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts + | Imm32_pair (hi, lo) -> load_hilo32 dest hi lo succ map_consts node_dec -let loadimm64 dest n succ map_consts = +let loadimm64 dest n succ map_consts node_dec = match make_immed64 n with | Imm64_single imm -> let op1 = OEaddilr0 imm in - let sv = find_or_addnmove op1 [] dest succ map_consts in + let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in build_head_tuple [] sv - | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts + | Imm64_pair (hi, lo) -> load_hilo64 dest hi lo succ map_consts node_dec | Imm64_large imm -> let op1 = OEloadli imm in - let sv = find_or_addnmove op1 [] dest succ map_consts in + let sv = find_or_addnmove op1 [] dest succ map_consts node_dec in build_head_tuple [] sv let get_opimm imm = function + | Addiw -> OEaddiw imm + | Andiw -> OEandiw imm + | Oriw -> OEoriw imm | Xoriw -> OExoriw imm | Sltiw -> OEsltiw imm | Sltiuw -> OEsltiuw imm + | Addil -> OEaddil imm + | Andil -> OEandil imm + | Oril -> OEoril imm | Xoril -> OExoril imm | Sltil -> OEsltil imm | Sltiul -> OEsltiul imm -let unzip_head_tuple ht r = match ht with l, Some r' -> r' | l, None -> r - let opimm32 a1 dest n succ k op opimm map_consts = match make_immed32 n with - | Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k + | Imm32_single imm -> + build_full_ilist (get_opimm imm opimm) [ a1 ] dest succ [] k map_consts | Imm32_pair (hi, lo) -> let r = r2pi () in - let ht = load_hilo32 r hi lo (n2pi ()) map_consts in + let ht = load_hilo32 r hi lo (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in - fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k + build_full_ilist op [ a1; r' ] dest succ (fst ht) k map_consts let opimm64 a1 dest n succ k op opimm map_consts = match make_immed64 n with - | Imm64_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k + | Imm64_single imm -> + build_full_ilist (get_opimm imm opimm) [ a1 ] dest succ [] k map_consts | Imm64_pair (hi, lo) -> let r = r2pi () in - let ht = load_hilo64 r hi lo (n2pi ()) map_consts in + let ht = load_hilo64 r hi lo (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in - fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k - | Imm64_large imm -> + build_full_ilist op [ a1; r' ] dest succ (fst ht) k map_consts + | Imm64_large imm ->( let r = r2pi () in let op1 = OEloadli imm in let inode = n2pi () in - let sv = find_or_addnmove op1 [] r inode map_consts in + let sv = find_or_addnmove op1 [] r inode map_consts true in let ht = build_head_tuple [] sv in let r' = unzip_head_tuple ht r in - fst ht @ Iop (op, [ a1; r' ], dest, succ) :: k + build_full_ilist op [ a1; r' ] dest succ (fst ht) k map_consts) + +let addimm32 a1 dest n succ k map_consts = + opimm32 a1 dest n succ k Oadd Addiw map_consts + +let andimm32 a1 dest n succ k map_consts = + opimm32 a1 dest n succ k Oand Andiw map_consts + +let orimm32 a1 dest n succ k map_consts = + opimm32 a1 dest n succ k Oor Oriw map_consts let xorimm32 a1 dest n succ k map_consts = opimm32 a1 dest n succ k Oxor Xoriw map_consts @@ -155,6 +190,12 @@ let sltimm32 a1 dest n succ k map_consts = let sltuimm32 a1 dest n succ k map_consts = opimm32 a1 dest n succ k (OEsltuw None) Sltiuw map_consts +let addimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oaddl Addil + +let andimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oandl Andil + +let orimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oorl Oril + let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril let sltimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltl None) Sltil @@ -205,95 +246,119 @@ let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k = | Cgt -> Icond (CEbltul optR0, [ a2; a1 ], succ1, succ2, info) :: k | Cge -> Icond (CEbgeul optR0, [ a1; a2 ], succ1, succ2, info) :: k -let cond_int32s is_x0 cmp a1 a2 dest tmp_reg succ k = +let cond_int32s is_x0 cmp a1 a2 dest tmp_reg succ map_consts = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEseqw optR0, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsnew optR0, [ a1; a2 ], dest, succ) :: k - | Clt -> Iop (OEsltw optR0, [ a1; a2 ], dest, succ) :: k + | Ceq -> [ Iop (OEseqw optR0, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsnew optR0, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltw optR0, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - Iop (OEsltw optR0, [ a2; a1 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k - | Cgt -> Iop (OEsltw optR0, [ a2; a1 ], dest, succ) :: k + let op = OEsltw optR0 in + let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] + | Cgt -> [ Iop (OEsltw optR0, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - Iop (OEsltw optR0, [ a1; a2 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + let op = OEsltw optR0 in + let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] -let cond_int32u is_x0 cmp a1 a2 dest tmp_reg succ k = +let cond_int32u is_x0 cmp a1 a2 dest tmp_reg succ map_consts = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEsequw optR0, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsneuw optR0, [ a1; a2 ], dest, succ) :: k - | Clt -> Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) :: k + | Ceq -> [ Iop (OEsequw optR0, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsneuw optR0, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - Iop (OEsltuw optR0, [ a2; a1 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k - | Cgt -> Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) :: k + let op = OEsltuw optR0 in + let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] + | Cgt -> [ Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - Iop (OEsltuw optR0, [ a1; a2 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + let op = OEsltuw optR0 in + let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] -let cond_int64s is_x0 cmp a1 a2 dest tmp_reg succ k = +let cond_int64s is_x0 cmp a1 a2 dest tmp_reg succ map_consts = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEseql optR0, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsnel optR0, [ a1; a2 ], dest, succ) :: k - | Clt -> Iop (OEsltl optR0, [ a1; a2 ], dest, succ) :: k + | Ceq -> [ Iop (OEseql optR0, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsnel optR0, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltl optR0, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - Iop (OEsltl optR0, [ a2; a1 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k - | Cgt -> Iop (OEsltl optR0, [ a2; a1 ], dest, succ) :: k + let op = OEsltl optR0 in + let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] + | Cgt -> [ Iop (OEsltl optR0, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - Iop (OEsltl optR0, [ a1; a2 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + let op = OEsltl optR0 in + let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] -let cond_int64u is_x0 cmp a1 a2 dest tmp_reg succ k = +let cond_int64u is_x0 cmp a1 a2 dest tmp_reg succ map_consts = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEsequl optR0, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsneul optR0, [ a1; a2 ], dest, succ) :: k - | Clt -> Iop (OEsltul optR0, [ a1; a2 ], dest, succ) :: k + | Ceq -> [ Iop (OEsequl optR0, [ a1; a2 ], dest, succ) ] + | Cne -> [ Iop (OEsneul optR0, [ a1; a2 ], dest, succ) ] + | Clt -> [ Iop (OEsltul optR0, [ a1; a2 ], dest, succ) ] | Cle -> let r = r2pi () in - Iop (OEsltul optR0, [ a2; a1 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k - | Cgt -> Iop (OEsltul optR0, [ a2; a1 ], dest, succ) :: k + let op = OEsltul optR0 in + let sv = find_or_addnmove op [ a2; a1 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] + | Cgt -> [ Iop (OEsltul optR0, [ a2; a1 ], dest, succ) ] | Cge -> let r = r2pi () in - Iop (OEsltul optR0, [ a1; a2 ], r, get tmp_reg) - :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k + let op = OEsltul optR0 in + let sv = find_or_addnmove op [ a1; a2 ] r (get tmp_reg) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + fst ht @ [ Iop (OExoriw Int.one, [ r' ], dest, succ) ] let is_normal_cmp = function Cne -> false | _ -> true -let cond_float cmp f1 f2 dest succ = +let cond_float cmp f1 f2 dest succ map_consts = match cmp with - | Ceq -> Iop (OEfeqd, [ f1; f2 ], dest, succ) - | Cne -> Iop (OEfeqd, [ f1; f2 ], dest, succ) - | Clt -> Iop (OEfltd, [ f1; f2 ], dest, succ) - | Cle -> Iop (OEfled, [ f1; f2 ], dest, succ) - | Cgt -> Iop (OEfltd, [ f2; f1 ], dest, succ) - | Cge -> Iop (OEfled, [ f2; f1 ], dest, succ) - -let cond_single cmp f1 f2 dest succ = + | Ceq -> [ Iop (OEfeqd, [ f1; f2 ], dest, succ) ] + | Cne -> [ Iop (OEfeqd, [ f1; f2 ], dest, succ) ] + | Clt -> [ Iop (OEfltd, [ f1; f2 ], dest, succ) ] + | Cle -> [ Iop (OEfled, [ f1; f2 ], dest, succ) ] + | Cgt -> [ Iop (OEfltd, [ f2; f1 ], dest, succ) ] + | Cge -> [ Iop (OEfled, [ f2; f1 ], dest, succ) ] + +let cond_single cmp f1 f2 dest succ map_consts = match cmp with - | Ceq -> Iop (OEfeqs, [ f1; f2 ], dest, succ) - | Cne -> Iop (OEfeqs, [ f1; f2 ], dest, succ) - | Clt -> Iop (OEflts, [ f1; f2 ], dest, succ) - | Cle -> Iop (OEfles, [ f1; f2 ], dest, succ) - | Cgt -> Iop (OEflts, [ f2; f1 ], dest, succ) - | Cge -> Iop (OEfles, [ f2; f1 ], dest, succ) + | Ceq -> [ Iop (OEfeqs, [ f1; f2 ], dest, succ) ] + | Cne -> [ Iop (OEfeqs, [ f1; f2 ], dest, succ) ] + | Clt -> [ Iop (OEflts, [ f1; f2 ], dest, succ) ] + | Cle -> [ Iop (OEfles, [ f1; f2 ], dest, succ) ] + | Cgt -> [ Iop (OEflts, [ f2; f1 ], dest, succ) ] + | Cge -> [ Iop (OEfles, [ f2; f1 ], dest, succ) ] let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k map_consts = if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k else let r = r2pi () in - let ht = loadimm32 r n (n2pi ()) map_consts in + let ht = loadimm32 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in fst ht @ cbranch_int32s false cmp a1 r' info succ1 succ2 k @@ -301,7 +366,7 @@ let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k map_consts = if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k else let r = r2pi () in - let ht = loadimm32 r n (n2pi ()) map_consts in + let ht = loadimm32 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in fst ht @ cbranch_int32u false cmp a1 r' info succ1 succ2 k @@ -309,7 +374,7 @@ let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k map_consts = if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k else let r = r2pi () in - let ht = loadimm64 r n (n2pi ()) map_consts in + let ht = loadimm64 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in fst ht @ cbranch_int64s false cmp a1 r' info succ1 succ2 k @@ -317,102 +382,103 @@ let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k map_consts = if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k else let r = r2pi () in - let ht = loadimm64 r n (n2pi ()) map_consts in + let ht = loadimm64 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in fst ht @ cbranch_int64u false cmp a1 r' info succ1 succ2 k let get_tmp_reg = function Cle | Cge -> Some (n2pi ()) | _ -> None -let expanse_condimm_int32s cmp a1 n dest succ k map_consts = +let expanse_condimm_int32s cmp a1 n dest succ map_consts = if Int.eq n Int.zero then let tmp_reg = get_tmp_reg cmp in - cond_int32s true cmp a1 a1 dest tmp_reg succ k + cond_int32s true cmp a1 a1 dest tmp_reg succ map_consts else match cmp with | Ceq | Cne -> let r = r2pi () in xorimm32 a1 r n (n2pi ()) - (cond_int32s true cmp r r dest None succ k) + (cond_int32s true cmp r r dest None succ map_consts) map_consts - | Clt -> sltimm32 a1 dest n succ k map_consts + | Clt -> sltimm32 a1 dest n succ [] map_consts | Cle -> if Int.eq n (Int.repr Int.max_signed) then - let ht = loadimm32 dest Int.one succ map_consts in - fst ht @ k - else sltimm32 a1 dest (Int.add n Int.one) succ k map_consts + let ht = loadimm32 dest Int.one succ map_consts false in + fst ht + else sltimm32 a1 dest (Int.add n Int.one) succ [] map_consts | _ -> let r = r2pi () in let tmp_reg = get_tmp_reg cmp in - let ht = loadimm32 r n (n2pi ()) map_consts in + let ht = loadimm32 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in - fst ht @ cond_int32s false cmp a1 r' dest tmp_reg succ k + fst ht @ cond_int32s false cmp a1 r' dest tmp_reg succ map_consts -let expanse_condimm_int32u cmp a1 n dest succ k map_consts = +let expanse_condimm_int32u cmp a1 n dest succ map_consts = let tmp_reg = get_tmp_reg cmp in - if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest tmp_reg succ k + if Int.eq n Int.zero then + cond_int32u true cmp a1 a1 dest tmp_reg succ map_consts else match cmp with - | Clt -> sltuimm32 a1 dest n succ k map_consts + | Clt -> sltuimm32 a1 dest n succ [] map_consts | _ -> let r = r2pi () in - let ht = loadimm32 r n (n2pi ()) map_consts in + let ht = loadimm32 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in - fst ht @ cond_int32u false cmp a1 r' dest tmp_reg succ k + fst ht @ cond_int32u false cmp a1 r' dest tmp_reg succ map_consts -let expanse_condimm_int64s cmp a1 n dest succ k map_consts = +let expanse_condimm_int64s cmp a1 n dest succ map_consts = if Int64.eq n Int64.zero then let tmp_reg = get_tmp_reg cmp in - cond_int64s true cmp a1 a1 dest tmp_reg succ k + cond_int64s true cmp a1 a1 dest tmp_reg succ map_consts else match cmp with | Ceq | Cne -> let r = r2pi () in xorimm64 a1 r n (n2pi ()) - (cond_int64s true cmp r r dest None succ k) + (cond_int64s true cmp r r dest None succ map_consts) map_consts - | Clt -> sltimm64 a1 dest n succ k map_consts + | Clt -> sltimm64 a1 dest n succ [] map_consts | Cle -> if Int64.eq n (Int64.repr Int64.max_signed) then - let ht = loadimm32 dest Int.one succ map_consts in - fst ht @ k - else sltimm64 a1 dest (Int64.add n Int64.one) succ k map_consts + let ht = loadimm32 dest Int.one succ map_consts false in + fst ht + else sltimm64 a1 dest (Int64.add n Int64.one) succ [] map_consts | _ -> let r = r2pi () in let tmp_reg = get_tmp_reg cmp in - let ht = loadimm64 r n (n2pi ()) map_consts in + let ht = loadimm64 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in - fst ht @ cond_int64s false cmp a1 r' dest tmp_reg succ k + fst ht @ cond_int64s false cmp a1 r' dest tmp_reg succ map_consts -let expanse_condimm_int64u cmp a1 n dest succ k map_consts = +let expanse_condimm_int64u cmp a1 n dest succ map_consts = let tmp_reg = get_tmp_reg cmp in - if Int64.eq n Int64.zero then cond_int64u true cmp a1 a1 dest tmp_reg succ k + if Int64.eq n Int64.zero then + cond_int64u true cmp a1 a1 dest tmp_reg succ map_consts else match cmp with - | Clt -> sltuimm64 a1 dest n succ k map_consts + | Clt -> sltuimm64 a1 dest n succ [] map_consts | _ -> let r = r2pi () in - let ht = loadimm64 r n (n2pi ()) map_consts in + let ht = loadimm64 r n (n2pi ()) map_consts true in let r' = unzip_head_tuple ht r in - fst ht @ cond_int64u false cmp a1 r' dest tmp_reg succ k + fst ht @ cond_int64u false cmp a1 r' dest tmp_reg succ map_consts -let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k = +let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ map_consts = let normal = is_normal_cmp cmp in let normal' = if cnot then not normal else normal in let succ' = if normal' then succ else n2pi () in - let insn = fn_cond cmp f1 f2 dest succ' in - insn - :: (if normal' then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k) + let insn = fn_cond cmp f1 f2 dest succ' map_consts in + if normal' then insn + else build_full_ilist (OExoriw Int.one) [ dest ] dest succ insn [] map_consts -let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k = +let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 map_consts = 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 cmp f1 f2 r (n2pi ()) in + let insn = List.hd (fn_cond cmp f1 f2 r (n2pi ()) map_consts) in insn :: - (if normal' then Icond (CEbnew (Some false), [ r; r ], succ1, succ2, info) - else Icond (CEbeqw (Some false), [ r; r ], succ1, succ2, info)) - :: k + (if normal' then [ Icond (CEbnew (Some false), [ r; r ], succ1, succ2, info) ] + else [ Icond (CEbeqw (Some false), [ r; r ], succ1, succ2, info) ]) let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] @@ -447,24 +513,19 @@ let write_pathmap initial esize pm' = in pm' := PTree.set initial path' !pm' -let rec write_tree exp initial current code' new_order = +let rec write_tree exp initial current code' new_order fturn = + (*Printf.eprintf "wt: node is %d\n" !node;*) let target_node, next_node = - if current = !node then ( - node := !node + 1; - (P.to_int initial, current)) - else (current, current - 1) + if fturn then (P.to_int initial, current) else (current, current - 1) in match exp with - | (Iop (_, _, _, succ) as inst) :: k -> + | inst :: k -> + (*let open PrintRTL in*) + (*print_instruction stderr (target_node, inst);*) code' := PTree.set (P.of_int target_node) inst !code'; new_order := P.of_int target_node :: !new_order; - write_tree k initial next_node code' new_order - | (Icond (_, _, succ1, succ2, _) as inst) :: k -> - code' := PTree.set (P.of_int target_node) inst !code'; - new_order := P.of_int target_node :: !new_order; - write_tree k initial next_node code' new_order + write_tree k initial next_node code' new_order false | [] -> () - | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction." let expanse (sb : superblock) code pm = (*debug_flag := true;*) @@ -487,54 +548,54 @@ let expanse (sb : superblock) code pm = | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> debug "Iop/Ccomp\n"; let tmp_reg = get_tmp_reg c in - exp := cond_int32s false c a1 a2 dest tmp_reg succ []; + exp := cond_int32s false c a1 a2 dest tmp_reg succ map_consts; was_exp := true | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> debug "Iop/Ccompu\n"; let tmp_reg = get_tmp_reg c in - exp := cond_int32u false c a1 a2 dest tmp_reg succ []; + exp := cond_int32u false c a1 a2 dest tmp_reg succ map_consts; was_exp := true | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccompimm\n"; - exp := expanse_condimm_int32s c a1 imm dest succ [] map_consts; + exp := expanse_condimm_int32s c a1 imm dest succ map_consts; was_exp := true | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccompuimm\n"; - exp := expanse_condimm_int32u c a1 imm dest succ [] map_consts; + exp := expanse_condimm_int32u c a1 imm dest succ map_consts; was_exp := true | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> debug "Iop/Ccompl\n"; let tmp_reg = get_tmp_reg c in - exp := cond_int64s false c a1 a2 dest tmp_reg succ []; + exp := cond_int64s false c a1 a2 dest tmp_reg succ map_consts; was_exp := true | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) -> debug "Iop/Ccomplu\n"; let tmp_reg = get_tmp_reg c in - exp := cond_int64u false c a1 a2 dest tmp_reg succ []; + exp := cond_int64u false c a1 a2 dest tmp_reg succ map_consts; was_exp := true | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccomplimm\n"; - exp := expanse_condimm_int64s c a1 imm dest succ [] map_consts; + exp := expanse_condimm_int64s c a1 imm dest succ map_consts; was_exp := true | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> debug "Iop/Ccompluimm\n"; - exp := expanse_condimm_int64u c a1 imm dest succ [] map_consts; + exp := expanse_condimm_int64u c a1 imm dest succ map_consts; was_exp := true | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) -> debug "Iop/Ccompf\n"; - exp := expanse_cond_fp false cond_float c f1 f2 dest succ []; + exp := expanse_cond_fp false cond_float c f1 f2 dest succ map_consts; was_exp := true | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) -> debug "Iop/Cnotcompf\n"; - exp := expanse_cond_fp true cond_float c f1 f2 dest succ []; + exp := expanse_cond_fp true cond_float c f1 f2 dest succ map_consts; was_exp := true | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) -> debug "Iop/Ccompfs\n"; - exp := expanse_cond_fp false cond_single c f1 f2 dest succ []; + exp := expanse_cond_fp false cond_single c f1 f2 dest succ map_consts; was_exp := true | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) -> debug "Iop/Cnotcompfs\n"; - exp := expanse_cond_fp true cond_single c f1 f2 dest succ []; + exp := expanse_cond_fp true cond_single c f1 f2 dest succ map_consts; was_exp := true (* Expansion of branches - Ccomp *) | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> @@ -584,24 +645,29 @@ let expanse (sb : superblock) code pm = | Icond (Ccompf c, f1 :: f2 :: nil, succ1, succ2, info) -> debug "Icond/Ccompf\n"; exp := - expanse_cbranch_fp false cond_float c f1 f2 info succ1 succ2 []; + expanse_cbranch_fp false cond_float c f1 f2 info succ1 succ2 + map_consts; was_branch := true; was_exp := true | Icond (Cnotcompf c, f1 :: f2 :: nil, succ1, succ2, info) -> debug "Icond/Cnotcompf\n"; - exp := expanse_cbranch_fp true cond_float c f1 f2 info succ1 succ2 []; + exp := + expanse_cbranch_fp true cond_float c f1 f2 info succ1 succ2 + map_consts; was_branch := true; was_exp := true | Icond (Ccompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> debug "Icond/Ccompfs\n"; exp := - expanse_cbranch_fp false cond_single c f1 f2 info succ1 succ2 []; + expanse_cbranch_fp false cond_single c f1 f2 info succ1 succ2 + map_consts; was_branch := true; was_exp := true | Icond (Cnotcompfs c, f1 :: f2 :: nil, succ1, succ2, info) -> debug "Icond/Cnotcompfs\n"; exp := - expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 []; + expanse_cbranch_fp true cond_single c f1 f2 info succ1 succ2 + map_consts; was_branch := true; was_exp := true | _ -> ()); @@ -611,22 +677,197 @@ let expanse (sb : superblock) code pm = | Iop (Ofloatconst f, nil, dest, succ) -> debug "Iop/Ofloatconst\n"; let r = r2pi () in + let ht = loadimm64 r (Floats.Float.to_bits f) (n2pi ()) map_consts true in + let r' = unzip_head_tuple ht r in exp := - [ - Iop (Olongconst (Floats.Float.to_bits f), [], r, n2pi ()); - Iop (Ofloat_of_bits, [ r ], dest, succ); - ]; + build_full_ilist Ofloat_of_bits [ r' ] dest succ (fst ht) [] + map_consts; was_exp := true | Iop (Osingleconst f, nil, dest, succ) -> debug "Iop/Osingleconst\n"; let r = r2pi () in + let ht = + loadimm32 r (Floats.Float32.to_bits f) (n2pi ()) map_consts true + in + let r' = unzip_head_tuple ht r in exp := - [ - Iop (Ointconst (Floats.Float32.to_bits f), [], r, n2pi ()); - Iop (Osingle_of_bits, [ r ], dest, succ); - ]; + build_full_ilist Osingle_of_bits [ r' ] dest succ (fst ht) [] + map_consts; was_exp := true | _ -> ()); + + (* TODO gourdinl flag ? *) + (match inst with + | Iop (Ointconst n, nil, dest, succ) -> + debug "Iop/Ointconst\n"; + let ht = loadimm32 dest n succ map_consts false in + exp := unzip_head_tuple_move ht dest succ; + was_exp := true + | Iop (Olongconst n, nil, dest, succ) -> + debug "Iop/Olongconst\n"; + let ht = loadimm64 dest n succ map_consts false in + exp := unzip_head_tuple_move ht dest succ; + was_exp := true + | Iop (Oaddimm n, a1 :: nil, dest, succ) -> + debug "Iop/Oaddimm\n"; + exp := addimm32 a1 dest n succ [] map_consts; + was_exp := true + | Iop (Oaddlimm n, a1 :: nil, dest, succ) -> + debug "Iop/Oaddlimm\n"; + exp := addimm64 a1 dest n succ [] map_consts; + was_exp := true + | Iop (Oandimm n, a1 :: nil, dest, succ) -> + debug "Iop/Oandimm\n"; + exp := andimm32 a1 dest n succ [] map_consts; + was_exp := true + | Iop (Oandlimm n, a1 :: nil, dest, succ) -> + debug "Iop/Oandlimm\n"; + exp := andimm64 a1 dest n succ [] map_consts; + was_exp := true + | Iop (Oorimm n, a1 :: nil, dest, succ) -> + debug "Iop/Oorimm\n"; + exp := orimm32 a1 dest n succ [] map_consts; + was_exp := true + | Iop (Oorlimm n, a1 :: nil, dest, succ) -> + debug "Iop/Oorlimm\n"; + exp := orimm64 a1 dest n succ [] map_consts; + was_exp := true + | Iop (Ocast8signed, a1 :: nil, dest, succ) -> + debug "Iop/cast8signed"; + let op = Oshlimm (Int.repr (Z.of_sint 24)) in + let r = r2pi () in + let sv = find_or_addnmove op [ a1 ] r (n2pi ()) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + exp := + build_full_ilist + (Oshrimm (Int.repr (Z.of_sint 24))) + [ r' ] dest succ (fst ht) [] map_consts; + was_exp := true + | Iop (Ocast16signed, a1 :: nil, dest, succ) -> + debug "Iop/cast8signed"; + let op = Oshlimm (Int.repr (Z.of_sint 16)) in + let r = r2pi () in + let sv = find_or_addnmove op [ a1 ] r (n2pi ()) map_consts true in + let ht = build_head_tuple [] sv in + let r' = unzip_head_tuple ht r in + exp := + build_full_ilist + (Oshrimm (Int.repr (Z.of_sint 16))) + [ r' ] dest succ (fst ht) [] map_consts; + was_exp := true + | Iop (Ocast32unsigned, a1 :: nil, dest, succ) -> + debug "Iop/Ocast32unsigned"; + let n2 = n2pi () in + let n1 = n2pi () in + let r1 = r2pi () in + let r2 = r2pi () in + let op1 = Ocast32signed in + let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in + let ht1 = build_head_tuple [] sv1 in + let r1' = unzip_head_tuple ht1 r1 in + + let op2 = Oshllimm (Int.repr (Z.of_sint 32)) in + let sv2 = find_or_addnmove op2 [ r1' ] r2 n2 map_consts true in + let ht2 = build_head_tuple (fst ht1) sv2 in + let r2' = unzip_head_tuple ht2 r2 in + + let op3 = Oshrluimm (Int.repr (Z.of_sint 32)) in + exp := build_full_ilist op3 [ r2' ] dest succ (fst ht2) [] map_consts + | Iop (Oshrximm n, a1 :: nil, dest, succ) -> + debug "Iop/Oshrximm"; + if Int.eq n Int.zero then exp := [ Iop (Omove, [ a1 ], dest, succ) ] + else if Int.eq n Int.one then + let n2 = n2pi () in + let n1 = n2pi () in + let r1 = r2pi () in + let r2 = r2pi () in + let op1 = Oshruimm (Int.repr (Z.of_sint 31)) in + let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in + let ht1 = build_head_tuple [] sv1 in + let r1' = unzip_head_tuple ht1 r1 in + + let op2 = Oadd in + let sv2 = find_or_addnmove op2 [ a1; r1' ] r2 n2 map_consts true in + let ht2 = build_head_tuple (fst ht1) sv2 in + let r2' = unzip_head_tuple ht2 r2 in + + let op3 = Oshrimm Int.one in + exp := + build_full_ilist op3 [ r2' ] dest succ (fst ht2) [] map_consts + else + let n3 = n2pi () in + let n2 = n2pi () in + let n1 = n2pi () in + let r1 = r2pi () in + let r2 = r2pi () in + let r3 = r2pi () in + let op1 = Oshrimm (Int.repr (Z.of_sint 31)) in + let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in + let ht1 = build_head_tuple [] sv1 in + let r1' = unzip_head_tuple ht1 r1 in + + let op2 = Oshruimm (Int.sub Int.iwordsize n) in + let sv2 = find_or_addnmove op2 [ r1' ] r2 n2 map_consts true in + let ht2 = build_head_tuple (fst ht1) sv2 in + let r2' = unzip_head_tuple ht2 r2 in + + let op3 = Oadd in + let sv3 = find_or_addnmove op3 [ a1; r2' ] r3 n3 map_consts true in + let ht3 = build_head_tuple (fst ht2) sv3 in + let r3' = unzip_head_tuple ht3 r3 in + + let op4 = Oshrimm n in + exp := + build_full_ilist op4 [ r3' ] dest succ (fst ht3) [] map_consts + | Iop (Oshrxlimm n, a1 :: nil, dest, succ) -> + debug "Iop/Oshrxlimm"; + if Int.eq n Int.zero then exp := [ Iop (Omove, [ a1 ], dest, succ) ] + else if Int.eq n Int.one then + let n2 = n2pi () in + let n1 = n2pi () in + let r1 = r2pi () in + let r2 = r2pi () in + let op1 = Oshrluimm (Int.repr (Z.of_sint 63)) in + let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in + let ht1 = build_head_tuple [] sv1 in + let r1' = unzip_head_tuple ht1 r1 in + + let op2 = Oaddl in + let sv2 = find_or_addnmove op2 [ a1; r1' ] r2 n2 map_consts true in + let ht2 = build_head_tuple (fst ht1) sv2 in + let r2' = unzip_head_tuple ht2 r2 in + + let op3 = Oshrlimm Int.one in + exp := + build_full_ilist op3 [ r2' ] dest succ (fst ht2) [] map_consts + else + let n3 = n2pi () in + let n2 = n2pi () in + let n1 = n2pi () in + let r1 = r2pi () in + let r2 = r2pi () in + let r3 = r2pi () in + let op1 = Oshrlimm (Int.repr (Z.of_sint 63)) in + let sv1 = find_or_addnmove op1 [ a1 ] r1 n1 map_consts true in + let ht1 = build_head_tuple [] sv1 in + let r1' = unzip_head_tuple ht1 r1 in + + let op2 = Oshrluimm (Int.sub Int64.iwordsize' n) in + let sv2 = find_or_addnmove op2 [ r1' ] r2 n2 map_consts true in + let ht2 = build_head_tuple (fst ht1) sv2 in + let r2' = unzip_head_tuple ht2 r2 in + + let op3 = Oaddl in + let sv3 = find_or_addnmove op3 [ a1; r2' ] r3 n3 map_consts true in + let ht3 = build_head_tuple (fst ht2) sv3 in + let r3' = unzip_head_tuple ht3 r3 in + + let op4 = Oshrlimm n in + exp := + build_full_ilist op4 [ r3' ] dest succ (fst ht3) [] map_consts + | _ -> ()); + if !was_exp then ( (if !was_branch && List.length !exp > 1 then let lives = PTree.get n !liveins in @@ -637,7 +878,7 @@ let expanse (sb : superblock) code pm = liveins := PTree.remove n !liveins | _ -> ()); write_pathmap sb.instructions.(0) (List.length !exp - 1) pm'; - write_tree !exp n !node code' new_order) + write_tree !exp n !node code' new_order true) else new_order := n :: !new_order) sb.instructions; sb.instructions <- Array.of_list (List.rev !new_order); |