Add options classes and use in functions (#349)

* Add options classes and use in functions

* Set Version: 0.2.47

* Remove default values from argparse calls

* Fix test

* Fix output format in test

* Fix test

* Fix test

* Wrap llvm and haskell dir in Path

* Fix formatting

* Try fixing compiletest-rs tests

---------

Co-authored-by: devops <devops@runtimeverification.com>

Author: nwatson22

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.2.46"
+version = "0.2.47"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

kmir/src/kmir/__init__.py

@@ -2,4 +2,4 @@
 
 from .kmir import KMIR
 
-VERSION: Final = '0.2.46'
+VERSION: Final = '0.2.47'

kmir/src/kmir/__main__.py

@@ -1,20 +1,19 @@
 import logging
 import sys
 from argparse import Namespace
-from pathlib import Path
-from typing import Any, Final, Iterable, Optional
+from typing import Any, Final, Iterable
 
+from pyk.cli.args import LoggingOptions
 from pyk.proof import APRProof
 from pyk.proof.reachability import APRFailureInfo
 from pyk.utils import BugReport, check_dir_path, check_file_path
 
 from . import VERSION
 from .cli import create_argument_parser
 from .kmir import KMIR
-from .parse import parse
-from .prove import get_claim_labels, prove, show_proof, view_proof
-from .run import run
-from .utils import NodeIdLike
+from .parse import ParseOptions, parse
+from .prove import ProveOptions, ShowProofOptions, ViewProofOptions, get_claim_labels, prove, show_proof, view_proof
+from .run import RunOptions, run
 
 _LOGGER: Final = logging.getLogger(__name__)
 _LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
@@ -25,128 +24,120 @@ def main() -> None:
     args = parser.parse_args()
     logging.basicConfig(level=_loglevel(args), format=_LOG_FORMAT)
 
+    stripped_args = {
+        key: val for (key, val) in vars(args).items() if val is not None and not (isinstance(val, Iterable) and not val)
+    }
+    options = generate_options(stripped_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(**vars(args))
+    execute(options)
+
+
+def generate_options(args: dict[str, Any]) -> LoggingOptions:
+    command = args['command']
+    match command:
+        case 'version':
+            return VersionOptions(args)
+        case 'parse':
+            return ParseOptions(args)
+        case 'run':
+            return RunOptions(args)
+        case 'prove':
+            return ProveOptions(args)
+        case 'show-proof':
+            return ShowProofOptions(args)
+        case 'view-proof':
+            return ViewProofOptions(args)
+        case _:
+            raise ValueError(f'Unrecognized command: {command}')
+
 
+class VersionOptions(LoggingOptions): ...
 
-def exec_version(**kwargs: Any) -> None:
+
+def exec_version(options: VersionOptions) -> None:
     print(f'KMIR Version: {VERSION}')
 
 
-def exec_parse(
-    mir_file: Path,
-    input: str,
-    output: str,
-    definition_dir: Optional[Path] = None,
-    **kwargs: Any,
-) -> None:
-    check_file_path(mir_file)
+def exec_parse(options: ParseOptions) -> None:
+    check_file_path(options.mir_file)
 
-    if definition_dir is None:
+    if options.definition_dir is None:
         raise RuntimeError('Cannot find KMIR LLVM definition, please specify --definition-dir, or KMIR_LLVM_DIR')
     else:
         # llvm_dir = Path(definition_dir)
-        check_dir_path(definition_dir)
+        check_dir_path(options.definition_dir)
 
-    kmir = KMIR(definition_dir)
+    kmir = KMIR(options.definition_dir)
     # _LOGGER.log( 'Call parser at {definition_dir}')
-    parse(kmir, mir_file, output=output)
+    parse(kmir, options)
     # print(proc_res.stdout) if output != 'none' else None
 
 
-def exec_run(
-    mir_file: Path,
-    output: str,
-    definition_dir: Optional[Path] = None,
-    depth: Optional[int] = None,
-    bug_report: bool = False,
-    # ignore_return_code: bool = False,
-    **kwargs: Any,
-) -> None:
+def exec_run(options: RunOptions) -> None:
     # mir_file = Path(input_file)
-    check_file_path(mir_file)
+    check_file_path(options.mir_file)
 
-    if definition_dir is None:
+    if options.definition_dir is None:
         raise RuntimeError('Cannot find KMIR LLVM definition, please specify --definition-dir, or KMIR_LLVM_DIR')
     else:
         # llvm_dir = Path(definition_dir)
-        check_dir_path(definition_dir)
+        check_dir_path(options.definition_dir)
 
-    if depth is not None:
-        assert depth < 0, ValueError(f'Argument "depth" must be non-negative, got: {depth}')
+    if options.depth is not None:
+        assert options.depth < 0, ValueError(f'Argument "depth" must be non-negative, got: {options.depth}')
 
-    if bug_report:
-        br = BugReport(mir_file.with_suffix('.bug_report.tar'))
-        kmir = KMIR(definition_dir, bug_report=br)
+    if options.bug_report:
+        br = BugReport(options.mir_file.with_suffix('.bug_report.tar'))
+        kmir = KMIR(options.definition_dir, bug_report=br)
     else:
-        kmir = KMIR(definition_dir)
-
-    run(kmir, mir_file, depth=depth, output=output)
-
-
-def exec_prove(
-    spec_file: Path,
-    smt_timeout: int,
-    smt_retry_limit: int,
-    claim_list: bool = False,
-    claim: Optional[str] = None,
-    definition_dir: Optional[Path] = None,
-    haskell_dir: Optional[Path] = None,
-    use_booster: bool = True,
-    bug_report: bool = False,
-    save_directory: Optional[Path] = None,
-    reinit: bool = False,
-    depth: Optional[int] = None,
-    trace_rewrites: bool = False,
-    **kwargs: Any,
-) -> None:
+        kmir = KMIR(options.definition_dir)
+
+    run(kmir, options)
+
+
+def exec_prove(options: ProveOptions) -> None:
     # TODO: workers
     # TODO: md_selector doesn't work
 
-    check_file_path(spec_file)
+    check_file_path(options.spec_file)
 
-    if definition_dir is None:
+    if options.definition_dir is None:
         raise RuntimeError('Cannot find KMIR LLVM definition, please specify --definition-dir, or KMIR_LLVM_DIR')
     else:
         # llvm_dir = Path(definition_dir)
-        check_dir_path(definition_dir)
+        check_dir_path(options.definition_dir)
 
-    if haskell_dir is None:
+    if options.haskell_dir is None:
         raise RuntimeError('Cannot find KMIR Haskell definition, please specify --haskell-dir, or KMIR_HASKELL_DIR')
     else:
         # haskell_dir = Path(haskell_dir)
-        check_dir_path(haskell_dir)
+        check_dir_path(options.haskell_dir)
 
     # if the save_directory is not provided, the proofs are saved to the same directory of spec_file
+    save_directory = options.save_directory
     if save_directory is None:
-        save_directory = spec_file.parent
+        save_directory = options.spec_file.parent
     else:
         check_dir_path(save_directory)
 
-    br = BugReport(spec_file.with_suffix('.bug_report.tar')) if bug_report else None
-    kmir = KMIR(definition_dir, haskell_dir=haskell_dir, use_booster=use_booster, bug_report=br)
+    br = BugReport(options.spec_file.with_suffix('.bug_report.tar')) if options.bug_report else None
+    kmir = KMIR(options.definition_dir, haskell_dir=options.haskell_dir, use_booster=options.use_booster, bug_report=br)
     # We provide configuration of which backend to use in a KMIR object.
     # `use_booster` is by default True, where Booster Backend is always used unless turned off
 
-    if claim_list:
-        claim_labels = get_claim_labels(kmir, spec_file)
+    if options.claim_list:
+        claim_labels = get_claim_labels(kmir, options.spec_file)
         print(*claim_labels, sep='\n')
         sys.exit(0)
 
     (passed, failed) = prove(
         kmir,
-        spec_file,
-        claim_label=claim,
-        save_directory=save_directory,
-        reinit=reinit,
-        depth=depth,
-        smt_timeout=smt_timeout,
-        smt_retry_limit=smt_retry_limit,
-        trace_rewrites=trace_rewrites,
+        options,
     )
 
     for proof in passed:
@@ -166,82 +157,53 @@ def exec_prove(
         sys.exit(1)
 
 
-def exec_show_proof(
-    claim_label: str,
-    proof_dir: Optional[Path] = None,
-    definition_dir: Optional[Path] = None,
-    haskell_dir: Optional[Path] = None,
-    nodes: Iterable[NodeIdLike] = (),
-    node_deltas: Iterable[tuple[NodeIdLike, NodeIdLike]] = (),
-    failure_info: bool = False,
-    to_module: bool = False,
-    # minimize: bool = True,
-    pending: bool = False,
-    failing: bool = False,
-    counterexample_info: bool = False,
-    **kwargs: Any,
-) -> None:
-    if proof_dir is None:
+def exec_show_proof(options: ShowProofOptions) -> None:
+    if options.proof_dir is None:
         raise RuntimeError('Proof directory is not specified, please provide the directory to all the proofs')
     else:
-        check_dir_path(proof_dir)
+        check_dir_path(options.proof_dir)
 
-    if definition_dir is None:
+    if options.definition_dir is None:
         raise RuntimeError('Cannot find KMIR LLVM definition, please specify --definition-dir, or KMIR_LLVM_DIR')
     else:
-        check_dir_path(definition_dir)
+        check_dir_path(options.definition_dir)
 
-    if haskell_dir is None:
+    if options.haskell_dir is None:
         raise RuntimeError('Cannot find KMIR Haskell definition, please specify --haskell-dir, or KMIR_HASKELL_DIR')
     else:
-        check_dir_path(haskell_dir)
+        check_dir_path(options.haskell_dir)
 
-    kmir = KMIR(definition_dir, haskell_dir=haskell_dir)
+    kmir = KMIR(options.definition_dir, haskell_dir=options.haskell_dir)
 
     show_output = show_proof(
         kmir,
-        claim_label,
-        proof_dir,
-        nodes,
-        node_deltas,
-        to_module,
-        failure_info,
-        pending,
-        failing,
-        counterexample_info,
+        options,
     )
 
     print(show_output)
 
 
-def exec_view_proof(
-    claim_label: str,
-    proof_dir: Optional[Path] = None,
-    definition_dir: Optional[Path] = None,
-    haskell_dir: Optional[Path] = None,
-    **kwargs: Any,
-) -> None:
+def exec_view_proof(options: ViewProofOptions) -> None:
     # TODO: include dirs
 
-    if proof_dir is None:
+    if options.proof_dir is None:
         raise RuntimeError('Proof directory is not specified, please provide the directory to all the proofs')
     else:
-        check_dir_path(proof_dir)
-    if definition_dir is None:
+        check_dir_path(options.proof_dir)
+    if options.definition_dir is None:
         raise RuntimeError('Cannot find KMIR LLVM definition, please specify --definition-dir, or KMIR_LLVM_DIR')
     else:
-        check_dir_path(definition_dir)
-    if haskell_dir is None:
+        check_dir_path(options.definition_dir)
+    if options.haskell_dir is None:
         raise RuntimeError('Cannot find KMIR Haskell definition, please specify --haskell-dir, or KMIR_HASKELL_DIR')
     else:
-        check_dir_path(haskell_dir)
+        check_dir_path(options.haskell_dir)
 
-    kmir = KMIR(definition_dir, haskell_dir=haskell_dir)
+    kmir = KMIR(options.definition_dir, haskell_dir=options.haskell_dir)
 
     view_proof(
         kmir,
-        claim_label,
-        proof_dir,
+        options,
     )