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
(**************************************************************************)
24
(** Export the slicing project *)
31
module T = SlicingTypes.Internals
32
module M = SlicingMacros
37
(*let m = Fct_slice.get_top_input_mark fi in*)
38
fi.T.fi_top (* || not (!Db.Slicing.Mark.is_bottom m) *)
40
(* Look at (only once) the callers of [kf] ([kf] included). *)
41
let exists_fun_callers fpred kf =
42
let table = ref VarinfoSet.empty in
43
let rec exists_fun_callers kf =
46
else let vf = Kernel_function.get_vi kf in
47
if VarinfoSet.mem vf !table
48
then false (* no way to call the initial [kf]. *)
50
(table := VarinfoSet.add vf !table ;
51
List.exists (fun (kf,_) -> exists_fun_callers kf) (!Db.Value.callers kf))
52
in exists_fun_callers kf
54
let is_src_fun_visible prj = exists_fun_callers (M.is_src_fun_visible prj)
56
let is_src_fun_called prj kf =
57
let kf_entry, _library = Globals.entry_point () in
60
then M.is_src_fun_visible prj f (* for the entry point *)
61
else M.is_src_fun_called prj f (* for the others *)
62
in exists_fun_callers fpred kf
64
module Visibility (SliceName : sig
65
val get : Db_types.kernel_function -> bool -> int -> string
67
type t_proj = T.t_project
69
Iff of (T.t_fct_slice * bool)
70
(* the boolean says if the src function of the slice is visible
71
* and can be used to give names *)
75
let fct_info project kf =
76
let fi = M.get_kf_fi project kf in
77
let slices = M.fi_slices fi in
78
let src_visible = is_src_fun_visible project kf in
79
M.debug 1 "[slicing:export] processing %a (%d slices/src %svisible)@."
80
Kernel_function.pretty_name kf (List.length slices)
81
(if src_visible then "" else "not ");
82
let need_addr = (Kernel_function.get_vi kf).vaddrof in
83
let src_name_used = src_visible || need_addr in
84
let info_list = List.map (fun ff -> Iff (ff, src_name_used)) slices in
85
if src_visible then Isrc :: info_list
86
else if need_addr then Iproto :: info_list (* TODO for #344 *)
89
let fct_name svar ff =
90
let name = match ff with
94
| Iff (ff, src_visible) ->
95
let kf = M.get_ff_kf ff in
96
let ff_num = ff.T.ff_id in
97
SliceName.get kf src_visible ff_num
99
M.debug 2 "[slicing:export] get fct_name = %s@." name;
102
let visible_mark m = not (!Db.Slicing.Mark.is_bottom m)
104
let param_visible ff_opt n = match ff_opt with
105
| Isrc | Iproto -> true
106
| Iff (ff,_) -> visible_mark (Fct_slice.get_param_mark ff n)
108
let body_visible ff_opt = match ff_opt with
109
| Iproto -> false | Isrc | Iff _ -> true
111
let inst_visible ff_opt inst = match ff_opt with
115
let m = !Db.Slicing.Slice.get_mark_from_stmt ff inst in
118
let label_visible ff_opt inst label = match ff_opt with
122
let m = !Db.Slicing.Slice.get_mark_from_label ff inst label in
125
let data_in_visible ff data_in = match data_in with
128
(* it is too difficult to know if the callers of this slice
129
* compute [data_in] or not, but let's see if, by chance,
130
* some data have been selected manually... *)
131
let m = Fct_slice.get_input_loc_under_mark ff data_in in
132
if !Db.Slicing.Mark.is_bottom m then
134
M.debug 2 "[Slicing:annotation_visible] data %a invisible@."
135
Locations.Zone.pretty data_in;
140
let data_nodes_visible ff (data_nodes, data_in) =
141
let visible = data_in_visible ff data_in in
142
let is_data_visible visi (n,z) =
143
let key = PdgTypes.Node.elem_key n in
144
let key = match z, key with
145
| Some z, PdgIndex.Key.SigCallKey
146
(call, PdgIndex.Signature.Out
147
(PdgIndex.Signature.OutLoc out_z)) ->
148
let z = Locations.Zone.narrow z out_z in
149
PdgIndex.Key.call_output_key (PdgIndex.Key.call_from_id call) z
152
let m = Fct_slice.get_node_key_mark ff key in
153
if !Db.Slicing.Mark.is_bottom m then
155
M.debug 2 "[slicing:annotation_visible] node %a invisible@."
156
(!Db.Pdg.pretty_node true) n;
161
let data_visible = List.fold_left is_data_visible visible data_nodes in
164
let annotation_visible ff_opt stmt ~before annot =
165
M.debug 2 "[slicing:annotation_visible] ?@.";
170
let kf = M.get_ff_kf ff in
171
let pdg = !Db.Pdg.get kf in
173
let ctrl_nodes, data_info =
174
!Db.Pdg.find_code_annot_nodes pdg before stmt annot in
175
let is_visible visi n =
176
let m = Fct_slice.get_node_mark ff n in
177
if !Db.Slicing.Mark.is_bottom m then
179
M.debug 3 "[slicing:annotation_visible] node %a invisible@."
180
(!Db.Pdg.pretty_node true) n;
185
let ctrl_visible = List.fold_left is_visible true ctrl_nodes in
186
let data_visible = data_nodes_visible ff data_info in
187
let visible = (ctrl_visible && data_visible) in
188
M.debug 2 "[Slicing:annotation_visible] -> %s@."
189
(if visible then "yes" else "no");
191
with Extlib.NotYetImplemented _ -> (* TODO remove this when ok *)
193
"[slicing:annotation_visible] not implemented -> invisible";
196
let fun_precond_visible ff_opt p =
197
M.debug 2 "[slicing:fun_precond_visible] %a ?@."
198
!Ast_printer.d_predicate_named
199
{ name = []; loc = locUnknown; content = p };
200
let visible = match ff_opt with
204
let kf = M.get_ff_kf ff in
205
let pdg = !Db.Pdg.get kf in
207
let data_info = !Db.Pdg.find_fun_precond_nodes pdg p in
208
data_nodes_visible ff data_info
209
with Extlib.NotYetImplemented _ -> (* TODO remove this when ok *)
210
true (* keep visible at the moment : needed by security analysis *)
211
in M.debug 2 "[Slicing:precond_visible] -> %s@."
212
(if visible then "yes" else "no");
215
let fun_postcond_visible ff_opt p =
216
M.debug 2 "[slicing:fun_postcond_visible] %a ?@."
217
!Ast_printer.d_predicate_named
218
{ name = []; loc = locUnknown; content = p };
219
let visible = match ff_opt with
223
let kf = M.get_ff_kf ff in
224
let pdg = !Db.Pdg.get kf in
226
let data_info = !Db.Pdg.find_fun_postcond_nodes pdg p in
227
data_nodes_visible ff data_info
228
with Extlib.NotYetImplemented _ -> (* TODO remove this when ok *)
229
true (* keep visible at the moment : needed by security analysis *)
230
in M.debug 2 "[slicing:fun_postcond_visible] -> %s@."
231
(if visible then "yes" else "no");
234
let fun_variant_visible ff_opt v =
235
M.debug 2 "[slicing:fun_variant_visible] %a ?@."
236
!Ast_printer.d_term v ;
237
let visible = match ff_opt with
241
let kf = M.get_ff_kf ff in
242
let pdg = !Db.Pdg.get kf in
244
let data_info = !Db.Pdg.find_fun_variant_nodes pdg v in
245
data_nodes_visible ff data_info
246
with Extlib.NotYetImplemented _ -> (* TODO remove this when ok *)
248
in M.debug 2 "[slicing:fun_variant_visible] -> %s@."
249
(if visible then "yes" else "no");
252
let fun_assign_visible _ff_opt _v =
253
M.debug 2 "[slicing:fun_assign_visible] ?@.";
254
let visible = (* TODO *) false
255
in M.debug 2 "[slicing:fun_assign_visible] -> %s@."
256
(if visible then "yes" else "no");
259
let loc_var_visible ff_opt var = match ff_opt with
263
let m = !Db.Slicing.Slice.get_mark_from_local_var ff var in
266
let res_call_visible ff call_stmt = match ff with
270
let key = PdgIndex.Key.call_outret_key call_stmt in
271
let _, ff_marks = slice.T.ff_marks in
273
let m = PdgIndex.FctIndex.find_info ff_marks key in
275
with PdgIndex.NotFound -> false
277
let result_visible _kf ff = match ff with
278
| Isrc | Iproto -> true
280
let key = PdgIndex.Key.output_key in
281
let _, ff_marks = slice.T.ff_marks in
283
let m = PdgIndex.FctIndex.find_info ff_marks key in
285
with PdgIndex.NotFound -> false
287
let called_info (project, ff) call_stmt =
288
let info = match ff with
289
| Isrc | Iproto -> None
292
let _, ff_marks = slice.T.ff_marks in
294
PdgIndex.FctIndex.find_call ff_marks call_stmt in
296
| None | Some (None) ->
297
Format.printf "Undefined called function call-%d\n"
300
| Some (Some (T.CallSrc _)) -> None
301
| Some (Some (T.CallSlice ff)) ->
302
let kf_ff = M.get_ff_kf ff in
303
let src_visible = is_src_fun_visible project kf_ff in
304
(Some (kf_ff, Iff (ff, src_visible)))
305
with PdgIndex.NotFound ->
306
(* the functor should call [called_info] only for visible calls *)
309
M.debug 2 "[slicing:export] called_info stmt %d -> %s@."
310
call_stmt.sid (if info = None then "src" else "some slice");
314
let default_slice_names kf _src_visible ff_num =
315
let fname = Kernel_function.get_name kf in
316
let kf_entry,_ = Globals.entry_point () in
317
if Kernel_function.equal kf kf_entry then fname
318
else (fname ^ "_slice_" ^ (string_of_int (ff_num)))
320
let extract new_proj_name ?(f_slice_names=default_slice_names) slicing_project =
321
M.debug 0 "[slicing] export to '%s'@." new_proj_name;
322
!Db.Slicing.Request.apply_all_internal slicing_project;
323
let fresh_project = Project.create new_proj_name in
324
let module S = struct let get = f_slice_names end in
325
let module Visi = Visibility (S) in
326
let module Transform = Filter.F (Visi) in
327
Transform.build_cil_file fresh_project slicing_project;
328
let ctx = Cmdline.get_selection_context () in
329
Project.copy ~only:ctx fresh_project;
330
!Db.Sparecode.rm_unused_globals ~project:fresh_project ();
335
compile-command: "make -C ../.."
added
removed
src/slicing/slicingTransform.ml
