Allow use of unchecked keyword to declare unchecked arrays?

[secure-sw-dev-bot]

This issue was copied from checkedc/checkedc#22

---

When an array declarator is declared to be checked, by default the checked property propagates to directly-nested array types. This is provided that the nested array types are declared as part of the declarator.

For example, int a checked[10][10]; declares a checked array of checked arrays. This should be thought of as syntactic shorthand for int a checked[10]checked[10]. In contrast, typedef int myarr[10]; myarr a checked[10] declares a checked array of unchecked arrays.

For the purposes of language completeness, it might be useful to allow programmers to declare an array to be unchecked. We don't recommend mixing checked arrays and unchecked arrays in multi-dimensional array declaration, but in incrementally converting code, the need for this come up. To do this, we might allow an array declarator to be prefixed by the 'unchecked' keyword.

[secure-sw-dev-bot]

Comment from @dtarditi:

I've thought some more about this and think that allowing checked arrays of unchecked arrays potentially introduces a lot of complexity into the language extension and understanding it. For the typedef case given above, it would be better to define that as a compile-time error.

Yes, this might put constraints on converting code. However, I'm guessing that the case of a multi-dimensional array being constructed via typedef's is rare. If people know of code that does this, I'd be interested in hear about that. If it is rare, the benefit of simplifying the language outweighs supporting this case.

The rules around multi-dimensional arrays are already subtle and complex. Allowing mixed checking just adds one more subtlety. As an example, consider the problems that we might run into subscripting the following variable.

int a checked[10]unchecked[10]

Suppose it is subscripted using a[k][m], where k and m are integer variables. This is equivalent to:
*(a[k] + m), which is equivalent to ((a + k) + m). Here is what might happen following the rules in the Checked C specification with the C11 rules for lvalue conversions:

1. a is converted to be a "checked pointer of an unchecked array of 5 integers".
2. a + k still has this type.
3. *(a + k) produces an lvalue that is an unchecked array of 5 integers. However, because *(a +k) has an array type, no lvalue conversion is performed (following the rules in Section 6.3.2.1 of the C11 specification). This means that *(a + k) does not actually access memory - it acts more like a type conversion.
4. Following the current rules in the Checked C specification, the unchecked array of 5 integers should be converted to be a "unchecked pointer to integers".
5. *(a + k) + m is an "unchecked pointer to integers".
6. When the expression in step 5 is dereferenced, there is no bounds checking.

[secure-sw-dev-bot]

Comment from @dtarditi:

The specification has been updated to explain how typedefs interact with the requirement that all dimensions of a multi-dimensional array either be checked or unchecked.