package mopsa

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

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

(** Powerset lattice with finite cardinality elements or ⊺. *)

open Mopsa_utils
open Core.All
open Top

module type ELT =
sig
  type t
  val compare: t -> t -> int
  val print : printer -> t -> unit
end


module Make(Elt: ELT) =
struct
  module Set = SetExt.Make(Elt)

  type v = Set.t

  type t = v with_top

  let bottom : t = Nt Set.empty

  let top : t = TOP

  let is_top (abs: t) = abs = TOP

  let subset (abs1:t) (abs2:t) : bool =
    top_included Set.subset abs1 abs2

  let equal (abs1:t) (abs2:t) : bool =
    top_equal Set.equal abs1 abs2

  let compare (abs1:t) (abs2:t) : int =
    match abs1, abs2 with
    | TOP, TOP -> 0
    | TOP, _ -> -1
    | _, TOP -> 1
    | Nt x1, Nt x2 -> Set.compare x1 x2

  let join (abs1:t) (abs2:t) : t =
    if abs1 == abs2 then abs1 else
    top_lift2 Set.union abs1 abs2

  let meet (abs1:t) (abs2:t) : t =
    if abs1 == abs2 then abs1 else
    top_neutral2 Set.inter abs1 abs2

  let union = join

  let inter = meet

  let diff (abs1:t) (abs2:t) : t =
    if is_top abs2
    then bottom
    else top_lift2 Set.diff abs1 abs2

  let widen ctx (abs1:t) (abs2:t) : t =
    top_absorb2
      (fun s1 s2 ->
         if Set.subset s2 s1 then
           abs2
         else
           TOP
      )
      abs1 abs2

  let print printer (abs:t) =
    match abs with
    | Top.TOP -> pp_string printer "⊤"
    | Top.Nt s ->
      if Set.is_empty s then pp_string printer "∅"
      else
        pp_set Elt.print printer (Set.to_poly_set s) ~sopen:"{" ~ssep:"," ~sclose:"}"

  let add v (abs:t) : t =
    top_lift1 (Set.add v) abs

  let fold (f:Elt.t->'a->'a) (abs:t) (init:'a) : 'a =
    top_to_exn abs |> (fun s -> Set.fold f s init)

  let remove (v:Elt.t) (abs:t) : t =
    top_lift1 (Set.remove v) abs

  let mem (v:Elt.t) (abs:t) : bool =
    top_dfl1 true (Set.mem v) abs

  let filter f (abs:t) : t =
    top_lift1 (Set.filter f) abs

  let partition f (abs:t) : t * t =
    match abs with
    | TOP -> TOP, TOP
    | Nt a ->
      let r1, r2 = Set.partition f a in
      Nt r1, Nt r2

  let exists f (abs:t) : bool =
    top_to_exn abs |> (fun s -> Set.exists f s)

  let for_all f (abs:t) : bool =
    top_to_exn abs |> (fun s -> Set.for_all f s)

  let cardinal (abs:t) : int =
    top_to_exn abs |> (fun s -> Set.cardinal s)

  let find f (abs:t) : Elt.t =
    top_to_exn abs |> (fun s -> Set.find f s)

  let choose (abs:t) : Elt.t =
    top_to_exn abs |> (fun s -> Set.choose s)

  let singleton (x:Elt.t) : t = Nt (Set.singleton x)

  let of_list (l:Elt.t list) =
    Nt (Set.of_list l)

  let is_empty (abs:t) =
    top_dfl1 false Set.is_empty abs

  let is_singleton a =
    top_apply (fun s ->
        Set.cardinal s = 1 (* FIXME: computing the cardinal for this check is inefficient *)
      ) false a

  let empty = bottom

  let is_bottom = is_empty

  let elements (abs:t) =
    top_to_exn abs |> Set.elements

  let map (f:Elt.t -> Elt.t)  (abs:t) : t =
    top_lift1 (Set.map f) abs

  let iter (f:Elt.t -> unit) (abs:t) : unit =
    top_to_exn abs |> Set.iter f

  let apply (f:Set.t -> 'a) (dfl:'a) (abs:t) : 'a = Top.top_apply f dfl abs

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