package frama-c

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

Source file Sigma.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
(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2025                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         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).            *)
(*                                                                        *)
(**************************************************************************)

module F = Lang.F

(* -------------------------------------------------------------------------- *)
(* --- Generic Chunk Type                                                 --- *)
(* -------------------------------------------------------------------------- *)

module type ChunkType =
sig
  type t
  val self : string
  val hash : t -> int
  val equal : t -> t -> bool
  val compare : t -> t -> int
  val pretty : Format.formatter -> t -> unit
  val tau_of_chunk : t -> F.tau
  val basename_of_chunk : t -> string
  val is_init : t -> bool
  val is_primary : t -> bool
  val is_framed : t -> bool
end

(* -------------------------------------------------------------------------- *)
(* --- Generic Sigma Factory                                              --- *)
(* -------------------------------------------------------------------------- *)

type ckind = ..

module type Tag =
sig
  val tag : int
  include ChunkType with type t := ckind
end

(* memory chunks *)
type chunk = { tag : (module Tag) ; ckind : ckind }
let ckind c = c.ckind

module Chunk : ChunkType with type t = chunk =
struct
  type t = chunk
  let self = "Core"
  let hash c =
    let module T = (val c.tag) in Qed.Hcons.hash_pair T.tag @@ T.hash c.ckind
  let equal a b =
    let module A = (val a.tag) in
    let module B = (val b.tag) in
    A.tag = B.tag && A.equal a.ckind b.ckind
  let compare a b =
    let module A = (val a.tag) in
    let module B = (val b.tag) in
    match A.is_primary a.ckind, B.is_primary b.ckind with
    | true, false -> (-1)
    | false, true -> (+1)
    | true, true | false, false ->
      let cmp = Int.compare A.tag B.tag in
      if cmp <> 0 then cmp else A.compare a.ckind b.ckind

  let pretty fmt c =
    let module T = (val c.tag) in T.pretty fmt c.ckind
  let tau_of_chunk c =
    let module T = (val c.tag) in T.tau_of_chunk c.ckind
  let basename_of_chunk c =
    let module T = (val c.tag) in T.basename_of_chunk c.ckind
  let is_init c =
    let module T = (val c.tag) in T.is_init c.ckind
  let is_primary c =
    let module T = (val c.tag) in T.is_primary c.ckind
  let is_framed c =
    let module T = (val c.tag) in T.is_framed c.ckind
end

module Heap = Qed.Collection.Make(Chunk)
module Domain = Heap.Set

(* -------------------------------------------------------------------------- *)
(* --- Domain                                                             --- *)
(* -------------------------------------------------------------------------- *)

type domain = Domain.t
let empty = Domain.empty
let union = Domain.union

(* -------------------------------------------------------------------------- *)
(* --- State                                                              --- *)
(* -------------------------------------------------------------------------- *)

type state = chunk F.Tmap.t

let apply f (s:state) : state =
  F.Tmap.fold (fun t c s -> F.Tmap.add (f t) c s) s F.Tmap.empty

(* -------------------------------------------------------------------------- *)
(* --- Sigma                                                              --- *)
(* -------------------------------------------------------------------------- *)

type sigma = F.var Heap.Map.t ref

let create () = ref Heap.Map.empty
let copy sigma = ref !sigma
let newchunk c =
  let module T = (val c.tag) in
  let basename = T.basename_of_chunk c.ckind in
  let tau = T.tau_of_chunk c.ckind in
  Lang.freshvar ~basename tau

let mem (sigma : sigma) c = Heap.Map.mem c !sigma
let domain (sigma : sigma) : domain = Heap.Map.domain !sigma
let state (sigma : sigma) : state =
  let s = ref F.Tmap.empty in
  Heap.Map.iter (fun c x -> s := F.Tmap.add (F.e_var x) c !s) !sigma ; !s

let get sigma c =
  let s = !sigma in
  try Heap.Map.find c s
  with Not_found ->
    let x = newchunk c in
    sigma := Heap.Map.add c x s ; x

let value sigma c = F.e_var @@ get sigma c

let merge a b =
  let pa = ref Passive.empty in
  let pb = ref Passive.empty in
  let merge_chunk c x y =
    if F.Var.equal x y then x else
      let z = newchunk c in
      pa := Passive.bind ~fresh:z ~bound:x !pa ;
      pb := Passive.bind ~fresh:z ~bound:y !pb ;
      z in
  let merged = Heap.Map.union merge_chunk !a !b in
  ref merged , !pa, !pb

let choose a b =
  let merge_chunck _ x y = if F.Var.compare x y <= 0 then x else y in
  ref @@ Heap.Map.union merge_chunck !a !b

let join a b =
  if a == b then Passive.empty else
    let p = ref Passive.empty in
    Heap.Map.iter2
      (fun chunk x y ->
         match x,y with
         | Some x , Some y -> p := Passive.join x y !p
         | Some x , None -> b := Heap.Map.add chunk x !b
         | None , Some y -> a := Heap.Map.add chunk y !a
         | None , None -> ())
      !a !b ; !p

