Dynamic type support limitations

Native support for dynamic types (bytes and bytes[]) has been added in https://github.com/runtimeverification/kontrol/pull/321. However, we identified the following three limitations that should be addressed further:

1. A test with an array of tuples parameter is branching and failing

    struct ComplexType {
        uint256 id;
        bytes content;
    }

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

which is caused by the length of content not being set properly. The fix is needed is the rule function processing and applying length annotations:

            for input in self.inputs:
                abi_type = input.to_abi()
                args.append(abi_type)
                rps = []
                if input.type == 'tuple':
                    for sub_input in input.components:
                        _abi_type = sub_input.to_abi()
                        rps.extend(_range_predicates(_abi_type, sub_input.dynamic_type_length))
                else:
                    rps = _range_predicates(abi_type, input.dynamic_type_length)

2. test_dynamic_byte_read test is failing and should be rewritten to something that tests the byte reading functionality more accurately, e.g.,

    function test_dynamic_byte_read(bytes memory data, uint256 offset, bytes1 value) public {
        vm.assume(offset < data.length);
        data[offset] = value;
        assertTrue(data[offset] == value);
    }

as suggested by @anvacaru. This test branches on { true #Equals ( notBool #asWord ( #buf ( 63 , lengthBytes ( VV0_data_114b9705:Bytes ) ) ) <=Int maxUInt64 ) } too.

3. The modification of the test_complex_type test with offset being symbolic fails:

    /// @custom:kontrol-length-equals content: 10000,
    /// @custom:kontrol-length-equals ba: 10,
    /// @custom:kontrol-length-equals ba[]:600,
    function test_complex_type(ComplexType calldata ctValues, bytes[] calldata ba, uint256 offset) public {
        require (ba.length == 10, "DynamicTypes: invalid length for bytes[]");
        vm.assume(offset < 10);
        assert(ctValues.content.length == 10000);
        assert(ba[offset].length == 600);
    }

It branches on

━━┓ constraint: { true #Equals ( (#asWord ( #range ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x03\xc0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x06@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x08\xc0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x0b@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\r\xc0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x10@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x12\xc0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x15@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x17\xc0\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02X" , ( 32 *Int VV3_offset_114b9705:Int ) , 32 ) )) s<Word (6689) ) ==Int 0 }

Here, the bytes literal contains offsets for individual elements in the array. With the offset being symbolic, it doesn’t know which value (containing the offset to the individual element) out of 10 it has to read, so it can’t decide if it’s less than 6689 (all of them are, but they are not getting enumerated them).

Start with src/kontrol/solc_to_k.py, especially rule and its length-annotation handling, then run the DynamicTypes.t.sol integration tests under src/tests/integration/test-data/foundry/test. Compare the array-of-tuples, dynamic byte read, and symbolic-offset failures with the expected examples in the issue. Done means the tests exercise the intended behavior without the reported branching or failure.