package mopsa

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

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

(** Union of two value abstractions *)

open Core.All
open Sig.Abstraction.Value
open Common
open Mopsa_utils


module Make(V1:VALUE)(V2:VALUE) : VALUE with type t = V1.t * V2.t =
struct

  (** {2 Header of the abstraction} *)
  (** ***************************** *)

  include Lattices.Pair.Make(V1)(V2)

  let name = "framework.combiners.value.union"

  let id = V_pair(V1.id,V2.id)

  let display = V1.display ^ " ∪ " ^ V2.display

  let accept_type t = V1.accept_type t || V2.accept_type t

  let print printer (v1,v2) =
    match V1.is_bottom v1, V2.is_bottom v2 with
    | true, true -> pp_string printer Bot.bot_string
    | false, true -> V1.print printer v1
    | true, false -> V2.print printer v2
    | false, false ->
      pp_obj_list printer
        [ pbox V1.print v1;
          pbox V2.print v2 ]
        ~lopen:"" ~lsep:"∨" ~lclose:""


  (** {2 Lattice operators} *)
  (** ********************* *)

  let is_bottom (v1,v2) = V1.is_bottom v1 && V2.is_bottom v2


  (** {2 Value managers} *)
  (** ****************** *)

  let v1_man (man:('v,t) value_man) : ('v,V1.t) value_man = {
    man with
    get  = (fun a -> man.get a |> fst);
    set  = (fun x a ->
        let (v1,v2) = man.get a in
        if x == v1 then a else man.set (x,v2) a);
  }

  let v2_man (man:('v,t) value_man) : ('v,V2.t) value_man = {
    man with
    get  = (fun a -> man.get a |> snd);
    set  = (fun x a ->
        let (v1,v2) = man.get a in
        if x == v2 then a else man.set (v1,x) a);
  }


  (** {2 Local semantics} *)
  (** ******************* *)


  (** Forward evaluation of expressions handled by [V1] or [V2] *)
  let eval man e : t =
    let man1 = v1_man man in
    let man2 = v2_man man in
    let accept1 = V1.accept_type e.etyp in
    let accept2 = V2.accept_type e.etyp in
    if accept1 && accept2 then
      (* Both domains can represent the value of the expression [e].
         In this case, we just pair the returned values *)
      let r1 = V1.eval man1 e in
      let r2 = V2.eval man2 e in
      (r1, r2)
    else
    if accept1 then
      (* Only [V1] can represent the value of [e]. However, [V2] can handle the
         expression in its extended semantics. So we need to combine the results
         of [V1.eval] and [V2.eval_ext]. *)
      let r1 = V1.eval man1 e in
      let r2 = V2.eval_ext man2 e in
      match r2 with
      | None   ->
        (* Since [V2] can't represent the value of [e], its value is set to ⊥ *)
        (r1,V2.bottom)
      | Some v ->
        (* When [V2.eval_ext] returns a value [v], we need to retrieve the part
           of [V1] in [v] in order to refine it with the result of [V1.eval] *)
        (V1.meet r1 (man1.get v), V2.bottom)
    else
    if accept2 then
      (* Dual case of accept1 *)
      let r1 = V1.eval_ext man1 e in
      let r2 = V2.eval man2 e in
      match r1 with
      | None   -> (V1.bottom,r2)
      | Some v -> (V1.bottom,V2.meet r2 (man2.get v))
    else
      assert false

  (** Filter of truth values *)
  let filter b t v =
    let doit f accept v bot =
      if accept t then f b t v
      else bot
    in
    let r1 = doit V1.filter V1.accept_type (fst v) V1.bottom in
    let r2 = doit V2.filter V2.accept_type (snd v) V2.bottom in
    (r1,r2)

  (** Backward evaluation of expressions *)
  let backward man e ve r : t vexpr =
    let man1 = v1_man man in
    let man2 = v2_man man in
    (** Sine we are refining the values of sub-expressions, we consider that a
       domain accepts a backward evaluation iff all sub-expressions are accepted
       *)
    let accept1 = for_all_child_expr (fun ee -> V1.accept_type ee.etyp) (fun s -> false) e in
    let accept2 = for_all_child_expr (fun ee -> V2.accept_type ee.etyp) (fun s -> false) e in
    if accept1 && accept2 then
      (* Both domains accept, so call [backward] on both of them *)
      let r1 = V1.backward man1 e (map_vexpr fst ve) r in
      let r2 = V2.backward man2 e (map_vexpr snd ve) r in
      (* Combine the values of each node in the tree *)
      map2_vexpr
        (fun v1 -> assert false)
        (fun v2 -> assert false)
        (fun v1 v2 -> (v1, v2))
        r1 r2
    else
    if accept1 then
      (* Similarly to [eval], when only one domain accepts the expression, we
         need to call the dual extended function of the other domain *)
      let r1 = V1.backward man1 e (map_vexpr fst ve) r in
      let r2 = V2.backward_ext man2 e (map_vexpr (fun v -> man.set v man.top) ve) r in
      match r2 with
      | None   ->
        (* Always put the refusing domain to ⊥ *)
        map_vexpr (fun v1 -> (v1,V2.bottom)) r1
      | Some rr2 ->
        (* Use the returned value to refine the result of [V1.backward] *)
        map2_vexpr
          (fun v1 -> assert false)
          (fun v2 -> assert false)
          (fun v1 v2 -> (V1.meet v1 (man1.get v2), V2.bottom))
          r1 rr2
    else
    if accept2 then
      let r1 = V1.backward_ext man1 e (map_vexpr (fun v -> man.set v man.top) ve) r in
      let r2 = V2.backward man2 e (map_vexpr snd ve) r in
      match r1 with
      | None   ->
        map_vexpr (fun v2 -> (V1.bottom,v2)) r2
      | Some rr1 ->
        map2_vexpr
          (fun v1 -> assert false)
          (fun v2 -> assert false)
          (fun v1 v2 -> (V1.bottom,V2.meet v2 (man2.get v1)))
          rr1 r2
    else
      failwith (Format.asprintf "not accepting type %a %b %b" pp_typ e.etyp accept1 accept2)
      (* assert false *)

  (** Backward refinement of values in a comparison *)
  let compare man op b e1 v1 e2 v2 : t * t =
    let man1 = v1_man man in
    let man2 = v2_man man in
    (* A domain needs to accepts both expressions *)
    let accept1 = V1.accept_type e1.etyp && V1.accept_type e2.etyp in
    let accept2 = V2.accept_type e1.etyp && V2.accept_type e2.etyp in
    if accept1 && accept2 then
      let (r11,r12) = V1.compare man1 op b e1 (fst v1) e2 (fst v2) in
      let (r21,r22) = V2.compare man2 op b e1 (snd v1) e2 (snd v2) in
      (r11,r21), (r12,r22)
    else
    if accept1 then
      (* Similar reasoning as [eval] and [backward] *)
      let (r11,r12) = V1.compare man1 op b e1 (fst v1) e2 (fst v2) in
      let r2 = V2.compare_ext man2 op b e1 (man.set v1 man.top) e2 (man.set v2 man.top) in
      match r2 with
      | None   -> (r11,V2.bottom), (r12,V2.bottom)
      | Some (r21,r22) ->
        (V1.meet r11 (man1.get r21), man2.get r21),
        (V1.meet r12 (man1.get r22), man2.get r22)
    else
    if accept2 then
      let r1 = V1.compare_ext man1 op b e1 (man.set v1 man.top) e2 (man.set v2 man.top) in
      let (r21,r22) = V2.compare man2 op b e1 (snd v1) e2 (snd v2) in
      match r1 with
      | None   -> (V1.bottom,r21), (V1.bottom,r22)
      | Some (r11,r12) ->
        (man1.get r11, V2.meet r21 (man2.get r11)),
        (man1.get r12, V2.meet r22 (man2.get r12))
    else
      assert false


  (** {2 Extended semantics} *)
  (** ********************** *)

  (** Extened evaluation of expressions, used when the expression can't be
      repsented in neither [V1] not [V2] *)
  let eval_ext man e =
    let r1 = V1.eval_ext (v1_man man) e in
    let r2 = V2.eval_ext (v2_man man) e in
    OptionExt.neutral2 man.meet r1 r2

  (** Extended backward evaluations, used when some sub-expressions can't be
     represented by [V1] not [V2] *)
  let backward_ext man e ev r =
    let r1 = V1.backward_ext (v1_man man) e ev r in
    let r2 = V2.backward_ext (v2_man man) e ev r in
    OptionExt.neutral2 (merge_vexpr man.meet) r1 r2

  (** Extended comparison between expressions outside the scope of [V1] and [V2] *)
  let compare_ext man op b e1 v1 e2 v2 =
    let r1 = V1.compare_ext (v1_man man) op b e1 v1 e2 v2 in
    let r2 = V2.compare_ext (v2_man man) op b e1 v1 e2 v2 in
    OptionExt.neutral2 (fun (r11,r12) (r21,r22) -> (man.meet r11 r21),(man.meet r12 r22)) r1 r2

  (** {2 Communication handlers} *)
  (** ************************** *)

  (** Cast an abstract element to an avalue *)
  let avalue aval (v1,v2) =
    OptionExt.neutral2
      (join_avalue aval)
      (V1.avalue aval v1)
      (V2.avalue aval v2)

  (** Handle queries *)
  let ask man query =
    OptionExt.neutral2
      (join_query query)
      (V1.ask (v1_man man) query)
      (V2.ask (v2_man man) query)
end

(** Create a union of a list of domains *)
let rec make (values:(module VALUE) list) : (module VALUE) =
  match values with
  | [] -> assert false
  | [v] -> v
  | hd::tl -> (module Make(val hd : VALUE)(val (make tl) : VALUE) : VALUE)
OCaml

Innovation. Community. Security.