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
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
|
open RTL
open RTLpath
open Registers
open Maps
open Camlcoq
open Datatypes
open Kildall
open Lattice
open DebugPrint
let get_some = function
| None -> failwith "Got None instead of Some _"
| Some thing -> thing
let successors_inst = function
| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) | Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> [n]
| Icond (_,_,n1,n2,_) -> [n1; n2]
| Ijumptable (_,l) -> l
| Itailcall _ | Ireturn _ -> []
let predicted_successor = function
| Inop n | Iop (_,_,_,n) | Iload (_,_,_,_,_,n) | Istore (_,_,_,_,n) -> Some n
| Icall (_,_,_,_,n) | Ibuiltin (_,_,_,n) -> None
| Icond (_,_,n1,n2,p) -> (
match p with
| Some true -> Some n1
| Some false -> Some n2
| None -> None )
| Ijumptable _ | Itailcall _ | Ireturn _ -> None
let non_predicted_successors i =
match predicted_successor i with
| None -> successors_inst i
| Some n -> List.filter (fun n' -> n != n') (successors_inst i)
let rec list_to_regset = function
| [] -> Regset.empty
| r::l -> Regset.add r (list_to_regset l)
let get_input_regs i =
let empty = Regset.empty in
match i with
| Inop _ -> empty
| Iop (_,lr,_,_) | Iload (_,_,_,lr,_,_) | Icond (_,lr,_,_,_) -> list_to_regset lr
| Istore (_,_,lr,r,_) -> Regset.add r (list_to_regset lr)
| Icall (_, ri, lr, _, _) | Itailcall (_, ri, lr) -> begin
let rs = list_to_regset lr in
match ri with
| Coq_inr _ -> rs
| Coq_inl r -> Regset.add r rs
end
| Ibuiltin (_, lbr, _, _) -> list_to_regset @@ AST.params_of_builtin_args lbr
| Ijumptable (r, _) -> Regset.add r empty
| Ireturn opr -> (match opr with Some r -> Regset.add r empty | None -> empty)
let get_output_reg i =
match i with
| Inop _ | Istore _ | Icond _ | Itailcall _ | Ijumptable _ | Ireturn _ -> None
| Iop (_, _, r, _) | Iload (_, _, _, _, r, _) | Icall (_, _, _, r, _) -> Some r
| Ibuiltin (_, _, brr, _) -> (match brr with AST.BR r -> Some r | _ -> None)
(* adapted from Linearizeaux.get_join_points *)
let get_join_points code entry =
let reached = ref (PTree.map (fun n i -> false) code) in
let reached_twice = ref (PTree.map (fun n i -> false) code) in
let rec traverse pc =
if get_some @@ PTree.get pc !reached then begin
if not (get_some @@ PTree.get pc !reached_twice) then
reached_twice := PTree.set pc true !reached_twice
end else begin
reached := PTree.set pc true !reached;
traverse_succs (successors_inst @@ get_some @@ PTree.get pc code)
end
and traverse_succs = function
| [] -> ()
| [pc] -> traverse pc
| pc :: l -> traverse pc; traverse_succs l
in traverse entry; !reached_twice
(* Does not set the input_regs and liveouts field *)
let get_path_map code entry join_points =
let visited = ref (PTree.map (fun n i -> false) code) in
let path_map = ref PTree.empty in
let rec dig_path e =
let psize = ref (-1) in
let path_successors = ref [] in
let rec dig_path_rec n : (path_info * node list) option =
if not (get_some @@ PTree.get n !visited) then
let inst = get_some @@ PTree.get n code in
begin
visited := PTree.set n true !visited;
psize := !psize + 1;
let successor = match predicted_successor inst with
| None -> None
| Some n' -> if get_some @@ PTree.get n' join_points then None else Some n'
in match successor with
| Some n' -> begin
path_successors := !path_successors @ non_predicted_successors inst;
dig_path_rec n'
end
| None -> Some ({ psize = (Camlcoq.Nat.of_int !psize);
input_regs = Regset.empty; pre_output_regs = Regset.empty; output_regs = Regset.empty },
!path_successors @ successors_inst inst)
end
else None
in match dig_path_rec e with
| None -> ()
| Some ret ->
let (path_info, succs) = ret in
begin
path_map := PTree.set e path_info !path_map;
List.iter dig_path succs
end
in begin
dig_path entry;
!path_map
end
let transfer f pc after = let open Liveness in
match PTree.get pc f.fn_code with
| Some i ->
(match i with
| Inop _ -> after
| Iop (_, args, res, _) ->
reg_list_live args (Regset.remove res after)
| Iload (_, _, _, args, dst, _) ->
reg_list_live args (Regset.remove dst after)
| Istore (_, _, args, src, _) ->
reg_list_live args (Regset.add src after)
| Icall (_, ros, args, res, _) ->
reg_list_live args (reg_sum_live ros (Regset.remove res after))
| Itailcall (_, ros, args) ->
reg_list_live args (reg_sum_live ros Regset.empty)
| Ibuiltin (_, args, res, _) ->
reg_list_live (AST.params_of_builtin_args args)
(reg_list_dead (AST.params_of_builtin_res res) after)
| Icond (_, args, _, _, _) ->
reg_list_live args after
| Ijumptable (arg, _) ->
Regset.add arg after
| Ireturn optarg ->
reg_option_live optarg Regset.empty)
| None -> Regset.empty
module RegsetLat = LFSet(Regset)
module DS = Backward_Dataflow_Solver(RegsetLat)(NodeSetBackward)
let analyze f =
let liveouts = get_some @@ DS.fixpoint f.fn_code successors_instr (transfer f) in
PTree.map (fun n _ -> let lo = PMap.get n liveouts in transfer f n lo) f.fn_code
(** OLD CODE - If needed to have our own kildall
let transfer after = let open Liveness in function
| Inop _ -> after
| Iop (_, args, res, _) ->
reg_list_live args (Regset.remove res after)
| Iload (_, _, _, args, dst, _) ->
reg_list_live args (Regset.remove dst after)
| Istore (_, _, args, src, _) ->
reg_list_live args (Regset.add src after)
| Icall (_, ros, args, res, _) ->
reg_list_live args (reg_sum_live ros (Regset.remove res after))
| Itailcall (_, ros, args) ->
reg_list_live args (reg_sum_live ros Regset.empty)
| Ibuiltin (_, args, res, _) ->
reg_list_live (AST.params_of_builtin_args args)
(reg_list_dead (AST.params_of_builtin_res res) after)
| Icond (_, args, _, _, _) ->
reg_list_live args after
| Ijumptable (arg, _) ->
Regset.add arg after
| Ireturn optarg ->
reg_option_live optarg Regset.empty
let get_last_nodes f =
let visited = ref (PTree.map (fun n i -> false) f.fn_code) in
let rec step n =
let inst = get_some @@ PTree.get n f.fn_code in
let successors = successors_inst inst in
if get_some @@ PTree.get n !visited then []
else begin
let analyze f =
let liveness = ref (PTree.map (fun n i -> None) f.fn_code) in
let predecessors = Duplicateaux.get_predecessors_rtl f.fn_code in
let last_nodes = get_last_nodes f in
let rec step liveout n = (* liveout is the input_regs from the successor *)
let inst = get_some @@ PTree.get n f.fn_code in
let continue = ref true in
let alive = match get_some @@ PTree.get n !liveness with
| None -> transfer liveout inst
| Some pre_alive -> begin
let union = Regset.union pre_alive liveout in
let new_alive = transfer union inst in
(if Regset.equal pre_alive new_alive then continue := false);
new_alive
end
in begin
liveness := PTree.set n (Some alive) !liveness;
if !continue then
let preds = get_some @@ PTree.get n predecessors in
List.iter (step alive) preds
end
in begin
List.iter (step Regset.empty) last_nodes;
let liveness_noopt = PTree.map (fun n i -> get_some i) !liveness in
begin
debug_flag := true;
dprintf "Liveness: "; print_ptree_regset liveness_noopt; dprintf "\n";
debug_flag := false;
liveness_noopt
end
end
*)
let rec traverse code n size =
let inst = get_some @@ PTree.get n code in
if (size == 0) then inst
else
let n' = get_some @@ predicted_successor inst in
traverse code n' (size-1)
let get_outputs liveness code n pi =
let last_instruction = traverse code n (Camlcoq.Nat.to_int pi.psize) in
let path_last_successors = successors_inst last_instruction in
let list_input_regs = List.map (
fun n -> get_some @@ PTree.get n liveness
) path_last_successors in
List.fold_left Regset.union Regset.empty list_input_regs
let set_pathmap_liveness f pm =
let liveness = analyze f in
let new_pm = ref PTree.empty in
let code = f.fn_code in
begin
debug "Liveness: "; print_ptree_regset liveness; debug "\n";
List.iter (fun (n, pi) ->
let inputs = get_some @@ PTree.get n liveness in
let outputs = get_outputs liveness code n pi in
new_pm := PTree.set n
{psize=pi.psize; input_regs=inputs; pre_output_regs=outputs; output_regs=outputs} !new_pm (* FIXME: STUB *)
) (PTree.elements pm);
!new_pm
end
let print_path_info pi = begin
debug "(psize=%d; " (Camlcoq.Nat.to_int pi.psize);
debug "input_regs=";
print_regset pi.input_regs;
debug "; output_regs=";
print_regset pi.output_regs;
debug ")"
end
let print_path_map path_map = begin
debug "[";
List.iter (fun (n,pi) ->
debug "\n\t";
debug "%d: " (P.to_int n);
print_path_info pi
) (PTree.elements path_map);
debug "]"
end
let build_path_map f =
let code = f.fn_code in
let entry = f.fn_entrypoint in
let join_points = get_join_points code entry in
let path_map = set_pathmap_liveness f @@ get_path_map code entry join_points in
begin
debug "Join points: ";
print_true_nodes join_points;
debug "\nPath map: ";
print_path_map path_map;
debug "\n";
path_map
end
|