package mopsa

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

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

(** Signature of a value abstraction. *)

open Core.All


(*==========================================================================*)
(**                          {2 Value manager}                              *)
(*==========================================================================*)

type ('v,'t) value_man = {
  bottom : 'v;
  top    : 'v;
  is_bottom : 'v -> bool;
  subset : 'v -> 'v -> bool;
  join : 'v -> 'v -> 'v;
  meet : 'v -> 'v -> 'v;
  print : printer -> 'v -> unit;
  get  : 'v -> 't;
  set  : 't -> 'v -> 'v;
  eval : expr -> 'v;
  avalue : 'r. 'r avalue_kind -> 'v -> 'r;
  ask : 'a 'r. ('a,'r) query -> 'r;
}


(*==========================================================================*)
(**                        {2 Valued expressions}                           *)
(*==========================================================================*)

type 'v vexpr =
  | Map of ('v * 'v vexpr) ExprMap.t

let empty_vexpr = Map ExprMap.empty

let singleton_vexpr e v ve =
  Map (ExprMap.singleton e (v,ve))

let root_vexpr = function
  | Map map -> Map (ExprMap.map (fun (v,ve) -> (v,empty_vexpr)) map)

let add_vexpr e v ve = function
  | Map map -> Map (ExprMap.add e (v,ve) map)

let refine_vexpr e v = function
  | Map map ->
    let r =
      match ExprMap.find_opt e map with
      | Some (_,ve) -> (v,ve)
      | None -> (v,empty_vexpr)
    in
    Map (ExprMap.add e r map)

let rec find_vexpr e = function
  | Map map ->
    try ExprMap.find e map
    with Not_found ->
      let rec iter = function
        | [] -> raise Not_found
        | (_,(_,vee))::tl ->
          try find_vexpr e vee
          with Not_found -> iter tl
      in
      iter (ExprMap.bindings map)

let find_vexpr_opt e ve =
  try Some (find_vexpr e ve)
  with Not_found -> None

let rec map_vexpr f = function
  | Map map ->
    let map' =
      ExprMap.map
        (fun (v,ve) -> (f v,map_vexpr f ve))
        map
    in
    Map map'

let fold_root_vexpr f init = function
  | Map map ->
    ExprMap.fold
      (fun e (v,ve) acc -> f acc e v ve)
      map init

let rec fold_vexpr f init = function
  | Map map ->
    ExprMap.fold
      (fun e (v,ve) acc -> fold_vexpr f (f acc e v ve) ve)
      map init

let rec map2_vexpr f1 f2 f ve1 ve2 =
  match ve1,ve2 with
  | Map m1, Map m2 ->
    let m =
      ExprMap.map2o
        (fun e (v1,ve1) -> f1 v1, map_vexpr f1 ve1)
        (fun e (v2,ve2) -> f2 v2, map_vexpr f2 ve2)
        (fun e (v1,ve1) (v2,ve2) ->
           (f v1 v2, map2_vexpr f1 f2 f ve1 ve2)
        )
        m1 m2 in
    Map m

let rec merge_vexpr vmerge ve1 ve2 =
  match ve1,ve2 with
  | Map m1, Map m2 ->
    let m =
      ExprMap.map2zo
        (fun e ve1 -> ve1)
        (fun e ve2 -> ve2)
        (fun e (v1,ve1) (v2,ve2) ->
           (vmerge v1 v2, merge_vexpr vmerge ve1 ve2)
        )
        m1 m2 in
    Map m

(*==========================================================================*)
(**                          {2 Value domain}                               *)
(*==========================================================================*)


module type VALUE =
sig
  type t
  val id : t id
  val accept_type : typ -> bool
  val name : string
  val display : string
  val bottom: t
  val top: t
  val is_bottom: t -> bool
  val subset: t -> t -> bool
  val join: t -> t -> t
  val meet: t -> t -> t
  val widen: 'a ctx -> t -> t -> t
  val eval : ('v,t) value_man -> expr -> t
  val avalue : 'r avalue_kind -> t -> 'r option
  val backward : ('v,t) value_man -> expr -> t vexpr -> 'v -> t vexpr
  val filter : bool -> typ -> t -> t
  val compare : ('v,t) value_man -> operator -> bool -> expr -> t -> expr -> t -> (t * t)
  val eval_ext : ('v,t) value_man -> expr -> 'v option
  val backward_ext : ('v,t) value_man -> expr -> 'v vexpr -> 'v -> 'v vexpr option
  val compare_ext : ('v,t) value_man -> operator -> bool -> expr -> 'v -> expr -> 'v -> ('v * 'v) option
  val ask : ('v,t) value_man -> ('a,'r) query -> 'r option
  val print: printer -> t -> unit
end

let default_filter b t v = v
let default_backward man e ve v = ve
let default_compare man op b e1 v1 e2 v2 = (v1,v2)

module DefaultValueFunctions =
struct
  let filter = default_filter
  let backward= default_backward
  let compare = default_compare
  let eval_ext man e = None
  let backward_ext man e ve v = None
  let compare_ext man op b e1 v1 e2 v2 = None
  let avalue avk v = None
  let ask man q = None
end


(*==========================================================================*)
(**                          {2 Registration}                               *)
(*==========================================================================*)

let values : (module VALUE) list ref = ref []

let register_value_abstraction dom =
  values := dom :: !values

let find_value_abstraction name =
  List.find (fun dom ->
      let module D = (val dom : VALUE) in
      compare D.name name = 0
    ) !values

let mem_value_abstraction name =
  List.exists (fun dom ->
      let module D = (val dom : VALUE) in
      compare D.name name = 0
    ) !values

let value_abstraction_names () =
  List.map (fun dom ->
      let module D = (val dom : VALUE) in
      D.name
    ) !values
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