Skip to content

Commit

Permalink
CN: Group comamnd line options
Browse files Browse the repository at this point in the history 
This commit groups the current CN options to make it clearer which are
used for what.

This could also be useful in preparation for switching to using
subcommands.
  • Loading branch information
@dc-mak
dc-mak committed Jul 14, 2024
1 parent e8a5fd5 commit a64e1b6
Showing 1 changed file with 132 additions and 125 deletions.
257 changes: 132 additions & 125 deletions backend/cn/main.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -239,10 +239,35 @@ open Cmdliner


(* some of these stolen from backend/driver *)
module Common_flags = struct
let file =
let doc = "Source C file" in
Arg.(required & pos ~rev:true 0 (some string) None & info [] ~docv:"FILE" ~doc)

(* copied from cerberus' executable (backend/driver/main.ml) *)
let macros =
let macro_pair =
let parser str =
match String.index_opt str '=' with
| None ->
Result.Ok (str, None)
| Some i ->
let macro = String.sub str 0 i in
let value = String.sub str (i+1) (String.length str - i - 1) in
let is_digit n = 48 <= n && n <= 57 in
if i = 0 || is_digit (Char.code (String.get macro 0)) then
Result.Error (`Msg "macro name must be a C identifier")
else
Result.Ok (macro, Some value) in
let printer ppf = function
| (m, None) -> Format.pp_print_string ppf m
| (m, Some v) -> Format.fprintf ppf "%s=%s" m v in
Arg.(conv (parser, printer)) in
let doc = "Adds an implicit #define into the predefines buffer which is \
read before the source file is preprocessed." in
Arg.(value & opt_all macro_pair [] & info ["D"; "define-macro"]
~docv:"NAME[=VALUE]" ~doc)

let incl_dirs =
let doc = "Add the specified directory to the search path for the\
C preprocessor." in
Expand All @@ -254,11 +279,6 @@ let incl_files =
read before the source file is preprocessed." in
Arg.(value & opt_all string [] & info ["include"] ~doc)

let loc_pp =
let doc = "Print pointer values as hexadecimal or as decimal values (hex | dec)" in
Arg.(value & opt (enum ["hex", Pp.Hex; "dec", Pp.Dec]) !Pp.loc_pp &
info ["locs"] ~docv:"HEX" ~doc)

let debug_level =
let doc = "Set the debug message level for cerberus to $(docv) (should range over [0-3])." in
Arg.(value & opt int 0 & info ["d"; "debug"] ~docv:"N" ~doc)
Expand All @@ -271,6 +291,38 @@ let print_sym_nums =
let doc = "Print numeric IDs of Cerberus symbols (variable names)." in
Arg.(value & flag & info ["n"; "print-sym-nums"] ~doc)

let no_timestamps =
let doc = "Disable timestamps in print-level debug messages" in
Arg.(value & flag & info ["no_timestamps"] ~doc)

(* copy-pasting from backend/driver/main.ml *)
let astprints =
let doc = "Pretty print the intermediate syntax tree for the listed languages \
(ranging over {cabs, ail, core, types})." in
Arg.(value & opt (list (enum [("cabs", Cabs); ("ail", Ail); ("core", Core); ("types", Types)])) [] &
info ["ast"] ~docv:"LANG1,..." ~doc)

let no_use_ity =
let doc = "(this switch should go away) in WellTyped.BaseTyping, do not use
integer type annotations placed by the Core elaboration" in
Arg.(value & flag & info["no-use-ity"] ~doc)

let no_inherit_loc =
let doc = "debugging: stop mucore terms inheriting location information from parents" in
Arg.(value & flag & info["no-inherit-loc"] ~doc)

let magic_comment_char_dollar =
let doc = "Override CN's default magic comment syntax to be \"/*\\$ ... \\$*/\"" in
Arg.(value & flag & info ["magic-comment-char-dollar"] ~doc)

end

module Verify_flags = struct
let loc_pp =
let doc = "Print pointer values as hexadecimal or as decimal values (hex | dec)" in
Arg.(value & opt (enum ["hex", Pp.Hex; "dec", Pp.Dec]) !Pp.loc_pp &
info ["locs"] ~docv:"HEX" ~doc)

let batch =
let doc = "Type check functions in batch/do not stop on first type error (unless `only` is used)" in
Arg.(value & flag & info ["batch"] ~doc)
Expand All @@ -283,19 +335,6 @@ let slow_smt_dir =
let doc = "Set the destination dir for logging slow smt queries (default is in system temp-dir)." in
Arg.(value & opt (some string) None & info ["slow-smt-dir"] ~docv:"FILE" ~doc)

let no_timestamps =
let doc = "Disable timestamps in print-level debug messages"
in
Arg.(value & flag & info ["no_timestamps"] ~doc)

let json =
let doc = "output in json format" in
Arg.(value & flag & info["json"] ~doc)

let output_dir =
let doc = "directory in which to output state files (overridden by --state-file)" in
Arg.(value & opt (some string) None & info ["output-dir"] ~docv:"FILE" ~doc)

let state_file =
let doc = "file in which to output the state" in
Arg.(value & opt (some string) None & info ["state-file"] ~docv:"FILE" ~doc)
Expand All @@ -304,10 +343,6 @@ let diag =
let doc = "explore branching diagnostics with key string" in
Arg.(value & opt (some string) None & info ["diag"] ~doc)

let lemmata =
let doc = "lemmata generation mode (target filename)" in
Arg.(value & opt (some string) None & info ["lemmata"] ~docv:"FILE" ~doc)

let csv_times =
let doc = "file in which to output csv timing information" in
Arg.(value & opt (some string) None & info ["times"] ~docv:"FILE" ~doc)
Expand All @@ -329,6 +364,20 @@ let solver_flags =
Arg.(value & opt (some (list string)) None
& info ["solver-flags"] ~docv:"X,Y,Z" ~doc)

let solver_path =
let doc = "Path to SMT solver executable" in
Arg.(value & opt (some string) None & info ["solver-path"] ~docv:"FILE" ~doc)

let solver_type =
let doc = "Specify the SMT solver interface" in
Arg.( value
& opt (some (enum [ "z3", Simple_smt.Z3
; "cvc5", Simple_smt.CVC5
]))
None
& info ["solver-type"] ~docv:"z3|cvc5" ~doc
)

let only =
let doc = "only type-check this function (or comma-separated names)" in
Arg.(value & opt (some string) None & info ["only"] ~doc)
Expand All @@ -337,7 +386,26 @@ let skip =
let doc = "skip type-checking of this function (or comma-separated names)" in
Arg.(value & opt (some string) None & info ["skip"] ~doc)

(* TODO remove this when VIP impl complete *)
let use_vip =
let doc = "use experimental VIP rules" in
Arg.(value & flag & info["vip"] ~doc)

let use_peval =
let doc = "(this switch should go away) run the Core partial evaluation phase" in
Arg.(value & flag & info["use-peval"] ~doc)

let json =
let doc = "output in json format" in
Arg.(value & flag & info["json"] ~doc)

let output_dir =
let doc = "directory in which to output state files (overridden by --state-file)" in
Arg.(value & opt (some string) None & info ["output-dir"] ~docv:"FILE" ~doc)

end

module Executable_spec_flags = struct
let output_decorated_dir =
let doc = "output a version of the translation unit decorated with C runtime
translations of the CN annotations to the provided directory" in
Expand All @@ -356,117 +424,56 @@ let copy_source_dir =
let doc = "Copy non-CN annotated files into output_decorated_dir for CN runtime testing" in
Arg.(value & flag & info ["copy_source_dir"] ~doc)

(* copy-pasting from backend/driver/main.ml *)
let astprints =
let doc = "Pretty print the intermediate syntax tree for the listed languages \
(ranging over {cabs, ail, core, types})." in
Arg.(value & opt (list (enum [("cabs", Cabs); ("ail", Ail); ("core", Core); ("types", Types)])) [] &
info ["ast"] ~docv:"LANG1,..." ~doc)

(* TODO remove this when VIP impl complete *)
let use_vip =
let doc = "use experimental VIP rules" in
Arg.(value & flag & info["vip"] ~doc)

let no_use_ity =
let doc = "(this switch should go away) in WellTyped.BaseTyping, do not use
integer type annotations placed by the Core elaboration" in
Arg.(value & flag & info["no-use-ity"] ~doc)

let use_peval =
let doc = "(this switch should go away) run the Core partial evaluation phase" in
Arg.(value & flag & info["use-peval"] ~doc)

let no_inherit_loc =
let doc = "debugging: stop mucore terms inheriting location information from parents" in
Arg.(value & flag & info["no-inherit-loc"] ~doc)

let magic_comment_char_dollar =
let doc = "Override CN's default magic comment syntax to be \"/*\\$ ... \\$*/\"" in
Arg.(value & flag & info ["magic-comment-char-dollar"] ~doc)

let solver_path =
let doc = "Path to SMT solver executable" in
Arg.(value & opt (some string) None & info ["solver-path"] ~docv:"FILE" ~doc)

let solver_type =
let doc = "Specify the SMT solver interface" in
Arg.( value
& opt (some (enum [ "z3", Simple_smt.Z3
; "cvc5", Simple_smt.CVC5
]))
None
& info ["solver-type"] ~docv:"z3|cvc5" ~doc
)


end

module Lemma = struct
let lemmata =
let doc = "lemmata generation mode (target filename)" in
Arg.(value & opt (some string) None & info ["lemmata"] ~docv:"FILE" ~doc)

end

(* copied from cerberus' executable (backend/driver/main.ml) *)
let macros =
let macro_pair =
let parser str =
match String.index_opt str '=' with
| None ->
Result.Ok (str, None)
| Some i ->
let macro = String.sub str 0 i in
let value = String.sub str (i+1) (String.length str - i - 1) in
let is_digit n = 48 <= n && n <= 57 in
if i = 0 || is_digit (Char.code (String.get macro 0)) then
Result.Error (`Msg "macro name must be a C identifier")
else
Result.Ok (macro, Some value) in
let printer ppf = function
| (m, None) -> Format.pp_print_string ppf m
| (m, Some v) -> Format.fprintf ppf "%s=%s" m v in
Arg.(conv (parser, printer)) in
let doc = "Adds an implicit #define into the predefines buffer which is \
read before the source file is preprocessed." in
Arg.(value & opt_all macro_pair [] & info ["D"; "define-macro"]
~docv:"NAME[=VALUE]" ~doc)

let () =
let open Term in
let check_t =
const main $
file $
macros $
incl_dirs $
incl_files $
loc_pp $
debug_level $
print_level $
print_sym_nums $
slow_smt_threshold $
slow_smt_dir $
no_timestamps $
json $
state_file $
output_dir $
diag $
lemmata $
only $
skip $
csv_times $
log_times $
random_seed $
solver_logging $
solver_flags $
solver_path $
solver_type $
output_decorated_dir $
output_decorated $
with_ownership_checking $
copy_source_dir $
astprints $
use_vip $
no_use_ity $
use_peval $
batch $
no_inherit_loc $
magic_comment_char_dollar
Common_flags.file $
Common_flags.macros $
Common_flags.incl_dirs $
Common_flags.incl_files $
Verify_flags.loc_pp $
Common_flags.debug_level $
Common_flags.print_level $
Common_flags.print_sym_nums $
Verify_flags.slow_smt_threshold $
Verify_flags.slow_smt_dir $
Common_flags.no_timestamps $
Verify_flags.json $
Verify_flags.state_file $
Verify_flags.output_dir $
Verify_flags.diag $
Lemma.lemmata $
Verify_flags.only $
Verify_flags.skip $
Verify_flags.csv_times $
Verify_flags.log_times $
Verify_flags.random_seed $
Verify_flags.solver_logging $
Verify_flags.solver_flags $
Verify_flags.solver_path $
Verify_flags.solver_type $
Executable_spec_flags.output_decorated_dir $
Executable_spec_flags.output_decorated $
Executable_spec_flags.with_ownership_checking $
Executable_spec_flags.copy_source_dir $
Common_flags.astprints $
Verify_flags.use_vip $
Common_flags.no_use_ity $
Verify_flags.use_peval $
Verify_flags.batch $
Common_flags.no_inherit_loc $
Common_flags.magic_comment_char_dollar
in
let version_str = "CN version: " ^ Cn_version.git_version in
let cn_info = Cmd.info "cn" ~version:version_str in
Expand Down

0 comments on commit a64e1b6

Please sign in to comment.