Merge branch 'feature/kernel/custom-parameters' into 'master'

[Kernel] Add a parameter builder for custom types

See merge request frama-c/frama-c!4450

src/kernel_services/cmdline_parameters/parameter_builder.ml

@@ -534,6 +534,127 @@ struct
     let is_empty () = Filepath.Normalized.is_empty (get ())
   end
 
+  (* ************************************************************************ *)
+  (** {3 Custom parameters} *)
+  (* ************************************************************************ *)
+
+  module Custom
+      (X: sig
+         include Parameter_sig.Input_with_arg
+         include Datatype.S
+         val default: t
+         val of_string: string -> t option
+         val to_string: t -> string
+       end) =
+  struct
+
+    include Build
+        (struct
+          include X
+          let default () = default
+          let functor_name = "Value"
+        end)
+
+    let possible_values = ref []
+    let set_possible_values s = possible_values := s
+    let get_possible_values () = !possible_values
+
+    (* Same interface as current module but with t replaced with string *)
+    module String_parameter =
+    struct
+      let get () =
+        X.to_string (get ())
+
+      let set s =
+        match X.of_string s with
+        | Some x -> set x
+        | None ->
+          (* Error during conversion from string to t, abort *)
+          let help_text =
+            match !possible_values with
+            | [] -> ""
+            | l ->
+              Format.asprintf "@ Possible values are: %a"
+                (Pretty_utils.pp_list ~sep:",@ " Format.pp_print_string) l
+          in
+          P.L.abort "invalid input '%s' for option %s. %s" s name help_text
+
+      let add_set_hook f =
+        let f' x1 x2 = f (X.to_string x1) (X.to_string x2) in
+        add_set_hook f'
+
+      let add_update_hook f =
+        let f' x1 x2 = f (X.to_string x1) (X.to_string x2) in
+        add_update_hook f'
+    end
+
+    let parameter =
+      let accessor =
+        let open String_parameter in
+        Typed_parameter.String (
+          { get; set; add_set_hook; add_update_hook },
+          get_possible_values)
+      in
+      let reconfigurable = is_parameter_reconfigurable stage in
+      let p =
+        Typed_parameter.create ~name ~help:X.help ~accessor
+          ~visible:is_visible ~reconfigurable ~is_set
+      in
+      add_parameter !Parameter_customize.group_ref stage p;
+      Cmdline.add_option option_name
+        ~argname:X.arg_name
+        ~help:X.help
+        ~visible:is_visible
+        ~ext_help:!Parameter_customize.optional_help_ref
+        ~plugin:P.shortname
+        ~group
+        stage
+        (Cmdline.String String_parameter.set);
+      Parameter_customize.reset ();
+      if is_dynamic then
+        Dynamic.register ~plugin:empty_string X.option_name Typed_parameter.ty p
+      else
+        p
+  end
+
+  module Enum
+      (X: sig
+         include Parameter_sig.Input_with_arg
+         type t
+         val default: t
+         val all_values: t list
+         val to_string: t -> string
+       end) =
+  struct
+    module Custom_input =
+    struct
+      include Datatype.Make (struct
+          include Datatype.Serializable_undefined
+          let name = "Parameter_builder.Enum(" ^ X.option_name ^ ")"
+          type t = X.t
+          let copy x = x
+          let compare = Stdlib.compare
+          let equal = Datatype.from_compare
+          let reprs = X.all_values
+        end)
+
+      include X
+
+      let of_string =
+        let table =
+          List.to_seq X.all_values
+          |> Seq.map (fun x -> X.to_string x, x)
+          |> Hashtbl.of_seq
+        in
+        Hashtbl.find_opt table
+    end
+
+    include Custom (Custom_input)
+
+    let () =
+      set_possible_values (List.map X.to_string X.all_values)
+  end
+
   (* ************************************************************************ *)
   (** {3 Collections} *)
   (* ************************************************************************ *)

src/kernel_services/cmdline_parameters/parameter_sig.ml

@@ -279,6 +279,21 @@ module type String = sig
   *)
 end
 
