[Eva] New message for the option -eva-domains with a description of each domain.

In the engine, registered domains must provide a description.
The domains description is printed on -eva-domains help or -eva-domains list.

src/plugins/value/domains/apron/apron_domain.ml

@@ -729,17 +729,23 @@ let () = Floating_point.set_round_nearest_even ()
 let make name enable (module Man: Input) =
   let module Domain = Domain_builder.Complete (Make (Man)) in
   let open Abstractions in
-  register ~enable { name; priority = 1;
+  let descr =
+    "Experimental binding to the " ^ name ^
+    " domain of the Apron library. \
+     See http://apron.cri.ensmp.fr/library for more details."
+  in
+  let name = "apron-" ^ name in
+  register ~enable { name; descr; priority = 1;
                      values = Single (module Main_values.Interval);
                      domain = Domain (module Domain); }
 
 let () =
   let open Value_parameters in
-  make "apron-octagon" ApronOctagon.get (module Apron_Octagon);
-  make "apron-box" ApronBox.get (module Apron_Box);
-  make "apron-polka-loose" PolkaLoose.get (module Apron_Polka_Loose);
-  make "apron-polka-strict" PolkaStrict.get (module Apron_Polka_Strict);
-  make "apron-polka-equality" PolkaEqualities.get (module Apron_Polka_Equalities);
+  make "octagon" ApronOctagon.get (module Apron_Octagon);
+  make "box" ApronBox.get (module Apron_Box);
+  make "polka-loose" PolkaLoose.get (module Apron_Polka_Loose);
+  make "polka-strict" PolkaStrict.get (module Apron_Polka_Strict);
+  make "polka-equality" PolkaEqualities.get (module Apron_Polka_Equalities);
   register_apron ()
 
 

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

@@ -155,6 +155,8 @@ let () =
   let open Abstractions in
   let domain =
     { name = "numerors";
+      descr = "Experimental. Infers ranges for the absolute and relative errors \
+               in floating-point computations. No support of loops.";
       priority = 0;
       values = Single (module Numerors_value);
       domain = Domain (module Domain); }

src/plugins/value/engine/abstractions.ml

@@ -40,6 +40,7 @@ type 'v domain =
 
 type 'v abstraction =
   { name: string;
+    descr: string;
     priority: int;
     values: 'v value;
     domain: 'v domain; }
@@ -66,7 +67,8 @@ module Config = struct
   let dynamic_abstractions : dynamic list ref = ref []
 
   let register ~enable abstraction =
-    Value_parameters.register_domain abstraction.name;
+    let { name; descr; } = abstraction in
+    Value_parameters.register_domain ~name ~descr;
     abstractions := (enable, Flag abstraction) :: !abstractions
 
   let dynamic_register ~configure ~make =
@@ -89,42 +91,74 @@ module Config = struct
   (* --- Register default abstractions -------------------------------------- *)
 
   let create ~enable abstract = register ~enable abstract; Flag abstract
-  let create_domain priority name enable values domain =
+  let create_domain priority name descr enable values domain =
     create ~enable
-      { name; priority; values = Single values; domain = Domain domain }
+      { name; descr; priority; values = Single values; domain = Domain domain }
 
   open Value_parameters
 
   (* Register standard domains over cvalues. *)
-  let make rank name enable =
-    create_domain rank name enable (module Main_values.CVal)
+  let make rank name descr enable =
+    create_domain rank name descr enable (module Main_values.CVal)
 
-  let cvalue = make 9 "cvalue" CvalueDomain.get (module Cvalue_domain.State)
+  let cvalue =
+    make 9 "cvalue"
+      "Main analysis domain, enabled by default. Should not be disabled."
+      CvalueDomain.get (module Cvalue_domain.State)
 
   let symbolic_locations =
-    make 7 "symbolic-locations" SymbolicLocsDomain.get (module Symbolic_locs.D)
+    make 7 "symbolic-locations"
+      "Infers values of symbolic locations represented by imprecise lvalues, \
+       such as t[i] or *p when the possible values of [i] or [p] are imprecise."
+      SymbolicLocsDomain.get (module Symbolic_locs.D)
 
   let equality_domain =
     { name = "equality";
+      descr = "Infers equalities between syntactic C expressions. \
+               Makes the analysis less dependent on temporary variables and \
+               intermediate computations.";
       priority = 8;
       values = Struct Abstract.Value.Unit;
       domain = Functor (module Equality_domain.Make); }
   let equality = create ~enable:EqualityDomain.get equality_domain
 
-  let gauges = make 6 "gauges" GaugesDomain.get (module Gauges_domain.D)
-  let octagon = make 6 "octagon" OctagonDomain.get (module Octagons)
+  let gauges =
+    make 6 "gauges"
+      "Infers linear inequalities between the variables modified within a loop \
+       and a special loop counter."
+      GaugesDomain.get (module Gauges_domain.D)
+
+  let octagon =
+    make 6 "octagon"
+      "Infers relations between scalar variables of the form b ≤ ±X ± Y ≤ e, \
+       where X, Y are program variables and b, e are constants."
+      OctagonDomain.get (module Octagons)
 
   let bitwise =
-    create_domain 3 "bitwise" BitwiseOffsmDomain.get
-      (module Offsm_value.Offsm) (module Offsm_domain.D)
+    create_domain 3 "bitwise"
+      "Infers bitwise information to interpret more precisely bitwise operators."
+      BitwiseOffsmDomain.get (module Offsm_value.Offsm) (module Offsm_domain.D)
 
   let sign =
-    create_domain 4 "sign" SignDomain.get
-      (module Sign_value) (module Sign_domain)
-
-  let inout = make 5 "inout" InoutDomain.get (module Inout_domain.D)
-  let traces = make 2 "traces" TracesDomain.get (module Traces_domain.D)
-  let printer = make 2 "printer" PrinterDomain.get (module Printer_domain)
+    create_domain 4 "sign"
+      "Infers the sign of program variables."
+      SignDomain.get (module Sign_value) (module Sign_domain)
+
+  let inout = make 5 "inout"
+      "Experimental. Infers the inputs and outputs of each function."
+      InoutDomain.get (module Inout_domain.D)
+
+  let traces =
+    make 2 "traces"
+      "Experimental. Builds an over-approximation of all the traces that lead \
+       to a statement."
+      TracesDomain.get (module Traces_domain.D)
+
+  let printer =
+    make 2 "printer"
+      "Debug domain, only useful for developers. Prints the transfer functions \
+       used during the analysis."
+      PrinterDomain.get (module Printer_domain)
 
   (* --- Default and legacy configurations ---------------------------------- *)
 

src/plugins/value/engine/abstractions.mli

@@ -57,12 +57,14 @@ type 'v domain =
   | Functor: (module domain_functor) -> _ domain
 
 (** Abstraction to be registered. The name of each abstraction must be unique.
+    The description is printed in the help message of the -eva-domains option.
     The priority can be any integer; domains with higher priority are always
     processed first. The domains currently provided by Eva have priority ranging
     between 1 and 19, so a priority of 0 (respectively 20) ensures that a new
     domain is processed after (respectively before) the classic Eva domains. *)
 type 'v abstraction =
   { name: string;      (** Name of the abstraction. Must be unique. *)
+    descr: string;     (** Short description of the abstraction. *)
     priority: int;     (** Domains with higher priority are processed first. *)
     values: 'v value;  (** The value abstraction. *)
     domain: 'v domain; (** The domain over the value abstraction. *)

src/plugins/value/value_parameters.ml

@@ -134,7 +134,7 @@ module Domains =
     end)
 let () = add_precision_dep Domains.parameter
 
-(* List of available domains. *)
+(* List (name, descr) of available domains. *)
 let domains_ref = ref []
 
 (* Help message for the -eva-domains option, with the list of currently
@@ -142,22 +142,36 @@ let domains_ref = ref []
 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)
+    "Enable a list of analysis domains. Available domains are: %a. \
+     Use -eva-domains help to print a short description of each domain."
+    pp_str_list (List.rev_map fst !domains_ref)
+
+(* Prints the list of available domains with their description. *)
+let domains_list () =
+  let pp_dom fmt (name, descr) =
+    Format.fprintf fmt "%-20s @[%t@]" name
+      (fun fmt -> Format.pp_print_text fmt descr)
+  in
+  feedback ~level:0
+    "List of available domains:@. %a@."
+    (Pretty_utils.pp_list ~sep:"@," pp_dom) (List.rev !domains_ref);
+  raise Cmdline.Exit
 
 (* Registers a new domain. Updates the help message of -eva-domains. *)
-let register_domain name =
+let register_domain ~name ~descr =
   Cmdline.replace_option_help
     Domains.option_name "eva" domains (domains_help ());
-  domains_ref := name :: !domains_ref
+  domains_ref := (name, descr) :: !domains_ref
 
 (* Checks that a domain has been registered. *)
 let check_domain domain =
-  if not (List.mem domain !domains_ref)
+  if domain = "help" || domain = "list"
+  then domains_list ()
+  else if not (List.exists (fun (name, _) -> name = 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)
+      domain pp_str_list (List.rev_map fst !domains_ref)
 
 let () =
   Domains.add_set_hook

src/plugins/value/value_parameters.mli

@@ -243,7 +243,7 @@ val dkey_callbacks : category
 val dkey_widening : category
 
 (** Registers available domain names for the -eva-domains option. *)
-val register_domain: string -> unit
+val register_domain: name:string -> descr:string -> unit
 
 (** Notifies that the binding to Apron domains is available. *)
 val register_apron: unit -> unit