-
Notifications
You must be signed in to change notification settings - Fork 87
/
ptranal.ml
600 lines (519 loc) · 19.1 KB
/
ptranal.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
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
(*
*
* Copyright (c) 2001-2002,
* John Kodumal <jkodumal@eecs.berkeley.edu>
* All rights reserved.
*
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* 1. Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
* 2. Redistributions in binary form must reproduce the above copyright
* notice, this list of conditions and the following disclaimer in the
* documentation and/or other materials provided with the distribution.
*
* 3. The names of the contributors may not be used to endorse or promote
* products derived from this software without specific prior written
* permission.
*
* THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
* IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
* TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
* PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER
* OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
* EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
* PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
* PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
* LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
* NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
* SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
*
*)
exception Bad_return
exception Bad_function
open Cil
module H = Hashtbl
module A = Olf
exception UnknownLocation = A.UnknownLocation
type access = A.lvalue * bool
type access_map = (lval, access) H.t
(** a mapping from varinfo's back to fundecs *)
module VarInfoKey =
struct
type t = varinfo
let compare v1 v2 = v1.vid - v2.vid
end
module F = Map.Make (VarInfoKey)
(***********************************************************************)
(* *)
(* Global Variables *)
(* *)
(***********************************************************************)
let model_strings = ref false
let print_constraints = A.print_constraints
let debug_constraints = A.debug_constraints
let debug_aliases = A.debug_aliases
let smart_aliases = A.smart_aliases
let debug = A.debug
let analyze_mono = A.analyze_mono
let no_flow = A.no_flow
let no_sub = A.no_sub
let fun_ptrs_as_funs = ref false
let show_progress = ref false
let debug_may_aliases = ref false
let found_undefined = ref false
let conservative_undefineds = ref false
let current_fundec : fundec option ref = ref None
let fun_access_map : (fundec, access_map) H.t = H.create 64
(* A mapping from varinfos to fundecs *)
let fun_varinfo_map = ref F.empty
let current_ret : A.tau option ref = ref None
let lvalue_hash : (varinfo,A.lvalue) H.t = H.create 64
let expressions : (exp,A.tau) H.t = H.create 64
let lvalues : (lval,A.lvalue) H.t = H.create 64
let fresh_index : (unit -> int) =
let count = ref 0 in
fun () ->
incr count;
!count
let alloc_names = [
"malloc";
"calloc";
"realloc";
"xmalloc";
"__builtin_alloca";
"alloca";
"kmalloc"
]
(* This function should be set by the client if it
* knows of functions returning a result that have
* no side effects. If the result is not used, then
* the call will be eliminated. *)
let callHasNoSideEffects : (exp -> bool) ref =
ref (fun _ -> false)
let all_globals : varinfo list ref = ref []
let all_functions : fundec list ref = ref []
(***********************************************************************)
(* *)
(* Utility Functions *)
(* *)
(***********************************************************************)
let is_undefined_fun = function
Lval (lh, o) ->
if isFunctionType (typeOfLval (lh, o)) then
match lh with
Var v -> v.vstorage = Extern
| _ -> false
else false
| _ -> false
let is_alloc_fun = function
Lval (lh, o) ->
if isFunctionType (typeOfLval (lh, o)) then
match lh with
Var v -> List.mem v.vname alloc_names
| _ -> false
else false
| _ -> false
let next_alloc = function
Lval (Var v, o) ->
let name = Printf.sprintf "%s@%d" v.vname (fresh_index ())
in
A.address (A.make_lvalue false name (Some v)) (* check *)
| _ -> raise Bad_return
let is_effect_free_fun = function
Lval (lh, o) when isFunctionType (typeOfLval (lh, o)) ->
begin
match lh with
Var v ->
begin
try ("CHECK_" = String.sub v.vname 0 6 ||
!callHasNoSideEffects (Lval(lh,o)))
with Invalid_argument _ -> false
end
| _ -> false
end
| _ -> false
(***********************************************************************)
(* *)
(* AST Traversal Functions *)
(* *)
(***********************************************************************)
(* should do nothing, might need to worry about Index case *)
(* let analyzeOffset (o : offset ) : A.tau = A.bottom () *)
let analyze_var_decl (v : varinfo ) : A.lvalue =
try H.find lvalue_hash v
with Not_found ->
let lv = A.make_lvalue false v.vname (Some v)
in
H.add lvalue_hash v lv;
lv
let isFunPtrType (t : typ) : bool =
match t with
TPtr (t, _) -> isFunctionType t
| _ -> false
let rec analyze_lval (lv : lval ) : A.lvalue =
let find_access (l : A.lvalue) (is_var : bool) : A.lvalue =
match !current_fundec with
None -> l
| Some f ->
let accesses = H.find fun_access_map f in
if H.mem accesses lv then l
else
begin
H.add accesses lv (l, is_var);
l
end in
let result =
match lv with
Var v, _ -> (* instantiate every syntactic occurrence of a function *)
let alv =
if isFunctionType (typeOfLval lv) then
A.instantiate (analyze_var_decl v) (fresh_index ())
else analyze_var_decl v
in
find_access alv true
| Mem e, _ ->
(* assert (not (isFunctionType(typeOf(e))) ); *)
let alv =
if !fun_ptrs_as_funs && isFunPtrType (typeOf e) then
analyze_expr_as_lval e
else A.deref (analyze_expr e)
in
find_access alv false
in
H.replace lvalues lv result;
result
and analyze_expr_as_lval (e : exp) : A.lvalue =
match e with
Lval l -> analyze_lval l
| _ -> assert false (* todo -- other kinds of expressions? *)
and analyze_expr (e : exp ) : A.tau =
let result =
match e with
Const (CStr s) ->
if !model_strings then
A.address (A.make_lvalue
false
s
(Some (makeVarinfo false s charConstPtrType)))
else A.bottom ()
| Const c -> A.bottom ()
| Lval l -> A.rvalue (analyze_lval l)
| SizeOf _ -> A.bottom ()
| SizeOfStr _ -> A.bottom ()
| AlignOf _ -> A.bottom ()
| UnOp (op, e, t) -> analyze_expr e
| BinOp (op, e, e', t) -> A.join (analyze_expr e) (analyze_expr e')
| Question (_, e, e', _) -> A.join (analyze_expr e) (analyze_expr e')
| CastE (t, e) -> analyze_expr e
| AddrOf l ->
if !fun_ptrs_as_funs && isFunctionType (typeOfLval l) then
A.rvalue (analyze_lval l)
else A.address (analyze_lval l)
| AddrOfLabel _ -> failwith "not implemented yet" (* XXX *)
| StartOf l -> A.address (analyze_lval l)
| AlignOfE _ -> A.bottom ()
| SizeOfE _ -> A.bottom ()
in
H.add expressions e result;
result
(* check *)
let rec analyze_init (i : init ) : A.tau =
match i with
SingleInit e -> analyze_expr e
| CompoundInit (t, oi) ->
A.join_inits (Util.list_map (function (_, i) -> analyze_init i) oi)
let analyze_instr (i : instr ) : unit =
match i with
Set (lval, rhs, l) ->
A.assign (analyze_lval lval) (analyze_expr rhs)
| Call (res, fexpr, actuals, l) ->
if not (isFunctionType (typeOf fexpr)) then
() (* todo : is this a varargs? *)
else if is_alloc_fun fexpr then
begin
if !debug then print_string "Found allocation function...\n";
match res with
Some r -> A.assign (analyze_lval r) (next_alloc fexpr)
| None -> ()
end
else if is_effect_free_fun fexpr then
List.iter (fun e -> ignore (analyze_expr e)) actuals
else (* todo : check to see if the thing is an undefined function *)
let fnres, site =
if is_undefined_fun fexpr && !conservative_undefineds then
A.apply_undefined (Util.list_map analyze_expr actuals)
else
A.apply (analyze_expr fexpr) (Util.list_map analyze_expr actuals)
in
begin
match res with
Some r ->
begin
A.assign_ret site (analyze_lval r) fnres;
found_undefined := true;
end
| None -> ()
end
| Asm _ -> ()
let rec analyze_stmt (s : stmt ) : unit =
match s.skind with
Instr il -> List.iter analyze_instr il
| Return (eo, l) ->
begin
match eo with
Some e ->
begin
match !current_ret with
Some ret -> A.return ret (analyze_expr e)
| None -> raise Bad_return
end
| None -> ()
end
| Goto (s', l) -> () (* analyze_stmt(!s') *)
| ComputedGoto (e, l) -> ()
| If (e, b, b', l) ->
(* ignore the expression e; expressions can't be side-effecting *)
analyze_block b;
analyze_block b'
| Switch (e, b, sl, l) ->
analyze_block b;
List.iter analyze_stmt sl
| Loop (b, l, _, _) -> analyze_block b
| Block b -> analyze_block b
| TryFinally (b, h, _) ->
analyze_block b;
analyze_block h
| TryExcept (b, (il, _), h, _) ->
analyze_block b;
List.iter analyze_instr il;
analyze_block h
| Break l -> ()
| Continue l -> ()
and analyze_block (b : block ) : unit =
List.iter analyze_stmt b.bstmts
let analyze_function (f : fundec ) : unit =
let oldlv = analyze_var_decl f.svar in
let ret = A.make_fresh (f.svar.vname ^ "_ret") in
let formals = Util.list_map analyze_var_decl f.sformals in
let newf = A.make_function f.svar.vname formals ret in
if !show_progress then
Printf.printf "Analyzing function %s\n" f.svar.vname;
fun_varinfo_map := F.add f.svar f (!fun_varinfo_map);
current_fundec := Some f;
H.add fun_access_map f (H.create 8);
A.assign oldlv newf;
current_ret := Some ret;
analyze_block f.sbody
let analyze_global (g : global ) : unit =
match g with
GVarDecl (v, l) -> () (* ignore (analyze_var_decl(v)) -- no need *)
| GVar (v, init, l) ->
all_globals := v :: !all_globals;
begin
match init.init with
Some i -> A.assign (analyze_var_decl v) (analyze_init i)
| None -> ignore (analyze_var_decl v)
end
| GFun (f, l) ->
all_functions := f :: !all_functions;
analyze_function f
| _ -> ()
let analyze_file (f : file) : unit =
iterGlobals f analyze_global
(***********************************************************************)
(* *)
(* High-level Query Interface *)
(* *)
(***********************************************************************)
(* Same as analyze_expr, but no constraints. *)
let rec traverse_expr (e : exp) : A.tau =
H.find expressions e
and traverse_expr_as_lval (e : exp) : A.lvalue =
match e with
| Lval l -> traverse_lval l
| _ -> assert false (* todo -- other kinds of expressions? *)
and traverse_lval (lv : lval ) : A.lvalue =
H.find lvalues lv
let may_alias (e1 : exp) (e2 : exp) : bool =
let tau1,tau2 = traverse_expr e1, traverse_expr e2 in
let result = A.may_alias tau1 tau2 in
if !debug_may_aliases then
begin
let doc1 = d_exp () e1 in
let doc2 = d_exp () e2 in
let s1 = Pretty.sprint ~width:30 doc1 in
let s2 = Pretty.sprint ~width:30 doc2 in
Printf.printf
"%s and %s may alias? %s\n"
s1
s2
(if result then "yes" else "no")
end;
result
let resolve_lval (lv : lval) : varinfo list =
A.points_to (traverse_lval lv)
let resolve_exp (e : exp) : varinfo list =
A.epoints_to (traverse_expr e)
let resolve_funptr (e : exp) : fundec list =
let varinfos = A.epoints_to (traverse_expr e) in
List.fold_left
(fun fdecs -> fun vinf ->
try F.find vinf !fun_varinfo_map :: fdecs
with Not_found -> fdecs)
[]
varinfos
let count_hash_elts h =
let result = ref 0 in
H.iter (fun _ -> fun _ -> incr result) lvalue_hash;
!result
let compute_may_aliases (b : bool) : unit =
let rec compute_may_aliases_aux (exps : exp list) =
match exps with
[] -> ()
| h :: t ->
ignore (Util.list_map (may_alias h) t);
compute_may_aliases_aux t
and exprs : exp list ref = ref [] in
H.iter (fun e -> fun _ -> exprs := e :: !exprs) expressions;
compute_may_aliases_aux !exprs
let compute_results (show_sets : bool) : unit =
let total_pointed_to = ref 0
and total_lvalues = H.length lvalue_hash
and counted_lvalues = ref 0
and lval_elts : (string * (string list)) list ref = ref [] in
let print_result (name, set) =
let rec print_set s =
match s with
[] -> ()
| h :: [] -> print_string h
| h :: t ->
print_string (h ^ ", ");
print_set t
and ptsize = List.length set in
total_pointed_to := !total_pointed_to + ptsize;
if ptsize > 0 then
begin
print_string (name ^ "(" ^ (string_of_int ptsize) ^ ") -> ");
print_set set;
print_newline ()
end
in
(* Make the most pessimistic assumptions about globals if an
undefined function is present. Such a function can write to every
global variable *)
let hose_globals () : unit =
List.iter
(fun vd -> A.assign_undefined (analyze_var_decl vd))
!all_globals
in
let show_progress_fn (counted : int ref) (total : int) : unit =
incr counted;
if !show_progress then
Printf.printf "Computed flow for %d of %d sets\n" !counted total
in
if !conservative_undefineds && !found_undefined then hose_globals ();
A.finished_constraints ();
if show_sets then
begin
print_endline "Computing points-to sets...";
Hashtbl.iter
(fun vinf -> fun lv ->
show_progress_fn counted_lvalues total_lvalues;
try lval_elts := (vinf.vname, A.points_to_names lv) :: !lval_elts
with A.UnknownLocation -> ())
lvalue_hash;
List.iter print_result !lval_elts;
Printf.printf
"Total number of things pointed to: %d\n"
!total_pointed_to
end;
if !debug_may_aliases then
begin
Printf.printf "Printing may alias relationships\n";
compute_may_aliases true
end
let print_types () : unit =
print_string "Printing inferred types of lvalues...\n";
Hashtbl.iter
(fun vi -> fun lv ->
Printf.printf "%s : %s\n" vi.vname (A.string_of_lvalue lv))
lvalue_hash
(** Alias queries. For each function, gather sets of locals, formals, and
globals. Do n^2 work for each of these functions, reporting whether or not
each pair of values is aliased. Aliasing is determined by taking points-to
set intersections.
*)
let compute_aliases = compute_may_aliases
(***********************************************************************)
(* *)
(* Abstract Location Interface *)
(* *)
(***********************************************************************)
type absloc = A.absloc
let rec lvalue_of_varinfo (vi : varinfo) : A.lvalue =
H.find lvalue_hash vi
let lvalue_of_lval = traverse_lval
let tau_of_expr = traverse_expr
(** return an abstract location for a varinfo, resp. lval *)
let absloc_of_varinfo vi =
A.absloc_of_lvalue (lvalue_of_varinfo vi)
let absloc_of_lval lv =
A.absloc_of_lvalue (lvalue_of_lval lv)
let absloc_e_points_to e =
A.absloc_epoints_to (tau_of_expr e)
let absloc_lval_aliases lv =
A.absloc_points_to (lvalue_of_lval lv)
(* all abslocs that e transitively points to *)
let absloc_e_transitive_points_to (e : Cil.exp) : absloc list =
let rec lv_trans_ptsto (worklist : varinfo list) (acc : varinfo list) : absloc list =
match worklist with
[] -> Util.list_map absloc_of_varinfo acc
| vi :: wklst'' ->
if List.mem vi acc then lv_trans_ptsto wklst'' acc
else
lv_trans_ptsto
(List.rev_append
(A.points_to (lvalue_of_varinfo vi))
wklst'')
(vi :: acc)
in
lv_trans_ptsto (A.epoints_to (tau_of_expr e)) []
let absloc_eq a b = A.absloc_eq (a, b)
let d_absloc: unit -> absloc -> Pretty.doc = A.d_absloc
let ptrAnalysis = ref false
let ptrResults = ref false
let ptrTypes = ref false
(** Turn this into a CIL feature *)
let feature : featureDescr = {
fd_name = "ptranal";
fd_enabled = ptrAnalysis;
fd_description = "alias analysis";
fd_extraopt = [
("--ptr_may_aliases",
Arg.Unit (fun _ -> debug_may_aliases := true),
" Print out results of may alias queries");
("--ptr_unify", Arg.Unit (fun _ -> no_sub := true),
" Make the alias analysis unification-based");
("--ptr_model_strings", Arg.Unit (fun _ -> model_strings := true),
" Make the alias analysis model string constants");
("--ptr_conservative",
Arg.Unit (fun _ -> conservative_undefineds := true),
" Treat undefineds conservatively in alias analysis");
("--ptr_results", Arg.Unit (fun _ -> ptrResults := true),
" print the results of the alias analysis");
("--ptr_mono", Arg.Unit (fun _ -> analyze_mono := true),
" run alias analysis monomorphically");
("--ptr_types",Arg.Unit (fun _ -> ptrTypes := true),
" print inferred points-to analysis types")
];
fd_doit = (function (f: file) ->
analyze_file f;
compute_results !ptrResults;
if !ptrTypes then print_types ());
fd_post_check = false (* No changes *)
}
let () = Feature.register feature