Functions with array arguments give "Unsupported ABI type for method` error

[lucasmt]

The function _range_predicate in solc_to_k.py does not support array types. As a result, if we try to foundry-kompile a function such as

function testArray(address[] memory array) public {
	assert(true);
}

that has an array as argument, we get the message Unsupported ABI type for method TestContract.method_TestContract_testArray_address[], will not generate calldata sugar: address[], and no rule of the form

rule  ( TestContract . testArray ( ... ) => #abiCallData ( ... ) )

is added to foundry.k. This makes it so that the function cannot be evaluated during symbolic execution. If we try to run kevm foundry-prove on this function, the execution just starts branching on conditions like

lengthBytes ( TestContract . testArray ( VV0_array_114b9705:K : address[] ) ) <Int 4

without ever stepping into the function.

[ehildenb]

From slack discussion with @iFrostizz :

Currently, when we have a function signature with types, we generate a rule that simplifies that function signature to its abi encoding, while at teh same time using an ensures clause to make sure the symbolic variables present are in the correct range: https://github.com/runtimeverification/evm-semantics/blob/a68c97a2280b7ac9f1fc81f142464d0a23793b8d/tests/foundry/contracts.k.check.expected#L80

This is an example generated rule for the KEVM foundry test-suite at tests/foundry
Those predicates in the ensures clause are generated by the _range_predicate thing you have linked above.
Currently, the logic there is "if it's a type we don't recognize directly, then return None, and don't generate the corresponnding rule with syntactic sugar".
Which means we can't write property tests about that function.

Here: https://github.com/runtimeverification/evm-semantics/blob/a68c97a2280b7ac9f1fc81f142464d0a23793b8d/kevm-pyk/src/kevm_pyk/solc_to_k.py#L15

We call _range_predicate to get the predicate used to constrain the symbolic value in the type.
And if it gives back None, then we just give up, and don't generate the overall rule.

I think there are two things we can do here:

• It's OK to still generate the rule itself, but leave the variable unconstrained, if the _range_predicate does not give back an appropriate predicate. This is less than ideal, because now you have an unconstrained variable, but,
• We can then make _range_predicate stronger, and able to handle more cases basically.

[lucasmt]

By the way, a similar issue also happens when a function has a struct argument.

[iFrostizz]

Partly fixed, please see runtimeverification/evm-semantics#1883 (comment) for reference.

[palinatolmach]

A related PR introducing support for structs: runtimeverification/evm-semantics#2051.

[palinatolmach]

Closed by #321.