package frama-c

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

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

(** Everything related with the marks. Mainly quite low level function. *)

open Pdg_types

(**/**)

let debug = false

(**/**)

(** a [Mark] is used to represent some information about the status of
 * a PDG element in a slice.
*)
module Mark : sig
  val bottom : SlicingInternals.mark
  val spare : SlicingInternals.mark
  val data : SlicingInternals.mark
  val ctrl : SlicingInternals.mark
  val addr : SlicingInternals.mark
  val mk_adc : bool -> bool -> bool -> SlicingInternals.mark

  val is_bottom : SlicingInternals.mark -> bool
  val is_top : SlicingInternals.mark -> bool
  val is_included : SlicingInternals.mark -> SlicingInternals.mark -> bool

  (** this operation has to be commutative.
      It is used to merge two slices into one.
  *)
  val merge : SlicingInternals.mark -> SlicingInternals.mark -> SlicingInternals.mark

  val inter : SlicingInternals.mark -> SlicingInternals.mark -> SlicingInternals.mark

  (** this operation add a new information to the old value.
   * @return (new_mark, is_new)
             where is_new=true if the new_mark is not included in the old one.
  *)
  val combine : old:SlicingInternals.mark -> SlicingInternals.mark -> bool * SlicingInternals.mark

  (** [minus m1 m2] provides the mark [m] that you have to merge with [m2] to
    * get at least [m1]. So : [m1 <= m U m2]
    * If [m1 <= m2] then [m = bot].
    * *)
  val minus : SlicingInternals.mark -> SlicingInternals.mark -> SlicingInternals.mark

  val pretty : Format.formatter -> SlicingInternals.mark -> unit

end = struct

  let spare = SlicingInternals.Spare

  (* Internal constructor *)
  let create_adc a d c =  SlicingInternals.Cav (PdgTypes.Dpd.make ~a ~d ~c ())

  let bottom = SlicingInternals.Cav PdgTypes.Dpd.bottom
  let top = SlicingInternals.Cav PdgTypes.Dpd.top

  let addr = create_adc true false  false
  let data = create_adc false true  false
  let ctrl = create_adc false false true

  let m_ad = create_adc true  true  false
  let m_ac = create_adc true  false true
  let m_dc = create_adc false true  true

  let create adc =
    match adc with
    | false, false, false -> bottom
    | true,  false, false -> addr
    | false, true,  false -> data
    | false, false, true  -> ctrl
    | true,  true,  false -> m_ad
    | true,  false, true  -> m_ac
    | false, true,  true  -> m_dc
    | true,  true,  true  -> top

  (* External constructor sharing same values *)
  let mk_adc a d c = create (a, d, c)
  let mk_mark dpd = create (PdgTypes.Dpd.adc_value dpd)

  let is_bottom m = (m = bottom)
  let is_top m = (m = top)

  let is_included m1 m2 =
    match m1,m2 with
    | SlicingInternals.Spare, SlicingInternals.Spare -> true
    | SlicingInternals.Spare, SlicingInternals.Cav _ -> not (is_bottom m2)
    | SlicingInternals.Cav _, SlicingInternals.Spare -> is_bottom m1
    | SlicingInternals.Cav d1, SlicingInternals.Cav d2 -> PdgTypes.Dpd.is_included d1 d2

  let merge m1 m2 =
    match m1,m2 with
    | SlicingInternals.Spare, SlicingInternals.Spare -> m1
    | SlicingInternals.Spare, SlicingInternals.Cav _ -> if is_bottom m2 then m1 else m2
    | SlicingInternals.Cav _,  SlicingInternals.Spare -> if is_bottom m1 then m2 else m1
    | SlicingInternals.Cav d1, SlicingInternals.Cav d2 -> mk_mark (PdgTypes.Dpd.combine d1 d2)

  let inter m1 m2 =
    if is_bottom m1 then m1
    else if is_bottom m2 then m2
    else (* m1 and m2 are not bottom => the result cannot be bottom *)
      match m1,m2 with
      | SlicingInternals.Spare, _ -> m1
      | _, SlicingInternals.Spare -> m2
      | SlicingInternals.Cav d1, SlicingInternals.Cav d2 ->
        let m = mk_mark (PdgTypes.Dpd.inter d1 d2) in
        if is_bottom m then spare else m

  let combine ~old m =
    match old, m with
    | SlicingInternals.Spare, SlicingInternals.Spare -> (false, old)
    | SlicingInternals.Cav old_d, SlicingInternals.Spare ->
      if PdgTypes.Dpd.is_bottom old_d then (true, m) else (false, old)
    | SlicingInternals.Spare, SlicingInternals.Cav new_d ->
      if PdgTypes.Dpd.is_bottom new_d then (false, old) else (true, m)
    | SlicingInternals.Cav old_d, SlicingInternals.Cav new_d ->
      let new_d = PdgTypes.Dpd.combine old_d new_d in
      if old_d = new_d then (false, old) else (true, mk_mark new_d)

  let minus m1 m2 =
    match m1,m2 with
    | SlicingInternals.Spare, SlicingInternals.Spare -> bottom
    | SlicingInternals.Spare, SlicingInternals.Cav d2 -> if PdgTypes.Dpd.is_bottom d2 then m1 else bottom
    | SlicingInternals.Cav _, SlicingInternals.Spare -> m1 (* even if [PdgTypes.Dpd.is_bottom d1] because m1 = bot *)
    | SlicingInternals.Cav d1, SlicingInternals.Cav d2 -> mk_mark (PdgTypes.Dpd.minus d1 d2)

  let pretty fmt m =
    match m with
    | SlicingInternals.Cav d -> PdgTypes.Dpd.pretty fmt d
    | SlicingInternals.Spare -> Format.fprintf fmt "[ S ]"

