From eb35c3000530e379dcd79e82f001a400be8b28e9 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Mar 2021 20:27:34 +0100 Subject: Adding a flag to test fp_init_exp --- driver/Clflags.ml | 1 + driver/Driver.ml | 1 + riscV/ExpansionOracle.ml | 307 ++++++++++++++++++++++++----------------------- 3 files changed, 159 insertions(+), 150 deletions(-) diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 4cff3f28..8d85e93a 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -106,6 +106,7 @@ let option_div_i32 = ref "stsud" let option_div_i64 = ref "stsud" let option_fcoalesce_mem = ref true let option_fexpanse_rtlcond = ref true +let option_fexpanse_fpconst = ref true let option_fforward_moves = ref false let option_fmove_loop_invariants = ref false let option_fnontrap_loads = ref true diff --git a/driver/Driver.ml b/driver/Driver.ml index 0c5d9cb4..9750981e 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -445,6 +445,7 @@ let cmdline_actions = @ f_opt "nontrap-loads" option_fnontrap_loads @ f_opt "coalesce-mem" option_fcoalesce_mem @ f_opt "expanse-rtlcond" option_fexpanse_rtlcond + @ f_opt "expanse-fpconst" option_fexpanse_fpconst @ f_opt "all-loads-nontrap" option_all_loads_nontrap @ f_opt "forward-moves" option_fforward_moves (* Code generation options *) diff --git a/riscV/ExpansionOracle.ml b/riscV/ExpansionOracle.ml index c6710a95..23e3c38e 100644 --- a/riscV/ExpansionOracle.ml +++ b/riscV/ExpansionOracle.ml @@ -389,156 +389,163 @@ let expanse (sb : superblock) code pm = let pm' = ref pm in Array.iter (fun n -> - was_branch := false; - was_exp := false; - let inst = get_some @@ PTree.get n code in - (match inst with - (* Expansion of conditions - Ocmp *) - | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, 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) -> - 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) -> - 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) -> - 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) -> - 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) -> - 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) -> - 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) -> - 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) -> - 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) -> - 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) -> - 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) -> - debug "Iop/Cnotcompfs\n"; - exp := expanse_cond_fp true cond_single c f1 f2 dest succ []; - was_exp := true - (* Expansion of branches - Ccomp *) - | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccomp\n"; - exp := cbranch_int32s false c a1 a2 info succ1 succ2 []; - was_branch := true; - was_exp := true - | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompu\n"; - exp := cbranch_int32u false c a1 a2 info succ1 succ2 []; - was_branch := true; - was_exp := true - | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> - debug "Icond/Ccompimm\n"; - exp := expanse_cbranchimm_int32s 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 - (* Expansion of fp constants *) - | Iop (Ofloatconst f, nil, dest, succ) -> - debug "Iop/Ofloatconst\n"; - let r = r2pi () in - exp := - [ - Iop (Olongconst (Floats.Float.to_bits f), [], r, n2pi ()); - Iop (Ofloat_of_bits, [ r ], dest, succ); - ]; - was_exp := true - | Iop (Osingleconst f, nil, dest, succ) -> - debug "Iop/Osingleconst\n"; - let r = r2pi () in - exp := - [ - Iop (Ointconst (Floats.Float32.to_bits f), [], r, n2pi ()); - Iop (Osingle_of_bits, [ r ], dest, succ); - ]; - was_exp := true - | _ -> new_order := n :: !new_order); - if !was_exp then ( - node := !node + 1; - (if !was_branch then - 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 - liveins := PTree.set new_branch_pc lives !liveins; - liveins := PTree.remove n !liveins - | _ -> ()); - write_pathmap sb.instructions.(0) (List.length !exp) pm'; - write_initial_node n code' new_order; - write_tree !exp !node code' new_order)) + begin ( + was_branch := false; + was_exp := false; + let inst = get_some @@ PTree.get n code in + if !Clflags.option_fexpanse_rtlcond then ( + match inst with + (* Expansion of conditions - Ocmp *) + | Iop (Ocmp (Ccomp c), a1 :: a2 :: nil, dest, succ) -> + debug "Iop/Ccomp\n"; + exp := cond_int32s false c a1 a2 dest succ []; + was_exp := true + | Iop (Ocmp (Ccompu c), a1 :: a2 :: nil, 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) -> + 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) -> + 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) -> + 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) -> + 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) -> + 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) -> + 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) -> + 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) -> + 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) -> + 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) -> + debug "Iop/Cnotcompfs\n"; + exp := expanse_cond_fp true cond_single c f1 f2 dest succ []; + was_exp := true + (* Expansion of branches - Ccomp *) + | Icond (Ccomp c, a1 :: a2 :: nil, succ1, succ2, info) -> + debug "Icond/Ccomp\n"; + exp := cbranch_int32s false c a1 a2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompu c, a1 :: a2 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompu\n"; + exp := cbranch_int32u false c a1 a2 info succ1 succ2 []; + was_branch := true; + was_exp := true + | Icond (Ccompimm (c, imm), a1 :: nil, succ1, succ2, info) -> + debug "Icond/Ccompimm\n"; + exp := expanse_cbranchimm_int32s 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 + | _ -> ()); + if (!Clflags.option_fexpanse_fpconst && not !was_exp) then ( + match inst with + (* Expansion of fp constants *) + | Iop (Ofloatconst f, nil, dest, succ) -> + debug "Iop/Ofloatconst\n"; + let r = r2pi () in + exp := + [ + Iop (Olongconst (Floats.Float.to_bits f), [], r, n2pi ()); + Iop (Ofloat_of_bits, [ r ], dest, succ); + ]; + was_exp := true + | Iop (Osingleconst f, nil, dest, succ) -> + debug "Iop/Osingleconst\n"; + let r = r2pi () in + exp := + [ + Iop (Ointconst (Floats.Float32.to_bits f), [], r, n2pi ()); + Iop (Osingle_of_bits, [ r ], dest, succ); + ]; + was_exp := true + | _ -> ()); + if !was_exp then ( + node := !node + 1; + (if !was_branch then + 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 + liveins := PTree.set new_branch_pc lives !liveins; + liveins := PTree.remove n !liveins + | _ -> ()); + write_pathmap sb.instructions.(0) (List.length !exp) pm'; + write_initial_node n code' new_order; + write_tree !exp !node code' new_order) + else new_order := n :: !new_order) + end) sb.instructions; sb.instructions <- Array.of_list (List.rev !new_order); sb.liveins <- !liveins; -- cgit