Have <jumpDests> as Bytes instead of Set (#2471)

* save jumpdests as bytes

* remove loadProgram cut rule

* Set Version: 1.0.594

* formatting

* Set Version: 1.0.595

* test-integration: update expected output

* update claims

* add --break-on-load-program

* Apply suggestions from code review

Co-authored-by: Petar Maksimović <[email protected]>

* evm.md: mark bad jump rule with owise

* cli.py: --break-on-load-program => --symbolic-immutables

* Set Version: 1.0.596

* Add review suggestions

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Petar Maksimovic <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.595"
+version = "1.0.596"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.595'
+VERSION: Final = '1.0.596'

kevm-pyk/src/kevm_pyk/__main__.py

@@ -382,6 +382,7 @@ def create_kcfg_explore() -> KCFGExplore:
                     options.break_on_calls,
                     options.break_on_storage,
                     options.break_on_basic_blocks,
+                    options.break_on_load_program,
                 ),
                 terminal_rules=KEVMSemantics.terminal_rules(options.break_every_step),
                 fail_fast=options.fail_fast,

kevm-pyk/src/kevm_pyk/cli.py

@@ -379,6 +379,7 @@ class ExploreOptions(Options):
     break_on_calls: bool
     break_on_storage: bool
     break_on_basic_blocks: bool
+    break_on_load_program: bool
     max_depth: int
     max_iterations: int | None
     failure_info: bool
@@ -394,6 +395,7 @@ def default() -> dict[str, Any]:
             'break_on_calls': False,
             'break_on_storage': False,
             'break_on_basic_blocks': False,
+            'break_on_load_program': False,
             'max_depth': 1000,
             'max_iterations': None,
             'failure_info': True,
@@ -1119,6 +1121,13 @@ def explore_args(self) -> ArgumentParser:
             action='store_true',
             help='Store a node for every EVM basic block (implies --break-on-calls).',
         )
