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
|
(* Calculate reaching definitions for each instruction.
* Determine when it is okay to replace some variables with
* expressions.
*
* After calling computeRDs on a fundec,
* ReachingDef.stmtStartData will contain a mapping from
* statement ids to data about which definitions reach each
* statement. ReachingDef.defIdStmtHash will contain a
* mapping from definition ids to the statement in which
* that definition takes place.
*
* instrRDs takes a list of instructions, and the
* definitions that reach the first instruction, and
* for each instruction figures out which definitions
* reach into or out of each instruction.
*
*)
open Cil
open Pretty
module E = Errormsg
module DF = Dataflow
module UD = Usedef
module IH = Inthash
module U = Util
module S = Stats
let debug_fn = ref ""
module IOS =
Set.Make(struct
type t = int option
let compare io1 io2 =
match io1, io2 with
Some i1, Some i2 -> Pervasives.compare i1 i2
| Some i1, None -> 1
| None, Some i2 -> -1
| None, None -> 0
end)
let debug = ref false
(* return the intersection of
Inthashes ih1 and ih2 *)
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'
(* Lookup varinfo in iosh. If the set contains None
or is not a singleton, return None, otherwise
return Some of the singleton *)
(* IOS.t IH.t -> varinfo -> int option *)
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
(* IOS.t IH.t -> varinfo -> IOS.t *)
let iosh_lookup iosh vi =
if IH.mem iosh vi.vid
then Some(IH.find iosh vi.vid)
else None
(* return Some(vid) if iosh contains defId.
return None otherwise *)
(* IOS.t IH.t -> int -> int option *)
let iosh_defId_find iosh defId =
(* int -> IOS.t -> int option -> int option*)
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
(* The resulting iosh will contain the
union of the same entries from iosh1 and
iosh2. If iosh1 has an entry that iosh2
does not, then the result will contain
None in addition to the things from the
entry in iosh1. *)
(* XXX this function is a performance bottleneck *)
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 ->
if not(IH.mem iosh1 id) then
let newset = IOS.add None ios2 in
IH.add iosh' id newset) iosh2;
iosh'
(* determine if two IOS.t IH.t s are the same *)
let iosh_equals iosh1 iosh2 =
(* if IH.length iosh1 = 0 && not(IH.length iosh2 = 0) ||
IH.length iosh2 = 0 && not(IH.length iosh1 = 0)*)
if not(IH.length iosh1 = IH.length iosh2)
then
(if !debug then ignore(E.log "iosh_equals: length not same\n");
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
(* replace an entire set with a singleton.
if nothing was there just add the singleton *)
(* IOS.t IH.t -> int -> varinfo -> unit *)
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
(* remove definitions that are killed.
add definitions that are gend *)
(* Takes the defs, the data, and a function for
obtaining the next def id *)
(* VS.t -> IOS.t IH.t -> (unit->int) -> unit *)
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
(* given reaching definitions into a list of
instructions, figure out the definitions that
reach in/out of each instruction *)
(* if out is true then calculate the definitions that
go out of each instruction, if it is false then
calculate the definitions reaching into each instruction *)
(* instr list -> int -> (varinfo IH.t * int) -> bool -> (varinfo IH.t * int) list *)
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 print_instr i (_,s', iosh') = *)
(* let d = d_instr () i ++ line in *)
(* fprint stdout 80 d; *)
(* flush stdout *)
(* in *)
let proc_one hil i =
match hil with
| [] ->
let _, defd = UD.computeUseDefInstr i in
if UD.VS.is_empty defd
then ((*if !debug then print_instr i ((), s, iosh);*)
[((), s, iosh)])
else
let iosh' = IH.copy iosh in
proc_defs defd iosh' (idMaker () s);
(*if !debug then
print_instr i ((), s + UD.VS.cardinal defd, iosh');*)
((), 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
((*if !debug then
print_instr i ((),s', iosh');*)
((), s', iosh')::l)
else let iosh'' = IH.copy iosh' in
proc_defs defd iosh'' (idMaker () s');
(*if !debug then
print_instr i ((), s' + UD.VS.cardinal defd, iosh'');*)
((),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
(* The right hand side of an assignment is either
a function call or an expression *)
type rhs = RDExp of exp | RDCall of instr
(* take the id number of a definition and return
the rhs of the definition if there is one.
Returns None if, for example, the definition is
caused by an assembly instruction *)
(* stmt IH.t -> (()*int*IOS.t IH.t) IH.t -> int -> (rhs * int * IOS.t IH.t) option *)
let rhsHtbl = IH.create 64 (* to avoid recomputation *)
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\n" defId) in
let (_,s,iosh) =
try IH.find stmdat stm.sid
with Not_found -> E.s (E.error "getDefRhs: sid %d not found \n" stm.sid) in
match stm.skind with
Instr il ->
let ivihl = instrRDs il stm.sid ((),s,iosh) true in (* defs that reach out of each instr *)
let ivihl_in = instrRDs il stm.sid ((),s,iosh) false in (* defs that reach into each instr *)
let iihl = List.combine (List.combine il ivihl) ivihl_in in
(try let ((i,(_,_,diosh)),(_,_,iosh_in)) = List.find (fun ((i,(_,_,iosh')),_) ->
match S.time "iosh_defId_find" (iosh_defId_find iosh') defId with
Some vid ->
(match i with
Set((Var vi',NoOffset),_,_) -> vi'.vid = vid (* _ -> NoOffset *)
| Call(Some(Var vi',NoOffset),_,_,_) -> vi'.vid = vid (* _ -> NoOffset *)
| 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\n"))
| 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) (* ? *)
with Not_found ->
(if !debug then ignore (E.log "getDefRhs: No instruction defines %d\n" defId);
IH.add rhsHtbl defId None;
None))
| _ -> E.s (E.error "getDefRhs: defining statement not an instruction list %d\n" defId)
(*None*)
let prettyprint didstmh stmdat () (_,s,iosh) = text ""
(*seq line (fun (vid,ios) ->
num vid ++ text ": " ++
IOS.fold (fun io d -> match io with
None -> d ++ text "None "
| Some i ->
let stm = IH.find didstmh i in
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)
(IH.tolist iosh)*)
module ReachingDef =
struct
let name = "Reaching Definitions"
let debug = debug
(* Should the analysis calculate may-reach
or must-reach *)
let mayReach = ref false
(* An integer that tells the id number of
the first definition *)
(* Also a hash from variable ids to a set of
definition ids that reach this statement.
None means there is a path to this point on which
there is no definition of the variable *)
type t = (unit * int * IOS.t IH.t)
let copy (_, i, iosh) = ((), i, IH.copy iosh)
(* entries for starting statements must
be added before calling compute *)
let stmtStartData = IH.create 32
(* a mapping from definition ids to
the statement corresponding to that id *)
let defIdStmtHash = IH.create 32
(* mapping from statement ids to statements
for better performance of ok_to_replace *)
let sidStmtHash = IH.create 64
(* pretty printer *)
let pretty = prettyprint defIdStmtHash stmtStartData
(* The first id to use when computeFirstPredecessor
is next called *)
let nextDefId = ref 0
(* Count the number of variable definitions in
a statement *)
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
(* the first predecessor is just the data in along with
the id of the first definition of the statement,
which we get from nextDefId *)
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;
((), startDefId, IH.copy iosh)
let combinePredecessors (stm:stmt) ~(old:t) ((_, s, iosh):t) =
match old with (_, os, oiosh) ->
if S.time "iosh_equals" (iosh_equals oiosh) iosh then None else
Some((), os, S.time "iosh_combine" (iosh_combine oiosh) iosh)
(* return an action that removes things that
are redefinied and adds the generated defs *)
let doInstr inst (_, s, iosh) =
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
(* all the work gets done at the instruction level *)
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);
DF.SDefault
let doGuard condition _ = DF.GDefault
let filterStmt stm = true
end
module RD = DF.ForwardsDataFlow(ReachingDef)
(* map all variables in vil to a set containing
None in iosh *)
(* IOS.t IH.t -> varinfo list -> () *)
let iosh_none_fill iosh vil =
List.iter (fun vi ->
IH.add iosh vi.vid (IOS.singleton None))
vil
(* Computes the reaching definitions for a
function. *)
(* Cil.fundec -> unit *)
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
let _ = IH.clear ReachingDef.stmtStartData in
let _ = IH.clear ReachingDef.defIdStmtHash in
let _ = IH.clear rhsHtbl in
let _ = Hashtbl.clear iRDsHtbl in
let _ = ReachingDef.nextDefId := 0 in
let fst_stm = List.hd slst in
let fst_iosh = IH.create 32 in
let _ = UD.onlyNoOffsetsAreDefs := false in
(*let _ = iosh_none_fill fst_iosh fdec.sformals in*)
let _ = IH.add ReachingDef.stmtStartData fst_stm.sid ((), 0, fst_iosh) in
let _ = ReachingDef.computeFirstPredecessor fst_stm ((), 0, fst_iosh) in
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
(* now ReachingDef.stmtStartData has the reaching def data in it *)
with Failure "hd" -> if compare fdec.svar.vname (!debug_fn) = 0 then
debug := false
(* return the definitions that reach the statement
with statement id sid *)
let getRDs sid =
try
Some (IH.find ReachingDef.stmtStartData sid)
with Not_found ->
None
(* E.s (E.error "getRDs: sid %d not found\n" sid) *)
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
(* Pretty print the reaching definition data for
a function *)
let ppFdec fdec =
seq line (fun stm ->
let ivih = IH.find ReachingDef.stmtStartData stm.sid in
ReachingDef.pretty () ivih) fdec.sbody.bstmts
(* If this class is extended with a visitor on expressions,
then the current rd data is available at each expression *)
class rdVisitorClass = object (self)
inherit nopCilVisitor
(* the statement being worked on *)
val mutable sid = -1
(* if a list of instructions is being processed,
then this is the corresponding list of
reaching definitions *)
val mutable rd_dat_lst = []
(* these are the reaching defs for the current
instruction if there is one *)
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 "hd" ->
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
|