Support for fixed arrays and structs as function parameters

[spencerhaoxiao]

1. Support fixed arrays as function arguments
2. Support the combination of, nested structs and multi-dimensional arrays and all their combinations
3. The predicate on an array argument is to add the relevant predicates on its element type.

[anvacaru]

Could you add some unit tests for this in https://github.com/runtimeverification/kontrol/blob/master/src/tests/unit/test_solc_to_k.py?

[palinatolmach]

@spencerhaoxiao could you please move a Solidity StructTest from #78 to this PR?

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

Line 569 in c40d8aa

contract StructTypeTest {

[palinatolmach]

As discussed with @anvacaru, we might want to remove references to array elements within #array and the rule generated for a test function accepting arrays as parameters — at the moment, the later looks like this (note that it doesn't kompile):

rule  ( S2KArrayTypeTest . S2KtestZUndstaticZUndarray ( V0_arr : uint256[3] ) => 
   #abiCallData ( "test_static_array" , #array ( #uint256 ( V0_arr_0_ ) , 3:Int , #uint256 ( V0_arr_0_ ) , #uint256 ( V0_arr_1_ ) , #uint256 ( V0_arr_2_ ) , .TypedArgs ) , .TypedArgs ) )
    ensures ( #rangeUInt ( 256 , V0_arr_0_ )
    andBool ( #rangeUInt ( 256 , V0_arr_1_ )
    andBool ( #rangeUInt ( 256 , V0_arr_2_ )
   )))

Referencing array elements is impractical for dynamically-sized arrays or statically-sized ones with a large number of elements. This, however, would make generation of range predicates for elements less straightforward, so I'll continue the investigation on it.

[palinatolmach]

Based on a discussion with @anvacaru and @PetarMax: for static arrays, we should try adding array elements to the left-hand side too.

[palinatolmach]

As @anvacaru has suggested, we'll proceed in three different directions: we will

• factor out struct support as implemented in Support for user-defined struct #78 back to merge it sooner
• attempt adding support for dynamic arrays by allowing calldata to be symbolic
• continue working on statically-sized array support as proposed in this PR, i.e., involving references to the elements of the array in the rules generated in solc_to_k,

in this order.

[anvacaru]

I'm closing this due to staleness.