end

(** a [SlicingInternals.pdg_mark] is associated with each element of the PDG in a slice.
  * The first component gives the mark propagated from a user request, while
  * the second one is used to propagate informations to the called functions.
*)

let mk_m1 m1 = { SlicingInternals.m1 = m1 ; m2 = Mark.bottom }

let mk_m2 m2 = { SlicingInternals.m1 = Mark.bottom ; m2 = m2}

let bottom_mark = { SlicingInternals.m1 = Mark.bottom ; m2 = Mark.bottom }
let user_mark m = Mark.merge m.SlicingInternals.m1 m.SlicingInternals.m2
let is_bottom_mark m = (Mark.is_bottom (user_mark m))

module MarkPair = struct
  let mk_m1_spare = mk_m1 Mark.spare
  let mk_gen_spare = mk_m2 Mark.spare

  let is_top m = (Mark.is_top m.SlicingInternals.m1) && (Mark.is_top m.SlicingInternals.m2)

  let is_ctrl m = (Mark.is_included Mark.ctrl (user_mark m))
  let is_addr m = (Mark.is_included Mark.addr (user_mark m))
  let is_data m = (Mark.is_included Mark.data (user_mark m))

  let is_spare m =
    not (is_bottom_mark m) && not (is_ctrl m || is_addr m || is_data m)

  let compare = SlicingInternals.compare_pdg_mark

  let _is_included ma mb =
    Mark.is_included ma.SlicingInternals.m1 mb.SlicingInternals.m1
    && Mark.is_included ma.SlicingInternals.m2 mb.SlicingInternals.m2

  let pretty fmt m =
    Format.fprintf fmt "@[<hv><%a,@ %a>@]"
      Mark.pretty m.SlicingInternals.m1 Mark.pretty m.SlicingInternals.m2

  let to_string m =
    Format.asprintf "%a" pretty m

  let minus ma mb =
    { SlicingInternals.m1 = Mark.minus ma.SlicingInternals.m1 mb.SlicingInternals.m1;
      m2 = Mark.minus ma.SlicingInternals.m2 mb.SlicingInternals.m2 }

  (** see {! Mark.merge} *)
  let merge ma mb =
    let m1 = Mark.merge ma.SlicingInternals.m1 mb.SlicingInternals.m1 in
    let m2 = Mark.merge ma.SlicingInternals.m2 mb.SlicingInternals.m2 in
    { SlicingInternals.m1 = m1 ; m2 = m2 }

  (** merge only ma_1 et mb_1, m_2 is always bottom *)
  let merge_user_marks ma mb =
    let m1 = Mark.merge ma.SlicingInternals.m1 mb.SlicingInternals.m1 in
    { SlicingInternals.m1 = m1 ; m2 = Mark.bottom }

  let rec merge_all marks =
    match marks with
    | [] -> bottom_mark
    | m :: [] -> m (* to avoid merging with bottom every time ! *)
    | m :: tl -> merge m (merge_all tl)

  let inter ma mb =
    let m1 = Mark.inter ma.SlicingInternals.m1 mb.SlicingInternals.m1 in
    let m2 = Mark.inter ma.SlicingInternals.m2 mb.SlicingInternals.m2 in
    { SlicingInternals.m1 = m1 ; m2 = m2 }

  let rec inter_all marks =
    match marks with
    | [] -> bottom_mark
    |  m :: [] -> m
    | m :: tl -> inter m (inter_all tl)

  (** [combine ma mb] is used to add the [mb] to the [ma].
    * @return two marks : the first one is the new mark (= merge),
    *   and the second is the one to propagate.
    *   Notice that if the mark to propagate is bottom,
    *   it means that [mb] was included in [ma].
  *)
  let combine ma mb =
    let combine_m ma mb =
      let is_new, mr = Mark.combine ~old:ma mb in
      let m_to_prop = if is_new then mr else Mark.bottom in
      mr, m_to_prop
    in
    let new_m1, prop1 = combine_m ma.SlicingInternals.m1 mb.SlicingInternals.m1 in
    let new_m2, prop2 = combine_m ma.SlicingInternals.m2 mb.SlicingInternals.m2 in
    { SlicingInternals.m1 = new_m1 ; m2 = new_m2 },
    { SlicingInternals.m1 = prop1 ; m2 = prop2 }

  (** we want to know if the called function [g] with output marks
   * [m_out_called] compute enough things to be used in [f] call
   * with output marks [m_out_call].
   * Remember the [mf1] marks propagates as [mg2] and the marks to add
   * can only be [m2] marks.
   * TODO : write this down in the specification
   *        and check with Patrick if it is ok.
   * *)
  let missing_output ~call:m_out_call ~called:m_out_called =
    if debug then
      Format.printf "check_out : call=%a called=%a\n" pretty m_out_call
        pretty m_out_called;
    let mf1 = m_out_call.SlicingInternals.m1 in
    let mf2 = m_out_call.SlicingInternals.m2 in
    let mg1 = m_out_called.SlicingInternals.m1 in
    let mg2 = m_out_called.SlicingInternals.m2 in
    let needed_mg2 = (* we need (mf1 + mf2) for this out in the call *)
      Mark.merge mf1 mf2 in
    let min_mg2 = (* let remove from needed_mg2 what we have in mg1 *)
      Mark.minus needed_mg2 mg1 in
    if Mark.is_included min_mg2 mg2 then None
    else let m2 = mk_m2 min_mg2 in
      if debug then
        Format.printf "check_out missing output -> %a\n" pretty m2;
      (Some m2)

  (** tells if the caller ([f]) computes enough inputs for the callee ([g]).
   * Remember that [mg1] has to be propagated as [mf1],
   * but [mg2] has to be propagated as [mf2=spare] *)
  let missing_input ~call:m_in_call ~called:m_in_called =
    let mf1 = m_in_call.SlicingInternals.m1 in
    let mf2 = m_in_call.SlicingInternals.m2 in
    let mg1 = m_in_called.SlicingInternals.m1 in
    let mg2 = m_in_called.SlicingInternals.m2 in
    let new_mf1 = if Mark.is_included mg1 mf1 then Mark.bottom else mg1 in
    let new_mf2 =
      if (not (Mark.is_bottom mg2)) && (Mark.is_bottom mf2) then
        Mark.spare
      else Mark.bottom
    in let new_m =     { SlicingInternals.m1 = new_mf1 ; m2 = new_mf2 } in
    if is_bottom_mark new_m then None else Some new_m

