diff options
Diffstat (limited to 'scheduling/PrintBTL.ml')
| -rw-r--r-- | scheduling/PrintBTL.ml | 118 |
1 files changed, 118 insertions, 0 deletions
diff --git a/scheduling/PrintBTL.ml b/scheduling/PrintBTL.ml new file mode 100644 index 00000000..89254301 --- /dev/null +++ b/scheduling/PrintBTL.ml @@ -0,0 +1,118 @@ +open Printf +open Camlcoq +open Datatypes +open Maps +open BTL +open PrintAST +open DebugPrint +open BTLtypes + +(* Printing of BTL code *) + +let reg pp r = fprintf pp "x%d" (P.to_int r) + +let rec regs pp = function + | [] -> () + | [ r ] -> reg pp r + | r1 :: rl -> fprintf pp "%a, %a" reg r1 regs rl + +let ros pp = function + | Coq_inl r -> reg pp r + | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) + +let print_succ pp s = fprintf pp "\tsucc %d\n" (P.to_int s) + +let print_pref pp pref = fprintf pp "%s" pref + +let rec print_iblock pp is_rec pref ib = + match ib with + | Bnop None -> + print_pref pp pref; + fprintf pp "??: Bnop None\n" + | Bnop (Some iinfo) -> + print_pref pp pref; + 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, iinfo) -> + print_pref pp pref; + 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, iinfo) -> + print_pref pp pref; + 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), iinfo) -> + print_pref pp pref; + 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), iinfo) -> + print_pref pp pref; + 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 "%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 "%d: Bcond: (%a) (prediction: %s)\n" iinfo.inumb + (PrintOp.print_condition reg) + (cond, args) + (match iinfo.pcond with + | None -> "none" + | Some true -> "branch" + | Some false -> "fallthrough"); + let pref' = pref ^ " " in + fprintf pp "%sifso = [\n" pref; + if is_rec then print_iblock pp is_rec pref' ib1 else fprintf pp "...\n"; + fprintf pp "%s]\n" pref; + 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), iinfo) -> + let tbl = Array.of_list tbl in + print_pref pp pref; + 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, iinfo) -> + print_pref pp pref; + fprintf pp "%d: Breturn\n" iinfo.inumb + | BF (Breturn (Some arg), iinfo) -> + print_pref pp pref; + fprintf pp "%d: Breturn: %a\n" iinfo.inumb reg arg + | BF (Bgoto s, iinfo) -> + print_pref pp pref; + 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 = + if !debug_flag then print_iblock pp false " " ib else () + +let print_btl_code pp btl = + if !debug_flag then ( + fprintf pp "\n"; + List.iter + (fun (n, ibf) -> + fprintf pp "[BTL Liveness] "; + print_regset ibf.input_regs; + 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") + else () |