Improve handling of command line options

[nwatson22]

We should fix the codebase across pyk, kontrol, and evm-semantics to reduce the number of times default values for command options need to be specified, as per runtimeverification/kontrol#298 (review). Ideally we'd also want to be able to move the instantiation of the classes analogous to ProveOptions up as far as possible so as to minimize passing around of individual options, so instead of looking like

def exec_prove(
    foundry_root: Path,
    max_depth: int = 1000,
    max_iterations: int | None = None,
    reinit: bool = False,
    tests: Iterable[tuple[str, int | None]] = (),
    include_summaries: Iterable[tuple[str, int | None]] = (),
    workers: int = 1,
    break_every_step: bool = False,
    break_on_jumpi: bool = False,
    break_on_calls: bool = True,
    break_on_storage: bool = False,
    break_on_basic_blocks: bool = False,
    break_on_cheatcodes: bool = False,
    bmc_depth: int | None = None,
    bug_report: BugReport | None = None,
    kore_rpc_command: str | Iterable[str] | None = None,
    use_booster: bool = True,
    smt_timeout: int | None = None,
    smt_retry_limit: int | None = None,
    smt_tactic: str | None = None,
    failure_info: bool = True,
    counterexample_info: bool = False,
    trace_rewrites: bool = False,
    auto_abstract_gas: bool = False,
    run_constructor: bool = False,
    fail_fast: bool = False,
    port: int | None = None,
    maude_port: int | None = None,
    use_gas: bool = False,
    summary_path: Path | None = None,
    **kwargs: Any,
) -> None:

exec prove could look more like

def exec_prove(
    options: ProveOptions
) -> None:

argparse has a feature where you can pass an object as a Namespace to parse_args() which it will populate with the args and their values as fields, so it would be nice if we could just use that out of the box, but it doesn't seem powerful enough for what we want to do (multiple different classes for different subcommands). The problem is that we would like the Options classes to be specific to a specific command, like ProveOptions for prove, RunOptions for run, etc. but to know which of these commands has been invoked you first need to call parse_args. It would be nice if there was a way to split the argument parsing into two stages where during the first it gets the subcommand and during the second it gets the options for that subcommand.

Possibly we could have routing logic like

    args = cli_parser.parse_args()
    if args.command.lower() == 'prove':
       options = ProveOptions(args)
    if args.command.lower() == 'run':
       options = RunOptions(args)
    ...
    executor_name = 'exec_' + args.command.lower().replace('-', '_')
    if executor_name not in globals():
        raise AssertionError(f'Unimplemented command: {args.command}')

    execute = globals()[executor_name]
    execute(options)

and then in the constructor for each Options class that takes a dict, that would be where we set the default values if the entry is missing from the dict.

@palinatolmach also pointed out that we want to be able to, in some cases, override the default values of inherited options for semantics-specific Options subclasses, so this should also be built with that in mind.

Adding better default argument handling in #916 (in progress).

[ehildenb]

It would be nice to have a single class called ProveOptions (and KompileOptions, RunOptions, ParseOptions, etc...), which export the functionality to:

• Parse CLI arguments.
• Parse TOML arguments.
• Set default values.
• Implement logic for prioritizing CLI, then TOML, then default arguments.
• Be importable into subclasses where the commands can be extended.

We can use argparse for parsing the CLI arguments and populating the initial namespace, and then a TOML parser to parse the TOML arguments and populate that namespace further (with anything not specified already by the CLI), and then further populate the namespace with the default values supplied by the class (or by downstream classes where they are overridden).

Ideally, all this logic would be hidden from the user, we'd basically do something like:

prove_options = ProveOptions(cli_args, toml_args)

Then be able to access properties of the ProveOptions class directly:

foundry_prove(prove_options: ProveOptions):
    ...
    some_function(prove_options.max_iterations)
    ...

[ovatman]

I think it may also be useful to distinguish between the tool options and functionality options. How about:

We can have a different {Tool}Options classes for pyk, kevm_pyk and kontrol where there's an inheritance relationship in reverse order. {Tool}Options classes do the following:

• Perform the initialization and set default values.
• Contain an argparse.ArgumentParser with no defaults set.
• Update itself with cli args and/or toml args. Update process would be to perform parsing via the ArgumentParser of the class and update all the values that are not set to None by the ArgumentParser .
• Spit out different kind of functionality specific {Function}Options objects. i.e. the invocation suggested above would be performed like foundry_prove(kontrol_options.prove_options())

[ehildenb]

Some sort of rough sketch:

class ProveOptions(Options):
    smt_timeout: int

    @staticmethod
    def default() -> dict[str, Any]:
        return {'smt_timeout': 125}

    def __init__(self, dct: dict[str, Any]) -> ProveOptions:
        self.smt_timeout = dict['smt_timeout'] if 'smt_timeout' in dict else ProveOptions.default['smt_timeout']

    @staticmethod
    def parser(base: ArgumentParser) -> ArgumentParser:
        prove_args = base.add_parser('prove', ...)
        # add prove arguments here

    @staticmethod
    def parse(self, parser: ArgumentParser, args: ???) -> ProveOptions:
        return ProveOptions(parser.parse(args))