Minor CLI and CT checker cleanups

[J08nY]

Extracted these from #736.

[vbgl]

You may want to add yourself to the AUTHORS file.

I don’t understand the purpose of the first commit.

[J08nY]

By using Arg.align the first commit prints the help nicely aligned:

Usage : jasminc [option] filename
  -version                   Display version information about this compiler (and exit)
  -o [filename]              Name of the output file
  -g                         Emit DWARF2 line number information
  -debug                     Print debug information
  -timings                   Print a timestamp and elapsed time after each pass
  -I [ident:path]            Bind ident to path for from ident require ...
  -latex [filename]          Generate the corresponding LATEX file (deprecated)
  -lea                       Use lea as much as possible (default is nolea)
  -nolea                     Try to use add and mul instead of lea
  -set0                      Use [xor x x] to set x to 0 (default is not)
  -noset0                    Do not use set0 option
  -ec [f]                    Extract function [f] and its dependencies to an easycrypt file
  -oec [filename]            Use filename as output destination for easycrypt extraction
  -oecarray [dir]            Output easycrypt array theories to the given path
  -CT                        Generate model for constant time verification
  -checkCT                   Check that the full program is constant time (using a type system)
  -checkCTon [f]             Check that the function [f] is constant time (using a type system)
  -infer                     Infer security level annotations of the constant time type system
  -checkSCT                  Check that the full program is speculative constant time (using a type system)
  -checkSCTon [f]            Check that the function [f] is speculative constant time (using a type system)
  -checkSCTafter {typing|cstexp|arraycopy|addarrinit|lowerspill|inline|rmfunc|unroll|splitting|renaming|rmphi|renamingd|rmarrinit|makeref|arrexp|rmglobals|lowering|slhlowering|propagate|stkalloc|rmreturn|ralloc|rallocd|linear|stackzero|tunnel|asm}
                             Run SCT checker after the given pass
  -slice [f]                 Keep function [f] and everything it needs
  -safety                    Generate model for safety verification
  -checksafety               Automatically check for safety
  -safetyparam               Parameter for automatic safety verification:
    format: "f_1>param_1|f_2>param_2|..." where each param_i is of the form:
    pt_1,...,pt_n;len_1,...,len_k
    pt_1,...,pt_n: input pointers of f_i
    len_1,...,len_k: input lengths of f_i
  -safetyconfig [filename]   Use filename (JSON) as configuration file for the safety checker
  -safetymakeconfigdoc [dir] Make the safety checker configuration docs in [dir]
  -nocheckalignment          Do not report alignment issue as safety violations
  -wlea                      Print warning when lea is used
  -w_                        Print warning when extra _ is introduced
  -wea                       Print warning when extra assignment is introduced
  -winsertarraycopy          Print warning when array copy is introduced
  -wduplicatevar             Print warning when two variables share the same name
  -wunusedvar                Print warning when a variable is not used
  -noinsertarraycopy         Do not automatically insert array copy
  -nowarning                 Do no print warnings
  -color {auto|always|never}
                             Print messages with color
  -help-intrinsics           List the set of intrinsic operators (and exit)
  -print-stack-alloc         Print the results of the stack allocation OCaml oracle
  -lazy-regalloc             Allocate variables to registers in program order
  -pall                      Print program after each compilation steps
  -print-dependencies        Print dependencies and exit
  -intel                     Use intel syntax (default is AT&T)
  -ATT                       Use AT&T syntax (default is AT&T)
  -call-conv {windows|linux}
                             Select calling convention (default depends on host architecture)
  -arch {x86-64|arm-m4}
                             Select target arch (default is x86-64)
  -stack-zero {loop|loopSCT|unrolled}
                             Select stack zeroization strategy for export functions
  -stack-zero-size {u8|u16|u32|u64|u128|u256}
                             Select stack zeroization size for export functions
  -pliveness                 Print liveness information during register allocation
  -ptyping                   Print program after typing
  -pcstexp                   Print program after param expansion
  -parraycopy                Print program after array copy
  -paddarrinit               Print program after add array initialisation
  -plowerspill               Print program after lower spill/unspill instructions
  -pinline                   Print program after inlining
  -prmfunc                   Print program after remove unused function
  -punroll                   Print program after unrolling
  -psplitting                Print program after liverange splitting
  -prenaming                 Print program after variable renaming to remove copies
  -prmphi                    Print program after remove phi nodes introduced by splitting
  -prenamingd                Print program after dead code after variable renaming to remove copies
  -prmarrinit                Print program after remove array initialisation
  -pmakeref                  Print program after add assignments before and after call to ensure that arguments and results are ref ptr
  -parrexp                   Print program after expansion of register arrays
  -prmglobals                Print program after remove globals variables
  -plowering                 Print program after lowering of instructions
  -pslhlowering              Print program after selective load hardening lowering of instructions
  -ppropagate                Print program after propagate inline variables
  -pstkalloc                 Print program after stack allocation
  -prmreturn                 Print program after remove unused returned values
  -pralloc                   Print program after register allocation
  -prallocd                  Print program after dead code after register allocation
  -plinear                   Print program after linearization
  -pstackzero                Print program after stack zeroization
  -ptunnel                   Print program after tunneling
  -pasm                      Print program after generation of assembly
  -until_typing              Stop after typing
  -until_cstexp              Stop after param expansion
  -until_arraycopy           Stop after array copy
  -until_addarrinit          Stop after add array initialisation
  -until_lowerspill          Stop after lower spill/unspill instructions
  -until_inline              Stop after inlining
  -until_rmfunc              Stop after remove unused function
  -until_unroll              Stop after unrolling
  -until_splitting           Stop after liverange splitting
  -until_renaming            Stop after variable renaming to remove copies
  -until_rmphi               Stop after remove phi nodes introduced by splitting
  -until_renamingd           Stop after dead code after variable renaming to remove copies
  -until_rmarrinit           Stop after remove array initialisation
  -until_makeref             Stop after add assignments before and after call to ensure that arguments and results are ref ptr
  -until_arrexp              Stop after expansion of register arrays
  -until_rmglobals           Stop after remove globals variables
  -until_lowering            Stop after lowering of instructions
  -until_slhlowering         Stop after selective load hardening lowering of instructions
  -until_propagate           Stop after propagate inline variables
  -until_stkalloc            Stop after stack allocation
  -until_rmreturn            Stop after remove unused returned values
  -until_ralloc              Stop after register allocation
  -until_rallocd             Stop after dead code after register allocation
  -until_linear              Stop after linearization
  -until_stackzero           Stop after stack zeroization
  -until_tunnel              Stop after tunneling
  -until_asm                 Stop after generation of assembly
  -help                      Display this list of options
  --help                     Display this list of options

