Source file compute_impact.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
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
open Cil_types
open Cil_datatype
open Pdg_types
open PdgIndex
open Reason_graph
(** Computation of the PDG nodes that are impacted by the "execution"
of some initial PDG nodes. This is implemented as a forward
inter-procedural analysis on top of the PDG plugin. *)
module NS = Pdg_aux.NS
type nodes = NS.t
module NM = PdgTypes.Node.Map
module KFS = Kernel_function.Hptset
module KFM = Kernel_function.Map
let kfmns_find_default key m =
try KFM.find key m
with Not_found -> NS.empty
type todo = {
kf: kernel_function ;
pdg: PdgTypes.Pdg.t ;
zone: Locations.Zone.t ;
init: bool ;
}
and todolist = todo NM.t
type result = nodes KFM.t
module KfKfCall = Datatype.Triple_with_collections
(Kernel_function)(Kernel_function)(Cil_datatype.Stmt)
(struct let module_name = "Impact.Compute.KfKfCall" end)
(** Worklist maintained by the plugin to build its results *)
type worklist = {
mutable todo: todolist (** nodes that are impacted, but that have not been
propagated yet. *);
mutable result: result (** impacted nodes. This field only grows.
An invariant is that nodes in [todolist] are not already in [result],
except with differing [init] fields. *);
mutable downward_calls: Pdg_aux.call_interface KfKfCall.Map.t
(** calls for which an input may be impacted. If so, we must compute the
impact within the called function. For each call, we associate to each
PDG input of the callee the nodes that define the input in the caller.
The contents of this field grow. *);
mutable callers: KFS.t (** all the callers of the functions in which the
initial nodes are located. Constant after initialization, used to
initialize [upward_calls] below. *);
mutable upward_calls: Pdg_aux.call_interface Lazy.t KfKfCall.Map.t
(** calls for which an output may be impacted. If so, we must compute the
impact after the call in the caller (which is part of the [callers]
field by construction). For each output node at the call point in the
caller, associate all the nodes of the callee that define this output.
The field is lazy: if the impact "dies" before before reaching the call,
we may avoid a costly computation. Constant once initialized. *);
mutable fun_changed_downward: KFS.t (** Functions in which a new pdg node has
been found since the last iteration. The impact on downward calls with
those callers will have to be computed again. *);
mutable fun_changed_upward: KFS.t (** Functions in which a new pdg node has
been found. The impact on upward calls to those callees
will have to be computed again. *);
skip: Locations.Zone.t (** Locations for which the impact is
dismissed. Nodes that involve only those zones
are skipped. Constant after initialization *);
mutable initial_nodes: nodes KFM.t
(** Nodes that are part of the initial impact query, or directly
equivalent to those (corresponding nodes in a caller). *);
mutable unimpacted_initial: nodes KFM.t
(** Initial nodes (as defined above) that are not "self-impacting"
so far. Those nodes will not be part of the final results. *);
mutable reason: reason_graph
(** Reasons why nodes in [result] are marked as impacted. *);
compute_reason: bool (** compute the field [reason]; may be costly *);
}
(** Extract the node of the kf that are only part of the initial impact *)
let unimpacted_initial_by_kf wl kf =
kfmns_find_default kf wl.unimpacted_initial
(** Extract the current results for a given function *)
let result_by_kf wl kf =
kfmns_find_default kf wl.result
let result_to_node_origin (r: result) : Reason_graph.nodes_origin =
KFM.fold
(fun kf ns acc ->
NS.fold (fun (n, _) acc -> PdgTypes.Node.Map.add n kf acc) ns acc)
r PdgTypes.Node.Map.empty
let initial_to_node_set (init: nodes KFM.t) : NS.t =
KFM.fold (fun _ -> NS.union) init NS.empty
(** Mark that [n] comes from an indirect impact, ie. remove it from the
set of initial nodes that are not impacted. *)
let remove_from_unimpacted_initial wl kf (n, z) =
let unimpacted = unimpacted_initial_by_kf wl kf in
if NS.mem' (n, z) unimpacted then begin
Options.debug ~level:2 "node of initial impact %a is indirectly impacted"
PdgTypes.Node.pretty n;
wl.unimpacted_initial <-
KFM.add kf (NS.remove n unimpacted) wl.unimpacted_initial;
end
;;
(** Add a node to the sets of impacted nodes. Update the various fields
of the worklist that need it. [init] indicates that the node
is added only because it belongs to the set of initial nodes. *)
let add_to_result wl n kf init =
if init = false then remove_from_unimpacted_initial wl kf n;
if not (KFS.mem kf wl.fun_changed_downward) then
wl.fun_changed_downward <- KFS.add kf wl.fun_changed_downward;
let set = result_by_kf wl kf in
let s' = NS.add' n set in
wl.result <- KFM.add kf s' wl.result
(** return [true] if the location in [n] is contained in [skip], in which
case the node should be skipped entirely *)
let node_to_skip skip n =
match Pdg.Api.node_key n with
| Key.SigKey (Signature.In (Signature.InImpl z))
| Key.SigKey (Signature.Out (Signature.OutLoc z))
| Key.SigCallKey (_, Signature.In (Signature.InImpl z))
| Key.SigCallKey (_, Signature.Out (Signature.OutLoc z)) ->
Locations.Zone.equal Locations.Zone.bottom
(Locations.Zone.diff z skip)
| _ -> false
(** Auxiliary function, used to refuse some nodes that should not go in
the results *)
let filter wl (n, z) =
not (Locations.Zone.is_bottom z) &&
match Pdg.Api.node_key n with
| Key.SigKey (Signature.In Signature.InCtrl) -> false
| Key.VarDecl _ -> false
| _ ->
if node_to_skip wl.skip n then (
Options.debug ~once:true ~level:2 "skipping node %a as required"
PdgTypes.Node.pretty n;
false)
else true
(** Add a new edge in the graph explaining the results *)
let add_to_reason wl ~nsrc ~ndst rt =
if wl.compute_reason && filter wl ndst then
let reason = Reason.Set.add (fst nsrc, fst ndst, rt) wl.reason in
Options.debug ~level:2 "@[<hov 4>Adding %a@ because of@ %a/%a@]"
Pdg_aux.pretty_node ndst Reason_graph.ReasonType.pretty rt
Pdg_aux.pretty_node nsrc;
wl.reason <- reason
;;
(** Add some nodes to the [todo] field of the worklist, while enforcing some
invariants. Some kind of pdg nodes must not appear in it, plus the nodes
must not be in result already. *)
let add_to_do_aux ~init wl kf pdg (pn, zone as n) =
if filter wl n then
let pp fmt =
Format.fprintf fmt "node %a (in %a)"
Pdg_aux.pretty_node n Kernel_function.pretty kf;
in
let add () =
let todo = { kf; pdg; init; zone } in
wl.todo <- NM.add pn todo wl.todo
in
try
let cur = NM.find pn wl.todo in
if (cur.init = true && init = false) ||
(not (Locations.Zone.is_included zone cur.zone))
then begin
Options.debug ~level:2 "todo list node %t is now init=false" pp;
add ();
end
with Not_found ->
if NS.mem' n (result_by_kf wl kf) then begin
if init = false && NS.mem' n (unimpacted_initial_by_kf wl kf) then begin
Options.debug ~level:2 "adding again node %t, with init=false" pp;
add ()
end
end
else begin
Options.debug ~level:2 "adding %t" pp;
add ()
end
;;
(** Build the initial value of the [todo] field, from a list of initial nodes *)
let initial_to_do_list wl kf pdg nodes =
List.iter (fun n -> add_to_do_aux ~init:true wl kf pdg n) nodes
(** Mark a new node as impacted, and simultaneously mark that it is equivalent
to nodes that are all initial nodes *)
let add_to_do_part_of_initial wl kf pdg n =
add_to_do_aux ~init:true wl kf pdg n;
let initial_nodes = kfmns_find_default kf wl.initial_nodes in
if not (NS.mem' n initial_nodes) then begin
Options.debug ~level:2 "node %a is a part of the initial impact"
Pdg_aux.pretty_node n;
let unimpacted_kf = unimpacted_initial_by_kf wl kf in
let new_unimpacted = NS.add' n unimpacted_kf in
let new_initial = NS.add' n initial_nodes in
wl.unimpacted_initial <- KFM.add kf new_unimpacted wl.unimpacted_initial;
wl.initial_nodes <- KFM.add kf new_initial wl.initial_nodes;
end
;;
(** From now on, most functions will pass [init = false] to [add_to_do_aux]. We
define an alias instead *)
let add_to_do = add_to_do_aux ~init:false
(** Purely intra-procedural propagation from one impacted node. Just follow
the PDG once, for all kind of dependencies. *)
let intraprocedural_one_node wl (node, z as nsrc) kf pdg =
Options.debug ~level:3 "intraprocedural part";
PdgTypes.Pdg.fold_direct_codpds pdg
(fun () (dpd, zopt) n ->
let follow = match zopt with
| None -> true
| Some z' -> Locations.Zone.intersects z z'
in
if follow then begin
let ndst = (n, Locations.Zone.top) in
add_to_reason wl ~nsrc ~ndst (Intraprocedural dpd);
add_to_do wl kf pdg ndst;
end
) () node;
Options.debug ~level:3 "intraprocedural part done"
(** Add a downward call to the worklist the first time it is encountered. This
functions implicitly caches the mapping from the PDG nodes of the caller to
the ones of the callee, as this information is expensive to compute *)
let add_downward_call wl (caller_kf, pdg) (called_kf, called_pdg) stmt =
Options.debug ~level:3 "downward part";
if not (KfKfCall.Map.mem (caller_kf, called_kf, stmt) wl.downward_calls) then
let callee = (called_kf, called_pdg) in
let deps = Pdg_aux.all_call_input_nodes ~caller:pdg ~callee stmt in
wl.downward_calls <-
KfKfCall.Map.add (caller_kf, called_kf, stmt) deps wl.downward_calls;
Options.debug ~level:3 "downard part done"
else
Options.debug ~level:3 "empty downward part"
;;
(** Propagate impact from node [node] if it corresponds to a call statement.
This is a partially inter-procedural propagation: some nodes of the
callee are directly in the worklist, and the call is registered in the
field [downward_calls]. *)
let downward_one_call_node wl (pnode, _ as node) caller_kf pdg =
match Pdg.Api.node_key pnode with
| Key.SigKey (Signature.In Signature.InCtrl)
| Key.VarDecl _
| Key.CallStmt _
-> assert false
| Key.SigKey _ | Key.Stmt _ | Key.Label _ ->
()
| Key.SigCallKey(id, key) ->
let stmt = Key.call_from_id id in
let called_kfs = Eva.Results.callee stmt in
List.iter
(fun called_kf ->
let called_pdg = Pdg.Api.get called_kf in
let nodes_callee, pdg_ok =
Options.debug ~level:3 "%a: considering call to %a"
Pdg_aux.pretty_node node Kernel_function.pretty called_kf;
try
(match key with
| Signature.In (Signature.InNum n) ->
(try [Pdg.Api.find_input_node called_pdg n,
Locations.Zone.top]
with Not_found -> [])
| Signature.In Signature.InCtrl ->
(try [Pdg.Api.find_entry_point_node called_pdg,
Locations.Zone.top]
with Not_found -> [])
| Signature.In (Signature.InImpl _) -> assert false
| Signature.Out _ -> []
), true
with
| Pdg.Api.Top ->
Options.warning
"no precise pdg for function %s. \n\
Ignoring this function in the analysis (potentially incorrect results)."
(Kernel_function.get_name called_kf);
[], false
| Pdg.Api.Bottom ->
[], false
| Not_found -> assert false
in
Options.debug ~level:4 "Direct call nodes %a"
(Pretty_utils.pp_list ~sep:" " Pdg_aux.pretty_node) nodes_callee;
List.iter
(fun n ->
add_to_reason wl ~nsrc:node ~ndst:n InterproceduralDownward;
add_to_do wl called_kf called_pdg n
) nodes_callee;
if pdg_ok then
add_downward_call wl (caller_kf, pdg) (called_kf, called_pdg) stmt
) called_kfs;
Options.debug ~level:3 "propagation of call %a done"
Pdg_aux.pretty_node node
let zone_restrict set_src_impact =
let aux (_, z) acc = Locations.Zone.join z acc in
NS.fold aux set_src_impact Locations.Zone.bottom
(** Propagate impact for one call registered in [downward_calls]. If the set
of impacted nodes in the caller intersect the nodes [deps] that define the
input [node] of the call, add [node] to the impacted nodes. *)
let downward_one_call_inputs wl kf_caller kf_callee (node, deps) =
let results_for_kf_caller = result_by_kf wl kf_caller in
if NS.intersects deps results_for_kf_caller then
let inter = NS.inter deps results_for_kf_caller in
let z = zone_restrict inter in
let node' = (node, z) in
NS.iter'
(fun nsrc ->
add_to_reason wl ~nsrc ~ndst:node' InterproceduralDownward)
inter;
add_to_do wl kf_callee (Pdg.Api.get kf_callee) node';
;;
(** Propagate impact for all calls registered in [downward_calls]. For each
caller, if new impacted nodes have been found, try to propagate the call.
Then, zero out the list of functions that must be considered again. *)
let downward_calls_inputs wl =
let aux (kf_caller, kf_callee, _stmt) ldeps =
if KFS.mem kf_caller wl.fun_changed_downward then begin
Options.debug ~level:3 "Inputs from call %a -> %a"
Kernel_function.pretty kf_caller Kernel_function.pretty kf_callee;
List.iter (downward_one_call_inputs wl kf_caller kf_callee) ldeps;
Options.debug ~level:3 "call done"
end
in
KfKfCall.Map.iter aux wl.downward_calls;
wl.fun_changed_downward <- KFS.empty
(** Fill out the field [upward_calls] of the worklist. This is done by
visiting (transitively) all the callers of functions in [kfs], and
registering all the calls found this way. The callers found are added
to the field [callers]. For each find, we find the nodes of the callee
that define a given output in the caller using [Pdg_aux.all_call_out_nodes].
[kfs] must be all the functions containing the initial nodes of the
analysis. *)
let all_upward_callers wl kfs =
let aux_call (caller, pdg_caller) (callee, pdg_callee) callsite =
Options.debug ~level:2 ~source:(fst (Cil_datatype.Stmt.loc callsite))
"Found call %a -> %a"
Kernel_function.pretty caller Kernel_function.pretty callee;
let nodes =
lazy (Pdg_aux.all_call_out_nodes ~callee:pdg_callee ~caller:pdg_caller
callsite)
in
wl.upward_calls <-
KfKfCall.Map.add (caller, callee, callsite) nodes wl.upward_calls
in
let rec fixpoint todo =
try
let kf = KFS.choose todo in
let todo = KFS.remove kf todo in
let todo =
if not (KFS.mem kf wl.callers) then (
Options.debug "Found caller %a" Kernel_function.pretty kf;
let pdg_kf = Pdg.Api.get kf in
List.fold_left
(fun todo (caller, callsites) ->
let pdg_caller = Pdg.Api.get caller in
List.iter (aux_call (caller, pdg_caller) (kf, pdg_kf)) callsites;
KFS.add caller todo
) todo (Eva.Results.callsites kf);
)
else todo
in
wl.callers <- KFS.add kf wl.callers;
fixpoint todo
with Not_found -> ()
in
fixpoint kfs
(** Upward propagation in all the callers. For all upward-registered calls,
find if new impacted nodes have been found in the callee. If so, check if
they intersect with the nodes of the callee defining the output. Then, mark
the (caller) output node as impacted. At the end, zero out the list of
function that must be examined again. *)
let upward_in_callers wl =
let aux (caller, callee, _callsite) l =
if KFS.mem callee wl.fun_changed_upward then
List.iter
(fun (n, nodes) ->
let results_for_callee = result_by_kf wl callee in
if NS.intersects nodes results_for_callee then
let inter = NS.inter nodes results_for_callee in
let unimpacted_callee = unimpacted_initial_by_kf wl callee in
let init =
NS.for_all' (fun n -> NS.mem' n unimpacted_callee) inter
in
let z = zone_restrict inter in
let n = (n, z) in
NS.iter' (fun nsrc ->
add_to_reason wl ~nsrc ~ndst:n InterproceduralUpward
) inter;
if init then
add_to_do_part_of_initial wl caller (Pdg.Api.get caller) n
else
add_to_do wl caller (Pdg.Api.get caller) n
) (Lazy.force l)
in
KfKfCall.Map.iter aux wl.upward_calls;
wl.fun_changed_upward <- KFS.empty
(** Compute the initial state of the worklist. *)
let initial_worklist ?(skip=Locations.Zone.bottom) ?(reason=false) nodes kf =
let initial =
KFM.add kf
(List.fold_left (fun s n -> NS.add' n s) NS.empty nodes)
KFM.empty;
in
let wl = {
todo = NM.empty;
result = KFM.empty;
downward_calls = KfKfCall.Map.empty;
callers = KFS.empty;
upward_calls = KfKfCall.Map.empty;
initial_nodes = initial;
unimpacted_initial = initial;
fun_changed_downward = KFS.empty;
fun_changed_upward = KFS.empty;
skip = skip;
reason = Reason.Set.empty;
compute_reason = reason;
}
in
initial_to_do_list wl kf (Pdg.Api.get kf) nodes;
let initial_callers =
if Options.Upward.get () then KFS.singleton kf else KFS.empty
in
all_upward_callers wl initial_callers;
wl
(** To compute the impact of a statement, find the initial PDG nodes that must
be put in the worklist. The only subtlety consists in skipping input nodes
on statements that are calls; otherwise, we would get an impact in the
callees of the call. *)
let initial_nodes ~skip kf stmt =
Options.debug ~level:3 "computing initial nodes for %d" stmt.sid;
let pdg = Pdg.Api.get kf in
if Eva.Results.is_reachable stmt then
try
let all = Pdg.Api.find_simple_stmt_nodes pdg stmt in
let filter n = match PdgTypes.Node.elem_key n with
| Key.SigCallKey (_, Signature.In _) -> false
| _ -> not (node_to_skip skip n)
in
List.filter filter all
with
| PdgTypes.Pdg.Top ->
Options.warning
"analysis of %a is too imprecise, impact cannot be computed@."
Kernel_function.pretty kf;
[]
| Not_found -> assert false
else begin
Options.debug ~level:3 "stmt %d is dead. skipping." stmt.sid;
[]
end
(** Choose one node to process in the todo list, if one remains *)
let pick wl =
try
let (n, _ as r) = NM.choose wl.todo in
wl.todo <- NM.remove n wl.todo;
Some r
with Not_found -> None
(** Empty the [todo] field of the worklist by applying as many basic steps as
possible: intra-procedural steps, plus basic inter-procedural steps on
downward calls. *)
let rec intraprocedural wl = match pick wl with
| None -> ()
| Some (pnode, { kf; pdg; init; zone }) ->
let node = pnode, zone in
add_to_result wl node kf init;
Async.yield ();
Options.debug ~level:2 "considering new node %a in %a:@ <%a>%t"
PdgTypes.Node.pretty pnode Kernel_function.pretty kf
Pdg_aux.pretty_node node
(fun fmt -> if init then Format.pp_print_string fmt " (init)");
intraprocedural_one_node wl node kf pdg;
downward_one_call_node wl node kf pdg;
intraprocedural wl
let something_to_do wl = not (NM.is_empty wl.todo)
(** Make the worklist reach a fixpoint, by propagating all possible source of
impact as much as possible. Due to the way calls are treated (by
intersecting new impacted nodes with constant sets of nodes), it is more
efficient to saturate the field [result] before calling
[downward_calls_inputs] and [upward_in_callers]. We also make sure all
downward propagation is done before starting upward propagation. *)
let rec fixpoint wl =
if something_to_do wl then begin
intraprocedural wl;
wl.fun_changed_upward <-
KFS.union wl.fun_changed_downward wl.fun_changed_upward;
downward_calls_inputs wl;
if something_to_do wl then
fixpoint wl
else (
upward_in_callers wl;
fixpoint wl
)
end
let remove_unimpacted _kf impact initial =
match impact, initial with
| None, None | Some _, None | None, Some _ -> impact
| Some impact, Some initial -> Some (NS.diff impact initial)
(** Impact of a set of nodes. Once the worklist has reached its fixpoint,
remove the initial nodes that are not self-impacting from the result,
and return this result. *)
let impact ?skip ?reason nodes kf =
let wl = initial_worklist ?skip ?reason nodes kf in
fixpoint wl;
let without_init =
KFM.merge remove_unimpacted wl.result wl.unimpacted_initial
in
without_init, wl.unimpacted_initial, wl.initial_nodes, wl.reason
(** Impact of a list of PDG nodes coming from the same function *)
let nodes_impacted_by_nodes ?(skip=Locations.Zone.bottom) ?(restrict=Locations.Zone.top) ?(reason=false) kf nodes =
let nodes = List.map (fun n -> n, restrict) nodes in
let r, unimpacted, initial, reason_graph = impact ~skip ~reason nodes kf in
let pp_kf fmt (kf, ns) =
Format.fprintf fmt "@[%a: %a@]@ " Kernel_function.pretty kf
(Pretty_utils.pp_iter ~sep:",@ " ~pre:"" ~suf:""
NS.iter' Pdg_aux.pretty_node) ns
in
let iter f = KFM.iter (fun kf ns -> f (kf, ns)) in
Options.debug ~level:1 "@[<v>Results:@ %a@]"
(Pretty_utils.pp_iter ~sep:"@ " ~pre:"" ~suf:"" iter pp_kf) r;
let reason_full = {
Reason_graph.reason_graph;
nodes_origin = result_to_node_origin r;
initial_nodes = initial_to_node_set initial;
} in
if reason then Reason_graph.print_dot_graph reason_full;
r, unimpacted, reason_full
(** Impact of a list stmts coming from the same function *)
let nodes_impacted_by_stmts ?(skip=Locations.Zone.bottom) ?(restrict=Locations.Zone.top) ?(reason=false) kf stmts =
let nodes = List.map (initial_nodes ~skip kf) stmts in
let nodes = List.concat nodes in
Options.debug
"about to compute impact for stmt(s) %a, %d initial nodes"
(Pretty_utils.pp_list ~sep:",@ " Stmt.pretty_sid) stmts
(List.length nodes);
nodes_impacted_by_nodes ~skip ~restrict ~reason kf nodes
(** Transform the result of an analysis into a set of PDG nodes *)
let result_to_nodes (res: result) : nodes =
KFM.fold (fun _ s acc -> NS.union s acc) res NS.empty
(** Transform a set of PDG nodes into a set of statements *)
let nodes_to_stmts ns =
let get_stmt node = Key.stmt (Pdg.Api.node_key node) in
let set =
NS.fold
(fun (n, _z) acc ->
Option.fold ~none:acc ~some:(fun s -> Stmt.Set.add s acc) (get_stmt n)
) ns Stmt.Set.empty
in
Stmt.Set.elements set
(** Impact of a list of statements as a set of statements *)
let stmts_impacted ?(skip=Locations.Zone.bottom) ~reason kf stmts =
let r, _, _ = nodes_impacted_by_stmts ~skip ~reason kf stmts in
nodes_to_stmts (result_to_nodes r)
(** Impact of a list of PDG nodes as a set of nodes *)
let nodes_impacted ?(skip=Locations.Zone.bottom) ~reason kf nodes =
let r, _, _ = nodes_impacted_by_nodes ~skip ~reason kf nodes in
result_to_nodes r
(** Nodes impacted in a given function *)
let impact_in_kf (res: result) kf = kfmns_find_default kf res
(** Computation of the [skip] field from a list of variables *)
let skip_bases vars =
let aux acc v =
let z = Locations.Zone.inject v Int_Intervals.top in
Locations.Zone.join z acc
in
List.fold_left aux Locations.Zone.bottom vars
(** Computation of the [skip] field from the [-impact-skip] option *)
let skip () =
let bases = Options.Skip.fold
(fun name l ->
let vi =
try
Base.of_varinfo (Globals.Vars.find_from_astinfo name Global)
with Not_found ->
if name = "NULL" then Base.null
else
Options.abort "cannot skip unknown variable %s" name
in
vi :: l) []
in
skip_bases bases