From 2408dd1aecf8d8c3bfd3b24a65f7f57cf602cb10 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 20 May 2021 11:58:40 +0200 Subject: Changing to an opaq record in BTL info, this is a broken commit --- scheduling/RTLtoBTLaux.ml | 44 ++++++++++++++++++++++++++------------------ 1 file changed, 26 insertions(+), 18 deletions(-) (limited to 'scheduling/RTLtoBTLaux.ml') diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml index 859bbf07..d4fd2643 100644 --- a/scheduling/RTLtoBTLaux.ml +++ b/scheduling/RTLtoBTLaux.ml @@ -6,37 +6,43 @@ open DebugPrint open PrintBTL open Camlcoq open AuxTools +open BTLaux -let mk_ni n = n +let undef_node = -1 +let mk_iinfo _inumb _pcond = { inumb = _inumb; pcond = _pcond } +let def_iinfo = { inumb = undef_node; pcond = None } + +let mk_binfo _bnumb = { bnumb = _bnumb } let encaps_final inst osucc = match inst with | BF _ | Bcond _ -> inst - | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc))) + | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo)) -let translate_inst ni inst is_final = +let translate_inst iinfo inst is_final = let osucc = ref None in let btli = match inst with | Inop s -> osucc := Some s; - Bnop ni + Bnop iinfo | Iop (op, lr, rd, s) -> osucc := Some s; - Bop (op, lr, rd, ni) + Bop (op, lr, rd, iinfo) | Iload (trap, chk, addr, lr, rd, s) -> osucc := Some s; - Bload (trap, chk, addr, lr, rd, ni) + Bload (trap, chk, addr, lr, rd, iinfo) | Istore (chk, addr, lr, rd, s) -> osucc := Some s; - Bstore (chk, addr, lr, rd, ni) - | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s, ni)) - | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr, ni)) - | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s, ni)) + Bstore (chk, addr, lr, rd, iinfo) + | Icall (sign, fn, lr, rd, s) -> BF (Bcall (sign, fn, lr, rd, s), iinfo) + | Itailcall (sign, fn, lr) -> BF (Btailcall (sign, fn, lr), iinfo) + | Ibuiltin (ef, lr, rd, s) -> BF (Bbuiltin (ef, lr, rd, s), iinfo) | Icond (cond, lr, ifso, ifnot, info) -> - Bcond (cond, lr, BF (Bgoto ifso), BF (Bgoto ifnot), info, ni) - | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl, ni)) - | Ireturn oreg -> BF (Breturn (oreg, ni)) + iinfo.pcond <- info; + Bcond (cond, lr, BF (Bgoto ifso, def_iinfo), BF (Bgoto ifnot, def_iinfo), iinfo) + | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl), iinfo) + | Ireturn oreg -> BF (Breturn (oreg), iinfo) in if is_final then encaps_final btli !osucc else btli @@ -52,7 +58,7 @@ let translate_function code entry join_points = let rec build_btl_block n = let inst = get_some @@ PTree.get n code in let psucc = predicted_successor inst in - let ni = mk_ni n in + let iinfo = mk_iinfo (p2i n) None in let succ = match psucc with | Some ps -> @@ -70,16 +76,18 @@ let translate_function code entry join_points = (* TODO gourdinl remove this *) assert (s = ifnot); next_nodes := !next_nodes @ non_predicted_successors inst psucc; - Bcond (cond, lr, BF (Bgoto ifso), build_btl_block s, info, ni) - | _ -> Bseq (translate_inst ni inst false, build_btl_block s)) + iinfo.pcond <- info; + Bcond (cond, lr, BF (Bgoto ifso, def_iinfo), build_btl_block s, iinfo) + | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s)) | None -> debug "BLOCK END.\n"; next_nodes := !next_nodes @ successors_inst inst; - translate_inst ni inst true + translate_inst iinfo inst true in let ib = build_btl_block e in let succs = !next_nodes in - let ibf = { entry = ib; input_regs = Regset.empty } in + let bi = mk_binfo (p2i e) in + let ibf = { entry = ib; input_regs = Regset.empty; binfo = bi } in btl_code := PTree.set e ibf !btl_code; List.iter build_btl_tree succs) in -- cgit