package frama-c

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

Source file slicingSelect.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
(**************************************************************************)
(*                                                                        *)
(*  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).            *)
(*                                                                        *)
(**************************************************************************)

open Cil_types
open Cil_datatype

open Pdg_types

(* ---------------------------------------------------------------------- *)
(** {1 For internal use} *)

let check_call stmt is_call =
  let err = match stmt.skind with
    | Instr (Call _ | Local_init(_, ConsInit _,_)) -> not is_call
    | _ -> is_call
  in
  if err then
    let str = if is_call then "not" else "" in
    let msg = "This statement is "^str^" a call" in
    raise (Invalid_argument msg)
  else stmt

let print_select fmt db_select =
  let db_fvar, select = db_select in
  Format.fprintf fmt "In %a : %a"
    Varinfo.pretty db_fvar SlicingActions.print_f_crit select

let get_select_kf (fvar, _select) = Globals.Functions.get fvar

let check_db_select fvar db_select =
  let db_fvar, select = db_select in
  if not (Cil_datatype.Varinfo.equal db_fvar fvar) then
    begin
      SlicingParameters.debug
        "slice name = %s <> select = %a@."
        (fvar.vname) print_select db_select ;
      raise (Invalid_argument
               "This selection doesn't belong to the given function");
    end;
  fvar, select

let empty_db_select kf = (Kernel_function.get_vi kf, SlicingInternals.CuSelect [])
let top_db_select kf m = (Kernel_function.get_vi kf, SlicingInternals.CuTop m)
let check_kf_db_select kf = check_db_select (Kernel_function.get_vi kf)
let _check_fi_db_select fi = check_db_select (SlicingMacros.fi_svar fi)
let check_ff_db_select ff = check_db_select (SlicingMacros.ff_svar ff)

let bottom_msg kf =
  SlicingParameters.feedback
    "bottom PDG for function '%s': ignore selection"
    (Kernel_function.get_name kf)

let basic_add_select kf select nodes ?(undef) nd_marks =
  let fvar, sel = check_kf_db_select kf select in
  match sel with
  | SlicingInternals.CuTop _ -> select
  | SlicingInternals.CuSelect sel ->
    let pdg = Pdg.Api.get kf in
    let nodes =
      List.map (fun n -> (n, None) (*TODO: add z_part ? *)) nodes in
    (* let nd_marks = SlicingActions.build_node_and_dpds_selection mark in *)
    (* let nd_marks = SlicingActions.build_simple_node_selection mark in *)
    let crit = [(nodes, nd_marks)] in
    let sel = SlicingActions.translate_crit_to_select pdg ~to_select:sel crit  in
    let sel = match undef with None -> sel
                             | Some (undef, mark) ->
                               PdgMarks.add_undef_in_to_select sel undef mark in
    let sel = SlicingInternals.CuSelect sel in
    (fvar, sel)

let select_pdg_nodes kf ?(select=empty_db_select kf) nodes mark =
  SlicingParameters.debug ~level:1 "[Register.select_pdg_nodes]" ;
  let nd_marks = SlicingActions.build_node_and_dpds_selection mark in
  try basic_add_select kf select nodes nd_marks
  with Pdg.Api.Top | Pdg.Api.Bottom ->
    assert false (* if we have node, we must have a pdg somewhere ! *)

let mk_select pdg sel nodes undef mark =
  let nd_marks = SlicingActions.build_simple_node_selection mark in
  let crit = [(nodes, nd_marks)] in
  let sel = SlicingActions.translate_crit_to_select pdg ~to_select:sel crit in
  let sel = PdgMarks.add_undef_in_to_select sel undef mark in
  let sel = SlicingInternals.CuSelect sel in
  sel

let select_stmt_zone kf ?(select=empty_db_select kf) stmt ~before loc mark =
  SlicingParameters.debug ~level:1 "[Register.select_stmt_zone] %a %s stmt %d (m=%a)"
    Locations.Zone.pretty loc
    (if before then "before" else "after") stmt.sid
    SlicingMarks.pretty_mark mark;
  if not (Eva.Results.is_reachable stmt) then
    begin
      SlicingParameters.feedback
        "@[Nothing to select for @[%a@]@ %s unreachable stmt of %a@]"
        Locations.Zone.pretty loc
        (if before then "before" else "after")
        Kernel_function.pretty kf;
      select
    end
  else
    let fvar, sel = check_kf_db_select kf select in
    match sel with
    | SlicingInternals.CuTop _ -> select
    | SlicingInternals.CuSelect sel ->
      try
        let pdg = Pdg.Api.get kf in
        let nodes, undef =
          Pdg.Api.find_location_nodes_at_stmt pdg stmt ~before loc in
        let sel = mk_select pdg sel nodes undef mark in
        (fvar, sel)
      with
      | Not_found -> (* stmt probably unreachable *)
        SlicingParameters.feedback
          "@[Nothing to select for @[%a@]@ %s required stmt in %a@]"
          Locations.Zone.pretty loc
          (if before then "before" else "after")
          Kernel_function.pretty kf;
        SlicingParameters.debug
          "@[Nothing to select for @[%a@]@ %s stmt %d in %a@]"
          Locations.Zone.pretty loc
          (if before then "before" else "after") stmt.sid
          Kernel_function.pretty kf;
        select
      | Pdg.Api.Top -> top_db_select kf mark
      | Pdg.Api.Bottom -> bottom_msg kf; select


