From 11afe3c8631147f88cedddb4315ba5b16a1b2b95 Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Wed, 20 Mar 2024 21:42:14 +0300 Subject: [PATCH 01/19] added toml reading options --- src/pyk/__main__.py | 67 +++++++++++++++++++++++++++++++++---------- src/pyk/cli/args.py | 69 +++++++++++++++++++++++++++++++++++++++------ src/pyk/cli/cli.py | 4 +++ src/pyk/cli/pyk.py | 61 +++++++++++++++++++++++++++++++++++++-- 4 files changed, 175 insertions(+), 26 deletions(-) diff --git a/src/pyk/__main__.py b/src/pyk/__main__.py index 6d6c5f8f9..8612a2308 100644 --- a/src/pyk/__main__.py +++ b/src/pyk/__main__.py @@ -8,11 +8,12 @@ from enum import Enum from pathlib import Path from typing import TYPE_CHECKING +import tomli from graphviz import Digraph -from .cli.args import KCLIArgs -from .cli.pyk import generate_options +from .cli.args import KCLIArgs, ConfigArgs +from .cli.pyk import generate_options, get_option_string_destination from .cli.utils import LOG_FORMAT, dir_path, file_path, loglevel from .coverage import get_rule_by_id, strip_coverage_logger from .cterm import CTerm @@ -42,6 +43,7 @@ if TYPE_CHECKING: from typing import Any, Final + from argparse import Namespace from .cli.pyk import ( CoverageOptions, @@ -74,10 +76,12 @@ def main() -> None: cli_parser = create_argument_parser() args = cli_parser.parse_args() + toml_args = parse_toml_args(args) - stripped_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) @@ -370,6 +374,7 @@ def exec_json_to_kore(options: JsonToKoreOptions) -> None: def create_argument_parser() -> ArgumentParser: k_cli_args = KCLIArgs() + config_args = ConfigArgs() pyk_args = ArgumentParser() pyk_args_command = pyk_args.add_subparsers(dest='command', required=True) @@ -377,7 +382,7 @@ def create_argument_parser() -> ArgumentParser: print_args = pyk_args_command.add_parser( 'print', help='Pretty print a term.', - parents=[k_cli_args.logging_args, k_cli_args.display_args], + parents=[k_cli_args.logging_args, k_cli_args.display_args, config_args.config_args], ) print_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') print_args.add_argument('term', type=FileType('r'), help='Input term (in format specified with --input).') @@ -389,7 +394,7 @@ def create_argument_parser() -> ArgumentParser: rpc_print_args = pyk_args_command.add_parser( 'rpc-print', help='Pretty-print an RPC request/response', - parents=[k_cli_args.logging_args], + parents=[k_cli_args.logging_args, config_args.config_args], ) rpc_print_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') rpc_print_args.add_argument( @@ -402,7 +407,7 @@ def create_argument_parser() -> ArgumentParser: rpc_kast_args = pyk_args_command.add_parser( 'rpc-kast', help='Convert an "execute" JSON RPC response to a new "execute" or "simplify" request, copying parameters from a reference request.', - parents=[k_cli_args.logging_args], + parents=[k_cli_args.logging_args, config_args.config_args], ) rpc_kast_args.add_argument( 'reference_request_file', @@ -419,7 +424,7 @@ def create_argument_parser() -> ArgumentParser: prove_legacy_args = pyk_args_command.add_parser( 'prove-legacy', help='Prove an input specification (using kprovex).', - parents=[k_cli_args.logging_args], + parents=[k_cli_args.logging_args, config_args.config_args], ) prove_legacy_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') prove_legacy_args.add_argument('main_file', type=str, help='Main file used for kompilation.') @@ -431,14 +436,14 @@ def create_argument_parser() -> ArgumentParser: kompile_args = pyk_args_command.add_parser( 'kompile', help='Kompile the K specification.', - parents=[k_cli_args.logging_args, k_cli_args.definition_args, k_cli_args.kompile_args], + parents=[k_cli_args.logging_args, k_cli_args.definition_args, k_cli_args.kompile_args, config_args.config_args], ) kompile_args.add_argument('main_file', type=str, help='File with the specification module.') run_args = pyk_args_command.add_parser( 'run', help='Run a given program using the K definition.', - parents=[k_cli_args.logging_args], + parents=[k_cli_args.logging_args, config_args.config_args], ) run_args.add_argument('pgm_file', type=str, help='File program to run in it.') run_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.') @@ -446,7 +451,7 @@ def create_argument_parser() -> ArgumentParser: prove_args = pyk_args_command.add_parser( 'prove', help='Prove an input specification (using RPC based prover).', - parents=[k_cli_args.logging_args], + parents=[k_cli_args.logging_args, config_args.config_args], ) prove_args.add_argument('spec_file', type=file_path, help='File with the specification module.') prove_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.') @@ -464,25 +469,57 @@ def create_argument_parser() -> ArgumentParser: graph_imports_args = pyk_args_command.add_parser( 'graph-imports', help='Graph the imports of a given definition.', - parents=[k_cli_args.logging_args], + parents=[k_cli_args.logging_args, config_args.config_args], ) graph_imports_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') coverage_args = pyk_args_command.add_parser( 'coverage', help='Convert coverage file to human readable log.', - parents=[k_cli_args.logging_args], + parents=[k_cli_args.logging_args, config_args.config_args], ) coverage_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') coverage_args.add_argument('coverage_file', type=FileType('r'), help='Coverage file to build log for.') coverage_args.add_argument('-o', '--output', type=FileType('w')) - pyk_args_command.add_parser('kore-to-json', help='Convert textual KORE to JSON', parents=[k_cli_args.logging_args]) + pyk_args_command.add_parser('kore-to-json', help='Convert textual KORE to JSON', parents=[k_cli_args.logging_args, config_args.config_args]) - pyk_args_command.add_parser('json-to-kore', help='Convert JSON to textual KORE', parents=[k_cli_args.logging_args]) + pyk_args_command.add_parser('json-to-kore', help='Convert JSON to textual KORE', parents=[k_cli_args.logging_args, config_args.config_args]) 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 + if __name__ == '__main__': main() diff --git a/src/pyk/cli/args.py b/src/pyk/cli/args.py index d9678e59b..3b78135b6 100644 --- a/src/pyk/cli/args.py +++ b/src/pyk/cli/args.py @@ -24,7 +24,12 @@ def default() -> dict[str, Any]: 'verbose': False, 'debug': False, } - + + @staticmethod + def from_option_string() -> dict[str, Any]: + return { + 'v': 'verbose', + } class OutputFileOptions(Options): output_file: IO[Any] @@ -38,8 +43,14 @@ def default() -> dict[str, Any]: class DefinitionOptions(Options): definition_dir: Path - - + + @staticmethod + def default() -> dict[str, Any]: + return { + 'output-definition': 'definition_dir', + 'definition': 'definition_dir', + } + class DisplayOptions(Options): minimize: bool @@ -48,7 +59,7 @@ def default() -> dict[str, Any]: return { 'minimize': True, } - + class KDefinitionOptions(Options): includes: list[str] @@ -66,7 +77,12 @@ def default() -> dict[str, Any]: 'md_selector': 'k', 'includes': [], } - + + @staticmethod + def from_option_string() -> dict[str, str]: + return { + 'includes': 'includes', + } class SaveDirOptions(Options): save_directory: Path | None @@ -77,7 +93,6 @@ def default() -> dict[str, Any]: 'save_directory': None, } - class SpecOptions(SaveDirOptions): spec_file: Path claim_labels: list[str] | None @@ -89,7 +104,13 @@ def default() -> dict[str, Any]: 'claim_labels': None, 'exclude_claim_labels': [], } - + + @staticmethod + def from_option_string() -> dict[str, str]: + return SaveDirOptions.from_option_string() | { + 'claim': 'claim_labels', + 'exclude-claim': 'exclude_claim_labels', + } class KompileOptions(Options): emit_json: bool @@ -133,7 +154,14 @@ def default() -> dict[str, Any]: 'gen_glr_bison_parser': False, 'bison_lists': False, } - + + @staticmethod + def from_option_string() -> dict[str, str]: + return { + 'with-llvm-library': 'llvm_library', + 'read-only-kompiled-directory': 'read_only', + 'ccopt': 'ccopts', + } class ParallelOptions(Options): workers: int @@ -144,6 +172,11 @@ def default() -> dict[str, Any]: 'workers': 1, } + @staticmethod + def from_option_string() -> dict[str, str]: + return { + 'j': 'workers', + } class BugReportOptions(Options): bug_report: BugReport | None @@ -166,7 +199,25 @@ def default() -> dict[str, Any]: 'smt_tactic': None, } - +class ConfigArgs: + @cached_property + def config_args(self) -> ArgumentParser: + args = ArgumentParser(add_help=False) + args.add_argument( + '--config-file', + dest='config_file', + type=file_path, + default=Path('./pyk.toml'), + help='Path to Pyk config file.', + ) + args.add_argument( + '--config-profile', + dest='config_profile', + default='default', + help='Config profile to be used.', + ) + return args + class KCLIArgs: @cached_property def logging_args(self) -> ArgumentParser: diff --git a/src/pyk/cli/cli.py b/src/pyk/cli/cli.py index cf0cf66ae..39fc1481f 100644 --- a/src/pyk/cli/cli.py +++ b/src/pyk/cli/cli.py @@ -16,3 +16,7 @@ def __init__(self, args: dict[str, Any]) -> None: for attr, val in _args.items(): self.__setattr__(attr, val) + + @staticmethod + def from_option_string() -> dict[str, str]: + return {} \ No newline at end of file diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index 41d66cccc..a3fceae79 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -50,6 +50,38 @@ def generate_options(args: dict[str, Any]) -> LoggingOptions: 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): KORE_JSON = 'kore-json' KAST_JSON = 'kast-json' @@ -65,20 +97,31 @@ 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 GraphImportsOptions(DefinitionOptions, LoggingOptions): - ... + @staticmethod + 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] @@ -95,6 +138,9 @@ def default() -> dict[str, Any]: '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): main_file: Path @@ -107,6 +153,10 @@ 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, KDefinitionOptions, KompileOptions): @@ -123,6 +173,9 @@ def default() -> dict[str, Any]: '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): spec_file: Path @@ -140,6 +193,10 @@ def default() -> dict[str, Any]: 'failure_info': 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): pgm_file: str From 283a1c6120e9dbf45fe28cf6eef4e3c2e3ae9120 Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Wed, 20 Mar 2024 21:43:59 +0300 Subject: [PATCH 02/19] format fixes --- src/pyk/__main__.py | 43 ++++++++++++++++++++-------------- src/pyk/cli/args.py | 25 +++++++++++++------- src/pyk/cli/cli.py | 2 +- src/pyk/cli/pyk.py | 57 +++++++++++++++++++++++++++++++++++---------- 4 files changed, 88 insertions(+), 39 deletions(-) diff --git a/src/pyk/__main__.py b/src/pyk/__main__.py index 8612a2308..4702c10e3 100644 --- a/src/pyk/__main__.py +++ b/src/pyk/__main__.py @@ -8,11 +8,11 @@ from enum import Enum from pathlib import Path from typing import TYPE_CHECKING -import tomli +import tomli from graphviz import Digraph -from .cli.args import KCLIArgs, ConfigArgs +from .cli.args import ConfigArgs, KCLIArgs from .cli.pyk import generate_options, get_option_string_destination from .cli.utils import LOG_FORMAT, dir_path, file_path, loglevel from .coverage import get_rule_by_id, strip_coverage_logger @@ -42,8 +42,8 @@ from .utils import check_file_path, ensure_dir_path if TYPE_CHECKING: - from typing import Any, Final from argparse import Namespace + from typing import Any, Final from .cli.pyk import ( CoverageOptions, @@ -80,8 +80,8 @@ def main() -> None: 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) @@ -482,9 +482,13 @@ def create_argument_parser() -> ArgumentParser: coverage_args.add_argument('coverage_file', type=FileType('r'), help='Coverage file to build log for.') coverage_args.add_argument('-o', '--output', type=FileType('w')) - pyk_args_command.add_parser('kore-to-json', help='Convert textual KORE to JSON', parents=[k_cli_args.logging_args, config_args.config_args]) + pyk_args_command.add_parser( + 'kore-to-json', help='Convert textual KORE to JSON', parents=[k_cli_args.logging_args, config_args.config_args] + ) - pyk_args_command.add_parser('json-to-kore', help='Convert JSON to textual KORE', parents=[k_cli_args.logging_args, config_args.config_args]) + pyk_args_command.add_parser( + 'json-to-kore', help='Convert JSON to textual KORE', parents=[k_cli_args.logging_args, config_args.config_args] + ) return pyk_args @@ -492,11 +496,11 @@ def create_argument_parser() -> ArgumentParser: 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} + 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 {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: @@ -507,19 +511,22 @@ def get_profile(toml_profile: dict[str, Any], profile_list: list[str]) -> dict[s '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"): + 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": + 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" - + toml_args['-O' + str(level)] = 'true' + return toml_args + if __name__ == '__main__': main() diff --git a/src/pyk/cli/args.py b/src/pyk/cli/args.py index 3b78135b6..5410d5303 100644 --- a/src/pyk/cli/args.py +++ b/src/pyk/cli/args.py @@ -24,13 +24,14 @@ def default() -> dict[str, Any]: 'verbose': False, 'debug': False, } - + @staticmethod def from_option_string() -> dict[str, Any]: return { 'v': 'verbose', } + class OutputFileOptions(Options): output_file: IO[Any] @@ -43,14 +44,15 @@ def default() -> dict[str, Any]: class DefinitionOptions(Options): definition_dir: Path - + @staticmethod def default() -> dict[str, Any]: return { 'output-definition': 'definition_dir', 'definition': 'definition_dir', } - + + class DisplayOptions(Options): minimize: bool @@ -59,7 +61,7 @@ def default() -> dict[str, Any]: return { 'minimize': True, } - + class KDefinitionOptions(Options): includes: list[str] @@ -77,13 +79,14 @@ def default() -> dict[str, Any]: 'md_selector': 'k', 'includes': [], } - + @staticmethod def from_option_string() -> dict[str, str]: return { 'includes': 'includes', } + class SaveDirOptions(Options): save_directory: Path | None @@ -93,6 +96,7 @@ def default() -> dict[str, Any]: 'save_directory': None, } + class SpecOptions(SaveDirOptions): spec_file: Path claim_labels: list[str] | None @@ -104,7 +108,7 @@ def default() -> dict[str, Any]: 'claim_labels': None, 'exclude_claim_labels': [], } - + @staticmethod def from_option_string() -> dict[str, str]: return SaveDirOptions.from_option_string() | { @@ -112,6 +116,7 @@ def from_option_string() -> dict[str, str]: 'exclude-claim': 'exclude_claim_labels', } + class KompileOptions(Options): emit_json: bool llvm_kompile: bool @@ -154,7 +159,7 @@ def default() -> dict[str, Any]: 'gen_glr_bison_parser': False, 'bison_lists': False, } - + @staticmethod def from_option_string() -> dict[str, str]: return { @@ -163,6 +168,7 @@ def from_option_string() -> dict[str, str]: 'ccopt': 'ccopts', } + class ParallelOptions(Options): workers: int @@ -178,6 +184,7 @@ def from_option_string() -> dict[str, str]: 'j': 'workers', } + class BugReportOptions(Options): bug_report: BugReport | None @@ -199,6 +206,7 @@ def default() -> dict[str, Any]: 'smt_tactic': None, } + class ConfigArgs: @cached_property def config_args(self) -> ArgumentParser: @@ -217,7 +225,8 @@ def config_args(self) -> ArgumentParser: help='Config profile to be used.', ) return args - + + class KCLIArgs: @cached_property def logging_args(self) -> ArgumentParser: diff --git a/src/pyk/cli/cli.py b/src/pyk/cli/cli.py index 39fc1481f..c606824d5 100644 --- a/src/pyk/cli/cli.py +++ b/src/pyk/cli/cli.py @@ -19,4 +19,4 @@ def __init__(self, args: dict[str, Any]) -> None: @staticmethod def from_option_string() -> dict[str, str]: - return {} \ No newline at end of file + return {} diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index a3fceae79..6ee9e9c3b 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -78,8 +78,8 @@ def get_option_string_destination(command: str, option_string: str) -> str: if option_string in option_string_destinations: return option_string_destinations[option_string] - else: - return option_string.replace('-','_') + else: + return option_string.replace('-', '_') class PrintInput(Enum): @@ -97,15 +97,20 @@ 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() + return ( + DefinitionOptions.from_option_string() + | OutputFileOptions.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() + return DefinitionOptions.from_option_string() | LoggingOptions.from_option_string() class RPCKastOptions(OutputFileOptions, LoggingOptions): @@ -114,14 +119,20 @@ class RPCKastOptions(OutputFileOptions, LoggingOptions): @staticmethod def from_option_string() -> dict[str, str]: - return OutputFileOptions.from_option_string() | LoggingOptions.from_option_string() + 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() + return ( + DefinitionOptions.from_option_string() + | OutputFileOptions.from_option_string() + | LoggingOptions.from_option_string() + ) + class PrintOptions(DefinitionOptions, OutputFileOptions, DisplayOptions, LoggingOptions): term: IO[Any] @@ -140,7 +151,13 @@ def default() -> dict[str, Any]: @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() + return ( + DefinitionOptions.from_option_string() + | OutputFileOptions.from_option_string() + | DisplayOptions.from_option_string() + | LoggingOptions.from_option_string() + ) + class ProveLegacyOptions(DefinitionOptions, OutputFileOptions, LoggingOptions): main_file: Path @@ -153,10 +170,15 @@ 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'} + return ( + DefinitionOptions.from_option_string() + | OutputFileOptions.from_option_string() + | LoggingOptions.from_option_string() + | {'kArgs': 'k_args'} + ) class KompileCommandOptions(LoggingOptions, KDefinitionOptions, KompileOptions): @@ -175,7 +197,13 @@ def default() -> dict[str, Any]: @staticmethod def from_option_string() -> dict[str, str]: - return KDefinitionOptions.from_option_string() | KompileOptions.from_option_string() | LoggingOptions.from_option_string() | {'definition': 'definition_dir'} + return ( + KDefinitionOptions.from_option_string() + | KompileOptions.from_option_string() + | LoggingOptions.from_option_string() + | {'definition': 'definition_dir'} + ) + class ProveOptions(LoggingOptions): spec_file: Path @@ -195,7 +223,12 @@ def default() -> dict[str, Any]: @staticmethod def from_option_string() -> dict[str, str]: - return KDefinitionOptions.from_option_string() | KompileOptions.from_option_string() | LoggingOptions.from_option_string() | {'definition': 'definition_dir'} + return ( + KDefinitionOptions.from_option_string() + | KompileOptions.from_option_string() + | LoggingOptions.from_option_string() + | {'definition': 'definition_dir'} + ) class RunOptions(LoggingOptions): From 70d7aa52414410b7032b1773f77634a19d92f310 Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Wed, 20 Mar 2024 22:37:41 +0300 Subject: [PATCH 03/19] reorganized and added unit tests --- src/pyk/__main__.py | 171 +------------------- src/pyk/cli/args.py | 4 + src/pyk/cli/pyk.py | 169 ++++++++++++++++++- src/tests/unit/test-data/pyk_toml_test.toml | 6 + src/tests/unit/test_toml_args.py | 55 +++++++ 5 files changed, 235 insertions(+), 170 deletions(-) create mode 100644 src/tests/unit/test-data/pyk_toml_test.toml create mode 100644 src/tests/unit/test_toml_args.py diff --git a/src/pyk/__main__.py b/src/pyk/__main__.py index 4702c10e3..4e3a4bb5b 100644 --- a/src/pyk/__main__.py +++ b/src/pyk/__main__.py @@ -3,18 +3,14 @@ import json import logging import sys -from argparse import ArgumentParser, FileType from collections.abc import Iterable -from enum import Enum from pathlib import Path from typing import TYPE_CHECKING -import tomli from graphviz import Digraph -from .cli.args import ConfigArgs, KCLIArgs -from .cli.pyk import generate_options, get_option_string_destination -from .cli.utils import LOG_FORMAT, dir_path, file_path, loglevel +from .cli.pyk import PrintInput, create_argument_parser, generate_options, parse_toml_args +from .cli.utils import LOG_FORMAT, loglevel from .coverage import get_rule_by_id, strip_coverage_logger from .cterm import CTerm from .kast.inner import KInner @@ -31,7 +27,6 @@ from .kore.parser import KoreParser from .kore.rpc import ExecuteResult, StopReason from .kore.syntax import Pattern, kore_term -from .ktool import TypeInferenceMode from .ktool.kompile import Kompile, KompileBackend from .ktool.kprint import KPrint from .ktool.kprove import KProve @@ -42,7 +37,6 @@ from .utils import check_file_path, ensure_dir_path if TYPE_CHECKING: - from argparse import Namespace from typing import Any, Final from .cli.pyk import ( @@ -63,11 +57,6 @@ _LOGGER: Final = logging.getLogger(__name__) -class PrintInput(Enum): - KORE_JSON = 'kore-json' - KAST_JSON = 'kast-json' - - def main() -> None: # KAST terms can end up nested quite deeply, because of the various assoc operators (eg. _Map_, _Set_, ...). # Most pyk operations are defined recursively, meaning you get a callstack the same depth as the term. @@ -372,161 +361,5 @@ def exec_json_to_kore(options: JsonToKoreOptions) -> None: sys.stdout.write('\n') -def create_argument_parser() -> ArgumentParser: - k_cli_args = KCLIArgs() - config_args = ConfigArgs() - - pyk_args = ArgumentParser() - pyk_args_command = pyk_args.add_subparsers(dest='command', required=True) - - print_args = pyk_args_command.add_parser( - 'print', - help='Pretty print a term.', - parents=[k_cli_args.logging_args, k_cli_args.display_args, config_args.config_args], - ) - print_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') - print_args.add_argument('term', type=FileType('r'), help='Input term (in format specified with --input).') - print_args.add_argument('--input', type=PrintInput, choices=list(PrintInput)) - print_args.add_argument('--omit-labels', nargs='?', help='List of labels to omit from output.') - print_args.add_argument('--keep-cells', nargs='?', help='List of cells with primitive values to keep in output.') - print_args.add_argument('--output-file', type=FileType('w')) - - rpc_print_args = pyk_args_command.add_parser( - 'rpc-print', - help='Pretty-print an RPC request/response', - parents=[k_cli_args.logging_args, config_args.config_args], - ) - rpc_print_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') - rpc_print_args.add_argument( - 'input_file', - type=FileType('r'), - help='An input file containing the JSON RPC request or response with KoreJSON payload.', - ) - rpc_print_args.add_argument('--output-file', type=FileType('w')) - - rpc_kast_args = pyk_args_command.add_parser( - 'rpc-kast', - help='Convert an "execute" JSON RPC response to a new "execute" or "simplify" request, copying parameters from a reference request.', - parents=[k_cli_args.logging_args, config_args.config_args], - ) - rpc_kast_args.add_argument( - 'reference_request_file', - type=FileType('r'), - help='An input file containing a JSON RPC request to server as a reference for the new request.', - ) - rpc_kast_args.add_argument( - 'response_file', - type=FileType('r'), - help='An input file containing a JSON RPC response with KoreJSON payload.', - ) - rpc_kast_args.add_argument('--output-file', type=FileType('w')) - - prove_legacy_args = pyk_args_command.add_parser( - 'prove-legacy', - help='Prove an input specification (using kprovex).', - parents=[k_cli_args.logging_args, config_args.config_args], - ) - prove_legacy_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') - prove_legacy_args.add_argument('main_file', type=str, help='Main file used for kompilation.') - prove_legacy_args.add_argument('spec_file', type=str, help='File with the specification module.') - prove_legacy_args.add_argument('spec_module', type=str, help='Module with claims to be proven.') - prove_legacy_args.add_argument('--output-file', type=FileType('w')) - prove_legacy_args.add_argument('kArgs', nargs='*', help='Arguments to pass through to K invocation.') - - kompile_args = pyk_args_command.add_parser( - 'kompile', - help='Kompile the K specification.', - parents=[k_cli_args.logging_args, k_cli_args.definition_args, k_cli_args.kompile_args, config_args.config_args], - ) - kompile_args.add_argument('main_file', type=str, help='File with the specification module.') - - run_args = pyk_args_command.add_parser( - 'run', - help='Run a given program using the K definition.', - parents=[k_cli_args.logging_args, config_args.config_args], - ) - run_args.add_argument('pgm_file', type=str, help='File program to run in it.') - run_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.') - - prove_args = pyk_args_command.add_parser( - 'prove', - help='Prove an input specification (using RPC based prover).', - parents=[k_cli_args.logging_args, config_args.config_args], - ) - prove_args.add_argument('spec_file', type=file_path, help='File with the specification module.') - prove_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.') - prove_args.add_argument('--spec-module', dest='spec_module', type=str, help='Module with claims to be proven.') - prove_args.add_argument( - '--type-inference-mode', type=TypeInferenceMode, help='Mode for doing K rule type inference in.' - ) - prove_args.add_argument( - '--failure-info', - default=None, - action='store_true', - help='Print out more information about proof failures.', - ) - - graph_imports_args = pyk_args_command.add_parser( - 'graph-imports', - help='Graph the imports of a given definition.', - parents=[k_cli_args.logging_args, config_args.config_args], - ) - graph_imports_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') - - coverage_args = pyk_args_command.add_parser( - 'coverage', - help='Convert coverage file to human readable log.', - parents=[k_cli_args.logging_args, config_args.config_args], - ) - coverage_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') - coverage_args.add_argument('coverage_file', type=FileType('r'), help='Coverage file to build log for.') - coverage_args.add_argument('-o', '--output', type=FileType('w')) - - pyk_args_command.add_parser( - 'kore-to-json', help='Convert textual KORE to JSON', parents=[k_cli_args.logging_args, config_args.config_args] - ) - - pyk_args_command.add_parser( - 'json-to-kore', help='Convert JSON to textual KORE', parents=[k_cli_args.logging_args, config_args.config_args] - ) - - 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 - - if __name__ == '__main__': main() diff --git a/src/pyk/cli/args.py b/src/pyk/cli/args.py index 5410d5303..6bfcbaeb3 100644 --- a/src/pyk/cli/args.py +++ b/src/pyk/cli/args.py @@ -166,6 +166,10 @@ def from_option_string() -> dict[str, str]: 'with-llvm-library': 'llvm_library', 'read-only-kompiled-directory': 'read_only', 'ccopt': 'ccopts', + 'O0': 'o0', + 'O1': 'o1', + 'O2': 'o2', + 'O3': 'o3', } diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index 6ee9e9c3b..bb7c76628 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -1,24 +1,35 @@ from __future__ import annotations +import logging +from argparse import ArgumentParser, FileType from enum import Enum from typing import IO, TYPE_CHECKING, Any +import tomli + from pyk.ktool.kompile import KompileBackend +from ..ktool import TypeInferenceMode from .args import ( + ConfigArgs, DefinitionOptions, DisplayOptions, + KCLIArgs, KDefinitionOptions, KompileOptions, LoggingOptions, OutputFileOptions, ) +from .utils import dir_path, file_path if TYPE_CHECKING: + from argparse import Namespace from collections.abc import Iterable from pathlib import Path + from typing import Final + - from pyk.ktool import TypeInferenceMode +_LOGGER: Final = logging.getLogger(__name__) def generate_options(args: dict[str, Any]) -> LoggingOptions: @@ -240,3 +251,159 @@ def default() -> dict[str, Any]: return { 'definition_dir': None, } + + +def create_argument_parser() -> ArgumentParser: + k_cli_args = KCLIArgs() + config_args = ConfigArgs() + + pyk_args = ArgumentParser() + pyk_args_command = pyk_args.add_subparsers(dest='command', required=True) + + print_args = pyk_args_command.add_parser( + 'print', + help='Pretty print a term.', + parents=[k_cli_args.logging_args, k_cli_args.display_args, config_args.config_args], + ) + print_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') + print_args.add_argument('term', type=FileType('r'), help='Input term (in format specified with --input).') + print_args.add_argument('--input', type=PrintInput, choices=list(PrintInput)) + print_args.add_argument('--omit-labels', nargs='?', help='List of labels to omit from output.') + print_args.add_argument('--keep-cells', nargs='?', help='List of cells with primitive values to keep in output.') + print_args.add_argument('--output-file', type=FileType('w')) + + rpc_print_args = pyk_args_command.add_parser( + 'rpc-print', + help='Pretty-print an RPC request/response', + parents=[k_cli_args.logging_args, config_args.config_args], + ) + rpc_print_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') + rpc_print_args.add_argument( + 'input_file', + type=FileType('r'), + help='An input file containing the JSON RPC request or response with KoreJSON payload.', + ) + rpc_print_args.add_argument('--output-file', type=FileType('w')) + + rpc_kast_args = pyk_args_command.add_parser( + 'rpc-kast', + help='Convert an "execute" JSON RPC response to a new "execute" or "simplify" request, copying parameters from a reference request.', + parents=[k_cli_args.logging_args, config_args.config_args], + ) + rpc_kast_args.add_argument( + 'reference_request_file', + type=FileType('r'), + help='An input file containing a JSON RPC request to server as a reference for the new request.', + ) + rpc_kast_args.add_argument( + 'response_file', + type=FileType('r'), + help='An input file containing a JSON RPC response with KoreJSON payload.', + ) + rpc_kast_args.add_argument('--output-file', type=FileType('w')) + + prove_legacy_args = pyk_args_command.add_parser( + 'prove-legacy', + help='Prove an input specification (using kprovex).', + parents=[k_cli_args.logging_args, config_args.config_args], + ) + prove_legacy_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') + prove_legacy_args.add_argument('main_file', type=str, help='Main file used for kompilation.') + prove_legacy_args.add_argument('spec_file', type=str, help='File with the specification module.') + prove_legacy_args.add_argument('spec_module', type=str, help='Module with claims to be proven.') + prove_legacy_args.add_argument('--output-file', type=FileType('w')) + prove_legacy_args.add_argument('kArgs', nargs='*', help='Arguments to pass through to K invocation.') + + kompile_args = pyk_args_command.add_parser( + 'kompile', + help='Kompile the K specification.', + parents=[k_cli_args.logging_args, k_cli_args.definition_args, k_cli_args.kompile_args, config_args.config_args], + ) + kompile_args.add_argument('main_file', type=str, help='File with the specification module.') + + run_args = pyk_args_command.add_parser( + 'run', + help='Run a given program using the K definition.', + parents=[k_cli_args.logging_args, config_args.config_args], + ) + run_args.add_argument('pgm_file', type=str, help='File program to run in it.') + run_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.') + + prove_args = pyk_args_command.add_parser( + 'prove', + help='Prove an input specification (using RPC based prover).', + parents=[k_cli_args.logging_args, config_args.config_args], + ) + prove_args.add_argument('spec_file', type=file_path, help='File with the specification module.') + prove_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.') + prove_args.add_argument('--spec-module', dest='spec_module', type=str, help='Module with claims to be proven.') + prove_args.add_argument( + '--type-inference-mode', type=TypeInferenceMode, help='Mode for doing K rule type inference in.' + ) + prove_args.add_argument( + '--failure-info', + default=None, + action='store_true', + help='Print out more information about proof failures.', + ) + + graph_imports_args = pyk_args_command.add_parser( + 'graph-imports', + help='Graph the imports of a given definition.', + parents=[k_cli_args.logging_args, config_args.config_args], + ) + graph_imports_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') + + coverage_args = pyk_args_command.add_parser( + 'coverage', + help='Convert coverage file to human readable log.', + parents=[k_cli_args.logging_args, config_args.config_args], + ) + coverage_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') + coverage_args.add_argument('coverage_file', type=FileType('r'), help='Coverage file to build log for.') + coverage_args.add_argument('-o', '--output', type=FileType('w')) + + pyk_args_command.add_parser( + 'kore-to-json', help='Convert textual KORE to JSON', parents=[k_cli_args.logging_args, config_args.config_args] + ) + + pyk_args_command.add_parser( + 'json-to-kore', help='Convert JSON to textual KORE', parents=[k_cli_args.logging_args, config_args.config_args] + ) + + 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 diff --git a/src/tests/unit/test-data/pyk_toml_test.toml b/src/tests/unit/test-data/pyk_toml_test.toml new file mode 100644 index 000000000..8e90f7b25 --- /dev/null +++ b/src/tests/unit/test-data/pyk_toml_test.toml @@ -0,0 +1,6 @@ +[coverage] +output = "default-file" + +[coverage.a_profile] +verbose = true +output = "a-profile-file" \ No newline at end of file diff --git a/src/tests/unit/test_toml_args.py b/src/tests/unit/test_toml_args.py new file mode 100644 index 000000000..2f10fbc5a --- /dev/null +++ b/src/tests/unit/test_toml_args.py @@ -0,0 +1,55 @@ +from __future__ import annotations + +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: + from typing import Final + +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' From 455705ea0f89d078f630a578e56cc63967091ce3 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 20 Mar 2024 19:42:31 +0000 Subject: [PATCH 04/19] Set Version: 0.1.729 --- docs/conf.py | 4 ++-- package/version | 2 +- pyproject.toml | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/conf.py b/docs/conf.py index 588126e27..ce29745ba 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '0.1.728' -release = '0.1.728' +version = '0.1.729' +release = '0.1.729' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/package/version b/package/version index b3469fa7a..316cde771 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.728 +0.1.729 diff --git a/pyproject.toml b/pyproject.toml index b3b5db3b7..29e32b509 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.728" +version = "0.1.729" description = "" authors = [ "Runtime Verification, Inc. ", From c4da86eab85005935a9da2c4d636696c9c060d0e Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Wed, 20 Mar 2024 22:53:35 +0300 Subject: [PATCH 05/19] fixed import sorting --- src/pyk/cli/pyk.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index dd027007a..0ce06a5ec 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -7,8 +7,8 @@ import tomli -from ..ktool.kompile import KompileBackend from ..ktool import TypeInferenceMode +from ..ktool.kompile import KompileBackend from .args import ( ConfigArgs, DefinitionOptions, From c2699538fb16d722a6e0a91d605f6d0b75c5e37a Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Thu, 21 Mar 2024 09:29:36 +0300 Subject: [PATCH 06/19] fixed missing warning_args parent --- src/pyk/cli/args.py | 8 +++++++- src/pyk/cli/pyk.py | 2 +- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/pyk/cli/args.py b/src/pyk/cli/args.py index a0e43298d..6eaf3bb82 100644 --- a/src/pyk/cli/args.py +++ b/src/pyk/cli/args.py @@ -42,7 +42,13 @@ def default() -> dict[str, Any]: 'warnings': None, 'warning_to_error': False, } - + + @staticmethod + def from_option_string() -> dict[str, Any]: + return { + 'w': 'warnings', + 'w2e': 'warning_to_error', + } class OutputFileOptions(Options): output_file: IO[Any] diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index 0ce06a5ec..48131818c 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -317,7 +317,7 @@ def create_argument_parser() -> ArgumentParser: kompile_args = pyk_args_command.add_parser( 'kompile', help='Kompile the K specification.', - parents=[k_cli_args.logging_args, k_cli_args.definition_args, k_cli_args.kompile_args, config_args.config_args], + parents=[k_cli_args.logging_args, k_cli_args.warning_args, k_cli_args.definition_args, k_cli_args.kompile_args, config_args.config_args], ) kompile_args.add_argument('main_file', type=str, help='File with the specification module.') From 1bebb3d11b7564f4313582cc6688d961d9ffded2 Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Thu, 21 Mar 2024 09:57:29 +0300 Subject: [PATCH 07/19] code formatting fixes --- src/pyk/cli/args.py | 3 ++- src/pyk/cli/pyk.py | 8 +++++++- 2 files changed, 9 insertions(+), 2 deletions(-) diff --git a/src/pyk/cli/args.py b/src/pyk/cli/args.py index 6eaf3bb82..a062542d9 100644 --- a/src/pyk/cli/args.py +++ b/src/pyk/cli/args.py @@ -42,7 +42,7 @@ def default() -> dict[str, Any]: 'warnings': None, 'warning_to_error': False, } - + @staticmethod def from_option_string() -> dict[str, Any]: return { @@ -50,6 +50,7 @@ def from_option_string() -> dict[str, Any]: 'w2e': 'warning_to_error', } + class OutputFileOptions(Options): output_file: IO[Any] diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index 48131818c..2df1ea0ff 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -317,7 +317,13 @@ def create_argument_parser() -> ArgumentParser: kompile_args = pyk_args_command.add_parser( 'kompile', help='Kompile the K specification.', - parents=[k_cli_args.logging_args, k_cli_args.warning_args, k_cli_args.definition_args, k_cli_args.kompile_args, config_args.config_args], + parents=[ + k_cli_args.logging_args, + k_cli_args.warning_args, + k_cli_args.definition_args, + k_cli_args.kompile_args, + config_args.config_args, + ], ) kompile_args.add_argument('main_file', type=str, help='File with the specification module.') From b6f40d1cbc3400f343a86294bcf1fad77062b147 Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Thu, 21 Mar 2024 10:10:33 +0300 Subject: [PATCH 08/19] removed config args form legacy commands --- src/pyk/cli/pyk.py | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index 2df1ea0ff..73cd04d9f 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -275,7 +275,7 @@ def create_argument_parser() -> ArgumentParser: rpc_print_args = pyk_args_command.add_parser( 'rpc-print', help='Pretty-print an RPC request/response', - parents=[k_cli_args.logging_args, config_args.config_args], + parents=[k_cli_args.logging_args], ) rpc_print_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') rpc_print_args.add_argument( @@ -288,7 +288,7 @@ def create_argument_parser() -> ArgumentParser: rpc_kast_args = pyk_args_command.add_parser( 'rpc-kast', help='Convert an "execute" JSON RPC response to a new "execute" or "simplify" request, copying parameters from a reference request.', - parents=[k_cli_args.logging_args, config_args.config_args], + parents=[k_cli_args.logging_args], ) rpc_kast_args.add_argument( 'reference_request_file', @@ -305,7 +305,7 @@ def create_argument_parser() -> ArgumentParser: prove_legacy_args = pyk_args_command.add_parser( 'prove-legacy', help='Prove an input specification (using kprovex).', - parents=[k_cli_args.logging_args, config_args.config_args], + parents=[k_cli_args.logging_args], ) prove_legacy_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') prove_legacy_args.add_argument('main_file', type=str, help='Main file used for kompilation.') @@ -322,7 +322,6 @@ def create_argument_parser() -> ArgumentParser: k_cli_args.warning_args, k_cli_args.definition_args, k_cli_args.kompile_args, - config_args.config_args, ], ) kompile_args.add_argument('main_file', type=str, help='File with the specification module.') @@ -330,7 +329,7 @@ def create_argument_parser() -> ArgumentParser: run_args = pyk_args_command.add_parser( 'run', help='Run a given program using the K definition.', - parents=[k_cli_args.logging_args, config_args.config_args], + parents=[k_cli_args.logging_args], ) run_args.add_argument('pgm_file', type=str, help='File program to run in it.') run_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.') From ac3f2a81133de265d7767eb1890561d9ae339e82 Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Thu, 21 Mar 2024 10:18:47 +0300 Subject: [PATCH 09/19] handles missing config_file attribute --- src/pyk/cli/pyk.py | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index 73cd04d9f..d2c82bf87 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -388,14 +388,16 @@ def get_profile(toml_profile: dict[str, Any], profile_list: list[str]) -> dict[s 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' - ) + if not hasattr(args, 'config_file') or not args.config_file.is_file(): + return {} + + 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 {} From a0fdff234e72a442a25544306759beb997362742 Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Mon, 25 Mar 2024 10:30:55 +0300 Subject: [PATCH 10/19] fixed underscore error --- src/pyk/cli/pyk.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index d2c82bf87..fcc035efa 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -404,7 +404,7 @@ def get_profile(toml_profile: dict[str, Any], profile_list: list[str]) -> dict[s ) 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'): + 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': From 8fa6a252e252ef63bb0134853ab2a90e5fa19c15 Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Mon, 25 Mar 2024 10:43:15 +0300 Subject: [PATCH 11/19] toml dict key fix --- src/pyk/cli/pyk.py | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index fcc035efa..eb0a771ee 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -402,15 +402,17 @@ def get_profile(toml_profile: dict[str, Any], profile_list: list[str]) -> dict[s 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()} + + toml_adj_args = {} 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': + opt_string = get_option_string_destination(args.command, k) + if opt_string[:3] == 'no_': + toml_adj_args[opt_string[3:]] = not v + elif 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' + toml_adj_args['-o' + str(level)] = True + else: + toml_adj_args[opt_string] = v - return toml_args + return toml_adj_args From 288921398be2602ebd7e152926b28bd2cca73b08 Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Mon, 25 Mar 2024 11:12:22 +0300 Subject: [PATCH 12/19] toml parser typing fix --- src/pyk/cli/pyk.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index eb0a771ee..6c8d480cb 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -379,7 +379,7 @@ def create_argument_parser() -> ArgumentParser: return pyk_args -def parse_toml_args(args: Namespace) -> dict[str, Any | Iterable]: +def parse_toml_args(args: Namespace) -> 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} @@ -387,7 +387,7 @@ def get_profile(toml_profile: dict[str, Any], profile_list: list[str]) -> dict[s 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 = {} + toml_args: dict[str, Any] = {} if not hasattr(args, 'config_file') or not args.config_file.is_file(): return {} @@ -402,8 +402,8 @@ def get_profile(toml_profile: dict[str, Any], profile_list: list[str]) -> dict[s toml_args = ( get_profile(toml_args[args.command], args.config_profile.split('.')) if args.command in toml_args else {} ) - - toml_adj_args = {} + + toml_adj_args: dict[str, Any] = {} for k, v in toml_args.items(): opt_string = get_option_string_destination(args.command, k) if opt_string[:3] == 'no_': From 49625b8222ad7bde9a9c2831bcab8877509144c2 Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 25 Mar 2024 08:27:59 +0000 Subject: [PATCH 13/19] Set Version: 0.1.732 --- docs/conf.py | 4 ++-- package/version | 2 +- pyproject.toml | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/conf.py b/docs/conf.py index 0a08f9f11..1df5fa332 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '0.1.731' -release = '0.1.731' +version = '0.1.732' +release = '0.1.732' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/package/version b/package/version index 2cfc82abf..28520fbd5 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.731 +0.1.732 diff --git a/pyproject.toml b/pyproject.toml index 969fea78b..29ff940c7 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.731" +version = "0.1.732" description = "" authors = [ "Runtime Verification, Inc. ", From cb898af99bc28772bc23e4137addf68d13b8f122 Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Mon, 25 Mar 2024 22:38:28 +0300 Subject: [PATCH 14/19] removed redundant agrument in test --- src/tests/unit/test_toml_args.py | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/src/tests/unit/test_toml_args.py b/src/tests/unit/test_toml_args.py index 2f10fbc5a..28873e5b4 100644 --- a/src/tests/unit/test_toml_args.py +++ b/src/tests/unit/test_toml_args.py @@ -37,16 +37,7 @@ def test_toml_read() -> None: 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', - ] + cmd_args = ['coverage', '--config-file', str(TEST_TOML), '--config-profile', 'a_profile', '.', str(TEST_TOML)] args = parser.parse_args(cmd_args) args_dict = parse_toml_args(args) assert 'verbose' in args_dict From e0f61d9b9d32534a4021e916eab246558b788f2c Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 15 Apr 2024 10:46:20 +0000 Subject: [PATCH 15/19] Set Version: 0.1.780 --- docs/conf.py | 4 ++-- package/version | 2 +- pyproject.toml | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/conf.py b/docs/conf.py index 09efd2158..84a17e839 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '0.1.779' -release = '0.1.779' +version = '0.1.780' +release = '0.1.780' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/package/version b/package/version index eddad3c85..e28e46c66 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.779 +0.1.780 diff --git a/pyproject.toml b/pyproject.toml index 4469514ac..ef3d0e474 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.779" +version = "0.1.780" description = "" authors = [ "Runtime Verification, Inc. ", From 8a04dfea2c4ce2c2cfac183e7c7ff0f6f5142a26 Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Wed, 20 Mar 2024 21:42:14 +0300 Subject: [PATCH 16/19] added toml reading options --- src/pyk/__main__.py | 34 ++++++++++++++++++++++++++++++ src/pyk/cli/args.py | 3 +-- src/pyk/cli/cli.py | 2 +- src/pyk/cli/pyk.py | 50 ++++++++------------------------------------- 4 files changed, 45 insertions(+), 44 deletions(-) diff --git a/src/pyk/__main__.py b/src/pyk/__main__.py index e6809c0b0..ccc9791a7 100644 --- a/src/pyk/__main__.py +++ b/src/pyk/__main__.py @@ -6,6 +6,7 @@ from collections.abc import Iterable from pathlib import Path from typing import TYPE_CHECKING +import tomli from graphviz import Digraph @@ -38,6 +39,7 @@ if TYPE_CHECKING: from typing import Any, Final + from argparse import Namespace from .cli.pyk import ( CoverageOptions, @@ -368,5 +370,37 @@ def exec_json_to_kore(options: JsonToKoreOptions) -> None: sys.stdout.write('\n') +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 + if __name__ == '__main__': main() diff --git a/src/pyk/cli/args.py b/src/pyk/cli/args.py index e896c7bc7..2c8e12c47 100644 --- a/src/pyk/cli/args.py +++ b/src/pyk/cli/args.py @@ -80,7 +80,7 @@ def default() -> dict[str, Any]: return { 'minimize': True, } - + class KDefinitionOptions(Options): includes: list[str] @@ -115,7 +115,6 @@ def default() -> dict[str, Any]: 'save_directory': None, } - class SpecOptions(SaveDirOptions): spec_file: Path claim_labels: list[str] | None diff --git a/src/pyk/cli/cli.py b/src/pyk/cli/cli.py index c606824d5..39fc1481f 100644 --- a/src/pyk/cli/cli.py +++ b/src/pyk/cli/cli.py @@ -19,4 +19,4 @@ def __init__(self, args: dict[str, Any]) -> None: @staticmethod def from_option_string() -> dict[str, str]: - return {} + return {} \ No newline at end of file diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index 3c68f0274..9cbbe2f0d 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -106,20 +106,15 @@ 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() - ) - + return DefinitionOptions.from_option_string() | OutputFileOptions.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() + return DefinitionOptions.from_option_string() | LoggingOptions.from_option_string() class RPCKastOptions(OutputFileOptions, LoggingOptions): @@ -136,12 +131,7 @@ class RPCPrintOptions(DefinitionOptions, OutputFileOptions, LoggingOptions): @staticmethod def from_option_string() -> dict[str, str]: - return ( - DefinitionOptions.from_option_string() - | OutputFileOptions.from_option_string() - | LoggingOptions.from_option_string() - ) - + return DefinitionOptions.from_option_string() | OutputFileOptions.from_option_string() | LoggingOptions.from_option_string() class PrintOptions(DefinitionOptions, OutputFileOptions, DisplayOptions, LoggingOptions): term: IO[Any] @@ -160,13 +150,7 @@ def default() -> dict[str, Any]: @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() - ) - + return DefinitionOptions.from_option_string() | OutputFileOptions.from_option_string() | DisplayOptions.from_option_string() | LoggingOptions.from_option_string() class ProveLegacyOptions(DefinitionOptions, OutputFileOptions, LoggingOptions): main_file: Path @@ -179,15 +163,10 @@ 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'} - ) + return DefinitionOptions.from_option_string() | OutputFileOptions.from_option_string() | LoggingOptions.from_option_string() | {'kArgs': 'k_args'} class KompileCommandOptions(LoggingOptions, WarningOptions, KDefinitionOptions, KompileOptions): @@ -206,13 +185,7 @@ def default() -> dict[str, Any]: @staticmethod def from_option_string() -> dict[str, str]: - return ( - KDefinitionOptions.from_option_string() - | KompileOptions.from_option_string() - | LoggingOptions.from_option_string() - | {'definition': 'definition_dir'} - ) - + return KDefinitionOptions.from_option_string() | KompileOptions.from_option_string() | LoggingOptions.from_option_string() | {'definition': 'definition_dir'} class ProveOptions(LoggingOptions): spec_file: Path @@ -232,12 +205,7 @@ def default() -> dict[str, Any]: @staticmethod def from_option_string() -> dict[str, str]: - return ( - KDefinitionOptions.from_option_string() - | KompileOptions.from_option_string() - | LoggingOptions.from_option_string() - | {'definition': 'definition_dir'} - ) + return KDefinitionOptions.from_option_string() | KompileOptions.from_option_string() | LoggingOptions.from_option_string() | {'definition': 'definition_dir'} class RunOptions(LoggingOptions): From 43694300b11d3f5d22d82b31ecbfc769f1676de3 Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Wed, 20 Mar 2024 21:43:59 +0300 Subject: [PATCH 17/19] format fixes --- src/pyk/__main__.py | 29 ++++++++++++++------------ src/pyk/cli/args.py | 3 ++- src/pyk/cli/cli.py | 2 +- src/pyk/cli/pyk.py | 50 +++++++++++++++++++++++++++++++++++++-------- 4 files changed, 60 insertions(+), 24 deletions(-) diff --git a/src/pyk/__main__.py b/src/pyk/__main__.py index ccc9791a7..5154d7d1a 100644 --- a/src/pyk/__main__.py +++ b/src/pyk/__main__.py @@ -6,8 +6,8 @@ from collections.abc import Iterable from pathlib import Path from typing import TYPE_CHECKING -import tomli +import tomli from graphviz import Digraph from .cli.pyk import PrintInput, create_argument_parser, generate_options, parse_toml_args @@ -38,8 +38,8 @@ from .utils import check_file_path, ensure_dir_path, exit_with_process_error if TYPE_CHECKING: - from typing import Any, Final from argparse import Namespace + from typing import Any, Final from .cli.pyk import ( CoverageOptions, @@ -373,11 +373,11 @@ def exec_json_to_kore(options: JsonToKoreOptions) -> None: 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} + 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 {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: @@ -388,19 +388,22 @@ def get_profile(toml_profile: dict[str, Any], profile_list: list[str]) -> dict[s '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"): + 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": + 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" - + toml_args['-O' + str(level)] = 'true' + return toml_args + if __name__ == '__main__': main() diff --git a/src/pyk/cli/args.py b/src/pyk/cli/args.py index 2c8e12c47..e896c7bc7 100644 --- a/src/pyk/cli/args.py +++ b/src/pyk/cli/args.py @@ -80,7 +80,7 @@ def default() -> dict[str, Any]: return { 'minimize': True, } - + class KDefinitionOptions(Options): includes: list[str] @@ -115,6 +115,7 @@ def default() -> dict[str, Any]: 'save_directory': None, } + class SpecOptions(SaveDirOptions): spec_file: Path claim_labels: list[str] | None diff --git a/src/pyk/cli/cli.py b/src/pyk/cli/cli.py index 39fc1481f..c606824d5 100644 --- a/src/pyk/cli/cli.py +++ b/src/pyk/cli/cli.py @@ -19,4 +19,4 @@ def __init__(self, args: dict[str, Any]) -> None: @staticmethod def from_option_string() -> dict[str, str]: - return {} \ No newline at end of file + return {} diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index 9cbbe2f0d..3c68f0274 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -106,15 +106,20 @@ 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() + return ( + DefinitionOptions.from_option_string() + | OutputFileOptions.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() + return DefinitionOptions.from_option_string() | LoggingOptions.from_option_string() class RPCKastOptions(OutputFileOptions, LoggingOptions): @@ -131,7 +136,12 @@ class RPCPrintOptions(DefinitionOptions, OutputFileOptions, LoggingOptions): @staticmethod def from_option_string() -> dict[str, str]: - return DefinitionOptions.from_option_string() | OutputFileOptions.from_option_string() | LoggingOptions.from_option_string() + return ( + DefinitionOptions.from_option_string() + | OutputFileOptions.from_option_string() + | LoggingOptions.from_option_string() + ) + class PrintOptions(DefinitionOptions, OutputFileOptions, DisplayOptions, LoggingOptions): term: IO[Any] @@ -150,7 +160,13 @@ def default() -> dict[str, Any]: @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() + return ( + DefinitionOptions.from_option_string() + | OutputFileOptions.from_option_string() + | DisplayOptions.from_option_string() + | LoggingOptions.from_option_string() + ) + class ProveLegacyOptions(DefinitionOptions, OutputFileOptions, LoggingOptions): main_file: Path @@ -163,10 +179,15 @@ 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'} + return ( + DefinitionOptions.from_option_string() + | OutputFileOptions.from_option_string() + | LoggingOptions.from_option_string() + | {'kArgs': 'k_args'} + ) class KompileCommandOptions(LoggingOptions, WarningOptions, KDefinitionOptions, KompileOptions): @@ -185,7 +206,13 @@ def default() -> dict[str, Any]: @staticmethod def from_option_string() -> dict[str, str]: - return KDefinitionOptions.from_option_string() | KompileOptions.from_option_string() | LoggingOptions.from_option_string() | {'definition': 'definition_dir'} + return ( + KDefinitionOptions.from_option_string() + | KompileOptions.from_option_string() + | LoggingOptions.from_option_string() + | {'definition': 'definition_dir'} + ) + class ProveOptions(LoggingOptions): spec_file: Path @@ -205,7 +232,12 @@ def default() -> dict[str, Any]: @staticmethod def from_option_string() -> dict[str, str]: - return KDefinitionOptions.from_option_string() | KompileOptions.from_option_string() | LoggingOptions.from_option_string() | {'definition': 'definition_dir'} + return ( + KDefinitionOptions.from_option_string() + | KompileOptions.from_option_string() + | LoggingOptions.from_option_string() + | {'definition': 'definition_dir'} + ) class RunOptions(LoggingOptions): From 8ce237c4610c2ff2f2ee8d722af8e1c0d52496f1 Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Wed, 20 Mar 2024 22:37:41 +0300 Subject: [PATCH 18/19] reorganized and added unit tests --- src/pyk/__main__.py | 37 ------------------ src/pyk/cli/pyk.py | 67 +++++++++++++++++--------------- src/tests/unit/test_toml_args.py | 11 +++++- 3 files changed, 45 insertions(+), 70 deletions(-) diff --git a/src/pyk/__main__.py b/src/pyk/__main__.py index 5154d7d1a..e6809c0b0 100644 --- a/src/pyk/__main__.py +++ b/src/pyk/__main__.py @@ -7,7 +7,6 @@ from pathlib import Path from typing import TYPE_CHECKING -import tomli from graphviz import Digraph from .cli.pyk import PrintInput, create_argument_parser, generate_options, parse_toml_args @@ -38,7 +37,6 @@ from .utils import check_file_path, ensure_dir_path, exit_with_process_error if TYPE_CHECKING: - from argparse import Namespace from typing import Any, Final from .cli.pyk import ( @@ -370,40 +368,5 @@ def exec_json_to_kore(options: JsonToKoreOptions) -> None: sys.stdout.write('\n') -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 - - if __name__ == '__main__': main() diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index 3c68f0274..7e6b684a0 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -1,5 +1,7 @@ from __future__ import annotations +import logging +from argparse import ArgumentParser, FileType import logging from argparse import ArgumentParser, FileType from enum import Enum @@ -7,13 +9,18 @@ import tomli +import tomli + from ..ktool import TypeInferenceMode from ..ktool.kompile import KompileBackend +from ..ktool import TypeInferenceMode from .args import ( + ConfigArgs, ConfigArgs, DefinitionOptions, DisplayOptions, KCLIArgs, + KCLIArgs, KDefinitionOptions, KompileOptions, LoggingOptions, @@ -21,15 +28,20 @@ WarningOptions, ) from .utils import dir_path, file_path +from .utils import dir_path, file_path if TYPE_CHECKING: + from argparse import Namespace from argparse import Namespace from collections.abc import Iterable from pathlib import Path from typing import Final + from typing import Final + _LOGGER: Final = logging.getLogger(__name__) +_LOGGER: Final = logging.getLogger(__name__) def generate_options(args: dict[str, Any]) -> LoggingOptions: @@ -273,7 +285,7 @@ def create_argument_parser() -> ArgumentParser: rpc_print_args = pyk_args_command.add_parser( 'rpc-print', help='Pretty-print an RPC request/response', - parents=[k_cli_args.logging_args], + parents=[k_cli_args.logging_args, config_args.config_args], ) rpc_print_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') rpc_print_args.add_argument( @@ -286,7 +298,7 @@ def create_argument_parser() -> ArgumentParser: rpc_kast_args = pyk_args_command.add_parser( 'rpc-kast', help='Convert an "execute" JSON RPC response to a new "execute" or "simplify" request, copying parameters from a reference request.', - parents=[k_cli_args.logging_args], + parents=[k_cli_args.logging_args, config_args.config_args], ) rpc_kast_args.add_argument( 'reference_request_file', @@ -303,7 +315,7 @@ def create_argument_parser() -> ArgumentParser: prove_legacy_args = pyk_args_command.add_parser( 'prove-legacy', help='Prove an input specification (using kprovex).', - parents=[k_cli_args.logging_args], + parents=[k_cli_args.logging_args, config_args.config_args], ) prove_legacy_args.add_argument('definition_dir', type=dir_path, help='Path to definition directory.') prove_legacy_args.add_argument('main_file', type=str, help='Main file used for kompilation.') @@ -315,19 +327,14 @@ def create_argument_parser() -> ArgumentParser: kompile_args = pyk_args_command.add_parser( 'kompile', help='Kompile the K specification.', - parents=[ - k_cli_args.logging_args, - k_cli_args.warning_args, - k_cli_args.definition_args, - k_cli_args.kompile_args, - ], + parents=[k_cli_args.logging_args, k_cli_args.definition_args, k_cli_args.kompile_args, config_args.config_args], ) kompile_args.add_argument('main_file', type=str, help='File with the specification module.') run_args = pyk_args_command.add_parser( 'run', help='Run a given program using the K definition.', - parents=[k_cli_args.logging_args], + parents=[k_cli_args.logging_args, config_args.config_args], ) run_args.add_argument('pgm_file', type=str, help='File program to run in it.') run_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.') @@ -377,7 +384,7 @@ def create_argument_parser() -> ArgumentParser: return pyk_args -def parse_toml_args(args: Namespace) -> dict[str, Any]: +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} @@ -385,32 +392,28 @@ def get_profile(toml_profile: dict[str, Any], profile_list: list[str]) -> dict[s 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: dict[str, Any] = {} - if not hasattr(args, 'config_file') or not args.config_file.is_file(): - return {} - - 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 = {} + 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_adj_args: dict[str, Any] = {} + toml_args = {get_option_string_destination(args.command, k): v for k, v in toml_args.items()} for k, v in toml_args.items(): - opt_string = get_option_string_destination(args.command, k) - if opt_string[:3] == 'no_': - toml_adj_args[opt_string[3:]] = not v - elif k == 'optimization-level': + 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 - toml_adj_args['-o' + str(level)] = True - else: - toml_adj_args[opt_string] = v + del toml_args[k] + toml_args['-o' + str(level)] = 'true' - return toml_adj_args + return toml_args diff --git a/src/tests/unit/test_toml_args.py b/src/tests/unit/test_toml_args.py index 28873e5b4..2f10fbc5a 100644 --- a/src/tests/unit/test_toml_args.py +++ b/src/tests/unit/test_toml_args.py @@ -37,7 +37,16 @@ def test_toml_read() -> None: def test_toml_profiles() -> None: parser = create_argument_parser() - cmd_args = ['coverage', '--config-file', str(TEST_TOML), '--config-profile', 'a_profile', '.', str(TEST_TOML)] + 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 From 2289509cf386d4be7198fba919d4a8cddca7d73d Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Tue, 16 Apr 2024 12:22:49 +0300 Subject: [PATCH 19/19] fixed optimization level parameter --- src/pyk/cli/pyk.py | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/pyk/cli/pyk.py b/src/pyk/cli/pyk.py index 7e6b684a0..1071ec59c 100644 --- a/src/pyk/cli/pyk.py +++ b/src/pyk/cli/pyk.py @@ -413,7 +413,8 @@ def get_profile(toml_profile: dict[str, Any], profile_list: list[str]) -> dict[s 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' + toml_adj_args['o' + str(level)] = True + else: + toml_adj_args[opt_string] = v return toml_args