Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refactor command line flag handling for plugins #842

Merged
merged 1 commit into from
Dec 18, 2024
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion src/bin/sail.ml
Original file line number Diff line number Diff line change
@@ -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)

64 changes: 64 additions & 0 deletions src/lib/flag.ml
Original file line number Diff line number Diff line change
@@ -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)
51 changes: 51 additions & 0 deletions src/lib/flag.mli
Original file line number Diff line number Diff line change
@@ -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
6 changes: 3 additions & 3 deletions src/lib/target.ml
Original file line number Diff line number Diff line change
@@ -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;
4 changes: 2 additions & 2 deletions src/lib/target.mli
Original file line number Diff line number Diff line change
@@ -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
56 changes: 31 additions & 25 deletions src/sail_c_backend/sail_plugin_c.ml
Original file line number Diff line number Diff line change
@@ -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 =
51 changes: 25 additions & 26 deletions src/sail_coq_backend/sail_plugin_coq.ml
Original file line number Diff line number Diff line change
@@ -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"
);
]

Loading