(** this one is similar to [select_stmt_zone] with the return statement
 * when the function is defined, but it can also be used for undefined functions. *)
let select_in_out_zone ~at_end ~use_undef kf select loc mark =
  SlicingParameters.debug
    "[Register.select_in_out_zone] select zone %a (m=%a) at %s of %a"
    Locations.Zone.pretty loc SlicingMarks.pretty_mark mark
    (if at_end then "end" else "begin") Kernel_function.pretty kf;
  let fvar, sel = check_kf_db_select kf select in
  match sel with
  | SlicingInternals.CuTop _ -> select
  | SlicingInternals.CuSelect sel ->
    try
      let pdg = Pdg.Api.get kf in
      let find =
        if at_end then Pdg.Api.find_location_nodes_at_end
        else Pdg.Api.find_location_nodes_at_begin in
      let nodes, undef = find pdg loc in
      let undef = if use_undef then undef else None in
      let sel = mk_select pdg sel nodes undef mark in
      (fvar, sel)
    with
    | Not_found -> (* in or out unreachable ? *)
      SlicingParameters.feedback
        "@[Nothing to select for zone %a (m=%a) at %s of %a@]"
        Locations.Zone.pretty loc SlicingMarks.pretty_mark mark
        (if at_end then "end" else "begin") Kernel_function.pretty kf;
      select
    | Pdg.Api.Top -> top_db_select kf mark
    | Pdg.Api.Bottom -> bottom_msg kf; select

let select_zone_at_end kf  ?(select=empty_db_select kf) loc mark =
  select_in_out_zone ~at_end:true ~use_undef:true kf select loc mark

let select_modified_output_zone kf  ?(select=empty_db_select kf) loc mark =
  select_in_out_zone ~at_end:true ~use_undef:false kf select loc mark

let select_zone_at_entry kf  ?(select=empty_db_select kf) loc mark =
  select_in_out_zone ~at_end:false ~use_undef:true kf select loc mark

let stmt_nodes_to_select pdg stmt =
  try
    let stmt_nodes = Pdg.Api.find_stmt_and_blocks_nodes pdg stmt in
    SlicingParameters.debug ~level:2 "[Register.stmt_nodes_to_select] results on stmt %d (%a)" stmt.sid
      (fun fmt l -> List.iter (Pdg.Api.pretty_node true fmt) l)
      stmt_nodes;
    stmt_nodes
  with Not_found ->
    SlicingParameters.debug ~level:2 "[Register.stmt_nodes_to_select] no results for stmt %d, probably unreachable" stmt.sid;
    []

let select_stmt_computation kf ?(select=empty_db_select kf) stmt mark =
  SlicingParameters.debug ~level:1 "[Register.select_stmt_computation] on stmt %d" stmt.sid;
  if not (Eva.Results.is_reachable stmt) then
    begin
      SlicingParameters.feedback
        "@[Nothing to select for an unreachable stmt of %a@]"
        Kernel_function.pretty kf;
      select
    end
  else
    try
      let pdg = Pdg.Api.get kf in
      let stmt_nodes = stmt_nodes_to_select pdg stmt in
      let nd_marks = SlicingActions.build_node_and_dpds_selection mark in
      basic_add_select kf select stmt_nodes nd_marks
    with Pdg.Api.Top -> top_db_select kf mark
       | Pdg.Api.Bottom -> bottom_msg kf; select

let select_label kf ?(select=empty_db_select kf) label mark =
  SlicingParameters.debug ~level:1 "[Register.select_label] on label "
  (* Logic_label.pretty label *);
  try
    let pdg = Pdg.Api.get kf in
    let nodes =
      let add_label_nodes l acc = match l with
        | StmtLabel stmt ->
          let add acc l =
            try Pdg.Api.find_label_node pdg !stmt l :: acc
            with Not_found -> acc
          in
          List.fold_left add acc (!stmt).labels
        | FormalLabel _ | BuiltinLabel _ -> acc
      in
      (* Logic_label.Set.fold add_label_nodes labels [] *)
      add_label_nodes label []
    in
    let nd_marks = SlicingActions.build_node_and_dpds_selection mark in
    basic_add_select kf select nodes nd_marks
  with Pdg.Api.Top -> top_db_select kf mark
     | Pdg.Api.Bottom -> bottom_msg kf; select

