From dfce4733d9caf171e1846ad3563e860b27a7fca7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 5 Dec 2017 17:44:06 +0100
Subject: [PATCH] [Eva] Numerors: add optionnal dependency on MPFR
---
Makefile | 16 ++
configure.in | 15 ++
share/Makefile.config.in | 3 +
src/plugins/value/engine/abstractions.ml | 26 ++-
src/plugins/value/values/errors_value.ko.ml | 45 ++++++
src/plugins/value/values/errors_value.mli | 3 +
.../{errors_value.ml => errors_value.ok.ml} | 151 +++++++++++-------
7 files changed, 198 insertions(+), 61 deletions(-)
create mode 100644 src/plugins/value/values/errors_value.ko.ml
rename src/plugins/value/values/{errors_value.ml => errors_value.ok.ml} (83%)
mode change 100644 => 100755
diff --git a/Makefile b/Makefile
index 047e9585655..7250c1a8197 100644
--- a/Makefile
+++ b/Makefile
@@ -824,6 +824,22 @@ endif
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
+src/plugins/value/values/errors_value.ml: \
+ src/plugins/value/values/errors_value.ok.ml share/Makefile.config
+ $(CP_IF_DIFF) $< $@
+ $(CHMOD_RO) $@
+else
+PLUGIN_REQUIRES:=
+src/plugins/value/values/errors_value.ml: \
+ src/plugins/value/values/errors_value.ko.ml share/Makefile.config
+ $(CP_IF_DIFF) $< $@
+ $(CHMOD_RO) $@
+endif
+GENERATED += src/plugins/value/values.errors_value.ml
+PLUGIN_DISTRIB_EXTERNAL:=values/errors_value.ok.ml values/errors_value.ko.ml
+
# These files are used by the GUI, but do not depend on Lablgtk
VALUE_GUI_AUX:=gui_files/gui_types gui_files/gui_eval \
gui_files/gui_callstacks_filters
diff --git a/configure.in b/configure.in
index 18e1a3af1b2..3b2520fbf19 100644
--- a/configure.in
+++ b/configure.in
@@ -367,6 +367,20 @@ else
AC_MSG_RESULT(not found. The corresponding domains won't be available in Eva)
fi;
+# mpfr
+#######
+
+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
+ HAS_MPFR="yes";
+ AC_MSG_RESULT(found)
+else
+ HAS_MPFR="no";
+ AC_MSG_RESULT(not found. The numeric error domain won't be available in Eva)
+fi;
+
# landmarks (profiling tool, for developers)
########
@@ -975,6 +989,7 @@ AC_SUBST(DOT)
AC_SUBST(HAS_DOT)
AC_SUBST(HAS_YOJSON)
AC_SUBST(HAS_APRON)
+AC_SUBST(HAS_MPFR)
AC_SUBST(HAS_LANDMARKS)
AC_SUBST(OCAMLBEST)
AC_SUBST(OCAMLVERSION)
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index e15ae74ad6d..993b677842a 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -115,6 +115,9 @@ HAS_YOJSON ?=@HAS_YOJSON@
# apron
HAS_APRON ?=@HAS_APRON@
+# mpfr
+HAS_MPFR ?=@HAS_MPFR@
+
# landmarks
HAS_LANDMARKS ?=@HAS_LANDMARKS@
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 6cd456aa81e..343e4a9baf9 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -507,7 +507,7 @@ module Reduce (Value : Abstract_value.External) = struct
component (coming currently from an Apron domain), reduce them from each
other. If the Cvalue is not a scalar do nothing, because we do not
currently use Apron for pointer offsets. *)
- let reduce =
+ let reduce_apron_itv =
match Value.get Main_values.interval_key, Value.get Main_values.cvalue_key with
| Some get_interval, Some get_cvalue ->
begin
@@ -536,6 +536,30 @@ module Reduce (Value : Abstract_value.External) = struct
end
| _, _ -> fun x -> x
+ let reduce_error =
+ match Value.get Errors_value.error_key, Value.get Main_values.cvalue_key with
+ | Some get_error, Some get_cvalue ->
+ begin
+ let set_error = Value.set Errors_value.error_key in
+ fun t ->
+ let cvalue = get_cvalue t in
+ try
+ let ival = Cvalue.V.project_ival cvalue in
+ match ival with
+ | Ival.Float fval ->
+ begin
+ let error = get_error t in
+ let error = Errors_value.reduce fval error in
+ match error with
+ | `Value error -> set_error error t
+ | `Bottom -> t (* TODO: we should be able to reduce to bottom. *)
+ end
+ | _ -> t
+ with Cvalue.V.Not_based_on_null -> t
+ end
+ | _, _ -> fun x -> x
+
+ let reduce t = reduce_apron_itv (reduce_error t)
end
let open_abstractions abstraction =
diff --git a/src/plugins/value/values/errors_value.ko.ml b/src/plugins/value/values/errors_value.ko.ml
new file mode 100644
index 00000000000..1af8ac32f04
--- /dev/null
+++ b/src/plugins/value/values/errors_value.ko.ml
@@ -0,0 +1,45 @@
+module T =
+ struct
+ type t = unit
+ include Datatype.Serializable_undefined
+ let compare () () = 0
+ let equal () () = true
+ let hash = Hashtbl.hash
+ let reprs = [()]
+ let name = "Value.Unit_value"
+ let pretty fmt () = Format.fprintf fmt "()"
+ end
+include Datatype.Make(T)
+
+let pretty_debug = pretty
+let pretty_typ _ = pretty
+
+let top = ()
+let is_included () () = true
+let join () () = ()
+let narrow () () = `Value ()
+
+let zero = ()
+let float_zeros = ()
+let top_int = ()
+let inject_int _ _ = ()
+let inject_address _ = ()
+
+let constant _ _ = ()
+let forward_unop ~context:_ _ _ () = `Value (), Alarmset.all
+let forward_binop ~context:_ _ _ () () = `Value (), Alarmset.all
+let backward_binop
+ ~input_type:_ ~resulting_type:_ _
+ ~left:() ~right:() ~result:()
+ = `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
+
+let truncate_integer _ _ () = `Value (), Alarmset.all
+let rewrap_integer _ () = ()
+let restrict_float ~remove_infinite:_ _ _ () = `Value (), Alarmset.all
+let cast ~src_typ:_ ~dst_typ:_ _ () = `Value (), Alarmset.all
+let resolve_functions () = `Top, true
+
+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.mli b/src/plugins/value/values/errors_value.mli
index fe27811f6f7..43f421915b1 100644
--- a/src/plugins/value/values/errors_value.mli
+++ b/src/plugins/value/values/errors_value.mli
@@ -24,4 +24,7 @@ include Abstract_value.Internal
val pretty_debug : t Pretty_utils.formatter
+(* Reduction of an error value according to a floating-point interval. *)
+val reduce: Fval.t -> t -> t Eval.or_bottom
+
val error_key : t Structure.Key_Value.k
diff --git a/src/plugins/value/values/errors_value.ml b/src/plugins/value/values/errors_value.ok.ml
old mode 100644
new mode 100755
similarity index 83%
rename from src/plugins/value/values/errors_value.ml
rename to src/plugins/value/values/errors_value.ok.ml
index 2da8236496a..bdf88f2fbfd
--- a/src/plugins/value/values/errors_value.ml
+++ b/src/plugins/value/values/errors_value.ok.ml
@@ -25,6 +25,8 @@ open Eval
open Abstract_interp
+(* module M = Mpfr *)
+
(*-----------------------------------------------------------------------------
* Generic intervals implementation
@@ -76,17 +78,17 @@ module Interval =
type elt = Elt.t
type t = elt * elt
let top = Elt.minimal_value, Elt.maximal_value
- let zero = Elt.zero, Elt.zero
+ 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 (_, y as a) (x', _ as b) =
- if compare a top = 0 then `Value b
- else if compare b top = 0 then `Value a
- else if Elt.pord x' y then `Value (x', y) else `Bottom
+ 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'
@@ -115,7 +117,7 @@ module R =
struct
type t = float
let zero = 0.0
- let minimal_value = min_float
+ let minimal_value = -. max_float
let maximal_value = max_float
let pord = ( <= )
let compare = Pervasives.compare
@@ -181,6 +183,50 @@ let narrow x y =
`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
+ 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
+ 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
@@ -244,47 +290,61 @@ module Abs_Err_Semantic : Semantic =
let approx = I.sub x.approx y.approx in
I.add abs_err (I.mul approx R.noise)
let mul x y =
- let d = max (I.max_abs x.abs_err) (I.max_abs y.abs_err) in
- let d2 = R.mul d d in
- let r = R.add (I.max_abs x.exact) (I.max_abs y.exact) in
- let f = R.mul (I.max_abs x.approx) (I.max_abs y.approx) in
- let v = R.add (R.add (R.mul f R.em) (R.mul r d)) d2 in
- (R.neg v, v)
- let div x y =
- let rx = I.max_abs x.exact in
- let ry = I.max_abs y.exact in
- let ex = I.max_abs x.abs_err in
- let ey = I.max_abs y.abs_err in
- let v = R.add (R.div (R.add rx ex) (R.add ry ey)) (R.div rx ry) in
- (R.neg v, v)
+ let mul = I.mul (I.mul x.approx y.approx) R.noise 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
+ *)
end
module Rel_Err_Semantic : 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.noise) R.one
+ let sqrt v =
+ I.sub (I.mul (I.sqrt (I.add v.rel_err R.one)) R.stderr) R.one
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 den = I.min_abs (I.add x.exact y.exact) in
let eps = R.add 1.0 R.em in
- let v = R.sub (R.mul (R.mul (R.div num den) d) eps) 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 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 den = I.min_abs (I.sub x.exact y.exact) in
let eps = R.add 1.0 R.em in
- let v = R.sub (R.mul (R.mul (R.div num den) d) eps) 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 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.noise) R.one
+ I.sub (I.mul (I.mul ex ey) R.stderr) R.one
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.noise) R.one
+ I.sub (I.mul (I.div ex ey) R.stderr) R.one
end
@@ -303,9 +363,13 @@ let constant _ = function
let forward_unop ~context:_ _ op v =
match op with
| Neg ->
- let x, y = v.exact in
- let x', y' = v.approx in
- return { v with exact = (-.x, -.y) ; approx = (-.x', -.y') }
+ 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 forward_binop ~context:_ _ op x y =
@@ -366,36 +430,3 @@ let resolve_functions _ = `Top, true
let error_key = Structure.Key_Value.create_key "error_values"
let structure = Structure.Key_Value.Leaf error_key
-(* Associated Datatype *)
-module T =
- struct
- type t = err
- include Datatype.Serializable_undefined
- 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@\nApprox : %a@\n Abs Err : %a@\n Rel Err : %a@\n"
- 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
--
GitLab