diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 02eb3da773..23f1453486 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -352,6 +352,7 @@ def create_kcfg_explore() -> KCFGExplore: max_iterations=options.max_iterations, cut_point_rules=KEVMSemantics.cut_point_rules( options.break_on_jumpi, + options.break_on_jump, options.break_on_calls, options.break_on_storage, options.break_on_basic_blocks, diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index ee4f4617e1..43e3f90daa 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -334,6 +334,7 @@ def get_argument_type() -> dict[str, Callable]: class ExploreOptions(Options): break_every_step: bool break_on_jumpi: bool + break_on_jump: bool break_on_calls: bool break_on_storage: bool break_on_basic_blocks: bool @@ -350,6 +351,7 @@ class ExploreOptions(Options): def default() -> dict[str, Any]: return { 'break_every_step': False, + 'break_on_jump': False, 'break_on_jumpi': False, 'break_on_calls': False, 'break_on_storage': False, @@ -1040,6 +1042,13 @@ def explore_args(self) -> ArgumentParser: dest='break_on_jumpi', default=None, action='store_true', + help='Store a node for every EVM jumpi opcode.', + ) + args.add_argument( + '--break-on-jump', + dest='break_on_jump', + default=None, + action='store_true', help='Store a node for every EVM jump opcode.', ) args.add_argument( diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index bf74746c3f..82f8c788d3 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -164,6 +164,7 @@ def custom_step(self, cterm: CTerm) -> KCFGExtendResult | None: @staticmethod def cut_point_rules( break_on_jumpi: bool, + break_on_jump: bool, break_on_calls: bool, break_on_storage: bool, break_on_basic_blocks: bool, @@ -172,6 +173,8 @@ def cut_point_rules( cut_point_rules = [] if break_on_jumpi: cut_point_rules.extend(['EVM.jumpi.true', 'EVM.jumpi.false']) + if break_on_jump: + cut_point_rules.extend(['EVM.jump']) if break_on_basic_blocks: cut_point_rules.append('EVM.end-basic-block') if break_on_calls or break_on_basic_blocks: diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index 56f673a5cc..5708f1ae4b 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1076,7 +1076,8 @@ The `JUMP*` family of operations affect the current program counter. syntax UnStackOp ::= "JUMP" // --------------------------- - rule JUMP DEST => #endBasicBlock ... + rule [jump]: + JUMP DEST => #endBasicBlock ... _ => DEST DESTS requires DEST