From e3e579af48ea179246d365db612e14be80ca060e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Tue, 11 Feb 2020 11:26:23 +0100
Subject: [PATCH] [Eva] New option -eva-domains that enables a list of domains.
---
src/plugins/value/engine/abstractions.ml | 7 ++--
src/plugins/value/engine/abstractions.mli | 5 +--
src/plugins/value/value_parameters.ml | 42 ++++++++++++++++++++++-
src/plugins/value/value_parameters.mli | 4 +++
4 files changed, 53 insertions(+), 5 deletions(-)
diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml
index 5e73c7d1374..0e06c7ac408 100644
--- a/src/plugins/value/engine/abstractions.ml
+++ b/src/plugins/value/engine/abstractions.ml
@@ -66,14 +66,17 @@ module Config = struct
let dynamic_abstractions : dynamic list ref = ref []
let register ~enable abstraction =
+ Value_parameters.register_domain abstraction.name;
abstractions := (enable, Flag abstraction) :: !abstractions
let dynamic_register ~configure ~make =
dynamic_abstractions := Dynamic (configure, make) :: !dynamic_abstractions
let configure () =
- let aux config (enable, flag) =
- if enable () then add flag config else config
+ let aux config (enable, (Flag domain as flag)) =
+ if enable () || Value_parameters.Domains.mem domain.name
+ then add flag config
+ else config
in
let config = List.fold_left aux empty !abstractions in
let aux config (Dynamic (configure, make)) =
diff --git a/src/plugins/value/engine/abstractions.mli b/src/plugins/value/engine/abstractions.mli
index 3d4ebe9e437..a29aed97b43 100644
--- a/src/plugins/value/engine/abstractions.mli
+++ b/src/plugins/value/engine/abstractions.mli
@@ -68,8 +68,9 @@ type 'v abstraction =
domain: 'v domain; (** The domain over the value abstraction. *)
}
-(** Register an abstraction. The abstraction is used in an Eva analysis only if
- [enable ()] returns true at the start of the analysis. *)
+(** Register an abstraction. The abstraction is used in an Eva analysis if
+ [enable ()] returns true at the start of the analysis, or if -eva-domains
+ has been set to the name of the abstraction. *)
val register: enable:(unit -> bool) -> 'v abstraction -> unit
(** Register a dynamic abstraction: the abstraction is built by applying
diff --git a/src/plugins/value/value_parameters.ml b/src/plugins/value/value_parameters.ml
index 8a3c6adf265..1e839e5afd1 100644
--- a/src/plugins/value/value_parameters.ml
+++ b/src/plugins/value/value_parameters.ml
@@ -124,8 +124,48 @@ let malloc = add_group "Dynamic allocation"
(* --- Eva domains --- *)
(* -------------------------------------------------------------------------- *)
+let () = Parameter_customize.set_group domains
+module Domains =
+ String_set
+ (struct
+ let option_name = "-eva-domains"
+ let arg_name = "d1,...,dn"
+ let help = "Enable a list of analysis domains."
+ end)
+let () = add_precision_dep Domains.parameter
+
+(* List of available domains. *)
+let domains_ref = ref []
+
+(* Help message for the -eva-domains option, with the list of currently
+ available domains. *)
+let domains_help () =
+ let pp_str_list = Pretty_utils.pp_list ~sep:", " Format.pp_print_string in
+ Format.asprintf
+ "Enable a list of analysis domains. Available domains are: %a"
+ pp_str_list (List.rev !domains_ref)
+
+(* Registers a new domain. Updates the help message of -eva-domains. *)
+let register_domain name =
+ Cmdline.replace_option_help
+ Domains.option_name "eva" domains (domains_help ());
+ domains_ref := name :: !domains_ref
+
+(* Checks that a domain has been registered. *)
+let check_domain domain =
+ if not (List.mem domain !domains_ref)
+ then
+ let pp_str_list = Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string in
+ abort "invalid domain %S for option -eva-domains.@.Possible domains are: %a"
+ domain pp_str_list (List.rev !domains_ref)
+
+let () =
+ Domains.add_set_hook
+ (fun _old domains -> Datatype.String.Set.iter check_domain domains)
+
(* Set of parameters defining the abstractions used in an Eva analysis. *)
-let parameters_abstractions = ref Typed_parameter.Set.empty
+let parameters_abstractions =
+ ref (Typed_parameter.Set.singleton Domains.parameter)
(* This functor must be used to create parameters for new domains of Eva. *)
module Domain_Parameter
diff --git a/src/plugins/value/value_parameters.mli b/src/plugins/value/value_parameters.mli
index 48882970b08..1b61fe9dcbc 100644
--- a/src/plugins/value/value_parameters.mli
+++ b/src/plugins/value/value_parameters.mli
@@ -28,6 +28,8 @@ module EnumerateCond: Parameter_sig.Bool
module OracleDepth: Parameter_sig.Int
module ReductionDepth: Parameter_sig.Int
+module Domains: Parameter_sig.String_set
+
module CvalueDomain: Parameter_sig.Bool
module EqualityDomain: Parameter_sig.Bool
module GaugesDomain: Parameter_sig.Bool
@@ -240,6 +242,8 @@ val dkey_callbacks : category
(** Debug category used to print the usage of widenings. *)
val dkey_widening : category
+(** Registers available domain names for the -eva-domains option. *)
+val register_domain: string -> unit
(** Notifies that the binding to Apron domains is available. *)
val register_apron: unit -> unit
--
GitLab