(** marking a call node means that a [choose_call] will have to decide that to
 * call according to the slicing-level, but anyway, the call will be visible.
*)
let select_minimal_call kf ?(select=empty_db_select kf) stmt m =
  SlicingParameters.debug ~level:1 "[Register.select_minimal_call]";
  try
    let pdg = Pdg.Api.get kf in
    let call = check_call stmt true in
    let call_node = Pdg.Api.find_call_ctrl_node pdg call in
    let nd_marks = SlicingActions.build_simple_node_selection m in
    basic_add_select kf select [call_node] nd_marks
  with Pdg.Api.Top -> top_db_select kf m
     | Pdg.Api.Bottom -> bottom_msg kf; select

let select_stmt_ctrl kf ?(select=empty_db_select kf) stmt =
  SlicingParameters.debug ~level:1 "[Register.select_stmt_ctrl] of sid:%d" stmt.sid;
  let mark = SlicingMarks.mk_user_mark ~ctrl:true ~data:false ~addr:false in
  try
    let pdg = Pdg.Api.get kf in
    let stmt_nodes = Pdg.Api.find_simple_stmt_nodes pdg stmt in
    let nd_marks = SlicingActions.build_ctrl_dpds_selection mark in
    basic_add_select kf select stmt_nodes nd_marks
  with Pdg.Api.Top -> top_db_select kf mark
     | Pdg.Api.Bottom -> bottom_msg kf; empty_db_select kf

let select_entry_point kf ?(select=empty_db_select kf) mark =
  SlicingParameters.debug ~level:1 "[Register.select_entry_point] of %a"
    Kernel_function.pretty kf;
  try
    let pdg = Pdg.Api.get kf in
    let node = Pdg.Api.find_entry_point_node pdg in
    let nd_marks = SlicingActions.build_simple_node_selection mark in
    basic_add_select kf select [node] nd_marks
  with Pdg.Api.Top -> top_db_select kf mark
     | Pdg.Api.Bottom -> bottom_msg kf; empty_db_select kf

let select_return kf ?(select=empty_db_select kf) mark =
  SlicingParameters.debug ~level:1 "[Register.select_return] of %a"
    Kernel_function.pretty kf;
  try
    let pdg = Pdg.Api.get kf in
    let node = Pdg.Api.find_ret_output_node pdg in
    let nd_marks = SlicingActions.build_simple_node_selection mark in
    basic_add_select kf select [node] nd_marks
  with
  | Not_found -> (* unreachable ? *)
    SlicingParameters.feedback
      "@[Nothing to select for return stmt of %a@]"
      Kernel_function.pretty kf;
    select
  | Pdg.Api.Top -> top_db_select kf mark
  | Pdg.Api.Bottom -> bottom_msg kf; empty_db_select kf

let select_decl_var kf ?(select=empty_db_select kf) vi mark =
  SlicingParameters.debug ~level:1 "[Register.select_decl_var] of %s in %a@."
    vi.Cil_types.vname Kernel_function.pretty kf;
  if vi.Cil_types.vglob (* no slicing request on globals *)
  then select
  else try
      let pdg = Pdg.Api.get kf in
      let node = Pdg.Api.find_decl_var_node pdg vi in
      let nd_marks = SlicingActions.build_simple_node_selection mark in
      basic_add_select kf select [node] nd_marks
    with
    | Not_found ->
      SlicingParameters.feedback
        "@[Nothing to select for %s declarationin %a@]"
        vi.Cil_types.vname Kernel_function.pretty kf;
      select
    | Pdg.Api.Top -> top_db_select kf mark
    | Pdg.Api.Bottom -> bottom_msg kf; empty_db_select kf


let merge_select select1 select2 =
  let select = match select1, select2 with
    | SlicingInternals.CuTop m, _ | _, SlicingInternals.CuTop m -> SlicingInternals.CuTop m
    | SlicingInternals.CuSelect select1, SlicingInternals.CuSelect select2 ->
      (* TODO : we can probably do better...*)
      SlicingInternals.CuSelect (select1 @ select2)
  in select

let merge_db_select db_select1 db_select2 =
  let fvar, select1 = db_select1 in
  let _, select2 = check_db_select fvar db_select2 in
  let select = merge_select select1 select2 in
  (fvar, select)

