package mopsa

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

Source file apron_transformer.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
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
(****************************************************************************)
(*                                                                          *)
(* 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/>.    *)
(*                                                                          *)
(****************************************************************************)


(** ToolBox module for Apron interfacing *)

open Mopsa
open Common
open Ast
open Apron_manager


module ApronTransformer(ApronManager : APRONMANAGER) =
struct

  let debug fmt = Debug.debug ~channel:"universal.numeric.relational.apron_transformer" fmt

  let with_context ctx a = a, ctx

  let is_numerical_var (v: var): bool =
    match vtyp v with
    | T_bool | T_int | T_float _ -> true
    | _ -> false

  let empty_env = Apron.Environment.make [| |] [| |]

  let print_env = Apron.Environment.print
      ~first:("[")
      ~sep:(",")
      ~last:("]")

  let filter_env int_filter real_filter env =
    let int_var, real_var = Apron.Environment.vars env in
    let list_int_var_to_keep =
      Array.fold_left (fun list_int_var_to_keep int_var ->
          if int_filter int_var then
            int_var :: list_int_var_to_keep
          else list_int_var_to_keep
        ) [] int_var
    in
    let list_real_var_to_keep =
      Array.fold_left (fun list_real_var_to_keep real_var ->
          if real_filter real_var then
            real_var :: list_real_var_to_keep
          else list_real_var_to_keep
        ) [] real_var
    in
    let array_int_res = Array.of_list list_int_var_to_keep in
    let array_real_res = Array.of_list list_real_var_to_keep in
    Apron.Environment.make array_int_res array_real_res

  let fold_env f env acc =
    let int_var, real_var = Apron.Environment.vars env in
    let acc' = Array.fold_left (fun acc x -> f x acc) acc int_var in
    Array.fold_left (fun acc x -> f x acc) acc' real_var

  let exists_env f env =
    let exception Exists in
    try
      let () = fold_env (fun e () -> if f e then raise Exists) env () in
      false
    with
    | Exists -> true

  let gce a b =
    filter_env
      (fun int_var -> Apron.Environment.mem_var b int_var)
      (fun int_var -> Apron.Environment.mem_var b int_var)
      a

  let diff a b =
    filter_env
      (fun int_var -> not (Apron.Environment.mem_var b int_var))
      (fun int_var -> not (Apron.Environment.mem_var b int_var))
      a

  (** Construct a list of linear constraints from an abstract value. *)
  let to_constraints (a,bnd) =
    let earray = Apron.Abstract1.to_lincons_array ApronManager.man a in
    let ll = ref [] in
    for i = 0 to Apron.Lincons1.array_length earray -1 do
      let l = ref [] in
      let cons = Apron.Lincons1.array_get earray i in
      Apron.Lincons1.iter (fun c v ->
          l := (c, Binding.apron_to_mopsa_var v bnd) :: !l
        ) cons;
      ll := (!l, Apron.Lincons1.get_cst cons, Apron.Lincons1.get_typ cons) ::  !ll
    done;
    !ll

  (** Restrict linear constraints involving variable [v] *)
  let constraints_of_var v constraints =
    List.filter (fun (cons,_,_) ->
        List.exists (fun (c, v') ->
            (compare_var v  v' = 0)
            && not (Apron.Coeff.is_zero c)
          ) cons
      ) constraints

  (** Get the list of variables with which [v] has numeric relations. Note that
     this function performs only one search iteration and doesn't return all
     related variables. *)
  let related_vars v (a,bnd) =
    to_constraints (a,bnd) |>
    constraints_of_var v |>
    List.fold_left (fun acc (cons,_,_) ->
        List.fold_left (fun acc (c, v') ->
            if compare_var v v' <> 0 && not (Apron.Coeff.is_zero c) then
              v' :: acc
            else
              acc
          ) acc cons
      ) []

  (** Get the list of constant variables *)
  let constant_vars (a,bnd) =
    let rec iter candidate l =
      match l with
      | [] -> candidate
      | (c, v) :: tl ->
        if Apron.Coeff.is_zero c
        then iter candidate tl
        else
          match candidate with
          | Some vv -> None
          | None -> iter (Some v) tl
    in
    to_constraints (a,bnd) |>
    List.fold_left (fun acc (cons,c,t) ->
        match t with
        | Apron.Lincons1.EQ ->
          begin
            match iter None cons with
            | None -> acc
            | Some v -> v :: acc
          end
        | _ -> acc
      ) []

  (** Similar to [get_related_vars], but ensures that all related variables are returned. *)
  let all_related_vars v a =
    let rec iter acc wq =
      if VarSet.is_empty wq then acc
      else
        let v = VarSet.choose wq in
        let wq = VarSet.remove v wq in
        if VarSet.mem v acc then iter acc wq
        else
          let acc = VarSet.add v acc in
          let related = related_vars v a |> VarSet.of_list in
          let new_related = VarSet.diff related acc in
          let wq = VarSet.union wq new_related in
          iter acc wq
    in
    iter VarSet.empty (VarSet.singleton v) |>
    VarSet.elements



  exception UnsupportedExpression (* Raised when an expression is not part of the concrete semantics *)
  exception ImpreciseExpression   (* Raised when Apron doesn't have a precise transfer function for the expression *)

  let binop_to_apron = function
    | O_plus  -> Apron.Texpr1.Add
    | O_minus -> Apron.Texpr1.Sub
    | O_mult  -> Apron.Texpr1.Mul
    | O_div   -> Apron.Texpr1.Div
    | O_ediv  -> Apron.Texpr1.Div
    | O_mod   -> Apron.Texpr1.Mod
    | O_erem  -> Apron.Texpr1.Mod
    | _ -> raise ImpreciseExpression

  let typ_to_apron = function
    | T_bool -> Apron.Texpr1.Int
    | T_int -> Apron.Texpr1.Int
    | T_float F_SINGLE -> Apron.Texpr1.Single
    | T_float F_DOUBLE -> Apron.Texpr1.Double
    | T_float F_LONG_DOUBLE -> Apron.Texpr1.Extended
    | T_float F_FLOAT128 -> Apron.Texpr1.Extended
    | T_float F_REAL -> Apron.Texpr1.Real
    | t -> panic ~loc:__LOC__ "typ_to_apron: unsupported type %a" pp_typ t

  let is_env_var v (abs,bnd) =
    let env = Apron.Abstract1.env abs in
    Apron.Environment.mem_var env (Binding.mopsa_to_apron_var v bnd |> fst)

  let is_env_var_apron v abs =
    let env = Apron.Abstract1.env abs in
    Apron.Environment.mem_var env v

  let remove_tmp tmpl abs =
    let env = Apron.Abstract1.env abs in
    let vars =
      List.filter (fun v -> is_env_var_apron v abs) tmpl
    in
    let env = Apron.Environment.remove env (Array.of_list vars) in
    Apron.Abstract1.change_environment ApronManager.man abs env true


  let rec exp_to_apron isnan exp (abs,bnd) l =
    if not (is_numeric_type (etyp exp)) then raise UnsupportedExpression else
      match ekind exp with
      | E_constant (C_int_interval (ItvUtils.IntBound.Finite lo, ItvUtils.IntBound.Finite hi)) when Z.(lo = hi) ->
        Apron.Texpr1.Cst(Apron.Coeff.Scalar(Apron.Scalar.of_mpq @@ Mpq.of_string @@ Z.to_string lo)),
        abs, bnd, l

      | E_constant C_top _
      | E_constant C_int_interval _
      | E_constant C_float_interval _
      | E_unop (O_wrap _, _) ->
        raise ImpreciseExpression

      | E_constant(C_bool true) ->
        Apron.Texpr1.Cst(Apron.Coeff.Scalar(Apron.Scalar.of_int 1)),
        abs, bnd, l

      | E_constant(C_bool false) ->
        Apron.Texpr1.Cst(Apron.Coeff.Scalar(Apron.Scalar.of_int 0)),
        abs, bnd, l

      | E_constant(C_int n) ->
        Apron.Texpr1.Cst(Apron.Coeff.Scalar(Apron.Scalar.of_mpq @@ Mpq.of_string @@ Z.to_string n)),
        abs, bnd, l

      | E_constant(C_float f) ->
        Apron.Texpr1.Cst(Apron.Coeff.Scalar(Apron.Scalar.of_float f)),
        abs, bnd, l

      | E_var (x, mode) when var_mode x mode = STRONG ->
        let xx, bnd = Binding.mopsa_to_apron_var x bnd in
        Apron.Texpr1.Var(xx), abs, bnd, l

      | E_var (x, mode) when var_mode x mode = WEAK ->
        let x' = mktmp ~typ:exp.etyp () in
        let x_apr, bnd = Binding.mopsa_to_apron_var x bnd in
        let x_apr', _ = Binding.mopsa_to_apron_var x' bnd in
        let abs = Apron.Abstract1.expand ApronManager.man abs x_apr [| x_apr' |] in
        (Apron.Texpr1.Var x_apr', abs, bnd, x_apr' :: l)

      | E_binop(O_convex_join, e1, e2) ->
        (* add tmp variable *)
        let tmp = mktmp ~typ:exp.etyp () in
        let tmp_apr, _ = Binding.mopsa_to_apron_var tmp bnd in
        let env = Apron.Environment.add (Apron.Abstract1.env abs) [|tmp_apr|] [||] in
        let abs = Apron.Abstract1.change_environment ApronManager.man abs env false in

        let e1', abs, bnd, l = exp_to_apron isnan e1 (abs,bnd) l in
        let e2', abs, bnd, l = exp_to_apron isnan e2 (abs,bnd) l in
        let typ' = typ_to_apron exp.etyp in
        let round = if typ' = Apron.Texpr1.Int then Apron.Texpr1.Zero else !opt_float_rounding in

        (* case 1: e1 <= tmp <= e2 *)
        let constraints_1 = tcons_array_of_tcons_list env [
          Apron.Tcons1.make (Apron.Texpr1.binop Apron.Texpr0.Sub (Apron.Texpr1.var env tmp_apr) (Apron.Texpr1.of_expr env e1') typ' round) Apron.Lincons0.SUPEQ;
          Apron.Tcons1.make (Apron.Texpr1.binop Apron.Texpr0.Sub (Apron.Texpr1.of_expr env e2') (Apron.Texpr1.var env tmp_apr) typ' round) Apron.Lincons0.SUPEQ;
        ] in
        let abs_1 = Apron.Abstract1.meet_tcons_array ApronManager.man abs constraints_1 in

        (* case 2: e2 <= tmp <= e1 *)
        let constraints_2 = tcons_array_of_tcons_list env [
          Apron.Tcons1.make (Apron.Texpr1.binop Apron.Texpr0.Sub (Apron.Texpr1.var env tmp_apr) (Apron.Texpr1.of_expr env e2') typ' round) Apron.Lincons0.SUPEQ;
          Apron.Tcons1.make (Apron.Texpr1.binop Apron.Texpr0.Sub (Apron.Texpr1.of_expr env e1') (Apron.Texpr1.var env tmp_apr) typ' round) Apron.Lincons0.SUPEQ;
        ] in
        let abs_2 = Apron.Abstract1.meet_tcons_array ApronManager.man abs constraints_2 in

        let abs = Apron.Abstract1.join ApronManager.man abs_1 abs_2 in
        (Apron.Texpr1.Var tmp_apr, abs, bnd, tmp_apr :: l)

      | E_binop((O_ediv|O_erem) as binop, e1, e2) ->
        let binop' = binop_to_apron binop in
        let e1', abs, bnd, l = exp_to_apron isnan e1 (abs,bnd) l in
        let e2', abs, bnd, l = exp_to_apron isnan e2 (abs,bnd) l in
        let typ' = typ_to_apron exp.etyp in
        let round = if typ' = Apron.Texpr1.Int then Apron.Texpr1.Down else !opt_float_rounding in
        Apron.Texpr1.Binop(binop', e1', e2', typ', round), abs, bnd, l

      | E_binop(binop, e1, e2) ->
        let binop' = binop_to_apron binop in
        let e1', abs, bnd, l = exp_to_apron isnan e1 (abs,bnd) l in
        let e2', abs, bnd, l = exp_to_apron isnan e2 (abs,bnd) l in
        let typ' = typ_to_apron exp.etyp in
        let round = if typ' = Apron.Texpr1.Int then Apron.Texpr1.Zero else !opt_float_rounding in
        Apron.Texpr1.Binop(binop', e1', e2', typ', round), abs, bnd, l

      | E_unop (O_plus, e) ->
        exp_to_apron isnan e (abs,bnd) l

      | E_unop(O_cast, e) ->
        let e', abs, bnd, l = exp_to_apron isnan e (abs,bnd) l in
        let typ' = typ_to_apron exp.etyp in
        let round = if typ' = Apron.Texpr1.Int then Apron.Texpr1.Zero else !opt_float_rounding in
        Apron.Texpr1.Unop(Apron.Texpr1.Cast, e', typ', round), abs, bnd, l

      | E_unop(O_minus, e) ->
        let e', abs, bnd, l = exp_to_apron isnan e (abs,bnd) l in
        let typ' = typ_to_apron e.etyp in
        let round = if typ' = Apron.Texpr1.Int then Apron.Texpr1.Zero else !opt_float_rounding in
        Apron.Texpr1.Unop(Apron.Texpr1.Neg, e', typ', round), abs, bnd, l

      | E_unop(O_sqrt, e) ->
        let e', abs, bnd, l = exp_to_apron isnan e (abs,bnd) l in
        let typ' = typ_to_apron exp.etyp in
        Apron.Texpr1.Unop(Apron.Texpr1.Sqrt, e', typ', !opt_float_rounding), abs, bnd, l

      | _ ->
        raise ImpreciseExpression


  and bexp_to_apron isnan exp (abs,bnd) l =
    match ekind exp with
    | E_binop((O_gt | O_ge | O_lt | O_le | O_eq) as comp_op, e0 , e1) ->
      if (is_float_type (etyp e0) && isnan e0) || (is_float_type (etyp e1) && isnan e1) then raise ImpreciseExpression;
      let e0', abs, bnd, l = exp_to_apron isnan e0 (abs,bnd) l in
      let e1', abs, bnd, l = exp_to_apron isnan e1 (abs,bnd) l in
      let rev, apron_comp_op = match comp_op with
        | O_gt -> false, Apron.Tcons1.SUP 
        | O_ge -> false, Apron.Tcons1.SUPEQ 
        | O_lt -> true, Apron.Tcons1.SUP
        | O_le -> true, Apron.Tcons1.SUPEQ 
        | O_eq -> false, Apron.Tcons1.EQ 
        | _ -> assert false
      in
      let e0', t0, e1', t1 =
        if rev then e1', e1.etyp, e0', e0.etyp
        else e0', e0.etyp, e1', e1.etyp in
      Dnf.singleton (apron_comp_op, e0', t0, e1', t1), abs, bnd, l

    | E_binop(O_ne, e0, e1) ->
      if (is_float_type (etyp e0) && isnan e0) || (is_float_type (etyp e1) && isnan e1) then raise ImpreciseExpression;
      let e0', abs, bnd, l = exp_to_apron isnan e0 (abs,bnd) l in
      let e1', abs, bnd, l = exp_to_apron isnan e1 (abs,bnd) l in
      Dnf.mk_or
        (Dnf.singleton (Apron.Tcons1.SUP, e0', e0.etyp, e1', e1.etyp))
        (Dnf.singleton (Apron.Tcons1.SUP, e1', e1.etyp, e0', e0.etyp)),
      abs, bnd, l

    | E_binop(O_log_or, e1, e2) ->
      let e1', abs, bnd, l = bexp_to_apron isnan e1 (abs,bnd) l in
      let e2', abs, bnd, l = bexp_to_apron isnan e2 (abs,bnd) l in
      Dnf.mk_or e1' e2', abs, bnd, l

    | E_binop(O_log_and,e1, e2) ->
      let e1', abs, bnd, l = bexp_to_apron isnan e1 (abs,bnd) l in
      let e2', abs, bnd, l = bexp_to_apron isnan e2 (abs,bnd) l in
      Dnf.mk_and e1' e2', abs, bnd, l

    | E_binop(O_log_xor, e1, e2) ->
      let e1' = mk_binop ~etyp:T_bool e1 O_eq (mk_zero ~typ:T_int exp.erange) exp.erange in
      let e2' = mk_binop ~etyp:T_bool e1 O_eq (mk_zero ~typ:T_int exp.erange) exp.erange in
      let e1', abs, bnd, l = exp_to_apron isnan e1' (abs,bnd) l in
      let e2', abs, bnd, l = exp_to_apron isnan e2' (abs,bnd) l in
      Dnf.singleton (Apron.Tcons1.DISEQ, e1', T_bool, e2', T_bool), abs, bnd, l

    | E_unop(O_log_not, exp') ->
      let dnf, abs, bnd, l = bexp_to_apron isnan exp' (abs,bnd) l in
      Dnf.mk_neg (fun (op, e1, t1, e2, t2) ->
          match op with
          | Apron.Tcons1.EQ ->
            Dnf.mk_or
              (Dnf.singleton (Apron.Tcons1.SUP, e1, t1, e2, t2))
              (Dnf.singleton (Apron.Tcons1.SUP, e2, t2, e1, t1))
          | Apron.Tcons1.SUP ->
            Dnf.singleton (Apron.Tcons1.SUPEQ, e2, t2, e1, t1)
          | Apron.Tcons1.SUPEQ ->
            Dnf.singleton (Apron.Tcons1.SUP, e2, t2, e1, t1)
          | _ -> assert false
        ) dnf,
      abs, bnd, l

    | _ ->
      let e0', abs, bnd, l = exp_to_apron isnan exp (abs,bnd) l in
      let e1' = Apron.Texpr1.Cst(Apron.Coeff.s_of_int 0) in
      Dnf.mk_or
        (Dnf.singleton (Apron.Tcons1.SUP, e0', exp.etyp, e1', T_int))
        (Dnf.singleton (Apron.Tcons1.SUP, e1', T_int, e0', exp.etyp)),
      abs, bnd, l

  and tcons_array_of_tcons_list env l =
    let n = List.length l in
    let cond_array = Apron.Tcons1.array_make env n in
    let () = List.iteri (fun i c ->
        Apron.Tcons1.array_set cond_array i c;
      ) l in
    cond_array

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