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

runtimeverification · Aug 29, 2024 · 3c82d1d · 3c82d1d
2 parents 9a663d7 + 24538ff
commit 3c82d1d
Show file tree

Hide file tree

Showing 6 changed files with 179 additions and 12 deletions.
diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py
@@ -217,25 +217,41 @@ def to_abi(self) -> KApply:
 
     def flattened(self) -> list[Input]:
         components = []
+        sub_components: tuple[Input, ...] = ()
 
         if self.type.endswith('[]'):
             if self.array_lengths is None:
                 raise ValueError(f'Array length bounds missing for {self.name}')
 
             base_type = self.type.rstrip('[]')
             if base_type == 'tuple':
-                components = [
-                    Input(
-                        f'{_c.name}_{i}',
-                        _c.type,
-                        _c.components,
-                        _c.idx,
-                        array_lengths=_c.array_lengths,
-                        dynamic_type_length=_c.dynamic_type_length,
-                    )
-                    for i in range(self.array_lengths[0])
-                    for _c in self.components
-                ]
+                for i in range(self.array_lengths[0]):
+                    for _c in self.components:
+                        # If this component is a tuple, append `_{i}` to its elements' names
+                        if _c.type == 'tuple':
+                            sub_components = tuple(
+                                Input(
+                                    f'{sub_component.name}_{i}',
+                                    sub_component.type,
+                                    sub_component.components,
+                                    sub_component.idx,
+                                    array_lengths=sub_component.array_lengths,
+                                    dynamic_type_length=sub_component.dynamic_type_length,
+                                )
+                                for sub_component in _c.components
+                            )
+                        else:
+                            sub_components = _c.components
+
+                        component = Input(
+                            f'{_c.name}_{i}',
+                            _c.type,
+                            sub_components,
+                            _c.idx,
+                            array_lengths=_c.array_lengths,
+                            dynamic_type_length=_c.dynamic_type_length,
+                        )
+                        components.append(component)
             else:
                 components = [Input(f'{self.name}_{i}', base_type, idx=self.idx) for i in range(self.array_lengths[0])]
         elif self.type == 'tuple':

diff --git a/src/tests/integration/test-data/foundry-prove-all b/src/tests/integration/test-data/foundry-prove-all
@@ -186,6 +186,7 @@ MockCallRevertTest.testMockCallEmptyAccount()
 MockFunctionTest.test_mock_function()
 MockFunctionTest.test_mock_function_all_args()
 MockFunctionTest.test_mock_function_concrete_args()
+NestedStructsTest.prove_fourfold_nested_struct(((((uint8,uint256),bytes32)[],bytes32)))
 OwnerUpOnlyTest.testFailIncrementAsNotOwner()
 OwnerUpOnlyTest.testIncrementAsNotOwner()
 OwnerUpOnlyTest.testIncrementAsOwner()

diff --git a/src/tests/integration/test-data/foundry-prove-skip-legacy b/src/tests/integration/test-data/foundry-prove-skip-legacy
@@ -183,6 +183,7 @@ MockCallRevertTest.testMockCallEmptyAccount()
 MockFunctionTest.test_mock_function()
 MockFunctionTest.test_mock_function_all_args()
 MockFunctionTest.test_mock_function_concrete_args()
+NestedStructsTest.prove_fourfold_nested_struct(((((uint8,uint256),bytes32)[],bytes32)))
 OwnerUpOnlyTest.testFailIncrementAsNotOwner()
 OwnerUpOnlyTest.testIncrementAsNotOwner()
 OwnerUpOnlyTest.testIncrementAsOwner()

diff --git a/src/tests/integration/test-data/foundry/test/NestedStructs.t.sol b/src/tests/integration/test-data/foundry/test/NestedStructs.t.sol
@@ -0,0 +1,34 @@
+// SPDX-License-Identifier: UNLICENSED
+pragma solidity =0.8.13;
+
+import "forge-std/Test.sol";
+
+contract NestedStructsTest is Test {
+    struct Processor {
+        Window windows;
+    }
+
+    struct Window {
+        Frame[] frames;
+        bytes32 hash;
+    }
+
+    struct Frame {
+        Pointer position;
+        bytes32 root;
+    }
+
+    struct Pointer {
+        PointerType pointerType;
+        uint256 value;
+    }
+
+    enum PointerType {
+        INT32,
+        INT64
+    }
+
+    function prove_fourfold_nested_struct(Processor calldata initialProcessor) external pure {
+        assert(initialProcessor.windows.frames.length == 2);
+    }
+}
diff --git a/src/tests/integration/test-data/show/contracts.k.expected b/src/tests/integration/test-data/show/contracts.k.expected
@@ -8301,6 +8301,113 @@ module S2KsrcZModMyToken-CONTRACT
     rule  ( selector ( "token()" ) => 4228666474 )
 
 
