package frama-c

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

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

(** Handle the project global object. *)

(**/**)

open Pdg_types

module T = SlicingInternals
module M = SlicingMacros

(**/**)

(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
(** {2 Managing the slices} *)

let add_proj_actions actions =
  let proj = SlicingState.get () in
  proj.T.actions <- actions @ proj.T.actions

(** Add a new slice for the function. It can be the case that it create actions
 * if the function has some persistent selection, that make function calls to
 * choose.
 * @raise SlicingTypes.NoPdg when the function has no PDG.
 * *)
let create_slice kf =
  let ff, actions = Fct_slice.make_new_ff (M.get_kf_fi kf) true in
  add_proj_actions actions; ff

(** Delete [ff_to_remove] if it is not called.
 * @raise T.CantRemoveCalledFf if it is.
*)
let remove_ff ff_to_remove =
  let rec remove ff_list ff_num = match ff_list with
    | [] -> raise Not_found
    | ff :: tail ->
      if ff.T.ff_id = ff_num then (Fct_slice.clear_ff ff; tail)
      else ff :: (remove tail ff_num)
  in let fi = ff_to_remove.T.ff_fct in
  let ff_num = ff_to_remove.T.ff_id in
  let new_ff_list = remove fi.T.fi_slices ff_num in
  fi.T.fi_slices <- new_ff_list

let call_src_and_remove_all_ff fi =
  let do_call actions (ff_caller, call_id) =
    let new_actions =
      Fct_slice.apply_change_call ff_caller call_id (T.CallSrc (Some fi))
    in new_actions @ actions
  in
  let do_ff actions ff =
    let calls = ff.SlicingInternals.ff_called_by in
    let actions = List.fold_left do_call actions calls in
    remove_ff ff;
    actions
  in
  List.fold_left do_ff [] fi.T.fi_slices

let rec remove_uncalled_slices () =
  let kf_entry, _ = Globals.entry_point () in
  let entry_name = Kernel_function.get_name kf_entry in
  let check_ff changes ff =
    match ff.T.ff_called_by with [] -> remove_ff ff; true | _ -> changes
  in let check_fi changes fi =
       if (M.fi_name fi) <> entry_name then
         List.fold_left check_ff changes (M.fi_slices fi)
       else changes
  in let changes = M.fold_fi check_fi false in
  if changes then remove_uncalled_slices () else ()

(** Build a new slice [ff] which contains the marks of [ff1] and [ff2]
 * and generate everything that is needed to choose the calls in [ff].
 * If [replace] also generate requests call [ff] instead of [ff1] and [ff2]. *)
let merge_slices ff1 ff2 replace =
  let ff, ff_actions = Fct_slice.merge_slices ff1 ff2 in
  if replace then
    begin
      let add actions (caller, call) =
        let rq = SlicingActions.mk_crit_change_call caller call
            (T.CallSlice ff) in
        rq :: actions
      in
      let actions = List.fold_left add [] ff2.T.ff_called_by in
      let actions = List.fold_left add actions ff1.T.ff_called_by in
      add_proj_actions actions
    end;
  add_proj_actions ff_actions;
  ff

let split_slice ff =
  let add (actions, slices) (caller, call) =
    let new_ff = Fct_slice.copy_slice ff in
    let rq = SlicingActions.mk_crit_change_call caller call
        (T.CallSlice new_ff) in
    rq::actions, new_ff::slices
  in
  let calls = List.tl ff.T.ff_called_by in (* keep ff for the first call *)
  let actions, slices = List.fold_left add ([], [ff]) calls in
  add_proj_actions actions;
  slices

(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
(** {2 Getting information } *)

let get_slices kf = M.fi_slices (M.get_kf_fi kf)

let get_slice_callers ff = List.map (fun (ff, _) -> ff) ff.T.ff_called_by

(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
(** {2 Adding requests } *)

let add_filter filter =
  let proj = SlicingState.get () in
  proj.T.actions <- filter :: proj.T.actions

                                (*
let add_fct_filter proj f_id criterion =
  let ff_res =
    match f_id with
      | T.FctSrc fi -> Fct_slice.make_new_ff fi
      | T.FctSliced ff -> ff
  in let filter = SlicingActions.mk_ff_user_crit ff_res criterion in
  let _ = add_filter proj filter in
    ff_res
    *)

(** Add an action to the action list to filter the function [fct_id] with
    the given criterion. The filter gives a name to the result of the filter
    which is a new slice if the function to filter is the source one,
    or the given slice otherwise.
*)
let add_fct_src_filter fi to_select =
  match to_select with
  (* T.CuSelect []  : don't ignore empty selection because
                      the input control node has to be selected anyway... *)
  | T.CuSelect select ->
    let filter = SlicingActions.mk_crit_fct_user_select fi select in
    add_filter filter
  | T.CuTop m ->
    let filter = SlicingActions.mk_crit_fct_top fi m in
    add_filter filter

    (*
let add_fct_src_filters proj fi actions =
  List.iter (fun a -> ignore (add_fct_src_filter proj fi a)) actions
                                                             *)

let add_fct_ff_filter ff to_select =
  match to_select with
  | T.CuSelect [] ->
    SlicingParameters.debug ~level:1
      "[SlicingProject.add_fct_ff_filter] (ignored empty selection)"
  | T.CuSelect select ->
    let filter = SlicingActions.mk_ff_user_select ff select in
    add_filter filter
  | T.CuTop _ -> assert false

(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
(** {2 Print} *)

let print_project fmt =
  let get_slices var_fct =
    let kf = Globals.Functions.get var_fct in
    let fct_info = M.get_kf_fi kf in
    M.fi_slices fct_info
  in
  let print glob =
    match glob with
    | Cil_types.GFun (func, _) -> (* function definition *)
      let slices = get_slices func.Cil_types.svar in
      List.iter (PrintSlice.print_marked_ff fmt) slices
    (* TODO see if we have to print the original function *)
    | _ ->
      PrintSlice.print_original_glob fmt glob
  in
  let source = Ast.get () in
  let global_decls = source.Cil_types.globals in
  List.iter print global_decls


let print_proj_worklist fmt =
  let proj = SlicingState.get () in
  Format.fprintf fmt "Slicing project worklist [%s] =@\n%a@.@."
    (Project.get_name (Project.current ()))
    SlicingActions.print_list_crit proj.T.actions

let print_project_and_worklist fmt =
  print_project fmt;
  print_proj_worklist fmt

let pretty_slice fmt ff =
  PrintSlice.print_marked_ff fmt ff;
  Format.pp_print_newline fmt ()

(*~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~*)
(** {2 Managing (and applying) requests} *)

(** apply the given criterion and returns the list of new criteria to
    add to the project worklist. *)
let apply_fct_crit ff to_select =
  let actions = Fct_slice.apply_add_marks ff to_select in
  actions

let apply_appli_crit appli_crit =
  match appli_crit with
  | T.CaCall fi_to_call ->
    let kf_to_call = M.get_fi_kf fi_to_call in
    let add_actions actions kf_caller =
      let fi_caller = M.get_kf_fi kf_caller in
      let mark = SlicingMarks.mk_user_spare in
      let action =
        SlicingActions.mk_crit_mark_calls fi_caller kf_to_call mark in
      action :: actions
    in List.fold_left add_actions [] (Eva.Results.callers kf_to_call)
  | _ ->
    SlicingParameters.not_yet_implemented
      "This slicing criterion on application"

(** Add persistent the marks [node_marks] in [fi] and also add the marks
 * to existing slices if any.
 * If the propagation is ON, some actions are generated to propagate the
 * persistent marks to the callers, and other actions are generated to
 * make all the calls to [fi] visible.
 * If there is no slice for [fi] we create a new one
 * if it is the original request.
 * It will be automatically created with the persistent marks.
 * If it is a propagation, no need to create a new slice
 * because it will be created when the call will be selected anyway.
 * *)
let add_persistent_marks fi node_marks orig propagate actions =
  let new_fi_marks, actions =
    Fct_slice.add_marks_to_fi fi node_marks propagate actions
  in
  let actions = match M.fi_slices fi with
    | [] -> (* no slice *)
      let actions =
        if orig then
          let _ff, new_actions = Fct_slice.make_new_ff fi true in
          (* TODO catch NoPdg and mark fi as Top *)
          new_actions @ actions
        else actions
      in actions
    | slices ->
      let add_filter acc ff =
        let a = SlicingActions.mk_ff_user_select ff node_marks in a::acc
      in
      List.fold_left add_filter actions slices
  in
  let actions =
    if propagate && new_fi_marks then
      let a = SlicingActions.mk_appli_select_calls fi in actions @ [a]
    else actions
  in actions

let apply_fct_action fct_crit =
  match fct_crit.T.cf_fct with
  | T.FctSliced ff ->
    let _ = M.get_ff_pdg ff in
    let new_filters =
      match fct_crit.T.cf_info with
      | T.CcUserMark (T.CuSelect []) ->
        SlicingParameters.debug ~level:1
          "[apply_fct_action] ignore empty selection on existing slice";
        []
      | T.CcUserMark (T.CuSelect crit) -> apply_fct_crit ff crit
      | T.CcUserMark (T.CuTop _) -> assert false (* impossible on ff ! *)
      | T.CcChangeCall (call, f) ->
        Fct_slice.apply_change_call ff call f
      | T.CcChooseCall call ->
        Fct_slice.apply_choose_call ff call
      | T.CcMissingInputs (call, input_marks, more_inputs) ->
        Fct_slice.apply_missing_inputs ff call
          (input_marks, more_inputs)
      | T.CcMissingOutputs (call, output_marks, more_outputs) ->
        Fct_slice.apply_missing_outputs ff call
          output_marks more_outputs
      | T.CcPropagate _ -> assert false (* not for ff at the moment *)
      | T.CcExamineCalls marks ->
        Fct_slice.apply_examine_calls ff marks
    in
    SlicingParameters.debug ~level:4 "[slicingProject.apply_fct_action] result =@\n%a"
      PrintSlice.print_marked_ff ff;
    new_filters
  | T.FctSrc fi -> (* the marks have to be added to all slices *)
    let propagate = SlicingParameters.Mode.Callers.get () in
    match fct_crit.T.cf_info with
    | T.CcUserMark (T.CuSelect to_select) ->
      add_persistent_marks fi to_select true propagate []
    | T.CcUserMark (T.CuTop m) ->
      SlicingParameters.result ~level:1 "unable to slice %s (-> TOP)"
        (M.fi_name fi);
      let filters = call_src_and_remove_all_ff fi in
      Fct_slice.add_top_mark_to_fi fi m propagate filters
    | T.CcPropagate [] ->
      SlicingParameters.debug ~level:1
        "[apply_fct_action] nothing to propagate";
      []
    | T.CcPropagate node_marks ->
      add_persistent_marks fi node_marks false propagate []
    | T.CcExamineCalls _
    | _ ->
      SlicingParameters.not_yet_implemented
        "This slicing criterion on source function"

(** apply [filter] and return a list of generated filters *)
let apply_action filter =
  SlicingParameters.debug ~level:1 "[SlicingProject.apply_action] : %a" SlicingActions.print_crit filter;
  let new_filters =
    try match filter with
      | T.CrFct fct_crit ->
        begin
          try (apply_fct_action fct_crit)
          with PdgTypes.Pdg.Bottom ->
            SlicingParameters.debug ~level:1 "  -> action ABORTED (PDG is bottom)" ;
            []
        end
      | T.CrAppli appli_crit ->
        apply_appli_crit appli_crit
    with Not_found -> (* catch unprocessed Not_found here *) assert false
  in
  SlicingParameters.debug ~level:1 "  -> %d generated filters : %a@."
    (List.length new_filters)
    SlicingActions.print_list_crit new_filters;
  new_filters

let get_next_filter () =
  let proj = SlicingState.get () in
  match proj.T.actions with
  | [] ->
    SlicingParameters.debug ~level:2
      "[SlicingProject.get_next_filter] No more filter";
    raise Not_found
  | f :: tail -> proj.T.actions <- tail; f

let apply_next_action () =
  SlicingParameters.debug ~level:2 "[SlicingProject.apply_next_action]";
  let proj = SlicingState.get () in
  let filter = get_next_filter () in
  let new_filters = apply_action filter in
  proj.T.actions <- new_filters @ proj.T.actions

let is_request_empty () =
  let proj = SlicingState.get () in
  proj.T.actions = []

let apply_all_actions () =
  let proj = SlicingState.get () in
  let nb_actions = List.length proj.T.actions in
  let rec apply actions = match actions with [] -> ()
                                           | a::actions ->
                                             SlicingParameters.feedback ~level:2 "applying sub action...";
                                             let new_filters = apply_action a in
                                             apply new_filters;
                                             apply actions
  in
  SlicingParameters.feedback ~level:1 "applying %d actions..." nb_actions;
  let rec apply_user n =
    try
      let a = get_next_filter () in
      SlicingParameters.feedback ~level:1 "applying actions: %d/%d..."
        n nb_actions;
      let new_filters = apply_action a in
      apply new_filters;
      apply_user (n+1)
    with Not_found ->
      if nb_actions > 0 then
        SlicingParameters.feedback
          ~level:2 "done (applying %d actions." nb_actions
  in
  apply_user 1

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