kevm-pyk/: separate option --break-on-jumps for breakin gon JUMPI instructions

Author: ehildenb

kevm-pyk/src/kevm_pyk/__main__.py

@@ -187,6 +187,7 @@ def exec_prove(
     workers: int = 1,
     simplify_init: bool = True,
     break_every_step: bool = False,
+    break_on_jumpi: bool = False,
     break_on_calls: bool = True,
     implication_every_block: bool = True,
     rpc_base_port: Optional[int] = None,
@@ -219,6 +220,7 @@ def exec_prove(
         max_iterations=max_iterations,
         workers=workers,
         break_every_step=break_every_step,
+        break_on_jumpi=break_on_jumpi,
         break_on_calls=break_on_calls,
         implication_every_block=implication_every_block,
         rpc_base_port=rpc_base_port,
@@ -276,6 +278,7 @@ def exec_foundry_prove(
     workers: int = 1,
     simplify_init: bool = True,
     break_every_step: bool = False,
+    break_on_jumpi: bool = False,
     break_on_calls: bool = True,
     implication_every_block: bool = True,
     rpc_base_port: Optional[int] = None,
@@ -296,6 +299,7 @@ def exec_foundry_prove(
         workers=workers,
         simplify_init=simplify_init,
         break_every_step=break_every_step,
+        break_on_jumpi=break_on_jumpi,
         break_on_calls=break_on_calls,
         implication_every_block=implication_every_block,
         rpc_base_port=rpc_base_port,
@@ -481,6 +485,13 @@ def parse(s: str) -> List[T]:
         action='store_true',
         help='Store a node for every EVM opcode step (expensive).',
     )
+    explore_args.add_argument(
+        '--break-on-jumpi',
+        dest='break_on_jumpi',
+        default=False,
+        action='store_true',
+        help='Store a node for every EVM jump opcode.',
+    )
     explore_args.add_argument(
         '--break-on-calls',
         dest='break_on_calls',

kevm-pyk/src/kevm_pyk/foundry.py

@@ -194,6 +194,7 @@ def foundry_prove(
     workers: int = 1,
     simplify_init: bool = True,
     break_every_step: bool = False,
+    break_on_jumpi: bool = False,
     break_on_calls: bool = True,
     implication_every_block: bool = True,
     rpc_base_port: Optional[int] = None,
@@ -279,6 +280,7 @@ def foundry_prove(
         max_iterations=max_iterations,
         workers=workers,
         break_every_step=break_every_step,
+        break_on_jumpi=break_on_jumpi,
         break_on_calls=break_on_calls,
         implication_every_block=implication_every_block,
         rpc_base_port=rpc_base_port,

kevm-pyk/src/kevm_pyk/utils.py

@@ -45,6 +45,7 @@ def parallel_kcfg_explore(
     max_iterations: Optional[int] = None,
     workers: int = 1,
     break_every_step: bool = False,
+    break_on_jumpi: bool = False,
     break_on_calls: bool = True,
     implication_every_block: bool = False,
     rpc_base_port: Optional[int] = None,
@@ -57,6 +58,8 @@ def _call_rpc(packed_args: Tuple[str, KCFG, int]) -> bool:
         terminal_rules = ['EVM.halt']
         if break_every_step:
             terminal_rules.append('EVM.step')
+        if break_on_jumpi:
+            terminal_rules.extend(['EVM.jumpi.true', 'EVM.jumpi.false'])
         if break_on_calls:
             terminal_rules.extend(
                 [
@@ -71,8 +74,6 @@ def _call_rpc(packed_args: Tuple[str, KCFG, int]) -> bool:
                     'EVM.return.exception',
                     'EVM.return.revert',
                     'EVM.return.success',
-                    'EVM.jumpi.true',
-                    'EVM.jumpi.false',
                 ]
             )
         base_port = rpc_base_port if rpc_base_port is not None else find_free_port()