From fd18b93bd5e3ed27ff01e7eb538ef84c4480af3e Mon Sep 17 00:00:00 2001 From: Alasdair Date: Wed, 18 Dec 2024 17:34:15 +0000 Subject: [PATCH] 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 | 2 +- src/lib/flag.ml | 64 +++++++++++++++ src/lib/flag.mli | 51 ++++++++++++ src/lib/target.ml | 6 +- src/lib/target.mli | 4 +- src/sail_c_backend/sail_plugin_c.ml | 56 ++++++++------ src/sail_coq_backend/sail_plugin_coq.ml | 51 ++++++------ src/sail_doc_backend/sail_plugin_doc.ml | 35 +++++---- src/sail_latex_backend/sail_plugin_latex.ml | 13 ++-- src/sail_lean_backend/sail_plugin_lean.ml | 8 +- src/sail_lem_backend/sail_plugin_lem.ml | 31 +++++--- src/sail_ocaml_backend/sail_plugin_ocaml.ml | 34 ++++---- src/sail_output/sail_plugin_output.ml | 6 +- src/sail_smt_backend/sail_plugin_smt.ml | 40 ++++++---- src/sail_sv_backend/sail_plugin_sv.ml | 86 +++++++++++---------- 15 files changed, 323 insertions(+), 164 deletions(-) create mode 100644 src/lib/flag.ml create mode 100644 src/lib/flag.mli 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)" ); ]