package mopsa

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

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

(** Program variables. *)


open Mopsa_utils
open Typ
open Semantic

let print_uniq_with_uid = ref true

(* force value of print_uniq_with_uid in the computation performed by f *)
let force_print_uniq_with_uid (b: bool) (f : unit -> 'a) : 'a=
  let old = !print_uniq_with_uid in
  print_uniq_with_uid := b;
  let r = f () in
  print_uniq_with_uid := old;
  r


type var_kind = ..


type mode =
  | WEAK
  | STRONG

type var = {
  vname : string;
  vkind : var_kind;
  vtyp  : typ;
  vmode : mode;
  vsemantic : semantic;
}


(** Accessor functions *)
let vname v = v.vname
let vkind v = v.vkind
let vtyp  v = v.vtyp
let vmode v = v.vmode
let vsemantic v = v.vsemantic

let mkv name kind ?(mode=STRONG) ?(semantic=any_semantic) typ =
  {vname = name; vkind = kind; vtyp = typ; vmode = mode; vsemantic = semantic }


(** Internal pretty printer chain over variable kinds *)
let var_pp_chain = TypeExt.mk_print_chain (fun fmt v ->
    Format.pp_print_string fmt v.vname
  )

(** Internal compare chain over variable kinds *)
let var_compare_chain = TypeExt.mk_compare_chain (fun v1 v2 ->
    Stdlib.compare v1.vkind v2.vkind
  )

let pp_mode fmt = function
  | STRONG -> Format.fprintf fmt "STRONG"
  | WEAK   -> Format.fprintf fmt "WEAK"

let pp_var fmt v = TypeExt.print var_pp_chain fmt v

let compare_mode (m1:mode) (m2:mode) = compare m1 m2

let compare_var v1 v2 =
  if v1 == v2 then 0 else
    Compare.compose [
        (fun () -> TypeExt.compare var_compare_chain v1 v2);
        (fun () -> compare_typ v1.vtyp v2.vtyp);
        (fun () -> compare_mode v1.vmode v2.vmode);
        (fun () -> compare_semantic v1.vsemantic v2.vsemantic);
      ]

let register_var_compare f = TypeExt.register_compare f var_compare_chain

let register_var_pp f = TypeExt.register_print f var_pp_chain

let register_var info = TypeExt.register info var_compare_chain var_pp_chain


(*========================================================================*)
(**                  {2 Generation of fresh variables}                    *)
(*========================================================================*)


(** Internal counter for fresh variables *)
let vcounter = ref 0


(** Create a fresh variable. Function [f] is given a fresh and unique
    identifier. It should return a unique name and a variable kind
*)
let mkfresh (f:int -> string * var_kind) typ ?(mode=STRONG) () =
  incr vcounter;
  let name, kind = f !vcounter in
  mkv name kind ~mode typ


(** Temporary fixes for frontends *)
let start_vcounter_at (d:int) : unit =
  assert (!vcounter <= d);
  vcounter := d

let get_vcounter_val () = !vcounter



(*========================================================================*)
(**                     {2 Common kinds of variables}                     *)
(*========================================================================*)

type var_kind +=

  (** Variables identified by their unique id *)
  | V_uniq of string (** Original name *) *
              int    (** Unique ID *)

  (** Temporary variables *)
  | V_tmp of int (** Unique ID *)

  (** Attribute attached to a variable *)
  | V_var_attr of var    (** Attach variable *) *
                  string (** Attribute *)

  (** Attribute attached to a range of program location *)
  | V_range_attr of Location.range (** Attach range *) *
                    string (** Attribute *)


(** Create a fresh temporary variable *)
let mk_uniq_var orig uid ?(mode=STRONG) typ =
  let name = orig ^ ":" ^ (string_of_int uid) in
  mkv name (V_uniq (orig, uid)) ~mode typ


(** Create a fresh variable with a unique ID *)
let mk_fresh_uniq_var orig ?(mode=STRONG) typ () =
  mkfresh (fun uid ->
      let name = orig ^ ":" ^ (string_of_int uid) in
      name, (V_uniq (orig, uid))
    ) typ ~mode ()


(** Create a fresh temporary variable *)
let mktmp ?(typ=T_any) ?(mode=STRONG) () =
  mkfresh (fun uid ->
      let name = "$tmp" ^ (string_of_int uid) in
      name, V_tmp uid
    ) typ ~mode ()


(** Create a variable attribute *)
let mk_attr_var v attr ?(mode=STRONG) ?(semantic=any_semantic) typ =
  let name = v.vname ^ "." ^ attr in
  mkv name (V_var_attr (v, attr)) ~mode ~semantic typ


(** Create a program range attribute *)
let mk_range_attr_var range attr ?(mode=STRONG) ?(semantic=any_semantic) typ =
  let name = Format.asprintf "%a.%s" Location.pp_range range attr in
  mkv name (V_range_attr (range, attr)) ~mode ~semantic typ


(** Return the original name of variables with UIDs *)
let get_orig_vname v =
  match v.vkind with
  | V_uniq (orig,_) -> orig
  | _ -> v.vname

(** Change the original name of variables with UIDs *)
let set_orig_vname name v =
  let uid = match v.vkind with V_uniq (_,uid) -> uid | _ -> assert false in
  mk_uniq_var name uid v.vtyp


(** Return the weakest mode between m1 and m2 *)
let weakest_mode m1 m2 =
  match m1, m2 with
  | STRONG, STRONG -> STRONG
  | _              -> WEAK

(** Registration of the common variable kinds *)
let () =
  register_var {
    compare = (fun next v1 v2 ->
        match vkind v1, vkind v2 with
        | V_uniq (orig,uid), V_uniq (orig',uid') ->
          Stdlib.compare uid uid'

        | V_tmp (uid), V_tmp (uid') ->
          Stdlib.compare uid uid'

        | V_var_attr (v,attr), V_var_attr (v',attr') ->
          Compare.compose [
            (fun () -> compare attr attr');
            (fun () -> compare_var v v');
          ]


        | V_range_attr (r,attr), V_range_attr (r',attr') ->
          Compare.compose [
            (fun () -> compare attr attr');
            (fun () -> Location.compare_range r r');
          ]

        | _ -> next v1 v2
      );
    print = (fun next fmt v ->
        match vkind v with
        | V_uniq (orig,uid) ->
          if !print_uniq_with_uid then Format.fprintf fmt "%s:%d" orig uid
          else Format.fprintf fmt "%s" orig

        | V_var_attr (v, a) -> Format.fprintf fmt "%s(%a)" a pp_var v

        | V_tmp _ | V_range_attr _ -> Format.pp_print_string fmt v.vname

        | _ -> next fmt v
      )
  }


(*========================================================================*)
(**                         {2 Utility modules}                           *)
(*========================================================================*)

module VarSet = SetExt.Make(struct type t = var let compare = compare_var end)
module VarMap = MapExt.Make(struct type t = var let compare = compare_var 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