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.

Sign up for GitHub

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

Jump to bottom

Minor CLI and CT checker cleanups #786

Merged
merged 3 commits into from
Apr 22, 2024
Merged

Minor CLI and CT checker cleanups #786

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
084a599
Make CLI options print pretty.
J08nY Feb 23, 2024
e19e6a5
Remove unused module.
J08nY Feb 21, 2024
e8e3eae
Fix typo.
J08nY Mar 7, 2024
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
7 changes: 3 additions & 4 deletions compiler/src/ct_checker_forward.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -34,7 +34,6 @@ end = struct
end

module Svl : Set.S with type elt = Vl.t = Set.Make(Vl)
module Mvl : Map.S with type key = Vl.t = Map.Make(Vl)

type level =
| Secret
Expand Down Expand Up @@ -541,15 +540,15 @@ let get_annot ensure_annot f =
(* -----------------------------------------------------------*)
let sdeclassify = "declassify"

let is_declasify annot =
let is_declassify annot =
Annot.ensure_uniq1 sdeclassify Annot.none annot <> None

let declassify_lvl annot lvl =
if is_declasify annot then Public
if is_declassify annot then Public
else lvl

let declassify_lvls annot lvls =
if is_declasify annot then List.map (fun _ -> Public) lvls
if is_declassify annot then List.map (fun _ -> Public) lvls
else lvls

(* [ty_instr env i] return env' such that env |- i : env' *)
Expand Down
104 changes: 52 additions & 52 deletions compiler/src/glob_options.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ type color = | Auto | Always | Never
let color = ref Auto

let ct_list = ref None
let infer = ref false
let infer = ref false

let sct_list = ref None

Expand Down Expand Up @@ -190,72 +190,72 @@ let set_sct_comp_pass s =

let print_option p =
let s, msg = print_strings p in
("-p"^s, Arg.Unit (set_printing p), "print program after "^msg)
("-p"^s, Arg.Unit (set_printing p), " Print program after "^msg)

let stop_after_option p =
let s, msg = print_strings p in
("-until_"^s, Arg.Unit (set_stop_after p), "stop after "^msg)
("-until_"^s, Arg.Unit (set_stop_after p), " Stop after "^msg)

