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
(** Slicing module public macros that should be used to avoid using the type
25
* concrete definition from other modules.
32
module T = SlicingTypes.Internals
38
(** {2 Debug and utils} *)
40
let has_debug n = Debug.has_debug Cmdline.Slicing.Mode.Verbose.get n
41
let debug n format = Debug.debug_f (has_debug n) format
43
let cbug assert_cond msg =
44
if not assert_cond then raise (SlicingTypes.Slicing_Internal_Error msg)
46
let bug msg = raise (SlicingTypes.Slicing_Internal_Error msg)
48
let sprintf = Cil.fprintf_to_string
52
let str_level_option opt = match opt with
53
| T.DontSlice -> "DontSlice"
54
| T.DontSliceButComputeMarks -> "DontSliceButComputeMarks"
55
| T.MinNbSlice -> "MinNbSlice"
56
| T.MaxNbSlice -> "MaxNbSlice"
58
let translate_num_to_slicing_level n =
61
| 1 -> T.DontSliceButComputeMarks
64
| _ -> raise SlicingTypes.WrongSlicingLevel
66
let get_default_level_option defined_function =
67
if defined_function || (Cmdline.Slicing.Mode.SliceUndef.get ()) then
68
translate_num_to_slicing_level (Cmdline.Slicing.Mode.Calls.get ())
71
let get_str_default_level_option defined_function =
72
str_level_option (get_default_level_option defined_function)
74
(** {2 Getting [fct_info] and others } *)
76
let get_proj_appli proj = proj.T.application
78
(** {4 getting [svar]} *)
80
let fi_svar fi = Kernel_function.get_vi fi.T.fi_kf
82
let ff_svar ff = fi_svar (ff.T.ff_fct)
84
(** {4 getting [fct_info]} *)
86
(** Get the fct_info if it exists or build a new fct_info. *)
87
let get_kf_fi proj kf =
88
let fct_var = Kernel_function.get_vi kf in
90
let fi = Cilutil.VarinfoHashtbl.find proj.T.functions fct_var in fi
93
try let def = Kernel_function.get_definition kf in Some def, true
94
with Kernel_function.No_Definition -> None, false
100
T.fi_level_option = get_default_level_option is_def;
101
T.fi_init_marks = None ;
103
T.fi_next_ff_num = 1;
106
Cilutil.VarinfoHashtbl.add proj.T.functions fct_var new_fi;
109
let fold_fi f acc proj =
110
Cilutil.VarinfoHashtbl.fold (fun _v fi acc -> f acc fi) proj.T.functions acc
112
let ff_fi ff = ff.T.ff_fct
114
let f_fi f = match f with
115
| T.FctSrc fct -> fct
116
| T.FctSliced ff -> ff_fi ff
118
(** {4 getting names} *)
120
let fi_name fi = let svar = fi_svar fi in svar.Cil_types.vname
122
(** get the name of the function corresponding to that slice. *)
125
let ff_id = ff.T.ff_id in
126
let fct_name = fi_name fi in
127
(fct_name ^ "_slice_" ^ (string_of_int (ff_id)))
129
let f_name f = match f with
130
| T.FctSrc fct -> fi_name fct
131
| T.FctSliced ff -> ff_name ff
133
let ff_src_name ff = fi_name (ff_fi ff)
136
Kernel_function.get_name ( PdgTypes.Pdg.get_kf pdg)
138
(** {4 getting [kernel_function]} *)
140
let get_fi_kf fi = fi.T.fi_kf
142
let get_ff_kf ff = let fi = ff_fi ff in get_fi_kf fi
144
let get_pdg_kf pdg = PdgTypes.Pdg.get_kf pdg
146
(** {4 getting PDG} *)
148
let get_fi_pdg fi = let kf = get_fi_kf fi in !Db.Pdg.get kf
150
let get_ff_pdg ff = get_fi_pdg (ff_fi ff)
152
(** {4 getting the slicing level} *)
155
let fi_slicing_level fi = fi.T.fi_level_option
157
let ff_slicing_level ff = fi_slicing_level (ff_fi ff)
159
let change_fi_slicing_level fi slicing_level =
160
fi.T.fi_level_option <- slicing_level
162
(** @raise SlicingTypes.WrongSlicingLevel if [n] is not valid.
164
let change_slicing_level proj kf n =
165
let slicing_level = translate_num_to_slicing_level n in
166
let fi = get_kf_fi proj kf in (* build if if it doesn't exist *)
167
change_fi_slicing_level fi slicing_level
169
(** {2 functions and slices} *)
171
let fi_slices fi = fi.T.fi_slices
173
(** {4 Comparisons} *)
175
let equal_fi fi1 fi2 =
176
let v1 = fi_svar fi1 in
177
let v2 = fi_svar fi2 in
180
let equal_ff ff1 ff2 = (equal_fi ff1.T.ff_fct ff2.T.ff_fct) &&
181
(ff1.T.ff_id = ff2.T.ff_id)
185
| T.FctSrc fi1, T.FctSrc fi2 -> equal_fi fi1 fi2
186
| T.FctSliced ff1, T.FctSliced ff2 -> equal_ff ff1 ff2
192
let same_call c1 c2 = (c1.sid = c2.sid)
194
let same_ff_call (f1,c1) (f2,c2) =
195
equal_ff f1 f2 && same_call c1 c2
197
let is_call_stmt stmt =
198
match stmt.skind with Instr (Call _) -> true | _ -> false
200
let get_called_kf call_stmt =
201
match call_stmt.skind with
202
| Instr (Call (_, funcexp,_,_)) ->
203
let _funcexp_dpds, called_functions =
204
!Db.Value.expr_to_kernel_function
205
~with_alarms:CilE.warn_none_mode
206
(Kstmt call_stmt) ~deps:(Some Locations.Zone.bottom) funcexp in
207
(match called_functions with | kf :: [] -> kf
208
| _ -> raise SlicingTypes.PtrCallExpr)
209
| _ -> raise (Invalid_argument "Not a call statement !")
212
let varf = Kernel_function.get_vi kf in
213
match varf.vtype with
214
TFun (_, _, is_variadic, _) -> is_variadic
215
| _ -> (bug "The variable of a kernel_function has to be a function !")
217
(** get the [fct_info] of the called function, if we know it *)
218
let get_fi_call proj call =
220
let kf = get_called_kf call in
221
if is_variadic kf then None
223
let fct_info = get_kf_fi proj kf in
225
with SlicingTypes.PtrCallExpr -> None
227
let is_src_fun_called proj kf =
228
let fi = get_kf_fi proj kf in
229
match fi.T.f_called_by with [] -> false | _ -> true
231
let is_src_fun_visible proj kf =
232
let is_fi_top fi = match fi.T.fi_top with None -> false | Some _ -> true
233
in is_src_fun_called proj kf || is_fi_top (get_kf_fi proj kf)
235
let get_calls_to_ff ff = ff.T.ff_called_by
237
let get_calls_to_src fi = fi.T.f_called_by
239
let fi_has_persistent_selection fi =
240
(match fi.T.fi_init_marks with None -> false | _ -> true)
242
let has_persistent_selection proj kf =
243
let fi = get_kf_fi proj kf in
244
fi_has_persistent_selection fi
249
compile-command: "LC_ALL=C make -C ../.. -j"
added
removed
src/slicing/slicingMacros.ml
