Improve Help Menu (#4109)

1. Group options by category. We already have structs in the source code
to do this (e.g. `CommonArgs`), so I just followed that structure. The
goal is to make it easier for users to tell what the options do--I don't
think it's currently clear that some of these arguments are for Cargo,
for example. Open to bikeshedding on the section names--I think "Common
Options" is a bit vague but couldn't think of anything better.
2. For each category, put its entries in alphabetical order.

New output from `cargo kani -h` below. Note that
#4110 will hide some of these
options.

```
cmzech@80a9971b5e20 playground % cargo kani -h    
Verify a Rust crate. For more information, see https://github.com/model-checking/kani

Usage: cargo-kani [OPTIONS] [COMMAND]

Commands:
  autoharness  Create and run harnesses automatically for eligible functions. Implies -Z function-contracts and -Z loop-contracts. See https://model-checking.github.io/kani/reference/experimental/autoharness.html for documentation
  list         List contracts and harnesses
  playback     Execute concrete playback testcases of a local package
  help         Print this message or the help of the given subcommand(s)

Options:
  -h, --help     Print help (see more with '--help')
  -V, --version  Print version

Verification Options:
      --cbmc-args [<CBMC_ARGS>...]
          Pass through directly to CBMC; must be the last flag. This feature is unstable and it requires `-Z unstable-options` to be used
      --concrete-playback <CONCRETE_PLAYBACK>
          Generate concrete playback unit test. If value supplied is 'print', Kani prints the unit test to stdout. If value supplied is 'inplace', Kani automatically adds the unit test to your source code. This option does not work with `--output-format old` [possible values: print, inplace]
      --default-unwind <DEFAULT_UNWIND>
          Specify the value used for loop unwinding in CBMC
      --exact
          When specified, the harness filter will only match the exact fully qualified name of a harness
      --fail-fast
          Stop the verification process as soon as one of the harnesses fails
      --force-build
          Force Kani to rebuild all packages before the verification
      --harness <HARNESS_FILTER>
          If specified, only run harnesses that match this filter. This option can be provided multiple times, which will run all tests matching any of the filters. If used with --exact, the harness filter will only match the exact fully qualified name of a harness
      --harness-timeout <HARNESS_TIMEOUT>
          Timeout for each harness with optional suffix ('s': seconds, 'm': minutes, 'h': hours). Default is seconds. This option is experimental and requires `-Z unstable-options` to be used
      --no-assertion-reach-checks
          Turn off assertion reachability checks
      --output-format <OUTPUT_FORMAT>
          Toggle between different styles of output [default: regular] [possible values: regular, terse, old]
      --randomize-layout [<RANDOMIZE_LAYOUT>]
          Randomize the layout of structures. This option can help catching code that relies on a specific layout chosen by the compiler that is not guaranteed to be stable in the future. If a value is given, it will be used as the seed for randomization See the `-Z randomize-layout` and `-Z layout-seed` arguments of the rust compiler
      --solver <SOLVER>
          Specify the CBMC solver to use. Overrides the harness `solver` attribute. If no solver is specified (with --solver or harness attribute), Kani will use CaDiCaL [possible values: cadical, kissat, minisat, bin=<SAT_SOLVER_BINARY>]
      --target-dir <TARGET_DIR>
          Directory for all generated artifacts
      --tests
          Enable test function verification. Only use this option when the entry point is a test function
      --unwind <UNWIND>
          Specify the value used for loop unwinding for the specified harness in CBMC

Memory Checks:
      --default-checks                Turn on all default checks
      --no-default-checks             Turn off all default checks
      --memory-safety-checks          Turn on default memory safety checks
      --no-memory-safety-checks       Turn off default memory safety checks
      --overflow-checks               Turn on default overflow checks
      --no-overflow-checks            Turn off default overflow checks
      --undefined-function-checks     Turn on undefined function checks
      --no-undefined-function-checks  Turn off undefined function checks
      --unwinding-checks              Turn on default unwinding checks
      --no-unwinding-checks           Turn off default unwinding checks

Common Options:
      --debug                        Produce full debug information
  -q, --quiet                        Produces no output, just an exit code and requested artifacts; overrides --verbose
  -v, --verbose                      Output processing stages and commands, along with minor debug information
  -Z, --unstable <UNSTABLE_FEATURE>  [possible values: async-lib, autoharness, concrete-playback, c-ffi, float-lib, function-contracts, gen-c, ghost-state, lean, list, loop-contracts, mem-predicates, restrict-vtable, source-coverage, stubbing, uninit-checks, unstable-options, valid-value-checks]

Cargo Common Options:
      --all-features          Activate all package features
  -e, --exclude <EXCLUDE>...  Exclude the specified packages
  -F, --features <FEATURES>   Comma separated list of package features to activate
      --manifest-path <PATH>  Path to Cargo.toml
      --no-default-features   Do not activate the `default` feature
  -p, --package <PACKAGE>...  Run Kani on the specified packages (see `cargo help pkgid` for the accepted format)
      --workspace             Build all packages in the workspace

Cargo Target Options:
      --bin <BIN>  Check only the specified binary target
      --bins       Check all binaries
      --lib        Check only the package's library unit tests
```

Resolves #1951

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: Carolyn Zech

kani-driver/src/args/cargo.rs

@@ -12,13 +12,15 @@ use std::path::PathBuf;
 /// These do not (currently) include cargo args that kani pays special attention to:
 /// for instance, we keep `--tests` and `--target-dir` elsewhere.
 #[derive(Debug, Default, clap::Args)]
+#[clap(next_help_heading = "Cargo Common Options")]
 pub struct CargoCommonArgs {
     /// Activate all package features
     #[arg(long)]
     pub all_features: bool,
-    /// Do not activate the `default` feature
-    #[arg(long)]
-    pub no_default_features: bool,
+
+    /// Exclude the specified packages
+    #[arg(long, short, requires("workspace"), conflicts_with("package"), num_args(1..))]
+    pub exclude: Vec<String>,
 
     // This tolerates spaces too, but we say "comma" only because this is the least error-prone approach...
     /// Comma separated list of package features to activate
@@ -29,17 +31,17 @@ pub struct CargoCommonArgs {
     #[arg(long, name = "PATH")]
     pub manifest_path: Option<PathBuf>,
 
-    /// Build all packages in the workspace
+    /// Do not activate the `default` feature
     #[arg(long)]
-    pub workspace: bool,
+    pub no_default_features: bool,
 
     /// Run Kani on the specified packages (see `cargo help pkgid` for the accepted format)
     #[arg(long, short, conflicts_with("workspace"), num_args(1..))]
     pub package: Vec<String>,
 
-    /// Exclude the specified packages
-    #[arg(long, short, requires("workspace"), conflicts_with("package"), num_args(1..))]
-    pub exclude: Vec<String>,
+    /// Build all packages in the workspace
+    #[arg(long)]
+    pub workspace: bool,
 }
 
 impl CargoCommonArgs {
@@ -98,6 +100,7 @@ impl ValidateArgs for CargoCommonArgs {
 /// See <https://doc.rust-lang.org/cargo/commands/cargo-test.html#target-selection> for more
 /// details.
 #[derive(Debug, Default, clap::Args)]
+#[clap(next_help_heading = "Cargo Target Options")]
 pub struct CargoTargetArgs {
     /// Check only the specified binary target.
     #[arg(long)]

kani-driver/src/args/common.rs

@@ -7,6 +7,7 @@ pub use kani_metadata::{EnabledUnstableFeatures, UnstableFeature};
 
 /// Common Kani arguments that we expect to be included in most subcommands.
 #[derive(Debug, clap::Args)]
+#[clap(next_help_heading = "Common Options")]
 pub struct CommonArgs {
     /// Produce full debug information
     #[arg(long)]

kani-driver/src/args/mod.rs

@@ -141,14 +141,14 @@ pub struct StandaloneArgs {
 /// When no subcommand is provided, there is an implied verification subcommand.
 #[derive(Debug, clap::Subcommand)]
 pub enum StandaloneSubcommand {
+    /// Create and run harnesses automatically for eligible functions. Implies -Z function-contracts and -Z loop-contracts.
+    Autoharness(Box<autoharness_args::StandaloneAutoharnessArgs>),
+    /// List contracts and harnesses.
+    List(Box<list_args::StandaloneListArgs>),
     /// Execute concrete playback testcases of a local crate.
     Playback(Box<playback_args::KaniPlaybackArgs>),
     /// Verify the rust standard library.
     VerifyStd(Box<std_args::VerifyStdArgs>),
-    /// List contracts and harnesses.
-    List(Box<list_args::StandaloneListArgs>),
-    /// Create and run harnesses automatically for eligible functions. Implies -Z function-contracts and -Z loop-contracts.
-    Autoharness(Box<autoharness_args::StandaloneAutoharnessArgs>),
 }
 
 #[derive(Debug, clap::Parser)]
@@ -172,102 +172,95 @@ pub enum CargoKaniSubcommand {
     #[command(hide = true)]
     Assess(Box<crate::assess::AssessArgs>),
 
-    /// Execute concrete playback testcases of a local package.
-    Playback(Box<playback_args::CargoPlaybackArgs>),
+    /// Create and run harnesses automatically for eligible functions. Implies -Z function-contracts and -Z loop-contracts.
+    /// See https://model-checking.github.io/kani/reference/experimental/autoharness.html for documentation.
+    Autoharness(Box<autoharness_args::CargoAutoharnessArgs>),
 
     /// List contracts and harnesses.
     List(Box<list_args::CargoListArgs>),
 
-    /// Create and run harnesses automatically for eligible functions. Implies -Z function-contracts and -Z loop-contracts.
-    /// See https://model-checking.github.io/kani/reference/experimental/autoharness.html for documentation.
-    Autoharness(Box<autoharness_args::CargoAutoharnessArgs>),
+    /// Execute concrete playback testcases of a local package.
+    Playback(Box<playback_args::CargoPlaybackArgs>),
 }
 
 // Common arguments for invoking Kani for verification purpose. This gets put into KaniContext,
 // whereas anything above is "local" to "main"'s control flow.
 #[derive(Debug, clap::Args)]
+#[clap(next_help_heading = "Verification Options")]
 pub struct VerificationArgs {
     /// Temporary option to trigger assess mode for out test suite
     /// where we are able to add options but not subcommands
     #[arg(long, hide = true)]
     pub assess: bool,
 
+    /// Link external C files referenced by Rust code.
+    /// This is an experimental feature and requires `-Z c-ffi` to be used
+    #[arg(long, hide = true, num_args(1..))]
+    pub c_lib: Vec<PathBuf>,
+
+    /// Pass through directly to CBMC; must be the last flag.
+    /// This feature is unstable and it requires `-Z unstable-options` to be used
+    #[arg(
+        long,
+        allow_hyphen_values = true,
+        num_args(0..)
+    )]
+    // consumes everything
+    pub cbmc_args: Vec<OsString>,
+
     /// Generate concrete playback unit test.
     /// If value supplied is 'print', Kani prints the unit test to stdout.
     /// If value supplied is 'inplace', Kani automatically adds the unit test to your source code.
     /// This option does not work with `--output-format old`.
     #[arg(long, ignore_case = true, value_enum)]
     pub concrete_playback: Option<ConcretePlaybackMode>,
-    /// Keep temporary files generated throughout Kani process. This is already the default
-    /// behavior for `cargo-kani`.
+
+    /// Enable Kani coverage output alongside verification result
     #[arg(long, hide_short_help = true)]
-    pub keep_temps: bool,
+    pub coverage: bool,
 
-    /// Generate C file equivalent to inputted program for debug purpose.
-    /// This feature is unstable, and it requires `-Z unstable-options` to be used
+    /// Specify the value used for loop unwinding in CBMC
+    #[arg(long)]
+    pub default_unwind: Option<u32>,
+
+    /// When specified, the harness filter will only match the exact fully qualified name of a harness
+    #[arg(long, requires("harnesses"))]
+    pub exact: bool,
+
+    /// Enable extra pointer checks such as invalid pointers in relation operations and pointer
+    /// arithmetic overflow.
+    /// This feature is unstable and it may yield false counter examples. It requires
+    /// `-Z unstable-options` to be used
     #[arg(long, hide_short_help = true)]
-    pub gen_c: bool,
+    pub extra_pointer_checks: bool,
 
-    /// Directory for all generated artifacts.
+    /// Stop the verification process as soon as one of the harnesses fails.
     #[arg(long)]
-    pub target_dir: Option<PathBuf>,
+    pub fail_fast: bool,
 
     /// Force Kani to rebuild all packages before the verification.
     #[arg(long)]
     pub force_build: bool,
 
-    /// Toggle between different styles of output
-    #[arg(long, default_value = "regular", ignore_case = true, value_enum)]
-    pub output_format: OutputFormat,
-
-    #[command(flatten)]
-    pub checks: CheckArgs,
+    /// Generate C file equivalent to inputted program for debug purpose.
+    /// This feature is unstable, and it requires `-Z unstable-options` to be used
+    #[arg(long, hide_short_help = true)]
+    pub gen_c: bool,
 
     /// If specified, only run harnesses that match this filter. This option can be provided
     /// multiple times, which will run all tests matching any of the filters.
     /// If used with --exact, the harness filter will only match the exact fully qualified name of a harness.
     #[arg(long = "harness", num_args(1), value_name = "HARNESS_FILTER")]
     pub harnesses: Vec<String>,
 
-    /// When specified, the harness filter will only match the exact fully qualified name of a harness
-    #[arg(long, requires("harnesses"))]
-    pub exact: bool,
-
-    /// Link external C files referenced by Rust code.
-    /// This is an experimental feature and requires `-Z c-ffi` to be used
-    #[arg(long, hide = true, num_args(1..))]
-    pub c_lib: Vec<PathBuf>,
-    /// Enable test function verification. Only use this option when the entry point is a test function
+    /// Timeout for each harness with optional suffix ('s': seconds, 'm': minutes, 'h': hours). Default is seconds. This option is experimental and requires `-Z unstable-options` to be used.
     #[arg(long)]
-    pub tests: bool,
-    /// Kani will only compile the crate. No verification will be performed
-    #[arg(long, hide_short_help = true)]
-    pub only_codegen: bool,
+    pub harness_timeout: Option<Timeout>,
 
-    /// Run Kani without codegen. Useful for quick feedback on whether the code would compile successfully (similar to `cargo check`).
-    /// This feature is unstable and requires `-Z unstable-options` to be used
+    /// Do not error out for crates containing `global_asm!`.
+    /// This option may impact the soundness of the analysis and may cause false proofs and/or counterexamples
     #[arg(long, hide_short_help = true)]
-    pub no_codegen: bool,
-
-    /// Specify the value used for loop unwinding in CBMC
-    #[arg(long)]
-    pub default_unwind: Option<u32>,
-    /// Specify the value used for loop unwinding for the specified harness in CBMC
-    #[arg(long, requires("harnesses"))]
-    pub unwind: Option<u32>,
-    /// Specify the CBMC solver to use. Overrides the harness `solver` attribute.
-    /// If no solver is specified (with --solver or harness attribute), Kani will use CaDiCaL.
-    #[arg(long, value_parser = CbmcSolverValueParser::new(CbmcSolver::VARIANTS))]
-    pub solver: Option<CbmcSolver>,
-    /// Pass through directly to CBMC; must be the last flag.
-    /// This feature is unstable and it requires `-Z unstable-options` to be used
-    #[arg(
-        long,
-        allow_hyphen_values = true,
-        num_args(0..)
-    )]
-    // consumes everything
-    pub cbmc_args: Vec<OsString>,
+    pub ignore_global_asm: bool,
 
     /// Number of threads to spawn to verify harnesses in parallel.
     /// Omit the flag entirely to run sequentially (i.e. one thread).
@@ -276,80 +269,99 @@ pub struct VerificationArgs {
     #[arg(short, long, hide_short_help = true)]
     pub jobs: Option<Option<usize>>,
 
-    /// Enable extra pointer checks such as invalid pointers in relation operations and pointer
-    /// arithmetic overflow.
-    /// This feature is unstable and it may yield false counter examples. It requires
-    /// `-Z unstable-options` to be used
+    /// Keep temporary files generated throughout Kani process. This is already the default
+    /// behavior for `cargo-kani`.
     #[arg(long, hide_short_help = true)]
-    pub extra_pointer_checks: bool,
+    pub keep_temps: bool,
 
-    /// Restrict the targets of virtual table function pointer calls.
-    /// This feature is unstable and it requires `-Z restrict-vtable` to be used
-    #[arg(long, hide = true, conflicts_with = "no_restrict_vtable")]
-    pub restrict_vtable: bool,
-    /// Disable restricting the targets of virtual table function pointer calls
+    /// Do not assert the function contracts of dependencies. Requires -Z function-contracts.
     #[arg(long, hide_short_help = true)]
-    pub no_restrict_vtable: bool,
+    pub no_assert_contracts: bool,
+
     /// Turn off assertion reachability checks
     #[arg(long)]
     pub no_assertion_reach_checks: bool,
 
-    /// Do not error out for crates containing `global_asm!`.
-    /// This option may impact the soundness of the analysis and may cause false proofs and/or counterexamples
+    /// Run Kani without codegen. Useful for quick feedback on whether the code would compile successfully (similar to `cargo check`).
+    /// This feature is unstable and requires `-Z unstable-options` to be used
     #[arg(long, hide_short_help = true)]
-    pub ignore_global_asm: bool,
-
-    /// Write the GotoC symbol table to a file in JSON format instead of goto binary format.
-    #[arg(long, hide = true)]
-    pub write_json_symtab: bool,
+    pub no_codegen: bool,
 
-    /// Execute CBMC's sanity checks to ensure the goto-program we generate is correct.
+    /// Disable restricting the targets of virtual table function pointer calls
     #[arg(long, hide_short_help = true)]
-    pub run_sanity_checks: bool,
+    pub no_restrict_vtable: bool,
 
     /// Disable CBMC's slice formula which prevents values from being assigned to redundant variables in traces.
     #[arg(long, hide_short_help = true)]
     pub no_slice_formula: bool,
 
-    /// Synthesize loop contracts for all loops.
-    #[arg(
-        long,
-        hide_short_help = true,
-        conflicts_with("unwind"),
-        conflicts_with("default_unwind")
-    )]
-    pub synthesize_loop_contracts: bool,
-
-    /// Do not assert the function contracts of dependencies. Requires -Z function-contracts.
+    /// Kani will only compile the crate. No verification will be performed
     #[arg(long, hide_short_help = true)]
-    pub no_assert_contracts: bool,
+    pub only_codegen: bool,
+
+    /// Toggle between different styles of output
+    #[arg(long, default_value = "regular", ignore_case = true, value_enum)]
+    pub output_format: OutputFormat,
 
-    //Harness Output into individual files
+    /// Write verification results into per-harness files, rather than to stdout
     #[arg(long, hide_short_help = true)]
     pub output_into_files: bool,
 
+    /// Print final LLBC for Lean backend. This requires the `-Z lean` option.
+    #[arg(long, hide = true)]
+    pub print_llbc: bool,
+
     /// Randomize the layout of structures. This option can help catching code that relies on
     /// a specific layout chosen by the compiler that is not guaranteed to be stable in the future.
     /// If a value is given, it will be used as the seed for randomization
     /// See the `-Z randomize-layout` and `-Z layout-seed` arguments of the rust compiler.
     #[arg(long)]
     pub randomize_layout: Option<Option<u64>>,
 
-    /// Enable Kani coverage output alongside verification result
+    /// Restrict the targets of virtual table function pointer calls.
+    /// This feature is unstable and it requires `-Z restrict-vtable` to be used
+    #[arg(long, hide = true, conflicts_with = "no_restrict_vtable")]
+    pub restrict_vtable: bool,
+
+    /// Execute CBMC's sanity checks to ensure the goto-program we generate is correct.
     #[arg(long, hide_short_help = true)]
-    pub coverage: bool,
+    pub run_sanity_checks: bool,
 
-    /// Print final LLBC for Lean backend. This requires the `-Z lean` option.
-    #[arg(long, hide = true)]
-    pub print_llbc: bool,
+    /// Specify the CBMC solver to use. Overrides the harness `solver` attribute.
+    /// If no solver is specified (with --solver or harness attribute), Kani will use CaDiCaL.
+    #[arg(long, value_parser = CbmcSolverValueParser::new(CbmcSolver::VARIANTS))]
+    pub solver: Option<CbmcSolver>,
 
-    /// Timeout for each harness with optional suffix ('s': seconds, 'm': minutes, 'h': hours). Default is seconds. This option is experimental and requires `-Z unstable-options` to be used.
+    /// Synthesize loop contracts for all loops.
+    #[arg(
+        long,
+        hide_short_help = true,
+        conflicts_with("unwind"),
+        conflicts_with("default_unwind")
+    )]
+    pub synthesize_loop_contracts: bool,
+
+    /// Directory for all generated artifacts.
     #[arg(long)]
-    pub harness_timeout: Option<Timeout>,
+    pub target_dir: Option<PathBuf>,
 
-    /// Stop the verification process as soon as one of the harnesses fails.
+    /// Enable test function verification. Only use this option when the entry point is a test function
     #[arg(long)]
-    pub fail_fast: bool,
+    pub tests: bool,
+
+    /// Specify the value used for loop unwinding for the specified harness in CBMC
+    #[arg(long, requires("harnesses"))]
+    pub unwind: Option<u32>,
+
+    /// Write the GotoC symbol table to a file in JSON format instead of goto binary format.
+    #[arg(long, hide = true)]
+    pub write_json_symtab: bool,
+
+    #[command(flatten)]
+    pub checks: CheckArgs,
+
+    #[command(flatten)]
+    pub common_args: CommonArgs,
 
     /// Arguments to pass down to Cargo
     #[command(flatten)]
@@ -358,9 +370,6 @@ pub struct VerificationArgs {
     /// Arguments used to select Cargo target.
     #[command(flatten)]
     pub target: CargoTargetArgs,
-
-    #[command(flatten)]
-    pub common_args: CommonArgs,
 }
 
 impl VerificationArgs {
@@ -421,6 +430,7 @@ pub enum OutputFormat {
 }
 
 #[derive(Debug, clap::Args)]
+#[clap(next_help_heading = "Memory Checks")]
 pub struct CheckArgs {
     // Rust argument parsers (/clap) don't have the convenient '--flag' and '--no-flag' boolean pairs, so approximate
     // We're put both here then create helper functions to "intepret"