diff --git a/docs/conf.py b/docs/conf.py index ca54b3eb2..daf561228 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '0.1.711' -release = '0.1.711' +version = '0.1.712' +release = '0.1.712' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/package/version b/package/version index 0b02207f0..235760fbf 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.711 +0.1.712 diff --git a/pyproject.toml b/pyproject.toml index c8499c169..5f86f380f 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.711" +version = "0.1.712" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/src/pyk/__main__.py b/src/pyk/__main__.py index bfef5d690..b2a7028ab 100644 --- a/src/pyk/__main__.py +++ b/src/pyk/__main__.py @@ -4,6 +4,7 @@ import logging import sys from argparse import ArgumentParser, FileType +from collections.abc import Iterable from enum import Enum from pathlib import Path from typing import TYPE_CHECKING @@ -11,7 +12,8 @@ from graphviz import Digraph from .cli.args import KCLIArgs -from .cli.utils import LOG_FORMAT, dir_path, loglevel +from .cli.pyk import generate_options +from .cli.utils import LOG_FORMAT, dir_path, file_path, loglevel from .coverage import get_rule_by_id, strip_coverage_logger from .cterm import CTerm from .kast.inner import KInner @@ -39,9 +41,22 @@ from .utils import check_file_path, ensure_dir_path if TYPE_CHECKING: - from argparse import Namespace from typing import Any, Final + from .cli.pyk import ( + CoverageOptions, + GraphImportsOptions, + JsonToKoreOptions, + KompileCommandOptions, + KoreToJsonOptions, + PrintOptions, + ProveLegacyOptions, + ProveOptions, + RPCKastOptions, + RPCPrintOptions, + RunOptions, + ) + _LOGGER: Final = logging.getLogger(__name__) @@ -60,6 +75,11 @@ def main() -> None: cli_parser = create_argument_parser() args = cli_parser.parse_args() + 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) + logging.basicConfig(level=loglevel(args), format=LOG_FORMAT) executor_name = 'exec_' + args.command.lower().replace('-', '_') @@ -67,29 +87,29 @@ def main() -> None: raise AssertionError(f'Unimplemented command: {args.command}') execute = globals()[executor_name] - execute(args) + execute(options) -def exec_print(args: Namespace) -> None: - kompiled_dir: Path = args.definition_dir +def exec_print(options: PrintOptions) -> None: + kompiled_dir: Path = options.definition_dir printer = KPrint(kompiled_dir) - if args.input == PrintInput.KORE_JSON: - _LOGGER.info(f'Reading Kore JSON from file: {args.term.name}') - kore = Pattern.from_json(args.term.read()) + if options.input == PrintInput.KORE_JSON: + _LOGGER.info(f'Reading Kore JSON from file: {options.term.name}') + kore = Pattern.from_json(options.term.read()) term = printer.kore_to_kast(kore) else: - _LOGGER.info(f'Reading Kast JSON from file: {args.term.name}') - term = KInner.from_json(args.term.read()) + _LOGGER.info(f'Reading Kast JSON from file: {options.term.name}') + term = KInner.from_json(options.term.read()) if is_top(term): - args.output_file.write(printer.pretty_print(term)) - _LOGGER.info(f'Wrote file: {args.output_file.name}') + options.output_file.write(printer.pretty_print(term)) + _LOGGER.info(f'Wrote file: {options.output_file.name}') else: - if args.minimize: - if args.omit_labels != '' and args.keep_cells != '': + if options.minimize: + if options.omit_labels is not None and options.keep_cells is not None: raise ValueError('You cannot use both --omit-labels and --keep-cells.') - abstract_labels = args.omit_labels.split(',') if args.omit_labels != '' else [] - keep_cells = args.keep_cells.split(',') if args.keep_cells != '' else [] + abstract_labels = options.omit_labels.split(',') if options.omit_labels is not None else [] + keep_cells = options.keep_cells.split(',') if options.keep_cells is not None else [] minimized_disjuncts = [] for disjunct in flatten_label('#Or', term): @@ -105,14 +125,14 @@ def exec_print(args: Namespace) -> None: minimized_disjuncts.append(config) term = propagate_up_constraints(mlOr(minimized_disjuncts, sort=GENERATED_TOP_CELL)) - args.output_file.write(printer.pretty_print(term)) - _LOGGER.info(f'Wrote file: {args.output_file.name}') + options.output_file.write(printer.pretty_print(term)) + _LOGGER.info(f'Wrote file: {options.output_file.name}') -def exec_rpc_print(args: Namespace) -> None: - kompiled_dir: Path = args.definition_dir +def exec_rpc_print(options: RPCPrintOptions) -> None: + kompiled_dir: Path = options.definition_dir printer = KPrint(kompiled_dir) - input_dict = json.loads(args.input_file.read()) + input_dict = json.loads(options.input_file.read()) output_buffer = [] def pretty_print_request(request_params: dict[str, Any]) -> list[str]: @@ -181,8 +201,8 @@ def pretty_print_execute_response(execute_result: ExecuteResult) -> list[str]: except KeyError as e: _LOGGER.critical(f'Could not find key {str(e)} in input JSON file') exit(1) - if args.output_file is not None: - args.output_file.write('\n'.join(output_buffer)) + if options.output_file is not None: + options.output_file.write('\n'.join(output_buffer)) else: print('\n'.join(output_buffer)) except ValueError as e: @@ -191,13 +211,13 @@ def pretty_print_execute_response(execute_result: ExecuteResult) -> list[str]: exit(1) -def exec_rpc_kast(args: Namespace) -> None: +def exec_rpc_kast(options: RPCKastOptions) -> None: """ Convert an 'execute' JSON RPC response to a new 'execute' or 'simplify' request, copying parameters from a reference request. """ - reference_request = json.loads(args.reference_request_file.read()) - input_dict = json.loads(args.response_file.read()) + reference_request = json.loads(options.reference_request_file.read()) + input_dict = json.loads(options.response_file.read()) execute_result = ExecuteResult.from_dict(input_dict['result']) non_state_keys = set(reference_request['params'].keys()).difference(['state']) request_params = {} @@ -210,75 +230,75 @@ def exec_rpc_kast(args: Namespace) -> None: 'method': reference_request['method'], 'params': request_params, } - args.output_file.write(json.dumps(request)) + options.output_file.write(json.dumps(request)) -def exec_prove_legacy(args: Namespace) -> None: - kompiled_dir: Path = args.definition_dir - kprover = KProve(kompiled_dir, args.main_file) - final_state = kprover.prove(Path(args.spec_file), spec_module_name=args.spec_module, args=args.kArgs) - args.output_file.write(json.dumps(mlOr([state.kast for state in final_state]).to_dict())) - _LOGGER.info(f'Wrote file: {args.output_file.name}') +def exec_prove_legacy(options: ProveLegacyOptions) -> None: + kompiled_dir: Path = options.definition_dir + kprover = KProve(kompiled_dir, options.main_file) + final_state = kprover.prove(Path(options.spec_file), spec_module_name=options.spec_module, args=options.k_args) + options.output_file.write(json.dumps(mlOr([state.kast for state in final_state]).to_dict())) + _LOGGER.info(f'Wrote file: {options.output_file.name}') -def exec_prove(args: Namespace) -> None: +def exec_prove(options: ProveOptions) -> None: kompiled_directory: Path - if args.definition_dir is None: + if options.definition_dir is None: kompiled_directory = Kompile.default_directory() _LOGGER.info(f'Using kompiled directory: {kompiled_directory}.') else: - kompiled_directory = args.definition_dir + kompiled_directory = options.definition_dir kprove = KProve(kompiled_directory) - proofs = kprove.prove_rpc(Path(args.spec_file), args.spec_module, type_inference_mode=args.type_inference_mode) + proofs = kprove.prove_rpc(options=options) for proof in sorted(proofs, key=lambda p: p.id): print('\n'.join(proof.summary.lines)) - if proof.failed and args.failure_info: + if proof.failed and options.failure_info: failure_info = proof.failure_info if type(failure_info) is APRFailureInfo: print('\n'.join(failure_info.print())) sys.exit(len([p.id for p in proofs if not p.passed])) -def exec_kompile(args: Namespace) -> None: - main_file = Path(args.main_file) +def exec_kompile(options: KompileCommandOptions) -> None: + main_file = Path(options.main_file) check_file_path(main_file) kompiled_directory: Path - if 'definition_dir' not in args: + if options.definition_dir is None: kompiled_directory = Path(f'{main_file.stem}-kompiled') ensure_dir_path(kompiled_directory) else: - kompiled_directory = args.definition_dir + kompiled_directory = options.definition_dir kompile_dict = { 'main_file': main_file, - 'backend': args.backend.value, - 'syntax_module': args.syntax_module, - 'main_module': args.main_module, - 'md_selector': args.md_selector, - 'include_dirs': (Path(include) for include in args.includes), + 'backend': options.backend.value, + 'syntax_module': options.syntax_module, + 'main_module': options.main_module, + 'md_selector': options.md_selector, + 'include_dirs': (Path(include) for include in options.includes), } Kompile.from_dict(kompile_dict)( output_dir=kompiled_directory, - type_inference_mode=args.type_inference_mode, + type_inference_mode=options.type_inference_mode, ) -def exec_run(args: Namespace) -> None: - pgm_file = Path(args.pgm_file) +def exec_run(options: RunOptions) -> None: + pgm_file = Path(options.pgm_file) check_file_path(pgm_file) kompiled_directory: Path - if 'definition_dir' not in args: + if options.definition_dir is None: kompiled_directory = Kompile.default_directory() _LOGGER.info(f'Using kompiled directory: {kompiled_directory}.') else: - kompiled_directory = args.definition_dir + kompiled_directory = options.definition_dir krun = KRun(kompiled_directory) rc, res = krun.krun(pgm_file) print(krun.pretty_print(res)) sys.exit(rc) -def exec_graph_imports(args: Namespace) -> None: - kompiled_dir: Path = args.definition_dir +def exec_graph_imports(options: GraphImportsOptions) -> None: + kompiled_dir: Path = options.definition_dir kprinter = KPrint(kompiled_dir) definition = kprinter.definition import_graph = Digraph() @@ -292,26 +312,26 @@ def exec_graph_imports(args: Namespace) -> None: _LOGGER.info(f'Wrote file: {graph_file}') -def exec_coverage(args: Namespace) -> None: - kompiled_dir: Path = args.definition_dir +def exec_coverage(options: CoverageOptions) -> None: + kompiled_dir: Path = options.definition_dir definition = remove_source_map(read_kast_definition(kompiled_dir / 'compiled.json')) pretty_printer = PrettyPrinter(definition) - for rid in args.coverage_file: + for rid in options.coverage_file: rule = minimize_rule(strip_coverage_logger(get_rule_by_id(definition, rid.strip()))) - args.output.write('\n\n') - args.output.write('Rule: ' + rid.strip()) - args.output.write('\nUnparsed:\n') - args.output.write(pretty_printer.print(rule)) - _LOGGER.info(f'Wrote file: {args.output.name}') + options.output_file.write('\n\n') + options.output_file.write('Rule: ' + rid.strip()) + options.output_file.write('\nUnparsed:\n') + options.output_file.write(pretty_printer.print(rule)) + _LOGGER.info(f'Wrote file: {options.output_file.name}') -def exec_kore_to_json(args: Namespace) -> None: +def exec_kore_to_json(options: KoreToJsonOptions) -> None: text = sys.stdin.read() kore = KoreParser(text).pattern() print(kore.json) -def exec_json_to_kore(args: dict[str, Any]) -> None: +def exec_json_to_kore(options: JsonToKoreOptions) -> None: text = sys.stdin.read() kore = Pattern.from_json(text) kore.write(sys.stdout) @@ -331,12 +351,10 @@ def create_argument_parser() -> ArgumentParser: ) print_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') print_args.add_argument('term', type=FileType('r'), help='Input term (in format specified with --input).') - print_args.add_argument('--input', default=PrintInput.KAST_JSON, type=PrintInput, choices=list(PrintInput)) - print_args.add_argument('--omit-labels', default='', nargs='?', help='List of labels to omit from output.') - print_args.add_argument( - '--keep-cells', default='', nargs='?', help='List of cells with primitive values to keep in output.' - ) - print_args.add_argument('--output-file', type=FileType('w'), default='-') + print_args.add_argument('--input', type=PrintInput, choices=list(PrintInput)) + print_args.add_argument('--omit-labels', nargs='?', help='List of labels to omit from output.') + print_args.add_argument('--keep-cells', nargs='?', help='List of cells with primitive values to keep in output.') + print_args.add_argument('--output-file', type=FileType('w')) rpc_print_args = pyk_args_command.add_parser( 'rpc-print', @@ -349,7 +367,7 @@ def create_argument_parser() -> ArgumentParser: type=FileType('r'), help='An input file containing the JSON RPC request or response with KoreJSON payload.', ) - rpc_print_args.add_argument('--output-file', type=FileType('w'), default='-') + rpc_print_args.add_argument('--output-file', type=FileType('w')) rpc_kast_args = pyk_args_command.add_parser( 'rpc-kast', @@ -366,7 +384,7 @@ def create_argument_parser() -> ArgumentParser: type=FileType('r'), help='An input file containing a JSON RPC response with KoreJSON payload.', ) - rpc_kast_args.add_argument('--output-file', type=FileType('w'), default='-') + rpc_kast_args.add_argument('--output-file', type=FileType('w')) prove_legacy_args = pyk_args_command.add_parser( 'prove-legacy', @@ -377,7 +395,7 @@ def create_argument_parser() -> ArgumentParser: prove_legacy_args.add_argument('main_file', type=str, help='Main file used for kompilation.') prove_legacy_args.add_argument('spec_file', type=str, help='File with the specification module.') prove_legacy_args.add_argument('spec_module', type=str, help='Module with claims to be proven.') - prove_legacy_args.add_argument('--output-file', type=FileType('w'), default='-') + prove_legacy_args.add_argument('--output-file', type=FileType('w')) prove_legacy_args.add_argument('kArgs', nargs='*', help='Arguments to pass through to K invocation.') kompile_args = pyk_args_command.add_parser( @@ -397,7 +415,6 @@ def create_argument_parser() -> ArgumentParser: '--backend', type=KompileBackend, dest='backend', - default=KompileBackend.LLVM, help='K backend to target with compilation.', ) kompile_args.add_argument( @@ -417,7 +434,7 @@ def create_argument_parser() -> ArgumentParser: help='Prove an input specification (using RPC based prover).', parents=[k_cli_args.logging_args], ) - prove_args.add_argument('spec_file', type=str, help='File with the specification module.') + prove_args.add_argument('spec_file', type=file_path, help='File with the specification module.') prove_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.') prove_args.add_argument('--spec-module', dest='spec_module', type=str, help='Module with claims to be proven.') prove_args.add_argument( @@ -425,7 +442,7 @@ def create_argument_parser() -> ArgumentParser: ) prove_args.add_argument( '--failure-info', - default=False, + default=None, action='store_true', help='Print out more information about proof failures.', ) @@ -444,7 +461,7 @@ def create_argument_parser() -> ArgumentParser: ) coverage_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') coverage_args.add_argument('coverage_file', type=FileType('r'), help='Coverage file to build log for.') - coverage_args.add_argument('-o', '--output', type=FileType('w'), default='-') + coverage_args.add_argument('-o', '--output', type=FileType('w')) pyk_args_command.add_parser('kore-to-json', help='Convert textual KORE to JSON', parents=[k_cli_args.logging_args]) diff --git a/src/pyk/cli/args.py b/src/pyk/cli/args.py index 027c709e9..bd032ae0b 100644 --- a/src/pyk/cli/args.py +++ b/src/pyk/cli/args.py @@ -1,16 +1,156 @@ from __future__ import annotations +import sys from argparse import ArgumentParser from functools import cached_property -from typing import TYPE_CHECKING +from typing import IO, TYPE_CHECKING, Any -from ..utils import ensure_dir_path +from pyk.utils import ensure_dir_path + +from .cli import Options from .utils import bug_report_arg, file_path if TYPE_CHECKING: - from typing import TypeVar + from pathlib import Path + + from ..utils import BugReport + + +class LoggingOptions(Options): + debug: bool + verbose: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'verbose': False, + 'debug': False, + } + + +class OutputFileOptions(Options): + output_file: IO[Any] + + @staticmethod + def default() -> dict[str, Any]: + return { + 'output_file': sys.stdout, + } + + +class DefinitionOptions(Options): + definition_dir: Path + + +class DisplayOptions(Options): + minimize: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'minimize': True, + } + + +class KDefinitionOptions(Options): + includes: list[str] + main_module: str | None + syntax_module: str | None + spec_module: str | None + md_selector: str + + @staticmethod + def default() -> dict[str, Any]: + return { + 'spec_module': None, + 'main_module': None, + 'syntax_module': None, + 'md_selector': 'k', + 'includes': [], + } + + +class SaveDirOptions(Options): + save_directory: Path | None + + @staticmethod + def default() -> dict[str, Any]: + return { + 'save_directory': None, + } + + +class SpecOptions(SaveDirOptions): + spec_file: Path + claim_labels: list[str] | None + exclude_claim_labels: list[str] + + @staticmethod + def default() -> dict[str, Any]: + return { + 'claim_labels': None, + 'exclude_claim_labels': [], + } + + +class KompileOptions(Options): + emit_json: bool + ccopts: list[str] + llvm_kompile: bool + llvm_library: bool + enable_llvm_debug: bool + read_only: bool + o0: bool + o1: bool + o2: bool + o3: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'emit_json': True, + 'llvm_kompile': False, + 'llvm_library': False, + 'enable_llvm_debug': False, + 'read_only': False, + 'o0': False, + 'o1': False, + 'o2': False, + 'o3': False, + 'ccopts': [], + } + + +class ParallelOptions(Options): + workers: int + + @staticmethod + def default() -> dict[str, Any]: + return { + 'workers': 1, + } + + +class BugReportOptions(Options): + bug_report: BugReport | None + + @staticmethod + def default() -> dict[str, Any]: + return {'bug_report': None} + + +class SMTOptions(Options): + smt_timeout: int + smt_retry_limit: int + smt_tactic: str | None - T = TypeVar('T') + @staticmethod + def default() -> dict[str, Any]: + return { + 'smt_timeout': 300, + 'smt_retry_limit': 10, + 'smt_tactic': None, + } class KCLIArgs: @@ -122,8 +262,8 @@ def definition_args(self) -> ArgumentParser: args.add_argument( '-I', type=str, dest='includes', default=[], action='append', help='Directories to lookup K definitions in.' ) - args.add_argument('--main-module', default=None, type=str, help='Name of the main module.') - args.add_argument('--syntax-module', default=None, type=str, help='Name of the syntax module.') + args.add_argument('--main-module', type=str, help='Name of the main module.') + args.add_argument('--syntax-module', type=str, help='Name of the syntax module.') args.add_argument( '--md-selector', type=str, diff --git a/src/pyk/cli/cli.py b/src/pyk/cli/cli.py new file mode 100644 index 000000000..cf0cf66ae --- /dev/null +++ b/src/pyk/cli/cli.py @@ -0,0 +1,18 @@ +from __future__ import annotations + +from typing import Any + + +class Options: + def __init__(self, args: dict[str, Any]) -> None: + # Get defaults from this and all superclasses that define them, preferring the most specific class + defaults: dict[str, Any] = {} + for cl in reversed(type(self).mro()): + if hasattr(cl, 'default'): + defaults = defaults | cl.default() + + # Overwrite defaults with args from command line + _args = defaults | args + + for attr, val in _args.items(): + self.__setattr__(attr, val) diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py new file mode 100644 index 000000000..b0e094f30 --- /dev/null +++ b/src/pyk/cli/pyk.py @@ -0,0 +1,145 @@ +from __future__ import annotations + +from enum import Enum +from typing import IO, TYPE_CHECKING, Any + +from pyk.ktool.kompile import KompileBackend + +from .args import DefinitionOptions, DisplayOptions, KDefinitionOptions, LoggingOptions, OutputFileOptions + +if TYPE_CHECKING: + from collections.abc import Iterable + from pathlib import Path + + from pyk.ktool import TypeInferenceMode + + +def generate_options(args: dict[str, Any]) -> LoggingOptions: + command = args['command'] + match command: + case 'json-to-kore': + return JsonToKoreOptions(args) + case 'kore-to-json': + return KoreToJsonOptions(args) + case 'coverage': + return CoverageOptions(args) + case 'graph-imports': + return GraphImportsOptions(args) + case 'rpc-kast': + return RPCKastOptions(args) + case 'rpc-print': + return RPCPrintOptions(args) + case 'print': + return PrintOptions(args) + case 'prove-legacy': + return ProveLegacyOptions(args) + case 'prove': + return ProveOptions(args) + case 'kompile': + return KompileCommandOptions(args) + case 'run': + return RunOptions(args) + case _: + raise ValueError(f'Unrecognized command: {command}') + + +class PrintInput(Enum): + KORE_JSON = 'kore-json' + KAST_JSON = 'kast-json' + + +class JsonToKoreOptions(LoggingOptions): + ... + + +class KoreToJsonOptions(LoggingOptions): + ... + + +class CoverageOptions(DefinitionOptions, OutputFileOptions, LoggingOptions): + coverage_file: IO[Any] + + +class GraphImportsOptions(DefinitionOptions, LoggingOptions): + ... + + +class RPCKastOptions(OutputFileOptions, LoggingOptions): + reference_request_file: IO[Any] + response_file: IO[Any] + + +class RPCPrintOptions(DefinitionOptions, OutputFileOptions, LoggingOptions): + input_file: IO[Any] + + +class PrintOptions(DefinitionOptions, OutputFileOptions, DisplayOptions, LoggingOptions): + term: IO[Any] + input: PrintInput + minimize: bool + omit_labels: str | None + keep_cells: str | None + + @staticmethod + def default() -> dict[str, Any]: + return { + 'input': PrintInput.KAST_JSON, + 'omit_labels': None, + 'keep_cells': None, + } + + +class ProveLegacyOptions(DefinitionOptions, OutputFileOptions, LoggingOptions): + main_file: Path + spec_file: Path + spec_module: str + k_args: Iterable[str] + + @staticmethod + def default() -> dict[str, Any]: + return { + 'k_args': [], + } + + +class KompileCommandOptions(LoggingOptions, KDefinitionOptions): + definition_dir: Path | None + main_file: str + backend: KompileBackend + type_inference_mode: TypeInferenceMode | None + + @staticmethod + def default() -> dict[str, Any]: + return { + 'definition_dir': None, + 'backend': KompileBackend.LLVM, + 'type_inference_mode': None, + } + + +class ProveOptions(LoggingOptions): + spec_file: Path + definition_dir: Path | None + spec_module: str | None + type_inference_mode: TypeInferenceMode | None + failure_info: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'definition_dir': None, + 'spec_module': None, + 'type_inference_mode': None, + 'failure_info': False, + } + + +class RunOptions(LoggingOptions): + pgm_file: str + definition_dir: Path | None + + @staticmethod + def default() -> dict[str, Any]: + return { + 'definition_dir': None, + } diff --git a/src/pyk/ktool/kprove.py b/src/pyk/ktool/kprove.py index 64f4c65c7..ce29f56bd 100644 --- a/src/pyk/ktool/kprove.py +++ b/src/pyk/ktool/kprove.py @@ -30,6 +30,7 @@ from subprocess import CompletedProcess from typing import Final + from ..cli.pyk import ProveOptions from ..kast.outer import KClaim, KRule, KRuleLike from ..kast.pretty import SymbolTable from ..kcfg.semantics import KCFGSemantics @@ -331,8 +332,7 @@ def prove_claim_rpc( def prove_rpc( self, - spec_file: Path, - spec_module_name: str, + options: ProveOptions, claim_labels: Iterable[str] | None = None, exclude_claim_labels: Iterable[str] | None = None, kcfg_semantics: KCFGSemantics | None = None, @@ -353,7 +353,6 @@ def prove_rpc( fallback_on: Iterable[FallbackReason] | None = None, interim_simplification: int | None = None, no_post_exec_simplify: bool = False, - type_inference_mode: TypeInferenceMode | None = None, ) -> list[Proof]: def _prove_claim_rpc(claim: KClaim) -> Proof: return self.prove_claim_rpc( @@ -379,14 +378,14 @@ def _prove_claim_rpc(claim: KClaim) -> Proof: ) all_claims = self.get_claims( - spec_file, - spec_module_name=spec_module_name, + options.spec_file, + spec_module_name=options.spec_module, claim_labels=claim_labels, exclude_claim_labels=exclude_claim_labels, - type_inference_mode=type_inference_mode, + type_inference_mode=options.type_inference_mode, ) if all_claims is None: - raise ValueError(f'No claims found in file: {spec_file}') + raise ValueError(f'No claims found in file: {options.spec_file}') return [_prove_claim_rpc(claim) for claim in all_claims] def get_claim_modules( diff --git a/src/tests/integration/ktool/test_imp.py b/src/tests/integration/ktool/test_imp.py index 78870e053..6cdb566d2 100644 --- a/src/tests/integration/ktool/test_imp.py +++ b/src/tests/integration/ktool/test_imp.py @@ -6,6 +6,7 @@ import pytest +from pyk.cli.pyk import ProveOptions from pyk.kast.inner import KApply, KSequence, KVariable from pyk.kcfg.semantics import KCFGSemantics from pyk.prelude.kbool import BOOL, notBool @@ -195,7 +196,14 @@ def test_prove_rpc( ) -> None: proof = single( kprove.prove_rpc( - Path(spec_file), spec_module, claim_labels=[claim_id], kcfg_semantics=ImpSemantics(kprove.definition) + ProveOptions( + { + 'spec_file': Path(spec_file), + 'spec_module': spec_module, + } + ), + claim_labels=[claim_id], + kcfg_semantics=ImpSemantics(kprove.definition), ) ) assert proof.status == proof_status