kevm-pyk/{evm,*.py}: add option --break-on-jump (#2653)

runtimeverification · Nov 7, 2024 · ccee56b · ccee56b
1 parent 1a7a2a6
commit ccee56b
Show file tree

Hide file tree

Showing 4 changed files with 15 additions and 1 deletion.
diff --git 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
@@ -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
@@ -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
@@ -1076,7 +1076,8 @@ The `JUMP*` family of operations affect the current program counter.
 
     syntax UnStackOp ::= "JUMP"
  // ---------------------------
-    rule <k> JUMP DEST => #endBasicBlock ... </k>
+    rule [jump]:
+         <k> JUMP DEST => #endBasicBlock ... </k>
          <pc> _ => DEST </pc>
          <jumpDests> DESTS </jumpDests>
       requires DEST <Int lengthBytes(DESTS) andBool DESTS[DEST] ==Int 1