diff --git a/package/version b/package/version index 63982f32f..9868d567e 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.194 +0.1.195 diff --git a/poetry.lock b/poetry.lock index 01fb8ab84..d653bdbcf 100644 --- a/poetry.lock +++ b/poetry.lock @@ -434,7 +434,7 @@ colors = ["colorama (>=0.4.6)"] [[package]] name = "kevm-pyk" -version = "1.0.489" +version = "1.0.493" description = "" optional = false python-versions = "^3.10" @@ -443,14 +443,14 @@ develop = false [package.dependencies] pathos = "*" -pyk = {git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.685"} +pyk = {git = "https://github.com/runtimeverification/pyk.git", branch = "noah/default-options"} tomlkit = "^0.11.6" [package.source] type = "git" url = "https://github.com/runtimeverification/evm-semantics.git" -reference = "v1.0.489" -resolved_reference = "302957e69c0410c884d546c27f96151e2c1793d2" +reference = "noah/kevm-default-options2" +resolved_reference = "32e329a47d714e0e3303409784a132b2677a68da" subdirectory = "kevm-pyk" [[package]] @@ -566,38 +566,38 @@ dill = ">=0.3.8" [[package]] name = "mypy" -version = "1.8.0" +version = "1.9.0" description = "Optional static typing for Python" optional = false python-versions = ">=3.8" files = [ - {file = "mypy-1.8.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:485a8942f671120f76afffff70f259e1cd0f0cfe08f81c05d8816d958d4577d3"}, - {file = "mypy-1.8.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:df9824ac11deaf007443e7ed2a4a26bebff98d2bc43c6da21b2b64185da011c4"}, - {file = "mypy-1.8.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:2afecd6354bbfb6e0160f4e4ad9ba6e4e003b767dd80d85516e71f2e955ab50d"}, - {file = "mypy-1.8.0-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:8963b83d53ee733a6e4196954502b33567ad07dfd74851f32be18eb932fb1cb9"}, - {file = "mypy-1.8.0-cp310-cp310-win_amd64.whl", hash = "sha256:e46f44b54ebddbeedbd3d5b289a893219065ef805d95094d16a0af6630f5d410"}, - {file = "mypy-1.8.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:855fe27b80375e5c5878492f0729540db47b186509c98dae341254c8f45f42ae"}, - {file = "mypy-1.8.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:4c886c6cce2d070bd7df4ec4a05a13ee20c0aa60cb587e8d1265b6c03cf91da3"}, - {file = "mypy-1.8.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d19c413b3c07cbecf1f991e2221746b0d2a9410b59cb3f4fb9557f0365a1a817"}, - {file = "mypy-1.8.0-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:9261ed810972061388918c83c3f5cd46079d875026ba97380f3e3978a72f503d"}, - {file = "mypy-1.8.0-cp311-cp311-win_amd64.whl", hash = "sha256:51720c776d148bad2372ca21ca29256ed483aa9a4cdefefcef49006dff2a6835"}, - {file = "mypy-1.8.0-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:52825b01f5c4c1c4eb0db253ec09c7aa17e1a7304d247c48b6f3599ef40db8bd"}, - {file = "mypy-1.8.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:f5ac9a4eeb1ec0f1ccdc6f326bcdb464de5f80eb07fb38b5ddd7b0de6bc61e55"}, - {file = "mypy-1.8.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:afe3fe972c645b4632c563d3f3eff1cdca2fa058f730df2b93a35e3b0c538218"}, - {file = "mypy-1.8.0-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:42c6680d256ab35637ef88891c6bd02514ccb7e1122133ac96055ff458f93fc3"}, - {file = "mypy-1.8.0-cp312-cp312-win_amd64.whl", hash = "sha256:720a5ca70e136b675af3af63db533c1c8c9181314d207568bbe79051f122669e"}, - {file = "mypy-1.8.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:028cf9f2cae89e202d7b6593cd98db6759379f17a319b5faf4f9978d7084cdc6"}, - {file = "mypy-1.8.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:4e6d97288757e1ddba10dd9549ac27982e3e74a49d8d0179fc14d4365c7add66"}, - {file = "mypy-1.8.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:7f1478736fcebb90f97e40aff11a5f253af890c845ee0c850fe80aa060a267c6"}, - {file = "mypy-1.8.0-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:42419861b43e6962a649068a61f4a4839205a3ef525b858377a960b9e2de6e0d"}, - {file = "mypy-1.8.0-cp38-cp38-win_amd64.whl", hash = "sha256:2b5b6c721bd4aabaadead3a5e6fa85c11c6c795e0c81a7215776ef8afc66de02"}, - {file = "mypy-1.8.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:5c1538c38584029352878a0466f03a8ee7547d7bd9f641f57a0f3017a7c905b8"}, - {file = "mypy-1.8.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:4ef4be7baf08a203170f29e89d79064463b7fc7a0908b9d0d5114e8009c3a259"}, - {file = "mypy-1.8.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:7178def594014aa6c35a8ff411cf37d682f428b3b5617ca79029d8ae72f5402b"}, - {file = "mypy-1.8.0-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:ab3c84fa13c04aeeeabb2a7f67a25ef5d77ac9d6486ff33ded762ef353aa5592"}, - {file = "mypy-1.8.0-cp39-cp39-win_amd64.whl", hash = "sha256:99b00bc72855812a60d253420d8a2eae839b0afa4938f09f4d2aa9bb4654263a"}, - {file = "mypy-1.8.0-py3-none-any.whl", hash = "sha256:538fd81bb5e430cc1381a443971c0475582ff9f434c16cd46d2c66763ce85d9d"}, - {file = "mypy-1.8.0.tar.gz", hash = "sha256:6ff8b244d7085a0b425b56d327b480c3b29cafbd2eff27316a004f9a7391ae07"}, + {file = "mypy-1.9.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:f8a67616990062232ee4c3952f41c779afac41405806042a8126fe96e098419f"}, + {file = "mypy-1.9.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:d357423fa57a489e8c47b7c85dfb96698caba13d66e086b412298a1a0ea3b0ed"}, + {file = "mypy-1.9.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:49c87c15aed320de9b438ae7b00c1ac91cd393c1b854c2ce538e2a72d55df150"}, + {file = "mypy-1.9.0-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:48533cdd345c3c2e5ef48ba3b0d3880b257b423e7995dada04248725c6f77374"}, + {file = "mypy-1.9.0-cp310-cp310-win_amd64.whl", hash = "sha256:4d3dbd346cfec7cb98e6cbb6e0f3c23618af826316188d587d1c1bc34f0ede03"}, + {file = "mypy-1.9.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:653265f9a2784db65bfca694d1edd23093ce49740b2244cde583aeb134c008f3"}, + {file = "mypy-1.9.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:3a3c007ff3ee90f69cf0a15cbcdf0995749569b86b6d2f327af01fd1b8aee9dc"}, + {file = "mypy-1.9.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:2418488264eb41f69cc64a69a745fad4a8f86649af4b1041a4c64ee61fc61129"}, + {file = "mypy-1.9.0-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:68edad3dc7d70f2f17ae4c6c1b9471a56138ca22722487eebacfd1eb5321d612"}, + {file = "mypy-1.9.0-cp311-cp311-win_amd64.whl", hash = "sha256:85ca5fcc24f0b4aeedc1d02f93707bccc04733f21d41c88334c5482219b1ccb3"}, + {file = "mypy-1.9.0-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:aceb1db093b04db5cd390821464504111b8ec3e351eb85afd1433490163d60cd"}, + {file = "mypy-1.9.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:0235391f1c6f6ce487b23b9dbd1327b4ec33bb93934aa986efe8a9563d9349e6"}, + {file = "mypy-1.9.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d4d5ddc13421ba3e2e082a6c2d74c2ddb3979c39b582dacd53dd5d9431237185"}, + {file = "mypy-1.9.0-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:190da1ee69b427d7efa8aa0d5e5ccd67a4fb04038c380237a0d96829cb157913"}, + {file = "mypy-1.9.0-cp312-cp312-win_amd64.whl", hash = "sha256:fe28657de3bfec596bbeef01cb219833ad9d38dd5393fc649f4b366840baefe6"}, + {file = "mypy-1.9.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:e54396d70be04b34f31d2edf3362c1edd023246c82f1730bbf8768c28db5361b"}, + {file = "mypy-1.9.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:5e6061f44f2313b94f920e91b204ec600982961e07a17e0f6cd83371cb23f5c2"}, + {file = "mypy-1.9.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:81a10926e5473c5fc3da8abb04119a1f5811a236dc3a38d92015cb1e6ba4cb9e"}, + {file = "mypy-1.9.0-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:b685154e22e4e9199fc95f298661deea28aaede5ae16ccc8cbb1045e716b3e04"}, + {file = "mypy-1.9.0-cp38-cp38-win_amd64.whl", hash = "sha256:5d741d3fc7c4da608764073089e5f58ef6352bedc223ff58f2f038c2c4698a89"}, + {file = "mypy-1.9.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:587ce887f75dd9700252a3abbc9c97bbe165a4a630597845c61279cf32dfbf02"}, + {file = "mypy-1.9.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:f88566144752999351725ac623471661c9d1cd8caa0134ff98cceeea181789f4"}, + {file = "mypy-1.9.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:61758fabd58ce4b0720ae1e2fea5cfd4431591d6d590b197775329264f86311d"}, + {file = "mypy-1.9.0-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:e49499be624dead83927e70c756970a0bc8240e9f769389cdf5714b0784ca6bf"}, + {file = "mypy-1.9.0-cp39-cp39-win_amd64.whl", hash = "sha256:571741dc4194b4f82d344b15e8837e8c5fcc462d66d076748142327626a1b6e9"}, + {file = "mypy-1.9.0-py3-none-any.whl", hash = "sha256:a260627a570559181a9ea5de61ac6297aa5af202f06fd7ab093ce74e7181e43e"}, + {file = "mypy-1.9.0.tar.gz", hash = "sha256:3cc5da0127e6a478cddd906068496a97a7618a21ce9b54bde5bf7e539c7af974"}, ] [package.dependencies] @@ -624,13 +624,13 @@ files = [ [[package]] name = "packaging" -version = "23.2" +version = "24.0" description = "Core utilities for Python packages" optional = false python-versions = ">=3.7" files = [ - {file = "packaging-23.2-py3-none-any.whl", hash = "sha256:8c491190033a9af7e1d931d0b5dacc2ef47509b34dd0de67ed209b5203fc88c7"}, - {file = "packaging-23.2.tar.gz", hash = "sha256:048fb0e9405036518eaaf48a55953c750c11e1a1b68e0dd1a9d62ed0c092cfc5"}, + {file = "packaging-24.0-py3-none-any.whl", hash = "sha256:2ddfb553fdf02fb784c234c7ba6ccc288296ceabec964ad2eae3777778130bc5"}, + {file = "packaging-24.0.tar.gz", hash = "sha256:eb82c5e3e56209074766e6885bb04b8c38a0c015d0a30036ebe7ece34c9989e9"}, ] [[package]] @@ -809,7 +809,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pyk" -version = "0.1.685" +version = "0.1.696" description = "" optional = false python-versions = "^3.10" @@ -830,8 +830,8 @@ xdg-base-dirs = "^6.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.685" -resolved_reference = "03a8ca03c8f93dcc78aecc335a262c4f1524edb2" +reference = "noah/default-options" +resolved_reference = "0407e934386617e294d6894c35369a34153e3060" [[package]] name = "pyperclip" @@ -1111,4 +1111,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "381dfe7b08ffa3ab758e485bc10d3600071d4f7a34c58df2c18f6cc4f2aa3139" +content-hash = "c0a94d48d82b0526d9153c2302a0972fcec12aa292c1be6ce2e1218063aa8dfc" diff --git a/pyproject.toml b/pyproject.toml index 3221e9021..81a7e174d 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.194" +version = "0.1.195" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", @@ -12,7 +12,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" -kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.489", subdirectory = "kevm-pyk" } +kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", branch = "noah/kevm-default-options2", subdirectory = "kevm-pyk" } [tool.poetry.group.dev.dependencies] autoflake = "*" diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index dabc802f1..d29d8178a 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.194' +VERSION: Final = '0.1.195' diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index 9d1689bcf..7aee0c1fa 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -3,21 +3,22 @@ import json import logging import sys -from argparse import ArgumentParser from typing import TYPE_CHECKING import pyk -from kevm_pyk.cli import node_id_like -from kevm_pyk.kompile import KompileTarget +from kevm_pyk.__main__ import ShowKCFGCommand, node_id_like +from kevm_pyk.cli import ExploreOptions, KEVMDisplayOptions, KOptions, KProveOptions +from kevm_pyk.cli import RPCOptions as KEVMRPCOptions from kevm_pyk.utils import arg_pair_of +from pyk.cli.args import BugReportOptions, KompileOptions, LoggingOptions, ParallelOptions, SMTOptions +from pyk.cli.cli import CLI, Command from pyk.cli.utils import file_path from pyk.kbuild.utils import KVersion, k_version from pyk.proof.reachability import APRFailureInfo, APRProof from pyk.proof.tui import APRProofViewer -from pyk.utils import ensure_dir_path from . import VERSION -from .cli import KontrolCLIArgs +from .cli import FoundryOptions, FoundryTestOptions, KGenOptions, KompileTargetOptions from .foundry import ( Foundry, foundry_get_model, @@ -38,11 +39,11 @@ ) from .kompile import foundry_kompile from .options import ProveOptions, RPCOptions -from .prove import foundry_prove, parse_test_version_tuple +from .prove import foundry_prove from .solc_to_k import solc_compile, solc_to_k if TYPE_CHECKING: - from argparse import Namespace + from argparse import ArgumentParser from collections.abc import Callable, Iterable from pathlib import Path from typing import Any, Final, TypeVar @@ -58,6 +59,21 @@ _LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s' +def list_of(elem_type: Callable[[str], T], delim: str = ';') -> Callable[[str], list[T]]: + def parse(s: str) -> list[T]: + return [elem_type(elem) for elem in s.split(delim)] + + return parse + + +def _parse_test_version_tuple(value: str) -> tuple[str, int | None]: + if ':' in value: + test, version = value.split(':') + return (test, int(version)) + else: + return (value, None) + + def _ignore_arg(args: dict[str, Any], arg: str, cli_option: str) -> None: if arg in args: if args[arg] is not None: @@ -79,18 +95,35 @@ def _load_foundry(foundry_root: Path, bug_report: BugReport | None = None) -> Fo def main() -> None: sys.setrecursionlimit(15000000) - parser = _create_argument_parser() - args = parser.parse_args() - logging.basicConfig(level=_loglevel(args), format=_LOG_FORMAT) + kontrol_cli = CLI( + { + VersionCommand, + CompileCommand, + SolcToKCommand, + BuildCommand, + LoadStateDiffCommand, + ProveCommand, + ShowCommand, + ToDotCommand, + SplitNodeCommand, + ListCommand, + ViewKCFGCommand, + RemoveNodeCommand, + RefuteNodeCommand, + UnRefuteNodeCommand, + SimplifyNodeCommand, + StepNodeCommand, + MergeNodesCommand, + SectionEdgeCommand, + GetModelCommand, + } + ) _check_k_version() - - 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)) + cmd = kontrol_cli.get_command() + assert isinstance(cmd, LoggingOptions) + logging.basicConfig(level=_loglevel(cmd), format=_LOG_FORMAT) + cmd.exec() def _check_k_version() -> None: @@ -121,891 +154,899 @@ def _compare_versions(ver1: KVersion, ver2: KVersion) -> bool: # Command implementation -def exec_load_state_diff( - name: str, - accesses_file: Path, - contract_names: Path | None, - output_dir_name: str | None, - foundry_root: Path, - license: str, - comment_generated_file: str, - condense_state_diff: bool = False, - **kwargs: Any, -) -> None: - foundry_state_diff( - name, - accesses_file, - contract_names=contract_names, - output_dir_name=output_dir_name, - foundry=_load_foundry(foundry_root), - license=license, - comment_generated_file=comment_generated_file, - condense_state_diff=condense_state_diff, - ) +class LoadStateDiffCommand(Command, FoundryOptions, LoggingOptions): + contract_name: str + accesses_file: Path + contract_names: Path | None + condense_state_diff: bool + output_dir_name: str | None + comment_generated_file: str + license: str + + @staticmethod + def default() -> dict[str, Any]: + return { + 'contract_names': None, + 'condense_state_diff': False, + 'output_dir_name': None, + 'comment_generated_file': '// This file was autogenerated by running `kontrol load-state-diff`. Do not edit this file manually.\n', + 'license': 'UNLICENSED', + } + + @staticmethod + def name() -> str: + return 'load-state-diff' + + @staticmethod + def help_str() -> str: + return 'Generate a state diff summary from an account access dict' + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('contract_name', type=str, help='Generated contract name') + parser.add_argument('accesses_file', type=file_path, help='Path to accesses file') + parser.add_argument( + '--contract-names', + dest='contract_names', + type=file_path, + help='Path to JSON containing deployment addresses and its respective contract names', + ) + parser.add_argument( + '--condense-state-diff', + dest='condense_state_diff', + type=bool, + help='Deploy state diff as a single file', + ) + parser.add_argument( + '--output-dir', + dest='output_dir_name', + type=str, + help='Path to write state diff .sol files, relative to foundry root', + ) + parser.add_argument( + '--comment-generated-files', + dest='comment_generated_file', + type=str, + help='Comment to write at the top of the auto generated state diff files', + ) + parser.add_argument( + '--license', + dest='license', + type=str, + help='License for the auto generated contracts', + ) + def exec(self) -> None: + foundry_state_diff( + self.contract_name, + self.accesses_file, + contract_names=self.contract_names, + output_dir_name=self.output_dir_name, + foundry=_load_foundry(self.foundry_root), + license=self.license, + comment_generated_file=self.comment_generated_file, + condense_state_diff=self.condense_state_diff, + ) -def exec_version(**kwargs: Any) -> None: - print(f'Kontrol version: {VERSION}') +class VersionCommand(Command, LoggingOptions): + @staticmethod + def name() -> str: + return 'version' -def exec_compile(contract_file: Path, **kwargs: Any) -> None: - res = solc_compile(contract_file) - print(json.dumps(res)) + @staticmethod + def help_str() -> str: + return 'Print out version of Kontrol command.' + def exec(self) -> None: + print(f'Kontrol version: {VERSION}') -def exec_solc_to_k( - contract_file: Path, - contract_name: str, - main_module: str | None, - requires: list[str], - imports: list[str], - target: str | None = None, - **kwargs: Any, -) -> None: - k_text = solc_to_k( - contract_file=contract_file, - contract_name=contract_name, - main_module=main_module, - requires=requires, - imports=imports, - ) - print(k_text) - - -def exec_build( - foundry_root: Path, - includes: Iterable[str] = (), - regen: bool = False, - rekompile: bool = False, - requires: Iterable[str] = (), - imports: Iterable[str] = (), - ccopts: Iterable[str] = (), - llvm_kompile: bool = True, - debug: bool = False, - llvm_library: bool = False, - verbose: bool = False, - target: KompileTarget | None = None, - no_forge_build: bool = False, - **kwargs: Any, -) -> None: - _ignore_arg(kwargs, 'main_module', f'--main-module {kwargs["main_module"]}') - _ignore_arg(kwargs, 'syntax_module', f'--syntax-module {kwargs["syntax_module"]}') - _ignore_arg(kwargs, 'spec_module', f'--spec-module {kwargs["spec_module"]}') - _ignore_arg(kwargs, 'o0', '-O0') - _ignore_arg(kwargs, 'o1', '-O1') - _ignore_arg(kwargs, 'o2', '-O2') - _ignore_arg(kwargs, 'o3', '-O3') - if target is None: - target = KompileTarget.HASKELL - foundry_kompile( - foundry=_load_foundry(foundry_root), - includes=includes, - regen=regen, - rekompile=rekompile, - requires=requires, - imports=imports, - ccopts=ccopts, - llvm_kompile=llvm_kompile, - debug=debug, - verbose=verbose, - target=target, - no_forge_build=no_forge_build, - ) +class CompileCommand(Command, LoggingOptions): + contract_file: Path -def exec_prove( - foundry_root: Path, - max_depth: int = 1000, - max_iterations: int | None = None, - reinit: bool = False, - tests: Iterable[tuple[str, int | None]] = (), - include_summaries: Iterable[tuple[str, int | None]] = (), - workers: int = 1, - break_every_step: bool = False, - break_on_jumpi: bool = False, - break_on_calls: bool = True, - break_on_storage: bool = False, - break_on_basic_blocks: bool = False, - break_on_cheatcodes: bool = False, - bmc_depth: int | None = None, - bug_report: BugReport | None = None, - kore_rpc_command: str | Iterable[str] | None = None, - use_booster: bool = True, - smt_timeout: int | None = None, - smt_retry_limit: int | None = None, - smt_tactic: str | None = None, - failure_info: bool = True, - counterexample_info: bool = False, - trace_rewrites: bool = False, - auto_abstract_gas: bool = False, - run_constructor: bool = False, - fail_fast: bool = False, - port: int | None = None, - maude_port: int | None = None, - use_gas: bool = False, - deployment_state_path: Path | None = None, - with_non_general_state: bool = False, - xml_test_report: bool = False, - cse: bool = False, - **kwargs: Any, -) -> None: - _ignore_arg(kwargs, 'main_module', f'--main-module: {kwargs["main_module"]}') - _ignore_arg(kwargs, 'syntax_module', f'--syntax-module: {kwargs["syntax_module"]}') - _ignore_arg(kwargs, 'definition_dir', f'--definition: {kwargs["definition_dir"]}') - _ignore_arg(kwargs, 'spec_module', f'--spec-module: {kwargs["spec_module"]}') - - if smt_timeout is None: - smt_timeout = 300 - if smt_retry_limit is None: - smt_retry_limit = 10 - - if isinstance(kore_rpc_command, str): - kore_rpc_command = kore_rpc_command.split() - - deployment_state_entries = read_deployment_state(deployment_state_path) if deployment_state_path else None - - prove_options = ProveOptions( - auto_abstract_gas=auto_abstract_gas, - reinit=reinit, - bug_report=bug_report, - bmc_depth=bmc_depth, - max_depth=max_depth, - break_every_step=break_every_step, - break_on_jumpi=break_on_jumpi, - break_on_calls=break_on_calls, - break_on_storage=break_on_storage, - break_on_basic_blocks=break_on_basic_blocks, - break_on_cheatcodes=break_on_cheatcodes, - workers=workers, - counterexample_info=counterexample_info, - max_iterations=max_iterations, - run_constructor=run_constructor, - fail_fast=fail_fast, - use_gas=use_gas, - deployment_state_entries=deployment_state_entries, - active_symbolik=with_non_general_state, - cse=cse, - ) + @staticmethod + def name() -> str: + return 'compile' - rpc_options = RPCOptions( - use_booster=use_booster, - kore_rpc_command=kore_rpc_command, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - smt_tactic=smt_tactic, - trace_rewrites=trace_rewrites, - port=port, - maude_port=maude_port, - ) + @staticmethod + def help_str() -> str: + return 'Generate combined JSON with solc compilation results.' - results = foundry_prove( - foundry=_load_foundry(foundry_root, bug_report), - prove_options=prove_options, - rpc_options=rpc_options, - tests=tests, - include_summaries=include_summaries, - xml_test_report=xml_test_report, - ) - failed = 0 - for proof in results: - if proof.passed: - print(f'PROOF PASSED: {proof.id}') - print(f'time: {proof.formatted_exec_time()}s') - else: - failed += 1 - print(f'PROOF FAILED: {proof.id}') - print(f'time: {proof.formatted_exec_time()}') - failure_log = None - if isinstance(proof, APRProof) and isinstance(proof.failure_info, APRFailureInfo): - failure_log = proof.failure_info - if failure_info and failure_log is not None: - log = failure_log.print() + Foundry.help_info() - for line in log: - print(line) - - sys.exit(failed) - - -def exec_show( - foundry_root: Path, - test: str, - version: int | None, - nodes: Iterable[NodeIdLike] = (), - node_deltas: Iterable[tuple[NodeIdLike, NodeIdLike]] = (), - to_module: bool = False, - to_kevm_claims: bool = False, - kevm_claim_dir: Path | None = None, - minimize: bool = True, - sort_collections: bool = False, - omit_unstable_output: bool = False, - pending: bool = False, - failing: bool = False, - failure_info: bool = False, - counterexample_info: bool = False, - port: int | None = None, - maude_port: int | None = None, - **kwargs: Any, -) -> None: - output = foundry_show( - foundry=_load_foundry(foundry_root), - test=test, - version=version, - nodes=nodes, - node_deltas=node_deltas, - to_module=to_module, - to_kevm_claims=to_kevm_claims, - kevm_claim_dir=kevm_claim_dir, - minimize=minimize, - omit_unstable_output=omit_unstable_output, - sort_collections=sort_collections, - pending=pending, - failing=failing, - failure_info=failure_info, - counterexample_info=counterexample_info, - port=port, - maude_port=maude_port, - ) - print(output) + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('contract_file', type=file_path, help='Path to contract file.') + def exec(self) -> None: + res = solc_compile(self.contract_file) + print(json.dumps(res)) -def exec_refute_node(foundry_root: Path, test: str, node: NodeIdLike, version: int | None, **kwargs: Any) -> None: - foundry_refute_node(foundry=_load_foundry(foundry_root), test=test, node=node, version=version) +class SolcToKCommand(Command, KOptions, KGenOptions, LoggingOptions): + contract_file: Path + contract_name: str -def exec_unrefute_node(foundry_root: Path, test: str, node: NodeIdLike, version: int | None, **kwargs: Any) -> None: - foundry_unrefute_node(foundry=_load_foundry(foundry_root), test=test, node=node, version=version) + @staticmethod + def name() -> str: + return 'solc-to-k' + @staticmethod + def help_str() -> str: + return 'Output helper K definition for given JSON output from solc compiler.' -def exec_split_node( - foundry_root: Path, test: str, node: NodeIdLike, branch_condition: str, version: int | None, **kwargs: Any -) -> None: - node_ids = foundry_split_node( - foundry=_load_foundry(foundry_root), test=test, node=node, branch_condition=branch_condition, version=version - ) + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('contract_file', type=file_path, help='Path to contract file.') + parser.add_argument('contract_name', type=str, help='Name of contract to generate K helpers for.') - print(f'Node {node} has been split into {node_ids} on condition {branch_condition}.') - - -def exec_to_dot(foundry_root: Path, test: str, version: int | None, **kwargs: Any) -> None: - foundry_to_dot(foundry=_load_foundry(foundry_root), test=test, version=version) - - -def exec_list(foundry_root: Path, **kwargs: Any) -> None: - stats = foundry_list(foundry=_load_foundry(foundry_root)) - print('\n'.join(stats)) - - -def exec_view_kcfg(foundry_root: Path, test: str, version: int | None, **kwargs: Any) -> None: - foundry = _load_foundry(foundry_root) - test_id = foundry.get_test_id(test, version) - contract_name, _ = test_id.split('.') - proof = foundry.get_apr_proof(test_id) - - def _short_info(cterm: CTerm) -> Iterable[str]: - return foundry.short_info_for_contract(contract_name, cterm) - - def _custom_view(elem: KCFGElem) -> Iterable[str]: - return foundry.custom_view(contract_name, elem) - - node_printer = foundry_node_printer(foundry, contract_name, proof) - viewer = APRProofViewer(proof, foundry.kevm, node_printer=node_printer, custom_view=_custom_view) - viewer.run() - - -def exec_remove_node(foundry_root: Path, test: str, node: NodeIdLike, version: int | None, **kwargs: Any) -> None: - foundry_remove_node(foundry=_load_foundry(foundry_root), test=test, version=version, node=node) - - -def exec_simplify_node( - foundry_root: Path, - test: str, - version: int | None, - node: NodeIdLike, - replace: bool = False, - minimize: bool = True, - sort_collections: bool = False, - bug_report: BugReport | None = None, - kore_rpc_command: str | Iterable[str] | None = None, - use_booster: bool = False, - smt_timeout: int | None = None, - smt_retry_limit: int | None = None, - smt_tactic: str | None = None, - trace_rewrites: bool = False, - port: int | None = None, - maude_port: int | None = None, - **kwargs: Any, -) -> None: - if smt_timeout is None: - smt_timeout = 300 - if smt_retry_limit is None: - smt_retry_limit = 10 - - if isinstance(kore_rpc_command, str): - kore_rpc_command = kore_rpc_command.split() - - rpc_options = RPCOptions( - use_booster=use_booster, - kore_rpc_command=kore_rpc_command, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - smt_tactic=smt_tactic, - trace_rewrites=trace_rewrites, - port=port, - maude_port=maude_port, - ) + def exec(self) -> None: + k_text = solc_to_k( + contract_file=self.contract_file, + contract_name=self.contract_name, + main_module=self.main_module, + requires=self.requires, + imports=self.imports, + ) + print(k_text) + + +class BuildCommand( + Command, KOptions, KGenOptions, KompileOptions, FoundryOptions, KompileTargetOptions, LoggingOptions +): + regen: bool + rekompile: bool + no_forge_build: bool + + @staticmethod + def name() -> str: + return 'build' + + @staticmethod + def help_str() -> str: + return 'Kompile K definition corresponding to given output directory.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'regen': False, + 'rekompile': False, + 'no_forge_build': False, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument( + '--regen', + dest='regen', + default=None, + action='store_true', + help='Regenerate foundry.k even if it already exists.', + ) + parser.add_argument( + '--rekompile', + dest='rekompile', + default=None, + action='store_true', + help='Rekompile foundry.k even if kompiled definition already exists.', + ) + parser.add_argument( + '--no-forge-build', + dest='no_forge_build', + default=None, + action='store_true', + help="Do not call 'forge build' during kompilation.", + ) - pretty_term = foundry_simplify_node( - foundry=_load_foundry(foundry_root, bug_report), - test=test, - version=version, - node=node, - rpc_options=rpc_options, - replace=replace, - minimize=minimize, - sort_collections=sort_collections, - bug_report=bug_report, - ) - print(f'Simplified:\n{pretty_term}') - - -def exec_step_node( - foundry_root: Path, - test: str, - version: int | None, - node: NodeIdLike, - repeat: int = 1, - depth: int = 1, - bug_report: BugReport | None = None, - kore_rpc_command: str | Iterable[str] | None = None, - use_booster: bool = False, - smt_timeout: int | None = None, - smt_retry_limit: int | None = None, - smt_tactic: str | None = None, - trace_rewrites: bool = False, - port: int | None = None, - maude_port: int | None = None, - **kwargs: Any, -) -> None: - if smt_timeout is None: - smt_timeout = 300 - if smt_retry_limit is None: - smt_retry_limit = 10 - - if isinstance(kore_rpc_command, str): - kore_rpc_command = kore_rpc_command.split() - - rpc_options = RPCOptions( - use_booster=use_booster, - kore_rpc_command=kore_rpc_command, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - smt_tactic=smt_tactic, - trace_rewrites=trace_rewrites, - port=port, - maude_port=maude_port, - ) + def exec(self) -> None: + foundry_kompile( + foundry=_load_foundry(self.foundry_root), + includes=self.includes, + regen=self.regen, + rekompile=self.rekompile, + requires=self.requires, + imports=self.imports, + ccopts=self.ccopts, + llvm_kompile=self.llvm_kompile, + debug=self.debug, + verbose=self.verbose, + target=self.target, + no_forge_build=self.no_forge_build, + ) - foundry_step_node( - foundry=_load_foundry(foundry_root, bug_report), - test=test, - version=version, - node=node, - rpc_options=rpc_options, - repeat=repeat, - depth=depth, - bug_report=bug_report, - ) +class ProveCommand( + Command, + LoggingOptions, + ParallelOptions, + KOptions, + KProveOptions, + SMTOptions, + KEVMRPCOptions, + BugReportOptions, + ExploreOptions, + FoundryOptions, +): + tests: list[tuple[str, int | None]] + reinit: bool + bmc_depth: int | None + run_constructor: bool + use_gas: bool + break_on_cheatcodes: bool + deployment_state_path: Path | None + include_summaries: list[tuple[str, int | None]] + with_non_general_state: bool + xml_test_report: bool + cse: bool + + @staticmethod + def name() -> str: + return 'prove' + + @staticmethod + def help_str() -> str: + return 'Run Foundry Proof.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'tests': [], + 'reinit': False, + 'bmc_depth': None, + 'run_constructor': False, + 'use_gas': False, + 'break_on_cheatcodes': False, + 'deployment_state_path': None, + 'include_summaries': [], + 'with_non_general_state': False, + 'xml_test_report': False, + 'cse': False, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument( + '--match-test', + type=_parse_test_version_tuple, + dest='tests', + action='append', + help=( + 'Specify contract function(s) to test using a regular expression. This will match functions' + " based on their full signature, e.g., 'ERC20Test.testTransfer(address,uint256)'. This option" + ' can be used multiple times to add more functions to test.' + ), + ) + parser.add_argument( + '--reinit', + dest='reinit', + default=None, + action='store_true', + help='Reinitialize CFGs even if they already exist.', + ) + parser.add_argument( + '--bmc-depth', + dest='bmc_depth', + type=int, + help='Enables bounded model checking. Specifies the maximum depth to unroll all loops to.', + ) + parser.add_argument( + '--run-constructor', + dest='run_constructor', + default=None, + action='store_true', + help='Include the contract constructor in the test execution.', + ) + parser.add_argument('--use-gas', dest='use_gas', default=None, action='store_true', help='Enables gas computation in KEVM.') + parser.add_argument( + '--break-on-cheatcodes', + dest='break_on_cheatcodes', + default=None, + action='store_true', + help='Break on all Foundry rules.', + ) + parser.add_argument( + '--init-node-from', + dest='deployment_state_path', + type=file_path, + help='Path to JSON file containing the deployment state of the deployment process used for the project.', + ) + parser.add_argument( + '--include-summary', + type=_parse_test_version_tuple, + dest='include_summaries', + action='append', + help='Specify a summary to include as a lemma.', + ) + parser.add_argument( + '--with-non-general-state', + dest='with_non_general_state', + default=None, + action='store_true', + help='Flag used by Simbolik to initialise the state of a non test function as if it was a test function.', + ) + parser.add_argument( + '--xml-test-report', + dest='xml_test_report', + default=None, + action='store_true', + help='Generate a JUnit XML report', + ) + parser.add_argument('--cse', dest='cse', default=None, action='store_true', help='Use Compositional Symbolic Execution') -def exec_merge_nodes( - foundry_root: Path, - test: str, - version: int | None, - nodes: Iterable[NodeIdLike], - **kwargs: Any, -) -> None: - foundry_merge_nodes(foundry=_load_foundry(foundry_root), node_ids=nodes, test=test, version=version) - - -def exec_section_edge( - foundry_root: Path, - test: str, - version: int | None, - edge: tuple[str, str], - sections: int = 2, - replace: bool = False, - bug_report: BugReport | None = None, - kore_rpc_command: str | Iterable[str] | None = None, - use_booster: bool = False, - smt_timeout: int | None = None, - smt_retry_limit: int | None = None, - smt_tactic: str | None = None, - trace_rewrites: bool = False, - port: int | None = None, - maude_port: int | None = None, - **kwargs: Any, -) -> None: - if smt_timeout is None: - smt_timeout = 300 - if smt_retry_limit is None: - smt_retry_limit = 10 - - if isinstance(kore_rpc_command, str): - kore_rpc_command = kore_rpc_command.split() - - rpc_options = RPCOptions( - use_booster=use_booster, - kore_rpc_command=kore_rpc_command, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - smt_tactic=smt_tactic, - trace_rewrites=trace_rewrites, - port=port, - maude_port=maude_port, - ) + def exec(self) -> None: + kore_rpc_command = ( + self.kore_rpc_command.split() if isinstance(self.kore_rpc_command, str) else self.kore_rpc_command + ) - foundry_section_edge( - foundry=_load_foundry(foundry_root, bug_report), - test=test, - version=version, - rpc_options=rpc_options, - edge=edge, - sections=sections, - replace=replace, - bug_report=bug_report, - ) + deployment_state_entries = ( + read_deployment_state(self.deployment_state_path) if self.deployment_state_path else None + ) + prove_options = ProveOptions( + auto_abstract_gas=self.auto_abstract_gas, + reinit=self.reinit, + bug_report=self.bug_report, + bmc_depth=self.bmc_depth, + max_depth=self.max_depth, + break_every_step=self.break_every_step, + break_on_jumpi=self.break_on_jumpi, + break_on_calls=self.break_on_calls, + break_on_storage=self.break_on_storage, + break_on_basic_blocks=self.break_on_basic_blocks, + break_on_cheatcodes=self.break_on_cheatcodes, + workers=self.workers, + counterexample_info=self.counterexample_info, + max_iterations=self.max_iterations, + run_constructor=self.run_constructor, + fail_fast=self.fail_fast, + use_gas=self.use_gas, + deployment_state_entries=deployment_state_entries, + active_symbolik=self.with_non_general_state, + cse=self.cse, + ) -def exec_get_model( - foundry_root: Path, - test: str, - version: int | None, - nodes: Iterable[NodeIdLike] = (), - pending: bool = False, - failing: bool = False, - bug_report: BugReport | None = None, - kore_rpc_command: str | Iterable[str] | None = None, - use_booster: bool = False, - smt_timeout: int | None = None, - smt_retry_limit: int | None = None, - smt_tactic: str | None = None, - trace_rewrites: bool = False, - port: int | None = None, - maude_port: int | None = None, - **kwargs: Any, -) -> None: - if smt_timeout is None: - smt_timeout = 300 - if smt_retry_limit is None: - smt_retry_limit = 10 - - if isinstance(kore_rpc_command, str): - kore_rpc_command = kore_rpc_command.split() - - rpc_options = RPCOptions( - use_booster=use_booster, - kore_rpc_command=kore_rpc_command, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - smt_tactic=smt_tactic, - trace_rewrites=trace_rewrites, - port=port, - maude_port=maude_port, - ) - output = foundry_get_model( - foundry=_load_foundry(foundry_root), - test=test, - version=version, - nodes=nodes, - rpc_options=rpc_options, - pending=pending, - failing=failing, - bug_report=bug_report, - ) - print(output) + rpc_options = RPCOptions( + use_booster=self.use_booster, + kore_rpc_command=kore_rpc_command, + smt_timeout=self.smt_timeout, + smt_retry_limit=self.smt_retry_limit, + smt_tactic=self.smt_tactic, + trace_rewrites=self.trace_rewrites, + port=self.port, + maude_port=self.maude_port, + ) + results = foundry_prove( + foundry=_load_foundry(self.foundry_root, self.bug_report), + prove_options=prove_options, + rpc_options=rpc_options, + tests=self.tests, + include_summaries=self.include_summaries, + xml_test_report=self.xml_test_report, + ) + failed = 0 + for proof in results: + if proof.passed: + print(f'PROOF PASSED: {proof.id}') + print(f'time: {proof.formatted_exec_time()}s') + else: + failed += 1 + print(f'PROOF FAILED: {proof.id}') + print(f'time: {proof.formatted_exec_time()}') + failure_log = None + if isinstance(proof, APRProof) and isinstance(proof.failure_info, APRFailureInfo): + failure_log = proof.failure_info + if self.failure_info and failure_log is not None: + log = failure_log.print() + Foundry.help_info() + for line in log: + print(line) + sys.exit(failed) + + +class ShowCommand( + ShowKCFGCommand, FoundryTestOptions, KOptions, KEVMDisplayOptions, FoundryOptions, KEVMRPCOptions, LoggingOptions +): + omit_unstable_output: bool + to_kevm_claims: bool + kevm_claim_dir: Path | None + + @staticmethod + def name() -> str: + return 'show' + + @staticmethod + def help_str() -> str: + return 'Print the CFG for a given proof.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'omit_unstable_output': False, + 'to_kevm_claims': False, + 'kevm_claim_dir': None, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument( + '--omit-unstable-output', + dest='omit_unstable_output', + default=None, + action='store_true', + help='Strip output that is likely to change without the contract logic changing', + ) + parser.add_argument( + '--to-kevm-claims', + dest='to_kevm_claims', + default=None, + action='store_true', + help='Generate a K module which can be run directly as KEVM claims for the given KCFG (best-effort).', + ) + parser.add_argument( + '--kevm-claim-dir', + dest='kevm_claim_dir', + help='Path to write KEVM claim files at.', + ) -# Helpers + def exec(self) -> None: + output = foundry_show( + foundry=_load_foundry(self.foundry_root), + test=self.test, + version=self.version, + nodes=self.nodes, + node_deltas=self.node_deltas, + to_module=self.to_module, + to_kevm_claims=self.to_kevm_claims, + kevm_claim_dir=self.kevm_claim_dir, + minimize=self.minimize, + omit_unstable_output=self.omit_unstable_output, + sort_collections=self.sort_collections, + pending=self.pending, + failing=self.failing, + failure_info=self.failure_info, + counterexample_info=self.counterexample_info, + port=self.port, + maude_port=self.maude_port, + ) + print(output) -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)] +class RefuteNodeCommand(Command, FoundryTestOptions, FoundryOptions, LoggingOptions): + node: NodeIdLike - return parse + @staticmethod + def name() -> str: + return 'refute-node' - kontrol_cli_args = KontrolCLIArgs() - parser = ArgumentParser(prog='kontrol') + @staticmethod + def help_str() -> str: + return 'Refute a node and add its refutation as a subproof.' - command_parser = parser.add_subparsers(dest='command', required=True) + @staticmethod + def default() -> dict[str, Any]: + return { + 'omit_unstable_output': False, + 'to_kevm_claims': False, + 'kevm_claim_dir': None, + } - command_parser.add_parser('version', help='Print out version of Kontrol command.') + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('node', type=node_id_like, help='Node to refute.') - solc_args = command_parser.add_parser('compile', help='Generate combined JSON with solc compilation results.') - solc_args.add_argument('contract_file', type=file_path, help='Path to contract file.') + def exec(self) -> None: + foundry_refute_node( + foundry=_load_foundry(self.foundry_root), test=self.test, node=self.node, version=self.version + ) - solc_to_k_args = command_parser.add_parser( - 'solc-to-k', - help='Output helper K definition for given JSON output from solc compiler.', - parents=[ - kontrol_cli_args.logging_args, - kontrol_cli_args.k_args, - kontrol_cli_args.k_gen_args, - ], - ) - solc_to_k_args.add_argument('contract_file', type=file_path, help='Path to contract file.') - solc_to_k_args.add_argument('contract_name', type=str, help='Name of contract to generate K helpers for.') - - build = command_parser.add_parser( - 'build', - help='Kompile K definition corresponding to given output directory.', - parents=[ - kontrol_cli_args.logging_args, - kontrol_cli_args.k_args, - kontrol_cli_args.k_gen_args, - kontrol_cli_args.kompile_args, - kontrol_cli_args.foundry_args, - kontrol_cli_args.kompile_target_args, - ], - ) - build.add_argument( - '--regen', - dest='regen', - default=False, - action='store_true', - help='Regenerate foundry.k even if it already exists.', - ) - build.add_argument( - '--rekompile', - dest='rekompile', - default=False, - action='store_true', - help='Rekompile foundry.k even if kompiled definition already exists.', - ) - build.add_argument( - '--no-forge-build', - dest='no_forge_build', - default=False, - action='store_true', - help="Do not call 'forge build' during kompilation.", - ) - state_diff_args = command_parser.add_parser( - 'load-state-diff', - help='Generate a state diff summary from an account access dict', - parents=[ - kontrol_cli_args.foundry_args, - ], - ) - state_diff_args.add_argument('name', type=str, help='Generated contract name') - state_diff_args.add_argument('accesses_file', type=file_path, help='Path to accesses file') - state_diff_args.add_argument( - '--contract-names', - dest='contract_names', - default=None, - type=file_path, - help='Path to JSON containing deployment addresses and its respective contract names', - ) - state_diff_args.add_argument( - '--condense-state-diff', - dest='condense_state_diff', - default=False, - type=bool, - help='Deploy state diff as a single file', - ) - state_diff_args.add_argument( - '--output-dir', - dest='output_dir_name', - default=None, - type=str, - help='Path to write state diff .sol files, relative to foundry root', - ) - state_diff_args.add_argument( - '--comment-generated-files', - dest='comment_generated_file', - default='// This file was autogenerated by running `kontrol load-state-diff`. Do not edit this file manually.\n', - type=str, - help='Comment to write at the top of the auto generated state diff files', - ) - state_diff_args.add_argument( - '--license', - dest='license', - default='UNLICENSED', - type=str, - help='License for the auto generated contracts', - ) +class UnRefuteNodeCommand(Command, FoundryTestOptions, FoundryOptions, LoggingOptions): + node: NodeIdLike - prove_args = command_parser.add_parser( - 'prove', - help='Run Foundry Proof.', - parents=[ - kontrol_cli_args.logging_args, - kontrol_cli_args.parallel_args, - kontrol_cli_args.k_args, - kontrol_cli_args.kprove_args, - kontrol_cli_args.smt_args, - kontrol_cli_args.rpc_args, - kontrol_cli_args.bug_report_args, - kontrol_cli_args.explore_args, - kontrol_cli_args.foundry_args, - ], - ) - prove_args.add_argument( - '--match-test', - type=parse_test_version_tuple, - dest='tests', - default=[], - action='append', - help=( - 'Specify contract function(s) to test using a regular expression. This will match functions' - " based on their full signature, e.g., 'ERC20Test.testTransfer(address,uint256)'. This option" - ' can be used multiple times to add more functions to test.' - ), - ) - prove_args.add_argument( - '--reinit', - dest='reinit', - default=False, - action='store_true', - help='Reinitialize CFGs even if they already exist.', - ) - prove_args.add_argument( - '--bmc-depth', - dest='bmc_depth', - default=None, - type=int, - help='Enables bounded model checking. Specifies the maximum depth to unroll all loops to.', - ) - prove_args.add_argument( - '--run-constructor', - dest='run_constructor', - default=False, - action='store_true', - help='Include the contract constructor in the test execution.', - ) - prove_args.add_argument( - '--use-gas', dest='use_gas', default=False, action='store_true', help='Enables gas computation in KEVM.' - ) - prove_args.add_argument( - '--break-on-cheatcodes', - dest='break_on_cheatcodes', - default=False, - action='store_true', - help='Break on all Foundry rules.', - ) - prove_args.add_argument( - '--init-node-from', - dest='deployment_state_path', - default=None, - type=file_path, - help='Path to JSON file containing the deployment state of the deployment process used for the project.', - ) - prove_args.add_argument( - '--include-summary', - type=parse_test_version_tuple, - dest='include_summaries', - default=[], - action='append', - help='Specify a summary to include as a lemma.', - ) - prove_args.add_argument( - '--with-non-general-state', - dest='with_non_general_state', - default=False, - action='store_true', - help='Flag used by Simbolik to initialise the state of a non test function as if it was a test function.', - ) - prove_args.add_argument( - '--xml-test-report', - dest='xml_test_report', - default=False, - action='store_true', - help='Generate a JUnit XML report', - ) - prove_args.add_argument( - '--cse', dest='cse', default=False, action='store_true', help='Use Compositional Symbolic Execution' - ) + @staticmethod + def name() -> str: + return 'unrefute-node' - show_args = command_parser.add_parser( - 'show', - help='Print the CFG for a given proof.', - parents=[ - kontrol_cli_args.foundry_test_args, - kontrol_cli_args.logging_args, - kontrol_cli_args.k_args, - kontrol_cli_args.kcfg_show_args, - kontrol_cli_args.display_args, - kontrol_cli_args.foundry_args, - ], - ) - show_args.add_argument( - '--omit-unstable-output', - dest='omit_unstable_output', - default=False, - action='store_true', - help='Strip output that is likely to change without the contract logic changing', - ) - show_args.add_argument( - '--to-kevm-claims', - dest='to_kevm_claims', - default=False, - action='store_true', - help='Generate a K module which can be run directly as KEVM claims for the given KCFG (best-effort).', - ) - show_args.add_argument( - '--kevm-claim-dir', - dest='kevm_claim_dir', - type=ensure_dir_path, - help='Path to write KEVM claim files at.', - ) + @staticmethod + def help_str() -> str: + return 'Disable refutation of a node and remove corresponding refutation subproof.' - command_parser.add_parser( - 'to-dot', - help='Dump the given CFG for the test as DOT for visualization.', - parents=[kontrol_cli_args.foundry_test_args, kontrol_cli_args.logging_args, kontrol_cli_args.foundry_args], - ) + @staticmethod + def default() -> dict[str, Any]: + return { + 'omit_unstable_output': False, + 'to_kevm_claims': False, + 'kevm_claim_dir': None, + } - command_parser.add_parser( - 'list', - help='List information about CFGs on disk', - parents=[kontrol_cli_args.logging_args, kontrol_cli_args.k_args, kontrol_cli_args.foundry_args], - ) + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('node', type=node_id_like, help='Node to unrefute.') - command_parser.add_parser( - 'view-kcfg', - help='Explore a given proof in the KCFG visualizer.', - parents=[kontrol_cli_args.foundry_test_args, kontrol_cli_args.logging_args, kontrol_cli_args.foundry_args], - ) + def exec(self) -> None: + foundry_unrefute_node( + foundry=_load_foundry(self.foundry_root), test=self.test, node=self.node, version=self.version + ) - remove_node = command_parser.add_parser( - 'remove-node', - help='Remove a node and its successors.', - parents=[kontrol_cli_args.foundry_test_args, kontrol_cli_args.logging_args, kontrol_cli_args.foundry_args], - ) - remove_node.add_argument('node', type=node_id_like, help='Node to remove CFG subgraph from.') - refute_node = command_parser.add_parser( - 'refute-node', - help='Refute a node and add its refutation as a subproof.', - parents=[kontrol_cli_args.foundry_test_args, kontrol_cli_args.logging_args, kontrol_cli_args.foundry_args], - ) - refute_node.add_argument('node', type=node_id_like, help='Node to refute.') +class SplitNodeCommand(Command, FoundryTestOptions, FoundryOptions, LoggingOptions): + node: NodeIdLike + branch_condition: str - unrefute_node = command_parser.add_parser( - 'unrefute-node', - help='Disable refutation of a node and remove corresponding refutation subproof.', - parents=[kontrol_cli_args.foundry_test_args, kontrol_cli_args.logging_args, kontrol_cli_args.foundry_args], - ) - unrefute_node.add_argument('node', type=node_id_like, help='Node to unrefute.') + @staticmethod + def name() -> str: + return 'split-node' - split_node = command_parser.add_parser( - 'split-node', - help='Split a node on a given branch condition.', - parents=[kontrol_cli_args.foundry_test_args, kontrol_cli_args.logging_args, kontrol_cli_args.foundry_args], - ) - split_node.add_argument('node', type=node_id_like, help='Node to split.') - split_node.add_argument('branch_condition', type=str, help='Branch condition written in K.') - - simplify_node = command_parser.add_parser( - 'simplify-node', - help='Simplify a given node, and potentially replace it.', - parents=[ - kontrol_cli_args.foundry_test_args, - kontrol_cli_args.logging_args, - kontrol_cli_args.smt_args, - kontrol_cli_args.rpc_args, - kontrol_cli_args.bug_report_args, - kontrol_cli_args.display_args, - kontrol_cli_args.foundry_args, - ], - ) - simplify_node.add_argument('node', type=node_id_like, help='Node to simplify in CFG.') - simplify_node.add_argument( - '--replace', default=False, help='Replace the original node with the simplified variant in the graph.' - ) + @staticmethod + def help_str() -> str: + return 'Split a node on a given branch condition.' - step_node = command_parser.add_parser( - 'step-node', - help='Step from a given node, adding it to the CFG.', - parents=[ - kontrol_cli_args.foundry_test_args, - kontrol_cli_args.logging_args, - kontrol_cli_args.rpc_args, - kontrol_cli_args.bug_report_args, - kontrol_cli_args.smt_args, - kontrol_cli_args.foundry_args, - ], - ) - step_node.add_argument('node', type=node_id_like, help='Node to step from in CFG.') - step_node.add_argument( - '--repeat', type=int, default=1, help='How many node expansions to do from the given start node (>= 1).' - ) - step_node.add_argument('--depth', type=int, default=1, help='How many steps to take from initial node on edge.') - merge_node = command_parser.add_parser( - 'merge-nodes', - help='Merge multiple nodes into one branch.', - parents=[ - kontrol_cli_args.foundry_test_args, - kontrol_cli_args.logging_args, - kontrol_cli_args.foundry_args, - ], - ) - merge_node.add_argument( - '--node', - type=node_id_like, - dest='nodes', - default=[], - action='append', - help='One node to be merged.', - ) + def exec(self) -> None: + node_ids = foundry_split_node( + foundry=_load_foundry(self.foundry_root), + test=self.test, + node=self.node, + branch_condition=self.branch_condition, + version=self.version, + ) - section_edge = command_parser.add_parser( - 'section-edge', - help='Given an edge in the graph, cut it into sections to get intermediate nodes.', - parents=[ - kontrol_cli_args.foundry_test_args, - kontrol_cli_args.logging_args, - kontrol_cli_args.rpc_args, - kontrol_cli_args.bug_report_args, - kontrol_cli_args.smt_args, - kontrol_cli_args.foundry_args, - ], - ) - section_edge.add_argument('edge', type=arg_pair_of(str, str), help='Edge to section in CFG.') - section_edge.add_argument('--sections', type=int, default=2, help='Number of sections to make from edge (>= 2).') - - get_model = command_parser.add_parser( - 'get-model', - help='Display a model for a given node.', - parents=[ - kontrol_cli_args.foundry_test_args, - kontrol_cli_args.logging_args, - kontrol_cli_args.rpc_args, - kontrol_cli_args.bug_report_args, - kontrol_cli_args.smt_args, - kontrol_cli_args.foundry_args, - ], - ) - get_model.add_argument( - '--node', - type=node_id_like, - dest='nodes', - default=[], - action='append', - help='List of nodes to display the models of.', - ) - get_model.add_argument( - '--pending', dest='pending', default=False, action='store_true', help='Also display models of pending nodes' - ) - get_model.add_argument( - '--failing', dest='failing', default=False, action='store_true', help='Also display models of failing nodes' - ) + print(f'Node {self.node} has been split into {node_ids} on condition {self.branch_condition}.') + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('node', type=node_id_like, help='Node to split.') + parser.add_argument('branch_condition', type=str, help='Branch condition written in K.') + + +class ToDotCommand(Command, FoundryTestOptions, FoundryOptions, LoggingOptions): + @staticmethod + def name() -> str: + return 'to-dot' + + @staticmethod + def help_str() -> str: + return 'Dump the given CFG for the test as DOT for visualization.' + + def exec(self) -> None: + foundry_to_dot(foundry=_load_foundry(self.foundry_root), test=self.test, version=self.version) + + +class ListCommand(Command, KOptions, FoundryOptions, LoggingOptions): + @staticmethod + def name() -> str: + return 'list' + + @staticmethod + def help_str() -> str: + return 'List information about CFGs on disk' + + def exec(self) -> None: + stats = foundry_list(foundry=_load_foundry(self.foundry_root)) + print('\n'.join(stats)) + + +class ViewKCFGCommand(Command, FoundryTestOptions, FoundryOptions, LoggingOptions): + @staticmethod + def name() -> str: + return 'view-kcfg' + + @staticmethod + def help_str() -> str: + return 'Explore a given proof in the KCFG visualizer.' + + def exec(self) -> None: + foundry = _load_foundry(self.foundry_root) + test_id = foundry.get_test_id(self.test, self.version) + contract_name, _ = test_id.split('.') + proof = foundry.get_apr_proof(test_id) + + def _short_info(cterm: CTerm) -> Iterable[str]: + return foundry.short_info_for_contract(contract_name, cterm) + + def _custom_view(elem: KCFGElem) -> Iterable[str]: + return foundry.custom_view(contract_name, elem) + + node_printer = foundry_node_printer(foundry, contract_name, proof) + viewer = APRProofViewer(proof, foundry.kevm, node_printer=node_printer, custom_view=_custom_view) + viewer.run() + + +class RemoveNodeCommand(Command, FoundryTestOptions, FoundryOptions, LoggingOptions): + node: NodeIdLike + + @staticmethod + def name() -> str: + return 'remove-node' + + @staticmethod + def help_str() -> str: + return 'Remove a node and its successors.' + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('node', type=node_id_like, help='Node to remove CFG subgraph from.') + + def exec(self) -> None: + foundry_remove_node( + foundry=_load_foundry(self.foundry_root), test=self.test, version=self.version, node=self.node + ) + + +class SimplifyNodeCommand( + Command, + FoundryTestOptions, + SMTOptions, + KEVMRPCOptions, + BugReportOptions, + KEVMDisplayOptions, + FoundryOptions, + LoggingOptions, +): + node: NodeIdLike + replace: bool + + @staticmethod + def name() -> str: + return 'simplify-node' + + @staticmethod + def help_str() -> str: + return 'Simplify a given node, and potentially replace it.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'replace': False, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('node', type=node_id_like, help='Node to simplify in CFG.') + parser.add_argument('--replace', help='Replace the original node with the simplified variant in the graph.') + + def exec(self) -> None: + kore_rpc_command = ( + self.kore_rpc_command.split() if isinstance(self.kore_rpc_command, str) else self.kore_rpc_command + ) + + rpc_options = RPCOptions( + use_booster=self.use_booster, + kore_rpc_command=kore_rpc_command, + smt_timeout=self.smt_timeout, + smt_retry_limit=self.smt_retry_limit, + smt_tactic=self.smt_tactic, + trace_rewrites=self.trace_rewrites, + port=self.port, + maude_port=self.maude_port, + ) + + pretty_term = foundry_simplify_node( + foundry=_load_foundry(self.foundry_root, self.bug_report), + test=self.test, + version=self.version, + node=self.node, + rpc_options=rpc_options, + replace=self.replace, + minimize=self.minimize, + sort_collections=self.sort_collections, + bug_report=self.bug_report, + ) + print(f'Simplified:\n{pretty_term}') + + +class StepNodeCommand( + Command, FoundryTestOptions, KEVMRPCOptions, BugReportOptions, SMTOptions, FoundryOptions, LoggingOptions +): + node: NodeIdLike + repeat: int + depth: int + + @staticmethod + def name() -> str: + return 'step-node' + + @staticmethod + def help_str() -> str: + return 'Step from a given node, adding it to the CFG.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'repeat': 1, + 'depth': 1, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('node', type=node_id_like, help='Node to step from in CFG.') + parser.add_argument( + '--repeat', type=int, help='How many node expansions to do from the given start node (>= 1).' + ) + parser.add_argument('--depth', type=int, help='How many steps to take from initial node on edge.') + + def exec(self) -> None: + kore_rpc_command = ( + self.kore_rpc_command.split() if isinstance(self.kore_rpc_command, str) else self.kore_rpc_command + ) + + rpc_options = RPCOptions( + use_booster=self.use_booster, + kore_rpc_command=kore_rpc_command, + smt_timeout=self.smt_timeout, + smt_retry_limit=self.smt_retry_limit, + smt_tactic=self.smt_tactic, + trace_rewrites=self.trace_rewrites, + port=self.port, + maude_port=self.maude_port, + ) + + foundry_step_node( + foundry=_load_foundry(self.foundry_root, self.bug_report), + test=self.test, + version=self.version, + node=self.node, + rpc_options=rpc_options, + repeat=self.repeat, + depth=self.depth, + bug_report=self.bug_report, + ) + + +class MergeNodesCommand(Command, FoundryTestOptions, FoundryOptions, LoggingOptions): + nodes: list[NodeIdLike] + + @staticmethod + def name() -> str: + return 'merge-nodes' + + @staticmethod + def help_str() -> str: + return 'Merge multiple nodes into one branch.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'nodes': [], + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument( + '--node', + type=node_id_like, + dest='nodes', + action='append', + help='One node to be merged.', + ) + + def exec(self) -> None: + foundry_merge_nodes( + foundry=_load_foundry(self.foundry_root), node_ids=self.nodes, test=self.test, version=self.version + ) + + +class SectionEdgeCommand( + Command, FoundryTestOptions, KEVMRPCOptions, BugReportOptions, SMTOptions, FoundryOptions, LoggingOptions +): + edge: tuple[str, str] + sections: int + + @staticmethod + def name() -> str: + return 'section-edge' - return parser + @staticmethod + def help_str() -> str: + return 'Given an edge in the graph, cut it into sections to get intermediate nodes.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'sections': 2, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('edge', type=arg_pair_of(str, str), help='Edge to section in CFG.') + parser.add_argument('--sections', type=int, help='Number of sections to make from edge (>= 2).') + + def exec(self) -> None: + kore_rpc_command = ( + self.kore_rpc_command.split() if isinstance(self.kore_rpc_command, str) else self.kore_rpc_command + ) + + rpc_options = RPCOptions( + use_booster=self.use_booster, + kore_rpc_command=kore_rpc_command, + smt_timeout=self.smt_timeout, + smt_retry_limit=self.smt_retry_limit, + smt_tactic=self.smt_tactic, + trace_rewrites=self.trace_rewrites, + port=self.port, + maude_port=self.maude_port, + ) + + foundry_section_edge( + foundry=_load_foundry(self.foundry_root, self.bug_report), + test=self.test, + version=self.version, + rpc_options=rpc_options, + edge=self.edge, + sections=self.sections, + bug_report=self.bug_report, + ) + + +class GetModelCommand( + Command, FoundryTestOptions, KEVMRPCOptions, BugReportOptions, SMTOptions, FoundryOptions, LoggingOptions +): + nodes: list[NodeIdLike] + pending: bool + failing: bool + + @staticmethod + def name() -> str: + return 'get-model' + + @staticmethod + def help_str() -> str: + return 'Display a model for a given node.' + + @staticmethod + def default() -> dict[str, Any]: + return { + 'nodes': [], + 'pending': False, + 'failing': False, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument( + '--node', + type=node_id_like, + dest='nodes', + action='append', + help='List of nodes to display the models of.', + ) + parser.add_argument( + '--pending', dest='pending', default=None, action='store_true', help='Also display models of pending nodes' + ) + parser.add_argument( + '--failing', dest='failing', default=None, action='store_true', help='Also display models of failing nodes' + ) + + def exec(self) -> None: + kore_rpc_command = ( + self.kore_rpc_command.split() if isinstance(self.kore_rpc_command, str) else self.kore_rpc_command + ) + + rpc_options = RPCOptions( + use_booster=self.use_booster, + kore_rpc_command=kore_rpc_command, + smt_timeout=self.smt_timeout, + smt_retry_limit=self.smt_retry_limit, + smt_tactic=self.smt_tactic, + trace_rewrites=self.trace_rewrites, + port=self.port, + maude_port=self.maude_port, + ) + output = foundry_get_model( + foundry=_load_foundry(self.foundry_root), + test=self.test, + version=self.version, + nodes=self.nodes, + rpc_options=rpc_options, + pending=self.pending, + failing=self.failing, + bug_report=self.bug_report, + ) + print(output) + + +# Helpers -def _loglevel(args: Namespace) -> int: +def _loglevel(args: LoggingOptions) -> int: if hasattr(args, 'debug') and args.debug: return logging.DEBUG diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py index 305426abb..fe11d4e5e 100644 --- a/src/kontrol/cli.py +++ b/src/kontrol/cli.py @@ -1,112 +1,157 @@ from __future__ import annotations -from argparse import ArgumentParser -from functools import cached_property from pathlib import Path from typing import TYPE_CHECKING -from kevm_pyk.cli import KEVMCLIArgs from kevm_pyk.kompile import KompileTarget +from pyk.cli.args import Options from pyk.cli.utils import dir_path if TYPE_CHECKING: - from typing import TypeVar + from argparse import ArgumentParser + from typing import Any, TypeVar T = TypeVar('T') -class KontrolCLIArgs(KEVMCLIArgs): - @cached_property - def foundry_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( +class FoundryOptions(Options): + foundry_root: Path + + @staticmethod + def default() -> dict[str, Any]: + return { + 'foundry_root': Path('.'), + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument( '--foundry-project-root', dest='foundry_root', type=dir_path, - default=Path('.'), help='Path to Foundry project root directory.', ) - return args - - @cached_property - def foundry_test_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument('test', type=str, help='Test to run') - args.add_argument('--version', type=int, default=None, required=False, help='Version of the test to use') - return args - - @cached_property - def k_gen_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( + + +class FoundryTestOptions(Options): + test: str + version: int | None + + @staticmethod + def default() -> dict[str, Any]: + return { + 'version': None, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument('test', type=str, help='Test to run') + parser.add_argument('--version', type=int, required=False, help='Version of the test to use') + + +class KGenOptions(Options): + requires: list[str] + imports: list[str] + + @staticmethod + def default() -> dict[str, Any]: + return { + 'requires': [], + 'imports': [], + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument( '--require', dest='requires', - default=[], action='append', help='Extra K requires to include in generated output.', ) - args.add_argument( + parser.add_argument( '--module-import', dest='imports', - default=[], action='append', help='Extra modules to import into generated main module.', ) - return args - @cached_property - def kompile_target_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( + +class KompileTargetOptions(Options): + target: KompileTarget + + @staticmethod + def default() -> dict[str, Any]: + return { + 'target': KompileTarget.HASKELL, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + parser.add_argument( '--target', type=KompileTarget, choices=[KompileTarget.HASKELL, KompileTarget.MAUDE], help='[haskell|maude]', ) - return args - @cached_property - def rpc_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( + +class RPCOptions(Options): + trace_rewrites: bool + kore_rpc_command: str | None + use_booster: bool + port: int | None + maude_port: int | None + + @staticmethod + def default() -> dict[str, Any]: + return { + 'trace_rewrites': False, + 'kore_rpc_command': None, + 'use_booster': True, + 'port': None, + 'maude_port': None, + } + + @staticmethod + def update_args(parser: ArgumentParser) -> None: + 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.', ) - 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=True, + default=None, action='store_true', help='Use the booster RPC server instead of kore-rpc.', ) - args.add_argument( + parser.add_argument( '--no-use-booster', dest='use_booster', + default=None, action='store_false', help='Do not use the booster RPC server instead of kore-rpc.', ) - 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 diff --git a/src/kontrol/foundry.py b/src/kontrol/foundry.py index 24c82c846..e4e4e74e4 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -1012,7 +1012,6 @@ def foundry_section_edge( rpc_options: RPCOptions, version: int | None = None, sections: int = 2, - replace: bool = False, bug_report: BugReport | None = None, ) -> None: test_id = foundry.get_test_id(test, version)