[Eva] Numerors domain registration.

Makefile

@@ -832,32 +832,18 @@ endif
 NUMERORS_FILES:= \
 	values/numerors/numerors_utils values/numerors/numerors_float \
 	values/numerors/numerors_interval values/numerors/numerors_arithmetics \
-	values/numerors/numerors_value
+	values/numerors/numerors_value domains/numerors/numerors_domain
 
 ifeq ($(HAS_MPFR),yes)
 PLUGIN_REQUIRES+= gmp
 PLUGIN_TESTS_DIRS+=value/numerors
 NUMERORS_CMO:= $(NUMERORS_FILES)
-src/plugins/value/domains/numerors/numerors_domain.ml: \
-		src/plugins/value/domains/numerors/numerors_domain.ok.ml \
-		share/Makefile.config
-	$(CP_IF_DIFF) $< $@
-	$(CHMOD_RO) $@
 else
 # Do not compile numerors files, but include them in the distributed files.
 NUMERORS_CMO:=
 PLUGIN_DISTRIB_EXTERNAL+= $(addsuffix .ml,$(NUMERORS_FILES))
 PLUGIN_DISTRIB_EXTERNAL+= $(addsuffix .mli,$(NUMERORS_FILES))
-src/plugins/value/domains/numerors/numerors_domain.ml: \
-		src/plugins/value/domains/numerors/numerors_domain.ko.ml \
-		share/Makefile.config
-	$(CP_IF_DIFF) $< $@
-	$(CHMOD_RO) $@
 endif
-PLUGIN_GENERATED+= src/plugins/value/domains/numerors/numerors_domain.ml
-PLUGIN_DISTRIB_EXTERNAL+= \
-	domains/numerors/numerors_domain.ok.ml \
-	domains/numerors/numerors_domain.ko.ml
 
 # General rules for ordering files within PLUGIN_CMO:
 # - try to keep the legacy Value before Eva
@@ -886,7 +872,6 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
 	domains/offsm_domain \
 	domains/symbolic_locs \
 	domains/sign_domain \
-	$(NUMERORS_CMO) domains/numerors/numerors_domain \
 	domains/cvalue/warn domains/cvalue/locals_scoping \
 	domains/cvalue/cvalue_offsetmap \
 	utils/value_results \
@@ -909,7 +894,7 @@ PLUGIN_CMO:= slevel/split_strategy value_parameters \
 	engine/iterator \
 	engine/initialization \
 	engine/compute_functions engine/analysis register \
-	$(APRON_CMO)
+	$(APRON_CMO) $(NUMERORS_CMO)
 PLUGIN_CMI:= values/abstract_value values/abstract_location \
 	domains/abstract_domain domains/simpler_domains
 PLUGIN_DEPENDENCIES:=Callgraph LoopAnalysis RteGen

src/plugins/value/domains/numerors/numerors_domain.ko.ml

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of Frama-C.                                         *)
-(*                                                                        *)
-(*  Copyright (C) 2007-2019                                               *)
-(*    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).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-#24 "src/plugins/value/domains/numerors/numerors_domain.ko.ml"
-
-type value
-type location = Precise_locs.precise_location
-let value_key = Structure.Key_Value.create_key "dummy_numerors_values"
-
-let ok = false
-
-let abort () =
-  Value_parameters.abort
-    "The numerors domain has been requested but is not available, as Frama-C \
-     did not found the MPFR library. The analysis is aborted."
-
-let add_numerors_value _ = abort ()
-let numerors_domain = abort
-
-let reduce_error _ = fun v -> v

src/plugins/value/domains/numerors/numerors_domain.ok.ml → src/plugins/value/domains/numerors/numerors_domain.ml

@@ -20,17 +20,10 @@
 (*                                                                        *)
 (**************************************************************************)
 
-#24 "src/plugins/value/domains/numerors/numerors_domain.ok.ml"
-
 open Eval
 open Cil_types
 
-type value = Numerors_value.t
-type location = Precise_locs.precise_location
-let value_key = Numerors_value.key
-
-let ok = true
-
+(* The numerors values, plus some builtin functions. *)
 module Numerors_Value = struct
   include Numerors_value
 
