1
(**************************************************************************)
3
(* This file is part of Frama-C. *)
5
(* Copyright (C) 2007-2008 *)
6
(* CEA (Commissariat � l'�nergie Atomique) *)
7
(* INRIA (Institut National de Recherche en Informatique et en *)
10
(* you can redistribute it and/or modify it under the terms of the GNU *)
11
(* Lesser General Public License as published by the Free Software *)
12
(* Foundation, version 2.1. *)
14
(* It is distributed in the hope that it will be useful, *)
15
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
16
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
17
(* GNU Lesser General Public License for more details. *)
19
(* See the GNU Lesser General Public License version v2.1 *)
20
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
22
(**************************************************************************)
26
module T = SlicingTypes.Internals
27
module M = SlicingMacros
28
module U = SlicingMacros
29
module C = SlicingCmds
30
module Act = SlicingActions
32
type appli = Project.t
34
let check_call stmt is_call =
35
let err = match stmt.skind with
36
| Instr (Call _) -> not is_call
40
let str = if is_call then "not" else "" in
41
let msg = "This statement is "^str^" a call" in
42
raise (Invalid_argument msg)
45
let pretty_list pretty fmt l = List.iter (pretty fmt) l
47
let print_select fmt db_select =
48
let db_fvar, select = db_select in
49
Format.fprintf fmt "In %a : %a@."
50
Ast_info.pretty_vname db_fvar Act.print_f_crit select
52
let get_select_kf (fvar, _select) = Globals.Functions.get fvar
54
let check_db_select fvar db_select =
55
let db_fvar, select = db_select in
56
if db_fvar.vid <> fvar.vid then
58
Format.printf "slice name = %s <> select = %a@."
59
(fvar.vname) print_select db_select;
60
raise (Invalid_argument
61
"This selection doesn't belong to the given function");
65
let empty_db_select kf = (Kernel_function.get_vi kf, T.CuSelect [])
66
let top_db_select kf m = (Kernel_function.get_vi kf, T.CuTop m)
67
let check_kf_db_select kf = check_db_select (Kernel_function.get_vi kf)
68
let check_fi_db_select fi = check_db_select (M.fi_svar fi)
69
let check_ff_db_select ff = check_db_select (M.ff_svar ff)
72
Cil.log "[slicing] bottom PDG for function '%s': ignore selection"
73
(Kernel_function.get_name kf)
75
let basic_add_select kf select nodes ?(undef) nd_marks =
76
let fvar, sel = check_kf_db_select kf select in
80
let pdg = !Db.Pdg.get kf in
82
List.map (fun n -> (n, None) (*TODO: add z_part ? *)) nodes in
83
(* let nd_marks = Act.build_node_and_dpds_selection mark in *)
84
(* let nd_marks = Act.build_simple_node_selection mark in *)
85
let crit = [(nodes, nd_marks)] in
86
let sel = Act.translate_crit_to_select pdg ~to_select:sel crit in
87
let sel = match undef with None -> sel
88
| Some (undef, mark) ->
89
PdgMarks.add_undef_in_to_select sel undef mark in
90
let sel = T.CuSelect sel in
93
let select_pdg_nodes kf ?(select=empty_db_select kf) nodes mark =
94
M.debug 1 "[slicing] select_pdg_nodes@." ;
95
let nd_marks = Act.build_node_and_dpds_selection mark in
96
try basic_add_select kf select nodes nd_marks
97
with Db.Pdg.Top | Db.Pdg.Bottom ->
98
assert false (* if we have node, we must have a pdg somewhere ! *)
100
let mk_select pdg sel nodes undef mark =
101
let nd_marks = Act.build_simple_node_selection mark in
102
let crit = [(nodes, nd_marks)] in
103
let sel = Act.translate_crit_to_select pdg ~to_select:sel crit in
104
let sel = PdgMarks.add_undef_in_to_select sel undef mark in
105
let sel = T.CuSelect sel in
108
let select_stmt_zone kf ?(select=empty_db_select kf) stmt ~before loc mark =
109
M.debug 1 "[slicing] select_stmt_zone %a %s stmt %d (m=%a)@."
110
Locations.Zone.pretty loc
111
(if before then "before" else "after") stmt.sid
112
SlicingMarks.pretty_mark mark;
113
let fvar, sel = check_kf_db_select kf select in
115
| T.CuTop _ -> select
118
let pdg = !Db.Pdg.get kf in
120
!Db.Pdg.find_location_nodes_at_stmt pdg stmt before loc in
121
let sel = mk_select pdg sel nodes undef mark in
124
| Db.Pdg.NotFound -> (* stmt probably unreachable *)
125
let msg = M.sprintf "%a %s stmt %d"
126
Locations.Zone.pretty loc
127
(if before then "before" else "after") stmt.sid
128
in Format.printf "Nothing to select for %s@." msg;
130
| Db.Pdg.Top -> top_db_select kf mark
131
| Db.Pdg.Bottom -> bottom_msg kf; select
134
(** this one is similar to [select_stmt_zone] with the return statement
135
* when the function is defined, but it can also be used for undefined functions. *)
136
let select_in_out_zone ~at_end ~use_undef kf select loc mark =
137
M.debug 1 "[slicing] select zone %a (m=%a) at %s of %a@."
138
Locations.Zone.pretty loc SlicingMarks.pretty_mark mark
139
(if at_end then "end" else "begin") Kernel_function.pretty_name kf;
140
let fvar, sel = check_kf_db_select kf select in
142
| T.CuTop _ -> select
145
let pdg = !Db.Pdg.get kf in
147
if at_end then !Db.Pdg.find_location_nodes_at_end
148
else !Db.Pdg.find_location_nodes_at_begin in
149
let nodes, undef = find pdg loc in
150
let undef = if use_undef then undef else None in
151
let sel = mk_select pdg sel nodes undef mark in
154
| Db.Pdg.NotFound -> assert false
155
| Db.Pdg.Top -> top_db_select kf mark
156
| Db.Pdg.Bottom -> bottom_msg kf; select
158
let select_zone_at_end kf ?(select=empty_db_select kf) loc mark =
159
select_in_out_zone ~at_end:true ~use_undef:true kf select loc mark
161
let select_modified_output_zone kf ?(select=empty_db_select kf) loc mark =
162
select_in_out_zone ~at_end:true ~use_undef:false kf select loc mark
164
let select_zone_at_entry kf ?(select=empty_db_select kf) loc mark =
165
select_in_out_zone ~at_end:false ~use_undef:true kf select loc mark
167
let stmt_nodes_to_select pdg stmt =
169
try !Db.Pdg.find_stmt_and_blocks_nodes pdg stmt with Db.Pdg.NotFound -> []
171
(* TODO : add this when visibility of anotations are ok
173
if List.length stmt_nodes > 1 then
174
begin (* this is surely a call statement *)
175
let out_and_ctrl node =
176
let key = PdgTypes.Node.elem_key node in
178
| PdgIndex.Key.SigCallKey (_, (PdgIndex.Signature.In _))
180
| PdgIndex.Key.SigCallKey (_, (PdgIndex.Signature.InCtrl))
181
| PdgIndex.Key.SigCallKey (_, (PdgIndex.Signature.Out _))
185
List.filter out_and_ctrl stmt_nodes
191
M.debug 2 " add_stmt_nodes on stmt %d (%a)@." stmt.sid
192
(fun fmt l -> List.iter (!Db.Pdg.pretty_node true fmt) l)
196
let select_stmt_computation kf ?(select=empty_db_select kf) stmt mark =
197
M.debug 1 "[slicing] select_stmt_computation on stmt %d@." stmt.sid;
199
let pdg = !Db.Pdg.get kf in
200
let stmt_nodes = stmt_nodes_to_select pdg stmt in
201
let nd_marks = Act.build_node_and_dpds_selection mark in
202
basic_add_select kf select stmt_nodes nd_marks
203
with Db.Pdg.Top -> top_db_select kf mark
204
| Db.Pdg.Bottom -> bottom_msg kf; select
206
(** marking a call node means that a [choose_call] will have to decide that to
207
* call according to the slicing-level, but anyway, the call will be visible.
209
let select_minimal_call kf ?(select=empty_db_select kf) stmt m =
210
M.debug 1 "[slicing] select_minimal_call@.";
212
let pdg = !Db.Pdg.get kf in
213
let call = check_call stmt true in
214
let call_node = !Db.Pdg.find_call_ctrl_node pdg call in
215
let nd_marks = Act.build_simple_node_selection m in
216
basic_add_select kf select [call_node] nd_marks
217
with Db.Pdg.Top -> top_db_select kf m
218
| Db.Pdg.Bottom -> bottom_msg kf; select
220
let select_stmt_ctrl kf ?(select=empty_db_select kf) stmt =
221
M.debug 1 "[slicing] select_stmt_ctrl of sid:%d@." stmt.sid;
222
let mark = SlicingMarks.mk_user_mark ~ctrl:true ~data:false ~addr:false in
224
let pdg = !Db.Pdg.get kf in
225
let stmt_nodes = !Db.Pdg.find_simple_stmt_nodes pdg stmt in
226
let nd_marks = Act.build_ctrl_dpds_selection mark in
227
basic_add_select kf select stmt_nodes nd_marks
228
with Db.Pdg.Top -> top_db_select kf mark
229
| Db.Pdg.Bottom -> bottom_msg kf; empty_db_select kf
231
let select_entry_point kf ?(select=empty_db_select kf) mark =
232
M.debug 1 "[slicing] select_entry_point of %a@."
233
Kernel_function.pretty_name kf;
235
let pdg = !Db.Pdg.get kf in
236
let node = !Db.Pdg.find_entry_point_node pdg in
237
let nd_marks = Act.build_simple_node_selection mark in
238
basic_add_select kf select [node] nd_marks
239
with Db.Pdg.Top -> top_db_select kf mark
240
| Db.Pdg.Bottom -> bottom_msg kf; empty_db_select kf
242
let select_return kf ?(select=empty_db_select kf) mark =
243
M.debug 1 "[slicing] select_return of %a@."
244
Kernel_function.pretty_name kf;
246
let pdg = !Db.Pdg.get kf in
247
let node = !Db.Pdg.find_ret_output_node pdg in
248
let nd_marks = Act.build_simple_node_selection mark in
249
basic_add_select kf select [node] nd_marks
251
| Db.Pdg.NotFound -> (* unreachable ? *) select
252
| Db.Pdg.Top -> top_db_select kf mark
253
| Db.Pdg.Bottom -> bottom_msg kf; empty_db_select kf
256
let merge_select select1 select2 =
257
let select = match select1, select2 with
258
| T.CuTop m, _ | _, T.CuTop m -> T.CuTop m
259
| T.CuSelect select1, T.CuSelect select2 ->
260
(* TODO : we can probably do better...*)
261
T.CuSelect (select1 @ select2)
264
let merge_db_select db_select1 db_select2 =
265
let fvar, select1 = db_select1 in
266
let _, select2 = check_db_select fvar db_select2 in
267
let select = merge_select select1 select2 in
270
let empty_selects () = Cilutil.VarinfoHashtbl.create 7
272
let add_to_selects db_select hsel =
273
let vf, select = db_select in
275
try let old_selection = Cilutil.VarinfoHashtbl.find hsel vf in
276
merge_select old_selection select
277
with Not_found -> select
278
in Cilutil.VarinfoHashtbl.replace hsel vf select
280
let fold_selects f hsel acc =
281
let dof v sel acc = f (v, sel) acc in
282
Cilutil.VarinfoHashtbl.fold dof hsel acc
284
let iter_selects f hsel = fold_selects (fun s _ -> f s) hsel ()
286
(** add [hsel1] to [hsel2] *)
287
let add_selects_to_selects hsel1 hsel2 =
288
let add (vf, sel) () = add_to_selects (vf, sel) hsel2 in
289
fold_selects add hsel1 ()
291
let print_fct_stmts fmt (_proj, kf) =
293
let pdg = !Db.Pdg.get kf in
294
PrintSlice.print_fct_from_pdg fmt pdg;
295
Format.pp_print_flush fmt ()
298
let add_crit_ff_change_call proj ff_caller call f_to_call =
299
let crit = Act.mk_crit_change_call ff_caller call f_to_call in
300
SlicingProject.add_filter proj crit
302
(** change the call to call the given slice.
303
* This is a user request, so it might be the case that
304
* the new function doesn't compute enough outputs :
305
* in that case, add outputs first.
307
let call_ff_in_caller proj ~caller ~to_call =
308
let kf_caller = M.get_ff_kf caller in
309
let kf_to_call = M.get_ff_kf to_call in
310
let call_stmts = !Db.Pdg.find_call_stmts ~caller:kf_caller kf_to_call in
311
let ff_to_call = T.CallSlice to_call in
312
let add_change_call stmt =
313
add_crit_ff_change_call proj caller stmt ff_to_call ;
314
match Fct_slice.check_outputs_before_change_call proj caller
317
| [c] -> SlicingProject.add_filter proj c
320
in List.iter add_change_call call_stmts
322
let call_fsrc_in_caller proj ~caller ~to_call =
323
let kf_caller = M.get_ff_kf caller in
324
let fi_to_call = M.get_kf_fi proj to_call in
325
let kf_to_call = M.get_fi_kf fi_to_call in
326
let call_stmts = !Db.Pdg.find_call_stmts ~caller:kf_caller kf_to_call in
327
let add_change_call stmt =
328
add_crit_ff_change_call proj caller stmt (T.CallSrc (Some fi_to_call))
329
in List.iter add_change_call call_stmts
331
let call_min_f_in_caller proj ~caller ~to_call =
332
let kf_caller = M.get_ff_kf caller in
333
let pdg = U.get_ff_pdg caller in
334
let call_stmts = !Db.Pdg.find_call_stmts ~caller:kf_caller to_call in
336
List.map (fun call -> (!Db.Pdg.find_call_ctrl_node pdg call),None)
338
let m = SlicingMarks.mk_user_spare in
339
let nd_marks = Act.build_simple_node_selection m in
340
let select = Act.translate_crit_to_select pdg [(call_nodes, nd_marks)] in
341
SlicingProject.add_fct_ff_filter proj caller (T.CuSelect select)
343
let is_already_selected ff db_select =
344
let _, select = check_ff_db_select ff db_select in
346
| T.CuTop _ -> assert false
347
| T.CuSelect to_select ->
348
(* let pdg = !Db.Pdg.get (Globals.Functions.get fvar) in *)
349
let new_marks = Fct_slice.filter_already_in ff to_select in
350
M.debug 1 "[slicing] is_already_selected %a ?@."
351
!Db.Slicing.Select.pretty db_select;
352
let ok = if new_marks = [] then true else false in
353
if ok then M.debug 1 "\t--> yes@."
354
else M.debug 1 "\t--> no (missing %a)@."
355
Act.print_sel_marks_list new_marks;
358
let add_ff_selection proj ff db_select =
359
M.debug 1 "[slicing:add_ff_selection] %a to %s@."
360
!Db.Slicing.Select.pretty db_select (M.ff_name ff);
361
let _, select = check_ff_db_select ff db_select in
362
SlicingProject.add_fct_ff_filter proj ff select
364
(** add a persistant selection to the function.
365
* This might change its slicing level in order to call slices later on. *)
366
let add_fi_selection proj db_select =
367
M.debug 1 "[slicing:add_fi_selection] %a@."
368
!Db.Slicing.Select.pretty db_select;
369
let kf = get_select_kf db_select in
370
let fi = M.get_kf_fi proj kf in
371
let _, select = db_select in
372
SlicingProject.add_fct_src_filter proj fi select;
373
match M.fi_slicing_level fi with
374
| T.DontSlice | T.DontSliceButComputeMarks ->
375
M.change_fi_slicing_level fi T.MinNbSlice;
376
M.debug 1 "[slicing] changing %s slicing level to %s@."
378
(M.str_level_option (M.fi_slicing_level fi))
380
| T.MinNbSlice | T.MaxNbSlice -> ()
382
let get_mark_from_param ff var =
383
let kf = M.get_ff_kf ff in
384
let param_list = Kernel_function.get_formals kf in
385
let rec find n var_list = match var_list with
386
| [] -> raise Not_found
387
| v :: var_list -> if v.vid = var.vid then n
388
else find (n+1) var_list
389
in let n = find 1 param_list in
390
Fct_slice.get_param_mark ff n
392
let get_called_slice ff stmt =
393
match stmt.skind with
394
| Instr (Call _) -> fst (Fct_slice.get_called_slice ff stmt)
397
let get_called_funcs ff stmt =
398
match stmt.skind with
399
| Instr (Call (_,expr_f,_,_)) ->
400
if snd (Fct_slice.get_called_slice ff stmt)
401
then snd (!Db.Value.expr_to_kernel_function
403
~with_alarms:CilE.warn_none_mode
411
let db_pretty fmt (_project, kf) =
412
try !Db.Pdg.pretty fmt (!Db.Pdg.get kf)
415
let dot_project ~filename ~title project =
416
PrintSlice.build_dot_project filename title project
419
M.debug 1 "[slicing] create_slice@.";
420
SlicingProject.create_slice
421
let copy_slice _proj ff =
422
M.debug 1 "[slicing] copy_slice@.";
423
Fct_slice.copy_slice ff
425
M.debug 1 "[slicing] split_slice@.";
426
SlicingProject.split_slice
427
let merge_slices proj ff_1 ff_2 ~replace =
428
M.debug 1 "[slicing] merge_slices@.";
429
SlicingProject.merge_slices proj ff_1 ff_2 replace
431
M.debug 1 "[slicing] remove_slice@.";
432
SlicingProject.remove_ff
434
let apply_next_action =
435
M.debug 1 "[slicing] apply_next_action@.";
436
SlicingProject.apply_next_action
438
let apply_all_actions =
439
M.debug 1 "[slicing] apply_all_actions@.";
440
SlicingProject.apply_all_actions
442
(** Global data managment *)
445
type t_project_management =
446
SlicingTypes.sl_project list * SlicingTypes.sl_project option
451
include Project.Datatype.Imperative
453
type t = t_project_management
454
let copy _ = assert false (* TODO: deep copy *)
455
let name = "t_project_management"
457
let default () = [], None
460
let name = "Slicing.Project"
461
let dependencies = [ ] (* others delayed below *)
464
let get_all () = let all,_current = P.get () in all
465
let get_project () = let _all,current = P.get () in current
466
let set_project proj_opt = P.set (get_all (), proj_opt)
467
let mk_project name =
468
!Db.Value.compute () ;
469
let project = (SlicingProject.mk_project name) in
470
let all,current = P.get () in
471
P.set ((project :: all), current);
474
(** {2 Initialisation of the slicing plugin } *)
477
Options.register_plugin_init
479
let add = Project.Computation.add_dependency P.self in
481
add !Db.Inputs.self_external;
482
add !Db.Outputs.self_external)
484
(** Register external functions into Db. *)
486
Db.Slicing.self := P.self;
487
Db.Slicing.Project.mk_project := mk_project;
488
Db.Slicing.Project.get_all := get_all;
489
Db.Slicing.Project.get_project := get_project;
490
Db.Slicing.Project.set_project := set_project;
491
Db.Slicing.Project.get_name := SlicingProject.get_name;
492
Db.Slicing.Project.pretty := SlicingProject.print_project_and_worklist ;
493
Db.Slicing.Project.print_dot := dot_project ;
494
Db.Slicing.Project.extract := SlicingTransform.extract ;
495
Db.Slicing.Project.is_directly_called_internal := M.is_src_fun_called ;
496
Db.Slicing.Project.is_called := SlicingTransform.is_src_fun_called ;
497
Db.Slicing.Project.has_persistent_selection := M.has_persistent_selection ;
498
Db.Slicing.Project.change_slicing_level := M.change_slicing_level ;
500
Db.Slicing.Select.select_stmt_internal := select_stmt_computation ;
501
Db.Slicing.Select.select_entry_point_internal := select_entry_point;
502
Db.Slicing.Select.select_return_internal := select_return;
503
Db.Slicing.Select.select_min_call_internal := select_minimal_call ;
504
Db.Slicing.Select.select_stmt_ctrl_internal := select_stmt_ctrl ;
505
Db.Slicing.Select.select_stmt_zone_internal := select_stmt_zone ;
506
Db.Slicing.Select.select_zone_at_entry_point_internal := select_zone_at_entry ;
507
Db.Slicing.Select.select_zone_at_end_internal := select_zone_at_end ;
508
Db.Slicing.Select.select_modified_output_zone_internal :=
509
select_modified_output_zone ;
510
Db.Slicing.Select.select_pdg_nodes_internal := select_pdg_nodes ;
512
Db.Slicing.Select.empty_selects := empty_selects ;
513
Db.Slicing.Select.add_to_selects_internal := add_to_selects ;
514
Db.Slicing.Select.iter_selects_internal := iter_selects ;
516
Db.Slicing.Select.merge_internal := merge_db_select ;
517
Db.Slicing.Select.get_function := get_select_kf;
518
Db.Slicing.Select.pretty := print_select;
520
(* higher level function from slicingCmds *)
521
Db.Slicing.Select.select_pdg_nodes := C.select_pdg_nodes ;
522
Db.Slicing.Select.select_stmt := C.select_stmt ;
523
Db.Slicing.Select.select_stmt_ctrl := C.select_stmt_ctrl ;
524
Db.Slicing.Select.select_stmt_lval := C.select_stmt_lval ;
525
Db.Slicing.Select.select_stmt_lval_rw := C.select_stmt_lval_rw ;
526
Db.Slicing.Select.select_stmt_zone := C.select_stmt_zone ;
527
Db.Slicing.Select.select_stmt_pred := C.select_stmt_pred ;
528
Db.Slicing.Select.select_stmt_term := C.select_stmt_term ;
529
Db.Slicing.Select.select_stmt_annot := C.select_stmt_annot ;
530
Db.Slicing.Select.select_stmt_annots := C.select_stmt_annots ;
531
Db.Slicing.Select.select_func_annots := C.select_func_annots ;
532
Db.Slicing.Select.select_func_lval := C.select_func_lval ;
533
Db.Slicing.Select.select_func_lval_rw := C.select_func_lval_rw ;
534
Db.Slicing.Select.select_func_zone := C.select_func_zone ;
535
Db.Slicing.Select.select_func_return := C.select_func_return ;
536
Db.Slicing.Select.select_func_calls_to := C.select_func_calls_to ;
537
Db.Slicing.Select.select_func_calls_into := C.select_func_calls_into ;
539
Db.Slicing.Slice.create := create_slice ;
540
Db.Slicing.Slice.remove := remove_slice ;
541
Db.Slicing.Slice.remove_uncalled := SlicingProject.remove_uncalled_slices ;
542
Db.Slicing.Slice.get_all := SlicingProject.get_slices ;
543
Db.Slicing.Slice.get_callers := SlicingProject.get_slice_callers ;
544
Db.Slicing.Slice.get_called_slice := get_called_slice ;
545
Db.Slicing.Slice.get_called_funcs := get_called_funcs ;
546
Db.Slicing.Slice.pretty := SlicingProject.pretty_slice ;
547
Db.Slicing.Slice.get_mark_from_stmt := Fct_slice.get_stmt_mark;
548
Db.Slicing.Slice.get_mark_from_label := Fct_slice.get_label_mark ;
549
Db.Slicing.Slice.get_mark_from_formal := get_mark_from_param ;
550
Db.Slicing.Slice.get_mark_from_local_var := Fct_slice.get_local_var_mark ;
551
Db.Slicing.Slice.get_user_mark_from_inputs := Fct_slice.merge_inputs_m1_mark ;
552
Db.Slicing.Slice.get_callers := SlicingProject.get_slice_callers ;
553
Db.Slicing.Slice.get_function := M.get_ff_kf ;
555
(* higher level function from slicingCmds *)
556
Db.Slicing.Request.propagate_user_marks := C.topologic_propagation ;
557
Db.Slicing.Request.add_selection := C.add_selection ;
558
Db.Slicing.Request.add_persistent_selection := C.add_persistent_selection ;
559
Db.Slicing.Request.add_persistent_cmdline := C.add_persistent_cmdline ;
561
Db.Slicing.Request.is_already_selected_internal := is_already_selected ;
562
Db.Slicing.Request.add_slice_selection_internal := add_ff_selection ;
563
Db.Slicing.Request.add_selection_internal := add_fi_selection ;
564
Db.Slicing.Request.add_call_slice := call_ff_in_caller ;
565
Db.Slicing.Request.add_call_fun := call_fsrc_in_caller ;
566
Db.Slicing.Request.add_call_min_fun := call_min_f_in_caller ;
567
Db.Slicing.Request.merge_slices := merge_slices ;
568
Db.Slicing.Request.copy_slice := copy_slice ;
569
Db.Slicing.Request.split_slice := split_slice ;
570
Db.Slicing.Request.apply_next_internal := apply_next_action ;
571
Db.Slicing.Request.apply_all_internal := apply_all_actions ;
572
Db.Slicing.Request.apply_all := C.apply_all ;
573
Db.Slicing.Request.pretty := SlicingProject.print_proj_worklist ;
575
Db.Slicing.Mark.compare := SlicingMarks.compare_marks ;
576
Db.Slicing.Mark.pretty := SlicingMarks.pretty_mark ;
577
Db.Slicing.Mark.make := SlicingMarks.mk_user_mark ;
578
Db.Slicing.Mark.is_bottom := SlicingMarks.is_bottom_mark ;
579
Db.Slicing.Mark.is_spare := SlicingMarks.is_spare_mark ;
580
Db.Slicing.Mark.is_ctrl := SlicingMarks.is_ctrl_mark ;
581
Db.Slicing.Mark.is_addr := SlicingMarks.is_addr_mark ;
582
Db.Slicing.Mark.is_data := SlicingMarks.is_data_mark ;
583
Db.Slicing.Mark.is_data := SlicingMarks.is_data_mark ;
584
Db.Slicing.Mark.get_from_src_func := Fct_slice.get_mark_from_src_fun;
589
if Cmdline.Slicing.is_on () then begin
590
Format.fprintf fmt "@\n[slicing] in progress...@.";
592
(* have to do the value analysis before the selections
593
* because some functions use its results,
594
* and the value analysis is not launched automatically. *)
595
!Db.Value.compute ();
597
let project = !Db.Slicing.Project.mk_project "Slicing" in
598
!Db.Slicing.Project.set_project (Some project);
599
!Db.Slicing.Request.add_persistent_cmdline project;
601
(* Apply all pending requests. *)
602
if Cmdline.Slicing.Mode.Verbose.get () > 2 then
603
Format.fprintf fmt "[slicing] requests:@\n %a@\n"
604
!Db.Slicing.Request.pretty project ;
605
!Db.Slicing.Request.apply_all_internal project;
607
if Cmdline.Slicing.Mode.Callers.get () then
608
!Db.Slicing.Slice.remove_uncalled project;
611
!Db.Slicing.Project.extract
612
(!Db.Slicing.Project.get_name project ^ " export")
615
if Cmdline.Slicing.Print.get () then begin
616
File.pretty (Cmdline.CodeOutput.get_fmt ()) ~prj:sliced_project;
617
if Cmdline.Slicing.Mode.Verbose.get () > 0 then
618
Format.fprintf fmt "Slicing result :@. %a@."
619
!Db.Slicing.Project.pretty project
622
Format.fprintf fmt "@\n====== SLICED CODE COMPUTED ======@.";
625
let () = Db.Main.extend main
627
(** Register the plugin options *)
629
Options.add_plugin ~name:"slicing" ~descr:"slicing analysis"
632
Arg.Unit Cmdline.Slicing.Print.on,
633
": pretty print the sliced code";
635
"-slice-undef-functions",
636
Arg.Unit Cmdline.Slicing.Mode.SliceUndef.on,
638
^ (if Cmdline.Slicing.Mode.SliceUndef.get () then "by default, " else "")
639
^ "allow the use of the -slicing-level option for calls to undefined functions";
641
"-no-slice-undef-functions",
642
Arg.Unit Cmdline.Slicing.Mode.SliceUndef.off,
644
^ (if Cmdline.Slicing.Mode.SliceUndef.get () then "" else "by default, ")
645
^ "don't slice the prototype of undefined functions";
648
Arg.Int (fun n -> match n with
649
| 0 | 1 | 2 | 3 -> Cmdline.Slicing.Mode.Calls.set n
651
(Arg.Help ("Invalid argument for -slicing-level option:" ^
652
" not in range [0-3]\n"))
654
"n : set the default level of slicing used to propagate to the calls\n"
655
^"\t0 : don't slice the called functions\n"
656
^"\t1 : don't slice the called functions but propagate the marks anyway\n"
657
^"\t2 : try to use existing slices, create at most one\n"
658
^"\t3 : most precise slices\n"
660
^ (Format.sprintf " (defaults to %d) " (Cmdline.Slicing.Mode.Calls.get ()))
661
^"is not used for calls to undefined functions\n"
662
^"\texcept when '-slice-undef-functions' option is set."
663
^"\n"; (* A new line as separator for
664
next options related to slicing requests.
665
Alphabetic order is used for them. *)
668
Arg.String Cmdline.Slicing.Select.Assert.add_set,
669
"f1,...,fn : select the assertions of functions f1,...,fn";
672
Arg.String Cmdline.Slicing.Select.Calls.add_set,
673
"f1,...,fn : select every calls to functions f1,...,fn, and all their effect";
676
Arg.String Cmdline.Slicing.Select.LoopInv.add_set,
677
"f1,...,fn : select the loop invariants of functions f1,...,fn";
680
Arg.String Cmdline.Slicing.Select.LoopVar.add_set,
681
"f1,...,fn : select the loop variants of functions f1,...,fn";
684
Arg.String Cmdline.Slicing.Select.Pragma.add_set,
685
"f1,...,fn : use the slicing pragmas in the code of functions f1,...,fn as slicing criteria\n"
686
^"\t//@slice pragma ctrl; : to reach this control-flow point\n"
687
^"\t//@slice pragma expr <expr_desc;> : to preserve the value of an expression at this control-flow point\n"
688
^"\t//@slice pragma stmt; : to preserve the effect of the next statement";
691
Arg.String Cmdline.Slicing.Select.Return.add_set,
692
"f1,...,fn : select the result (returned value) of functions f1,...,fn";
695
Arg.String Cmdline.Slicing.Select.Threat.add_set,
696
"f1,...,fn : select the threats of functions f1,...,fn";
699
Arg.String Cmdline.Slicing.Select.Value.add_set,
700
"v1,...,vn : select the result of left-values v1,...,vn at the end of the function given as entry point\n"
701
^"\t (addresses are evaluated at the beginning of the function given as entry point)";
704
Arg.String Cmdline.Slicing.Select.RdAccess.add_set,
705
"v1,...,vn : select the read accesses to left-values v1,...,vn\n"
706
^"\t (addresses are evaluated at the beginning of the function given as entry point)";
709
Arg.String Cmdline.Slicing.Select.WrAccess.add_set,
710
"v1,...,vn : select the write accesses to left-values v1,...,vn\n"
711
^"\t (addresses are evaluated at the beginning of the function given as entry point)"
712
^"\n"; (* A new line as separator for
713
next options related to debug. *)
716
Arg.Int Cmdline.Slicing.Mode.Verbose.set,
717
" n : set the level of slicing debug to n";
720
Arg.Unit Cmdline.Slicing.Mode.Verbose.incr,
721
": increment the level of slicing debug";
724
Arg.Unit Cmdline.Slicing.Mode.Callers.off,
725
": don't propagate the slicing to the function callers";
added
removed
src/slicing/register.ml
