From 9a5a3ec37e903a7f9ebb4c66684a7f4b80ac2410 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Fri, 23 Aug 2019 18:05:13 +0200
Subject: [PATCH] [Eva] Numerors domain registration.
---
Makefile | 19 +--
.../domains/numerors/numerors_domain.ko.ml | 39 -----
...merors_domain.ok.ml => numerors_domain.ml} | 141 +++++++++---------
.../domains/numerors/numerors_domain.mli | 31 +---
src/plugins/value/value_parameters.ml | 13 ++
src/plugins/value/value_parameters.mli | 3 +
6 files changed, 92 insertions(+), 154 deletions(-)
delete mode 100644 src/plugins/value/domains/numerors/numerors_domain.ko.ml
rename src/plugins/value/domains/numerors/{numerors_domain.ok.ml => numerors_domain.ml} (57%)
diff --git a/Makefile b/Makefile
index c475e1a48da..a4ba43c60ea 100644
--- a/Makefile
+++ b/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
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ko.ml b/src/plugins/value/domains/numerors/numerors_domain.ko.ml
deleted file mode 100644
index eb6bc8b9a4f..00000000000
--- a/src/plugins/value/domains/numerors/numerors_domain.ko.ml
+++ /dev/null
@@ -1,39 +0,0 @@
-(**************************************************************************)
-(* *)
-(* 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
diff --git a/src/plugins/value/domains/numerors/numerors_domain.ok.ml b/src/plugins/value/domains/numerors/numerors_domain.ml
similarity index 57%
rename from src/plugins/value/domains/numerors/numerors_domain.ok.ml
rename to src/plugins/value/domains/numerors/numerors_domain.ml
index 0837c354d0f..338214a370c 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.ok.ml
+++ b/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 ()
diff --git a/src/plugins/value/domains/numerors/numerors_domain.mli b/src/plugins/value/domains/numerors/numerors_domain.mli
index c00510fa309..6fcd35b31ee 100644
--- a/src/plugins/value/domains/numerors/numerors_domain.mli
+++ b/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. *)
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index ccd4fa66c36..1de1430a7c1 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/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"
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 22a72b258e9..3e0fb860496 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/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 ../../.."
--
GitLab