package mopsa

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

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


(** Generators of identifiers for domains and values *)

open Mopsa_utils
open Eq


type _ id = ..

type _ id += I_stateful_domain : 'a id -> 'a id
type _ id += I_stateless_domain : 'a id -> 'a id
type _ id += I_value : 'a id -> 'a id


type witness = {
  eq :  'a 'b. 'a id -> 'b id -> ('a,'b) eq option;
}

type witness_chain = {
  eq :  'a 'b. witness -> 'a id -> 'b id -> ('a,'b) eq option;
}

let empty_witness : witness = {
  eq = (fun _ _ -> None)
}

type pool =
  { mutable stateful : witness;
    mutable stateless: witness;
    mutable value: witness;
    mutable others: witness; }

let pool =
  { stateful = empty_witness;
    stateless = empty_witness;
    value = empty_witness;
    others = empty_witness; }


let register_id (w:witness_chain) =
  let old = pool.others in
  pool.others <- { eq = (fun (type a) (type b) (id1:a id) (id2:b id) -> w.eq old id1 id2) }

let register_stateful_id (w:witness_chain) =
  let old = pool.stateful in
  pool.stateful <- { eq = (fun (type a) (type b) (id1:a id) (id2:b id) -> w.eq old id1 id2) }

let register_stateless_id (w:witness_chain) =
  let old = pool.stateless in
  pool.stateless <- { eq = (fun (type a) (type b) (id1:a id) (id2:b id) -> w.eq old id1 id2) }

let register_value_id (w:witness_chain) =
  let old = pool.value in
  pool.value <- { eq = (fun (type a) (type b) (id1:a id) (id2:b id) -> w.eq old id1 id2) }


(** Equality witness of domain identifiers *)
let equal_id (id1:'a id) (id2:'b id) : ('a,'b) eq option =
  match id1, id2 with
  | I_stateful_domain i1, I_stateful_domain i2 ->
    pool.stateful.eq i1 i2

  | I_stateful_domain _, _ | _, I_stateful_domain _ -> None

  | I_stateless_domain i1, I_stateless_domain i2 ->
    pool.stateless.eq i1 i2

  | I_stateless_domain _, _ | _, I_stateless_domain _ -> None

  | I_value i1, I_value i2 ->
    pool.value.eq i1 i2

  | I_value _, _ | _, I_value _ -> None

  | _ -> pool.others.eq id1 id2


(** Generator of a new identifier *)

module GenId(Spec:sig
    type t
  end) =
struct

  type _ id += Id : Spec.t id

  let id = Id

  let () = register_id {
      eq = (
        let f : type a b. witness -> a id -> b id -> (a,b) eq option = fun next id1 id2 ->
          match id1, id2 with
          | Id, Id -> Some Eq
          | _      -> next.eq id1 id2
        in
        f
      );
    }

end

module GenDomainId(Spec:sig
    type t
    val name : string
  end) =
struct

  type _ id += Id : Spec.t id

  let id = I_stateful_domain Id

  let name = Spec.name

  let debug fmt = Debug.debug ~channel:Spec.name fmt

  let () = register_stateful_id {
      eq = (
        let f : type a b. witness -> a id -> b id -> (a,b) eq option = fun next id1 id2 ->
          match id1, id2 with
          | Id, Id -> Some Eq
          | _      -> next.eq id1 id2
        in
        f
      );
    }
end


(** Generator of a new identifier for stateless domains *)
module GenStatelessDomainId(Spec:sig
    val name : string
  end)
=
struct

  type _ id += Id : unit id

  let id = I_stateless_domain Id

  let name = Spec.name

  let debug fmt = Debug.debug ~channel:Spec.name fmt

  let () = register_stateless_id {
      eq = (
        let f : type a b. witness -> a id -> b id -> (a,b) eq option = fun next id1 id2 ->
          match id1, id2 with
          | Id, Id -> Some Eq
          | _      -> next.eq id1 id2
        in
        f
      );
    }

end


(** Generator of a new value identifier *)
module GenValueId(Spec:sig
    type t
    val name : string
    val display : string
  end) =
struct

  type _ id += Id : Spec.t id

  let id = I_value Id

  let name = Spec.name

  let display = Spec.display

  let debug fmt = Debug.debug ~channel:Spec.name fmt

  let () = register_value_id {
      eq = (
        let f : type a b. witness -> a id -> b id -> (a,b) eq option = fun next id1 id2 ->
          match id1, id2 with
          | Id, Id -> Some Eq
          | _      -> next.eq id1 id2
        in
        f
      );
    }
end
OCaml

Innovation. Community. Security.