+        args.add_argument(
+            '--symbolic-constructor',
+            dest='break_on_load_program',
+            default=None,
+            action='store_true',
+            help='Enable support for symbolic parameters in Solidity constructor code.',
+        )
         args.add_argument(
             '--max-depth',
             dest='max_depth',

kevm-pyk/src/kevm_pyk/kevm.py

@@ -25,11 +25,11 @@
 from pyk.ktool.kprove import KProve
 from pyk.ktool.krun import KRun
 from pyk.prelude.bytes import BYTES, pretty_bytes
-from pyk.prelude.collections import set_of
 from pyk.prelude.kbool import notBool
 from pyk.prelude.kint import INT, eqInt, intToken, ltInt
 from pyk.prelude.ml import mlEqualsFalse, mlEqualsTrue
 from pyk.prelude.string import stringToken
+from pyk.prelude.utils import token
 from pyk.proof.reachability import APRProof
 from pyk.proof.show import APRProofNodePrinter
 
@@ -157,9 +157,7 @@ def custom_step(self, cterm: CTerm) -> KCFGExtendResult | None:
         :return: If the K_CELL matches the load_pattern, a Step with depth 1 is returned together with the new configuration, also registering that the `EVM.program.load` rule has been applied. Otherwise, None is returned.
         :rtype: KCFGExtendResult | None
         """
-        load_pattern = KSequence(
-            [KApply('#loadProgram__EVM_KItem_Bytes', KVariable('###BYTECODE')), KVariable('###CONTINUATION')]
-        )
+        load_pattern = KSequence([KApply('loadProgram', KVariable('###BYTECODE')), KVariable('###CONTINUATION')])
         subst = load_pattern.match(cterm.cell('K_CELL'))
         if subst is not None:
             bytecode_sections = flatten_label('_+Bytes__BYTES-HOOKED_Bytes_Bytes_Bytes', subst['###BYTECODE'])
@@ -172,9 +170,13 @@ def custom_step(self, cterm: CTerm) -> KCFGExtendResult | None:
 
     @staticmethod
     def cut_point_rules(
-        break_on_jumpi: bool, break_on_calls: bool, break_on_storage: bool, break_on_basic_blocks: bool
+        break_on_jumpi: bool,
+        break_on_calls: bool,
+        break_on_storage: bool,
+        break_on_basic_blocks: bool,
+        break_on_load_program: bool,
     ) -> list[str]:
-        cut_point_rules = ['EVM.program.load']
+        cut_point_rules = []
         if break_on_jumpi:
             cut_point_rules.extend(['EVM.jumpi.true', 'EVM.jumpi.false'])
         if break_on_basic_blocks:
@@ -198,6 +200,8 @@ def cut_point_rules(
             )
         if break_on_storage:
             cut_point_rules.extend(['EVM.sstore', 'EVM.sload'])
+        if break_on_load_program:
+            cut_point_rules.extend(['EVM.program.load'])
         return cut_point_rules
 
     @staticmethod
@@ -670,43 +674,43 @@ def compute_jumpdests(sections: list[KInner]) -> KInner:
     :return: This function iterates over each section, appending the jump destinations (0x5B) from the bytecode in a KAst Set.
     :rtype: KInner
     """
-    offset = 0
-    jumpdests = []
+    mutable_jumpdests = bytearray(b'')
     for s in sections:
         if type(s) is KApply and s.label == KLabel('buf'):
             width_token = s.args[0]
             assert type(width_token) is KToken
-            offset += int(width_token.token)
+            mutable_jumpdests += bytes(int(width_token.token))
         elif type(s) is KToken and s.sort == BYTES:
             bytecode = pretty_bytes(s)
-            jumpdests.extend(_process_jumpdests(bytecode, offset))
-            offset += len(bytecode)
+            mutable_jumpdests += _process_jumpdests(bytecode)
         else:
             raise ValueError(f'Cannot compute jumpdests for type: {type(s)}')
 
-    return set_of(jumpdests)
+    return token(bytes(mutable_jumpdests))
 
 
-def _process_jumpdests(bytecode: bytes, offset: int) -> list[KToken]:
+def _process_jumpdests(bytecode: bytes) -> bytes:
     """Computes the location of JUMPDEST opcodes from a given bytecode while avoiding bytes from within the PUSH opcodes.
 
     :param bytecode: The bytecode of the contract as bytes.
     :type bytecode: bytes
     :param offset: The offset to add to each position index to align it with the broader code structure.
     :type offset: int
-    :return:  A list of intToken instances representing the positions of all found jump destinations in the bytecode adjusted by the offset.
-    :rtype: list[KToken]
+    :return: A bytes object where each byte corresponds to a position in the input bytecode. Positions containing a valid JUMPDEST opcode are marked
+    with `0x01` while all other positions are marked with `0x00`.
+    :rtype: bytes
     """
     push1 = 0x60
     push32 = 0x7F
     jumpdest = 0x5B
+    bytecode_length = len(bytecode)
     i = 0
-    jumpdests: list[KToken] = []
-    while i < len(bytecode):
+    jumpdests = bytearray(bytecode_length)
+    while i < bytecode_length:
         if push1 <= bytecode[i] <= push32:
             i += bytecode[i] - push1 + 2
         else:
             if bytecode[i] == jumpdest:
-                jumpdests.append(intToken(offset + i))
+                jumpdests[i] = 0x1
             i += 1
-    return jumpdests
+    return bytes(jumpdests)

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md

@@ -55,7 +55,7 @@ In the comments next to each cell, we've marked which component of the YellowPap
 
             <callState>
               <program>   .Bytes </program>
-              <jumpDests> .Set   </jumpDests>
+              <jumpDests> .Bytes </jumpDests>
 
               // I_*
               <id>        .Account </id>                    // I_a
@@ -1039,14 +1039,12 @@ The `JUMP*` family of operations affect the current program counter.
 
     syntax UnStackOp ::= "JUMP"
  // ---------------------------
-    rule <k> JUMP DEST => #endBasicBlock... </k>
+    rule <k> JUMP DEST => #endBasicBlock ... </k>
          <pc> _ => DEST </pc>
          <jumpDests> DESTS </jumpDests>
-      requires DEST in DESTS
+      requires DEST <Int lengthBytes(DESTS) andBool DESTS[DEST] ==Int 1
 
-    rule <k> JUMP DEST => #end EVMC_BAD_JUMP_DESTINATION ... </k>
-         <jumpDests> DESTS </jumpDests>
-      requires notBool DEST in DESTS
+    rule <k> JUMP _ => #end EVMC_BAD_JUMP_DESTINATION ... </k> [owise]
 
     syntax BinStackOp ::= "JUMPI"
  // -----------------------------
@@ -1113,7 +1111,7 @@ These operators query about the current return data buffer.
          <output> RD </output>
 
     syntax TernStackOp ::= "RETURNDATACOPY"
- // ----------------------------------------
+ // ---------------------------------------
     rule <k> RETURNDATACOPY MEMSTART DATASTART DATAWIDTH => .K ... </k>
          <localMem> LM => LM [ MEMSTART := #range(RD, DATASTART, DATAWIDTH) ] </localMem>
          <output> RD </output>
@@ -1349,8 +1347,8 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
          <wordStack>    _ => .WordStack </wordStack>
          <localMem>     _ => .Bytes     </localMem>
 
-    syntax KItem ::= "#loadProgram" Bytes
- // -------------------------------------
+    syntax KItem ::= "#loadProgram" Bytes [symbol(loadProgram)]
+ // -----------------------------------------------------------
     rule [program.load]:
          <k> #loadProgram BYTES => .K ... </k>
          <program> _ => BYTES </program>
@@ -1395,17 +1393,17 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
     rule <k> #accessAccounts ADDRSET:Set => .K ... </k>
          <accessedAccounts> TOUCHED_ACCOUNTS => TOUCHED_ACCOUNTS |Set ADDRSET </accessedAccounts>
 
-    syntax Set ::= #computeValidJumpDests(Bytes)            [symbol(computeValidJumpDests),    function, memo, total]
-                 | #computeValidJumpDests(Bytes, Int, List) [symbol(computeValidJumpDestsAux), function             ]
- // -----------------------------------------------------------------------------------------------------------------
-    rule #computeValidJumpDests(PGM) => #computeValidJumpDests(PGM, 0, .List)
+    syntax Bytes ::= #computeValidJumpDests(Bytes)             [symbol(computeValidJumpDests),    function, memo, total]
+                   | #computeValidJumpDests(Bytes, Int, Bytes) [symbol(computeValidJumpDestsAux), function             ]
+ // --------------------------------------------------------------------------------------------------------------------
+    rule #computeValidJumpDests(PGM) => #computeValidJumpDests(PGM, 0, padRightBytes(.Bytes, lengthBytes(PGM), 0))
 
-    syntax Set ::= #computeValidJumpDestsWithinBound(Bytes, Int, List) [klabel(#computeValidJumpDestsWithinBound), function]
- // ------------------------------------------------------------------------------------------------------------------------
-    rule #computeValidJumpDests(PGM, I, RESULT) => List2Set(RESULT) requires I >=Int lengthBytes(PGM)
+    syntax Bytes ::= #computeValidJumpDestsWithinBound(Bytes, Int, Bytes) [symbol(computeValidJumpDestsWithinBound), function]
+ // --------------------------------------------------------------------------------------------------------------------------
+    rule #computeValidJumpDests(PGM, I, RESULT) => RESULT requires I >=Int lengthBytes(PGM)
     rule #computeValidJumpDests(PGM, I, RESULT) => #computeValidJumpDestsWithinBound(PGM, I, RESULT) requires I <Int lengthBytes(PGM)
 
-    rule #computeValidJumpDestsWithinBound(PGM, I, RESULT) => #computeValidJumpDests(PGM, I +Int 1, RESULT ListItem(I)) requires PGM [ I ] ==Int 91
+    rule #computeValidJumpDestsWithinBound(PGM, I, RESULT) => #computeValidJumpDests(PGM, I +Int 1, RESULT[I <- 1]) requires PGM [ I ] ==Int 91
     rule #computeValidJumpDestsWithinBound(PGM, I, RESULT) => #computeValidJumpDests(PGM, I +Int #widthOpCode(PGM [ I ]), RESULT) requires notBool PGM [ I ] ==Int 91
 ```
 

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md

@@ -32,7 +32,7 @@ module STATE-UTILS
          <callDepth>        _ => 0          </callDepth>
          <callStack>        _ => .List      </callStack>
          <program>          _ => .Bytes     </program>
-         <jumpDests>        _ => .Set       </jumpDests>
+         <jumpDests>        _ => .Bytes     </jumpDests>
          <id>               _ => .Account   </id>
          <caller>           _ => .Account   </caller>
          <callData>         _ => .Bytes     </callData>

kevm-pyk/src/tests/unit/test_kevm.py

@@ -9,7 +9,6 @@
     from pyk.kast.inner import KInner
 
 from pyk.kast.inner import KApply, KToken, KVariable
-from pyk.prelude.collections import set_of
 from pyk.prelude.utils import token
 
 from kevm_pyk.kevm import KEVM, compute_jumpdests
@@ -55,7 +54,7 @@ def test_kinner_to_hex(test_id: str, input: KInner, result: KInner) -> None:
 
 
 JUMPDESTS_DATA: Final = [
-    ('empty', [], set_of([])),
+    ('empty', [], token(b'')),
     (
         'with_buf',
         [
@@ -64,26 +63,14 @@ def test_kinner_to_hex(test_id: str, input: KInner, result: KInner) -> None:
             ),
             KEVM.buf(token(32), KVariable('VV0_x', 'Int')),
         ],
-        set_of(
-            [
-                token(16),
-                token(47),
-                token(55),
-                token(73),
-                token(80),
-                token(119),
-                token(144),
-                token(149),
-                token(187),
-            ]
-        ),
+        token(bytes([1 if i in [16, 47, 55, 73, 80, 119, 144, 149, 187] else 0 for i in range(291)])),
     ),
     (
         'single_jumpdest',
         [
             token(b'['),
         ],
-        set_of([token(0)]),
+        token(b'\x01'),
     ),
     (
         'multiple_bytes',
@@ -92,7 +79,7 @@ def test_kinner_to_hex(test_id: str, input: KInner, result: KInner) -> None:
             token(b'\x00\x00[\x00\x00'),
             token(b'\x00['),
         ],
-        set_of([token(16), token(19), token(23)]),
+        token(bytes([1 if i in [16, 19, 23] else 0 for i in range(24)])),
     ),
     (
         'multiple_bufs',
@@ -104,9 +91,9 @@ def test_kinner_to_hex(test_id: str, input: KInner, result: KInner) -> None:
             KEVM.buf(token(32), KVariable('VV0_y', 'Int')),
             token(b'\x00[[[\x00[\x00\x00'),
         ],
-        set_of([token(68), token(104), token(105), token(106), token(108)]),
+        token(bytes([1 if i in [68, 104, 105, 106, 108] else 0 for i in range(111)])),
     ),
-    ('jump_to_push', [token(bytes.fromhex('6001600055600A56605B5B'))], set_of([token(10)])),
+    ('jump_to_push', [token(bytes.fromhex('6001600055600A56605B5B'))], token(bytes.fromhex('0000000000000000000001'))),
 ]
 
 

package/version

@@ -1 +1 @@
-1.0.595
+1.0.596

tests/failing/ContractCreationSpam_d0g0v0.json.expected

@@ -39,7 +39,7 @@
           b""
         </program>
         <jumpDests>
-          .Set
+          b""
         </jumpDests>
         <id>
           .Account

tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected

@@ -39,7 +39,7 @@
           b""
         </program>
         <jumpDests>
-          .Set
+          b""
         </jumpDests>
         <id>
           .Account