end

(** [SigMarks] works on the marks in function signatures.
*)
module SigMarks = struct

  open PdgIndex

  type t = SlicingInternals.pdg_mark Signature.t

  let pretty = Signature.pretty MarkPair.pretty

  let get_input_mark (sgn:t) n = Signature.find_input sgn n
  let get_in_ctrl_mark (sgn:t) = Signature.find_in_ctrl sgn
  let get_in_top_mark (sgn:t) = Signature.find_in_top sgn

  let get_all_input_marks (sgn:t) =
    Signature.fold_all_inputs (fun acc (k, m) -> (k, m)::acc) [] sgn

  let get_matching_input_marks (sgn:t) z =
    Signature.fold_all_inputs
      (fun acc (k, m) ->
         match k with
         | PdgIndex.Signature.InCtrl | PdgIndex.Signature.InNum _ ->
           (k, m) :: acc
         | PdgIndex.Signature.InImpl z' ->
           if Locations.Zone.intersects z z' then (k, m) :: acc else acc
      ) [] sgn

  exception Visible
  let raise_if_visible () (_, m) =
    if is_bottom_mark m then () else raise Visible

  let some_visible_out cm =
    try Signature.fold_all_outputs raise_if_visible () cm ; false
    with Visible -> true

  let is_topin_visible cm =
    try
      let m = get_in_top_mark cm in
      not (is_bottom_mark m)
    with Not_found -> false

  let ctrl_visible cm =
    try
      let ctrl_m = get_in_ctrl_mark cm in
      not (is_bottom_mark ctrl_m)
    with Not_found -> false

  let some_visible_in cm =
    try Signature.fold_num_inputs raise_if_visible () cm ; ctrl_visible cm
    with Visible -> true

  let merge_inputs_m1_mark cm =
    Signature.fold_all_inputs (fun acc (_, m) -> MarkPair.merge_user_marks acc m)
      bottom_mark cm

  (** @return an under-approximation of the mark for the given location.
   * If the location is not included in the union of the implicit inputs,
   * it returns bottom.
   * Else, it returns the intersection of the inputs that intersect the location.
  *)
  let get_input_loc_under_mark cm loc =
    if debug then
      Format.printf "get_input_loc_under_mark of %a"
        Locations.Zone.pretty loc;
    assert (not (Locations.Zone.equal Locations.Zone.bottom loc));
    let do_in (marked_inputs, marks) (in_loc, m) =
      if is_bottom_mark m then (marked_inputs, [])
      else if Locations.Zone.intersects in_loc loc
      then
        let marked_inputs = Locations.Zone.link marked_inputs in_loc in
        let marks = m::marks in
        (marked_inputs, marks)
      else
        (marked_inputs, marks)
    in
    let marked_inputs = Locations.Zone.bottom in
    let marked_inputs, marks =
      Signature.fold_impl_inputs do_in (marked_inputs, []) cm in
    let m =
      if Locations.Zone.is_included loc marked_inputs
      then MarkPair.inter_all marks
      else bottom_mark
    in
    if debug then
      Format.printf "get_input_loc_under_mark : m = %a"
        MarkPair.pretty m;
    m

  let something_visible cm =
    some_visible_out cm || some_visible_in cm || ctrl_visible cm

  let get_marked_out_zone call_marks =
    let add (out0, out_zone) (out_key, m_out)  =
      if is_bottom_mark m_out then (out0, out_zone)
      else match out_key with
        | PdgIndex.Signature.OutRet -> true, out_zone
        | PdgIndex.Signature.OutLoc z ->
          out0, Locations.Zone.join out_zone z
    in Signature.fold_all_outputs add  (false, Locations.Zone.bottom) call_marks


