package frama-c

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

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

open Pdg_types
open PdgIndex

(** compute the marks to propagate in the caller nodes from the marks of
 * a function inputs [in_marks].
*)
let in_marks_to_caller pdg call m2m ?(rqs=[]) in_marks =
  let add_n_m acc n z_opt m =
    let select = PdgMarks.mk_select_node ~z_opt n in
    match m2m select m with
    | None -> acc
    | Some m -> PdgMarks.add_to_select acc select m
  in
  let build rqs (in_key, m) =
    match in_key with
    | Signature.InCtrl ->
      add_n_m rqs (Sets.find_call_ctrl_node pdg call) None m
    | Signature.InNum in_num ->
      add_n_m rqs (Sets.find_call_num_input_node pdg call in_num) None m
    | Signature.InImpl zone ->
      let nodes, undef =
        Sets.find_location_nodes_at_stmt pdg call ~before:true zone
      in
      let rqs =
        List.fold_left (fun acc (n,z) -> add_n_m acc n z m) rqs nodes in
      let rqs = match undef with None -> rqs
                               | Some z ->
                                 match m2m (PdgMarks.mk_select_undef_zone z) m with None -> rqs
                                                                                  | Some m -> PdgMarks.add_undef_in_to_select rqs undef m
      in rqs
  in List.fold_left build rqs in_marks

(** some new input marks has been added in a called function.
 * Build the list of what is to be propagated in the callers.
 * Be careful that some Pdg can be top : in that case, a list of mark is
 * returned (Beware that m2m has NOT been called in that case).
 * *)
let translate_in_marks pdg_called in_new_marks
    ?(m2m=fun _ _ _ m -> Some m) other_rqs =
  let kf_called = PdgTypes.Pdg.get_kf pdg_called in
  let translate pdg rqs call =
    in_marks_to_caller pdg call (m2m (Some call) pdg) ~rqs in_new_marks
  in
  let build rqs caller =
    let pdg_caller = Pdg_tbl.get caller in
    let caller_rqs =
      try
        let call_stmts = Sets.find_call_stmts ~caller kf_called in
        (* TODO : more intelligent merge ? *)
        let rqs = List.fold_left (translate pdg_caller) [] call_stmts in
        PdgMarks.SelList rqs
      with PdgTypes.Pdg.Top ->
        let marks = List.fold_left (fun acc (_, m) -> m::acc) [] in_new_marks
        in PdgMarks.SelTopMarks marks (* #345 *)
    in
    (pdg_caller, caller_rqs)::rqs
  in
  List.fold_left build other_rqs (Eva.Results.callers kf_called)

let call_out_marks_to_called called_pdg m2m ?(rqs=[]) out_marks =
  let build rqs (out_key, m) =
    let nodes, undef = Sets.find_output_nodes called_pdg out_key in
    let sel =
      List.map (fun (n, _z_opt) -> PdgMarks.mk_select_node ~z_opt:None n) nodes in
    let sel = match undef with None -> sel
                             | Some undef -> (PdgMarks.mk_select_undef_zone undef)::sel
    in
    let add acc s = match m2m s m with
      | None -> acc
      | Some m -> (s, m)::acc
    in
    let rqs = List.fold_left add rqs sel in
    rqs
  in
  List.fold_left build rqs out_marks

let translate_out_mark _pdg m2m other_rqs (call, l) =
  let add_list l_out_m rqs called_kf  =
    let called_pdg = Pdg_tbl.get called_kf in
    let m2m = m2m (Some call) called_pdg in
    try
      let node_marks =
        call_out_marks_to_called called_pdg m2m ~rqs:[] l_out_m
      in (called_pdg, PdgMarks.SelList node_marks)::rqs
    with PdgTypes.Pdg.Top ->
      (* no PDG for this function : forget the new marks
       * because anyway, the source function will be called.
       * *)
      rqs
  in
  let all_called = Eva.Results.callee call in
  List.fold_left (add_list l) other_rqs all_called

(** [add_new_marks_to_rqs pdg new_marks other_rqs] translates [new_marks]
 * that were computed during intraprocedural propagation into requests,
 * and add them to [other_rqs].
 *
 * The functions [in_m2m] and [out_m2m] can be used to modify the marks during
 * propagation :
 *- [in_m2m call_stmt call_in_node mark] :
      provide the mark to propagate to the [call_in_node]
      knowing that the mark of the called function has been modify to [mark]
 *- [out_m2m out_node mark] :
      provide the mark to propagate to the [out_node]
      knowing that a call output mark has been modify to [mark].
*)
let translate_marks_to_prop pdg new_marks
    ?(in_m2m=fun _ _ _ m -> Some m)
    ?(out_m2m=fun _ _ _ m -> Some m)
    other_rqs =
  let in_marks, out_marks = new_marks in
  let other_rqs = translate_in_marks pdg in_marks ~m2m:in_m2m other_rqs in
  let rqs =
    List.fold_left (translate_out_mark pdg out_m2m) other_rqs out_marks
  in rqs


(** To also use interprocedural propagation, the user can instantiate this
 * functor. This is, of course, not mandatory because one can want to use a more
 * complex propagation (like slicing for instance, that has more than one
 * version for a source function). *)
module F_Proj (C : PdgMarks.Config) :
  PdgMarks.Proj with type mark = C.M.t
                 and type call_info = C.M.call_info
= struct

  module F = PdgMarks.F_Fct (C.M)

  type mark = C.M.t
  type call_info = C.M.call_info
  type fct = F.fi
  type fct_info = F.t
  type t = fct_info Varinfo.Hashtbl.t

  let empty () = Varinfo.Hashtbl.create 10

  let find_marks proj fct_var =
    try let f = Varinfo.Hashtbl.find proj fct_var in Some (F.get_idx f)
    with Not_found -> None

  let get proj pdg =
    let kf = PdgTypes.Pdg.get_kf pdg in
    let fct_var = Kernel_function.get_vi kf in
    try Varinfo.Hashtbl.find proj fct_var
    with Not_found ->
      let pdg = Pdg_tbl.get kf in
      let info = F.create pdg in
      Varinfo.Hashtbl.add proj fct_var info;
      info

  (** Add the marks to the pdg nodes.
   * @return a merge between the input [other_rqs] and the new requests produced.
   * *)
  let apply_fct_rqs proj (pdg, mark_list) other_rqs =
    match mark_list with
    | PdgMarks.SelList []
    | PdgMarks.SelTopMarks [] ->
      (* don't want to build the marks when calling [get]
         if there is nothing to do... *)
      other_rqs
    | PdgMarks.SelList mark_list ->
      let fm = get proj pdg in
      let to_prop = F.mark_and_propagate fm mark_list in
      let rqs = translate_marks_to_prop pdg to_prop
          ~in_m2m:C.mark_to_prop_to_caller_input
          ~out_m2m:C.mark_to_prop_to_called_output
          other_rqs in
      rqs
    | PdgMarks.SelTopMarks _marks -> (* TODO #345 *)
      Pdg_parameters.not_yet_implemented "mark propagation in Top PDG"

  (** Add the marks to the pdg nodes and also apply all the produced requests
   * to do the interprocedural propagation. *)
  let mark_and_propagate proj pdg node_marks =
    let rec apply_all rqs = match rqs with
      | [] -> ()
      | rq :: tl_rqs ->
        let new_rqs = apply_fct_rqs proj rq tl_rqs in
        apply_all new_rqs
    in apply_all [(pdg, PdgMarks.SelList node_marks)]
end

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