diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-28 11:44:11 +0200 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-28 11:44:11 +0200 |
commit | 05b24fdb11414100b9b04867e6e2d3a1a9054162 (patch) | |
tree | 6ae4a50a2f311c6b2786e64de12d4d5f7755f865 /scheduling/BTLtoRTLaux.ml | |
parent | 56901933d110adef341312e1c7630b672827b41d (diff) | |
download | compcert-kvx-05b24fdb11414100b9b04867e6e2d3a1a9054162.tar.gz compcert-kvx-05b24fdb11414100b9b04867e6e2d3a1a9054162.zip |
Improvements in scheduling and renumbering BTL code
Diffstat (limited to 'scheduling/BTLtoRTLaux.ml')
-rw-r--r-- | scheduling/BTLtoRTLaux.ml | 117 |
1 files changed, 51 insertions, 66 deletions
diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml index 6d8c3d87..8e728bd2 100644 --- a/scheduling/BTLtoRTLaux.ml +++ b/scheduling/BTLtoRTLaux.ml @@ -4,6 +4,7 @@ open RTL open Camlcoq open RTLcommonaux open DebugPrint +open PrintBTL open BTLcommonaux open BTLtypes open BTLRenumber @@ -14,74 +15,58 @@ let get_ib_num ib = P.of_int (get_inumb_or_next ib) let translate_function btl entry = let rtl_code = ref PTree.empty in - let btl = reset_visited_ibf btl in - let rec build_rtl_tree e = - let ibf = get_some @@ PTree.get e btl in - if ibf.binfo.visited then () - else ( + let rec translate_btl_block ib k = + debug "Entering translate_btl_block...\n"; + print_btl_inst stderr ib; + let rtli = + 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), + get_inumb iinfo ) + | Bcond (_, _, _, _, _) -> + failwith "translate_function: unsupported Bcond" + | Bseq (ib1, ib2) -> + translate_btl_block ib1 (Some ib2); + translate_btl_block ib2 None; + None + | Bnop (Some iinfo) -> + Some (Inop (get_ib_num (get_some k)), get_inumb iinfo) + | Bnop None -> + failwith + "translate_function: Bnop None can only be in the right child of \ + Bcond" + | 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) -> + Some + ( Iload (trap, chk, addr, lr, rd, get_ib_num (get_some k)), + get_inumb iinfo ) + | Bstore (chk, addr, lr, src, iinfo) -> + Some + ( Istore (chk, addr, lr, src, get_ib_num (get_some k)), + get_inumb iinfo ) + | BF (Bcall (sign, fn, lr, rd, s), iinfo) -> + Some (Icall (sign, fn, lr, rd, s), get_inumb iinfo) + | BF (Btailcall (sign, fn, lr), iinfo) -> + Some (Itailcall (sign, fn, lr), get_inumb iinfo) + | BF (Bbuiltin (ef, lr, rd, s), iinfo) -> + Some (Ibuiltin (ef, lr, rd, s), get_inumb iinfo) + | BF (Bjumptable (arg, tbl), iinfo) -> + Some (Ijumptable (arg, tbl), get_inumb iinfo) + | BF (Breturn oreg, iinfo) -> Some (Ireturn oreg, get_inumb iinfo) + | BF (Bgoto s, iinfo) -> None + in + match rtli with + | Some (inst, inumb) -> rtl_code := PTree.set inumb inst !rtl_code + | None -> () + in + List.iter + (fun (n, ibf) -> ibf.binfo.visited <- true; let ib = ibf.entry in - let next_nodes = ref [] in - let rec translate_btl_block ib k = - let rtli = - (* TODO gourdinl remove assertions *) - match ib with - | 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, _), Bnop None, iinfo) -> - assert (iinfo.pcond = Some false); - next_nodes := s1 :: !next_nodes; - Some - ( Icond (cond, lr, s1, get_ib_num (get_some k), iinfo.pcond), - get_inumb iinfo ) - | Bcond (_, _, _, _, _) -> - failwith "translate_function: unsupported Bcond" - | Bseq (ib1, ib2) -> - translate_btl_block ib1 (Some ib2); - translate_btl_block ib2 None; - None - | Bnop (Some iinfo) -> - Some (Inop (get_ib_num (get_some k)), get_inumb iinfo) - | Bnop None -> - failwith - "translate_function: Bnop None can only be in the right child \ - of Bcond" - | 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) -> - Some - ( Iload (trap, chk, addr, lr, rd, get_ib_num (get_some k)), - get_inumb iinfo ) - | Bstore (chk, addr, lr, src, iinfo) -> - Some - ( Istore (chk, addr, lr, src, get_ib_num (get_some k)), - get_inumb iinfo ) - | BF (Bcall (sign, fn, lr, rd, s), iinfo) -> - next_nodes := s :: !next_nodes; - Some (Icall (sign, fn, lr, rd, s), get_inumb iinfo) - | BF (Btailcall (sign, fn, lr), iinfo) -> - Some (Itailcall (sign, fn, lr), get_inumb iinfo) - | BF (Bbuiltin (ef, lr, rd, s), iinfo) -> - next_nodes := s :: !next_nodes; - Some (Ibuiltin (ef, lr, rd, s), get_inumb iinfo) - | BF (Bjumptable (arg, tbl), iinfo) -> - next_nodes := tbl @ !next_nodes; - Some (Ijumptable (arg, tbl), get_inumb iinfo) - | BF (Breturn oreg, iinfo) -> Some (Ireturn oreg, get_inumb iinfo) - | BF (Bgoto s, iinfo) -> - next_nodes := s :: !next_nodes; - None - in - match rtli with - | Some (inst, inumb) -> rtl_code := PTree.set inumb inst !rtl_code - | None -> () - in - translate_btl_block ib None; - let succs = !next_nodes in - List.iter build_rtl_tree succs) - in - build_rtl_tree entry; + translate_btl_block ib None) + (PTree.elements btl); !rtl_code let btl2rtl (f : BTL.coq_function) = |