From 6cb5d64a0f5bd0cd3b5cdbe30e663df4aecf306e Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 25 Apr 2024 17:32:49 -0500 Subject: [PATCH 01/16] Add Option and OptionsHandler classes --- pyk/src/pyk/cli/cli.py | 56 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 55 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/cli/cli.py b/pyk/src/pyk/cli/cli.py index c606824d575..fe229d11fa5 100644 --- a/pyk/src/pyk/cli/cli.py +++ b/pyk/src/pyk/cli/cli.py @@ -1,6 +1,60 @@ from __future__ import annotations -from typing import Any +from typing import Any, Generic, Iterable +from abc import ABC, abstractmethod + +T = TypeVar('T') +O = TypeVar('O', bound=Options) + +class CLI: + _command_handlers: list[OptionsHandler] + + def __init__(self, command_handlers: Iterable[OptionsHandler] = ()) -> None: + self._command_handlers = list(command_handlers) + + def add_command(self, command_handler: OptionsHandler) -> None: + self._command_handlers.append(command_handler) + + +class Option(Generic[T]): + _name: str + _cmd_line_name: str + _toml_name: str + _optional: bool + _help_str: str | None + _default: T + + def __init__( + self, + name: str, + cmd_line_name: str | None = None, + toml_name: str | None = None, + optional: bool = False, + help_str: str | None = None, + default: T | str = 'NoDefault', + ) -> None: + self._name = name, + self._cmd_line_name = cmd_line_name or name + self._toml_name = cmd_line_name or name + self._optional = optional + self._help_str = help_str + + if default == 'NoDefault' and optional: + raise ValueError(f'Optional option {name} must define a default value.') + if default != 'NoDefault' and not optional: + raise ValueError(f'Required option {name} cannot take a default value.') + + self._default = default + + +class OptionsHandler(Generic[O], ABC): + + def add_option(self, ) -> dict[str, Any]: + ... + + @abstractmethod + def default(self) -> dict[str, Any]: + ... class Options: From 94d10986a70cfd288ab8203764a889750eeb2160 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 26 Apr 2024 15:42:41 -0500 Subject: [PATCH 02/16] Expand CLI, Options, Option, and Command classes --- pyk/src/pyk/cli/cli.py | 171 ++++++++++++++++++++++++++++++++++------- 1 file changed, 143 insertions(+), 28 deletions(-) diff --git a/pyk/src/pyk/cli/cli.py b/pyk/src/pyk/cli/cli.py index fe229d11fa5..6bd9ca71cf2 100644 --- a/pyk/src/pyk/cli/cli.py +++ b/pyk/src/pyk/cli/cli.py @@ -1,43 +1,124 @@ from __future__ import annotations +from enum import Enum from typing import Any, Generic, Iterable from abc import ABC, abstractmethod +from argparse import ArgumentParser T = TypeVar('T') O = TypeVar('O', bound=Options) class CLI: - _command_handlers: list[OptionsHandler] - - def __init__(self, command_handlers: Iterable[OptionsHandler] = ()) -> None: - self._command_handlers = list(command_handlers) - - def add_command(self, command_handler: OptionsHandler) -> None: - self._command_handlers.append(command_handler) + _commands: list[Command] + + def __init__(self, commands: Iterable[Command] = ()) -> None: + self._commands = list(commands) + + def add_command(self, command: Command) -> None: + self._commands.append(command) + + def create_argument_parser(self) -> ArgumentParser: + args = ArgumentParser() + subparsers = args.add_subparsers(dest='command', required=True) + for command in self._commands: + command_args = subparsers.add_parser(name=command.name, help=command.help_str) + for option in command.options: + + if option.type is bool and option.is_optional: + command_args.add_argument( + option.cmd_line_name, + **(option.aliases), + default='NoDefault', + required=False, + type=option.type, + help=option.help_str, + metavar=options.metavar, + action='store_false' if option.default else 'store_true', + dest=option.name, + ) + elif isinstance(option.type, Enum) and option.is_optional: + command_args.add_argument( + option.cmd_line_name, + **(option.aliases), + default='NoDefault', + required=False, + type=option.type, + help=option.help_str, + metavar=options.metavar, + dest=option.name, + choices=list(options.type), + ) + elif isinstance(option.type, Iterable) and option.is_optional: + command_args.add_argument( + option.cmd_line_name, + **(option.aliases), + default='NoDefault', + required=False, + type=option.type, + help=option.help_str, + metavar=options.metavar, + action='append', + dest=option.name, + ) + else: + command_args.add_argument( + option.cmd_line_name, + **(option.aliases), + default='NoDefault', + required=(not options.is_optional), + type=option.type, + help=option.help_str, + metavar=options.metavar, + dest=option.name, + ) + return args + + def generate_command(self, args: dict[str, Any]) -> Command + + def get_command(self) -> Command: + parser = self.create_argument_parser() + args = parser.parse_args() + stripped_args = { + key: val + for (key, val) in vars(args).items() + if val != 'NoDefault' + } + return self.generate_command(stripped_args) + + + def get_and_exec_command(self) -> None: + cmd = self.get_command() + cmd.exec() class Option(Generic[T]): _name: str + _aliases: list[str] _cmd_line_name: str _toml_name: str _optional: bool _help_str: str | None + _metavar: str | None _default: T def __init__( self, name: str, + aliases: Iterable[str] = (), cmd_line_name: str | None = None, toml_name: str | None = None, optional: bool = False, help_str: str | None = None, + metavar: str | None = None, default: T | str = 'NoDefault', ) -> None: self._name = name, + self._aliases = list(aliases) self._cmd_line_name = cmd_line_name or name self._toml_name = cmd_line_name or name self._optional = optional self._help_str = help_str + self._metavar = metavar if default == 'NoDefault' and optional: raise ValueError(f'Optional option {name} must define a default value.') @@ -46,31 +127,65 @@ def __init__( self._default = default + @property + def is_optional(self) -> bool: + return self._optional -class OptionsHandler(Generic[O], ABC): + @property + def name(self) -> str: + return self._name - def add_option(self, ) -> dict[str, Any]: - ... + @property + def aliases(self) -> list[str]: + return self._aliases + + @property + def cmd_line_name(self) -> str: + return self._cmd_line_name + + @property + def toml_name(self) -> str: + return self._toml_name + + @property + def help_str(self) -> str: + return self._help_str + + @property + def metavar(self) -> str: + return self._metavar + + @property + def type(self) -> str: + return T + +class Command: + _options: Options + _name: str + _help_str: str + + @property + def name(self) -> str: + return self._name + + @property + def help_str(self) -> str: + return self._help_str + + @property + def options(self) -> Options: + return self._options @abstractmethod - def default(self) -> dict[str, Any]: + def exec(self) -> None: ... - 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) - - @staticmethod - def from_option_string() -> dict[str, str]: - return {} + _options: dict[str, Option] + + def add_option(self, option: Option) -> dict[str, Any]: + self._options[option.name] = option + + def override_default(self, option_name: str, value: T) -> None: + if not self._options[option_name].is_optional: + raise ValueError(f'Cannot provide a default value for a required parameter: {option_name}') From ec3cb3cbe1cc336c4d05644e4da043bea34d9bd8 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 26 Apr 2024 19:07:42 -0500 Subject: [PATCH 03/16] Fill out automatic argument parser generation and options extraction --- pyk/src/pyk/cli/args.py | 107 ++++++++++++++++++++++++++++++++--- pyk/src/pyk/cli/cli.py | 121 ++++++++++++++++++++++++++-------------- 2 files changed, 180 insertions(+), 48 deletions(-) diff --git a/pyk/src/pyk/cli/args.py b/pyk/src/pyk/cli/args.py index 41bbdbe7b3b..ef3c1fe585a 100644 --- a/pyk/src/pyk/cli/args.py +++ b/pyk/src/pyk/cli/args.py @@ -7,7 +7,7 @@ from typing import IO, TYPE_CHECKING, Any from ..ktool.kompile import KompileBackend, LLVMKompileType, TypeInferenceMode, Warnings -from .cli import Options +from .cli import Option, Options, OptionsGroup from .utils import bug_report_arg, dir_path, ensure_dir_path, file_path if TYPE_CHECKING: @@ -16,6 +16,28 @@ from ..utils import BugReport +class LoggingOptionsGroup(OptionsGroup): + def __init__(self) -> None: + super().__init__() + self.add_option( + Option( + name='debug', cmd_line_name='--debug', type=bool, optional=True, default=False, help_str='Debug output.' + ) + ) + self.add_option( + Option( + name='verbose', + cmd_line_name='--verbose', + aliases=['-v'], + toml_name='v', + type=bool, + optional=True, + default=False, + help_str='Debug output.', + ) + ) + + class LoggingOptions(Options): debug: bool verbose: bool @@ -34,6 +56,35 @@ def from_option_string() -> dict[str, Any]: } +class WarningOptionsGroup(OptionsGroup): + def __init__(self) -> None: + super().__init__() + self.add_option( + Option( + name='warnings_to_errors', + cmd_line_name='--warnings-to-errors', + aliases=['-w2e'], + default=False, + help_str='Turn warnings into errors (no effect on pyk, only subcommands).', + optional=True, + toml_name='w2e', + type=bool, + ) + ) + self.add_option( + Option( + name='warnings', + cmd_line_name='--warnings', + aliases=['-w'], + default=False, + help_str='Warnings to print about (no effect on pyk, only subcommands).', + optional=True, + toml_name='w', + type=Warnings, + ) + ) + + class WarningOptions(Options): warnings: Warnings | None warnings_to_errors: bool @@ -53,6 +104,20 @@ def from_option_string() -> dict[str, Any]: } +class OutputFileOptionsGroup(OptionsGroup): + def __init__(self) -> None: + super().__init__() + self.add_option( + Option( + name='output_file', + cmd_line_name='--output-file', + default=sys.stdout, + optional=True, + type=IO[Any], + ) + ) + + class OutputFileOptions(Options): output_file: IO[Any] @@ -63,17 +128,31 @@ def default() -> dict[str, Any]: } +class DefinitionOptionsGroup(OptionsGroup): + def __init__(self) -> None: + super().__init__() + self.add_option( + Option(name='definition_dir', toml_name='definition', type=Path, help_str='Path to definition directory.') + ) + + class DefinitionOptions(Options): definition_dir: Path @staticmethod - def default() -> dict[str, Any]: + def from_option_string() -> dict[str, Any]: return { 'output-definition': 'definition_dir', 'definition': 'definition_dir', } +class DisplayOptionsGroup(OptionsGroup): + def __init__(self) -> None: + super().__init__() + self.add_option(Option(name='minimize', type=bool, optional=True, default=True, help_str='Minimize output.')) + + class DisplayOptions(Options): minimize: bool @@ -84,6 +163,20 @@ def default() -> dict[str, Any]: } + +class KDefinitionOptionsGroup(OptionsGroup): + def __init__(self) -> None: + super().__init__() + self.add_option(Option(name='includes', cmd_line_name='-I', type=list[str], optional=True, default=[], + help_str='Directories to lookup K definitions in.')) + self.add_option(Option(name='main_module', cmd_line_name='--main-module', type=(str | None), optional=True, default=None, + help_str='Name of the main module.')) + self.add_option(Option(name='syntax_module', cmd_line_name='--syntax-module', type=str | None, optional=True, default=None, + help_str='Name of the syntax module.')) + self.add_option(Option(name='md_selector', cmd_line_name='--md-selector', type=str, optional=True, + default='k', help_str='Code selector expression to use when reading markdown.')) + + class KDefinitionOptions(Options): includes: list[str] main_module: str | None @@ -101,11 +194,11 @@ def default() -> dict[str, Any]: 'includes': [], } - @staticmethod - def from_option_string() -> dict[str, str]: - return { - 'includes': 'includes', - } +# @staticmethod +# def from_option_string() -> dict[str, str]: +# return { +# 'includes': 'includes', +# } class SaveDirOptions(Options): diff --git a/pyk/src/pyk/cli/cli.py b/pyk/src/pyk/cli/cli.py index 6bd9ca71cf2..a7980b25d56 100644 --- a/pyk/src/pyk/cli/cli.py +++ b/pyk/src/pyk/cli/cli.py @@ -1,12 +1,12 @@ from __future__ import annotations -from enum import Enum -from typing import Any, Generic, Iterable -from abc import ABC, abstractmethod +from abc import abstractmethod from argparse import ArgumentParser +from enum import Enum +from typing import Any, Generic, Iterable, TypeVar T = TypeVar('T') -O = TypeVar('O', bound=Options) + class CLI: _commands: list[Command] @@ -27,67 +27,65 @@ def create_argument_parser(self) -> ArgumentParser: if option.type is bool and option.is_optional: command_args.add_argument( option.cmd_line_name, - **(option.aliases), - default='NoDefault', + *(option.aliases), + default='NoDefault', required=False, type=option.type, help=option.help_str, - metavar=options.metavar, + metavar=option.metavar, action='store_false' if option.default else 'store_true', dest=option.name, ) - elif isinstance(option.type, Enum) and option.is_optional: + elif issubclass(option.type, Enum) and option.is_optional: command_args.add_argument( option.cmd_line_name, - **(option.aliases), + *(option.aliases), default='NoDefault', required=False, type=option.type, help=option.help_str, - metavar=options.metavar, + metavar=option.metavar, dest=option.name, - choices=list(options.type), + choices=list(option.type), ) elif isinstance(option.type, Iterable) and option.is_optional: command_args.add_argument( option.cmd_line_name, - **(option.aliases), + *(option.aliases), default='NoDefault', required=False, type=option.type, help=option.help_str, - metavar=options.metavar, + metavar=option.metavar, action='append', dest=option.name, ) else: command_args.add_argument( option.cmd_line_name, - **(option.aliases), + *(option.aliases), default='NoDefault', - required=(not options.is_optional), + required=(not option.is_optional), type=option.type, help=option.help_str, - metavar=options.metavar, + metavar=option.metavar, dest=option.name, ) return args - def generate_command(self, args: dict[str, Any]) -> Command + def get_command(self, args: dict[str, Any]) -> Command: + command_name = args['command'].lower() + for command in self._commands: + if command.name.lower() == command_name: + return command + raise ValueError(f'Commmand {command_name} not found.') - def get_command(self) -> Command: + def get_and_exec_command(self) -> None: parser = self.create_argument_parser() args = parser.parse_args() - stripped_args = { - key: val - for (key, val) in vars(args).items() - if val != 'NoDefault' - } - return self.generate_command(stripped_args) - - - def get_and_exec_command(self) -> None: - cmd = self.get_command() + stripped_args = {key: val for (key, val) in vars(args).items() if val != 'NoDefault'} + cmd = self.get_command(stripped_args) + cmd.extract(stripped_args) cmd.exec() @@ -99,11 +97,13 @@ class Option(Generic[T]): _optional: bool _help_str: str | None _metavar: str | None - _default: T + _default: T | str + _type: type[Any] def __init__( self, name: str, + type: type[Any], aliases: Iterable[str] = (), cmd_line_name: str | None = None, toml_name: str | None = None, @@ -112,13 +112,14 @@ def __init__( metavar: str | None = None, default: T | str = 'NoDefault', ) -> None: - self._name = name, + self._name = name self._aliases = list(aliases) self._cmd_line_name = cmd_line_name or name self._toml_name = cmd_line_name or name self._optional = optional self._help_str = help_str self._metavar = metavar + self._type = type if default == 'NoDefault' and optional: raise ValueError(f'Optional option {name} must define a default value.') @@ -148,22 +149,36 @@ def toml_name(self) -> str: return self._toml_name @property - def help_str(self) -> str: + def help_str(self) -> str | None: return self._help_str @property - def metavar(self) -> str: + def metavar(self) -> str | None: return self._metavar @property - def type(self) -> str: - return T + def default(self) -> T | str: + return self._default + + @property + def type(self) -> type: + return self._type + class Command: - _options: Options + _options_group: OptionsGroup _name: str _help_str: str + def extract(self, args: dict[str, Any]) -> None: + for option in self._options_group.options: + if option.name in args: + assert isinstance(args[option.name], option.type) + self.__setattr__(option.name, args[option.name]) + # TODO elif option exists in TOML file, set it to the value from there + else: + self.__setattr__(option.name, option.default) + @property def name(self) -> str: return self._name @@ -173,19 +188,43 @@ def help_str(self) -> str: return self._help_str @property - def options(self) -> Options: - return self._options + def options(self) -> list[Option]: + return self._options_group.options @abstractmethod - def exec(self) -> None: - ... + def exec(self) -> None: ... -class Options: + +class OptionsGroup: _options: dict[str, Option] - def add_option(self, option: Option) -> dict[str, Any]: + def add_option(self, option: Option) -> None: self._options[option.name] = option def override_default(self, option_name: str, value: T) -> None: if not self._options[option_name].is_optional: raise ValueError(f'Cannot provide a default value for a required parameter: {option_name}') + + @property + def options(self) -> list[Option]: + return list(self._options.values()) + + +# TODO remove once all implementing semantics use `CLI` system +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) + + @staticmethod + def from_option_string() -> dict[str, str]: + return {} From b34af86c8617b523639f60a872bdba0b7c020ed9 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 29 Apr 2024 19:11:23 -0500 Subject: [PATCH 04/16] Add type-specific Options classes --- pyk/src/pyk/cli/args.py | 140 ++++++++++++++++---- pyk/src/pyk/cli/cli.py | 282 +++++++++++++++++++++++++++++++--------- 2 files changed, 340 insertions(+), 82 deletions(-) diff --git a/pyk/src/pyk/cli/args.py b/pyk/src/pyk/cli/args.py index ef3c1fe585a..ac05c9d3e65 100644 --- a/pyk/src/pyk/cli/args.py +++ b/pyk/src/pyk/cli/args.py @@ -7,7 +7,16 @@ from typing import IO, TYPE_CHECKING, Any from ..ktool.kompile import KompileBackend, LLVMKompileType, TypeInferenceMode, Warnings -from .cli import Option, Options, OptionsGroup +from .cli import ( + BoolOption, + DirPathOption, + EnumOption, + Options, + OptionsGroup, + StringListOption, + StringOption, + WriteFileOption, +) from .utils import bug_report_arg, dir_path, ensure_dir_path, file_path if TYPE_CHECKING: @@ -20,17 +29,14 @@ class LoggingOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() self.add_option( - Option( - name='debug', cmd_line_name='--debug', type=bool, optional=True, default=False, help_str='Debug output.' - ) + BoolOption(name='debug', cmd_line_name='--debug', optional=True, default=False, help_str='Debug output.') ) self.add_option( - Option( + BoolOption( name='verbose', cmd_line_name='--verbose', aliases=['-v'], toml_name='v', - type=bool, optional=True, default=False, help_str='Debug output.', @@ -60,7 +66,7 @@ class WarningOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() self.add_option( - Option( + BoolOption( name='warnings_to_errors', cmd_line_name='--warnings-to-errors', aliases=['-w2e'], @@ -68,11 +74,10 @@ def __init__(self) -> None: help_str='Turn warnings into errors (no effect on pyk, only subcommands).', optional=True, toml_name='w2e', - type=bool, ) ) self.add_option( - Option( + EnumOption( name='warnings', cmd_line_name='--warnings', aliases=['-w'], @@ -80,7 +85,7 @@ def __init__(self) -> None: help_str='Warnings to print about (no effect on pyk, only subcommands).', optional=True, toml_name='w', - type=Warnings, + enum_type=Warnings, ) ) @@ -108,12 +113,11 @@ class OutputFileOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() self.add_option( - Option( + WriteFileOption( name='output_file', cmd_line_name='--output-file', default=sys.stdout, optional=True, - type=IO[Any], ) ) @@ -132,7 +136,7 @@ class DefinitionOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() self.add_option( - Option(name='definition_dir', toml_name='definition', type=Path, help_str='Path to definition directory.') + DirPathOption(name='definition_dir', toml_name='definition', help_str='Path to definition directory.') ) @@ -150,7 +154,7 @@ def from_option_string() -> dict[str, Any]: class DisplayOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() - self.add_option(Option(name='minimize', type=bool, optional=True, default=True, help_str='Minimize output.')) + self.add_option(BoolOption(name='minimize', optional=True, default=True, help_str='Minimize output.')) class DisplayOptions(Options): @@ -163,18 +167,45 @@ def default() -> dict[str, Any]: } - class KDefinitionOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() - self.add_option(Option(name='includes', cmd_line_name='-I', type=list[str], optional=True, default=[], - help_str='Directories to lookup K definitions in.')) - self.add_option(Option(name='main_module', cmd_line_name='--main-module', type=(str | None), optional=True, default=None, - help_str='Name of the main module.')) - self.add_option(Option(name='syntax_module', cmd_line_name='--syntax-module', type=str | None, optional=True, default=None, - help_str='Name of the syntax module.')) - self.add_option(Option(name='md_selector', cmd_line_name='--md-selector', type=str, optional=True, - default='k', help_str='Code selector expression to use when reading markdown.')) + self.add_option( + StringListOption( + name='includes', + cmd_line_name='-I', + optional=True, + default=[], + help_str='Directories to lookup K definitions in.', + ) + ) + self.add_option( + StringOption( + name='main_module', + cmd_line_name='--main-module', + optional=True, + default=None, + help_str='Name of the main module.', + ) + ) + self.add_option( + StringOption( + name='syntax_module', + cmd_line_name='--syntax-module', + optional=True, + default=None, + help_str='Name of the syntax module.', + ) + ) + self.add_option( + StringOption( + name='md_selector', + cmd_line_name='--md-selector', + optional=True, + default='k', + help_str='Code selector expression to use when reading markdown.', + ) + ) class KDefinitionOptions(Options): @@ -194,6 +225,7 @@ def default() -> dict[str, Any]: 'includes': [], } + # @staticmethod # def from_option_string() -> dict[str, str]: # return { @@ -201,6 +233,29 @@ def default() -> dict[str, Any]: # } +class SaveDirOptionsGroup(OptionsGroup): + def __init__(self) -> None: + super().__init__() + self.add_option( + DirPathOption( + name='save_directory', + cmd_line_name='--save-directory', + optional=True, + default=None, + help_str='Directory to save proof artifacts at for reuse.', + ) + ) + self.add_option( + DirPathOption( + name='temp_directory', + cmd_line_name='--temp-directory', + optional=True, + default=None, + help_str='Directory to save proof intermediate temporaries to.', + ) + ) + + class SaveDirOptions(Options): save_directory: Path | None temp_directory: Path | None @@ -213,6 +268,45 @@ def default() -> dict[str, Any]: } +class SpecOptionsGroup(OptionsGroup): + def __init__(self) -> None: + super().__init__() + self.add_option( + DirPathOption( + name='spec_file', + optional=False, + help_str='Path to spec file.', + ) + ) + self.add_option( + StringOption( + name='spec_module', + cmd_line_name='--spec-module', + optional=True, + default=None, + help_str='Module with claims to be proven.', + ) + ) + self.add_option( + StringListOption( + name='claim_labels', + cmd_line_name='--claim', + optional=True, + default=None, + help_str='Only prove listed claims, MODULE_NAME.claim-id', + ) + ) + self.add_option( + StringListOption( + name='exclude_claim_labels', + cmd_line_name='--exclude-claim', + optional=True, + default=None, + help_str='Skip listed claims, MODULE_NAME.claim-id', + ) + ) + + class SpecOptions(SaveDirOptions): spec_file: Path spec_module: str | None diff --git a/pyk/src/pyk/cli/cli.py b/pyk/src/pyk/cli/cli.py index a7980b25d56..950538950d5 100644 --- a/pyk/src/pyk/cli/cli.py +++ b/pyk/src/pyk/cli/cli.py @@ -1,12 +1,22 @@ from __future__ import annotations from abc import abstractmethod -from argparse import ArgumentParser -from enum import Enum -from typing import Any, Generic, Iterable, TypeVar +from argparse import ArgumentParser, FileType +from pathlib import Path + +# from enum import Enum +from typing import IO, TYPE_CHECKING, Any, Iterable, TypeVar + +from ..utils import ensure_dir_path T = TypeVar('T') +if TYPE_CHECKING: + from enum import EnumMeta + + # from argparse import _SubParsersAction + from types import UnionType + class CLI: _commands: list[Command] @@ -23,54 +33,55 @@ def create_argument_parser(self) -> ArgumentParser: for command in self._commands: command_args = subparsers.add_parser(name=command.name, help=command.help_str) for option in command.options: - - if option.type is bool and option.is_optional: - command_args.add_argument( - option.cmd_line_name, - *(option.aliases), - default='NoDefault', - required=False, - type=option.type, - help=option.help_str, - metavar=option.metavar, - action='store_false' if option.default else 'store_true', - dest=option.name, - ) - elif issubclass(option.type, Enum) and option.is_optional: - command_args.add_argument( - option.cmd_line_name, - *(option.aliases), - default='NoDefault', - required=False, - type=option.type, - help=option.help_str, - metavar=option.metavar, - dest=option.name, - choices=list(option.type), - ) - elif isinstance(option.type, Iterable) and option.is_optional: - command_args.add_argument( - option.cmd_line_name, - *(option.aliases), - default='NoDefault', - required=False, - type=option.type, - help=option.help_str, - metavar=option.metavar, - action='append', - dest=option.name, - ) - else: - command_args.add_argument( - option.cmd_line_name, - *(option.aliases), - default='NoDefault', - required=(not option.is_optional), - type=option.type, - help=option.help_str, - metavar=option.metavar, - dest=option.name, - ) + option.add_arg(command_args) + + # if option.type is bool and option.is_optional: + # command_args.add_argument( + # option.cmd_line_name, + # *(option.aliases), + # default='NoDefault', + # required=False, + # type=option.type, + # help=option.help_str, + # metavar=option.metavar, + # action='store_false' if option.default else 'store_true', + # dest=option.name, + # ) + # elif issubclass(option.type, Enum) and option.is_optional: + # command_args.add_argument( + # option.cmd_line_name, + # *(option.aliases), + # default='NoDefault', + # required=False, + # type=option.type, + # help=option.help_str, + # metavar=option.metavar, + # dest=option.name, + # choices=list(option.type), + # ) + # elif isinstance(option.type, Iterable) and option.is_optional: + # command_args.add_argument( + # option.cmd_line_name, + # *(option.aliases), + # default='NoDefault', + # required=False, + # type=option.type, + # help=option.help_str, + # metavar=option.metavar, + # action='append', + # dest=option.name, + # ) + # else: + # command_args.add_argument( + # option.cmd_line_name, + # *(option.aliases), + # default='NoDefault', + # required=(not option.is_optional), + # type=option.type, + # help=option.help_str, + # metavar=option.metavar, + # dest=option.name, + # ) return args def get_command(self, args: dict[str, Any]) -> Command: @@ -89,7 +100,7 @@ def get_and_exec_command(self) -> None: cmd.exec() -class Option(Generic[T]): +class Option: _name: str _aliases: list[str] _cmd_line_name: str @@ -97,20 +108,18 @@ class Option(Generic[T]): _optional: bool _help_str: str | None _metavar: str | None - _default: T | str - _type: type[Any] + _default: Any def __init__( self, name: str, - type: type[Any], aliases: Iterable[str] = (), cmd_line_name: str | None = None, toml_name: str | None = None, optional: bool = False, help_str: str | None = None, metavar: str | None = None, - default: T | str = 'NoDefault', + default: Any = 'NoDefault', ) -> None: self._name = name self._aliases = list(aliases) @@ -126,7 +135,10 @@ def __init__( if default != 'NoDefault' and not optional: raise ValueError(f'Required option {name} cannot take a default value.') - self._default = default + self.set_default(default) + + @abstractmethod + def add_arg(self, parser: ArgumentParser) -> None: ... @property def is_optional(self) -> bool: @@ -157,14 +169,163 @@ def metavar(self) -> str | None: return self._metavar @property - def default(self) -> T | str: + def default(self) -> Any: return self._default + @abstractmethod + def set_default(self, default: Any) -> None: ... + @property - def type(self) -> type: + def type(self) -> type | UnionType: return self._type +class IntOption(Option): + + def set_default(self, default: Any) -> None: + assert isinstance(default, int) + self._default = default + + def add_arg(self, args: ArgumentParser) -> None: + args.add_argument( + self.cmd_line_name, + *(self.aliases), + default='NoDefault', + required=self.is_optional, + type=int, + help=self.help_str, + metavar=self.metavar, + dest=self.name, + ) + + +class BoolOption(Option): + + def set_default(self, default: Any) -> None: + assert isinstance(default, bool) + self._default = default + + def add_arg(self, args: ArgumentParser) -> None: + args.add_argument( + self.cmd_line_name, + *(self.aliases), + default='NoDefault', + required=self.is_optional, + type=bool, + help=self.help_str, + metavar=self.metavar, + action='store_false' if self.default else 'store_true', + dest=self.name, + ) + + +class StringOption(Option): + + def set_default(self, default: Any) -> None: + assert isinstance(default, str) + self._default = default + + def add_arg(self, args: ArgumentParser) -> None: + args.add_argument( + self.cmd_line_name, + *(self.aliases), + default='NoDefault', + required=not self.is_optional, + type=bool, + help=self.help_str, + metavar=self.metavar, + dest=self.name, + ) + + +class EnumOption(Option): + _enum_type: EnumMeta + + def __init__( + self, + enum_type: EnumMeta, + *args: Any, + **kwargs: Any, + ) -> None: + self._enum_type = enum_type + super.__init__(*args, **kwargs) + + def set_default(self, default: Any) -> None: + assert isinstance(default, self._enum_type) + self._default = default + + def add_arg(self, args: ArgumentParser) -> None: + args.add_argument( + self.cmd_line_name, + *(self.aliases), + default='NoDefault', + required=self.is_optional, + type=self._enum_type, + help=self.help_str, + metavar=self.metavar, + dest=self.name, + choices=list(self._enum_type), + ) + + +class WriteFileOption(Option): + + def set_default(self, default: Any) -> None: + assert isinstance(default, IO) + self._default = default + + def add_arg(self, args: ArgumentParser) -> None: + args.add_argument( + self.cmd_line_name, + *(self.aliases), + default='NoDefault', + required=self.is_optional, + type=FileType('w'), + help=self.help_str, + metavar=self.metavar, + dest=self.name, + ) + + +class DirPathOption(Option): + + def set_default(self, default: Any) -> None: + assert isinstance(default, Path) + self._default = default + + def add_arg(self, args: ArgumentParser) -> None: + args.add_argument( + self.cmd_line_name, + *(self.aliases), + default='NoDefault', + required=self.is_optional, + type=ensure_dir_path, + help=self.help_str, + metavar=self.metavar, + dest=self.name, + ) + + +class StringListOption(Option): + + def set_default(self, default: Any) -> None: + assert isinstance(default, Iterable) + self._default = default + + def add_arg(self, args: ArgumentParser) -> None: + args.add_argument( + self.cmd_line_name, + *(self.aliases), + default='NoDefault', + required=self.is_optional, + type=list[str], + help=self.help_str, + metavar=self.metavar, + dest=self.name, + action='append', + ) + + class Command: _options_group: OptionsGroup _name: str @@ -204,6 +365,9 @@ def add_option(self, option: Option) -> None: def override_default(self, option_name: str, value: T) -> None: if not self._options[option_name].is_optional: raise ValueError(f'Cannot provide a default value for a required parameter: {option_name}') + if option_name not in self._options: + raise ValueError(f'Cannot find option with name: {option_name}') + self._options[option_name].set_default(value) @property def options(self) -> list[Option]: From db7bba7434a9d876e50a2ad811f707e829c24942 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 29 Apr 2024 20:20:25 -0500 Subject: [PATCH 05/16] Add kompile options using new system --- pyk/src/pyk/cli/args.py | 216 ++++++++++++++++++++++++++++++++++++++++ pyk/src/pyk/cli/cli.py | 2 +- 2 files changed, 217 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/cli/args.py b/pyk/src/pyk/cli/args.py index ac05c9d3e65..7ff65868b51 100644 --- a/pyk/src/pyk/cli/args.py +++ b/pyk/src/pyk/cli/args.py @@ -11,6 +11,7 @@ BoolOption, DirPathOption, EnumOption, + IntOption, Options, OptionsGroup, StringListOption, @@ -291,6 +292,7 @@ def __init__(self) -> None: StringListOption( name='claim_labels', cmd_line_name='--claim', + toml_name='claim', optional=True, default=None, help_str='Only prove listed claims, MODULE_NAME.claim-id', @@ -300,6 +302,7 @@ def __init__(self) -> None: StringListOption( name='exclude_claim_labels', cmd_line_name='--exclude-claim', + toml_name='exclude-claim', optional=True, default=None, help_str='Skip listed claims, MODULE_NAME.claim-id', @@ -329,6 +332,187 @@ def from_option_string() -> dict[str, str]: } +class KompileOptionsGroup(OptionsGroup): + def __init__(self) -> None: + super().__init__() + self.add_option( + BoolOption( + name='emit_json', + cmd_line_name='--emit-json', + default=True, + help_str='Emit JSON definition after compilation.', + optional=True, + ) + ) + self.add_option( + BoolOption( + name='llvm_kompile', + cmd_line_name='--no-llvm-kompile', + default=False, + help_str='Do not run llvm-kompile process.', + optional=True, + ) + ) + self.add_option( + BoolOption( + name='llvm_library', + cmd_line_name='--with-llvm-library', + toml_name='with-llvm-library', + default=False, + help_str='Make kompile generate a dynamic llvm library.', + optional=True, + ) + ) + self.add_option( + BoolOption( + name='enable_llvm_debug', + cmd_line_name='--enable-llvm-debug', + default=False, + help_str='Make kompile generate debug symbols for llvm.', + optional=True, + ) + ) + self.add_option( + EnumOption( + enum_type=LLVMKompileType, + name='llvm_kompile_type', + cmd_line_name='--llvm-kompile-type', + default=None, + help_str='Mode to kompile LLVM backend in.', + ) + ) + self.add_option( + DirPathOption( + name='llvm_kompile_output', + cmd_line_name='--llvm-kompile-output', + default=None, + help_str='Location to put kompiled LLVM backend at.', + ) + ) + self.add_option( + BoolOption( + name='llvm_proof_hint_instrumentation', + cmd_line_name='--llvm-proof-hint-instrumentation', + default=False, + help_str='Enable proof hint generation in LLVM backend kompilation.', + optional=True, + ) + ) + self.add_option( + BoolOption( + name='read_only', + cmd_line_name='--read-only-kompiled-directory', + toml_name='read-only-kompiled-directory', + default=False, + help_str='Generate a kompiled directory that K will not attempt to write to afterwards.', + optional=True, + ) + ) + self.add_option( + BoolOption( + name='o0', + cmd_line_name='-O0', + toml_name='O0', + default=False, + help_str='Optimization level 0.', + optional=True, + ) + ) + self.add_option( + BoolOption( + name='o1', + cmd_line_name='-O1', + toml_name='O1', + default=False, + help_str='Optimization level 1.', + optional=True, + ) + ) + self.add_option( + BoolOption( + name='o2', + cmd_line_name='-O2', + toml_name='O2', + default=False, + help_str='Optimization level 2.', + optional=True, + ) + ) + self.add_option( + BoolOption( + name='o3', + cmd_line_name='-O3', + toml_name='O3', + default=False, + help_str='Optimization level 3.', + optional=True, + ) + ) + self.add_option( + StringListOption( + name='ccopts', + cmd_line_name='-ccopt', + optional=True, + default=[], + help_str='Additional arguments to pass to llvm-kompile', + ) + ) + self.add_option( + BoolOption( + name='enable_search', + cmd_line_name='--enable-search', + optional=True, + default=False, + help_str='Enable search mode on LLVM backend krun.', + ) + ) + self.add_option( + BoolOption( + name='coverage', + cmd_line_name='--coverage', + optional=True, + default=False, + help_str='Enable logging semantic rule coverage measurement.', + ) + ) + self.add_option( + BoolOption( + name='gen_bison_parser', + cmd_line_name='--gen-bison-parser', + optional=True, + default=False, + help_str='Generate standalone Bison parser for program sort.', + ) + ) + self.add_option( + BoolOption( + name='gen_glr_bison_parser', + cmd_line_name='--gen-glr-bison-parser', + optional=True, + default=False, + help_str='Generate standalone GLR Bison parser for program sort.', + ) + ) + self.add_option( + BoolOption( + name='bison_lists', + cmd_line_name='--bison-lists', + optional=True, + default=False, + help_str='Disable List{Sort} parsing to make grammar LR(1) for Bison parser.', + ) + ) + self.add_option( + BoolOption( + name='no_exc_wrap', + cmd_line_name='--no-exc-wrap', + optional=True, + default=False, + help_str='Do not wrap the output on the CLI.', + ) + ) + + class KompileOptions(Options): emit_json: bool llvm_kompile: bool @@ -387,6 +571,22 @@ def from_option_string() -> dict[str, str]: } +class ParallelOptionsGroup(OptionsGroup): + def __init__(self) -> None: + super().__init__() + self.add_option( + IntOption( + name='workers', + aliases=['-j'], + cmd_line_name='--workers', + toml_name='j', + default=1, + help_str='Number of processes to run in parallel', + optional=True, + ) + ) + + class ParallelOptions(Options): workers: int @@ -403,6 +603,22 @@ def from_option_string() -> dict[str, str]: } +# class BugReportOptionsGroup(OptionsGroup): +# def __init__(self) -> None: +# super().__init__() +# self.add_option( +# IntOption( +# name='workers', +# aliases=['-j'], +# cmd_line_name='--workers', +# toml_name='j', +# default=1, +# help_str='Number of processes to run in parallel', +# optional=True, +# ) +# ) + + class BugReportOptions(Options): bug_report: BugReport | None diff --git a/pyk/src/pyk/cli/cli.py b/pyk/src/pyk/cli/cli.py index 950538950d5..eefb395d357 100644 --- a/pyk/src/pyk/cli/cli.py +++ b/pyk/src/pyk/cli/cli.py @@ -247,8 +247,8 @@ def __init__( *args: Any, **kwargs: Any, ) -> None: - self._enum_type = enum_type super.__init__(*args, **kwargs) + self._enum_type = enum_type def set_default(self, default: Any) -> None: assert isinstance(default, self._enum_type) From 6a156e974ce675da0db90c219a53c50d2547d2e6 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 30 Apr 2024 14:42:03 -0500 Subject: [PATCH 06/16] Move 3 commands to new system --- pyk/src/pyk/__main__.py | 142 ++++++++++++------- pyk/src/pyk/cli/args.py | 63 +++++++-- pyk/src/pyk/cli/cli.py | 105 +++++++------- pyk/src/pyk/cli/pyk.py | 198 +++++++++++++-------------- pyk/src/tests/unit/test_toml_args.py | 84 ++++++------ 5 files changed, 336 insertions(+), 256 deletions(-) diff --git a/pyk/src/pyk/__main__.py b/pyk/src/pyk/__main__.py index ccd22598709..9fc054d8bcd 100644 --- a/pyk/src/pyk/__main__.py +++ b/pyk/src/pyk/__main__.py @@ -3,14 +3,14 @@ import json import logging import sys -from collections.abc import Iterable from pathlib import Path from typing import TYPE_CHECKING from graphviz import Digraph -from .cli.pyk import PrintInput, create_argument_parser, generate_options, parse_toml_args -from .cli.utils import LOG_FORMAT, loglevel +from .cli.args import DefinitionOptionsGroup, LoggingOptionsGroup, OutputFileOptionsGroup +from .cli.cli import CLI, Command, ReadFileOption +from .cli.pyk import PrintInput from .coverage import get_rule_by_id, strip_coverage_logger from .cterm import CTerm from .kast.inner import KInner @@ -38,14 +38,11 @@ from .utils import check_file_path, ensure_dir_path, exit_with_process_error if TYPE_CHECKING: - from typing import Any, Final + from typing import IO, Any, Final from .cli.pyk import ( - CoverageOptions, GraphImportsOptions, - JsonToKoreOptions, KompileCommandOptions, - KoreToJsonOptions, PrintOptions, ProveLegacyOptions, ProveOptions, @@ -64,24 +61,29 @@ def main() -> None: # This change makes it so that in most cases, by default, pyk doesn't run out of stack space. sys.setrecursionlimit(10**7) - cli_parser = create_argument_parser() - args = cli_parser.parse_args() - toml_args = parse_toml_args(args) - - stripped_args = toml_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('-', '_') - if executor_name not in globals(): - raise AssertionError(f'Unimplemented command: {args.command}') - - execute = globals()[executor_name] - execute(options) + cli = CLI([JsonToKoreCommand(), JsonToKoreCommand(), CoverageCommand()]) + cli.get_and_exec_command() + + +# +# cli_parser = create_argument_parser() +# args = cli_parser.parse_args() +# toml_args = parse_toml_args(args) +# +# stripped_args = toml_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('-', '_') +# if executor_name not in globals(): +# raise AssertionError(f'Unimplemented command: {args.command}') +# +# execute = globals()[executor_name] +# execute(options) def exec_print(options: PrintOptions) -> None: @@ -357,30 +359,78 @@ def exec_graph_imports(options: GraphImportsOptions) -> None: _LOGGER.info(f'Wrote file: {graph_file}') -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 options.coverage_file: - rule = minimize_rule(strip_coverage_logger(get_rule_by_id(definition, rid.strip()))) - 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}') +class CoverageOptionsGroup(DefinitionOptionsGroup, OutputFileOptionsGroup, LoggingOptionsGroup): + coverage_file: IO[Any] - -def exec_kore_to_json(options: KoreToJsonOptions) -> None: - text = sys.stdin.read() - kore = KoreParser(text).pattern() - print(kore.json) + def __init__(self) -> None: + super().__init__() + self.add_option( + ReadFileOption(name='coverage_file', optional=False, help_str='Coverage fild to build log for.') + ) -def exec_json_to_kore(options: JsonToKoreOptions) -> None: - text = sys.stdin.read() - kore = Pattern.from_json(text) - kore.write(sys.stdout) - sys.stdout.write('\n') +class CoverageCommand(Command[CoverageOptionsGroup]): + def __init__(self) -> None: + super().__init__('coverage-options', 'Convert coverage file to human readable log.', CoverageOptionsGroup()) + + def exec(self) -> None: + kompiled_dir: Path = self.options.definition_dir + definition = remove_source_map(read_kast_definition(kompiled_dir / 'compiled.json')) + pretty_printer = PrettyPrinter(definition) + for rid in self.options.coverage_file: + rule = minimize_rule(strip_coverage_logger(get_rule_by_id(definition, rid.strip()))) + self.options.output_file.write('\n\n') + self.options.output_file.write('Rule: ' + rid.strip()) + self.options.output_file.write('\nUnparsed:\n') + self.options.output_file.write(pretty_printer.print(rule)) + _LOGGER.info(f'Wrote file: {self.options.output_file.name}') + + +# 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 options.coverage_file: +# rule = minimize_rule(strip_coverage_logger(get_rule_by_id(definition, rid.strip()))) +# 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}') + + +class KoreToJsonCommand(Command[LoggingOptionsGroup]): + def __init__(self) -> None: + super().__init__('kore-to-json', 'convert textual KORE to JSON', LoggingOptionsGroup()) + + def exec(self) -> None: + text = sys.stdin.read() + kore = KoreParser(text).pattern() + print(kore.json) + + +# def exec_kore_to_json(options: KoreToJsonOptions) -> None: +# text = sys.stdin.read() +# kore = KoreParser(text).pattern() +# print(kore.json) + + +class JsonToKoreCommand(Command[LoggingOptionsGroup]): + def __init__(self) -> None: + super().__init__('json-to-kore', 'convert JSON to textual KORE', LoggingOptionsGroup()) + + def exec(self) -> None: + text = sys.stdin.read() + kore = Pattern.from_json(text) + kore.write(sys.stdout) + sys.stdout.write('\n') + + +# def exec_json_to_kore(options: JsonToKoreOptions) -> None: +# text = sys.stdin.read() +# kore = Pattern.from_json(text) +# kore.write(sys.stdout) +# sys.stdout.write('\n') if __name__ == '__main__': diff --git a/pyk/src/pyk/cli/args.py b/pyk/src/pyk/cli/args.py index 7ff65868b51..bf5d0ba232b 100644 --- a/pyk/src/pyk/cli/args.py +++ b/pyk/src/pyk/cli/args.py @@ -9,6 +9,7 @@ from ..ktool.kompile import KompileBackend, LLVMKompileType, TypeInferenceMode, Warnings from .cli import ( BoolOption, + BugReportOption, DirPathOption, EnumOption, IntOption, @@ -111,6 +112,8 @@ def from_option_string() -> dict[str, Any]: class OutputFileOptionsGroup(OptionsGroup): + output_file: IO[Any] + def __init__(self) -> None: super().__init__() self.add_option( @@ -134,6 +137,8 @@ def default() -> dict[str, Any]: class DefinitionOptionsGroup(OptionsGroup): + definition_dir: Path + def __init__(self) -> None: super().__init__() self.add_option( @@ -603,20 +608,18 @@ def from_option_string() -> dict[str, str]: } -# class BugReportOptionsGroup(OptionsGroup): -# def __init__(self) -> None: -# super().__init__() -# self.add_option( -# IntOption( -# name='workers', -# aliases=['-j'], -# cmd_line_name='--workers', -# toml_name='j', -# default=1, -# help_str='Number of processes to run in parallel', -# optional=True, -# ) -# ) +class BugReportOptionsGroup(OptionsGroup): + def __init__(self) -> None: + super().__init__() + self.add_option( + BugReportOption( + name='bug_report', + cmd_line_name='--bug-report', + default=None, + help_str='Generate bug report with given name.', + optional=True, + ) + ) class BugReportOptions(Options): @@ -627,6 +630,38 @@ def default() -> dict[str, Any]: return {'bug_report': None} +class SMTOptionsGroup(OptionsGroup): + def __init__(self) -> None: + super().__init__() + self.add_option( + IntOption( + name='smt_timeout', + cmd_line_name='--smt-timeout', + default=300, + help_str='Timeout in ms to use for SMT queries.', + optional=True, + ) + ) + self.add_option( + IntOption( + name='smt_retry_limit', + cmd_line_name='--smt-retry-limit', + default=10, + help_str='Number of times to retry SMT queries with scaling timeouts.', + optional=True, + ) + ) + self.add_option( + StringOption( + name='smt_tactic', + cmd_line_name='--smt-tactic', + default=None, + help_str='Z3 tactic to use when checking satisfiability. Example: (check-sat-using-smt)', + optional=True, + ) + ) + + class SMTOptions(Options): smt_timeout: int smt_retry_limit: int diff --git a/pyk/src/pyk/cli/cli.py b/pyk/src/pyk/cli/cli.py index eefb395d357..fba73a7b76d 100644 --- a/pyk/src/pyk/cli/cli.py +++ b/pyk/src/pyk/cli/cli.py @@ -5,11 +5,13 @@ from pathlib import Path # from enum import Enum -from typing import IO, TYPE_CHECKING, Any, Iterable, TypeVar +from typing import IO, TYPE_CHECKING, Any, Generic, Iterable, TypeVar from ..utils import ensure_dir_path +from .utils import BugReport, bug_report_arg T = TypeVar('T') +OG = TypeVar('OG', bound='OptionsGroup') if TYPE_CHECKING: from enum import EnumMeta @@ -32,56 +34,8 @@ def create_argument_parser(self) -> ArgumentParser: subparsers = args.add_subparsers(dest='command', required=True) for command in self._commands: command_args = subparsers.add_parser(name=command.name, help=command.help_str) - for option in command.options: + for option in command._options_group.options: option.add_arg(command_args) - - # if option.type is bool and option.is_optional: - # command_args.add_argument( - # option.cmd_line_name, - # *(option.aliases), - # default='NoDefault', - # required=False, - # type=option.type, - # help=option.help_str, - # metavar=option.metavar, - # action='store_false' if option.default else 'store_true', - # dest=option.name, - # ) - # elif issubclass(option.type, Enum) and option.is_optional: - # command_args.add_argument( - # option.cmd_line_name, - # *(option.aliases), - # default='NoDefault', - # required=False, - # type=option.type, - # help=option.help_str, - # metavar=option.metavar, - # dest=option.name, - # choices=list(option.type), - # ) - # elif isinstance(option.type, Iterable) and option.is_optional: - # command_args.add_argument( - # option.cmd_line_name, - # *(option.aliases), - # default='NoDefault', - # required=False, - # type=option.type, - # help=option.help_str, - # metavar=option.metavar, - # action='append', - # dest=option.name, - # ) - # else: - # command_args.add_argument( - # option.cmd_line_name, - # *(option.aliases), - # default='NoDefault', - # required=(not option.is_optional), - # type=option.type, - # help=option.help_str, - # metavar=option.metavar, - # dest=option.name, - # ) return args def get_command(self, args: dict[str, Any]) -> Command: @@ -268,6 +222,25 @@ def add_arg(self, args: ArgumentParser) -> None: ) +class ReadFileOption(Option): + + def set_default(self, default: Any) -> None: + assert isinstance(default, IO) + self._default = default + + def add_arg(self, args: ArgumentParser) -> None: + args.add_argument( + self.cmd_line_name, + *(self.aliases), + default='NoDefault', + required=self.is_optional, + type=FileType('r'), + help=self.help_str, + metavar=self.metavar, + dest=self.name, + ) + + class WriteFileOption(Option): def set_default(self, default: Any) -> None: @@ -287,6 +260,25 @@ def add_arg(self, args: ArgumentParser) -> None: ) +class BugReportOption(Option): + + def set_default(self, default: Any) -> None: + assert isinstance(default, BugReport) + self._default = default + + def add_arg(self, args: ArgumentParser) -> None: + args.add_argument( + self.cmd_line_name, + *(self.aliases), + default='NoDefault', + required=self.is_optional, + type=bug_report_arg, + help=self.help_str, + metavar=self.metavar, + dest=self.name, + ) + + class DirPathOption(Option): def set_default(self, default: Any) -> None: @@ -326,8 +318,8 @@ def add_arg(self, args: ArgumentParser) -> None: ) -class Command: - _options_group: OptionsGroup +class Command(Generic[OG]): + _options_group: OG _name: str _help_str: str @@ -340,6 +332,11 @@ def extract(self, args: dict[str, Any]) -> None: else: self.__setattr__(option.name, option.default) + def __init__(self, name: str, help_str: str, options_group: OG) -> None: + self._name = name + self._help_str = help_str + self._options_group = options_group + @property def name(self) -> str: return self._name @@ -349,8 +346,8 @@ def help_str(self) -> str: return self._help_str @property - def options(self) -> list[Option]: - return self._options_group.options + def options(self) -> OG: + return self._options_group @abstractmethod def exec(self) -> None: ... diff --git a/pyk/src/pyk/cli/pyk.py b/pyk/src/pyk/cli/pyk.py index b5d381ef3c2..d3ab081565e 100644 --- a/pyk/src/pyk/cli/pyk.py +++ b/pyk/src/pyk/cli/pyk.py @@ -5,8 +5,6 @@ from enum import Enum from typing import IO, TYPE_CHECKING, Any -import tomli - from ..ktool.kompile import KompileBackend from .args import ( ConfigArgs, @@ -23,8 +21,10 @@ ) from .utils import dir_path +# import tomli + + if TYPE_CHECKING: - from argparse import Namespace from collections.abc import Iterable from pathlib import Path from typing import Final @@ -34,67 +34,67 @@ _LOGGER: Final = logging.getLogger(__name__) -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 'show': - return ProveOptions(args) - case 'kompile': - return KompileCommandOptions(args) - case 'run': - return RunOptions(args) - case _: - raise ValueError(f'Unrecognized command: {command}') - - -def get_option_string_destination(command: str, option_string: str) -> str: - option_string_destinations = {} - match command: - case 'json-to-kore': - option_string_destinations = JsonToKoreOptions.from_option_string() - case 'kore-to-json': - option_string_destinations = KoreToJsonOptions.from_option_string() - case 'coverage': - option_string_destinations = CoverageOptions.from_option_string() - case 'graph-imports': - option_string_destinations = GraphImportsOptions.from_option_string() - case 'rpc-kast': - option_string_destinations = RPCKastOptions.from_option_string() - case 'rpc-print': - option_string_destinations = RPCPrintOptions.from_option_string() - case 'print': - option_string_destinations = PrintOptions.from_option_string() - case 'prove-legacy': - option_string_destinations = ProveLegacyOptions.from_option_string() - case 'prove': - option_string_destinations = ProveOptions.from_option_string() - case 'kompile': - option_string_destinations = KompileCommandOptions.from_option_string() - case 'run': - option_string_destinations = RunOptions.from_option_string() - - if option_string in option_string_destinations: - return option_string_destinations[option_string] - else: - return option_string.replace('-', '_') +# 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 'show': +# return ProveOptions(args) +# case 'kompile': +# return KompileCommandOptions(args) +# case 'run': +# return RunOptions(args) +# case _: +# raise ValueError(f'Unrecognized command: {command}') + + +# def get_option_string_destination(command: str, option_string: str) -> str: +# option_string_destinations = {} +# match command: +# case 'json-to-kore': +# option_string_destinations = JsonToKoreOptions.from_option_string() +# case 'kore-to-json': +# option_string_destinations = KoreToJsonOptions.from_option_string() +# case 'coverage': +# option_string_destinations = CoverageOptions.from_option_string() +# case 'graph-imports': +# option_string_destinations = GraphImportsOptions.from_option_string() +# case 'rpc-kast': +# option_string_destinations = RPCKastOptions.from_option_string() +# case 'rpc-print': +# option_string_destinations = RPCPrintOptions.from_option_string() +# case 'print': +# option_string_destinations = PrintOptions.from_option_string() +# case 'prove-legacy': +# option_string_destinations = ProveLegacyOptions.from_option_string() +# case 'prove': +# option_string_destinations = ProveOptions.from_option_string() +# case 'kompile': +# option_string_destinations = KompileCommandOptions.from_option_string() +# case 'run': +# option_string_destinations = RunOptions.from_option_string() +# +# if option_string in option_string_destinations: +# return option_string_destinations[option_string] +# else: +# return option_string.replace('-', '_') class PrintInput(Enum): @@ -102,10 +102,10 @@ class PrintInput(Enum): KAST_JSON = 'kast-json' -class JsonToKoreOptions(LoggingOptions): ... +# class JsonToKoreOptions(LoggingOptions): ... -class KoreToJsonOptions(LoggingOptions): ... +# class KoreToJsonOptions(LoggingOptions): ... class CoverageOptions(DefinitionOptions, OutputFileOptions, LoggingOptions): @@ -409,36 +409,36 @@ def create_argument_parser() -> ArgumentParser: return pyk_args -def parse_toml_args(args: Namespace) -> dict[str, Any | Iterable]: - def get_profile(toml_profile: dict[str, Any], profile_list: list[str]) -> dict[str, Any]: - if len(profile_list) == 0 or profile_list[0] not in toml_profile: - return {k: v for k, v in toml_profile.items() if type(v) is not dict} - elif len(profile_list) == 1: - return {k: v for k, v in toml_profile[profile_list[0]].items() if type(v) is not dict} - return get_profile(toml_profile[profile_list[0]], profile_list[1:]) - - toml_args = {} - if args.config_file.is_file(): - with open(args.config_file, 'rb') as config_file: - try: - toml_args = tomli.load(config_file) - except tomli.TOMLDecodeError: - _LOGGER.error( - 'Input config file is not in TOML format, ignoring the file and carrying on with the provided command line agruments' - ) - - toml_args = ( - get_profile(toml_args[args.command], args.config_profile.split('.')) if args.command in toml_args else {} - ) - toml_args = {get_option_string_destination(args.command, k): v for k, v in toml_args.items()} - for k, v in toml_args.items(): - if k[:3] == 'no-' and (v == 'true' or v == 'false'): - del toml_args[k] - toml_args[k[3:]] = 'false' if v == 'true' else 'true' - if k == 'optimization-level': - level = toml_args[k] if toml_args[k] >= 0 else 0 - level = level if toml_args[k] <= 3 else 3 - del toml_args[k] - toml_args['-o' + str(level)] = 'true' - - return toml_args +# def parse_toml_args(args: Namespace) -> dict[str, Any | Iterable]: +# def get_profile(toml_profile: dict[str, Any], profile_list: list[str]) -> dict[str, Any]: +# if len(profile_list) == 0 or profile_list[0] not in toml_profile: +# return {k: v for k, v in toml_profile.items() if type(v) is not dict} +# elif len(profile_list) == 1: +# return {k: v for k, v in toml_profile[profile_list[0]].items() if type(v) is not dict} +# return get_profile(toml_profile[profile_list[0]], profile_list[1:]) +# +# toml_args = {} +# if args.config_file.is_file(): +# with open(args.config_file, 'rb') as config_file: +# try: +# toml_args = tomli.load(config_file) +# except tomli.TOMLDecodeError: +# _LOGGER.error( +# 'Input config file is not in TOML format, ignoring the file and carrying on with the provided command line agruments' +# ) +# +# toml_args = ( +# get_profile(toml_args[args.command], args.config_profile.split('.')) if args.command in toml_args else {} +# ) +# toml_args = {get_option_string_destination(args.command, k): v for k, v in toml_args.items()} +# for k, v in toml_args.items(): +# if k[:3] == 'no-' and (v == 'true' or v == 'false'): +# del toml_args[k] +# toml_args[k[3:]] = 'false' if v == 'true' else 'true' +# if k == 'optimization-level': +# level = toml_args[k] if toml_args[k] >= 0 else 0 +# level = level if toml_args[k] <= 3 else 3 +# del toml_args[k] +# toml_args['-o' + str(level)] = 'true' +# +# return toml_args diff --git a/pyk/src/tests/unit/test_toml_args.py b/pyk/src/tests/unit/test_toml_args.py index 2f10fbc5a4a..522d84bc336 100644 --- a/pyk/src/tests/unit/test_toml_args.py +++ b/pyk/src/tests/unit/test_toml_args.py @@ -2,8 +2,6 @@ from typing import TYPE_CHECKING -from pyk.cli.pyk import create_argument_parser, parse_toml_args - from .utils import TEST_DATA_DIR if TYPE_CHECKING: @@ -12,44 +10,44 @@ TEST_TOML: Final = TEST_DATA_DIR / 'pyk_toml_test.toml' -def test_continue_when_default_toml_absent() -> None: - parser = create_argument_parser() - cmd_args = ['coverage', '.', str(TEST_TOML)] - args = parser.parse_args(cmd_args) - assert hasattr(args, 'config_file') - assert str(args.config_file) == 'pyk.toml' - assert hasattr(args, 'config_profile') - assert str(args.config_profile) == 'default' - args_dict = parse_toml_args(args) - assert len(args_dict) == 0 - - -def test_toml_read() -> None: - parser = create_argument_parser() - cmd_args = ['coverage', '--config-file', str(TEST_TOML), '.', str(TEST_TOML), '--verbose'] - args = parser.parse_args(cmd_args) - args_dict = parse_toml_args(args) - assert 'output' in args_dict - assert args_dict['output'] == 'default-file' - assert hasattr(args, 'verbose') - assert args.verbose - - -def test_toml_profiles() -> None: - parser = create_argument_parser() - cmd_args = [ - 'coverage', - '--config-file', - str(TEST_TOML), - '--config-profile', - 'a_profile', - '.', - str(TEST_TOML), - '--verbose', - ] - args = parser.parse_args(cmd_args) - args_dict = parse_toml_args(args) - assert 'verbose' in args_dict - assert args_dict['verbose'] - assert 'output' in args_dict - assert args_dict['output'] == 'a-profile-file' +# def test_continue_when_default_toml_absent() -> None: +# parser = create_argument_parser() +# cmd_args = ['coverage', '.', str(TEST_TOML)] +# args = parser.parse_args(cmd_args) +# assert hasattr(args, 'config_file') +# assert str(args.config_file) == 'pyk.toml' +# assert hasattr(args, 'config_profile') +# assert str(args.config_profile) == 'default' +# args_dict = parse_toml_args(args) +# assert len(args_dict) == 0 +# +# +# def test_toml_read() -> None: +# parser = create_argument_parser() +# cmd_args = ['coverage', '--config-file', str(TEST_TOML), '.', str(TEST_TOML), '--verbose'] +# args = parser.parse_args(cmd_args) +# args_dict = parse_toml_args(args) +# assert 'output' in args_dict +# assert args_dict['output'] == 'default-file' +# assert hasattr(args, 'verbose') +# assert args.verbose +# +# +# def test_toml_profiles() -> None: +# parser = create_argument_parser() +# cmd_args = [ +# 'coverage', +# '--config-file', +# str(TEST_TOML), +# '--config-profile', +# 'a_profile', +# '.', +# str(TEST_TOML), +# '--verbose', +# ] +# args = parser.parse_args(cmd_args) +# args_dict = parse_toml_args(args) +# assert 'verbose' in args_dict +# assert args_dict['verbose'] +# assert 'output' in args_dict +# assert args_dict['output'] == 'a-profile-file' From 8a0d2b8d139ab0ef166412aa1f49a4ee4ba8141b Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 30 Apr 2024 15:50:30 -0500 Subject: [PATCH 07/16] Move kompile and run commands to new system --- pyk/src/pyk/__main__.py | 388 ++++++++++++++++++++++++++++++---------- pyk/src/pyk/cli/args.py | 28 +++ pyk/src/pyk/cli/pyk.py | 81 +++++---- 3 files changed, 366 insertions(+), 131 deletions(-) diff --git a/pyk/src/pyk/__main__.py b/pyk/src/pyk/__main__.py index 9fc054d8bcd..4349e63edce 100644 --- a/pyk/src/pyk/__main__.py +++ b/pyk/src/pyk/__main__.py @@ -8,8 +8,15 @@ from graphviz import Digraph -from .cli.args import DefinitionOptionsGroup, LoggingOptionsGroup, OutputFileOptionsGroup -from .cli.cli import CLI, Command, ReadFileOption +from .cli.args import ( + DefinitionOptionsGroup, + KDefinitionOptionsGroup, + KompileOptionsGroup, + LoggingOptionsGroup, + OutputFileOptionsGroup, + WarningOptionsGroup, +) +from .cli.cli import CLI, Command, DirPathOption, EnumOption, ReadFileOption, StringOption from .cli.pyk import PrintInput from .coverage import get_rule_by_id, strip_coverage_logger from .cterm import CTerm @@ -27,6 +34,7 @@ from .kore.parser import KoreParser from .kore.rpc import ExecuteResult, StopReason from .kore.syntax import Pattern, kore_term +from .ktool._ktool import TypeInferenceMode from .ktool.kompile import Kompile, KompileBackend from .ktool.kprint import KPrint from .ktool.kprove import KProve @@ -40,16 +48,7 @@ if TYPE_CHECKING: from typing import IO, Any, Final - from .cli.pyk import ( - GraphImportsOptions, - KompileCommandOptions, - PrintOptions, - ProveLegacyOptions, - ProveOptions, - RPCKastOptions, - RPCPrintOptions, - RunOptions, - ) + from .cli.pyk import PrintOptions, ProveLegacyOptions, ProveOptions, RPCKastOptions, RPCPrintOptions _LOGGER: Final = logging.getLogger(__name__) @@ -269,94 +268,303 @@ def exec_show(options: ProveOptions) -> None: exec_prove(options) -def exec_kompile(options: KompileCommandOptions) -> None: - main_file = Path(options.main_file) - check_file_path(main_file) - - kompiled_directory: Path - if options.definition_dir is None: - kompiled_directory = Path(f'{main_file.stem}-kompiled') - ensure_dir_path(kompiled_directory) - else: - kompiled_directory = options.definition_dir +# class KompileCommandOptions(LoggingOptions, WarningOptions, KDefinitionOptions, KompileOptions): +# 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, +# } +# +# @staticmethod +# def from_option_string() -> dict[str, str]: +# return ( +# KDefinitionOptions.from_option_string() +# | KompileOptions.from_option_string() +# | LoggingOptions.from_option_string() +# | {'definition': 'definition_dir'} +# ) + + +class KompileCommandOptionsGroup( + LoggingOptionsGroup, WarningOptionsGroup, KDefinitionOptionsGroup, KompileOptionsGroup +): + definition_dir: Path | None + main_file: str + backend: KompileBackend + type_inference_mode: TypeInferenceMode | None - kompile_dict: dict[str, Any] = { - 'main_file': main_file, - '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), - 'emit_json': options.emit_json, - 'coverage': options.coverage, - 'gen_bison_parser': options.gen_bison_parser, - 'gen_glr_bison_parser': options.gen_glr_bison_parser, - 'bison_lists': options.bison_lists, - } - if options.backend == KompileBackend.LLVM: - kompile_dict['ccopts'] = options.ccopts - kompile_dict['enable_search'] = options.enable_search - kompile_dict['llvm_kompile_type'] = options.llvm_kompile_type - kompile_dict['llvm_kompile_output'] = options.llvm_kompile_output - kompile_dict['llvm_proof_hint_instrumentation'] = options.llvm_proof_hint_instrumentation - elif len(options.ccopts) > 0: - raise ValueError(f'Option `-ccopt` requires `--backend llvm`, not: --backend {options.backend.value}') - elif options.enable_search: - raise ValueError(f'Option `--enable-search` requires `--backend llvm`, not: --backend {options.backend.value}') - elif options.llvm_kompile_type: - raise ValueError( - f'Option `--llvm-kompile-type` requires `--backend llvm`, not: --backend {options.backend.value}' + def __init__(self) -> None: + super().__init__() + self.add_option( + DirPathOption( + name='definition_dir', + cmd_line_name='--output-definition', + aliases=['--definition'], + toml_name='definition', + default=None, + help_str='Path to kompile definition to.', + optional=True, + ) + ) + self.add_option( + StringOption( + name='main_file', + optional=False, + help_str='File with the specification module.', + ) ) - elif options.llvm_kompile_output: - raise ValueError( - f'Option `--llvm-kompile-output` requires `--backend llvm`, not: --backend {options.backend.value}' + self.add_option( + EnumOption( + enum_type=KompileBackend, + name='backend', + cmd_line_name='--backend', + default=KompileBackend.LLVM, + help_str='K backend to target with compilation.', + optional=True, + ) ) - elif options.llvm_proof_hint_instrumentation: - raise ValueError( - f'Option `--llvm-proof-hint-intrumentation` requires `--backend llvm`, not: --backend {options.backend.value}' + self.add_option( + EnumOption( + enum_type=TypeInferenceMode, + name='type_inference_mode', + cmd_line_name='--type-inference-mode', + default=None, + help_str='Mode for doing K rule type inference in.', + optional=True, + ) ) - try: - Kompile.from_dict(kompile_dict)( - output_dir=kompiled_directory, - type_inference_mode=options.type_inference_mode, - warnings=options.warnings, - warnings_to_errors=options.warnings_to_errors, - no_exc_wrap=options.no_exc_wrap, + +class KompileCommand(Command[KompileCommandOptionsGroup]): + def __init__(self) -> None: + super().__init__('kompile', 'Kompile the K specification', KompileCommandOptionsGroup()) + + def exec(self) -> None: + main_file = Path(self.options.main_file) + check_file_path(main_file) + + kompiled_directory: Path + if self.options.definition_dir is None: + kompiled_directory = Path(f'{main_file.stem}-kompiled') + ensure_dir_path(kompiled_directory) + else: + kompiled_directory = self.options.definition_dir + + kompile_dict: dict[str, Any] = { + 'main_file': main_file, + 'backend': self.options.backend.value, + 'syntax_module': self.options.syntax_module, + 'main_module': self.options.main_module, + 'md_selector': self.options.md_selector, + 'include_dirs': (Path(include) for include in self.options.includes), + 'emit_json': self.options.emit_json, + 'coverage': self.options.coverage, + 'gen_bison_parser': self.options.gen_bison_parser, + 'gen_glr_bison_parser': self.options.gen_glr_bison_parser, + 'bison_lists': self.options.bison_lists, + } + if self.options.backend == KompileBackend.LLVM: + kompile_dict['ccopts'] = self.options.ccopts + kompile_dict['enable_search'] = self.options.enable_search + kompile_dict['llvm_kompile_type'] = self.options.llvm_kompile_type + kompile_dict['llvm_kompile_output'] = self.options.llvm_kompile_output + kompile_dict['llvm_proof_hint_instrumentation'] = self.options.llvm_proof_hint_instrumentation + elif len(self.options.ccopts) > 0: + raise ValueError(f'Option `-ccopt` requires `--backend llvm`, not: --backend {self.options.backend.value}') + elif self.options.enable_search: + raise ValueError( + f'Option `--enable-search` requires `--backend llvm`, not: --backend {self.options.backend.value}' + ) + elif self.options.llvm_kompile_type: + raise ValueError( + f'Option `--llvm-kompile-type` requires `--backend llvm`, not: --backend {self.options.backend.value}' + ) + elif self.options.llvm_kompile_output: + raise ValueError( + f'Option `--llvm-kompile-output` requires `--backend llvm`, not: --backend {self.options.backend.value}' + ) + elif self.options.llvm_proof_hint_instrumentation: + raise ValueError( + f'Option `--llvm-proof-hint-intrumentation` requires `--backend llvm`, not: --backend {self.options.backend.value}' + ) + + try: + Kompile.from_dict(kompile_dict)( + output_dir=kompiled_directory, + type_inference_mode=self.options.type_inference_mode, + warnings=self.options.warnings, + warnings_to_errors=self.options.warnings_to_errors, + no_exc_wrap=self.options.no_exc_wrap, + ) + except RuntimeError as err: + _, _, _, _, cpe = err.args + exit_with_process_error(cpe) + + +# def exec_kompile(options: KompileCommandOptions) -> None: +# main_file = Path(options.main_file) +# check_file_path(main_file) +# +# kompiled_directory: Path +# if options.definition_dir is None: +# kompiled_directory = Path(f'{main_file.stem}-kompiled') +# ensure_dir_path(kompiled_directory) +# else: +# kompiled_directory = options.definition_dir +# +# kompile_dict: dict[str, Any] = { +# 'main_file': main_file, +# '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), +# 'emit_json': options.emit_json, +# 'coverage': options.coverage, +# 'gen_bison_parser': options.gen_bison_parser, +# 'gen_glr_bison_parser': options.gen_glr_bison_parser, +# 'bison_lists': options.bison_lists, +# } +# if options.backend == KompileBackend.LLVM: +# kompile_dict['ccopts'] = options.ccopts +# kompile_dict['enable_search'] = options.enable_search +# kompile_dict['llvm_kompile_type'] = options.llvm_kompile_type +# kompile_dict['llvm_kompile_output'] = options.llvm_kompile_output +# kompile_dict['llvm_proof_hint_instrumentation'] = options.llvm_proof_hint_instrumentation +# elif len(options.ccopts) > 0: +# raise ValueError(f'Option `-ccopt` requires `--backend llvm`, not: --backend {options.backend.value}') +# elif options.enable_search: +# raise ValueError(f'Option `--enable-search` requires `--backend llvm`, not: --backend {options.backend.value}') +# elif options.llvm_kompile_type: +# raise ValueError( +# f'Option `--llvm-kompile-type` requires `--backend llvm`, not: --backend {options.backend.value}' +# ) +# elif options.llvm_kompile_output: +# raise ValueError( +# f'Option `--llvm-kompile-output` requires `--backend llvm`, not: --backend {options.backend.value}' +# ) +# elif options.llvm_proof_hint_instrumentation: +# raise ValueError( +# f'Option `--llvm-proof-hint-intrumentation` requires `--backend llvm`, not: --backend {options.backend.value}' +# ) +# +# try: +# Kompile.from_dict(kompile_dict)( +# output_dir=kompiled_directory, +# type_inference_mode=options.type_inference_mode, +# warnings=options.warnings, +# warnings_to_errors=options.warnings_to_errors, +# no_exc_wrap=options.no_exc_wrap, +# ) +# except RuntimeError as err: +# _, _, _, _, cpe = err.args +# exit_with_process_error(cpe) + + +# class RunOptions(LoggingOptions): +# pgm_file: str +# definition_dir: Path | None +# +# @staticmethod +# def default() -> dict[str, Any]: +# return { +# 'definition_dir': None, +# } + + +class RunOptionsGroup(LoggingOptionsGroup): + pgm_file: str + definition_dir: Path | None + + def __init__(self) -> None: + super().__init__() + self.add_option(StringOption(name='pgm_file', optional=False, help_str='File program to run in it.')) + self.add_option( + DirPathOption( + name='definition_dir', + cmd_line_name='--definition', + optional=False, + help_str='Path to definition to use.', + ) ) - except RuntimeError as err: - _, _, _, _, cpe = err.args - exit_with_process_error(cpe) -def exec_run(options: RunOptions) -> None: - pgm_file = Path(options.pgm_file) - check_file_path(pgm_file) - kompiled_directory: Path - if options.definition_dir is None: - kompiled_directory = Kompile.default_directory() - _LOGGER.info(f'Using kompiled directory: {kompiled_directory}.') - else: - kompiled_directory = options.definition_dir - krun = KRun(kompiled_directory) - rc, res = krun.krun(pgm_file) - print(krun.pretty_print(res)) - sys.exit(rc) +class RunCommand(Command[RunOptionsGroup]): + def __init__(self) -> None: + super().__init__('run', 'Run a given program using the K definition.', RunOptionsGroup()) + def exec(self) -> None: + pgm_file = Path(self.options.pgm_file) + check_file_path(pgm_file) + kompiled_directory: Path + if self.options.definition_dir is None: + kompiled_directory = Kompile.default_directory() + _LOGGER.info(f'Using kompiled directory: {kompiled_directory}.') + else: + kompiled_directory = self.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(options: GraphImportsOptions) -> None: - kompiled_dir: Path = options.definition_dir - kprinter = KPrint(kompiled_dir) - definition = kprinter.definition - import_graph = Digraph() - graph_file = kompiled_dir / 'import-graph' - for module in definition.modules: - module_name = module.name - import_graph.node(module_name) - for module_import in module.imports: - import_graph.edge(module_name, module_import.name) - import_graph.render(graph_file) - _LOGGER.info(f'Wrote file: {graph_file}') + +# def exec_run(options: RunOptions) -> None: +# pgm_file = Path(options.pgm_file) +# check_file_path(pgm_file) +# kompiled_directory: Path +# if options.definition_dir is None: +# kompiled_directory = Kompile.default_directory() +# _LOGGER.info(f'Using kompiled directory: {kompiled_directory}.') +# else: +# kompiled_directory = options.definition_dir +# krun = KRun(kompiled_directory) +# rc, res = krun.krun(pgm_file) +# print(krun.pretty_print(res)) +# sys.exit(rc) + + +class GraphImportsOptionsGroup(DefinitionOptionsGroup, LoggingOptionsGroup): ... + + +class GraphImportsCommand(Command[GraphImportsOptionsGroup]): + def __init__(self) -> None: + super().__init__('graph-imports', 'Graph the imports of a given definition', GraphImportsOptionsGroup()) + + def exec(self) -> None: + kompiled_dir: Path = self.options.definition_dir + kprinter = KPrint(kompiled_dir) + definition = kprinter.definition + import_graph = Digraph() + graph_file = kompiled_dir / 'import-graph' + for module in definition.modules: + module_name = module.name + import_graph.node(module_name) + for module_import in module.imports: + import_graph.edge(module_name, module_import.name) + import_graph.render(graph_file) + _LOGGER.info(f'Wrote file: {graph_file}') + + +# def exec_graph_imports(options: GraphImportsOptions) -> None: +# kompiled_dir: Path = options.definition_dir +# kprinter = KPrint(kompiled_dir) +# definition = kprinter.definition +# import_graph = Digraph() +# graph_file = kompiled_dir / 'import-graph' +# for module in definition.modules: +# module_name = module.name +# import_graph.node(module_name) +# for module_import in module.imports: +# import_graph.edge(module_name, module_import.name) +# import_graph.render(graph_file) +# _LOGGER.info(f'Wrote file: {graph_file}') class CoverageOptionsGroup(DefinitionOptionsGroup, OutputFileOptionsGroup, LoggingOptionsGroup): diff --git a/pyk/src/pyk/cli/args.py b/pyk/src/pyk/cli/args.py index bf5d0ba232b..83bbedda113 100644 --- a/pyk/src/pyk/cli/args.py +++ b/pyk/src/pyk/cli/args.py @@ -65,6 +65,9 @@ def from_option_string() -> dict[str, Any]: class WarningOptionsGroup(OptionsGroup): + warnings: Warnings | None + warnings_to_errors: bool + def __init__(self) -> None: super().__init__() self.add_option( @@ -174,6 +177,11 @@ def default() -> dict[str, Any]: class KDefinitionOptionsGroup(OptionsGroup): + includes: list[str] + main_module: str + syntax_module: str + md_selector: str + def __init__(self) -> None: super().__init__() self.add_option( @@ -338,6 +346,26 @@ def from_option_string() -> dict[str, str]: class KompileOptionsGroup(OptionsGroup): + emit_json: bool + llvm_kompile: bool + llvm_library: bool + enable_llvm_debug: bool + llvm_kompile_type: LLVMKompileType + llvm_kompile_output: Path + llvm_proof_hint_instrumentation: bool + read_only: bool + o0: bool + o1: bool + o2: bool + o3: bool + ccopts: list[str] + enable_search: bool + coverage: bool + gen_bison_parser: bool + gen_glr_bison_parser: bool + bison_lists: bool + no_exc_wrap: bool + def __init__(self) -> None: super().__init__() self.add_option( diff --git a/pyk/src/pyk/cli/pyk.py b/pyk/src/pyk/cli/pyk.py index d3ab081565e..607f8651eb8 100644 --- a/pyk/src/pyk/cli/pyk.py +++ b/pyk/src/pyk/cli/pyk.py @@ -5,7 +5,6 @@ from enum import Enum from typing import IO, TYPE_CHECKING, Any -from ..ktool.kompile import KompileBackend from .args import ( ConfigArgs, DefinitionOptions, @@ -17,7 +16,6 @@ OutputFileOptions, SaveDirOptions, SpecOptions, - WarningOptions, ) from .utils import dir_path @@ -90,7 +88,7 @@ # option_string_destinations = KompileCommandOptions.from_option_string() # case 'run': # option_string_destinations = RunOptions.from_option_string() -# +# # if option_string in option_string_destinations: # return option_string_destinations[option_string] # else: @@ -120,10 +118,10 @@ def from_option_string() -> dict[str, str]: ) -class GraphImportsOptions(DefinitionOptions, LoggingOptions): - @staticmethod - def from_option_string() -> dict[str, str]: - return DefinitionOptions.from_option_string() | LoggingOptions.from_option_string() +# class GraphImportsOptions(DefinitionOptions, LoggingOptions): +# @staticmethod +# def from_option_string() -> dict[str, str]: +# return DefinitionOptions.from_option_string() | LoggingOptions.from_option_string() class RPCKastOptions(OutputFileOptions, LoggingOptions): @@ -194,28 +192,29 @@ def from_option_string() -> dict[str, str]: ) -class KompileCommandOptions(LoggingOptions, WarningOptions, KDefinitionOptions, KompileOptions): - 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, - } - - @staticmethod - def from_option_string() -> dict[str, str]: - return ( - KDefinitionOptions.from_option_string() - | KompileOptions.from_option_string() - | LoggingOptions.from_option_string() - | {'definition': 'definition_dir'} - ) +# class KompileCommandOptions(LoggingOptions, WarningOptions, KDefinitionOptions, KompileOptions): +# 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, +# } +# +# @staticmethod +# def from_option_string() -> dict[str, str]: +# return ( +# KDefinitionOptions.from_option_string() +# | KompileOptions.from_option_string() +# | LoggingOptions.from_option_string() +# | {'definition': 'definition_dir'} +# ) +# class ProveOptions(LoggingOptions, SpecOptions, SaveDirOptions): @@ -249,15 +248,15 @@ def from_option_string() -> dict[str, str]: ) -class RunOptions(LoggingOptions): - pgm_file: str - definition_dir: Path | None - - @staticmethod - def default() -> dict[str, Any]: - return { - 'definition_dir': None, - } +# class RunOptions(LoggingOptions): +# pgm_file: str +# definition_dir: Path | None +# +# @staticmethod +# def default() -> dict[str, Any]: +# return { +# 'definition_dir': None, +# } def create_argument_parser() -> ArgumentParser: @@ -416,7 +415,7 @@ def create_argument_parser() -> ArgumentParser: # elif len(profile_list) == 1: # return {k: v for k, v in toml_profile[profile_list[0]].items() if type(v) is not dict} # return get_profile(toml_profile[profile_list[0]], profile_list[1:]) -# +# # toml_args = {} # if args.config_file.is_file(): # with open(args.config_file, 'rb') as config_file: @@ -426,7 +425,7 @@ def create_argument_parser() -> ArgumentParser: # _LOGGER.error( # 'Input config file is not in TOML format, ignoring the file and carrying on with the provided command line agruments' # ) -# +# # toml_args = ( # get_profile(toml_args[args.command], args.config_profile.split('.')) if args.command in toml_args else {} # ) @@ -440,5 +439,5 @@ def create_argument_parser() -> ArgumentParser: # level = level if toml_args[k] <= 3 else 3 # del toml_args[k] # toml_args['-o' + str(level)] = 'true' -# +# # return toml_args From 2da8b01cf430b6eb5f956cbda8eae5982045d587 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 1 May 2024 15:33:07 -0500 Subject: [PATCH 08/16] Add Prove, ProveLegacy, and Show commands to new system --- pyk/src/pyk/__main__.py | 289 +++++++++++++++++--- pyk/src/pyk/cli/args.py | 8 + pyk/src/pyk/cli/cli.py | 20 +- pyk/src/pyk/cli/pyk.py | 115 ++++---- pyk/src/pyk/ktool/kprove.py | 4 +- pyk/src/tests/integration/ktool/test_imp.py | 20 +- 6 files changed, 332 insertions(+), 124 deletions(-) diff --git a/pyk/src/pyk/__main__.py b/pyk/src/pyk/__main__.py index 4349e63edce..89c5fa54ff7 100644 --- a/pyk/src/pyk/__main__.py +++ b/pyk/src/pyk/__main__.py @@ -10,13 +10,17 @@ from .cli.args import ( DefinitionOptionsGroup, + IntOption, KDefinitionOptionsGroup, KompileOptionsGroup, LoggingOptionsGroup, OutputFileOptionsGroup, + SaveDirOptionsGroup, + SpecOptionsGroup, + StringListOption, WarningOptionsGroup, ) -from .cli.cli import CLI, Command, DirPathOption, EnumOption, ReadFileOption, StringOption +from .cli.cli import CLI, BoolOption, Command, DirPathOption, EnumOption, ReadFileOption, StringOption from .cli.pyk import PrintInput from .coverage import get_rule_by_id, strip_coverage_logger from .cterm import CTerm @@ -46,9 +50,9 @@ from .utils import check_file_path, ensure_dir_path, exit_with_process_error if TYPE_CHECKING: - from typing import IO, Any, Final + from typing import IO, Any, Final, Iterable - from .cli.pyk import PrintOptions, ProveLegacyOptions, ProveOptions, RPCKastOptions, RPCPrintOptions + from .cli.pyk import PrintOptions, RPCKastOptions, RPCPrintOptions _LOGGER: Final = logging.getLogger(__name__) @@ -228,44 +232,251 @@ def exec_rpc_kast(options: RPCKastOptions) -> None: options.output_file.write(json.dumps(request)) -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}') +# 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': [], +# } +# +# @staticmethod +# def from_option_string() -> dict[str, str]: +# return ( +# DefinitionOptions.from_option_string() +# | OutputFileOptions.from_option_string() +# | LoggingOptions.from_option_string() +# | {'kArgs': 'k_args'} +# ) -def exec_prove(options: ProveOptions) -> None: - kompiled_directory: Path - if options.definition_dir is None: - kompiled_directory = Kompile.default_directory() - _LOGGER.info(f'Using kompiled directory: {kompiled_directory}.') - else: - kompiled_directory = options.definition_dir - kprove = KProve(kompiled_directory, use_directory=options.temp_directory) - try: - proofs = kprove.prove_rpc(options=options) - except RuntimeError as err: - _, _, _, cpe = err.args - exit_with_process_error(cpe) - for proof in sorted(proofs, key=lambda p: p.id): - print('\n'.join(proof.summary.lines)) - if proof.failed and options.failure_info: - failure_info = proof.failure_info - if type(failure_info) is APRFailureInfo: - print('\n'.join(failure_info.print())) - if options.show_kcfg and type(proof) is APRProof: - node_printer = APRProofNodePrinter(proof, kprove, full_printer=True, minimize=False) - show = APRProofShow(kprove, node_printer=node_printer) - print('\n'.join(show.show(proof))) - sys.exit(len([p.id for p in proofs if not p.passed])) - - -def exec_show(options: ProveOptions) -> None: - options.max_iterations = 0 - options.show_kcfg = True - exec_prove(options) +class ProveLegacyOptionsGroup(DefinitionOptionsGroup, OutputFileOptionsGroup, LoggingOptionsGroup): + main_file: Path + spec_file: Path + spec_module: str + k_args: Iterable[str] + + def __init__(self) -> None: + super().__init__() + + self.add_option(DirPathOption(name='main_file', help_str='Main file used for kompilation', optional=False)) + self.add_option(DirPathOption(name='spec_file', help_str='File with the specification module.', optional=False)) + self.add_option(StringOption(name='spec_module', help_str='Module with claims to be proven', optional=False)) + self.add_option( + StringListOption( + name='k_args', + cmd_line_name='kArgs', + toml_name='kArgs', + help_str='Arguments to pass through to K invocation.', + optional=True, + ) + ) + + +class ProveLegacyCommand(Command[ProveLegacyOptionsGroup]): + def __init__(self) -> None: + super().__init__('prove-legacy', 'Prove an input specification (using kprovex).', ProveLegacyOptionsGroup()) + + def exec(self) -> None: + kompiled_dir: Path = self.options.definition_dir + kprover = KProve(kompiled_dir, self.options.main_file) + final_state = kprover.prove( + Path(self.options.spec_file), spec_module_name=self.options.spec_module, args=self.options.k_args + ) + self.options.output_file.write(json.dumps(mlOr([state.kast for state in final_state]).to_dict())) + _LOGGER.info(f'Wrote file: {self.options.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}') + + +# class ProveOptions(LoggingOptions, SpecOptions, SaveDirOptions): +# definition_dir: Path | None +# type_inference_mode: TypeInferenceMode | None +# failure_info: bool +# kore_rpc_command: str | Iterable[str] | None +# max_depth: int | None +# max_iterations: int | None +# show_kcfg: bool +# +# @staticmethod +# def default() -> dict[str, Any]: +# return { +# 'definition_dir': None, +# 'type_inference_mode': None, +# 'failure_info': False, +# 'kore_rpc_command': None, +# 'max_depth': None, +# 'max_iterations': None, +# 'show_kcfg': False, +# } +# +# @staticmethod +# def from_option_string() -> dict[str, str]: +# return ( +# KDefinitionOptions.from_option_string() +# | KompileOptions.from_option_string() +# | LoggingOptions.from_option_string() +# | {'definition': 'definition_dir'} +# ) + + +class ProveOptionsGroup(LoggingOptionsGroup, SpecOptionsGroup, SaveDirOptionsGroup): + definition_dir: Path | None + type_inference_mode: TypeInferenceMode | None + failure_info: bool + kore_rpc_command: str | Iterable[str] | None + max_depth: int | None + max_iterations: int | None + show_kcfg: bool + + def __init__(self) -> None: + super().__init__() + + self.add_option( + DirPathOption( + name='definition_dir', + cmd_line_name='--definition', + toml_name='definition', + help_str='Path to definition to use.', + optional=True, + default=None, + ) + ) + self.add_option( + EnumOption( + enum_type=TypeInferenceMode, + name='type_inference_mode', + cmd_line_name='--type-inference-mode', + help_str='Mode for doing K rule type inference in.', + optional=True, + default=None, + ) + ) + self.add_option( + BoolOption( + name='failure_info', + cmd_line_name='--failure-info', + help_str='Print out more information about proof failures.', + default=None, + ) + ) + self.add_option( + StringOption( + name='kore_rpc_command', + cmd_line_name='--kore-rpc-command', + help_str='Custom command to start RPC server', + default=None, + ) + ) + self.add_option( + IntOption( + name='max_depth', + cmd_line_name='--max-depth', + help_str='Maximum number of steps to take in symbolic execution per basic block.', + default=None, + optional=True, + ) + ) + self.add_option( + IntOption( + name='max_iterations', + cmd_line_name='--max-iterations', + help_str='Maximum number of KCFG explorations to take in attempting to discharge proof.', + default=None, + optional=True, + ) + ) + self.add_option( + BoolOption( + name='show_kcfg', + cmd_line_name='--show-kcfg', + help_str='Display the resulting proof KCFG.', + default=False, + optional=True, + ) + ) + + +class ProveCommand(Command[ProveOptionsGroup]): + def __init__(self) -> None: + super().__init__('prove', 'Prove an input specification (using RPC based prover).', ProveOptionsGroup()) + + def exec(self) -> None: + kompiled_directory: Path + if self.options.definition_dir is None: + kompiled_directory = Kompile.default_directory() + _LOGGER.info(f'Using kompiled directory: {kompiled_directory}.') + else: + kompiled_directory = self.options.definition_dir + kprove = KProve(kompiled_directory, use_directory=self.options.temp_directory) + try: + proofs = kprove.prove_rpc(options=self.options) + except RuntimeError as err: + _, _, _, cpe = err.args + exit_with_process_error(cpe) + for proof in sorted(proofs, key=lambda p: p.id): + print('\n'.join(proof.summary.lines)) + if proof.failed and self.options.failure_info: + failure_info = proof.failure_info + if type(failure_info) is APRFailureInfo: + print('\n'.join(failure_info.print())) + if self.options.show_kcfg and type(proof) is APRProof: + node_printer = APRProofNodePrinter(proof, kprove, full_printer=True, minimize=False) + show = APRProofShow(kprove, node_printer=node_printer) + print('\n'.join(show.show(proof))) + sys.exit(len([p.id for p in proofs if not p.passed])) + + +# def exec_prove(options: ProveOptions) -> None: +# kompiled_directory: Path +# if options.definition_dir is None: +# kompiled_directory = Kompile.default_directory() +# _LOGGER.info(f'Using kompiled directory: {kompiled_directory}.') +# else: +# kompiled_directory = options.definition_dir +# kprove = KProve(kompiled_directory, use_directory=options.temp_directory) +# try: +# proofs = kprove.prove_rpc(options=options) +# except RuntimeError as err: +# _, _, _, cpe = err.args +# exit_with_process_error(cpe) +# for proof in sorted(proofs, key=lambda p: p.id): +# print('\n'.join(proof.summary.lines)) +# if proof.failed and options.failure_info: +# failure_info = proof.failure_info +# if type(failure_info) is APRFailureInfo: +# print('\n'.join(failure_info.print())) +# if options.show_kcfg and type(proof) is APRProof: +# node_printer = APRProofNodePrinter(proof, kprove, full_printer=True, minimize=False) +# show = APRProofShow(kprove, node_printer=node_printer) +# print('\n'.join(show.show(proof))) +# sys.exit(len([p.id for p in proofs if not p.passed])) + + +class ShowCommand(ProveCommand): + def __init__(self) -> None: + Command.__init__(self, 'show', 'Display the status of a given proof', ProveOptionsGroup()) + + def exec(self) -> None: + self.options.max_iterations = 0 + self.options.show_kcfg = True + super().exec() + + +# def exec_show(options: ProveOptions) -> None: +# options.max_iterations = 0 +# options.show_kcfg = True +# exec_prove(options) # class KompileCommandOptions(LoggingOptions, WarningOptions, KDefinitionOptions, KompileOptions): diff --git a/pyk/src/pyk/cli/args.py b/pyk/src/pyk/cli/args.py index 83bbedda113..61324221d1c 100644 --- a/pyk/src/pyk/cli/args.py +++ b/pyk/src/pyk/cli/args.py @@ -248,6 +248,9 @@ def default() -> dict[str, Any]: class SaveDirOptionsGroup(OptionsGroup): + save_directory: Path | None + temp_directory: Path | None + def __init__(self) -> None: super().__init__() self.add_option( @@ -283,6 +286,11 @@ def default() -> dict[str, Any]: class SpecOptionsGroup(OptionsGroup): + spec_file: Path + spec_module: str | None + claim_labels: Iterable[str] | None + exclude_claim_labels: Iterable[str] | None + def __init__(self) -> None: super().__init__() self.add_option( diff --git a/pyk/src/pyk/cli/cli.py b/pyk/src/pyk/cli/cli.py index fba73a7b76d..e54399d4449 100644 --- a/pyk/src/pyk/cli/cli.py +++ b/pyk/src/pyk/cli/cli.py @@ -50,7 +50,7 @@ def get_and_exec_command(self) -> None: args = parser.parse_args() stripped_args = {key: val for (key, val) in vars(args).items() if val != 'NoDefault'} cmd = self.get_command(stripped_args) - cmd.extract(stripped_args) + cmd._options_group.extract(stripped_args) cmd.exec() @@ -323,15 +323,6 @@ class Command(Generic[OG]): _name: str _help_str: str - def extract(self, args: dict[str, Any]) -> None: - for option in self._options_group.options: - if option.name in args: - assert isinstance(args[option.name], option.type) - self.__setattr__(option.name, args[option.name]) - # TODO elif option exists in TOML file, set it to the value from there - else: - self.__setattr__(option.name, option.default) - def __init__(self, name: str, help_str: str, options_group: OG) -> None: self._name = name self._help_str = help_str @@ -356,6 +347,15 @@ def exec(self) -> None: ... class OptionsGroup: _options: dict[str, Option] + def extract(self, args: dict[str, Any]) -> None: + for option in self.options: + if option.name in args: + assert isinstance(args[option.name], option.type) + self.__setattr__(option.name, args[option.name]) + # TODO elif option exists in TOML file, set it to the value from there + else: + self.__setattr__(option.name, option.default) + def add_option(self, option: Option) -> None: self._options[option.name] = option diff --git a/pyk/src/pyk/cli/pyk.py b/pyk/src/pyk/cli/pyk.py index 607f8651eb8..96c3125239a 100644 --- a/pyk/src/pyk/cli/pyk.py +++ b/pyk/src/pyk/cli/pyk.py @@ -5,30 +5,15 @@ from enum import Enum from typing import IO, TYPE_CHECKING, Any -from .args import ( - ConfigArgs, - DefinitionOptions, - DisplayOptions, - KCLIArgs, - KDefinitionOptions, - KompileOptions, - LoggingOptions, - OutputFileOptions, - SaveDirOptions, - SpecOptions, -) +from .args import ConfigArgs, DefinitionOptions, DisplayOptions, KCLIArgs, LoggingOptions, OutputFileOptions from .utils import dir_path # import tomli if TYPE_CHECKING: - from collections.abc import Iterable - from pathlib import Path from typing import Final - from pyk.ktool import TypeInferenceMode - _LOGGER: Final = logging.getLogger(__name__) @@ -170,26 +155,26 @@ def from_option_string() -> dict[str, str]: ) -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': [], - } - - @staticmethod - def from_option_string() -> dict[str, str]: - return ( - DefinitionOptions.from_option_string() - | OutputFileOptions.from_option_string() - | LoggingOptions.from_option_string() - | {'kArgs': 'k_args'} - ) +# 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': [], +# } +# +# @staticmethod +# def from_option_string() -> dict[str, str]: +# return ( +# DefinitionOptions.from_option_string() +# | OutputFileOptions.from_option_string() +# | LoggingOptions.from_option_string() +# | {'kArgs': 'k_args'} +# ) # class KompileCommandOptions(LoggingOptions, WarningOptions, KDefinitionOptions, KompileOptions): @@ -217,35 +202,35 @@ def from_option_string() -> dict[str, str]: # -class ProveOptions(LoggingOptions, SpecOptions, SaveDirOptions): - definition_dir: Path | None - type_inference_mode: TypeInferenceMode | None - failure_info: bool - kore_rpc_command: str | Iterable[str] | None - max_depth: int | None - max_iterations: int | None - show_kcfg: bool - - @staticmethod - def default() -> dict[str, Any]: - return { - 'definition_dir': None, - 'type_inference_mode': None, - 'failure_info': False, - 'kore_rpc_command': None, - 'max_depth': None, - 'max_iterations': None, - 'show_kcfg': False, - } - - @staticmethod - def from_option_string() -> dict[str, str]: - return ( - KDefinitionOptions.from_option_string() - | KompileOptions.from_option_string() - | LoggingOptions.from_option_string() - | {'definition': 'definition_dir'} - ) +# class ProveOptions(LoggingOptions, SpecOptions, SaveDirOptions): +# definition_dir: Path | None +# type_inference_mode: TypeInferenceMode | None +# failure_info: bool +# kore_rpc_command: str | Iterable[str] | None +# max_depth: int | None +# max_iterations: int | None +# show_kcfg: bool +# +# @staticmethod +# def default() -> dict[str, Any]: +# return { +# 'definition_dir': None, +# 'type_inference_mode': None, +# 'failure_info': False, +# 'kore_rpc_command': None, +# 'max_depth': None, +# 'max_iterations': None, +# 'show_kcfg': False, +# } +# +# @staticmethod +# def from_option_string() -> dict[str, str]: +# return ( +# KDefinitionOptions.from_option_string() +# | KompileOptions.from_option_string() +# | LoggingOptions.from_option_string() +# | {'definition': 'definition_dir'} +# ) # class RunOptions(LoggingOptions): diff --git a/pyk/src/pyk/ktool/kprove.py b/pyk/src/pyk/ktool/kprove.py index c9c90fed78b..a6171c9f08f 100644 --- a/pyk/src/pyk/ktool/kprove.py +++ b/pyk/src/pyk/ktool/kprove.py @@ -30,7 +30,7 @@ from subprocess import CompletedProcess from typing import Final - from ..cli.pyk import ProveOptions + from ..__main__ import ProveOptionsGroup from ..kast.outer import KClaim, KRule, KRuleLike from ..kast.pretty import SymbolTable from ..kcfg.semantics import KCFGSemantics @@ -350,7 +350,7 @@ def prove_claim_rpc( def prove_rpc( self, - options: ProveOptions, + options: ProveOptionsGroup, kcfg_semantics: KCFGSemantics | None = None, id: str | None = None, port: int | None = None, diff --git a/pyk/src/tests/integration/ktool/test_imp.py b/pyk/src/tests/integration/ktool/test_imp.py index ba8fcf6a230..4aa524c6386 100644 --- a/pyk/src/tests/integration/ktool/test_imp.py +++ b/pyk/src/tests/integration/ktool/test_imp.py @@ -6,7 +6,7 @@ import pytest -from pyk.cli.pyk import ProveOptions +from pyk.__main__ import ProveOptionsGroup from pyk.kast.inner import KApply, KSequence, KVariable from pyk.kcfg.semantics import KCFGSemantics from pyk.proof import ProofStatus @@ -170,15 +170,19 @@ def test_prove_rpc( claim_id: str, proof_status: ProofStatus, ) -> None: + + options = ProveOptionsGroup() + options.extract( + { + 'spec_file': Path(spec_file), + 'spec_module': spec_module, + 'claim_labels': [claim_id], + } + ) + proof = single( kprove.prove_rpc( - ProveOptions( - { - 'spec_file': Path(spec_file), - 'spec_module': spec_module, - 'claim_labels': [claim_id], - } - ), + options=options, kcfg_semantics=ImpSemantics(kprove.definition), ) ) From ae7c69750a6636bf7bc5a44dabfbbe0b6fcc6678 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 1 May 2024 16:28:54 -0500 Subject: [PATCH 09/16] Finish converting commands to new system --- pyk/src/pyk/__main__.py | 623 +++++++++++++++------------------------- pyk/src/pyk/cli/args.py | 8 +- pyk/src/pyk/cli/pyk.py | 112 ++++---- 3 files changed, 288 insertions(+), 455 deletions(-) diff --git a/pyk/src/pyk/__main__.py b/pyk/src/pyk/__main__.py index 89c5fa54ff7..d368c3cb7a6 100644 --- a/pyk/src/pyk/__main__.py +++ b/pyk/src/pyk/__main__.py @@ -10,6 +10,7 @@ from .cli.args import ( DefinitionOptionsGroup, + DisplayOptionsGroup, IntOption, KDefinitionOptionsGroup, KompileOptionsGroup, @@ -52,8 +53,6 @@ if TYPE_CHECKING: from typing import IO, Any, Final, Iterable - from .cli.pyk import PrintOptions, RPCKastOptions, RPCPrintOptions - _LOGGER: Final = logging.getLogger(__name__) @@ -68,190 +67,240 @@ def main() -> None: cli.get_and_exec_command() -# -# cli_parser = create_argument_parser() -# args = cli_parser.parse_args() -# toml_args = parse_toml_args(args) -# -# stripped_args = toml_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('-', '_') -# if executor_name not in globals(): -# raise AssertionError(f'Unimplemented command: {args.command}') -# -# execute = globals()[executor_name] -# execute(options) - - -def exec_print(options: PrintOptions) -> None: - kompiled_dir: Path = options.definition_dir - printer = KPrint(kompiled_dir) - 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: {options.term.name}') - term = KInner.from_json(options.term.read()) - if is_top(term): - options.output_file.write(printer.pretty_print(term)) - _LOGGER.info(f'Wrote file: {options.output_file.name}') - else: - 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 = 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): - try: - minimized = minimize_term(disjunct, abstract_labels=abstract_labels, keep_cells=keep_cells) - config, constraint = split_config_and_constraints(minimized) - except ValueError as err: - raise ValueError('The minimized term does not contain a config cell.') from err +class PrintOptionsGroup(DefinitionOptionsGroup, OutputFileOptionsGroup, DisplayOptionsGroup, LoggingOptionsGroup): + term: IO[Any] + input: PrintInput + omit_labels: str | None + keep_cells: str | None + + def __init__(self) -> None: + super().__init__() + self.add_option( + ReadFileOption(name='term', optional=False, help_str='Input term (in format specified with --input)') + ) + self.add_option( + EnumOption( + name='input', + cmd_line_name='--input', + optional=True, + default=PrintInput.KAST_JSON, + help_str='Input format.', + enum_type=PrintInput, + ) + ) + self.add_option( + StringOption( + name='omit_labels', + cmd_line_name='--omit-labels', + optional=True, + default=None, + help_str='List of labels to omit from output', + ) + ) + self.add_option( + StringOption( + name='keep_cells', + cmd_line_name='--keep-cells', + optional=True, + default=None, + help_str='List of cells with primitive values to keep in output', + ) + ) - if not is_top(constraint): - minimized_disjuncts.append(mlAnd([config, constraint], sort=GENERATED_TOP_CELL)) - else: - minimized_disjuncts.append(config) - term = propagate_up_constraints(mlOr(minimized_disjuncts, sort=GENERATED_TOP_CELL)) - options.output_file.write(printer.pretty_print(term)) - _LOGGER.info(f'Wrote file: {options.output_file.name}') +class PrintCommand(Command[PrintOptionsGroup]): + def __init__(self) -> None: + super().__init__('print', 'Pretty print a term.', PrintOptionsGroup()) + def exec(self) -> None: + kompiled_dir: Path = self.options.definition_dir + printer = KPrint(kompiled_dir) + if self.options.input == PrintInput.KORE_JSON: + _LOGGER.info(f'Reading Kore JSON from file: {self.options.term.name}') + kore = Pattern.from_json(self.options.term.read()) + term = printer.kore_to_kast(kore) + else: + _LOGGER.info(f'Reading Kast JSON from file: {self.options.term.name}') + term = KInner.from_json(self.options.term.read()) + if is_top(term): + self.options.output_file.write(printer.pretty_print(term)) + _LOGGER.info(f'Wrote file: {self.options.output_file.name}') + else: + if self.options.minimize: + if self.options.omit_labels is not None and self.options.keep_cells is not None: + raise ValueError('You cannot use both --omit-labels and --keep-cells.') -def exec_rpc_print(options: RPCPrintOptions) -> None: - kompiled_dir: Path = options.definition_dir - printer = KPrint(kompiled_dir) - input_dict = json.loads(options.input_file.read()) - output_buffer = [] + abstract_labels = self.options.omit_labels.split(',') if self.options.omit_labels is not None else [] + keep_cells = self.options.keep_cells.split(',') if self.options.keep_cells is not None else [] + minimized_disjuncts = [] - def pretty_print_request(request_params: dict[str, Any]) -> list[str]: - output_buffer = [] - non_state_keys = set(request_params.keys()).difference(['state']) - for key in non_state_keys: - output_buffer.append(f'{key}: {request_params[key]}') - state = CTerm.from_kast(printer.kore_to_kast(kore_term(request_params['state']))) - output_buffer.append('State:') - output_buffer.append(printer.pretty_print(state.kast, sort_collections=True)) - return output_buffer + for disjunct in flatten_label('#Or', term): + try: + minimized = minimize_term(disjunct, abstract_labels=abstract_labels, keep_cells=keep_cells) + config, constraint = split_config_and_constraints(minimized) + except ValueError as err: + raise ValueError('The minimized term does not contain a config cell.') from err - def pretty_print_execute_response(execute_result: ExecuteResult) -> list[str]: - output_buffer = [] - output_buffer.append(f'Depth: {execute_result.depth}') - output_buffer.append(f'Stop reason: {execute_result.reason.value}') - if execute_result.reason == StopReason.TERMINAL_RULE or execute_result.reason == StopReason.CUT_POINT_RULE: - output_buffer.append(f'Stop rule: {execute_result.rule}') - output_buffer.append( - f'Number of next states: {len(execute_result.next_states) if execute_result.next_states is not None else 0}' + if not is_top(constraint): + minimized_disjuncts.append(mlAnd([config, constraint], sort=GENERATED_TOP_CELL)) + else: + minimized_disjuncts.append(config) + term = propagate_up_constraints(mlOr(minimized_disjuncts, sort=GENERATED_TOP_CELL)) + + self.options.output_file.write(printer.pretty_print(term)) + _LOGGER.info(f'Wrote file: {self.options.output_file.name}') + + +class RPCPrintOptionsGroup(DefinitionOptionsGroup, OutputFileOptionsGroup, LoggingOptionsGroup): + input_file: IO[Any] + + def __init__(self) -> None: + super().__init__() + self.add_option( + ReadFileOption( + 'input_file', + optional=False, + help_str='An input file containing the JSON RPC request or response with KoreJSON payload.', + ) ) - state = CTerm.from_kast(printer.kore_to_kast(execute_result.state.kore)) - output_buffer.append('State:') - output_buffer.append(printer.pretty_print(state.kast, sort_collections=True)) - if execute_result.next_states is not None: - next_states = [CTerm.from_kast(printer.kore_to_kast(s.kore)) for s in execute_result.next_states] - for i, s in enumerate(next_states): - output_buffer.append(f'Next state #{i}:') - output_buffer.append(printer.pretty_print(s.kast, sort_collections=True)) - return output_buffer - - try: - if 'method' in input_dict: - output_buffer.append('JSON RPC request') - output_buffer.append(f'id: {input_dict["id"]}') - output_buffer.append(f'Method: {input_dict["method"]}') - try: - if 'state' in input_dict['params']: - output_buffer += pretty_print_request(input_dict['params']) - else: # this is an "add-module" request, skip trying to print state - for key in input_dict['params'].keys(): - output_buffer.append(f'{key}: {input_dict["params"][key]}') - except KeyError as e: - _LOGGER.critical(f'Could not find key {str(e)} in input JSON file') - exit(1) - else: - if not 'result' in input_dict: - _LOGGER.critical('The input is neither a request not a resonse') - exit(1) - output_buffer.append('JSON RPC Response') - output_buffer.append(f'id: {input_dict["id"]}') - if list(input_dict['result'].keys()) == ['state']: # this is a "simplify" response - output_buffer.append('Method: simplify') - state = CTerm.from_kast(printer.kore_to_kast(kore_term(input_dict['result']['state']))) - output_buffer.append('State:') - output_buffer.append(printer.pretty_print(state.kast, sort_collections=True)) - elif list(input_dict['result'].keys()) == ['module']: # this is an "add-module" response - output_buffer.append('Method: add-module') - output_buffer.append('Module:') - output_buffer.append(input_dict['result']['module']) - else: - try: # assume it is an "execute" response - output_buffer.append('Method: execute') - execute_result = ExecuteResult.from_dict(input_dict['result']) - output_buffer += pretty_print_execute_response(execute_result) + + +class RPCPrintCommand(Command[RPCPrintOptionsGroup]): + def __init__(self) -> None: + super().__init__('rpc-print', 'Pretty-print an RPC request/response', RPCPrintOptionsGroup()) + + def exec(self) -> None: + kompiled_dir: Path = self.options.definition_dir + printer = KPrint(kompiled_dir) + input_dict = json.loads(self.options.input_file.read()) + output_buffer = [] + + def pretty_print_request(request_params: dict[str, Any]) -> list[str]: + output_buffer = [] + non_state_keys = set(request_params.keys()).difference(['state']) + for key in non_state_keys: + output_buffer.append(f'{key}: {request_params[key]}') + state = CTerm.from_kast(printer.kore_to_kast(kore_term(request_params['state']))) + output_buffer.append('State:') + output_buffer.append(printer.pretty_print(state.kast, sort_collections=True)) + return output_buffer + + def pretty_print_execute_response(execute_result: ExecuteResult) -> list[str]: + output_buffer = [] + output_buffer.append(f'Depth: {execute_result.depth}') + output_buffer.append(f'Stop reason: {execute_result.reason.value}') + if execute_result.reason == StopReason.TERMINAL_RULE or execute_result.reason == StopReason.CUT_POINT_RULE: + output_buffer.append(f'Stop rule: {execute_result.rule}') + output_buffer.append( + f'Number of next states: {len(execute_result.next_states) if execute_result.next_states is not None else 0}' + ) + state = CTerm.from_kast(printer.kore_to_kast(execute_result.state.kore)) + output_buffer.append('State:') + output_buffer.append(printer.pretty_print(state.kast, sort_collections=True)) + if execute_result.next_states is not None: + next_states = [CTerm.from_kast(printer.kore_to_kast(s.kore)) for s in execute_result.next_states] + for i, s in enumerate(next_states): + output_buffer.append(f'Next state #{i}:') + output_buffer.append(printer.pretty_print(s.kast, sort_collections=True)) + return output_buffer + + try: + if 'method' in input_dict: + output_buffer.append('JSON RPC request') + output_buffer.append(f'id: {input_dict["id"]}') + output_buffer.append(f'Method: {input_dict["method"]}') + try: + if 'state' in input_dict['params']: + output_buffer += pretty_print_request(input_dict['params']) + else: # this is an "add-module" request, skip trying to print state + for key in input_dict['params'].keys(): + output_buffer.append(f'{key}: {input_dict["params"][key]}') except KeyError as e: _LOGGER.critical(f'Could not find key {str(e)} in input JSON file') exit(1) - 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: - # shorten and print the error message in case kore_to_kast throws ValueError - _LOGGER.critical(str(e)[:200]) - exit(1) - - -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(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 = {} - for key in non_state_keys: - request_params[key] = reference_request['params'][key] - request_params['state'] = {'format': 'KORE', 'version': 1, 'term': execute_result.state.kore.dict} - request = { - 'jsonrpc': reference_request['jsonrpc'], - 'id': reference_request['id'], - 'method': reference_request['method'], - 'params': request_params, - } - options.output_file.write(json.dumps(request)) - - -# 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': [], -# } -# -# @staticmethod -# def from_option_string() -> dict[str, str]: -# return ( -# DefinitionOptions.from_option_string() -# | OutputFileOptions.from_option_string() -# | LoggingOptions.from_option_string() -# | {'kArgs': 'k_args'} -# ) + else: + if not 'result' in input_dict: + _LOGGER.critical('The input is neither a request not a resonse') + exit(1) + output_buffer.append('JSON RPC Response') + output_buffer.append(f'id: {input_dict["id"]}') + if list(input_dict['result'].keys()) == ['state']: # this is a "simplify" response + output_buffer.append('Method: simplify') + state = CTerm.from_kast(printer.kore_to_kast(kore_term(input_dict['result']['state']))) + output_buffer.append('State:') + output_buffer.append(printer.pretty_print(state.kast, sort_collections=True)) + elif list(input_dict['result'].keys()) == ['module']: # this is an "add-module" response + output_buffer.append('Method: add-module') + output_buffer.append('Module:') + output_buffer.append(input_dict['result']['module']) + else: + try: # assume it is an "execute" response + output_buffer.append('Method: execute') + execute_result = ExecuteResult.from_dict(input_dict['result']) + output_buffer += pretty_print_execute_response(execute_result) + except KeyError as e: + _LOGGER.critical(f'Could not find key {str(e)} in input JSON file') + exit(1) + if self.options.output_file is not None: + self.options.output_file.write('\n'.join(output_buffer)) + else: + print('\n'.join(output_buffer)) + except ValueError as e: + # shorten and print the error message in case kore_to_kast throws ValueError + _LOGGER.critical(str(e)[:200]) + exit(1) + + +class RPCKastOptionsGroup(OutputFileOptionsGroup, LoggingOptionsGroup): + reference_request_file: IO[Any] + response_file: IO[Any] + + def __init__(self) -> None: + super().__init__() + self.add_option( + ReadFileOption( + name='reference_request_file', + optional=False, + help_str='An input file containing a JSON RPC request to server as a reference for the new request.', + ) + ) + self.add_option( + ReadFileOption( + name='response_file', + optional=False, + help_str='An input file containing a JSON RPC reesponse with KoreJSON payload.', + ) + ) + + +class RPCKastCommand(Command[RPCKastOptionsGroup]): + def __init__(self) -> None: + super().__init__( + 'rpc-kast', + 'Convert an "execute" JSON RPC response to a new "execute" or "simplify" request, copying paraemeters from a reference request.', + RPCKastOptionsGroup(), + ) + + def exec(self) -> None: + """ + Convert an 'execute' JSON RPC response to a new 'execute' or 'simplify' request, + copying parameters from a reference request. + """ + reference_request = json.loads(self.options.reference_request_file.read()) + input_dict = json.loads(self.options.response_file.read()) + execute_result = ExecuteResult.from_dict(input_dict['result']) + non_state_keys = set(reference_request['params'].keys()).difference(['state']) + request_params = {} + for key in non_state_keys: + request_params[key] = reference_request['params'][key] + request_params['state'] = {'format': 'KORE', 'version': 1, 'term': execute_result.state.kore.dict} + request = { + 'jsonrpc': reference_request['jsonrpc'], + 'id': reference_request['id'], + 'method': reference_request['method'], + 'params': request_params, + } + self.options.output_file.write(json.dumps(request)) class ProveLegacyOptionsGroup(DefinitionOptionsGroup, OutputFileOptionsGroup, LoggingOptionsGroup): @@ -291,45 +340,6 @@ def exec(self) -> None: _LOGGER.info(f'Wrote file: {self.options.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}') - - -# class ProveOptions(LoggingOptions, SpecOptions, SaveDirOptions): -# definition_dir: Path | None -# type_inference_mode: TypeInferenceMode | None -# failure_info: bool -# kore_rpc_command: str | Iterable[str] | None -# max_depth: int | None -# max_iterations: int | None -# show_kcfg: bool -# -# @staticmethod -# def default() -> dict[str, Any]: -# return { -# 'definition_dir': None, -# 'type_inference_mode': None, -# 'failure_info': False, -# 'kore_rpc_command': None, -# 'max_depth': None, -# 'max_iterations': None, -# 'show_kcfg': False, -# } -# -# @staticmethod -# def from_option_string() -> dict[str, str]: -# return ( -# KDefinitionOptions.from_option_string() -# | KompileOptions.from_option_string() -# | LoggingOptions.from_option_string() -# | {'definition': 'definition_dir'} -# ) - - class ProveOptionsGroup(LoggingOptionsGroup, SpecOptionsGroup, SaveDirOptionsGroup): definition_dir: Path | None type_inference_mode: TypeInferenceMode | None @@ -437,32 +447,6 @@ def exec(self) -> None: sys.exit(len([p.id for p in proofs if not p.passed])) -# def exec_prove(options: ProveOptions) -> None: -# kompiled_directory: Path -# if options.definition_dir is None: -# kompiled_directory = Kompile.default_directory() -# _LOGGER.info(f'Using kompiled directory: {kompiled_directory}.') -# else: -# kompiled_directory = options.definition_dir -# kprove = KProve(kompiled_directory, use_directory=options.temp_directory) -# try: -# proofs = kprove.prove_rpc(options=options) -# except RuntimeError as err: -# _, _, _, cpe = err.args -# exit_with_process_error(cpe) -# for proof in sorted(proofs, key=lambda p: p.id): -# print('\n'.join(proof.summary.lines)) -# if proof.failed and options.failure_info: -# failure_info = proof.failure_info -# if type(failure_info) is APRFailureInfo: -# print('\n'.join(failure_info.print())) -# if options.show_kcfg and type(proof) is APRProof: -# node_printer = APRProofNodePrinter(proof, kprove, full_printer=True, minimize=False) -# show = APRProofShow(kprove, node_printer=node_printer) -# print('\n'.join(show.show(proof))) -# sys.exit(len([p.id for p in proofs if not p.passed])) - - class ShowCommand(ProveCommand): def __init__(self) -> None: Command.__init__(self, 'show', 'Display the status of a given proof', ProveOptionsGroup()) @@ -473,36 +457,6 @@ def exec(self) -> None: super().exec() -# def exec_show(options: ProveOptions) -> None: -# options.max_iterations = 0 -# options.show_kcfg = True -# exec_prove(options) - - -# class KompileCommandOptions(LoggingOptions, WarningOptions, KDefinitionOptions, KompileOptions): -# 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, -# } -# -# @staticmethod -# def from_option_string() -> dict[str, str]: -# return ( -# KDefinitionOptions.from_option_string() -# | KompileOptions.from_option_string() -# | LoggingOptions.from_option_string() -# | {'definition': 'definition_dir'} -# ) - - class KompileCommandOptionsGroup( LoggingOptionsGroup, WarningOptionsGroup, KDefinitionOptionsGroup, KompileOptionsGroup ): @@ -619,77 +573,6 @@ def exec(self) -> None: exit_with_process_error(cpe) -# def exec_kompile(options: KompileCommandOptions) -> None: -# main_file = Path(options.main_file) -# check_file_path(main_file) -# -# kompiled_directory: Path -# if options.definition_dir is None: -# kompiled_directory = Path(f'{main_file.stem}-kompiled') -# ensure_dir_path(kompiled_directory) -# else: -# kompiled_directory = options.definition_dir -# -# kompile_dict: dict[str, Any] = { -# 'main_file': main_file, -# '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), -# 'emit_json': options.emit_json, -# 'coverage': options.coverage, -# 'gen_bison_parser': options.gen_bison_parser, -# 'gen_glr_bison_parser': options.gen_glr_bison_parser, -# 'bison_lists': options.bison_lists, -# } -# if options.backend == KompileBackend.LLVM: -# kompile_dict['ccopts'] = options.ccopts -# kompile_dict['enable_search'] = options.enable_search -# kompile_dict['llvm_kompile_type'] = options.llvm_kompile_type -# kompile_dict['llvm_kompile_output'] = options.llvm_kompile_output -# kompile_dict['llvm_proof_hint_instrumentation'] = options.llvm_proof_hint_instrumentation -# elif len(options.ccopts) > 0: -# raise ValueError(f'Option `-ccopt` requires `--backend llvm`, not: --backend {options.backend.value}') -# elif options.enable_search: -# raise ValueError(f'Option `--enable-search` requires `--backend llvm`, not: --backend {options.backend.value}') -# elif options.llvm_kompile_type: -# raise ValueError( -# f'Option `--llvm-kompile-type` requires `--backend llvm`, not: --backend {options.backend.value}' -# ) -# elif options.llvm_kompile_output: -# raise ValueError( -# f'Option `--llvm-kompile-output` requires `--backend llvm`, not: --backend {options.backend.value}' -# ) -# elif options.llvm_proof_hint_instrumentation: -# raise ValueError( -# f'Option `--llvm-proof-hint-intrumentation` requires `--backend llvm`, not: --backend {options.backend.value}' -# ) -# -# try: -# Kompile.from_dict(kompile_dict)( -# output_dir=kompiled_directory, -# type_inference_mode=options.type_inference_mode, -# warnings=options.warnings, -# warnings_to_errors=options.warnings_to_errors, -# no_exc_wrap=options.no_exc_wrap, -# ) -# except RuntimeError as err: -# _, _, _, _, cpe = err.args -# exit_with_process_error(cpe) - - -# class RunOptions(LoggingOptions): -# pgm_file: str -# definition_dir: Path | None -# -# @staticmethod -# def default() -> dict[str, Any]: -# return { -# 'definition_dir': None, -# } - - class RunOptionsGroup(LoggingOptionsGroup): pgm_file: str definition_dir: Path | None @@ -726,21 +609,6 @@ def exec(self) -> None: sys.exit(rc) -# def exec_run(options: RunOptions) -> None: -# pgm_file = Path(options.pgm_file) -# check_file_path(pgm_file) -# kompiled_directory: Path -# if options.definition_dir is None: -# kompiled_directory = Kompile.default_directory() -# _LOGGER.info(f'Using kompiled directory: {kompiled_directory}.') -# else: -# kompiled_directory = options.definition_dir -# krun = KRun(kompiled_directory) -# rc, res = krun.krun(pgm_file) -# print(krun.pretty_print(res)) -# sys.exit(rc) - - class GraphImportsOptionsGroup(DefinitionOptionsGroup, LoggingOptionsGroup): ... @@ -763,21 +631,6 @@ def exec(self) -> None: _LOGGER.info(f'Wrote file: {graph_file}') -# def exec_graph_imports(options: GraphImportsOptions) -> None: -# kompiled_dir: Path = options.definition_dir -# kprinter = KPrint(kompiled_dir) -# definition = kprinter.definition -# import_graph = Digraph() -# graph_file = kompiled_dir / 'import-graph' -# for module in definition.modules: -# module_name = module.name -# import_graph.node(module_name) -# for module_import in module.imports: -# import_graph.edge(module_name, module_import.name) -# import_graph.render(graph_file) -# _LOGGER.info(f'Wrote file: {graph_file}') - - class CoverageOptionsGroup(DefinitionOptionsGroup, OutputFileOptionsGroup, LoggingOptionsGroup): coverage_file: IO[Any] @@ -805,19 +658,6 @@ def exec(self) -> None: _LOGGER.info(f'Wrote file: {self.options.output_file.name}') -# 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 options.coverage_file: -# rule = minimize_rule(strip_coverage_logger(get_rule_by_id(definition, rid.strip()))) -# 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}') - - class KoreToJsonCommand(Command[LoggingOptionsGroup]): def __init__(self) -> None: super().__init__('kore-to-json', 'convert textual KORE to JSON', LoggingOptionsGroup()) @@ -828,12 +668,6 @@ def exec(self) -> None: print(kore.json) -# def exec_kore_to_json(options: KoreToJsonOptions) -> None: -# text = sys.stdin.read() -# kore = KoreParser(text).pattern() -# print(kore.json) - - class JsonToKoreCommand(Command[LoggingOptionsGroup]): def __init__(self) -> None: super().__init__('json-to-kore', 'convert JSON to textual KORE', LoggingOptionsGroup()) @@ -845,12 +679,5 @@ def exec(self) -> None: sys.stdout.write('\n') -# def exec_json_to_kore(options: JsonToKoreOptions) -> None: -# text = sys.stdin.read() -# kore = Pattern.from_json(text) -# kore.write(sys.stdout) -# sys.stdout.write('\n') - - if __name__ == '__main__': main() diff --git a/pyk/src/pyk/cli/args.py b/pyk/src/pyk/cli/args.py index 61324221d1c..0aaa478e806 100644 --- a/pyk/src/pyk/cli/args.py +++ b/pyk/src/pyk/cli/args.py @@ -161,9 +161,15 @@ def from_option_string() -> dict[str, Any]: class DisplayOptionsGroup(OptionsGroup): + minimize: bool + def __init__(self) -> None: super().__init__() - self.add_option(BoolOption(name='minimize', optional=True, default=True, help_str='Minimize output.')) + self.add_option( + BoolOption( + name='minimize', cmd_line_name='--minimize', optional=True, default=True, help_str='Minimize output.' + ) + ) class DisplayOptions(Options): diff --git a/pyk/src/pyk/cli/pyk.py b/pyk/src/pyk/cli/pyk.py index 96c3125239a..6817a4db88e 100644 --- a/pyk/src/pyk/cli/pyk.py +++ b/pyk/src/pyk/cli/pyk.py @@ -3,9 +3,9 @@ import logging from argparse import ArgumentParser, FileType from enum import Enum -from typing import IO, TYPE_CHECKING, Any +from typing import TYPE_CHECKING -from .args import ConfigArgs, DefinitionOptions, DisplayOptions, KCLIArgs, LoggingOptions, OutputFileOptions +from .args import ConfigArgs, KCLIArgs from .utils import dir_path # import tomli @@ -91,16 +91,16 @@ class PrintInput(Enum): # class KoreToJsonOptions(LoggingOptions): ... -class CoverageOptions(DefinitionOptions, OutputFileOptions, LoggingOptions): - coverage_file: IO[Any] - - @staticmethod - def from_option_string() -> dict[str, str]: - return ( - DefinitionOptions.from_option_string() - | OutputFileOptions.from_option_string() - | LoggingOptions.from_option_string() - ) +# class CoverageOptions(DefinitionOptions, OutputFileOptions, LoggingOptions): +# coverage_file: IO[Any] +# +# @staticmethod +# def from_option_string() -> dict[str, str]: +# return ( +# DefinitionOptions.from_option_string() +# | OutputFileOptions.from_option_string() +# | LoggingOptions.from_option_string() +# ) # class GraphImportsOptions(DefinitionOptions, LoggingOptions): @@ -109,50 +109,50 @@ def from_option_string() -> dict[str, str]: # return DefinitionOptions.from_option_string() | LoggingOptions.from_option_string() -class RPCKastOptions(OutputFileOptions, LoggingOptions): - reference_request_file: IO[Any] - response_file: IO[Any] - - @staticmethod - def from_option_string() -> dict[str, str]: - return OutputFileOptions.from_option_string() | LoggingOptions.from_option_string() - - -class RPCPrintOptions(DefinitionOptions, OutputFileOptions, LoggingOptions): - input_file: IO[Any] - - @staticmethod - def from_option_string() -> dict[str, str]: - return ( - DefinitionOptions.from_option_string() - | OutputFileOptions.from_option_string() - | LoggingOptions.from_option_string() - ) - - -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, - } - - @staticmethod - def from_option_string() -> dict[str, str]: - return ( - DefinitionOptions.from_option_string() - | OutputFileOptions.from_option_string() - | DisplayOptions.from_option_string() - | LoggingOptions.from_option_string() - ) +# class RPCKastOptions(OutputFileOptions, LoggingOptions): +# reference_request_file: IO[Any] +# response_file: IO[Any] +# +# @staticmethod +# def from_option_string() -> dict[str, str]: +# return OutputFileOptions.from_option_string() | LoggingOptions.from_option_string() +# +# +# class RPCPrintOptions(DefinitionOptions, OutputFileOptions, LoggingOptions): +# input_file: IO[Any] +# +# @staticmethod +# def from_option_string() -> dict[str, str]: +# return ( +# DefinitionOptions.from_option_string() +# | OutputFileOptions.from_option_string() +# | LoggingOptions.from_option_string() +# ) +# +# +# 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, +# } +# +# @staticmethod +# def from_option_string() -> dict[str, str]: +# return ( +# DefinitionOptions.from_option_string() +# | OutputFileOptions.from_option_string() +# | DisplayOptions.from_option_string() +# | LoggingOptions.from_option_string() +# ) # class ProveLegacyOptions(DefinitionOptions, OutputFileOptions, LoggingOptions): From 5ca694c2c05362f6ce4551941f258636264c8512 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 2 May 2024 18:16:41 -0500 Subject: [PATCH 10/16] Mirror add_argument interface more closely --- pyk/src/pyk/__main__.py | 108 +++++------ pyk/src/pyk/cli/args.py | 395 +++++++++++----------------------------- pyk/src/pyk/cli/cli.py | 278 ++++------------------------ 3 files changed, 196 insertions(+), 585 deletions(-) diff --git a/pyk/src/pyk/__main__.py b/pyk/src/pyk/__main__.py index d368c3cb7a6..d9e27427cd0 100644 --- a/pyk/src/pyk/__main__.py +++ b/pyk/src/pyk/__main__.py @@ -5,23 +5,22 @@ import sys from pathlib import Path from typing import TYPE_CHECKING +from argparse import FileType from graphviz import Digraph from .cli.args import ( DefinitionOptionsGroup, DisplayOptionsGroup, - IntOption, KDefinitionOptionsGroup, KompileOptionsGroup, LoggingOptionsGroup, OutputFileOptionsGroup, SaveDirOptionsGroup, SpecOptionsGroup, - StringListOption, WarningOptionsGroup, ) -from .cli.cli import CLI, BoolOption, Command, DirPathOption, EnumOption, ReadFileOption, StringOption +from .cli.cli import CLI, Command, Option from .cli.pyk import PrintInput from .coverage import get_rule_by_id, strip_coverage_logger from .cterm import CTerm @@ -70,44 +69,26 @@ def main() -> None: class PrintOptionsGroup(DefinitionOptionsGroup, OutputFileOptionsGroup, DisplayOptionsGroup, LoggingOptionsGroup): term: IO[Any] input: PrintInput - omit_labels: str | None - keep_cells: str | None + omit_labels: list[str] | None + keep_cells: list[str] | None def __init__(self) -> None: super().__init__() self.add_option( - ReadFileOption(name='term', optional=False, help_str='Input term (in format specified with --input)') + Option('term', FileType('r'), help_str='Input term (in format specified with --input)', required=True) ) self.add_option( - EnumOption( - name='input', - cmd_line_name='--input', - optional=True, - default=PrintInput.KAST_JSON, - help_str='Input format.', - enum_type=PrintInput, - ) + Option('--input', PrintInput, 'input', help_str='Input format', choices=list(PrintInput), default=PrintInput.KAST_JSON) ) self.add_option( - StringOption( - name='omit_labels', - cmd_line_name='--omit-labels', - optional=True, - default=None, - help_str='List of labels to omit from output', - ) + Option('--omit-labels', str, 'omit_labels', help_str='List of labels to omit from output.', nargs='?', default=[]) ) self.add_option( - StringOption( - name='keep_cells', - cmd_line_name='--keep-cells', - optional=True, - default=None, - help_str='List of cells with primitive values to keep in output', - ) + Option('--keep-cells', str, 'keep_cells', help_str='List of cells with primitive values to keep in output.', nargs='?', default=[]) ) + class PrintCommand(Command[PrintOptionsGroup]): def __init__(self) -> None: super().__init__('print', 'Pretty print a term.', PrintOptionsGroup()) @@ -157,11 +138,7 @@ class RPCPrintOptionsGroup(DefinitionOptionsGroup, OutputFileOptionsGroup, Loggi def __init__(self) -> None: super().__init__() self.add_option( - ReadFileOption( - 'input_file', - optional=False, - help_str='An input file containing the JSON RPC request or response with KoreJSON payload.', - ) + Option('input_file', FileType('r'), help_str='An input file containing the JSON RPC request or response with KoreJSON payload. ', required=True) ) @@ -258,18 +235,10 @@ class RPCKastOptionsGroup(OutputFileOptionsGroup, LoggingOptionsGroup): def __init__(self) -> None: super().__init__() self.add_option( - ReadFileOption( - name='reference_request_file', - optional=False, - help_str='An input file containing a JSON RPC request to server as a reference for the new request.', - ) + Option('reference_request_file', FileType('r'), help_str='An input file containing a JSON RPC request to serve as a reference for the new request.', required=True) ) self.add_option( - ReadFileOption( - name='response_file', - optional=False, - help_str='An input file containing a JSON RPC reesponse with KoreJSON payload.', - ) + Option('response_file', FileType('r'), help_str='An input file containing a JSON RPC response with KoreJSON payload.', required=True) ) @@ -312,17 +281,17 @@ class ProveLegacyOptionsGroup(DefinitionOptionsGroup, OutputFileOptionsGroup, Lo def __init__(self) -> None: super().__init__() - self.add_option(DirPathOption(name='main_file', help_str='Main file used for kompilation', optional=False)) - self.add_option(DirPathOption(name='spec_file', help_str='File with the specification module.', optional=False)) - self.add_option(StringOption(name='spec_module', help_str='Module with claims to be proven', optional=False)) self.add_option( - StringListOption( - name='k_args', - cmd_line_name='kArgs', - toml_name='kArgs', - help_str='Arguments to pass through to K invocation.', - optional=True, - ) + Option('main_file', str, help_str='Main file used for kompilation', required=True) + ) + self.add_option( + Option('spec_file', str, help_str='File with the specification module.', required=True) + ) + self.add_option( + Option('spec_module', str, help_str='Module with claims to be proven.', required=True) + ) + self.add_option( + Option('kArgs', str, 'k_args', 'Module with claims to be proven.', required=True, nargs='*') ) @@ -351,6 +320,39 @@ class ProveOptionsGroup(LoggingOptionsGroup, SpecOptionsGroup, SaveDirOptionsGro def __init__(self) -> None: super().__init__() + self.add_option( + Option() + ) + + + prove_args = pyk_args_command.add_parser( + 'prove', + help='Prove an input specification (using RPC based prover).', + parents=[k_cli_args.logging_args, k_cli_args.spec_args, config_args.config_args], + ) + + prove_args.add_argument( + '--failure-info', + default=None, + action='store_true', + help='Print out more information about proof failures.', + ) + prove_args.add_argument( + '--show-kcfg', + default=None, + action='store_true', + help='Display the resulting proof KCFG.', + ) + prove_args.add_argument( + '--max-depth', + type=int, + help='Maximum number of steps to take in symbolic execution per basic block.', + ) + prove_args.add_argument( + '--max-iterations', + type=int, + help='Maximum number of KCFG explorations to take in attempting to discharge proof.', + ) self.add_option( DirPathOption( diff --git a/pyk/src/pyk/cli/args.py b/pyk/src/pyk/cli/args.py index 0aaa478e806..b8885397d82 100644 --- a/pyk/src/pyk/cli/args.py +++ b/pyk/src/pyk/cli/args.py @@ -5,20 +5,10 @@ from functools import cached_property from pathlib import Path from typing import IO, TYPE_CHECKING, Any +from argparse import FileType from ..ktool.kompile import KompileBackend, LLVMKompileType, TypeInferenceMode, Warnings -from .cli import ( - BoolOption, - BugReportOption, - DirPathOption, - EnumOption, - IntOption, - Options, - OptionsGroup, - StringListOption, - StringOption, - WriteFileOption, -) +from .cli import Option, Options, OptionsGroup from .utils import bug_report_arg, dir_path, ensure_dir_path, file_path if TYPE_CHECKING: @@ -30,19 +20,9 @@ class LoggingOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() + self.add_option(Option('--debug', bool, 'debug', 'Debug output.', default=False, action='store_true')) self.add_option( - BoolOption(name='debug', cmd_line_name='--debug', optional=True, default=False, help_str='Debug output.') - ) - self.add_option( - BoolOption( - name='verbose', - cmd_line_name='--verbose', - aliases=['-v'], - toml_name='v', - optional=True, - default=False, - help_str='Debug output.', - ) + Option('--verbose', bool, 'verbose', 'Verbose output', default=False, action='store_true', aliases=['-v']) ) @@ -71,26 +51,25 @@ class WarningOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() self.add_option( - BoolOption( - name='warnings_to_errors', - cmd_line_name='--warnings-to-errors', - aliases=['-w2e'], + Option( + '--warnings-to-errors', + bool, + 'warnings_to_errors', + 'Turn warnings into errors (no effect on pyk, only subcommands).', default=False, - help_str='Turn warnings into errors (no effect on pyk, only subcommands).', - optional=True, + action='store_true', toml_name='w2e', ) ) self.add_option( - EnumOption( - name='warnings', - cmd_line_name='--warnings', - aliases=['-w'], - default=False, - help_str='Warnings to print about (no effect on pyk, only subcommands).', - optional=True, + Option( + '--warnings', + Warnings, + 'warnings', + 'Warnings to print about (no effect on pyk, only subcommands).', + default=None, toml_name='w', - enum_type=Warnings, + choices=list(Warnings), ) ) @@ -120,11 +99,12 @@ class OutputFileOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() self.add_option( - WriteFileOption( - name='output_file', - cmd_line_name='--output-file', + Option( + '--output-file', + FileType('w'), + 'output_file', + 'Output File', default=sys.stdout, - optional=True, ) ) @@ -145,7 +125,7 @@ class DefinitionOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() self.add_option( - DirPathOption(name='definition_dir', toml_name='definition', help_str='Path to definition directory.') + Option('--definition', dir_path, 'definition_dir', 'Path to definition to use.', default=None) ) @@ -166,8 +146,8 @@ class DisplayOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() self.add_option( - BoolOption( - name='minimize', cmd_line_name='--minimize', optional=True, default=True, help_str='Minimize output.' + Option( + '--minimize', bool, 'minimize', 'Minimize output.', action='store_true', default=True ) ) @@ -184,46 +164,35 @@ def default() -> dict[str, Any]: class KDefinitionOptionsGroup(OptionsGroup): includes: list[str] - main_module: str - syntax_module: str + main_module: str | None + syntax_module: str | None md_selector: str + def __init__(self) -> None: super().__init__() self.add_option( - StringListOption( - name='includes', - cmd_line_name='-I', - optional=True, - default=[], - help_str='Directories to lookup K definitions in.', + Option( + '-I', str, 'includes', 'Directories to lookup K definitions in.', action='append', default=[], + ) ) self.add_option( - StringOption( - name='main_module', - cmd_line_name='--main-module', - optional=True, - default=None, - help_str='Name of the main module.', + Option( + '--main-module', str, 'main_module', 'Name of the main module.', default=None, + ) ) self.add_option( - StringOption( - name='syntax_module', - cmd_line_name='--syntax-module', - optional=True, - default=None, - help_str='Name of the syntax module.', + Option( + '--syntax-module', str, 'syntax_module', 'Name of the syntax module.', default=None, + ) ) self.add_option( - StringOption( - name='md_selector', - cmd_line_name='--md-selector', - optional=True, - default='k', - help_str='Code selector expression to use when reading markdown.', + Option( + '--md-selector', str, 'md_selector', 'Code selector expression to use when reading markdown.', default='k', + ) ) @@ -246,12 +215,6 @@ def default() -> dict[str, Any]: } -# @staticmethod -# def from_option_string() -> dict[str, str]: -# return { -# 'includes': 'includes', -# } - class SaveDirOptionsGroup(OptionsGroup): save_directory: Path | None @@ -260,21 +223,13 @@ class SaveDirOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() self.add_option( - DirPathOption( - name='save_directory', - cmd_line_name='--save-directory', - optional=True, - default=None, - help_str='Directory to save proof artifacts at for reuse.', + Option( + '--save-directory', ensure_dir_path, 'save_directory', 'Directory to save proof artifacts at for reuse.', default=None, ) ) self.add_option( - DirPathOption( - name='temp_directory', - cmd_line_name='--temp-directory', - optional=True, - default=None, - help_str='Directory to save proof intermediate temporaries to.', + Option( + '--temp-directory', ensure_dir_path, 'temp_directory', 'Directory to save proof intermediate temporaries to.', default=None, ) ) @@ -300,43 +255,47 @@ class SpecOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() self.add_option( - DirPathOption( - name='spec_file', - optional=False, - help_str='Path to spec file.', + Option( + 'spec_file', + file_path, + help_str='Path to spec_file.', + required=True, ) ) self.add_option( - StringOption( - name='spec_module', - cmd_line_name='--spec-module', - optional=True, + Option( + '--spec-module', + str, + 'spec_module', + 'Module with claims to be proven.', default=None, - help_str='Module with claims to be proven.', ) ) self.add_option( - StringListOption( - name='claim_labels', - cmd_line_name='--claim', - toml_name='claim', - optional=True, + Option( + '--claim', + str, + 'claim_labels', + 'Only prove listed claims, MODULE_NAME.claim-id', + action='append', default=None, - help_str='Only prove listed claims, MODULE_NAME.claim-id', + toml_name='claim', ) ) self.add_option( - StringListOption( - name='exclude_claim_labels', - cmd_line_name='--exclude-claim', - toml_name='exclude-claim', - optional=True, + Option( + '--exclude_claim', + str, + 'exclude_claim_labels', + 'Skip listed claims, MODULE_NAME.claim-id', + action='append', default=None, - help_str='Skip listed claims, MODULE_NAME.claim-id', + toml_name='exclude-claim', ) ) + class SpecOptions(SaveDirOptions): spec_file: Path spec_module: str | None @@ -364,8 +323,8 @@ class KompileOptionsGroup(OptionsGroup): llvm_kompile: bool llvm_library: bool enable_llvm_debug: bool - llvm_kompile_type: LLVMKompileType - llvm_kompile_output: Path + llvm_kompile_type: LLVMKompileType | None + llvm_kompile_output: Path | None llvm_proof_hint_instrumentation: bool read_only: bool o0: bool @@ -380,183 +339,65 @@ class KompileOptionsGroup(OptionsGroup): bison_lists: bool no_exc_wrap: bool + def __init__(self) -> None: super().__init__() self.add_option( - BoolOption( - name='emit_json', - cmd_line_name='--emit-json', - default=True, - help_str='Emit JSON definition after compilation.', - optional=True, - ) + Option('--emit-json', bool, 'emit_json', 'Emit JSON definition after compilation.', action='store_true', default=False) ) self.add_option( - BoolOption( - name='llvm_kompile', - cmd_line_name='--no-llvm-kompile', - default=False, - help_str='Do not run llvm-kompile process.', - optional=True, - ) + Option('--no-llvm-kompile', bool, 'llvm_kompile', 'Do not run llvm-kompile process.', action='store_false', default=True) ) self.add_option( - BoolOption( - name='llvm_library', - cmd_line_name='--with-llvm-library', - toml_name='with-llvm-library', - default=False, - help_str='Make kompile generate a dynamic llvm library.', - optional=True, - ) + Option('--with-llvm-library', bool, 'llvm_library', 'Make kompile generate a dynamic llvm library.', action='store_true', default=False) ) self.add_option( - BoolOption( - name='enable_llvm_debug', - cmd_line_name='--enable-llvm-debug', - default=False, - help_str='Make kompile generate debug symbols for llvm.', - optional=True, - ) + Option('--enable-llvm-debug', bool, 'enable_llvm_debug', 'Make kompile generate debug symbols for llvm.', action='store_true', default=False) ) self.add_option( - EnumOption( - enum_type=LLVMKompileType, - name='llvm_kompile_type', - cmd_line_name='--llvm-kompile-type', - default=None, - help_str='Mode to kompile LLVM backend in.', - ) + Option('--llvm-kompile-type', LLVMKompileType, 'llvm_kompile_type', 'Mode to kompile LLVM backend in.', default=None, choices=list(LLVMKompileType)) ) self.add_option( - DirPathOption( - name='llvm_kompile_output', - cmd_line_name='--llvm-kompile-output', - default=None, - help_str='Location to put kompiled LLVM backend at.', - ) + Option('--llvm-kompile-output', ensure_dir_path, 'llvm_kompile_output', 'Location to put kompiled LLVM backend at.', default=None) ) self.add_option( - BoolOption( - name='llvm_proof_hint_instrumentation', - cmd_line_name='--llvm-proof-hint-instrumentation', - default=False, - help_str='Enable proof hint generation in LLVM backend kompilation.', - optional=True, - ) + Option('--llvm-proof-hint-instrumentation', bool, 'llvm_proof_hint_instrumentation', 'Enable proof hint generation in LLVM backend kompilation', action='store_true', default=False) ) self.add_option( - BoolOption( - name='read_only', - cmd_line_name='--read-only-kompiled-directory', - toml_name='read-only-kompiled-directory', - default=False, - help_str='Generate a kompiled directory that K will not attempt to write to afterwards.', - optional=True, - ) + Option('--read-only-kompiled-directory', bool, 'read_only', 'Generate a kompiled directory that K will not attempt to write to afterwards.', action='store_true', default=False) ) self.add_option( - BoolOption( - name='o0', - cmd_line_name='-O0', - toml_name='O0', - default=False, - help_str='Optimization level 0.', - optional=True, - ) + Option('-O0', bool, 'o0', 'Optimization level 0', action='store_true', default=False) ) self.add_option( - BoolOption( - name='o1', - cmd_line_name='-O1', - toml_name='O1', - default=False, - help_str='Optimization level 1.', - optional=True, - ) + Option('-O1', bool, 'o1', 'Optimization level 1', action='store_true', default=False) ) self.add_option( - BoolOption( - name='o2', - cmd_line_name='-O2', - toml_name='O2', - default=False, - help_str='Optimization level 2.', - optional=True, - ) + Option('-O2', bool, 'o2', 'Optimization level 2', action='store_true', default=False) ) self.add_option( - BoolOption( - name='o3', - cmd_line_name='-O3', - toml_name='O3', - default=False, - help_str='Optimization level 3.', - optional=True, - ) + Option('-O3', bool, 'o3', 'Optimization level 3', action='store_true', default=False) ) self.add_option( - StringListOption( - name='ccopts', - cmd_line_name='-ccopt', - optional=True, - default=[], - help_str='Additional arguments to pass to llvm-kompile', - ) + Option('-ccopt', str, 'ccopts', 'Additional arguments to pass to llvm-kompile', action='append', default=[]) ) self.add_option( - BoolOption( - name='enable_search', - cmd_line_name='--enable-search', - optional=True, - default=False, - help_str='Enable search mode on LLVM backend krun.', - ) + Option('--enable-search', bool, 'enable_search', 'Enable search mode on LLVM backend krun', action='store_true', default=False) ) self.add_option( - BoolOption( - name='coverage', - cmd_line_name='--coverage', - optional=True, - default=False, - help_str='Enable logging semantic rule coverage measurement.', - ) + Option('--coverage', bool, 'coverage', 'Enable logging semantics rule coverage measurement', action='store_true', default=False) ) self.add_option( - BoolOption( - name='gen_bison_parser', - cmd_line_name='--gen-bison-parser', - optional=True, - default=False, - help_str='Generate standalone Bison parser for program sort.', - ) + Option('--gen-bison-parser', bool, 'gen_bison_parser', 'Generate standolone Bison parser for program sort.', action='store_true', default=False) ) self.add_option( - BoolOption( - name='gen_glr_bison_parser', - cmd_line_name='--gen-glr-bison-parser', - optional=True, - default=False, - help_str='Generate standalone GLR Bison parser for program sort.', - ) + Option('--gen-glr-bison-parser', bool, 'gen_glr_bison_parser', 'Generate standolone GLR Bison parser for program sort.', action='store_true', default=False) ) self.add_option( - BoolOption( - name='bison_lists', - cmd_line_name='--bison-lists', - optional=True, - default=False, - help_str='Disable List{Sort} parsing to make grammar LR(1) for Bison parser.', - ) + Option('--bison-lists', bool, 'bison_lists', 'Disable List{Sort} parsing to make grammar LR(1) for Bison parser.', action='store_true', default=False) ) self.add_option( - BoolOption( - name='no_exc_wrap', - cmd_line_name='--no-exc-wrap', - optional=True, - default=False, - help_str='Do not wrap the output on the CLI.', - ) + Option('--no-exc-wrap', bool, 'no_exc_wrap', 'Do not wrap the output on the CLI.', action='store_true', default=False) ) @@ -619,17 +460,13 @@ def from_option_string() -> dict[str, str]: class ParallelOptionsGroup(OptionsGroup): + workers: int + def __init__(self) -> None: super().__init__() self.add_option( - IntOption( - name='workers', - aliases=['-j'], - cmd_line_name='--workers', - toml_name='j', - default=1, - help_str='Number of processes to run in parallel', - optional=True, + Option( + '--workers', int, 'workers', 'Number of processes to run in parallel', aliases=['-j'], default=1, toml_name='j' ) ) @@ -651,17 +488,13 @@ def from_option_string() -> dict[str, str]: class BugReportOptionsGroup(OptionsGroup): + bug_report: BugReport | None + def __init__(self) -> None: super().__init__() - self.add_option( - BugReportOption( - name='bug_report', - cmd_line_name='--bug-report', - default=None, - help_str='Generate bug report with given name.', - optional=True, - ) - ) + self.add_option(Option( + '--bug-report', bug_report_arg, 'bug_report', 'Generate bug report with given name.', default=None, + )) class BugReportOptions(Options): @@ -673,34 +506,20 @@ def default() -> dict[str, Any]: class SMTOptionsGroup(OptionsGroup): + smt_timeout: int + smt_retry_limit: int + smt_tactic: str | None + def __init__(self) -> None: super().__init__() self.add_option( - IntOption( - name='smt_timeout', - cmd_line_name='--smt-timeout', - default=300, - help_str='Timeout in ms to use for SMT queries.', - optional=True, - ) + Option('--smt-timeout', int, 'smt_timeout', 'Timeout in ms to use for SMT queries.', default=300) ) self.add_option( - IntOption( - name='smt_retry_limit', - cmd_line_name='--smt-retry-limit', - default=10, - help_str='Number of times to retry SMT queries with scaling timeouts.', - optional=True, - ) + Option('--smt-retry-limit', int, 'smt_retry_limit', 'Number of times to retry SMT queries with scaling timeouts.', default=10) ) self.add_option( - StringOption( - name='smt_tactic', - cmd_line_name='--smt-tactic', - default=None, - help_str='Z3 tactic to use when checking satisfiability. Example: (check-sat-using-smt)', - optional=True, - ) + Option('--smt-tactic', str, 'smt_tactic', 'Z3 tactic to use with checking satisfiability. Example: (check-sat-using-smt)', default=None) ) diff --git a/pyk/src/pyk/cli/cli.py b/pyk/src/pyk/cli/cli.py index e54399d4449..419b2d8435b 100644 --- a/pyk/src/pyk/cli/cli.py +++ b/pyk/src/pyk/cli/cli.py @@ -1,24 +1,14 @@ from __future__ import annotations from abc import abstractmethod -from argparse import ArgumentParser, FileType -from pathlib import Path +from argparse import ArgumentParser # from enum import Enum -from typing import IO, TYPE_CHECKING, Any, Generic, Iterable, TypeVar - -from ..utils import ensure_dir_path -from .utils import BugReport, bug_report_arg +from typing import Any, Callable, Generic, Iterable, TypeVar T = TypeVar('T') OG = TypeVar('OG', bound='OptionsGroup') -if TYPE_CHECKING: - from enum import EnumMeta - - # from argparse import _SubParsersAction - from types import UnionType - class CLI: _commands: list[Command] @@ -57,265 +47,66 @@ def get_and_exec_command(self) -> None: class Option: _name: str _aliases: list[str] - _cmd_line_name: str + _dest: str _toml_name: str - _optional: bool + _action: str | None + _choices: list[str] | None + _const: Any | None + _default: Any | None _help_str: str | None _metavar: str | None - _default: Any + _nargs: int | str | None + _required: bool + _type: Callable[[str], Any] def __init__( self, name: str, - aliases: Iterable[str] = (), - cmd_line_name: str | None = None, - toml_name: str | None = None, - optional: bool = False, + arg_type: Callable[[str], Any], + dest: str | None = None, help_str: str | None = None, + action: str | None = None, + choices: list[str] | None = None, + const: Any | None = None, + aliases: Iterable[str] = (), + default: Any | str = 'NoDefault', metavar: str | None = None, - default: Any = 'NoDefault', + nargs: int | str | None = None, + required: bool = False, + toml_name: str | None = None, ) -> None: self._name = name self._aliases = list(aliases) - self._cmd_line_name = cmd_line_name or name - self._toml_name = cmd_line_name or name - self._optional = optional + self._dest = dest or name + self._toml_name = (toml_name or dest) or name + self._action = action + self._choices = choices + self._const = const + self._default = default self._help_str = help_str self._metavar = metavar - self._type = type - - if default == 'NoDefault' and optional: - raise ValueError(f'Optional option {name} must define a default value.') - if default != 'NoDefault' and not optional: - raise ValueError(f'Required option {name} cannot take a default value.') + self._nargs = nargs + self._required = required + self._type = arg_type self.set_default(default) - @abstractmethod - def add_arg(self, parser: ArgumentParser) -> None: ... + def add_arg(self, args: ArgumentParser) -> None: ... # TODO - @property - def is_optional(self) -> bool: - return self._optional + def set_default(self, default: Any) -> None: + self._default = default @property def name(self) -> str: return self._name - @property - def aliases(self) -> list[str]: - return self._aliases - - @property - def cmd_line_name(self) -> str: - return self._cmd_line_name - - @property - def toml_name(self) -> str: - return self._toml_name - - @property - def help_str(self) -> str | None: - return self._help_str - - @property - def metavar(self) -> str | None: - return self._metavar - @property def default(self) -> Any: return self._default - @abstractmethod - def set_default(self, default: Any) -> None: ... - @property - def type(self) -> type | UnionType: - return self._type - - -class IntOption(Option): - - def set_default(self, default: Any) -> None: - assert isinstance(default, int) - self._default = default - - def add_arg(self, args: ArgumentParser) -> None: - args.add_argument( - self.cmd_line_name, - *(self.aliases), - default='NoDefault', - required=self.is_optional, - type=int, - help=self.help_str, - metavar=self.metavar, - dest=self.name, - ) - - -class BoolOption(Option): - - def set_default(self, default: Any) -> None: - assert isinstance(default, bool) - self._default = default - - def add_arg(self, args: ArgumentParser) -> None: - args.add_argument( - self.cmd_line_name, - *(self.aliases), - default='NoDefault', - required=self.is_optional, - type=bool, - help=self.help_str, - metavar=self.metavar, - action='store_false' if self.default else 'store_true', - dest=self.name, - ) - - -class StringOption(Option): - - def set_default(self, default: Any) -> None: - assert isinstance(default, str) - self._default = default - - def add_arg(self, args: ArgumentParser) -> None: - args.add_argument( - self.cmd_line_name, - *(self.aliases), - default='NoDefault', - required=not self.is_optional, - type=bool, - help=self.help_str, - metavar=self.metavar, - dest=self.name, - ) - - -class EnumOption(Option): - _enum_type: EnumMeta - - def __init__( - self, - enum_type: EnumMeta, - *args: Any, - **kwargs: Any, - ) -> None: - super.__init__(*args, **kwargs) - self._enum_type = enum_type - - def set_default(self, default: Any) -> None: - assert isinstance(default, self._enum_type) - self._default = default - - def add_arg(self, args: ArgumentParser) -> None: - args.add_argument( - self.cmd_line_name, - *(self.aliases), - default='NoDefault', - required=self.is_optional, - type=self._enum_type, - help=self.help_str, - metavar=self.metavar, - dest=self.name, - choices=list(self._enum_type), - ) - - -class ReadFileOption(Option): - - def set_default(self, default: Any) -> None: - assert isinstance(default, IO) - self._default = default - - def add_arg(self, args: ArgumentParser) -> None: - args.add_argument( - self.cmd_line_name, - *(self.aliases), - default='NoDefault', - required=self.is_optional, - type=FileType('r'), - help=self.help_str, - metavar=self.metavar, - dest=self.name, - ) - - -class WriteFileOption(Option): - - def set_default(self, default: Any) -> None: - assert isinstance(default, IO) - self._default = default - - def add_arg(self, args: ArgumentParser) -> None: - args.add_argument( - self.cmd_line_name, - *(self.aliases), - default='NoDefault', - required=self.is_optional, - type=FileType('w'), - help=self.help_str, - metavar=self.metavar, - dest=self.name, - ) - - -class BugReportOption(Option): - - def set_default(self, default: Any) -> None: - assert isinstance(default, BugReport) - self._default = default - - def add_arg(self, args: ArgumentParser) -> None: - args.add_argument( - self.cmd_line_name, - *(self.aliases), - default='NoDefault', - required=self.is_optional, - type=bug_report_arg, - help=self.help_str, - metavar=self.metavar, - dest=self.name, - ) - - -class DirPathOption(Option): - - def set_default(self, default: Any) -> None: - assert isinstance(default, Path) - self._default = default - - def add_arg(self, args: ArgumentParser) -> None: - args.add_argument( - self.cmd_line_name, - *(self.aliases), - default='NoDefault', - required=self.is_optional, - type=ensure_dir_path, - help=self.help_str, - metavar=self.metavar, - dest=self.name, - ) - - -class StringListOption(Option): - - def set_default(self, default: Any) -> None: - assert isinstance(default, Iterable) - self._default = default - - def add_arg(self, args: ArgumentParser) -> None: - args.add_argument( - self.cmd_line_name, - *(self.aliases), - default='NoDefault', - required=self.is_optional, - type=list[str], - help=self.help_str, - metavar=self.metavar, - dest=self.name, - action='append', - ) + def is_optional(self) -> bool: + return not self._required class Command(Generic[OG]): @@ -350,7 +141,6 @@ class OptionsGroup: def extract(self, args: dict[str, Any]) -> None: for option in self.options: if option.name in args: - assert isinstance(args[option.name], option.type) self.__setattr__(option.name, args[option.name]) # TODO elif option exists in TOML file, set it to the value from there else: From eeef4189469b909350c0b7a6614b2a03da8cb348 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 3 May 2024 14:16:12 -0500 Subject: [PATCH 11/16] Finish converting to plain Option --- pyk/src/pyk/__main__.py | 242 ++++++++++++++--------------------- pyk/src/pyk/cli/args.py | 276 +++++++++++++++++++++++++++++----------- 2 files changed, 302 insertions(+), 216 deletions(-) diff --git a/pyk/src/pyk/__main__.py b/pyk/src/pyk/__main__.py index d9e27427cd0..38dacc672d2 100644 --- a/pyk/src/pyk/__main__.py +++ b/pyk/src/pyk/__main__.py @@ -3,12 +3,14 @@ import json import logging import sys +from argparse import FileType from pathlib import Path from typing import TYPE_CHECKING -from argparse import FileType from graphviz import Digraph +from pyk.cli.utils import dir_path + from .cli.args import ( DefinitionOptionsGroup, DisplayOptionsGroup, @@ -16,7 +18,6 @@ KompileOptionsGroup, LoggingOptionsGroup, OutputFileOptionsGroup, - SaveDirOptionsGroup, SpecOptionsGroup, WarningOptionsGroup, ) @@ -69,8 +70,8 @@ def main() -> None: class PrintOptionsGroup(DefinitionOptionsGroup, OutputFileOptionsGroup, DisplayOptionsGroup, LoggingOptionsGroup): term: IO[Any] input: PrintInput - omit_labels: list[str] | None - keep_cells: list[str] | None + omit_labels: str | None + keep_cells: str | None def __init__(self) -> None: super().__init__() @@ -78,17 +79,37 @@ def __init__(self) -> None: Option('term', FileType('r'), help_str='Input term (in format specified with --input)', required=True) ) self.add_option( - Option('--input', PrintInput, 'input', help_str='Input format', choices=list(PrintInput), default=PrintInput.KAST_JSON) + Option( + '--input', + PrintInput, + 'input', + help_str='Input format', + choices=list(PrintInput), + default=PrintInput.KAST_JSON, + ) ) self.add_option( - Option('--omit-labels', str, 'omit_labels', help_str='List of labels to omit from output.', nargs='?', default=[]) + Option( + '--omit-labels', + str, + 'omit_labels', + help_str='List of labels to omit from output.', + nargs='?', + default=[], + ) ) self.add_option( - Option('--keep-cells', str, 'keep_cells', help_str='List of cells with primitive values to keep in output.', nargs='?', default=[]) + Option( + '--keep-cells', + str, + 'keep_cells', + help_str='List of cells with primitive values to keep in output.', + nargs='?', + default=[], + ) ) - class PrintCommand(Command[PrintOptionsGroup]): def __init__(self) -> None: super().__init__('print', 'Pretty print a term.', PrintOptionsGroup()) @@ -138,7 +159,12 @@ class RPCPrintOptionsGroup(DefinitionOptionsGroup, OutputFileOptionsGroup, Loggi def __init__(self) -> None: super().__init__() self.add_option( - Option('input_file', FileType('r'), help_str='An input file containing the JSON RPC request or response with KoreJSON payload. ', required=True) + Option( + 'input_file', + FileType('r'), + help_str='An input file containing the JSON RPC request or response with KoreJSON payload. ', + required=True, + ) ) @@ -235,10 +261,20 @@ class RPCKastOptionsGroup(OutputFileOptionsGroup, LoggingOptionsGroup): def __init__(self) -> None: super().__init__() self.add_option( - Option('reference_request_file', FileType('r'), help_str='An input file containing a JSON RPC request to serve as a reference for the new request.', required=True) + Option( + 'reference_request_file', + FileType('r'), + help_str='An input file containing a JSON RPC request to serve as a reference for the new request.', + required=True, + ) ) self.add_option( - Option('response_file', FileType('r'), help_str='An input file containing a JSON RPC response with KoreJSON payload.', required=True) + Option( + 'response_file', + FileType('r'), + help_str='An input file containing a JSON RPC response with KoreJSON payload.', + required=True, + ) ) @@ -281,18 +317,10 @@ class ProveLegacyOptionsGroup(DefinitionOptionsGroup, OutputFileOptionsGroup, Lo def __init__(self) -> None: super().__init__() - self.add_option( - Option('main_file', str, help_str='Main file used for kompilation', required=True) - ) - self.add_option( - Option('spec_file', str, help_str='File with the specification module.', required=True) - ) - self.add_option( - Option('spec_module', str, help_str='Module with claims to be proven.', required=True) - ) - self.add_option( - Option('kArgs', str, 'k_args', 'Module with claims to be proven.', required=True, nargs='*') - ) + self.add_option(Option('main_file', str, help_str='Main file used for kompilation', required=True)) + self.add_option(Option('spec_file', str, help_str='File with the specification module.', required=True)) + self.add_option(Option('spec_module', str, help_str='Module with claims to be proven.', required=True)) + self.add_option(Option('kArgs', str, 'k_args', 'Module with claims to be proven.', required=True, nargs='*')) class ProveLegacyCommand(Command[ProveLegacyOptionsGroup]): @@ -309,9 +337,7 @@ def exec(self) -> None: _LOGGER.info(f'Wrote file: {self.options.output_file.name}') -class ProveOptionsGroup(LoggingOptionsGroup, SpecOptionsGroup, SaveDirOptionsGroup): - definition_dir: Path | None - type_inference_mode: TypeInferenceMode | None +class ProveOptionsGroup(LoggingOptionsGroup, SpecOptionsGroup): failure_info: bool kore_rpc_command: str | Iterable[str] | None max_depth: int | None @@ -321,101 +347,45 @@ class ProveOptionsGroup(LoggingOptionsGroup, SpecOptionsGroup, SaveDirOptionsGro def __init__(self) -> None: super().__init__() self.add_option( - Option() - ) - - - prove_args = pyk_args_command.add_parser( - 'prove', - help='Prove an input specification (using RPC based prover).', - parents=[k_cli_args.logging_args, k_cli_args.spec_args, config_args.config_args], - ) - - prove_args.add_argument( - '--failure-info', - default=None, - action='store_true', - help='Print out more information about proof failures.', - ) - prove_args.add_argument( - '--show-kcfg', - default=None, - action='store_true', - help='Display the resulting proof KCFG.', - ) - prove_args.add_argument( - '--max-depth', - type=int, - help='Maximum number of steps to take in symbolic execution per basic block.', - ) - prove_args.add_argument( - '--max-iterations', - type=int, - help='Maximum number of KCFG explorations to take in attempting to discharge proof.', - ) - - self.add_option( - DirPathOption( - name='definition_dir', - cmd_line_name='--definition', - toml_name='definition', - help_str='Path to definition to use.', - optional=True, - default=None, - ) - ) - self.add_option( - EnumOption( - enum_type=TypeInferenceMode, - name='type_inference_mode', - cmd_line_name='--type-inference-mode', - help_str='Mode for doing K rule type inference in.', - optional=True, - default=None, - ) - ) - self.add_option( - BoolOption( - name='failure_info', - cmd_line_name='--failure-info', - help_str='Print out more information about proof failures.', - default=None, + Option( + '--failure-info', + bool, + 'failure_info', + 'Print out more information about proof failures.', + default=False, + action='store_true', ) ) self.add_option( - StringOption( - name='kore_rpc_command', - cmd_line_name='--kore-rpc-command', - help_str='Custom command to start RPC server', - default=None, + Option( + '--show-kcfg', + bool, + 'show_kcfg', + 'Display the resulting proof KCFG.', + default=False, + action='store_true', ) ) self.add_option( - IntOption( - name='max_depth', - cmd_line_name='--max-depth', - help_str='Maximum number of steps to take in symbolic execution per basic block.', + Option( + '--max-depth', + int, + 'max_depth', + 'Maximum number of stepss to take in symbolic execution per basic block.', default=None, - optional=True, ) ) self.add_option( - IntOption( - name='max_iterations', - cmd_line_name='--max-iterations', - help_str='Maximum number of KCFG explorations to take in attempting to discharge proof.', + Option( + '--max-iterations', + int, + 'max_iterations', + 'Maximum number of KCFG explorations to take in attempting to discharge proof.', default=None, - optional=True, ) ) self.add_option( - BoolOption( - name='show_kcfg', - cmd_line_name='--show-kcfg', - help_str='Display the resulting proof KCFG.', - default=False, - optional=True, - ) + Option('--kore-rpc-command', str, 'kore_rpc_command', 'Custom command to start RPC server.', default=None) ) @@ -470,41 +440,34 @@ class KompileCommandOptionsGroup( def __init__(self) -> None: super().__init__() self.add_option( - DirPathOption( - name='definition_dir', - cmd_line_name='--output-definition', - aliases=['--definition'], + Option( + '--output-definition', + ensure_dir_path, + 'definition_dir', + 'Path to definition to use.', toml_name='definition', - default=None, - help_str='Path to kompile definition to.', - optional=True, - ) - ) - self.add_option( - StringOption( - name='main_file', - optional=False, - help_str='File with the specification module.', + aliases=['--definition'], ) ) + self.add_option(Option('main_file', str, required=True, help_str='File with the specification module.')) self.add_option( - EnumOption( - enum_type=KompileBackend, - name='backend', - cmd_line_name='--backend', + Option( + '--backend', + KompileBackend, + 'backend', + 'K backend to target with compilation.', + choices=list(KompileBackend), default=KompileBackend.LLVM, - help_str='K backend to target with compilation.', - optional=True, ) ) self.add_option( - EnumOption( - enum_type=TypeInferenceMode, - name='type_inference_mode', - cmd_line_name='--type-inference-mode', + Option( + '--type-inference-mode', + TypeInferenceMode, + 'type_inference_mode', + 'Mode for doing K rule type inference in.', + choices=list(TypeInferenceMode), default=None, - help_str='Mode for doing K rule type inference in.', - optional=True, ) ) @@ -581,15 +544,8 @@ class RunOptionsGroup(LoggingOptionsGroup): def __init__(self) -> None: super().__init__() - self.add_option(StringOption(name='pgm_file', optional=False, help_str='File program to run in it.')) - self.add_option( - DirPathOption( - name='definition_dir', - cmd_line_name='--definition', - optional=False, - help_str='Path to definition to use.', - ) - ) + self.add_option(Option('pgm_file', str, required=True, help_str='File program to run in it.')) + self.add_option(Option('--definition', dir_path, 'definition_dir', 'Path to definition to use', default=None)) class RunCommand(Command[RunOptionsGroup]): @@ -639,7 +595,7 @@ class CoverageOptionsGroup(DefinitionOptionsGroup, OutputFileOptionsGroup, Loggi def __init__(self) -> None: super().__init__() self.add_option( - ReadFileOption(name='coverage_file', optional=False, help_str='Coverage fild to build log for.') + Option('coverage_file', FileType('r'), required=True, help_str='Coverage file to build log for.') ) diff --git a/pyk/src/pyk/cli/args.py b/pyk/src/pyk/cli/args.py index b8885397d82..caf2e3b40e3 100644 --- a/pyk/src/pyk/cli/args.py +++ b/pyk/src/pyk/cli/args.py @@ -1,11 +1,10 @@ from __future__ import annotations import sys -from argparse import ArgumentParser +from argparse import ArgumentParser, FileType from functools import cached_property from pathlib import Path from typing import IO, TYPE_CHECKING, Any -from argparse import FileType from ..ktool.kompile import KompileBackend, LLVMKompileType, TypeInferenceMode, Warnings from .cli import Option, Options, OptionsGroup @@ -124,9 +123,7 @@ class DefinitionOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() - self.add_option( - Option('--definition', dir_path, 'definition_dir', 'Path to definition to use.', default=None) - ) + self.add_option(Option('--definition', dir_path, 'definition_dir', 'Path to definition to use.', default=None)) class DefinitionOptions(Options): @@ -145,11 +142,7 @@ class DisplayOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() - self.add_option( - Option( - '--minimize', bool, 'minimize', 'Minimize output.', action='store_true', default=True - ) - ) + self.add_option(Option('--minimize', bool, 'minimize', 'Minimize output.', action='store_true', default=True)) class DisplayOptions(Options): @@ -168,31 +161,43 @@ class KDefinitionOptionsGroup(OptionsGroup): syntax_module: str | None md_selector: str - def __init__(self) -> None: super().__init__() self.add_option( Option( - '-I', str, 'includes', 'Directories to lookup K definitions in.', action='append', default=[], - + '-I', + str, + 'includes', + 'Directories to lookup K definitions in.', + action='append', + default=[], ) ) self.add_option( Option( - '--main-module', str, 'main_module', 'Name of the main module.', default=None, - + '--main-module', + str, + 'main_module', + 'Name of the main module.', + default=None, ) ) self.add_option( Option( - '--syntax-module', str, 'syntax_module', 'Name of the syntax module.', default=None, - + '--syntax-module', + str, + 'syntax_module', + 'Name of the syntax module.', + default=None, ) ) self.add_option( Option( - '--md-selector', str, 'md_selector', 'Code selector expression to use when reading markdown.', default='k', - + '--md-selector', + str, + 'md_selector', + 'Code selector expression to use when reading markdown.', + default='k', ) ) @@ -215,25 +220,6 @@ def default() -> dict[str, Any]: } - -class SaveDirOptionsGroup(OptionsGroup): - save_directory: Path | None - temp_directory: Path | None - - def __init__(self) -> None: - super().__init__() - self.add_option( - Option( - '--save-directory', ensure_dir_path, 'save_directory', 'Directory to save proof artifacts at for reuse.', default=None, - ) - ) - self.add_option( - Option( - '--temp-directory', ensure_dir_path, 'temp_directory', 'Directory to save proof intermediate temporaries to.', default=None, - ) - ) - - class SaveDirOptions(Options): save_directory: Path | None temp_directory: Path | None @@ -251,6 +237,10 @@ class SpecOptionsGroup(OptionsGroup): spec_module: str | None claim_labels: Iterable[str] | None exclude_claim_labels: Iterable[str] | None + definition_dir: Path | None + type_inference_mode: TypeInferenceMode + save_directory: Path | None + temp_directory: Path | None def __init__(self) -> None: super().__init__() @@ -293,7 +283,35 @@ def __init__(self) -> None: toml_name='exclude-claim', ) ) - + self.add_option(Option('--definition', dir_path, 'definition_dir', 'Path to definition to use.')) + self.add_option( + Option( + '--type-inference-mode', + TypeInferenceMode, + 'type_inference_mode', + 'Mode for doing K rule type inference in.', + choices=list(TypeInferenceMode), + default=TypeInferenceMode.DEFAULT, + ) + ) + self.add_option( + Option( + '--save-directory', + ensure_dir_path, + 'save_directory', + 'Directory to save proof artifacts at for reuse.', + default=None, + ) + ) + self.add_option( + Option( + '--temp-directory', + ensure_dir_path, + 'temp_directory', + 'Directory to save proof intermediate temporaries to.', + default=None, + ) + ) class SpecOptions(SaveDirOptions): @@ -339,65 +357,153 @@ class KompileOptionsGroup(OptionsGroup): bison_lists: bool no_exc_wrap: bool - def __init__(self) -> None: super().__init__() self.add_option( - Option('--emit-json', bool, 'emit_json', 'Emit JSON definition after compilation.', action='store_true', default=False) - ) - self.add_option( - Option('--no-llvm-kompile', bool, 'llvm_kompile', 'Do not run llvm-kompile process.', action='store_false', default=True) - ) - self.add_option( - Option('--with-llvm-library', bool, 'llvm_library', 'Make kompile generate a dynamic llvm library.', action='store_true', default=False) - ) - self.add_option( - Option('--enable-llvm-debug', bool, 'enable_llvm_debug', 'Make kompile generate debug symbols for llvm.', action='store_true', default=False) - ) - self.add_option( - Option('--llvm-kompile-type', LLVMKompileType, 'llvm_kompile_type', 'Mode to kompile LLVM backend in.', default=None, choices=list(LLVMKompileType)) + Option( + '--emit-json', + bool, + 'emit_json', + 'Emit JSON definition after compilation.', + action='store_true', + default=False, + ) ) self.add_option( - Option('--llvm-kompile-output', ensure_dir_path, 'llvm_kompile_output', 'Location to put kompiled LLVM backend at.', default=None) + Option( + '--no-llvm-kompile', + bool, + 'llvm_kompile', + 'Do not run llvm-kompile process.', + action='store_false', + default=True, + ) ) self.add_option( - Option('--llvm-proof-hint-instrumentation', bool, 'llvm_proof_hint_instrumentation', 'Enable proof hint generation in LLVM backend kompilation', action='store_true', default=False) + Option( + '--with-llvm-library', + bool, + 'llvm_library', + 'Make kompile generate a dynamic llvm library.', + action='store_true', + default=False, + ) ) self.add_option( - Option('--read-only-kompiled-directory', bool, 'read_only', 'Generate a kompiled directory that K will not attempt to write to afterwards.', action='store_true', default=False) + Option( + '--enable-llvm-debug', + bool, + 'enable_llvm_debug', + 'Make kompile generate debug symbols for llvm.', + action='store_true', + default=False, + ) ) self.add_option( - Option('-O0', bool, 'o0', 'Optimization level 0', action='store_true', default=False) + Option( + '--llvm-kompile-type', + LLVMKompileType, + 'llvm_kompile_type', + 'Mode to kompile LLVM backend in.', + default=None, + choices=list(LLVMKompileType), + ) ) self.add_option( - Option('-O1', bool, 'o1', 'Optimization level 1', action='store_true', default=False) + Option( + '--llvm-kompile-output', + ensure_dir_path, + 'llvm_kompile_output', + 'Location to put kompiled LLVM backend at.', + default=None, + ) ) self.add_option( - Option('-O2', bool, 'o2', 'Optimization level 2', action='store_true', default=False) + Option( + '--llvm-proof-hint-instrumentation', + bool, + 'llvm_proof_hint_instrumentation', + 'Enable proof hint generation in LLVM backend kompilation', + action='store_true', + default=False, + ) ) self.add_option( - Option('-O3', bool, 'o3', 'Optimization level 3', action='store_true', default=False) + Option( + '--read-only-kompiled-directory', + bool, + 'read_only', + 'Generate a kompiled directory that K will not attempt to write to afterwards.', + action='store_true', + default=False, + ) ) + self.add_option(Option('-O0', bool, 'o0', 'Optimization level 0', action='store_true', default=False)) + self.add_option(Option('-O1', bool, 'o1', 'Optimization level 1', action='store_true', default=False)) + self.add_option(Option('-O2', bool, 'o2', 'Optimization level 2', action='store_true', default=False)) + self.add_option(Option('-O3', bool, 'o3', 'Optimization level 3', action='store_true', default=False)) self.add_option( - Option('-ccopt', str, 'ccopts', 'Additional arguments to pass to llvm-kompile', action='append', default=[]) + Option('-ccopt', str, 'ccopts', 'Additional arguments to pass to llvm-kompile', action='append', default=[]) ) self.add_option( - Option('--enable-search', bool, 'enable_search', 'Enable search mode on LLVM backend krun', action='store_true', default=False) + Option( + '--enable-search', + bool, + 'enable_search', + 'Enable search mode on LLVM backend krun', + action='store_true', + default=False, + ) ) self.add_option( - Option('--coverage', bool, 'coverage', 'Enable logging semantics rule coverage measurement', action='store_true', default=False) + Option( + '--coverage', + bool, + 'coverage', + 'Enable logging semantics rule coverage measurement', + action='store_true', + default=False, + ) ) self.add_option( - Option('--gen-bison-parser', bool, 'gen_bison_parser', 'Generate standolone Bison parser for program sort.', action='store_true', default=False) + Option( + '--gen-bison-parser', + bool, + 'gen_bison_parser', + 'Generate standolone Bison parser for program sort.', + action='store_true', + default=False, + ) ) self.add_option( - Option('--gen-glr-bison-parser', bool, 'gen_glr_bison_parser', 'Generate standolone GLR Bison parser for program sort.', action='store_true', default=False) + Option( + '--gen-glr-bison-parser', + bool, + 'gen_glr_bison_parser', + 'Generate standolone GLR Bison parser for program sort.', + action='store_true', + default=False, + ) ) self.add_option( - Option('--bison-lists', bool, 'bison_lists', 'Disable List{Sort} parsing to make grammar LR(1) for Bison parser.', action='store_true', default=False) + Option( + '--bison-lists', + bool, + 'bison_lists', + 'Disable List{Sort} parsing to make grammar LR(1) for Bison parser.', + action='store_true', + default=False, + ) ) self.add_option( - Option('--no-exc-wrap', bool, 'no_exc_wrap', 'Do not wrap the output on the CLI.', action='store_true', default=False) + Option( + '--no-exc-wrap', + bool, + 'no_exc_wrap', + 'Do not wrap the output on the CLI.', + action='store_true', + default=False, + ) ) @@ -466,7 +572,13 @@ def __init__(self) -> None: super().__init__() self.add_option( Option( - '--workers', int, 'workers', 'Number of processes to run in parallel', aliases=['-j'], default=1, toml_name='j' + '--workers', + int, + 'workers', + 'Number of processes to run in parallel', + aliases=['-j'], + default=1, + toml_name='j', ) ) @@ -492,9 +604,15 @@ class BugReportOptionsGroup(OptionsGroup): def __init__(self) -> None: super().__init__() - self.add_option(Option( - '--bug-report', bug_report_arg, 'bug_report', 'Generate bug report with given name.', default=None, - )) + self.add_option( + Option( + '--bug-report', + bug_report_arg, + 'bug_report', + 'Generate bug report with given name.', + default=None, + ) + ) class BugReportOptions(Options): @@ -516,10 +634,22 @@ def __init__(self) -> None: Option('--smt-timeout', int, 'smt_timeout', 'Timeout in ms to use for SMT queries.', default=300) ) self.add_option( - Option('--smt-retry-limit', int, 'smt_retry_limit', 'Number of times to retry SMT queries with scaling timeouts.', default=10) + Option( + '--smt-retry-limit', + int, + 'smt_retry_limit', + 'Number of times to retry SMT queries with scaling timeouts.', + default=10, + ) ) self.add_option( - Option('--smt-tactic', str, 'smt_tactic', 'Z3 tactic to use with checking satisfiability. Example: (check-sat-using-smt)', default=None) + Option( + '--smt-tactic', + str, + 'smt_tactic', + 'Z3 tactic to use with checking satisfiability. Example: (check-sat-using-smt)', + default=None, + ) ) From 4eebc14241471de36b7e2a69862326ddcbc54e51 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 3 May 2024 14:51:08 -0500 Subject: [PATCH 12/16] Implement generic add_arg --- pyk/src/pyk/cli/cli.py | 24 +++++++++++++++++++++++- 1 file changed, 23 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/cli/cli.py b/pyk/src/pyk/cli/cli.py index 419b2d8435b..b38d2305673 100644 --- a/pyk/src/pyk/cli/cli.py +++ b/pyk/src/pyk/cli/cli.py @@ -91,7 +91,29 @@ def __init__( self.set_default(default) - def add_arg(self, args: ArgumentParser) -> None: ... # TODO + def add_arg(self, args: ArgumentParser) -> None: + + params: dict[str, Any] = {} + params['dest'] = self._dest + params['type'] = self._type + if self._action is not None: + params['action'] = self._action + if self._choices is not None: + params['choices'] = self._choices + if self._const is not None: + params['const'] = self._const + if self._default is not None: + params['default'] = self._default + if self._help_str is not None: + params['help'] = self._help_str + if self._metavar is not None: + params['metavar'] = self._metavar + if self._nargs is not None: + params['nargs'] = self._nargs + if self._required is not None: + params['required'] = self._required + + args.add_argument(self._name, *(self._aliases), **params) def set_default(self, default: Any) -> None: self._default = default From 10d0dfd5e7535e74fcc9ce50c379ad27fac9ec97 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 6 May 2024 21:03:27 -0500 Subject: [PATCH 13/16] Integrate toml parsing into new system --- pyk/src/pyk/cli/cli.py | 72 ++++++++++++++++++++- pyk/src/tests/integration/ktool/test_imp.py | 3 +- 2 files changed, 71 insertions(+), 4 deletions(-) diff --git a/pyk/src/pyk/cli/cli.py b/pyk/src/pyk/cli/cli.py index b38d2305673..a35898f47a1 100644 --- a/pyk/src/pyk/cli/cli.py +++ b/pyk/src/pyk/cli/cli.py @@ -1,14 +1,22 @@ from __future__ import annotations +import logging from abc import abstractmethod from argparse import ArgumentParser +from pathlib import Path # from enum import Enum -from typing import Any, Callable, Generic, Iterable, TypeVar +from typing import Any, Callable, Final, Generic, Iterable, TypeVar + +import tomli + +from ..cli.utils import file_path T = TypeVar('T') OG = TypeVar('OG', bound='OptionsGroup') +_LOGGER: Final = logging.getLogger(__name__) + class CLI: _commands: list[Command] @@ -40,7 +48,7 @@ def get_and_exec_command(self) -> None: args = parser.parse_args() stripped_args = {key: val for (key, val) in vars(args).items() if val != 'NoDefault'} cmd = self.get_command(stripped_args) - cmd._options_group.extract(stripped_args) + cmd._options_group.extract(stripped_args, cmd.name) cmd.exec() @@ -122,6 +130,10 @@ def set_default(self, default: Any) -> None: def name(self) -> str: return self._name + @property + def toml_name(self) -> str: + return self._toml_name + @property def default(self) -> Any: return self._default @@ -157,14 +169,62 @@ def options(self) -> OG: def exec(self) -> None: ... +def parse_toml_args(args: OptionsGroup, command: str) -> dict[str, Any]: + def get_profile(toml_profile: dict[str, Any], profile_list: list[str]) -> dict[str, Any]: + if len(profile_list) == 0 or profile_list[0] not in toml_profile: + return {k: v for k, v in toml_profile.items() if type(v) is not dict} + elif len(profile_list) == 1: + return {k: v for k, v in toml_profile[profile_list[0]].items() if type(v) is not dict} + return get_profile(toml_profile[profile_list[0]], profile_list[1:]) + + toml_args = {} + if args.config_file.is_file(): + with open(args.config_file, 'rb') as config_file: + try: + toml_args = tomli.load(config_file) + except tomli.TOMLDecodeError: + _LOGGER.error( + 'Input config file is not in TOML format, ignoring the file and carrying on with the provided command line agruments' + ) + + toml_args = get_profile(toml_args[command], args.config_profile.split('.')) if command in toml_args else {} + toml_args = {args.get_toml_name_destination(k): v for k, v in toml_args.items()} + for k, v in toml_args.items(): + if k[:3] == 'no-' and (v == 'true' or v == 'false'): + del toml_args[k] + toml_args[k[3:]] = 'false' if v == 'true' else 'true' + if k == 'optimization-level': + level = toml_args[k] if toml_args[k] >= 0 else 0 + level = level if toml_args[k] <= 3 else 3 + del toml_args[k] + toml_args['-o' + str(level)] = 'true' + + return toml_args + + class OptionsGroup: _options: dict[str, Option] + config_file: Path + config_profile: str + + def __init__(self) -> None: + self.add_option( + Option('--config-file', file_path, 'config_file', 'Path to Pyk config file.', default=Path('./pyk.toml')) + ) + self.add_option( + Option('--config-profile', str, 'config_profile', 'Config profile to be used.', default='default') + ) + + def extract(self, args: dict[str, Any], command: str) -> None: + + toml_args = parse_toml_args(self, command) - def extract(self, args: dict[str, Any]) -> None: for option in self.options: if option.name in args: self.__setattr__(option.name, args[option.name]) # TODO elif option exists in TOML file, set it to the value from there + elif option.name in toml_args: + self.__setattr__(option.name, toml_args[option.name]) else: self.__setattr__(option.name, option.default) @@ -182,6 +242,12 @@ def override_default(self, option_name: str, value: T) -> None: def options(self) -> list[Option]: return list(self._options.values()) + def get_toml_name_destination(self, option_string: str) -> str: + for option in self.options: + if option.toml_name == option_string: + return option.name + raise ValueError(f'Cannot find option with toml_name {option_string}.') + # TODO remove once all implementing semantics use `CLI` system class Options: diff --git a/pyk/src/tests/integration/ktool/test_imp.py b/pyk/src/tests/integration/ktool/test_imp.py index 4aa524c6386..0a1d22cca53 100644 --- a/pyk/src/tests/integration/ktool/test_imp.py +++ b/pyk/src/tests/integration/ktool/test_imp.py @@ -177,7 +177,8 @@ def test_prove_rpc( 'spec_file': Path(spec_file), 'spec_module': spec_module, 'claim_labels': [claim_id], - } + }, + 'prove', ) proof = single( From 4ade3ff8db2389f2fbc449ac2a648c16d4813e16 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 6 May 2024 21:04:53 -0500 Subject: [PATCH 14/16] Use null object instead of string sentinel --- pyk/src/pyk/cli/cli.py | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/pyk/src/pyk/cli/cli.py b/pyk/src/pyk/cli/cli.py index a35898f47a1..64245b527f9 100644 --- a/pyk/src/pyk/cli/cli.py +++ b/pyk/src/pyk/cli/cli.py @@ -17,6 +17,8 @@ _LOGGER: Final = logging.getLogger(__name__) +NO_DEFAULT: Final = object() + class CLI: _commands: list[Command] @@ -46,7 +48,7 @@ def get_command(self, args: dict[str, Any]) -> Command: def get_and_exec_command(self) -> None: parser = self.create_argument_parser() args = parser.parse_args() - stripped_args = {key: val for (key, val) in vars(args).items() if val != 'NoDefault'} + stripped_args = {key: val for (key, val) in vars(args).items() if val != NO_DEFAULT} cmd = self.get_command(stripped_args) cmd._options_group.extract(stripped_args, cmd.name) cmd.exec() @@ -77,7 +79,7 @@ def __init__( choices: list[str] | None = None, const: Any | None = None, aliases: Iterable[str] = (), - default: Any | str = 'NoDefault', + default: Any | str = NO_DEFAULT, metavar: str | None = None, nargs: int | str | None = None, required: bool = False, From fec21ed52f9fbb3bee9d61f9e6c2b0e8e1516c9b Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 7 May 2024 17:33:49 -0500 Subject: [PATCH 15/16] pyupgrade --- pyk/src/pyk/__main__.py | 4 ++-- pyk/src/pyk/cli/cli.py | 5 ++++- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/__main__.py b/pyk/src/pyk/__main__.py index 65209d6b6e2..2358523002c 100644 --- a/pyk/src/pyk/__main__.py +++ b/pyk/src/pyk/__main__.py @@ -56,8 +56,8 @@ from .utils import check_dir_path, check_file_path, ensure_dir_path, exit_with_process_error if TYPE_CHECKING: - from collections.abc import Iterator - from typing import IO, Any, Final, Iterable + from collections.abc import Iterable, Iterator + from typing import IO, Any, Final _LOGGER: Final = logging.getLogger(__name__) diff --git a/pyk/src/pyk/cli/cli.py b/pyk/src/pyk/cli/cli.py index 64245b527f9..e763a2454df 100644 --- a/pyk/src/pyk/cli/cli.py +++ b/pyk/src/pyk/cli/cli.py @@ -6,12 +6,15 @@ from pathlib import Path # from enum import Enum -from typing import Any, Callable, Final, Generic, Iterable, TypeVar +from typing import TYPE_CHECKING, Any, Final, Generic, TypeVar import tomli from ..cli.utils import file_path +if TYPE_CHECKING: + from collections.abc import Callable, Iterable + T = TypeVar('T') OG = TypeVar('OG', bound='OptionsGroup') From 15b811d15d0787ff3ba5d8ba5c96565af902cab5 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 7 May 2024 19:20:59 -0500 Subject: [PATCH 16/16] Fix toml parsing --- pyk/src/pyk/cli/cli.py | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/pyk/src/pyk/cli/cli.py b/pyk/src/pyk/cli/cli.py index e763a2454df..fc4fb07aab9 100644 --- a/pyk/src/pyk/cli/cli.py +++ b/pyk/src/pyk/cli/cli.py @@ -135,6 +135,10 @@ def set_default(self, default: Any) -> None: def name(self) -> str: return self._name + @property + def dest(self) -> str: + return self._dest + @property def toml_name(self) -> str: return self._toml_name @@ -213,6 +217,7 @@ class OptionsGroup: config_profile: str def __init__(self) -> None: + self._options = {} self.add_option( Option('--config-file', file_path, 'config_file', 'Path to Pyk config file.', default=Path('./pyk.toml')) ) @@ -222,19 +227,27 @@ def __init__(self) -> None: def extract(self, args: dict[str, Any], command: str) -> None: + config_file = args['config_file'] if 'config_file' in args else self.option_by_name('config_file').default + self.__setattr__('config_file', config_file) + + config_profile = ( + args['config_profile'] if 'config_profile' in args else self.option_by_name('config_profile').default + ) + self.__setattr__('config_profile', config_profile) + toml_args = parse_toml_args(self, command) for option in self.options: if option.name in args: - self.__setattr__(option.name, args[option.name]) + self.__setattr__(option.dest, args[option.name]) # TODO elif option exists in TOML file, set it to the value from there elif option.name in toml_args: - self.__setattr__(option.name, toml_args[option.name]) + self.__setattr__(option.dest, toml_args[option.name]) else: - self.__setattr__(option.name, option.default) + self.__setattr__(option.dest, option.default) def add_option(self, option: Option) -> None: - self._options[option.name] = option + self._options[option.dest] = option def override_default(self, option_name: str, value: T) -> None: if not self._options[option_name].is_optional: @@ -247,6 +260,9 @@ def override_default(self, option_name: str, value: T) -> None: def options(self) -> list[Option]: return list(self._options.values()) + def option_by_name(self, name: str) -> Option: + return self._options[name] + def get_toml_name_destination(self, option_string: str) -> str: for option in self.options: if option.toml_name == option_string: