package mopsa

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

Source file change.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
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
(****************************************************************************)
(*                                                                          *)
(* 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/>.    *)
(*                                                                          *)
(****************************************************************************)

(** Changes are used to log the statements executed during the computation of
    a post-state *)

open Ast.Var
open Ast.Stmt
open Ast.Expr
open Mopsa_utils
open Path

type change =
  | Change_empty
  | Change_block of stmt list
  | Change_seq   of change list
  | Change_join  of change * change
  | Change_meet  of change * change

let rec pp_change fmt = function
  | Change_empty -> ()
  | Change_block b ->
    Format.fprintf fmt "@[<hv2>{ %a }@]"
      (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt ";@ ") pp_stmt)
      b
  | Change_seq seq ->
    Format.fprintf fmt "@[<hv2>{ %a }@]"
      (Format.pp_print_list ~pp_sep:(fun fmt () -> Format.fprintf fmt "⨟@ ") pp_change)
      seq
  | Change_join (e1,e2) ->
    Format.fprintf fmt "@[<hv2>( %a ∨ @ %a )@]"
      pp_change e1
      pp_change e2
  | Change_meet (e1,e2) ->
    Format.fprintf fmt "@[<hv2>( %a ∧ @ %a )@]"
      pp_change e1
      pp_change e2

let rec compare_change e1 e2 =
  if e1 == e2 then 0
  else
    match e1,e2 with
    | Change_empty, Change_empty -> 0

    | Change_block s1, Change_block s2 ->
      Compare.list compare_stmt s1 s2

    | Change_seq s1, Change_seq s2 ->
      Compare.list compare_change s1 s2

    | Change_join (e1,e2), Change_join (f1,f2) ->
      Compare.pair compare_change compare_change (e1,e2) (f1,f2)

    | Change_meet (e1,e2), Change_meet (f1,f2) ->
      Compare.pair compare_change compare_change (e1,e2) (f1,f2)

    | _ -> compare e1 e2

let empty_change = Change_empty

let rec is_empty_change = function
  | Change_empty -> true
  | Change_block _ -> false
  | Change_seq l -> List.for_all is_empty_change l
  | Change_join(e1,e2) -> is_empty_change e1 && is_empty_change e2
  | Change_meet(e1,e2) -> is_empty_change e1 && is_empty_change e2

let join_change e1 e2 =
  if e1 == e2 then e1 else
  if is_empty_change e1 then e2 else
  if is_empty_change e2 then e1 else
    match e1,e2 with
    | Change_empty, x -> x
    | x, Change_empty -> x
    | _ -> Change_join(e1,e2)

let meet_change e1 e2 =
  if e1 == e2 then e1 else
  if is_empty_change e1 then e2 else
  if is_empty_change e2 then e1 else
    match e1,e2 with
    | Change_empty, x -> x
    | x, Change_empty -> x
    | _ -> Change_meet(e1,e2)

(** Join two changes *)
let add_stmt_to_change s = function
  | Change_empty -> Change_block [s]
  | Change_block b -> Change_block (s::b)
  | Change_seq l -> Change_seq (Change_block [s]::l)
  | e -> Change_seq [Change_block [s];e]

(** Meet two changes *)
let rec concat_change old recent =
  if is_empty_change old then recent else
  if is_empty_change recent then old
  else
    match old,recent with
    | Change_empty, Change_empty -> Change_empty
    | Change_block b1, Change_block b2 -> Change_block (b2@b1)
    | Change_seq l1, Change_seq l2 -> Change_seq (l2@l1)
    | Change_seq l, x -> Change_seq(x::l)
    | x, Change_seq l -> Change_seq(l@[x])
    | _ -> Change_seq [recent;old]

type change_map = change PathMap.t

let pp_change_map fmt map =
  if PathMap.is_empty map then
    Format.pp_print_string fmt ""
  else
    Format.fprintf fmt "@[<v>%a@]"
      (Format.pp_print_list
         ~pp_sep:(fun fmt () -> Format.fprintf fmt "@,")
         (fun fmt (path, change) -> Format.fprintf fmt "%a: %a" pp_path path pp_change change)
      ) (PathMap.bindings map)

let compare_change_map m1 m2 =
  if m1 == m2 then 0
  else PathMap.compare compare_change m1 m2 

let empty_change_map = PathMap.empty

let singleton_change_map path change = PathMap.singleton path change

let is_empty_change_map m =
  PathMap.for_all (fun _ e -> is_empty_change e) m

let concat_change_map old recent =
  PathMap.map2zo
    (fun p1 e1 -> e1)
    (fun p2 e2 -> e2)
    (fun p e1 e2 -> concat_change e1 e2)
    old recent

let join_change_map map1 map2 =
  PathMap.map2zo
    (fun p1 e1 -> e1)
    (fun p1 e2 -> e2)
    (fun p e1 e2 -> join_change e1 e2)
    map1 map2

let meet_change_map map1 map2 =
  PathMap.map2zo
    (fun p1 e1 -> e1)
    (fun p1 e2 -> e2)
    (fun p e1 e2 -> meet_change e1 e2)
    map1 map2

let get_change path map =
  match PathMap.find_opt path map with
  | None   -> Change_empty
  | Some e -> e

let add_stmt_to_change_map stmt path map =
  let change =
    match PathMap.find_opt path map with
    | None ->
      Change_block [stmt]
    | Some old ->
      add_stmt_to_change stmt old
  in
  PathMap.add path change map


