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
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
|
(* *********************************************************************)
(* *)
(* 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. *)
(* *)
(* *********************************************************************)
(** The XTL intermediate language for register allocation *)
open Datatypes
open Camlcoq
open Maps
open AST
open Registers
open Op
open Locations
type var = V of reg * typ | L of loc
type node = P.t
type instruction =
| Xmove of var * var
| Xreload of var * var
| Xspill of var * var
| Xparmove of var list * var list * var * var
| Xop of operation * var list * var
| Xload of memory_chunk * addressing * var list * var
| Xstore of memory_chunk * addressing * var list * var
| Xcall of signature * (var, ident) sum * var list * var list
| Xtailcall of signature * (var, ident) sum * var list
| Xbuiltin of external_function * var list * var list
| Xbranch of node
| Xcond of condition * var list * node * node
| Xjumptable of var * node list
| Xreturn of var list
type block = instruction list
(* terminated by one of Xbranch, Xcond, Xjumptable, Xtailcall or Xreturn *)
type code = block PTree.t
(* mapping node -> block *)
type xfunction = {
fn_sig: signature;
fn_stacksize: Z.t;
fn_code: code;
fn_entrypoint: node
}
(* Type of a variable *)
let typeof = function V(_, ty) -> ty | L l -> Loc.coq_type l
(* Constructors for type [var] *)
let vloc l = L l
let vlocs ll = List.map vloc ll
let vmreg mr = L(R mr)
let vmregs mrl = List.map vmreg mrl
(* Sets of variables *)
module VSet = Set.Make(struct type t = var let compare = compare end)
(*** Generation of fresh registers and fresh register variables *)
let next_temp = ref P.one
let twin_table : (int32, P.t) Hashtbl.t = Hashtbl.create 27
let reset_temps () =
next_temp := P.one; Hashtbl.clear twin_table
let new_reg() =
let r = !next_temp in next_temp := P.succ !next_temp; r
let new_temp ty = V (new_reg(), ty)
let twin_reg r =
let r = P.to_int32 r in
try
Hashtbl.find twin_table r
with Not_found ->
let t = new_reg() in Hashtbl.add twin_table r t; t
(*** Successors (for dataflow analysis) *)
let rec successors_block = function
| Xbranch s :: _ -> [s]
| Xtailcall(sg, vos, args) :: _ -> []
| Xcond(cond, args, s1, s2) :: _ -> [s1; s2]
| Xjumptable(arg, tbl) :: _ -> tbl
| Xreturn _:: _ -> []
| instr :: blk -> successors_block blk
| [] -> assert false
let successors fn =
PTree.map1 successors_block fn.fn_code
(**** Type checking for XTL *)
exception Type_error
exception Type_error_at of node
let set_var_type v ty =
if typeof v <> ty then raise Type_error
let rec set_vars_type vl tyl =
match vl, tyl with
| [], [] -> ()
| v1 :: vl, ty1 :: tyl -> set_var_type v1 ty1; set_vars_type vl tyl
| _, _ -> raise Type_error
let unify_var_type v1 v2 =
if typeof v1 <> typeof v2 then raise Type_error
let type_instr = function
| Xmove(src, dst) | Xspill(src, dst) | Xreload(src, dst) ->
unify_var_type src dst
| Xparmove(srcs, dsts, itmp, ftmp) ->
List.iter2 unify_var_type srcs dsts;
set_var_type itmp Tint;
set_var_type ftmp Tfloat
| Xop(op, args, res) ->
let (targs, tres) = type_of_operation op in
set_vars_type args targs;
set_var_type res tres
| Xload(chunk, addr, args, dst) ->
set_vars_type args (type_of_addressing addr);
set_var_type dst (type_of_chunk chunk)
| Xstore(chunk, addr, args, src) ->
set_vars_type args (type_of_addressing addr);
set_var_type src (type_of_chunk chunk)
| Xcall(sg, Coq_inl v, args, res) ->
set_var_type v Tint
| Xcall(sg, Coq_inr id, args, res) ->
()
| Xtailcall(sg, Coq_inl v, args) ->
set_var_type v Tint
| Xtailcall(sg, Coq_inr id, args) ->
()
| Xbuiltin(ef, args, res) ->
let sg = ef_sig ef in
set_vars_type args sg.sig_args;
set_vars_type res (Events.proj_sig_res' sg)
| Xbranch s ->
()
| Xcond(cond, args, s1, s2) ->
set_vars_type args (type_of_condition cond)
| Xjumptable(arg, tbl) ->
set_var_type arg Tint
| Xreturn args ->
()
let type_block blk =
List.iter type_instr blk
let type_function f =
PTree.fold
(fun () pc blk ->
try
type_block blk
with Type_error ->
raise (Type_error_at pc))
f.fn_code ()
(*** A generic framework for transforming extended basic blocks *)
(* Determine instructions that start an extended basic block.
These are instructions that have >= 2 predecessors. *)
let basic_blocks_map f = (* return mapping pc -> number of predecessors *)
let add_successor map s =
PMap.set s (1 + PMap.get s map) map in
let add_successors_block map pc blk =
List.fold_left add_successor map (successors_block blk) in
PTree.fold add_successors_block f.fn_code
(PMap.set f.fn_entrypoint 2 (PMap.init 0))
let transform_basic_blocks
(transf: node -> block -> 'state -> block * 'state)
(top: 'state)
f =
let bbmap = basic_blocks_map f in
let rec transform_block st newcode pc bb =
assert (PTree.get pc newcode = None);
let (bb', st') = transf pc bb st in
(* Record new code after transformation *)
let newcode' = PTree.set pc bb' newcode in
(* Propagate outgoing state to all successors *)
List.fold_left (transform_successor st') newcode' (successors_block bb)
and transform_successor st newcode pc =
if PMap.get pc bbmap <> 1 then newcode else begin
match PTree.get pc f.fn_code with
| None -> newcode
| Some bb -> transform_block st newcode pc bb
end in
(* Iterate over all extended basic block heads *)
let newcode =
PTree.fold
(fun newcode pc bb ->
if PMap.get pc bbmap >= 2
then transform_block top newcode pc bb
else newcode)
f.fn_code PTree.empty
in {f with fn_code = newcode}
|
