diff options
| -rw-r--r-- | scheduling/BTLRenumber.ml | 16 | ||||
| -rw-r--r-- | scheduling/BTLScheduleraux.ml | 7 | ||||
| -rw-r--r-- | scheduling/BTLcommonaux.ml | 14 | ||||
| -rw-r--r-- | scheduling/BTLtoRTLaux.ml | 117 | ||||
| -rw-r--r-- | scheduling/RTLtoBTLaux.ml | 5 |
5 files changed, 65 insertions, 94 deletions
diff --git a/scheduling/BTLRenumber.ml b/scheduling/BTLRenumber.ml index 36f3bcf5..58d4f7ac 100644 --- a/scheduling/BTLRenumber.ml +++ b/scheduling/BTLRenumber.ml @@ -3,6 +3,8 @@ open BTL open RTLcommonaux open BTLcommonaux open BTLtypes +open DebugPrint +open PrintBTL let recompute_inumbs btl entry = let btl = reset_visited_ib (reset_visited_ibf btl) in @@ -53,13 +55,6 @@ let recompute_inumbs btl entry = walk succ None; iinfo.inumb <- ipos () | Bseq (ib1, ib2) -> walk ib1 (Some ib2) - | Bcond (_, _, BF (Bgoto s1, iinfoL), BF (Bgoto s2, iinfoR), iinfo) -> - iinfoL.visited <- true; - iinfoR.visited <- true; - let ib1 = get_some @@ PTree.get s1 btl in - let ib2 = get_some @@ PTree.get s2 btl in - walk_smallest_child (p2i s1) (p2i s2) ib1.entry ib2.entry; - iinfo.inumb <- ipos () | Bcond (_, _, BF (Bgoto s1, iinfoL), Bnop None, iinfoF) -> iinfoL.visited <- true; let ib1 = get_some @@ PTree.get s1 btl in @@ -104,8 +99,13 @@ let regenerate_btl_tree btl entry = PTree.set n_pos ibf ord_btl) btl PTree.empty in + debug "Renumbered BTL with new_entry=%d:\n" (p2i !new_entry); + print_btl_code stderr ord_btl; (ord_btl, !new_entry) let renumber btl entry = + (*debug_flag := true;*) let btl' = recompute_inumbs btl entry in - regenerate_btl_tree btl' entry + let ord_btl, new_entry = regenerate_btl_tree btl' entry in + (*debug_flag := false;*) + (ord_btl, new_entry) diff --git a/scheduling/BTLScheduleraux.ml b/scheduling/BTLScheduleraux.ml index 4b5ebb32..ad0c307d 100644 --- a/scheduling/BTLScheduleraux.ml +++ b/scheduling/BTLScheduleraux.ml @@ -80,7 +80,6 @@ let build_constraints_and_resources (opweights : opweights) insts btl = in Array.iteri (fun i inst -> - (* TODO gourdinl liveins for Bcond *) match inst with | Bnop _ -> let rs = Array.map (fun _ -> 0) opweights.pipelined_resource_bounds in @@ -203,13 +202,13 @@ let flatten_blk_basics ibf = | BF (_, _) -> last := Some ib; [] - | Bseq (ib1, ib2) -> traverse_blk ib1 @ traverse_blk ib2 - | Bcond (_, _, _, _, iinfo) -> ( + | Bseq ((Bcond (_, _, _, _, iinfo) as ib1), ib2) -> ( match iinfo.pcond with - | Some _ -> [ ib ] + | Some _ -> [ ib1 ] @ traverse_blk ib2 | None -> last := Some ib; []) + | Bseq (ib1, ib2) -> traverse_blk ib1 @ traverse_blk ib2 | _ -> [ ib ] in let ibl = traverse_blk ib in diff --git a/scheduling/BTLcommonaux.ml b/scheduling/BTLcommonaux.ml index dabf760a..4605d613 100644 --- a/scheduling/BTLcommonaux.ml +++ b/scheduling/BTLcommonaux.ml @@ -68,17 +68,3 @@ let rec get_inumb_or_next = function iinfo.inumb | Bseq (ib1, _) -> get_inumb_or_next ib1 | _ -> failwith "get_inumb_or_next: Bnop None" - -let rec set_next_inumb btl pos = function - | BF (Bgoto s, _) -> - let ib' = (get_some @@ PTree.get s btl).entry in - set_next_inumb btl pos ib' - | BF (_, iinfo) - | Bnop (Some iinfo) - | Bop (_, _, _, iinfo) - | Bload (_, _, _, _, _, iinfo) - | Bstore (_, _, _, _, iinfo) - | Bcond (_, _, _, _, iinfo) -> - iinfo.inumb <- pos - | Bseq (ib1, _) -> set_next_inumb btl pos ib1 - | _ -> failwith "get_inumb_or_next: Bnop None" 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) = diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml index 056fe213..d04326ea 100644 --- a/scheduling/RTLtoBTLaux.ml +++ b/scheduling/RTLtoBTLaux.ml @@ -10,7 +10,7 @@ open BTLScheduleraux let encaps_final inst osucc = match inst with - | BF _ | Bcond _ -> inst + | BF _ -> inst | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo ())) let translate_inst (iinfo : BTL.inst_info) inst is_final = @@ -33,12 +33,13 @@ let translate_inst (iinfo : BTL.inst_info) inst is_final = | 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) -> + osucc := Some ifnot; iinfo.pcond <- info; Bcond ( cond, lr, BF (Bgoto ifso, def_iinfo ()), - BF (Bgoto ifnot, def_iinfo ()), + Bnop None, iinfo ) | Ijumptable (arg, tbl) -> BF (Bjumptable (arg, tbl), iinfo) | Ireturn oreg -> BF (Breturn oreg, iinfo) |