Source file slicingCmds.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
(** Those functions were previously outside the slicing module to show how to
* use the slicing API. So, they are supposed to use the slicing module through
* Db.Slicing only. There are mainly high level functions which make easier
* to achieve simple tasks. *)
open Cil_types
type set = SlicingTypes.Fct_user_crit.t Cil_datatype.Varinfo.Map.t
let apply_all_actions () =
SlicingParameters.debug ~level:1 "[Api.apply_all_internal]";
SlicingParameters.feedback ~level:1 "applying all slicing requests...";
SlicingParameters.debug ~level:2 "pending requests:@\n %t@\n"
SlicingProject.print_proj_worklist;
let r = SlicingProject.apply_all_actions () in
SlicingParameters.feedback ~level:2 "done (applying all slicing requests).";
r
let apply_next_action () =
SlicingParameters.debug ~level:1 "[Api.apply_next_internal]";
SlicingProject.apply_next_action ()
let apply_all ~propagate_to_callers =
SlicingParameters.debug ~level:1 "[Api.apply_all]";
assert (not propagate_to_callers) ;
try
while (true)
do
apply_next_action ()
done
with Not_found -> ()
let get_select_kf (fvar, _select) = Globals.Functions.get fvar
let get_lval_zone ?(for_writing=false) stmt lval =
let open Eva.Results in
before stmt |> eval_address ~for_writing lval |> as_zone
(** Utilities for [kinstr]. *)
module Kinstr: sig
val iter_from_func : (stmt -> unit) -> kernel_function -> unit
val is_rw_zone : (Locations.Zone.t option * Locations.Zone.t option) -> stmt -> Locations.Zone.t option * Locations.Zone.t option
end
=
struct
(** Iter on statements of a kernel function *)
let iter_from_func f kf =
let definition = Kernel_function.get_definition kf in
List.iter f definition.sallstmts
(** Get directly read/written [Zone.t] by the statement.
* i.e. directly means when [ki] is a call,
it doesn't don't look at the assigns clause of the called function. *)
let get_rw_zone stmt =
assert (Eva.Analysis.is_computed ());
let lval_process read_zone stmt lv =
let zloc = get_lval_zone ~for_writing:true stmt lv in
let deps = Eva.Results.(before stmt |> address_deps lv) in
Locations.Zone.join read_zone deps, zloc
in
let call_process lv f args _loc =
let read_zone = Eva.Results.(before stmt |> expr_deps f) in
let add_args arg inputs =
Locations.Zone.join inputs Eva.Results.(before stmt |> expr_deps arg)
in
let read_zone = List.fold_right add_args args read_zone in
let read_zone,write_zone =
match lv with
| None -> read_zone , Locations.Zone.bottom
| Some lv -> lval_process read_zone stmt lv
in read_zone,write_zone
in
match stmt.skind with
| Switch (exp,_,_,_)
| If (exp,_,_,_) ->
Eva.Results.(before stmt |> expr_deps exp), Locations.Zone.bottom
| Instr (Set (lv,exp,_)) ->
let read_zone = Eva.Results.(before stmt |> expr_deps exp) in
lval_process read_zone stmt lv
| Instr (Local_init (v, AssignInit i, _)) ->
let rec collect zone i =
match i with
| SingleInit e ->
Locations.Zone.join zone Eva.Results.(before stmt |> expr_deps e)
| CompoundInit (_,l) ->
List.fold_left
(fun acc (_,i) -> collect acc i) zone l
in
let read_zone = collect Locations.Zone.bottom i in
lval_process read_zone stmt (Cil.var v)
| Instr (Call (lvaloption,funcexp,argl,l)) ->
call_process lvaloption funcexp argl l
| Instr (Local_init(v, ConsInit(f, args, k),l)) ->
Cil.treat_constructor_as_func call_process v f args k l
| _ -> Locations.Zone.bottom, Locations.Zone.bottom
(** Look at intersection of [rd_zone_opt]/[wr_zone_opt] with the
directly read/written [Zone.t] by the statement.
* i.e. directly means when [ki] is a call,
it doesn't don't look at the assigns clause of the called function. *)
let is_rw_zone (rd_zone_opt, wr_zone_opt) stmt =
let rd_zone, wr_zone = get_rw_zone stmt in
let inter_zone zone_opt zone =
match zone_opt with
| None -> zone_opt
| Some zone_requested ->
if Locations.Zone.intersects zone_requested zone
then let inter = Locations.Zone.narrow zone_requested zone
in Some inter
else None
in inter_zone rd_zone_opt rd_zone, inter_zone wr_zone_opt wr_zone
end
(** Topologically propagate user marks to callers in whole project *)
let topologic_propagation project =
apply_all_actions project;
Callgraph.Uses.iter_in_rev_order
(fun kf ->
SlicingParameters.debug ~level:3
"doing topologic propagation for function: %a"
Kernel_function.pretty kf;
apply_all_actions project)
let add_to_selection set selection =
SlicingSelect.Selections.add_to_selects selection set
(** Registered as a slicing selection function:
Add a selection of the pdg nodes. *)
let select_pdg_nodes set mark nodes kf =
let selection = SlicingSelect.select_pdg_nodes kf nodes mark
in add_to_selection set selection
(** Registered as a slicing selection function:
Add a selection of the statement. *)
let select_stmt set ~spare stmt kf =
let stmt_mark = SlicingMarks.mk_user_mark
~data:(not spare) ~addr:(not spare) ~ctrl:(not spare) in
let selection = SlicingSelect.select_stmt_computation kf stmt stmt_mark
in add_to_selection set selection
(** Add a selection to the entrance of the function [kf]
and add a selection to its return if [~return] is true
and add a selection to [~inputs] parts of its inputs
and add a selection to [~outputs] parts of its outputs*)
let select_entry_point_and_some_inputs_outputs set ~mark kf ~return ~outputs ~inputs =
SlicingParameters.debug ~level:3
"select_entry_point_and_some_inputs_outputs %a"
Kernel_function.pretty kf ;
let set = let selection = SlicingSelect.select_entry_point kf mark in
add_to_selection set selection
in
let set =
if (Locations.Zone.equal Locations.Zone.bottom inputs)
then set
else let selection = SlicingSelect.select_zone_at_entry kf inputs mark in
add_to_selection set selection
in if ((Locations.Zone.equal Locations.Zone.bottom outputs) && not return) ||
(try
let stmt = Kernel_function.find_return kf
in if Eva.Results.is_reachable stmt then
false
else
begin
SlicingParameters.feedback
"@[Nothing to select for unreachable return stmt of %a@]"
Kernel_function.pretty kf;
true
end
with Kernel_function.No_Statement -> false)
then set
else
let set =
if (Locations.Zone.equal Locations.Zone.bottom outputs)
then set
else let selection = SlicingSelect.select_modified_output_zone kf outputs mark in
add_to_selection set selection
in if return
then let selection = SlicingSelect.select_return kf mark in
add_to_selection set selection
else set
let generic_select_func_calls select_stmt set ~spare kf =
assert (Eva.Analysis.is_computed ());
let callers = Eva.Results.callsites kf in
let select_calls acc (caller, stmts) =
List.fold_left (fun acc s -> select_stmt acc ~spare s caller) acc stmts
in
List.fold_left select_calls set callers
(** Registered as a slicing selection function:
Add a selection of calls to a [kf]. *)
let select_func_calls_into set ~spare kf =
let add_to_select set ~spare select =
let mark =
let nspare = not spare in
SlicingMarks.mk_user_mark ~data:nspare ~addr:nspare ~ctrl:nspare
in add_to_selection set (select mark)
in
let kf_entry, _library = Globals.entry_point () in
if Kernel_function.equal kf_entry kf then
add_to_select set ~spare (SlicingSelect.select_entry_point kf)
else
let select_min_call set ~spare ki kf =
add_to_select set ~spare (SlicingSelect.select_minimal_call kf ki)
in
generic_select_func_calls select_min_call set ~spare kf
(** Registered as a slicing selection function:
Add a selection of calls to a [kf]. *)
let select_func_calls_to set ~spare kf =
let kf_entry, _library = Globals.entry_point () in
if Kernel_function.equal kf_entry kf then
begin
let mark =
let nspare = not spare in
SlicingMarks.mk_user_mark ~data:nspare ~addr:nspare ~ctrl:nspare
in
assert (Eva.Analysis.is_computed ());
let outputs = Inout.kf_external_outputs kf in
select_entry_point_and_some_inputs_outputs set ~mark kf
~return:true
~outputs
~inputs:Locations.Zone.bottom
end
else
generic_select_func_calls select_stmt set ~spare kf
(** Registered as a slicing selection function:
Add selection of function outputs. *)
let select_func_zone set mark zone kf =
let selection = SlicingSelect.select_zone_at_end kf zone mark
in add_to_selection set selection
(** Registered as a slicing selection function:
Add a selection of the [kf] return statement. *)
let select_func_return set ~spare kf =
try
let ki = Kernel_function.find_return kf
in select_stmt set ~spare ki kf
with Kernel_function.No_Statement ->
let mark =
SlicingMarks.mk_user_mark
~data:(not spare) ~addr:(not spare) ~ctrl:(not spare)
in
select_entry_point_and_some_inputs_outputs
set
~mark
kf
~return:true
~outputs:Locations.Zone.bottom
~inputs:Locations.Zone.bottom
(** Registered as a slicing selection function:
Add a selection of the statement reachability.
Note: add also a transparent selection on the whole statement. *)
let select_stmt_ctrl set ~spare ki kf =
let ctrl_mark =
SlicingMarks.mk_user_mark ~data:false ~addr:false ~ctrl:(not spare) in
let selection = SlicingSelect.select_stmt_computation kf ki ctrl_mark
in add_to_selection set selection
(** Registered as a slicing selection function:
Add a selection of data relative to a statement.
Note: add also a transparent selection on the whole statement. *)
let select_stmt_zone set mark zone ~before ki kf =
let selection =
SlicingSelect.select_stmt_zone kf ki ~before zone mark
in let set = add_to_selection set selection
in select_stmt_ctrl set ~spare:true ki kf
(** Registered as a slicing selection function:
Add a selection of data relative to a statement.
Variables of [lval_str] string are bounded
relatively to the whole scope of the function [kf].
The interpretation of the address of the lvalues is
done just before the execution of the statement [~eval].
The selection preserve the value of these lvalues before
or after (c.f. boolean [~before]) the statement [ki].
Note: add also a transparent selection on the whole statement. *)
let select_stmt_lval set mark lval_str ~before ki ~eval kf =
assert (Eva.Analysis.is_computed ());
if Datatype.String.Set.is_empty lval_str
then set
else
let zone =
Datatype.String.Set.fold
(fun lval_str acc ->
let lval_term = Logic_parse_string.term_lval kf lval_str in
let lval =
Logic_to_c.term_lval_to_lval lval_term
in
let zone = get_lval_zone eval lval in
Locations.Zone.join zone acc)
lval_str
Locations.Zone.bottom
in
select_stmt_zone set mark zone ~before ki kf
(** Add a selection of data relative to read/write accesses.
Interpret the [~rd] lvalues and the [~wr] lvalues from [~eval]
statements of [kf]:
- Variables of [lval_str] string are bounded
relatively to the whole scope of the function [kf].
- The interpretation of the address of the lvalues is
done just before the execution of the statement [~eval].
Find read/write accesses from the whole project if [ki_opt]=None.
Otherwise, restrict the research among the direct effect of [ki_opt] statement.
i.e. when [ki_opt] is a call, the selection doesn't look at the assigns clause
of a call. *)
let select_lval_rw set mark ~rd ~wr ~eval kf ki_opt=
assert (Eva.Analysis.is_computed ());
let zone_option ~for_writing lval_str =
if Datatype.String.Set.is_empty lval_str
then None
else
let zone =
Datatype.String.Set.fold
(fun lval_str acc ->
let lval_term = Logic_parse_string.term_lval kf lval_str in
let lval = Logic_to_c.term_lval_to_lval lval_term in
let zone = get_lval_zone ~for_writing eval lval in
Locations.Zone.join zone acc)
lval_str Locations.Zone.bottom
in SlicingParameters.debug ~level:3
"select_lval_rw %a zone=%a"
Kernel_function.pretty kf
Locations.Zone.pretty zone;
Some zone
in
let zone_rd_opt = zone_option ~for_writing:false rd in
let zone_wr_opt = zone_option ~for_writing:true wr in
match zone_rd_opt, zone_wr_opt with
| None, None -> set
| (_, _) as zone_option_rw ->
let ac = ref set in
let select_rw_from_stmt kf ki =
let rd_zone_opt, wr_zone_opt = Kinstr.is_rw_zone zone_option_rw ki in
let select_zone ~before zone_opt =
match zone_opt with
| None -> !ac
| Some zone ->
SlicingParameters.debug ~level:3
"select_lval_rw sid=%d before=%b zone=%a"
ki.sid before Locations.Zone.pretty zone;
select_stmt_zone !ac mark zone ~before ki kf ;
in
ac := select_zone ~before:true rd_zone_opt ;
ac := select_zone ~before:false wr_zone_opt
in (match ki_opt with
| Some ki -> select_rw_from_stmt kf ki
| None ->
Globals.Functions.iter
(fun kf ->
if Eva.Results.is_called kf then
if not (Eva.Analysis.use_spec_instead_of_definition kf)
then
Kinstr.iter_from_func (select_rw_from_stmt kf) kf
else begin
let select_inter_zone fsel zone_opt zone =
match zone_opt with
| None -> ()
| Some zone_requested ->
if Locations.Zone.intersects zone_requested zone
then let inter = Locations.Zone.narrow zone_requested zone
in fsel inter
else () in
let select_wr outputs =
ac := select_entry_point_and_some_inputs_outputs !ac ~mark kf
~return:false ~outputs ~inputs:Locations.Zone.bottom
and select_rd inputs =
ac := select_entry_point_and_some_inputs_outputs !ac ~mark kf
~return:false ~inputs ~outputs:Locations.Zone.bottom
in
assert (Eva.Results.is_called kf) ;
select_inter_zone select_wr zone_wr_opt (Inout.kf_external_outputs kf) ;
select_inter_zone select_rd zone_rd_opt (Inout.kf_external_inputs kf)
end
));
!ac
(** Registered as a slicing selection function:
Add a selection of rw accesses to lvalues relative to a statement.
Variables of [~rd] and [~wr] string are bounded
relatively to the whole scope of the function [kf].
The interpretation of the address of the lvalues is
done just before the execution of the statement [~eval].
The selection preserve the [~rd] and ~[wr] accesses
directly contained into the statement [ki].
i.e. when [ki] is a call, the selection doesn't look at
the assigns clause of the called function.
Note: add also a transparent selection on the whole statement.*)
let select_stmt_lval_rw set mark ~rd ~wr ki ~eval kf =
select_lval_rw set mark ~rd ~wr ~eval kf (Some ki)
(** Add a selection of the declaration of [vi]. *)
let select_decl_var set mark vi kf =
let selection = SlicingSelect.select_decl_var kf vi mark in
add_to_selection set selection
let select_ZoneAnnot_pragmas set ~spare pragmas kf =
let set =
Cil_datatype.Stmt.Set.fold
(fun ki' acc -> select_stmt acc ~spare ki' kf)
pragmas.Logic_deps.stmt set
in
Cil_datatype.Stmt.Set.fold
(fun ki' acc -> select_stmt_ctrl acc ~spare ki' kf)
pragmas.Logic_deps.ctrl
set
let select_ZoneAnnot_zones_decl_vars set mark (zones,decl_vars) kf =
let set =
Cil_datatype.Varinfo.Set.fold
(fun vi acc -> select_decl_var acc mark vi kf)
decl_vars.Logic_deps.var
set
in
let set =
Cil_datatype.Logic_label.Set.fold
(fun l acc ->
let selection = SlicingSelect.select_label kf l mark
in add_to_selection acc selection)
decl_vars.Logic_deps.lbl
set
in
List.fold_right
(fun z acc ->
select_stmt_zone acc mark
z.Logic_deps.zone
~before:z.Logic_deps.before
z.Logic_deps.ki
kf)
zones set
let get_or_raise (info_data_opt, info_decl) = match info_data_opt with
| None ->
SlicingParameters.not_yet_implemented
"%s" !Logic_deps.not_yet_implemented
| Some info_data -> info_data, info_decl
(** Registered as a slicing selection function:
Add selection of the annotations related to a statement.
Note: add also a transparent selection on the whole statement. *)
let select_stmt_pred set mark pred ki kf =
let zones_decl_vars =
Logic_deps.from_pred pred (Logic_deps.mk_ctx_stmt_annot kf ki)
in
select_ZoneAnnot_zones_decl_vars set mark (get_or_raise zones_decl_vars) kf
(** Registered as a slicing selection function:
Add selection of the annotations related to a statement.
Note: add also a transparent selection on the whole statement. *)
let select_stmt_term set mark term ki kf =
let zones_decl_vars =
Logic_deps.from_term term (Logic_deps.mk_ctx_stmt_annot kf ki)
in
select_ZoneAnnot_zones_decl_vars set mark (get_or_raise zones_decl_vars) kf
(** Registered as a slicing selection function:
Add selection of the annotations related to a statement.
Note: add also a transparent selection on the whole statement. *)
let select_stmt_annot set mark ~spare annot ki kf =
let zones_decl_vars,pragmas =
Logic_deps.from_stmt_annot annot (ki, kf)
in let set = select_ZoneAnnot_pragmas set ~spare pragmas kf
in select_ZoneAnnot_zones_decl_vars set mark (get_or_raise zones_decl_vars) kf
(** Registered as a slicing selection function:
Add selection of the annotations related to a statement.
Note: add also a transparent selection on the whole statement. *)
let select_stmt_annots set mark ~spare ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop_var ki kf =
let zones_decl_vars,pragmas =
Logic_deps.from_stmt_annots
(Some (Logic_deps.code_annot_filter
~threat ~user_assert ~slicing_pragma
~loop_inv ~loop_var ~others:false))
(ki, kf)
in let set = select_ZoneAnnot_pragmas set ~spare pragmas kf
in select_ZoneAnnot_zones_decl_vars set mark (get_or_raise zones_decl_vars) kf
(** Registered as a slicing selection function:
Add a selection of the annotations related to a function. *)
let select_func_annots set mark ~spare ~threat ~user_assert ~slicing_pragma ~loop_inv ~loop_var kf =
try
let zones_decl_vars,pragmas =
Logic_deps.from_func_annots Kinstr.iter_from_func
(Some
(Logic_deps.code_annot_filter
~threat ~user_assert ~slicing_pragma ~loop_inv
~loop_var ~others:false))
kf
in let set = select_ZoneAnnot_pragmas set ~spare pragmas kf
in select_ZoneAnnot_zones_decl_vars set mark (get_or_raise zones_decl_vars) kf
with Kernel_function.No_Definition ->
SlicingParameters.warning ~wkey:SlicingParameters.wkey_cmdline
"No definition for function '%a'. \
Slicing requests from the command line are ignored."
Kernel_function.pretty kf;
Cil_datatype.Varinfo.Map.empty
(** Registered as a slicing selection function:
Add selection of function outputs.
Variables of [lval_str] string are bounded
relatively to the whole scope of the function [kf].
The interpretation of the address of the lvalues is
done just before the execution of the first statement [kf].
The selection preserve the value of these lvalues before
execution of the return statement. *)
let select_func_lval set mark lval_str kf =
if Datatype.String.Set.is_empty lval_str
then set
else
let ki_scope_eval = Kernel_function.find_first_stmt kf in
select_stmt_lval
set mark lval_str
~before:false
(Kernel_function.find_return kf)
~eval:ki_scope_eval
kf
(** Registered as a slicing selection function:
Add a selection of data relative to read/write accesses.
Interpret the [~rd] lvalues and the [~wr] lvalues from [~eval]
statements of [kf]:
- Variables of [lval_str] string are bounded
relatively to the whole scope of the function [kf].
- The interpretation of the address of the lvalues is
done just before the execution of the statement [~eval].
Find read/write accesses from the whole project if [ki_opt]=None. *)
let select_func_lval_rw set mark ~rd ~wr ~eval kf =
if Datatype.String.Set.is_empty rd && Datatype.String.Set.is_empty wr
then set
else select_lval_rw set mark ~rd ~wr ~eval kf None
(** Registered as a slicing request function:
Add selections to all concerned slices, as slicing requests and apply them,
kernel function by kernel function.
Note:
- the function begins by applying the remaining internal requests.
- the requests added for the last kernel function are not applied. *)
let add_selection set =
let add_selection prev selection =
let kf = get_select_kf selection in
let r = match prev with
None -> apply_all_actions () ; Some (kf)
| Some prev_kf -> if prev_kf == kf then prev else None
and make_request slice =
SlicingSelect.add_ff_selection slice selection
and slices =
let slices = SlicingProject.get_slices kf
in if slices = [] then [SlicingProject.create_slice kf] else slices
in List.iter make_request slices ;
r
in ignore (SlicingSelect.Selections.fold_selects_internal add_selection None set)
(** Registered as a slicing request function:
Add selections that will be applied to all the slices of the function
(already existing or created later)
Note:
- the function begins by applying the remaining internal requests.
- the requests added for the last kernel function are not applied. *)
let add_persistent_selection set =
let add_selection prev selection =
let kf = get_select_kf selection in
let r = match prev with
None -> apply_all_actions () ; Some (kf)
| Some prev_kf -> if prev_kf == kf then prev else None
in SlicingSelect.add_fi_selection selection; r
in ignore (SlicingSelect.Selections.fold_selects_internal add_selection None set)
(** Registered as a slicing request function:
Add selections that will be applied to all the slices of the function
(already existing or created later)
Note:
- the function begins by applying the remaining internal requests.
- the requests added for the last kernel function are not applied. *)
let add_persistent_cmdline () =
SlicingParameters.feedback ~level:1
"interpreting slicing requests from the command line...";
begin try
let selection = ref Cil_datatype.Varinfo.Map.empty in
let top_mark = SlicingMarks.mk_user_mark ~addr:true ~ctrl:true ~data:true in
Globals.Functions.iter
(fun kf ->
let add_selection opt select =
if Kernel_function.Set.mem kf (opt ()) then
selection := select !selection ~spare:false kf
in
add_selection
SlicingParameters.Select.Return.get
select_func_return;
add_selection
SlicingParameters.Select.Calls.get
select_func_calls_to;
add_selection
SlicingParameters.Select.Pragma.get
(fun s -> select_func_annots s top_mark
~threat:false ~user_assert:false ~slicing_pragma:true
~loop_inv:false ~loop_var:false);
add_selection
SlicingParameters.Select.Threat.get
(fun s -> select_func_annots s top_mark
~threat:true ~user_assert:false ~slicing_pragma:false
~loop_inv:false ~loop_var:false);
add_selection
SlicingParameters.Select.Assert.get
(fun s -> select_func_annots s top_mark
~threat:false ~user_assert:true ~slicing_pragma:false
~loop_inv:false ~loop_var:false);
add_selection
SlicingParameters.Select.LoopInv.get
(fun s -> select_func_annots s top_mark
~threat:false ~user_assert:false ~slicing_pragma:false
~loop_inv:true ~loop_var:false);
add_selection
SlicingParameters.Select.LoopVar.get
(fun s -> select_func_annots s top_mark
~threat:false ~user_assert:false ~slicing_pragma:false
~loop_inv:false ~loop_var:true);
);
if not (Datatype.String.Set.is_empty
(SlicingParameters.Select.Value.get ()))
||
not (Datatype.String.Set.is_empty
(SlicingParameters.Select.RdAccess.get ()))
||
not (Datatype.String.Set.is_empty
(SlicingParameters.Select.WrAccess.get ()))
then begin
let kf = fst (Globals.entry_point ()) in
let ki_scope_eval = Kernel_function.find_first_stmt kf in
selection := select_func_lval !selection top_mark
(SlicingParameters.Select.Value.get ()) kf;
selection := select_func_lval_rw !selection top_mark
~rd:(SlicingParameters.Select.RdAccess.get ())
~wr:(SlicingParameters.Select.WrAccess.get ())
~eval:ki_scope_eval kf ;
SlicingParameters.Select.Value.clear () ;
SlicingParameters.Select.RdAccess.clear () ;
SlicingParameters.Select.WrAccess.clear () ;
end;
add_persistent_selection !selection;
with Logic_parse_string.Error(_loc,msg) ->
SlicingParameters.warning ~wkey:SlicingParameters.wkey_cmdline
"%s. Slicing requests from the command line are ignored." msg
end;
SlicingParameters.feedback ~level:2
"done (interpreting slicing requests from the command line)."