From fd1a0395e540ee9fcd91d8f09161b34a22d9c51e Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 1 Mar 2021 23:16:02 +0100 Subject: Try to save values in virtual registers during expansion --- riscV/ExpansionOracle.ml | 189 +++++++++++++++++++++++++---------------------- 1 file changed, 100 insertions(+), 89 deletions(-) (limited to 'riscV/ExpansionOracle.ml') diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 41a2227b..95a300c5 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -29,6 +29,10 @@ let r2p () = Camlcoq.P.of_int !reg let n2p () = Camlcoq.P.of_int !node +let r2pi () = + reg := !reg + 1; + r2p () + let n2pi () = node := !node + 1; n2p () @@ -36,27 +40,27 @@ let n2pi () = type immt = Xoriw | Xoril | Sltiw | Sltiuw | Sltil | Sltiul let load_hilo32 a1 dest hi lo succ is_long k = - if Int.eq lo Int.zero then Iop (OEluiw (hi, is_long), [a1], dest, succ) :: k + if Int.eq lo Int.zero then Iop (OEluiw (hi, is_long), [ a1 ], dest, succ) :: k else - Iop (OEluiw (hi, is_long), [a1], dest, n2pi ()) - :: Iop (Oaddimm lo, [ dest ], dest, succ) - :: k + let r = r2pi () in + Iop (OEluiw (hi, is_long), [ a1 ], r, n2pi ()) + :: Iop (Oaddimm lo, [ r ], dest, succ) :: k let load_hilo64 a1 dest hi lo succ k = - if Int64.eq lo Int64.zero then Iop (OEluil hi, [a1], dest, succ) :: k + if Int64.eq lo Int64.zero then Iop (OEluil hi, [ a1 ], dest, succ) :: k else - Iop (OEluil hi, [a1], dest, n2pi ()) - :: Iop (Oaddlimm lo, [ dest ], dest, succ) - :: k + let r = r2pi () in + Iop (OEluil hi, [ a1 ], r, n2pi ()) + :: Iop (Oaddlimm lo, [ r ], dest, succ) :: k let loadimm32 a1 dest n succ is_long k = match make_immed32 n with - | Imm32_single imm -> Iop (OEaddiwr0 (imm, is_long), [a1], dest, succ) :: k + | Imm32_single imm -> Iop (OEaddiwr0 (imm, is_long), [ a1 ], dest, succ) :: k | Imm32_pair (hi, lo) -> load_hilo32 a1 dest hi lo succ is_long k let loadimm64 a1 dest n succ k = match make_immed64 n with - | Imm64_single imm -> Iop (OEaddilr0 imm, [a1], dest, succ) :: k + | Imm64_single imm -> Iop (OEaddilr0 imm, [ a1 ], dest, succ) :: k | Imm64_pair (hi, lo) -> load_hilo64 a1 dest hi lo succ k | Imm64_large imm -> Iop (OEloadli imm, [], dest, succ) :: k @@ -72,28 +76,28 @@ let opimm32 a1 dest n succ is_long k op opimm = match make_immed32 n with | Imm32_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k | Imm32_pair (hi, lo) -> - reg := !reg + 1; - load_hilo32 a1 (r2p ()) hi lo (n2pi ()) is_long - (Iop (op, [ a1; r2p () ], dest, succ) :: k) + let r = r2pi () in + load_hilo32 a1 r hi lo (n2pi ()) is_long + (Iop (op, [ a1; r ], dest, succ) :: k) let opimm64 a1 dest n succ k op opimm = match make_immed64 n with | Imm64_single imm -> Iop (get_opimm imm opimm, [ a1 ], dest, succ) :: k | Imm64_pair (hi, lo) -> - reg := !reg + 1; - load_hilo64 a1 (r2p ()) hi lo (n2pi ()) - (Iop (op, [ a1; r2p () ], dest, succ) :: k) + let r = r2pi () in + load_hilo64 a1 r hi lo (n2pi ()) (Iop (op, [ a1; r ], dest, succ) :: k) | Imm64_large imm -> - reg := !reg + 1; - Iop (OEloadli imm, [], r2p (), n2pi ()) - :: Iop (op, [ a1; r2p () ], dest, succ) - :: k + let r = r2pi () in + Iop (OEloadli imm, [], r, n2pi ()) :: Iop (op, [ a1; r ], dest, succ) :: k -let xorimm32 a1 dest n succ is_long k = opimm32 a1 dest n succ is_long k Oxor Xoriw +let xorimm32 a1 dest n succ is_long k = + opimm32 a1 dest n succ is_long k Oxor Xoriw -let sltimm32 a1 dest n succ is_long k = opimm32 a1 dest n succ is_long k (OEsltw None) Sltiw +let sltimm32 a1 dest n succ is_long k = + opimm32 a1 dest n succ is_long k (OEsltw None) Sltiw -let sltuimm32 a1 dest n succ is_long k = opimm32 a1 dest n succ is_long k (OEsltuw None) Sltiuw +let sltuimm32 a1 dest n succ is_long k = + opimm32 a1 dest n succ is_long k (OEsltuw None) Sltiuw let xorimm64 a1 dest n succ k = opimm64 a1 dest n succ k Oxorl Xoril @@ -152,14 +156,14 @@ let cond_int32s is_x0 cmp a1 a2 dest succ k = | Cne -> Iop (OEsnew optR0, [ a1; a2 ], dest, succ) :: k | Clt -> Iop (OEsltw optR0, [ a1; a2 ], dest, succ) :: k | Cle -> - Iop (OEsltw optR0, [ a2; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k + let r = r2pi () in + Iop (OEsltw optR0, [ a2; a1 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k | Cgt -> Iop (OEsltw optR0, [ a2; a1 ], dest, succ) :: k | Cge -> - Iop (OEsltw optR0, [ a1; a2 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k + let r = r2pi () in + Iop (OEsltw optR0, [ a1; a2 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k let cond_int32u is_x0 cmp a1 a2 dest succ k = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in @@ -168,14 +172,14 @@ let cond_int32u is_x0 cmp a1 a2 dest succ k = | Cne -> Iop (OEsneuw optR0, [ a1; a2 ], dest, succ) :: k | Clt -> Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) :: k | Cle -> - Iop (OEsltuw optR0, [ a2; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k + let r = r2pi () in + Iop (OEsltuw optR0, [ a2; a1 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k | Cgt -> Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) :: k | Cge -> - Iop (OEsltuw optR0, [ a1; a2 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k + let r = r2pi () in + Iop (OEsltuw optR0, [ a1; a2 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k let cond_int64s is_x0 cmp a1 a2 dest succ k = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in @@ -184,14 +188,14 @@ let cond_int64s is_x0 cmp a1 a2 dest succ k = | Cne -> Iop (OEsnel optR0, [ a1; a2 ], dest, succ) :: k | Clt -> Iop (OEsltl optR0, [ a1; a2 ], dest, succ) :: k | Cle -> - Iop (OEsltl optR0, [ a2; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k + let r = r2pi () in + Iop (OEsltl optR0, [ a2; a1 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k | Cgt -> Iop (OEsltl optR0, [ a2; a1 ], dest, succ) :: k | Cge -> - Iop (OEsltl optR0, [ a1; a2 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k + let r = r2pi () in + Iop (OEsltl optR0, [ a1; a2 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k let cond_int64u is_x0 cmp a1 a2 dest succ k = let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in @@ -200,14 +204,14 @@ let cond_int64u is_x0 cmp a1 a2 dest succ k = | Cne -> Iop (OEsneul optR0, [ a1; a2 ], dest, succ) :: k | Clt -> Iop (OEsltul optR0, [ a1; a2 ], dest, succ) :: k | Cle -> - Iop (OEsltul optR0, [ a2; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k + let r = r2pi () in + Iop (OEsltul optR0, [ a2; a1 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k | Cgt -> Iop (OEsltul optR0, [ a2; a1 ], dest, succ) :: k | Cge -> - Iop (OEsltul optR0, [ a1; a2 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k + let r = r2pi () in + Iop (OEsltul optR0, [ a1; a2 ], r, n2pi ()) + :: Iop (OExoriw Int.one, [ r ], dest, succ) :: k let is_normal_cmp = function Cne -> false | _ -> true @@ -231,47 +235,48 @@ let cond_single cmp f1 f2 dest succ = let expanse_cbranchimm_int32s cmp a1 n info succ1 succ2 k = if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k - else ( - reg := !reg + 1; - loadimm32 a1 (r2p ()) n (n2pi ()) false - (cbranch_int32s false cmp a1 (r2p ()) info succ1 succ2 k)) + else + let r = r2pi () in + loadimm32 a1 r n (n2pi ()) false + (cbranch_int32s false cmp a1 r info succ1 succ2 k) let expanse_cbranchimm_int32u cmp a1 n info succ1 succ2 k = if Int.eq n Int.zero then cbranch_int32u true cmp a1 a1 info succ1 succ2 k - else ( - reg := !reg + 1; - loadimm32 a1 (r2p ()) n (n2pi ()) false - (cbranch_int32u false cmp a1 (r2p ()) info succ1 succ2 k)) + else + let r = r2pi () in + loadimm32 a1 r n (n2pi ()) false + (cbranch_int32u false cmp a1 r info succ1 succ2 k) let expanse_cbranchimm_int64s cmp a1 n info succ1 succ2 k = if Int64.eq n Int64.zero then cbranch_int64s true cmp a1 a1 info succ1 succ2 k - else ( - reg := !reg + 1; - loadimm64 a1 (r2p ()) n (n2pi ()) - (cbranch_int64s false cmp a1 (r2p ()) info succ1 succ2 k)) + else + let r = r2pi () in + loadimm64 a1 r n (n2pi ()) + (cbranch_int64s false cmp a1 r info succ1 succ2 k) let expanse_cbranchimm_int64u cmp a1 n info succ1 succ2 k = if Int64.eq n Int64.zero then cbranch_int64u true cmp a1 a1 info succ1 succ2 k - else ( - reg := !reg + 1; - loadimm64 a1 (r2p ()) n (n2pi ()) - (cbranch_int64u false cmp a1 (r2p ()) info succ1 succ2 k)) + else + let r = r2pi () in + loadimm64 a1 r n (n2pi ()) + (cbranch_int64u false cmp a1 r info succ1 succ2 k) let expanse_condimm_int32s cmp a1 n dest succ k = if Int.eq n Int.zero then cond_int32s true cmp a1 a1 dest succ k else match cmp with | Ceq | Cne -> - xorimm32 a1 dest n (n2pi ()) false - (cond_int32s true cmp dest dest dest succ k) + let r = r2pi () in + xorimm32 a1 r n (n2pi ()) false (cond_int32s true cmp r r dest succ k) | Clt -> sltimm32 a1 dest n succ false k | Cle -> - if Int.eq n (Int.repr Int.max_signed) then loadimm32 a1 dest Int.one succ false k + if Int.eq n (Int.repr Int.max_signed) then + loadimm32 a1 dest Int.one succ false k else sltimm32 a1 dest (Int.add n Int.one) succ false k | _ -> - reg := !reg + 1; - loadimm32 a1 (r2p ()) n (n2pi ()) false - (cond_int32s false cmp a1 (r2p ()) dest succ k) + let r = r2pi () in + loadimm32 a1 r n (n2pi ()) false + (cond_int32s false cmp a1 r dest succ k) let expanse_condimm_int32u cmp a1 n dest succ k = if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest succ k @@ -279,27 +284,25 @@ let expanse_condimm_int32u cmp a1 n dest succ k = match cmp with | Clt -> sltuimm32 a1 dest n succ false k | _ -> - reg := !reg + 1; - loadimm32 a1 (r2p ()) n (n2pi ()) false - (cond_int32u false cmp a1 (r2p ()) dest succ k) + let r = r2pi () in + loadimm32 a1 r n (n2pi ()) false + (cond_int32u false cmp a1 r dest succ k) let expanse_condimm_int64s cmp a1 n dest succ k = if Int64.eq n Int64.zero then cond_int64s true cmp a1 a1 dest succ k else match cmp with | Ceq | Cne -> - reg := !reg + 1; - xorimm64 a1 (r2p ()) n (n2pi ()) - (cond_int64s true cmp (r2p ()) (r2p ()) dest succ k) + let r = r2pi () in + xorimm64 a1 r n (n2pi ()) (cond_int64s true cmp r r dest succ k) | Clt -> sltimm64 a1 dest n succ k | Cle -> if Int64.eq n (Int64.repr Int64.max_signed) then loadimm32 a1 dest Int.one succ true k else sltimm64 a1 dest (Int64.add n Int64.one) succ k | _ -> - reg := !reg + 1; - loadimm64 a1 (r2p ()) n (n2pi ()) - (cond_int64s false cmp a1 (r2p ()) dest succ k) + let r = r2pi () in + loadimm64 a1 r n (n2pi ()) (cond_int64s false cmp a1 r dest succ k) let expanse_condimm_int64u cmp a1 n dest succ k = if Int64.eq n Int64.zero then cond_int64u true cmp a1 a1 dest succ k @@ -307,9 +310,8 @@ let expanse_condimm_int64u cmp a1 n dest succ k = match cmp with | Clt -> sltuimm64 a1 dest n succ k | _ -> - reg := !reg + 1; - loadimm64 a1 (r2p ()) n (n2pi ()) - (cond_int64u false cmp a1 (r2p ()) dest succ k) + let r = r2pi () in + loadimm64 a1 r n (n2pi ()) (cond_int64u false cmp a1 r dest succ k) let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k = let normal = is_normal_cmp cmp in @@ -320,14 +322,14 @@ let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k = :: (if normal' then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k) let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k = - reg := !reg + 1; + 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 (r2p ()) (n2pi ()) in + let insn = fn_cond cmp f1 f2 r (n2pi ()) in insn - :: (if normal' then - Icond (CEbnew (Some false), [ r2p (); r2p () ], succ1, succ2, info) - else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) + :: + (if normal' then Icond (CEbnew (Some false), [ r; r ], succ1, succ2, info) + else Icond (CEbeqw (Some false), [ r; r ], succ1, succ2, info)) :: k let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] @@ -352,8 +354,15 @@ let write_initial_node initial code' new_order = let write_pathmap initial esize pm' = 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 + 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' let rec write_tree exp current code' new_order = @@ -500,7 +509,9 @@ let expanse (sb : superblock) code pm = let lives = PTree.get n !liveins in match lives with | Some lives -> - let new_branch_pc = Camlcoq.P.of_int (!node - ((List.length !exp) - 1)) in + let new_branch_pc = + Camlcoq.P.of_int (!node - (List.length !exp - 1)) + in liveins := PTree.set new_branch_pc lives !liveins; liveins := PTree.remove n !liveins | _ -> ()); -- cgit