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
|
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.opt_info 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 ()
|
