diff --git a/src/bin/sail.ml b/src/bin/sail.ml
index 07fec203b..dad0f27b6 100644
--- a/src/bin/sail.ml
+++ b/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)
diff --git a/src/lib/flag.ml b/src/lib/flag.ml
new file mode 100644
index 000000000..ddfa2ed77
--- /dev/null
+++ b/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 REMS: Rigorous *)
+(* Engineering for Mainstream Systems, 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)
diff --git a/src/lib/flag.mli b/src/lib/flag.mli
new file mode 100644
index 000000000..5d378814a
--- /dev/null
+++ b/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 REMS: Rigorous *)
+(* Engineering for Mainstream Systems, 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
diff --git a/src/lib/target.ml b/src/lib/target.ml
index b2c8a7e4a..16e4d179a 100644
--- a/src/lib/target.ml
+++ b/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;
diff --git a/src/lib/target.mli b/src/lib/target.mli
index 5ab1d8182..d360cd170 100644
--- a/src/lib/target.mli
+++ b/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
diff --git a/src/sail_c_backend/sail_plugin_c.ml b/src/sail_c_backend/sail_plugin_c.ml
index 37d1af537..13670e812 100644
--- a/src/sail_c_backend/sail_plugin_c.ml
+++ b/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),
- " 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 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),
- " 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),
- " 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)),
- " 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 =
diff --git a/src/sail_coq_backend/sail_plugin_coq.ml b/src/sail_coq_backend/sail_plugin_coq.ml
index 41988d7be..a5afe5722 100644
--- a/src/sail_coq_backend/sail_plugin_coq.ml
+++ b/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),
- " 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),
- " 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),
- " 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),
- " 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),
- " 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),
- " 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),
- " (debug) produce debug messages for Coq output on given function"
+ "produce debug messages for Coq output on given function"
);
]
diff --git a/src/sail_doc_backend/sail_plugin_doc.ml b/src/sail_doc_backend/sail_plugin_doc.ml
index e9c77cb2f..f803b3dcf 100644
--- a/src/sail_doc_backend/sail_plugin_doc.ml
+++ b/src/sail_doc_backend/sail_plugin_doc.ml
@@ -69,24 +69,30 @@ let embedding_option () =
let doc_options =
[
- ( "-doc_format",
+ ( Flag.create ~prefix:["doc"] ~arg:"format" "format",
Arg.String (fun format -> opt_doc_format := format),
- " Output documentation in the chosen format, either latex or asciidoc (default asciidoc)"
+ "Output documentation in the chosen format, either latex or asciidoc (default asciidoc)"
);
- ( "-doc_file",
+ ( Flag.create ~prefix:["doc"] ~arg:"file" "file",
Arg.String (fun file -> opt_doc_files := file :: !opt_doc_files),
- " Document only the provided files"
+ "Document only the provided files"
);
- ( "-doc_embed",
+ ( Flag.create ~prefix:["doc"] ~arg:"plain|base64" "embed",
Arg.String (fun format -> opt_doc_embed := Some format),
- " Embed all documentation contents into the documentation bundle rather than referencing it"
+ "Embed all documentation contents into the documentation bundle rather than referencing it"
);
- ( "-doc_embed_with_location",
+ ( Flag.create ~prefix:["doc"] "embed_with_location",
Arg.Set opt_doc_embed_with_location,
- " When used with --doc-embed, include both the contents and locations"
+ "When used with --doc-embed, include both the contents and locations"
+ );
+ ( Flag.create ~prefix:["doc"] "compact",
+ Arg.Unit (fun _ -> opt_doc_compact := true),
+ "Use compact documentation format"
+ );
+ ( Flag.create ~prefix:["doc"] ~arg:"file" "bundle",
+ Arg.String (fun file -> opt_doc_bundle := file),
+ "Name for documentation bundle file"
);
- ("-doc_compact", Arg.Unit (fun _ -> opt_doc_compact := true), " Use compact documentation format");
- ("-doc_bundle", Arg.String (fun file -> opt_doc_bundle := file), " Name for documentation bundle file");
]
let output_docinfo doc_dir docinfo =
@@ -136,10 +142,13 @@ let _ =
let html_options =
[
- ("-html_css", Arg.String (fun file -> opt_html_css := Some file), " CSS file for html output");
- ( "-html_link_prefix",
+ ( Flag.create ~prefix:["html"] ~arg:"file" "css",
+ Arg.String (fun file -> opt_html_css := Some file),
+ "CSS file for html output"
+ );
+ ( Flag.create ~prefix:["html"] ~arg:"string" "link_prefix",
Arg.String (fun prefix -> opt_html_link_prefix := prefix),
- " Prefix links in HTML output with string"
+ "Prefix links in HTML output with string"
);
]
diff --git a/src/sail_latex_backend/sail_plugin_latex.ml b/src/sail_latex_backend/sail_plugin_latex.ml
index bbbfcc5d6..a66ee3b48 100644
--- a/src/sail_latex_backend/sail_plugin_latex.ml
+++ b/src/sail_latex_backend/sail_plugin_latex.ml
@@ -50,12 +50,15 @@ open Interactive.State
let latex_options =
[
- ( "-latex_prefix",
+ ( Flag.create ~prefix:["latex"] ~arg:"prefix" "prefix",
Arg.String (fun prefix -> Latex.opt_prefix := prefix),
- " set a custom prefix for generated LaTeX labels and macro commands (default sail)"
+ "set a custom prefix for generated LaTeX labels and macro commands (default sail)"
);
- ("-latex_full_valspecs", Arg.Clear Latex.opt_simple_val, " print full valspecs in LaTeX output");
- ( "-latex_abbrevs",
+ ( Flag.create ~prefix:["latex"] "full_valspecs",
+ Arg.Clear Latex.opt_simple_val,
+ "print full valspecs in LaTeX output"
+ );
+ ( Flag.create ~prefix:["latex"] "abbrevs",
Arg.String
(fun s ->
let abbrevs = String.split_on_char ';' s in
@@ -68,7 +71,7 @@ let latex_options =
| None -> Latex.opt_abbrevs := filtered
| Some abbrev -> raise (Arg.Bad (abbrev ^ " does not end in a '.'"))
),
- " semicolon-separated list of abbreviations to fix spacing for in LaTeX output (default 'e.g.;i.e.')"
+ "semicolon-separated list of abbreviations to fix spacing for in LaTeX output (default 'e.g.;i.e.')"
);
]
diff --git a/src/sail_lean_backend/sail_plugin_lean.ml b/src/sail_lean_backend/sail_plugin_lean.ml
index 231cfbe1b..882063b41 100644
--- a/src/sail_lean_backend/sail_plugin_lean.ml
+++ b/src/sail_lean_backend/sail_plugin_lean.ml
@@ -77,13 +77,13 @@ let lean_version : string = "lean4:nightly-2024-09-25"
let lean_options =
[
- ( "-lean_output_dir",
+ ( Flag.create ~prefix:["lean"] ~arg:"directory" "output_dir",
Arg.String (fun dir -> opt_lean_output_dir := Some dir),
- " set a custom directory to output generated Lean"
+ "set a custom directory to output generated Lean"
);
- ( "-lean_force_output",
+ ( Flag.create ~prefix:["lean"] "force_output",
Arg.Unit (fun () -> opt_lean_force_output := true),
- " removes the content of the output directory if it is non-empty"
+ "removes the content of the output directory if it is non-empty"
);
]
diff --git a/src/sail_lem_backend/sail_plugin_lem.ml b/src/sail_lem_backend/sail_plugin_lem.ml
index 2fe2d41ef..3e022ec97 100644
--- a/src/sail_lem_backend/sail_plugin_lem.ml
+++ b/src/sail_lem_backend/sail_plugin_lem.ml
@@ -57,24 +57,33 @@ let opt_lem_split_files : bool ref = ref false
let lem_options =
[
- ( "-lem_output_dir",
+ ( Flag.create ~prefix:["lem"] ~arg:"directory" "output_dir",
Arg.String (fun dir -> opt_lem_output_dir := Some dir),
- " set a custom directory to output generated Lem"
+ "set a custom directory to output generated Lem"
);
- ( "-isa_output_dir",
+ ( Flag.create ~prefix:["lem"] ~arg:"directory" ~hide_prefix:true "isa_output_dir",
Arg.String (fun dir -> opt_isa_output_dir := Some dir),
- " set a custom directory to output generated Isabelle auxiliary theories"
+ "set a custom directory to output generated Isabelle auxiliary theories"
);
- ("-lem_split_files", Arg.Set opt_lem_split_files, " split output into multiple files, one per input file");
- ( "-lem_lib",
+ ( Flag.create ~prefix:["lem"] "split_files",
+ Arg.Set opt_lem_split_files,
+ "split output into multiple files, one per input file"
+ );
+ ( Flag.create ~prefix:["lem"] ~arg:"filename" "lib",
Arg.String (fun l -> opt_libs_lem := l :: !opt_libs_lem),
- " provide additional library to open in Lem output"
+ "provide additional library to open in Lem output"
+ );
+ ( Flag.create ~prefix:["lem"] "sequential",
+ Arg.Set Pretty_print_lem.opt_sequential,
+ "use sequential state monad for Lem output"
+ );
+ ( Flag.create ~prefix:["lem"] "mwords",
+ Arg.Set Monomorphise.opt_mwords,
+ "use native machine word library for Lem output"
);
- ("-lem_sequential", Arg.Set Pretty_print_lem.opt_sequential, " use sequential state monad for Lem output");
- ("-lem_mwords", Arg.Set Monomorphise.opt_mwords, " use native machine word library for Lem output");
- ( "-lem_extern_type",
+ ( Flag.create ~prefix:["lem"] ~arg:"typename" "extern_type",
Arg.String Pretty_print_lem.(fun ty -> opt_extern_types := ty :: !opt_extern_types),
- " do not generate a definition for the type"
+ "do not generate a definition for the type"
);
]
diff --git a/src/sail_ocaml_backend/sail_plugin_ocaml.ml b/src/sail_ocaml_backend/sail_plugin_ocaml.ml
index 9934dbf65..08bd2be5b 100644
--- a/src/sail_ocaml_backend/sail_plugin_ocaml.ml
+++ b/src/sail_ocaml_backend/sail_plugin_ocaml.ml
@@ -52,22 +52,22 @@ let opt_ocaml_generators = ref ([] : string list)
let ocaml_options =
[
- ("-ocaml_nobuild", Arg.Set Ocaml_backend.opt_ocaml_nobuild, " do not build generated OCaml");
- ( "-ocaml_trace",
+ (Flag.create ~prefix:["ocaml"] "nobuild", Arg.Set Ocaml_backend.opt_ocaml_nobuild, "do not build generated OCaml");
+ ( Flag.create ~prefix:["ocaml"] "trace",
Arg.Set Ocaml_backend.opt_trace_ocaml,
- " output an OCaml translated version of the input with tracing instrumentation, implies -ocaml"
+ "output an OCaml translated version of the input with tracing instrumentation, implies -ocaml"
);
- ( "-ocaml_build_dir",
+ ( Flag.create ~prefix:["ocaml"] ~arg:"directory" "build_dir",
Arg.String (fun dir -> Ocaml_backend.opt_ocaml_build_dir := dir),
- " set a custom directory to build generated OCaml"
+ "set a custom directory to build generated OCaml"
);
- ( "-ocaml_coverage",
+ ( Flag.create ~prefix:["ocaml"] "coverage",
Arg.Set Ocaml_backend.opt_ocaml_coverage,
- " build OCaml with bisect_ppx coverage reporting (requires opam packages bisect_ppx-ocamlbuild and bisect_ppx)."
+ "build OCaml with bisect_ppx coverage reporting (requires opam packages bisect_ppx-ocamlbuild and bisect_ppx)."
);
- ( "-ocaml_generators",
+ ( Flag.create ~prefix:["ocaml"] ~arg:"types" "generators",
Arg.String (fun s -> opt_ocaml_generators := s :: !opt_ocaml_generators),
- " produce random generators for the given types"
+ "produce random generators for the given types"
);
]
@@ -115,17 +115,17 @@ let opt_tofrominterp_output_dir : string option ref = ref None
let tofrominterp_options =
[
- ( "-tofrominterp_lem",
+ ( Flag.create ~prefix:["tofrominterp"] "lem",
Arg.Set ToFromInterp_backend.lem_mode,
- " output embedding translation for the Lem backend rather than the OCaml backend, implies -tofrominterp"
+ "output embedding translation for the Lem backend rather than the OCaml backend, implies -tofrominterp"
);
- ( "-tofrominterp_mwords",
+ ( Flag.create ~prefix:["tofrominterp"] "mwords",
Arg.Set ToFromInterp_backend.mword_mode,
- " output embedding translation in machine-word mode rather than bit-list mode, implies -tofrominterp"
+ "output embedding translation in machine-word mode rather than bit-list mode, implies -tofrominterp"
);
- ( "-tofrominterp_output_dir",
+ ( Flag.create ~prefix:["tofrominterp"] ~arg:"directory" "output_dir",
Arg.String (fun dir -> opt_tofrominterp_output_dir := Some dir),
- " set a custom directory to output embedding translation OCaml"
+ "set a custom directory to output embedding translation OCaml"
);
]
@@ -149,7 +149,7 @@ let tofrominterp_target out_file { ast; _ } =
let _ =
Target.register ~name:"tofrominterp"
- ~description:" output OCaml functions to translate between shallow embedding and interpreter"
+ ~description:"output OCaml functions to translate between shallow embedding and interpreter"
~options:tofrominterp_options ~rewrites:tofrominterp_rewrites tofrominterp_target
let marshal_target out_file { ast; env; _ } =
@@ -164,5 +164,5 @@ let marshal_target out_file { ast; env; _ } =
close_out f
let _ =
- Target.register ~name:"marshal" ~description:" OCaml-marshal out the rewritten AST to a file"
+ Target.register ~name:"marshal" ~description:"OCaml-marshal out the rewritten AST to a file"
~rewrites:tofrominterp_rewrites marshal_target
diff --git a/src/sail_output/sail_plugin_output.ml b/src/sail_output/sail_plugin_output.ml
index b2e642293..415f8c66e 100644
--- a/src/sail_output/sail_plugin_output.ml
+++ b/src/sail_output/sail_plugin_output.ml
@@ -50,9 +50,9 @@ open Interactive.State
let output_sail_options =
[
- ( "-output_sail_dir",
+ ( Flag.create ~prefix:["output_sail"] ~arg:"directory" "dir",
Arg.String (fun dir -> Frontend.opt_reformat := Some dir),
- " set a directory to output pretty-printed Sail"
+ "set a directory to output pretty-printed Sail"
);
]
@@ -63,4 +63,4 @@ let sail_target out_file { ast; _ } =
let _ =
Target.register ~name:"sail" ~flag:"output_sail" ~options:output_sail_options
- ~description:" print Sail code after type checking and initial rewriting" sail_target
+ ~description:"print Sail code after type checking and initial rewriting" sail_target
diff --git a/src/sail_smt_backend/sail_plugin_smt.ml b/src/sail_smt_backend/sail_plugin_smt.ml
index 3b530a9c4..4ada592f9 100644
--- a/src/sail_smt_backend/sail_plugin_smt.ml
+++ b/src/sail_smt_backend/sail_plugin_smt.ml
@@ -64,30 +64,42 @@ let set_smt_auto_solver arg =
let smt_options =
[
- ("-smt_auto", Arg.Tuple [Arg.Set opt_smt_auto], " automatically call the smt solver on generated SMT");
- ( "-smt_auto_solver",
+ ( Flag.create ~prefix:["smt"] "auto",
+ Arg.Tuple [Arg.Set opt_smt_auto],
+ "automatically call the smt solver on generated SMT"
+ );
+ ( Flag.create ~prefix:["smt"] ~arg:"cvc4/cvc5/z3" "auto_solver",
Arg.Tuple [Arg.Set opt_smt_auto; Arg.String set_smt_auto_solver],
- " set the solver to use for counterexample checks (default cvc5)"
+ "set the solver to use for counterexample checks (default cvc5)"
+ );
+ ( Flag.create ~prefix:["smt"] "ignore_overflow",
+ Arg.Set opt_smt_ignore_overflow,
+ "ignore integer overflow in generated SMT"
);
- ("-smt_ignore_overflow", Arg.Set opt_smt_ignore_overflow, " ignore integer overflow in generated SMT");
- ( "-smt_int_size",
+ ( Flag.create ~prefix:["smt"] ~arg:"n" "int_size",
Arg.String (fun n -> opt_smt_unknown_integer_width := int_of_string n),
- " set a bound of n on the maximum integer bitwidth for generated SMT (default 128)"
+ "set a bound of n on the maximum integer bitwidth for generated SMT (default 128)"
);
- ("-smt_propagate_vars", Arg.Unit (fun () -> ()), " (deprecated) propgate variables through generated SMT");
- ( "-smt_bits_size",
+ ( Flag.create ~prefix:["smt"] "propagate_vars",
+ Arg.Unit (fun () -> ()),
+ "(deprecated) propgate variables through generated SMT"
+ );
+ ( Flag.create ~prefix:["smt"] ~arg:"n" "bits_size",
Arg.String (fun n -> opt_smt_unknown_bitvector_width := int_of_string n),
- " set a size bound of n for unknown-length bitvectors in generated SMT (default 64)"
+ "set a size bound of n for unknown-length bitvectors in generated SMT (default 64)"
);
- ( "-smt_vector_size",
+ ( Flag.create ~prefix:["smt"] ~arg:"n" "vector_size",
Arg.String (fun n -> opt_smt_unknown_generic_vector_width := int_of_string n),
- " set a bound of 2 ^ n for generic vectors in generated SMT (default 5)"
+ "set a bound of 2 ^ n for generic vectors in generated SMT (default 5)"
);
- ( "-smt_include",
+ ( Flag.create ~prefix:["smt"] ~arg:"filename" "include",
Arg.String (fun i -> opt_smt_includes := i :: !opt_smt_includes),
- " insert additional file in SMT output"
+ "insert additional file in SMT output"
+ );
+ ( Flag.create ~prefix:["smt"] "disable_specialization",
+ Arg.Clear opt_smt_specialize,
+ "Disable generic specialization when generating SMT"
);
- ("-smt_disable_specialization", Arg.Clear opt_smt_specialize, " Disable generic specialization when generating SMT");
]
let smt_rewrites =
diff --git a/src/sail_sv_backend/sail_plugin_sv.ml b/src/sail_sv_backend/sail_plugin_sv.ml
index c73f9626a..6af55cc08 100644
--- a/src/sail_sv_backend/sail_plugin_sv.ml
+++ b/src/sail_sv_backend/sail_plugin_sv.ml
@@ -108,23 +108,23 @@ let opt_disable_optimizations = ref false
let verilog_options =
[
- ( "-sv_output_dir",
+ ( Flag.create ~prefix:["sv"] ~arg:"path" "output_dir",
Arg.String (fun s -> opt_output_dir := Some s),
- " set the output directory for generated SystemVerilog files"
+ "set the output directory for generated SystemVerilog files"
);
- ( "-sv_include",
+ ( Flag.create ~prefix:["sv"] ~arg:"file" "include",
Arg.String (fun s -> opt_includes := s :: !opt_includes),
- " add include directive to generated SystemVerilog file"
+ "add include directive to generated SystemVerilog file"
);
- ( "-sv_toplevel",
+ ( Flag.create ~prefix:["sv"] ~arg:"id" "toplevel",
Arg.String
(fun s ->
Specialize.add_initial_calls (IdSet.singleton (mk_id s));
opt_toplevel := s
),
- " Sail function to use as toplevel module"
+ "Sail function to use as toplevel module"
);
- ( "-sv_verilate",
+ ( Flag.create ~prefix:["sv"] ~arg:"compile|run" "verilate",
Arg.String
(fun opt ->
if opt = "run" then opt_verilate := Verilator_run
@@ -135,59 +135,65 @@ let verilog_options =
"Invalid argument for -sv_verilate option. Valid options are either 'run' or 'compile'."
)
),
- " Invoke verilator on generated output"
+ "Invoke verilator on generated output"
);
- ( "-sv_verilate_args",
+ ( Flag.create ~prefix:["sv"] ~arg:"string" "verilate_args",
Arg.String (fun s -> append_flag opt_verilate_args s),
- " Extra arguments to pass to verilator"
+ "Extra arguments to pass to verilator"
);
- ( "-sv_verilate_cflags",
+ ( Flag.create ~prefix:["sv"] ~arg:"string" "verilate_cflags",
Arg.String (fun s -> append_flag opt_verilate_cflags s),
- " Verilator CFLAGS argument"
+ "Verilator CFLAGS argument"
);
- ( "-sv_verilate_ldflags",
+ ( Flag.create ~prefix:["sv"] ~arg:"string" "verilate_ldflags",
Arg.String (fun s -> append_flag opt_verilate_ldflags s),
- " Verilator LDFLAGS argument"
+ "Verilator LDFLAGS argument"
);
- ( "-sv_verilate_link_sail_runtime",
+ ( Flag.create ~prefix:["sv"] "verilate_link_sail_runtime",
Arg.Set opt_verilate_link_sail_runtime,
- " Link the Sail C runtime with the generated verilator C++"
+ "Link the Sail C runtime with the generated verilator C++"
);
- ("-sv_verilate_jobs", Arg.Int (fun i -> opt_verilate_jobs := i), " Provide the -j option to verilator");
- ("-sv_lines", Arg.Set opt_line_directives, " output `line directives");
- ("-sv_comb", Arg.Set opt_comb, " output an always_comb block instead of initial block");
- ("-sv_inregs", Arg.Set opt_inregs, " take register values from inputs");
- ("-sv_outregs", Arg.Set opt_outregs, " output register values");
- ( "-sv_int_size",
+ ( Flag.create ~prefix:["sv"] ~arg:"n" "verilate_jobs",
+ Arg.Int (fun i -> opt_verilate_jobs := i),
+ "Provide the -j option to verilator"
+ );
+ (Flag.create ~prefix:["sv"] "lines", Arg.Set opt_line_directives, "output `line directives");
+ (Flag.create ~prefix:["sv"] "comb", Arg.Set opt_comb, "output an always_comb block instead of initial block");
+ (Flag.create ~prefix:["sv"] "inregs", Arg.Set opt_inregs, "take register values from inputs");
+ (Flag.create ~prefix:["sv"] "outregs", Arg.Set opt_outregs, "output register values");
+ ( Flag.create ~prefix:["sv"] ~arg:"n" "int_size",
Arg.Int (fun i -> opt_max_unknown_integer_width := i),
- " set the maximum width for unknown integers"
+ "set the maximum width for unknown integers"
);
- ( "-sv_bits_size",
+ ( Flag.create ~prefix:["sv"] ~arg:"n" "bits_size",
Arg.Int (fun i -> opt_max_unknown_bitvector_width := i),
- " set the maximum width for bitvectors with unknown width"
+ "set the maximum width for bitvectors with unknown width"
);
- ("-sv_no_strings", Arg.Set opt_no_strings, " don't emit any strings, instead emit units");
- ("-sv_no_packed", Arg.Set opt_no_packed, " don't emit packed datastructures");
- ("-sv_no_assertions", Arg.Set opt_no_assertions, " ignore all Sail asserts");
- ("-sv_never_pack_unions", Arg.Set opt_never_pack_unions, " never emit a packed union");
- ("-sv_padding", Arg.Set opt_padding, " add padding on packed unions");
- ( "-sv_unreachable",
+ (Flag.create ~prefix:["sv"] "no_strings", Arg.Set opt_no_strings, "don't emit any strings, instead emit units");
+ (Flag.create ~prefix:["sv"] "no_packed", Arg.Set opt_no_packed, "don't emit packed datastructures");
+ (Flag.create ~prefix:["sv"] "no_assertions", Arg.Set opt_no_assertions, "ignore all Sail asserts");
+ (Flag.create ~prefix:["sv"] "never_pack_unions", Arg.Set opt_never_pack_unions, "never emit a packed union");
+ (Flag.create ~prefix:["sv"] "padding", Arg.Set opt_padding, "add padding on packed unions");
+ ( Flag.create ~prefix:["sv"] ~arg:"functionname" "unreachable",
Arg.String (fun fn -> opt_unreachable := fn :: !opt_unreachable),
- " Mark function as unreachable."
+ "Mark function as unreachable."
);
- ("-sv_nomem", Arg.Set opt_nomem, " don't emit a dynamic memory implementation");
- ( "-sv_fun2wires",
+ (Flag.create ~prefix:["sv"] "nomem", Arg.Set opt_nomem, "don't emit a dynamic memory implementation");
+ ( Flag.create ~prefix:["sv"] ~arg:"functionname" "fun2wires",
Arg.String (fun fn -> opt_fun2wires := fn :: !opt_fun2wires),
- " Use input/output ports instead of emitting a function call"
+ "Use input/output ports instead of emitting a function call"
);
- ( "-sv_specialize",
+ ( Flag.create ~prefix:["sv"] ~arg:"n" "specialize",
Arg.Int (fun i -> opt_int_specialize := Some i),
- " Run n specialization passes on Sail Int-kinded type variables"
+ "Run n specialization passes on Sail Int-kinded type variables"
+ );
+ ( Flag.create ~prefix:["sv"] "disable_optimizations",
+ Arg.Set opt_disable_optimizations,
+ "disable SystemVerilog specific optimizations"
);
- ("-sv_disable_optimizations", Arg.Set opt_disable_optimizations, " disable SystemVerilog specific optimizations");
- ( "-sv_dpi",
+ ( Flag.create ~prefix:["sv"] ~arg:"set" "dpi",
Arg.String (fun s -> opt_dpi_sets := StringSet.add s !opt_dpi_sets),
- " Use SystemVerilog DPI-C for a set of primitives (e.g. memory)"
+ "Use SystemVerilog DPI-C for a set of primitives (e.g. memory)"
);
]