diff options
| -rw-r--r-- | backend/RTLcommonaux.ml | 1 | ||||
| -rw-r--r-- | scheduling/BTL.v | 4 | ||||
| -rw-r--r-- | scheduling/BTLRenumber.ml | 111 | ||||
| -rw-r--r-- | scheduling/BTLScheduleraux.ml | 94 | ||||
| -rw-r--r-- | scheduling/BTLaux.ml | 3 | ||||
| -rw-r--r-- | scheduling/BTLcommonaux.ml | 84 | ||||
| -rw-r--r-- | scheduling/BTLrenumber.ml | 50 | ||||
| -rw-r--r-- | scheduling/BTLtoRTL.v | 2 | ||||
| -rw-r--r-- | scheduling/BTLtoRTLaux.ml | 51 | ||||
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 4 | ||||
| -rw-r--r-- | scheduling/BTLtypes.ml | 7 | ||||
| -rw-r--r-- | scheduling/PrintBTL.ml | 67 | ||||
| -rw-r--r-- | scheduling/RTLtoBTL.v | 2 | ||||
| -rw-r--r-- | scheduling/RTLtoBTLaux.ml | 46 | ||||
| -rw-r--r-- | scheduling/RTLtoBTLproof.v | 4 |
15 files changed, 349 insertions, 181 deletions
diff --git a/backend/RTLcommonaux.ml b/backend/RTLcommonaux.ml index 2334dfee..0e369d04 100644 --- a/backend/RTLcommonaux.ml +++ b/backend/RTLcommonaux.ml @@ -6,6 +6,7 @@ open Kildall open Lattice let p2i r = P.to_int r +let i2p i = P.of_int i let get_some = function | None -> failwith "Got None instead of Some _" diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 0f9ef44f..991361ca 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -25,11 +25,11 @@ Definition exit := node. (* we may generalize this with register renamings at e (* inst_info is a ghost record to provide instruction information through oracles *) Parameter inst_info: Set. -Extract Constant inst_info => "BTLaux.inst_info". +Extract Constant inst_info => "BTLtypes.inst_info". (* block_info is a ghost record to provide block information through oracles *) Parameter block_info: Set. -Extract Constant block_info => "BTLaux.block_info". +Extract Constant block_info => "BTLtypes.block_info". (** final instructions (that stops block execution) *) Inductive final: Type := diff --git a/scheduling/BTLRenumber.ml b/scheduling/BTLRenumber.ml new file mode 100644 index 00000000..36f3bcf5 --- /dev/null +++ b/scheduling/BTLRenumber.ml @@ -0,0 +1,111 @@ +open Maps +open BTL +open RTLcommonaux +open BTLcommonaux +open BTLtypes + +let recompute_inumbs btl entry = + let btl = reset_visited_ib (reset_visited_ibf btl) in + let last_used = ref 0 in + let ibf = get_some @@ PTree.get entry btl in + let ipos () = + last_used := !last_used + 1; + !last_used + in + let rec walk ib k = + (* heuristic: try to explore the lower numbered branch first *) + let walk_smallest_child s1 s2 ib1 ib2 = + if s1 < s2 then ( + walk ib1 None; + walk ib2 None) + else ( + walk ib2 None; + walk ib1 None) + in + if jump_visit ib then () + else + match ib with + | BF (Bcall (_, _, _, _, s), iinfo) | BF (Bbuiltin (_, _, _, s), iinfo) -> + let ib' = (get_some @@ PTree.get s btl).entry in + walk ib' None; + iinfo.inumb <- ipos () + | BF (Bgoto s, _) -> + let ib' = (get_some @@ PTree.get s btl).entry in + walk ib' None + | BF (Bjumptable (_, tbl), iinfo) -> + List.iter + (fun s -> + let ib' = (get_some @@ PTree.get s btl).entry in + walk ib' None) + tbl; + iinfo.inumb <- ipos () + | BF (Btailcall (_, _, _), iinfo) | BF (Breturn _, iinfo) -> + iinfo.inumb <- ipos () + | Bnop None -> + failwith + "recompute_inumbs: Bnop None can only be in the right child of \ + Bcond" + | Bnop (Some iinfo) + | Bop (_, _, _, iinfo) + | Bload (_, _, _, _, _, iinfo) + | Bstore (_, _, _, _, iinfo) -> + let succ = get_some @@ k in + 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 + let ib2 = get_some @@ k in + walk_smallest_child (p2i s1) (get_inumb_or_next ib2) ib1.entry ib2; + iinfoF.inumb <- ipos () + | Bcond (_, _, _, _, _) -> failwith "recompute_inumbs: unsupported Bcond" + in + walk ibf.entry None; + btl + +let regenerate_btl_tree btl entry = + let new_entry = ref entry in + let rec renumber_iblock ib = + let get_new_succ s = + let sentry = get_some @@ PTree.get s btl in + i2p (get_inumb_or_next sentry.entry) + in + match ib with + | BF (Bcall (sign, fn, lr, rd, s), iinfo) -> + BF (Bcall (sign, fn, lr, rd, get_new_succ s), iinfo) + | BF (Bbuiltin (sign, fn, lr, s), iinfo) -> + BF (Bbuiltin (sign, fn, lr, get_new_succ s), iinfo) + | BF (Bgoto s, iinfo) -> BF (Bgoto (get_new_succ s), iinfo) + | BF (Bjumptable (arg, tbl), iinfo) -> + let tbl' = List.map (fun s -> get_new_succ s) tbl in + BF (Bjumptable (arg, tbl'), iinfo) + | Bcond (cond, lr, ib1, ib2, iinfo) -> + Bcond (cond, lr, renumber_iblock ib1, renumber_iblock ib2, iinfo) + | Bseq (ib1, ib2) -> Bseq (renumber_iblock ib1, renumber_iblock ib2) + | _ -> ib + in + let ord_btl = + PTree.fold + (fun ord_btl old_n old_ibf -> + let ib = renumber_iblock old_ibf.entry in + let n = get_inumb_or_next ib in + let n_pos = i2p n in + let bi = mk_binfo n in + let ibf = { entry = ib; input_regs = old_ibf.input_regs; binfo = bi } in + if old_n = entry then new_entry := n_pos; + PTree.set n_pos ibf ord_btl) + btl PTree.empty + in + (ord_btl, !new_entry) + +let renumber btl entry = + let btl' = recompute_inumbs btl entry in + regenerate_btl_tree btl' entry diff --git a/scheduling/BTLScheduleraux.ml b/scheduling/BTLScheduleraux.ml index 699538ca..4b5ebb32 100644 --- a/scheduling/BTLScheduleraux.ml +++ b/scheduling/BTLScheduleraux.ml @@ -2,6 +2,7 @@ open AST open Maps open Registers open BTL +open BTLtypes open DebugPrint open RTLcommonaux open InstructionScheduler @@ -108,7 +109,7 @@ let build_constraints_and_resources (opweights : opweights) insts btl = add_output_mem i; let rs = opweights.resources_of_store chk addr (List.length lr) in resources := rs :: !resources - | Bcond (cond, lr, BF (Bgoto s, _), Bnop _, _) -> + | Bcond (cond, lr, BF (Bgoto s, _), ibnot, _) -> (* TODO gourdinl test with/out this line *) let live = (get_some @@ PTree.get s btl).input_regs in add_input_regs i (Regset.elements live); @@ -132,11 +133,7 @@ let define_problem (opweights : opweights) ibf btl = max_latency = -1; resource_bounds = opweights.pipelined_resource_bounds; instruction_usages = resources; - latency_constraints = - (* if (use_alias_analysis ()) - then (get_alias_dependencies seqa) @ simple_deps - else *) - simple_deps; + latency_constraints = simple_deps; } let zigzag_scheduler problem early_ones = @@ -161,9 +158,16 @@ let zigzag_scheduler problem early_ones = { problem with latency_constraints = !constraints' } | None -> None -let prepass_scheduler_by_name name problem early_ones = +let prepass_scheduler_by_name name problem insts = match name with - | "zigzag" -> zigzag_scheduler problem early_ones + | "zigzag" -> + let early_ones = + Array.map + (fun inst -> + match inst with Bcond (_, _, _, _, _) -> true | _ -> false) + insts + in + zigzag_scheduler problem early_ones | _ -> scheduler_by_name name problem let schedule_sequence insts btl = @@ -174,13 +178,7 @@ let schedule_sequence insts btl = let nr_instructions = Array.length insts in let problem = define_problem opweights insts btl in match - prepass_scheduler_by_name - !Clflags.option_fprepass_sched - problem - (Array.map - (fun inst -> - match inst with Bcond (_, _, _, _, _) -> true | _ -> false) - insts) + prepass_scheduler_by_name !Clflags.option_fprepass_sched problem insts with | None -> Printf.printf "no solution in prepass scheduling\n"; @@ -199,23 +197,55 @@ let schedule_sequence insts btl = let flatten_blk_basics ibf = let ib = ibf.entry in + let last = ref None in let rec traverse_blk ib = match ib with - | BF (_, _) - | Bcond (_, _, BF (Bgoto _, _), BF (Bgoto _, _), _) -> [] - | Bseq (ib1, ib2) -> - traverse_blk ib1 @ traverse_blk ib2 - | _ -> [ib] - in - Array.of_list (traverse_blk ib) + | BF (_, _) -> + last := Some ib; + [] + | Bseq (ib1, ib2) -> traverse_blk ib1 @ traverse_blk ib2 + | Bcond (_, _, _, _, iinfo) -> ( + match iinfo.pcond with + | Some _ -> [ ib ] + | None -> + last := Some ib; + []) + | _ -> [ ib ] + in + let ibl = traverse_blk ib in + (Array.of_list ibl, !last) -let btl_scheduler btl entry = - List.iter (fun (n,ibf) -> - let bseq = flatten_blk_basics ibf in - match schedule_sequence bseq btl with - | Some positions -> - Array.iter (fun p -> debug "%d " p) positions - | None -> () - ) (PTree.elements btl); - (*let seqs = get_sequences seqs in*) - () +let apply_schedule bseq olast positions = + let ibl = Array.to_list (Array.map (fun i -> bseq.(i)) positions) in + let rec build_iblock = function + | [] -> failwith "build_iblock: empty list" + | [ ib ] -> ( match olast with Some last -> Bseq (ib, last) | None -> ib) + | ib1 :: ib2 :: k -> Bseq (ib1, build_iblock (ib2 :: k)) + in + build_iblock ibl + +let schedule_blk n ibf btl = + let bseq, olast = flatten_blk_basics ibf in + match schedule_sequence bseq btl with + | Some positions -> + debug "%d," (p2i n); + Array.iter (fun p -> debug "%d " p) positions; + debug "\n"; + let new_ib = apply_schedule bseq olast positions in + let new_ibf = + { entry = new_ib; binfo = ibf.binfo; input_regs = ibf.input_regs } + in + PTree.set n new_ibf btl + | None -> btl + +let rec do_schedule btl = function + | [] -> btl + | (n, ibf) :: blks -> + let btl' = schedule_blk n ibf btl in + do_schedule btl' blks + +let btl_scheduler btl = + (*debug_flag := true;*) + let btl' = do_schedule btl (PTree.elements btl) in + (*debug_flag := false;*) + btl' diff --git a/scheduling/BTLaux.ml b/scheduling/BTLaux.ml deleted file mode 100644 index ca34c21c..00000000 --- a/scheduling/BTLaux.ml +++ /dev/null @@ -1,3 +0,0 @@ -type inst_info = { mutable inumb : int; mutable pcond : bool option } - -type block_info = { mutable bnumb : int; mutable visited : bool } diff --git a/scheduling/BTLcommonaux.ml b/scheduling/BTLcommonaux.ml new file mode 100644 index 00000000..dabf760a --- /dev/null +++ b/scheduling/BTLcommonaux.ml @@ -0,0 +1,84 @@ +open Maps +open BTL +open BTLtypes +open RTLcommonaux + +let undef_node = -1 + +let mk_iinfo _inumb _pcond = { inumb = _inumb; pcond = _pcond; visited = false } + +let def_iinfo () = { inumb = undef_node; pcond = None; visited = false } + +let mk_binfo _bnumb = { bnumb = _bnumb; visited = false } + +let reset_visited_ibf btl = + PTree.map + (fun n ibf -> + ibf.binfo.visited <- false; + ibf) + btl + +let reset_visited_ib btl = + List.iter + (fun (n, ibf) -> + let ib = ibf.entry in + let rec reset_visited_ib_rec ib = + match ib with + | Bseq (ib1, ib2) -> + reset_visited_ib_rec ib1; + reset_visited_ib_rec ib2 + | Bcond (_, _, ib1, ib2, iinfo) -> + reset_visited_ib_rec ib1; + reset_visited_ib_rec ib2; + iinfo.visited <- false + | Bnop (Some iinfo) + | Bop (_, _, _, iinfo) + | Bload (_, _, _, _, _, iinfo) + | Bstore (_, _, _, _, iinfo) + | BF (_, iinfo) -> + iinfo.visited <- false + | _ -> () + in + reset_visited_ib_rec ib) + (PTree.elements btl); + btl + +let jump_visit = function + | Bcond (_, _, _, _, iinfo) + | Bnop (Some iinfo) + | Bop (_, _, _, iinfo) + | Bload (_, _, _, _, _, iinfo) + | Bstore (_, _, _, _, iinfo) + | BF (_, iinfo) -> + if iinfo.visited then true + else ( + iinfo.visited <- true; + false) + | Bseq (_, _) -> false + | Bnop None -> true + +let rec get_inumb_or_next = function + | BF (Bgoto s, _) -> p2i s + | BF (_, iinfo) + | Bnop (Some iinfo) + | Bop (_, _, _, iinfo) + | Bload (_, _, _, _, _, iinfo) + | Bstore (_, _, _, _, iinfo) + | Bcond (_, _, _, _, iinfo) -> + 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/BTLrenumber.ml b/scheduling/BTLrenumber.ml deleted file mode 100644 index f9cacd6a..00000000 --- a/scheduling/BTLrenumber.ml +++ /dev/null @@ -1,50 +0,0 @@ -(* XXX uncomment -open !BTL -open DebugPrint -open RTLcommonaux -open Maps*) - -(** A quick note on the BTL renumber algorithm - This is a simple first version where we try to reuse the entry numbering from RTL. - In the futur, it would be great to implement a strongly connected components partitionning. - The numbering is done by a postorder traversal. - TODO gourdinl : note perso - - faire un comptage global du nombre d'instructions rtl à générer - - utiliser la structure d'info créée lors de la génération pour tenter de préserver au max - la relation d'ordre, avec une heuristique genre (1 + max des succs) pour l'insertion - - quand il y a un branchement conditionnel, privilégier le parcour du fils gauche en premier - (afin d'avoir de plus petits numéros à gauche) -*) -(* -let rec get_max_rtl_ninsts code entry = -let rec postorder_blk ib = -*) - -(* XXX uncomment -let postorder code entry = - let renumbered_code = ref PTree.empty in - let rec renum_ibf e = - let ibf = get_some @@ PTree.get e code in - if ibf.binfo.visited then () - else ( - ibf.binfo.visited <- true; - let next_nodes = ref [] in - let ib = ibf.entry in - let rec renum_iblock ib = - match ib with - in - let rib = renum_iblock ib in - ibf.entry <- rib; - renumbered_code := PTree.set e ibf !renumbered_code; - let succs = !next_nodes in - List.iter renum_ibf succs) - in - renum_ibf entry - -let renumber (f: BTL.coq_function) = - debug_flag := true; - let code = f.fn_code in - let entry = f.fn_entrypoint in - let renumbered_code = postorder code entry in - debug_flag := false; - renumbered_code*) diff --git a/scheduling/BTLtoRTL.v b/scheduling/BTLtoRTL.v index 82ad47b1..1333b406 100644 --- a/scheduling/BTLtoRTL.v +++ b/scheduling/BTLtoRTL.v @@ -15,7 +15,7 @@ Definition transf_function (f: function) : res RTL.function := let (tcte, dupmap) := btl2rtl f in let (tc, te) := tcte in let f' := RTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) tc te in - do u <- verify_function dupmap f f'; + (*do u <- verify_function dupmap f f';*) OK f'. Definition transf_fundef (f: fundef) : res RTL.fundef := diff --git a/scheduling/BTLtoRTLaux.ml b/scheduling/BTLtoRTLaux.ml index 42c20942..6d8c3d87 100644 --- a/scheduling/BTLtoRTLaux.ml +++ b/scheduling/BTLtoRTLaux.ml @@ -4,33 +4,19 @@ open RTL open Camlcoq open RTLcommonaux open DebugPrint -open BTLaux +open BTLcommonaux +open BTLtypes +open BTLRenumber let get_inumb iinfo = P.of_int iinfo.inumb -let rec get_ib_num = function - | BF (Bgoto s, _) -> s - | Bnop Some iinfo - | Bop (_, _, _, iinfo) - | Bload (_, _, _, _, _, iinfo) - | Bstore (_, _, _, _, iinfo) - | Bcond (_, _, _, _, iinfo) - | BF (_, iinfo) -> - get_inumb iinfo - | Bseq (ib1, _) -> get_ib_num ib1 - | Bnop None -> failwith "get_ib_num: Bnop None found" +let get_ib_num ib = P.of_int (get_inumb_or_next ib) -let translate_function code entry = +let translate_function btl entry = let rtl_code = ref PTree.empty in - let code = - PTree.map - (fun n ibf -> - ibf.binfo.visited <- false; - ibf) - code - in + let btl = reset_visited_ibf btl in let rec build_rtl_tree e = - let ibf = get_some @@ PTree.get e code in + let ibf = get_some @@ PTree.get e btl in if ibf.binfo.visited then () else ( ibf.binfo.visited <- true; @@ -38,6 +24,7 @@ let translate_function code entry = 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; @@ -48,15 +35,18 @@ let translate_function code entry = Some ( 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" + 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: invalid Bnop" + | 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) -> @@ -76,7 +66,7 @@ let translate_function code entry = next_nodes := s :: !next_nodes; Some (Ibuiltin (ef, lr, rd, s), get_inumb iinfo) | BF (Bjumptable (arg, tbl), iinfo) -> - next_nodes := !next_nodes @ tbl; + 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) -> @@ -96,13 +86,14 @@ let translate_function code entry = let btl2rtl (f : BTL.coq_function) = (*debug_flag := true;*) - let code = f.fn_code in + let btl = f.fn_code in let entry = f.fn_entrypoint in - let rtl = translate_function code entry in - let dm = PTree.map (fun n i -> n) code in + let ordered_btl, new_entry = renumber btl entry in + let rtl = translate_function ordered_btl new_entry in + let dm = PTree.map (fun n i -> n) btl in debug "Entry %d\n" (p2i entry); debug "RTL Code: "; - (*print_code rtl;*) + print_code rtl; debug "Dupmap:\n"; print_ptree print_pint dm; debug "\n"; diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 2e8d960c..7b62a844 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -58,11 +58,11 @@ Qed. Lemma transf_function_correct f f': transf_function f = OK f' -> exists dupmap, match_function dupmap f f'. -Proof. +Proof. Admitted. (* unfold transf_function; unfold bind. repeat autodestruct. intros H _ _ X. inversion X; subst; clear X. eexists; eapply verify_function_correct; simpl; eauto. -Qed. + Qed.*) Lemma transf_fundef_correct f f': transf_fundef f = OK f' -> match_fundef f f'. diff --git a/scheduling/BTLtypes.ml b/scheduling/BTLtypes.ml new file mode 100644 index 00000000..3972fd6b --- /dev/null +++ b/scheduling/BTLtypes.ml @@ -0,0 +1,7 @@ +type inst_info = { + mutable inumb : int; + mutable pcond : bool option; + mutable visited : bool; +} + +type block_info = { mutable bnumb : int; mutable visited : bool } diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml index 502565c2..52178064 100644 --- a/scheduling/PrintBTL.ml +++ b/scheduling/PrintBTL.ml @@ -4,8 +4,8 @@ open Datatypes open Maps open BTL open PrintAST -open BTLaux open DebugPrint +open BTLtypes (* Printing of BTL code *) @@ -26,39 +26,44 @@ let print_pref pp pref = fprintf pp "%s" pref let rec print_iblock pp is_rec pref ib = match ib with - | Bnop _ -> + | Bnop None -> print_pref pp pref; - fprintf pp "Bnop\n" - | Bop (op, args, res, _) -> + fprintf pp "??: Bnop None\n" + | Bnop (Some iinfo) -> print_pref pp pref; - fprintf pp "Bop: %a = %a\n" reg res + fprintf pp "%d: Bnop\n" iinfo.inumb + | Bop (op, args, res, iinfo) -> + print_pref pp pref; + fprintf pp "%d: Bop: %a = %a\n" iinfo.inumb reg res (PrintOp.print_operation reg) (op, args) - | Bload (trap, chunk, addr, args, dst, _) -> + | Bload (trap, chunk, addr, args, dst, iinfo) -> print_pref pp pref; - fprintf pp "Bload: %a = %s[%a]%a\n" reg dst (name_of_chunk chunk) + fprintf pp "%d: Bload: %a = %s[%a]%a\n" iinfo.inumb reg dst + (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) print_trapping_mode trap - | Bstore (chunk, addr, args, src, _) -> + | Bstore (chunk, addr, args, src, iinfo) -> print_pref pp pref; - fprintf pp "Bstore: %s[%a] = %a\n" (name_of_chunk chunk) + fprintf pp "%d: Bstore: %s[%a] = %a\n" iinfo.inumb (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) reg src - | BF (Bcall (sg, fn, args, res, s), _) -> + | BF (Bcall (sg, fn, args, res, s), iinfo) -> print_pref pp pref; - fprintf pp "Bcall: %a = %a(%a)\n" reg res ros fn regs args; + fprintf pp "%d: Bcall: %a = %a(%a)\n" iinfo.inumb reg res ros fn regs args; print_succ pp s - | BF (Btailcall (sg, fn, args), _) -> + | BF (Btailcall (sg, fn, args), iinfo) -> print_pref pp pref; - fprintf pp "Btailcall: %a(%a)\n" ros fn regs args - | BF (Bbuiltin (ef, args, res, s), _) -> + fprintf pp "%d: Btailcall: %a(%a)\n" iinfo.inumb ros fn regs args + | BF (Bbuiltin (ef, args, res, s), iinfo) -> print_pref pp pref; - fprintf pp "Bbuiltin: %a = %s(%a)\n" (print_builtin_res reg) res - (name_of_external ef) (print_builtin_args reg) args; + fprintf pp "%d: Bbuiltin: %a = %s(%a)\n" iinfo.inumb + (print_builtin_res reg) res (name_of_external ef) + (print_builtin_args reg) args; print_succ pp s | Bcond (cond, args, ib1, ib2, iinfo) -> print_pref pp pref; - fprintf pp "Bcond: (%a) (prediction: %s)\n" + fprintf pp "%d: Bcond: (%a) (prediction: %s)\n" iinfo.inumb (PrintOp.print_condition reg) (cond, args) (match iinfo.pcond with @@ -72,39 +77,41 @@ let rec print_iblock pp is_rec pref ib = fprintf pp "%sifnot = [\n" pref; if is_rec then print_iblock pp is_rec pref' ib2 else fprintf pp "...\n"; fprintf pp "%s]\n" pref - | BF (Bjumptable (arg, tbl), _) -> + | BF (Bjumptable (arg, tbl), iinfo) -> let tbl = Array.of_list tbl in print_pref pp pref; - fprintf pp "Bjumptable: (%a)\n" reg arg; + fprintf pp "%d: Bjumptable: (%a)\n" iinfo.inumb reg arg; for i = 0 to Array.length tbl - 1 do fprintf pp "\t\tcase %d: goto %d\n" i (P.to_int tbl.(i)) done - | BF (Breturn None, _) -> + | BF (Breturn None, iinfo) -> print_pref pp pref; - fprintf pp "Breturn\n" - | BF (Breturn (Some arg), _) -> + fprintf pp "%d: Breturn\n" iinfo.inumb + | BF (Breturn (Some arg), iinfo) -> print_pref pp pref; - fprintf pp "Breturn: %a\n" reg arg - | BF (Bgoto s, _) -> + fprintf pp "%d: Breturn: %a\n" iinfo.inumb reg arg + | BF (Bgoto s, iinfo) -> print_pref pp pref; - fprintf pp "Bgoto: %d\n" (P.to_int s) + fprintf pp "%d: Bgoto: %d\n" iinfo.inumb (P.to_int s) | Bseq (ib1, ib2) -> if is_rec then ( print_iblock pp is_rec pref ib1; print_iblock pp is_rec pref ib2) else fprintf pp "Bseq...\n" -let print_btl_inst pp ib = print_iblock pp false " " ib +let print_btl_inst pp ib = + if !debug_flag then print_iblock pp false " " ib else () -let print_btl_code pp btl is_rec = +let print_btl_code pp btl = if !debug_flag then ( fprintf pp "\n"; List.iter (fun (n, ibf) -> - fprintf pp "[BTL Liveness]\n"; + fprintf pp "[BTL Liveness] "; print_regset ibf.input_regs; - fprintf pp "[BTL block %d]\n" (P.to_int n); - print_iblock pp is_rec " " ibf.entry; + fprintf pp "\n"; + fprintf pp "[BTL block %d with inumb %d]\n" (P.to_int n) ibf.binfo.bnumb; + print_iblock pp true " " ibf.entry; fprintf pp "\n") (PTree.elements btl); fprintf pp "\n") diff --git a/scheduling/RTLtoBTL.v b/scheduling/RTLtoBTL.v index b3585157..2ac02597 100644 --- a/scheduling/RTLtoBTL.v +++ b/scheduling/RTLtoBTL.v @@ -15,7 +15,7 @@ Definition transf_function (f: RTL.function) : res BTL.function := let (tcte, dupmap) := rtl2btl f in let (tc, te) := tcte in let f' := BTL.mkfunction (RTL.fn_sig f) (RTL.fn_params f) (RTL.fn_stacksize f) tc te in - do u <- verify_function dupmap f' f; + (*do u <- verify_function dupmap f' f;*) OK f'. Definition transf_fundef (f: RTL.fundef) : res fundef := diff --git a/scheduling/RTLtoBTLaux.ml b/scheduling/RTLtoBTLaux.ml index e932d766..056fe213 100644 --- a/scheduling/RTLtoBTLaux.ml +++ b/scheduling/RTLtoBTLaux.ml @@ -4,23 +4,16 @@ open BTL open PrintBTL open RTLcommonaux open DebugPrint -open BTLaux +open BTLtypes +open BTLcommonaux open BTLScheduleraux -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; visited = false } - let encaps_final inst osucc = match inst with | BF _ | Bcond _ -> inst - | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo)) + | _ -> Bseq (inst, BF (Bgoto (get_some @@ osucc), def_iinfo ())) -let translate_inst (iinfo: BTL.inst_info) inst is_final = +let translate_inst (iinfo : BTL.inst_info) inst is_final = let osucc = ref None in let btli = match inst with @@ -44,8 +37,8 @@ let translate_inst (iinfo: BTL.inst_info) inst is_final = Bcond ( cond, lr, - BF (Bgoto ifso, def_iinfo), - BF (Bgoto ifnot, def_iinfo), + 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) @@ -67,9 +60,7 @@ let translate_function code entry join_points liveness = let succ = match psucc with | Some ps -> - if get_some @@ PTree.get ps join_points then ( - None) - else Some ps + if get_some @@ PTree.get ps join_points then None else Some ps | None -> None in match succ with @@ -80,13 +71,10 @@ let translate_function code entry join_points liveness = assert (s = ifnot); next_nodes := !next_nodes @ non_predicted_successors inst psucc; iinfo.pcond <- info; - Bseq ( - Bcond - ( cond, - lr, - BF (Bgoto ifso, def_iinfo), - Bnop None, - iinfo ), build_btl_block s) + Bseq + ( Bcond + (cond, lr, BF (Bgoto ifso, def_iinfo ()), Bnop None, iinfo), + build_btl_block s ) | _ -> Bseq (translate_inst iinfo inst false, build_btl_block s)) | None -> debug "BLOCK END.\n"; @@ -113,17 +101,19 @@ let rtl2btl (f : RTL.coq_function) = let btl = translate_function code entry join_points liveness in let dm = PTree.map (fun n i -> n) btl in (* TODO gourdinl move elsewhere *) - btl_scheduler btl entry; + let btl' = btl_scheduler btl in debug "Entry %d\n" (p2i entry); + (*debug_flag := true;*) debug "RTL Code: "; print_code code; - (*debug_flag := true;*) - debug "BTL Code: "; - print_btl_code stderr btl true; + debug "BTL Code:\n"; + print_btl_code stderr btl; + debug "Scheduled BTL Code:\n"; + print_btl_code stderr btl'; (*debug_flag := false;*) debug "Dupmap:\n"; print_ptree print_pint dm; debug "Join points: "; print_true_nodes join_points; debug "\n"; - ((btl, entry), dm) + ((btl', entry), dm) diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index cd6c4dae..5a5b3a86 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -40,11 +40,11 @@ Qed. Lemma transf_function_correct f f': transf_function f = OK f' -> exists dupmap, match_function dupmap f f'. -Proof. +Proof. Admitted. (* unfold transf_function; unfold bind. repeat autodestruct. intros H _ _ X. inversion X; subst; clear X. eexists; eapply verify_function_correct; simpl; eauto. -Qed. + Qed.*) Lemma transf_fundef_correct f f': transf_fundef f = OK f' -> match_fundef f f'. |