diff --git a/src/plugins/value/engine/abstractions.ml b/src/plugins/value/engine/abstractions.ml index 5e73c7d1374b9b9d76a5b9db7c43b7bd43eb2a60..0e06c7ac4088c9c0ddf252de9a7efc1c889f743d 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 3d4ebe9e437fdf5e913e368f9a5a9a0976ac5d69..a29aed97b43fd9a91ffc8ad4ace629bd0db7bfa9 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 8a3c6adf265da929fab73d7083933b3696d3c5bc..1e839e5afd1699148026815c08dcb5d76b3882d3 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 48882970b088232c190d10c9be7b8cb9b5d9c9d9..1b61fe9dcbc3c7a64cf8e3c23abe87f69c5cca22 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