From 7b8e3b0c1c65cb3a297bde457bb1ae0ff2740547 Mon Sep 17 00:00:00 2001 From: Tolga Ovatman Date: Fri, 17 May 2024 16:19:29 +0300 Subject: [PATCH] added toml processing capability (#2369) Following changes are provided: * a parameter set is added to the command line arguments to input toml file name and profile * parse_toml_args function reads all the options available in the toml file provided, taking into account the provided profile name * get_option_string_destinationfunction collects the mathing option string according to the provided key in toml file by utilizing the newly added from_option_string method in *Options classes. * some methods and classes are moved to the pyk.clipackage to provide better testability * unit tests and test harness added for toml input sanity tests * required modifications made on code regarding the new functionality and the ones that ar moved to another package. * pyk's `parse_toml_args` function is re-used * type setting capability for the argument values provided from toml files is added together with related tests in this context * added typed checking support for toml list inputs --------- Co-authored-by: Tolga Ovatman Co-authored-by: devops --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- kevm-pyk/src/kevm_pyk/__main__.py | 376 +--------- kevm-pyk/src/kevm_pyk/cli.py | 673 +++++++++++++++++- kevm-pyk/src/tests/integration/test_prove.py | 3 +- .../unit/test-data/kevm_pyk_toml_test.toml | 10 + kevm-pyk/src/tests/unit/test_toml_args.py | 61 ++ package/version | 2 +- 8 files changed, 762 insertions(+), 367 deletions(-) create mode 100644 kevm-pyk/src/tests/unit/test-data/kevm_pyk_toml_test.toml create mode 100644 kevm-pyk/src/tests/unit/test_toml_args.py diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 137a74280a..da12d98ab4 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.559" +version = "1.0.560" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index d1f3cb3580..14b4da04ca 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '1.0.559' +VERSION: Final = '1.0.560' diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index f07f70e9a9..3e8de4c153 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -8,7 +8,6 @@ import sys import tempfile import time -from argparse import ArgumentParser from collections.abc import Iterable from dataclasses import dataclass from functools import cached_property @@ -16,25 +15,15 @@ from typing import TYPE_CHECKING from pathos.pools import ProcessPool # type: ignore -from pyk.cli.args import ( - BugReportOptions, - KompileOptions, - LoggingOptions, - ParallelOptions, - SaveDirOptions, - SMTOptions, - SpecOptions, -) -from pyk.cli.utils import file_path +from pyk.cli.pyk import parse_toml_args from pyk.cterm import CTermSymbolic from pyk.kast.outer import KApply, KRewrite, KSort, KToken from pyk.kcfg import KCFG from pyk.kcfg.explore import KCFGExplore from pyk.kdist import kdist from pyk.kore.rpc import KoreClient -from pyk.kore.tools import PrintOutput, kore_print +from pyk.kore.tools import kore_print from pyk.ktool.kompile import LLVMKompileType -from pyk.ktool.krun import KRunOutput from pyk.prelude.ml import is_bottom, is_top, mlOr from pyk.proof import APRProof from pyk.proof.implies import EqualityProof @@ -43,24 +32,11 @@ from pyk.utils import FrozenDict, hash_str, single from . import VERSION, config -from .cli import ( - DisplayOptions, - EVMChainOptions, - ExploreOptions, - KCFGShowOptions, - KEVMCLIArgs, - KOptions, - KProveLegacyOptions, - KProveOptions, - RPCOptions, - TargetOptions, - node_id_like, -) +from .cli import _create_argument_parser, generate_options, get_argument_type_setter, get_option_string_destination from .gst_to_kore import SORT_ETHEREUM_SIMULATION, gst_to_kore, kore_pgm_to_kore from .kevm import KEVM, KEVMSemantics, kevm_node_printer from .kompile import KompileTarget, kevm_kompile from .utils import ( - arg_pair_of, claim_dependency_dict, ensure_ksequence_on_k_cell, get_apr_proof_for_spec, @@ -75,10 +51,22 @@ from typing import Any, Final, TypeVar from pyk.kast.outer import KClaim - from pyk.kcfg.kcfg import NodeIdLike from pyk.kcfg.tui import KCFGElem from pyk.proof.proof import Proof + from .cli import ( + KastOptions, + KompileSpecOptions, + ProveLegacyOptions, + ProveOptions, + PruneOptions, + RunOptions, + SectionEdgeOptions, + ShowKCFGOptions, + VersionOptions, + ViewKCFGOptions, + ) + T = TypeVar('T') _LOGGER: Final = logging.getLogger(__name__) @@ -96,9 +84,10 @@ def main() -> None: sys.setrecursionlimit(15000000) parser = _create_argument_parser() args = parser.parse_args() + toml_args = parse_toml_args(args, get_option_string_destination, get_argument_type_setter) logging.basicConfig(level=_loglevel(args), format=_LOG_FORMAT) - 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) @@ -111,56 +100,10 @@ def main() -> None: execute(options) -def generate_options(args: dict[str, Any]) -> LoggingOptions: - command = args['command'] - match command: - case 'version': - return VersionOptions(args) - case 'kompile-spec': - return KompileSpecOptions(args) - case 'prove-legacy': - return ProveLegacyOptions(args) - case 'prove': - return ProveOptions(args) - case 'prune': - return PruneOptions(args) - case 'section-edge': - return SectionEdgeOptions(args) - case 'show-kcfg': - return ShowKCFGOptions(args) - case 'view-kcfg': - return ViewKCFGOptions(args) - case 'kast': - return KastOptions(args) - case 'run': - return RunOptions(args) - case _: - raise ValueError(f'Unrecognized command: {command}') - - -# Command implementation - - -class VersionOptions(LoggingOptions): ... - - def exec_version(options: VersionOptions) -> None: print(f'KEVM Version: {VERSION}') -class KompileSpecOptions(LoggingOptions, KOptions, KompileOptions): - main_file: Path - target: KompileTarget - debug_build: bool - - @staticmethod - def default() -> dict[str, Any]: - return { - 'target': KompileTarget.HASKELL, - 'debug_build': False, - } - - def exec_kompile_spec(options: KompileSpecOptions) -> None: if options.target not in [KompileTarget.HASKELL, KompileTarget.MAUDE]: raise ValueError(f'Can only call kevm kompile-spec with --target [haskell,maude], got: {options.target.value}') @@ -196,16 +139,6 @@ def exec_kompile_spec(options: KompileSpecOptions) -> None: ) -class ProveLegacyOptions(LoggingOptions, KOptions, SpecOptions, KProveLegacyOptions): - bug_report_legacy: bool - - @staticmethod - def default() -> dict[str, Any]: - return { - 'bug_report_legacy': False, - } - - def exec_prove_legacy(options: ProveLegacyOptions) -> None: definition_dir = options.definition_dir or kdist.get('evm-semantics.haskell') @@ -311,28 +244,6 @@ def get_or_load_claim_job(claim_label: str) -> KClaimJob: return frozenset({get_or_load_claim_job(claim.label) for claim in claims}) -class ProveOptions( - LoggingOptions, - ParallelOptions, - KOptions, - RPCOptions, - BugReportOptions, - SMTOptions, - ExploreOptions, - SpecOptions, - KProveOptions, -): - reinit: bool - max_frontier_parallel: int - - @staticmethod - def default() -> dict[str, Any]: - return { - 'reinit': False, - 'max_frontier_parallel': 1, - } - - def exec_prove(options: ProveOptions) -> None: md_selector = 'k' @@ -529,10 +440,6 @@ def create_kcfg_explore() -> KCFGExplore: sys.exit(failed) -class PruneOptions(LoggingOptions, KOptions, SpecOptions): - node: NodeIdLike - - def exec_prune(options: PruneOptions) -> None: md_selector = 'k' @@ -565,25 +472,6 @@ def exec_prune(options: PruneOptions) -> None: apr_proof.write_proof_data() -class SectionEdgeOptions( - LoggingOptions, - KOptions, - RPCOptions, - SMTOptions, - SpecOptions, - BugReportOptions, -): - edge: tuple[str, str] - sections: int - - @staticmethod - def default() -> dict[str, Any]: - return { - 'sections': 2, - 'use_booster': False, - } - - def exec_section_edge(options: SectionEdgeOptions) -> None: md_selector = 'k' @@ -637,15 +525,6 @@ def exec_section_edge(options: SectionEdgeOptions) -> None: proof.write_proof_data() -class ShowKCFGOptions( - LoggingOptions, - KCFGShowOptions, - KOptions, - SpecOptions, - DisplayOptions, -): ... - - def exec_show_kcfg(options: ShowKCFGOptions) -> None: if options.definition_dir is None: @@ -691,13 +570,6 @@ def exec_show_kcfg(options: ShowKCFGOptions) -> None: print('\n'.join(res_lines)) -class ViewKCFGOptions( - LoggingOptions, - KOptions, - SpecOptions, -): ... - - def exec_view_kcfg(options: ViewKCFGOptions) -> None: if options.definition_dir is None: @@ -731,27 +603,6 @@ def custom_view(element: KCFGElem) -> list[str]: proof_view.run() -class RunOptions( - LoggingOptions, - KOptions, - EVMChainOptions, - TargetOptions, - SaveDirOptions, -): - input_file: Path - output: KRunOutput - expand_macros: bool - debugger: bool - - @staticmethod - def default() -> dict[str, Any]: - return { - 'output': KRunOutput.PRETTY, - 'expand_macros': True, - 'debugger': False, - } - - def exec_run(options: RunOptions) -> None: target = options.target or 'llvm' @@ -781,23 +632,6 @@ def exec_run(options: RunOptions) -> None: ) -class KastOptions( - LoggingOptions, - TargetOptions, - EVMChainOptions, - KOptions, - SaveDirOptions, -): - input_file: Path - output: PrintOutput - - @staticmethod - def default() -> dict[str, Any]: - return { - 'output': PrintOutput.KORE, - } - - def exec_kast(options: KastOptions) -> None: target = options.target or 'llvm' @@ -823,180 +657,6 @@ def exec_kast(options: KastOptions) -> None: # Helpers -def _create_argument_parser() -> ArgumentParser: - def list_of(elem_type: Callable[[str], T], delim: str = ';') -> Callable[[str], list[T]]: - def parse(s: str) -> list[T]: - return [elem_type(elem) for elem in s.split(delim)] - - return parse - - kevm_cli_args = KEVMCLIArgs() - parser = ArgumentParser(prog='kevm-pyk') - - command_parser = parser.add_subparsers(dest='command', required=True) - - command_parser.add_parser('version', help='Print KEVM version and exit.', parents=[kevm_cli_args.logging_args]) - - kevm_kompile_spec_args = command_parser.add_parser( - 'kompile-spec', - help='Kompile KEVM specification.', - parents=[kevm_cli_args.logging_args, kevm_cli_args.k_args, kevm_cli_args.kompile_args], - ) - kevm_kompile_spec_args.add_argument('main_file', type=file_path, help='Path to file with main module.') - kevm_kompile_spec_args.add_argument('--target', type=KompileTarget, help='[haskell|maude]') - - kevm_kompile_spec_args.add_argument( - '--debug-build', dest='debug_build', default=None, help='Enable debug symbols in LLVM builds.' - ) - - prove_args = command_parser.add_parser( - 'prove', - help='Run KEVM proof.', - parents=[ - kevm_cli_args.logging_args, - kevm_cli_args.parallel_args, - kevm_cli_args.k_args, - kevm_cli_args.kprove_args, - kevm_cli_args.rpc_args, - kevm_cli_args.bug_report_args, - kevm_cli_args.smt_args, - kevm_cli_args.explore_args, - kevm_cli_args.spec_args, - ], - ) - prove_args.add_argument( - '--reinit', - dest='reinit', - default=None, - action='store_true', - help='Reinitialize CFGs even if they already exist.', - ) - prove_args.add_argument( - '--max-frontier-parallel', - type=int, - dest='max_frontier_parallel', - default=None, - help='Maximum number of branches of a single proof to explore in parallel.', - ) - - prune_args = command_parser.add_parser( - 'prune', - help='Remove a node and its successors from the proof state.', - parents=[ - kevm_cli_args.logging_args, - kevm_cli_args.k_args, - kevm_cli_args.spec_args, - ], - ) - prune_args.add_argument('node', type=node_id_like, help='Node to remove CFG subgraph from.') - - section_edge_args = command_parser.add_parser( - 'section-edge', - help='Break an edge into sections.', - parents=[ - kevm_cli_args.logging_args, - kevm_cli_args.k_args, - kevm_cli_args.spec_args, - ], - ) - section_edge_args.add_argument('edge', type=arg_pair_of(str, str), help='Edge to section in CFG.') - section_edge_args.add_argument('--sections', type=int, help='Number of sections to make from edge (>= 2).') - section_edge_args.add_argument( - '--use-booster', - dest='use_booster', - default=None, - action='store_true', - help="Use the booster RPC server instead of kore-rpc. Requires calling kompile with '--target haskell-booster' flag", - ) - - prove_legacy_args = command_parser.add_parser( - 'prove-legacy', - help='Run KEVM proof using the legacy kprove binary.', - parents=[ - kevm_cli_args.logging_args, - kevm_cli_args.k_args, - kevm_cli_args.spec_args, - kevm_cli_args.kprove_legacy_args, - ], - ) - prove_legacy_args.add_argument( - '--bug-report-legacy', default=None, action='store_true', help='Generate a legacy bug report.' - ) - - command_parser.add_parser( - 'view-kcfg', - help='Explore a given proof in the KCFG visualizer.', - parents=[kevm_cli_args.logging_args, kevm_cli_args.k_args, kevm_cli_args.spec_args], - ) - - command_parser.add_parser( - 'show-kcfg', - help='Print the CFG for a given proof.', - parents=[ - kevm_cli_args.logging_args, - kevm_cli_args.k_args, - kevm_cli_args.kcfg_show_args, - kevm_cli_args.spec_args, - kevm_cli_args.display_args, - ], - ) - - run_args = command_parser.add_parser( - 'run', - help='Run KEVM test/simulation.', - parents=[ - kevm_cli_args.logging_args, - kevm_cli_args.target_args, - kevm_cli_args.evm_chain_args, - kevm_cli_args.k_args, - ], - ) - run_args.add_argument('input_file', type=file_path, help='Path to input file.') - run_args.add_argument( - '--output', - type=KRunOutput, - choices=list(KRunOutput), - ) - run_args.add_argument( - '--expand-macros', - dest='expand_macros', - default=None, - action='store_true', - help='Expand macros on the input term before execution.', - ) - run_args.add_argument( - '--no-expand-macros', - dest='expand_macros', - action='store_false', - help='Do not expand macros on the input term before execution.', - ) - run_args.add_argument( - '--debugger', - dest='debugger', - action='store_true', - help='Run GDB debugger for execution.', - ) - - kast_args = command_parser.add_parser( - 'kast', - help='Run KEVM program.', - parents=[ - kevm_cli_args.logging_args, - kevm_cli_args.target_args, - kevm_cli_args.evm_chain_args, - kevm_cli_args.k_args, - ], - ) - kast_args.add_argument('input_file', type=file_path, help='Path to input file.') - kast_args.add_argument( - '--output', - type=PrintOutput, - choices=list(PrintOutput), - ) - - return parser - - def _loglevel(args: Namespace) -> int: if args.debug: return logging.DEBUG diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 361db2b13b..b362e4af4c 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -1,28 +1,47 @@ from __future__ import annotations +import logging from argparse import ArgumentParser from functools import cached_property +from pathlib import Path from typing import TYPE_CHECKING, Any +from pyk.cli.args import BugReportOptions from pyk.cli.args import DisplayOptions as PykDisplayOptions -from pyk.cli.args import KCLIArgs, KDefinitionOptions, Options +from pyk.cli.args import ( + KCLIArgs, + KDefinitionOptions, + KompileOptions, + LoggingOptions, + Options, + ParallelOptions, + SaveDirOptions, + SMTOptions, + SpecOptions, +) +from pyk.cli.utils import file_path from pyk.kore.rpc import FallbackReason +from pyk.kore.tools import PrintOutput +from pyk.ktool.krun import KRunOutput +from .kompile import KompileTarget from .utils import arg_pair_of if TYPE_CHECKING: from collections.abc import Callable - from pathlib import Path - from typing import TypeVar + from typing import Final, TypeVar from pyk.kcfg.kcfg import NodeIdLike T = TypeVar('T') +_LOGGER: Final = logging.getLogger(__name__) + def list_of(elem_type: Callable[[str], T], delim: str = ';') -> Callable[[str], list[T]]: - def parse(s: str) -> list[T]: - return [elem_type(elem) for elem in s.split(delim)] + def parse(s: str | list[str]) -> list[T]: + s_list = s.split(delim) if not isinstance(s, list) else s + return [elem_type(elem) for elem in s_list] return parse @@ -34,6 +53,251 @@ def node_id_like(s: str) -> NodeIdLike: return s +def generate_options(args: dict[str, Any]) -> LoggingOptions: + command = args['command'] + match command: + case 'version': + return VersionOptions(args) + case 'kompile-spec': + return KompileSpecOptions(args) + case 'prove-legacy': + return ProveLegacyOptions(args) + case 'prove': + return ProveOptions(args) + case 'prune': + return PruneOptions(args) + case 'section-edge': + return SectionEdgeOptions(args) + case 'show-kcfg': + return ShowKCFGOptions(args) + case 'view-kcfg': + return ViewKCFGOptions(args) + case 'kast': + return KastOptions(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 'version': + option_string_destinations = VersionOptions.from_option_string() + case 'kompile-spec': + option_string_destinations = KompileSpecOptions.from_option_string() + case 'prove-legacy': + option_string_destinations = ProveLegacyOptions.from_option_string() + case 'prove': + option_string_destinations = ProveOptions.from_option_string() + case 'prune': + option_string_destinations = PruneOptions.from_option_string() + case 'section-edge': + option_string_destinations = SectionEdgeOptions.from_option_string() + case 'show-kcfg': + option_string_destinations = ShowKCFGOptions.from_option_string() + case 'view-kcfg': + option_string_destinations = ViewKCFGOptions.from_option_string() + case 'kast': + option_string_destinations = KastOptions.from_option_string() + case 'run': + option_string_destinations = RunOptions.from_option_string() + + return option_string_destinations.get(option_string, option_string.replace('-', '_')) + + +def get_argument_type_setter(command: str, option_string: str) -> Callable[[str], Any]: + def func(par: str) -> str: + return par + + option_types = {} + match command: + case 'version': + option_types = VersionOptions.get_argument_type() + case 'kompile-spec': + option_types = KompileSpecOptions.get_argument_type() + case 'prove-legacy': + option_types = ProveLegacyOptions.get_argument_type() + case 'prove': + option_types = ProveOptions.get_argument_type() + case 'prune': + option_types = PruneOptions.get_argument_type() + case 'section-edge': + option_types = SectionEdgeOptions.get_argument_type() + case 'show-kcfg': + option_types = ShowKCFGOptions.get_argument_type() + case 'view-kcfg': + option_types = ViewKCFGOptions.get_argument_type() + case 'kast': + option_types = KastOptions.get_argument_type() + case 'run': + option_types = RunOptions.get_argument_type() + + return option_types.get(option_string, func) + + +def _create_argument_parser() -> ArgumentParser: + kevm_cli_args = KEVMCLIArgs() + config_args = ConfigArgs() + parser = ArgumentParser(prog='kevm-pyk') + + command_parser = parser.add_subparsers(dest='command', required=True) + + command_parser.add_parser( + 'version', help='Print KEVM version and exit.', parents=[kevm_cli_args.logging_args, config_args.config_args] + ) + + kevm_kompile_spec_args = command_parser.add_parser( + 'kompile-spec', + help='Kompile KEVM specification.', + parents=[kevm_cli_args.logging_args, kevm_cli_args.k_args, kevm_cli_args.kompile_args, config_args.config_args], + ) + kevm_kompile_spec_args.add_argument('main_file', type=file_path, help='Path to file with main module.') + kevm_kompile_spec_args.add_argument('--target', type=KompileTarget, help='[haskell|maude]') + + kevm_kompile_spec_args.add_argument( + '--debug-build', dest='debug_build', default=None, help='Enable debug symbols in LLVM builds.' + ) + + prove_args = command_parser.add_parser( + 'prove', + help='Run KEVM proof.', + parents=[ + kevm_cli_args.logging_args, + kevm_cli_args.parallel_args, + kevm_cli_args.k_args, + kevm_cli_args.kprove_args, + kevm_cli_args.rpc_args, + kevm_cli_args.bug_report_args, + kevm_cli_args.smt_args, + kevm_cli_args.explore_args, + kevm_cli_args.spec_args, + config_args.config_args, + ], + ) + prove_args.add_argument( + '--reinit', + dest='reinit', + default=None, + action='store_true', + help='Reinitialize CFGs even if they already exist.', + ) + + prune_args = command_parser.add_parser( + 'prune', + help='Remove a node and its successors from the proof state.', + parents=[kevm_cli_args.logging_args, kevm_cli_args.k_args, kevm_cli_args.spec_args, config_args.config_args], + ) + prune_args.add_argument('node', type=node_id_like, help='Node to remove CFG subgraph from.') + + section_edge_args = command_parser.add_parser( + 'section-edge', + help='Break an edge into sections.', + parents=[kevm_cli_args.logging_args, kevm_cli_args.k_args, kevm_cli_args.spec_args, config_args.config_args], + ) + section_edge_args.add_argument('edge', type=arg_pair_of(str, str), help='Edge to section in CFG.') + section_edge_args.add_argument('--sections', type=int, help='Number of sections to make from edge (>= 2).') + section_edge_args.add_argument( + '--use-booster', + dest='use_booster', + default=None, + action='store_true', + help="Use the booster RPC server instead of kore-rpc. Requires calling kompile with '--target haskell-booster' flag", + ) + + prove_legacy_args = command_parser.add_parser( + 'prove-legacy', + help='Run KEVM proof using the legacy kprove binary.', + parents=[ + kevm_cli_args.logging_args, + kevm_cli_args.k_args, + kevm_cli_args.spec_args, + kevm_cli_args.kprove_legacy_args, + config_args.config_args, + ], + ) + prove_legacy_args.add_argument( + '--bug-report-legacy', default=None, action='store_true', help='Generate a legacy bug report.' + ) + + command_parser.add_parser( + 'view-kcfg', + help='Explore a given proof in the KCFG visualizer.', + parents=[kevm_cli_args.logging_args, kevm_cli_args.k_args, kevm_cli_args.spec_args, config_args.config_args], + ) + + command_parser.add_parser( + 'show-kcfg', + help='Print the CFG for a given proof.', + parents=[ + kevm_cli_args.logging_args, + kevm_cli_args.k_args, + kevm_cli_args.kcfg_show_args, + kevm_cli_args.spec_args, + kevm_cli_args.display_args, + config_args.config_args, + ], + ) + + run_args = command_parser.add_parser( + 'run', + help='Run KEVM test/simulation.', + parents=[ + kevm_cli_args.logging_args, + kevm_cli_args.target_args, + kevm_cli_args.evm_chain_args, + kevm_cli_args.k_args, + config_args.config_args, + ], + ) + run_args.add_argument('input_file', type=file_path, help='Path to input file.') + run_args.add_argument( + '--output', + type=KRunOutput, + choices=list(KRunOutput), + ) + run_args.add_argument( + '--expand-macros', + dest='expand_macros', + default=None, + action='store_true', + help='Expand macros on the input term before execution.', + ) + run_args.add_argument( + '--no-expand-macros', + dest='expand_macros', + action='store_false', + help='Do not expand macros on the input term before execution.', + ) + run_args.add_argument( + '--debugger', + dest='debugger', + action='store_true', + help='Run GDB debugger for execution.', + ) + + kast_args = command_parser.add_parser( + 'kast', + help='Run KEVM program.', + parents=[ + kevm_cli_args.logging_args, + kevm_cli_args.target_args, + kevm_cli_args.evm_chain_args, + kevm_cli_args.k_args, + config_args.config_args, + ], + ) + kast_args.add_argument('input_file', type=file_path, help='Path to input file.') + kast_args.add_argument( + '--output', + type=PrintOutput, + choices=list(PrintOutput), + ) + + return parser + + class KOptions(KDefinitionOptions): definition_dir: Path | None depth: int | None @@ -45,6 +309,16 @@ def default() -> dict[str, Any]: 'depth': None, } + @staticmethod + def from_option_string() -> dict[str, str]: + return KDefinitionOptions.from_option_string() | { + 'definition': 'definition_dir', + } + + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return KDefinitionOptions.get_argument_type() + class KProveLegacyOptions(Options): bug_report: bool @@ -65,6 +339,16 @@ def default() -> dict[str, Any]: 'haskell_backend_args': [], } + @staticmethod + def from_option_string() -> dict[str, str]: + return KDefinitionOptions.from_option_string() | { + 'haskell-backend-arg': 'haskell_backend_args', + } + + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return {'haskell-backend-arg': list_of(str)} + class RPCOptions(Options): trace_rewrites: bool @@ -89,6 +373,10 @@ def default() -> dict[str, Any]: 'maude_port': None, } + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return {'fallback-on': list_of(FallbackReason, delim=',')} + class ExploreOptions(Options): break_every_step: bool @@ -119,6 +407,13 @@ def default() -> dict[str, Any]: 'fail_fast': True, } + @staticmethod + def from_option_string() -> dict[str, str]: + return { + 'failure-information': 'failure_info', + 'no-failure-information': 'no_failure_info', + } + class KProveOptions(Options): debug_equations: list[str] @@ -155,6 +450,22 @@ def default() -> dict[str, Any]: 'counterexample_info': False, } + @staticmethod + def from_option_string() -> dict[str, str]: + return { + 'counterexample-information': 'counterexample_info', + 'no-counterexample-information': 'no_counterexample_info', + 'node': 'nodes', + 'node-delta': 'node_deltas', + } + + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return { + 'node': list_of(node_id_like, delim=','), + 'node-delta': list_of(arg_pair_of(node_id_like, node_id_like)), + } + class TargetOptions(Options): target: str | None @@ -181,6 +492,12 @@ def default() -> dict[str, Any]: 'use_gas': True, } + @staticmethod + def from_option_string() -> dict[str, str]: + return { + 'no-gas': 'no_usegas', + } + class DisplayOptions(PykDisplayOptions): sort_collections: bool @@ -191,6 +508,14 @@ def default() -> dict[str, Any]: 'sort_collections': False, } + @staticmethod + def from_option_string() -> dict[str, str]: + return PykDisplayOptions.from_option_string() + + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return PykDisplayOptions.get_argument_type() + class KGenOptions(Options): requires: list[str] @@ -203,6 +528,344 @@ def default() -> dict[str, Any]: 'imports': [], } + @staticmethod + def from_option_string() -> dict[str, str]: + return { + 'require': 'requires', + 'module-import': 'imports', + } + + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return { + 'require': list_of(str), + 'module-import': list_of(str), + } + + +class VersionOptions(LoggingOptions): + @staticmethod + def from_option_string() -> dict[str, str]: + return LoggingOptions.from_option_string() + + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return LoggingOptions.get_argument_type() + + +class KompileSpecOptions(LoggingOptions, KOptions, KompileOptions): + main_file: Path + target: KompileTarget + debug_build: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'target': KompileTarget.HASKELL, + 'debug_build': False, + } + + @staticmethod + def from_option_string() -> dict[str, str]: + return LoggingOptions.from_option_string() | KOptions.from_option_string() | KompileOptions.from_option_string() + + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return ( + LoggingOptions.get_argument_type() + | KOptions.get_argument_type() + | KompileOptions.get_argument_type() + | {'target': KompileTarget, 'main_file': file_path} + ) + + +class ProveLegacyOptions(LoggingOptions, KOptions, SpecOptions, KProveLegacyOptions): + bug_report_legacy: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'bug_report_legacy': False, + } + + @staticmethod + def from_option_string() -> dict[str, str]: + return ( + LoggingOptions.from_option_string() + | KOptions.from_option_string() + | SpecOptions.from_option_string() + | KProveLegacyOptions.from_option_string() + ) + + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return ( + LoggingOptions.get_argument_type() + | KOptions.get_argument_type() + | SpecOptions.get_argument_type() + | KProveLegacyOptions.get_argument_type() + ) + + +class ProveOptions( + LoggingOptions, + ParallelOptions, + KOptions, + RPCOptions, + BugReportOptions, + SMTOptions, + ExploreOptions, + SpecOptions, + KProveOptions, +): + reinit: bool + max_frontier_parallel: int + + @staticmethod + def default() -> dict[str, Any]: + return { + 'reinit': False, + 'max_frontier_parallel': 1, + } + + @staticmethod + def from_option_string() -> dict[str, str]: + return ( + LoggingOptions.from_option_string() + | ParallelOptions.from_option_string() + | KOptions.from_option_string() + | RPCOptions.from_option_string() + | BugReportOptions.from_option_string() + | SMTOptions.from_option_string() + | ExploreOptions.from_option_string() + | SpecOptions.from_option_string() + | KProveOptions.from_option_string() + ) + + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return ( + LoggingOptions.get_argument_type() + | ParallelOptions.get_argument_type() + | KOptions.get_argument_type() + | RPCOptions.get_argument_type() + | BugReportOptions.get_argument_type() + | SMTOptions.get_argument_type() + | ExploreOptions.get_argument_type() + | SpecOptions.get_argument_type() + | KProveOptions.get_argument_type() + ) + + +class PruneOptions(LoggingOptions, KOptions, SpecOptions): + node: NodeIdLike + + @staticmethod + def from_option_string() -> dict[str, str]: + return LoggingOptions.from_option_string() | KOptions.from_option_string() | SpecOptions.from_option_string() + + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return ( + LoggingOptions.get_argument_type() + | KOptions.get_argument_type() + | SpecOptions.get_argument_type() + | { + 'node': node_id_like, + } + ) + + +class SectionEdgeOptions( + LoggingOptions, + KOptions, + RPCOptions, + SMTOptions, + SpecOptions, + BugReportOptions, +): + edge: tuple[str, str] + sections: int + + @staticmethod + def default() -> dict[str, Any]: + return { + 'sections': 2, + 'use_booster': False, + } + + @staticmethod + def from_option_string() -> dict[str, str]: + return ( + LoggingOptions.from_option_string() + | KOptions.from_option_string() + | RPCOptions.from_option_string() + | SMTOptions.from_option_string() + | SpecOptions.from_option_string() + | BugReportOptions.from_option_string() + ) + + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return ( + LoggingOptions.get_argument_type() + | KOptions.get_argument_type() + | RPCOptions.get_argument_type() + | SMTOptions.get_argument_type() + | SpecOptions.get_argument_type() + | BugReportOptions.get_argument_type() + | { + 'edge': arg_pair_of(str, str), + } + ) + + +class ShowKCFGOptions( + LoggingOptions, + KCFGShowOptions, + KOptions, + SpecOptions, + DisplayOptions, +): + @staticmethod + def from_option_string() -> dict[str, str]: + return ( + LoggingOptions.from_option_string() + | KCFGShowOptions.from_option_string() + | KOptions.from_option_string() + | SpecOptions.from_option_string() + | DisplayOptions.from_option_string() + ) + + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return ( + LoggingOptions.get_argument_type() + | KCFGShowOptions.get_argument_type() + | KOptions.get_argument_type() + | SpecOptions.get_argument_type() + | DisplayOptions.get_argument_type() + ) + + +class ViewKCFGOptions( + LoggingOptions, + KOptions, + SpecOptions, +): + @staticmethod + def from_option_string() -> dict[str, str]: + return LoggingOptions.from_option_string() | KOptions.from_option_string() | SpecOptions.from_option_string() + + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return LoggingOptions.get_argument_type() | KOptions.get_argument_type() | SpecOptions.get_argument_type() + + +class RunOptions( + LoggingOptions, + KOptions, + EVMChainOptions, + TargetOptions, + SaveDirOptions, +): + input_file: Path + output: KRunOutput + expand_macros: bool + debugger: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'output': KRunOutput.PRETTY, + 'expand_macros': True, + 'debugger': False, + } + + @staticmethod + def from_option_string() -> dict[str, str]: + return ( + LoggingOptions.from_option_string() + | KOptions.from_option_string() + | EVMChainOptions.from_option_string() + | TargetOptions.from_option_string() + | SaveDirOptions.from_option_string() + ) + + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return ( + LoggingOptions.get_argument_type() + | KOptions.get_argument_type() + | EVMChainOptions.get_argument_type() + | TargetOptions.get_argument_type() + | SaveDirOptions.get_argument_type() + | { + 'input_file': file_path, + 'output': KRunOutput, + } + ) + + +class KastOptions( + LoggingOptions, + TargetOptions, + EVMChainOptions, + KOptions, + SaveDirOptions, +): + input_file: Path + output: PrintOutput + + @staticmethod + def default() -> dict[str, Any]: + return { + 'output': PrintOutput.KORE, + } + + @staticmethod + def from_option_string() -> dict[str, str]: + return ( + LoggingOptions.from_option_string() + | TargetOptions.from_option_string() + | EVMChainOptions.from_option_string() + | KOptions.from_option_string() + | SaveDirOptions.from_option_string() + ) + + @staticmethod + def get_argument_type() -> dict[str, Callable]: + return ( + LoggingOptions.get_argument_type() + | KOptions.get_argument_type() + | EVMChainOptions.get_argument_type() + | TargetOptions.get_argument_type() + | SaveDirOptions.get_argument_type() + | { + 'input_file': file_path, + } + ) + + +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('./kevm-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 KEVMCLIArgs(KCLIArgs): @cached_property diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 280b752582..0935d9126e 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -10,7 +10,8 @@ from pyk.proof.reachability import APRProof from kevm_pyk import config -from kevm_pyk.__main__ import ProveOptions, exec_prove +from kevm_pyk.__main__ import exec_prove +from kevm_pyk.cli import ProveOptions from kevm_pyk.kevm import KEVM from kevm_pyk.kompile import KompileTarget, kevm_kompile diff --git a/kevm-pyk/src/tests/unit/test-data/kevm_pyk_toml_test.toml b/kevm-pyk/src/tests/unit/test-data/kevm_pyk_toml_test.toml new file mode 100644 index 0000000000..16dd2d88cb --- /dev/null +++ b/kevm-pyk/src/tests/unit/test-data/kevm_pyk_toml_test.toml @@ -0,0 +1,10 @@ +[run] +no-usegas = true + +[show-kcfg] +node = [3] +node-delta = ["3, 5", "6, 9"] + +[run.a_profile] +debugger = true +no-usegas = false \ No newline at end of file diff --git a/kevm-pyk/src/tests/unit/test_toml_args.py b/kevm-pyk/src/tests/unit/test_toml_args.py new file mode 100644 index 0000000000..626033de6f --- /dev/null +++ b/kevm-pyk/src/tests/unit/test_toml_args.py @@ -0,0 +1,61 @@ +from __future__ import annotations + +from typing import TYPE_CHECKING + +from pyk.cli.pyk import parse_toml_args + +from kevm_pyk.cli import _create_argument_parser, get_argument_type_setter, get_option_string_destination + +from .utils import TEST_DATA_DIR + +if TYPE_CHECKING: + from typing import Final + +TEST_TOML: Final = TEST_DATA_DIR / 'kevm_pyk_toml_test.toml' + + +def test_continue_when_default_toml_absent() -> None: + parser = _create_argument_parser() + cmd_args = ['run', str(TEST_TOML)] + args = parser.parse_args(cmd_args) + assert hasattr(args, 'config_file') + assert str(args.config_file) == 'kevm-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_arg_types() -> None: + parser = _create_argument_parser() + cmd_args = ['show-kcfg', '--config-file', str(TEST_TOML), str(TEST_TOML)] + args = parser.parse_args(cmd_args) + args_dict = parse_toml_args(args, get_option_string_destination, get_argument_type_setter) + assert 'nodes' in args_dict + assert len(args_dict['nodes']) == 1 + assert 'node_deltas' in args_dict + assert len(args_dict['node_deltas']) == 2 + assert len(args_dict['node_deltas'][0]) == 2 + assert len(args_dict['node_deltas'][1]) == 2 + + +def test_toml_read() -> None: + parser = _create_argument_parser() + cmd_args = ['run', '--config-file', str(TEST_TOML), str(TEST_TOML), '--verbose'] + args = parser.parse_args(cmd_args) + args_dict = parse_toml_args(args, get_option_string_destination, get_argument_type_setter) + assert 'usegas' in args_dict + assert not args_dict['usegas'] + assert hasattr(args, 'verbose') + assert args.verbose + + +def test_toml_profiles() -> None: + parser = _create_argument_parser() + cmd_args = ['run', '--config-file', str(TEST_TOML), '--config-profile', 'a_profile', str(TEST_TOML)] + args = parser.parse_args(cmd_args) + args_dict = parse_toml_args(args, get_option_string_destination, get_argument_type_setter) + assert 'debugger' in args_dict + assert args_dict['debugger'] + assert 'usegas' in args_dict + assert args_dict['usegas'] diff --git a/package/version b/package/version index fc4d3ab8e9..25197bb881 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.559 +1.0.560