Source file reachingdefs.ml
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
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
open GoblintCil
open Pretty
open Liveness
module E = Errormsg
module DF = Dataflow
module UD = Usedef
module L = Liveness
module IH = Inthash
module U = Util
module S = Stats
let debug_fn = ref ""
let doTime = ref false
let time s f a =
if !doTime then
S.time s f a
else f a
module IOS =
Set.Make(struct
type t = int option
let compare io1 io2 =
match io1, io2 with
Some i1, Some i2 -> Stdlib.compare i1 i2
| Some i1, None -> 1
| None, Some i2 -> -1
| None, None -> 0
end)
let debug = ref false
let ih_inter ih1 ih2 =
let ih' = IH.copy ih1 in
IH.iter (fun id vi ->
if not(IH.mem ih2 id) then
IH.remove ih' id else
()) ih1;
ih'
let ih_union ih1 ih2 =
let ih' = IH.copy ih1 in
IH.iter (fun id vi ->
if not(IH.mem ih' id)
then IH.add ih' id vi
else ()) ih2;
ih'
let iosh_singleton_lookup iosh vi =
if IH.mem iosh vi.vid then
let ios = IH.find iosh vi.vid in
if not (IOS.cardinal ios = 1) then None
else IOS.choose ios
else None
let iosh_lookup iosh vi =
if IH.mem iosh vi.vid
then Some(IH.find iosh vi.vid)
else None
let iosh_defId_find iosh defId =
let get_vid vid ios io =
match io with
Some(i) -> Some(i)
| None ->
let there = IOS.exists
(function None -> false
| Some(i') -> defId = i') ios in
if there then Some(vid) else None
in
IH.fold get_vid iosh None
let iosh_combine iosh1 iosh2 =
let iosh' = IH.copy iosh1 in
IH.iter (fun id ios1 ->
try let ios2 = IH.find iosh2 id in
let newset = IOS.union ios1 ios2 in
IH.replace iosh' id newset;
with Not_found ->
let newset = IOS.add None ios1 in
IH.replace iosh' id newset) iosh1;
IH.iter (fun id ios2 ->
try ignore(IH.find iosh1 id)
with Not_found -> begin
let newset = IOS.add None ios2 in
IH.add iosh' id newset end) iosh2;
iosh'
let iosh_equals iosh1 iosh2 =
if not(IH.length iosh1 = IH.length iosh2)
then
(if !debug then ignore(E.log "iosh_equals: length not same: %d %d\n"
(IH.length iosh1) (IH.length iosh2));
false)
else
IH.fold (fun vid ios b ->
if not b then b else
try let ios2 = IH.find iosh2 vid in
if not(IOS.compare ios ios2 = 0) then
(if !debug then ignore(E.log "iosh_equals: sets for vid %d not equal\n" vid);
false)
else true
with Not_found ->
(if !debug then ignore(E.log "iosh_equals: vid %d not in iosh2\n" vid);
false)) iosh1 true
let iosh_replace iosh i vi =
if IH.mem iosh vi.vid then
let newset = IOS.singleton (Some i) in
IH.replace iosh vi.vid newset
else
let newset = IOS.singleton (Some i) in
IH.add iosh vi.vid newset
let iosh_filter_dead iosh vs = iosh
let proc_defs vs iosh f =
let pd vi =
let newi = f() in
if !debug then
ignore (E.log "proc_defs: genning %d\n" newi);
iosh_replace iosh newi vi
in
UD.VS.iter pd vs
let idMaker () start =
let counter = ref start in
fun () ->
let ret = !counter in
counter := !counter + 1;
ret
let iRDsHtbl = Hashtbl.create 128
let instrRDs il sid (ivih, s, iosh) out =
if Hashtbl.mem iRDsHtbl (sid,out) then Hashtbl.find iRDsHtbl (sid,out) else
let proc_one hil i =
match hil with
| [] ->
let _, defd = UD.computeUseDefInstr i in
if UD.VS.is_empty defd
then (
[((), s, iosh)])
else
let iosh' = IH.copy iosh in
proc_defs defd iosh' (idMaker () s);
((), s + UD.VS.cardinal defd, iosh')::hil
| (_, s', iosh')::hrst as l ->
let _, defd = UD.computeUseDefInstr i in
if UD.VS.is_empty defd
then
(
((), s', iosh')::l)
else let iosh'' = IH.copy iosh' in
proc_defs defd iosh'' (idMaker () s');
((),s' + UD.VS.cardinal defd, iosh'')::l
in
let folded = List.fold_left proc_one [((),s,iosh)] il in
let foldedout = List.tl (List.rev folded) in
let foldednotout = List.rev (List.tl folded) in
Hashtbl.add iRDsHtbl (sid,true) foldedout;
Hashtbl.add iRDsHtbl (sid,false) foldednotout;
if out then foldedout else foldednotout
type rhs = RDExp of exp | RDCall of instr
let rhsHtbl = IH.create 64
let getDefRhs didstmh stmdat defId =
if IH.mem rhsHtbl defId then IH.find rhsHtbl defId else
let stm =
try IH.find didstmh defId
with Not_found -> E.s (E.error "getDefRhs: defId %d not found" defId) in
let (_,s,iosh) =
try IH.find stmdat stm.sid
with Not_found -> E.s (E.error "getDefRhs: sid %d not found" stm.sid) in
match stm.skind with
Instr il ->
let ivihl = instrRDs il stm.sid ((),s,iosh) true in
let ivihl_in = instrRDs il stm.sid ((),s,iosh) false in
begin try
let iihl = List.combine (List.combine il ivihl) ivihl_in in
(try let ((i,(_,_,diosh)),(_,_,iosh_in)) = List.find (fun ((i,(_,_,iosh')),_) ->
match time "iosh_defId_find" (iosh_defId_find iosh') defId with
Some vid ->
(match i with
Set((Var vi',NoOffset),_,_,_) -> vi'.vid = vid
| Call(Some(Var vi',NoOffset),_,_,_,_) -> vi'.vid = vid
| Call(None,_,_,_,_) -> false
| Asm(_,_,sll,_,_,_) -> List.exists
(function (_,_,(Var vi',NoOffset)) -> vi'.vid = vid | _ -> false) sll
| _ -> false)
| None -> false) iihl in
(match i with
Set((lh,_),e,_,_) ->
(match lh with
Var(vi') ->
(IH.add rhsHtbl defId (Some(RDExp(e),stm.sid,iosh_in));
Some(RDExp(e), stm.sid, iosh_in))
| _ -> E.s (E.error "Reaching Defs getDefRhs: right vi not first"))
| Call(lvo,e,el,_,_) ->
(IH.add rhsHtbl defId (Some(RDCall(i),stm.sid,iosh_in));
Some(RDCall(i), stm.sid, iosh_in))
| Asm(a,sl,slvl,sel,sl',_) -> None
| VarDecl _ -> None
)
with Not_found ->
(if !debug then ignore (E.log "getDefRhs: No instruction defines %d\n" defId);
IH.add rhsHtbl defId None;
None))
with Invalid_argument _ -> None end
| _ -> E.s (E.error "getDefRhs: defining statement not an instruction list %d" defId)
let prettyprint didstmh stmdat () (_,s,iosh) =
seq ~sep:line ~doit:(fun (vid,ios) ->
num vid ++ text ": " ++
IOS.fold (fun io d -> match io with
None -> d ++ text "None "
| Some i ->
match getDefRhs didstmh stmdat i with
None -> d ++ num i
| Some(RDExp(e),_,_) ->
d ++ num i ++ text " " ++ (d_exp () e)
| Some(RDCall(c),_,_) ->
d ++ num i ++ text " " ++ (d_instr () c))
ios nil)
~elements:(IH.tolist iosh)
module ReachingDef =
struct
let name = "Reaching Definitions"
let debug = debug
let mayReach = ref false
type t = (unit * int * IOS.t IH.t)
let copy (_, i, iosh) = ((), i, IH.copy iosh)
let stmtStartData = IH.create 32
let defIdStmtHash = IH.create 32
let sidStmtHash = IH.create 64
let pretty = prettyprint defIdStmtHash stmtStartData
let nextDefId = ref 0
let num_defs stm =
match stm.skind with
Instr(il) -> List.fold_left (fun s i ->
let _, d = UD.computeUseDefInstr i in
s + UD.VS.cardinal d) 0 il
| _ -> let _, d = UD.computeUseDefStmtKind stm.skind in
UD.VS.cardinal d
let computeFirstPredecessor stm (_, s, iosh) =
let startDefId = max !nextDefId s in
let numds = num_defs stm in
let rec loop n =
if n < 0
then ()
else
(if !debug then
ignore (E.log "RD: defId %d -> stm %d\n" (startDefId + n) stm.sid);
IH.add defIdStmtHash (startDefId + n) stm;
loop (n-1))
in
loop (numds - 1);
nextDefId := startDefId + numds;
match L.getLiveSet stm.sid with
| None -> ((), startDefId, IH.copy iosh)
| Some vs -> ((), startDefId, iosh_filter_dead (IH.copy iosh) vs)
let combinePredecessors (stm:stmt) ~(old:t) ((_, s, iosh):t) =
match old with (_, os, oiosh) -> begin
if time "iosh_equals" (iosh_equals oiosh) iosh
then None
else begin
Some((), os, time "iosh_combine" (iosh_combine oiosh) iosh)
end
end
let doInstr inst (_, s, iosh) =
if !debug then E.log "RD: looking at %a\n" d_instr inst;
let transform (_, s', iosh') =
let _, defd = UD.computeUseDefInstr inst in
proc_defs defd iosh' (idMaker () s');
((), s' + UD.VS.cardinal defd, iosh')
in
DF.Post transform
let doStmt stm (_, s, iosh) =
if not(IH.mem sidStmtHash stm.sid) then
IH.add sidStmtHash stm.sid stm;
if !debug then ignore(E.log "RD: looking at %a\n" d_stmt stm);
match L.getLiveSet stm.sid with
| None -> DF.SDefault
| Some vs -> begin
DF.SUse((),s,iosh_filter_dead iosh vs)
end
let doGuard condition _ = DF.GDefault
let filterStmt stm = true
end
module RD = DF.ForwardsDataFlow(ReachingDef)
let iosh_none_fill iosh vil =
List.iter (fun vi ->
IH.add iosh vi.vid (IOS.singleton None))
vil
let clearMemos () =
IH.clear rhsHtbl;
Hashtbl.clear iRDsHtbl
let computeRDs fdec =
try
if compare fdec.svar.vname (!debug_fn) = 0 then
(debug := true;
ignore (E.log "%s =\n%a\n" (!debug_fn) d_block fdec.sbody));
let bdy = fdec.sbody in
let slst = bdy.bstmts in
IH.clear ReachingDef.stmtStartData;
IH.clear ReachingDef.defIdStmtHash;
IH.clear rhsHtbl;
Hashtbl.clear iRDsHtbl;
ReachingDef.nextDefId := 0;
let fst_stm = List.hd slst in
let fst_iosh = IH.create 32 in
UD.onlyNoOffsetsAreDefs := true;
IH.add ReachingDef.stmtStartData fst_stm.sid ((), 0, fst_iosh);
time "liveness" L.computeLiveness fdec;
UD.onlyNoOffsetsAreDefs := true;
ignore(ReachingDef.computeFirstPredecessor fst_stm ((), 0, fst_iosh));
(match L.getLiveSet fst_stm.sid with
| None -> if !debug then ignore(E.log "Nothing live at fst_stm\n")
| Some vs -> ignore(iosh_filter_dead fst_iosh vs));
if !debug then
ignore (E.log "computeRDs: fst_stm.sid=%d\n" fst_stm.sid);
RD.compute [fst_stm];
if compare fdec.svar.vname (!debug_fn) = 0 then
debug := false
with Failure _ -> if compare fdec.svar.vname (!debug_fn) = 0 then
debug := false
let getRDs sid =
try
Some (IH.find ReachingDef.stmtStartData sid)
with Not_found ->
None
let getDefIdStmt defid =
try
Some(IH.find ReachingDef.defIdStmtHash defid)
with Not_found ->
None
let getStmt sid =
try Some(IH.find ReachingDef.sidStmtHash sid)
with Not_found -> None
let getSimpRhs defId =
let rhso = getDefRhs ReachingDef.defIdStmtHash
ReachingDef.stmtStartData defId in
match rhso with None -> None
| Some(r,_,_) -> Some(r)
let isDefInstr i defId =
match getSimpRhs defId with
Some(RDCall i') -> Util.equals i i'
| _ -> false
let ppFdec fdec =
seq ~sep:line ~doit:(fun stm ->
let ivih = IH.find ReachingDef.stmtStartData stm.sid in
ReachingDef.pretty () ivih) ~elements:fdec.sbody.bstmts
class rdVisitorClass = object (self)
inherit nopCilVisitor
val mutable sid = -1
val mutable rd_dat_lst = []
val mutable cur_rd_dat = None
method! vstmt stm =
sid <- stm.sid;
match getRDs sid with
None ->
if !debug then ignore(E.log "rdVis: stm %d had no data\n" sid);
cur_rd_dat <- None;
DoChildren
| Some(_,s,iosh) ->
match stm.skind with
Instr il ->
if !debug then ignore(E.log "rdVis: visit il\n");
rd_dat_lst <- instrRDs il stm.sid ((),s,iosh) false;
DoChildren
| _ ->
if !debug then ignore(E.log "rdVis: visit non-il\n");
cur_rd_dat <- None;
DoChildren
method! vinst i =
if !debug then ignore(E.log "rdVis: before %a, rd_dat_lst is %d long\n"
d_instr i (List.length rd_dat_lst));
try
cur_rd_dat <- Some(List.hd rd_dat_lst);
rd_dat_lst <- List.tl rd_dat_lst;
DoChildren
with Failure _ ->
if !debug then ignore(E.log "rdVis: il rd_dat_lst mismatch\n");
DoChildren
method get_cur_iosh () =
match cur_rd_dat with
None -> (match getRDs sid with
None -> None
| Some(_,_,iosh) -> Some iosh)
| Some(_,_,iosh) -> Some iosh
end