[Eva - Numerors] Propagate module name and split the main file

src/plugins/value/values/numerors/numerors_float.ml

+open Numerors_utils
+
+
+(*-----------------------------------------------------------------------------
+ *      Float representation. The MPFR numbers are always positives.
+ *---------------------------------------------------------------------------*)
+type t  = Sign.t * num
+and num = Nan | Inf | Float of Mpfrf.t
+
+
+(*-----------------------------------------------------------------------------
+ *                           Pretty printer
+ *---------------------------------------------------------------------------*)
+let pretty fmt (s, n) =
+  let pp_num fmt = function
+    | Nan     -> Format.fprintf fmt "Nan"
+    | Inf     -> Format.fprintf fmt "Inf"
+    | Float f -> Format.fprintf fmt "%a" Mpfrf.print f
+  in Format.fprintf fmt "%a%a" Sign.pretty s pp_num n
+
+
+(*-----------------------------------------------------------------------------
+ *                          Internal functions
+ *---------------------------------------------------------------------------*)
+(* Set asked precision and call the function *)
+let set_precision p f = Mpfr.set_default_prec (Precisions.get p) ; f
+
+(* Rebuild the correct MPFR with the sign *)
+let rebuild ?rnd s n =
+  let r = match rnd with Some r -> r | None -> Mpfr.Near in
+  match s with Sign.Positive -> n | Sign.Negative -> Mpfrf.neg n r
+
+
+(*-----------------------------------------------------------------------------
+ *                Methods to get informations on floats
+ *---------------------------------------------------------------------------*)
+let sign_of (s, _) = s
+let precision_of (_, n) =
+  match n with
+  | Nan | Inf -> None
+  | Float f -> Precisions.of_int (Mpfr.get_prec (Mpfrf.to_mpfr f))
+
+
+(*-----------------------------------------------------------------------------
+ *                              Constructors
+ *---------------------------------------------------------------------------*)
+let nan = Sign.Positive, Nan
+let mpfr_zero p = set_precision p Mpfrf.of_float 0.0 Mpfr.Zero 
+let pos_zero p  = Sign.Positive, Float (mpfr_zero p)
+let neg_zero p  = Sign.Negative, Float (mpfr_zero p)
+let pos_inf     = Sign.Positive, Inf
+let neg_inf     = Sign.Negative, Inf
+
+let of_mpfr f =
+  let s = Sign.of_mpfr f in
+  let n =
+    if Mpfrf.inf_p f then Inf
+    else if Mpfrf.nan_p f then Nan
+    else Float (Mpfrf.abs f Mpfr.Near)
+  in s, n  
+
+let of_int    ?(rnd = Mpfr.Near) p i =
+  of_mpfr (set_precision p Mpfrf.of_int    i rnd)
+
+let of_float  ?(rnd = Mpfr.Near) p f =
+  of_mpfr (set_precision p Mpfrf.of_float  f rnd)
+
+let of_string ?(rnd = Mpfr.Near) p s =
+  let s = List.hd (String.split_on_char 'f' s) in
+  of_mpfr (set_precision p Mpfrf.of_string s rnd)
+
+
+(*-----------------------------------------------------------------------------
+ *                        Comparison methods
+ *---------------------------------------------------------------------------*)
+let compare (sx, nx) (sy, ny) =
+  match nx, ny with
+  | Nan, Nan -> 0 | Nan, _ -> 1 | _, Nan -> -1
+  | Inf, _ -> if Sign.eq sx Sign.Negative then -1 else 1
+  | _, Inf -> if Sign.eq sy Sign.Positive then -1 else 1
+  | Float fx, Float fy -> Mpfrf.cmp (rebuild sx fx) (rebuild sy fy)
+let eq a b = compare a b =  0
+let le a b = compare a b <= 0
+let lt a b = compare a b <  0
+let ge a b = compare a b >= 0
+let gt a b = compare a b >  0
+
+
+(*-----------------------------------------------------------------------------
+ *                Methods to check properties on floats
+ *---------------------------------------------------------------------------*)
+let is_nan (_, n) = match n with Nan -> true | _ -> false
+let is_inf (_, n) = match n with Inf -> true | _ -> false
+let is_pos (s, _) = Sign.eq s Sign.Positive
+let is_neg (s, _) = Sign.eq s Sign.Negative
+let is_a_zero f =
+  match precision_of f with
+  | Some p -> eq f (pos_zero p)
+  | None -> false
+let is_pos_zero f = is_pos f && is_a_zero f
+let is_neg_zero f = is_neg f && is_a_zero f
+let is_strictly_pos f = is_pos f && not (is_a_zero f)
+let is_strictly_neg f = is_neg f && not (is_a_zero f)
+
+
+(*-----------------------------------------------------------------------------
+ *                Cast a float to the asked precision
+ *---------------------------------------------------------------------------*)
+let cast ?(rnd = Mpfr.Near) ~prec (s, n) =
+  match n with
+  | Float x ->
+    let x' = Mpfrf.to_mpfr x in
+    let r = Mpfr.init () in
+    let old = Mpfr.get_default_rounding_mode () in
+    Mpfr.set_default_rounding_mode rnd ;
+    Mpfr.set_prec r (Precisions.get prec) ;
+    let _ = Mpfr.set r x' Mpfr.Near in
+    Mpfr.set_default_rounding_mode old ;
+    s, Float (Mpfrf.of_mpfr r)
+  | _ -> (s, n)
+
+
+(*-----------------------------------------------------------------------------
+ *          Return the second argument with the sign of the first
+ *---------------------------------------------------------------------------*)
+let apply_sign (s, _) (_, n) = (s, n)
+
+(*-----------------------------------------------------------------------------
+ *                            Arithmetics
+ *-----------------------------------------------------------------------------
+ *  The IEEE-754 norm does not specify the propagation of the sign bit with
+ *  Nan operands. For the addition and the substraction, we set it to Positive.
+ *  For the multiplication and the division, we set it to the exclusive or
+ *  between the signs of the operands.
+ *---------------------------------------------------------------------------*)
+let normal_op rnd p op (sa, fa) (sb, fb) =
+  let x, y = rebuild sa fa, rebuild sb fb in
+  of_mpfr (set_precision p op x y rnd)
+
+let add ?(rnd = Mpfr.Near) ~prec (sa, na) (sb, nb) =
+  match na, nb with
+  | Nan, _ | _, Nan -> Sign.Positive, Nan
+  | Inf, Inf when Sign.eq sa sb -> sa, Inf
+  | Inf, Inf -> Sign.Positive, Nan
+  | Inf, Float _ -> sa, Inf
+  | Float _, Inf -> sb, Inf
+  | Float fa, Float fb -> normal_op rnd prec Mpfrf.add (sa, fa) (sb, fb)
+
+let sub ?(rnd = Mpfr.Near) ~prec (sa, na) (sb, nb) =
+  match na, nb with
+  | Nan, _ | _, Nan -> Sign.Positive, Nan
+  | Inf, Inf when not (Sign.eq sa sb) -> sa, Inf
+  | Inf, Inf -> Sign.Positive, Nan
+  | Inf, Float _ -> sa, Inf
+  | Float _, Inf -> Sign.neg sb, Inf
+  | Float fa, Float fb -> normal_op rnd prec Mpfrf.sub (sa, fa) (sb, fb)
+
+let mul ?(rnd = Mpfr.Near) ~prec (sa, na) (sb, nb) =
+  match na, nb with
+  | Nan, _ | _, Nan -> Sign.mul sa sb, Nan
+  | Inf, _ | _, Inf -> Sign.mul sa sb, Inf
+  | Float fa, Float fb -> normal_op rnd prec Mpfrf.mul (sa, fa) (sb, fb)
+
+let div ?(rnd = Mpfr.Near) ~prec (sa, na) (sb, nb) =
+  match na, nb with
+  | Nan, _ | _, Nan -> Sign.mul sa sb, Nan
+  | Inf, Inf -> Sign.mul sa sb, Nan
+  | Inf, Float _ -> Sign.mul sa sb, Inf
+  | Float _, Inf -> Sign.mul sa sb, Float (mpfr_zero prec)
+  | Float fa, Float fb -> normal_op rnd prec Mpfrf.div (sa, fa) (sb, fb)
+
+let neg (sa, na) = Sign.neg sa  , na
+let abs (_ , na) = Sign.Positive, na
+
+let sqrt ?(rnd = Mpfr.Near) ~prec (sa, na) =
+  match na with
+  | Inf when Sign.eq sa Sign.Positive -> sa, Inf
+  | Float x when Sign.eq sa Sign.Positive ->
+    of_mpfr (set_precision prec Mpfrf.sqrt x rnd)
+  | _ -> sa, Nan
+
+(* Min and Max *)
+let min x y = if compare x y <= 0 then x else y
+let max x y = if compare x y <= 0 then y else x