end

(** The mark associated with a call stmt is composed of
 * marks for the call inputs (numbered form 1 to [max_in])
 * and marks for the call outputs (numbered from 0 to [max_out] *)

(** {2 Exported things} *)

(** {3 on marks} *)

let mk_gen_spare = MarkPair.mk_gen_spare
let mk_user_spare = MarkPair.mk_m1_spare
let mk_user_mark ~data ~addr ~ctrl =
  if addr || data || ctrl then
    mk_m1 (Mark.mk_adc  addr data ctrl)
  else mk_user_spare

let is_top_mark = MarkPair.is_top
let is_spare_mark = MarkPair.is_spare
let is_ctrl_mark = MarkPair.is_ctrl
let is_addr_mark = MarkPair.is_addr
let is_data_mark = MarkPair.is_data

let merge_marks = MarkPair.merge_all
let combine_marks = MarkPair.combine
let inter_marks = MarkPair.inter_all
let minus_marks = MarkPair.minus
let compare_marks = MarkPair.compare
let pretty_mark = MarkPair.pretty
let mark_to_string = MarkPair.to_string

let missing_input_mark = MarkPair.missing_input
let missing_output_mark = MarkPair.missing_output

(** {3 on signatures} *)

type sig_marks = SigMarks.t

let empty_sig = PdgIndex.Signature.empty
let get_input_mark = SigMarks.get_input_mark
let get_all_input_marks = SigMarks.get_all_input_marks
let get_matching_input_marks = SigMarks.get_matching_input_marks
let merge_inputs_m1_mark = SigMarks.merge_inputs_m1_mark
let get_input_loc_under_mark = SigMarks.get_input_loc_under_mark
(*let same_output_visibility = SigMarks.same_output_visibility*)
let get_in_ctrl_mark = SigMarks.get_in_ctrl_mark
let something_visible = SigMarks.something_visible
let some_visible_out = SigMarks.some_visible_out
let is_topin_visible = SigMarks.is_topin_visible
let get_marked_out_zone = SigMarks.get_marked_out_zone
let pretty_sig = SigMarks.pretty

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