diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index d44a3faa5..260e36e45 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -217,6 +217,7 @@ 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: @@ -224,18 +225,33 @@ def flattened(self) -> list[Input]: 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 index acaeae372..a7807eba4 100644 --- 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 index 4096951c6..f161401aa 100644 --- 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 new file mode 100644 index 000000000..4835492d6 --- /dev/null +++ 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 index da05767bc..c967d5442 100644 --- 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 index dd1c6d260..a25645d37 100644 --- 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