+(** Signature for a custom parameter. *)
+module type Custom = sig
+  include S
+
+  val set_possible_values: string list -> unit
+  (** Set what are the acceptable values for this parameter.
+      If the given list is empty, then all values are acceptable.
+      @since Frama-C+dev *)
+
+  val get_possible_values: unit -> string list
+  (** What are the acceptable values for this parameter.
+      If the returned list is empty, then all values are acceptable.
+      @since Frama-C+dev *)
+end
+
 (* ************************************************************************** *)
 (** {3 Custom signatures} *)
 (* ************************************************************************** *)
@@ -558,6 +573,28 @@ module type Builder = sig
           and vice-versa. *)
     end): Filepath
 
+  (** Allow using custom types as parameters.
+      @since Frama-c+dev *)
+  module Custom(X: sig
+      include Input_with_arg
+      include Datatype.S
+      val default: t
+      val of_string: string -> t option
+      val to_string: t -> string
+    end) : Custom with type t = X.t
+
+  (** A fixed set of possible values, represented by a type [t], intended to be
+      a variant with only a finite number of possible constructions.
+      Note that [t] must be comparable using [Stdlib.compare].
+      @since Frama-c+dev *)
+  module Enum(X : sig
+      include Input_with_arg
+      type t
+      val default: t
+      val all_values: t list
+      val to_string: t -> string
+    end) : S with type t = X.t
+
   exception Cannot_build of string
   module Make_set
       (E:

src/plugins/eva/engine/iterator.ml

@@ -100,15 +100,6 @@ module Make_Dataflow
 
   (* --- Plugin parameters --- *)
 
-  type descending_strategy = NoIteration | FullIteration | ExitIteration
-
-  let descending_iteration : descending_strategy =
-    match Parameters.DescendingIteration.get () with
-    | "no" -> NoIteration
-    | "exits" -> ExitIteration
-    | "full" -> FullIteration
-    | _ -> assert false
-
   let hierachical_convergence : bool =
     Parameters.HierarchicalConvergence.get ()
 
@@ -584,7 +575,7 @@ module Make_Dataflow
         incr iteration_count;
       done;
       (* Descending sequence *)
-      let l =  match descending_iteration with
+      let l =  match Parameters.DescendingIteration.get () with
         | NoIteration -> []
         | ExitIteration ->
           Self.debug ~dkey

src/plugins/eva/parameters.ml

@@ -566,20 +566,27 @@ let () = add_correctness_dep InitializationPaddingGlobals.parameter
 
 (* --- Iteration strategy --- *)
 
+type descending_strategy = NoIteration | FullIteration | ExitIteration
+
 let () = Parameter_customize.set_group precision_tuning
 let () = Parameter_customize.is_invisible ()
 module DescendingIteration =
-  String
+  Enum
     (struct
-      let default = "no"
       let option_name = "-eva-descending-iteration"
       let arg_name = "no|exits|full"
       let help = "Experimental. After hitting a postfix point, try to improve \
                   the precision with either a <full> iteration or an iteration \
                   from loop head to exit paths (<exits>) or do not try anything \
                   (<no>). Default is <no>."
+      type t = descending_strategy
+      let default = NoIteration
+      let all_values = [NoIteration ; FullIteration ; ExitIteration]
+      let to_string = function
+        | NoIteration -> "no"
+        | FullIteration -> "full"
+        | ExitIteration -> "exits"
     end)
-let () = DescendingIteration.set_possible_values ["no" ; "exits" ; "full"]
 let () = add_precision_dep DescendingIteration.parameter
 
 let () = Parameter_customize.set_group precision_tuning

src/plugins/eva/parameters.mli

@@ -62,7 +62,9 @@ module WarnSignedConvertedDowncast: Parameter_sig.Bool
 module WarnPointerSubstraction: Parameter_sig.Bool
 module WarnCopyIndeterminate: Parameter_sig.Kernel_function_set
 
-module DescendingIteration: Parameter_sig.String
+type descending_strategy = NoIteration | FullIteration | ExitIteration
+
+module DescendingIteration: Parameter_sig.S with type t = descending_strategy
 module HierarchicalConvergence: Parameter_sig.Bool
 module WideningDelay: Parameter_sig.Int
 module WideningPeriod: Parameter_sig.Int