1
1
from __future__ import annotations
2
2
3
3
import logging
4
- from typing import TYPE_CHECKING
4
+ from typing import TYPE_CHECKING , NamedTuple
5
5
6
6
from pyk .cterm import CTerm
7
7
from pyk .kast import KInner
48
48
_LOGGER : Final = logging .getLogger (__name__ )
49
49
50
50
51
- class CustomStep :
51
+ class CustomStep ( NamedTuple ) :
52
52
"""Encapsulates a custom step definition consisting of an abstract pattern and its execution function."""
53
53
54
54
pattern : KSequence
55
55
exec_fn : Callable [[Subst , CTerm , CTermSymbolic ], KCFGExtendResult | None ]
56
56
57
- def __init__ (
58
- self , pattern : KSequence , exec_fn : Callable [[Subst , CTerm , CTermSymbolic ], KCFGExtendResult | None ]
59
- ) -> None :
60
- self .pattern = pattern
61
- self .exec_fn = exec_fn
62
-
63
57
def check_pattern_match (self , cterm : CTerm ) -> bool :
64
58
return self .pattern .match (cterm .cell ('K_CELL' )) is not None
65
59
@@ -76,13 +70,13 @@ def try_execute(self, cterm: CTerm, cterm_symbolic: CTermSymbolic) -> KCFGExtend
76
70
class KEVMSemantics (DefaultSemantics ):
77
71
auto_abstract_gas : bool
78
72
allow_symbolic_program : bool
79
- _custom_steps : tuple [CustomStep ]
73
+ _custom_steps : tuple [CustomStep , ... ]
80
74
81
75
def __init__ (
82
76
self ,
83
77
auto_abstract_gas : bool = False ,
84
78
allow_symbolic_program : bool = False ,
85
- custom_step_definitions : tuple [CustomStep ] = None ,
79
+ custom_step_definitions : tuple [CustomStep ] | None = None ,
86
80
) -> None :
87
81
self .auto_abstract_gas = auto_abstract_gas
88
82
self .allow_symbolic_program = allow_symbolic_program
@@ -249,7 +243,7 @@ def _exec_load_custom_step(self, subst: Subst, cterm: CTerm, _c: CTermSymbolic)
249
243
return Step (new_cterm , 1 , (), ['EVM.program.load' ], cut = True )
250
244
251
245
def can_make_custom_step (self , cterm : CTerm ) -> bool :
252
- return any (c_step .check_pattern_match () for c_step in self ._custom_steps )
246
+ return any (c_step .check_pattern_match (cterm ) for c_step in self ._custom_steps )
253
247
254
248
def is_mergeable (self , ct1 : CTerm , ct2 : CTerm ) -> bool :
255
249
"""Given two CTerms of Edges' targets, check if they are mergeable.
0 commit comments