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
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
(* *********************************************************************)
(* *)
(* The Compcert verified compiler *)
(* *)
(* Xavier Leroy, INRIA Paris-Rocquencourt *)
(* *)
(* Copyright Institut National de Recherche en Informatique et en *)
(* Automatique. All rights reserved. This file is distributed *)
(* under the terms of the INRIA Non-Commercial License Agreement. *)
(* *)
(* *********************************************************************)
(** Pretty-printer for XTL *)
open Printf
open Camlcoq
open Datatypes
open Maps
open AST
open Registers
open Op
open Locations
open PrintAST
open PrintOp
open XTL
let mreg pp r =
match Machregsaux.name_of_register r with
| Some s -> fprintf pp "%s" s
| None -> fprintf pp "<unknown machreg>"
let short_name_of_type = function
| Tint -> 'i'
| Tfloat -> 'f'
| Tlong -> 'l'
| Tsingle -> 's'
let loc pp = function
| R r -> mreg pp r
| S(Local, ofs, ty) ->
fprintf pp "L%c%ld" (short_name_of_type ty) (camlint_of_coqint ofs)
| S(Incoming, ofs, ty) ->
fprintf pp "I%c%ld" (short_name_of_type ty) (camlint_of_coqint ofs)
| S(Outgoing, ofs, ty) ->
fprintf pp "O%c%ld" (short_name_of_type ty) (camlint_of_coqint ofs)
let current_alloc = ref (None: (var -> loc) option)
let current_liveness = ref (None: VSet.t PMap.t option)
let reg pp r ty =
match !current_alloc with
| 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
| L l -> loc pp l
let rec vars pp = function
| [] -> ()
| [r] -> var pp r
| r1::rl -> fprintf pp "%a, %a" var r1 vars rl
let ros pp = function
| Coq_inl r -> var pp r
| Coq_inr s -> fprintf pp "\"%s\"" (extern_atom s)
let liveset pp lv =
fprintf pp "{";
VSet.iter (function V(r, ty) -> fprintf pp " x%d" (P.to_int r)
| L l -> ())
lv;
fprintf pp " }"
let print_succ pp s dfl =
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
| Xreload(src, dst) ->
fprintf pp "%a =r %a" var dst var src
| Xspill(src, dst) ->
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
| Xop(op, args, res) ->
fprintf pp "%a = %a" var res (print_operation var) (op, args)
| Xload(chunk, addr, args, dst) ->
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"
(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
| Xtailcall(sg, fn, args) ->
fprintf pp "tailcall %a(%a)" ros fn vars args
| Xbuiltin(ef, args, res) ->
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 %d else goto %d"
(print_condition var) (cond, args)
(P.to_int s1) (P.to_int s2)
| Xjumptable(arg, tbl) ->
let tbl = Array.of_list tbl in
fprintf pp "jumptable (%a)" var arg;
for i = 0 to Array.length tbl - 1 do
fprintf pp "\n\t\tcase %d: goto %d" i (P.to_int tbl.(i))
done
| Xreturn args ->
fprintf pp "return %a" vars args
let rec print_instructions pp succ = function
| [] -> ()
| [i] -> print_instruction pp succ i
| i :: il ->
print_instruction pp succ i;
fprintf pp "; ";
print_instructions pp succ il
let print_block pp (pc, blk) =
fprintf pp "%5d:\t" pc;
print_instructions pp (pc - 1) blk;
fprintf pp "\n";
match !current_liveness with
| None -> ()
| 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() {\n";
let instrs =
List.sort
(fun (pc1, _) (pc2, _) -> Pervasives.compare pc2 pc1)
(List.map
(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 | [] -> -1);
List.iter (print_block pp) instrs;
fprintf pp "}\n\n";
current_alloc := None;
current_liveness := None
|
