package mopsa

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

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

(** Common constructs for numeric abstractions. *)

open Mopsa
open Ast

module I = ItvUtils.IntItv
module C = CongUtils.IntCong


(** {2 Integer intervals} *)
(** ********************* *)

(** Integer intervals *)
type int_itv = I.t_with_bot

type _ avalue_kind += V_int_interval : int_itv avalue_kind
(** Query to evaluate the integer interval of an expression *)

type _ avalue_kind += V_int_interval_fast : int_itv avalue_kind
(** Same as [V_int_interval] but should be handled by optimized domains, such Boxes *)

let mk_int_interval_query ?(fast=true) e =
  if fast then Q_avalue (e,V_int_interval_fast)
  else Q_avalue (e,V_int_interval)

let pp_int_interval fmt itv = I.fprint_bot fmt itv

let compare_int_interval itv1 itv2 = I.compare_bot itv1 itv2

(** Creates var \in itv constraint *)
let constraints_of_itv var (itv : int_itv) range : expr =
  match itv with
  | Nb (ItvUtils.IntBound.Finite lo, ItvUtils.IntBound.Finite hi) ->
    mk_in var (mk_z lo range) (mk_z hi range) range
  | Nb (ItvUtils.IntBound.MINF, ItvUtils.IntBound.Finite hi) -> mk_le var (mk_z hi range) range
  | Nb (ItvUtils.IntBound.Finite lo, ItvUtils.IntBound.PINF) -> mk_ge var (mk_z lo range) range
  | Nb _ -> mk_true range
  | BOT -> assert false


(** {2 Integer intervals with congruence} *)
(** ************************************* *)

(** Integer step intervals *)
type int_congr_itv = int_itv * C.t_with_bot


(** Query to evaluate the integer interval of an expression *)
type _ avalue_kind += V_int_congr_interval : int_congr_itv avalue_kind

let mk_int_congr_interval_query e = Q_avalue (e,V_int_congr_interval)



(** {2 Rounding mode of floats} *)
(** *************************** *)

let opt_float_rounding = ref Apron.Texpr1.Near

let rounding_option_name = "universal.numeric.rounding"

let () =
  register_shared_option rounding_option_name {
    key = "-float-rounding-mode";
    category = "Numeric";
    spec = Symbol (
        ["near"; "zero"; "up"; "down"; "rnd"],
        (function
          | "near" -> opt_float_rounding := Apron.Texpr1.Near
          | "zero" -> opt_float_rounding := Apron.Texpr1.Zero
          | "up"   -> opt_float_rounding := Apron.Texpr1.Up
          | "down" -> opt_float_rounding := Apron.Texpr1.Down
          | "rnd"  -> opt_float_rounding := Apron.Texpr1.Rnd
          | x -> Exceptions.panic "unknown rounding mode %s" x
        )
      );
    doc = "rounding mode of floating-point computations.";
    default = "near";
  }


(** {2 Float intervals} *)
(** ******************* *)

module F = ItvUtils.FloatItvNan


(** Float intervals *)
type float_itv = F.t

type _ avalue_kind +=
  | V_float_interval : float_prec -> float_itv avalue_kind (** Query to evaluate the float interval of an expression, with infinities and NaN *)
  | V_float_maybenan : float_prec -> bool avalue_kind

let mk_float_interval_query ?(prec=F_DOUBLE) e = Q_avalue (e,V_float_interval prec)
let mk_float_maybenan_query ?(prec=F_DOUBLE) e = Q_avalue (e,V_float_maybenan prec)

let pp_float_interval fmt itv = F.fprint F.dfl_fmt fmt itv

let compare_float_interval itv1 itv2 = F.compare itv1 itv2

let prec : Ast.float_prec -> ItvUtils.FloatItvNan.prec = function
    | F_SINGLE -> `SINGLE
    | F_DOUBLE -> `DOUBLE
    | F_LONG_DOUBLE -> `EXTRA
    | F_FLOAT128 -> `EXTRA
    | F_REAL -> `REAL

let round () : ItvUtils.FloatItvNan.round =
  match !opt_float_rounding with
  | Apron.Texpr1.Near -> `NEAR
  | Apron.Texpr1.Zero -> `ZERO
  | Apron.Texpr1.Up -> `UP
  | Apron.Texpr1.Down -> `DOWN
  | Apron.Texpr1.Rnd -> `ANY



(** {2 Fast assume on numeric conditions} *)
(** ************************************* *)

(** Get the intervals of a numeric expression *)
let interval_of_num_expr e man flow : int_itv =
  match expr_to_z e with
  | Some n -> I.of_range_bot n n
  | None -> ask_and_reduce man.ask (mk_int_interval_query ~fast:true e) flow

(** Evaluate a numeric condition using intervals *)
let eval_num_cond cond man flow : bool option =
  (* Skip expressions that contain non-universal sub-expressions or statements *)
  if exists_expr (fun e -> not (is_universal_type e.etyp)) (fun s -> true) cond then
    None
  else
    (* Evaluate the interval of the condition *)
    match interval_of_num_expr cond man flow with
    | Bot.Nb itv ->
      begin match I.contains_zero itv, I.contains_nonzero itv with
        | true, false -> Some false
        | false, true -> Some true
        | _           -> None
      end
    | _ -> None


(** Optimized assume function that uses intervals to check a
    condition or falls back to classic assume *)
