runtimeverification / kontrol

BSD 3-Clause "New" or "Revised" License
55 stars 9 forks source link

Array length for `tuple[]` might be set incorrectly in calldata #463

Closed palinatolmach closed 5 months ago

palinatolmach commented 8 months ago

While testing this PR, I found that while the following test is passing:

    /// @custom:kontrol-array-length-equals ctValues: 10,
    /// @custom:kontrol-bytes-length-equals content: 10000,
    function test_dynamic_struct_array(ComplexType[] calldata ctValues) public {
        require (ctValues.length == 10, "DynamicTypes: invalid length for ComplexType[]");
        assert(ctValues[9].content.length == 10000);
    }

A test that has ComplexType[] calldata ctValues followed by another dynamic type (bytes[] ba), doesn't pass:

    /// @custom:kontrol-array-length-equals ctValues: 10,
    /// @custom:kontrol-bytes-length-equals content: 10000,
    /// @custom:kontrol-array-length-equals ba: 10,
    /// @custom:kontrol-bytes-length-equals ba: 600,
    function test_complex_type_array(ComplexType[] calldata ctValues, bytes[] calldata ba) public {
        require (ctValues.length == 10, "DynamicTypes: invalid length for ComplexType[]");
        require (ba.length == 10, "DynamicTypes: invalid length for bytes[]");
        assert(ctValues[9].content.length == 10000);
        assert(ba[9].length == 600);
    }

Specifically, it seems to be failing the check on the length of ctValues:

require (ctValues.length == 10, "DynamicTypes: invalid length for ComplexType[]");

which means that the length for it might be located in the calldata incorrectly. I'll submit a separate issue on it. The test_complex_type_array test above is present in the test suite but is skipped.

Originally posted by @palinatolmach in https://github.com/runtimeverification/kontrol/issues/462#issuecomment-2003635558.

palinatolmach commented 5 months ago

Closed by https://github.com/runtimeverification/evm-semantics/pull/2455.