+endmodule
+
+module S2KtestZModNestedStructsTest-CONTRACT
+    imports public FOUNDRY
+
+    syntax Contract ::= S2KtestZModNestedStructsTestContract
+
+    syntax S2KtestZModNestedStructsTestContract ::= "S2KtestZModNestedStructsTest" [symbol("contract_test%NestedStructsTest")]
+
+    syntax Bytes ::= S2KtestZModNestedStructsTestContract "." S2KtestZModNestedStructsTestMethod [function, symbol("method_test%NestedStructsTest")]
+
+    syntax S2KtestZModNestedStructsTestMethod ::= "S2KISZUndTEST" "(" ")" [symbol("method_test%NestedStructsTest_S2KISZUndTEST_")]
+
+    syntax S2KtestZModNestedStructsTestMethod ::= "S2KexcludeArtifacts" "(" ")" [symbol("method_test%NestedStructsTest_S2KexcludeArtifacts_")]
+
+    syntax S2KtestZModNestedStructsTestMethod ::= "S2KexcludeContracts" "(" ")" [symbol("method_test%NestedStructsTest_S2KexcludeContracts_")]
+
+    syntax S2KtestZModNestedStructsTestMethod ::= "S2KexcludeSenders" "(" ")" [symbol("method_test%NestedStructsTest_S2KexcludeSenders_")]
+
+    syntax S2KtestZModNestedStructsTestMethod ::= "S2Kfailed" "(" ")" [symbol("method_test%NestedStructsTest_S2Kfailed_")]
+
+    syntax S2KtestZModNestedStructsTestMethod ::= "S2KproveZUndfourfoldZUndnestedZUndstruct" "(" Int ":" "uint8" "," Int ":" "uint256" "," Int ":" "bytes32" "," Int ":" "uint8" "," Int ":" "uint256" "," Int ":" "bytes32" "," Int ":" "bytes32" ")" [symbol("method_test%NestedStructsTest_S2KproveZUndfourfoldZUndnestedZUndstruct_uint8_uint256_bytes32_uint8_uint256_bytes32_bytes32")]
+
+    syntax S2KtestZModNestedStructsTestMethod ::= "S2KtargetArtifactSelectors" "(" ")" [symbol("method_test%NestedStructsTest_S2KtargetArtifactSelectors_")]
+
+    syntax S2KtestZModNestedStructsTestMethod ::= "S2KtargetArtifacts" "(" ")" [symbol("method_test%NestedStructsTest_S2KtargetArtifacts_")]
+
+    syntax S2KtestZModNestedStructsTestMethod ::= "S2KtargetContracts" "(" ")" [symbol("method_test%NestedStructsTest_S2KtargetContracts_")]
+
+    syntax S2KtestZModNestedStructsTestMethod ::= "S2KtargetSelectors" "(" ")" [symbol("method_test%NestedStructsTest_S2KtargetSelectors_")]
+
+    syntax S2KtestZModNestedStructsTestMethod ::= "S2KtargetSenders" "(" ")" [symbol("method_test%NestedStructsTest_S2KtargetSenders_")]
+
+    rule  ( S2KtestZModNestedStructsTest . S2KISZUndTEST ( ) => #abiCallData ( "IS_TEST" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModNestedStructsTest . S2KexcludeArtifacts ( ) => #abiCallData ( "excludeArtifacts" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModNestedStructsTest . S2KexcludeContracts ( ) => #abiCallData ( "excludeContracts" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModNestedStructsTest . S2KexcludeSenders ( ) => #abiCallData ( "excludeSenders" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModNestedStructsTest . S2Kfailed ( ) => #abiCallData ( "failed" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModNestedStructsTest . S2KproveZUndfourfoldZUndnestedZUndstruct ( V0_pointerType_0 : uint8 , V1_value_0 : uint256 , V1_root_0 : bytes32 , V0_pointerType_1 : uint8 , V1_value_1 : uint256 , V1_root_1 : bytes32 , V2_hash : bytes32 ) => #abiCallData ( "prove_fourfold_nested_struct" , ( #tuple ( ( #tuple ( ( #array ( #tuple ( ( #tuple ( ( #uint8 ( V0_pointerType_0 ) , ( #uint256 ( V1_value_0 ) , .TypedArgs ) ) ) , ( #bytes32 ( V1_root_0 ) , .TypedArgs ) ) ) , 2 , ( #tuple ( ( #tuple ( ( #uint8 ( V0_pointerType_0 ) , ( #uint256 ( V1_value_0 ) , .TypedArgs ) ) ) , ( #bytes32 ( V1_root_0 ) , .TypedArgs ) ) ) , ( #tuple ( ( #tuple ( ( #uint8 ( V0_pointerType_1 ) , ( #uint256 ( V1_value_1 ) , .TypedArgs ) ) ) , ( #bytes32 ( V1_root_1 ) , .TypedArgs ) ) ) , .TypedArgs ) ) ) , ( #bytes32 ( V2_hash ) , .TypedArgs ) ) ) , .TypedArgs ) ) , .TypedArgs ) ) )
+       ensures ( #rangeUInt ( 8 , V0_pointerType_0 )
+       andBool ( #rangeUInt ( 256 , V1_value_0 )
+       andBool ( #rangeBytes ( 32 , V1_root_0 )
+       andBool ( #rangeUInt ( 8 , V0_pointerType_1 )
+       andBool ( #rangeUInt ( 256 , V1_value_1 )
+       andBool ( #rangeBytes ( 32 , V1_root_1 )
+       andBool ( #rangeBytes ( 32 , V2_hash )
+               )))))))
+
+
+    rule  ( S2KtestZModNestedStructsTest . S2KtargetArtifactSelectors ( ) => #abiCallData ( "targetArtifactSelectors" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModNestedStructsTest . S2KtargetArtifacts ( ) => #abiCallData ( "targetArtifacts" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModNestedStructsTest . S2KtargetContracts ( ) => #abiCallData ( "targetContracts" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModNestedStructsTest . S2KtargetSelectors ( ) => #abiCallData ( "targetSelectors" , .TypedArgs ) )
+
+
+    rule  ( S2KtestZModNestedStructsTest . S2KtargetSenders ( ) => #abiCallData ( "targetSenders" , .TypedArgs ) )
+
+
+    rule  ( selector ( "IS_TEST()" ) => 4202047188 )
+
+
+    rule  ( selector ( "excludeArtifacts()" ) => 3041954473 )
+
+
+    rule  ( selector ( "excludeContracts()" ) => 3792478065 )
+
+
+    rule  ( selector ( "excludeSenders()" ) => 517440284 )
+
+
+    rule  ( selector ( "failed()" ) => 3124842406 )
+
+
+    rule  ( selector ( "prove_fourfold_nested_struct(((((uint8,uint256),bytes32)[],bytes32)))" ) => 1548118009 )
+
+
+    rule  ( selector ( "targetArtifactSelectors()" ) => 1725540768 )
+
+
+    rule  ( selector ( "targetArtifacts()" ) => 2233625729 )
+
+
+    rule  ( selector ( "targetContracts()" ) => 1064470260 )
+
+
+    rule  ( selector ( "targetSelectors()" ) => 2439649222 )
+
+
+    rule  ( selector ( "targetSenders()" ) => 1046363171 )
+
+
 endmodule
 
 module S2KtestZModNoImport-CONTRACT

diff --git a/src/tests/integration/test-data/show/foundry.k.expected b/src/tests/integration/test-data/show/foundry.k.expected
@@ -99,6 +99,7 @@ module FOUNDRY-MAIN
     imports public S2KtestZModModelMockFunctionContract-VERIFICATION
     imports public S2KsrcZModMyIERC20-VERIFICATION
     imports public S2KsrcZModMyToken-VERIFICATION
+    imports public S2KtestZModNestedStructsTest-VERIFICATION
     imports public S2KtestZModNoImport-VERIFICATION
     imports public S2KsrcZModcseZModUIntBinaryOp-VERIFICATION
     imports public S2KsrcZModcseZModUIntUnaryOp-VERIFICATION
@@ -820,6 +821,13 @@ module S2KsrcZModMyToken-VERIFICATION
 
 
 
+endmodule
+
+module S2KtestZModNestedStructsTest-VERIFICATION
+    imports public S2KtestZModNestedStructsTest-CONTRACT
+
+
+
 endmodule
 
 module S2KtestZModNoImport-VERIFICATION