From 5673d04d22334c2493efe5a2ff8108768e089be2 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 30 Sep 2021 15:35:21 +0200 Subject: fix issue #247 by using a BTL's ghostfield --- scheduling/BTLScheduleraux.ml | 15 +++++++++++---- scheduling/BTLcommonaux.ml | 4 ++-- scheduling/BTLtoRTLaux.ml | 2 +- scheduling/BTLtypes.ml | 20 ++++++++++++++++++-- scheduling/PrintBTL.ml | 2 +- scheduling/RTLtoBTLaux.ml | 4 ++-- 6 files changed, 35 insertions(+), 12 deletions(-) (limited to 'scheduling') diff --git a/scheduling/BTLScheduleraux.ml b/scheduling/BTLScheduleraux.ml index 0e682c4c..38bc685c 100644 --- a/scheduling/BTLScheduleraux.ml +++ b/scheduling/BTLScheduleraux.ml @@ -19,7 +19,7 @@ let flatten_blk_basics ibf = last := Some ib; [] | Bseq ((Bcond (_, _, _, _, iinfo) as ib1), ib2) -> ( - match iinfo.pcond with + match iinfo.opt_info with | Some _ -> [ ib1 ] @ traverse_blk ib2 | None -> last := Some ib; @@ -78,7 +78,8 @@ let apply_schedule bseq olast positions = let set_old = Hashtbl.find cbs_above_old n' in let set_new = Hashtbl.find cbs_above_new n' in if SI.subset set_old set_new then - bseq_new.(n') <- Bload (AST.TRAP, a, b, c, d, e) + if get_some @@ e.opt_info then + bseq_new.(n') <- Bload (AST.TRAP, a, b, c, d, e) else assert !config.has_non_trapping_loads | _ -> ()) bseq); @@ -277,7 +278,13 @@ let turn_all_loads_nontrap n ibf btl = let rec traverse_rec ib = match ib with | Bseq (ib1, ib2) -> Bseq (traverse_rec ib1, traverse_rec ib2) - | Bload (t, a, b, c, d, e) -> Bload (AST.NOTRAP, a, b, c, d, e) + | Bload (t, a, b, c, d, e) -> + let _opt_info = + match t with + | AST.TRAP -> Some true + | AST.NOTRAP -> Some false in + e.opt_info <- _opt_info; + Bload (AST.NOTRAP, a, b, c, d, e) | _ -> ib in let ib' = traverse_rec ibf.entry in @@ -304,7 +311,7 @@ let compute_liveins n ibf btl = iinfo.liveins <- Regset.union iinfo.liveins lives) tbl | Bcond (_, _, BF (Bgoto succ, _), Bnop None, iinfo) -> ( - match iinfo.pcond with + match iinfo.opt_info with | Some predb -> assert (predb = false); let lives = (get_some @@ PTree.get succ btl).input_regs in diff --git a/scheduling/BTLcommonaux.ml b/scheduling/BTLcommonaux.ml index 577e4828..11a7ee7f 100644 --- a/scheduling/BTLcommonaux.ml +++ b/scheduling/BTLcommonaux.ml @@ -6,9 +6,9 @@ open RTLcommonaux let undef_node = -1 -let mk_iinfo _inumb _pcond = { inumb = _inumb; pcond = _pcond; visited = false; liveins = Regset.empty } +let mk_iinfo _inumb _opt_info = { inumb = _inumb; opt_info = _opt_info; visited = false; liveins = Regset.empty } -let def_iinfo () = { inumb = undef_node; pcond = None; visited = false; liveins = Regset.empty } +let def_iinfo () = { inumb = undef_node; opt_info = None; visited = false; liveins = Regset.empty } let mk_binfo _bnumb _s_output_regs _typing = { diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml index ddec991d..47262b3e 100644 --- a/scheduling/BTLtoRTLaux.ml +++ b/scheduling/BTLtoRTLaux.ml @@ -22,7 +22,7 @@ let translate_function btl entry = match ib with | Bcond (cond, lr, BF (Bgoto s1, _), Bnop None, iinfo) -> Some - ( Icond (cond, lr, s1, get_ib_num (get_some k), iinfo.pcond), + ( Icond (cond, lr, s1, get_ib_num (get_some k), iinfo.opt_info), get_inumb iinfo ) | Bcond (_, _, _, _, _) -> failwith "translate_function: unsupported Bcond" diff --git a/scheduling/BTLtypes.ml b/scheduling/BTLtypes.ml index 12ca30e8..64001adf 100644 --- a/scheduling/BTLtypes.ml +++ b/scheduling/BTLtypes.ml @@ -2,10 +2,19 @@ open Registers type inst_info = { mutable inumb : int; - mutable pcond : bool option; + mutable opt_info : bool option; mutable visited : bool; - mutable liveins: Regset.t; + mutable liveins : Regset.t; } +(** This struct is a ghost field attached to each BTL instruction + * inumb: int field used for remembering the original numbering of CFG + * opt_info: option bool used for various tests: + * - On Bcond, stores the prediction information + * - On Bload, stores the trapping information (if Some false, the load was + * initially non-trapping, and the opposite if some true) + * visited: boolean used to mark nodes + * liveins: set of lives registers + *) type block_info = { mutable bnumb : int; @@ -13,3 +22,10 @@ type block_info = { s_output_regs : Regset.t; typing : RTLtyping.regenv; } +(** Struct attached to each BTL iblock_info type + * bnumb: int representing the block id in the BTL CFG + * visited: boolean used to mark blocks + * s_output_regs: set of output registers + * typing: field transferring RTL typing information in BTL (used in regpres + * scheduling) + *) diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml index 89254301..64e83651 100644 --- a/scheduling/PrintBTL.ml +++ b/scheduling/PrintBTL.ml @@ -66,7 +66,7 @@ let rec print_iblock pp is_rec pref ib = fprintf pp "%d: Bcond: (%a) (prediction: %s)\n" iinfo.inumb (PrintOp.print_condition reg) (cond, args) - (match iinfo.pcond with + (match iinfo.opt_info with | None -> "none" | Some true -> "branch" | Some false -> "fallthrough"); diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml index 3c06f4cb..0ed6ec61 100644 --- a/scheduling/RTLtoBTLaux.ml +++ b/scheduling/RTLtoBTLaux.ml @@ -33,7 +33,7 @@ let translate_inst (iinfo : BTL.inst_info) inst is_final = | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s), iinfo) | Icond (cond, lr, ifso, ifnot, info) -> osucc := Some ifnot; - iinfo.pcond <- info; + iinfo.opt_info <- info; Bcond ( cond, lr, @@ -70,7 +70,7 @@ let translate_function code entry join_points liveness (typing : RTLtyping.regen | Icond (cond, lr, ifso, ifnot, info) -> assert (s = ifnot); next_nodes := !next_nodes @ non_predicted_successors inst psucc; - iinfo.pcond <- info; + iinfo.opt_info <- info; Bseq ( Bcond (cond, lr, BF (Bgoto ifso, def_iinfo ()), Bnop None, iinfo), -- cgit