Add struct support

include/kframework/abi.md

@@ -134,9 +134,14 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
                       | #array   ( TypedArg , Int , TypedArgs ) [klabel(abi_type_array),   symbol]
  // ----------------------------------------------------------------------------------------------
 
-    syntax TypedArgs ::= List{TypedArg, ","} [klabel(typedArgs)]
+    syntax TypedArgs ::= List{TypedArg, ","} [klabel(typedArgs)             ]
+                       | #tuple(TypedArgs)   [klabel(abi_type_tuple, symbol)]
  // ------------------------------------------------------------
 
+    rule #typeName(#tuple(.TypedArgs))                 => "()"
+    rule #typeName(#tuple(TARGA:TypedArg, .TypedArgs)) => "(" +String #typeName(TARGA) +String ")"
+    rule #typeName(#tuple(TARGA:TypedArg, TARGS))      => "(" +String #generateSignatureArgs(TARGA, TARGS) +String ")"
+
     syntax Bytes ::= #abiCallData ( String , TypedArgs ) [function]
  // ---------------------------------------------------------------
     rule #abiCallData( FNAME , ARGS ) => #signatureCallData(FNAME, ARGS) +Bytes #encodeArgs(ARGS)
@@ -154,7 +159,8 @@ where `F1 : F2 : F3 : F4` is the (two's complement) byte-array representation of
     rule #generateSignatureArgs(TARGA:TypedArg, .TypedArgs)            => #typeName(TARGA)
     rule #generateSignatureArgs(TARGA:TypedArg, TARGB:TypedArg, TARGS) => #typeName(TARGA) +String "," +String #generateSignatureArgs(TARGB, TARGS)
 
-    syntax String ::= #typeName ( TypedArg ) [function, total]
+    syntax String ::= #typeName ( TypedArg  )                            [function, total]
+                    | #typeName ( TypedArgs )                            [function, total]
  // ----------------------------------------------------------
     rule #typeName(   #address( _ )) => "address"
 

kevm-pyk/pyproject.toml

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

kevm-pyk/src/kevm_pyk/kevm.py

@@ -1,7 +1,7 @@
 from __future__ import annotations
 
 import logging
-from typing import TYPE_CHECKING
+from typing import TYPE_CHECKING, Sequence
 
 from pyk.cterm import CTerm
 from pyk.kast.inner import KApply, KLabel, KSequence, KSort, KVariable, build_assoc
@@ -322,7 +322,7 @@ def lookup(map: KInner, key: KInner) -> KApply:
         return KApply('#lookup(_,_)_EVM-TYPES_Int_Map_Int', [map, key])
 
     @staticmethod
-    def abi_calldata(name: str, args: list[KInner]) -> KApply:
+    def abi_calldata(name: str, args: list[KApply]) -> KApply:
         return KApply('#abiCallData(_,_)_EVM-ABI_Bytes_String_TypedArgs', [stringToken(name), KEVM.typed_args(args)])
 
     @staticmethod
@@ -341,6 +341,10 @@ def abi_bool(b: KInner) -> KApply:
     def abi_type(type: str, value: KInner) -> KApply:
         return KApply('abi_type_' + type, [value])
 
+    @staticmethod
+    def abi_tuple(values: Sequence[KInner]) -> KApply:
+        return KApply('abi_type_tuple', values)
+
     @staticmethod
     def empty_typedargs() -> KApply:
         return KApply('.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs')
@@ -385,12 +389,20 @@ def intlist(ints: list[KInner]) -> KApply:
         return res
 
     @staticmethod
-    def typed_args(args: list[KInner]) -> KApply:
+    def typed_args(args: list[KApply]) -> KApply:
         res = KApply('.List{"_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs"}_TypedArgs')
-        for i in reversed(args):
-            res = KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', [i, res])
+        for arg in reversed(args):
+            res = KEVM.to_typed_arg(arg, res)
         return res
 
+    @staticmethod
+    def to_typed_arg(arg: KApply, res: KApply) -> KApply:
+        if arg.label == 'abi_type_tuple':
+            # TODO add tuple TypedArgs
+            return KEVM.typed_args([arg for arg in arg.args if type(arg) is KApply])
+        else:
+            return KApply('_,__EVM-ABI_TypedArgs_TypedArg_TypedArgs', [arg, res])
+
     @staticmethod
     def accounts(accts: list[KInner]) -> KInner:
         wrapped_accounts: list[KInner] = []

kevm-pyk/src/kontrol/solc_to_k.py

@@ -12,7 +12,7 @@
 from pyk.kast.kast import KAtt
 from pyk.kast.manip import abstract_term_safely
 from pyk.kast.outer import KDefinition, KFlatModule, KImport, KNonTerminal, KProduction, KRequire, KRule, KTerminal
-from pyk.prelude.kbool import TRUE, andBool
+from pyk.prelude.kbool import andBool
 from pyk.prelude.kint import intToken
 from pyk.prelude.string import stringToken
 from pyk.utils import FrozenDict, hash_str, run_process, single
@@ -65,15 +65,50 @@ def solc_to_k(
     return _kprint.pretty_print(bin_runtime_definition, unalias=False) + '\n'
 
 
+@dataclass(frozen=True)
+class Input:
+    name: str
+    type: str
+    components: list[Input]
+
+    @staticmethod
+    def from_dict(_input: dict) -> Input:
+        name = _input['name']
+        type = _input['type']
+        if _input.get('components') is not None and _input['type'] != 'tuple[]':
+            return Input(name, type, Input.recurse_comp(_input['components']))
+        else:
+            return Input(name, type, [])
+
+    @staticmethod
+    def recurse_comp(components: dict) -> list[Input]:
+        comps = []
+        for comp in components:
+            _name = comp['name']
+            _type = comp['type']
+            if comp.get('components') is not None and type != 'tuple[]':
+                new_comps = Input.recurse_comp(comp['components'])
+            else:
+                new_comps = []
+            comps.append(Input(_name, _type, new_comps))
+        return comps
+
+    def to_abi(self) -> KApply:
+        if self.type == 'tuple':
+            tup, _ = Contract.recurse_components(self.components, 0)
+            return tup
+        else:
+            return Contract.make_single_type(self, 0)
+
+
 @dataclass
 class Contract:
     @dataclass
     class Method:
         name: str
         id: int
         sort: KSort
-        arg_names: tuple[str, ...]
-        arg_types: tuple[str, ...]
+        inputs: list[Input]
         contract_name: str
         contract_digest: str
         contract_storage_digest: str
@@ -95,8 +130,11 @@ def __init__(
             self.signature = msig
             self.name = abi['name']
             self.id = id
-            self.arg_names = tuple([f'V{i}_{input["name"].replace("-", "_")}' for i, input in enumerate(abi['inputs'])])
-            self.arg_types = tuple([input['type'] for input in abi['inputs']])
+            # nest_inputs = [Input.from_dict(input) for input in abi['inputs']]
+            # inputs = [input for inputs in nest_inputs for input in inputs]
+            self.inputs = [Input.from_dict(input) for input in abi['inputs']]
+            self.arg_names = tuple([f'V{i}_{input.name.replace("-", "_")}' for i, input in enumerate(self.inputs)])
+            self.arg_types = tuple([input.type for input in self.inputs])
             self.contract_name = contract_name
             self.contract_digest = contract_digest
             self.contract_storage_digest = contract_storage_digest
@@ -192,19 +230,27 @@ def rule(self, contract: KInner, application_label: KLabel, contract_name: str)
             arg_vars = [KVariable(aname) for aname in self.arg_names]
             prod_klabel = self.unique_klabel
             assert prod_klabel is not None
-            args: list[KInner] = []
+            args: list[KApply] = []
             conjuncts: list[KInner] = []
-            for input_name, input_type in zip(self.arg_names, self.arg_types, strict=True):
-                args.append(KEVM.abi_type(input_type, KVariable(input_name)))
-                rp = _range_predicate(KVariable(input_name), input_type)
-                if rp is None:
-                    _LOGGER.info(
-                        f'Unsupported ABI type for method {contract_name}.{prod_klabel.name}, will not generate calldata sugar: {input_type}'
-                    )
-                    return None
-                conjuncts.append(rp)
+            for input in self.inputs:
+                abi_type = input.to_abi()
+                args.append(abi_type)
+                rps = _range_predicates(abi_type)
+                for rp in rps:
+                    if rp is None:
+                        # TODO infer a type
+                        _LOGGER.info(
+                            f'Unsupported ABI type for method {contract_name}.{prod_klabel.name}, will not generate calldata sugar:'
+                        )
+                        return None
+                    conjuncts.append(rp)
             lhs = KApply(application_label, [contract, KApply(prod_klabel, arg_vars)])
             rhs = KEVM.abi_calldata(self.name, args)
+            if contract_name == 'CounterTest':
+                print(self.inputs)
+                print(args)
+                print(lhs)
+                print(rhs)
             ensures = andBool(conjuncts)
             return KRule(KRewrite(lhs, rhs), ensures=ensures)
 
@@ -479,6 +525,30 @@ def method_sentences(self) -> list[KSentence]:
         res.extend(method.selector_alias_rule for method in self.methods)
         return res if len(res) > 1 else []
 
+    @staticmethod
+    def make_single_type(input: Input, i: int) -> KApply:
+        input_name = f'V{i}_{input.name.replace("-", "_")}'
+        input_type = input.type
+        return KEVM.abi_type(input_type, KVariable(input_name))
+
+    @staticmethod
+    def recurse_components(components: list[Input], i: int) -> tuple[KApply, int]:
+        """
+        do a recursive build of types if this is a tuple
+        """
+        abi_types = []
+        for comp in components:
+            # nested tuple
+            if comp.type == 'tuple':
+                tup, j = Contract.recurse_components(comp.components, i)
+                i = j
+                abi_type = tup
+            else:
+                abi_type = Contract.make_single_type(comp, i)
+                i += 1
+            abi_types.append(abi_type)
+        return (KEVM.abi_tuple(abi_types), i)
+
     @property
     def field_sentences(self) -> list[KSentence]:
         prods: list[KSentence] = [self.subsort_field]
@@ -620,7 +690,24 @@ def _evm_base_sort_int(type_label: str) -> bool:
     return success
 
 
-def _range_predicate(term: KInner, type_label: str) -> KInner | None:
+def _range_predicates(abi: KApply) -> list[KApply | None]:
+    rp: list[KApply | None] = []
+    if abi.label.name == 'abi_type_tuple':
+        for arg in abi.args:
+            if type(arg) is KApply:
+                rp += _range_predicates(arg)
+    else:
+        if abi.label.name == 'abi_type_tuple':
+            for arg in abi.args:
+                if type(arg) is KApply:
+                    rp += _range_predicates(arg)
+        else:
+            type_label = abi.label.name.removeprefix('abi_type_')
+            rp.append(_range_predicate(single(abi.args), type_label))
+    return rp
+
+
+def _range_predicate(term: KInner, type_label: str) -> KApply | None:
     match type_label:
         case 'address':
             return KEVM.range_address(term)
@@ -629,7 +716,7 @@ def _range_predicate(term: KInner, type_label: str) -> KInner | None:
         case 'bytes':
             return KEVM.range_uint(128, KEVM.size_bytes(term))
         case 'string':
-            return TRUE
+            return KEVM.range_uint(128, KEVM.size_bytes(term))
 
     predicate_functions = [
         _range_predicate_uint,
@@ -646,7 +733,7 @@ def _range_predicate(term: KInner, type_label: str) -> KInner | None:
     return None
 
 
-def _range_predicate_uint(term: KInner, type_label: str) -> tuple[bool, KInner | None]:
+def _range_predicate_uint(term: KInner, type_label: str) -> tuple[bool, KApply | None]:
     if type_label.startswith('uint') and not type_label.endswith(']'):
         if type_label == 'uint':
             width = 256
@@ -659,7 +746,7 @@ def _range_predicate_uint(term: KInner, type_label: str) -> tuple[bool, KInner |
         return (False, None)
 
 
-def _range_predicate_int(term: KInner, type_label: str) -> tuple[bool, KInner | None]:
+def _range_predicate_int(term: KInner, type_label: str) -> tuple[bool, KApply | None]:
     if type_label.startswith('int') and not type_label.endswith(']'):
         if type_label == 'int':
             width = 256
@@ -672,7 +759,7 @@ def _range_predicate_int(term: KInner, type_label: str) -> tuple[bool, KInner |
         return (False, None)
 
 
-def _range_predicate_bytes(term: KInner, type_label: str) -> tuple[bool, KInner | None]:
+def _range_predicate_bytes(term: KInner, type_label: str) -> tuple[bool, KApply | None]:
     if type_label.startswith('bytes') and not type_label.endswith(']'):
         str_width = type_label[5:]
         if str_width != '':

kevm-pyk/src/tests/integration/test-data/foundry-prove-all

@@ -293,3 +293,4 @@ IntTypeTest.test_uint256(uint256)
 IntTypeTest.test_uint256_fail(uint256)
 IntTypeTest.test_uint64(uint64)
 IntTypeTest.test_uint64_fail(uint64)
+StructTypeTest.test_vars((uint8,bytes32,uint32))

kevm-pyk/src/tests/integration/test-data/foundry/test/TypeTest.t.sol

@@ -564,3 +564,18 @@ contract BytesTypeTest {
         assert(type(uint32).max > uint32(x));
     }
 }
+
+
+contract StructTypeTest {
+    struct Vars {
+        uint8 a;
+        bytes32 slot;
+        uint32 timestamp;
+    }
+
+    function test_vars(Vars calldata vars) public pure {
+        assert(type(uint8).max >= vars.a);
+        assert(type(bytes32).max >= vars.slot);
+        assert(type(uint32).max >= vars.timestamp);
+    }
+}