For that to work, some characters at the start of the help text needed to be changed.

To me, that is much more readable than the current help (that mixes case, seperators and is not aligned):

Usage : jasminc [option] filename
  -version display version information about this compiler (and exits)
  -o [filename]: name of the output file
  -g emit DWARF2 line number information
  -debug : print debug information
  -timings : print a timestamp and elapsed time after each pass
  -I [ident:path]: bind ident to path for from ident require ...
  -latex [filename]: generate the corresponding LATEX file (deprecated)
  -lea : use lea as much as possible (default is nolea)
  -nolea : try to use add and mul instead of lea
  -set0 : use [xor x x] to set x to 0 (default is not)
  -noset0 : do not use set0 option
  -ec [f]: extract function [f] and its dependencies to an easycrypt file
  -oec [filename]: use filename as output destination for easycrypt extraction
  -oecarray [dir]: output easycrypt array theories to the given path
  -CT : generates model for constant time verification
  -checkCT : checks that the full program is constant time (using a type system) (deprecated)
  -checkCTon [f]: checks that the function [f] is constant time (using a type system) (deprecated)
  -infer infers security level annotations of the constant time type system (deprecated)
  -checkSCT : checks that the full program is speculative constant time (using a type system)
  -checkSCTon [f]: checks that the function [f] is speculative constant time (using a type system)
  -checkSCTafter {typing|cstexp|arraycopy|addarrinit|lowerspill|inline|rmfunc|unroll|splitting|renaming|rmphi|renamingd|rmarrinit|makeref|arrexp|rmglobals|lowering|slhlowering|propagate|stkalloc|rmreturn|ralloc|rallocd|linear|stackzero|tunnel|asm}start sct checker after given pass
  -slice [f]: keep function [f] and all what it needs
  -safety : generates model for safety verification
  -checksafety : automatically check for safety
  -safetyparam parameter for automatic safety verification:
    format: "f_1>param_1|f_2>param_2|..." where each param_i is of the form:
    pt_1,...,pt_n;len_1,...,len_k
    pt_1,...,pt_n: input pointers of f_i
    len_1,...,len_k: input lengths of f_i
  -safetyconfig [filename]: use filename (JSON) as configuration file for the safety checker
  -safetymakeconfigdoc [dir]: make the safety checker configuration docs in [dir]
  -nocheckalignment do not report alignment issue as safety violations
  -wlea : print warning when lea is used
  -w_ : print warning when extra _ is introduced
  -wea : print warning when extra assignment is introduced
  -winsertarraycopy : print warning when array copy is introduced
  -wduplicatevar : print warning when two variables share the same name
  -wunusedvar : print warning when a variable is not used
  -noinsertarraycopy : do not automatically insert array copy
  -nowarning : do no print warning
  -color {auto|always|never}: print messages with color
  -help-intrinsics List the set of intrinsic operators
  -print-stack-alloc : print the results of the stack allocation OCaml oracle
  -lazy-regalloc 	Allocate variables to registers in program order
  -pall print program after each compilation steps
  -print-dependencies : print dependencies and exit
  -intel use intel syntax (default is AT&T)
  -ATT use AT&T syntax (default is AT&T)
  -call-conv {windows|linux}: select calling convention (default depend on host architecture)
  -arch {x86-64|arm-m4}: select target arch (default is x86-64)
  -stack-zero {loop|loopSCT|unrolled}: select stack zeroization strategy for export functions
  -stack-zero-size {u8|u16|u32|u64|u128|u256}: select stack zeroization size for export functions
  -pliveness : print liveness information during register allocation
  -ptyping print program after typing
  -pcstexp print program after param expansion
  -parraycopy print program after array copy
  -paddarrinit print program after add array initialisation
  -plowerspill print program after lower spill/unspill instructions
  -pinline print program after inlining
  -prmfunc print program after remove unused function
  -punroll print program after unrolling
  -psplitting print program after liverange splitting
  -prenaming print program after variable renaming to remove copies
  -prmphi print program after remove phi nodes introduced by splitting
  -prenamingd print program after dead code after variable renaming to remove copies
  -prmarrinit print program after remove array initialisation
  -pmakeref print program after add assignments before and after call to ensure that arguments and results are ref ptr
  -parrexp print program after expansion of register arrays
  -prmglobals print program after remove globals variables
  -plowering print program after lowering of instructions
  -pslhlowering print program after selective load hardening lowering of instructions
  -ppropagate print program after propagate inline variables
  -pstkalloc print program after stack allocation
  -prmreturn print program after remove unused returned values
  -pralloc print program after register allocation
  -prallocd print program after dead code after register allocation
  -plinear print program after linearization
  -pstackzero print program after stack zeroization
  -ptunnel print program after tunneling
  -pasm print program after generation of assembly
  -until_typing stop after typing
  -until_cstexp stop after param expansion
  -until_arraycopy stop after array copy
  -until_addarrinit stop after add array initialisation
  -until_lowerspill stop after lower spill/unspill instructions
  -until_inline stop after inlining
  -until_rmfunc stop after remove unused function
  -until_unroll stop after unrolling
  -until_splitting stop after liverange splitting
  -until_renaming stop after variable renaming to remove copies
  -until_rmphi stop after remove phi nodes introduced by splitting
  -until_renamingd stop after dead code after variable renaming to remove copies
  -until_rmarrinit stop after remove array initialisation
  -until_makeref stop after add assignments before and after call to ensure that arguments and results are ref ptr
  -until_arrexp stop after expansion of register arrays
  -until_rmglobals stop after remove globals variables
  -until_lowering stop after lowering of instructions
  -until_slhlowering stop after selective load hardening lowering of instructions
  -until_propagate stop after propagate inline variables
  -until_stkalloc stop after stack allocation
  -until_rmreturn stop after remove unused returned values
  -until_ralloc stop after register allocation
  -until_rallocd stop after dead code after register allocation
  -until_linear stop after linearization
  -until_stackzero stop after stack zeroization
  -until_tunnel stop after tunneling
  -until_asm stop after generation of assembly
  -help  Display this list of options
  --help  Display this list of options

[vbgl]

At least, before your change, it is clear that humans are not expected to read the output of -help.

[vbgl]

I still don’t like the first commit, but that’s probably a matter of taste.