module Selections = struct

  let add_to_selects db_select set =
    let vf, select = db_select in
    let select =
      try merge_select (Cil_datatype.Varinfo.Map.find vf set) select
      with Not_found -> select
    in
    Cil_datatype.Varinfo.Map.add vf select set

  let iter_selects_internal f set =
    Cil_datatype.Varinfo.Map.iter (fun v sel -> f (v, sel)) set

  let fold_selects_internal f acc selections  =
    let r = ref acc in
    let dof select = r := f !r select in
    iter_selects_internal dof selections; !r
end

let add_crit_ff_change_call ff_caller call f_to_call =
  let crit = SlicingActions.mk_crit_change_call ff_caller call f_to_call in
  SlicingProject.add_filter crit

(** change the call to call the given slice.
 * This is a user request, so it might be the case that
 * the new function doesn't compute enough outputs :
 * in that case, add outputs first.
*)
let call_ff_in_caller ~caller ~to_call =
  let kf_caller = SlicingMacros.get_ff_kf caller in
  let kf_to_call = SlicingMacros.get_ff_kf to_call in
  let call_stmts = Pdg.Api.find_call_stmts ~caller:kf_caller  kf_to_call in
  let ff_to_call = SlicingInternals.CallSlice to_call in
  let add_change_call stmt =
    add_crit_ff_change_call caller stmt ff_to_call ;
    match Fct_slice.check_outputs_before_change_call caller
            stmt to_call with
    | [] -> ()
    | [c] -> SlicingProject.add_filter c
    | _ -> assert false

  in List.iter add_change_call call_stmts

let call_fsrc_in_caller ~caller ~to_call =
  let kf_caller = SlicingMacros.get_ff_kf caller in
  let fi_to_call = SlicingMacros.get_kf_fi to_call in
  let kf_to_call = SlicingMacros.get_fi_kf fi_to_call in
  let call_stmts = Pdg.Api.find_call_stmts ~caller:kf_caller kf_to_call in
  let add_change_call stmt =
    add_crit_ff_change_call caller stmt (SlicingInternals.CallSrc (Some fi_to_call))
  in List.iter add_change_call call_stmts

let call_min_f_in_caller ~caller ~to_call =
  let kf_caller = SlicingMacros.get_ff_kf caller in
  let pdg = SlicingMacros.get_ff_pdg caller in
  let call_stmts = Pdg.Api.find_call_stmts ~caller:kf_caller to_call in
  let call_nodes =
    List.map (fun call -> (Pdg.Api.find_call_ctrl_node pdg call),None)
      call_stmts in
  let m = SlicingMarks.mk_user_spare in
  let nd_marks = SlicingActions.build_simple_node_selection m in
  let select = SlicingActions.translate_crit_to_select pdg [(call_nodes, nd_marks)] in
  SlicingProject.add_fct_ff_filter caller (SlicingInternals.CuSelect select)

let is_already_selected ff db_select =
  let _, select = check_ff_db_select ff db_select in
  match select with
  | SlicingInternals.CuTop _ -> assert false
  | SlicingInternals.CuSelect to_select ->
    (* let pdg = Pdg.Api.get (Globals.Functions.get fvar) in *)
    let new_marks = Fct_slice.filter_already_in ff to_select in
    let ok = if new_marks = [] then true else false in
    if ok then
      SlicingParameters.debug ~level:1
        "[Api.is_already_selected] %a ?\t--> yes"
        print_select db_select
    else SlicingParameters.debug ~level:1
        "[Api.is_already_selected] %a ?\t--> no (missing %a)"
        print_select db_select
        SlicingActions.print_sel_marks_list new_marks;
    ok

let add_ff_selection ff db_select =
  SlicingParameters.debug ~level:1 "[Api.add_ff_selection] %a to %s"
    print_select db_select (SlicingMacros.ff_name ff);
  let _, select = check_ff_db_select ff db_select in
  SlicingProject.add_fct_ff_filter ff select

(** add a persistent selection to the function.
 * This might change its slicing level in order to call slices later on. *)
let add_fi_selection db_select =
  SlicingParameters.debug ~level:1 "[Api.add_fi_selection] %a"
    print_select db_select;
  let kf = get_select_kf db_select in
  let fi = SlicingMacros.get_kf_fi kf in
  let _, select = db_select in
  SlicingProject.add_fct_src_filter fi select;
  match fi.SlicingInternals.fi_level_option with
  |  SlicingInternals.DontSlice |  SlicingInternals.DontSliceButComputeMarks ->
    SlicingMacros.change_fi_slicing_level fi  SlicingInternals.MinNbSlice;
    SlicingParameters.debug ~level:1 "[Register.add_fi_selection] changing %s slicing level to %s@."
      (SlicingMacros.fi_name fi)
      (SlicingMacros.str_level_option  fi.SlicingInternals.fi_level_option)

  |  SlicingInternals.MinNbSlice |  SlicingInternals.MaxNbSlice -> ()
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