package mopsa

  1. Overview
  2. Docs
package mopsa
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Source file partial_inversible_map.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
(****************************************************************************)
(*                                                                          *)
(* This file is part of MOPSA, a Modular Open Platform for Static Analysis. *)
(*                                                                          *)
(* Copyright (C) 2017-2019 The MOPSA Project.                               *)
(*                                                                          *)
(* This program is free software: 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, either version 3 of the License, or     *)
(* (at your option) any later version.                                      *)
(*                                                                          *)
(* This program 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.                      *)
(*                                                                          *)
(* You should have received a copy of the GNU Lesser General Public License *)
(* along with this program.  If not, see <http://www.gnu.org/licenses/>.    *)
(*                                                                          *)
(****************************************************************************)


(** Lattice of partial inversible maps.

    Sets of partial maps M ∈ ℘(𝕂 ⇀ 𝕍) from concrete keys set 𝕂 to
    concrete values set 𝕍 are abstracted as a set of partial maps ℳ ∈
    𝕂 ⇀ (℘(𝕍) ∪ {⊤}).
*)



open Mopsa_utils
open Bot_top
open Top
open Core.All



(** Signature of ordered types with printers *)
module type ORDER =
sig
  type t
  val compare: t -> t -> int
  val print : Print.printer -> t -> unit
end


module Make
    (Key   : ORDER)
    (Value : ORDER)
=
struct


  (** Inversible relations between keys and values *)
  module Relation = InvRelation.Make(Key)(Value)


  (** Set of keys *)
  module KeySet = Relation.DomSet


  (** Set of values *)
  module ValueSet = Relation.CoDomSet


  (** Inversible maps are represented as a set of relations between keys and
      values, in addition to a set of keys mapped to ⊤
  *)
  type map = {
    relations: Relation.t;
    top_keys: Relation.DomSet.t
  }


  (** Type of inversible maps with ⊤ and ⊥ *)
  type t = map with_bot_top


  (** ⊥ element *)
  let bottom : t = BOT


  (** ⊤ element *)
  let top : t = TOP


  (** Check whether [a] is ⊥ *)
  let is_bottom (a:t) : bool =
    match a with
    | BOT -> true
    | TOP -> false
    | Nbt m -> false


  (** Printing. *)
  let print printer (a:t) : unit =
    match a with
    | BOT ->
      pp_string printer "⊥"

    | TOP ->
      pp_string printer "⊤"

    | Nbt m when Relation.is_empty m.relations
              && KeySet.is_empty m.top_keys ->
      pp_string printer "∅"

    | Nbt m ->
      Relation.iter_domain (fun k vs ->
          pprint printer ~path:[pkey Key.print k]
            (pbox (pp_list Value.print ~lopen:"{" ~lsep:", " ~lclose:"}") (ValueSet.elements vs))
        ) m.relations;
      KeySet.iter (fun k ->
          pp_string printer "⊤"
            ~path:[pkey Key.print k]
        ) m.top_keys


  (** Singleton of empty map *)
  let empty : t = Nbt { relations = Relation.empty; top_keys = KeySet.empty }


  (** Remove a set of keys from a relation *)
  let remove_relation_keys (keys:KeySet.t) (rel:Relation.t) : Relation.t =
    KeySet.fold Relation.remove_image keys rel


  (** Inclusion test. *)
  let subset (a1:t) (a2:t) : bool =
    if a1 == a2 then true else
    match a1, a2 with
    | BOT, _ -> true
    | _, BOT -> false
    | _, TOP -> true
    | TOP, _ -> false
    | Nbt m1, Nbt m2 ->
      (* Remove keys of m1 that valuate to ⊤ in m2 *)
      let m1' = { m1 with relations = remove_relation_keys m2.top_keys m1.relations } in
      Relation.subset m1'.relations m2.relations &&
      KeySet.subset m1'.top_keys m2.top_keys


  (** Join two sets of partial maps. *)
  let join (a1:t) (a2:t) : t =
    if a1 == a2 then a1 else
    match a1, a2 with
      | BOT, x | x, BOT -> x
      | TOP, _ | _, TOP -> TOP
      | Nbt m1, Nbt m2 ->
        (* Remove keys that valuate to ⊤ in m1 or m2 *)
        let m1' = { m1 with relations = remove_relation_keys m2.top_keys m1.relations } in
        let m2' = { m2 with relations = remove_relation_keys m1.top_keys m2.relations } in
        Nbt {
          relations = Relation.union m1'.relations m2'.relations;
          top_keys = KeySet.union m1.top_keys m2.top_keys;
        }


  (** Meet. *)
  let meet (a1:t) (a2:t) : t =
    if a1 == a2 then a1 else
    match a1, a2 with
      | BOT, x | x, BOT -> BOT
      | TOP, x | x, TOP -> x
      | Nbt m1, Nbt m2 ->
        (* In addition to bindings that are part of the two relations,
           keep the bindings that are in one relation only if the key
           belongs to ⊤ keys of the other abstract element.
        *)
        try
          Nbt (
            let relations = Relation.map2zo_domain
                (fun k1 vs1 ->
                   (* Check if k1 is mapped to ⊤ in m2 *)
                   if KeySet.mem k1 m2.top_keys
                   then vs1
                   else raise Bot.Found_BOT
                )
                (fun k2 vs2 ->
                   (* Check if k2 is mapped to ⊤ in m1 *)
                   if KeySet.mem k2 m1.top_keys
                   then vs2
                   else raise Bot.Found_BOT
                )
                (fun k vs1 vs2 ->
                   let vs = ValueSet.inter vs1 vs2 in
                   if ValueSet.is_empty vs
                   then raise Bot.Found_BOT
                   else vs
                )
                m1.relations m2.relations
            in
            let top_keys = KeySet.inter m1.top_keys m2.top_keys in
            { relations; top_keys }
          )
        with Bot.Found_BOT -> bottom


  (** Widening operator *)
  let widen ctx (a1:t) (a2:t) : t =
    let a2 = join a1 a2 in
    if a1 == a2 then a1 else
      match a1, a2 with
      | BOT, x | x, BOT -> x
      | TOP, x | x, TOP -> TOP
      | Nbt m1, Nbt m2 ->
        (* Find the keys that belong only to m2, i.e. new relations. These keys will be mapped to ⊤. *)
        let instable_keys = Relation.fold2_diff
            (fun _ _ acc -> acc)
            (fun k _ acc -> KeySet.add k acc)
            m1.relations m2.relations KeySet.empty
        in
        (* Remove instable_keys from m2 relations and add them to top_keys *)
        Nbt {
          relations = remove_relation_keys instable_keys m2.relations;
          top_keys = KeySet.union m2.top_keys instable_keys
        }


  (** Find the set of values attached to a key. Raise [Not_found] of the key is not found. *)
  let find (k: Key.t) (a:t) : ValueSet.t with_top =
    match a with
    | BOT -> Nt ValueSet.empty
    | TOP -> TOP
    | Nbt m ->
      if KeySet.mem k m.top_keys then TOP else Nt (Relation.image k m.relations)


  (** Find keys attached to value [v] in [a] *)
  let find_inverse (v:Value.t) (a:t) : KeySet.t with_top =
    match a with
    | BOT -> Nt (KeySet.empty)
    | TOP -> TOP
    | Nbt m ->
      let s1 = Relation.inverse v m.relations in
      let s2 = m.top_keys in
      Nt (KeySet.union s1 s2)


  (** Remove all bindings [(k,-)] in [a] *)
  let remove (k: Key.t) (a:t) : t =
    match a with
    | BOT -> BOT
    | TOP -> TOP
    | Nbt m ->
      Nbt { relations = Relation.remove_image k m.relations; top_keys = KeySet.remove k m.top_keys }


  (** Remove all bindings [(-,v)] in [a] *)
  let remove_inverse (v:Value.t) (a:t) : t =
    match a with
    | BOT -> BOT
    | TOP -> TOP
    | Nbt m ->
      Nbt { m with relations = Relation.remove_inverse v m.relations }


  (** [filter f a] keeps all bindings [(k,vs)] in [a] such that [f k vs] is true *)
  let filter (f:Key.t -> ValueSet.t with_top -> bool) (a:t) : t =
    match a with
    | BOT -> BOT
    | TOP -> TOP
    | Nbt m ->
      Nbt { relations = Relation.filter_domain (fun k vs -> f k (Top.Nt vs)) m.relations;
            top_keys  = KeySet.filter (fun k -> f k Top.TOP) m.top_keys }

  (** [filter_inverse f a] keeps all inverse bindings [(v,ks)] in [a] such that [f v ks] is true *)
  let filter_inverse (f:Value.t -> KeySet.t -> bool) (a:t) : t =
    match a with
    | BOT -> BOT
    | TOP -> TOP
    | Nbt m -> Nbt { m with relations = Relation.filter_codomain f m.relations }

  (* val filter_inverse : (value -> KeySet.t -> bool) -> t
   * (\** [filter_inverse f a] keeps all inverse bindings [(v,ks)] in [a] such that [f v ks] is true *\) *)

  (** Add bindings [(k,vs)] to [a]. Previous bindings are overwritten. *)
  let set (k: Key.t) (vs:ValueSet.t with_top) (a:t) : t =
    match vs with
    | Nt s when ValueSet.is_empty s -> BOT
    | _ ->
      match a with
      | BOT -> BOT
      | TOP -> TOP
      | Nbt m ->
        match vs with
        | TOP -> Nbt { top_keys = KeySet.add k m.top_keys; relations = Relation.remove_image k m.relations }
        | Nt vs -> Nbt { top_keys = KeySet.remove k m.top_keys; relations = Relation.set_image k vs m.relations }


  (** [add_inverse v ks a] adds the binding [(k,{v} ∪ find k a)] to [a], where [k] ∈ [ks]. *)
  let add_inverse (v:Value.t) (ks:KeySet.t) (a:t) : t =
    match a with
    | BOT -> BOT
    | TOP -> TOP
    | Nbt m ->
      (* Do not add bindings for keys k ∈ m.top_keys *)
      let ks' = KeySet.diff ks m.top_keys in
      Nbt { m with relations = Relation.add_inverse_set v ks' m.relations }


  (** Rename key [k] to [k'] *)
  let rename (k: Key.t) (k': Key.t) (a:t) : t =
    let v = find k a in
    let a = remove k a in
    set k' v a

  (** Rename value [v] to [v'] *)
  let rename_inverse (v: Value.t) (v': Value.t) (a:t) : t =
    let ks = find_inverse v a in
    let a = remove_inverse v a in
    match ks with
    | TOP ->
       assert(a = TOP);
       TOP
    | Nt ks ->
       add_inverse v' ks a

  (** Create a map with singleton binding [(k,{v})] *)
  let singleton (k:Key.t) (v:Value.t) : t =
    Nbt {
      top_keys = KeySet.empty;
      relations = Relation.singleton k v;
    }


  (** Check whether a binding [(k,-)] exists in [a] *)
  let mem (k:Key.t) (a:t) : bool =
    match a with
    | BOT -> false
    | TOP -> true
    | Nbt m -> Relation.mem_domain k m.relations ||
               KeySet.mem k m.top_keys

  (** Check whether a binding [(-,v)] exists in [a] *)
  let mem_inverse (v:Value.t) (a:t) : bool =
    match a with
    | BOT -> false
    | TOP -> true
    | Nbt m -> Relation.mem_codomain v m.relations ||
                 not @@ Relation.DomSet.is_empty m.top_keys

  (** [fold f a init] folds function [f] over elements [(k,vs)] *)
  let fold (f:Key.t -> ValueSet.t with_top -> 'a -> 'a) (a:t) (init:'a) : 'a =
    match a with
    | BOT -> init
    | TOP -> raise Found_TOP
    | Nbt m ->
      KeySet.fold (fun k acc -> f k TOP acc) m.top_keys init |>
      Relation.fold_domain (fun k vs acc -> f k (Nt vs) acc) m.relations

  (** Replace bindings [(k,vs)] in [a] with [(k,f vs)] *)
  let map (f:ValueSet.t with_top -> ValueSet.t with_top) (a:t) : t =
    match a with
    | BOT -> BOT
    | TOP -> TOP
    | Nbt m ->
      fold (fun k vs acc ->
          set k (f vs) acc
        ) a empty


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