package frama-c

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

Source file slicingTransform.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
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
(**************************************************************************)
(*                                                                        *)
(*  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).            *)
(*                                                                        *)
(**************************************************************************)

(** Export the slicing project *)

(**/**)
open Cil_types
open Cil

open Pdg_types

(**/**)

module Visibility (SliceName : sig
    val get : kernel_function -> bool -> int -> string
  end) = struct

  exception EraseAssigns
  exception EraseAllocation

  type proj = unit
  type transform = {
    slice: SlicingInternals.fct_slice;
    src_visible: bool (* whether the src function of the slice is visible and
                         can be used to give names *);
    keep_body: bool (* if false and the function has a body, the body will be
                       removed. Ignored otherwise *);
  }
  type fct =
    | Iff of transform
    | Isrc of bool (* same meaning as keep_body *)
    | Iproto

  let keep_body kf =
    Kernel_function.is_definition kf &&
    not (Eva.Analysis.use_spec_instead_of_definition kf)

  (* _project is left to comply with a module signature defined outside
     the slicing module (in filter) *)
  let fct_info _proj kf =
    let fi = SlicingMacros.get_kf_fi kf in
    let slices = SlicingMacros.fi_slices fi in
    let src_visible = Fct_slice.is_src_fun_visible kf in
    SlicingParameters.debug ~level:1 "[SlicingTransform.Visibility.fct_info] processing %a (%d slices/src %svisible)"
      Kernel_function.pretty kf (List.length slices)
      (if src_visible then "" else "not ");
    let need_addr = (Kernel_function.get_vi kf).vaddrof in
    let src_name_used = src_visible || need_addr in
    let keep_body = keep_body kf in
    let info_list =
      List.map
        (fun ff -> Iff {slice = ff; src_visible = src_name_used; keep_body})
        slices
    in
    if src_visible    then Isrc keep_body :: info_list
    else if need_addr then  Iproto :: info_list (* TODO for #344 *)
    else info_list

  let fct_name svar ff =
    let name = match ff with
      | Isrc _ | Iproto ->
        let kf_entry,_ = Globals.entry_point () in
        let vi_entry = Kernel_function.get_vi kf_entry in
        if Cil_datatype.Varinfo.equal svar vi_entry then
          svar.vname ^ "_orig"
        else svar.vname
      | Iff {slice = ff; src_visible} ->
        let kf = SlicingMacros.get_ff_kf ff in
        let ff_num = ff.SlicingInternals.ff_id in
        SliceName.get kf src_visible ff_num
    in
    SlicingParameters.debug ~level:2 "[SlicingTransform.Visibility.fct_name] get fct_name = %s" name;
    name

  let visible_mark m = not (SlicingMarks.is_bottom_mark m)

  let param_visible ff_opt n = match ff_opt with
    | Isrc _ | Iproto -> true
    | Iff {slice = ff} -> visible_mark (Fct_slice.get_param_mark ff n)

  let body_visible ff_opt = match ff_opt with
    | Iproto -> false
    | Isrc keep -> keep
    | Iff {keep_body} -> keep_body

  let inst_visible ff_opt inst = match ff_opt with
    | Isrc _ -> true
    | Iproto -> false
    | Iff {slice = ff} ->
      let m = Fct_slice.get_stmt_mark ff inst in
      visible_mark m

  let label_visible ff_opt inst label =  match ff_opt with
    | Isrc _ -> true
    | Iproto -> false
    | Iff {slice = ff} ->
      let m = Fct_slice.get_label_mark ff inst label in
      let v = visible_mark m in
      SlicingParameters.debug ~level:2
        "[SlicingTransform.Visibility.label_visible] label %a is %svisible"
        Printer.pp_label label (if v then "" else "in");
      v

  let data_in_visible ff data_in = match data_in with
    | None -> true
    | Some data_in ->
      (* it is too difficult to know if the callers of this slice
       * compute [data_in] or not, but let's see if, by chance,
       * some data have been selected manually... *)
      let m = Fct_slice.get_input_loc_under_mark ff data_in in
      let v = visible_mark m in
      SlicingParameters.debug ~level:2
        "[SlicingTransform.Visibility.data_in_visible] data %a is %svisible"
        Locations.Zone.pretty data_in (if v then "" else "in");
      v

  let all_nodes_visible ff nodes =
    let is_visible visi n =
      let m = Fct_slice.get_node_mark ff n in
      if SlicingMarks.is_bottom_mark m then
        begin
          SlicingParameters.debug ~level:3
            "[SlicingTransform.Visibility.all_nodes_visible] node %a invisible"
            (Pdg.Api.pretty_node true) n;
          false
        end
      else visi
    in  List.fold_left is_visible true nodes

  exception NoDataInfo

  let data_nodes_visible ff (decl_nodes, data_info) =
    let keep_annots = SlicingParameters.Mode.KeepAnnotations.get () in
    SlicingParameters.debug ~level:2
      "[SlicingTransform.Visibility.data_nodes_visible (with keep_annots = %s)] ?"
      (if keep_annots then "true" else "false");
    let decls_visible = all_nodes_visible ff decl_nodes in
    if keep_annots then decls_visible
    else
      match data_info with
      | None -> raise NoDataInfo
      | Some (data_nodes, data_in) ->
        let is_data_visible visi (n,z) =
          let key = PdgTypes.Node.elem_key n in
          let key = match z, key with
            | Some z, PdgIndex.Key.SigCallKey
                (call, PdgIndex.Signature.Out
                   (PdgIndex.Signature.OutLoc out_z)) ->
              let z = Locations.Zone.narrow z out_z in
              PdgIndex.Key.call_output_key (PdgIndex.Key.call_from_id call) z
            | _, _ -> key
          in
          let m = Fct_slice.get_node_key_mark ff key in
          if SlicingMarks.is_bottom_mark m then
            begin
              SlicingParameters.debug ~level:2
                "[SlicingTransform.Visibility.data_nodes_visible]@\n\
                 node %a invisible"
                (Pdg.Api.pretty_node true) n;
              false
            end
          else visi
        in
        let visible = decls_visible && data_in_visible ff data_in in
        let data_visible = List.fold_left is_data_visible visible data_nodes in
        data_visible

  (* work-around to avoid outputting annotations with type errors:
     in case we end up with NotImplemented somewhere, we keep the annotation
     iff all C variables occurring in there are visible.
  *)
  let all_logic_var_visible, all_logic_var_visible_identified_term, all_logic_var_visible_term,
      all_logic_var_visible_assigns, all_logic_var_visible_deps =
    let module Exn = struct exception Invisible end in
    let vis ff = object
      inherit Visitor.frama_c_inplace
      method! vlogic_var_use v =
        match v.lv_origin with
          None -> DoChildren
        | Some v when
            v.vformal &&
            not
              (visible_mark
                 (Fct_slice.get_param_mark ff
                    (Kernel_function.get_formal_position v
                       (SlicingMacros.get_ff_kf ff)+1)))
          (* For some reason, pdg counts parameters starting
             from 1 *)
          -> raise Exn.Invisible
        | Some v when
            not v.vglob &&
            not (visible_mark (Fct_slice.get_local_var_mark ff v)) ->
          raise Exn.Invisible
        | Some _ -> DoChildren
    end
    in (fun ff pred ->
        try
          ignore (Visitor.visitFramacPredicate (vis ff) pred); true
        with Exn.Invisible -> false),
       (fun ff term ->
          try
            ignore (Visitor.visitFramacIdTerm (vis ff) term); true
          with Exn.Invisible -> false),
       (fun ff term ->
          try
            ignore (Visitor.visitFramacTerm (vis ff) term); true
          with Exn.Invisible -> false),
       (fun ff (b,_) ->
          try
            ignore (Visitor.visitFramacTerm (vis ff) b.it_content); true
          with Exn.Invisible -> false),
       (fun ff d ->
          try
            ignore (Visitor.visitFramacTerm (vis ff) d.it_content); true
          with Exn.Invisible -> false)

  let annotation_visible ff_opt stmt annot =
    SlicingParameters.debug ~current:true ~level:2
      "[SlicingTransform.Visibility.annotation_visible] ?";
    Eva.Results.is_reachable stmt &&
    Alarms.find annot = None && (* Always drop alarms: the alarms table
                                   in the new project is not synchronized *)
    match ff_opt with
    | Isrc _ -> true
    | Iproto -> false
    | Iff {slice = ff} ->
      let kf = SlicingMacros.get_ff_kf ff  in
      let pdg = Pdg.Api.get kf in
      try
        let ctrl_nodes, decl_nodes, data_info =
          Pdg.Api.find_code_annot_nodes pdg stmt annot
        in
        let data_visible = data_nodes_visible ff (decl_nodes, data_info) in
        let visible = ((all_nodes_visible ff ctrl_nodes) && data_visible) in
        SlicingParameters.debug ~level:2
          "[SlicingTransform.Visibility.annotation_visible] -> %s"
          (if visible then "yes" else "no");
        visible
      with
      | NoDataInfo ->
        SlicingParameters.debug ~level:2
          "[SlicingTransform.Visibility.annotation_visible] \
           not implemented -> invisible"; false
      | Logic_deps.NYI msg ->
        SlicingParameters.warning ~current:true ~once:true
          "Dropping unsupported ACSL annotation";
        SlicingParameters.debug ~level:2
          "[SlicingTransform.Visibility.annotation_visible] \
           %s -> invisible" msg;
        false


  let fun_precond_visible ff_opt p =
    SlicingParameters.debug ~level:2
      "[SlicingTransform.Visibility.fun_precond_visible] %a ?"
      Printer.pp_predicate p;
    let visible = match ff_opt with
      | Isrc _ -> true
      | Iproto -> true
      | Iff {slice = ff} ->
        let kf = SlicingMacros.get_ff_kf ff  in
        let pdg = Pdg.Api.get kf in
        try
          let nodes = Pdg.Api.find_fun_precond_nodes pdg p in
          data_nodes_visible ff nodes
        with NoDataInfo ->
          all_logic_var_visible ff p

    in SlicingParameters.debug ~level:2 "[SlicingTransform.Visibility.precond_visible] -> %s"
      (if visible then "yes" else "no");
    visible

  let fun_postcond_visible ff_opt p =
    SlicingParameters.debug ~level:2
      "[SlicingTransform.Visibility.fun_postcond_visible] %a ?"
      Printer.pp_predicate p;
    let visible = match ff_opt with
      | Isrc _ -> true
      | Iproto -> true
      | Iff {slice = ff} ->
        let kf = SlicingMacros.get_ff_kf ff  in
        let pdg = Pdg.Api.get kf in
        try
          let nodes = Pdg.Api.find_fun_postcond_nodes pdg p in
          data_nodes_visible ff nodes
        with NoDataInfo -> all_logic_var_visible ff p

    in SlicingParameters.debug ~level:2
      "[SlicingTransform.Visibility.fun_postcond_visible] -> %s"
      (if visible then "yes" else "no");
    visible

  let fun_variant_visible ff_opt v =
    SlicingParameters.debug ~level:2
      "[SlicingTransform.Visibility.fun_variant_visible] %a ?"
      Printer.pp_term v ;
    let visible = match ff_opt with
      | Isrc _ -> true
      | Iproto -> true
      | Iff {slice = ff} ->
        let kf = SlicingMacros.get_ff_kf ff  in
        let pdg = Pdg.Api.get kf in
        try
          let nodes = Pdg.Api.find_fun_variant_nodes pdg v in
          data_nodes_visible ff nodes
        with NoDataInfo -> all_logic_var_visible_term ff v
    in SlicingParameters.debug ~level:2 "[SlicingTransform.Visibility.fun_variant_visible] -> %s"
      (if visible then "yes" else "no");
    visible

  let fun_frees_visible ff_opt v =
    let keep_annots = SlicingParameters.Mode.KeepAnnotations.get () in
    SlicingParameters.debug ~level:2
      "[SlicingTransform.Visibility.fun_frees_visible \
       (with keep_annots = %B)] ?"
      keep_annots;
    if not keep_annots then raise EraseAllocation;
    let visible =
      match ff_opt with
      | Isrc _ -> true
      | Iproto -> true
      | Iff {slice = ff} -> all_logic_var_visible_identified_term ff v
    in SlicingParameters.debug ~level:2 "[SlicingTransform.Visibility.fun_frees_visible] -> %s"
      (if visible then "yes" else "no");
    visible

  let fun_allocates_visible ff_opt v =
    let keep_annots = SlicingParameters.Mode.KeepAnnotations.get () in
    SlicingParameters.debug ~level:2
      "[SlicingTransform.Visibility.fun_allocates_visible \
       (with keep_annots = %B)] ?"
      keep_annots;
    if not keep_annots then raise EraseAllocation;
    let visible =
      match ff_opt with
      | Isrc _ -> true
      | Iproto -> true
      | Iff {slice = ff} -> all_logic_var_visible_identified_term ff v
    in SlicingParameters.debug ~level:2 "[SlicingTransform.Visibility.fun_allocates_visible] -> %s"
      (if visible then "yes" else "no");
    visible

  let fun_assign_visible ff_opt v =
    let keep_annots = SlicingParameters.Mode.KeepAnnotations.get () in
    SlicingParameters.debug ~level:2
      "[SlicingTransform.Visibility.fun_assign_visible \
       (with keep_annots = %B)] ?"
      keep_annots;
    if not keep_annots then raise EraseAssigns;
    let visible =
      match ff_opt with
      | Isrc _ -> true
      | Iproto -> true
      | Iff {slice = ff} -> all_logic_var_visible_assigns ff v
    in SlicingParameters.debug ~level:2 "[SlicingTransform.Visibility.fun_assign_visible] -> %s"
      (if visible then "yes" else "no");
    visible

  let fun_deps_visible ff_opt v =
    let keep_annots = SlicingParameters.Mode.KeepAnnotations.get () in
    SlicingParameters.debug ~level:2
      "[SlicingTransform.Visibility.fun_deps_visible \
       (with keep_annots = %B)] ?"
      keep_annots;
    let visible =
      match ff_opt with
      | Isrc _ -> true
      | Iproto -> true
      | Iff {slice = ff} -> all_logic_var_visible_deps ff v
    in
    SlicingParameters.debug ~level:2
      "[SlicingTransform.Visibility.fun_deps_visible] -> %s"
      (if visible then "yes" else "no");
    visible

  let loc_var_visible ff_opt var = match ff_opt with
    | Isrc _ -> true
    | Iproto -> false
    | Iff {slice = ff} ->
      let m = Fct_slice.get_local_var_mark ff var in
      visible_mark m

  let res_call_visible ff call_stmt = match ff with
    | Isrc _ -> true
    | Iproto -> false
    | Iff {slice = ff} ->
      let key = PdgIndex.Key.call_outret_key call_stmt in
      let _, ff_marks = ff.SlicingInternals.ff_marks in
      try
        let m = PdgIndex.FctIndex.find_info ff_marks key in
        visible_mark m
      with Not_found -> false

  let result_visible _kf ff = match ff with
    | Isrc _ | Iproto -> true
    | Iff {slice = ff} ->
      let key = PdgIndex.Key.output_key in
      let _, ff_marks = ff.SlicingInternals.ff_marks in
      try
        let m = PdgIndex.FctIndex.find_info ff_marks key in
        visible_mark m
      with Not_found -> false

  (* _project is left to comply with a module signature defined outside
     the slicing module (in filter) *)
  let called_info (_project, ff) call_stmt =
    let info = match ff with
      | Isrc _ | Iproto -> None
      | Iff {slice = ff} ->
        try
          let _, ff_marks = ff.SlicingInternals.ff_marks in
          let called, _ =
            PdgIndex.FctIndex.find_call ff_marks call_stmt in
          match called with
          | None | Some (None) ->
            SlicingParameters.error "Undefined called function call-%d\n"
              call_stmt.sid;
            assert false
          | Some (Some (SlicingInternals.CallSrc _)) -> None
          | Some (Some (SlicingInternals.CallSlice ff)) ->
            let kf_ff = SlicingMacros.get_ff_kf ff in
            (* BY: no idea why this is not the same code as in fct_info *)
            let src_visible = Fct_slice.is_src_fun_visible kf_ff in
            let keep_body = keep_body kf_ff in
            Some (kf_ff, Iff { slice = ff; src_visible; keep_body})
        with Not_found ->
          (* the functor should call [called_info] only for visible calls *)
          assert false
    in
    SlicingParameters.debug ~level:2 "[SlicingTransform.Visibility.called_info] called_info stmt %d -> %s@."
      call_stmt.sid (if info = None then "src" else "some slice");
    info

  let cond_edge_visible _ff_opt s =
    Eva.Results.condition_truth_value s

end

let default_slice_names kf _src_visible ff_num =
  let fname = Kernel_function.get_name kf in
  let kf_entry,_ = Globals.entry_point () in
  if Kernel_function.equal kf kf_entry then fname
  else Printf.sprintf "%s_slice_%d" fname ff_num

let extract ~f_slice_names new_proj_name =
  SlicingParameters.feedback ~level:1
    "exporting project to '%s'..." new_proj_name;
  SlicingParameters.feedback ~level:1 "applying all slicing requests...";
  SlicingProject.apply_all_actions ();
  SlicingParameters.feedback ~level:2 "done (applying all slicing requests).";
  let module S = struct let get = f_slice_names end in
  let module Visi = Visibility (S) in
  let module Transform = Filter.F (Visi) in
  let tmp_prj =
    Transform.build_cil_file (new_proj_name ^ " tmp") ()
  in
  let new_prj =
    Sparecode.Register.rm_unused_globals ~new_proj_name ~project:tmp_prj ()
  in
  Project.remove ~project:tmp_prj ();
  let ctx = Parameter_state.get_selection_context () in
  Project.copy ~selection:ctx new_prj;
  SlicingParameters.feedback
    ~level:2 "done (exporting project to '%s')." new_proj_name;
  new_prj

(*
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