[Eva] Numerors: add optionnal dependency on MPFR

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

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)

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@
 

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 =

src/plugins/value/values/errors_value.ko.ml

+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

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

src/plugins/value/values/errors_value.ml → 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