let options = [
"-version" , Arg.Set help_version , "display version information about this compiler (and exits)";
"-o" , Arg.Set_string outfile, "[filename]: name of the output file";
"-g" , Arg.Set dwarf , "emit DWARF2 line number information";
"-debug" , Arg.Set debug , ": print debug information";
"-timings" , Arg.Set timings , ": print a timestamp and elapsed time after each pass";
"-I" , Arg.String set_idirs , "[ident:path]: bind ident to path for from ident require ...";
"-latex" , Arg.Set_string latexfile, "[filename]: generate the corresponding LATEX file (deprecated)";
"-lea" , Arg.Set lea , ": use lea as much as possible (default is nolea)";
"-nolea" , Arg.Clear lea , ": try to use add and mul instead of lea";
"-set0" , Arg.Set set0 , ": use [xor x x] to set x to 0 (default is not)";
"-noset0" , Arg.Clear set0 , ": do not use set0 option";
"-ec" , Arg.String set_ec , "[f]: extract function [f] and its dependencies to an easycrypt file";
"-oec" , Arg.Set_string ecfile , "[filename]: use filename as output destination for easycrypt extraction";
"-oecarray" , Arg.String set_ec_array_path, "[dir]: output easycrypt array theories to the given path";
"-CT" , Arg.Unit set_constTime , ": generates model for constant time verification";
"-checkCT", Arg.Unit set_ct , ": checks that the full program is constant time (using a type system) (deprecated)";
"-checkCTon", Arg.String set_ct_on , "[f]: checks that the function [f] is constant time (using a type system) (deprecated)";
"-infer" , Arg.Set infer , "infers security level annotations of the constant time type system (deprecated)";
J08nY marked this conversation as resolved.
Show resolved Hide resolved
"-checkSCT", Arg.Unit set_sct , ": checks that the full program is speculative constant time (using a type system)";
"-checkSCTon", Arg.String set_sct_on, "[f]: checks that the function [f] is speculative constant time (using a type system)";
"-checkSCTafter", Arg.Symbol(compiler_step_symbol, set_sct_comp_pass), "start sct checker after given pass";
"-slice" , Arg.String set_slice , "[f]: keep function [f] and all what it needs";
"-safety", Arg.Unit set_safety , ": generates model for safety verification";
"-checksafety", Arg.Unit set_checksafety, ": automatically check for safety";
"-version" , Arg.Set help_version , " Display version information about this compiler (and exit)";
"-o" , Arg.Set_string outfile, "[filename] Name of the output file";
"-g" , Arg.Set dwarf , " Emit DWARF2 line number information";
"-debug" , Arg.Set debug , " Print debug information";
"-timings" , Arg.Set timings , " Print a timestamp and elapsed time after each pass";
"-I" , Arg.String set_idirs , "[ident:path] Bind ident to path for from ident require ...";
"-latex" , Arg.Set_string latexfile, "[filename] Generate the corresponding LATEX file (deprecated)";
"-lea" , Arg.Set lea , " Use lea as much as possible (default is nolea)";
"-nolea" , Arg.Clear lea , " Try to use add and mul instead of lea";
"-set0" , Arg.Set set0 , " Use [xor x x] to set x to 0 (default is not)";
"-noset0" , Arg.Clear set0 , " Do not use set0 option";
"-ec" , Arg.String set_ec , "[f] Extract function [f] and its dependencies to an easycrypt file";
"-oec" , Arg.Set_string ecfile , "[filename] Use filename as output destination for easycrypt extraction";
"-oecarray" , Arg.String set_ec_array_path, "[dir] Output easycrypt array theories to the given path";
"-CT" , Arg.Unit set_constTime , " Generate model for constant time verification";
"-checkCT", Arg.Unit set_ct , " Check that the full program is constant time (using a type system) (deprecated)";
"-checkCTon", Arg.String set_ct_on , "[f] Check that the function [f] is constant time (using a type system) (deprecated)";
"-infer" , Arg.Set infer , " Infer security level annotations of the constant time type system (deprecated)";
"-checkSCT", Arg.Unit set_sct , " Check that the full program is speculative constant time (using a type system)";
"-checkSCTon", Arg.String set_sct_on, "[f] Check that the function [f] is speculative constant time (using a type system)";
"-checkSCTafter", Arg.Symbol(compiler_step_symbol, set_sct_comp_pass), " Run SCT checker after the given pass";
"-slice" , Arg.String set_slice , "[f] Keep function [f] and everything it needs";
"-safety", Arg.Unit set_safety , " Generate model for safety verification";
"-checksafety", Arg.Unit set_checksafety, " Automatically check for safety";
"-safetyparam", Arg.String set_safetyparam,
"parameter for automatic safety verification:\n \
" Parameter for automatic safety verification:\n \
format: \"f_1>param_1|f_2>param_2|...\" \
where each param_i is of the form:\n \
pt_1,...,pt_n;len_1,...,len_k\n \
pt_1,...,pt_n: input pointers of f_i\n \
len_1,...,len_k: input lengths of f_i";
"-safetyconfig", Arg.String set_safetyconfig, "[filename]: use filename (JSON) as configuration file for the safety checker";
"-safetymakeconfigdoc", Arg.String set_safety_makeconfigdoc, "[dir]: make the safety checker configuration docs in [dir]";
"-nocheckalignment", Arg.Set trust_aligned, "do not report alignment issue as safety violations";
"-wlea", Arg.Unit (add_warning UseLea), ": print warning when lea is used";
"-w_" , Arg.Unit (add_warning IntroduceNone), ": print warning when extra _ is introduced";
"-wea", Arg.Unit (add_warning ExtraAssignment), ": print warning when extra assignment is introduced";
"-winsertarraycopy", Arg.Unit (add_warning IntroduceArrayCopy), ": print warning when array copy is introduced";
"-wduplicatevar", Arg.Unit (add_warning DuplicateVar), ": print warning when two variables share the same name";
"-wunusedvar", Arg.Unit (add_warning UnusedVar), ": print warning when a variable is not used";
"-noinsertarraycopy", Arg.Clear introduce_array_copy, ": do not automatically insert array copy";
"-nowarning", Arg.Unit (nowarning), ": do no print warning";
"-color", Arg.Symbol (["auto"; "always"; "never"], set_color), ": print messages with color";
"-help-intrinsics", Arg.Set help_intrinsics, "List the set of intrinsic operators";
"-print-stack-alloc", Arg.Set print_stack_alloc, ": print the results of the stack allocation OCaml oracle";
"-lazy-regalloc", Arg.Set lazy_regalloc, "\tAllocate variables to registers in program order";
"-pall" , Arg.Unit set_all_print, "print program after each compilation steps";
"-print-dependencies", Arg.Set print_dependencies, ": print dependencies and exit";
"-intel", Arg.Unit (set_syntax `Intel), "use intel syntax (default is AT&T)";
"-ATT", Arg.Unit (set_syntax `ATT), "use AT&T syntax (default is AT&T)";
"-call-conv", Arg.Symbol (["windows"; "linux"], set_cc), ": select calling convention (default depend on host architecture)";
"-arch", Arg.Symbol (["x86-64"; "arm-m4"], set_target_arch), ": select target arch (default is x86-64)";
"-safetyconfig", Arg.String set_safetyconfig, "[filename] Use filename (JSON) as configuration file for the safety checker";
"-safetymakeconfigdoc", Arg.String set_safety_makeconfigdoc, "[dir] Make the safety checker configuration docs in [dir]";
"-nocheckalignment", Arg.Set trust_aligned, " Do not report alignment issue as safety violations";
"-wlea", Arg.Unit (add_warning UseLea), " Print warning when lea is used";
"-w_" , Arg.Unit (add_warning IntroduceNone), " Print warning when extra _ is introduced";
"-wea", Arg.Unit (add_warning ExtraAssignment), " Print warning when extra assignment is introduced";
"-winsertarraycopy", Arg.Unit (add_warning IntroduceArrayCopy), " Print warning when array copy is introduced";
"-wduplicatevar", Arg.Unit (add_warning DuplicateVar), " Print warning when two variables share the same name";
"-wunusedvar", Arg.Unit (add_warning UnusedVar), " Print warning when a variable is not used";
"-noinsertarraycopy", Arg.Clear introduce_array_copy, " Do not automatically insert array copy";
"-nowarning", Arg.Unit (nowarning), " Do no print warnings";
"-color", Arg.Symbol (["auto"; "always"; "never"], set_color), " Print messages with color";
"-help-intrinsics", Arg.Set help_intrinsics, " List the set of intrinsic operators (and exit)";
"-print-stack-alloc", Arg.Set print_stack_alloc, " Print the results of the stack allocation OCaml oracle";
"-lazy-regalloc", Arg.Set lazy_regalloc, " Allocate variables to registers in program order";
"-pall" , Arg.Unit set_all_print, " Print program after each compilation steps";
"-print-dependencies", Arg.Set print_dependencies, " Print dependencies and exit";
"-intel", Arg.Unit (set_syntax `Intel), " Use intel syntax (default is AT&T)";
"-ATT", Arg.Unit (set_syntax `ATT), " Use AT&T syntax (default is AT&T)";
"-call-conv", Arg.Symbol (["windows"; "linux"], set_cc), " Select calling convention (default depends on host architecture)";
"-arch", Arg.Symbol (["x86-64"; "arm-m4"], set_target_arch), " Select target arch (default is x86-64)";
"-stack-zero",
Arg.Symbol (List.map fst stack_zero_strategies, set_stack_zero_strategy),
": select stack zeroization strategy for export functions";
" Select stack zeroization strategy for export functions";
"-stack-zero-size",
Arg.Symbol (List.map fst Annot.ws_strings, set_stack_zero_size),
": select stack zeroization size for export functions";
"-pliveness", Arg.Set print_liveness, ": print liveness information during register allocation"
" Select stack zeroization size for export functions";
"-pliveness", Arg.Set print_liveness, " Print liveness information during register allocation"
] @ List.map print_option Compiler.compiler_step_list @ List.map stop_after_option Compiler.compiler_step_list

