diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 07abef9414..af58eae9ce 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, @@ -174,7 +175,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, @@ -207,8 +208,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] @@ -242,7 +242,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, @@ -571,6 +571,7 @@ def parse(s: str) -> list[T]: 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, @@ -602,7 +603,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=[ @@ -612,6 +613,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 6ea215dbef..a9b7318cdb 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -172,12 +172,6 @@ def foundry_test_args(self) -> ArgumentParser: @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, diff --git a/kevm-pyk/src/kontrol/__main__.py b/kevm-pyk/src/kontrol/__main__.py index 402b0ea57f..5eab8f2d12 100644 --- a/kevm-pyk/src/kontrol/__main__.py +++ b/kevm-pyk/src/kontrol/__main__.py @@ -42,6 +42,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') @@ -155,7 +156,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, @@ -289,7 +290,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, @@ -323,7 +324,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, @@ -353,7 +354,6 @@ def exec_foundry_merge_nodes( test: str, id: str | None, nodes: Iterable[NodeIdLike], - bug_report: bool = False, **kwargs: Any, ) -> None: foundry_merge_nodes(foundry_root=foundry_root, node_ids=nodes, test=test, id=id) @@ -366,7 +366,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, @@ -485,6 +485,7 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]: 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, ], @@ -579,6 +580,7 @@ def _parse_test_id_tuple(value: str) -> tuple[str, str | None]: 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, ], @@ -595,6 +597,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.rpc_args, + kevm_cli_args.bug_report_args, kevm_cli_args.smt_args, kevm_cli_args.foundry_args, ], @@ -631,6 +634,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.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 8fdb8b711b..61e632976f 100644 --- a/kevm-pyk/src/kontrol/foundry.py +++ b/kevm-pyk/src/kontrol/foundry.py @@ -27,7 +27,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 ( @@ -52,6 +52,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__) @@ -620,7 +621,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, @@ -636,8 +637,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) foundry.mk_proofs_dir() @@ -728,7 +728,7 @@ def _init_and_run_proof(_init_problem: tuple[str, str, str | None]) -> tuple[boo foundry.kevm, kcfg_semantics=KEVMSemantics(auto_abstract_gas=auto_abstract_gas), id=test_id, - bug_report=br, + bug_report=bug_report, kore_rpc_command=kore_rpc_command, llvm_definition_dir=llvm_definition_dir, smt_timeout=smt_timeout, @@ -917,14 +917,13 @@ 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, port: int | None = None, ) -> 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) test_id = foundry.get_test_id(test, id) apr_proof = foundry.get_apr_proof(test_id) cterm = apr_proof.kcfg.node(node).cterm @@ -934,7 +933,7 @@ def foundry_simplify_node( 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, @@ -954,7 +953,7 @@ def foundry_merge_nodes( test: str, node_ids: Iterable[NodeIdLike], id: str | None = None, - 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: @@ -969,8 +968,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) test_id = foundry.get_test_id(test, id) apr_proof = foundry.get_apr_proof(test_id) @@ -1003,7 +1001,7 @@ def foundry_step_node( id: str | None = None, 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, @@ -1014,8 +1012,7 @@ 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) test_id = foundry.get_test_id(test, id) apr_proof = foundry.get_apr_proof(test_id) start_server = port is None @@ -1024,7 +1021,7 @@ def foundry_step_node( 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, @@ -1043,14 +1040,13 @@ def foundry_section_edge( id: str | None = None, 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, port: int | None = None, ) -> 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) test_id = foundry.get_test_id(test, id) apr_proof = foundry.get_apr_proof(test_id) source_id, target_id = edge @@ -1060,7 +1056,7 @@ def foundry_section_edge( 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, diff --git a/kevm-pyk/src/tests/integration/test_foundry_prove.py b/kevm-pyk/src/tests/integration/test_foundry_prove.py index bc3cfd348b..0e3e4f545f 100644 --- a/kevm-pyk/src/tests/integration/test_foundry_prove.py +++ b/kevm-pyk/src/tests/integration/test_foundry_prove.py @@ -27,6 +27,7 @@ from typing import Final from pyk.kore.rpc import KoreServer + from pyk.utils import BugReport from pytest import TempPathFactory @@ -50,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: @@ -116,14 +117,24 @@ 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, server: KoreServer + test_id: str, + foundry_root: Path, + update_expected_output: bool, + use_booster: bool, + bug_report: BugReport | None, + server: KoreServer, ) -> None: if test_id in SKIPPED_PROVE_TESTS or (update_expected_output and not test_id in SHOW_TESTS): pytest.skip() # When prove_res = foundry_prove( - foundry_root, tests=[(test_id, None)], simplify_init=False, counterexample_info=True, port=server.port + foundry_root, + tests=[(test_id, None)], + simplify_init=False, + counterexample_info=True, + port=server.port, + bug_report=bug_report, ) # Then @@ -195,7 +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, 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() @@ -206,13 +217,14 @@ def test_foundry_bmc(test_id: str, foundry_root: Path, use_booster: bool, server bmc_depth=3, simplify_init=False, port=server.port, + bug_report=bug_report, ) # Then assert_pass(test_id, prove_res) -def test_foundry_merge_nodes(foundry_root: Path, use_booster: bool, 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( @@ -220,6 +232,7 @@ def test_foundry_merge_nodes(foundry_root: Path, use_booster: bool, server: Kore tests=[(test, None)], max_iterations=4, port=server.port, + bug_report=bug_report, ) check_pending(foundry_root, test, [6, 7]) @@ -236,6 +249,7 @@ def test_foundry_merge_nodes(foundry_root: Path, use_booster: bool, server: Kore foundry_root, tests=[(test, None)], port=server.port, + bug_report=bug_report, ) assert_pass(test, prove_res) @@ -249,13 +263,18 @@ def check_pending(foundry_root: Path, test: str, pending: list[int]) -> None: def test_foundry_auto_abstraction( - foundry_root: Path, update_expected_output: bool, server: KoreServer, use_booster: bool + foundry_root: Path, + update_expected_output: bool, + bug_report: BugReport | None, + server: KoreServer, + use_booster: bool, ) -> None: test_id = 'GasTest.testInfiniteGas()' foundry_prove( foundry_root, tests=[(test_id, None)], auto_abstract_gas=True, + bug_report=bug_report, port=server.port, simplify_init=False, ) @@ -279,7 +298,9 @@ def test_foundry_auto_abstraction( 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, server: KoreServer) -> None: +def test_foundry_remove_node( + foundry_root: Path, update_expected_output: bool, bug_report: BugReport | None, server: KoreServer +) -> None: test = 'AssertTest.test_assert_true()' foundry = Foundry(foundry_root) @@ -288,6 +309,7 @@ def test_foundry_remove_node(foundry_root: Path, update_expected_output: bool, s foundry_root, tests=[(test, None)], port=server.port, + bug_report=bug_report, ) assert_pass(test, prove_res) @@ -305,6 +327,7 @@ def test_foundry_remove_node(foundry_root: Path, update_expected_output: bool, s foundry_root, tests=[(test, None)], port=server.port, + bug_report=bug_report, ) assert_pass(test, prove_res) @@ -353,7 +376,9 @@ 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, server: KoreServer) -> None: +def test_foundry_resume_proof( + foundry_root: Path, update_expected_output: bool, bug_report: BugReport | None, server: KoreServer +) -> None: foundry = Foundry(foundry_root) test = 'AssumeTest.test_assume_false(uint256,uint256)' @@ -364,6 +389,7 @@ def test_foundry_resume_proof(foundry_root: Path, update_expected_output: bool, max_iterations=4, reinit=True, port=server.port, + bug_report=bug_report, ) id = id_for_test(test, prove_res) @@ -377,5 +403,6 @@ def test_foundry_resume_proof(foundry_root: Path, update_expected_output: bool, max_iterations=6, reinit=False, port=server.port, + bug_report=bug_report, ) assert_fail(test, prove_res) diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 46b34f3ed5..9a8a6665cc 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)