let assume_num cond ~fthen ~felse ?(route=toplevel) man flow =
  let r1 =
    (* Use [eval_num_cond] directly without evaluation if the expression
       contains only pure universal sub-expressions (no statement) *)
    if for_all_expr (fun e -> is_universal_type e.etyp) (fun s -> false) cond then
      match eval_num_cond cond man flow with
      | Some true  -> Some (fthen flow)
      | Some false -> Some (felse flow)
      | None       -> None
    else
      None
  in
  match r1 with
  | Some r -> r
  | None ->
    (* Evaluate the expression if it is not a pure universal expression, or when
       [eval_num_cond] failed *)
    man.eval cond flow ~translate:"Universal" >>$ fun ncond flow ->
    match eval_num_cond ncond man flow with
    | Some true  -> fthen flow
    | Some false -> felse flow
    | None       -> assume ncond ~fthen ~felse ~eval:false man flow


(** {2 Widening thresholds} *)
(** *********************** *)

open Framework.Combiners.Value.Nonrel

module K = GenContextKey
    (struct
      type 'a t = SetExt.ZSet.t
      let print pp fmt s =
        Format.fprintf fmt "widening thresholds: @[%a@]"
          (SetExt.ZSet.fprint
             SetExtSig.{
               print_empty = "∅";
               print_begin = "{";
               print_sep = ", ";
               print_end = "}";
             }
             Z.pp_print
          ) s
    end)

(** Key for accessing widening thresholds *)
let widening_thresholds_ctx_key = K.key

(** Add a constant to the widening thresholds of a variable *)
let add_widening_threshold var n ctx =
  let thresholds =
    try find_var_ctx var widening_thresholds_ctx_key ctx
    with Not_found -> SetExt.ZSet.empty
  in
  add_var_ctx var widening_thresholds_ctx_key
    (SetExt.ZSet.add n thresholds) ctx

(** Remove all widening thresholds of a variable *)
let remove_widening_thresholds var ctx =
  remove_var_ctx var widening_thresholds_ctx_key ctx


let () =
  register_avalue {
    typ = (fun (type a) next (avk:a avalue_kind) ->
        match avk with
        | V_int_interval -> T_int
        | V_int_interval_fast -> T_int
        | V_int_congr_interval -> T_int
        | V_float_interval p -> T_float p
        | _ -> next.pool_typ avk
      );
    bottom = (
      let f : type a. avalue_pool -> a avalue_kind -> a =
        fun next avk ->
          match avk with
          | V_int_interval -> (Bot.BOT:int_itv)
          | V_int_interval_fast -> (Bot.BOT:int_itv)
          | V_int_congr_interval -> (Bot.BOT,Bot.BOT)
          | V_float_interval p -> F.bot
          | _ -> next.pool_bottom avk
      in f
    );
    top = (
      let f : type a. avalue_pool -> a avalue_kind -> a =
        fun next avk ->
          match avk with
          | V_int_interval -> Bot.Nb I.minf_inf
          | V_int_interval_fast -> Bot.Nb I.minf_inf
          | V_int_congr_interval -> (Bot.Nb I.minf_inf,Bot.Nb C.minf_inf)
          | V_float_interval p ->
            begin match p with
                | F_SINGLE -> F.single_special
                | F_DOUBLE -> F.double_special
                | F_LONG_DOUBLE -> F.extra
                | F_FLOAT128 -> F.extra
                | F_REAL -> F.real
            end
          | _ -> next.pool_top avk
      in f
    );
    join = (
      let f : type a. avalue_pool -> a avalue_kind -> a -> a -> a =
        fun next avk av1 av2 ->
          match avk with
          | V_int_interval -> I.join_bot av1 av2
          | V_int_interval_fast -> I.join_bot av1 av2
          | V_int_congr_interval -> I.join_bot (fst av1) (fst av2), C.join_bot (snd av1) (snd av2)
          | V_float_interval p -> F.join av1 av2
          | _ -> next.pool_join avk av1 av2
      in f
    );
    meet = (
      let f : type a. avalue_pool -> a avalue_kind -> a -> a -> a =
        fun next avk av1 av2 ->
          match avk with
          | V_int_interval -> I.meet_bot av1 av2
          | V_int_interval_fast -> I.meet_bot av1 av2
          | V_int_congr_interval -> I.meet_bot (fst av1) (fst av2), C.meet_bot (snd av1) (snd av2)
          | V_float_interval p -> F.meet av1 av2
          | _ -> next.pool_meet avk av1 av2
      in f
    );
    print = (
      let f : type a. avalue_pool -> a avalue_kind -> Format.formatter -> a -> unit =
        fun next avk fmt av ->
          match avk with
          | V_int_interval -> I.fprint_bot fmt av
          | V_int_interval_fast -> I.fprint_bot fmt av
          | V_int_congr_interval -> Format.fprintf fmt "%a:%a" I.fprint_bot (fst av) C.fprint_bot (snd av)
          | V_float_interval p -> F.fprint F.dfl_fmt fmt av
          | _ -> next.pool_print avk fmt av
      in f
    );
    compare = (
      let f : type a b. avalue_pool -> a avalue_kind -> a -> b avalue_kind -> b -> int =
        fun next avk1 av1 avk2 av2 ->
          match avk1,avk2 with
          | V_int_interval, V_int_interval -> I.compare_bot av1 av2
          | V_int_interval_fast, V_int_interval_fast -> I.compare_bot av1 av2
          | V_int_congr_interval, V_int_congr_interval -> Compare.pair I.compare_bot C.compare_bot av1 av2
          | V_float_interval p1, V_float_interval p2 -> Compare.pair compare F.compare (p1,av1) (p2,av2)
          | _ -> next.pool_compare avk1 av1 avk2 av2
      in f
    )
  }
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