From 1971cb58c0466113c3bf34a3daf65bba73f4c117 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Thu, 24 Aug 2023 21:29:20 +0000 Subject: [PATCH 01/10] kevm-pyk/{cli,__main__,foundry}: use upstreamed KCLIArgs.bug_report_args --- kevm-pyk/src/kevm_pyk/__main__.py | 21 ++++++++++-------- kevm-pyk/src/kevm_pyk/cli.py | 17 --------------- kevm-pyk/src/kontrol/__main__.py | 20 ++++++++--------- kevm-pyk/src/kontrol/foundry.py | 36 ++++++++++++++----------------- 4 files changed, 38 insertions(+), 56 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index f3e8b6ba12..3ae880fe48 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -20,7 +20,7 @@ from pyk.proof.equality import EqualityProof from pyk.proof.show import APRProofShow from pyk.proof.tui import APRProofViewer -from pyk.utils import BugReport, single +from pyk.utils import single from .cli import KEVMCLIArgs, node_id_like from .config import INCLUDE_DIR, KEVM_LIB @@ -37,6 +37,7 @@ from pyk.kast.outer import KClaim from pyk.kcfg.kcfg import NodeIdLike from pyk.proof.proof import Proof + from pyk.utils import BugReport T = TypeVar('T') @@ -127,7 +128,7 @@ def exec_prove_legacy( spec_file: Path, definition_dir: Path | None = None, includes: Iterable[str] = (), - bug_report: bool = False, + bug_report_legacy: bool = False, save_directory: Path | None = None, spec_module: str | None = None, claim_labels: Iterable[str] | None = None, @@ -153,7 +154,7 @@ def exec_prove_legacy( final_state = kevm.prove_legacy( spec_file=spec_file, includes=include_dirs, - bug_report=bug_report, + bug_report=bug_report_legacy, spec_module=spec_module, claim_labels=claim_labels, exclude_claim_labels=exclude_claim_labels, @@ -173,7 +174,7 @@ def exec_prove( spec_file: Path, includes: Iterable[str], definition_dir: Path | None = None, - bug_report: bool = False, + bug_report: BugReport | None = None, save_directory: Path | None = None, spec_module: str | None = None, claim_labels: Iterable[str] | None = None, @@ -206,8 +207,7 @@ def exec_prove( if smt_retry_limit is None: smt_retry_limit = 10 - br = BugReport(spec_file.with_suffix('.bug_report')) if bug_report else None - kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=br) + kevm = KEVM(definition_dir, use_directory=save_directory, bug_report=bug_report) include_dirs = [Path(include) for include in includes] include_dirs += [INCLUDE_DIR] @@ -241,7 +241,7 @@ def _init_and_run_proof(claim: KClaim) -> tuple[bool, list[str] | None]: kevm, kcfg_semantics=KEVMSemantics(auto_abstract_gas=auto_abstract_gas), id=claim.label, - bug_report=br, + bug_report=bug_report, kore_rpc_command=kore_rpc_command, smt_timeout=smt_timeout, smt_retry_limit=smt_retry_limit, @@ -573,7 +573,7 @@ def parse(s: str) -> list[T]: kevm_cli_args.parallel_args, kevm_cli_args.k_args, kevm_cli_args.kprove_args, - kevm_cli_args.rpc_args, + kevm_cli_args.bug_report_args, kevm_cli_args.smt_args, kevm_cli_args.explore_args, kevm_cli_args.spec_args, @@ -605,7 +605,7 @@ def parse(s: str) -> list[T]: ) prune_proof_args.add_argument('node', type=node_id_like, help='Node to remove CFG subgraph from.') - command_parser.add_parser( + prove_legacy_args = command_parser.add_parser( 'prove-legacy', help='Run KEVM proof using the legacy kprove binary.', parents=[ @@ -615,6 +615,9 @@ def parse(s: str) -> list[T]: kevm_cli_args.kprove_legacy_args, ], ) + prove_legacy_args.add_argument( + '--bug-report-legacy', default=False, action='store_true', help='Generate a legacy bug report.' + ) command_parser.add_parser( 'view-kcfg', diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 50bfa43759..678161bd59 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -162,23 +162,6 @@ def foundry_args(self) -> ArgumentParser: ) return args - @cached_property - def rpc_args(self) -> ArgumentParser: - args = ArgumentParser(add_help=False) - args.add_argument( - '--bug-report', - default=False, - action='store_true', - help='Generate a haskell-backend bug report for the execution.', - ) - args.add_argument( - '--trace-rewrites', - default=False, - action='store_true', - help='Log traces of all simplification and rewrite rule applications.', - ) - return args - @cached_property def explore_args(self) -> ArgumentParser: args = ArgumentParser(add_help=False) diff --git a/kevm-pyk/src/kontrol/__main__.py b/kevm-pyk/src/kontrol/__main__.py index 5e7ae6f32f..336f3cfdf2 100644 --- a/kevm-pyk/src/kontrol/__main__.py +++ b/kevm-pyk/src/kontrol/__main__.py @@ -40,6 +40,7 @@ from pyk.cterm import CTerm from pyk.kcfg.kcfg import NodeIdLike from pyk.kcfg.tui import KCFGElem + from pyk.utils import BugReport T = TypeVar('T') @@ -153,7 +154,7 @@ def exec_foundry_prove( break_on_jumpi: bool = False, break_on_calls: bool = True, bmc_depth: int | None = None, - bug_report: bool = False, + bug_report: BugReport | None = None, kore_rpc_command: str | Iterable[str] | None = None, use_booster: bool = False, smt_timeout: int | None = None, @@ -283,7 +284,7 @@ def exec_foundry_simplify_node( replace: bool = False, minimize: bool = True, sort_collections: bool = False, - bug_report: bool = False, + bug_report: BugReport | None = None, smt_timeout: int | None = None, smt_retry_limit: int | None = None, trace_rewrites: bool = False, @@ -315,7 +316,7 @@ def exec_foundry_step_node( node: NodeIdLike, repeat: int = 1, depth: int = 1, - bug_report: bool = False, + bug_report: BugReport | None = None, smt_timeout: int | None = None, smt_retry_limit: int | None = None, trace_rewrites: bool = False, @@ -343,7 +344,6 @@ def exec_foundry_merge_nodes( foundry_root: Path, test: str, nodes: Iterable[NodeIdLike], - bug_report: bool = False, **kwargs: Any, ) -> None: foundry_merge_nodes(foundry_root=foundry_root, node_ids=nodes, test=test) @@ -355,7 +355,7 @@ def exec_foundry_section_edge( edge: tuple[str, str], sections: int = 2, replace: bool = False, - bug_report: bool = False, + bug_report: BugReport | None = None, smt_timeout: int | None = None, smt_retry_limit: int | None = None, trace_rewrites: bool = False, @@ -460,7 +460,7 @@ def parse(s: str) -> list[T]: kevm_cli_args.k_args, kevm_cli_args.kprove_args, kevm_cli_args.smt_args, - kevm_cli_args.rpc_args, + kevm_cli_args.bug_report_args, kevm_cli_args.explore_args, kevm_cli_args.foundry_args, ], @@ -556,7 +556,7 @@ def parse(s: str) -> list[T]: parents=[ kevm_cli_args.logging_args, kevm_cli_args.smt_args, - kevm_cli_args.rpc_args, + kevm_cli_args.bug_report_args, kevm_cli_args.display_args, kevm_cli_args.foundry_args, ], @@ -572,7 +572,7 @@ def parse(s: str) -> list[T]: help='Step from a given node, adding it to the CFG.', parents=[ kevm_cli_args.logging_args, - kevm_cli_args.rpc_args, + kevm_cli_args.bug_report_args, kevm_cli_args.smt_args, kevm_cli_args.foundry_args, ], @@ -608,7 +608,7 @@ def parse(s: str) -> list[T]: help='Given an edge in the graph, cut it into sections to get intermediate nodes.', parents=[ kevm_cli_args.logging_args, - kevm_cli_args.rpc_args, + kevm_cli_args.bug_report_args, kevm_cli_args.smt_args, kevm_cli_args.foundry_args, ], @@ -624,7 +624,7 @@ def parse(s: str) -> list[T]: help='Display a model for a given node.', parents=[ kevm_cli_args.logging_args, - kevm_cli_args.rpc_args, + kevm_cli_args.bug_report_args, kevm_cli_args.smt_args, kevm_cli_args.foundry_args, ], diff --git a/kevm-pyk/src/kontrol/foundry.py b/kevm-pyk/src/kontrol/foundry.py index ac0d2dbbb0..61839828ac 100644 --- a/kevm-pyk/src/kontrol/foundry.py +++ b/kevm-pyk/src/kontrol/foundry.py @@ -25,7 +25,7 @@ from pyk.proof.proof import Proof from pyk.proof.reachability import APRBMCProof, APRProof from pyk.proof.show import APRBMCProofNodePrinter, APRProofNodePrinter, APRProofShow -from pyk.utils import BugReport, ensure_dir_path, hash_str, run_process, single, unique +from pyk.utils import ensure_dir_path, hash_str, run_process, single, unique from kevm_pyk.kevm import KEVM, KEVMNodePrinter, KEVMSemantics from kevm_pyk.utils import ( @@ -50,6 +50,7 @@ from pyk.kcfg.kcfg import NodeIdLike from pyk.kcfg.tui import KCFGElem from pyk.proof.show import NodePrinter + from pyk.utils import BugReport _LOGGER: Final = logging.getLogger(__name__) @@ -496,7 +497,7 @@ def foundry_prove( break_on_jumpi: bool = False, break_on_calls: bool = True, bmc_depth: int | None = None, - bug_report: bool = False, + bug_report: BugReport | None = None, kore_rpc_command: str | Iterable[str] | None = None, use_booster: bool = False, smt_timeout: int | None = None, @@ -511,8 +512,7 @@ def foundry_prove( 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}') - br = BugReport(foundry_root / 'bug_report') if bug_report else None - foundry = Foundry(foundry_root, bug_report=br) + foundry = Foundry(foundry_root, bug_report=bug_report) save_directory = foundry.out / 'apr_proofs' save_directory.mkdir(exist_ok=True) @@ -594,7 +594,7 @@ def _init_and_run_proof(_init_problem: tuple[str, str]) -> tuple[bool, list[str] foundry.kevm, kcfg_semantics=KEVMSemantics(auto_abstract_gas=auto_abstract_gas), id=proof_id, - bug_report=br, + bug_report=bug_report, kore_rpc_command=kore_rpc_command, llvm_definition_dir=llvm_definition_dir, smt_timeout=smt_timeout, @@ -771,20 +771,19 @@ def foundry_simplify_node( replace: bool = False, minimize: bool = True, sort_collections: bool = False, - bug_report: bool = False, + bug_report: BugReport | None = None, smt_timeout: int | None = None, smt_retry_limit: int | None = None, trace_rewrites: bool = False, ) -> str: - br = BugReport(Path(f'{test}.bug_report')) if bug_report else None - foundry = Foundry(foundry_root, bug_report=br) + foundry = Foundry(foundry_root, bug_report=bug_report) apr_proof = foundry.get_apr_proof(test) cterm = apr_proof.kcfg.node(node).cterm with legacy_explore( foundry.kevm, kcfg_semantics=KEVMSemantics(), id=apr_proof.id, - bug_report=br, + bug_report=bug_report, smt_timeout=smt_timeout, smt_retry_limit=smt_retry_limit, trace_rewrites=trace_rewrites, @@ -801,7 +800,7 @@ def foundry_merge_nodes( foundry_root: Path, test: str, node_ids: Iterable[NodeIdLike], - bug_report: bool = False, + bug_report: BugReport | None = None, include_disjunct: bool = False, ) -> None: def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool: @@ -814,8 +813,7 @@ def check_cells_equal(cell: str, nodes: Iterable[KCFG.Node]) -> bool: return False return True - br = BugReport(Path(f'{test}.bug_report')) if bug_report else None - foundry = Foundry(foundry_root, bug_report=br) + foundry = Foundry(foundry_root, bug_report=bug_report) proof = foundry.get_apr_proof(test) if not isinstance(proof, APRProof): @@ -849,7 +847,7 @@ def foundry_step_node( node: NodeIdLike, repeat: int = 1, depth: int = 1, - bug_report: bool = False, + bug_report: BugReport | None = None, smt_timeout: int | None = None, smt_retry_limit: int | None = None, trace_rewrites: bool = False, @@ -859,15 +857,14 @@ def foundry_step_node( if depth < 1: raise ValueError(f'Expected positive value for --depth, got: {depth}') - br = BugReport(Path(f'{test}.bug_report')) if bug_report else None - foundry = Foundry(foundry_root, bug_report=br) + foundry = Foundry(foundry_root, bug_report=bug_report) apr_proof = foundry.get_apr_proof(test) with legacy_explore( foundry.kevm, kcfg_semantics=KEVMSemantics(), id=apr_proof.id, - bug_report=br, + bug_report=bug_report, smt_timeout=smt_timeout, smt_retry_limit=smt_retry_limit, trace_rewrites=trace_rewrites, @@ -883,20 +880,19 @@ def foundry_section_edge( edge: tuple[str, str], sections: int = 2, replace: bool = False, - bug_report: bool = False, + bug_report: BugReport | None = None, smt_timeout: int | None = None, smt_retry_limit: int | None = None, trace_rewrites: bool = False, ) -> None: - br = BugReport(Path(f'{test}.bug_report')) if bug_report else None - foundry = Foundry(foundry_root, bug_report=br) + foundry = Foundry(foundry_root, bug_report=bug_report) apr_proof = foundry.get_apr_proof(test) source_id, target_id = edge with legacy_explore( foundry.kevm, kcfg_semantics=KEVMSemantics(), id=apr_proof.id, - bug_report=br, + bug_report=bug_report, smt_timeout=smt_timeout, smt_retry_limit=smt_retry_limit, trace_rewrites=trace_rewrites, From 3913eeb6b5aac86a49d59be12c58ea1d9c851b55 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Fri, 25 Aug 2023 16:48:12 +0000 Subject: [PATCH 02/10] kevm-pyk/{test_prove,test_foundry_prove}: allow generating bug reports --- .../tests/integration/test_foundry_prove.py | 26 ++++++++++++++----- kevm-pyk/src/tests/integration/test_prove.py | 4 +++ 2 files changed, 24 insertions(+), 6 deletions(-) diff --git a/kevm-pyk/src/tests/integration/test_foundry_prove.py b/kevm-pyk/src/tests/integration/test_foundry_prove.py index c427f159e0..4606fccd97 100644 --- a/kevm-pyk/src/tests/integration/test_foundry_prove.py +++ b/kevm-pyk/src/tests/integration/test_foundry_prove.py @@ -23,6 +23,7 @@ from pathlib import Path from typing import Final + from pyk.utils import BugReport from pytest import TempPathFactory @@ -95,7 +96,9 @@ def assert_or_update_k_output(k_file: Path, expected_file: Path, *, update: bool @pytest.mark.parametrize('test_id', ALL_PROVE_TESTS) -def test_foundry_prove(test_id: str, foundry_root: Path, update_expected_output: bool, use_booster: bool) -> None: +def test_foundry_prove( + test_id: str, foundry_root: Path, update_expected_output: bool, use_booster: bool, bug_report: BugReport | None +) -> None: if test_id in SKIPPED_PROVE_TESTS or (update_expected_output and not test_id in SHOW_TESTS): pytest.skip() @@ -108,6 +111,7 @@ def test_foundry_prove(test_id: str, foundry_root: Path, update_expected_output: smt_retry_limit=10, use_booster=use_booster, counterexample_info=True, + bug_report=bug_report, ) # Then @@ -181,7 +185,7 @@ def test_foundry_fail(test_id: str, foundry_root: Path, update_expected_output: @pytest.mark.parametrize('test_id', ALL_BMC_TESTS) -def test_foundry_bmc(test_id: str, foundry_root: Path, use_booster: bool) -> None: +def test_foundry_bmc(test_id: str, foundry_root: Path, use_booster: bool, bug_report: BugReport | None) -> None: if test_id in SKIPPED_BMC_TESTS: pytest.skip() @@ -194,13 +198,14 @@ def test_foundry_bmc(test_id: str, foundry_root: Path, use_booster: bool) -> Non smt_timeout=300, smt_retry_limit=10, use_booster=use_booster, + bug_report=bug_report, ) # Then assert_pass(test_id, prove_res) -def test_foundry_merge_nodes(foundry_root: Path, use_booster: bool) -> None: +def test_foundry_merge_nodes(foundry_root: Path, use_booster: bool, bug_report: BugReport | None) -> None: test_id = 'AssertTest.test_branch_merge(uint256)' foundry_prove( @@ -210,6 +215,7 @@ def test_foundry_merge_nodes(foundry_root: Path, use_booster: bool) -> None: smt_retry_limit=10, max_iterations=4, use_booster=use_booster, + bug_report=bug_report, ) check_pending(foundry_root, test_id, [6, 7]) @@ -228,6 +234,7 @@ def test_foundry_merge_nodes(foundry_root: Path, use_booster: bool) -> None: smt_timeout=300, smt_retry_limit=10, use_booster=use_booster, + bug_report=bug_report, ) assert_pass(test_id, prove_res) @@ -238,7 +245,9 @@ def check_pending(foundry_root: Path, test: str, pending: list[int]) -> None: assert [node.id for node in proof.pending] == pending -def test_foundry_auto_abstraction(foundry_root: Path, update_expected_output: bool) -> None: +def test_foundry_auto_abstraction( + foundry_root: Path, update_expected_output: bool, bug_report: BugReport | None +) -> None: test_id = 'GasTest.testInfiniteGas()' foundry_prove( foundry_root, @@ -246,6 +255,7 @@ def test_foundry_auto_abstraction(foundry_root: Path, update_expected_output: bo smt_timeout=300, smt_retry_limit=10, auto_abstract_gas=True, + bug_report=bug_report, ) show_res = foundry_show( @@ -265,7 +275,7 @@ def test_foundry_auto_abstraction(foundry_root: Path, update_expected_output: bo assert_or_update_show_output(show_res, TEST_DATA_DIR / 'gas-abstraction.expected', update=update_expected_output) -def test_foundry_remove_node(foundry_root: Path, update_expected_output: bool) -> None: +def test_foundry_remove_node(foundry_root: Path, update_expected_output: bool, bug_report: BugReport | None) -> None: test = 'AssertTest.test_assert_true()' foundry = Foundry(foundry_root) @@ -275,6 +285,7 @@ def test_foundry_remove_node(foundry_root: Path, update_expected_output: bool) - tests=[test], smt_timeout=300, smt_retry_limit=10, + bug_report=bug_report, ) assert_pass(test, prove_res) @@ -292,6 +303,7 @@ def test_foundry_remove_node(foundry_root: Path, update_expected_output: bool) - tests=[test], smt_timeout=300, smt_retry_limit=10, + bug_report=bug_report, ) assert_pass(test, prove_res) @@ -336,7 +348,7 @@ def assert_or_update_show_output(show_res: str, expected_file: Path, *, update: assert actual_text == expected_text -def test_foundry_resume_proof(foundry_root: Path, update_expected_output: bool) -> None: +def test_foundry_resume_proof(foundry_root: Path, update_expected_output: bool, bug_report: BugReport | None) -> None: foundry = Foundry(foundry_root) test_id = 'AssumeTest.test_assume_false(uint256,uint256)' @@ -348,6 +360,7 @@ def test_foundry_resume_proof(foundry_root: Path, update_expected_output: bool) auto_abstract_gas=True, max_iterations=4, reinit=True, + bug_report=bug_report, ) proof = foundry.get_apr_proof(test_id) @@ -361,5 +374,6 @@ def test_foundry_resume_proof(foundry_root: Path, update_expected_output: bool) auto_abstract_gas=True, max_iterations=6, reinit=False, + bug_report=bug_report, ) assert_fail(test_id, prove_res) diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 34e28c5e6a..5449b65378 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -20,6 +20,7 @@ from pathlib import Path from typing import Any, Final + from pyk.utils import BugReport from pytest import LogCaptureFixture, TempPathFactory @@ -217,6 +218,7 @@ def test_pyk_prove( tmp_path: Path, caplog: LogCaptureFixture, use_booster: bool, + bug_report: BugReport | None, ) -> None: caplog.set_level(logging.INFO) @@ -240,6 +242,7 @@ def test_pyk_prove( smt_retry_limit=10, md_selector='foo', # TODO Ignored flag, this is to avoid KeyError use_booster=use_booster, + bug_report=bug_report, ) except BaseException: raise @@ -272,6 +275,7 @@ def test_legacy_prove( kompiled_target_for: Callable[[Path, bool], KompiledTarget], tmp_path: Path, caplog: LogCaptureFixture, + bug_report: BugReport | None, ) -> None: caplog.set_level(logging.INFO) From 78f6d85e185848876ac1e10772789500dc9579c7 Mon Sep 17 00:00:00 2001 From: devops Date: Sun, 27 Aug 2023 23:10:08 +0000 Subject: [PATCH 03/10] Set Version: 1.0.280 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index f83ad4789d..9bf892ab2f 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.279" +version = "1.0.280" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 900d25ea87..f416f538a6 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.279) unstable; urgency=medium +kevm (1.0.280) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index e83845c706..4418310f44 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.279 +1.0.280 From fa79ebb49e4ce789707b549a0ac34bf9216933d2 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 6 Sep 2023 14:48:43 +0000 Subject: [PATCH 04/10] Set Version: 1.0.286 --- package/debian/changelog | 2 +- package/version | 4 ---- 2 files changed, 1 insertion(+), 5 deletions(-) diff --git a/package/debian/changelog b/package/debian/changelog index 23b0abc404..7a4f957a6d 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,5 +1,5 @@ <<<<<<< HEAD -kevm (1.0.280) unstable; urgency=medium +kevm (1.0.286) unstable; urgency=medium ======= kevm (1.0.286) unstable; urgency=medium >>>>>>> upstream/master diff --git a/package/version b/package/version index c42f1477f6..c3ace87fe2 100644 --- a/package/version +++ b/package/version @@ -1,5 +1 @@ -<<<<<<< HEAD -1.0.280 -======= 1.0.286 ->>>>>>> upstream/master From 1a81907ba5ccee2e23d2dd4f14d164a726af20ef Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 6 Sep 2023 14:49:33 +0000 Subject: [PATCH 05/10] Set Version: 1.0.287 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 4 ++-- package/version | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 9512696aee..cbdbc5f1a3 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.286" +version = "1.0.287" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 7a4f957a6d..46ca334ff0 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,7 +1,7 @@ <<<<<<< HEAD -kevm (1.0.286) unstable; urgency=medium +kevm (1.0.287) unstable; urgency=medium ======= -kevm (1.0.286) unstable; urgency=medium +kevm (1.0.287) unstable; urgency=medium >>>>>>> upstream/master * Initial Release. diff --git a/package/version b/package/version index c3ace87fe2..44b743e430 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.286 +1.0.287 From 5896c6e344717d4982ff41691c96d6495e03abcb Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 6 Sep 2023 14:51:10 +0000 Subject: [PATCH 06/10] {kevm-pyk,kontrol}/__main__: add rpc_args --- kevm-pyk/src/kevm_pyk/__main__.py | 1 + kevm-pyk/src/kontrol/__main__.py | 5 +++++ 2 files changed, 6 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 43d015a98b..65da66dc2f 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -572,6 +572,7 @@ def parse(s: str) -> list[T]: kevm_cli_args.parallel_args, kevm_cli_args.k_args, kevm_cli_args.kprove_args, + kevm_cli_args.rpc_args, kevm_cli_args.bug_report_args, kevm_cli_args.smt_args, kevm_cli_args.explore_args, diff --git a/kevm-pyk/src/kontrol/__main__.py b/kevm-pyk/src/kontrol/__main__.py index 65f91f8437..a06074652c 100644 --- a/kevm-pyk/src/kontrol/__main__.py +++ b/kevm-pyk/src/kontrol/__main__.py @@ -484,6 +484,7 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]: kevm_cli_args.k_args, kevm_cli_args.kprove_args, kevm_cli_args.smt_args, + kevm_cli_args.rpc_args, kevm_cli_args.bug_report_args, kevm_cli_args.explore_args, kevm_cli_args.foundry_args, @@ -578,6 +579,7 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]: kevm_cli_args.foundry_test_args, kevm_cli_args.logging_args, kevm_cli_args.smt_args, + kevm_cli_args.rpc_args, kevm_cli_args.bug_report_args, kevm_cli_args.display_args, kevm_cli_args.foundry_args, @@ -594,6 +596,7 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]: parents=[ kevm_cli_args.foundry_test_args, kevm_cli_args.logging_args, + kevm_cli_args.rpc_args, kevm_cli_args.bug_report_args, kevm_cli_args.smt_args, kevm_cli_args.foundry_args, @@ -630,6 +633,7 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]: parents=[ kevm_cli_args.foundry_test_args, kevm_cli_args.logging_args, + kevm_cli_args.rpc_args, kevm_cli_args.bug_report_args, kevm_cli_args.smt_args, kevm_cli_args.foundry_args, @@ -646,6 +650,7 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]: parents=[ kevm_cli_args.foundry_test_args, kevm_cli_args.logging_args, + kevm_cli_args.rpc_args, kevm_cli_args.bug_report_args, kevm_cli_args.smt_args, kevm_cli_args.foundry_args, From 25ea01b9ae2a44306ef565109b5e0b6b859753ac Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 6 Sep 2023 14:54:08 +0000 Subject: [PATCH 07/10] test_foundry_prove: remove use_booster arguments where not used --- kevm-pyk/src/tests/integration/test_foundry_prove.py | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/kevm-pyk/src/tests/integration/test_foundry_prove.py b/kevm-pyk/src/tests/integration/test_foundry_prove.py index 606256c386..0e3e4f545f 100644 --- a/kevm-pyk/src/tests/integration/test_foundry_prove.py +++ b/kevm-pyk/src/tests/integration/test_foundry_prove.py @@ -51,7 +51,7 @@ def server(foundry_root: Path, use_booster: bool) -> Iterator[KoreServer]: @pytest.fixture(scope='session') -def foundry_root(tmp_path_factory: TempPathFactory, worker_id: str, use_booster: bool) -> Path: +def foundry_root(tmp_path_factory: TempPathFactory, worker_id: str) -> Path: if worker_id == 'master': root_tmp_dir = tmp_path_factory.getbasetemp() else: @@ -206,9 +206,7 @@ def test_foundry_fail( @pytest.mark.parametrize('test_id', ALL_BMC_TESTS) -def test_foundry_bmc( - test_id: str, foundry_root: Path, use_booster: bool, bug_report: BugReport | None, server: KoreServer -) -> None: +def test_foundry_bmc(test_id: str, foundry_root: Path, bug_report: BugReport | None, server: KoreServer) -> None: if test_id in SKIPPED_BMC_TESTS: pytest.skip() @@ -226,9 +224,7 @@ def test_foundry_bmc( assert_pass(test_id, prove_res) -def test_foundry_merge_nodes( - foundry_root: Path, use_booster: bool, bug_report: BugReport | None, server: KoreServer -) -> None: +def test_foundry_merge_nodes(foundry_root: Path, bug_report: BugReport | None, server: KoreServer) -> None: test = 'AssertTest.test_branch_merge(uint256)' foundry_prove( From cff3df688bb90b2a0c0e10e8ccd2ace28911a133 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 6 Sep 2023 15:05:02 +0000 Subject: [PATCH 08/10] package/debian/changelog: fx merge conflict --- package/debian/changelog | 4 ---- 1 file changed, 4 deletions(-) diff --git a/package/debian/changelog b/package/debian/changelog index 46ca334ff0..66c9cdbe80 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,8 +1,4 @@ -<<<<<<< HEAD kevm (1.0.287) unstable; urgency=medium -======= -kevm (1.0.287) unstable; urgency=medium ->>>>>>> upstream/master * Initial Release. From a44e43c9311d20ed5554a6ab78d37fd8f17b8cbc Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 6 Sep 2023 15:09:53 +0000 Subject: [PATCH 09/10] kontrol/__main__: remove unused bug_report_args --- kevm-pyk/src/kontrol/__main__.py | 1 - 1 file changed, 1 deletion(-) diff --git a/kevm-pyk/src/kontrol/__main__.py b/kevm-pyk/src/kontrol/__main__.py index a06074652c..5eab8f2d12 100644 --- a/kevm-pyk/src/kontrol/__main__.py +++ b/kevm-pyk/src/kontrol/__main__.py @@ -651,7 +651,6 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]: kevm_cli_args.foundry_test_args, kevm_cli_args.logging_args, kevm_cli_args.rpc_args, - kevm_cli_args.bug_report_args, kevm_cli_args.smt_args, kevm_cli_args.foundry_args, ], From cfa95bf3229216c265f1073a32cfab46335db1d4 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 7 Sep 2023 15:04:50 +0000 Subject: [PATCH 10/10] Set Version: 1.0.289 --- kevm-pyk/pyproject.toml | 2 +- package/debian/changelog | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index c138f4f094..5ffe49f2a3 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.288" +version = "1.0.289" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/package/debian/changelog b/package/debian/changelog index 621663df1e..b1311419e4 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.288) unstable; urgency=medium +kevm (1.0.289) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 3dbd46e6c2..c7119f13e9 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.288 +1.0.289