From 25eb1fd3c9d997e460dff3e03d87e398e616c726 Mon Sep 17 00:00:00 2001 From: Graydon Hoare Date: Thu, 24 Jun 2010 10:34:47 -0700 Subject: [PATCH] Add fmt module, move out some common format helpers, add instruction-selection tracing and make selection use queues rather than list refs. --- src/Makefile | 2 +- src/boot/be/asm.ml | 77 ++++++++++++++++++++++++++++++++++- src/boot/be/il.ml | 45 +++----------------- src/boot/be/x86.ml | 88 +++++++++++++++++++++++++--------------- src/boot/driver/main.ml | 4 +- src/boot/fe/ast.ml | 26 +----------- src/boot/fe/pexp.ml | 2 +- src/boot/llvm/lltrans.ml | 2 +- src/boot/me/dwarf.ml | 26 ++++++------ src/boot/me/resolve.ml | 6 +-- src/boot/me/semant.ml | 2 +- src/boot/me/trans.ml | 28 ++++++------- src/boot/me/typestate.ml | 16 ++++---- src/boot/me/walk.ml | 2 +- src/boot/util/fmt.ml | 83 +++++++++++++++++++++++++++++++++++++ 15 files changed, 266 insertions(+), 143 deletions(-) create mode 100644 src/boot/util/fmt.ml diff --git a/src/Makefile b/src/Makefile index bc187567039..c2064a1e554 100644 --- a/src/Makefile +++ b/src/Makefile @@ -205,7 +205,7 @@ endif # List them in link order. # Nobody calculates the link-order DAG automatically, sadly. -UTIL_BOT_MLS := $(addprefix boot/util/, common.ml bits.ml) +UTIL_BOT_MLS := $(addprefix boot/util/, fmt.ml common.ml bits.ml) DRIVER_BOT_MLS := $(addprefix boot/driver/, session.ml) BE_MLS := $(addprefix boot/be/, x86.ml ra.ml pe.ml elf.ml \ macho.ml) diff --git a/src/boot/be/asm.ml b/src/boot/be/asm.ml index 10b2142aad6..4b05e347ea6 100644 --- a/src/boot/be/asm.ml +++ b/src/boot/be/asm.ml @@ -62,7 +62,7 @@ *) open Common;; - +open Fmt;; let log (sess:Session.sess) = Session.log "asm" @@ -201,6 +201,41 @@ let rec eval64 (e:expr64) | EXT e -> Int64.of_int32 (eval32 e) ;; +let rec string_of_expr64 (e64:expr64) : string = + let bin op a b = + Printf.sprintf "(%s %s %s)" (string_of_expr64 a) op (string_of_expr64 b) + in + let bini op a b = + Printf.sprintf "(%s %s %d)" (string_of_expr64 a) op b + in + match e64 with + IMM i when (i64_lt i 0L) -> Printf.sprintf "-0x%Lx" (Int64.neg i) + | IMM i -> Printf.sprintf "0x%Lx" i + | ADD (a,b) -> bin "+" a b + | SUB (a,b) -> bin "-" a b + | MUL (a,b) -> bin "*" a b + | DIV (a,b) -> bin "/" a b + | REM (a,b) -> bin "%" a b + | MAX (a,b) -> + Printf.sprintf "(max %s %s)" + (string_of_expr64 a) (string_of_expr64 b) + | ALIGN (a,b) -> + Printf.sprintf "(align %s %s)" + (string_of_expr64 a) (string_of_expr64 b) + | SLL (a,b) -> bini "<<" a b + | SLR (a,b) -> bini ">>" a b + | SAR (a,b) -> bini ">>>" a b + | AND (a,b) -> bin "&" a b + | XOR (a,b) -> bin "xor" a b + | OR (a,b) -> bin "|" a b + | NOT a -> Printf.sprintf "(not %s)" (string_of_expr64 a) + | NEG a -> Printf.sprintf "-%s" (string_of_expr64 a) + | F_POS f -> Printf.sprintf "<%s>.fpos" f.fixup_name + | F_SZ f -> Printf.sprintf "<%s>.fsz" f.fixup_name + | M_POS f -> Printf.sprintf "<%s>.mpos" f.fixup_name + | M_SZ f -> Printf.sprintf "<%s>.msz" f.fixup_name + | EXT _ -> "??ext??" +;; type frag = MARK (* MARK == 'PAD (IMM 0L)' *) @@ -226,6 +261,46 @@ and relaxation = relax_choice: int ref; } ;; + +let rec fmt_frag (ff:Format.formatter) (f:frag) : unit = + match f with + MARK -> fmt ff "MARK" + | SEQ fs -> fmt_bracketed_arr_sep "[" "]" ", " fmt_frag ff fs + | PAD i -> fmt ff "PAD(%d)" i + | BSS i -> fmt ff "BSZ(%Ld)" i + | MEMPOS i -> fmt ff "MEMPOS(%Ld)" i + | BYTE i -> fmt ff "0x%x" i + | BYTES iz -> + fmt ff "BYTES"; + fmt_bracketed_arr_sep "(" ")" ", " + (fun ff i -> fmt ff "0x%x" i) ff iz + | CHAR c -> fmt ff "CHAR(%s)" (Char.escaped c) + | STRING s -> fmt ff "STRING(%s)" (String.escaped s) + | ZSTRING s -> fmt ff "ZSTRING(%s)" (String.escaped s) + | ULEB128 e -> fmt ff "ULEB128(%s)" (string_of_expr64 e) + | SLEB128 e -> fmt ff "SLEB128(%s)" (string_of_expr64 e) + | WORD (tm, e) -> + fmt ff "%s:%s" + (string_of_ty_mach tm) (string_of_expr64 e) + | ALIGN_FILE (i, f) -> + fmt ff "ALIGN_FILE(%d, " i; + fmt_frag ff f; + fmt ff ")" + | ALIGN_MEM (i, f) -> + fmt ff "ALIGN_MEM(%d, " i; + fmt_frag ff f; + fmt ff ")" + | DEF (fix, f) -> + fmt ff "DEF(%s, " fix.fixup_name; + fmt_frag ff f; + fmt ff ")" + | RELAX r -> + fmt ff "RELAX("; + fmt_arr_sep ", " fmt_frag ff r.relax_options +;; + +let sprintf_frag = Fmt.sprintf_fmt fmt_frag;; + exception Relax_more of relaxation;; let new_relaxation (frags:frag array) = diff --git a/src/boot/be/il.ml b/src/boot/be/il.ml index e095e627b71..b77516b74dc 100644 --- a/src/boot/be/il.ml +++ b/src/boot/be/il.ml @@ -522,54 +522,18 @@ let string_of_reg (f:hreg_formatter) (r:reg) : string = | Hreg i -> f i ;; -let rec string_of_expr64 (e64:Asm.expr64) : string = - let bin op a b = - Printf.sprintf "(%s %s %s)" (string_of_expr64 a) op (string_of_expr64 b) - in - let bini op a b = - Printf.sprintf "(%s %s %d)" (string_of_expr64 a) op b - in - match e64 with - Asm.IMM i when (i64_lt i 0L) -> Printf.sprintf "-0x%Lx" (Int64.neg i) - | Asm.IMM i -> Printf.sprintf "0x%Lx" i - | Asm.ADD (a,b) -> bin "+" a b - | Asm.SUB (a,b) -> bin "-" a b - | Asm.MUL (a,b) -> bin "*" a b - | Asm.DIV (a,b) -> bin "/" a b - | Asm.REM (a,b) -> bin "%" a b - | Asm.MAX (a,b) -> - Printf.sprintf "(max %s %s)" - (string_of_expr64 a) (string_of_expr64 b) - | Asm.ALIGN (a,b) -> - Printf.sprintf "(align %s %s)" - (string_of_expr64 a) (string_of_expr64 b) - | Asm.SLL (a,b) -> bini "<<" a b - | Asm.SLR (a,b) -> bini ">>" a b - | Asm.SAR (a,b) -> bini ">>>" a b - | Asm.AND (a,b) -> bin "&" a b - | Asm.XOR (a,b) -> bin "xor" a b - | Asm.OR (a,b) -> bin "|" a b - | Asm.NOT a -> Printf.sprintf "(not %s)" (string_of_expr64 a) - | Asm.NEG a -> Printf.sprintf "-%s" (string_of_expr64 a) - | Asm.F_POS f -> Printf.sprintf "<%s>.fpos" f.fixup_name - | Asm.F_SZ f -> Printf.sprintf "<%s>.fsz" f.fixup_name - | Asm.M_POS f -> Printf.sprintf "<%s>.mpos" f.fixup_name - | Asm.M_SZ f -> Printf.sprintf "<%s>.msz" f.fixup_name - | Asm.EXT _ -> "??ext??" -;; - let string_of_off (e:Asm.expr64 option) : string = match e with None -> "" | Some (Asm.IMM i) when (i64_lt i 0L) -> Printf.sprintf " - 0x%Lx" (Int64.neg i) - | Some e' -> " + " ^ (string_of_expr64 e') + | Some e' -> " + " ^ (Asm.string_of_expr64 e') ;; let string_of_mem (f:hreg_formatter) (a:mem) : string = match a with Abs e -> - Printf.sprintf "[%s]" (string_of_expr64 e) + Printf.sprintf "[%s]" (Asm.string_of_expr64 e) | RegIn (r, off) -> Printf.sprintf "[%s%s]" (string_of_reg f r) (string_of_off off) | Spill i -> @@ -605,9 +569,10 @@ let string_of_operand (f:hreg_formatter) (op:operand) : string = | Imm (i, ty) -> if !log_iltypes then - Printf.sprintf "$%s:%s" (string_of_expr64 i) (string_of_ty_mach ty) + Printf.sprintf "$%s:%s" + (Asm.string_of_expr64 i) (string_of_ty_mach ty) else - Printf.sprintf "$%s" (string_of_expr64 i) + Printf.sprintf "$%s" (Asm.string_of_expr64 i) ;; diff --git a/src/boot/be/x86.ml b/src/boot/be/x86.ml index 01b7e29970d..a1770d06d1a 100644 --- a/src/boot/be/x86.ml +++ b/src/boot/be/x86.ml @@ -73,6 +73,19 @@ * *) + +let log (sess:Session.sess) = + Session.log "insn" + sess.Session.sess_log_insn + sess.Session.sess_log_out +;; + +let iflog (sess:Session.sess) (thunk:(unit -> unit)) : unit = + if sess.Session.sess_log_insn + then thunk () + else () +;; + open Common;; exception Unrecognized @@ -2147,44 +2160,55 @@ let new_emitter_without_vregs _ : Il.emitter = false None ;; -let select_insns (sess:Session.sess) (q:Il.quads) : Asm.frag = +let select_insns (sess:Session.sess) (qs:Il.quads) : Asm.frag = let scopes = Stack.create () in let fixups = Stack.create () in - let pop_frags _ = - Asm.SEQ (Array.of_list - (List.rev - (!(Stack.pop scopes)))) + let append frag = + Queue.add frag (Stack.top scopes) in - ignore (Stack.push (ref []) scopes); - for i = 0 to (Array.length q) - 1 do - let append frag = - let frags = Stack.top scopes in - frags := frag :: (!frags) - in - begin - match q.(i).Il.quad_fixup with - None -> () - | Some f -> append (Asm.DEF (f, Asm.MARK)) - end; - begin - match q.(i).Il.quad_body with - Il.Enter f -> - Stack.push f fixups; - Stack.push (ref []) scopes; - | Il.Leave -> - append (Asm.DEF (Stack.pop fixups, pop_frags ())) - | _ -> - try - append (select_insn q.(i)) - with + let pop_frags _ = + Asm.SEQ (queue_to_arr (Stack.pop scopes)) + in + ignore (Stack.push (Queue.create()) scopes); + Array.iteri + begin + fun i q -> + begin + match q.Il.quad_fixup with + None -> () + | Some f -> append (Asm.DEF (f, Asm.MARK)) + end; + begin + let qstr _ = Il.string_of_quad reg_str q in + match q.Il.quad_body with + Il.Enter f -> + Stack.push f fixups; + Stack.push (Queue.create()) scopes; + | Il.Leave -> + append (Asm.DEF (Stack.pop fixups, pop_frags ())) + | _ -> + try + let _ = + iflog sess (fun _ -> + log sess "quad %d: %s" i (qstr())) + in + let frag = select_insn q in + let _ = + iflog sess (fun _ -> + log sess "frag %d: %a" i + Asm.sprintf_frag frag) + in + append frag + with Unrecognized -> Session.fail sess - "E:Assembly error: unrecognized quad: %s\n%!" - (Il.string_of_quad reg_str q.(i)); + "E:Assembly error: unrecognized quad %d: %s\n%!" + i (qstr()); () - end - done; - pop_frags() + end + end + qs; + pop_frags() ;; let frags_of_emitted_quads (sess:Session.sess) (e:Il.emitter) : Asm.frag = diff --git a/src/boot/driver/main.ml b/src/boot/driver/main.ml index c5199a82681..1841659095f 100644 --- a/src/boot/driver/main.ml +++ b/src/boot/driver/main.ml @@ -90,7 +90,7 @@ let set_default_output_filename (sess:Session.sess) : unit = let dump_sig (filename:filename) : unit = let items = Lib.get_file_mod sess abi filename (ref (Node 0)) (ref (Opaque 0)) in - Printf.fprintf stdout "%s\n" (Ast.fmt_to_str Ast.fmt_mod_items items); + Printf.fprintf stdout "%s\n" (Fmt.fmt_to_str Ast.fmt_mod_items items); exit 0 ;; @@ -289,7 +289,7 @@ then begin Printf.fprintf stdout "Post-parse AST:\n"; Format.set_margin 80; - Printf.fprintf stdout "%s\n" (Ast.fmt_to_str Ast.fmt_crate crate) + Printf.fprintf stdout "%s\n" (Fmt.fmt_to_str Ast.fmt_crate crate) end let list_to_seq ls = Asm.SEQ (Array.of_list ls);; diff --git a/src/boot/fe/ast.ml b/src/boot/fe/ast.ml index 438d9de9052..0903751066c 100644 --- a/src/boot/fe/ast.ml +++ b/src/boot/fe/ast.ml @@ -7,6 +7,7 @@ *) open Common;; +open Fmt;; (* * Slot names are given by a dot-separated path within the current @@ -464,8 +465,6 @@ let sane_name (n:name) : bool = (* FIXME (issue #19): finish all parts with ?foo? as their output. *) -let fmt = Format.fprintf;; - let fmt_ident (ff:Format.formatter) (i:ident) : unit = fmt ff "%s" i @@ -700,13 +699,6 @@ and fmt_carg (ff:Format.formatter) (ca:carg) : unit = CARG_path cp -> fmt_carg_path ff cp | CARG_lit lit -> fmt_lit ff lit -and fmt_obox ff = Format.pp_open_box ff 4 -and fmt_obox_3 ff = Format.pp_open_box ff 3 -and fmt_cbox ff = Format.pp_close_box ff () -and fmt_obr ff = fmt ff "{" -and fmt_cbr ff = fmt ff "@\n}" -and fmt_cbb ff = (fmt_cbox ff; fmt_cbr ff) - and fmt_stmts (ff:Format.formatter) (ss:stmt array) : unit = Array.iter (fmt_stmt ff) ss; @@ -1316,22 +1308,6 @@ and fmt_crate (ff:Format.formatter) (c:crate) : unit = fmt_mod_view ff view; fmt_mod_items ff items - -let fmt_to_str (f:Format.formatter -> 'a -> unit) (v:'a) : string = - let buf = Buffer.create 16 in - let bf = Format.formatter_of_buffer buf in - begin - f bf v; - Format.pp_print_flush bf (); - Buffer.contents buf - end - -let sprintf_fmt - (f:Format.formatter -> 'a -> unit) - : (unit -> 'a -> string) = - (fun _ -> fmt_to_str f) - - let sprintf_expr = sprintf_fmt fmt_expr;; let sprintf_name = sprintf_fmt fmt_name;; let sprintf_lval = sprintf_fmt fmt_lval;; diff --git a/src/boot/fe/pexp.ml b/src/boot/fe/pexp.ml index 49eeeb5b648..13d6d2b593d 100644 --- a/src/boot/fe/pexp.ml +++ b/src/boot/fe/pexp.ml @@ -975,7 +975,7 @@ let expand_pexp_custom (args:token array) (body:string option) : pexp' = - let nstr = Ast.fmt_to_str Ast.fmt_name name in + let nstr = Fmt.fmt_to_str Ast.fmt_name name in match (nstr, (Array.length args), body) with ("shell", 0, Some cmd) -> diff --git a/src/boot/llvm/lltrans.ml b/src/boot/llvm/lltrans.ml index 7f985d25927..a3278fcda70 100644 --- a/src/boot/llvm/lltrans.ml +++ b/src/boot/llvm/lltrans.ml @@ -831,7 +831,7 @@ let trans_crate | Ast.STMT_check_expr expr -> let llexpr = trans_expr expr in let (llfail, llfailbuilder) = new_block None "fail" in - let reason = Ast.fmt_to_str Ast.fmt_expr expr in + let reason = Fmt.fmt_to_str Ast.fmt_expr expr in trans_fail llfailbuilder lltask reason head.id; let (llok, llokbuilder) = new_block None "ok" in ignore (Llvm.build_cond_br llexpr llok llfail llbuilder); diff --git a/src/boot/me/dwarf.ml b/src/boot/me/dwarf.ml index 9423d4ee7f3..56b66f70811 100644 --- a/src/boot/me/dwarf.ml +++ b/src/boot/me/dwarf.ml @@ -1428,7 +1428,7 @@ let dwarf_visitor | Il.Bits64 -> TY_i64 in - let path_name _ = Ast.fmt_to_str Ast.fmt_name (Walk.path_to_name path) in + let path_name _ = Fmt.fmt_to_str Ast.fmt_name (Walk.path_to_name path) in let (abbrev_table:(abbrev, int) Hashtbl.t) = Hashtbl.create 0 in @@ -2496,29 +2496,29 @@ let fmt_dies : unit = let ((root:int),(dies:(int,die) Hashtbl.t)) = dies in let rec fmt_die die = - Ast.fmt ff "@\nDIE <0x%x> %s" die.die_off (dw_tag_to_string die.die_tag); + Fmt.fmt ff "@\nDIE <0x%x> %s" die.die_off (dw_tag_to_string die.die_tag); Array.iter begin fun (at,(form,data)) -> - Ast.fmt ff "@\n %s = " (dw_at_to_string at); + Fmt.fmt ff "@\n %s = " (dw_at_to_string at); begin match data with - DATA_num n -> Ast.fmt ff "0x%x" n - | DATA_str s -> Ast.fmt ff "\"%s\"" s - | DATA_other -> Ast.fmt ff "" + DATA_num n -> Fmt.fmt ff "0x%x" n + | DATA_str s -> Fmt.fmt ff "\"%s\"" s + | DATA_other -> Fmt.fmt ff "" end; - Ast.fmt ff " (%s)" (dw_form_to_string form) + Fmt.fmt ff " (%s)" (dw_form_to_string form) end die.die_attrs; if (Array.length die.die_children) != 0 then begin - Ast.fmt ff "@\n"; - Ast.fmt_obox ff; - Ast.fmt ff " children: "; - Ast.fmt_obr ff; + Fmt.fmt ff "@\n"; + Fmt.fmt_obox ff; + Fmt.fmt ff " children: "; + Fmt.fmt_obr ff; Array.iter fmt_die die.die_children; - Ast.fmt_cbb ff + Fmt.fmt_cbb ff end; in fmt_die (Hashtbl.find dies root) @@ -2613,7 +2613,7 @@ let read_dies begin fun _ -> log sess "read DIEs:"; - log sess "%s" (Ast.fmt_to_str fmt_dies (root, all_dies)); + log sess "%s" (Fmt.fmt_to_str fmt_dies (root, all_dies)); end; (root, all_dies) ;; diff --git a/src/boot/me/resolve.ml b/src/boot/me/resolve.ml index bfbac10d407..2c718778197 100644 --- a/src/boot/me/resolve.ml +++ b/src/boot/me/resolve.ml @@ -445,9 +445,9 @@ and lookup_type_by_name log cx "applying %d type args to %d params" (Array.length args) (Array.length params); log cx "params: %s" - (Ast.fmt_to_str Ast.fmt_decl_params params); + (Fmt.fmt_to_str Ast.fmt_decl_params params); log cx "args: %s" - (Ast.fmt_to_str Ast.fmt_app_args args); + (Fmt.fmt_to_str Ast.fmt_app_args args); end; let ty = rebuild_ty_under_params ty params args true in iflog cx (fun _ -> log cx "--- lookup_type_by_name %a ==> %a" @@ -538,7 +538,7 @@ let type_resolving_visitor log cx "collected resolved slot #%d with type %s" (int_of_node slot.id) (match slot.node.Ast.slot_ty with None -> "??" - | Some t -> (Ast.fmt_to_str Ast.fmt_ty t)); + | Some t -> (Fmt.fmt_to_str Ast.fmt_ty t)); inner.Walk.visit_slot_identified_pre slot in diff --git a/src/boot/me/semant.ml b/src/boot/me/semant.ml index f7acccfb885..d33eb6d9020 100644 --- a/src/boot/me/semant.ml +++ b/src/boot/me/semant.ml @@ -65,7 +65,7 @@ type file_code = (node_id, item_code) Hashtbl.t;; type data_frags = (data, (fixup * Asm.frag)) Hashtbl.t;; let string_of_name (n:Ast.name) : string = - Ast.fmt_to_str Ast.fmt_name n + Fmt.fmt_to_str Ast.fmt_name n ;; (* The only need for a carg is to uniquely identify a constraint-arg diff --git a/src/boot/me/trans.ml b/src/boot/me/trans.ml index a7ff502c31f..7cb77e0cec5 100644 --- a/src/boot/me/trans.ml +++ b/src/boot/me/trans.ml @@ -812,7 +812,7 @@ let trans_visitor (Printf.sprintf "access outer frame slot #%d = %s" (int_of_node slot_id) - (Ast.fmt_to_str + (Fmt.fmt_to_str Ast.fmt_slot_key k)) end in @@ -1214,7 +1214,7 @@ let trans_visitor iflog begin fun _ -> - annotate (Ast.fmt_to_str Ast.fmt_atom atom) + annotate (Fmt.fmt_to_str Ast.fmt_atom atom) end; match atom with @@ -1788,7 +1788,7 @@ let trans_visitor iflog begin fun _ -> - annotate ((Ast.fmt_to_str Ast.fmt_expr expr) ^ + annotate ((Fmt.fmt_to_str Ast.fmt_expr expr) ^ ": cond, finale") end in @@ -1875,7 +1875,7 @@ let trans_visitor iflog begin fun _ -> - annotate ((Ast.fmt_to_str Ast.fmt_expr expr) ^ + annotate ((Fmt.fmt_to_str Ast.fmt_expr expr) ^ ": plain exit, finale") end in @@ -2037,7 +2037,7 @@ let trans_visitor and trans_check_expr (e:Ast.expr) : unit = let fwd_jmps = trans_cond false e in - trans_cond_fail (Ast.fmt_to_str Ast.fmt_expr e) fwd_jmps + trans_cond_fail (Fmt.fmt_to_str Ast.fmt_expr e) fwd_jmps and trans_malloc (dst:Il.cell) (nbytes:Il.operand) : unit = trans_upcall "upcall_malloc" dst [| nbytes |] @@ -2489,7 +2489,7 @@ let trans_visitor : unit = iflog (fun _ -> annotate ("copy_ty: referent data of type " ^ - (Ast.fmt_to_str Ast.fmt_ty ty))); + (Fmt.fmt_to_str Ast.fmt_ty ty))); match ty with Ast.TY_nil | Ast.TY_bool @@ -2626,7 +2626,7 @@ let trans_visitor | MEM_interior when type_is_structured ty -> (iflog (fun _ -> annotate ("mark interior slot " ^ - (Ast.fmt_to_str Ast.fmt_slot slot)))); + (Fmt.fmt_to_str Ast.fmt_slot slot)))); let (mem, _) = need_mem_cell cell in let tmp = next_vreg_cell Il.voidptr_t in let ty = maybe_iso curr_iso ty in @@ -2750,7 +2750,7 @@ let trans_visitor | MEM_interior when type_is_structured ty -> (iflog (fun _ -> annotate ("drop interior slot " ^ - (Ast.fmt_to_str Ast.fmt_slot slot)))); + (Fmt.fmt_to_str Ast.fmt_slot slot)))); let (mem, _) = need_mem_cell cell in let vr = next_vreg_cell Il.voidptr_t in lea vr mem; @@ -2767,7 +2767,7 @@ let trans_visitor if cx.ctxt_sess.Session.sess_trace_drop || cx.ctxt_sess.Session.sess_log_trans then - let slotstr = Ast.fmt_to_str Ast.fmt_ty ty in + let slotstr = Fmt.fmt_to_str Ast.fmt_ty ty in let str = step ^ " " ^ slotstr in begin annotate str; @@ -2785,7 +2785,7 @@ let trans_visitor | MEM_rc_opaque -> "MEM_rc_struct" | MEM_interior -> "MEM_rc_struct" in - let slotstr = Ast.fmt_to_str Ast.fmt_slot slot in + let slotstr = Fmt.fmt_to_str Ast.fmt_slot slot in let str = step ^ " " ^ mctrl_str ^ " " ^ slotstr in begin annotate str; @@ -3733,7 +3733,7 @@ let trans_visitor iflog (fun _ -> annotate (Printf.sprintf "callee_drop_slot %d = %s " (int_of_node slot_id) - (Ast.fmt_to_str Ast.fmt_slot_key k))); + (Fmt.fmt_to_str Ast.fmt_slot_key k))); drop_slot_in_current_frame (cell_of_block_slot slot_id) slot None @@ -3829,7 +3829,7 @@ let trans_visitor (Printf.sprintf "post-stmt, drop_slot %d = %s " (int_of_node slot_id) - (Ast.fmt_to_str Ast.fmt_slot_key k))); + (Fmt.fmt_to_str Ast.fmt_slot_key k))); drop_slot_in_current_frame (cell_of_block_slot slot_id) slot None end @@ -3841,7 +3841,7 @@ let trans_visitor iflog begin fun _ -> - let s = Ast.fmt_to_str Ast.fmt_stmt_body stmt in + let s = Fmt.fmt_to_str Ast.fmt_stmt_body stmt in log cx "translating stmt: %s" s; annotate s; end; @@ -4910,7 +4910,7 @@ let fixup_assigning_visitor : Walk.visitor = let path_name (_:unit) : string = - Ast.fmt_to_str Ast.fmt_name (Walk.path_to_name path) + Fmt.fmt_to_str Ast.fmt_name (Walk.path_to_name path) in let enter_file_for id = diff --git a/src/boot/me/typestate.ml b/src/boot/me/typestate.ml index 4671d0f4d0a..1824a56d874 100644 --- a/src/boot/me/typestate.ml +++ b/src/boot/me/typestate.ml @@ -91,7 +91,7 @@ let fmt_constr_key cx ckey = let fmt_constr_arg carg = match carg with Constr_arg_lit lit -> - Ast.fmt_to_str Ast.fmt_lit lit + Fmt.fmt_to_str Ast.fmt_lit lit | Constr_arg_node (id, pth) -> let rec fmt_pth pth = match pth with @@ -99,19 +99,19 @@ let fmt_constr_key cx ckey = if referent_is_slot cx id then let key = Hashtbl.find cx.ctxt_slot_keys id in - Ast.fmt_to_str Ast.fmt_slot_key key + Fmt.fmt_to_str Ast.fmt_slot_key key else let n = Hashtbl.find cx.ctxt_all_item_names id in - Ast.fmt_to_str Ast.fmt_name n + Fmt.fmt_to_str Ast.fmt_name n | Ast.CARG_ext (pth, nc) -> let b = fmt_pth pth in - b ^ (Ast.fmt_to_str Ast.fmt_name_component nc) + b ^ (Fmt.fmt_to_str Ast.fmt_name_component nc) in fmt_pth pth in let pred_name = Hashtbl.find cx.ctxt_all_item_names cid in Printf.sprintf "%s(%s)" - (Ast.fmt_to_str Ast.fmt_name pred_name) + (Fmt.fmt_to_str Ast.fmt_name pred_name) (String.concat ", " (List.map fmt_constr_arg @@ -120,7 +120,7 @@ let fmt_constr_key cx ckey = | Constr_init n when Hashtbl.mem cx.ctxt_slot_keys n -> Printf.sprintf "" (int_of_node n) - (Ast.fmt_to_str Ast.fmt_slot_key (Hashtbl.find cx.ctxt_slot_keys n)) + (Fmt.fmt_to_str Ast.fmt_slot_key (Hashtbl.find cx.ctxt_slot_keys n)) | Constr_init n -> Printf.sprintf "" (int_of_node n) ;; @@ -820,7 +820,7 @@ let run_dataflow cx graph : unit = iflog cx (fun _ -> log cx "stmt %d: '%s'" (int_of_node node) (match htab_search cx.ctxt_all_stmts node with None -> "??" - | Some stmt -> Ast.fmt_to_str Ast.fmt_stmt stmt)); + | Some stmt -> Fmt.fmt_to_str Ast.fmt_stmt stmt)); iflog cx (fun _ -> log cx "stmt %d:" (int_of_node node)); iflog cx (fun _ -> log cx " prestate %s" (fmt_constr_bitv prestate)); @@ -875,7 +875,7 @@ let typestate_verify_visitor "Unsatisfied precondition constraint %s at stmt %d: %s" constr_str (int_of_node s.id) - (Ast.fmt_to_str Ast.fmt_stmt + (Fmt.fmt_to_str Ast.fmt_stmt (Hashtbl.find cx.ctxt_all_stmts s.id))) (Bits.to_list precond); inner.Walk.visit_stmt_pre s diff --git a/src/boot/me/walk.ml b/src/boot/me/walk.ml index a8d74cad266..30b30e32e53 100644 --- a/src/boot/me/walk.ml +++ b/src/boot/me/walk.ml @@ -145,7 +145,7 @@ let mod_item_logging_visitor (path:Ast.name_component Stack.t) (inner:visitor) : visitor = - let path_name _ = Ast.fmt_to_str Ast.fmt_name (path_to_name path) in + let path_name _ = Fmt.fmt_to_str Ast.fmt_name (path_to_name path) in let visit_mod_item_pre name params item = logfn (Printf.sprintf "entering %s" (path_name())); inner.visit_mod_item_pre name params item; diff --git a/src/boot/util/fmt.ml b/src/boot/util/fmt.ml new file mode 100644 index 00000000000..650224ba42b --- /dev/null +++ b/src/boot/util/fmt.ml @@ -0,0 +1,83 @@ +(* + * Common formatting helpers. + *) + +let fmt = Format.fprintf +;; + +let fmt_str ff = fmt ff "%s" +;; + +let fmt_obox ff = Format.pp_open_box ff 4;; +let fmt_obox_3 ff = Format.pp_open_box ff 3;; +let fmt_cbox ff = Format.pp_close_box ff ();; +let fmt_obr ff = fmt ff "{";; +let fmt_cbr ff = fmt ff "@\n}";; +let fmt_cbb ff = (fmt_cbox ff; fmt_cbr ff);; + +let fmt_bracketed + (bra:string) + (ket:string) + (inner:Format.formatter -> 'a -> unit) + (ff:Format.formatter) + (a:'a) + : unit = + fmt_str ff bra; + inner ff a; + fmt_str ff ket +;; + +let fmt_arr_sep + (sep:string) + (inner:Format.formatter -> 'a -> unit) + (ff:Format.formatter) + (az:'a array) + : unit = + Array.iteri + begin + fun i a -> + if i <> 0 + then fmt_str ff sep; + inner ff a + end + az +;; + +let fmt_bracketed_arr_sep + (bra:string) + (ket:string) + (sep:string) + (inner:Format.formatter -> 'a -> unit) + (ff:Format.formatter) + (az:'a array) + : unit = + fmt_bracketed bra ket + (fmt_arr_sep sep inner) + ff az +;; + +let fmt_to_str (f:Format.formatter -> 'a -> unit) (v:'a) : string = + let buf = Buffer.create 16 in + let bf = Format.formatter_of_buffer buf in + begin + f bf v; + Format.pp_print_flush bf (); + Buffer.contents buf + end +;; + +let sprintf_fmt + (f:Format.formatter -> 'a -> unit) + : (unit -> 'a -> string) = + (fun _ -> fmt_to_str f) +;; + + +(* + * Local Variables: + * fill-column: 78; + * indent-tabs-mode: nil + * buffer-file-coding-system: utf-8-unix + * compile-command: "make -k -C ../.. 2>&1 | sed -e 's/\\/x\\//x:\\//g'"; + * End: + *)