let havoc sigma domain =
  let ys = Domain.mapping newchunk domain in
  ref @@ Heap.Map.union (fun _v _old y -> y) !sigma ys

let remove_chunks sigma domain =
  ref @@ Heap.Map.filter (fun c _ -> not @@ Domain.mem c domain) !sigma

let havoc_chunk sigma c =
  let x = newchunk c in
  ref @@ Heap.Map.add c x !sigma

let is_init c =
  let module T = (val c.tag) in T.is_init c.ckind

let is_framed c =
  let module T = (val c.tag) in T.is_framed c.ckind

let havoc_any ~call sigma =
  let framer c x = if call && is_framed c then x else newchunk c in
  ref @@ Heap.Map.mapi framer !sigma

(* Merge All *)

type usage = Used of F.var | Unused

let merge_list (ls : sigma list) : sigma * Passive.t list =
  (* Get a map of the chunks (the data is not important) *)
  let domain =
    Heap.Map.map (fun _ -> []) @@
    let dunion _ c _ = c in
    List.fold_left
      (fun acc s -> Heap.Map.merge dunion acc !s)
      Heap.Map.empty ls in
  (* Accumulate usage for each c, preserving the order of the list *)
  let usage =
    let umerge _ c e =
      match c, e with
      | Some c, Some x -> Some (Used x :: c)
      | Some c, None -> Some (Unused :: c)
      | None, _ -> assert false in
    List.fold_left
      (fun acc s -> Heap.Map.merge umerge acc !s)
      domain (List.rev ls) in
  (* Build the passive for each sigma of the list, and the final sigma *)
  let passives = ref @@ List.map (fun _ -> Passive.empty) ls in
  let choose c uses =
    let used = function Used _ -> true | Unused -> false in
    let compatible x = function Used y -> F.Var.equal x y | Unused -> true in
    match List.filter used uses with
    | [] -> assert false
    | Used x :: others when List.for_all (compatible x) others -> x
    | _ ->
      let fresh = newchunk c in
      let join pa = function
        | Unused -> pa
        | Used bound -> Passive.bind ~fresh ~bound pa in
      passives := List.map2 join !passives uses ; fresh
  in ref @@ Heap.Map.mapi choose usage, !passives

(* Effects *)

let writes ~(pre:sigma) ~(post:sigma) : domain =
  let domain = ref Domain.empty in
  Heap.Map.iter2
    (fun c u v ->
       let written =
         match u,v with
         | Some x , Some y -> not @@ F.Var.equal x y
         | None , Some _ -> true
         | Some _ , None -> false (* no need to create a new *)
         | None, None -> assert false
       in if written then domain := Domain.add c !domain
    ) !pre !post ;
  !domain

let assigned ~(pre:sigma) ~(post:sigma) written =
  let p = ref Bag.empty in
  Heap.Map.iter2
    (fun chunk x y ->
       if not (Domain.mem chunk written) then
         match x,y with
         | Some x , Some y when x != y ->
           p := Bag.add (F.p_equal (F.e_var x) (F.e_var y)) !p
         | Some x , None -> post := Heap.Map.add chunk x !post
         | None , Some y -> pre := Heap.Map.add chunk y !pre
         | _ -> ())
    !pre !post ; !p

let iter f s = Heap.Map.iter f !s
let iter2 f a b = Heap.Map.iter2 f !a !b

let pretty fmt sigma =
  begin
    Format.fprintf fmt "{@[<hov 2>" ;
    Heap.Map.iter
      (fun c x ->
         let module T = (val c.tag) in
         Format.fprintf fmt "@ %a:%a" T.pretty c.ckind F.Var.pretty x)
      !sigma ;
    Format.fprintf fmt "@]}" ;
  end

(* -------------------------------------------------------------------------- *)
(* --- Chunks                                                             --- *)
(* -------------------------------------------------------------------------- *)

module Make(C : ChunkType) =
struct
  type ckind += Mu of C.t
  module T =
  struct
    let self = C.self
    let tag = Obj.Extension_constructor.id [%extension_constructor Mu]
    let map f = function Mu m -> f m | _ -> assert false
    let map2 f a b =
      match a,b with Mu a, Mu b -> f a b | _ -> assert false
    let hash = map C.hash
    let equal = map2 C.equal
    let compare = map2 C.compare
    let is_init = map C.is_init
    let is_primary = map C.is_primary
    let is_framed = map C.is_framed
    let tau_of_chunk = map C.tau_of_chunk
    let basename_of_chunk = map C.basename_of_chunk
    let pretty fmt = map (C.pretty fmt)
  end
  let tag = (module T : Tag)
  let chunk c = { tag ; ckind = Mu c }
  let mem sigma c = mem sigma @@ chunk c
  let get sigma c = get sigma @@ chunk c
  let value sigma c = value sigma @@ chunk c
  let singleton c = Domain.singleton @@ chunk 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