Merge remote-tracking branch 'origin/master' into release

runtimeverification · Nov 26, 2024 · 8beb0d5 · 8beb0d5
2 parents 865beb5 + 27e4914
commit 8beb0d5
Show file tree

Hide file tree

Showing 3 changed files with 36 additions and 10 deletions.
diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py
@@ -818,11 +818,13 @@ def process_references(bytecode: dict, target_lib_refs: dict, update_link_ranges
         self.constructor = None
 
         contract_ast_nodes = [
-            node
+            (node, node.get('contractKind'))
             for node in self.contract_json['ast']['nodes']
             if node['nodeType'] == 'ContractDefinition' and node['name'] == self._name
         ]
-        contract_ast = single(contract_ast_nodes) if len(contract_ast_nodes) > 0 else {'nodes': []}
+        contract_ast, contract_kind = (
+            single(contract_ast_nodes) if len(contract_ast_nodes) > 0 else ({'nodes': []}, None)
+        )
         function_asts = {
             node['functionSelector']: node
             for node in contract_ast['nodes']
@@ -843,7 +845,7 @@ def process_references(bytecode: dict, target_lib_refs: dict, update_link_ranges
 
         for method in contract_json['abi']:
             if method['type'] == 'function':
-                msig = method_sig_from_abi(method)
+                msig = method_sig_from_abi(method, contract_kind == 'library')
                 method_selector: str = str(evm['methodIdentifiers'][msig])
                 mid = int(method_selector, 16)
                 method_ast = function_asts[method_selector] if method_selector in function_asts else {}
@@ -1334,7 +1336,7 @@ def _range_predicate_bytes(term: KInner, type_label: str) -> tuple[bool, KApply
     return (False, None)
 
 
-def method_sig_from_abi(method_json: dict) -> str:
+def method_sig_from_abi(method_json: dict, is_library: bool = False) -> str:
     def unparse_input(input_json: dict) -> str:
         array_sizes = []
         base_type = input_json['type']
@@ -1343,12 +1345,16 @@ def unparse_input(input_json: dict) -> str:
             array_sizes.append(array_size_str if array_size_str != '' else '')
             base_type = base_type.rpartition('[')[0]
         if base_type == 'tuple':
-            input_type = '('
-            for i, component in enumerate(input_json['components']):
-                if i != 0:
-                    input_type += ','
-                input_type += unparse_input(component)
-            input_type += ')'
+            # If the contract is a library, structs are not unpacked
+            if not is_library:
+                input_type = '('
+                for i, component in enumerate(input_json['components']):
+                    if i != 0:
+                        input_type += ','
+                    input_type += unparse_input(component)
+                input_type += ')'
+            else:
+                input_type = input_json['internalType'].split(' ')[1]
         else:
             input_type = base_type
         for array_size in reversed(array_sizes):

diff --git a/src/tests/integration/test-data/foundry/test/ExternalLibTest.t.sol b/src/tests/integration/test-data/foundry/test/ExternalLibTest.t.sol
@@ -4,6 +4,15 @@ pragma solidity =0.8.13;
 import "forge-std/Test.sol";
 
 library SimpleMath {
+    struct LibStruct {
+        uint256 elementOne;
+        address elementTwo;
+    }
+
+    function structInput(LibStruct memory s) public pure returns (uint256) {
+        return s.elementOne;
+    }
+
     function square(uint256 x) public pure returns (uint256) {
         return x * x;
     }

diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected
@@ -4931,12 +4931,23 @@ module S2KtestZModSimpleMath-CONTRACT
 
     syntax S2KtestZModSimpleMathMethod ::= "S2Ksquare" "(" Int ":" "uint256" ")" [symbol("method_test%SimpleMath_S2Ksquare_uint256")]
 
+    syntax S2KtestZModSimpleMathMethod ::= "S2KstructInput" "(" Int ":" "uint256" "," Int ":" "address" ")" [symbol("method_test%SimpleMath_S2KstructInput_uint256_address")]
+
     rule  ( S2KtestZModSimpleMath . S2Ksquare ( KV0_x : uint256 ) => #abiCallData ( "square" , ( #uint256 ( KV0_x ) , .TypedArgs ) ) )
        ensures #rangeUInt ( 256 , KV0_x )
 
 
+    rule  ( S2KtestZModSimpleMath . S2KstructInput ( KV0_elementOne : uint256 , KV1_elementTwo : address ) => #abiCallData ( "structInput" , ( #tuple ( ( #uint256 ( KV0_elementOne ) , ( #address ( KV1_elementTwo ) , .TypedArgs ) ) ) , .TypedArgs ) ) )
+       ensures ( #rangeUInt ( 256 , KV0_elementOne )
+       andBool ( #rangeAddress ( KV1_elementTwo )
+               ))
+
+
     rule  ( selector ( "square(uint256)" ) => 2066295049 )
 
+
+    rule  ( selector ( "structInput(SimpleMath.LibStruct)" ) => 1313163024 )
+
 
 endmodule