From bfa344188f72eedd2b47ebc294276806cf0e28a6 Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Wed, 28 Feb 2024 15:57:50 -0600 Subject: [PATCH 01/28] Inherit from pyk options classes --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__main__.py | 164 +------- kevm-pyk/src/kevm_pyk/cli.py | 609 ++++++++++++++++++--------- kevm-pyk/src/kevm_pyk/gst_to_kore.py | 6 +- 4 files changed, 438 insertions(+), 343 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 68bfdc210f..8f2746b668 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -13,7 +13,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -pyk = { git = "https://github.com/runtimeverification/pyk.git", tag="v0.1.663" } +pyk = { git = "https://github.com/runtimeverification/pyk.git", branch="noah/default-options" } tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 4ea9e3ca1f..f7516f9efb 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -15,14 +15,12 @@ from typing import TYPE_CHECKING from pathos.pools import ProcessPool # type: ignore -from pyk.cli.utils import file_path from pyk.cterm import CTerm from pyk.kast.outer import KApply, KRewrite, KSort, KToken from pyk.kcfg import KCFG from pyk.kdist import kdist -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_top, mlOr from pyk.proof import APRProof from pyk.proof.implies import EqualityProof @@ -31,7 +29,17 @@ from pyk.utils import FrozenDict, hash_str, single from . import VERSION, config -from .cli import KEVMCLIArgs, node_id_like +from .cli import ( + KastOptions, + KompileSpecOptions, + ProveLegacyOptions, + ProveOptions, + PruneProofOptions, + RunOptions, + ShowKCFGOptions, + VersionOptions, + ViewKCFGOptions, +) 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 @@ -53,6 +61,8 @@ from pyk.kcfg.kcfg import NodeIdLike from pyk.kcfg.tui import KCFGElem from pyk.kore.rpc import FallbackReason + from pyk.kore.tools import PrintOutput + from pyk.ktool.krun import KRunOutput from pyk.proof.proof import Proof from pyk.utils import BugReport @@ -699,147 +709,19 @@ def parse(s: str) -> list[T]: 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( - '-o', '--output-definition', type=Path, dest='output_dir', help='Path to write kompiled definition to.' - ) - kevm_kompile_spec_args.add_argument( - '--debug-build', dest='debug_build', default=False, 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=False, - action='store_true', - help='Reinitialize CFGs even if they already exist.', - ) - - prune_proof_args = command_parser.add_parser( - 'prune-proof', - 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_proof_args.add_argument('node', type=node_id_like, help='Node to remove CFG subgraph from.') - - 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=False, 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', - default=KRunOutput.PRETTY, - type=KRunOutput, - choices=list(KRunOutput), - ) - run_args.add_argument( - '--expand-macros', - dest='expand_macros', - default=True, - 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', - default=PrintOutput.KORE, - type=PrintOutput, - choices=list(PrintOutput), - ) + command_parser = VersionOptions.parser(command_parser) + command_parser = KompileSpecOptions.parser(command_parser) + command_parser = ProveOptions.parser(command_parser) + command_parser = PruneProofOptions.parser(command_parser) + command_parser = ProveLegacyOptions.parser(command_parser) + command_parser = ViewKCFGOptions.parser(command_parser) + command_parser = ShowKCFGOptions.parser(command_parser) + command_parser = RunOptions.parser(command_parser) + command_parser = KastOptions.parser(command_parser) return parser diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index c5e4ac5fba..7b810b4f3a 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -2,14 +2,30 @@ from argparse import ArgumentParser from functools import cached_property -from typing import TYPE_CHECKING +from pathlib import Path +from typing import TYPE_CHECKING, Any -from pyk.cli.args import KCLIArgs +from pyk.cli.args import ( + BugReportOptions, + DisplayOptions, + KDefinitionOptions, + KompileOptions, + LoggingOptions, + Options, + ParallelOptions, + 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 argparse import _SubParsersAction from collections.abc import Callable from typing import TypeVar @@ -32,316 +48,563 @@ def node_id_like(s: str) -> NodeIdLike: return s -class KEVMCLIArgs(KCLIArgs): - @cached_property - def target_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument('--target', choices=['llvm', 'haskell', 'haskell-standalone', 'foundry']) - return args +class KEVMDisplayOptions(DisplayOptions): + @staticmethod + def default() -> dict[str, Any]: + return {'sort_collections': False} - @cached_property - def k_args(self) -> ArgumentParser: - args = super().definition_args - args.add_argument('--depth', default=None, type=int, help='Maximum depth to execute to.') - return args + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument( + '--sort-collections', + dest='sort_collections', + default=None, + action='store_true', + help='Sort collections before outputting term.', + ) + return parser - @cached_property - def kprove_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( + +class KOptions(KDefinitionOptions): + + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument('--depth', default=None, type=int, help='Maximum depth to execute to.') + return parser + + +class KompileSpecOptions(LoggingOptions, KOptions, KompileOptions): + @staticmethod + def default() -> dict[str, Any]: + return { + 'debug_build': False, + } + + @staticmethod + def parser(base: _SubParsersAction) -> _SubParsersAction: + base.add_parser( + 'kompile-spec', + help='Kompile KEVM specification.', + parents=[KompileSpecOptions.all_args()], + ) + return base + + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument('main_file', type=file_path, help='Path to file with main module.') + parser.add_argument('--target', type=KompileTarget, help='[haskell|maude]') + parser.add_argument( + '-o', '--output-definition', type=Path, dest='output_dir', help='Path to write kompiled definition to.' + ) + parser.add_argument( + '--debug-build', dest='debug_build', default=None, help='Enable debug symbols in LLVM builds.' + ) + return parser + + +class ShowKCFGOptions(LoggingOptions, KOptions, SpecOptions, DisplayOptions): + @staticmethod + def parser(base: _SubParsersAction) -> _SubParsersAction: + base.add_parser( + 'show-kcfg', + help='Print the CFG for a given proof.', + parents=[ShowKCFGOptions.all_args()], + ) + return base + + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument( + '--node', + type=node_id_like, + dest='nodes', + default=[], + action='append', + help='List of nodes to display as well.', + ) + parser.add_argument( + '--node-delta', + type=arg_pair_of(node_id_like, node_id_like), + dest='node_deltas', + default=[], + action='append', + help='List of nodes to display delta for.', + ) + parser.add_argument( + '--failure-information', + dest='failure_info', + default=False, + action='store_true', + help='Show failure summary for cfg', + ) + parser.add_argument( + '--no-failure-information', + dest='failure_info', + action='store_false', + help='Do not show failure summary for cfg', + ) + parser.add_argument( + '--to-module', dest='to_module', default=False, action='store_true', help='Output edges as a K module.' + ) + parser.add_argument( + '--pending', dest='pending', default=False, action='store_true', help='Also display pending nodes' + ) + parser.add_argument( + '--failing', dest='failing', default=False, action='store_true', help='Also display failing nodes' + ) + parser.add_argument( + '--counterexample-information', + dest='counterexample_info', + default=False, + action='store_true', + help="Show models for failing nodes. Should be called with the '--failure-information' flag", + ) + return parser + + +class KProveOptions(Options): + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument( '--debug-equations', type=list_of(str, delim=','), default=[], help='Comma-separate list of equations to debug.', ) - args.add_argument( + parser.add_argument( '--always-check-subsumption', dest='always-check_subsumption', default=True, action='store_true', help='Check subsumption even on non-terminal nodes.', ) - args.add_argument( + parser.add_argument( '--no-always-check-subsumption', dest='always-check_subsumption', action='store_false', help='Do not check subsumption on non-terminal nodes.', ) - args.add_argument( + parser.add_argument( '--fast-check-subsumption', dest='fast_check_subsumption', default=False, action='store_true', help='Use fast-check on k-cell to determine subsumption.', ) - return args - - @cached_property - def kprove_legacy_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( - '--bug-report', - default=False, - action='store_true', - help='Generate a haskell-backend bug report for the execution.', - ) - args.add_argument( - '--debugger', - dest='debugger', - default=False, - action='store_true', - help='Launch proof in an interactive debugger.', - ) - args.add_argument( - '--max-depth', - dest='max_depth', - default=None, - type=int, - help='The maximum number of computational steps to prove.', - ) - args.add_argument( - '--max-counterexamples', - type=int, - dest='max_counterexamples', - default=None, - help='Maximum number of counterexamples reported before a forcible stop.', - ) - args.add_argument( - '--branching-allowed', - type=int, - dest='branching_allowed', - default=None, - help='Number of branching events allowed before a forcible stop.', - ) - args.add_argument( - '--haskell-backend-arg', - dest='haskell_backend_args', - default=[], - action='append', - help='Arguments passed to the Haskell backend execution engine.', - ) - return args - - @cached_property - def evm_chain_args(self) -> ArgumentParser: - schedules = ( - 'DEFAULT', - 'FRONTIER', - 'HOMESTEAD', - 'TANGERINE_WHISTLE', - 'SPURIOUS_DRAGON', - 'BYZANTIUM', - 'CONSTANTINOPLE', - 'PETERSBURG', - 'ISTANBUL', - 'BERLIN', - 'LONDON', - 'MERGE', - 'SHANGHAI', - ) - modes = ('NORMAL', 'VMTESTS') + return parser - args = ArgumentParser(add_help=False) - args.add_argument( - '--schedule', - choices=schedules, - default='SHANGHAI', - help=f"schedule to use for execution [{'|'.join(schedules)}]", - ) - args.add_argument('--chainid', type=int, default=1, help='chain ID to use for execution') - args.add_argument( - '--mode', - choices=modes, - default='NORMAL', - help="execution mode to use [{'|'.join(modes)}]", - ) - args.add_argument( - '--no-gas', action='store_false', dest='usegas', default=True, help='omit gas cost computations' - ) - return args - @cached_property - def display_args(self) -> ArgumentParser: - args = super().display_args - args.add_argument( - '--sort-collections', - dest='sort_collections', - default=False, - action='store_true', - help='Sort collections before outputting term.', - ) - return args - - @cached_property - def rpc_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( +class RPCOptions(Options): + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument( '--trace-rewrites', dest='trace_rewrites', default=False, action='store_true', help='Log traces of all simplification and rewrite rule applications.', ) - args.add_argument( + parser.add_argument( '--kore-rpc-command', dest='kore_rpc_command', type=str, default=None, help='Custom command to start RPC server', ) - args.add_argument( + parser.add_argument( '--use-booster', dest='use_booster', default=False, action='store_true', help='Use the booster RPC server instead of kore-rpc.', ) - args.add_argument( + parser.add_argument( '--fallback-on', dest='fallback_on', type=list_of(FallbackReason, delim=','), help='Comma-separated reasons to fallback from booster to kore, only usable with --use-booster. Options [Branching,Aborted,Stuck].', ) - args.add_argument( + parser.add_argument( '--post-exec-simplify', dest='post_exec_simplify', default=True, action='store_true', help='Always simplify states with kore backend after booster execution, only usable with --use-booster.', ) - args.add_argument( + parser.add_argument( '--no-post-exec-simplify', dest='post_exec_simplify', action='store_false', help='Do not simplify states with kore backend after booster execution, only usable with --use-booster.', ) - args.add_argument( + parser.add_argument( '--interim-simplification', dest='interim_simplification', type=int, help='Max number of steps to execute before applying simplifier to term in booster backend, only usable with --use-booster.', ) - args.add_argument( + parser.add_argument( '--port', dest='port', type=int, default=None, help='Use existing RPC server on named port', ) - args.add_argument( + parser.add_argument( '--maude-port', dest='maude_port', type=int, default=None, help='Use existing Maude RPC server on named port', ) - return args + return parser - @cached_property - def explore_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( + +class ExploreOptions(Options): + + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument( '--break-every-step', dest='break_every_step', default=False, action='store_true', help='Store a node for every EVM opcode step (expensive).', ) - args.add_argument( + parser.add_argument( '--break-on-jumpi', dest='break_on_jumpi', default=False, action='store_true', help='Store a node for every EVM jump opcode.', ) - args.add_argument( + parser.add_argument( '--break-on-calls', dest='break_on_calls', default=False, action='store_true', help='Store a node for every EVM call made.', ) - args.add_argument( + parser.add_argument( '--no-break-on-calls', dest='break_on_calls', default=True, action='store_false', help='Do not store a node for every EVM call made.', ) - args.add_argument( + parser.add_argument( '--break-on-storage', dest='break_on_storage', default=False, action='store_true', help='Store a node for every EVM SSTORE/SLOAD made.', ) - args.add_argument( + parser.add_argument( '--break-on-basic-blocks', dest='break_on_basic_blocks', default=False, action='store_true', help='Store a node for every EVM basic block (implies --break-on-calls).', ) - args.add_argument( + parser.add_argument( '--max-depth', dest='max_depth', default=1000, type=int, help='Maximum number of K steps before the state is saved in a new node in the CFG. Branching will cause this to happen earlier.', ) - args.add_argument( + parser.add_argument( '--max-iterations', dest='max_iterations', default=None, type=int, help='Number of times to expand the next pending node in the CFG.', ) - args.add_argument( + parser.add_argument( '--failure-information', dest='failure_info', default=True, action='store_true', help='Show failure summary for all failing tests', ) - args.add_argument( + parser.add_argument( '--no-failure-information', dest='failure_info', action='store_false', help='Do not show failure summary for failing tests', ) - args.add_argument( + parser.add_argument( '--auto-abstract-gas', dest='auto_abstract_gas', action='store_true', help='Automatically extract gas cell when infinite gas is enabled', ) - args.add_argument( + parser.add_argument( '--counterexample-information', dest='counterexample_info', default=True, action='store_true', help='Show models for failing nodes.', ) - args.add_argument( + parser.add_argument( '--no-counterexample-information', dest='counterexample_info', action='store_false', help='Do not show models for failing nodes.', ) - args.add_argument( + parser.add_argument( '--fail-fast', dest='fail_fast', default=True, action='store_true', help='Stop execution on other branches if a failing node is detected.', ) - args.add_argument( + parser.add_argument( '--no-fail-fast', dest='fail_fast', action='store_false', help='Continue execution on other branches if a failing node is detected.', ) - return args + return parser + + +class ProveOptions( + LoggingOptions, KOptions, ParallelOptions, KProveOptions, BugReportOptions, SMTOptions, ExploreOptions, SpecOptions +): + @staticmethod + def parser(base: _SubParsersAction) -> _SubParsersAction: + base.add_parser( + 'prove', + help='Run KEVM proof.', + parents=[ProveOptions.all_args()], + ) + return base + + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument( + '--reinit', + dest='reinit', + default=False, + action='store_true', + help='Reinitialize CFGs even if they already exist.', + ) + return parser + + +class VersionOptions(LoggingOptions): + @staticmethod + def parser(base: _SubParsersAction) -> _SubParsersAction: + base.add_parser( + 'version', + help='Print KEVM version and exit.', + parents=[VersionOptions.all_args()], + ) + return base + + +class PruneProofOptions(LoggingOptions, KOptions, SpecOptions): + @staticmethod + def parser(base: _SubParsersAction) -> _SubParsersAction: + base.add_parser( + 'prune-proof', + help='Remove a node and its successors from the proof state.', + parents=[PruneProofOptions.all_args()], + ) + return base + + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument('node', type=node_id_like, help='Node to remove CFG subgraph from.') + return parser + + +class KProveLegacyOptions(Options): + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument( + '--bug-report', + default=False, + action='store_true', + help='Generate a haskell-backend bug report for the execution.', + ) + parser.add_argument( + '--debugger', + dest='debugger', + default=False, + action='store_true', + help='Launch proof in an interactive debugger.', + ) + parser.add_argument( + '--max-depth', + dest='max_depth', + default=None, + type=int, + help='The maximum number of computational steps to prove.', + ) + parser.add_argument( + '--max-counterexamples', + type=int, + dest='max_counterexamples', + default=None, + help='Maximum number of counterexamples reported before a forcible stop.', + ) + parser.add_argument( + '--branching-allowed', + type=int, + dest='branching_allowed', + default=None, + help='Number of branching events allowed before a forcible stop.', + ) + parser.add_argument( + '--haskell-backend-arg', + dest='haskell_backend_args', + default=[], + action='append', + help='Arguments passed to the Haskell backend execution engine.', + ) + return parser + + +class ProveLegacyOptions(LoggingOptions, KOptions, SpecOptions, KProveLegacyOptions): + @staticmethod + def parser(base: _SubParsersAction) -> _SubParsersAction: + base.add_parser( + 'prove-legacy', + help='Run KEVM proof using the legacy kprove binary.', + parents=[ProveLegacyOptions.all_args()], + ) + return base + + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument( + '--bug-report-legacy', default=False, action='store_true', help='Generate a legacy bug report.' + ) + return parser + + +class ViewKCFGOptions(LoggingOptions, KOptions, SpecOptions): + @staticmethod + def parser(base: _SubParsersAction) -> _SubParsersAction: + base.add_parser( + 'view-kcfg', + help='Explore a given proof in the KCFG visualizer.', + parents=[ViewKCFGOptions.all_args()], + ) + return base + + +class TargetOptions(Options): + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument('--target', choices=['llvm', 'haskell', 'haskell-standalone', 'foundry']) + return parser + + +class EVMChainOptions(Options): + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + schedules = ( + 'DEFAULT', + 'FRONTIER', + 'HOMESTEAD', + 'TANGERINE_WHISTLE', + 'SPURIOUS_DRAGON', + 'BYZANTIUM', + 'CONSTANTINOPLE', + 'PETERSBURG', + 'ISTANBUL', + 'BERLIN', + 'LONDON', + 'MERGE', + 'SHANGHAI', + ) + modes = ('NORMAL', 'VMTESTS') + + parser.add_argument( + '--schedule', + choices=schedules, + default='SHANGHAI', + help=f"schedule to use for execution [{'|'.join(schedules)}]", + ) + parser.add_argument('--chainid', type=int, default=1, help='chain ID to use for execution') + parser.add_argument( + '--mode', + choices=modes, + default='NORMAL', + help="execution mode to use [{'|'.join(modes)}]", + ) + parser.add_argument( + '--no-gas', action='store_false', dest='usegas', default=True, help='omit gas cost computations' + ) + return parser + + +class RunOptions(LoggingOptions, KOptions, TargetOptions, EVMChainOptions): + @staticmethod + def parser(base: _SubParsersAction) -> _SubParsersAction: + base.add_parser( + 'run', + help='Run KEVM test/simulation.', + parents=[RunOptions.all_args()], + ) + return base + + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument('input_file', type=file_path, help='Path to input file.') + parser.add_argument( + '--output', + default=KRunOutput.PRETTY, + type=KRunOutput, + choices=list(KRunOutput), + ) + parser.add_argument( + '--expand-macros', + dest='expand_macros', + default=True, + action='store_true', + help='Expand macros on the input term before execution.', + ) + parser.add_argument( + '--no-expand-macros', + dest='expand_macros', + action='store_false', + help='Do not expand macros on the input term before execution.', + ) + parser.add_argument( + '--debugger', + dest='debugger', + action='store_true', + help='Run GDB debugger for execution.', + ) + return parser + + +class KastOptions(LoggingOptions, TargetOptions, EVMChainOptions, KOptions): + @staticmethod + def parser(base: _SubParsersAction) -> _SubParsersAction: + base.add_parser( + 'kast', + help='Run KEVM program.', + parents=[KastOptions.all_args()], + ) + return base + + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument('input_file', type=file_path, help='Path to input file.') + parser.add_argument( + '--output', + default=PrintOutput.KORE, + type=PrintOutput, + choices=list(PrintOutput), + ) + return parser + + +class KEVMCLIArgs: @cached_property def k_gen_args(self) -> ArgumentParser: @@ -361,53 +624,3 @@ def k_gen_args(self) -> ArgumentParser: help='Extra modules to import into generated main module.', ) return args - - @cached_property - def kcfg_show_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( - '--node', - type=node_id_like, - dest='nodes', - default=[], - action='append', - help='List of nodes to display as well.', - ) - args.add_argument( - '--node-delta', - type=arg_pair_of(node_id_like, node_id_like), - dest='node_deltas', - default=[], - action='append', - help='List of nodes to display delta for.', - ) - args.add_argument( - '--failure-information', - dest='failure_info', - default=False, - action='store_true', - help='Show failure summary for cfg', - ) - args.add_argument( - '--no-failure-information', - dest='failure_info', - action='store_false', - help='Do not show failure summary for cfg', - ) - args.add_argument( - '--to-module', dest='to_module', default=False, action='store_true', help='Output edges as a K module.' - ) - args.add_argument( - '--pending', dest='pending', default=False, action='store_true', help='Also display pending nodes' - ) - args.add_argument( - '--failing', dest='failing', default=False, action='store_true', help='Also display failing nodes' - ) - args.add_argument( - '--counterexample-information', - dest='counterexample_info', - default=False, - action='store_true', - help="Show models for failing nodes. Should be called with the '--failure-information' flag", - ) - return args diff --git a/kevm-pyk/src/kevm_pyk/gst_to_kore.py b/kevm-pyk/src/kevm_pyk/gst_to_kore.py index fa7f92447c..95c1a6fd9b 100644 --- a/kevm-pyk/src/kevm_pyk/gst_to_kore.py +++ b/kevm-pyk/src/kevm_pyk/gst_to_kore.py @@ -10,7 +10,7 @@ from pyk.kore.prelude import BOOL, INT, SORT_JSON, SORT_K_ITEM, bool_dv, inj, int_dv, json_to_kore, top_cell_initializer from pyk.kore.syntax import App, SortApp -from .cli import KEVMCLIArgs +from .cli import EVMChainOptions if TYPE_CHECKING: from argparse import Namespace @@ -67,10 +67,10 @@ def _exec_gst_to_kore(input_file: Path, schedule: str, mode: str, chainid: int, def _parse_args() -> Namespace: - kevm_cli_args = KEVMCLIArgs() + EVMChainOptions.all_args() parser = ArgumentParser( description='Convert a GeneralStateTest to Kore for compsumption by KEVM', - parents=[kevm_cli_args.evm_chain_args], + parents=[EVMChainOptions.all_args()], ) parser.add_argument('input_file', type=file_path, help='path to GST') return parser.parse_args() From 07d1191f515b97c41211659fb7d24bbc32797c8c Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Wed, 28 Feb 2024 18:05:15 -0600 Subject: [PATCH 02/28] Add type hints and default values --- kevm-pyk/src/kevm_pyk/cli.py | 218 +++++++++++++++++++++++++++++------ 1 file changed, 185 insertions(+), 33 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 7b810b4f3a..881b288451 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -49,6 +49,8 @@ def node_id_like(s: str) -> NodeIdLike: class KEVMDisplayOptions(DisplayOptions): + sort_collections: bool + @staticmethod def default() -> dict[str, Any]: return {'sort_collections': False} @@ -66,6 +68,11 @@ def args(parser: ArgumentParser) -> ArgumentParser: class KOptions(KDefinitionOptions): + depth: int | None + + @staticmethod + def default() -> dict[str, Any]: + return {'depth': None} @staticmethod def args(parser: ArgumentParser) -> ArgumentParser: @@ -74,6 +81,11 @@ def args(parser: ArgumentParser) -> ArgumentParser: class KompileSpecOptions(LoggingOptions, KOptions, KompileOptions): + main_file: Path + target: KompileTarget + output_dir: Path + debug_build: bool + @staticmethod def default() -> dict[str, Any]: return { @@ -103,6 +115,14 @@ def args(parser: ArgumentParser) -> ArgumentParser: class ShowKCFGOptions(LoggingOptions, KOptions, SpecOptions, DisplayOptions): + nodes: list[NodeIdLike] + node_deltas: list[tuple[NodeIdLike, NodeIdLike]] + failure_info: bool + to_module: bool + pending: bool + failing: bool + counterexample_info: bool + @staticmethod def parser(base: _SubParsersAction) -> _SubParsersAction: base.add_parser( @@ -112,6 +132,16 @@ def parser(base: _SubParsersAction) -> _SubParsersAction: ) return base + @staticmethod + def default() -> dict[str, Any]: + return { + 'failure_info': False, + 'to_module': False, + 'pending': False, + 'failing': False, + 'counterexample_info': False, + } + @staticmethod def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( @@ -133,7 +163,7 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--failure-information', dest='failure_info', - default=False, + default=None, action='store_true', help='Show failure summary for cfg', ) @@ -144,18 +174,18 @@ def args(parser: ArgumentParser) -> ArgumentParser: help='Do not show failure summary for cfg', ) parser.add_argument( - '--to-module', dest='to_module', default=False, action='store_true', help='Output edges as a K module.' + '--to-module', dest='to_module', default=None, action='store_true', help='Output edges as a K module.' ) parser.add_argument( - '--pending', dest='pending', default=False, action='store_true', help='Also display pending nodes' + '--pending', dest='pending', default=None, action='store_true', help='Also display pending nodes' ) parser.add_argument( - '--failing', dest='failing', default=False, action='store_true', help='Also display failing nodes' + '--failing', dest='failing', default=None, action='store_true', help='Also display failing nodes' ) parser.add_argument( '--counterexample-information', dest='counterexample_info', - default=False, + default=None, action='store_true', help="Show models for failing nodes. Should be called with the '--failure-information' flag", ) @@ -163,6 +193,17 @@ def args(parser: ArgumentParser) -> ArgumentParser: class KProveOptions(Options): + debug_equations: list[str] + always_check_subsumption: bool + fast_check_subsumption: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'always_check_subsumption': True, + 'fast_check_subsumption': False, + } + @staticmethod def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( @@ -173,21 +214,21 @@ def args(parser: ArgumentParser) -> ArgumentParser: ) parser.add_argument( '--always-check-subsumption', - dest='always-check_subsumption', - default=True, + dest='always_check_subsumption', + default=None, action='store_true', help='Check subsumption even on non-terminal nodes.', ) parser.add_argument( '--no-always-check-subsumption', - dest='always-check_subsumption', + dest='always_check_subsumption', action='store_false', help='Do not check subsumption on non-terminal nodes.', ) parser.add_argument( '--fast-check-subsumption', dest='fast_check_subsumption', - default=False, + default=None, action='store_true', help='Use fast-check on k-cell to determine subsumption.', ) @@ -195,12 +236,29 @@ def args(parser: ArgumentParser) -> ArgumentParser: class RPCOptions(Options): + trace_rewrites: bool + kore_rpc_command: str + use_booster: bool + fallback_on: list[FallbackReason] + post_exec_simplify: bool + interim_simplification: int + port: int | None + maude_port: int | None + + @staticmethod + def default() -> dict[str, Any]: + return { + 'trace_rewrites': False, + 'use_booster': False, + 'post_exec_simplify': True, + } + @staticmethod def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--trace-rewrites', dest='trace_rewrites', - default=False, + default=None, action='store_true', help='Log traces of all simplification and rewrite rule applications.', ) @@ -214,7 +272,7 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--use-booster', dest='use_booster', - default=False, + default=None, action='store_true', help='Use the booster RPC server instead of kore-rpc.', ) @@ -227,7 +285,7 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--post-exec-simplify', dest='post_exec_simplify', - default=True, + default=None, action='store_true', help='Always simplify states with kore backend after booster execution, only usable with --use-booster.', ) @@ -261,55 +319,80 @@ def args(parser: ArgumentParser) -> ArgumentParser: class ExploreOptions(Options): + break_every_step: bool + break_on_jumpi: bool + break_on_calls: bool + break_on_storage: bool + break_on_basic_blocks: bool + max_depth: int + max_iterations: int | None + failure_info: bool + auto_abstract_gas: bool + counterexample_info: bool + fail_fast: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'break_every_step': False, + 'break_on_jumpi': False, + 'break_on_calls': False, + 'break_on_storage': False, + 'break_on_basic_blocks': False, + 'max_depth': 1000, + 'failure_info': True, + 'counterexample_info': True, + 'fail_fast': True, + } @staticmethod def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--break-every-step', dest='break_every_step', - default=False, + default=None, action='store_true', help='Store a node for every EVM opcode step (expensive).', ) parser.add_argument( '--break-on-jumpi', dest='break_on_jumpi', - default=False, + default=None, action='store_true', help='Store a node for every EVM jump opcode.', ) parser.add_argument( '--break-on-calls', dest='break_on_calls', - default=False, + default=None, action='store_true', help='Store a node for every EVM call made.', ) parser.add_argument( '--no-break-on-calls', dest='break_on_calls', - default=True, + default=None, action='store_false', help='Do not store a node for every EVM call made.', ) parser.add_argument( '--break-on-storage', dest='break_on_storage', - default=False, + default=None, action='store_true', help='Store a node for every EVM SSTORE/SLOAD made.', ) parser.add_argument( '--break-on-basic-blocks', dest='break_on_basic_blocks', - default=False, + default=None, action='store_true', help='Store a node for every EVM basic block (implies --break-on-calls).', ) parser.add_argument( '--max-depth', dest='max_depth', - default=1000, + default=None, type=int, help='Maximum number of K steps before the state is saved in a new node in the CFG. Branching will cause this to happen earlier.', ) @@ -323,7 +406,7 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--failure-information', dest='failure_info', - default=True, + default=None, action='store_true', help='Show failure summary for all failing tests', ) @@ -342,7 +425,7 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--counterexample-information', dest='counterexample_info', - default=True, + default=None, action='store_true', help='Show models for failing nodes.', ) @@ -355,7 +438,7 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--fail-fast', dest='fail_fast', - default=True, + default=None, action='store_true', help='Stop execution on other branches if a failing node is detected.', ) @@ -371,6 +454,14 @@ def args(parser: ArgumentParser) -> ArgumentParser: class ProveOptions( LoggingOptions, KOptions, ParallelOptions, KProveOptions, BugReportOptions, SMTOptions, ExploreOptions, SpecOptions ): + reinit: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'reinit': False, + } + @staticmethod def parser(base: _SubParsersAction) -> _SubParsersAction: base.add_parser( @@ -385,7 +476,7 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--reinit', dest='reinit', - default=False, + default=None, action='store_true', help='Reinitialize CFGs even if they already exist.', ) @@ -404,6 +495,8 @@ def parser(base: _SubParsersAction) -> _SubParsersAction: class PruneProofOptions(LoggingOptions, KOptions, SpecOptions): + node: NodeIdLike + @staticmethod def parser(base: _SubParsersAction) -> _SubParsersAction: base.add_parser( @@ -420,18 +513,32 @@ def args(parser: ArgumentParser) -> ArgumentParser: class KProveLegacyOptions(Options): + bug_report: bool + debugger: bool + max_depth: int | None + max_counterexamples: int | None + branching_allowed: int | None + haskell_backend_args: list[str] + + @staticmethod + def default() -> dict[str, Any]: + return { + 'bug_report': False, + 'debugger': False, + } + @staticmethod def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--bug-report', - default=False, + default=None, action='store_true', help='Generate a haskell-backend bug report for the execution.', ) parser.add_argument( '--debugger', dest='debugger', - default=False, + default=None, action='store_true', help='Launch proof in an interactive debugger.', ) @@ -467,6 +574,14 @@ def args(parser: ArgumentParser) -> ArgumentParser: class ProveLegacyOptions(LoggingOptions, KOptions, SpecOptions, KProveLegacyOptions): + bug_report_legacy: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'bug_report_legacy': False, + } + @staticmethod def parser(base: _SubParsersAction) -> _SubParsersAction: base.add_parser( @@ -479,7 +594,7 @@ def parser(base: _SubParsersAction) -> _SubParsersAction: @staticmethod def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( - '--bug-report-legacy', default=False, action='store_true', help='Generate a legacy bug report.' + '--bug-report-legacy', default=None, action='store_true', help='Generate a legacy bug report.' ) return parser @@ -496,6 +611,8 @@ def parser(base: _SubParsersAction) -> _SubParsersAction: class TargetOptions(Options): + target: str + @staticmethod def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument('--target', choices=['llvm', 'haskell', 'haskell-standalone', 'foundry']) @@ -503,6 +620,20 @@ def args(parser: ArgumentParser) -> ArgumentParser: class EVMChainOptions(Options): + schedule: str + chainid: int + mode: str + usegas: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'schedule': 'SHANGHAI', + 'chainid': 1, + 'mode': 'NORMAL', + 'usegas': False, + } + @staticmethod def args(parser: ArgumentParser) -> ArgumentParser: schedules = ( @@ -525,23 +656,35 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--schedule', choices=schedules, - default='SHANGHAI', + default=None, help=f"schedule to use for execution [{'|'.join(schedules)}]", ) - parser.add_argument('--chainid', type=int, default=1, help='chain ID to use for execution') + parser.add_argument('--chainid', type=int, default=None, help='chain ID to use for execution') parser.add_argument( '--mode', choices=modes, - default='NORMAL', + default=None, help="execution mode to use [{'|'.join(modes)}]", ) parser.add_argument( - '--no-gas', action='store_false', dest='usegas', default=True, help='omit gas cost computations' + '--no-gas', action='store_false', dest='usegas', default=None, help='omit gas cost computations' ) return parser class RunOptions(LoggingOptions, KOptions, TargetOptions, EVMChainOptions): + input_file: Path + output: KRunOutput + expand_macros: bool + debugger: bool + + @staticmethod + def default() -> dict[str, Any]: + return { + 'output': KRunOutput.PRETTY, + 'expand_macros': True, + } + @staticmethod def parser(base: _SubParsersAction) -> _SubParsersAction: base.add_parser( @@ -556,14 +699,14 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument('input_file', type=file_path, help='Path to input file.') parser.add_argument( '--output', - default=KRunOutput.PRETTY, + default=None, type=KRunOutput, choices=list(KRunOutput), ) parser.add_argument( '--expand-macros', dest='expand_macros', - default=True, + default=None, action='store_true', help='Expand macros on the input term before execution.', ) @@ -583,6 +726,15 @@ def args(parser: ArgumentParser) -> ArgumentParser: class KastOptions(LoggingOptions, TargetOptions, EVMChainOptions, KOptions): + input_file: Path + output: PrintOutput + + @staticmethod + def default() -> dict[str, Any]: + return { + 'output': PrintOutput.KORE, + } + @staticmethod def parser(base: _SubParsersAction) -> _SubParsersAction: base.add_parser( @@ -597,7 +749,7 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument('input_file', type=file_path, help='Path to input file.') parser.add_argument( '--output', - default=PrintOutput.KORE, + default=None, type=PrintOutput, choices=list(PrintOutput), ) From 80f5f468bb2085be13b60a292595d0e78c6a70e8 Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Wed, 28 Feb 2024 19:04:18 -0600 Subject: [PATCH 03/28] Start applying options to exec functions --- kevm-pyk/src/kevm_pyk/__main__.py | 133 +++++++++++++----------------- kevm-pyk/src/kevm_pyk/cli.py | 27 ++++++ 2 files changed, 83 insertions(+), 77 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index f7516f9efb..d4d46fd378 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -39,6 +39,7 @@ ShowKCFGOptions, VersionOptions, ViewKCFGOptions, + generate_command_options, ) from .gst_to_kore import SORT_ETHEREUM_SIMULATION, gst_to_kore, kore_pgm_to_kore from .kevm import KEVM, KEVMSemantics, kevm_node_printer @@ -84,120 +85,98 @@ def main() -> None: parser = _create_argument_parser() args = parser.parse_args() logging.basicConfig(level=_loglevel(args), format=_LOG_FORMAT) + options = generate_command_options({key: val for (key, val) in vars(args).items() if val is not None}) executor_name = 'exec_' + args.command.lower().replace('-', '_') if executor_name not in globals(): raise AssertionError(f'Unimplemented command: {args.command}') execute = globals()[executor_name] - execute(**vars(args)) + execute(options) # Command implementation -def exec_version(**kwargs: Any) -> None: +def exec_version(options: VersionOptions) -> None: print(f'KEVM Version: {VERSION}') -def exec_kompile_spec( - output_dir: Path | None, - main_file: Path, - emit_json: bool, - includes: list[str], - main_module: str | None, - syntax_module: str | None, - target: KompileTarget | None = None, - read_only: bool = False, - ccopts: Iterable[str] = (), - o0: bool = False, - o1: bool = False, - o2: bool = False, - o3: bool = False, - enable_llvm_debug: bool = False, - llvm_library: bool = False, - debug_build: bool = False, - debug: bool = False, - verbose: bool = False, - **kwargs: Any, -) -> None: - if target is None: - target = KompileTarget.HASKELL - - if target not in [KompileTarget.HASKELL, KompileTarget.MAUDE]: - raise ValueError(f'Can only call kevm kompile-spec with --target [haskell,maude], got: {target.value}') - - output_dir = output_dir or Path() +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}') optimization = 0 - if o1: + if options.o1: optimization = 1 - if o2: + if options.o2: optimization = 2 - if o3: + if options.o3: optimization = 3 - if debug_build: + if options.debug_build: optimization = 0 kevm_kompile( - target, - output_dir=output_dir, - main_file=main_file, - main_module=main_module, - syntax_module=syntax_module, - includes=includes, - emit_json=emit_json, - read_only=read_only, - ccopts=ccopts, + options.target, + output_dir=options.output_dir, + main_file=options.main_file, + main_module=options.main_module, + syntax_module=options.syntax_module, + includes=options.includes, + emit_json=options.emit_json, + read_only=options.read_only, + ccopts=options.ccopts, optimization=optimization, - enable_llvm_debug=enable_llvm_debug, - llvm_kompile_type=LLVMKompileType.C if llvm_library else LLVMKompileType.MAIN, - debug_build=debug_build, - debug=debug, - verbose=verbose, + enable_llvm_debug=options.enable_llvm_debug, + llvm_kompile_type=LLVMKompileType.C if options.llvm_library else LLVMKompileType.MAIN, + debug_build=options.debug_build, + debug=options.debug, + verbose=options.verbose, ) def exec_prove_legacy( - spec_file: Path, - definition_dir: Path | None = None, - includes: Iterable[str] = (), - bug_report_legacy: bool = False, - save_directory: Path | None = None, - spec_module: str | None = None, - claim_labels: Iterable[str] | None = None, - exclude_claim_labels: Iterable[str] = (), - debug: bool = False, - debugger: bool = False, - max_depth: int | None = None, - max_counterexamples: int | None = None, - branching_allowed: int | None = None, - haskell_backend_args: Iterable[str] = (), - **kwargs: Any, + options: ProveLegacyOptions, + # spec_file: Path, + # definition_dir: Path | None = None, + # includes: Iterable[str] = (), + # bug_report_legacy: bool = False, + # save_directory: Path | None = None, + # spec_module: str | None = None, + # claim_labels: Iterable[str] | None = None, + # exclude_claim_labels: Iterable[str] = (), + # debug: bool = False, + # debugger: bool = False, + # max_depth: int | None = None, + # max_counterexamples: int | None = None, + # branching_allowed: int | None = None, + # haskell_backend_args: Iterable[str] = (), + # **kwargs: Any, ) -> None: - _ignore_arg(kwargs, 'md_selector', f'--md-selector: {kwargs["md_selector"]}') + # _ignore_arg(kwargs, 'md_selector', f'--md-selector: {kwargs["md_selector"]}') + definition_dir = options.definition_dir if definition_dir is None: definition_dir = kdist.get('evm-semantics.haskell') - kevm = KEVM(definition_dir, use_directory=save_directory) + kevm = KEVM(definition_dir, use_directory=options.save_directory) - include_dirs = [Path(include) for include in includes] + include_dirs = [Path(include) for include in options.includes] include_dirs += config.INCLUDE_DIRS final_state = kevm.prove_legacy( - spec_file=spec_file, + spec_file=options.spec_file, includes=include_dirs, - bug_report=bug_report_legacy, - spec_module=spec_module, - claim_labels=claim_labels, - exclude_claim_labels=exclude_claim_labels, - debug=debug, - debugger=debugger, - max_depth=max_depth, - max_counterexamples=max_counterexamples, - branching_allowed=branching_allowed, - haskell_backend_args=haskell_backend_args, + bug_report=options.bug_report_legacy, + spec_module=options.spec_module, + claim_labels=options.claim_labels, + exclude_claim_labels=options.exclude_claim_labels, + debug=options.debug, + debugger=options.debugger, + max_depth=options.max_depth, + max_counterexamples=options.max_counterexamples, + branching_allowed=options.branching_allowed, + haskell_backend_args=options.haskell_backend_args, ) final_kast = mlOr([state.kast for state in final_state]) print(kevm.pretty_print(final_kast)) diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 881b288451..871647f712 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -48,6 +48,31 @@ def node_id_like(s: str) -> NodeIdLike: return s +def generate_command_options(args: dict[str, Any]) -> LoggingOptions: + command = args['command'].lower() + match command: + case 'version': + return VersionOptions(args) + case 'kompile-spec': + return KompileSpecOptions(args) + case 'prove': + return ProveOptions(args) + case 'prune-proof': + return PruneProofOptions(args) + case 'prove-legacy': + return ProveLegacyOptions(args) + case 'view-kcfg': + return ViewKCFGOptions(args) + case 'show-kcfg': + return ShowKCFGOptions(args) + case 'run': + return RunOptions(args) + case 'kast': + return KastOptions(args) + case _: + raise ValueError('Unrecognized command.') + + class KEVMDisplayOptions(DisplayOptions): sort_collections: bool @@ -90,6 +115,8 @@ class KompileSpecOptions(LoggingOptions, KOptions, KompileOptions): def default() -> dict[str, Any]: return { 'debug_build': False, + 'output_dir': Path(), + 'target': KompileTarget.HASKELL, } @staticmethod From a883f0f2ec7d636813ba08415ce41a53f3f1f538 Mon Sep 17 00:00:00 2001 From: devops <devops@runtimeverification.com> Date: Thu, 29 Feb 2024 01:07:30 +0000 Subject: [PATCH 04/28] Set Version: 1.0.467 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 8f2746b668..2123f2e67a 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.466" +version = "1.0.467" description = "" authors = [ "Runtime Verification, Inc. <contact@runtimeverification.com>", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index ac5494b695..d6207a4caf 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.466' +VERSION: Final = '1.0.467' diff --git a/package/version b/package/version index 9c52351c13..168ef9f3e5 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.466 +1.0.467 From e19a8dc442df0bde4b85d3d5c641752ea0903104 Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Thu, 29 Feb 2024 15:18:10 -0600 Subject: [PATCH 05/28] Add some missing default options --- kevm-pyk/src/kevm_pyk/cli.py | 20 ++++++++++++++++++-- 1 file changed, 18 insertions(+), 2 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 871647f712..2be249ef2d 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -264,11 +264,11 @@ def args(parser: ArgumentParser) -> ArgumentParser: class RPCOptions(Options): trace_rewrites: bool - kore_rpc_command: str + kore_rpc_command: str | None use_booster: bool fallback_on: list[FallbackReason] post_exec_simplify: bool - interim_simplification: int + interim_simplification: int | None port: int | None maude_port: int | None @@ -278,6 +278,10 @@ def default() -> dict[str, Any]: 'trace_rewrites': False, 'use_booster': False, 'post_exec_simplify': True, + 'kore_rpc_command': None, + 'interim_simplification': None, + 'port': None, + 'maude_port': None, } @staticmethod @@ -370,6 +374,8 @@ def default() -> dict[str, Any]: 'failure_info': True, 'counterexample_info': True, 'fail_fast': True, + 'max_iterations': None, + 'auto_abstract_gas': False, } @staticmethod @@ -552,6 +558,9 @@ def default() -> dict[str, Any]: return { 'bug_report': False, 'debugger': False, + 'max_depth': None, + 'max_counterexamples': None, + 'branching_allowed': None, } @staticmethod @@ -640,6 +649,12 @@ def parser(base: _SubParsersAction) -> _SubParsersAction: class TargetOptions(Options): target: str + @staticmethod + def default() -> dict[str, Any]: + return { + 'target': 'haskell', + } + @staticmethod def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument('--target', choices=['llvm', 'haskell', 'haskell-standalone', 'foundry']) @@ -710,6 +725,7 @@ def default() -> dict[str, Any]: return { 'output': KRunOutput.PRETTY, 'expand_macros': True, + 'debugger': False, } @staticmethod From 3803e04940763c013a478eeefba4392dd6d1566a Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Thu, 29 Feb 2024 15:18:23 -0600 Subject: [PATCH 06/28] Add some missing default options --- kevm-pyk/pyproject.toml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 8f2746b668..d5b0dec493 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -13,7 +13,8 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -pyk = { git = "https://github.com/runtimeverification/pyk.git", branch="noah/default-options" } +# pyk = { git = "https://github.com/runtimeverification/pyk.git", branch="noah/default-options" } +pyk = { path = "/home/noah/dev/pyk", develop=true } tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] From 242a7204c899ecb6d107672e187ef4be7d50f1c4 Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Thu, 29 Feb 2024 17:10:08 -0600 Subject: [PATCH 07/28] Integrate with the rest of the command exec functions --- kevm-pyk/src/kevm_pyk/__main__.py | 350 +++++++------------ kevm-pyk/src/kevm_pyk/cli.py | 22 +- kevm-pyk/src/tests/integration/test_prove.py | 26 +- 3 files changed, 149 insertions(+), 249 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index d4d46fd378..40b6239201 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -59,13 +59,8 @@ 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.kore.rpc import FallbackReason - from pyk.kore.tools import PrintOutput - from pyk.ktool.krun import KRunOutput from pyk.proof.proof import Proof - from pyk.utils import BugReport T = TypeVar('T') @@ -135,26 +130,7 @@ def exec_kompile_spec(options: KompileSpecOptions) -> None: ) -def exec_prove_legacy( - options: ProveLegacyOptions, - # spec_file: Path, - # definition_dir: Path | None = None, - # includes: Iterable[str] = (), - # bug_report_legacy: bool = False, - # save_directory: Path | None = None, - # spec_module: str | None = None, - # claim_labels: Iterable[str] | None = None, - # exclude_claim_labels: Iterable[str] = (), - # debug: bool = False, - # debugger: bool = False, - # max_depth: int | None = None, - # max_counterexamples: int | None = None, - # branching_allowed: int | None = None, - # haskell_backend_args: Iterable[str] = (), - # **kwargs: Any, -) -> None: - # _ignore_arg(kwargs, 'md_selector', f'--md-selector: {kwargs["md_selector"]}') - +def exec_prove_legacy(options: ProveLegacyOptions) -> None: definition_dir = options.definition_dir if definition_dir is None: definition_dir = kdist.get('evm-semantics.haskell') @@ -261,64 +237,26 @@ def get_or_load_claim_job(claim_label: str) -> KClaimJob: return frozenset({get_or_load_claim_job(claim.label) for claim in claims}) -def exec_prove( - spec_file: Path, - includes: Iterable[str], - definition_dir: Path | None = None, - bug_report: BugReport | None = None, - save_directory: Path | None = None, - spec_module: str | None = None, - claim_labels: Iterable[str] | None = None, - exclude_claim_labels: Iterable[str] = (), - reinit: bool = False, - max_depth: int = 1000, - max_iterations: int | None = None, - workers: int = 1, - break_every_step: bool = False, - break_on_jumpi: bool = False, - break_on_calls: bool = False, - break_on_storage: bool = False, - break_on_basic_blocks: bool = False, - kore_rpc_command: str | Iterable[str] | None = None, - use_booster: bool = False, - smt_timeout: int | None = None, - smt_retry_limit: int | None = None, - trace_rewrites: bool = False, - failure_info: bool = True, - auto_abstract_gas: bool = False, - fail_fast: bool = False, - always_check_subsumption: bool = True, - fast_check_subsumption: bool = False, - fallback_on: Iterable[FallbackReason] | None = None, - interim_simplification: int | None = None, - post_exec_simplify: bool = True, - **kwargs: Any, -) -> None: - _ignore_arg(kwargs, 'md_selector', f'--md-selector: {kwargs["md_selector"]}') +def exec_prove(options: ProveOptions) -> None: md_selector = 'k' - if save_directory is None: - save_directory = Path(tempfile.mkdtemp()) - + save_directory = options.save_directory if options.save_directory is not None else Path(tempfile.mkdtemp()) digest_file = save_directory / 'digest' - if definition_dir is None: - definition_dir = kdist.get('evm-semantics.haskell') - - if smt_timeout is None: - smt_timeout = 300 - if smt_retry_limit is None: - smt_retry_limit = 10 + definition_dir = ( + options.definition_dir if options.definition_dir is not None else kdist.get('evm-semantics.haskell') + ) - kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=bug_report) + kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=options.bug_report) - include_dirs = [Path(include) for include in includes] + include_dirs = [Path(include) for include in options.includes] include_dirs += config.INCLUDE_DIRS - if kore_rpc_command is None: - kore_rpc_command = ('kore-rpc-booster',) if use_booster else ('kore-rpc',) - elif isinstance(kore_rpc_command, str): - kore_rpc_command = kore_rpc_command.split() + kore_rpc_command: Iterable[str] + if options.kore_rpc_command is None: + kore_rpc_command = ('kore-rpc-booster',) if options.use_booster else ('kore-rpc',) + elif isinstance(options.kore_rpc_command, str): + kore_rpc_command = options.kore_rpc_command.split() def is_functional(claim: KClaim) -> bool: claim_lhs = claim.body @@ -326,20 +264,22 @@ def is_functional(claim: KClaim) -> bool: claim_lhs = claim_lhs.lhs return not (type(claim_lhs) is KApply and claim_lhs.label.name == '<generatedTop>') - llvm_definition_dir = definition_dir / 'llvm-library' if use_booster else None + llvm_definition_dir = definition_dir / 'llvm-library' if options.use_booster else None - _LOGGER.info(f'Extracting claims from file: {spec_file}') + _LOGGER.info(f'Extracting claims from file: {options.spec_file}') all_claims = kevm.get_claims( - spec_file, - spec_module_name=spec_module, + options.spec_file, + spec_module_name=options.spec_module, include_dirs=include_dirs, md_selector=md_selector, - claim_labels=claim_labels, - exclude_claim_labels=exclude_claim_labels, + claim_labels=options.claim_labels, + exclude_claim_labels=options.exclude_claim_labels, ) if all_claims is None: - raise ValueError(f'No claims found in file: {spec_file}') - spec_module_name = spec_module if spec_module is not None else os.path.splitext(spec_file.name)[0].upper() + raise ValueError(f'No claims found in file: {options.spec_file}') + spec_module_name = ( + options.spec_module if options.spec_module is not None else os.path.splitext(options.spec_file.name)[0].upper() + ) all_claim_jobs = init_claim_jobs(spec_module_name, all_claims) all_claim_jobs_by_label = {c.claim.label: c for c in all_claim_jobs} claims_graph = claim_dependency_dict(all_claims, spec_module_name=spec_module_name) @@ -354,26 +294,26 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]: claim_job.update_digest(digest_file) with legacy_explore( kevm, - kcfg_semantics=KEVMSemantics(auto_abstract_gas=auto_abstract_gas), + kcfg_semantics=KEVMSemantics(auto_abstract_gas=options.auto_abstract_gas), id=claim.label, llvm_definition_dir=llvm_definition_dir, - bug_report=bug_report, + bug_report=options.bug_report, kore_rpc_command=kore_rpc_command, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - trace_rewrites=trace_rewrites, - fallback_on=fallback_on, - interim_simplification=interim_simplification, - no_post_exec_simplify=(not post_exec_simplify), + smt_timeout=options.smt_timeout, + smt_retry_limit=options.smt_retry_limit, + trace_rewrites=options.trace_rewrites, + fallback_on=options.fallback_on, + interim_simplification=options.interim_simplification, + no_post_exec_simplify=(not options.post_exec_simplify), ) as kcfg_explore: proof_problem: Proof if is_functional(claim): - if not reinit and up_to_date and EqualityProof.proof_exists(claim.label, save_directory): + if not options.reinit and up_to_date and EqualityProof.proof_exists(claim.label, save_directory): proof_problem = EqualityProof.read_proof_data(save_directory, claim.label) else: proof_problem = EqualityProof.from_claim(claim, kevm.definition, proof_dir=save_directory) else: - if not reinit and up_to_date and APRProof.proof_data_exists(claim.label, save_directory): + if not options.reinit and up_to_date and APRProof.proof_data_exists(claim.label, save_directory): proof_problem = APRProof.read_proof_data(save_directory, claim.label) else: @@ -418,15 +358,18 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]: passed = run_prover( proof_problem, kcfg_explore, - max_depth=max_depth, - max_iterations=max_iterations, + max_depth=options.max_depth, + max_iterations=options.max_iterations, cut_point_rules=KEVMSemantics.cut_point_rules( - break_on_jumpi, break_on_calls, break_on_storage, break_on_basic_blocks + options.break_on_jumpi, + options.break_on_calls, + options.break_on_storage, + options.break_on_basic_blocks, ), - terminal_rules=KEVMSemantics.terminal_rules(break_every_step), - fail_fast=fail_fast, - always_check_subsumption=always_check_subsumption, - fast_check_subsumption=fast_check_subsumption, + terminal_rules=KEVMSemantics.terminal_rules(options.break_every_step), + fail_fast=options.fail_fast, + always_check_subsumption=options.always_check_subsumption, + fast_check_subsumption=options.fast_check_subsumption, ) end_time = time.time() _LOGGER.info(f'Proof timing {proof_problem.id}: {end_time - start_time}s') @@ -438,7 +381,7 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]: topological_sorter = graphlib.TopologicalSorter(claims_graph) topological_sorter.prepare() - with wrap_process_pool(workers=workers) as process_pool: + with wrap_process_pool(workers=options.workers) as process_pool: selected_results: list[tuple[bool, list[str] | None]] = [] selected_claims = [] while topological_sorter.is_active(): @@ -459,7 +402,7 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]: else: failed += 1 print(f'PROOF FAILED: {job.claim.label}') - if failure_info and failure_log is not None: + if options.failure_info and failure_log is not None: for line in failure_log: print(line) @@ -467,84 +410,61 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]: sys.exit(failed) -def exec_prune_proof( - definition_dir: Path, - spec_file: Path, - node: NodeIdLike, - includes: Iterable[str] = (), - save_directory: Path | None = None, - spec_module: str | None = None, - claim_labels: Iterable[str] | None = None, - exclude_claim_labels: Iterable[str] = (), - **kwargs: Any, -) -> None: - _ignore_arg(kwargs, 'md_selector', f'--md-selector: {kwargs["md_selector"]}') +def exec_prune_proof(options: PruneProofOptions) -> None: md_selector = 'k' - if save_directory is None: + if options.save_directory is None: raise ValueError('Must pass --save-directory to prune-proof!') - _LOGGER.warning(f'definition_dir: {definition_dir}') - kevm = KEVM(definition_dir, use_directory=save_directory) + if options.definition_dir is None: + raise ValueError('Must pass --definition to prune-proof!') + + kevm = KEVM(options.definition_dir, use_directory=options.save_directory) - include_dirs = [Path(include) for include in includes] + include_dirs = [Path(include) for include in options.includes] include_dirs += config.INCLUDE_DIRS - _LOGGER.info(f'Extracting claims from file: {spec_file}') + _LOGGER.info(f'Extracting claims from file: {options.spec_file}') claim = single( kevm.get_claims( - spec_file, - spec_module_name=spec_module, + options.spec_file, + spec_module_name=options.spec_module, include_dirs=include_dirs, md_selector=md_selector, - claim_labels=claim_labels, - exclude_claim_labels=exclude_claim_labels, + claim_labels=options.claim_labels, + exclude_claim_labels=options.exclude_claim_labels, ) ) - apr_proof = APRProof.read_proof_data(save_directory, claim.label) - node_ids = apr_proof.prune(node) - _LOGGER.info(f'Pruned nodes: {node_ids}') + apr_proof = APRProof.read_proof_data(options.save_directory, claim.label) + node_ids = apr_proof.prune(options.node) + print(f'Pruned nodes: {node_ids}') apr_proof.write_proof_data() -def exec_show_kcfg( - definition_dir: Path, - spec_file: Path, - save_directory: Path | None = None, - includes: Iterable[str] = (), - claim_labels: Iterable[str] | None = None, - exclude_claim_labels: Iterable[str] = (), - spec_module: str | None = None, - md_selector: str | None = None, - nodes: Iterable[NodeIdLike] = (), - node_deltas: Iterable[tuple[NodeIdLike, NodeIdLike]] = (), - to_module: bool = False, - minimize: bool = True, - failure_info: bool = False, - sort_collections: bool = False, - pending: bool = False, - failing: bool = False, - **kwargs: Any, -) -> None: - kevm = KEVM(definition_dir) - include_dirs = [Path(include) for include in includes] +def exec_show_kcfg(options: ShowKCFGOptions) -> None: + if options.definition_dir is None: + raise ValueError('Must pass --definition to show-kcfg!') + + kevm = KEVM(options.definition_dir) + include_dirs = [Path(include) for include in options.includes] include_dirs += config.INCLUDE_DIRS proof = get_apr_proof_for_spec( kevm, - spec_file, - save_directory=save_directory, - spec_module_name=spec_module, + options.spec_file, + save_directory=options.save_directory, + spec_module_name=options.spec_module, include_dirs=include_dirs, - md_selector=md_selector, - claim_labels=claim_labels, - exclude_claim_labels=exclude_claim_labels, + md_selector=options.md_selector, + claim_labels=options.claim_labels, + exclude_claim_labels=options.exclude_claim_labels, ) - if pending: - nodes = list(nodes) + [node.id for node in proof.pending] - if failing: - nodes = list(nodes) + [node.id for node in proof.failing] + nodes = [] + if options.pending: + nodes = list(options.nodes) + [node.id for node in proof.pending] + if options.failing: + nodes = list(options.nodes) + [node.id for node in proof.failing] node_printer = kevm_node_printer(kevm, proof) proof_show = APRProofShow(kevm, node_printer=node_printer) @@ -552,42 +472,35 @@ def exec_show_kcfg( res_lines = proof_show.show( proof, nodes=nodes, - node_deltas=node_deltas, - to_module=to_module, - minimize=minimize, - sort_collections=sort_collections, + node_deltas=options.node_deltas, + to_module=options.to_module, + minimize=options.minimize, + sort_collections=options.sort_collections, ) - if failure_info: + if options.failure_info: with legacy_explore(kevm, kcfg_semantics=KEVMSemantics(), id=proof.id) as kcfg_explore: res_lines += print_failure_info(proof, kcfg_explore) print('\n'.join(res_lines)) -def exec_view_kcfg( - definition_dir: Path, - spec_file: Path, - save_directory: Path | None = None, - includes: Iterable[str] = (), - claim_labels: Iterable[str] | None = None, - exclude_claim_labels: Iterable[str] = (), - spec_module: str | None = None, - md_selector: str | None = None, - **kwargs: Any, -) -> None: - kevm = KEVM(definition_dir) - include_dirs = [Path(include) for include in includes] +def exec_view_kcfg(options: ViewKCFGOptions) -> None: + if options.definition_dir is None: + raise ValueError('Must pass --definition to view-kcfg!') + + kevm = KEVM(options.definition_dir) + include_dirs = [Path(include) for include in options.includes] include_dirs += config.INCLUDE_DIRS proof = get_apr_proof_for_spec( kevm, - spec_file, - save_directory=save_directory, - spec_module_name=spec_module, + options.spec_file, + save_directory=options.save_directory, + spec_module_name=options.spec_module, include_dirs=include_dirs, - md_selector=md_selector, - claim_labels=claim_labels, - exclude_claim_labels=exclude_claim_labels, + md_selector=options.md_selector, + claim_labels=options.claim_labels, + exclude_claim_labels=options.exclude_claim_labels, ) node_printer = kevm_node_printer(kevm, proof) @@ -604,77 +517,50 @@ def custom_view(element: KCFGElem) -> list[str]: proof_view.run() -def exec_run( - input_file: Path, - expand_macros: bool, - depth: int | None, - output: KRunOutput, - schedule: str, - mode: str, - chainid: int, - usegas: bool, - target: str | None = None, - save_directory: Path | None = None, - debugger: bool = False, - **kwargs: Any, -) -> None: - if target is None: - target = 'llvm' - - target_fqn = f'evm-semantics.{target}' - - _ignore_arg(kwargs, 'definition_dir', f'--definition: {kwargs["definition_dir"]}') - kevm = KEVM(kdist.get(target_fqn), use_directory=save_directory) +def exec_run(options: RunOptions) -> None: + target_fqn = f'evm-semantics.{options.target}' + + kevm = KEVM(kdist.get(target_fqn), use_directory=options.save_directory) try: - json_read = json.loads(input_file.read_text()) - kore_pattern = gst_to_kore(json_read, schedule, mode, chainid, usegas) + json_read = json.loads(options.input_file.read_text()) + kore_pattern = gst_to_kore(json_read, options.schedule, options.mode, options.chainid, options.usegas) except json.JSONDecodeError: - pgm_token = KToken(input_file.read_text(), KSort('EthereumSimulation')) + pgm_token = KToken(options.input_file.read_text(), KSort('EthereumSimulation')) kast_pgm = kevm.parse_token(pgm_token) kore_pgm = kevm.kast_to_kore(kast_pgm, sort=KSort('EthereumSimulation')) - kore_pattern = kore_pgm_to_kore(kore_pgm, SORT_ETHEREUM_SIMULATION, schedule, mode, chainid, usegas) + kore_pattern = kore_pgm_to_kore( + kore_pgm, SORT_ETHEREUM_SIMULATION, options.schedule, options.mode, options.chainid, options.usegas + ) kevm.run( kore_pattern, - depth=depth, + depth=options.depth, term=True, - expand_macros=expand_macros, - output=output, + expand_macros=options.expand_macros, + output=options.output, check=True, - debugger=debugger, + debugger=options.debugger, ) -def exec_kast( - input_file: Path, - output: PrintOutput, - schedule: str, - mode: str, - chainid: int, - usegas: bool, - target: str | None = None, - save_directory: Path | None = None, - **kwargs: Any, -) -> None: - if target is None: - target = 'llvm' - - target_fqn = f'evm-semantics.{target}' +def exec_kast(options: KastOptions) -> None: + target_fqn = f'evm-semantics.{options.target}' - _ignore_arg(kwargs, 'definition_dir', f'--definition: {kwargs["definition_dir"]}') - kevm = KEVM(kdist.get(target_fqn), use_directory=save_directory) + kevm = KEVM(kdist.get(target_fqn), use_directory=options.save_directory) try: - json_read = json.loads(input_file.read_text()) - kore_pattern = gst_to_kore(json_read, schedule, mode, chainid, usegas) + json_read = json.loads(options.input_file.read_text()) + kore_pattern = gst_to_kore(json_read, options.schedule, options.mode, options.chainid, options.usegas) except json.JSONDecodeError: - pgm_token = KToken(input_file.read_text(), KSort('EthereumSimulation')) + pgm_token = KToken(options.input_file.read_text(), KSort('EthereumSimulation')) kast_pgm = kevm.parse_token(pgm_token) kore_pgm = kevm.kast_to_kore(kast_pgm) - kore_pattern = kore_pgm_to_kore(kore_pgm, SORT_ETHEREUM_SIMULATION, schedule, mode, chainid, usegas) + kore_pattern = kore_pgm_to_kore( + kore_pgm, SORT_ETHEREUM_SIMULATION, options.schedule, options.mode, options.chainid, options.usegas + ) - output_text = kore_print(kore_pattern, definition_dir=kevm.definition_dir, output=output) + output_text = kore_print(kore_pattern, definition_dir=kevm.definition_dir, output=options.output) print(output_text) diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 2be249ef2d..40184906d9 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -13,6 +13,7 @@ LoggingOptions, Options, ParallelOptions, + SaveDirOptions, SMTOptions, SpecOptions, ) @@ -141,7 +142,7 @@ def args(parser: ArgumentParser) -> ArgumentParser: return parser -class ShowKCFGOptions(LoggingOptions, KOptions, SpecOptions, DisplayOptions): +class ShowKCFGOptions(LoggingOptions, KOptions, SpecOptions, KEVMDisplayOptions): nodes: list[NodeIdLike] node_deltas: list[tuple[NodeIdLike, NodeIdLike]] failure_info: bool @@ -266,7 +267,7 @@ class RPCOptions(Options): trace_rewrites: bool kore_rpc_command: str | None use_booster: bool - fallback_on: list[FallbackReason] + fallback_on: list[FallbackReason] | None post_exec_simplify: bool interim_simplification: int | None port: int | None @@ -282,6 +283,7 @@ def default() -> dict[str, Any]: 'interim_simplification': None, 'port': None, 'maude_port': None, + 'fallback_on': None, } @staticmethod @@ -485,7 +487,15 @@ def args(parser: ArgumentParser) -> ArgumentParser: class ProveOptions( - LoggingOptions, KOptions, ParallelOptions, KProveOptions, BugReportOptions, SMTOptions, ExploreOptions, SpecOptions + LoggingOptions, + KOptions, + ParallelOptions, + KProveOptions, + BugReportOptions, + SMTOptions, + ExploreOptions, + SpecOptions, + RPCOptions, ): reinit: bool @@ -652,7 +662,7 @@ class TargetOptions(Options): @staticmethod def default() -> dict[str, Any]: return { - 'target': 'haskell', + 'target': 'llvm', } @staticmethod @@ -714,7 +724,7 @@ def args(parser: ArgumentParser) -> ArgumentParser: return parser -class RunOptions(LoggingOptions, KOptions, TargetOptions, EVMChainOptions): +class RunOptions(LoggingOptions, KOptions, TargetOptions, EVMChainOptions, SaveDirOptions): input_file: Path output: KRunOutput expand_macros: bool @@ -768,7 +778,7 @@ def args(parser: ArgumentParser) -> ArgumentParser: return parser -class KastOptions(LoggingOptions, TargetOptions, EVMChainOptions, KOptions): +class KastOptions(LoggingOptions, TargetOptions, EVMChainOptions, SaveDirOptions): input_file: Path output: PrintOutput diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index fc10d65ba6..5b39a0afef 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -10,6 +10,7 @@ from kevm_pyk import config 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 @@ -222,18 +223,21 @@ def test_pyk_prove( definition_dir = kompiled_target_for(spec_file) name = str(spec_file.relative_to(SPEC_DIR)) break_on_calls = name in TEST_PARAMS and TEST_PARAMS[name].break_on_calls - exec_prove( - spec_file=spec_file, - definition_dir=definition_dir, - includes=[str(include_dir) for include_dir in config.INCLUDE_DIRS], - save_directory=use_directory, - smt_timeout=300, - smt_retry_limit=10, - md_selector='foo', # TODO Ignored flag, this is to avoid KeyError - use_booster=use_booster, - bug_report=bug_report, - break_on_calls=break_on_calls, + + options = ProveOptions( + { + 'spec_file': spec_file, + 'definition_dir': definition_dir, + 'includes': [str(include_dir) for include_dir in config.INCLUDE_DIRS], + 'save_directory': use_directory, + 'md_selector': 'foo', + 'use_booster': use_booster, + 'bug_report': bug_report, + 'break_on_calls': break_on_calls, + } ) + + exec_prove(options) if name in TEST_PARAMS: params = TEST_PARAMS[name] if params.leaf_number is not None and params.main_claim_id is not None: From 8150335064d1f834c55f7b8e5fce06fe7bab3e7c Mon Sep 17 00:00:00 2001 From: devops <devops@runtimeverification.com> Date: Mon, 4 Mar 2024 21:18:40 +0000 Subject: [PATCH 08/28] Set Version: 1.0.478 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 7e683bb02d..eae11cb4e3 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.477" +version = "1.0.478" description = "" authors = [ "Runtime Verification, Inc. <contact@runtimeverification.com>", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 689d6f2cb3..eb13e3f3a3 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.477' +VERSION: Final = '1.0.478' diff --git a/package/version b/package/version index fb5bced929..2dd3986f2b 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.477 +1.0.478 From acd6a96dc266aacd42f2566fe008664d6b9ca726 Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Mon, 4 Mar 2024 17:56:18 -0600 Subject: [PATCH 09/28] Update to use new system --- kevm-pyk/src/kevm_pyk/__main__.py | 1105 +++++++++++------- kevm-pyk/src/kevm_pyk/cli.py | 365 +----- kevm-pyk/src/tests/integration/test_prove.py | 7 +- 3 files changed, 705 insertions(+), 772 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 40b6239201..a7bda88a76 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -8,43 +8,53 @@ import sys import tempfile import time -from argparse import ArgumentParser from dataclasses import dataclass from functools import cached_property from pathlib import Path from typing import TYPE_CHECKING from pathos.pools import ProcessPool # type: ignore +from pyk.cli.args import ( + CLI, + BugReportOptions, + Command, + KompileOptions, + ParallelOptions, + SaveDirOptions, + SMTOptions, + SpecOptions, +) +from pyk.cli.utils import file_path from pyk.cterm import CTerm from pyk.kast.outer import KApply, KRewrite, KSort, KToken from pyk.kcfg import KCFG from pyk.kdist import kdist -from pyk.kore.tools import kore_print +from pyk.kore.tools import PrintOutput, kore_print from pyk.ktool.kompile import LLVMKompileType +from pyk.ktool.krun import KRunOutput from pyk.prelude.ml import is_top, mlOr -from pyk.proof import APRProof from pyk.proof.implies import EqualityProof +from pyk.proof.reachability import APRProof from pyk.proof.show import APRProofShow from pyk.proof.tui import APRProofViewer from pyk.utils import FrozenDict, hash_str, single from . import VERSION, config from .cli import ( - KastOptions, - KompileSpecOptions, - ProveLegacyOptions, - ProveOptions, - PruneProofOptions, - RunOptions, - ShowKCFGOptions, - VersionOptions, - ViewKCFGOptions, - generate_command_options, + EVMChainOptions, + ExploreOptions, + KEVMDisplayOptions, + KOptions, + KProveLegacyOptions, + KProveOptions, + RPCOptions, + TargetOptions, ) 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, @@ -54,11 +64,12 @@ ) if TYPE_CHECKING: - from argparse import Namespace + from argparse import ArgumentParser, Namespace from collections.abc import Callable, Iterable, Iterator 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 @@ -77,87 +88,219 @@ def _ignore_arg(args: dict[str, Any], arg: str, cli_option: str) -> None: def main() -> None: sys.setrecursionlimit(15000000) - parser = _create_argument_parser() + + kevm_cli = CLI( + ( + KastCommand, + KompileSpecCommand, + ProveLegacyCommand, + ProveCommand, + PruneProofCommand, + RunCommand, + ShowKCFGCommand, + VersionCommand, + ViewKCFGCommand, + ) + ) + parser = kevm_cli.create_argument_parser() args = parser.parse_args() - logging.basicConfig(level=_loglevel(args), format=_LOG_FORMAT) - options = generate_command_options({key: val for (key, val) in vars(args).items() if val is not None}) - executor_name = 'exec_' + args.command.lower().replace('-', '_') - if executor_name not in globals(): - raise AssertionError(f'Unimplemented command: {args.command}') + logging.basicConfig(level=_loglevel(args), format=_LOG_FORMAT) + command = kevm_cli.generate_command({key: val for (key, val) in vars(args).items() if val is not None}) + command.exec() + + +class KompileSpecCommand(Command, KOptions, KompileOptions): + main_file: Path + target: KompileTarget + output_dir: Path + debug_build: bool + + @staticmethod + def name() -> str: + return 'kompile-spec' + + @staticmethod + def help_str() -> str: + return 'Kompile KEVM specification.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'debug_build': False, + 'output_dir': Path(), + 'target': KompileTarget.HASKELL, + } + + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument('main_file', type=file_path, help='Path to file with main module.') + parser.add_argument('--target', type=KompileTarget, help='[haskell|maude]') + parser.add_argument( + '-o', '--output-definition', type=Path, dest='output_dir', help='Path to write kompiled definition to.' + ) + parser.add_argument( + '--debug-build', dest='debug_build', default=None, help='Enable debug symbols in LLVM builds.' + ) + return parser - execute = globals()[executor_name] - execute(options) + def exec(self) -> None: + if self.target not in [KompileTarget.HASKELL, KompileTarget.MAUDE]: + raise ValueError(f'Can only call kevm kompile-spec with --target [haskell,maude], got: {self.target.value}') + optimization = 0 + if self.o1: + optimization = 1 + if self.o2: + optimization = 2 + if self.o3: + optimization = 3 + if self.debug_build: + optimization = 0 + + kevm_kompile( + self.target, + output_dir=self.output_dir, + main_file=self.main_file, + main_module=self.main_module, + syntax_module=self.syntax_module, + includes=self.includes, + emit_json=self.emit_json, + read_only=self.read_only, + ccopts=self.ccopts, + optimization=optimization, + enable_llvm_debug=self.enable_llvm_debug, + llvm_kompile_type=LLVMKompileType.C if self.llvm_library else LLVMKompileType.MAIN, + debug_build=self.debug_build, + debug=self.debug, + verbose=self.verbose, + ) -# Command implementation +class ShowKCFGCommand(Command, KOptions, SpecOptions, KEVMDisplayOptions): + nodes: list[NodeIdLike] + node_deltas: list[tuple[NodeIdLike, NodeIdLike]] + failure_info: bool + to_module: bool + pending: bool + failing: bool + counterexample_info: bool + + @staticmethod + def name() -> str: + return 'show-kcfg' + + @staticmethod + def help_str() -> str: + return 'Print the CFG for a given proof.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'failure_info': False, + 'to_module': False, + 'pending': False, + 'failing': False, + 'counterexample_info': False, + } + + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument( + '--node', + type=node_id_like, + dest='nodes', + default=[], + action='append', + help='List of nodes to display as well.', + ) + parser.add_argument( + '--node-delta', + type=arg_pair_of(node_id_like, node_id_like), + dest='node_deltas', + default=[], + action='append', + help='List of nodes to display delta for.', + ) + parser.add_argument( + '--failure-information', + dest='failure_info', + default=None, + action='store_true', + help='Show failure summary for cfg', + ) + parser.add_argument( + '--no-failure-information', + dest='failure_info', + action='store_false', + help='Do not show failure summary for cfg', + ) + parser.add_argument( + '--to-module', dest='to_module', default=None, action='store_true', help='Output edges as a K module.' + ) + parser.add_argument( + '--pending', dest='pending', default=None, action='store_true', help='Also display pending nodes' + ) + parser.add_argument( + '--failing', dest='failing', default=None, action='store_true', help='Also display failing nodes' + ) + parser.add_argument( + '--counterexample-information', + dest='counterexample_info', + default=None, + action='store_true', + help="Show models for failing nodes. Should be called with the '--failure-information' flag", + ) + return parser -def exec_version(options: VersionOptions) -> None: - print(f'KEVM Version: {VERSION}') + def exec(self) -> None: + if self.definition_dir is None: + raise ValueError('Must pass --definition to show-kcfg!') + kevm = KEVM(self.definition_dir) + include_dirs = [Path(include) for include in self.includes] + include_dirs += config.INCLUDE_DIRS + proof = get_apr_proof_for_spec( + kevm, + self.spec_file, + save_directory=self.save_directory, + spec_module_name=self.spec_module, + include_dirs=include_dirs, + md_selector=self.md_selector, + claim_labels=self.claim_labels, + exclude_claim_labels=self.exclude_claim_labels, + ) -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}') + nodes = [] + if self.pending: + nodes = list(self.nodes) + [node.id for node in proof.pending] + if self.failing: + nodes = list(self.nodes) + [node.id for node in proof.failing] + + node_printer = kevm_node_printer(kevm, proof) + proof_show = APRProofShow(kevm, node_printer=node_printer) + + res_lines = proof_show.show( + proof, + nodes=nodes, + node_deltas=self.node_deltas, + to_module=self.to_module, + minimize=self.minimize, + sort_collections=self.sort_collections, + ) - optimization = 0 - if options.o1: - optimization = 1 - if options.o2: - optimization = 2 - if options.o3: - optimization = 3 - if options.debug_build: - optimization = 0 + if self.failure_info: + with legacy_explore(kevm, kcfg_semantics=KEVMSemantics(), id=proof.id) as kcfg_explore: + res_lines += print_failure_info(proof, kcfg_explore) - kevm_kompile( - options.target, - output_dir=options.output_dir, - main_file=options.main_file, - main_module=options.main_module, - syntax_module=options.syntax_module, - includes=options.includes, - emit_json=options.emit_json, - read_only=options.read_only, - ccopts=options.ccopts, - optimization=optimization, - enable_llvm_debug=options.enable_llvm_debug, - llvm_kompile_type=LLVMKompileType.C if options.llvm_library else LLVMKompileType.MAIN, - debug_build=options.debug_build, - debug=options.debug, - verbose=options.verbose, - ) + print('\n'.join(res_lines)) -def exec_prove_legacy(options: ProveLegacyOptions) -> None: - definition_dir = options.definition_dir - if definition_dir is None: - definition_dir = kdist.get('evm-semantics.haskell') - - kevm = KEVM(definition_dir, use_directory=options.save_directory) - - include_dirs = [Path(include) for include in options.includes] - include_dirs += config.INCLUDE_DIRS - - final_state = kevm.prove_legacy( - spec_file=options.spec_file, - includes=include_dirs, - bug_report=options.bug_report_legacy, - spec_module=options.spec_module, - claim_labels=options.claim_labels, - exclude_claim_labels=options.exclude_claim_labels, - debug=options.debug, - debugger=options.debugger, - max_depth=options.max_depth, - max_counterexamples=options.max_counterexamples, - branching_allowed=options.branching_allowed, - haskell_backend_args=options.haskell_backend_args, - ) - final_kast = mlOr([state.kast for state in final_state]) - print(kevm.pretty_print(final_kast)) - if not is_top(final_kast): - raise SystemExit(1) +def node_id_like(s: str) -> NodeIdLike: + try: + return int(s) + except ValueError: + return s class ZeroProcessPool: @@ -165,15 +308,6 @@ def map(self, f: Callable[[Any], Any], xs: list[Any]) -> list[Any]: return [f(x) for x in xs] -@contextlib.contextmanager -def wrap_process_pool(workers: int) -> Iterator[ZeroProcessPool | ProcessPool]: - if workers <= 1: - yield ZeroProcessPool() - else: - with ProcessPool(ncpus=workers) as pp: - yield pp - - class JSONEncoder(json.JSONEncoder): def default(self, obj: Any) -> Any: if isinstance(obj, FrozenDict): @@ -237,358 +371,513 @@ def get_or_load_claim_job(claim_label: str) -> KClaimJob: return frozenset({get_or_load_claim_job(claim.label) for claim in claims}) -def exec_prove(options: ProveOptions) -> None: - md_selector = 'k' +@contextlib.contextmanager +def wrap_process_pool(workers: int) -> Iterator[ZeroProcessPool | ProcessPool]: + if workers <= 1: + yield ZeroProcessPool() + else: + with ProcessPool(ncpus=workers) as pp: + yield pp - save_directory = options.save_directory if options.save_directory is not None else Path(tempfile.mkdtemp()) - digest_file = save_directory / 'digest' - definition_dir = ( - options.definition_dir if options.definition_dir is not None else kdist.get('evm-semantics.haskell') - ) +class ProveCommand( + Command, + KOptions, + ParallelOptions, + KProveOptions, + BugReportOptions, + SMTOptions, + ExploreOptions, + SpecOptions, + RPCOptions, +): + reinit: bool + + @staticmethod + def name() -> str: + return 'prove' + + @staticmethod + def help_str() -> str: + return 'Run KEVM proof.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'reinit': False, + } + + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument( + '--reinit', + dest='reinit', + default=None, + action='store_true', + help='Reinitialize CFGs even if they already exist.', + ) + return parser - kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=options.bug_report) - - include_dirs = [Path(include) for include in options.includes] - include_dirs += config.INCLUDE_DIRS - - kore_rpc_command: Iterable[str] - if options.kore_rpc_command is None: - kore_rpc_command = ('kore-rpc-booster',) if options.use_booster else ('kore-rpc',) - elif isinstance(options.kore_rpc_command, str): - kore_rpc_command = options.kore_rpc_command.split() - - def is_functional(claim: KClaim) -> bool: - claim_lhs = claim.body - if type(claim_lhs) is KRewrite: - claim_lhs = claim_lhs.lhs - return not (type(claim_lhs) is KApply and claim_lhs.label.name == '<generatedTop>') - - llvm_definition_dir = definition_dir / 'llvm-library' if options.use_booster else None - - _LOGGER.info(f'Extracting claims from file: {options.spec_file}') - all_claims = kevm.get_claims( - options.spec_file, - spec_module_name=options.spec_module, - include_dirs=include_dirs, - md_selector=md_selector, - claim_labels=options.claim_labels, - exclude_claim_labels=options.exclude_claim_labels, - ) - if all_claims is None: - raise ValueError(f'No claims found in file: {options.spec_file}') - spec_module_name = ( - options.spec_module if options.spec_module is not None else os.path.splitext(options.spec_file.name)[0].upper() - ) - all_claim_jobs = init_claim_jobs(spec_module_name, all_claims) - all_claim_jobs_by_label = {c.claim.label: c for c in all_claim_jobs} - claims_graph = claim_dependency_dict(all_claims, spec_module_name=spec_module_name) - - def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]: - claim = claim_job.claim - up_to_date = claim_job.up_to_date(digest_file) - if up_to_date: - _LOGGER.info(f'Claim is up to date: {claim.label}') - else: - _LOGGER.info(f'Claim reinitialized because it is out of date: {claim.label}') - claim_job.update_digest(digest_file) - with legacy_explore( - kevm, - kcfg_semantics=KEVMSemantics(auto_abstract_gas=options.auto_abstract_gas), - id=claim.label, - llvm_definition_dir=llvm_definition_dir, - bug_report=options.bug_report, - kore_rpc_command=kore_rpc_command, - smt_timeout=options.smt_timeout, - smt_retry_limit=options.smt_retry_limit, - trace_rewrites=options.trace_rewrites, - fallback_on=options.fallback_on, - interim_simplification=options.interim_simplification, - no_post_exec_simplify=(not options.post_exec_simplify), - ) as kcfg_explore: - proof_problem: Proof - if is_functional(claim): - if not options.reinit and up_to_date and EqualityProof.proof_exists(claim.label, save_directory): - proof_problem = EqualityProof.read_proof_data(save_directory, claim.label) - else: - proof_problem = EqualityProof.from_claim(claim, kevm.definition, proof_dir=save_directory) - else: - if not options.reinit and up_to_date and APRProof.proof_data_exists(claim.label, save_directory): - proof_problem = APRProof.read_proof_data(save_directory, claim.label) + def exec(self) -> None: + md_selector = 'k' - else: - _LOGGER.info(f'Converting claim to KCFG: {claim.label}') - kcfg, init_node_id, target_node_id = KCFG.from_claim(kevm.definition, claim) - - new_init = ensure_ksequence_on_k_cell(kcfg.node(init_node_id).cterm) - new_target = ensure_ksequence_on_k_cell(kcfg.node(target_node_id).cterm) - - _LOGGER.info(f'Computing definedness constraint for initial node: {claim.label}') - new_init = kcfg_explore.cterm_symbolic.assume_defined(new_init) - - _LOGGER.info(f'Simplifying initial and target node: {claim.label}') - new_init, _ = kcfg_explore.cterm_symbolic.simplify(new_init) - new_target, _ = kcfg_explore.cterm_symbolic.simplify(new_target) - if CTerm._is_bottom(new_init.kast): - raise ValueError('Simplifying initial node led to #Bottom, are you sure your LHS is defined?') - if CTerm._is_top(new_target.kast): - raise ValueError('Simplifying target node led to #Bottom, are you sure your RHS is defined?') - - kcfg.replace_node(init_node_id, new_init) - kcfg.replace_node(target_node_id, new_target) - - proof_problem = APRProof( - claim.label, - kcfg, - [], - init_node_id, - target_node_id, - {}, - proof_dir=save_directory, - subproof_ids=claims_graph[claim.label], - admitted=claim.is_trusted, - ) - - if proof_problem.admitted: - proof_problem.write_proof_data() - _LOGGER.info(f'Skipping execution of proof because it is marked as admitted: {proof_problem.id}') - return True, None - - start_time = time.time() - passed = run_prover( - proof_problem, - kcfg_explore, - max_depth=options.max_depth, - max_iterations=options.max_iterations, - cut_point_rules=KEVMSemantics.cut_point_rules( - options.break_on_jumpi, - options.break_on_calls, - options.break_on_storage, - options.break_on_basic_blocks, - ), - terminal_rules=KEVMSemantics.terminal_rules(options.break_every_step), - fail_fast=options.fail_fast, - always_check_subsumption=options.always_check_subsumption, - fast_check_subsumption=options.fast_check_subsumption, - ) - end_time = time.time() - _LOGGER.info(f'Proof timing {proof_problem.id}: {end_time - start_time}s') - failure_log = None - if not passed: - failure_log = print_failure_info(proof_problem, kcfg_explore) - - return passed, failure_log - - topological_sorter = graphlib.TopologicalSorter(claims_graph) - topological_sorter.prepare() - with wrap_process_pool(workers=options.workers) as process_pool: - selected_results: list[tuple[bool, list[str] | None]] = [] - selected_claims = [] - while topological_sorter.is_active(): - ready = topological_sorter.get_ready() - _LOGGER.info(f'Discharging proof obligations: {ready}') - curr_claim_list = [all_claim_jobs_by_label[label] for label in ready] - results: list[tuple[bool, list[str] | None]] = process_pool.map(_init_and_run_proof, curr_claim_list) - for label in ready: - topological_sorter.done(label) - selected_results.extend(results) - selected_claims.extend(curr_claim_list) - - failed = 0 - for job, r in zip(selected_claims, selected_results, strict=True): - passed, failure_log = r - if passed: - print(f'PROOF PASSED: {job.claim.label}') - else: - failed += 1 - print(f'PROOF FAILED: {job.claim.label}') - if options.failure_info and failure_log is not None: - for line in failure_log: - print(line) - - if failed: - sys.exit(failed) - - -def exec_prune_proof(options: PruneProofOptions) -> None: - md_selector = 'k' - - if options.save_directory is None: - raise ValueError('Must pass --save-directory to prune-proof!') - - if options.definition_dir is None: - raise ValueError('Must pass --definition to prune-proof!') - - kevm = KEVM(options.definition_dir, use_directory=options.save_directory) - - include_dirs = [Path(include) for include in options.includes] - include_dirs += config.INCLUDE_DIRS - - _LOGGER.info(f'Extracting claims from file: {options.spec_file}') - claim = single( - kevm.get_claims( - options.spec_file, - spec_module_name=options.spec_module, + save_directory = self.save_directory if self.save_directory is not None else Path(tempfile.mkdtemp()) + digest_file = save_directory / 'digest' + + definition_dir = self.definition_dir if self.definition_dir is not None else kdist.get('evm-semantics.haskell') + + kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=self.bug_report) + + include_dirs = [Path(include) for include in self.includes] + include_dirs += config.INCLUDE_DIRS + + kore_rpc_command: Iterable[str] + if self.kore_rpc_command is None: + kore_rpc_command = ('kore-rpc-booster',) if self.use_booster else ('kore-rpc',) + elif isinstance(self.kore_rpc_command, str): + kore_rpc_command = self.kore_rpc_command.split() + + def is_functional(claim: KClaim) -> bool: + claim_lhs = claim.body + if type(claim_lhs) is KRewrite: + claim_lhs = claim_lhs.lhs + return not (type(claim_lhs) is KApply and claim_lhs.label.name == '<generatedTop>') + + llvm_definition_dir = definition_dir / 'llvm-library' if self.use_booster else None + + _LOGGER.info(f'Extracting claims from file: {self.spec_file}') + all_claims = kevm.get_claims( + self.spec_file, + spec_module_name=self.spec_module, include_dirs=include_dirs, md_selector=md_selector, - claim_labels=options.claim_labels, - exclude_claim_labels=options.exclude_claim_labels, + claim_labels=self.claim_labels, + exclude_claim_labels=self.exclude_claim_labels, ) - ) + if all_claims is None: + raise ValueError(f'No claims found in file: {self.spec_file}') + spec_module_name = ( + self.spec_module if self.spec_module is not None else os.path.splitext(self.spec_file.name)[0].upper() + ) + all_claim_jobs = init_claim_jobs(spec_module_name, all_claims) + all_claim_jobs_by_label = {c.claim.label: c for c in all_claim_jobs} + claims_graph = claim_dependency_dict(all_claims, spec_module_name=spec_module_name) + + def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]: + claim = claim_job.claim + up_to_date = claim_job.up_to_date(digest_file) + if up_to_date: + _LOGGER.info(f'Claim is up to date: {claim.label}') + else: + _LOGGER.info(f'Claim reinitialized because it is out of date: {claim.label}') + claim_job.update_digest(digest_file) + with legacy_explore( + kevm, + kcfg_semantics=KEVMSemantics(auto_abstract_gas=self.auto_abstract_gas), + id=claim.label, + llvm_definition_dir=llvm_definition_dir, + bug_report=self.bug_report, + kore_rpc_command=kore_rpc_command, + smt_timeout=self.smt_timeout, + smt_retry_limit=self.smt_retry_limit, + trace_rewrites=self.trace_rewrites, + fallback_on=self.fallback_on, + interim_simplification=self.interim_simplification, + no_post_exec_simplify=(not self.post_exec_simplify), + ) as kcfg_explore: + proof_problem: Proof + if is_functional(claim): + if not self.reinit and up_to_date and EqualityProof.proof_exists(claim.label, save_directory): + proof_problem = EqualityProof.read_proof_data(save_directory, claim.label) + else: + proof_problem = EqualityProof.from_claim(claim, kevm.definition, proof_dir=save_directory) + else: + if not self.reinit and up_to_date and APRProof.proof_data_exists(claim.label, save_directory): + proof_problem = APRProof.read_proof_data(save_directory, claim.label) + + else: + _LOGGER.info(f'Converting claim to KCFG: {claim.label}') + kcfg, init_node_id, target_node_id = KCFG.from_claim(kevm.definition, claim) + + new_init = ensure_ksequence_on_k_cell(kcfg.node(init_node_id).cterm) + new_target = ensure_ksequence_on_k_cell(kcfg.node(target_node_id).cterm) + + _LOGGER.info(f'Computing definedness constraint for initial node: {claim.label}') + new_init = kcfg_explore.cterm_symbolic.assume_defined(new_init) + + _LOGGER.info(f'Simplifying initial and target node: {claim.label}') + new_init, _ = kcfg_explore.cterm_symbolic.simplify(new_init) + new_target, _ = kcfg_explore.cterm_symbolic.simplify(new_target) + if CTerm._is_bottom(new_init.kast): + raise ValueError( + 'Simplifying initial node led to #Bottom, are you sure your LHS is defined?' + ) + if CTerm._is_top(new_target.kast): + raise ValueError( + 'Simplifying target node led to #Bottom, are you sure your RHS is defined?' + ) + + kcfg.replace_node(init_node_id, new_init) + kcfg.replace_node(target_node_id, new_target) + + proof_problem = APRProof( + claim.label, + kcfg, + [], + init_node_id, + target_node_id, + {}, + proof_dir=save_directory, + subproof_ids=claims_graph[claim.label], + admitted=claim.is_trusted, + ) + + if proof_problem.admitted: + proof_problem.write_proof_data() + _LOGGER.info(f'Skipping execution of proof because it is marked as admitted: {proof_problem.id}') + return True, None + + start_time = time.time() + passed = run_prover( + proof_problem, + kcfg_explore, + max_depth=self.max_depth, + max_iterations=self.max_iterations, + cut_point_rules=KEVMSemantics.cut_point_rules( + self.break_on_jumpi, + self.break_on_calls, + self.break_on_storage, + self.break_on_basic_blocks, + ), + terminal_rules=KEVMSemantics.terminal_rules(self.break_every_step), + fail_fast=self.fail_fast, + always_check_subsumption=self.always_check_subsumption, + fast_check_subsumption=self.fast_check_subsumption, + ) + end_time = time.time() + _LOGGER.info(f'Proof timing {proof_problem.id}: {end_time - start_time}s') + failure_log = None + if not passed: + failure_log = print_failure_info(proof_problem, kcfg_explore) + + return passed, failure_log + + topological_sorter = graphlib.TopologicalSorter(claims_graph) + topological_sorter.prepare() + with wrap_process_pool(workers=self.workers) as process_pool: + selected_results: list[tuple[bool, list[str] | None]] = [] + selected_claims = [] + while topological_sorter.is_active(): + ready = topological_sorter.get_ready() + _LOGGER.info(f'Discharging proof obligations: {ready}') + curr_claim_list = [all_claim_jobs_by_label[label] for label in ready] + results: list[tuple[bool, list[str] | None]] = process_pool.map(_init_and_run_proof, curr_claim_list) + for label in ready: + topological_sorter.done(label) + selected_results.extend(results) + selected_claims.extend(curr_claim_list) + + failed = 0 + for job, r in zip(selected_claims, selected_results, strict=True): + passed, failure_log = r + if passed: + print(f'PROOF PASSED: {job.claim.label}') + else: + failed += 1 + print(f'PROOF FAILED: {job.claim.label}') + if self.failure_info and failure_log is not None: + for line in failure_log: + print(line) - apr_proof = APRProof.read_proof_data(options.save_directory, claim.label) - node_ids = apr_proof.prune(options.node) - print(f'Pruned nodes: {node_ids}') - apr_proof.write_proof_data() - - -def exec_show_kcfg(options: ShowKCFGOptions) -> None: - if options.definition_dir is None: - raise ValueError('Must pass --definition to show-kcfg!') - - kevm = KEVM(options.definition_dir) - include_dirs = [Path(include) for include in options.includes] - include_dirs += config.INCLUDE_DIRS - proof = get_apr_proof_for_spec( - kevm, - options.spec_file, - save_directory=options.save_directory, - spec_module_name=options.spec_module, - include_dirs=include_dirs, - md_selector=options.md_selector, - claim_labels=options.claim_labels, - exclude_claim_labels=options.exclude_claim_labels, - ) + if failed: + sys.exit(failed) - nodes = [] - if options.pending: - nodes = list(options.nodes) + [node.id for node in proof.pending] - if options.failing: - nodes = list(options.nodes) + [node.id for node in proof.failing] - - node_printer = kevm_node_printer(kevm, proof) - proof_show = APRProofShow(kevm, node_printer=node_printer) - - res_lines = proof_show.show( - proof, - nodes=nodes, - node_deltas=options.node_deltas, - to_module=options.to_module, - minimize=options.minimize, - sort_collections=options.sort_collections, - ) - if options.failure_info: - with legacy_explore(kevm, kcfg_semantics=KEVMSemantics(), id=proof.id) as kcfg_explore: - res_lines += print_failure_info(proof, kcfg_explore) - - print('\n'.join(res_lines)) - - -def exec_view_kcfg(options: ViewKCFGOptions) -> None: - if options.definition_dir is None: - raise ValueError('Must pass --definition to view-kcfg!') - - kevm = KEVM(options.definition_dir) - include_dirs = [Path(include) for include in options.includes] - include_dirs += config.INCLUDE_DIRS - proof = get_apr_proof_for_spec( - kevm, - options.spec_file, - save_directory=options.save_directory, - spec_module_name=options.spec_module, - include_dirs=include_dirs, - md_selector=options.md_selector, - claim_labels=options.claim_labels, - exclude_claim_labels=options.exclude_claim_labels, - ) +class VersionCommand(Command): + @staticmethod + def name() -> str: + return 'version' - node_printer = kevm_node_printer(kevm, proof) + @staticmethod + def help_str() -> str: + return 'Print KEVM version and exit.' - def custom_view(element: KCFGElem) -> list[str]: - if type(element) is KCFG.Edge: - return list(element.rules) - if type(element) is KCFG.NDBranch: - return list(element.rules) - return [] + def exec(self) -> None: + print(f'KEVM Version: {VERSION}') - proof_view = APRProofViewer(proof, kevm, node_printer=node_printer, custom_view=custom_view) - proof_view.run() +class PruneProofCommand(Command, KOptions, SpecOptions): + node: NodeIdLike + @staticmethod + def name() -> str: + return 'prune-proof' -def exec_run(options: RunOptions) -> None: - target_fqn = f'evm-semantics.{options.target}' + @staticmethod + def help_str() -> str: + return 'Remove a node and its successors from the proof state.' - kevm = KEVM(kdist.get(target_fqn), use_directory=options.save_directory) + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument('node', type=node_id_like, help='Node to remove CFG subgraph from.') + return parser - try: - json_read = json.loads(options.input_file.read_text()) - kore_pattern = gst_to_kore(json_read, options.schedule, options.mode, options.chainid, options.usegas) - except json.JSONDecodeError: - pgm_token = KToken(options.input_file.read_text(), KSort('EthereumSimulation')) - kast_pgm = kevm.parse_token(pgm_token) - kore_pgm = kevm.kast_to_kore(kast_pgm, sort=KSort('EthereumSimulation')) - kore_pattern = kore_pgm_to_kore( - kore_pgm, SORT_ETHEREUM_SIMULATION, options.schedule, options.mode, options.chainid, options.usegas + def exec(self) -> None: + md_selector = 'k' + + if self.save_directory is None: + raise ValueError('Must pass --save-directory to prune-proof!') + + if self.definition_dir is None: + raise ValueError('Must pass --definition to prune-proof!') + + kevm = KEVM(self.definition_dir, use_directory=self.save_directory) + + include_dirs = [Path(include) for include in self.includes] + include_dirs += config.INCLUDE_DIRS + + _LOGGER.info(f'Extracting claims from file: {self.spec_file}') + claim = single( + kevm.get_claims( + self.spec_file, + spec_module_name=self.spec_module, + include_dirs=include_dirs, + md_selector=md_selector, + claim_labels=self.claim_labels, + exclude_claim_labels=self.exclude_claim_labels, + ) ) - kevm.run( - kore_pattern, - depth=options.depth, - term=True, - expand_macros=options.expand_macros, - output=options.output, - check=True, - debugger=options.debugger, - ) + apr_proof = APRProof.read_proof_data(self.save_directory, claim.label) + node_ids = apr_proof.prune(self.node) + print(f'Pruned nodes: {node_ids}') + apr_proof.write_proof_data() -def exec_kast(options: KastOptions) -> None: - target_fqn = f'evm-semantics.{options.target}' +class ProveLegacyCommand(Command, KOptions, SpecOptions, KProveLegacyOptions): + bug_report_legacy: bool - kevm = KEVM(kdist.get(target_fqn), use_directory=options.save_directory) + @staticmethod + def name() -> str: + return 'prove-legacy' - try: - json_read = json.loads(options.input_file.read_text()) - kore_pattern = gst_to_kore(json_read, options.schedule, options.mode, options.chainid, options.usegas) - except json.JSONDecodeError: - pgm_token = KToken(options.input_file.read_text(), KSort('EthereumSimulation')) - kast_pgm = kevm.parse_token(pgm_token) - kore_pgm = kevm.kast_to_kore(kast_pgm) - kore_pattern = kore_pgm_to_kore( - kore_pgm, SORT_ETHEREUM_SIMULATION, options.schedule, options.mode, options.chainid, options.usegas + @staticmethod + def help_str() -> str: + return 'Run KEVM proof using the legacy kprove binary.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'bug_report_legacy': False, + } + + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument( + '--bug-report-legacy', default=None, action='store_true', help='Generate a legacy bug report.' + ) + return parser + + def exec(self) -> None: + definition_dir = self.definition_dir + if definition_dir is None: + definition_dir = kdist.get('evm-semantics.haskell') + + kevm = KEVM(definition_dir, use_directory=self.save_directory) + + include_dirs = [Path(include) for include in self.includes] + include_dirs += config.INCLUDE_DIRS + + final_state = kevm.prove_legacy( + spec_file=self.spec_file, + includes=include_dirs, + bug_report=self.bug_report_legacy, + spec_module=self.spec_module, + claim_labels=self.claim_labels, + exclude_claim_labels=self.exclude_claim_labels, + debug=self.debug, + debugger=self.debugger, + max_depth=self.max_depth, + max_counterexamples=self.max_counterexamples, + branching_allowed=self.branching_allowed, + haskell_backend_args=self.haskell_backend_args, ) + final_kast = mlOr([state.kast for state in final_state]) + print(kevm.pretty_print(final_kast)) + if not is_top(final_kast): + raise SystemExit(1) - output_text = kore_print(kore_pattern, definition_dir=kevm.definition_dir, output=options.output) - print(output_text) +class ViewKCFGCommand(Command, KOptions, SpecOptions): + @staticmethod + def name() -> str: + return 'view-kcfg' -# Helpers + @staticmethod + def help_str() -> str: + return 'Explore a given proof in the KCFG visualizer.' + def exec(self) -> None: + if self.definition_dir is None: + raise ValueError('Must pass --definition to view-kcfg!') -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)] + kevm = KEVM(self.definition_dir) + include_dirs = [Path(include) for include in self.includes] + include_dirs += config.INCLUDE_DIRS + proof = get_apr_proof_for_spec( + kevm, + self.spec_file, + save_directory=self.save_directory, + spec_module_name=self.spec_module, + include_dirs=include_dirs, + md_selector=self.md_selector, + claim_labels=self.claim_labels, + exclude_claim_labels=self.exclude_claim_labels, + ) - return parse + node_printer = kevm_node_printer(kevm, proof) + + def custom_view(element: KCFGElem) -> list[str]: + if type(element) is KCFG.Edge: + return list(element.rules) + if type(element) is KCFG.NDBranch: + return list(element.rules) + return [] + + proof_view = APRProofViewer(proof, kevm, node_printer=node_printer, custom_view=custom_view) + + proof_view.run() + + +class RunCommand(Command, KOptions, TargetOptions, EVMChainOptions, SaveDirOptions): + input_file: Path + output: KRunOutput + expand_macros: bool + debugger: bool + + @staticmethod + def name() -> str: + return 'run' + + @staticmethod + def help_str() -> str: + return 'Run KEVM test/simulation.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'output': KRunOutput.PRETTY, + 'expand_macros': True, + 'debugger': False, + } + + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument('input_file', type=file_path, help='Path to input file.') + parser.add_argument( + '--output', + default=None, + type=KRunOutput, + choices=list(KRunOutput), + ) + parser.add_argument( + '--expand-macros', + dest='expand_macros', + default=None, + action='store_true', + help='Expand macros on the input term before execution.', + ) + parser.add_argument( + '--no-expand-macros', + dest='expand_macros', + action='store_false', + help='Do not expand macros on the input term before execution.', + ) + parser.add_argument( + '--debugger', + dest='debugger', + action='store_true', + help='Run GDB debugger for execution.', + ) + return parser + + def exec(self) -> None: + target_fqn = f'evm-semantics.{self.target}' + + kevm = KEVM(kdist.get(target_fqn), use_directory=self.save_directory) + + try: + json_read = json.loads(self.input_file.read_text()) + kore_pattern = gst_to_kore(json_read, self.schedule, self.mode, self.chainid, self.usegas) + except json.JSONDecodeError: + pgm_token = KToken(self.input_file.read_text(), KSort('EthereumSimulation')) + kast_pgm = kevm.parse_token(pgm_token) + kore_pgm = kevm.kast_to_kore(kast_pgm, sort=KSort('EthereumSimulation')) + kore_pattern = kore_pgm_to_kore( + kore_pgm, SORT_ETHEREUM_SIMULATION, self.schedule, self.mode, self.chainid, self.usegas + ) - parser = ArgumentParser(prog='kevm-pyk') + kevm.run( + kore_pattern, + depth=self.depth, + term=True, + expand_macros=self.expand_macros, + output=self.output, + check=True, + debugger=self.debugger, + ) - command_parser = parser.add_subparsers(dest='command', required=True) - command_parser = VersionOptions.parser(command_parser) - command_parser = KompileSpecOptions.parser(command_parser) - command_parser = ProveOptions.parser(command_parser) - command_parser = PruneProofOptions.parser(command_parser) - command_parser = ProveLegacyOptions.parser(command_parser) - command_parser = ViewKCFGOptions.parser(command_parser) - command_parser = ShowKCFGOptions.parser(command_parser) - command_parser = RunOptions.parser(command_parser) - command_parser = KastOptions.parser(command_parser) +class KastCommand(Command, TargetOptions, EVMChainOptions, SaveDirOptions): + input_file: Path + output: PrintOutput + + @staticmethod + def name() -> str: + return 'kast' + + @staticmethod + def help_str() -> str: + return 'Run KEVM program.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'output': PrintOutput.KORE, + } + + @staticmethod + def args(parser: ArgumentParser) -> ArgumentParser: + parser.add_argument('input_file', type=file_path, help='Path to input file.') + parser.add_argument( + '--output', + default=None, + type=PrintOutput, + choices=list(PrintOutput), + ) + return parser + + def exec(self) -> None: + target_fqn = f'evm-semantics.{self.target}' + + kevm = KEVM(kdist.get(target_fqn), use_directory=self.save_directory) + + try: + json_read = json.loads(self.input_file.read_text()) + kore_pattern = gst_to_kore(json_read, self.schedule, self.mode, self.chainid, self.usegas) + except json.JSONDecodeError: + pgm_token = KToken(self.input_file.read_text(), KSort('EthereumSimulation')) + kast_pgm = kevm.parse_token(pgm_token) + kore_pgm = kevm.kast_to_kore(kast_pgm) + kore_pattern = kore_pgm_to_kore( + kore_pgm, SORT_ETHEREUM_SIMULATION, self.schedule, self.mode, self.chainid, self.usegas + ) + + output_text = kore_print(kore_pattern, definition_dir=kevm.definition_dir, output=self.output) + print(output_text) - return parser + +# Helpers def _loglevel(args: Namespace) -> int: diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 40184906d9..f225adeca3 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -1,39 +1,21 @@ 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, - DisplayOptions, - KDefinitionOptions, - KompileOptions, - LoggingOptions, - Options, - ParallelOptions, - SaveDirOptions, - SMTOptions, - SpecOptions, -) -from pyk.cli.utils import file_path +from pyk.cli.args import DisplayOptions, KDefinitionOptions, Options 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 argparse import _SubParsersAction from collections.abc import Callable - from typing import TypeVar - - from pyk.kcfg.kcfg import NodeIdLike + from typing import Final, TypeVar 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]: @@ -42,38 +24,6 @@ def parse(s: str) -> list[T]: return parse -def node_id_like(s: str) -> NodeIdLike: - try: - return int(s) - except ValueError: - return s - - -def generate_command_options(args: dict[str, Any]) -> LoggingOptions: - command = args['command'].lower() - match command: - case 'version': - return VersionOptions(args) - case 'kompile-spec': - return KompileSpecOptions(args) - case 'prove': - return ProveOptions(args) - case 'prune-proof': - return PruneProofOptions(args) - case 'prove-legacy': - return ProveLegacyOptions(args) - case 'view-kcfg': - return ViewKCFGOptions(args) - case 'show-kcfg': - return ShowKCFGOptions(args) - case 'run': - return RunOptions(args) - case 'kast': - return KastOptions(args) - case _: - raise ValueError('Unrecognized command.') - - class KEVMDisplayOptions(DisplayOptions): sort_collections: bool @@ -106,120 +56,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: return parser -class KompileSpecOptions(LoggingOptions, KOptions, KompileOptions): - main_file: Path - target: KompileTarget - output_dir: Path - debug_build: bool - - @staticmethod - def default() -> dict[str, Any]: - return { - 'debug_build': False, - 'output_dir': Path(), - 'target': KompileTarget.HASKELL, - } - - @staticmethod - def parser(base: _SubParsersAction) -> _SubParsersAction: - base.add_parser( - 'kompile-spec', - help='Kompile KEVM specification.', - parents=[KompileSpecOptions.all_args()], - ) - return base - - @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: - parser.add_argument('main_file', type=file_path, help='Path to file with main module.') - parser.add_argument('--target', type=KompileTarget, help='[haskell|maude]') - parser.add_argument( - '-o', '--output-definition', type=Path, dest='output_dir', help='Path to write kompiled definition to.' - ) - parser.add_argument( - '--debug-build', dest='debug_build', default=None, help='Enable debug symbols in LLVM builds.' - ) - return parser - - -class ShowKCFGOptions(LoggingOptions, KOptions, SpecOptions, KEVMDisplayOptions): - nodes: list[NodeIdLike] - node_deltas: list[tuple[NodeIdLike, NodeIdLike]] - failure_info: bool - to_module: bool - pending: bool - failing: bool - counterexample_info: bool - - @staticmethod - def parser(base: _SubParsersAction) -> _SubParsersAction: - base.add_parser( - 'show-kcfg', - help='Print the CFG for a given proof.', - parents=[ShowKCFGOptions.all_args()], - ) - return base - - @staticmethod - def default() -> dict[str, Any]: - return { - 'failure_info': False, - 'to_module': False, - 'pending': False, - 'failing': False, - 'counterexample_info': False, - } - - @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: - parser.add_argument( - '--node', - type=node_id_like, - dest='nodes', - default=[], - action='append', - help='List of nodes to display as well.', - ) - parser.add_argument( - '--node-delta', - type=arg_pair_of(node_id_like, node_id_like), - dest='node_deltas', - default=[], - action='append', - help='List of nodes to display delta for.', - ) - parser.add_argument( - '--failure-information', - dest='failure_info', - default=None, - action='store_true', - help='Show failure summary for cfg', - ) - parser.add_argument( - '--no-failure-information', - dest='failure_info', - action='store_false', - help='Do not show failure summary for cfg', - ) - parser.add_argument( - '--to-module', dest='to_module', default=None, action='store_true', help='Output edges as a K module.' - ) - parser.add_argument( - '--pending', dest='pending', default=None, action='store_true', help='Also display pending nodes' - ) - parser.add_argument( - '--failing', dest='failing', default=None, action='store_true', help='Also display failing nodes' - ) - parser.add_argument( - '--counterexample-information', - dest='counterexample_info', - default=None, - action='store_true', - help="Show models for failing nodes. Should be called with the '--failure-information' flag", - ) - return parser - - class KProveOptions(Options): debug_equations: list[str] always_check_subsumption: bool @@ -486,75 +322,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: return parser -class ProveOptions( - LoggingOptions, - KOptions, - ParallelOptions, - KProveOptions, - BugReportOptions, - SMTOptions, - ExploreOptions, - SpecOptions, - RPCOptions, -): - reinit: bool - - @staticmethod - def default() -> dict[str, Any]: - return { - 'reinit': False, - } - - @staticmethod - def parser(base: _SubParsersAction) -> _SubParsersAction: - base.add_parser( - 'prove', - help='Run KEVM proof.', - parents=[ProveOptions.all_args()], - ) - return base - - @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: - parser.add_argument( - '--reinit', - dest='reinit', - default=None, - action='store_true', - help='Reinitialize CFGs even if they already exist.', - ) - return parser - - -class VersionOptions(LoggingOptions): - @staticmethod - def parser(base: _SubParsersAction) -> _SubParsersAction: - base.add_parser( - 'version', - help='Print KEVM version and exit.', - parents=[VersionOptions.all_args()], - ) - return base - - -class PruneProofOptions(LoggingOptions, KOptions, SpecOptions): - node: NodeIdLike - - @staticmethod - def parser(base: _SubParsersAction) -> _SubParsersAction: - base.add_parser( - 'prune-proof', - help='Remove a node and its successors from the proof state.', - parents=[PruneProofOptions.all_args()], - ) - return base - - @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: - parser.add_argument('node', type=node_id_like, help='Node to remove CFG subgraph from.') - return parser - - class KProveLegacyOptions(Options): bug_report: bool debugger: bool @@ -619,43 +386,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: return parser -class ProveLegacyOptions(LoggingOptions, KOptions, SpecOptions, KProveLegacyOptions): - bug_report_legacy: bool - - @staticmethod - def default() -> dict[str, Any]: - return { - 'bug_report_legacy': False, - } - - @staticmethod - def parser(base: _SubParsersAction) -> _SubParsersAction: - base.add_parser( - 'prove-legacy', - help='Run KEVM proof using the legacy kprove binary.', - parents=[ProveLegacyOptions.all_args()], - ) - return base - - @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: - parser.add_argument( - '--bug-report-legacy', default=None, action='store_true', help='Generate a legacy bug report.' - ) - return parser - - -class ViewKCFGOptions(LoggingOptions, KOptions, SpecOptions): - @staticmethod - def parser(base: _SubParsersAction) -> _SubParsersAction: - base.add_parser( - 'view-kcfg', - help='Explore a given proof in the KCFG visualizer.', - parents=[ViewKCFGOptions.all_args()], - ) - return base - - class TargetOptions(Options): target: str @@ -724,91 +454,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: return parser -class RunOptions(LoggingOptions, KOptions, TargetOptions, EVMChainOptions, 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 parser(base: _SubParsersAction) -> _SubParsersAction: - base.add_parser( - 'run', - help='Run KEVM test/simulation.', - parents=[RunOptions.all_args()], - ) - return base - - @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: - parser.add_argument('input_file', type=file_path, help='Path to input file.') - parser.add_argument( - '--output', - default=None, - type=KRunOutput, - choices=list(KRunOutput), - ) - parser.add_argument( - '--expand-macros', - dest='expand_macros', - default=None, - action='store_true', - help='Expand macros on the input term before execution.', - ) - parser.add_argument( - '--no-expand-macros', - dest='expand_macros', - action='store_false', - help='Do not expand macros on the input term before execution.', - ) - parser.add_argument( - '--debugger', - dest='debugger', - action='store_true', - help='Run GDB debugger for execution.', - ) - return parser - - -class KastOptions(LoggingOptions, TargetOptions, EVMChainOptions, SaveDirOptions): - input_file: Path - output: PrintOutput - - @staticmethod - def default() -> dict[str, Any]: - return { - 'output': PrintOutput.KORE, - } - - @staticmethod - def parser(base: _SubParsersAction) -> _SubParsersAction: - base.add_parser( - 'kast', - help='Run KEVM program.', - parents=[KastOptions.all_args()], - ) - return base - - @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: - parser.add_argument('input_file', type=file_path, help='Path to input file.') - parser.add_argument( - '--output', - default=None, - type=PrintOutput, - choices=list(PrintOutput), - ) - return parser - - class KEVMCLIArgs: @cached_property diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 5b39a0afef..3d77af61c4 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -9,8 +9,7 @@ from pyk.proof.reachability import APRProof from kevm_pyk import config -from kevm_pyk.__main__ import exec_prove -from kevm_pyk.cli import ProveOptions +from kevm_pyk.__main__ import ProveCommand from kevm_pyk.kevm import KEVM from kevm_pyk.kompile import KompileTarget, kevm_kompile @@ -224,7 +223,7 @@ def test_pyk_prove( name = str(spec_file.relative_to(SPEC_DIR)) break_on_calls = name in TEST_PARAMS and TEST_PARAMS[name].break_on_calls - options = ProveOptions( + options = ProveCommand( { 'spec_file': spec_file, 'definition_dir': definition_dir, @@ -237,7 +236,7 @@ def test_pyk_prove( } ) - exec_prove(options) + options.exec() if name in TEST_PARAMS: params = TEST_PARAMS[name] if params.leaf_number is not None and params.main_claim_id is not None: From 07d4fd4873d8dc1bf1152110fe67d621001759cb Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Mon, 4 Mar 2024 18:00:39 -0600 Subject: [PATCH 10/28] Remove default=None, use default() for lists --- kevm-pyk/src/kevm_pyk/__main__.py | 30 ++++------------- kevm-pyk/src/kevm_pyk/cli.py | 54 ++++++++----------------------- 2 files changed, 21 insertions(+), 63 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index a7bda88a76..72178a8f8c 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -139,9 +139,7 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '-o', '--output-definition', type=Path, dest='output_dir', help='Path to write kompiled definition to.' ) - parser.add_argument( - '--debug-build', dest='debug_build', default=None, help='Enable debug symbols in LLVM builds.' - ) + parser.add_argument('--debug-build', dest='debug_build', help='Enable debug symbols in LLVM builds.') return parser def exec(self) -> None: @@ -202,6 +200,8 @@ def default() -> dict[str, Any]: 'pending': False, 'failing': False, 'counterexample_info': False, + 'nodes': [], + 'node_deltas': [], } @staticmethod @@ -210,7 +210,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: '--node', type=node_id_like, dest='nodes', - default=[], action='append', help='List of nodes to display as well.', ) @@ -218,14 +217,12 @@ def args(parser: ArgumentParser) -> ArgumentParser: '--node-delta', type=arg_pair_of(node_id_like, node_id_like), dest='node_deltas', - default=[], action='append', help='List of nodes to display delta for.', ) parser.add_argument( '--failure-information', dest='failure_info', - default=None, action='store_true', help='Show failure summary for cfg', ) @@ -235,19 +232,12 @@ def args(parser: ArgumentParser) -> ArgumentParser: action='store_false', help='Do not show failure summary for cfg', ) - parser.add_argument( - '--to-module', dest='to_module', default=None, action='store_true', help='Output edges as a K module.' - ) - parser.add_argument( - '--pending', dest='pending', default=None, action='store_true', help='Also display pending nodes' - ) - parser.add_argument( - '--failing', dest='failing', default=None, action='store_true', help='Also display failing nodes' - ) + parser.add_argument('--to-module', dest='to_module', action='store_true', help='Output edges as a K module.') + parser.add_argument('--pending', dest='pending', action='store_true', help='Also display pending nodes') + parser.add_argument('--failing', dest='failing', action='store_true', help='Also display failing nodes') parser.add_argument( '--counterexample-information', dest='counterexample_info', - default=None, action='store_true', help="Show models for failing nodes. Should be called with the '--failure-information' flag", ) @@ -412,7 +402,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--reinit', dest='reinit', - default=None, action='store_true', help='Reinitialize CFGs even if they already exist.', ) @@ -673,9 +662,7 @@ def default() -> dict[str, Any]: @staticmethod def args(parser: ArgumentParser) -> ArgumentParser: - parser.add_argument( - '--bug-report-legacy', default=None, action='store_true', help='Generate a legacy bug report.' - ) + parser.add_argument('--bug-report-legacy', action='store_true', help='Generate a legacy bug report.') return parser def exec(self) -> None: @@ -776,14 +763,12 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument('input_file', type=file_path, help='Path to input file.') parser.add_argument( '--output', - default=None, type=KRunOutput, choices=list(KRunOutput), ) parser.add_argument( '--expand-macros', dest='expand_macros', - default=None, action='store_true', help='Expand macros on the input term before execution.', ) @@ -851,7 +836,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument('input_file', type=file_path, help='Path to input file.') parser.add_argument( '--output', - default=None, type=PrintOutput, choices=list(PrintOutput), ) diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index f225adeca3..b9dab197a7 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -36,7 +36,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--sort-collections', dest='sort_collections', - default=None, action='store_true', help='Sort collections before outputting term.', ) @@ -52,7 +51,7 @@ def default() -> dict[str, Any]: @staticmethod def args(parser: ArgumentParser) -> ArgumentParser: - parser.add_argument('--depth', default=None, type=int, help='Maximum depth to execute to.') + parser.add_argument('--depth', type=int, help='Maximum depth to execute to.') return parser @@ -63,23 +62,18 @@ class KProveOptions(Options): @staticmethod def default() -> dict[str, Any]: - return { - 'always_check_subsumption': True, - 'fast_check_subsumption': False, - } + return {'always_check_subsumption': True, 'fast_check_subsumption': False, 'debug_equations': []} @staticmethod def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--debug-equations', type=list_of(str, delim=','), - default=[], help='Comma-separate list of equations to debug.', ) parser.add_argument( '--always-check-subsumption', dest='always_check_subsumption', - default=None, action='store_true', help='Check subsumption even on non-terminal nodes.', ) @@ -92,7 +86,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--fast-check-subsumption', dest='fast_check_subsumption', - default=None, action='store_true', help='Use fast-check on k-cell to determine subsumption.', ) @@ -127,7 +120,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--trace-rewrites', dest='trace_rewrites', - default=None, action='store_true', help='Log traces of all simplification and rewrite rule applications.', ) @@ -135,13 +127,11 @@ def args(parser: ArgumentParser) -> ArgumentParser: '--kore-rpc-command', dest='kore_rpc_command', type=str, - default=None, help='Custom command to start RPC server', ) parser.add_argument( '--use-booster', dest='use_booster', - default=None, action='store_true', help='Use the booster RPC server instead of kore-rpc.', ) @@ -154,7 +144,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--post-exec-simplify', dest='post_exec_simplify', - default=None, action='store_true', help='Always simplify states with kore backend after booster execution, only usable with --use-booster.', ) @@ -174,14 +163,12 @@ def args(parser: ArgumentParser) -> ArgumentParser: '--port', dest='port', type=int, - default=None, help='Use existing RPC server on named port', ) parser.add_argument( '--maude-port', dest='maude_port', type=int, - default=None, help='Use existing Maude RPC server on named port', ) return parser @@ -221,63 +208,54 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--break-every-step', dest='break_every_step', - default=None, action='store_true', help='Store a node for every EVM opcode step (expensive).', ) parser.add_argument( '--break-on-jumpi', dest='break_on_jumpi', - default=None, action='store_true', help='Store a node for every EVM jump opcode.', ) parser.add_argument( '--break-on-calls', dest='break_on_calls', - default=None, action='store_true', help='Store a node for every EVM call made.', ) parser.add_argument( '--no-break-on-calls', dest='break_on_calls', - default=None, action='store_false', help='Do not store a node for every EVM call made.', ) parser.add_argument( '--break-on-storage', dest='break_on_storage', - default=None, action='store_true', help='Store a node for every EVM SSTORE/SLOAD made.', ) parser.add_argument( '--break-on-basic-blocks', dest='break_on_basic_blocks', - default=None, action='store_true', help='Store a node for every EVM basic block (implies --break-on-calls).', ) parser.add_argument( '--max-depth', dest='max_depth', - default=None, type=int, help='Maximum number of K steps before the state is saved in a new node in the CFG. Branching will cause this to happen earlier.', ) parser.add_argument( '--max-iterations', dest='max_iterations', - default=None, type=int, help='Number of times to expand the next pending node in the CFG.', ) parser.add_argument( '--failure-information', dest='failure_info', - default=None, action='store_true', help='Show failure summary for all failing tests', ) @@ -296,7 +274,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--counterexample-information', dest='counterexample_info', - default=None, action='store_true', help='Show models for failing nodes.', ) @@ -309,7 +286,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--fail-fast', dest='fail_fast', - default=None, action='store_true', help='Stop execution on other branches if a failing node is detected.', ) @@ -338,27 +314,25 @@ def default() -> dict[str, Any]: 'max_depth': None, 'max_counterexamples': None, 'branching_allowed': None, + 'haskell_backend_args': [], } @staticmethod def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--bug-report', - default=None, action='store_true', help='Generate a haskell-backend bug report for the execution.', ) parser.add_argument( '--debugger', dest='debugger', - default=None, action='store_true', help='Launch proof in an interactive debugger.', ) parser.add_argument( '--max-depth', dest='max_depth', - default=None, type=int, help='The maximum number of computational steps to prove.', ) @@ -366,20 +340,17 @@ def args(parser: ArgumentParser) -> ArgumentParser: '--max-counterexamples', type=int, dest='max_counterexamples', - default=None, help='Maximum number of counterexamples reported before a forcible stop.', ) parser.add_argument( '--branching-allowed', type=int, dest='branching_allowed', - default=None, help='Number of branching events allowed before a forcible stop.', ) parser.add_argument( '--haskell-backend-arg', dest='haskell_backend_args', - default=[], action='append', help='Arguments passed to the Haskell backend execution engine.', ) @@ -438,23 +409,28 @@ def args(parser: ArgumentParser) -> ArgumentParser: parser.add_argument( '--schedule', choices=schedules, - default=None, help=f"schedule to use for execution [{'|'.join(schedules)}]", ) - parser.add_argument('--chainid', type=int, default=None, help='chain ID to use for execution') + parser.add_argument('--chainid', type=int, help='chain ID to use for execution') parser.add_argument( '--mode', choices=modes, - default=None, help="execution mode to use [{'|'.join(modes)}]", ) - parser.add_argument( - '--no-gas', action='store_false', dest='usegas', default=None, help='omit gas cost computations' - ) + parser.add_argument('--no-gas', action='store_false', dest='usegas', help='omit gas cost computations') return parser class KEVMCLIArgs: + requires: list[str] + imports: list[str] + + @staticmethod + def default() -> dict[str, Any]: + return { + 'requires': [], + 'imports': [], + } @cached_property def k_gen_args(self) -> ArgumentParser: @@ -462,14 +438,12 @@ def k_gen_args(self) -> ArgumentParser: args.add_argument( '--require', dest='requires', - default=[], action='append', help='Extra K requires to include in generated output.', ) args.add_argument( '--module-import', dest='imports', - default=[], action='append', help='Extra modules to import into generated main module.', ) From bcc12fa07508c0952123b480b6cc00241bce08eb Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Mon, 4 Mar 2024 18:12:56 -0600 Subject: [PATCH 11/28] Rename args to update_args, don't return parser when updating --- kevm-pyk/src/kevm_pyk/__main__.py | 21 +++++++-------------- kevm-pyk/src/kevm_pyk/cli.py | 24 ++++++++---------------- 2 files changed, 15 insertions(+), 30 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 72178a8f8c..dcd5da653a 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -133,14 +133,13 @@ def default() -> dict[str, Any]: } @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: + def update_args(parser: ArgumentParser) -> None: parser.add_argument('main_file', type=file_path, help='Path to file with main module.') parser.add_argument('--target', type=KompileTarget, help='[haskell|maude]') parser.add_argument( '-o', '--output-definition', type=Path, dest='output_dir', help='Path to write kompiled definition to.' ) parser.add_argument('--debug-build', dest='debug_build', help='Enable debug symbols in LLVM builds.') - return parser def exec(self) -> None: if self.target not in [KompileTarget.HASKELL, KompileTarget.MAUDE]: @@ -205,7 +204,7 @@ def default() -> dict[str, Any]: } @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: + def update_args(parser: ArgumentParser) -> None: parser.add_argument( '--node', type=node_id_like, @@ -241,7 +240,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: action='store_true', help="Show models for failing nodes. Should be called with the '--failure-information' flag", ) - return parser def exec(self) -> None: if self.definition_dir is None: @@ -398,14 +396,13 @@ def default() -> dict[str, Any]: } @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: + def update_args(parser: ArgumentParser) -> None: parser.add_argument( '--reinit', dest='reinit', action='store_true', help='Reinitialize CFGs even if they already exist.', ) - return parser def exec(self) -> None: md_selector = 'k' @@ -607,9 +604,8 @@ def help_str() -> str: return 'Remove a node and its successors from the proof state.' @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: + def update_args(parser: ArgumentParser) -> None: parser.add_argument('node', type=node_id_like, help='Node to remove CFG subgraph from.') - return parser def exec(self) -> None: md_selector = 'k' @@ -661,9 +657,8 @@ def default() -> dict[str, Any]: } @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: + def update_args(parser: ArgumentParser) -> None: parser.add_argument('--bug-report-legacy', action='store_true', help='Generate a legacy bug report.') - return parser def exec(self) -> None: definition_dir = self.definition_dir @@ -759,7 +754,7 @@ def default() -> dict[str, Any]: } @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: + def update_args(parser: ArgumentParser) -> None: parser.add_argument('input_file', type=file_path, help='Path to input file.') parser.add_argument( '--output', @@ -784,7 +779,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: action='store_true', help='Run GDB debugger for execution.', ) - return parser def exec(self) -> None: target_fqn = f'evm-semantics.{self.target}' @@ -832,14 +826,13 @@ def default() -> dict[str, Any]: } @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: + def update_args(parser: ArgumentParser) -> None: parser.add_argument('input_file', type=file_path, help='Path to input file.') parser.add_argument( '--output', type=PrintOutput, choices=list(PrintOutput), ) - return parser def exec(self) -> None: target_fqn = f'evm-semantics.{self.target}' diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index b9dab197a7..454302bb05 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -32,14 +32,13 @@ def default() -> dict[str, Any]: return {'sort_collections': False} @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: + def update_args(parser: ArgumentParser) -> None: parser.add_argument( '--sort-collections', dest='sort_collections', action='store_true', help='Sort collections before outputting term.', ) - return parser class KOptions(KDefinitionOptions): @@ -50,9 +49,8 @@ def default() -> dict[str, Any]: return {'depth': None} @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: + def update_args(parser: ArgumentParser) -> None: parser.add_argument('--depth', type=int, help='Maximum depth to execute to.') - return parser class KProveOptions(Options): @@ -65,7 +63,7 @@ def default() -> dict[str, Any]: return {'always_check_subsumption': True, 'fast_check_subsumption': False, 'debug_equations': []} @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: + def update_args(parser: ArgumentParser) -> None: parser.add_argument( '--debug-equations', type=list_of(str, delim=','), @@ -89,7 +87,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: action='store_true', help='Use fast-check on k-cell to determine subsumption.', ) - return parser class RPCOptions(Options): @@ -116,7 +113,7 @@ def default() -> dict[str, Any]: } @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: + def update_args(parser: ArgumentParser) -> None: parser.add_argument( '--trace-rewrites', dest='trace_rewrites', @@ -171,7 +168,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: type=int, help='Use existing Maude RPC server on named port', ) - return parser class ExploreOptions(Options): @@ -204,7 +200,7 @@ def default() -> dict[str, Any]: } @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: + def update_args(parser: ArgumentParser) -> None: parser.add_argument( '--break-every-step', dest='break_every_step', @@ -295,7 +291,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: action='store_false', help='Continue execution on other branches if a failing node is detected.', ) - return parser class KProveLegacyOptions(Options): @@ -318,7 +313,7 @@ def default() -> dict[str, Any]: } @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: + def update_args(parser: ArgumentParser) -> None: parser.add_argument( '--bug-report', action='store_true', @@ -354,7 +349,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: action='append', help='Arguments passed to the Haskell backend execution engine.', ) - return parser class TargetOptions(Options): @@ -367,9 +361,8 @@ def default() -> dict[str, Any]: } @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: + def update_args(parser: ArgumentParser) -> None: parser.add_argument('--target', choices=['llvm', 'haskell', 'haskell-standalone', 'foundry']) - return parser class EVMChainOptions(Options): @@ -388,7 +381,7 @@ def default() -> dict[str, Any]: } @staticmethod - def args(parser: ArgumentParser) -> ArgumentParser: + def update_args(parser: ArgumentParser) -> None: schedules = ( 'DEFAULT', 'FRONTIER', @@ -418,7 +411,6 @@ def args(parser: ArgumentParser) -> ArgumentParser: help="execution mode to use [{'|'.join(modes)}]", ) parser.add_argument('--no-gas', action='store_false', dest='usegas', help='omit gas cost computations') - return parser class KEVMCLIArgs: From ebcf30b1f4d244b93a67879272096298d7055fa7 Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Tue, 5 Mar 2024 15:17:28 -0600 Subject: [PATCH 12/28] Update for new pyk branch version --- kevm-pyk/poetry.lock | 10 +++++----- kevm-pyk/pyproject.toml | 4 ++-- kevm-pyk/src/kevm_pyk/__main__.py | 12 ++---------- 3 files changed, 9 insertions(+), 17 deletions(-) diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index ae2248cd8a..915c5aa473 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -1,4 +1,4 @@ -# This file is automatically @generated by Poetry 1.8.1 and should not be changed by hand. +# This file is automatically @generated by Poetry 1.6.1 and should not be changed by hand. [[package]] name = "attrs" @@ -814,7 +814,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pyk" -version = "0.1.675" +version = "0.1.682" description = "" optional = false python-versions = "^3.10" @@ -835,8 +835,8 @@ xdg-base-dirs = "^6.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.675" -resolved_reference = "223cd775151e96051fc560849a9c4e2e7fb01a2e" +reference = "noah/default-options" +resolved_reference = "fdbfc37112780718afd0039fe82af960a65e6da2" [[package]] name = "pyperclip" @@ -1116,4 +1116,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "1842222e8a6a9d21a16340704f7cd91a2eaef38c63e1feb462882aaac2a84e09" +content-hash = "a0691f5001072ff9b3bd87d11d453206d425029f5c535fb89b0e43a4e0952566" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index eae11cb4e3..610960ee3d 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -13,8 +13,8 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -# pyk = { git = "https://github.com/runtimeverification/pyk.git", branch="noah/default-options" } -pyk = { path = "/home/noah/dev/pyk", develop=true } +pyk = { git = "https://github.com/runtimeverification/pyk.git", branch="noah/default-options" } +# pyk = { path = "/home/noah/dev/pyk", develop=true } tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index dcd5da653a..622b04acca 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -14,16 +14,8 @@ from typing import TYPE_CHECKING from pathos.pools import ProcessPool # type: ignore -from pyk.cli.args import ( - CLI, - BugReportOptions, - Command, - KompileOptions, - ParallelOptions, - SaveDirOptions, - SMTOptions, - SpecOptions, -) +from pyk.cli.args import BugReportOptions, KompileOptions, ParallelOptions, SaveDirOptions, SMTOptions, SpecOptions +from pyk.cli.cli import CLI, Command from pyk.cli.utils import file_path from pyk.cterm import CTerm from pyk.kast.outer import KApply, KRewrite, KSort, KToken From 44c2ee4e200463bf196763d77ec5507eba1cac83 Mon Sep 17 00:00:00 2001 From: devops <devops@runtimeverification.com> Date: Tue, 5 Mar 2024 21:19:53 +0000 Subject: [PATCH 13/28] Set Version: 1.0.480 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 1b3ee1a0c4..53ab1d260a 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.479" +version = "1.0.480" description = "" authors = [ "Runtime Verification, Inc. <contact@runtimeverification.com>", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 8f66f09222..dce4a067a3 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.479' +VERSION: Final = '1.0.480' diff --git a/package/version b/package/version index 2b3ce9eab0..35864cde42 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.479 +1.0.480 From 8d29e0b26da50ec1e75e0c2fb931318fc08fb5d9 Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Tue, 5 Mar 2024 15:28:02 -0600 Subject: [PATCH 14/28] Update poetry.lock --- kevm-pyk/poetry.lock | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index e7418cefde..9c9fff2a70 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -1,4 +1,4 @@ -# This file is automatically @generated by Poetry 1.6.1 and should not be changed by hand. +# This file is automatically @generated by Poetry 1.8.2 and should not be changed by hand. [[package]] name = "attrs" @@ -814,7 +814,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pyk" -version = "0.1.682" +version = "0.1.675" description = "" optional = false python-versions = "^3.10" @@ -835,8 +835,8 @@ xdg-base-dirs = "^6.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "noah/default-options" -resolved_reference = "fdbfc37112780718afd0039fe82af960a65e6da2" +reference = "v0.1.675" +resolved_reference = "223cd775151e96051fc560849a9c4e2e7fb01a2e" [[package]] name = "pyperclip" @@ -1116,4 +1116,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "a0691f5001072ff9b3bd87d11d453206d425029f5c535fb89b0e43a4e0952566" +content-hash = "6462f817ef63c7f1205edb873da5bcd6d22c1bba47168976d02910934d598606" From 0eb2998d517b79419d7161475b8c222eff9f7d94 Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Tue, 5 Mar 2024 15:28:23 -0600 Subject: [PATCH 15/28] Update poetry.lock --- kevm-pyk/poetry.lock | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 9c9fff2a70..7b67a7278a 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -1,4 +1,4 @@ -# This file is automatically @generated by Poetry 1.8.2 and should not be changed by hand. +# This file is automatically @generated by Poetry 1.6.1 and should not be changed by hand. [[package]] name = "attrs" @@ -814,7 +814,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pyk" -version = "0.1.675" +version = "0.1.682" description = "" optional = false python-versions = "^3.10" @@ -835,8 +835,8 @@ xdg-base-dirs = "^6.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.675" -resolved_reference = "223cd775151e96051fc560849a9c4e2e7fb01a2e" +reference = "noah/default-options" +resolved_reference = "2e6885fdaf813b3fe130f4651346e8f77983e86a" [[package]] name = "pyperclip" @@ -1116,4 +1116,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "6462f817ef63c7f1205edb873da5bcd6d22c1bba47168976d02910934d598606" +content-hash = "f9c9cf626577f8f7c110ed6f5d6464485ba9de1abe9047785163e77bd406073e" From 42d7035a6362417666c9eebf4f50adf28c658cee Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Tue, 5 Mar 2024 16:15:31 -0600 Subject: [PATCH 16/28] Update pyproject.toml --- kevm-pyk/pyproject.toml | 1 - 1 file changed, 1 deletion(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 53ab1d260a..3838f134ec 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -14,7 +14,6 @@ authors = [ python = "^3.10" pathos = "*" pyk = { git = "https://github.com/runtimeverification/pyk.git", branch="noah/default-options" } -# pyk = { path = "/home/noah/dev/pyk", develop=true } tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] From f07165356fabffab8abfc4ef8b3823490f05df2e Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Tue, 5 Mar 2024 16:41:49 -0600 Subject: [PATCH 17/28] update poetry.lock --- kevm-pyk/poetry.lock | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 7b67a7278a..7aaab46584 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -814,7 +814,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pyk" -version = "0.1.682" +version = "0.1.683" description = "" optional = false python-versions = "^3.10" @@ -836,7 +836,7 @@ xdg-base-dirs = "^6.0.1" type = "git" url = "https://github.com/runtimeverification/pyk.git" reference = "noah/default-options" -resolved_reference = "2e6885fdaf813b3fe130f4651346e8f77983e86a" +resolved_reference = "6546289c2c74d3c874e38d7dd53b3ebedd3dce5d" [[package]] name = "pyperclip" From 48b1bb2e2d584a5fc5b5c383d4007139c5fa11e3 Mon Sep 17 00:00:00 2001 From: devops <devops@runtimeverification.com> Date: Tue, 5 Mar 2024 22:45:33 +0000 Subject: [PATCH 18/28] Set Version: 1.0.481 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 3838f134ec..75aea53ef6 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.480" +version = "1.0.481" description = "" authors = [ "Runtime Verification, Inc. <contact@runtimeverification.com>", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index dce4a067a3..0d19172da0 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.480' +VERSION: Final = '1.0.481' diff --git a/package/version b/package/version index 35864cde42..45f0b1a188 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.480 +1.0.481 From 39a83f7ae33a02b2fab67d72648ba4d80af3bfb3 Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Wed, 6 Mar 2024 13:45:30 -0600 Subject: [PATCH 19/28] Update to use CLI.get_command() --- kevm-pyk/src/kevm_pyk/__main__.py | 39 ++++++++++++++++++------------- 1 file changed, 23 insertions(+), 16 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 622b04acca..934c563833 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -14,7 +14,15 @@ from typing import TYPE_CHECKING from pathos.pools import ProcessPool # type: ignore -from pyk.cli.args import BugReportOptions, KompileOptions, ParallelOptions, SaveDirOptions, SMTOptions, SpecOptions +from pyk.cli.args import ( + BugReportOptions, + KompileOptions, + LoggingOptions, + ParallelOptions, + SaveDirOptions, + SMTOptions, + SpecOptions, +) from pyk.cli.cli import CLI, Command from pyk.cli.utils import file_path from pyk.cterm import CTerm @@ -56,7 +64,7 @@ ) if TYPE_CHECKING: - from argparse import ArgumentParser, Namespace + from argparse import ArgumentParser from collections.abc import Callable, Iterable, Iterator from typing import Any, Final, TypeVar @@ -94,15 +102,13 @@ def main() -> None: ViewKCFGCommand, ) ) - parser = kevm_cli.create_argument_parser() - args = parser.parse_args() - - logging.basicConfig(level=_loglevel(args), format=_LOG_FORMAT) - command = kevm_cli.generate_command({key: val for (key, val) in vars(args).items() if val is not None}) + command = kevm_cli.get_command() + assert isinstance(command, LoggingOptions) + logging.basicConfig(level=_loglevel(command), format=_LOG_FORMAT) command.exec() -class KompileSpecCommand(Command, KOptions, KompileOptions): +class KompileSpecCommand(Command, KOptions, KompileOptions, LoggingOptions): main_file: Path target: KompileTarget output_dir: Path @@ -166,7 +172,7 @@ def exec(self) -> None: ) -class ShowKCFGCommand(Command, KOptions, SpecOptions, KEVMDisplayOptions): +class ShowKCFGCommand(Command, KOptions, SpecOptions, KEVMDisplayOptions, LoggingOptions): nodes: list[NodeIdLike] node_deltas: list[tuple[NodeIdLike, NodeIdLike]] failure_info: bool @@ -370,6 +376,7 @@ class ProveCommand( ExploreOptions, SpecOptions, RPCOptions, + LoggingOptions, ): reinit: bool @@ -571,7 +578,7 @@ def _init_and_run_proof(claim_job: KClaimJob) -> tuple[bool, list[str] | None]: sys.exit(failed) -class VersionCommand(Command): +class VersionCommand(Command, LoggingOptions): @staticmethod def name() -> str: return 'version' @@ -584,7 +591,7 @@ def exec(self) -> None: print(f'KEVM Version: {VERSION}') -class PruneProofCommand(Command, KOptions, SpecOptions): +class PruneProofCommand(Command, KOptions, SpecOptions, LoggingOptions): node: NodeIdLike @staticmethod @@ -631,7 +638,7 @@ def exec(self) -> None: apr_proof.write_proof_data() -class ProveLegacyCommand(Command, KOptions, SpecOptions, KProveLegacyOptions): +class ProveLegacyCommand(Command, KOptions, SpecOptions, KProveLegacyOptions, LoggingOptions): bug_report_legacy: bool @staticmethod @@ -682,7 +689,7 @@ def exec(self) -> None: raise SystemExit(1) -class ViewKCFGCommand(Command, KOptions, SpecOptions): +class ViewKCFGCommand(Command, KOptions, SpecOptions, LoggingOptions): @staticmethod def name() -> str: return 'view-kcfg' @@ -723,7 +730,7 @@ def custom_view(element: KCFGElem) -> list[str]: proof_view.run() -class RunCommand(Command, KOptions, TargetOptions, EVMChainOptions, SaveDirOptions): +class RunCommand(Command, KOptions, TargetOptions, EVMChainOptions, SaveDirOptions, LoggingOptions): input_file: Path output: KRunOutput expand_macros: bool @@ -799,7 +806,7 @@ def exec(self) -> None: ) -class KastCommand(Command, TargetOptions, EVMChainOptions, SaveDirOptions): +class KastCommand(Command, TargetOptions, EVMChainOptions, SaveDirOptions, LoggingOptions): input_file: Path output: PrintOutput @@ -849,7 +856,7 @@ def exec(self) -> None: # Helpers -def _loglevel(args: Namespace) -> int: +def _loglevel(args: LoggingOptions) -> int: if args.debug: return logging.DEBUG From 5ee91e87956ff12e4a3202a845d05ab26db513d3 Mon Sep 17 00:00:00 2001 From: devops <devops@runtimeverification.com> Date: Wed, 6 Mar 2024 19:48:18 +0000 Subject: [PATCH 20/28] Set Version: 1.0.483 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 04ffa01f00..560e186b1c 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.482" +version = "1.0.483" description = "" authors = [ "Runtime Verification, Inc. <contact@runtimeverification.com>", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 9fd27fad1b..eaa6796854 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.482' +VERSION: Final = '1.0.483' diff --git a/package/version b/package/version index be59341a70..62fbca6cbc 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.482 +1.0.483 From 29e4803789432971dac2030b21c5d6d39ae3b008 Mon Sep 17 00:00:00 2001 From: devops <devops@runtimeverification.com> Date: Wed, 6 Mar 2024 21:40:40 +0000 Subject: [PATCH 21/28] Set Version: 1.0.484 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 560e186b1c..956f1054cf 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.483" +version = "1.0.484" description = "" authors = [ "Runtime Verification, Inc. <contact@runtimeverification.com>", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index eaa6796854..f7dc8a362d 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.483' +VERSION: Final = '1.0.484' diff --git a/package/version b/package/version index 62fbca6cbc..2597f4c655 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.483 +1.0.484 From 7c6cb8c03e046104501fec2b511388725387920a Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Wed, 6 Mar 2024 21:21:59 -0600 Subject: [PATCH 22/28] Merge master into branch --- kevm-pyk/poetry.lock | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 8cdec9fb48..65de5d3e87 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -836,7 +836,7 @@ xdg-base-dirs = "^6.0.1" type = "git" url = "https://github.com/runtimeverification/pyk.git" reference = "noah/default-options" -resolved_reference = "7e872808b932c07c15d56364a1843c983997204a" +resolved_reference = "2f58d508170fd354fedb9824c17a22ed495c9051" [[package]] name = "pyperclip" From bb545100da6ab23963135971650a31cf1e4e8c7b Mon Sep 17 00:00:00 2001 From: devops <devops@runtimeverification.com> Date: Thu, 7 Mar 2024 03:23:25 +0000 Subject: [PATCH 23/28] Set Version: 1.0.485 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 5267871154..4b5715e278 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.484" +version = "1.0.485" description = "" authors = [ "Runtime Verification, Inc. <contact@runtimeverification.com>", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index f7dc8a362d..2888bbf053 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.484' +VERSION: Final = '1.0.485' diff --git a/package/version b/package/version index 2597f4c655..8abaebbe9b 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.484 +1.0.485 From ee28f4d13b55a1ccbcb16865d73b1635676efe5b Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Fri, 8 Mar 2024 13:30:56 -0600 Subject: [PATCH 24/28] Fix formatting --- kevm-pyk/src/kevm_pyk/__main__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 108f48cdb0..1f6e54e80c 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -853,7 +853,6 @@ def exec(self) -> None: print(output_text) - class SectionEdgeCommand(Command, LoggingOptions, KOptions, SpecOptions, RPCOptions, BugReportOptions, SMTOptions): edge: tuple[str, str] sections: int @@ -935,6 +934,7 @@ def exec(self) -> None: ) proof.write_proof_data() + # Helpers From 6bd0b0407397907dc7b6f16524be7b82f66c730a Mon Sep 17 00:00:00 2001 From: devops <devops@runtimeverification.com> Date: Fri, 8 Mar 2024 19:39:03 +0000 Subject: [PATCH 25/28] Set Version: 1.0.490 --- package/version | 4 ---- 1 file changed, 4 deletions(-) diff --git a/package/version b/package/version index 4eee911e97..7021ba06ec 100644 --- a/package/version +++ b/package/version @@ -1,5 +1 @@ -<<<<<<< HEAD -1.0.485 -======= 1.0.490 ->>>>>>> origin/master From dcdbb26e06ba2c2c0368d2520c3a52cff319c41a Mon Sep 17 00:00:00 2001 From: devops <devops@runtimeverification.com> Date: Fri, 8 Mar 2024 19:43:09 +0000 Subject: [PATCH 26/28] Set Version: 1.0.491 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 8f0efdf346..74bd5a1a12 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.490" +version = "1.0.491" description = "" authors = [ "Runtime Verification, Inc. <contact@runtimeverification.com>", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index a78a28de51..249ea16fe1 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.490' +VERSION: Final = '1.0.491' diff --git a/package/version b/package/version index 7021ba06ec..3ba5134368 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.490 +1.0.491 From 5938605d5cacd65d12c7012b548f8010ade455f1 Mon Sep 17 00:00:00 2001 From: Noah Watson <noah@nwatson.xyz> Date: Fri, 8 Mar 2024 13:59:36 -0600 Subject: [PATCH 27/28] Update nix flake --- flake.lock | 8 ++++---- flake.nix | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/flake.lock b/flake.lock index 32ccd73360..8643333d5f 100644 --- a/flake.lock +++ b/flake.lock @@ -529,16 +529,16 @@ "poetry2nix": "poetry2nix" }, "locked": { - "lastModified": 1709859653, - "narHash": "sha256-p8DZ6hJkhdxu79YNp1wwzcrtt3fIC1aD5g4J+OviW4Y=", + "lastModified": 1709926220, + "narHash": "sha256-8f4tkKi2p/Oj7gpOZ09sozYbk3766URN4b/Qj61MD5c=", "owner": "runtimeverification", "repo": "pyk", - "rev": "e8537c085944d51c35fdd2ea50de46375c3b9d59", + "rev": "89d0c0270836df0420918bceec463aaf0986f436", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.691", + "ref": "noah/default-options", "repo": "pyk", "type": "github" } diff --git a/flake.nix b/flake.nix index aee8bc0155..da251c972c 100644 --- a/flake.nix +++ b/flake.nix @@ -6,7 +6,7 @@ nixpkgs.follows = "k-framework/nixpkgs"; flake-utils.follows = "k-framework/flake-utils"; rv-utils.follows = "k-framework/rv-utils"; - pyk.url = "github:runtimeverification/pyk/v0.1.691"; + pyk.url = "github:runtimeverification/pyk/noah/default-options"; nixpkgs-pyk.follows = "pyk/nixpkgs"; poetry2nix.follows = "pyk/poetry2nix"; blockchain-k-plugin = { From e0773c8c5f855731ecf5a1cf3cbf9ea94ca430d9 Mon Sep 17 00:00:00 2001 From: devops <devops@runtimeverification.com> Date: Mon, 11 Mar 2024 19:28:50 +0000 Subject: [PATCH 28/28] Set Version: 1.0.493 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index f84a4a19f3..91ec1a4689 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.492" +version = "1.0.493" description = "" authors = [ "Runtime Verification, Inc. <contact@runtimeverification.com>", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 176f3a8fa4..f40b3d75c4 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.492' +VERSION: Final = '1.0.493' diff --git a/package/version b/package/version index b9c0a675e9..cdf6f00a1c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.492 +1.0.493