From 3e6844222d39b8a76bf0af20b9cbb0dfa2e35b5a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 21 May 2021 21:18:59 +0200 Subject: Now supporting Bnop insertion in conditions --- scheduling/BTLtoRTLaux.ml | 17 ++++++----------- 1 file changed, 6 insertions(+), 11 deletions(-) (limited to 'scheduling/BTLtoRTLaux.ml') diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml index b4833b2c..36d3e6a4 100644 --- a/scheduling/BTLtoRTLaux.ml +++ b/scheduling/BTLtoRTLaux.ml @@ -6,15 +6,11 @@ open AuxTools open DebugPrint open BTLaux -let is_atom = function - | Bseq (_, _) | Bcond (_, _, _, _, _) -> false - | _ -> true - let get_inumb iinfo = P.of_int iinfo.inumb let rec get_ib_num = function | BF (Bgoto s, _) -> s - | Bnop iinfo + | Bnop Some iinfo | Bop (_, _, _, iinfo) | Bload (_, _, _, _, _, iinfo) | Bstore (_, _, _, _, iinfo) @@ -22,6 +18,7 @@ let rec get_ib_num = function | BF (_, iinfo) -> get_inumb iinfo | Bseq (ib1, _) -> get_ib_num ib1 + | Bnop None -> failwith "get_ib_num: Bnop None found" let translate_function code entry = let rtl_code = ref PTree.empty in @@ -45,23 +42,21 @@ let translate_function code entry = | Bcond (cond, lr, BF (Bgoto s1, _), BF (Bgoto s2, _), iinfo) -> next_nodes := s1 :: s2 :: !next_nodes; Some (Icond (cond, lr, s1, s2, iinfo.pcond), get_inumb iinfo) - | Bcond (cond, lr, BF (Bgoto s1, _), ib2, iinfo) -> + | Bcond (cond, lr, BF (Bgoto s1, _), Bnop None, iinfo) -> assert (iinfo.pcond = Some false); next_nodes := s1 :: !next_nodes; - translate_btl_block ib2 None; Some - ( Icond (cond, lr, s1, get_ib_num ib2, iinfo.pcond), + ( Icond (cond, lr, s1, get_ib_num (get_some k), iinfo.pcond), get_inumb iinfo ) (* TODO gourdinl remove dynamic check *) | Bcond (_, _, _, _, _) -> failwith "translate_function: invalid Bcond" | Bseq (ib1, ib2) -> - (* TODO gourdinl remove dynamic check *) - assert (is_atom ib1); translate_btl_block ib1 (Some ib2); translate_btl_block ib2 None; None - | Bnop iinfo -> Some (Inop (get_ib_num (get_some k)), get_inumb iinfo) + | Bnop Some iinfo -> Some (Inop (get_ib_num (get_some k)), get_inumb iinfo) + | Bnop None -> failwith "translate_function: invalid Bnop" | Bop (op, lr, rd, iinfo) -> Some (Iop (op, lr, rd, get_ib_num (get_some k)), get_inumb iinfo) | Bload (trap, chk, addr, lr, rd, iinfo) -> -- cgit