Skip to content

Commit fd18b93

Browse files
AlasdairAlasdair
committed
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`.
1 parent 304b491 commit fd18b93

File tree

15 files changed

+323
-164
lines changed

15 files changed

+323
-164
lines changed

‎src/bin/sail.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,7 @@ let add_target_header plugin opts =
149149
let load_plugin opts plugin =
150150
try
151151
if is_bytecode then Dynlink.loadfile plugin else Dynlink.loadfile_private plugin;
152-
let plugin_opts = Target.extract_options () |> fix_options |> target_align in
152+
let plugin_opts = Target.extract_options () |> List.map Flag.to_arg |> fix_options |> target_align in
153153
opts := add_target_header plugin !opts @ plugin_opts
154154
with Dynlink.Error msg -> prerr_endline ("Failed to load plugin " ^ plugin ^ ": " ^ Dynlink.error_message msg)
155155

‎src/lib/flag.ml‎

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
(****************************************************************************)
2+
(* Sail *)
3+
(* *)
4+
(* Sail and the Sail architecture models here, comprising all files and *)
5+
(* directories except the ASL-derived Sail code in the aarch64 directory, *)
6+
(* are subject to the BSD two-clause licence below. *)
7+
(* *)
8+
(* The ASL derived parts of the ARMv8.3 specification in *)
9+
(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *)
10+
(* *)
11+
(* Copyright (c) 2013-2021 *)
12+
(* Kathyrn Gray *)
13+
(* Shaked Flur *)
14+
(* Stephen Kell *)
15+
(* Gabriel Kerneis *)
16+
(* Robert Norton-Wright *)
17+
(* Christopher Pulte *)
18+
(* Peter Sewell *)
19+
(* Alasdair Armstrong *)
20+
(* Brian Campbell *)
21+
(* Thomas Bauereiss *)
22+
(* Anthony Fox *)
23+
(* Jon French *)
24+
(* Dominic Mulligan *)
25+
(* Stephen Kell *)
26+
(* Mark Wassell *)
27+
(* Alastair Reid (Arm Ltd) *)
28+
(* *)
29+
(* All rights reserved. *)
30+
(* *)
31+
(* This work was partially supported by EPSRC grant EP/K008528/1 <a *)
32+
(* href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous *)
33+
(* Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA *)
34+
(* KTF funding, and donations from Arm. This project has received *)
35+
(* funding from the European Research Council (ERC) under the European *)
36+
(* Union’s Horizon 2020 research and innovation programme (grant *)
37+
(* agreement No 789108, ELVER). *)
38+
(* *)
39+
(* This software was developed by SRI International and the University of *)
40+
(* Cambridge Computer Laboratory (Department of Computer Science and *)
41+
(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *)
42+
(* and FA8750-10-C-0237 ("CTSRD"). *)
43+
(* *)
44+
(* SPDX-License-Identifier: BSD-2-Clause *)
45+
(****************************************************************************)
46+
47+
open Arg
48+
49+
type t = { prefix : string list; hide_prefix : bool; debug : bool; hide : bool; arg : string option; key : string }
50+
51+
let create ?(prefix = []) ?(hide_prefix = false) ?(debug = false) ?(hide = false) ?arg key =
52+
{ prefix; hide_prefix; debug; hide; arg; key }
53+
54+
let underscore_sep = Util.string_of_list "_" (fun s -> s)
55+
56+
let to_arg (flag, spec, doc) =
57+
let apply_prefix key =
58+
match flag.prefix with [] -> key | _ when flag.hide_prefix -> key | _ -> underscore_sep flag.prefix ^ "_" ^ key
59+
in
60+
let key =
61+
"-" ^ if flag.key = "" then underscore_sep flag.prefix else (if flag.debug then "d" else "") ^ apply_prefix flag.key
62+
in
63+
let arg_prefix = match flag.arg with Some desc -> "<" ^ desc ^ "> " | None -> " " in
64+
(key, spec, if flag.hide then "" else arg_prefix ^ (if flag.debug then "(debug) " else "") ^ doc)

‎src/lib/flag.mli‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,51 @@
1+
(****************************************************************************)
2+
(* Sail *)
3+
(* *)
4+
(* Sail and the Sail architecture models here, comprising all files and *)
5+
(* directories except the ASL-derived Sail code in the aarch64 directory, *)
6+
(* are subject to the BSD two-clause licence below. *)
7+
(* *)
8+
(* The ASL derived parts of the ARMv8.3 specification in *)
9+
(* aarch64/no_vector and aarch64/full are copyright ARM Ltd. *)
10+
(* *)
11+
(* Copyright (c) 2013-2021 *)
12+
(* Kathyrn Gray *)
13+
(* Shaked Flur *)
14+
(* Stephen Kell *)
15+
(* Gabriel Kerneis *)
16+
(* Robert Norton-Wright *)
17+
(* Christopher Pulte *)
18+
(* Peter Sewell *)
19+
(* Alasdair Armstrong *)
20+
(* Brian Campbell *)
21+
(* Thomas Bauereiss *)
22+
(* Anthony Fox *)
23+
(* Jon French *)
24+
(* Dominic Mulligan *)
25+
(* Stephen Kell *)
26+
(* Mark Wassell *)
27+
(* Alastair Reid (Arm Ltd) *)
28+
(* *)
29+
(* All rights reserved. *)
30+
(* *)
31+
(* This work was partially supported by EPSRC grant EP/K008528/1 <a *)
32+
(* href="http://www.cl.cam.ac.uk/users/pes20/rems">REMS: Rigorous *)
33+
(* Engineering for Mainstream Systems</a>, an ARM iCASE award, EPSRC IAA *)
34+
(* KTF funding, and donations from Arm. This project has received *)
35+
(* funding from the European Research Council (ERC) under the European *)
36+
(* Union’s Horizon 2020 research and innovation programme (grant *)
37+
(* agreement No 789108, ELVER). *)
38+
(* *)
39+
(* This software was developed by SRI International and the University of *)
40+
(* Cambridge Computer Laboratory (Department of Computer Science and *)
41+
(* Technology) under DARPA/AFRL contracts FA8650-18-C-7809 ("CIFV") *)
42+
(* and FA8750-10-C-0237 ("CTSRD"). *)
43+
(* *)
44+
(* SPDX-License-Identifier: BSD-2-Clause *)
45+
(****************************************************************************)
46+
47+
type t
48+
49+
val create : ?prefix:string list -> ?hide_prefix:bool -> ?debug:bool -> ?hide:bool -> ?arg:string -> string -> t
50+
51+
val to_arg : t * Arg.spec * string -> Arg.key * Arg.spec * Arg.doc

‎src/lib/target.ml‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ module StringMap = Map.Make (String)
5252

5353
type target = {
5454
name : string;
55-
options : (Arg.key * Arg.spec * Arg.doc) list;
55+
options : (Flag.t * Arg.spec * string) list;
5656
pre_parse_hook : unit -> unit;
5757
pre_initial_check_hook : string list -> unit;
5858
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
9393
prerr_endline ("Cannot use multiple Sail targets simultaneously: " ^ tgt ^ " and " ^ name);
9494
exit 1
9595
in
96-
let desc = match desc with Some desc -> desc | None -> " invoke the Sail " ^ name ^ " target" in
96+
let desc = match desc with Some desc -> desc | None -> "invoke the Sail " ^ name ^ " target" in
9797
let flag = match flag with Some flag -> flag | None -> name in
9898
let tgt =
9999
{
100100
name;
101-
options = ("-" ^ flag, Arg.Unit set_target, desc) :: options;
101+
options = (Flag.create ~prefix:[flag] "", Arg.Unit set_target, desc) :: options;
102102
pre_parse_hook;
103103
pre_initial_check_hook;
104104
pre_rewrites_hook;

‎src/lib/target.mli‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -106,7 +106,7 @@ val register :
106106
name:string ->
107107
?flag:string ->
108108
?description:string ->
109-
?options:(Arg.key * Arg.spec * Arg.doc) list ->
109+
?options:(Flag.t * Arg.spec * string) list ->
110110
?pre_parse_hook:(unit -> unit) ->
111111
?pre_initial_check_hook:(string list -> unit) ->
112112
?pre_rewrites_hook:(typed_ast -> Effects.side_effect_info -> Env.t -> unit) ->
@@ -130,4 +130,4 @@ val get : name:string -> target option
130130
val extract_registered : unit -> string list
131131

132132
(** Used internally to dynamically update the option list when loading plugins *)
133-
val extract_options : unit -> (Arg.key * Arg.spec * Arg.doc) list
133+
val extract_options : unit -> (Flag.t * Arg.spec * string) list

‎src/sail_c_backend/sail_plugin_c.ml‎

Lines changed: 31 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -53,39 +53,42 @@ let opt_specialize_c = ref false
5353

5454
let c_options =
5555
[
56-
( "-c_include",
56+
( Flag.create ~prefix:["c"] ~arg:"filename" "include",
5757
Arg.String (fun i -> opt_includes_c := i :: !opt_includes_c),
58-
"<filename> provide additional include for C output"
58+
"provide additional include for C output"
5959
);
60-
("-c_no_main", Arg.Set C_backend.opt_no_main, " do not generate the main() function");
61-
("-c_no_rts", Arg.Set C_backend.opt_no_rts, " do not include the Sail runtime");
62-
( "-c_no_lib",
60+
(Flag.create ~prefix:["c"] "no_main", Arg.Set C_backend.opt_no_main, "do not generate the main() function");
61+
(Flag.create ~prefix:["c"] "no_rts", Arg.Set C_backend.opt_no_rts, "do not include the Sail runtime");
62+
( Flag.create ~prefix:["c"] "no_lib",
6363
Arg.Tuple [Arg.Set C_backend.opt_no_lib; Arg.Set C_backend.opt_no_rts],
64-
" do not include the Sail runtime or library"
64+
"do not include the Sail runtime or library"
6565
);
66-
("-c_prefix", Arg.String (fun prefix -> C_backend.opt_prefix := prefix), "<prefix> prefix generated C functions");
67-
( "-c_extra_params",
66+
( Flag.create ~prefix:["c"] ~arg:"prefix" "prefix",
67+
Arg.String (fun prefix -> C_backend.opt_prefix := prefix),
68+
"prefix generated C functions"
69+
);
70+
( Flag.create ~prefix:["c"] ~arg:"parameters" "extra_params",
6871
Arg.String (fun params -> C_backend.opt_extra_params := Some params),
69-
"<parameters> generate C functions with additional parameters"
72+
"generate C functions with additional parameters"
7073
);
71-
( "-c_extra_args",
74+
( Flag.create ~prefix:["c"] ~arg:"arguments" "extra_args",
7275
Arg.String (fun args -> C_backend.opt_extra_arguments := Some args),
73-
"<arguments> supply extra argument to every generated C function call"
76+
"supply extra argument to every generated C function call"
7477
);
75-
("-c_specialize", Arg.Set opt_specialize_c, " specialize integer arguments in C output");
76-
( "-c_preserve",
78+
(Flag.create ~prefix:["c"] "specialize", Arg.Set opt_specialize_c, "specialize integer arguments in C output");
79+
( Flag.create ~prefix:["c"] "preserve",
7780
Arg.String (fun str -> Specialize.add_initial_calls (Ast_util.IdSet.singleton (Ast_util.mk_id str))),
78-
" make sure the provided function identifier is preserved in C output"
81+
"make sure the provided function identifier is preserved in C output"
7982
);
80-
( "-c_fold_unit",
83+
( Flag.create ~prefix:["c"] "fold_unit",
8184
Arg.String (fun str -> Constant_fold.opt_fold_to_unit := Util.split_on_char ',' str),
82-
" remove comma separated list of functions from C output, replacing them with unit"
85+
"remove comma separated list of functions from C output, replacing them with unit"
8386
);
84-
( "-c_coverage",
87+
( Flag.create ~prefix:["c"] ~arg:"file" "coverage",
8588
Arg.String (fun str -> C_backend.opt_branch_coverage := Some (open_out str)),
86-
"<file> Turn on coverage tracking and output information about all branches and functions to a file"
89+
"Turn on coverage tracking and output information about all branches and functions to a file"
8790
);
88-
( "-O",
91+
( Flag.create ~prefix:["c"] ~hide_prefix:true "O",
8992
Arg.Tuple
9093
[
9194
Arg.Set C_backend.optimize_primops;
@@ -94,17 +97,20 @@ let c_options =
9497
Arg.Set C_backend.optimize_struct_updates;
9598
Arg.Set C_backend.optimize_alias;
9699
],
97-
" turn on optimizations for C compilation"
100+
"turn on optimizations for C compilation"
98101
);
99-
( "-Ofixed_int",
102+
( Flag.create ~prefix:["c"] ~hide_prefix:true "Ofixed_int",
100103
Arg.Set C_backend.optimize_fixed_int,
101-
" assume fixed size integers rather than GMP arbitrary precision integers"
104+
"assume fixed size integers rather than GMP arbitrary precision integers"
102105
);
103-
( "-Ofixed_bits",
106+
( Flag.create ~prefix:["c"] ~hide_prefix:true "Ofixed_bits",
104107
Arg.Set C_backend.optimize_fixed_bits,
105-
" assume fixed size bitvectors rather than arbitrary precision bitvectors"
108+
"assume fixed size bitvectors rather than arbitrary precision bitvectors"
109+
);
110+
( Flag.create ~prefix:["c"] ~hide_prefix:true "static",
111+
Arg.Set C_backend.opt_static,
112+
"make generated C functions static"
106113
);
107-
("-static", Arg.Set C_backend.opt_static, " make generated C functions static");
108114
]
109115

110116
let c_rewrites =

‎src/sail_coq_backend/sail_plugin_coq.ml‎

Lines changed: 25 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -58,58 +58,57 @@ let opt_coq_lib_style : Pretty_print_coq.library_style option ref = ref None
5858

5959
let coq_options =
6060
[
61-
( "-coq_output_dir",
61+
( Flag.create ~prefix:["coq"] ~arg:"directory" "output_dir",
6262
Arg.String (fun dir -> opt_coq_output_dir := Some dir),
63-
"<directory> set a custom directory to output generated Coq"
63+
"set a custom directory to output generated Coq"
6464
);
65-
( "-coq_lib",
65+
( Flag.create ~prefix:["coq"] ~arg:"filename" "lib",
6666
Arg.String (fun l -> opt_libs_coq := l :: !opt_libs_coq),
67-
"<filename> provide additional library to open in Coq output"
67+
"provide additional library to open in Coq output"
6868
);
69-
( "-coq_alt_modules",
69+
( Flag.create ~prefix:["coq"] ~arg:"filename" "alt_modules",
7070
Arg.String (fun l -> opt_alt_modules_coq := l :: !opt_alt_modules_coq),
71-
"<filename> provide alternative modules to open in Coq output"
71+
"provide alternative modules to open in Coq output"
7272
);
73-
( "-coq_alt_modules2",
73+
( Flag.create ~prefix:["coq"] ~arg:"filename" "alt_modules2",
7474
Arg.String (fun l -> opt_alt_modules2_coq := l :: !opt_alt_modules2_coq),
75-
"<filename> provide additional alternative modules to open only in main (non-_types) Coq output, and suppress \
76-
default definitions of MR and M monads"
75+
"provide additional alternative modules to open only in main (non-_types) Coq output, and suppress default \
76+
definitions of MR and M monads"
7777
);
78-
( "-coq_extern_type",
78+
( Flag.create ~prefix:["coq"] ~arg:"typename" "extern_type",
7979
Arg.String Pretty_print_coq.(fun ty -> opt_extern_types := ty :: !opt_extern_types),
80-
"<typename> do not generate a definition for the type"
80+
"do not generate a definition for the type"
8181
);
82-
( "-coq_generate_extern_types",
82+
( Flag.create ~prefix:["coq"] "generate_extern_types",
8383
Arg.Set Pretty_print_coq.opt_generate_extern_types,
84-
" generate only extern types rather than suppressing them"
84+
"generate only extern types rather than suppressing them"
8585
);
86-
( "-coq_isla",
86+
( Flag.create ~prefix:["coq"] ~arg:"filename" "isla",
8787
Arg.String (fun fname -> opt_coq_isla := Some fname),
88-
"<filename> generate Coq code for decoding Isla trace values"
88+
"generate Coq code for decoding Isla trace values"
8989
);
90-
( "-coq_record_update",
90+
( Flag.create ~prefix:["coq"] "record_update",
9191
Arg.Set Pretty_print_coq.opt_coq_record_update,
92-
" use coq-record-update package's syntax for record updates"
92+
"use coq-record-update package's syntax for record updates"
9393
);
94-
( "-coq_lib_style",
94+
( Flag.create ~prefix:["coq"] "lib_style",
9595
Arg.Symbol
9696
( ["bbv"; "stdpp"],
9797
fun s -> opt_coq_lib_style := match s with "bbv" -> Some BBV | "stdpp" -> Some Stdpp | _ -> assert false
9898
),
99-
" select which style of Coq library to use (default: stdpp when the concurrency interfaces is used, bbv \
100-
otherwise)"
99+
"select which style of Coq library to use (default: stdpp when the concurrency interfaces is used, bbv otherwise)"
101100
);
102-
( "-dcoq_undef_axioms",
101+
( Flag.create ~prefix:["coq"] ~debug:true "undef_axioms",
103102
Arg.Set Pretty_print_coq.opt_undef_axioms,
104-
" (debug) generate axioms for functions that are declared but not defined"
103+
"generate axioms for functions that are declared but not defined"
105104
);
106-
( "-dcoq_warn_nonex",
105+
( Flag.create ~prefix:["coq"] ~debug:true "warn_nonex",
107106
Arg.Set Rewrites.opt_coq_warn_nonexhaustive,
108-
" (debug) generate warnings for non-exhaustive pattern matches in the Coq backend"
107+
"generate warnings for non-exhaustive pattern matches in the Coq backend"
109108
);
110-
( "-dcoq_debug_on",
109+
( Flag.create ~prefix:["coq"] ~arg:"function" ~debug:true "debug_on",
111110
Arg.String (fun f -> Pretty_print_coq.opt_debug_on := f :: !Pretty_print_coq.opt_debug_on),
112-
"<function> (debug) produce debug messages for Coq output on given function"
111+
"produce debug messages for Coq output on given function"
113112
);
114113
]
115114

0 commit comments

Comments
 (0)