package frama-c

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

Source file mt_types.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of Frama-C.                                         *)
(*                                                                        *)
(*  Copyright (C) 2007-2025                                               *)
(*    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 Mt_cil
open Mt_memory.Types
open Mt_lib
module ALoc = Analysis_location


(* -------------------------------------------------------------------------- *)
(* --- Variable access kind                                               --- *)
(* -------------------------------------------------------------------------- *)


type rw = Read | Write of Locations.location
        | ReadAloc of ALoc.t | WriteAloc of ALoc.t

module RW = struct
  include Datatype.Make(
    struct
      include Datatype.Serializable_undefined
      type t = rw
      let name = "rw"
      let reprs = [Read]
      let equal rw1 rw2 = match rw1, rw2 with
        | Read, Read -> true
        | Write l1, Write l2 -> Locations.Location.equal l1 l2
        | Read, Write _ | Write _, Read -> false
        | ReadAloc aloc1, ReadAloc aloc2
        | WriteAloc aloc1, WriteAloc aloc2 -> ALoc.equal aloc1 aloc2
        | ReadAloc _, WriteAloc _ | WriteAloc _, ReadAloc _ -> false
        | (Read | Write _), (ReadAloc _ | WriteAloc _)
        | (ReadAloc _ | WriteAloc _), (Read | Write _) -> false
      let compare rw1 rw2 = match rw1, rw2 with
        | Read, Read -> 0
        | Write l1, Write l2 -> Locations.Location.compare l1 l2
        | Read, Write _ -> -1
        | Write _, Read -> 1
        | ReadAloc aloc1, ReadAloc aloc2
        | WriteAloc aloc1, WriteAloc aloc2 -> ALoc.compare aloc1 aloc2
        | ReadAloc _, WriteAloc _ -> -1
        | WriteAloc _, ReadAloc _ -> +1
        | (Read | Write _), (ReadAloc _ | WriteAloc _) -> -2
        | (ReadAloc _ | WriteAloc _), (Read | Write _) -> +2
      let hash = function
        | ReadAloc aloc -> 1 + Hashtbl.hash (1, ALoc.hash aloc)
        | WriteAloc aloc -> 1 + Hashtbl.hash (2, ALoc.hash aloc)
        | Write l -> 1 + Hashtbl.hash (3, Locations.Location.hash l)
        | Read -> 0
      let pretty fmt rw = Format.fprintf fmt "%s"
          (match rw with
           | Read -> "read"
           | Write _ -> "write"
           | ReadAloc _ -> "read"
           | WriteAloc _ -> "write"
          )
    end)

  let loc op =
    match op with
    | Read | Write _ -> Location.unknown
    | ReadAloc aloc | WriteAloc aloc -> ALoc.loc aloc

  let is_read op =
    match op with
    | Read -> true
    | Write _ -> false
    | ReadAloc _ -> true
    | WriteAloc _ -> false

  let pretty_op fmt rw = pretty fmt rw

  let pretty_loc fmt rw =
    match rw with
    | Read -> Format.fprintf fmt "<noloc>"
    | Write l -> Locations.Location.pretty fmt l
    | ReadAloc aloc | WriteAloc aloc -> ALoc.pretty_loc fmt aloc
end

(* -------------------------------------------------------------------------- *)
(* --- Multi-threading events                                             --- *)
(* -------------------------------------------------------------------------- *)

type event =
  | CreateThread of Thread.t
  | StartThread of Thread.t
  | SuspendThread of Thread.t
  | CancelThread of Thread.t
  | ThreadExit of value
  | MutexLock of Mutex.t
  | MutexRelease of Mutex.t
  | CreateQueue of Mqueue.t * int option
  | SendMsg of Mqueue.t * (slice * int)
  | ReceiveMsg of Mqueue.t * pointer * int
  | VarAccess of rw * Locations.Zone.t
  | Dummy of string * value list

module Event = struct
  type t = event

  let pretty fmt = function
    | CreateThread th -> Format.fprintf fmt "Create thread %a" Thread.pretty th
    | StartThread th -> Format.fprintf fmt "Start thread %a" Thread.pretty th
    | SuspendThread th -> Format.fprintf fmt "Suspend thread %a" Thread.pretty th
    | CancelThread th -> Format.fprintf fmt "Cancel thread %a" Thread.pretty th
    | ThreadExit v -> Format.fprintf fmt "Thread exit, with code %a"
                        Cvalue.V.pretty v
    | MutexLock m -> Format.fprintf fmt "Lock %a" Mutex.pretty m
    | MutexRelease m -> Format.fprintf fmt "Release %a" Mutex.pretty m
    | CreateQueue (q, s) ->
      Format.fprintf fmt "Creating queue %a%a" Mqueue.pretty q
        (fun fmt -> function None -> ()
                           | Some s -> Format.fprintf fmt " (size %d)" s) s
    | SendMsg (q, (v, _s)) -> Format.fprintf fmt
                                "Sending@ message@ on %a,@ content@ %a"
                                Mqueue.pretty q Mt_memory.pretty_slice v
    | ReceiveMsg (q, loc, size) -> Format.fprintf fmt
                                     "Receiving@ message@ on %a,@ max size %d,@ stored in %a."
                                     Mqueue.pretty q size Pointer.pretty loc
    | VarAccess (rw, loc) ->
      Format.fprintf fmt "Var access@ %a@ of %a"
        RW.pretty rw Locations.Zone.pretty loc
    | Dummy (s, l) ->
      Format.fprintf fmt "%s %a" s
        (Pretty_utils.pp_list ~sep:"@ " Cvalue.V.pretty) l

  let equal a1 a2 = match a1, a2 with
    | CreateThread th1, CreateThread th2
    | StartThread th1, StartThread th2
    | SuspendThread th1, SuspendThread th2
    | CancelThread th1, CancelThread th2 -> Thread.equal th1 th2
    | MutexLock m1, MutexLock m2
    | MutexRelease m1, MutexRelease m2 -> Mutex.equal m1 m2
    | CreateQueue (q1, s1), CreateQueue (q2, s2) ->
      Mqueue.equal q1 q2 && s1 = s2
    | SendMsg (q1, (v1, s1)), SendMsg (q2, (v2, s2)) ->
      Mqueue.equal q1 q2 && Cvalue.V_Offsetmap.equal v1 v2 && s1 = s2
    | ReceiveMsg (q1, l1, s1), ReceiveMsg (q2, l2, s2) ->
      s1 = s2 && Mqueue.equal q1 q2 && Pointer.equal l1 l2
    | VarAccess (rw1, z1), VarAccess (rw2, z2) ->
      RW.equal rw1 rw2 && Locations.Zone.equal z1 z2
    | (CreateThread _ | StartThread _ | SuspendThread _ | CancelThread _
      | ThreadExit _
      | MutexLock _ | MutexRelease _ | CreateQueue _
      | SendMsg _ | ReceiveMsg _ | VarAccess _ | Dummy _), _ ->
      false


  let compare a1 a2 = match a1, a2 with
    | CreateThread th1, CreateThread th2
    | StartThread th1, StartThread th2
    | SuspendThread th1, SuspendThread th2
    | CancelThread th1, CancelThread th2 -> Thread.compare th1 th2
    | MutexLock m1, MutexLock m2
    | MutexRelease m1, MutexRelease m2 -> Mutex.compare m1 m2
    | ThreadExit v1, ThreadExit v2 -> Cvalue.V.compare v1 v2
    | CreateQueue (q1, s1), CreateQueue (q2, s2) ->
      comp compare s1 s2 Mqueue.compare q1 q2
    | SendMsg (q1, (v1, s1)), SendMsg (q2, (v2, s2)) ->
      comp Stdlib.compare s1 s2
        (comp Cvalue.V_Offsetmap.compare v1 v2 Mqueue.compare)
        q1 q2
    | ReceiveMsg (q1, l1, s1), ReceiveMsg (q2, l2, s2) ->
      comp Stdlib.compare s1 s2
        (comp Pointer.compare l1 l2 Mqueue.compare)
        q1 q2
    | VarAccess (rw1, z1), VarAccess (rw2, z2) ->
      comp RW.compare rw1 rw2 Locations.Zone.compare z1 z2
    | Dummy (s1, l1), Dummy (s2, l2) ->
      comp String.compare s1 s2
        (Extlib.list_compare Cvalue.V.compare) l1 l2
    | (CreateThread _ | StartThread _ | SuspendThread _ | CancelThread _
      | ThreadExit _
      | MutexLock _ | MutexRelease _ | CreateQueue _
      | SendMsg _ | ReceiveMsg _ | VarAccess _ | Dummy _), _ ->
      Mt_lib.compare_tag a1 a2

  let hash = function
    | CreateThread th -> Hashtbl.hash (Thread.hash th, 0)
    | CancelThread th -> Hashtbl.hash (Thread.hash th, 1)
    | MutexLock m -> Hashtbl.hash (Mutex.hash m, 2)
    | MutexRelease m -> Hashtbl.hash (Mutex.hash m, 3)
    | CreateQueue (q, s) -> Hashtbl.hash (Mqueue.hash q, s, 4)
    | SendMsg (q, (v, s)) ->
      Hashtbl.hash (Mqueue.hash q, Cvalue.V_Offsetmap.hash v, s, 5)
    | ReceiveMsg (q, l, size) ->
      Hashtbl.hash (Mqueue.hash q, Pointer.hash l, size, 6)
    | VarAccess (rw, z) -> Hashtbl.hash (RW.hash rw, Locations.Zone.hash z, 7)
    | ThreadExit v -> Hashtbl.hash (Cvalue.V.hash v, 8)
    | Dummy (s, l) -> Hashtbl.hash (s, List.map Cvalue.V.hash l, 9)
    | StartThread th -> Hashtbl.hash (Thread.hash th, 10)
    | SuspendThread th -> Hashtbl.hash (Thread.hash th, 11)

end

module EventsSet = struct
  include Set.Make(Event)

  let threads_created s =
    fold (fun act l -> match act with
        | CreateThread id -> id :: l
        | _ -> l) s []

  let pretty ?(sep=("@ ": (_, _, _, _, _, _) format6)) () fmt =
    Pretty_utils.pp_iter ~pre:"" ~suf:"" ~sep iter Event.pretty fmt

end
type events_set = EventsSet.t


(* -------------------------------------------------------------------------- *)
(* --- Execution traces                                                   --- *)
(* -------------------------------------------------------------------------- *)

module Trace =
struct

  module TriesStacks = Trie.Make(Map.Make(StackElt))

  type data = {
    trace_events: events_set;
    trace_states: state Stmt.Map.t;
    trace_states_after: state Stmt.Map.t;
  }

  let join_data d1 d2 = {
    trace_events = EventsSet.union d1.trace_events d2.trace_events;
    trace_states = merge_map_functions_states d1.trace_states d2.trace_states;
    trace_states_after =
      merge_map_functions_states d1.trace_states_after d2.trace_states_after;
  }

  type t = data TriesStacks.t

  let empty = TriesStacks.empty

  let is_empty = TriesStacks.is_empty

  let default = {
    trace_events = EventsSet.empty;
    trace_states = Stmt.Map.empty;
    trace_states_after = Stmt.Map.empty;
  }

  let union = TriesStacks.union (fun _ d1 d2 -> Some (join_data d1 d2))

  let add_prefix = TriesStacks.add_prefix

  let add_aux f (trie: t) (stack : stack) =
    let cur =
      try TriesStacks.find stack trie
      with Not_found -> default
    in
    TriesStacks.add stack (f cur) trie

  let add_event t s evt =
    add_aux
      (fun d -> { d with trace_events = EventsSet.add evt d.trace_events}) t [s]

  let add_states t ~before ~after =
    add_aux
      (fun d -> { d with
                  trace_states = merge_map_non_map_functions_states d.trace_states before;
                  trace_states_after =
                    merge_map_non_map_functions_states d.trace_states_after after;
                })
      t []

  let subtrace_at_call trie call =
    try TriesStacks.select_prefix call trie
    with Not_found -> empty

  let no_deep_call trie =
    (* this is true if the trie only contains a singleton key of size 1 *)
    TriesStacks.prefixes_seq trie () = Seq.Nil


  let find_at_stmt trie stmt =
    TriesStacks.prefixes_seq trie
    |> Seq.filter
      (fun ((_,kinstr), _) ->
         match kinstr with
         | Kglobal -> false
         | Kstmt s -> Cil_datatype.Stmt.equal s stmt)
    |> List.of_seq


  let at_root trie =
    TriesStacks.find_opt [] trie

  let at_call trie call =
    try Some (TriesStacks.find [call] trie)
    with Not_found -> None

  let fold (trie : t) f =
    TriesStacks.fold
      (fun stack d -> EventsSet.fold (f stack) d.trace_events) trie

  let fold' t f = fold t (fun _ -> f)

  let iter (trie : t) f =
    TriesStacks.iter
      (fun stack d -> EventsSet.iter (f stack) d.trace_events) trie

  let iter' t f = iter t (fun _ -> f)

  let exists (trie : t) f =
    TriesStacks.exists
      (fun stack d -> EventsSet.exists (f stack) d.trace_events) trie

  let find_events f t =
    fold' t (fun evt acc -> if f evt then EventsSet.add evt acc else acc)
      EventsSet.empty


  let pretty fmt t =
    Format.fprintf fmt "@[<v>";
    TriesStacks.iter
      (fun stack d ->
         Format.fprintf fmt
           "stack:@ %a@ actions:@[%a@]@ @ "
           Stack.pretty stack (EventsSet.pretty ()) d.trace_events) t;
    Format.fprintf fmt "@]@.";
end


(* -------------------------------------------------------------------------- *)
(* --- Live threads/taken mutexes at a given point of execution           --- *)
(* -------------------------------------------------------------------------- *)

type presence_flag = NotPresent | Present | MaybePresent

module PresenceFlag = struct

  include Datatype.Make(
    struct
      include Datatype.Serializable_undefined
      type t = presence_flag
      let name = "Mt_types.presence_flag"
      let reprs = [NotPresent; Present; MaybePresent]
      let equal : t -> t -> _ = (=)
      let compare : t -> t -> int = Stdlib.compare
      let hash : t -> _ = Hashtbl.hash
    end)

  let combine p1 p2 = match p1, p2 with
    | Present, Present -> Present
    | NotPresent, NotPresent -> NotPresent
    | _ -> MaybePresent

  let fast_equal = equal

end


module type Presence = sig
  type key
  type t

  module KeySet: Set.S with type elt = key

  val pretty: t Pretty_utils.formatter

  val equal: t -> t -> bool
  val hash: t -> int
  val compare: t -> t -> int

  val empty: t
  val is_empty: t -> bool

  val find: t -> key -> presence_flag

  val add: key -> presence_flag -> t -> t

  val combine: t -> t -> t

  val only_present: t -> KeySet.t
end


module MakePresence (Key: Datatype.S_with_collections) = struct
  (* Implementation of maps on threads with hashing information. Invariant:
     we never store [NotPresent] inside the table, as it is the default
     value, and this introduces non-canonicity problems. (This is not
     disastrous per se, but this also implies that [equal m1 m2] does not
     imply [hash m1 = hash m2], a bad idea...) *)
  module M = Rangemap.Make(Key)(PresenceFlag)

  type t = M.t
  type key = Key.t

  module KeySet = Key.Set

  let pretty_with_flag fmt (th, p) = match p with
    | NotPresent -> ()
    | MaybePresent -> Format.fprintf fmt "(?)%a" Key.pretty th
    | Present -> Format.fprintf fmt "%a" Key.pretty th

  let pretty = Pretty_utils.pp_iter ~pre:"" ~suf:"" ~sep:"@ "
      (fun f -> M.iter (fun k v -> f (k, v))) pretty_with_flag

  let equal = M.equal
  let compare = M.compare
  let hash = M.hash

  let find (p : t) id =
    try M.find id p
    with Not_found -> NotPresent

  let add k v m =
    match v with
    | NotPresent -> M.remove k m
    | _ -> M.add k v m

  let conv = function
    | None -> NotPresent
    | Some v -> v

  let combine_aux f =
    let aux p1 p2 =
      match f (conv p1) (conv p2) with
      | NotPresent -> None (* Make sure not to store NotPresent *)
      | p -> Some p
    in
    M.merge (fun _ -> aux)


  let combine = combine_aux PresenceFlag.combine

  let empty = M.empty

  let is_empty = M.is_empty

  let only_present m =
    let aux id flag acc =
      if flag = Present then Key.Set.add id acc else acc
    in
    M.fold aux m KeySet.empty


end


module ThreadPresence = MakePresence (Thread)
module MutexPresence = MakePresence (Mutex)
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