package frama-c

  1. Overview
  2. Docs
package frama-c
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file slicingMacros.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2024                                               *)
(*    CEA (Commissariat à l'énergie atomique et aux énergies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It is distributed in the hope that it will be useful,                 *)
(*  but WITHOUT ANY WARRANTY; without even the implied warranty of        *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the         *)
(*  GNU Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(** Slicing  module public macros that should be used to avoid  using the type
 * concrete definition from other modules.
*)

(**/**)

open Cil_types

open Pdg_types

(**/**)

(** {2 Options} *)

let str_level_option opt = match opt with
  |  SlicingInternals.DontSlice -> "DontSlice"
  |  SlicingInternals.DontSliceButComputeMarks -> "DontSliceButComputeMarks"
  |  SlicingInternals.MinNbSlice -> "MinNbSlice"
  |  SlicingInternals.MaxNbSlice -> "MaxNbSlice"

let translate_num_to_slicing_level n =
  match n with
  | 0 -> SlicingInternals.DontSlice
  | 1 -> SlicingInternals.DontSliceButComputeMarks
  | 2 -> SlicingInternals.MinNbSlice
  | 3 -> SlicingInternals.MaxNbSlice
  | _ -> raise SlicingTypes.WrongSlicingLevel

let get_default_level_option defined_function =
  if defined_function || (SlicingParameters.Mode.SliceUndef.get ()) then
    translate_num_to_slicing_level (SlicingParameters.Mode.Calls.get ())
  else SlicingInternals.DontSlice


(** {2 Getting [fct_info] and others } *)

(** {4 getting [svar]} *)

let fi_svar fi = Kernel_function.get_vi fi.SlicingInternals.fi_kf

let ff_svar ff = fi_svar (ff.SlicingInternals.ff_fct)

(** {4 getting [fct_info]} *)

(** Get the fct_info if it exists or build a new fct_info. *)
let get_kf_fi kf =
  let fct_var = Kernel_function.get_vi kf in
  let proj = SlicingState.get () in
  try Cil_datatype.Varinfo.Hashtbl.find proj.SlicingInternals.functions fct_var
  with Not_found ->
    let fi_def, is_def =
      match kf.fundec with
      | Declaration _ -> None, false
      | Definition _ when Eva.Analysis.use_spec_instead_of_definition kf ->
        None, false
      | Definition (def, _) -> Some def, true
    in
    let new_fi = {
      SlicingInternals.fi_kf = kf;
      SlicingInternals.fi_def = fi_def;
      SlicingInternals.fi_top = None;
      SlicingInternals.fi_level_option = get_default_level_option is_def;
      SlicingInternals.fi_init_marks = None ;
      SlicingInternals.fi_slices = [] ;
      SlicingInternals.fi_next_ff_num = 1;
      SlicingInternals.f_called_by = [] }
    in
    Cil_datatype.Varinfo.Hashtbl.add proj.SlicingInternals.functions fct_var new_fi;
    new_fi

let fold_fi f acc =
  let proj = SlicingState.get () in
  Cil_datatype.Varinfo.Hashtbl.fold
    (fun _v fi acc -> f acc fi)
    proj.SlicingInternals.functions
    acc



(** {4 getting num id} *)
let get_ff_id ff = ff.SlicingInternals.ff_id

(** {4 getting names} *)

let fi_name fi = let svar = fi_svar fi in svar.Cil_types.vname

(** get the name of the function corresponding to that slice. *)
let ff_name ff =
  let fi = ff.SlicingInternals.ff_fct in
  let ff_id = get_ff_id ff in
  let fct_name = fi_name fi in
  (fct_name ^ "_slice_" ^ (string_of_int (ff_id)))

let f_name f = match f with
  | SlicingInternals.FctSrc fct -> fi_name fct
  | SlicingInternals.FctSliced ff -> ff_name ff

let ff_src_name ff = fi_name ff.SlicingInternals.ff_fct

(** {4 getting [kernel_function]} *)

let get_fi_kf fi = fi.SlicingInternals.fi_kf

let get_ff_kf ff =  let fi = ff.SlicingInternals.ff_fct in get_fi_kf fi

let get_pdg_kf pdg = PdgTypes.Pdg.get_kf pdg

(** {4 getting PDG} *)

let get_fi_pdg fi = let kf = get_fi_kf fi in  Pdg.Api.get kf

let get_ff_pdg ff = get_fi_pdg ff.SlicingInternals.ff_fct

(** {4 getting the slicing level} *)


let ff_slicing_level ff = ff.SlicingInternals.ff_fct.SlicingInternals.fi_level_option

let change_fi_slicing_level fi slicing_level =
  fi.SlicingInternals.fi_level_option <- slicing_level

(** @raise SlicingTypes.WrongSlicingLevel if [n] is not valid.
 * *)
let change_slicing_level kf n =
  let slicing_level = translate_num_to_slicing_level n in
  let fi = get_kf_fi kf in (* build if if it doesn't exist *)
  change_fi_slicing_level fi slicing_level

(** {2 functions and slices} *)

let fi_slices fi = fi.SlicingInternals.fi_slices

(** {4 Comparisons} *)

let equal_fi fi1 fi2 =
  let v1 = fi_svar fi1 in
  let v2 = fi_svar fi2 in
  Cil_datatype.Varinfo.equal v1 v2

let equal_ff ff1 ff2 = (equal_fi ff1.SlicingInternals.ff_fct ff2.SlicingInternals.ff_fct) &&
                       ((get_ff_id ff1) = (get_ff_id ff2))


(** {2 Calls} *)

let same_call c1 c2 = (c1.sid = c2.sid)

let same_ff_call (f1,c1) (f2,c2) =
  equal_ff f1 f2 && same_call c1 c2

let is_call_stmt stmt =
  match stmt.skind with
  | Instr (Call _ | Local_init(_, ConsInit _,_)) -> true | _ -> false

let get_called_kf call_stmt = match call_stmt.skind with
  | Instr (Call _) ->
    (match Eva.Results.callee call_stmt with
     | [kf] -> kf
     | _ -> raise SlicingTypes.PtrCallExpr)
  | Instr (Local_init(_, ConsInit (f, _, _), _)) -> Globals.Functions.get f
  | _ -> invalid_arg "Not a call statement !"

let is_variadic kf =
  let varf = Kernel_function.get_vi kf in
  match varf.vtype with
  | TFun (_, _, is_variadic, _) -> is_variadic
  | _ -> assert false

(** get the [fct_info] of the called function, if we know it *)
let get_fi_call call =
  try
    let kf = get_called_kf call in
    if is_variadic kf then None
    else
      let fct_info = get_kf_fi kf in
      Some fct_info
  with SlicingTypes.PtrCallExpr -> None

let is_src_fun_called kf =
  let fi = get_kf_fi kf in
  match fi.SlicingInternals.f_called_by with [] -> false | _ -> true

let is_src_fun_visible kf =
  let is_fi_top fi = match fi.SlicingInternals.fi_top with None -> false | Some _ -> true
  in is_src_fun_called kf || is_fi_top (get_kf_fi kf)

let fi_has_persistent_selection fi =
  (match fi.SlicingInternals.fi_init_marks with None -> false | _ -> true)

let has_persistent_selection kf =
  let fi = get_kf_fi kf in
  fi_has_persistent_selection fi


(*
Local Variables:
compile-command: "make -C ../../.."
End:
*)
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct