Merge remote-tracking branch 'origin/master' into _update-deps/runtim…

…everification/pyk
runtimeverification · Sep 8, 2023 · 4cfeb6c · 4cfeb6c
2 parents d18fe61 + 692a31c
commit 4cfeb6c
Show file tree

Hide file tree

Showing 6 changed files with 76 additions and 47 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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,