1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
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 ()
(* TODO gourdinl remove or adapt this?
let print_function pp id f =
fprintf pp "%s(%a) {\n" (extern_atom id) regs f.fn_params;
let instrs = List.map (fun (n, i) -> i.entry) (PTree.elements f.fn_code) in
List.iter (print_iblock pp true "") instrs;
fprintf pp "}\n\n"
let print_globdef pp (id, gd) =
match gd with Gfun (Internal f) -> print_function pp id f | _ -> ()
let print_program pp (prog : BTL.program) =
List.iter (print_globdef pp) prog.prog_defs*)
|
