package mopsa

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

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

(** Interval abstraction of float values. *)

open Mopsa
open Sig.Abstraction.Simplified_value
open Ast
open Bot
open Common

module I = ItvUtils.FloatItvNan
module FI = ItvUtils.FloatItv
module II = ItvUtils.IntItv


let prec_of_type = function
  | T_float p -> p
  | _ -> assert false

       
(* We first use the simplified signature to handle float operations *)
module SimplifiedValue =
struct

  (** Types *)

  type t = I.t

  include GenValueId(
    struct
      type nonrec t = t
      let name = "universal.numeric.values.intervals.float"
      let display = "float-itv"
    end
    )


  let () =
    import_shared_option rounding_option_name name

  let accept_type = function
    | T_float _ -> true
    | _ -> false

  (** Lattice operations *)

  let bottom = I.bot

  let top_of_prec = function
    | F_SINGLE -> I.single_special
    | F_DOUBLE -> I.double_special
    | F_LONG_DOUBLE -> I.extra
    | F_FLOAT128 -> I.extra
    | F_REAL -> I.real

  (* Relative precision of float types.
     If prec_level t1 >= prec_level t2, then t1 can represent all values
     that t2 can, and there is no rounding error.
   *)
  let prec_level = function
    | F_SINGLE -> 1
    | F_DOUBLE -> 2
    | F_LONG_DOUBLE -> 3
    | F_FLOAT128 -> 4
    | F_REAL -> 5

  let top = top_of_prec F_LONG_DOUBLE

  let is_bottom = I.is_bot

  let subset (a1:t) (a2:t) : bool = I.included a1 a2

  let join (a1:t) (a2:t) : t = I.join a1 a2

  let meet (a1:t) (a2:t) : t = I.meet a1 a2

  let widen ctx (a1:t) (a2:t) : t = I.widen a1 a2

  let print printer (a:t) = unformat (I.fprint I.dfl_fmt) printer a

  let filter_class itv c =
    { I.itv = if c.float_valid then itv.I.itv else BOT;
      I.pinf = c.float_inf && itv.I.pinf;
      I.minf = c.float_inf && itv.I.minf;
      I.nan = c.float_nan && itv.I.nan;
    }


  (** Arithmetic operators *)

  let constant c tr =
    let p = prec_of_type tr in
    match c with
    | C_float i ->
      I.of_float_prec (prec p) (round ()) i i

    | C_float_interval (lo,up) ->
      I.of_float_prec (prec p) (round ()) lo up

    | C_avalue(V_float_interval _, itv) -> (itv:t)

    | C_top (T_float p) ->
      top_of_prec p

    | _ -> top_of_prec p


  let unop op t a tr =
    let p = prec_of_type tr in
    match op with
    | O_minus -> I.neg a
    | O_plus  -> a
    | O_sqrt  -> I.sqrt (prec p) (round ()) a
    | O_cast  ->
       if prec_level p >= prec_level (prec_of_type t) then a
       else I.round (prec p) (round()) a
    | O_filter_float_class c -> filter_class a c
    | _ -> top_of_prec p


  let binop op t1 a1 t2 a2 tr =
    let p = prec_of_type tr in
    match op with
    | O_plus  -> I.add (prec p) (round ()) a1 a2
    | O_minus -> I.sub (prec p) (round ()) a1 a2
    | O_mult  -> I.mul (prec p) (round ()) a1 a2
    | O_div   -> I.div (prec p) (round ()) a1 a2
    | O_mod   -> I.fmod (prec p) (round ()) a1 a2
    | _       -> top_of_prec p

  let filter b t a =
    let p = prec_of_type t in
    if b then I.filter_nonzero (prec p) a
    else I.filter_nonzero_false (prec p) a

  let backward_unop op t a tr r =
    let p = prec_of_type tr in
    match op with
    | O_minus -> I.bwd_neg a r
    | O_plus  -> I.meet a r
    | O_sqrt  -> I.bwd_sqrt (prec p) (round ()) a r
    | O_cast  ->
       if prec_level p >= prec_level (prec_of_type t) then I.meet a r
       else I.bwd_round (prec p) (round()) a r
    | _       -> a

  let backward_binop op t1 a1 t2 a2 tr r =
    let p = prec_of_type tr in
    match op with
    | O_plus  -> I.bwd_add (prec p) (round ()) a1 a2 r
    | O_minus -> I.bwd_sub (prec p) (round ()) a1 a2 r
    | O_mult  -> I.bwd_mul (prec p) (round ()) a1 a2 r
    | O_div   -> I.bwd_div (prec p) (round ()) a1 a2 r
    | O_mod   -> I.bwd_fmod (prec p) (round ()) a1 a2 r
    | _       -> default_backward_binop op t1 a1 t2 a2 tr r


  let compare op b t1 a1 t2 a2 =
    let p = prec_of_type t1 in
    match b, op with
    | true, O_eq | false, O_ne -> I.filter_eq  (prec p) a1 a2
    | true, O_ne | false, O_eq -> I.filter_neq (prec p) a1 a2
    | true, O_lt -> I.filter_lt  (prec p) a1 a2
    | true, O_le -> I.filter_leq (prec p) a1 a2
    | true, O_gt -> I.filter_gt  (prec p) a1 a2
    | true, O_ge -> I.filter_geq (prec p) a1 a2
    | false, O_le -> I.filter_leq_false (prec p) a1 a2
    | false, O_lt -> I.filter_lt_false  (prec p) a1 a2
    | false, O_ge -> I.filter_geq_false (prec p) a1 a2
    | false, O_gt -> I.filter_gt_false  (prec p) a1 a2
    | _ -> a1,a2


  let avalue : type r. r avalue_kind -> t -> r option = fun aval a ->
    match aval with
    | V_float_interval _ -> Some a
    | V_float_maybenan _ -> Some a.nan
    | _ -> None


