mikros/rust
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add fmt module, move out some common format helpers, add instruction-selection tracing and make selection use queues rather than list refs.

Browse Source
This commit is contained in:
Graydon Hoare 2010-06-24 10:34:47 -07:00
parent 4a1f86ccd7
commit 25eb1fd3c9
15 changed files with 266 additions and 143 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Makefile
View File

@ -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)

77
src/boot/be/asm.ml
View File

@ -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) =

45
src/boot/be/il.ml
View File

@ -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)
;;

88
src/boot/be/x86.ml
View File

@ -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 =

4
src/boot/driver/main.ml
View File

@ -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);;

26
src/boot/fe/ast.ml
View File

@ -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;;

2
src/boot/fe/pexp.ml
View File

@ -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) ->

2
src/boot/llvm/lltrans.ml
View File

@ -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);

26
src/boot/me/dwarf.ml
View File

@ -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 "<other>"
DATA_num n -> Fmt.fmt ff "0x%x" n
| DATA_str s -> Fmt.fmt ff "\"%s\"" s
| DATA_other -> Fmt.fmt ff "<other>"
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)
;;

6
src/boot/me/resolve.ml
View File

@ -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

2
src/boot/me/semant.ml
View File

@ -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

28
src/boot/me/trans.ml
View File

@ -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 =

16
src/boot/me/typestate.ml
View File

@ -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 "<init #%d = %s>"
(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 "<init #%d>" (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

2
src/boot/me/walk.ml
View File

@ -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;

83
src/boot/util/fmt.ml Normal file
View File

@ -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:
*)