Consider removing array sizes from their types.

[otrho]

We currently store the size of an array in the type a couple of ways -- with a range: Option<ExprKey> and with size: Option<i64>. Both are obviously optional and we may easily have an array type with unknown size.

Soon we'll add support explicitly for 'variable' or essentially unknown sized arrays for which the size is known only at runtime. The size will be fixed and not actually variable, but only known at runtime.

Currently two arrays of different size have the same type, i.e., int[2] is the same as int[222].

Having the size in the type is useful for bounds checking and confirming correct behaviours when using a valueless union (aka an enum) as the indexing range. But it adds a lot of complexity to the type system -- it's the only reason Type has a dependency on ExprKey -- and it makes managing expressions much more complex. Not only do we need to worry about exprs in const declarations, predicate parameters, let expressions and constraints, but also in any of their types, just in case they are arrays. (But even then only optionally.)

I think that given we'll have explicitly unknown sized arrays coming soon and the above complexity, it makes sense to remove the array size from the type and for it to be stored only with the expression, if known. This would help the type checker -- consts wouldn't need to be evaluated especially before type checking -- and would simplify the backend or other places where the array size is required.

The only question I have is perhaps whether to remove the size from the language. Do we only allow an array type to be written as int[] or bool[][][] rather than having the explicit sizes? We will need to allow int[] style declarations for unknown sized arrays when they arrive, so perhaps we have all arrays declared as such?

When using these types, they can be optionally attached to const and let decls, but they always have a RHS initialiser, which will dictate the array size. let ary: int[] = [1, 2, 3] is explicitly a 3 element array, though its type doesn't know that.

Predicate parameters will need to allow unknown sized arrays anyway, so there is no initialiser and the length of the array is a runtime value. A len(ary) intrinsic will be used.

[mohammadfawaz]

I like how much this simplifies things.

One thing we lose though is predicate parameters that are arrays of fixed size as in:

predicate foo(a: int[3]) {

}

where we would have to add constraint that guarantees that the size of a in the solution is 3.

That being said, I think we could probably get around this by immediately converting this information as a constraint where the above would be transformed (by the compiler) to:

predicate foo(a: int[]) {
    constraint len(a) == 3;
}

So, the user would still encode size information between [..] but the compiler would move that information into a constraint. This can be done very early, even before type checking (or even by the parser like we used to do with initialized decision variables back in the days).

[otrho]

Hrmm, yep, it's tricky. The main point here is to remove the optional range and size from the array type. So having int[3] allowed sometimes means we'd have to store the size in the parameter itself somehow. This might not be a bad idea in general, to always have the param sizes pre-computed/available.

[mohammadfawaz]

I was just thinking we would turn the size information into a constraint right away.. the 3 above wouldn't even go into the type.. it would just become a constraint in the parser and its purpose is constraining the solution. So the 3 will not actually be used for compile-time OOB checks for example.

[otrho]

I was just thinking we would turn the size information into a constraint right away.. the 3 above wouldn't even go into the type.. it would just become a constraint in the parser and its purpose is constraining the solution. So the 3 will not actually be used for compile-time OOB checks for example.

Yikes, our parser already does waaay too much. I guess it's already just pushing constraints into the Predicate as they're parsed, but if ever we re-do the parser/macro system in the future this wouldn't be possible.

[mohammadfawaz]

Yeah that's true. Maybe it's one of those things that has to get resolved right after the initial ast is produced (which will have the size in the array type) but the next phase doesn't have the size in the type (it would be a different Type enum)