From 453fc1679d5660fe98a2f545e30b305147801b05 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 27 Oct 2023 14:06:41 -0500 Subject: [PATCH 1/7] Add escaping to sort_field --- src/kontrol/solc_to_k.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index 390e4f92f..11e4b4970 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -490,7 +490,7 @@ def sort(self) -> KSort: @property def sort_field(self) -> KSort: - return KSort(f'{self.name}Field') + return KSort(f'{Contract.escaped(self.name, "S2K")}Field') @property def sort_method(self) -> KSort: From 3bd825636547bba4119d917973c34cc18684d077 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 5 Mar 2024 19:31:20 -0600 Subject: [PATCH 2/7] Use new commands/arguments system --- pyproject.toml | 2 +- src/kontrol/__main__.py | 1639 ++++++++++++++++++++------------------- src/kontrol/cli.py | 132 ++-- src/kontrol/foundry.py | 1 - 4 files changed, 908 insertions(+), 866 deletions(-) diff --git a/pyproject.toml b/pyproject.toml index 86e766ffe..f0d8797ef 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -12,7 +12,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" -kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.477", subdirectory = "kevm-pyk" } +kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", branch = "noah/kevm-default-options", subdirectory = "kevm-pyk" } [tool.poetry.group.dev.dependencies] autoflake = "*" diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index dfc81788c..9cb51155c 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, @@ -41,7 +42,7 @@ from .solc_to_k import solc_compile, solc_to_k if TYPE_CHECKING: - from argparse import Namespace + from argparse import ArgumentParser, Namespace from collections.abc import Callable, Iterable from pathlib import Path from typing import Any, Final, TypeVar @@ -57,6 +58,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: @@ -78,18 +94,38 @@ def _load_foundry(foundry_root: Path, bug_report: BugReport | None = None) -> Fo def main() -> None: sys.setrecursionlimit(15000000) - parser = _create_argument_parser() + kontrol_cli = CLI( + { + VersionCommand, + CompileCommand, + SolcToKCommand, + BuildCommand, + LoadStateDiffCommand, + ProveCommand, + ShowCommand, + ToDotCommand, + ListCommand, + ViewKCFGCommand, + RemoveNodeCommand, + RefuteNodeCommand, + UnRefuteNodeCommand, + SimplifyNodeCommand, + StepNodeCommand, + MergeNodesCommand, + SectionEdgeCommand, + GetModelCommand, + } + ) + parser = kontrol_cli.create_argument_parser() args = parser.parse_args() + + command = kontrol_cli.generate_command({key: val for (key, val) in vars(args).items() if val is not None}) + logging.basicConfig(level=_loglevel(args), format=_LOG_FORMAT) _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)) + command.exec() def _check_k_version() -> None: @@ -120,870 +156,835 @@ 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): + 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): + @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): + 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, - **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, - ) + @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}') - else: - failed += 1 - print(f'PROOF FAILED: {proof.id}') - 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): + 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_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) + @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.') + 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): + 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', + action='store_true', + help='Regenerate foundry.k even if it already exists.', + ) + parser.add_argument( + '--rekompile', + dest='rekompile', + action='store_true', + help='Rekompile foundry.k even if kompiled definition already exists.', + ) + parser.add_argument( + '--no-forge-build', + dest='no_forge_build', + action='store_true', + help="Do not call 'forge build' during kompilation.", + ) -def exec_list(foundry_root: Path, **kwargs: Any) -> None: - stats = foundry_list(foundry=_load_foundry(foundry_root)) - print('\n'.join(stats)) + 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, + ) -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) +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 + + @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, + } + + @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', + 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', + action='store_true', + help='Include the contract constructor in the test execution.', + ) + parser.add_argument('--use-gas', dest='use_gas', action='store_true', help='Enables gas computation in KEVM.') + parser.add_argument( + '--break-on-cheatcodes', + dest='break_on_cheatcodes', + 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', + 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', + action='store_true', + help='Generate a JUnit XML report', + ) - def _short_info(cterm: CTerm) -> Iterable[str]: - return foundry.short_info_for_contract(contract_name, cterm) + def exec(self) -> None: + kore_rpc_command = ( + self.kore_rpc_command.split() if isinstance(self.kore_rpc_command, str) else self.kore_rpc_command + ) - def _custom_view(elem: KCFGElem) -> Iterable[str]: - return foundry.custom_view(contract_name, elem) + deployment_state_entries = ( + read_deployment_state(self.deployment_state_path) if self.deployment_state_path else None + ) - node_printer = foundry_node_printer(foundry, contract_name, proof) - viewer = APRProofViewer(proof, foundry.kevm, node_printer=node_printer, custom_view=_custom_view) - viewer.run() + 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, + ) + 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, + ) -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) + 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}') + else: + failed += 1 + print(f'PROOF FAILED: {proof.id}') + 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): + 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', + 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', + 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.', + ) + 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 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() +class RefuteNodeCommand(Command, FoundryTestOptions, FoundryOptions): + node: NodeIdLike - 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 name() -> str: + return 'refute-node' - 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, - ) + @staticmethod + def help_str() -> str: + return 'Refute a node and add its refutation as a subproof.' - 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, - ) + @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('node', type=node_id_like, help='Node to refute.') -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: + foundry_refute_node( + foundry=_load_foundry(self.foundry_root), test=self.test, node=self.node, version=self.version + ) - 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, - ) +class UnRefuteNodeCommand(Command, FoundryTestOptions, FoundryOptions): + node: NodeIdLike -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) + @staticmethod + def name() -> str: + return 'unrefute-node' + @staticmethod + def help_str() -> str: + return 'Disable refutation of a node and remove corresponding refutation subproof.' -# Helpers + @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('node', type=node_id_like, help='Node to unrefute.') -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)] + def exec(self) -> None: + foundry_unrefute_node( + foundry=_load_foundry(self.foundry_root), test=self.test, node=self.node, version=self.version + ) - return parse - kontrol_cli_args = KontrolCLIArgs() - parser = ArgumentParser(prog='kontrol') +class ToDotCommand(Command, FoundryTestOptions, FoundryOptions): + @staticmethod + def name() -> str: + return 'to-dot' - command_parser = parser.add_subparsers(dest='command', required=True) + @staticmethod + def help_str() -> str: + return 'Dump the given CFG for the test as DOT for visualization.' - command_parser.add_parser('version', help='Print out version of Kontrol command.') + def exec(self) -> None: + foundry_to_dot(foundry=_load_foundry(self.foundry_root), test=self.test, version=self.version) - 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.') - 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.') - - 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) - - 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.", - ) +class ListCommand(Command, KOptions, FoundryOptions): + @staticmethod + def name() -> str: + return 'list' - 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', - ) + @staticmethod + def help_str() -> str: + return 'List information about CFGs on disk' - 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', - ) + def exec(self) -> None: + stats = foundry_list(foundry=_load_foundry(self.foundry_root)) + print('\n'.join(stats)) - 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.', - ) - 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], - ) +class ViewKCFGCommand(Command, FoundryTestOptions, FoundryOptions): + @staticmethod + def name() -> str: + return 'view-kcfg' - 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 help_str() -> str: + return 'Explore a given proof in the KCFG visualizer.' - 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 = _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) - 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.') + def _short_info(cterm: CTerm) -> Iterable[str]: + return foundry.short_info_for_contract(contract_name, cterm) - 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.') + def _custom_view(elem: KCFGElem) -> Iterable[str]: + return foundry.custom_view(contract_name, elem) - 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.') - - 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.' - ) + node_printer = foundry_node_printer(foundry, contract_name, proof) + viewer = APRProofViewer(proof, foundry.kevm, node_printer=node_printer, custom_view=_custom_view) + viewer.run() - 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.', - ) - 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' - ) +class RemoveNodeCommand(Command, FoundryTestOptions, FoundryOptions): + node: NodeIdLike - return parser + @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 +): + 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): + 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): + 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): + edge: tuple[str, str] + sections: int + + @staticmethod + def name() -> str: + return 'section-edge' + + @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): + 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', action='store_true', help='Also display models of pending nodes' + ) + parser.add_argument( + '--failing', dest='failing', 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: diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py index 305426abb..a90b8ec9e 100644 --- a/src/kontrol/cli.py +++ b/src/kontrol/cli.py @@ -1,112 +1,154 @@ 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, 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, 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', 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 175209f51..7d8eee0f8 100644 --- a/src/kontrol/foundry.py +++ b/src/kontrol/foundry.py @@ -972,7 +972,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) From 3461269b6332d8e070ffdb9abc61bef0924c8fbc Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 6 Mar 2024 20:14:27 -0600 Subject: [PATCH 3/7] Use get_command() --- src/kontrol/__main__.py | 67 ++++++++++++++++++++++++----------------- 1 file changed, 40 insertions(+), 27 deletions(-) diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index 9cb51155c..cf07385c5 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -42,7 +42,7 @@ from .solc_to_k import solc_compile, solc_to_k if TYPE_CHECKING: - from argparse import ArgumentParser, Namespace + from argparse import ArgumentParser from collections.abc import Callable, Iterable from pathlib import Path from typing import Any, Final, TypeVar @@ -116,16 +116,12 @@ def main() -> None: GetModelCommand, } ) - parser = kontrol_cli.create_argument_parser() - args = parser.parse_args() - - command = kontrol_cli.generate_command({key: val for (key, val) in vars(args).items() if val is not None}) - - logging.basicConfig(level=_loglevel(args), format=_LOG_FORMAT) _check_k_version() - - command.exec() + cmd = kontrol_cli.get_command() + assert isinstance(cmd, LoggingOptions) + logging.basicConfig(level=_loglevel(cmd), format=_LOG_FORMAT) + cmd.exec() def _check_k_version() -> None: @@ -156,7 +152,7 @@ def _compare_versions(ver1: KVersion, ver2: KVersion) -> bool: # Command implementation -class LoadStateDiffCommand(Command, FoundryOptions): +class LoadStateDiffCommand(Command, FoundryOptions, LoggingOptions): contract_name: str accesses_file: Path contract_names: Path | None @@ -231,7 +227,7 @@ def exec(self) -> None: ) -class VersionCommand(Command): +class VersionCommand(Command, LoggingOptions): @staticmethod def name() -> str: return 'version' @@ -244,7 +240,7 @@ def exec(self) -> None: print(f'Kontrol version: {VERSION}') -class CompileCommand(Command): +class CompileCommand(Command, LoggingOptions): contract_file: Path @staticmethod @@ -264,7 +260,7 @@ def exec(self) -> None: print(json.dumps(res)) -class SolcToKCommand(Command, KOptions, KGenOptions): +class SolcToKCommand(Command, KOptions, KGenOptions, LoggingOptions): contract_file: Path contract_name: str @@ -292,7 +288,9 @@ def exec(self) -> None: print(k_text) -class BuildCommand(Command, KOptions, KGenOptions, KompileOptions, FoundryOptions, KompileTargetOptions): +class BuildCommand( + Command, KOptions, KGenOptions, KompileOptions, FoundryOptions, KompileTargetOptions, LoggingOptions +): regen: bool rekompile: bool no_forge_build: bool @@ -529,7 +527,9 @@ def exec(self) -> None: sys.exit(failed) -class ShowCommand(ShowKCFGCommand, FoundryTestOptions, KOptions, KEVMDisplayOptions, FoundryOptions, KEVMRPCOptions): +class ShowCommand( + ShowKCFGCommand, FoundryTestOptions, KOptions, KEVMDisplayOptions, FoundryOptions, KEVMRPCOptions, LoggingOptions +): omit_unstable_output: bool to_kevm_claims: bool kevm_claim_dir: Path | None @@ -593,7 +593,7 @@ def exec(self) -> None: print(output) -class RefuteNodeCommand(Command, FoundryTestOptions, FoundryOptions): +class RefuteNodeCommand(Command, FoundryTestOptions, FoundryOptions, LoggingOptions): node: NodeIdLike @staticmethod @@ -622,7 +622,7 @@ def exec(self) -> None: ) -class UnRefuteNodeCommand(Command, FoundryTestOptions, FoundryOptions): +class UnRefuteNodeCommand(Command, FoundryTestOptions, FoundryOptions, LoggingOptions): node: NodeIdLike @staticmethod @@ -651,7 +651,7 @@ def exec(self) -> None: ) -class ToDotCommand(Command, FoundryTestOptions, FoundryOptions): +class ToDotCommand(Command, FoundryTestOptions, FoundryOptions, LoggingOptions): @staticmethod def name() -> str: return 'to-dot' @@ -664,7 +664,7 @@ def exec(self) -> None: foundry_to_dot(foundry=_load_foundry(self.foundry_root), test=self.test, version=self.version) -class ListCommand(Command, KOptions, FoundryOptions): +class ListCommand(Command, KOptions, FoundryOptions, LoggingOptions): @staticmethod def name() -> str: return 'list' @@ -678,7 +678,7 @@ def exec(self) -> None: print('\n'.join(stats)) -class ViewKCFGCommand(Command, FoundryTestOptions, FoundryOptions): +class ViewKCFGCommand(Command, FoundryTestOptions, FoundryOptions, LoggingOptions): @staticmethod def name() -> str: return 'view-kcfg' @@ -704,7 +704,7 @@ def _custom_view(elem: KCFGElem) -> Iterable[str]: viewer.run() -class RemoveNodeCommand(Command, FoundryTestOptions, FoundryOptions): +class RemoveNodeCommand(Command, FoundryTestOptions, FoundryOptions, LoggingOptions): node: NodeIdLike @staticmethod @@ -726,7 +726,14 @@ def exec(self) -> None: class SimplifyNodeCommand( - Command, FoundryTestOptions, SMTOptions, KEVMRPCOptions, BugReportOptions, KEVMDisplayOptions, FoundryOptions + Command, + FoundryTestOptions, + SMTOptions, + KEVMRPCOptions, + BugReportOptions, + KEVMDisplayOptions, + FoundryOptions, + LoggingOptions, ): node: NodeIdLike replace: bool @@ -780,7 +787,9 @@ def exec(self) -> None: print(f'Simplified:\n{pretty_term}') -class StepNodeCommand(Command, FoundryTestOptions, KEVMRPCOptions, BugReportOptions, SMTOptions, FoundryOptions): +class StepNodeCommand( + Command, FoundryTestOptions, KEVMRPCOptions, BugReportOptions, SMTOptions, FoundryOptions, LoggingOptions +): node: NodeIdLike repeat: int depth: int @@ -836,7 +845,7 @@ def exec(self) -> None: ) -class MergeNodesCommand(Command, FoundryTestOptions, FoundryOptions): +class MergeNodesCommand(Command, FoundryTestOptions, FoundryOptions, LoggingOptions): nodes: list[NodeIdLike] @staticmethod @@ -869,7 +878,9 @@ def exec(self) -> None: ) -class SectionEdgeCommand(Command, FoundryTestOptions, KEVMRPCOptions, BugReportOptions, SMTOptions, FoundryOptions): +class SectionEdgeCommand( + Command, FoundryTestOptions, KEVMRPCOptions, BugReportOptions, SMTOptions, FoundryOptions, LoggingOptions +): edge: tuple[str, str] sections: int @@ -919,7 +930,9 @@ def exec(self) -> None: ) -class GetModelCommand(Command, FoundryTestOptions, KEVMRPCOptions, BugReportOptions, SMTOptions, FoundryOptions): +class GetModelCommand( + Command, FoundryTestOptions, KEVMRPCOptions, BugReportOptions, SMTOptions, FoundryOptions, LoggingOptions +): nodes: list[NodeIdLike] pending: bool failing: bool @@ -987,7 +1000,7 @@ def exec(self) -> None: # Helpers -def _loglevel(args: Namespace) -> int: +def _loglevel(args: LoggingOptions) -> int: if hasattr(args, 'debug') and args.debug: return logging.DEBUG From f6a91ada27454fdcc7973a06d999a21f6870c4c0 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 7 Mar 2024 02:25:49 +0000 Subject: [PATCH 4/7] Set Version: 0.1.188 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index fd39f6dee..64b5cd7f1 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.187 +0.1.188 diff --git a/pyproject.toml b/pyproject.toml index 33dfd193b..7a7527bc0 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.187" +version = "0.1.188" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 62bf313dc..cf1dcbf50 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.187' +VERSION: Final = '0.1.188' From 9a2cdc3ed0272c0977d110fa4780e2fb41de1183 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 6 Mar 2024 21:20:27 -0600 Subject: [PATCH 5/7] Update poetry.lock --- poetry.lock | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/poetry.lock b/poetry.lock index 2d94dcbae..dd2387af2 100644 --- a/poetry.lock +++ b/poetry.lock @@ -1,4 +1,4 @@ -# This file is automatically @generated by Poetry 1.7.0 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" @@ -434,7 +434,7 @@ colors = ["colorama (>=0.4.6)"] [[package]] name = "kevm-pyk" -version = "1.0.482" +version = "1.0.484" 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.681"} +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.482" -resolved_reference = "65f4327edf082bb2ead886eb83b3d47f697363dd" +reference = "noah/kevm-default-options" +resolved_reference = "29e4803789432971dac2030b21c5d6d39ae3b008" subdirectory = "kevm-pyk" [[package]] @@ -809,7 +809,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pyk" -version = "0.1.681" +version = "0.1.686" 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.681" -resolved_reference = "2c9a739d0e20dceb70076e01a31999bb5b5e8b5e" +reference = "noah/default-options" +resolved_reference = "2f58d508170fd354fedb9824c17a22ed495c9051" [[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 = "7f8012ff5759ab3c4f3a7f5ef3893bdb56a52e0caf144f688ef25abec92fe915" +content-hash = "916afbae0a76927b36734bea9a69a1e9500e3c30f21191715ee448b76eea1821" From 3a5f77cda4c3f4b220a5cb70b89ecdb3b132be1f Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 11 Mar 2024 22:29:29 +0000 Subject: [PATCH 6/7] Set Version: 0.1.195 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) 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/pyproject.toml b/pyproject.toml index e81542b32..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. ", 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' From fba2bf2e9912d4fc3d3e165619d245e27158f7af Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Mon, 11 Mar 2024 17:31:10 -0500 Subject: [PATCH 7/7] Use default=None for boolean options --- src/kontrol/__main__.py | 18 ++++++++++++++---- src/kontrol/cli.py | 3 +++ 2 files changed, 17 insertions(+), 4 deletions(-) diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index 858c04df7..7aee0c1fa 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -318,18 +318,21 @@ 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.", ) @@ -415,6 +418,7 @@ def update_args(parser: ArgumentParser) -> None: parser.add_argument( '--reinit', dest='reinit', + default=None, action='store_true', help='Reinitialize CFGs even if they already exist.', ) @@ -427,13 +431,15 @@ def update_args(parser: ArgumentParser) -> None: 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', action='store_true', help='Enables gas computation in KEVM.') + 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.', ) @@ -453,16 +459,18 @@ def update_args(parser: ArgumentParser) -> None: 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', action='store_true', help='Use Compositional Symbolic Execution') + parser.add_argument('--cse', dest='cse', default=None, action='store_true', help='Use Compositional Symbolic Execution') def exec(self) -> None: kore_rpc_command = ( @@ -562,12 +570,14 @@ 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).', ) @@ -999,10 +1009,10 @@ def update_args(parser: ArgumentParser) -> None: help='List of nodes to display the models of.', ) parser.add_argument( - '--pending', dest='pending', action='store_true', help='Also display models of pending nodes' + '--pending', dest='pending', default=None, action='store_true', help='Also display models of pending nodes' ) parser.add_argument( - '--failing', dest='failing', action='store_true', help='Also display models of failing nodes' + '--failing', dest='failing', default=None, action='store_true', help='Also display models of failing nodes' ) def exec(self) -> None: diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py index a90b8ec9e..fe11d4e5e 100644 --- a/src/kontrol/cli.py +++ b/src/kontrol/cli.py @@ -117,6 +117,7 @@ def update_args(parser: ArgumentParser) -> None: parser.add_argument( '--trace-rewrites', dest='trace_rewrites', + default=None, action='store_true', help='Log traces of all simplification and rewrite rule applications.', ) @@ -129,12 +130,14 @@ def update_args(parser: ArgumentParser) -> None: parser.add_argument( '--use-booster', dest='use_booster', + default=None, action='store_true', help='Use the booster RPC server instead of kore-rpc.', ) 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.', )