(** {2 Generic merge} *)
(** ***************** *)

(** Change of a statement in terms of modified and removed variables *)
type change_vars = {
  modified: VarSet.t;
  removed: VarSet.t;
}

let compare_change_vars ve1 ve2 =
  Compare.pair VarSet.compare VarSet.compare
    (ve1.modified,ve1.removed)
    (ve2.modified,ve2.removed)

let is_empty_change_vars e =
  VarSet.is_empty e.modified &&
  VarSet.is_empty e.removed

(** Get the changes of a statement *)
let rec get_stmt_change_vars ~custom stmt : change_vars =
  match custom stmt with
  | Some ve -> ve
  | None ->
    match skind stmt with
    | S_add { ekind = E_var (var, _) } ->
      { modified = VarSet.singleton var;
        removed = VarSet.empty }

    | S_remove { ekind = E_var (var, _) } ->
      { modified = VarSet.empty ;
        removed = VarSet.singleton var; }

    | S_assign ({ ekind = E_var (var, _) },_) ->
      { modified = VarSet.singleton var;
        removed = VarSet.empty }

    | S_assume (e) ->
      { modified = VarSet.empty;
        removed = VarSet.empty }

    | S_rename ( {ekind = E_var (var1, _)}, {ekind = E_var (var2, _)} ) ->
      { modified = VarSet.singleton var2;
        removed = VarSet.singleton var1 }

    | S_expand({ekind = E_var(var,_)}, vl) ->
      { modified = VarSet.of_list (List.map (function {ekind = E_var(v,_)} -> v | _ -> assert false) vl);
        removed = VarSet.empty }

    | S_fold({ekind = E_var(var,_)}, vl) ->
      { modified = VarSet.singleton var;
        removed = VarSet.of_list (List.map (function {ekind = E_var(v,_)} -> v | _ -> assert false) vl) }

    | S_forget { ekind = E_var (var, _) } ->
      { modified = VarSet.singleton var;
        removed = VarSet.empty }

    | _ -> Exceptions.panic "generic merge: unsupported statement %a" pp_stmt stmt

let rec get_change_vars ~custom = function
  | Change_empty -> { modified = VarSet.empty; removed = VarSet.empty }
  | Change_block b ->
    (** Fold from the right because changes are stored in reverse order
       (head of the list is the last recorded change) *)
    List.fold_right
      (fun s acc ->
         let change = get_stmt_change_vars ~custom s in
         { modified = VarSet.union change.modified (VarSet.diff acc.modified change.removed);
           removed  = VarSet.union change.removed (VarSet.diff acc.removed change.modified); }
      ) b {modified = VarSet.empty; removed = VarSet.empty}
  | Change_seq l ->
    (** Fold from the right because changes are stored in reverse order
       (head of the list is the last recorded change) *)
    List.fold_right
      (fun e acc ->
         let change = get_change_vars ~custom e in
         { modified = VarSet.union change.modified (VarSet.diff acc.modified change.removed);
           removed  = VarSet.union change.removed (VarSet.diff acc.removed change.modified); }
      ) l {modified = VarSet.empty; removed = VarSet.empty}
  | Change_join(e1,e2) ->
    let ve1 = get_change_vars ~custom e1
    and ve2 = get_change_vars ~custom e2 in
    { modified = VarSet.union ve1.modified ve2.modified;
      removed = VarSet.union (VarSet.diff ve1.removed ve2.modified) (VarSet.diff ve2.removed ve1.modified); }
  | Change_meet(e1,e2) ->
    let ve1 = get_change_vars ~custom e1
    and ve2 = get_change_vars ~custom e2 in
    { modified = VarSet.union ve1.modified ve2.modified;
      removed = VarSet.union (VarSet.diff ve1.removed ve2.modified) (VarSet.diff ve2.removed ve1.modified); }

(** Apply changes on an abstract element *)
let apply_change_vars change ~add ~remove ~find (other:'a) (this:'a) : 'a =
  let a = VarSet.fold (fun v acc ->
      try add v (find v other) acc
      with _ -> Exceptions.panic "generic merge: error while adding variable %a" pp_var v
    ) change.modified this
  in
  VarSet.fold (fun v acc ->
      try remove v acc
      with _ -> Exceptions.panic "generic merge: error while removing variable %a" pp_var v
    ) change.removed a
  

(** Generic merge operator for non-relational domains *)
let generic_merge ~add ~find ~remove ?(custom=(fun stmt -> None)) (a1, e1) (a2, e2) =
  if e1 == e2 then a1,a1 else
  let ve1 = get_change_vars ~custom e1 in
  let ve2 = get_change_vars ~custom e2 in
  if compare_change_vars ve1 ve2 = 0 then a1,a2
  else
    let a2' = apply_change_vars ve1 a1 a2 ~add ~remove ~find in
    let a1' = apply_change_vars ve2 a2 a1 ~add ~remove ~find in
    a1',a2'

let opt_change_tracker_enabled = ref false
let enable_change_tracker () = opt_change_tracker_enabled := true
let disable_change_tracker () = opt_change_tracker_enabled := false
let is_change_tracker_enabled () = !opt_change_tracker_enabled
let set_change_tracker_state b = opt_change_tracker_enabled := b

let with_change_tracker f =
  let old = is_change_tracker_enabled () in
  enable_change_tracker ();
  let ret = f () in
  set_change_tracker_state old;
  ret
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