end


(* We lift now to the advanced signature to handle mixed operations with integers *)
open Sig.Abstraction.Value
module Value =
struct

  module V = MakeValue(SimplifiedValue)
  include SimplifiedValue
  include V

  (** Casts of integers to floats *)
  let cast_from_int man p e =
    match e.etyp with
    | T_int | T_bool ->
      (* Get the value of the intger *)
      let v = man.eval e in
      (* Convert it to an interval *)
      let int_itv = man.avalue V_int_interval v in
      (* Cast it to a float *)
      I.of_int_itv_bot (prec p) (round ()) int_itv

    | _ -> top_of_prec p

  (** Evaluation of float expressions *)
  let eval man e =
    match ekind e with
    | E_unop(O_cast,ee) when is_int_type (etyp ee) ->
       cast_from_int man (prec_of_type e.etyp) ee
    | _ -> V.eval man e

  (** Backward evaluation of class predicates *)
  let backward_float_class man c e ve (r:int_itv) =
    match r with
    (* Refine only when the truth value of the predicate is a constant *)
    | Bot.Nb (Finite lo, Finite hi) when Z.(lo = hi) ->
      let b = Z.(lo <> zero) in
      (* Get the float value *)
      let a,_ = find_vexpr e ve in
      let c = if b then c else inv_float_class c in
      (* Refine [a] depending on the class *)
      let a' = filter_class a c in
      (* Refine [e] with the new value *)
      refine_vexpr e (meet a a') ve
    | _ -> ve

  (* Backward evaluations of float expressions *)
  let backward man e ve r =
    match ekind e with
    | E_unop(O_float_class cls, ee) -> backward_float_class man cls ee ve (man.avalue V_int_interval r)
    | _ -> backward man e ve r

  (* Extended backward evaluation of casts of integers *)
  let backward_ext_cast man p e ve r =
    match e.etyp with
    | T_int | T_bool ->
      (* Get the intger value *)
      let v,_ = find_vexpr e ve in
      (* Convert to an interval *)
      let iitv = man.avalue V_int_interval v in
      begin match iitv with
        | BOT    -> None
        | Nb itv ->
          (* Refine it knowing that the result of the cast is [r] *)
          let iitv' = ItvUtils.FloatItvNan.bwd_of_int_itv (prec p) (round ()) itv r in
          (* Evaluate the new float value *)
          let v' = man.eval (mk_avalue_expr V_int_interval iitv' e.erange) in
          (* Put it in the evaluation tree *)
          refine_vexpr e (man.meet v v') ve |>
          OptionExt.return
      end
    | _ -> None

  (** Extended backward evaluation of mixed-types expressions *)
  let backward_ext man e ve r =
    match ekind e with
    | E_unop(O_cast,ee) -> backward_ext_cast man (prec_of_type e.etyp) ee ve (man.get r)
    | _ -> V.backward_ext man e ve r

end


let () =
  register_value_abstraction (module Value)
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