src/plugins/value/values/numerors/numerors_float.mli

+open Numerors_utils
+
+type t
+
+val pretty : Format.formatter -> t -> unit
+
+val sign_of : t -> Sign.t
+val precision_of : t -> Precisions.t option
+
+val nan : t
+val pos_inf : t
+val neg_inf : t
+val pos_zero : Precisions.t -> t
+val neg_zero : Precisions.t -> t
+
+val of_mpfr : Mpfrf.t -> t
+val of_int : ?rnd:Mpfr.round -> Precisions.t -> int -> t
+val of_float : ?rnd:Mpfr.round -> Precisions.t -> float -> t
+val of_string : ?rnd:Mpfr.round -> Precisions.t -> string -> t
+
+val compare : t -> t -> int
+val eq : t -> t -> bool
+val le : t -> t -> bool
+val lt : t -> t -> bool
+val ge : t -> t -> bool
+val gt : t -> t -> bool
+
+val is_nan : t -> bool
+val is_inf : t -> bool
+val is_pos : t -> bool
+val is_neg : t -> bool
+val is_a_zero : t -> bool
+val is_pos_zero : t -> bool
+val is_neg_zero : t -> bool
+val is_strictly_pos : t -> bool
+val is_strictly_neg : t -> bool
+
+val cast : ?rnd:Mpfr.round -> prec:Precisions.t -> t -> t
+
+val apply_sign : t -> t -> t
+
+val add : ?rnd:Mpfr.round -> prec:Precisions.t -> t -> t -> t
+val sub : ?rnd:Mpfr.round -> prec:Precisions.t -> t -> t -> t
+val mul : ?rnd:Mpfr.round -> prec:Precisions.t -> t -> t -> t
+val div : ?rnd:Mpfr.round -> prec:Precisions.t -> t -> t -> t
+
+val neg : t -> t
+val abs : t -> t
+
+val sqrt : ?rnd:Mpfr.round -> prec:Precisions.t -> t -> t
+
+val min : t -> t -> t
+val max : t -> t -> t

