From 3e8a0ef0999fa2243da5afcbef9f15d8642d2c85 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Tue, 17 Oct 2023 18:11:47 -0500 Subject: [PATCH 01/12] Add GlobalOptions class to encapsulate options constant for one kontrol prove run --- src/kontrol/__main__.py | 8 +++ src/kontrol/options.py | 35 ++++++++++ src/kontrol/prove.py | 142 ++++++++++++++++++---------------------- 3 files changed, 105 insertions(+), 80 deletions(-) create mode 100644 src/kontrol/options.py diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index 45591dd16..41d98f4da 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -161,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"]}') @@ -528,6 +529,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 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..5cb3caf43 --- /dev/null +++ b/src/kontrol/options.py @@ -0,0 +1,35 @@ +from __future__ import annotations + +from dataclasses import dataclass +from typing import TYPE_CHECKING + +if TYPE_CHECKING: + from collections.abc import Iterable + from pathlib import Path + + from pyk.utils import BugReport + + from .foundry import Foundry + + +@dataclass +class GlobalOptions: + foundry: Foundry + auto_abstract_gas: bool + bug_report: BugReport | None + kore_rpc_command: str | Iterable[str] | None + llvm_definition_dir: Path | None + 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 diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 2a685765e..6c6b22323 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -27,6 +27,7 @@ from pyk.utils import run_process, unique from .foundry import Foundry +from .options import GlobalOptions from .solc_to_k import Contract if TYPE_CHECKING: @@ -65,6 +66,7 @@ def foundry_prove( auto_abstract_gas: bool = False, port: int | None = None, run_constructor: bool = False, + fail_fast: 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}') @@ -109,28 +111,35 @@ def foundry_prove( for test in constructor_tests: test.method.update_digest(foundry.digest_file) + llvm_definition_dir = foundry.llvm_library if use_booster else None + + options = GlobalOptions( + foundry=foundry, + auto_abstract_gas=auto_abstract_gas, + 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, + simplify_init=simplify_init, + 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, + ) + 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, - simplify_init=simplify_init, - 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, + options=options, port=port, - run_constructor=run_constructor, ) if run_constructor: @@ -217,71 +226,49 @@ 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, - simplify_init: bool, - 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, + options: GlobalOptions, port: int | None, - run_constructor: bool = False, ) -> 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 with legacy_explore( - foundry.kevm, - kcfg_semantics=KEVMSemantics(auto_abstract_gas=auto_abstract_gas), + options.foundry.kevm, + 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=options.llvm_definition_dir, + smt_timeout=options.smt_timeout, + smt_retry_limit=options.smt_retry_limit, + trace_rewrites=options.trace_rewrites, start_server=start_server, port=port, ) as kcfg_explore: proof = method_to_apr_proof( - foundry, test, kcfg_explore, - simplify_init=simplify_init, - bmc_depth=bmc_depth, - run_constructor=run_constructor, + options=options, ) passed = kevm_prove( - foundry.kevm, + options.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 = [] @@ -358,15 +345,12 @@ def _contract_to_apr_proof( def method_to_apr_proof( - foundry: Foundry, test: FoundryTest, kcfg_explore: KCFGExplore, - simplify_init: bool = True, - bmc_depth: int | None = None, - run_constructor: bool = False, + options: GlobalOptions, ) -> APRProof | APRBMCProof: - if Proof.proof_data_exists(test.id, foundry.proofs_dir): - apr_proof = foundry.get_apr_proof(test.id) + if Proof.proof_data_exists(test.id, options.foundry.proofs_dir): + apr_proof = options.foundry.get_apr_proof(test.id) apr_proof.write_proof_data() return apr_proof @@ -375,20 +359,19 @@ def method_to_apr_proof( _LOGGER.info(f'Creating proof from constructor for test: {test.id}') elif test.method.signature != 'setUp()' and 'setUp' in test.contract.method_by_name: _LOGGER.info(f'Using setUp method for test: {test.id}') - setup_proof = _load_setup_proof(foundry, test.contract) - elif run_constructor: + setup_proof = _load_setup_proof(options.foundry, test.contract) + elif options.run_constructor: _LOGGER.info(f'Using constructor final state as initial state for test: {test.id}') - setup_proof = _load_constructor_proof(foundry, test.contract) + setup_proof = _load_constructor_proof(options.foundry, test.contract) kcfg, init_node_id, target_node_id = method_to_initialized_cfg( - foundry, test, kcfg_explore, + options=options, setup_proof=setup_proof, - simplify_init=simplify_init, ) - if bmc_depth is not None: + if options.bmc_depth is not None: apr_proof = APRBMCProof( test.id, kcfg, @@ -396,11 +379,11 @@ def method_to_apr_proof( init_node_id, target_node_id, {}, - bmc_depth, - proof_dir=foundry.proofs_dir, + options.bmc_depth, + proof_dir=options.foundry.proofs_dir, ) else: - apr_proof = APRProof(test.id, kcfg, [], init_node_id, target_node_id, {}, proof_dir=foundry.proofs_dir) + apr_proof = APRProof(test.id, kcfg, [], init_node_id, target_node_id, {}, proof_dir=options.foundry.proofs_dir) apr_proof.write_proof_data() return apr_proof @@ -442,16 +425,15 @@ def _load_constructor_proof(foundry: Foundry, contract: Contract) -> APRProof: def method_to_initialized_cfg( - foundry: Foundry, test: FoundryTest, kcfg_explore: KCFGExplore, + options: GlobalOptions, *, setup_proof: APRProof | None = None, - simplify_init: bool = True, ) -> tuple[KCFG, int, int]: _LOGGER.info(f'Initializing KCFG for test: {test.id}') - empty_config = foundry.kevm.definition.empty_config(GENERATED_TOP_CELL) + empty_config = options.foundry.kevm.definition.empty_config(GENERATED_TOP_CELL) kcfg, new_node_ids, init_node_id, target_node_id = _method_to_cfg( empty_config, test.contract, @@ -462,7 +444,7 @@ def method_to_initialized_cfg( for node_id in new_node_ids: _LOGGER.info(f'Expanding macros in node {node_id} for test: {test.name}') init_term = kcfg.node(node_id).cterm.kast - init_term = KDefinition__expand_macros(foundry.kevm.definition, init_term) + init_term = KDefinition__expand_macros(options.foundry.kevm.definition, init_term) init_cterm = CTerm.from_kast(init_term) _LOGGER.info(f'Computing definedness constraint for node {node_id} for test: {test.name}') init_cterm = kcfg_explore.cterm_assume_defined(init_cterm) @@ -470,11 +452,11 @@ def method_to_initialized_cfg( _LOGGER.info(f'Expanding macros in target state for test: {test.name}') target_term = kcfg.node(target_node_id).cterm.kast - target_term = KDefinition__expand_macros(foundry.kevm.definition, target_term) + target_term = KDefinition__expand_macros(options.foundry.kevm.definition, target_term) target_cterm = CTerm.from_kast(target_term) kcfg.replace_node(target_node_id, target_cterm) - if simplify_init: + if options.simplify_init: _LOGGER.info(f'Simplifying KCFG for test: {test.name}') kcfg_explore.simplify(kcfg, {}) From 95be5ac8105f87e1c03ec617b9ef7dc19ffcf9b9 Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 17 Oct 2023 23:13:50 +0000 Subject: [PATCH 02/12] Set Version: 0.1.28 --- 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 a2e1aa9d9..baec65a93 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.27 +0.1.28 diff --git a/pyproject.toml b/pyproject.toml index e8ce4e1e5..67cee4165 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.27" +version = "0.1.28" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 88965db67..7640e8d16 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.27' +VERSION: Final = '0.1.28' From 106fe0a1b1b49a57ee8dd4412f3fc8b81bbeb4fd Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 18 Oct 2023 20:28:18 +0000 Subject: [PATCH 03/12] Set Version: 0.1.30 --- 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 5ef49d2f0..013adb716 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.29 +0.1.30 diff --git a/pyproject.toml b/pyproject.toml index ecd0a402b..c3b1d838a 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.29" +version = "0.1.30" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index bcde77717..f3bac6ec6 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.29' +VERSION: Final = '0.1.30' From f820e203681345342cd9d202b6716309ed39f4e1 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 19 Oct 2023 14:39:47 -0500 Subject: [PATCH 04/12] Don't pass options on public function --- src/kontrol/prove.py | 50 +++++++++++++++++++++++++------------------- 1 file changed, 29 insertions(+), 21 deletions(-) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index fe92b77f4..53855c216 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -245,9 +245,12 @@ def init_and_run_proof(test: FoundryTest) -> tuple[bool, list[str] | None]: port=port, ) as kcfg_explore: proof = method_to_apr_proof( - test, - kcfg_explore, - options=options, + test=test, + foundry=options.foundry, + kcfg_explore=kcfg_explore, + simplify_init=options.simplify_init, + bmc_depth=options.bmc_depth, + run_constructor=options.run_constructor, ) passed = kevm_prove( @@ -281,11 +284,14 @@ def init_and_run_proof(test: FoundryTest) -> tuple[bool, list[str] | None]: def method_to_apr_proof( test: FoundryTest, + foundry: Foundry, kcfg_explore: KCFGExplore, - options: GlobalOptions, + simplify_init: bool = True, + bmc_depth: int | None = None, + run_constructor: bool = False, ) -> APRProof | APRBMCProof: - if Proof.proof_data_exists(test.id, options.foundry.proofs_dir): - apr_proof = options.foundry.get_apr_proof(test.id) + if Proof.proof_data_exists(test.id, foundry.proofs_dir): + apr_proof = foundry.get_apr_proof(test.id) apr_proof.write_proof_data() return apr_proof @@ -294,19 +300,20 @@ def method_to_apr_proof( _LOGGER.info(f'Creating proof from constructor for test: {test.id}') elif test.method.signature != 'setUp()' and 'setUp' in test.contract.method_by_name: _LOGGER.info(f'Using setUp method for test: {test.id}') - setup_proof = _load_setup_proof(options.foundry, test.contract) - elif options.run_constructor: + setup_proof = _load_setup_proof(foundry, test.contract) + elif run_constructor: _LOGGER.info(f'Using constructor final state as initial state for test: {test.id}') - setup_proof = _load_constructor_proof(options.foundry, test.contract) + setup_proof = _load_constructor_proof(foundry, test.contract) kcfg, init_node_id, target_node_id = method_to_initialized_cfg( - test, - kcfg_explore, - options=options, + foundry=foundry, + test=test, + kcfg_explore=kcfg_explore, setup_proof=setup_proof, + simplify_init=simplify_init, ) - if options.bmc_depth is not None: + if bmc_depth is not None: apr_proof = APRBMCProof( test.id, kcfg, @@ -314,11 +321,11 @@ def method_to_apr_proof( init_node_id, target_node_id, {}, - options.bmc_depth, - proof_dir=options.foundry.proofs_dir, + bmc_depth, + proof_dir=foundry.proofs_dir, ) else: - apr_proof = APRProof(test.id, kcfg, [], init_node_id, target_node_id, {}, proof_dir=options.foundry.proofs_dir) + apr_proof = APRProof(test.id, kcfg, [], init_node_id, target_node_id, {}, proof_dir=foundry.proofs_dir) apr_proof.write_proof_data() return apr_proof @@ -339,15 +346,16 @@ def _load_constructor_proof(foundry: Foundry, contract: Contract) -> APRProof: def method_to_initialized_cfg( + foundry: Foundry, test: FoundryTest, kcfg_explore: KCFGExplore, - options: GlobalOptions, *, setup_proof: APRProof | None = None, + simplify_init: bool = True, ) -> tuple[KCFG, int, int]: _LOGGER.info(f'Initializing KCFG for test: {test.id}') - empty_config = options.foundry.kevm.definition.empty_config(GENERATED_TOP_CELL) + empty_config = foundry.kevm.definition.empty_config(GENERATED_TOP_CELL) kcfg, new_node_ids, init_node_id, target_node_id = _method_to_cfg( empty_config, test.contract, @@ -358,7 +366,7 @@ def method_to_initialized_cfg( for node_id in new_node_ids: _LOGGER.info(f'Expanding macros in node {node_id} for test: {test.name}') init_term = kcfg.node(node_id).cterm.kast - init_term = KDefinition__expand_macros(options.foundry.kevm.definition, init_term) + init_term = KDefinition__expand_macros(foundry.kevm.definition, init_term) init_cterm = CTerm.from_kast(init_term) _LOGGER.info(f'Computing definedness constraint for node {node_id} for test: {test.name}') init_cterm = kcfg_explore.cterm_assume_defined(init_cterm) @@ -366,11 +374,11 @@ def method_to_initialized_cfg( _LOGGER.info(f'Expanding macros in target state for test: {test.name}') target_term = kcfg.node(target_node_id).cterm.kast - target_term = KDefinition__expand_macros(options.foundry.kevm.definition, target_term) + target_term = KDefinition__expand_macros(foundry.kevm.definition, target_term) target_cterm = CTerm.from_kast(target_term) kcfg.replace_node(target_node_id, target_cterm) - if options.simplify_init: + if simplify_init: _LOGGER.info(f'Simplifying KCFG for test: {test.name}') kcfg_explore.simplify(kcfg, {}) From 434b1b9a869024b50b172adb988245f3977c8064 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 19 Oct 2023 16:12:16 -0500 Subject: [PATCH 05/12] Move options construction to exec_prove, add constructor with default args --- src/kontrol/__main__.py | 34 ++++--- src/kontrol/options.py | 56 +++++++++-- src/kontrol/prove.py | 93 +++++------------- src/tests/integration/test_foundry_prove.py | 101 ++++++++++++-------- src/tests/profiling/test_foundry_prove.py | 13 ++- 5 files changed, 164 insertions(+), 133 deletions(-) diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index 41d98f4da..c259871ce 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 GlobalOptions from .prove import foundry_prove from .solc_to_k import solc_compile, solc_to_k @@ -177,27 +178,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, - reinit=reinit, - tests=tests, - workers=workers, - simplify_init=simplify_init, - break_every_step=break_every_step, - break_on_jumpi=break_on_jumpi, - break_on_calls=break_on_calls, - bmc_depth=bmc_depth, + options = GlobalOptions( + auto_abstract_gas=auto_abstract_gas, 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, + simplify_init=simplify_init, + 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(): diff --git a/src/kontrol/options.py b/src/kontrol/options.py index 5cb3caf43..f6f02d246 100644 --- a/src/kontrol/options.py +++ b/src/kontrol/options.py @@ -5,20 +5,16 @@ if TYPE_CHECKING: from collections.abc import Iterable - from pathlib import Path from pyk.utils import BugReport - from .foundry import Foundry - -@dataclass +@dataclass(frozen=True) class GlobalOptions: - foundry: Foundry auto_abstract_gas: bool bug_report: BugReport | None + use_booster: bool kore_rpc_command: str | Iterable[str] | None - llvm_definition_dir: Path | None smt_timeout: int | None smt_retry_limit: int | None trace_rewrites: bool @@ -33,3 +29,51 @@ class GlobalOptions: 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, + simplify_init: bool = True, + 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',) + 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, 'simplify_init', simplify_init) + 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 53855c216..5949072bb 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -26,7 +26,6 @@ from pyk.utils import run_process, unique from .foundry import Foundry -from .options import GlobalOptions from .solc_to_k import Contract if TYPE_CHECKING: @@ -36,7 +35,8 @@ from pyk.kast.inner import KInner from pyk.kcfg import KCFGExplore - from pyk.utils import BugReport + + from .options import GlobalOptions _LOGGER: Final = logging.getLogger(__name__) @@ -44,35 +44,17 @@ def foundry_prove( foundry_root: Path, - max_depth: int = 1000, - max_iterations: int | None = None, - reinit: bool = False, + options: GlobalOptions, tests: Iterable[tuple[str, int | None]] = (), - workers: int = 1, - simplify_init: bool = True, - 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, - fail_fast: 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: @@ -80,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}') @@ -110,38 +89,16 @@ def foundry_prove( for test in constructor_tests: test.method.update_digest(foundry.digest_file) - llvm_definition_dir = foundry.llvm_library if use_booster else None - - options = GlobalOptions( - foundry=foundry, - auto_abstract_gas=auto_abstract_gas, - 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, - simplify_init=simplify_init, - 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, - ) + # llvm_definition_dir = foundry.llvm_library if options.use_booster else None def run_prover(test_suite: list[FoundryTest]) -> dict[tuple[str, int], tuple[bool, list[str] | None]]: return _run_cfg_group( - test_suite, + tests=test_suite, + foundry=foundry, options=options, - port=port, ) - 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] @@ -225,28 +182,28 @@ def collect_constructors(foundry: Foundry, contracts: Iterable[Contract] = (), * def _run_cfg_group( tests: list[FoundryTest], + foundry: Foundry, options: GlobalOptions, - port: int | None, ) -> dict[tuple[str, int], tuple[bool, list[str] | None]]: def init_and_run_proof(test: FoundryTest) -> tuple[bool, list[str] | None]: - start_server = port is None + start_server = options.port is None with legacy_explore( - options.foundry.kevm, + foundry.kevm, kcfg_semantics=KEVMSemantics(auto_abstract_gas=options.auto_abstract_gas), id=test.id, bug_report=options.bug_report, kore_rpc_command=options.kore_rpc_command, - llvm_definition_dir=options.llvm_definition_dir, + 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( test=test, - foundry=options.foundry, + foundry=foundry, kcfg_explore=kcfg_explore, simplify_init=options.simplify_init, bmc_depth=options.bmc_depth, @@ -254,7 +211,7 @@ def init_and_run_proof(test: FoundryTest) -> tuple[bool, list[str] | None]: ) passed = kevm_prove( - options.foundry.kevm, + foundry.kevm, proof, kcfg_explore, max_depth=options.max_depth, diff --git a/src/tests/integration/test_foundry_prove.py b/src/tests/integration/test_foundry_prove.py index a9a12db99..d8c29817c 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 GlobalOptions from kontrol.prove import foundry_prove from .utils import TEST_DATA_DIR @@ -129,10 +130,12 @@ def test_foundry_prove( prove_res = foundry_prove( foundry_root, tests=[(test_id, None)], - simplify_init=False, - counterexample_info=True, - port=server.port, - bug_report=bug_report, + options=GlobalOptions( + simplify_init=False, + counterexample_info=True, + bug_report=bug_report, + port=server.port, + ), ) # Then @@ -170,9 +173,11 @@ def test_foundry_fail( prove_res = foundry_prove( foundry_root, tests=[(test_id, None)], - simplify_init=False, - counterexample_info=True, - port=server.port, + options=GlobalOptions( + simplify_init=False, + counterexample_info=True, + port=server.port, + ), ) # Then @@ -212,10 +217,12 @@ 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, - simplify_init=False, - port=server.port, - bug_report=bug_report, + options=GlobalOptions( + bmc_depth=3, + simplify_init=False, + port=server.port, + bug_report=bug_report, + ), ) # Then @@ -228,9 +235,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=GlobalOptions( + max_iterations=2, + port=server.port, + bug_report=bug_report, + ), ) check_pending(foundry_root, test, [4, 5]) @@ -247,8 +256,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=GlobalOptions( + port=server.port, + bug_report=bug_report, + ), ) assert_pass(test, prove_res) @@ -272,10 +283,12 @@ def test_foundry_auto_abstraction( foundry_prove( foundry_root, tests=[(test_id, None)], - auto_abstract_gas=True, - bug_report=bug_report, - port=server.port, - simplify_init=False, + options=GlobalOptions( + auto_abstract_gas=True, + bug_report=bug_report, + port=server.port, + simplify_init=False, + ), ) if use_booster: @@ -307,8 +320,10 @@ def test_foundry_remove_node( prove_res = foundry_prove( foundry_root, tests=[(test, None)], - port=server.port, - bug_report=bug_report, + options=GlobalOptions( + port=server.port, + bug_report=bug_report, + ), ) assert_pass(test, prove_res) @@ -325,8 +340,10 @@ def test_foundry_remove_node( prove_res = foundry_prove( foundry_root, tests=[(test, None)], - port=server.port, - bug_report=bug_report, + options=GlobalOptions( + port=server.port, + bug_report=bug_report, + ), ) assert_pass(test, prove_res) @@ -384,11 +401,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=GlobalOptions( + auto_abstract_gas=True, + max_iterations=4, + reinit=True, + port=server.port, + bug_report=bug_report, + ), ) id = id_for_test(test, prove_res) @@ -398,11 +417,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=GlobalOptions( + auto_abstract_gas=True, + max_iterations=6, + reinit=False, + port=server.port, + bug_report=bug_report, + ), ) assert_fail(test, prove_res) @@ -416,11 +437,13 @@ def test_foundry_init_code(test: str, foundry_root: Path, use_booster: bool) -> prove_res = foundry_prove( foundry_root, tests=[(test, None)], - simplify_init=False, - smt_timeout=300, - smt_retry_limit=10, - use_booster=use_booster, - run_constructor=True, + options=GlobalOptions( + simplify_init=False, + smt_timeout=300, + smt_retry_limit=10, + use_booster=use_booster, + run_constructor=True, + ), ) # Then diff --git a/src/tests/profiling/test_foundry_prove.py b/src/tests/profiling/test_foundry_prove.py index 335d92bfc..bbafedcfc 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 GlobalOptions from kontrol.prove import foundry_prove from .utils import TEST_DATA_DIR @@ -36,11 +37,13 @@ def test_foundy_prove(profile: Profiler, use_booster: bool, tmp_path: Path) -> N foundry_prove( foundry_root, tests=[('AssertTest.test_revert_branch', None)], - simplify_init=False, - smt_timeout=300, - smt_retry_limit=10, - counterexample_info=True, - use_booster=use_booster, + options=GlobalOptions( + simplify_init=False, + smt_timeout=300, + smt_retry_limit=10, + counterexample_info=True, + use_booster=use_booster, + ), ) From e0abfdbdd88d894828bb81cc87e98c33ccd74277 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 19 Oct 2023 16:12:53 -0500 Subject: [PATCH 06/12] Fix typo in help message --- src/kontrol/__main__.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index c259871ce..df4cb14f4 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -538,7 +538,7 @@ def _parse_test_version_tuple(value: str) -> tuple[str, int | None]: dest='fail_fast', default=False, action='store_true', - help='Stop execution on other branches if failing node is detected.', + help='Stop execution on other branches if a failing node is detected.', ) show_args = command_parser.add_parser( From 515c080f2d755b3c181ec230c8ce7869fb4d0914 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 19 Oct 2023 16:15:23 -0500 Subject: [PATCH 07/12] Rename class to ProveOptions --- src/kontrol/__main__.py | 4 ++-- src/kontrol/options.py | 2 +- src/kontrol/prove.py | 6 +++--- src/tests/integration/test_foundry_prove.py | 24 ++++++++++----------- src/tests/profiling/test_foundry_prove.py | 4 ++-- 5 files changed, 20 insertions(+), 20 deletions(-) diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index df4cb14f4..0382f2e92 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -28,7 +28,7 @@ foundry_to_dot, ) from .kompile import foundry_kompile -from .options import GlobalOptions +from .options import ProveOptions from .prove import foundry_prove from .solc_to_k import solc_compile, solc_to_k @@ -178,7 +178,7 @@ def exec_prove( if isinstance(kore_rpc_command, str): kore_rpc_command = kore_rpc_command.split() - options = GlobalOptions( + options = ProveOptions( auto_abstract_gas=auto_abstract_gas, bug_report=bug_report, kore_rpc_command=kore_rpc_command, diff --git a/src/kontrol/options.py b/src/kontrol/options.py index f6f02d246..d8f0428f8 100644 --- a/src/kontrol/options.py +++ b/src/kontrol/options.py @@ -10,7 +10,7 @@ @dataclass(frozen=True) -class GlobalOptions: +class ProveOptions: auto_abstract_gas: bool bug_report: BugReport | None use_booster: bool diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 5949072bb..6a85debba 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -36,7 +36,7 @@ from pyk.kast.inner import KInner from pyk.kcfg import KCFGExplore - from .options import GlobalOptions + from .options import ProveOptions _LOGGER: Final = logging.getLogger(__name__) @@ -44,7 +44,7 @@ def foundry_prove( foundry_root: Path, - options: GlobalOptions, + options: ProveOptions, tests: Iterable[tuple[str, int | None]] = (), ) -> dict[tuple[str, int], tuple[bool, list[str] | None]]: if options.workers <= 0: @@ -183,7 +183,7 @@ def collect_constructors(foundry: Foundry, contracts: Iterable[Contract] = (), * def _run_cfg_group( tests: list[FoundryTest], foundry: Foundry, - options: GlobalOptions, + options: ProveOptions, ) -> dict[tuple[str, int], tuple[bool, list[str] | None]]: def init_and_run_proof(test: FoundryTest) -> tuple[bool, list[str] | None]: start_server = options.port is None diff --git a/src/tests/integration/test_foundry_prove.py b/src/tests/integration/test_foundry_prove.py index d8c29817c..96f6a394f 100644 --- a/src/tests/integration/test_foundry_prove.py +++ b/src/tests/integration/test_foundry_prove.py @@ -12,7 +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 GlobalOptions +from kontrol.options import ProveOptions from kontrol.prove import foundry_prove from .utils import TEST_DATA_DIR @@ -130,7 +130,7 @@ def test_foundry_prove( prove_res = foundry_prove( foundry_root, tests=[(test_id, None)], - options=GlobalOptions( + options=ProveOptions( simplify_init=False, counterexample_info=True, bug_report=bug_report, @@ -173,7 +173,7 @@ def test_foundry_fail( prove_res = foundry_prove( foundry_root, tests=[(test_id, None)], - options=GlobalOptions( + options=ProveOptions( simplify_init=False, counterexample_info=True, port=server.port, @@ -217,7 +217,7 @@ def test_foundry_bmc(test_id: str, foundry_root: Path, bug_report: BugReport | N prove_res = foundry_prove( foundry_root, tests=[(test_id, None)], - options=GlobalOptions( + options=ProveOptions( bmc_depth=3, simplify_init=False, port=server.port, @@ -235,7 +235,7 @@ def test_foundry_merge_nodes(foundry_root: Path, bug_report: BugReport | None, s foundry_prove( foundry_root, tests=[(test, None)], - options=GlobalOptions( + options=ProveOptions( max_iterations=2, port=server.port, bug_report=bug_report, @@ -256,7 +256,7 @@ def test_foundry_merge_nodes(foundry_root: Path, bug_report: BugReport | None, s prove_res = foundry_prove( foundry_root, tests=[(test, None)], - options=GlobalOptions( + options=ProveOptions( port=server.port, bug_report=bug_report, ), @@ -283,7 +283,7 @@ def test_foundry_auto_abstraction( foundry_prove( foundry_root, tests=[(test_id, None)], - options=GlobalOptions( + options=ProveOptions( auto_abstract_gas=True, bug_report=bug_report, port=server.port, @@ -320,7 +320,7 @@ def test_foundry_remove_node( prove_res = foundry_prove( foundry_root, tests=[(test, None)], - options=GlobalOptions( + options=ProveOptions( port=server.port, bug_report=bug_report, ), @@ -340,7 +340,7 @@ def test_foundry_remove_node( prove_res = foundry_prove( foundry_root, tests=[(test, None)], - options=GlobalOptions( + options=ProveOptions( port=server.port, bug_report=bug_report, ), @@ -401,7 +401,7 @@ def test_foundry_resume_proof( prove_res = foundry_prove( foundry_root, tests=[(test, None)], - options=GlobalOptions( + options=ProveOptions( auto_abstract_gas=True, max_iterations=4, reinit=True, @@ -417,7 +417,7 @@ def test_foundry_resume_proof( prove_res = foundry_prove( foundry_root, tests=[(test, id)], - options=GlobalOptions( + options=ProveOptions( auto_abstract_gas=True, max_iterations=6, reinit=False, @@ -437,7 +437,7 @@ def test_foundry_init_code(test: str, foundry_root: Path, use_booster: bool) -> prove_res = foundry_prove( foundry_root, tests=[(test, None)], - options=GlobalOptions( + options=ProveOptions( simplify_init=False, smt_timeout=300, smt_retry_limit=10, diff --git a/src/tests/profiling/test_foundry_prove.py b/src/tests/profiling/test_foundry_prove.py index bbafedcfc..22b6628c1 100644 --- a/src/tests/profiling/test_foundry_prove.py +++ b/src/tests/profiling/test_foundry_prove.py @@ -7,7 +7,7 @@ from pyk.utils import run_process from kontrol.kompile import foundry_kompile -from kontrol.options import GlobalOptions +from kontrol.options import ProveOptions from kontrol.prove import foundry_prove from .utils import TEST_DATA_DIR @@ -37,7 +37,7 @@ def test_foundy_prove(profile: Profiler, use_booster: bool, tmp_path: Path) -> N foundry_prove( foundry_root, tests=[('AssertTest.test_revert_branch', None)], - options=GlobalOptions( + options=ProveOptions( simplify_init=False, smt_timeout=300, smt_retry_limit=10, From 351fdb9977f5305a5ec2580261dfbdb721a0b6f4 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 19 Oct 2023 21:36:24 +0000 Subject: [PATCH 08/12] Set Version: 0.1.33 --- 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 28d007539..50140e353 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.32 +0.1.33 diff --git a/pyproject.toml b/pyproject.toml index 2e8c90975..9216c12ed 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.32" +version = "0.1.33" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 29d57dae6..7aa6780b4 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.32' +VERSION: Final = '0.1.33' From bb4509729f07f0ef7edcd878f2be1213240a385d Mon Sep 17 00:00:00 2001 From: Noah Watson <107630091+nwatson22@users.noreply.github.com> Date: Thu, 19 Oct 2023 16:55:38 -0500 Subject: [PATCH 09/12] Update src/kontrol/prove.py --- src/kontrol/prove.py | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 6c099eee7..10ec0f4ca 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -89,8 +89,6 @@ def foundry_prove( for test in constructor_tests: test.method.update_digest(foundry.digest_file) - # llvm_definition_dir = foundry.llvm_library if options.use_booster else None - def run_prover(test_suite: list[FoundryTest]) -> dict[tuple[str, int], tuple[bool, list[str] | None]]: return _run_cfg_group( tests=test_suite, From 08388a3b2998d1d55456505c1a4e5eae3dc9b5fb Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Fri, 20 Oct 2023 13:01:16 -0500 Subject: [PATCH 10/12] Address comments --- src/kontrol/options.py | 6 +++++- src/kontrol/prove.py | 4 ++-- src/tests/integration/test_foundry_prove.py | 11 +++++++++-- src/tests/profiling/test_foundry_prove.py | 4 +++- 4 files changed, 19 insertions(+), 6 deletions(-) diff --git a/src/kontrol/options.py b/src/kontrol/options.py index 11a97d372..438f74c89 100644 --- a/src/kontrol/options.py +++ b/src/kontrol/options.py @@ -14,7 +14,7 @@ class ProveOptions: auto_abstract_gas: bool bug_report: BugReport | None use_booster: bool - kore_rpc_command: str | Iterable[str] | None + kore_rpc_command: tuple[str, ...] smt_timeout: int | None smt_retry_limit: int | None trace_rewrites: bool @@ -56,6 +56,10 @@ def __init__( ) -> 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) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 10ec0f4ca..16c5578fb 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -258,7 +258,7 @@ def method_to_apr_proof( _LOGGER.info(f'Using constructor final state as initial state for test: {test.id}') setup_proof = _load_constructor_proof(foundry, test.contract) - kcfg, init_node_id, target_node_id = method_to_initialized_cfg( + kcfg, init_node_id, target_node_id = _method_to_initialized_cfg( foundry=foundry, test=test, kcfg_explore=kcfg_explore, @@ -297,7 +297,7 @@ def _load_constructor_proof(foundry: Foundry, contract: Contract) -> APRProof: return apr_proof -def method_to_initialized_cfg( +def _method_to_initialized_cfg( foundry: Foundry, test: FoundryTest, kcfg_explore: KCFGExplore, diff --git a/src/tests/integration/test_foundry_prove.py b/src/tests/integration/test_foundry_prove.py index e20b0a37d..4f755dc9b 100644 --- a/src/tests/integration/test_foundry_prove.py +++ b/src/tests/integration/test_foundry_prove.py @@ -166,7 +166,12 @@ 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( @@ -174,6 +179,7 @@ def test_foundry_fail( tests=[(test_id, None)], options=ProveOptions( counterexample_info=True, + bug_report=bug_report, port=server.port, ), ) @@ -428,7 +434,7 @@ 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, @@ -438,6 +444,7 @@ def test_foundry_init_code(test: str, foundry_root: Path, use_booster: bool) -> smt_retry_limit=10, use_booster=use_booster, run_constructor=True, + bug_report=bug_report, ), ) diff --git a/src/tests/profiling/test_foundry_prove.py b/src/tests/profiling/test_foundry_prove.py index 7585f0ce3..9b528b6f1 100644 --- a/src/tests/profiling/test_foundry_prove.py +++ b/src/tests/profiling/test_foundry_prove.py @@ -17,6 +17,7 @@ from typing import Final from pyk.testing import Profiler + from pyk.utils import BugReport sys.setrecursionlimit(10**7) @@ -25,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) @@ -41,6 +42,7 @@ def test_foundy_prove(profile: Profiler, use_booster: bool, tmp_path: Path) -> N smt_timeout=300, smt_retry_limit=10, counterexample_info=True, + bug_report=bug_report, use_booster=use_booster, ), ) From 24311215242e84f49c11c193d2fe3a3768c44061 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 20 Oct 2023 18:01:33 +0000 Subject: [PATCH 11/12] Set Version: 0.1.34 --- 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 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 9216c12ed..41dd71160 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' From fc562a0af31597291c8519b858ed30144012323d Mon Sep 17 00:00:00 2001 From: Noah Watson <107630091+nwatson22@users.noreply.github.com> Date: Fri, 20 Oct 2023 14:55:02 -0500 Subject: [PATCH 12/12] Update src/kontrol/options.py MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Tamás Tóth --- src/kontrol/options.py | 1 + 1 file changed, 1 insertion(+) diff --git a/src/kontrol/options.py b/src/kontrol/options.py index 438f74c89..de80f9db7 100644 --- a/src/kontrol/options.py +++ b/src/kontrol/options.py @@ -34,6 +34,7 @@ class ProveOptions: def __init__( self, + *, auto_abstract_gas: bool = False, bug_report: BugReport | None = None, use_booster: bool = True,