From acb41b1af6e5e4c933e3be1b17f6e5012eca794d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sat, 6 Feb 2021 16:53:46 +0100 Subject: cond and branches expanded --- riscV/ExpansionOracle.ml | 432 +++++++++++++++++++++++++++-------------------- 1 file changed, 251 insertions(+), 181 deletions(-) (limited to 'riscV/ExpansionOracle.ml') diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index 9e494d0a..af14811d 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -18,8 +18,6 @@ open RTL open Op open Asmgen open DebugPrint - -(*open PrintRTL*) open! Integers let reg = ref 1 @@ -102,150 +100,169 @@ let sltimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltl None) Sltil let sltuimm64 a1 dest n succ k = opimm64 a1 dest n succ k (OEsltul None) Sltiul -let cond_int32s_x0 cmp a1 dest succ k = - match cmp with - | Ceq -> Iop (OEseqw (Some false), [ a1; a1 ], dest, succ) :: k - | Cne -> Iop (OEsnew (Some false), [ a1; a1 ], dest, succ) :: k - | Clt -> Iop (OEsltw (Some false), [ a1; a1 ], dest, succ) :: k - | Cle -> - Iop (OEsltw (Some true), [ a1; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k - | Cgt -> Iop (OEsltw (Some true), [ a1; a1 ], dest, succ) :: k - | Cge -> - Iop (OEsltw (Some false), [ a1; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k +let is_inv_cmp = function Cle | Cgt -> true | _ -> false -let cond_int32s_reg cmp a1 a2 dest succ k = - match cmp with - | Ceq -> Iop (OEseqw None, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsnew None, [ a1; a2 ], dest, succ) :: k - | Clt -> Iop (OEsltw None, [ a1; a2 ], dest, succ) :: k - | Cle -> - Iop (OEsltw None, [ a2; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k - | Cgt -> Iop (OEsltw None, [ a2; a1 ], dest, succ) :: k - | Cge -> - Iop (OEsltw None, [ a1; a2 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k +let make_optR0 is_x0 is_inv = if is_x0 then Some is_inv else None -let cond_int32u_x0 cmp a1 dest succ k = +let cbranch_int32s is_x0 cmp a1 a2 info succ1 succ2 k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEseqw (Some false), [ a1; a1 ], dest, succ) :: k - | Cne -> Iop (OEsnew (Some false), [ a1; a1 ], dest, succ) :: k - | Clt -> Iop (OEsltuw (Some false), [ a1; a1 ], dest, succ) :: k - | Cle -> - Iop (OEsltuw (Some true), [ a1; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k - | Cgt -> Iop (OEsltuw (Some true), [ a1; a1 ], dest, succ) :: k - | Cge -> - Iop (OEsltuw (Some false), [ a1; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k - -let cond_int32u_reg cmp a1 a2 dest succ k = + | Ceq -> Icond (CEbeqw optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbnew optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Clt -> Icond (CEbltw optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cle -> Icond (CEbgew optR0, [ a2; a1 ], succ1, succ2, info) :: k + | Cgt -> Icond (CEbltw optR0, [ a2; a1 ], succ1, succ2, info) :: k + | Cge -> Icond (CEbgew optR0, [ a1; a2 ], succ1, succ2, info) :: k + +let cbranch_int32u is_x0 cmp a1 a2 info succ1 succ2 k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEseqw None, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsnew None, [ a1; a2 ], dest, succ) :: k - | Clt -> Iop (OEsltuw None, [ a1; a2 ], dest, succ) :: k - | Cle -> - Iop (OEsltuw None, [ a2; a1 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k - | Cgt -> Iop (OEsltuw None, [ a2; a1 ], dest, succ) :: k - | Cge -> - Iop (OEsltuw None, [ a1; a2 ], dest, n2pi ()) - :: Iop (OExoriw Int.one, [ dest ], dest, succ) - :: k - -let cond_int64s_x0 cmp a1 dest succ k = + | Ceq -> Icond (CEbeqw optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbnew optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Clt -> Icond (CEbltuw optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cle -> Icond (CEbgeuw optR0, [ a2; a1 ], succ1, succ2, info) :: k + | Cgt -> Icond (CEbltuw optR0, [ a2; a1 ], succ1, succ2, info) :: k + | Cge -> Icond (CEbgeuw optR0, [ a1; a2 ], succ1, succ2, info) :: k + +let cbranch_int64s is_x0 cmp a1 a2 info succ1 succ2 k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Icond (CEbeql optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbnel optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Clt -> Icond (CEbltl optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cle -> Icond (CEbgel optR0, [ a2; a1 ], succ1, succ2, info) :: k + | Cgt -> Icond (CEbltl optR0, [ a2; a1 ], succ1, succ2, info) :: k + | Cge -> Icond (CEbgel optR0, [ a1; a2 ], succ1, succ2, info) :: k + +let cbranch_int64u is_x0 cmp a1 a2 info succ1 succ2 k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in + match cmp with + | Ceq -> Icond (CEbeql optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cne -> Icond (CEbnel optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Clt -> Icond (CEbltul optR0, [ a1; a2 ], succ1, succ2, info) :: k + | Cle -> Icond (CEbgeul optR0, [ a2; a1 ], succ1, succ2, info) :: 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 succ k = + let optR0 = make_optR0 is_x0 (is_inv_cmp cmp) in match cmp with - | Ceq -> Iop (OEseql (Some false), [ a1; a1 ], dest, succ) :: k - | Cne -> Iop (OEsnel (Some false), [ a1; a1 ], dest, succ) :: k - | Clt -> Iop (OEsltl (Some false), [ a1; a1 ], dest, succ) :: k + | 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 | Cle -> - Iop (OEsltl (Some true), [ a1; a1 ], dest, n2pi ()) + Iop (OEsltw optR0, [ a2; a1 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k - | Cgt -> Iop (OEsltl (Some true), [ a1; a1 ], dest, succ) :: k + | Cgt -> Iop (OEsltw optR0, [ a2; a1 ], dest, succ) :: k | Cge -> - Iop (OEsltl (Some false), [ a1; a1 ], dest, n2pi ()) + Iop (OEsltw optR0, [ a1; a2 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k -let cond_int64s_reg cmp a1 a2 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 match cmp with - | Ceq -> Iop (OEseql None, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsnel None, [ a1; a2 ], dest, succ) :: k - | Clt -> Iop (OEsltl None, [ a1; a2 ], dest, succ) :: k + | Ceq -> Iop (OEseqw optR0, [ a1; a2 ], dest, succ) :: k + | Cne -> Iop (OEsnew optR0, [ a1; a2 ], dest, succ) :: k + | Clt -> Iop (OEsltuw optR0, [ a1; a2 ], dest, succ) :: k | Cle -> - Iop (OEsltl None, [ a2; a1 ], dest, n2pi ()) + Iop (OEsltuw optR0, [ a2; a1 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k - | Cgt -> Iop (OEsltl None, [ a2; a1 ], dest, succ) :: k + | Cgt -> Iop (OEsltuw optR0, [ a2; a1 ], dest, succ) :: k | Cge -> - Iop (OEsltl None, [ a1; a2 ], dest, n2pi ()) + Iop (OEsltuw optR0, [ a1; a2 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k -let cond_int64u_x0 cmp a1 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 match cmp with - | Ceq -> Iop (OEseql (Some false), [ a1; a1 ], dest, succ) :: k - | Cne -> Iop (OEsnel (Some false), [ a1; a1 ], dest, succ) :: k - | Clt -> Iop (OEsltul (Some false), [ a1; a1 ], dest, succ) :: k + | 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 | Cle -> - Iop (OEsltul (Some true), [ a1; a1 ], dest, n2pi ()) + Iop (OEsltl optR0, [ a2; a1 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k - | Cgt -> Iop (OEsltul (Some true), [ a1; a1 ], dest, succ) :: k + | Cgt -> Iop (OEsltl optR0, [ a2; a1 ], dest, succ) :: k | Cge -> - Iop (OEsltul (Some false), [ a1; a1 ], dest, n2pi ()) + Iop (OEsltl optR0, [ a1; a2 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k -let cond_int64u_reg cmp a1 a2 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 match cmp with - | Ceq -> Iop (OEseql None, [ a1; a2 ], dest, succ) :: k - | Cne -> Iop (OEsnel None, [ a1; a2 ], dest, succ) :: k - | Clt -> Iop (OEsltul None, [ a1; a2 ], dest, succ) :: k + | Ceq -> Iop (OEseql optR0, [ a1; a2 ], dest, succ) :: k + | Cne -> Iop (OEsnel optR0, [ a1; a2 ], dest, succ) :: k + | Clt -> Iop (OEsltul optR0, [ a1; a2 ], dest, succ) :: k | Cle -> - Iop (OEsltul None, [ a2; a1 ], dest, n2pi ()) + Iop (OEsltul optR0, [ a2; a1 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k - | Cgt -> Iop (OEsltul None, [ a2; a1 ], dest, succ) :: k + | Cgt -> Iop (OEsltul optR0, [ a2; a1 ], dest, succ) :: k | Cge -> - Iop (OEsltul None, [ a1; a2 ], dest, n2pi ()) + Iop (OEsltul optR0, [ a1; a2 ], dest, n2pi ()) :: Iop (OExoriw Int.one, [ dest ], dest, succ) :: k +let is_normal_cmp = function Cne -> false | _ -> true + let cond_float cmp f1 f2 dest succ = match cmp with - | Ceq -> (Iop (OEfeqd, [ f1; f2 ], dest, succ), true) - | Cne -> (Iop (OEfeqd, [ f1; f2 ], dest, succ), false) - | Clt -> (Iop (OEfltd, [ f1; f2 ], dest, succ), true) - | Cle -> (Iop (OEfled, [ f1; f2 ], dest, succ), true) - | Cgt -> (Iop (OEfltd, [ f2; f1 ], dest, succ), true) - | Cge -> (Iop (OEfled, [ f2; f1 ], dest, succ), true) + | 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 = match cmp with - | Ceq -> (Iop (OEfeqs, [ f1; f2 ], dest, succ), true) - | Cne -> (Iop (OEfeqs, [ f1; f2 ], dest, succ), false) - | Clt -> (Iop (OEflts, [ f1; f2 ], dest, succ), true) - | Cle -> (Iop (OEfles, [ f1; f2 ], dest, succ), true) - | Cgt -> (Iop (OEflts, [ f2; f1 ], dest, succ), true) - | Cge -> (Iop (OEfles, [ f2; f1 ], dest, succ), true) + | 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 = + if Int.eq n Int.zero then cbranch_int32s true cmp a1 a1 info succ1 succ2 k + else ( + reg := !reg + 1; + loadimm32 (r2p ()) n (n2pi ()) + (cbranch_int32s false cmp a1 (r2p ()) 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 (r2p ()) n (n2pi ()) + (cbranch_int32u false cmp a1 (r2p ()) 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 (r2p ()) n (n2pi ()) + (cbranch_int64s false cmp a1 (r2p ()) 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 (r2p ()) n (n2pi ()) + (cbranch_int64u false cmp a1 (r2p ()) info succ1 succ2 k)) let expanse_condimm_int32s cmp a1 n dest succ k = - if Int.eq n Int.zero then cond_int32s_x0 cmp a1 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 ()) (cond_int32s_x0 cmp dest dest succ k) + xorimm32 a1 dest n (n2pi ()) + (cond_int32s true cmp dest dest dest succ k) | Clt -> sltimm32 a1 dest n succ k | Cle -> if Int.eq n (Int.repr Int.max_signed) then loadimm32 dest Int.one succ k @@ -253,26 +270,26 @@ let expanse_condimm_int32s cmp a1 n dest succ k = | _ -> reg := !reg + 1; loadimm32 (r2p ()) n (n2pi ()) - (cond_int32s_reg cmp a1 (r2p ()) dest succ k) + (cond_int32s false cmp a1 (r2p ()) dest succ k) let expanse_condimm_int32u cmp a1 n dest succ k = - if Int.eq n Int.zero then cond_int32u_x0 cmp a1 dest succ k + if Int.eq n Int.zero then cond_int32u true cmp a1 a1 dest succ k else match cmp with | Clt -> sltuimm32 a1 dest n succ k | _ -> reg := !reg + 1; loadimm32 (r2p ()) n (n2pi ()) - (cond_int32u_reg cmp a1 (r2p ()) dest succ k) + (cond_int32u false cmp a1 (r2p ()) dest succ k) let expanse_condimm_int64s cmp a1 n dest succ k = - if Int.eq n Int.zero then cond_int64s_x0 cmp a1 dest succ k + if Int.eq n Int.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_x0 cmp (r2p ()) dest succ k) + (cond_int64s true cmp (r2p ()) (r2p ()) dest succ k) | Clt -> sltimm64 a1 dest n succ k | Cle -> if Int64.eq n (Int64.repr Int64.max_signed) then @@ -281,47 +298,36 @@ let expanse_condimm_int64s cmp a1 n dest succ k = | _ -> reg := !reg + 1; loadimm64 (r2p ()) n (n2pi ()) - (cond_int64s_reg cmp a1 (r2p ()) dest succ k) + (cond_int64s false cmp a1 (r2p ()) dest succ k) let expanse_condimm_int64u cmp a1 n dest succ k = - if Int64.eq n Int64.zero then cond_int64u_x0 cmp a1 dest succ k + if Int64.eq n Int64.zero then cond_int64u true cmp a1 a1 dest succ k else match cmp with | Clt -> sltuimm64 a1 dest n succ k | _ -> reg := !reg + 1; loadimm64 (r2p ()) n (n2pi ()) - (cond_int64u_reg cmp a1 (r2p ()) dest succ k) - -let expanse_cond_float cmp f1 f2 dest succ k = - let insn, normal = cond_float cmp f1 f2 dest succ in - insn - :: (if normal then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k) + (cond_int64u false cmp a1 (r2p ()) dest succ k) -let expanse_cond_not_float cmp f1 f2 dest succ k = - let insn, normal = cond_float cmp f1 f2 dest succ in +let expanse_cond_fp cnot fn_cond cmp f1 f2 dest succ k = + 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 Iop (OExoriw Int.one, [ dest ], dest, succ) :: k else k) + :: (if normal' then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k) -let expanse_cond_single cmp f1 f2 dest succ k = - let insn, normal = cond_single cmp f1 f2 dest succ in +let expanse_cbranch_fp cnot fn_cond cmp f1 f2 info succ1 succ2 k = + reg := !reg + 1; + 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 insn - :: (if normal then k else Iop (OExoriw Int.one, [ dest ], dest, succ) :: k) - -let expanse_cond_not_single cmp f1 f2 dest succ k = - let insn, normal = cond_single cmp f1 f2 dest succ in - insn - :: (if normal then Iop (OExoriw Int.one, [ dest ], dest, succ) :: k else k) - -let rec write_tree exp n code' = - match exp with - | (Iop (_, _, _, succ) as inst) :: k -> - (*print_instruction stderr (0,inst);*) - (*Printf.eprintf "PLACING NODE %d\n" (Camlcoq.P.to_int n);*) - code' := PTree.set n inst !code'; - (*Printf.eprintf "WITH SUCC %d\n" (Camlcoq.P.to_int succ);*) - write_tree k (Camlcoq.P.of_int (Camlcoq.P.to_int n + 1)) code' - | _ -> !code' + :: (if normal' then + Icond (CEbnew (Some false), [ r2p (); r2p () ], succ1, succ2, info) + else Icond (CEbeqw (Some false), [ r2p (); r2p () ], succ1, succ2, info)) + :: k let get_regindent = function Coq_inr _ -> [] | Coq_inl r -> [ r ] @@ -339,94 +345,158 @@ let get_regs_inst = function | Ireturn (Some r) -> [ r ] | _ -> [] -let generate_head_order n start_node new_order = - Printf.eprintf "GEN n %d start %d node %d\n" (Camlcoq.P.to_int n) - (Camlcoq.P.to_int start_node) - !node; - for i = !node downto Camlcoq.P.to_int start_node do - new_order := !new_order @ [ Camlcoq.P.of_int i ] - done; - new_order := n :: !new_order +let rec write_tree' exp current initial code' new_order = + if current = !node then ( + code' := PTree.set initial (Inop (n2p ())) !code'; + new_order := initial :: !new_order); + match exp with + | (Iop (_, _, _, succ) as inst) :: k -> + code' := PTree.set (Camlcoq.P.of_int current) inst !code'; + new_order := Camlcoq.P.of_int current :: !new_order; + write_tree' k (current - 1) initial code' new_order + | (Icond (_, _, succ1, succ2, _) as inst) :: k -> + code' := PTree.set (Camlcoq.P.of_int current) inst !code'; + new_order := Camlcoq.P.of_int current :: !new_order; + write_tree' k (current - 1) initial code' new_order + | [] -> () + | _ -> failwith "ExpansionOracle.write_tree: inconsistent instruction." let expanse (sb : superblock) code = - debug_flag := true; 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 Array.iter (fun n -> + was_branch := false; was_exp := false; let inst = get_some @@ PTree.get n code in - let start_node = Camlcoq.P.of_int (!node + 1) in (match inst with | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> - Printf.eprintf "Ccomp\n"; - exp := cond_int32s_reg c a1 a2 dest succ []; + debug "Iop/Ccomp\n"; + exp := cond_int32s false c a1 a2 dest succ []; was_exp := true | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, dest, succ) -> - Printf.eprintf "Ccompu\n"; - exp := cond_int32u_reg c a1 a2 dest succ []; + debug "Iop/Ccompu\n"; + exp := cond_int32u false c a1 a2 dest succ []; was_exp := true | Iop (Ocmp (Ccompimm (c, imm)), a1 :: nil, dest, succ) -> - Printf.eprintf "Ccompimm\n"; + debug "Iop/Ccompimm\n"; exp := expanse_condimm_int32s c a1 imm dest succ []; was_exp := true | Iop (Ocmp (Ccompuimm (c, imm)), a1 :: nil, dest, succ) -> - Printf.eprintf "Ccompuimm\n"; + debug "Iop/Ccompuimm\n"; exp := expanse_condimm_int32u c a1 imm dest succ []; was_exp := true | Iop (Ocmp (Ccompl c), a1 :: a2 :: nil, dest, succ) -> - Printf.eprintf "Ccompl\n"; - exp := cond_int64s_reg c a1 a2 dest succ []; + debug "Iop/Ccompl\n"; + exp := cond_int64s false c a1 a2 dest succ []; was_exp := true | Iop (Ocmp (Ccomplu c), a1 :: a2 :: nil, dest, succ) -> - Printf.eprintf "Ccomplu\n"; - exp := cond_int64u_reg c a1 a2 dest succ []; + debug "Iop/Ccomplu\n"; + exp := cond_int64u false c a1 a2 dest succ []; was_exp := true | Iop (Ocmp (Ccomplimm (c, imm)), a1 :: nil, dest, succ) -> - (*Printf.eprintf "Ccomplimm\n";*) - (*Printf.eprintf "[EXPANSION] Last node is: %d\n" !node;*) - (*Printf.eprintf "[EXPANSION] Last reg is: %d\n" !reg;*) - (*Printf.eprintf "CUR IS %d\n" (Camlcoq.P.to_int n);*) - (*Printf.eprintf "SUCC IS %d\n" (Camlcoq.P.to_int succ);*) - (*debug "[EXPANSION] Replace this:\n";*) - (*print_instruction stderr (0,inst);*) - (*debug "[EXPANSION] With:\n";*) - (*Printf.eprintf "entry is %d\n" (Camlcoq.P.to_int !entry);*) - (*entry := n2p()*) + debug "Iop/Ccomplimm\n"; exp := expanse_condimm_int64s c a1 imm dest succ []; was_exp := true | Iop (Ocmp (Ccompluimm (c, imm)), a1 :: nil, dest, succ) -> - Printf.eprintf "Ccompluimm\n"; + debug "Iop/Ccompluimm\n"; exp := expanse_condimm_int64u c a1 imm dest succ []; was_exp := true | Iop (Ocmp (Ccompf c), f1 :: f2 :: nil, dest, succ) -> - Printf.eprintf "Ccompf\n"; - exp := expanse_cond_float c f1 f2 dest succ []; + debug "Iop/Ccompf\n"; + exp := expanse_cond_fp false cond_float c f1 f2 dest succ []; was_exp := true | Iop (Ocmp (Cnotcompf c), f1 :: f2 :: nil, dest, succ) -> - Printf.eprintf "Cnotcompf\n"; - exp := expanse_cond_not_float c f1 f2 dest succ []; + debug "Iop/Cnotcompf\n"; + exp := expanse_cond_fp true cond_float c f1 f2 dest succ []; was_exp := true | Iop (Ocmp (Ccompfs c), f1 :: f2 :: nil, dest, succ) -> - Printf.eprintf "Ccompfs\n"; - exp := expanse_cond_single c f1 f2 dest succ []; + debug "Iop/Ccompfs\n"; + exp := expanse_cond_fp false cond_single c f1 f2 dest succ []; was_exp := true | Iop (Ocmp (Cnotcompfs c), f1 :: f2 :: nil, dest, succ) -> - Printf.eprintf "Cnotcompfs\n"; - exp := expanse_cond_not_single c f1 f2 dest succ []; + debug "Iop/Cnotcompfs\n"; + exp := expanse_cond_fp true cond_single c f1 f2 dest succ []; + was_exp := true + | 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 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 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 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 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 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 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 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 true cond_single c f1 f2 info succ1 succ2 []; + was_branch := true; was_exp := true - | _ -> new_order := !new_order @ [ n ]); + | _ -> new_order := n :: !new_order); if !was_exp then ( - code' := write_tree (List.rev !exp) start_node code'; - let first = Inop (n2pi ()) in - code' := PTree.set n first !code'; - generate_head_order n start_node new_order)) + node := !node + 1; + (if !was_branch then + let lives = PTree.get n !liveins in + match lives with + | Some lives -> + liveins := PTree.set (n2p ()) lives !liveins; + liveins := PTree.remove n !liveins + | _ -> ()); + write_tree' !exp !node n code' new_order)) sb.instructions; - sb.instructions <- Array.of_list !new_order; - (*print_arrayp sb.instructions;*) - debug_flag := false; + sb.instructions <- Array.of_list (List.rev !new_order); + sb.liveins <- !liveins; !code' let rec find_last_node_reg = function -- cgit