diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-21 21:18:59 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-21 21:18:59 +0200 |
| commit | 3e6844222d39b8a76bf0af20b9cbb0dfa2e35b5a (patch) | |
| tree | abbb54fca752a15a190e66dcb902a42b0be97cd9 /scheduling/BTLtoRTLaux.ml | |
| parent | 65247b67cbd469b9cd3bea22410bd11af450696c (diff) | |
| download | compcert-kvx-3e6844222d39b8a76bf0af20b9cbb0dfa2e35b5a.tar.gz compcert-kvx-3e6844222d39b8a76bf0af20b9cbb0dfa2e35b5a.zip | |
Now supporting Bnop insertion in conditions
Diffstat (limited to 'scheduling/BTLtoRTLaux.ml')
| -rw-r--r-- | scheduling/BTLtoRTLaux.ml | 17 |
1 files changed, 6 insertions, 11 deletions
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) -> |