From 132a6c5cb18b4795f90b1b8dfc26fea0baa6ac82 Mon Sep 17 00:00:00 2001 From: Noah Watson <107630091+nwatson22@users.noreply.github.com> Date: Fri, 20 Oct 2023 20:26:26 -0500 Subject: [PATCH] Encapsulate program-level options (#108) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * Add GlobalOptions class to encapsulate options constant for one kontrol prove run * Set Version: 0.1.28 * Set Version: 0.1.30 * Don't pass options on public function * Move options construction to exec_prove, add constructor with default args * Fix typo in help message * Rename class to ProveOptions * Set Version: 0.1.33 * Update src/kontrol/prove.py * Address comments * Set Version: 0.1.34 * Update src/kontrol/options.py Co-authored-by: Tamás Tóth --------- Co-authored-by: devops Co-authored-by: Tamás Tóth --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- src/kontrol/__main__.py | 39 ++++-- src/kontrol/options.py | 82 +++++++++++ src/kontrol/prove.py | 142 +++++++------------- src/tests/integration/test_foundry_prove.py | 102 +++++++++----- src/tests/profiling/test_foundry_prove.py | 15 ++- 8 files changed, 232 insertions(+), 154 deletions(-) create mode 100644 src/kontrol/options.py diff --git a/package/version b/package/version index 50140e353..9dd179330 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.33 +0.1.34 diff --git a/pyproject.toml b/pyproject.toml index 85a9e6785..947bf64d8 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.33" +version = "0.1.34" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 7aa6780b4..eba1e2e9f 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.33' +VERSION: Final = '0.1.34' diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index 68bbef766..dc1b3a742 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -28,6 +28,7 @@ foundry_to_dot, ) from .kompile import foundry_kompile +from .options import ProveOptions from .prove import foundry_prove from .solc_to_k import solc_compile, solc_to_k @@ -160,6 +161,7 @@ def exec_prove( trace_rewrites: bool = False, auto_abstract_gas: bool = False, run_constructor: bool = False, + fail_fast: bool = False, **kwargs: Any, ) -> None: _ignore_arg(kwargs, 'main_module', f'--main-module: {kwargs["main_module"]}') @@ -175,26 +177,30 @@ def exec_prove( if isinstance(kore_rpc_command, str): kore_rpc_command = kore_rpc_command.split() - results = foundry_prove( - foundry_root=foundry_root, - max_depth=max_depth, - max_iterations=max_iterations, + options = ProveOptions( + auto_abstract_gas=auto_abstract_gas, reinit=reinit, - tests=tests, - workers=workers, - break_every_step=break_every_step, - break_on_jumpi=break_on_jumpi, - break_on_calls=break_on_calls, - bmc_depth=bmc_depth, bug_report=bug_report, kore_rpc_command=kore_rpc_command, - use_booster=use_booster, - counterexample_info=counterexample_info, smt_timeout=smt_timeout, smt_retry_limit=smt_retry_limit, trace_rewrites=trace_rewrites, - auto_abstract_gas=auto_abstract_gas, + 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, + workers=workers, + counterexample_info=counterexample_info, + max_iterations=max_iterations, run_constructor=run_constructor, + fail_fast=fail_fast, + ) + + results = foundry_prove( + foundry_root=foundry_root, + options=options, + tests=tests, ) failed = 0 for pid, r in results.items(): @@ -526,6 +532,13 @@ def _parse_test_version_tuple(value: str) -> tuple[str, int | None]: action='store_true', help='Include the contract constructor in the test execution.', ) + prove_args.add_argument( + '--fail-fast', + dest='fail_fast', + default=False, + action='store_true', + help='Stop execution on other branches if a failing node is detected.', + ) show_args = command_parser.add_parser( 'show', diff --git a/src/kontrol/options.py b/src/kontrol/options.py new file mode 100644 index 000000000..de80f9db7 --- /dev/null +++ b/src/kontrol/options.py @@ -0,0 +1,82 @@ +from __future__ import annotations + +from dataclasses import dataclass +from typing import TYPE_CHECKING + +if TYPE_CHECKING: + from collections.abc import Iterable + + from pyk.utils import BugReport + + +@dataclass(frozen=True) +class ProveOptions: + auto_abstract_gas: bool + bug_report: BugReport | None + use_booster: bool + kore_rpc_command: tuple[str, ...] + smt_timeout: int | None + smt_retry_limit: int | None + trace_rewrites: bool + simplify_init: bool + bmc_depth: int | None + max_depth: int + break_every_step: bool + break_on_jumpi: bool + break_on_calls: bool + workers: int + counterexample_info: bool + max_iterations: int | None + run_constructor: bool + fail_fast: bool + reinit: bool + port: int | None + + def __init__( + self, + *, + auto_abstract_gas: bool = False, + bug_report: BugReport | None = None, + use_booster: bool = True, + kore_rpc_command: str | Iterable[str] | None = None, + smt_timeout: int | None = None, + smt_retry_limit: int | None = None, + trace_rewrites: bool = False, + bmc_depth: int | None = None, + max_depth: int = 1000, + break_every_step: bool = False, + break_on_jumpi: bool = False, + break_on_calls: bool = True, + workers: int = 1, + counterexample_info: bool = False, + max_iterations: int | None = None, + run_constructor: bool = False, + fail_fast: bool = True, + reinit: bool = False, + port: int | None = None, + ) -> None: + if kore_rpc_command is None: + kore_rpc_command = ('kore-rpc-booster',) if use_booster else ('kore-rpc',) + elif isinstance(kore_rpc_command, str): + kore_rpc_command = (kore_rpc_command,) + else: + kore_rpc_command = tuple(kore_rpc_command) + object.__setattr__(self, 'auto_abstract_gas', auto_abstract_gas) + object.__setattr__(self, 'bug_report', bug_report) + object.__setattr__(self, 'use_booster', use_booster) + object.__setattr__(self, 'kore_rpc_command', kore_rpc_command) + object.__setattr__(self, 'smt_timeout', smt_timeout) + object.__setattr__(self, 'smt_retry_limit', smt_retry_limit) + object.__setattr__(self, 'trace_rewrites', trace_rewrites) + object.__setattr__(self, 'bmc_depth', bmc_depth) + object.__setattr__(self, 'max_depth', max_depth) + object.__setattr__(self, 'break_every_step', break_every_step) + object.__setattr__(self, 'break_on_jumpi', break_on_jumpi) + object.__setattr__(self, 'break_on_calls', break_on_calls) + object.__setattr__(self, 'workers', workers) + object.__setattr__(self, 'counterexample_info', counterexample_info) + object.__setattr__(self, 'max_iterations', max_iterations) + object.__setattr__(self, 'run_constructor', run_constructor) + object.__setattr__(self, 'fail_fast', fail_fast) + object.__setattr__(self, 'reinit', reinit) + object.__setattr__(self, 'port', port) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 4b0a82961..16c5578fb 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -35,7 +35,8 @@ from pyk.kast.inner import KInner from pyk.kcfg import KCFGExplore - from pyk.utils import BugReport + + from .options import ProveOptions _LOGGER: Final = logging.getLogger(__name__) @@ -43,33 +44,17 @@ def foundry_prove( foundry_root: Path, - max_depth: int = 1000, - max_iterations: int | None = None, - reinit: bool = False, + options: ProveOptions, tests: Iterable[tuple[str, int | None]] = (), - workers: int = 1, - break_every_step: bool = False, - break_on_jumpi: bool = False, - break_on_calls: bool = True, - bmc_depth: int | None = None, - 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, - failure_info: bool = True, - counterexample_info: bool = False, - trace_rewrites: bool = False, - auto_abstract_gas: bool = False, - port: int | None = None, - run_constructor: bool = False, ) -> dict[tuple[str, int], tuple[bool, list[str] | None]]: - if workers <= 0: - raise ValueError(f'Must have at least one worker, found: --workers {workers}') - if max_iterations is not None and max_iterations < 0: - raise ValueError(f'Must have a non-negative number of iterations, found: --max-iterations {max_iterations}') + if options.workers <= 0: + raise ValueError(f'Must have at least one worker, found: --workers {options.workers}') + if options.max_iterations is not None and options.max_iterations < 0: + raise ValueError( + f'Must have a non-negative number of iterations, found: --max-iterations {options.max_iterations}' + ) - if use_booster: + if options.use_booster: try: run_process(('which', 'kore-rpc-booster'), pipe_stderr=True).stdout.strip() except CalledProcessError: @@ -77,20 +62,17 @@ def foundry_prove( "Couldn't locate the kore-rpc-booster RPC binary. Please put 'kore-rpc-booster' on PATH manually or using kup install/kup shell." ) from None - if kore_rpc_command is None: - kore_rpc_command = ('kore-rpc-booster',) if use_booster else ('kore-rpc',) - - foundry = Foundry(foundry_root, bug_report=bug_report) + foundry = Foundry(foundry_root, bug_report=options.bug_report) foundry.mk_proofs_dir() - test_suite = collect_tests(foundry, tests, reinit=reinit) + test_suite = collect_tests(foundry, tests, reinit=options.reinit) test_names = [test.name for test in test_suite] contracts = [test.contract for test in test_suite] - setup_method_tests = collect_setup_methods(foundry, contracts, reinit=reinit) + setup_method_tests = collect_setup_methods(foundry, contracts, reinit=options.reinit) setup_method_names = [test.name for test in setup_method_tests] - constructor_tests = collect_constructors(foundry, contracts, reinit=reinit) + constructor_tests = collect_constructors(foundry, contracts, reinit=options.reinit) constructor_names = [test.name for test in constructor_tests] _LOGGER.info(f'Running tests: {test_names}') @@ -109,28 +91,12 @@ def foundry_prove( def run_prover(test_suite: list[FoundryTest]) -> dict[tuple[str, int], tuple[bool, list[str] | None]]: return _run_cfg_group( - test_suite, - foundry, - max_depth=max_depth, - max_iterations=max_iterations, - workers=workers, - break_every_step=break_every_step, - break_on_jumpi=break_on_jumpi, - break_on_calls=break_on_calls, - bmc_depth=bmc_depth, - bug_report=bug_report, - kore_rpc_command=kore_rpc_command, - use_booster=use_booster, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - counterexample_info=counterexample_info, - trace_rewrites=trace_rewrites, - auto_abstract_gas=auto_abstract_gas, - port=port, - run_constructor=run_constructor, + tests=test_suite, + foundry=foundry, + options=options, ) - if run_constructor: + if options.run_constructor: _LOGGER.info(f'Running initialization code for contracts in parallel: {constructor_names}') results = run_prover(constructor_tests) failed = [init_cfg for init_cfg, passed in results.items() if not passed] @@ -215,68 +181,50 @@ def collect_constructors(foundry: Foundry, contracts: Iterable[Contract] = (), * def _run_cfg_group( tests: list[FoundryTest], foundry: Foundry, - *, - max_depth: int, - max_iterations: int | None, - workers: int, - break_every_step: bool, - break_on_jumpi: bool, - break_on_calls: bool, - bmc_depth: int | None, - bug_report: BugReport | None, - kore_rpc_command: str | Iterable[str] | None, - use_booster: bool, - smt_timeout: int | None, - smt_retry_limit: int | None, - counterexample_info: bool, - trace_rewrites: bool, - auto_abstract_gas: bool, - port: int | None, - run_constructor: bool = False, + options: ProveOptions, ) -> dict[tuple[str, int], tuple[bool, list[str] | None]]: def init_and_run_proof(test: FoundryTest) -> tuple[bool, list[str] | None]: - llvm_definition_dir = foundry.llvm_library if use_booster else None - start_server = port is None + start_server = options.port is None with legacy_explore( foundry.kevm, - kcfg_semantics=KEVMSemantics(auto_abstract_gas=auto_abstract_gas), + kcfg_semantics=KEVMSemantics(auto_abstract_gas=options.auto_abstract_gas), id=test.id, - bug_report=bug_report, - kore_rpc_command=kore_rpc_command, - llvm_definition_dir=llvm_definition_dir, - smt_timeout=smt_timeout, - smt_retry_limit=smt_retry_limit, - trace_rewrites=trace_rewrites, + bug_report=options.bug_report, + kore_rpc_command=options.kore_rpc_command, + llvm_definition_dir=foundry.llvm_library if options.use_booster else None, + smt_timeout=options.smt_timeout, + smt_retry_limit=options.smt_retry_limit, + trace_rewrites=options.trace_rewrites, start_server=start_server, - port=port, + port=options.port, ) as kcfg_explore: proof = method_to_apr_proof( - foundry, - test, - kcfg_explore, - bmc_depth=bmc_depth, - run_constructor=run_constructor, + test=test, + foundry=foundry, + kcfg_explore=kcfg_explore, + bmc_depth=options.bmc_depth, + run_constructor=options.run_constructor, ) passed = kevm_prove( foundry.kevm, proof, kcfg_explore, - max_depth=max_depth, - max_iterations=max_iterations, - break_every_step=break_every_step, - break_on_jumpi=break_on_jumpi, - break_on_calls=break_on_calls, + max_depth=options.max_depth, + max_iterations=options.max_iterations, + break_every_step=options.break_every_step, + break_on_jumpi=options.break_on_jumpi, + break_on_calls=options.break_on_calls, ) failure_log = None if not passed: - failure_log = print_failure_info(proof, kcfg_explore, counterexample_info) + failure_log = print_failure_info(proof, kcfg_explore, options.counterexample_info) return passed, failure_log _apr_proofs: list[tuple[bool, list[str] | None]] - if workers > 1: - with ProcessPool(ncpus=workers) as process_pool: + if options.workers > 1: + with ProcessPool(ncpus=options.workers) as process_pool: _apr_proofs = process_pool.map(init_and_run_proof, tests) else: _apr_proofs = [] @@ -289,8 +237,8 @@ def init_and_run_proof(test: FoundryTest) -> tuple[bool, list[str] | None]: def method_to_apr_proof( - foundry: Foundry, test: FoundryTest, + foundry: Foundry, kcfg_explore: KCFGExplore, bmc_depth: int | None = None, run_constructor: bool = False, @@ -311,9 +259,9 @@ def method_to_apr_proof( setup_proof = _load_constructor_proof(foundry, test.contract) kcfg, init_node_id, target_node_id = _method_to_initialized_cfg( - foundry, - test, - kcfg_explore, + foundry=foundry, + test=test, + kcfg_explore=kcfg_explore, setup_proof=setup_proof, ) diff --git a/src/tests/integration/test_foundry_prove.py b/src/tests/integration/test_foundry_prove.py index 2b401bd4b..4f755dc9b 100644 --- a/src/tests/integration/test_foundry_prove.py +++ b/src/tests/integration/test_foundry_prove.py @@ -12,6 +12,7 @@ from kontrol.foundry import Foundry, foundry_merge_nodes, foundry_remove_node, foundry_show, foundry_step_node from kontrol.kompile import foundry_kompile +from kontrol.options import ProveOptions from kontrol.prove import foundry_prove from .utils import TEST_DATA_DIR @@ -129,9 +130,11 @@ def test_foundry_prove( prove_res = foundry_prove( foundry_root, tests=[(test_id, None)], - counterexample_info=True, - port=server.port, - bug_report=bug_report, + options=ProveOptions( + counterexample_info=True, + bug_report=bug_report, + port=server.port, + ), ) # Then @@ -163,14 +166,22 @@ def test_foundry_prove( @pytest.mark.parametrize('test_id', FAIL_TESTS) def test_foundry_fail( - test_id: str, foundry_root: Path, update_expected_output: bool, use_booster: bool, server: KoreServer + test_id: str, + foundry_root: Path, + update_expected_output: bool, + use_booster: bool, + bug_report: BugReport | None, + server: KoreServer, ) -> None: # When prove_res = foundry_prove( foundry_root, tests=[(test_id, None)], - counterexample_info=True, - port=server.port, + options=ProveOptions( + counterexample_info=True, + bug_report=bug_report, + port=server.port, + ), ) # Then @@ -210,9 +221,11 @@ def test_foundry_bmc(test_id: str, foundry_root: Path, bug_report: BugReport | N prove_res = foundry_prove( foundry_root, tests=[(test_id, None)], - bmc_depth=3, - port=server.port, - bug_report=bug_report, + options=ProveOptions( + bmc_depth=3, + port=server.port, + bug_report=bug_report, + ), ) # Then @@ -225,9 +238,11 @@ def test_foundry_merge_nodes(foundry_root: Path, bug_report: BugReport | None, s foundry_prove( foundry_root, tests=[(test, None)], - max_iterations=2, - port=server.port, - bug_report=bug_report, + options=ProveOptions( + max_iterations=2, + port=server.port, + bug_report=bug_report, + ), ) check_pending(foundry_root, test, [4, 5]) @@ -244,8 +259,10 @@ def test_foundry_merge_nodes(foundry_root: Path, bug_report: BugReport | None, s prove_res = foundry_prove( foundry_root, tests=[(test, None)], - port=server.port, - bug_report=bug_report, + options=ProveOptions( + port=server.port, + bug_report=bug_report, + ), ) assert_pass(test, prove_res) @@ -269,9 +286,11 @@ def test_foundry_auto_abstraction( foundry_prove( foundry_root, tests=[(test_id, None)], - auto_abstract_gas=True, - bug_report=bug_report, - port=server.port, + options=ProveOptions( + auto_abstract_gas=True, + bug_report=bug_report, + port=server.port, + ), ) if use_booster: @@ -303,8 +322,10 @@ def test_foundry_remove_node( prove_res = foundry_prove( foundry_root, tests=[(test, None)], - port=server.port, - bug_report=bug_report, + options=ProveOptions( + port=server.port, + bug_report=bug_report, + ), ) assert_pass(test, prove_res) @@ -321,8 +342,10 @@ def test_foundry_remove_node( prove_res = foundry_prove( foundry_root, tests=[(test, None)], - port=server.port, - bug_report=bug_report, + options=ProveOptions( + port=server.port, + bug_report=bug_report, + ), ) assert_pass(test, prove_res) @@ -380,11 +403,13 @@ def test_foundry_resume_proof( prove_res = foundry_prove( foundry_root, tests=[(test, None)], - auto_abstract_gas=True, - max_iterations=4, - reinit=True, - port=server.port, - bug_report=bug_report, + options=ProveOptions( + auto_abstract_gas=True, + max_iterations=4, + reinit=True, + port=server.port, + bug_report=bug_report, + ), ) id = id_for_test(test, prove_res) @@ -394,11 +419,13 @@ def test_foundry_resume_proof( prove_res = foundry_prove( foundry_root, tests=[(test, id)], - auto_abstract_gas=True, - max_iterations=6, - reinit=False, - port=server.port, - bug_report=bug_report, + options=ProveOptions( + auto_abstract_gas=True, + max_iterations=6, + reinit=False, + port=server.port, + bug_report=bug_report, + ), ) assert_fail(test, prove_res) @@ -407,15 +434,18 @@ def test_foundry_resume_proof( @pytest.mark.parametrize('test', ALL_INIT_CODE_TESTS) -def test_foundry_init_code(test: str, foundry_root: Path, use_booster: bool) -> None: +def test_foundry_init_code(test: str, foundry_root: Path, bug_report: BugReport | None, use_booster: bool) -> None: # When prove_res = foundry_prove( foundry_root, tests=[(test, None)], - smt_timeout=300, - smt_retry_limit=10, - use_booster=use_booster, - run_constructor=True, + options=ProveOptions( + smt_timeout=300, + smt_retry_limit=10, + use_booster=use_booster, + run_constructor=True, + bug_report=bug_report, + ), ) # Then diff --git a/src/tests/profiling/test_foundry_prove.py b/src/tests/profiling/test_foundry_prove.py index 37674d599..9b528b6f1 100644 --- a/src/tests/profiling/test_foundry_prove.py +++ b/src/tests/profiling/test_foundry_prove.py @@ -7,6 +7,7 @@ from pyk.utils import run_process from kontrol.kompile import foundry_kompile +from kontrol.options import ProveOptions from kontrol.prove import foundry_prove from .utils import TEST_DATA_DIR @@ -16,6 +17,7 @@ from typing import Final from pyk.testing import Profiler + from pyk.utils import BugReport sys.setrecursionlimit(10**7) @@ -24,7 +26,7 @@ FORGE_STD_REF: Final = '75f1746' -def test_foundy_prove(profile: Profiler, use_booster: bool, tmp_path: Path) -> None: +def test_foundy_prove(profile: Profiler, use_booster: bool, bug_report: BugReport | None, tmp_path: Path) -> None: foundry_root = tmp_path / 'foundry' _forge_build(foundry_root) @@ -36,10 +38,13 @@ def test_foundy_prove(profile: Profiler, use_booster: bool, tmp_path: Path) -> N foundry_prove( foundry_root, tests=[('AssertTest.test_revert_branch', None)], - smt_timeout=300, - smt_retry_limit=10, - counterexample_info=True, - use_booster=use_booster, + options=ProveOptions( + smt_timeout=300, + smt_retry_limit=10, + counterexample_info=True, + bug_report=bug_report, + use_booster=use_booster, + ), )