diff --git a/Makefile b/Makefile
index 7250c1a8197d9b17fe19358d5ff850fc23ee1c37..233831ab22d1783d9e4ca97a4b44d18ecb59ef55 100644
--- a/Makefile
+++ b/Makefile
@@ -825,7 +825,7 @@ PLUGIN_GENERATED := src/plugins/value/domains/apron/apron_domain.ml
PLUGIN_DISTRIB_EXTERNAL:=domains/apron/apron_domain.ok.ml domains/apron/apron_domain.ko.ml
ifeq ($(HAS_MPFR),yes)
-PLUGIN_REQUIRES:= mlmpfr
+PLUGIN_REQUIRES:= gmp
src/plugins/value/values/errors_value.ml: \
src/plugins/value/values/errors_value.ok.ml share/Makefile.config
$(CP_IF_DIFF) $< $@
diff --git a/Makefile.generating b/Makefile.generating
index 7265432b405fc56ead4219c351b1b13da8bc371d..af873d23e5c06045ea8729337a525ebfcf31700a 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -195,6 +195,7 @@ endif
for PKG in $(LIBRARY_NAMES); do echo PKG $$PKG >> .merlin; done
for PKG in $(LIBRARY_NAMES_GUI); do echo PKG $$PKG >> .merlin; done
for PKG in $(MERLIN_PACKAGES); do echo PKG $$PKG >> .merlin; done
+ echo "PKG gmp" >> .merlin
echo "B lib/plugins" >> .merlin
echo "B lib/plugins/gui" >> .merlin
find src \( -name '.*' -o -name tests -o -name doc -o -name '*.cache' \) -prune \
diff --git a/configure.in b/configure.in
index 3b2520fbf1930c3c3c5755b2886d38957baa215e..b08b5ff6c69162827a8205c11e82722bc79a02bd 100644
--- a/configure.in
+++ b/configure.in
@@ -372,8 +372,8 @@ fi;
AC_MSG_CHECKING(for MPFR)
-MPFR_PATH=$($OCAMLFIND query mlmpfr 2>/dev/null | tr -d '\r\n')
-if test -f "$MPFR_PATH/mlmpfr.$DYN_SUFFIX"; then
+MPFR_PATH=$($OCAMLFIND query gmp 2>/dev/null | tr -d '\r\n')
+if test -f "$MPFR_PATH/gmp.$DYN_SUFFIX"; then
HAS_MPFR="yes";
AC_MSG_RESULT(found)
else
diff --git a/src/libraries/utils/hptmap.ml b/src/libraries/utils/hptmap.ml
index 38109b77bd9cb4c39655e2bce83434f85fbf07c8..ef2c929ff585485075457881c40f11dfcd4d0e67 100644
--- a/src/libraries/utils/hptmap.ml
+++ b/src/libraries/utils/hptmap.ml
@@ -241,19 +241,26 @@ struct
open Structural_descr
let r = Recursive.create ()
let structural_descr =
- t_sum
- [| [| Key.packed_descr; V.packed_descr; p_abstract |];
- [| p_abstract;
- p_abstract;
- recursive_pack r;
- recursive_pack r;
- p_abstract |] |]
+ if Descr.is_unmarshable Key.descr || Descr.is_unmarshable V.descr
+ then t_unknown
+ else
+ t_sum
+ [| [| Key.packed_descr; V.packed_descr; p_abstract |];
+ [| p_abstract;
+ p_abstract;
+ recursive_pack r;
+ recursive_pack r;
+ p_abstract |] |]
let () = Recursive.update r structural_descr
let reprs = [ Empty ]
let equal = ( == )
let compare = compare
let hash = hash_generic
- let rehash x = !rehash_ref x
+ let rehash =
+ if Descr.is_unmarshable Key.descr || Descr.is_unmarshable V.descr
+ then Datatype.undefined
+ else fun x -> !rehash_ref x
+
let copy = Datatype.undefined
let internal_pretty_code = Datatype.pp_fail
let pretty = pretty
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index b62ef10637d45e7c71e04632c774ef9236570682..cba3b824536900affaa20ccabf0913d787b42b97 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -970,6 +970,19 @@ let () = Ast.apply_after_computed (fun _ ->
BuiltinsOverrides.add (kf, Some "Frama_C_load_state");
)
+let () = Parameter_customize.set_group precision_tuning
+module RealSignificandBits =
+ Int
+ (struct
+ let default = 128
+ let option_name = "-real-significand"
+ let arg_name = "n"
+ let help =
+ "set <n> the significand size of the MPFR representation \
+ of reals used by the Error Domain (defaults to 128)"
+ end)
+let () = add_precision_dep RealSignificandBits.parameter
+
(* ------------------------------------------------------------------------- *)
(* --- Messages --- *)
(* ------------------------------------------------------------------------- *)
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index dd5e461fb717ca34ac8228ac66ec1e19fd48d7b1..b42dc7d9343903409ec518dd8b9cee5062679bf4 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -99,6 +99,8 @@ module LoadFunctionState:
val get_SaveFunctionState : unit -> Cil_types.kernel_function * string
val get_LoadFunctionState : unit -> Cil_types.kernel_function * string
+module RealSignificandBits : Parameter_sig.Int
+
module UndefinedPointerComparisonPropagateAll: Parameter_sig.Bool
module WarnPointerComparison: Parameter_sig.String
diff --git a/src/plugins/value/values/errors_value.ko.ml b/src/plugins/value/values/errors_value.ko.ml
index 1af8ac32f042d1b8047e44dc905afe9d956118c6..6067524c74d4a503a233f44d4ae39e644f49185f 100644
--- a/src/plugins/value/values/errors_value.ko.ml
+++ b/src/plugins/value/values/errors_value.ko.ml
@@ -18,6 +18,7 @@ let top = ()
let is_included () () = true
let join () () = ()
let narrow () () = `Value ()
+let reduce _ () = `Value ()
let zero = ()
let float_zeros = ()
diff --git a/src/plugins/value/values/errors_value.ml b/src/plugins/value/values/errors_value.ml
new file mode 100755
index 0000000000000000000000000000000000000000..90b45ab39a30da491afc3e05aa39653f58e7e703
--- /dev/null
+++ b/src/plugins/value/values/errors_value.ml
@@ -0,0 +1,542 @@
+(**************************************************************************)
+(* *)
+(* This file is part of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2017 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* 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, version 2.1. *)
+(* *)
+(* It 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. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Cil_types
+open Eval
+
+
+(*-----------------------------------------------------------------------------
+ * Module describing the different precisions that will be manipulated
+ *---------------------------------------------------------------------------*)
+module Precisions = struct
+ type t = Simple | Double | Long_Double | Real | Undefined
+ let get = function
+ | Simple -> 24
+ | Double -> 53
+ | Long_Double -> 64
+ | Real -> Value_parameters.RealSignificandBits.get ()
+ | Undefined -> -1
+ let pretty fmt p = Format.fprintf fmt "%i" (get p)
+ let compare a b =
+ let x, y = get a, get b in
+ if x < y then -1
+ else if x > y then 1
+ else 0
+ let max a b = if compare a b <= 0 then b else a
+end
+
+
+(*-----------------------------------------------------------------------------
+ * Sign type for infinites and zeros
+ *---------------------------------------------------------------------------*)
+type sign = Positive | Negative
+
+
+(*-----------------------------------------------------------------------------
+ * Module representing numbers with a specified precision
+ *---------------------------------------------------------------------------*)
+(*
+module type FSig = sig
+ type t
+ val pretty : Format.formatter -> t -> unit
+ val compare : t -> t -> int
+ val of_int : ?rnd:Mpfr.round -> Precisions.t -> int -> t
+ val of_float : ?rnd:Mpfr.round -> Precisions.t -> float -> t
+ val make_inf : Precisions.t -> sign -> t
+ val make_zero : Precisions.t -> sign -> 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 : ?rnd:Mpfr.round -> ?prec:Precisions.t -> t -> t
+ val abs : ?rnd:Mpfr.round -> ?prec:Precisions.t -> t -> t
+ val sqrt : ?rnd:Mpfr.round -> ?prec:Precisions.t -> t -> t
+ val max : t -> t -> t
+ val min : t -> t -> t
+end
+*)
+
+module F = struct
+
+ type t = Mpfrf.t * Precisions.t
+
+ let set_prec p f =
+ match p with
+ | Precisions.Undefined -> f
+ | _ -> Mpfr.set_default_prec (Precisions.get p) ; f
+
+ let pretty fmt (x, p) =
+ Format.fprintf fmt "%a:%a" Mpfrf.print x Precisions.pretty p
+
+ let compare (x, _) (y, _) = Mpfrf.cmp x y
+
+ let of_int ?(rnd = Mpfr.Near) prec i =
+ set_prec prec Mpfrf.of_int i rnd, prec
+
+ let of_float ?(rnd = Mpfr.Near) prec f =
+ set_prec prec Mpfrf.of_float f rnd, prec
+
+ let of_string ?(rnd = Mpfr.Near) prec s =
+ set_prec prec Mpfrf.of_string s rnd, prec
+
+ let make_inf sign =
+ let sign_int = if sign = Positive then 1 else -1 in
+ let tmp = Mpfr.init () in Mpfr.set_inf tmp sign_int ;
+ Mpfrf.of_mpfr tmp, Precisions.Undefined
+
+ let make_zero sign =
+ let zero = if sign = Positive then 0.0 else ~-. 0.0 in
+ of_float Precisions.Undefined zero
+
+ let add ?(rnd = Mpfr.Near) ?prec (x, px) (y, py) =
+ let p = match prec with
+ | None -> Precisions.max px py
+ | Some p -> p
+ in set_prec p Mpfrf.add x y rnd, p
+
+ let sub ?(rnd = Mpfr.Near) ?prec (x, px) (y, py) =
+ let p = match prec with
+ | None -> Precisions.max px py
+ | Some p -> p
+ in set_prec p Mpfrf.sub x y rnd, p
+
+ let mul ?(rnd = Mpfr.Near) ?prec (x, px) (y, py) =
+ let p = match prec with
+ | None -> Precisions.max px py
+ | Some p -> p
+ in set_prec p Mpfrf.mul x y rnd, p
+
+ let div ?(rnd = Mpfr.Near) ?prec (x, px) (y, py) =
+ let p = match prec with
+ | None -> Precisions.max px py
+ | Some p -> p
+ in set_prec p Mpfrf.div x y rnd, p
+
+ let max x y = if compare x y <= 0 then y else x
+ let min x y = if compare x y <= 0 then x else y
+
+ let neg ?(rnd = Mpfr.Near) ?prec (x, px) =
+ let p = match prec with
+ | None -> px
+ | Some p -> p
+ in set_prec p Mpfrf.neg x rnd, p
+
+ let abs ?(rnd = Mpfr.Near) ?prec (x, px) =
+ let p = match prec with
+ | None -> px
+ | Some p -> p
+ in set_prec p Mpfrf.abs x rnd, p
+
+ let sqrt ?(rnd = Mpfr.Near) ?prec (x, px) =
+ let p = match prec with
+ | None -> px
+ | Some p -> p
+ in set_prec p Mpfrf.sqrt x rnd, p
+
+end
+
+
+(*-----------------------------------------------------------------------------
+ * Intervals definition
+ *---------------------------------------------------------------------------*)
+module I = struct
+
+ type t = F.t * F.t
+
+ let get_prec ((_, px), (_, py)) f =
+ match px, py with
+ | Precisions.Undefined, Precisions.Undefined -> f Precisions.Undefined
+ | _, Precisions.Undefined -> f px
+ | Precisions.Undefined, _ -> f py
+ | _ ->
+ if Precisions.compare px py == 0 then f px
+ else failwith "Differents precisions in the same interval"
+
+ let top = F.make_inf Negative, F.make_inf Positive
+ let zero = F.make_zero Negative, F.make_zero Positive
+
+ let of_floats ~prec (x, y) =
+ F.of_float ~rnd:Mpfr.Down prec x,
+ F.of_float ~rnd:Mpfr.Up prec y
+
+ let of_strings ~prec (x, y) =
+ F.of_string ~rnd:Mpfr.Down prec x,
+ F.of_string ~rnd:Mpfr.Up prec y
+
+ let pretty fmt (x, y) =
+ Format.fprintf fmt "[%a ; %a]" F.pretty x F.pretty y
+
+ let compare (x, y) (x', y') =
+ let c = F.compare x x' in
+ if c = 0 then F.compare y y' else c
+
+ let is_included (x, y) (x', y') =
+ F.compare x x' <= 0 && F.compare y y' <= 0
+
+ let join (x, y) (x', y') = F.min x x', F.max y y'
+
+ let narrow (x, y) (x', y') =
+ if F.compare x' y <= 0 || F.compare x y' <= 0 then
+ `Value (F.max x x', F.min y y')
+ else `Bottom
+
+ let neg (x, y) =
+ let f p =
+ F.neg ~rnd:Mpfr.Down ~prec:p y,
+ F.neg ~rnd:Mpfr.Up ~prec:p x
+ in get_prec (x, y) f
+
+ let sqrt (x, y) =
+ let f p =
+ let (x, px) = F.sqrt ~rnd:Mpfr.Down ~prec:p x in
+ let (y, py) = F.sqrt ~rnd:Mpfr.Up ~prec:p y in
+ if Mpfr.nan_p x || Mpfr.nan_p y then `Bottom
+ else `Value ((x, px), (y, py))
+ in get_prec (x, y) f
+
+ let add (x, y) (x', y') =
+ F.add ~rnd:Mpfr.Down x x', F.add ~rnd:Mpfr.Up y y'
+
+ let sub (x, y) (x', y') =
+ F.sub ~rnd:Mpfr.Down x y', F.sub ~rnd:Mpfr.Up y x'
+
+ let mul (x, y) (x', y') =
+ let s, s' = [x ; x ; y ; y], [x' ; y' ; x' ; y'] in
+ let s_minus = List.map2 (F.mul ~rnd:Mpfr.Down) s s' in
+ let s_plus = List.map2 (F.mul ~rnd:Mpfr.Up ) s s' in
+ let get f l = List.fold_left f (List.hd l) (List.tl l) in
+ get F.min s_minus, get F.max s_plus
+
+ let div (x, y) (x', y') =
+ let s, s' = [x ; x ; y ; y], [x' ; y' ; x' ; y'] in
+ let s_minus = List.map2 (F.div ~rnd:Mpfr.Down) s s' in
+ let s_plus = List.map2 (F.div ~rnd:Mpfr.Up ) s s' in
+ let get f l = List.fold_left f (List.hd l) (List.tl l) in
+ let (min, pmin) = get F.min s_minus in
+ let (max, pmax) = get F.max s_plus in
+ if Mpfr.inf_p min || Mpfr.inf_p max then `Bottom
+ else `Value ((min, pmin), (max, pmax))
+
+ let max_abs (x, y) = F.max (F.abs x) (F.abs y)
+ let min_abs (x, y) = F.min (F.abs x) (F.abs y)
+
+end
+
+
+module Cst = struct
+ let e = F.of_float Precisions.Real (2.0 ** (~-.53.0))
+ let e_interval = F.neg e, e
+ let one_interval = I.of_floats ~prec:Precisions.Real (1.0, 1.0)
+ let std_error = I.add one_interval e_interval
+end
+
+(*-----------------------------------------------------------------------------
+ * Abstract value for numerical errors estimation
+ *---------------------------------------------------------------------------*)
+
+(* The abstract value is a record with four fields :
+ * - exact : interval abstraction of the real value
+ * - approx : interval abstraction of the float value
+ * - abs_err : interval abstraction of the absolute error value
+ * - rel_err : interval abstraction of the relative error value
+ * A zonotope abstraction for each of those fields may be added *)
+type err =
+ { exact : I.t
+ ; approx : I.t
+ ; abs_err : I.t
+ ; rel_err : I.t
+ }
+
+(* Lattice Structure *)
+let top =
+ { exact = I.top
+ ; approx = I.top
+ ; abs_err = I.top
+ ; rel_err = I.top
+ }
+
+let is_included x y =
+ I.is_included x.exact y.exact &&
+ I.is_included x.approx y.approx &&
+ I.is_included x.abs_err y.abs_err &&
+ I.is_included x.rel_err y.rel_err
+
+let join x y =
+ { exact = I.join x.exact y.exact
+ ; approx = I.join x.approx y.approx
+ ; abs_err = I.join x.abs_err y.abs_err
+ ; rel_err = I.join x.rel_err y.rel_err
+ }
+
+let narrow x y =
+ let exact = I.narrow x.exact y.exact in
+ let approx = I.narrow x.approx y.approx in
+ let abs_err = I.narrow x.abs_err y.abs_err in
+ let rel_err = I.narrow x.rel_err y.rel_err in
+ match exact, approx, abs_err, rel_err with
+ | `Value exact, `Value approx,`Value abs_err, `Value rel_err ->
+ `Value { exact ; approx ; abs_err ; rel_err }
+ | _, _, _, _ -> `Bottom
+
+let reduce fval t =
+ match Fval.min_and_max fval with
+ | Some (min, max), false ->
+ let itv = Fval.F.to_float min, Fval.F.to_float max in
+ let itv = I.of_floats Precisions.Double itv in
+ I.narrow t.approx itv >>-: fun approx ->
+ { t with approx }
+ (* Do not reduce when NaN occurs. *)
+ | _ -> `Value t
+
+(* Associated Datatype *)
+module T =
+ struct
+ type t = err
+ include Datatype.Undefined
+ let structural_descr = Structural_descr.t_unknown
+ let compare x y =
+ let cmp_exact = I.compare x.exact y.exact in
+ let cmp_approx = I.compare x.approx y.approx in
+ let cmp_abs_err = I.compare x.abs_err y.abs_err in
+ let cmp_rel_err = I.compare x.rel_err y.rel_err in
+ if cmp_exact = 0 then
+ if cmp_approx = 0 then
+ if cmp_abs_err = 0 then
+ cmp_rel_err
+ else cmp_abs_err
+ else cmp_approx
+ else cmp_exact
+ let equal = Datatype.from_compare
+ let hash = Hashtbl.hash
+ let reprs = [top]
+ let name = "Value.Error_values.Errors"
+ let pretty fmt v =
+ Format.fprintf fmt
+ "Exact : %a@ Approx : %a@ Abs Err : %a@ Rel Err : %a"
+ I.pretty v.exact
+ I.pretty v.approx
+ I.pretty v.abs_err
+ I.pretty v.rel_err
+ end
+include Datatype.Make(T)
+
+let pretty_debug = pretty
+let pretty_typ _ = pretty
+
+(* Constructors *)
+let zero = top
+
+let float_zeros =
+ { exact = I.zero
+ ; approx = I.zero
+ ; abs_err = I.zero
+ ; rel_err = I.zero
+ }
+
+let top_int = top
+
+let inject_int _ _ = top
+
+let inject_address _ = top
+
+
+(*-----------------------------------------------------------------------------
+ * Semantics definitions
+ *---------------------------------------------------------------------------*)
+(* Semantics *)
+module type Semantic =
+ sig
+ val neg : err -> I.t
+ val sqrt : err -> I.t or_bottom
+ val add : err -> err -> I.t
+ val sub : err -> err -> I.t
+ val mul : err -> err -> I.t
+ val div : err -> err -> I.t or_bottom
+ end
+
+
+module Exact_Sem : Semantic =
+ struct
+ let neg v = I.neg v.exact
+ let sqrt v = I.sqrt v.exact
+ let add x y = I.add x.exact y.exact
+ let sub x y = I.sub x.exact y.exact
+ let mul x y = I.mul x.exact y.exact
+ let div x y = I.div x.exact y.exact
+ end
+
+module Approx_Sem : Semantic =
+ struct
+ let neg v = I.neg v.approx
+ let sqrt v = I.sqrt v.approx
+ let add x y = I.add x.approx y.approx
+ let sub x y = I.sub x.approx y.approx
+ let mul x y = I.mul x.approx y.approx
+ let div x y = I.div x.approx y.approx
+ end
+
+module Abs_Err_Sem : Semantic =
+ struct
+ let neg v = I.neg v.abs_err
+ let sqrt v =
+ let approx = Approx_Sem.sqrt v in
+ let exact = Exact_Sem.sqrt v in
+ match approx, exact with
+ | `Value x, `Value y -> `Value (I.sub x y)
+ | _, _ -> `Bottom
+ let add x y =
+ let abs_err = I.add x.abs_err y.abs_err in
+ let approx = I.add x.approx y.approx in
+ I.add abs_err (I.mul approx Cst.e_interval)
+ let sub x y =
+ let abs_err = I.sub x.abs_err y.abs_err in
+ let approx = I.sub x.approx y.approx in
+ I.add abs_err (I.mul approx Cst.e_interval)
+ let mul x y =
+ let mul = I.mul (I.mul x.approx y.approx) Cst.e_interval in
+ let xey = I.mul x.exact y.abs_err in
+ let yex = I.mul y.exact x.abs_err in
+ let exy = I.mul x.abs_err y.abs_err in
+ I.add (I.add mul (I.add xey yex)) exy
+ let div x y =
+ let xyapprox = I.div x.approx y.approx in
+ let xyexact = I.div x.exact y.exact in
+ match xyapprox, xyexact with
+ | `Value ap, `Value ex -> `Value (I.sub (I.mul ap Cst.std_error) ex)
+ | _, _ -> `Bottom
+ end
+
+module Rel_Err_Sem : Semantic =
+ struct
+ let neg v = I.neg v.rel_err
+ let sqrt v =
+ let f s = I.sub (I.mul s Cst.std_error) Cst.one_interval in
+ (I.sqrt (I.add v.rel_err Cst.one_interval)) >>-: f
+ let add x y =
+ let d = F.max (I.max_abs x.rel_err) (I.max_abs y.rel_err) in
+ let num = F.add (I.max_abs x.exact) (I.max_abs y.exact) in
+ let den = I.min_abs (I.add x.exact y.exact) in
+ let eps = F.add (F.of_float Precisions.Real 1.0) Cst.e in
+ let v = F.add (F.mul (F.mul (F.div num den) d) eps) Cst.e in
+ (F.neg ~rnd:Mpfr.Down v, v)
+ let sub x y =
+ let d = F.max (I.max_abs x.rel_err) (I.max_abs y.rel_err) in
+ let num = F.add (I.max_abs x.exact) (I.max_abs y.exact) in
+ let den = I.min_abs (I.sub x.exact y.exact) in
+ let eps = F.add (F.of_float Precisions.Real 1.0) Cst.e in
+ let v = F.add (F.mul (F.mul (F.div num den) d) eps) Cst.e in
+ (F.neg ~rnd:Mpfr.Down v, v)
+ let mul x y =
+ let ex = I.add Cst.one_interval x.rel_err in
+ let ey = I.add Cst.one_interval y.rel_err in
+ I.sub (I.mul (I.mul ex ey) Cst.std_error) Cst.one_interval
+ let div x y =
+ let ex = I.add Cst.one_interval x.rel_err in
+ let ey = I.add Cst.one_interval y.rel_err in
+ let f d = I.sub (I.mul d Cst.std_error) Cst.one_interval in
+ (I.div ex ey) >>-: f
+ end
+
+
+(* Forward operations *)
+let return v = `Value v, Alarmset.all
+
+let constant _ = function
+ | CReal (r, fkind, opt) ->
+ let prec = match fkind with
+ | FFloat -> Precisions.Simple
+ | FDouble -> Precisions.Double
+ | FLongDouble -> Precisions.Long_Double
+ in
+ let exact = match opt with
+ | Some s -> I.of_strings Precisions.Real (s, s)
+ | None -> I.of_floats Precisions.Real (r, r)
+ in
+ { exact = exact ; approx = I.of_floats prec (r, r)
+ ; abs_err = I.zero ; rel_err = I.zero
+ }
+ | _ -> top
+
+let forward_unop ~context:_ _ op v = match op with
+ | Neg ->
+ let exact , approx = Exact_Sem.neg v, Approx_Sem.neg v in
+ let abs_err, rel_err = Abs_Err_Sem.neg v, Rel_Err_Sem.neg v in
+ return { exact ; approx ; abs_err ; rel_err }
+ | _ -> return top
+
+let forward_binop ~context:_ _ op x y =
+ let calculate_errors exact approx prg_abs prg_rel =
+ let cal_abs = I.sub approx exact in
+ let cal_rel = I.div cal_abs exact in
+ let abs_err = match I.narrow prg_abs cal_abs with
+ | `Value v -> v | `Bottom -> prg_abs
+ in
+ let rel_err = match cal_rel >>- (I.narrow prg_rel) with
+ | `Value v -> v | `Bottom -> prg_rel
+ in
+ return { exact ; approx ; abs_err ; rel_err }
+ in
+ match op with
+ | PlusA ->
+ let exact , approx = Exact_Sem.add x y, Approx_Sem.add x y in
+ let prg_abs, prg_rel = Abs_Err_Sem.add x y, Rel_Err_Sem.add x y in
+ calculate_errors exact approx prg_abs prg_rel
+ | MinusA ->
+ let exact , approx = Exact_Sem.sub x y, Approx_Sem.sub x y in
+ let prg_abs, prg_rel = Abs_Err_Sem.sub x y, Rel_Err_Sem.sub x y in
+ calculate_errors exact approx prg_abs prg_rel
+ | Mult ->
+ let exact , approx = Exact_Sem.mul x y, Approx_Sem.mul x y in
+ let prg_abs, prg_rel = Abs_Err_Sem.mul x y, Rel_Err_Sem.mul x y in
+ calculate_errors exact approx prg_abs prg_rel
+ | Div ->
+ let exact_b , approx_b = Exact_Sem.div x y, Approx_Sem.div x y in
+ let prg_abs_b, prg_rel_b = Abs_Err_Sem.div x y, Rel_Err_Sem.div x y in
+ let res = match exact_b, approx_b, prg_abs_b, prg_rel_b with
+ | `Value exact, `Value approx, `Value prg_abs, `Value prg_rel ->
+ calculate_errors exact approx prg_abs prg_rel
+ | _, _, _, _ -> `Bottom, Alarmset.all
+ in res
+ | _ -> return top
+
+
+(* Backward operations *)
+let backward_binop ~input_type:_ ~resulting_type:_ op
+ ~left:_ ~right:_ ~result:_ =
+ match op with
+ | _ -> `Value (None, None)
+let backward_unop ~typ_arg:_ _ ~arg:_ ~res:_ = `Value None
+let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ = `Value None
+
+
+(* Reinterpret and Cast *)
+let truncate_integer _ _ _ = return top
+let rewrap_integer _ _ = top
+let restrict_float ~remove_infinite:_ _ _ t = return t
+let cast ~src_typ:_ ~dst_typ:_ _ _ = return top
+let resolve_functions _ = `Top, true
+
+
+(* Misc *)
+let error_key = Structure.Key_Value.create_key "error_values"
+let structure = Structure.Key_Value.Leaf error_key
+
diff --git a/src/plugins/value/values/errors_value.ok.ml b/src/plugins/value/values/errors_value.ok.ml
index bdf88f2fbfd3d6ae374fefec4cc1c15676631b1a..c0f281b750df98c57781669b29f9fc1702aa21c0 100755
--- a/src/plugins/value/values/errors_value.ok.ml
+++ b/src/plugins/value/values/errors_value.ok.ml
@@ -22,127 +22,226 @@
open Cil_types
open Eval
-open Abstract_interp
-(* module M = Mpfr *)
+(*-----------------------------------------------------------------------------
+ * Module describing the different precisions that will be manipulated
+ *---------------------------------------------------------------------------*)
+module Precisions = struct
+ type t = Simple | Double | Long_Double | Real | Undefined
+ let real_prec = Value_parameters.RealSignificandBits.get ()
+ let get = function
+ | Simple -> 24
+ | Double -> 53
+ | Long_Double -> 64
+ | Real -> real_prec
+ | Undefined -> -1
+ let pretty fmt p = Format.fprintf fmt "%i" (get p)
+ let compare a b =
+ let x, y = get a, get b in
+ if x < y then -1
+ else if x > y then 1
+ else 0
+ let max a b = if compare a b <= 0 then b else a
+end
(*-----------------------------------------------------------------------------
- * Generic intervals implementation
+ * Sign type for infinites and zeros
*---------------------------------------------------------------------------*)
-module type IElement =
- sig
- type t
- val zero : t
- val minimal_value : t
- val maximal_value : t
- val pord : t -> t -> bool
- val compare : t -> t -> int
- val max : t -> t -> t
- val min : t -> t -> t
- val add : t -> t -> t
- val sub : t -> t -> t
- val mul : t -> t -> t
- val div : t -> t -> t
- val abs : t -> t
- val neg : t -> t
- val sqrt : t -> t
- val pretty : Format.formatter -> t -> unit
- end
+type sign = Positive | Negative
-module Interval =
- struct
- module type S =
- sig
- type elt
- type t = elt * elt
- val top : t
- val zero : t
- val compare : t -> t -> int
- val pord : t -> t -> bool
- val join : t -> t -> t
- val narrow : t -> t -> t or_bottom
- val neg : t -> t
- val sqrt : t -> t
- val add : t -> t -> t
- val sub : t -> t -> t
- val mul : t -> t -> t
- val div : t -> t -> t
- val max_abs : t -> elt
- val min_abs : t -> elt
- val pretty : Format.formatter -> t -> unit
- end
- module Make (Elt : IElement) : (S with type elt = Elt.t) =
- struct
- type elt = Elt.t
- type t = elt * elt
- let top = Elt.minimal_value, Elt.maximal_value
- let zero = Elt.neg Elt.zero, Elt.zero
- let compare (x, y) (x', y') =
- let cmp = Elt.compare x x' in
- if cmp != 0 then cmp
- else Elt.compare y y'
- let pord (x, y) (x', y') = Elt.pord x x' && Elt.pord y y'
- let join (x, y) (x', y') = Elt.min x x', Elt.max y y'
- let narrow (x, y) (x', y') =
- if Elt.pord x' y || Elt.pord x y' then
- `Value (Elt.max x x', Elt.min y y')
- else `Bottom
- let neg (x, y) = Elt.neg y, Elt.neg x
- let sqrt (x, y) = Elt.sqrt x, Elt.sqrt y
- let add (x, y) (x', y') = Elt.add x x', Elt.add y y'
- let sub (x, y) (x', y') = Elt.sub x y', Elt.sub y x'
- let mul (x, y) (x', y') =
- let s = List.map2 Elt.mul [x ; x ; y ; y] [x' ; y' ; x' ; y'] in
- let get f = List.fold_left f (List.hd s) (List.tl s) in
- get Elt.min, get Elt.max
- let div (x, y) (x', y') =
- let s = List.map2 Elt.div [x ; x ; y ; y] [x' ; y' ; x' ; y'] in
- let get f = List.fold_left f (List.hd s) (List.tl s) in
- get Elt.min, get Elt.max
- let max_abs (x, y) = max (Elt.abs x) (Elt.abs y)
- let min_abs (x, y) = min (Elt.abs x) (Elt.abs y)
- let pretty fmt (x, y) =
- Format.fprintf fmt "[%a ; %a]" Elt.pretty x Elt.pretty y
- end
- end
+(*-----------------------------------------------------------------------------
+ * Module representing numbers with a specified precision
+ *---------------------------------------------------------------------------*)
+module F = struct
+
+ type t = Mpfrf.t * Precisions.t
+
+ let set_prec p f =
+ match p with
+ | Precisions.Undefined -> f
+ | _ -> Mpfr.set_default_prec (Precisions.get p) ; f
+
+ let pretty fmt (x, p) =
+ Format.fprintf fmt "%a:%a" Mpfrf.print x Precisions.pretty p
+
+ let compare (x, _) (y, _) = Mpfrf.cmp x y
+
+ let of_int ?(rnd = Mpfr.Near) prec i =
+ set_prec prec Mpfrf.of_int i rnd, prec
+
+ let of_float ?(rnd = Mpfr.Near) prec f =
+ set_prec prec Mpfrf.of_float f rnd, prec
+
+ let of_string ?(rnd = Mpfr.Near) prec s =
+ set_prec prec Mpfrf.of_string s rnd, prec
+
+ let make_inf sign =
+ let sign_int = if sign = Positive then 1 else -1 in
+ let tmp = Mpfr.init () in Mpfr.set_inf tmp sign_int ;
+ Mpfrf.of_mpfr tmp, Precisions.Undefined
+
+ let make_zero sign =
+ let zero = if sign = Positive then 0.0 else ~-. 0.0 in
+ of_float Precisions.Undefined zero
+
+ let add ?(rnd = Mpfr.Near) ?prec (x, px) (y, py) =
+ let p = match prec with
+ | None -> Precisions.max px py
+ | Some p -> p
+ in set_prec p Mpfrf.add x y rnd, p
+
+ let sub ?(rnd = Mpfr.Near) ?prec (x, px) (y, py) =
+ let p = match prec with
+ | None -> Precisions.max px py
+ | Some p -> p
+ in set_prec p Mpfrf.sub x y rnd, p
+
+ let mul ?(rnd = Mpfr.Near) ?prec (x, px) (y, py) =
+ let p = match prec with
+ | None -> Precisions.max px py
+ | Some p -> p
+ in set_prec p Mpfrf.mul x y rnd, p
+
+ let div ?(rnd = Mpfr.Near) ?prec (x, px) (y, py) =
+ let p = match prec with
+ | None -> Precisions.max px py
+ | Some p -> p
+ in set_prec p Mpfrf.div x y rnd, p
+
+ let max x y = if compare x y <= 0 then y else x
+ let min x y = if compare x y <= 0 then x else y
+
+ let neg ?(rnd = Mpfr.Near) ?prec (x, px) =
+ let p = match prec with
+ | None -> px
+ | Some p -> p
+ in set_prec p Mpfrf.neg x rnd, p
+
+ let abs ?(rnd = Mpfr.Near) ?prec (x, px) =
+ let p = match prec with
+ | None -> px
+ | Some p -> p
+ in set_prec p Mpfrf.abs x rnd, p
+
+ let sqrt ?(rnd = Mpfr.Near) ?prec (x, px) =
+ let p = match prec with
+ | None -> px
+ | Some p -> p
+ in set_prec p Mpfrf.sqrt x rnd, p
+
+end
(*-----------------------------------------------------------------------------
- * Intervals instanciation for floats
+ * Intervals definition
*---------------------------------------------------------------------------*)
-module R =
- struct
- type t = float
- let zero = 0.0
- let minimal_value = -. max_float
- let maximal_value = max_float
- let pord = ( <= )
- let compare = Pervasives.compare
- let max = Pervasives.max
- let min = Pervasives.min
- let neg v = -. v
- let add = ( +. )
- let sub = ( -. )
- let mul = ( *. )
- let div = ( /. )
- let abs = abs_float
- let sqrt = sqrt
- let pretty = Format.pp_print_float
- let one = 1.0, 1.0
- let em = 2.0 ** -53.0
- let noise = -.em, em
- let stderr = 1.0 -. em, 1.0 +. em
- end
+module I = struct
+
+ type t = F.t * F.t
+
+ let get_prec ((_, px), (_, py)) f =
+ match px, py with
+ | Precisions.Undefined, Precisions.Undefined -> f Precisions.Undefined
+ | _, Precisions.Undefined -> f px
+ | Precisions.Undefined, _ -> f py
+ | _ ->
+ if Precisions.compare px py == 0 then f px
+ else failwith "Differents precisions in the same interval"
+
+ let top = F.make_inf Negative, F.make_inf Positive
+ let zero = F.make_zero Negative, F.make_zero Positive
+
+ let of_floats ~prec (x, y) =
+ F.of_float ~rnd:Mpfr.Down prec x,
+ F.of_float ~rnd:Mpfr.Up prec y
+
+ let of_strings ~prec (x, y) =
+ F.of_string ~rnd:Mpfr.Down prec x,
+ F.of_string ~rnd:Mpfr.Up prec y
+
+ let pretty fmt (x, y) =
+ Format.fprintf fmt "[%a ; %a]" F.pretty x F.pretty y
+
+ let compare (x, y) (x', y') =
+ let c = F.compare x x' in
+ if c = 0 then F.compare y y' else c
+
+ let is_included (x, y) (x', y') =
+ F.compare x x' <= 0 && F.compare y y' <= 0
+
+ let join (x, y) (x', y') = F.min x x', F.max y y'
+
+ let narrow (x, y) (x', y') =
+ if F.compare x' y <= 0 || F.compare x y' <= 0 then
+ `Value (F.max x x', F.min y y')
+ else `Bottom
+
+ let neg (x, y) =
+ let f p =
+ F.neg ~rnd:Mpfr.Down ~prec:p y,
+ F.neg ~rnd:Mpfr.Up ~prec:p x
+ in get_prec (x, y) f
+
+ let sqrt (x, y) =
+ let f p =
+ let (x, px) = F.sqrt ~rnd:Mpfr.Down ~prec:p x in
+ let (y, py) = F.sqrt ~rnd:Mpfr.Up ~prec:p y in
+ if Mpfr.nan_p x || Mpfr.nan_p y then `Bottom
+ else `Value ((x, px), (y, py))
+ in get_prec (x, y) f
+
+ let add (x, y) (x', y') =
+ F.add ~rnd:Mpfr.Down x x', F.add ~rnd:Mpfr.Up y y'
+
+ let sub (x, y) (x', y') =
+ F.sub ~rnd:Mpfr.Down x y', F.sub ~rnd:Mpfr.Up y x'
+
+ let mul (x, y) (x', y') =
+ let s, s' = [x ; x ; y ; y], [x' ; y' ; x' ; y'] in
+ let s_minus = List.map2 (F.mul ~rnd:Mpfr.Down) s s' in
+ let s_plus = List.map2 (F.mul ~rnd:Mpfr.Up ) s s' in
+ let get f l = List.fold_left f (List.hd l) (List.tl l) in
+ get F.min s_minus, get F.max s_plus
+
+ let div (x, y) (x', y') =
+ let s, s' = [x ; x ; y ; y], [x' ; y' ; x' ; y'] in
+ let s_minus = List.map2 (F.div ~rnd:Mpfr.Down) s s' in
+ let s_plus = List.map2 (F.div ~rnd:Mpfr.Up ) s s' in
+ let get f l = List.fold_left f (List.hd l) (List.tl l) in
+ let (min, pmin) = get F.min s_minus in
+ let (max, pmax) = get F.max s_plus in
+ if Mpfr.inf_p min || Mpfr.inf_p max then `Bottom
+ else `Value ((min, pmin), (max, pmax))
+
+ let max_abs (x, y) = F.max (F.abs x) (F.abs y)
+ let min_abs (x, y) = F.min (F.abs x) (F.abs y)
+
+end
-module I = Interval.Make(R)
+(*-----------------------------------------------------------------------------
+ * Constants definitions
+ *---------------------------------------------------------------------------*)
+module Cst = struct
+ let e = F.of_float Precisions.Real (2.0 ** (~-.53.0))
+ let e_interval = F.neg e, e
+ let one_interval = I.of_floats ~prec:Precisions.Real (1.0, 1.0)
+ let std_error = I.add one_interval e_interval
+end
(*-----------------------------------------------------------------------------
- * Abstract value for numerical errors estimation
+ * Abstract value for numerical errors estimation
+ *-----------------------------------------------------------------------------
+ * The abstract value is a record with four fields :
+ * - exact : interval abstraction of the real value
+ * - approx : interval abstraction of the float value
+ * - abs_err : interval abstraction of the absolute error value
+ * - rel_err : interval abstraction of the relative error value
+ * A zonotope abstraction for each of those fields may be added
*---------------------------------------------------------------------------*)
type err =
{ exact : I.t
@@ -151,7 +250,6 @@ type err =
; rel_err : I.t
}
-
(* Lattice Structure *)
let top =
{ exact = I.top
@@ -161,10 +259,10 @@ let top =
}
let is_included x y =
- I.pord x.exact y.exact &&
- I.pord x.approx y.approx &&
- I.pord x.abs_err y.abs_err &&
- I.pord x.rel_err y.rel_err
+ I.is_included x.exact y.exact &&
+ I.is_included x.approx y.approx &&
+ I.is_included x.abs_err y.abs_err &&
+ I.is_included x.rel_err y.rel_err
let join x y =
{ exact = I.join x.exact y.exact
@@ -176,28 +274,29 @@ let join x y =
let narrow x y =
let exact = I.narrow x.exact y.exact in
let approx = I.narrow x.approx y.approx in
- let abs_err = I.narrow x.abs_err y.abs_err in
- let rel_err = I.narrow x.rel_err y.rel_err in
+ let abs_err = I.narrow x.abs_err y.abs_err in
+ let rel_err = I.narrow x.rel_err y.rel_err in
match exact, approx, abs_err, rel_err with
| `Value exact, `Value approx,`Value abs_err, `Value rel_err ->
- `Value { exact ; approx ; abs_err ; rel_err }
+ `Value { exact ; approx ; abs_err ; rel_err }
| _, _, _, _ -> `Bottom
let reduce fval t =
match Fval.min_and_max fval with
| Some (min, max), false ->
let itv = Fval.F.to_float min, Fval.F.to_float max in
+ let itv = I.of_floats Precisions.Double itv in
I.narrow t.approx itv >>-: fun approx ->
{ t with approx }
(* Do not reduce when NaN occurs. *)
| _ -> `Value t
-
(* Associated Datatype *)
module T =
struct
type t = err
- include Datatype.Serializable_undefined
+ include Datatype.Undefined
+ let structural_descr = Structural_descr.t_unknown
let compare x y =
let cmp_exact = I.compare x.exact y.exact in
let cmp_approx = I.compare x.approx y.approx in
@@ -227,7 +326,6 @@ include Datatype.Make(T)
let pretty_debug = pretty
let pretty_typ _ = pretty
-
(* Constructors *)
let zero = top
@@ -245,19 +343,22 @@ let inject_int _ _ = top
let inject_address _ = top
-(* Semantics *)
-module type Semantic =
+(*-----------------------------------------------------------------------------
+ * Semantics definitions
+ *---------------------------------------------------------------------------*)
+module type Semantic = (* Move it to MLI ? *)
sig
val neg : err -> I.t
- val sqrt : err -> I.t
+ val sqrt : err -> I.t or_bottom
val add : err -> err -> I.t
val sub : err -> err -> I.t
val mul : err -> err -> I.t
- val div : err -> err -> I.t
+ val div : err -> err -> I.t or_bottom
end
-
-module Exact_Semantic : Semantic =
+(* The exact semantic is implemented as the concrete semantic on the exact
+ * field of the abstract value *)
+module Exact_Sem : Semantic =
struct
let neg v = I.neg v.exact
let sqrt v = I.sqrt v.exact
@@ -267,148 +368,151 @@ module Exact_Semantic : Semantic =
let div x y = I.div x.exact y.exact
end
-module Approx_Semantic : Semantic =
+(* The approx semantic is implemented as the concrete semantic on the
+ * approx field of the abstract value *)
+module Approx_Sem : Semantic =
struct
- let neg v = I.neg v.approx
- let sqrt v = I.mul (I.sqrt v.approx) R.stderr
- let add x y = I.mul (I.add x.approx y.approx) R.stderr
- let sub x y = I.mul (I.sub x.approx y.approx) R.stderr
- let mul x y = I.mul (I.mul x.approx y.approx) R.stderr
- let div x y = I.mul (I.div x.approx y.approx) R.stderr
+ let neg v = I.neg v.approx
+ let sqrt v = I.sqrt v.approx
+ let add x y = I.add x.approx y.approx
+ let sub x y = I.sub x.approx y.approx
+ let mul x y = I.mul x.approx y.approx
+ let div x y = I.div x.approx y.approx
end
-module Abs_Err_Semantic : Semantic =
+(* Implementation of the abstract semantic for the absolute errors.
+ * A narrow with the calculation <Approx - Exact> is done during the
+ * forward operations *)
+module Abs_Err_Sem : Semantic =
struct
let neg v = I.neg v.abs_err
- let sqrt v = I.sub (Approx_Semantic.sqrt v) (Exact_Semantic.sqrt v)
+ let sqrt v =
+ let approx = Approx_Sem.sqrt v in
+ let exact = Exact_Sem.sqrt v in
+ match approx, exact with
+ | `Value x, `Value y -> `Value (I.sub x y)
+ | _, _ -> `Bottom
let add x y =
let abs_err = I.add x.abs_err y.abs_err in
let approx = I.add x.approx y.approx in
- I.add abs_err (I.mul approx R.noise)
+ I.add abs_err (I.mul approx Cst.e_interval)
let sub x y =
let abs_err = I.sub x.abs_err y.abs_err in
let approx = I.sub x.approx y.approx in
- I.add abs_err (I.mul approx R.noise)
+ I.add abs_err (I.mul approx Cst.e_interval)
let mul x y =
- let mul = I.mul (I.mul x.approx y.approx) R.noise in
+ let mul = I.mul (I.mul x.approx y.approx) Cst.e_interval in
let xey = I.mul x.exact y.abs_err in
let yex = I.mul y.exact x.abs_err in
let exy = I.mul x.abs_err y.abs_err in
I.add (I.add mul (I.add xey yex)) exy
let div x y =
- Format.printf "Input :@. x = @[%a@]@. y = @[%a@]@."
- pretty x pretty y ;
let xyapprox = I.div x.approx y.approx in
- Format.printf "Approx of (x/y) = %a@." I.pretty xyapprox ;
let xyexact = I.div x.exact y.exact in
- Format.printf "Exact of (x/y) = %a@." I.pretty xyexact ;
- let mul = I.mul xyapprox R.stderr in
- Format.printf "With stderr : %a@." I.pretty mul ;
- let r = I.sub mul xyexact in
- Format.printf "Result : %a@." I.pretty r ; r
- (*
- let ey = I.mul (I.div x.exact y.exact) y.abs_err in
- Format.printf "(x/y)*E(y) : %a@." I.pretty ey ;
- let xe = I.mul x.approx R.noise in
- Format.printf "P(x)*e : %a@." I.pretty xe ;
- let tmp = I.add (I.sub x.approx ey) xe in
- Format.printf "Numerator : %a@." I.pretty tmp ;
- let r = I.div (I.add (I.sub x.approx ey) xe) y.approx in
- Format.printf "Result : %a@." I.pretty r ; r
- *)
+ match xyapprox, xyexact with
+ | `Value ap, `Value ex -> `Value (I.sub (I.mul ap Cst.std_error) ex)
+ | _, _ -> `Bottom
end
-module Rel_Err_Semantic : Semantic =
+(* Implementation of the abstract semantic for the relative errors.
+ * A narrow with the calculation <(Approx - Exact) / Exact> is done
+ * during the forward operations *)
+module Rel_Err_Sem : Semantic =
struct
let neg v = I.neg v.rel_err
let sqrt v =
- I.sub (I.mul (I.sqrt (I.add v.rel_err R.one)) R.stderr) R.one
+ let f s = I.sub (I.mul s Cst.std_error) Cst.one_interval in
+ (I.sqrt (I.add v.rel_err Cst.one_interval)) >>-: f
let add x y =
- let d = max (I.max_abs x.rel_err) (I.max_abs y.rel_err) in
- let num = R.add (I.max_abs x.exact) (I.max_abs y.exact) in
+ let d = F.max (I.max_abs x.rel_err) (I.max_abs y.rel_err) in
+ let num = F.add (I.max_abs x.exact) (I.max_abs y.exact) in
let den = I.min_abs (I.add x.exact y.exact) in
- let eps = R.add 1.0 R.em in
- let v = R.add (R.mul (R.mul (R.div num den) d) eps) R.em in
- (R.neg v, v)
+ let eps = F.add (F.of_float Precisions.Real 1.0) Cst.e in
+ let v = F.add (F.mul (F.mul (F.div num den) d) eps) Cst.e in
+ (F.neg ~rnd:Mpfr.Down v, v)
let sub x y =
- let d = max (I.max_abs x.rel_err) (I.max_abs y.rel_err) in
- let num = R.add (I.max_abs x.exact) (I.max_abs y.exact) in
+ let d = F.max (I.max_abs x.rel_err) (I.max_abs y.rel_err) in
+ let num = F.add (I.max_abs x.exact) (I.max_abs y.exact) in
let den = I.min_abs (I.sub x.exact y.exact) in
- let eps = R.add 1.0 R.em in
- let v = R.add (R.mul (R.mul (R.div num den) d) eps) R.em in
- (R.neg v, v)
+ let eps = F.add (F.of_float Precisions.Real 1.0) Cst.e in
+ let v = F.add (F.mul (F.mul (F.div num den) d) eps) Cst.e in
+ (F.neg ~rnd:Mpfr.Down v, v)
let mul x y =
- let ex = I.add R.one x.rel_err in
- let ey = I.add R.one y.rel_err in
- I.sub (I.mul (I.mul ex ey) R.stderr) R.one
+ let ex = I.add Cst.one_interval x.rel_err in
+ let ey = I.add Cst.one_interval y.rel_err in
+ I.sub (I.mul (I.mul ex ey) Cst.std_error) Cst.one_interval
let div x y =
- let ex = I.add R.one x.rel_err in
- let ey = I.add R.one y.rel_err in
- I.sub (I.mul (I.div ex ey) R.stderr) R.one
+ let ex = I.add Cst.one_interval x.rel_err in
+ let ey = I.add Cst.one_interval y.rel_err in
+ let f d = I.sub (I.mul d Cst.std_error) Cst.one_interval in
+ (I.div ex ey) >>-: f
end
-(* Forward operations *)
+(*-----------------------------------------------------------------------------
+ * Operations on abstract values
+ *---------------------------------------------------------------------------*)
let return v = `Value v, Alarmset.all
let constant _ = function
- | CReal (r, _, _) ->
- { exact = (r, r)
- ; approx = (r, r)
- ; abs_err = I.zero
- ; rel_err = I.zero
- }
+ | CReal (r, fkind, opt) ->
+ let prec = match fkind with
+ | FFloat -> Precisions.Simple
+ | FDouble -> Precisions.Double
+ | FLongDouble -> Precisions.Long_Double
+ in
+ let exact = match opt with
+ | Some s -> I.of_strings Precisions.Real (s, s)
+ | None -> I.of_floats Precisions.Real (r, r)
+ in
+ { exact ; approx = I.of_floats prec (r, r)
+ ; abs_err = I.zero ; rel_err = I.zero
+ }
| _ -> top
-let forward_unop ~context:_ _ op v =
- match op with
+(* Forward operations *)
+let forward_unop ~context:_ _ op v = match op with
| Neg ->
- let v =
- { exact = Exact_Semantic.neg v
- ; approx = Approx_Semantic.neg v
- ; abs_err = Abs_Err_Semantic.neg v
- ; rel_err = Rel_Err_Semantic.neg v
- }
- in return v
- | _ -> return top
+ let exact , approx = Exact_Sem.neg v, Approx_Sem.neg v in
+ let abs_err, rel_err = Abs_Err_Sem.neg v, Rel_Err_Sem.neg v in
+ return { exact ; approx ; abs_err ; rel_err }
+ | LNot | BNot -> return top
let forward_binop ~context:_ _ op x y =
+ let calculate_errors exact approx prg_abs prg_rel =
+ let cal_abs = I.sub approx exact in
+ let cal_rel = I.div cal_abs exact in
+ let abs_err = match I.narrow prg_abs cal_abs with
+ | `Value v -> v | `Bottom -> prg_abs
+ in
+ let rel_err = match cal_rel >>- (I.narrow prg_rel) with
+ | `Value v -> v | `Bottom -> prg_rel
+ in
+ return { exact ; approx ; abs_err ; rel_err }
+ in
match op with
| PlusA ->
- let v =
- { exact = Exact_Semantic.add x y
- ; approx = Approx_Semantic.add x y
- ; abs_err = Abs_Err_Semantic.add x y
- ; rel_err = Rel_Err_Semantic.add x y
- }
- in return v
+ let exact , approx = Exact_Sem.add x y, Approx_Sem.add x y in
+ let prg_abs, prg_rel = Abs_Err_Sem.add x y, Rel_Err_Sem.add x y in
+ calculate_errors exact approx prg_abs prg_rel
| MinusA ->
- let v =
- { exact = Exact_Semantic.sub x y
- ; approx = Approx_Semantic.sub x y
- ; abs_err = Abs_Err_Semantic.sub x y
- ; rel_err = Rel_Err_Semantic.sub x y
- }
- in return v
+ let exact , approx = Exact_Sem.sub x y, Approx_Sem.sub x y in
+ let prg_abs, prg_rel = Abs_Err_Sem.sub x y, Rel_Err_Sem.sub x y in
+ calculate_errors exact approx prg_abs prg_rel
| Mult ->
- let v =
- { exact = Exact_Semantic.mul x y
- ; approx = Approx_Semantic.mul x y
- ; abs_err = Abs_Err_Semantic.mul x y
- ; rel_err = Rel_Err_Semantic.mul x y
- }
- in return v
+ let exact , approx = Exact_Sem.mul x y, Approx_Sem.mul x y in
+ let prg_abs, prg_rel = Abs_Err_Sem.mul x y, Rel_Err_Sem.mul x y in
+ calculate_errors exact approx prg_abs prg_rel
| Div ->
- let v =
- { exact = Exact_Semantic.div x y
- ; approx = Approx_Semantic.div x y
- ; abs_err = Abs_Err_Semantic.div x y
- ; rel_err = Rel_Err_Semantic.div x y
- }
- in return v
+ let exact_b , approx_b = Exact_Sem.div x y, Approx_Sem.div x y in
+ let prg_abs_b, prg_rel_b = Abs_Err_Sem.div x y, Rel_Err_Sem.div x y in
+ let res = match exact_b, approx_b, prg_abs_b, prg_rel_b with
+ | `Value exact, `Value approx, `Value prg_abs, `Value prg_rel ->
+ calculate_errors exact approx prg_abs prg_rel
+ | _, _, _, _ -> `Bottom, Alarmset.all
+ in res
| _ -> return top
-
(* Backward operations *)
let backward_binop ~input_type:_ ~resulting_type:_ op
~left:_ ~right:_ ~result:_ =
@@ -417,7 +521,6 @@ let backward_binop ~input_type:_ ~resulting_type:_ op
let backward_unop ~typ_arg:_ _ ~arg:_ ~res:_ = `Value None
let backward_cast ~src_typ:_ ~dst_typ:_ ~src_val:_ ~dst_val:_ = `Value None
-
(* Reinterpret and Cast *)
let truncate_integer _ _ _ = return top
let rewrap_integer _ _ = top
@@ -425,8 +528,6 @@ let restrict_float ~remove_infinite:_ _ _ t = return t
let cast ~src_typ:_ ~dst_typ:_ _ _ = return top
let resolve_functions _ = `Top, true
-
(* Misc *)
let error_key = Structure.Key_Value.create_key "error_values"
let structure = Structure.Key_Value.Leaf error_key
-