@@ -87,65 +80,7 @@ module Numerors_Value = struct
     ]
 end
 
-let add_numerors_value (module Value: Abstract.Value.Internal) =
-  let module External_Value = Structure.Open (Abstract.Value) (Value) in
-  let module V = struct
-    include Value_product.Make (Value) (Numerors_value)
-
-    let structure =
-      Abstract.Value.(Node (Value.structure,
-                            Leaf (Numerors_value.key, (module Numerors_value))))
-
-    let forward_cast = match External_Value.get Main_values.CVal.key with
-      | None -> forward_cast
-      | Some get_cvalue ->
-        fun ~src_type ~dst_type (value, num) ->
-          forward_cast ~src_type ~dst_type (value, num) >>-: fun (value', num) ->
-          let num = match src_type, dst_type with
-            | Eval_typ.TSInt _, Eval_typ.TSFloat fkind ->
-              begin
-                try
-                  let cvalue = get_cvalue value in
-                  let ival = Cvalue.V.project_ival cvalue in
-                  match Ival.min_and_max ival with
-                  | Some min, Some max ->
-                    let min, max = Integer.to_int min, Integer.to_int max in
-                    let prec = Numerors_utils.Precisions.of_fkind fkind in
-                    Numerors_value.of_ints ~prec min max
-                  | _, _ -> num
-                (* Integer.to_int may fail for too big integers. *)
-                with Cvalue.V.Not_based_on_null | Z.Overflow -> num
-              end
-            | _, _ -> num
-          in
-          value', num
-  end in
-  (module V: Abstract.Value.Internal)
-
-let reduce_error (type v) (module V: Abstract.Value.External with type t = v) =
-  match V.get Numerors_value.key, V.get Main_values.CVal.key with
-  | Some get_error, Some get_cvalue ->
-    begin
-      let set_error = V.set Numerors_value.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 = Numerors_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
-
-
+(* The numerors domain: a simple memory over the numerors value. *)
 module Domain = struct
   module Name = struct let name = "numerors" end
   include Simple_memory.Make_Domain (Name) (Numerors_Value)
@@ -161,7 +96,71 @@ module Domain = struct
     | _, _ -> ()
 end
 
-let numerors_domain () =
-  Value_parameters.warning "The numerors domain is experimental.";
-  (module Domain: Abstract_domain.Leaf with type value = value
-                                        and type location = location)
+(* Reduced product between the cvalue values and the numerors values. *)
+let reduce_error cvalue error =
+  try
+    let ival = Cvalue.V.project_ival cvalue in
+    match ival with
+    | Ival.Float fval ->
+      begin
+        match Numerors_value.reduce fval error with
+        | `Value error -> cvalue, error
+        | `Bottom -> cvalue, error (* TODO: we should be able to reduce to bottom. *)
+      end
+    | _ -> cvalue, error
+  with Cvalue.V.Not_based_on_null -> cvalue, error
+
+(* Reduction of the numerors value resulting from a cast from int to float type,
+   using the cvalue component of value abstractions. *)
+let reduce_cast (module Abstract: Abstractions.S) =
+  let module Val = struct
+    include Abstract.Val
+
+    (* Redefines the [forward_cast] function of the value component. *)
+    let forward_cast =
+      (* If cvalue or numerors do not belong to the abstraction, no reduction:
+         the [forward_cast] function is unchanged. *)
+      match get Main_values.CVal.key, mem Numerors_value.key with
+      | None, _ | _, false -> forward_cast
+      | Some get_cvalue, true ->
+        (* Otherwise, applies the [forward_cast] function, but updates the
+           numerors component of the result. *)
+        fun ~src_type ~dst_type value ->
+          forward_cast ~src_type ~dst_type value >>-: fun result ->
+          match src_type, dst_type with
+          | Eval_typ.TSInt _, Eval_typ.TSFloat fkind ->
+            begin
+              try
+                let cvalue = get_cvalue value in
+                let ival = Cvalue.V.project_ival cvalue in
+                match Ival.min_and_max ival with
+                | Some min, Some max ->
+                  let min, max = Integer.to_int min, Integer.to_int max in
+                  let prec = Numerors_utils.Precisions.of_fkind fkind in
+                  let num = Numerors_value.of_ints ~prec min max in
+                  set Numerors_value.key num result
+                | _, _ -> result
+              (* Integer.to_int may fail for too big integers. *)
+              with Cvalue.V.Not_based_on_null | Z.Overflow -> result
+            end
+          | _, _ -> result
+  end in
+  (module struct
+    module Val = Val
+    module Loc = Abstract.Loc
+    module Dom = Abstract.Dom
+  end: Abstractions.S)
+
+(* Register the domain as an Eva abstractions. *)
+let () =
+  let open Abstractions in
+  let domain =
+    { name = "numerors";
+      values = Single (module Numerors_value);
+      domain = Domain (module Domain); }
+  in
+  let reduced_product = Main_values.CVal.key, Numerors_value.key, reduce_error in
+  register ~enable:Value_parameters.NumerorsDomain.get domain;
+  register_value_reduction reduced_product;
+  register_hook reduce_cast;
+  Value_parameters.register_numerors ()

src/plugins/value/domains/numerors/numerors_domain.mli

@@ -20,30 +20,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type value
-type location = Precise_locs.precise_location
-val value_key : value Structure.Key_Value.key
-
-(** True if the numerors domain is available;
-    False if the MPFR library has not been found. *)
-val ok: bool
-
-(** Functions used by the engine to build numerors abstractions. *)
-
-(** Builds the product between a given value module and the numerors value
-    module. If the given value module contains Cvalue, uses cvalues to reduce
-    numerors values on casts from integer to floating-point values.
-    Fails if numerors domain is not available.  *)
-val add_numerors_value:
-  (module Abstract.Value.Internal) -> (module Abstract.Value.Internal)
-
-(* From a given abstract value product, creates the reduction function that
-   reduces numerors values by using cvalues. Returns the identity if the given
-   value product does not contain numerors and cvalue componants. *)
-val reduce_error:
-  (module Abstract.Value.External with type t = 'v) -> ('v -> 'v)
-
-(** Returns the numerors domain module, if available. Fails otherwise. *)
-val numerors_domain:
-  unit -> (module Abstract_domain.Leaf with type value = value
-                                        and type location = location)
+(** Numerors domain: computes over-approximations of the rounding errors bounds
+    of floating-point computations.
+    Nothing is exported: the domain is registered as an analysis abstraction
+    in the Eva engine, enabled by the -eva-numerors-domain option. *)

src/plugins/value/value_parameters.ml

@@ -174,6 +174,18 @@ module BitwiseOffsmDomain = Domain_Parameter
       let default = false
     end)
 
+let numerors_available = ref false
+let register_numerors () = numerors_available := true
+
+let numerors_hook _ _ =
+  if not !numerors_available
+  then
+    abort
+      "The numerors domain has been requested but is not available,@ \
+       as Frama-C did not found the MPFR library. The analysis is aborted."
+  else if not (is_debug_key_enabled dkey_experimental) then
+    warning  "The numerors domain is experimental.";
+
 module NumerorsDomain = Domain_Parameter
     (struct
       let option_name = "-eva-numerors-domain"
@@ -182,6 +194,7 @@ module NumerorsDomain = Domain_Parameter
                   computations"
       let default = false
     end)
+let () = NumerorsDomain.add_set_hook numerors_hook
 
 let apron_help = "Experimental binding of the numerical domains provided \
                   by the APRON library: http://apron.cri.ensmp.fr/library \n"

src/plugins/value/value_parameters.mli

@@ -237,6 +237,9 @@ val dkey_widening : category
 (** Notifies that the binding to Apron domains is available. *)
 val register_apron: unit -> unit
 
+(** Notifies that the numerors domain is available. *)
+val register_numerors: unit -> unit
+
 (*
 Local Variables:
 compile-command: "make -C ../../.."