src/plugins/value/values/numerors/numerors_utils.ml

+open Cil_types
+
+(*-----------------------------------------------------------------------------
+ *     Module describing the different precisions that will be manipulated
+ *---------------------------------------------------------------------------*)
+module Precisions = struct
+
+  type t = Simple | Double | Long_Double | Real
+
+  let rp : int = Value_parameters.RealSignificandBits.get ()
+
+  let pretty fmt = function
+    | Simple -> Format.fprintf fmt "Simple"
+    | Double -> Format.fprintf fmt "Double"
+    | Long_Double -> Format.fprintf fmt "Long Double"
+    | Real -> Format.fprintf fmt "Real"
+
+  let of_fkind = function
+    | FFloat      -> Simple
+    | FDouble     -> Double
+    | FLongDouble -> Long_Double
+
+  let get = function
+    | Simple      -> 23 | Double      -> 52
+    | Long_Double -> 64 | Real        -> rp
+
+  let of_int i =
+    if i = get Simple then Some Simple
+    else if i = get Double then Some Double
+    else if i = get Long_Double then Some Long_Double
+    else if i = get Real then Some Real
+    else None
+
+  let compare a b = Pervasives.compare (get a) (get b)
+  let eq a b = compare a b =  0
+  let le a b = compare a b <= 0
+  let lt a b = compare a b <  0
+  let ge a b = compare a b >= 0
+  let gt a b = compare a b >  0
+
+  let max a b = if compare a b <= 0 then b else a
+  let min a b = if compare a b <= 0 then a else b
+
+end
+
+
+(*-----------------------------------------------------------------------------
+ *                         Sign type for infinites
+ *---------------------------------------------------------------------------*)
+module Sign = struct
+
+  type t = Positive | Negative
+
+  let pretty fmt = function
+    | Positive -> Format.fprintf fmt "+"
+    | Negative -> Format.fprintf fmt "-"
+
+  let of_int i = if i < 0 then Negative else Positive
+  let of_mpfr f = of_int (Mpfrf.sgn f)
+
+  let compare a b =
+    match a, b with
+    | Positive, Positive | Negative, Negative -> 0
+    | Positive, Negative ->  1
+    | Negative, Positive -> -1
+  let eq a b = compare a b = 0
+  let le a b = compare a b <= 0
+  let lt a b = compare a b <  0
+  let ge a b = compare a b >= 0
+  let gt a b = compare a b >  0
+
+  let neg s = if s = Positive then Negative else Positive
+  let mul a b = if eq a b then Positive else Negative
+
+end
+
+

src/plugins/value/values/numerors/numerors_utils.mli

+module Precisions : sig
+
+  type t = Simple | Double | Long_Double | Real
+
+  val pretty : Format.formatter -> t -> unit
+  
+  val of_fkind : Cil_types.fkind -> t
+  val of_int : int -> t option
+  val get : t -> int
+
+  val compare : t -> t -> int
+  val eq : t -> t -> bool
+  val le : t -> t -> bool
+  val lt : t -> t -> bool
+  val ge : t -> t -> bool
+  val gt : t -> t -> bool
+
+  val max : t -> t -> t
+  val min : t -> t -> t
+
+end
+
+
+module Sign : sig
+  
+  type t = Positive | Negative
+  
+  val pretty : Format.formatter -> t -> unit
+
+  val of_int : int -> t
+  val of_mpfr : Mpfrf.t -> t
+
+  val compare : t -> t -> int
+  val eq : t -> t -> bool
+  val le : t -> t -> bool
+  val lt : t -> t -> bool
+  val ge : t -> t -> bool
+  val gt : t -> t -> bool
+
+  val neg : t -> t
+  val mul : t -> t -> t  
+
+end