Refactor command line flag handling for plugins

Flags are now created with the `Flag.create` function.

These are then converted into the strings Arg.parse and similar use
in `src/bin/sail.ml`. The output of `sail -h` remains the same, so no
actual flags have changed.

Flags can now have more data, i.e. rather than "-lem_split_files", it can now be:
```
Flag.create ~prefix:["lem"] "split_files"
```
meaning we can now recognize this flag is part of the lem options and parse it from e.g.
a JSON configuration file as `lem.split_files`.

src/bin/sail.ml

@@ -149,7 +149,7 @@ let add_target_header plugin opts =
 let load_plugin opts plugin =
   try
     if is_bytecode then Dynlink.loadfile plugin else Dynlink.loadfile_private plugin;
-    let plugin_opts = Target.extract_options () |> fix_options |> target_align in
+    let plugin_opts = Target.extract_options () |> List.map Flag.to_arg |> fix_options |> target_align in
     opts := add_target_header plugin !opts @ plugin_opts
   with Dynlink.Error msg -> prerr_endline ("Failed to load plugin " ^ plugin ^ ": " ^ Dynlink.error_message msg)
 

src/lib/flag.ml

@@ -0,0 +1,64 @@
+(****************************************************************************)
+(*     Sail                                                                 *)
+(*                                                                          *)
+(*  Sail and the Sail architecture models here, comprising all files and    *)
+(*  directories except the ASL-derived Sail code in the aarch64 directory,  *)
+(*  are subject to the BSD two-clause licence below.                        *)
+(*                                                                          *)
+(*  The ASL derived parts of the ARMv8.3 specification in                   *)
+(*  aarch64/no_vector and aarch64/full are copyright ARM Ltd.               *)
+(*                                                                          *)
+(*  Copyright (c) 2013-2021                                                 *)
+(*    Kathyrn Gray                                                          *)
+(*    Shaked Flur                                                           *)
+(*    Stephen Kell                                                          *)
+(*    Gabriel Kerneis                                                       *)
+(*    Robert Norton-Wright                                                  *)
+(*    Christopher Pulte                                                     *)
+(*    Peter Sewell                                                          *)
+(*    Alasdair Armstrong                                                    *)
+(*    Brian Campbell                                                        *)
+(*    Thomas Bauereiss                                                      *)
+(*    Anthony Fox                                                           *)
+(*    Jon French                                                            *)
+(*    Dominic Mulligan                                                      *)
+(*    Stephen Kell                                                          *)
+(*    Mark Wassell                                                          *)
+(*    Alastair Reid (Arm Ltd)                                               *)
+(*                                                                          *)
+(*  All rights reserved.                                                    *)
+(*                                                                          *)
+(*  This work was partially supported by EPSRC grant EP/K008528/1 <a        *)
+(*  href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous          *)
+(*  Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA   *)
+(*  KTF funding, and donations from Arm.  This project has received         *)
+(*  funding from the European Research Council (ERC) under the European     *)
+(*  Union’s Horizon 2020 research and innovation programme (grant           *)
+(*  agreement No 789108, ELVER).                                            *)
+(*                                                                          *)
+(*  This software was developed by SRI International and the University of  *)
+(*  Cambridge Computer Laboratory (Department of Computer Science and       *)
+(*  Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV")        *)
+(*  and FA8750-10-C-0237 ("CTSRD").                                         *)
+(*                                                                          *)
+(*  SPDX-License-Identifier: BSD-2-Clause                                   *)
+(****************************************************************************)
+
+open Arg
+
+type t = { prefix : string list; hide_prefix : bool; debug : bool; hide : bool; arg : string option; key : string }
+
+let create ?(prefix = []) ?(hide_prefix = false) ?(debug = false) ?(hide = false) ?arg key =
+  { prefix; hide_prefix; debug; hide; arg; key }
+
+let underscore_sep = Util.string_of_list "_" (fun s -> s)
+
+let to_arg (flag, spec, doc) =
+  let apply_prefix key =
+    match flag.prefix with [] -> key | _ when flag.hide_prefix -> key | _ -> underscore_sep flag.prefix ^ "_" ^ key
+  in
+  let key =
+    "-" ^ if flag.key = "" then underscore_sep flag.prefix else (if flag.debug then "d" else "") ^ apply_prefix flag.key
+  in
+  let arg_prefix = match flag.arg with Some desc -> "<" ^ desc ^ "> " | None -> " " in
+  (key, spec, if flag.hide then "" else arg_prefix ^ (if flag.debug then "(debug) " else "") ^ doc)

src/lib/flag.mli

@@ -0,0 +1,51 @@
+(****************************************************************************)
+(*     Sail                                                                 *)
+(*                                                                          *)
+(*  Sail and the Sail architecture models here, comprising all files and    *)
+(*  directories except the ASL-derived Sail code in the aarch64 directory,  *)
+(*  are subject to the BSD two-clause licence below.                        *)
+(*                                                                          *)
+(*  The ASL derived parts of the ARMv8.3 specification in                   *)
+(*  aarch64/no_vector and aarch64/full are copyright ARM Ltd.               *)
+(*                                                                          *)
+(*  Copyright (c) 2013-2021                                                 *)
+(*    Kathyrn Gray                                                          *)
+(*    Shaked Flur                                                           *)
+(*    Stephen Kell                                                          *)
+(*    Gabriel Kerneis                                                       *)
+(*    Robert Norton-Wright                                                  *)
+(*    Christopher Pulte                                                     *)
+(*    Peter Sewell                                                          *)
+(*    Alasdair Armstrong                                                    *)
+(*    Brian Campbell                                                        *)
+(*    Thomas Bauereiss                                                      *)
+(*    Anthony Fox                                                           *)
+(*    Jon French                                                            *)
+(*    Dominic Mulligan                                                      *)
+(*    Stephen Kell                                                          *)
+(*    Mark Wassell                                                          *)
+(*    Alastair Reid (Arm Ltd)                                               *)
+(*                                                                          *)
+(*  All rights reserved.                                                    *)
+(*                                                                          *)
+(*  This work was partially supported by EPSRC grant EP/K008528/1 <a        *)
+(*  href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous          *)
+(*  Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA   *)
+(*  KTF funding, and donations from Arm.  This project has received         *)
+(*  funding from the European Research Council (ERC) under the European     *)
+(*  Union’s Horizon 2020 research and innovation programme (grant           *)
+(*  agreement No 789108, ELVER).                                            *)
+(*                                                                          *)
+(*  This software was developed by SRI International and the University of  *)
+(*  Cambridge Computer Laboratory (Department of Computer Science and       *)
+(*  Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV")        *)
+(*  and FA8750-10-C-0237 ("CTSRD").                                         *)
+(*                                                                          *)
+(*  SPDX-License-Identifier: BSD-2-Clause                                   *)
+(****************************************************************************)
+
+type t
+
+val create : ?prefix:string list -> ?hide_prefix:bool -> ?debug:bool -> ?hide:bool -> ?arg:string -> string -> t
+
+val to_arg : t * Arg.spec * string -> Arg.key * Arg.spec * Arg.doc

src/lib/target.ml

@@ -52,7 +52,7 @@ module StringMap = Map.Make (String)
 
 type target = {
   name : string;
-  options : (Arg.key * Arg.spec * Arg.doc) list;
+  options : (Flag.t * Arg.spec * string) list;
   pre_parse_hook : unit -> unit;
   pre_initial_check_hook : string list -> unit;
   pre_rewrites_hook : typed_ast -> Effects.side_effect_info -> Env.t -> unit;
@@ -93,12 +93,12 @@ let register ~name ?flag ?description:desc ?(options = []) ?(pre_parse_hook = fu
         prerr_endline ("Cannot use multiple Sail targets simultaneously: " ^ tgt ^ " and " ^ name);
         exit 1
   in
-  let desc = match desc with Some desc -> desc | None -> " invoke the Sail " ^ name ^ " target" in
+  let desc = match desc with Some desc -> desc | None -> "invoke the Sail " ^ name ^ " target" in
   let flag = match flag with Some flag -> flag | None -> name in
   let tgt =
     {
       name;
-      options = ("-" ^ flag, Arg.Unit set_target, desc) :: options;
+      options = (Flag.create ~prefix:[flag] "", Arg.Unit set_target, desc) :: options;
       pre_parse_hook;
       pre_initial_check_hook;
       pre_rewrites_hook;

src/lib/target.mli

@@ -106,7 +106,7 @@ val register :
   name:string ->
   ?flag:string ->
   ?description:string ->
-  ?options:(Arg.key * Arg.spec * Arg.doc) list ->
+  ?options:(Flag.t * Arg.spec * string) list ->
   ?pre_parse_hook:(unit -> unit) ->
   ?pre_initial_check_hook:(string list -> unit) ->
   ?pre_rewrites_hook:(typed_ast -> Effects.side_effect_info -> Env.t -> unit) ->
@@ -130,4 +130,4 @@ val get : name:string -> target option
 val extract_registered : unit -> string list
 
 (** Used internally to dynamically update the option list when loading plugins *)
-val extract_options : unit -> (Arg.key * Arg.spec * Arg.doc) list
+val extract_options : unit -> (Flag.t * Arg.spec * string) list

src/sail_c_backend/sail_plugin_c.ml

@@ -53,39 +53,42 @@ let opt_specialize_c = ref false
 
 let c_options =
   [
-    ( "-c_include",
+    ( Flag.create ~prefix:["c"] ~arg:"filename" "include",
       Arg.String (fun i -> opt_includes_c := i :: !opt_includes_c),
-      "<filename> provide additional include for C output"
+      "provide additional include for C output"
     );
-    ("-c_no_main", Arg.Set C_backend.opt_no_main, " do not generate the main() function");
-    ("-c_no_rts", Arg.Set C_backend.opt_no_rts, " do not include the Sail runtime");
-    ( "-c_no_lib",
+    (Flag.create ~prefix:["c"] "no_main", Arg.Set C_backend.opt_no_main, "do not generate the main() function");
+    (Flag.create ~prefix:["c"] "no_rts", Arg.Set C_backend.opt_no_rts, "do not include the Sail runtime");
+    ( Flag.create ~prefix:["c"] "no_lib",
       Arg.Tuple [Arg.Set C_backend.opt_no_lib; Arg.Set C_backend.opt_no_rts],
-      " do not include the Sail runtime or library"
+      "do not include the Sail runtime or library"
     );
-    ("-c_prefix", Arg.String (fun prefix -> C_backend.opt_prefix := prefix), "<prefix> prefix generated C functions");
-    ( "-c_extra_params",
+    ( Flag.create ~prefix:["c"] ~arg:"prefix" "prefix",
+      Arg.String (fun prefix -> C_backend.opt_prefix := prefix),
+      "prefix generated C functions"
+    );
+    ( Flag.create ~prefix:["c"] ~arg:"parameters" "extra_params",
       Arg.String (fun params -> C_backend.opt_extra_params := Some params),
-      "<parameters> generate C functions with additional parameters"
+      "generate C functions with additional parameters"
     );
-    ( "-c_extra_args",
+    ( Flag.create ~prefix:["c"] ~arg:"arguments" "extra_args",
       Arg.String (fun args -> C_backend.opt_extra_arguments := Some args),
-      "<arguments> supply extra argument to every generated C function call"
+      "supply extra argument to every generated C function call"
     );
-    ("-c_specialize", Arg.Set opt_specialize_c, " specialize integer arguments in C output");
-    ( "-c_preserve",
+    (Flag.create ~prefix:["c"] "specialize", Arg.Set opt_specialize_c, "specialize integer arguments in C output");
+    ( Flag.create ~prefix:["c"] "preserve",
       Arg.String (fun str -> Specialize.add_initial_calls (Ast_util.IdSet.singleton (Ast_util.mk_id str))),
-      " make sure the provided function identifier is preserved in C output"
+      "make sure the provided function identifier is preserved in C output"
     );
-    ( "-c_fold_unit",
+    ( Flag.create ~prefix:["c"] "fold_unit",
       Arg.String (fun str -> Constant_fold.opt_fold_to_unit := Util.split_on_char ',' str),
-      " remove comma separated list of functions from C output, replacing them with unit"
+      "remove comma separated list of functions from C output, replacing them with unit"
     );
-    ( "-c_coverage",
+    ( Flag.create ~prefix:["c"] ~arg:"file" "coverage",
       Arg.String (fun str -> C_backend.opt_branch_coverage := Some (open_out str)),
-      "<file> Turn on coverage tracking and output information about all branches and functions to a file"
+      "Turn on coverage tracking and output information about all branches and functions to a file"
     );
-    ( "-O",
+    ( Flag.create ~prefix:["c"] ~hide_prefix:true "O",
       Arg.Tuple
         [
           Arg.Set C_backend.optimize_primops;
@@ -94,17 +97,20 @@ let c_options =
           Arg.Set C_backend.optimize_struct_updates;
           Arg.Set C_backend.optimize_alias;
         ],
-      " turn on optimizations for C compilation"
+      "turn on optimizations for C compilation"
     );
-    ( "-Ofixed_int",
+    ( Flag.create ~prefix:["c"] ~hide_prefix:true "Ofixed_int",
       Arg.Set C_backend.optimize_fixed_int,
-      " assume fixed size integers rather than GMP arbitrary precision integers"
+      "assume fixed size integers rather than GMP arbitrary precision integers"
     );
-    ( "-Ofixed_bits",
+    ( Flag.create ~prefix:["c"] ~hide_prefix:true "Ofixed_bits",
       Arg.Set C_backend.optimize_fixed_bits,
-      " assume fixed size bitvectors rather than arbitrary precision bitvectors"
+      "assume fixed size bitvectors rather than arbitrary precision bitvectors"
+    );
+    ( Flag.create ~prefix:["c"] ~hide_prefix:true "static",
+      Arg.Set C_backend.opt_static,
+      "make generated C functions static"
     );
-    ("-static", Arg.Set C_backend.opt_static, " make generated C functions static");
   ]
 
 let c_rewrites =

src/sail_coq_backend/sail_plugin_coq.ml

@@ -58,58 +58,57 @@ let opt_coq_lib_style : Pretty_print_coq.library_style option ref = ref None
 
 let coq_options =
   [
-    ( "-coq_output_dir",
+    ( Flag.create ~prefix:["coq"] ~arg:"directory" "output_dir",
       Arg.String (fun dir -> opt_coq_output_dir := Some dir),
-      "<directory> set a custom directory to output generated Coq"
+      "set a custom directory to output generated Coq"
     );
-    ( "-coq_lib",
+    ( Flag.create ~prefix:["coq"] ~arg:"filename" "lib",
       Arg.String (fun l -> opt_libs_coq := l :: !opt_libs_coq),
-      "<filename> provide additional library to open in Coq output"
+      "provide additional library to open in Coq output"
     );
-    ( "-coq_alt_modules",
+    ( Flag.create ~prefix:["coq"] ~arg:"filename" "alt_modules",
       Arg.String (fun l -> opt_alt_modules_coq := l :: !opt_alt_modules_coq),
-      "<filename> provide alternative modules to open in Coq output"
+      "provide alternative modules to open in Coq output"
     );
-    ( "-coq_alt_modules2",
+    ( Flag.create ~prefix:["coq"] ~arg:"filename" "alt_modules2",
       Arg.String (fun l -> opt_alt_modules2_coq := l :: !opt_alt_modules2_coq),
-      "<filename> provide additional alternative modules to open only in main (non-_types) Coq output, and suppress \
-       default definitions of MR and M monads"
+      "provide additional alternative modules to open only in main (non-_types) Coq output, and suppress default \
+       definitions of MR and M monads"
     );
-    ( "-coq_extern_type",
+    ( Flag.create ~prefix:["coq"] ~arg:"typename" "extern_type",
       Arg.String Pretty_print_coq.(fun ty -> opt_extern_types := ty :: !opt_extern_types),
-      "<typename> do not generate a definition for the type"
+      "do not generate a definition for the type"
     );
-    ( "-coq_generate_extern_types",
+    ( Flag.create ~prefix:["coq"] "generate_extern_types",
       Arg.Set Pretty_print_coq.opt_generate_extern_types,
-      " generate only extern types rather than suppressing them"
+      "generate only extern types rather than suppressing them"
     );
-    ( "-coq_isla",
+    ( Flag.create ~prefix:["coq"] ~arg:"filename" "isla",
       Arg.String (fun fname -> opt_coq_isla := Some fname),
-      "<filename> generate Coq code for decoding Isla trace values"
+      "generate Coq code for decoding Isla trace values"
     );
-    ( "-coq_record_update",
+    ( Flag.create ~prefix:["coq"] "record_update",
       Arg.Set Pretty_print_coq.opt_coq_record_update,
-      " use coq-record-update package's syntax for record updates"
+      "use coq-record-update package's syntax for record updates"
     );
-    ( "-coq_lib_style",
+    ( Flag.create ~prefix:["coq"] "lib_style",
       Arg.Symbol
         ( ["bbv"; "stdpp"],
           fun s -> opt_coq_lib_style := match s with "bbv" -> Some BBV | "stdpp" -> Some Stdpp | _ -> assert false
         ),
-      " select which style of Coq library to use (default: stdpp when the concurrency interfaces is used, bbv \
-       otherwise)"
+      "select which style of Coq library to use (default: stdpp when the concurrency interfaces is used, bbv otherwise)"
     );
-    ( "-dcoq_undef_axioms",
+    ( Flag.create ~prefix:["coq"] ~debug:true "undef_axioms",
       Arg.Set Pretty_print_coq.opt_undef_axioms,
-      " (debug) generate axioms for functions that are declared but not defined"
+      "generate axioms for functions that are declared but not defined"
     );
-    ( "-dcoq_warn_nonex",
+    ( Flag.create ~prefix:["coq"] ~debug:true "warn_nonex",
       Arg.Set Rewrites.opt_coq_warn_nonexhaustive,
-      " (debug) generate warnings for non-exhaustive pattern matches in the Coq backend"
+      "generate warnings for non-exhaustive pattern matches in the Coq backend"
     );
-    ( "-dcoq_debug_on",
+    ( Flag.create ~prefix:["coq"] ~arg:"function" ~debug:true "debug_on",
       Arg.String (fun f -> Pretty_print_coq.opt_debug_on := f :: !Pretty_print_coq.opt_debug_on),
-      "<function> (debug) produce debug messages for Coq output on given function"
+      "produce debug messages for Coq output on given function"
     );
   ]