let usage_msg = "Usage : jasminc [option] filename"
Expand Down
4 changes: 2 additions & 2 deletions compiler/src/main_compiler.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ let parse () =
(* Set default option values *)
if Sys.win32 then set_cc "windows";
(* Parse command-line arguments *)
Arg.parse options set_in usage_msg;
Arg.parse (Arg.align options) set_in usage_msg;
let c =
match !color with
| Auto -> Unix.isatty (Unix.descr_of_out_channel stderr)
Expand Down Expand Up @@ -284,7 +284,7 @@ let main () =
exit 1

| UsageError ->
Arg.usage options usage_msg;
Arg.usage (Arg.align options) usage_msg;
exit 1

| CLIerror e ->
Expand Down
6 changes: 3 additions & 3 deletions compiler/src/sct_checker_forward.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -926,7 +926,7 @@ let ty_lvals env (msf_e : msf_e) xs tys : msf_e =

let sdeclassify = "declassify"

let is_declasify annot =
let is_declassify annot =
Annot.ensure_uniq1 sdeclassify Annot.none annot <> None

let declassify_lvl env (_, s) = (Env.public env, s)
Expand All @@ -935,11 +935,11 @@ let declassify env = function
| Direct le -> Direct (declassify_lvl env le)
| Indirect (lp, le) -> Indirect (lp, declassify_lvl env le)

let declassify_ty env annot ty = if is_declasify annot
let declassify_ty env annot ty = if is_declassify annot
then declassify env ty
else ty

let declassify_tys env annot tys = if is_declasify annot
let declassify_tys env annot tys = if is_declassify annot
then List.map (declassify env) tys
else tys

Expand Down