From c45548041d9f8849e4f7425cd4e71520d2d6341c Mon Sep 17 00:00:00 2001 From: xleroy Date: Thu, 26 Sep 2013 13:39:09 +0000 Subject: Do not use Format for faster printing of RTL, XTL, LTL, Mach git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2337 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/PrintLTL.ml | 58 ++++++++++++++++++++++----------------------- backend/PrintMach.ml | 46 ++++++++++++++++++------------------ backend/PrintRTL.ml | 66 +++++++++++++++++++++++++--------------------------- backend/PrintXTL.ml | 65 +++++++++++++++++++++++++-------------------------- backend/Regalloc.ml | 29 +++++++++++------------ 5 files changed, 128 insertions(+), 136 deletions(-) (limited to 'backend') diff --git a/backend/PrintLTL.ml b/backend/PrintLTL.ml index 702c213..52e5130 100644 --- a/backend/PrintLTL.ml +++ b/backend/PrintLTL.ml @@ -12,7 +12,7 @@ (** Pretty-printers for RTL code *) -open Format +open Printf open Camlcoq open Datatypes open Maps @@ -57,73 +57,72 @@ let ros pp = function | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) let print_succ pp s dfl = - let s = P.to_int32 s in - if s <> dfl then fprintf pp "goto %ld" s + let s = P.to_int s in + if s <> dfl then fprintf pp "goto %d" s let print_instruction pp succ = function | Lop(op, args, res) -> - fprintf pp "%a = %a;" mreg res (print_operation mreg) (op, args) + fprintf pp "%a = %a" mreg res (print_operation mreg) (op, args) | Lload(chunk, addr, args, dst) -> - fprintf pp "%a = %s[%a];" + fprintf pp "%a = %s[%a]" mreg dst (name_of_chunk chunk) (print_addressing mreg) (addr, args) | Lgetstack(sl, ofs, ty, dst) -> - fprintf pp "%a = %a;" mreg dst slot (sl, ofs, ty) + fprintf pp "%a = %a" mreg dst slot (sl, ofs, ty) | Lsetstack(src, sl, ofs, ty) -> - fprintf pp "%a = %a;" slot (sl, ofs, ty) mreg src + fprintf pp "%a = %a" slot (sl, ofs, ty) mreg src | Lstore(chunk, addr, args, src) -> - fprintf pp "%s[%a] = %a;" + fprintf pp "%s[%a] = %a" (name_of_chunk chunk) (print_addressing mreg) (addr, args) mreg src | Lcall(sg, fn) -> - fprintf pp "call %a;" ros fn + fprintf pp "call %a" ros fn | Ltailcall(sg, fn) -> - fprintf pp "tailcall %a;" ros fn + fprintf pp "tailcall %a" ros fn | Lbuiltin(ef, args, res) -> - fprintf pp "%a = builtin %s(%a);" + fprintf pp "%a = %s(%a)" mregs res (name_of_external ef) mregs args | Lannot(ef, args) -> - fprintf pp "builtin %s(%a);" + fprintf pp "%s(%a)" (name_of_external ef) locs args | Lbranch s -> print_succ pp s succ | Lcond(cond, args, s1, s2) -> - fprintf pp "if (%a) goto %ld else goto %ld" + fprintf pp "if (%a) goto %d else goto %d" (print_condition mreg) (cond, args) - (P.to_int32 s1) (P.to_int32 s2) + (P.to_int s1) (P.to_int s2) | Ljumptable(arg, tbl) -> let tbl = Array.of_list tbl in - fprintf pp "@[jumptable (%a)" mreg arg; + fprintf pp "jumptable (%a)" mreg arg; for i = 0 to Array.length tbl - 1 do - fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i)) - done; - fprintf pp "@]" + fprintf pp "\n\t\tcase %d: goto %d" i (P.to_int tbl.(i)) + done | Lreturn -> fprintf pp "return" let rec print_instructions pp succ = function | [] -> () - | [i] -> print_instruction pp succ i + | [i] -> print_instruction pp succ i | i :: il -> print_instruction pp succ i; - fprintf pp "@ "; + fprintf pp "; "; print_instructions pp succ il let print_block pp (pc, blk) = - fprintf pp "%5ld: @[" pc; - print_instructions pp (Int32.pred pc) blk; - fprintf pp "@]@ " + fprintf pp "%5d:\t" pc; + print_instructions pp (pc - 1) blk; + fprintf pp "\n" let print_function pp id f = - fprintf pp "@[%s() {@ " (extern_atom id); + fprintf pp "%s() {\n" (extern_atom id); let instrs = List.sort (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1) (List.rev_map - (fun (pc, i) -> (P.to_int32 pc, i)) + (fun (pc, i) -> (P.to_int pc, i)) (PTree.elements f.fn_code)) in - print_succ pp f.fn_entrypoint - (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l); + print_succ pp f.fn_entrypoint + (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1); List.iter (print_block pp) instrs; - fprintf pp "@;<0 -2>}@]@." + fprintf pp "}\n\n" let print_globdef pp (id, gd) = match gd with @@ -140,6 +139,5 @@ let print_if prog = | None -> () | Some f -> let oc = open_out f in - let pp = formatter_of_out_channel oc in - print_program pp prog; + print_program oc prog; close_out oc diff --git a/backend/PrintMach.ml b/backend/PrintMach.ml index e7cb947..b356ca9 100644 --- a/backend/PrintMach.ml +++ b/backend/PrintMach.ml @@ -12,7 +12,7 @@ (** Pretty-printer for Mach code *) -open Format +open Printf open Camlcoq open Datatypes open Maps @@ -50,57 +50,56 @@ let ros pp = function let print_instruction pp i = match i with | Mgetstack(ofs, ty, res) -> - fprintf pp "%a = stack(%ld, %s)@ " + fprintf pp "\t%a = stack(%ld, %s)\n" reg res (camlint_of_coqint ofs) (name_of_type ty) | Msetstack(arg, ofs, ty) -> - fprintf pp "stack(%ld, %s) = %a@ " + fprintf pp "\tstack(%ld, %s) = %a\n" (camlint_of_coqint ofs) (name_of_type ty) reg arg | Mgetparam(ofs, ty, res) -> - fprintf pp "%a = param(%ld, %s)@ " + fprintf pp "\t%a = param(%ld, %s)\n" reg res (camlint_of_coqint ofs) (name_of_type ty) | Mop(op, args, res) -> - fprintf pp "%a = %a@ " + fprintf pp "\t%a = %a\n" reg res (PrintOp.print_operation reg) (op, args) | Mload(chunk, addr, args, dst) -> - fprintf pp "%a = %s[%a]@ " + fprintf pp "\t%a = %s[%a]\n" reg dst (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) | Mstore(chunk, addr, args, src) -> - fprintf pp "%s[%a] = %a@ " + fprintf pp "\t%s[%a] = %a\n" (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) reg src | Mcall(sg, fn) -> - fprintf pp "call %a@ " ros fn + fprintf pp "\tcall %a\n" ros fn | Mtailcall(sg, fn) -> - fprintf pp "tailcall %a@ " ros fn + fprintf pp "\ttailcall %a\n" ros fn | Mbuiltin(ef, args, res) -> - fprintf pp "%a = builtin %s(%a)@ " + fprintf pp "\t%a = %s(%a)\n" regs res (name_of_external ef) regs args | Mannot(ef, args) -> - fprintf pp "%s(%a)@ " (name_of_external ef) annot_params args + fprintf pp "\t%s(%a)\n" (name_of_external ef) annot_params args | Mlabel lbl -> - fprintf pp "%ld:@ " (P.to_int32 lbl) + fprintf pp "%5d:" (P.to_int lbl) | Mgoto lbl -> - fprintf pp "goto %ld@ " (P.to_int32 lbl) + fprintf pp "\tgoto %d\n" (P.to_int lbl) | Mcond(cond, args, lbl) -> - fprintf pp "if (%a) goto %ld@ " + fprintf pp "\tif (%a) goto %d\n" (PrintOp.print_condition reg) (cond, args) - (P.to_int32 lbl) + (P.to_int lbl) | Mjumptable(arg, tbl) -> let tbl = Array.of_list tbl in - fprintf pp "@[jumptable (%a)" reg arg; + fprintf pp "\tjumptable (%a)\n" reg arg; for i = 0 to Array.length tbl - 1 do - fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i)) - done; - fprintf pp "@]@ " + fprintf pp "\t\tcase %d: goto %d\n" i (P.to_int tbl.(i)) + done | Mreturn -> - fprintf pp "return@ " + fprintf pp "\treturn\n" let print_function pp id f = - fprintf pp "@[%s() {@ " (extern_atom id); + fprintf pp "%s() {\n" (extern_atom id); List.iter (print_instruction pp) f.fn_code; - fprintf pp "@;<0 -2>}@]@." + fprintf pp "}\n\n" let print_globdef pp (id, gd) = match gd with @@ -117,6 +116,5 @@ let print_if prog = | None -> () | Some f -> let oc = open_out f in - let pp = formatter_of_out_channel oc in - print_program pp prog; + print_program oc prog; close_out oc diff --git a/backend/PrintRTL.ml b/backend/PrintRTL.ml index 0cdf505..429199e 100644 --- a/backend/PrintRTL.ml +++ b/backend/PrintRTL.ml @@ -12,7 +12,7 @@ (** Pretty-printers for RTL code *) -open Format +open Printf open Camlcoq open Datatypes open Maps @@ -25,7 +25,7 @@ open PrintOp (* Printing of RTL code *) let reg pp r = - fprintf pp "x%ld" (P.to_int32 r) + fprintf pp "x%d" (P.to_int r) let rec regs pp = function | [] -> () @@ -37,71 +37,70 @@ let ros pp = function | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) let print_succ pp s dfl = - let s = P.to_int32 s in - if s <> dfl then fprintf pp " goto %ld@ " s + let s = P.to_int s in + if s <> dfl then fprintf pp "\tgoto %d\n" s let print_instruction pp (pc, i) = - fprintf pp "%5ld: " pc; + fprintf pp "%5d:\t" pc; match i with | Inop s -> - let s = P.to_int32 s in - if s = Int32.pred pc - then fprintf pp "nop@ " - else fprintf pp "goto %ld@ " s + let s = P.to_int s in + if s = pc - 1 + then fprintf pp "nop\n" + else fprintf pp "goto %d\n" s | Iop(op, args, res, s) -> - fprintf pp "%a = %a@ " + fprintf pp "%a = %a\n" reg res (PrintOp.print_operation reg) (op, args); - print_succ pp s (Int32.pred pc) + print_succ pp s (pc - 1) | Iload(chunk, addr, args, dst, s) -> - fprintf pp "%a = %s[%a]@ " + fprintf pp "%a = %s[%a]\n" reg dst (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args); - print_succ pp s (Int32.pred pc) + print_succ pp s (pc - 1) | Istore(chunk, addr, args, src, s) -> - fprintf pp "%s[%a] = %a@ " + fprintf pp "%s[%a] = %a\n" (name_of_chunk chunk) (PrintOp.print_addressing reg) (addr, args) reg src; - print_succ pp s (Int32.pred pc) + print_succ pp s (pc - 1) | Icall(sg, fn, args, res, s) -> - fprintf pp "%a = %a(%a)@ " + fprintf pp "%a = %a(%a)\n" reg res ros fn regs args; - print_succ pp s (Int32.pred pc) + print_succ pp s (pc - 1) | Itailcall(sg, fn, args) -> - fprintf pp "tailcall %a(%a)@ " + fprintf pp "tailcall %a(%a)\n" ros fn regs args | Ibuiltin(ef, args, res, s) -> - fprintf pp "%a = builtin %s(%a)@ " + fprintf pp "%a = %s(%a)\n" reg res (name_of_external ef) regs args; - print_succ pp s (Int32.pred pc) + print_succ pp s (pc - 1) | Icond(cond, args, s1, s2) -> - fprintf pp "if (%a) goto %ld else goto %ld@ " + fprintf pp "if (%a) goto %d else goto %d\n" (PrintOp.print_condition reg) (cond, args) - (P.to_int32 s1) (P.to_int32 s2) + (P.to_int s1) (P.to_int s2) | Ijumptable(arg, tbl) -> let tbl = Array.of_list tbl in - fprintf pp "@[jumptable (%a)" reg arg; + fprintf pp "jumptable (%a)\n" reg arg; for i = 0 to Array.length tbl - 1 do - fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i)) - done; - fprintf pp "@]@ " + fprintf pp "\t\tcase %d: goto %d\n" i (P.to_int tbl.(i)) + done | Ireturn None -> - fprintf pp "return@ " + fprintf pp "return\n" | Ireturn (Some arg) -> - fprintf pp "return %a@ " reg arg + fprintf pp "return %a\n" reg arg let print_function pp id f = - fprintf pp "@[%s(%a) {@ " (extern_atom id) regs f.fn_params; + fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params; let instrs = List.sort (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1) (List.rev_map - (fun (pc, i) -> (P.to_int32 pc, i)) + (fun (pc, i) -> (P.to_int pc, i)) (PTree.elements f.fn_code)) in print_succ pp f.fn_entrypoint - (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l); + (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1); List.iter (print_instruction pp) instrs; - fprintf pp "@;<0 -2>}@]@." + fprintf pp "}\n\n" let print_globdef pp (id, gd) = match gd with @@ -116,8 +115,7 @@ let print_if optdest prog = | None -> () | Some f -> let oc = open_out f in - let pp = formatter_of_out_channel oc in - print_program pp prog; + print_program oc prog; close_out oc let destination_rtl : string option ref = ref None diff --git a/backend/PrintXTL.ml b/backend/PrintXTL.ml index 258baba..ff45809 100644 --- a/backend/PrintXTL.ml +++ b/backend/PrintXTL.ml @@ -12,7 +12,7 @@ (** Pretty-printer for XTL *) -open Format +open Printf open Camlcoq open Datatypes open Maps @@ -49,8 +49,8 @@ let current_liveness = ref (None: VSet.t PMap.t option) let reg pp r ty = match !current_alloc with - | None -> fprintf pp "x%ld" (P.to_int32 r) - | Some alloc -> fprintf pp "x%ld{%a}" (P.to_int32 r) loc (alloc (V(r, ty))) + | None -> fprintf pp "x%d" (P.to_int r) + | Some alloc -> fprintf pp "x%d{%a}" (P.to_int r) loc (alloc (V(r, ty))) let var pp = function | V(r, ty) -> reg pp r ty @@ -66,53 +66,52 @@ let ros pp = function | Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s) let liveset pp lv = - fprintf pp "@[{"; - VSet.iter (function V(r, ty) -> fprintf pp "@ x%ld" (P.to_int32 r) + fprintf pp "{"; + VSet.iter (function V(r, ty) -> fprintf pp " x%d" (P.to_int r) | L l -> ()) lv; - fprintf pp " }@]" + fprintf pp " }" let print_succ pp s dfl = - let s = P.to_int32 s in - if s <> dfl then fprintf pp "goto %ld" s + let s = P.to_int s in + if s <> dfl then fprintf pp "goto %d" s let print_instruction pp succ = function | Xmove(src, dst) -> - fprintf pp "%a = %a;" var dst var src + fprintf pp "%a = %a" var dst var src | Xreload(src, dst) -> - fprintf pp "%a =r %a;" var dst var src + fprintf pp "%a =r %a" var dst var src | Xspill(src, dst) -> - fprintf pp "%a =s %a;" var dst var src + fprintf pp "%a =s %a" var dst var src | Xparmove(srcs, dsts, t1, t2) -> - fprintf pp "(%a) = (%a) using %a, %a;" vars dsts vars srcs var t1 var t2 + fprintf pp "(%a) = (%a) using %a, %a" vars dsts vars srcs var t1 var t2 | Xop(op, args, res) -> - fprintf pp "%a = %a;" var res (print_operation var) (op, args) + fprintf pp "%a = %a" var res (print_operation var) (op, args) | Xload(chunk, addr, args, dst) -> - fprintf pp "%a = %s[%a];" + fprintf pp "%a = %s[%a]" var dst (name_of_chunk chunk) (print_addressing var) (addr, args) | Xstore(chunk, addr, args, src) -> - fprintf pp "%s[%a] = %a;" + fprintf pp "%s[%a] = %a" (name_of_chunk chunk) (print_addressing var) (addr, args) var src | Xcall(sg, fn, args, res) -> - fprintf pp "%a = call %a(%a);" vars res ros fn vars args + fprintf pp "%a = call %a(%a)" vars res ros fn vars args | Xtailcall(sg, fn, args) -> - fprintf pp "tailcall %a(%a);" ros fn vars args + fprintf pp "tailcall %a(%a)" ros fn vars args | Xbuiltin(ef, args, res) -> - fprintf pp "%a = builtin %s(%a);" + fprintf pp "%a = %s(%a)" vars res (name_of_external ef) vars args | Xbranch s -> print_succ pp s succ | Xcond(cond, args, s1, s2) -> - fprintf pp "if (%a) goto %ld else goto %ld" + fprintf pp "if (%a) goto %d else goto %d" (print_condition var) (cond, args) - (P.to_int32 s1) (P.to_int32 s2) + (P.to_int s1) (P.to_int s2) | Xjumptable(arg, tbl) -> let tbl = Array.of_list tbl in - fprintf pp "@[jumptable (%a)" var arg; + fprintf pp "jumptable (%a)" var arg; for i = 0 to Array.length tbl - 1 do - fprintf pp "@ case %d: goto %ld" i (P.to_int32 tbl.(i)) - done; - fprintf pp "@]" + fprintf pp "\n\t\tcase %d: goto %d" i (P.to_int tbl.(i)) + done | Xreturn args -> fprintf pp "return %a" vars args @@ -121,31 +120,31 @@ let rec print_instructions pp succ = function | [i] -> print_instruction pp succ i | i :: il -> print_instruction pp succ i; - fprintf pp "@ "; + fprintf pp "; "; print_instructions pp succ il let print_block pp (pc, blk) = - fprintf pp "%5ld: @[" pc; - print_instructions pp (Int32.pred pc) blk; - fprintf pp "@]@ "; + fprintf pp "%5d:\t" pc; + print_instructions pp (pc - 1) blk; + fprintf pp "\n"; match !current_liveness with | None -> () - | Some liveness -> fprintf pp "%a@ " liveset (PMap.get (P.of_int32 pc) liveness) + | Some liveness -> fprintf pp "%a\n" liveset (PMap.get (P.of_int pc) liveness) let print_function pp ?alloc ?live f = current_alloc := alloc; current_liveness := live; - fprintf pp "@[f() {@ "; + fprintf pp "f() {\n"; let instrs = List.sort (fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1) (List.map - (fun (pc, i) -> (P.to_int32 pc, i)) + (fun (pc, i) -> (P.to_int pc, i)) (PTree.elements f.fn_code)) in print_succ pp f.fn_entrypoint - (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1l); + (match instrs with (pc1, _) :: _ -> pc1 | [] -> -1); List.iter (print_block pp) instrs; - fprintf pp "@;<0 -2>}@]@."; + fprintf pp "}\n\n"; current_alloc := None; current_liveness := None diff --git a/backend/Regalloc.ml b/backend/Regalloc.ml index 3c56b43..8a3c05e 100644 --- a/backend/Regalloc.ml +++ b/backend/Regalloc.ml @@ -26,7 +26,7 @@ End Repeat *) -open Format +open Printf open Clflags open Camlcoq open Datatypes @@ -56,13 +56,13 @@ let is_two_address op args = (* For tracing *) let destination_alloctrace : string option ref = ref None -let pp = ref std_formatter +let pp = ref stdout let init_trace () = - if !option_dalloctrace && !pp == std_formatter then begin + if !option_dalloctrace && !pp == stdout then begin match !destination_alloctrace with | None -> () (* should not happen *) - | Some f -> pp := formatter_of_out_channel (open_out f) + | Some f -> pp := open_out f end @@ -428,13 +428,12 @@ let spill_costs f = (fun () blk -> charge_block blk) f.fn_code (); if !option_dalloctrace then begin - fprintf !pp "------------------ Unspillable variables --------------@ @."; - fprintf !pp "@["; + fprintf !pp "------------------ Unspillable variables --------------\n\n"; PTree.fold (fun () r st -> - if st.cost = max_int then fprintf !pp "@ x%ld" (P.to_int32 r)) + if st.cost = max_int then fprintf !pp "x%d " (P.to_int r)) !costs (); - fprintf !pp "@]@ @." + fprintf !pp "\n\n" end; (* Result is cost function: pseudoreg -> stats *) get_stats @@ -938,7 +937,7 @@ exception Timeout let rec first_round f liveness = let alloc = find_coloring f liveness in if !option_dalloctrace then begin - fprintf !pp "-------------- After initial register allocation@ @."; + fprintf !pp "-------------- After initial register allocation\n\n"; PrintXTL.print_function !pp ~alloc: alloc ~live: liveness f end; let ts = tospill_function f alloc in @@ -950,7 +949,7 @@ and more_rounds f ts count = let liveness = liveness_analysis f' in let alloc = find_coloring f' liveness in if !option_dalloctrace then begin - fprintf !pp "-------------- After register allocation (round %d)@ @." count; + fprintf !pp "-------------- After register allocation (round %d)\n\n" count; PrintXTL.print_function !pp ~alloc: alloc ~live: liveness f' end; let ts' = tospill_function f' alloc in @@ -958,9 +957,9 @@ and more_rounds f ts count = then success f' alloc else begin if !option_dalloctrace then begin - fprintf !pp "--- Remain to be spilled:@ @."; + fprintf !pp "--- Remain to be spilled:\n"; VSet.iter (fun v -> fprintf !pp "%a " PrintXTL.var v) ts'; - fprintf !pp "@ @." + fprintf !pp "\n\n" end; more_rounds f (VSet.union ts ts') (count + 1) end @@ -968,7 +967,7 @@ and more_rounds f ts count = and success f alloc = let f' = transl_function f alloc in if !option_dalloctrace then begin - fprintf !pp "-------------- Candidate allocation@ @."; + fprintf !pp "-------------- Candidate allocation\n\n"; PrintLTL.print_function !pp P.one f' end; f' @@ -987,12 +986,12 @@ let regalloc f = let liveness = liveness_analysis f2 in let f3 = dead_code_elimination f2 liveness in if !option_dalloctrace then begin - fprintf !pp "-------------- Initial XTL@ @."; + fprintf !pp "-------------- Initial XTL\n\n"; PrintXTL.print_function !pp f3 end; try OK(first_round f3 liveness) - with + with | Timeout -> Error(msg (coqstring_of_camlstring "Spilling fails to converge")) | Type_error_at pc -> -- cgit v1.2.3