Add 2nd type annotations on casts

[rossberg]

This specifies the changes to cast instructions as discussed, and implements them in interpreter and test suite. Also removes _canon suffixes.

Two points of note:

1. For the binary format, I tentatively went with a single opcode (0xfb4f) for all the variants of cast branches, followed by a flag byte currently carrying 3 bits: one for each nullability, and one for direction (_fail vs regular). This avoids allocating 8 separate opcodes (or 6, since 2 wouldn't validate) and also allows for later extensions without combinatorial explosion of opcodes. Makes more sense to me, but let's discuss if you think different.
2. I tweaked the text format to use regular reference type notation on cast instructions (e.g., ref.cast (ref null $t), br_on_cast $l anyref (ref $t)). This looks less weird, especially with the two annotations on branches, and it also conveniently allows using the shorthands.

Fixes #342 and supersedes PR #347.

[jakobkummerow]

0xfb4f is currently unused, so that's a good choice for a binary encoding that doesn't break ongoing test coverage for the various prototype implementations. (And of course we'll compact the encoding space once the proposal's instruction set is final.)

[titzer]

I think having taken/not taken (_fail vs regular) as separate opcodes would be helpful. I am also ok with encoding the null-handling as an immediate. I am also fine with 6 different opcodes.

[rossberg]

I still expect these to remain fairly cold instructions, so I'm not too worried about the byte. My bigger concern with 6 opcodes is that it doesn't scale well. If we add another dimension (say, RTTs ;) ) it already doubles to 12, and so on.

The other oddity is that by making 2 combinations syntactically unrepresentable, it's technically not two reftype immediates anymore, but something rather irregular.

[conrad-watt]

The other oddity is that by making 2 combinations syntactically unrepresentable, it's technically not two reftype immediates anymore, but something rather irregular.

This could be considered a feature. I do find it a little odd that, if we express the existing null-check flag as part of a reftype immediate, the semantics of the instruction changes based on that "internal" part of the type annotation.

[rossberg]

@conrad-watt, I'm not sure I follow. This has nothing to do with the operational behaviour. What I'm saying is that, although the abstract syntax is essentially br_on_cast rt1 rt2, there would in fact be some combinations of types that are prohibited syntactically, and not merely by the static type constraint rt2 <: rt1 like all others. That is a phasing conflation.

[conrad-watt]

I guess I'm trying to make a broader argument that it makes more sense for us to think, abstractly, of the operations being split up as follows:

br_on_cast lab null? ht ht br_on_cast_fail lab null? ht ht br_on_cast_nonnull lab ht ht br_on_cast_nonnull_fail lab ht ht

This is essentially what I sketched here but with an explicit second heap type annotation. My intuition is that this makes the semantic behaviour (dependent on the presence or absence of null?) and the refinement of the branch/non-branch output type easier to reason about.

I think if one instead rolls all of these cases inside the null? parts of two reftype annotations, one ends up with a bunch of side-conditions to distinguish each case (and refinement) that don't feel totally natural to me - i.e. the reftype annotations aren't really used as reftypes, but more like "heaptype with a helpful bool flag" (see also my review comment just above).

EDIT: and once you move away from the reftype conceptualisation of the instructions, i'd argue it makes sense to have at least 4, and arguably 6 separate instruction encodings.

[rossberg]

I have to disagree. This would be overcomplicating matters. The semantics is actually fairly simple and regular now:

• Dynamically, the instruction simply checks subtyping between two reference types: the dynamic one of the operand and the target type.

• Statically, it has an input type and two output types:

  • the output type of the success path is the annotated target type,
  • the output type of the failure path is the diff of input type and target type.

If we had more general union types, that diff would literally be a set-like diff. With our current algebra, null is the only element we can express individually, so the diff is approximate and only affects null.

[tlively]

Changes LGTM. FWIW I had previously viewed the reftype annotations as "heap types with helpful bools" as Conrad put it, but with two of them corresponding to the input and desired output, I actually think of them as reftypes now. I guess the weird part is that they're not encoded in the binary format using the normal reftype encoding, but I definitely wouldn't want the encoding to be any larger, so I'm glad we're not doing that. I don't feel too strongly about which of the current options we go with.

[Liedtke]

There are a few questions / concerns that came up while trying to add the new instruction to V8:

1) [Removed, I confused myself on the binary format for br_on_cast.] 2) Cast from non-nullable to nullable: As we have two null bits, it is possible to specify that the source type is non-nullable but the target type is nullable. In that case the validation type for the variant of a successful cast becomes nullable, correct? (Also meaning that this flag combination is not treated as a validation error.) 3) When casting from a nullable type to a nullable type using br_on_cast, the fall-through type becomes non-nullable, so the decoder refines the type to something more specific. However, this refinement only applies to the nullability, not to the heap type? Asked differently, when doing an upcast in a br_on_cast_fail e.g. from arrayref to anyref, the branch is de-facto unreachable as the cast can never fail. I assume that the branch signature still has to align with the source type as specified in the br_on_cast_fail immediates? (So the branch label has to be typed as arrayref or any supertype in this example.)

[tlively]

@rossberg, it would be good to get clarity on the proposed validation rules and how they are represented in the prose and binary format.

[rossberg]

Re (2): As you can see from the typing rule in the PR, it simply requires that for br_on_cast rt1 rt2, the second type is a subtype of the first -- because it's meant to be a downcast. From the subtyping rules for reference types it follows immediately that this will reject the case br_on_cast (ref $t1) (ref null $t2), because the latter type can never be a subtype of the former.

Re (3): Yes, the refinement only applies to nullability, since our type system isn't expressive enough to express any form of refinement on the heap type. Computing a meaningful type difference for such a refinement would only work for union types, which we do not have. Consequently, the type difference operation is an approximation that leaves the heap type unchanged.

I don't follow your question regarding an upcast. You neither can nor need to use br_on_cast for upcasts -- going from arrayref to anyref is just subsumption (implicit use of subtyping), so never requires a cast, nor could it ever fail.

[Liedtke]

@rossberg Thanks for clarifying! I didn't notice the semantic change that the target type has to be a subtype of the source type immediate as previously the type on the value stack only had to be in the same type hierarchy. I wrongly assumed "If I use the type on the value stack as the source type immediate (rt1), there isn't any difference to the old behavior".

[rossberg]

Right, with the old typing, the situation was more complicated, because we needed to allow sufficient flexibility in the typing rule to maintain type preservation under reduction. With an explicit type annotation, it all is much simpler.

By ordinary subtyping, the actual stack operand can of course still be a subtype of the input annotation -- and therefor a super-, sub-, or even sibling type of the target. So it is no less expressive than before. But you have to pick a suitable input type annotation that is a common supertype.

[eqrion]

If I understand this right, there will be one binary opcode for br_on_cast, but two text format 'tokens' br_on_cast and br_on_cast_fail.

I wonder if it would be more regular to move the on_fail part to be a text format immediate like br_on_cast onfail=true. The only other precedent I know of for a non 1:1 text token to binary opcode is select, but that's a single text token that has two different opcodes.

I don't think it's a big deal either way, but it would seem nice to keep this regular and have the text format resemble the binary as close as we can.

[rossberg]

@eqrion, yes, I'd be fine with making the distinction via some separate token if others feel strongly about it.

[tlively]

I would also prefer that we use a single instruction name if we are going to use a single opcode. This will improve error messages in V8 (without complicating their existing code) as well.

[tlively]

We decided at the meeting this morning to use two different opcodes for the fail and non-fail cases.

[rossberg]

Done.

[tlively]

@Liedtke and @jakobkummerow, will we be able to implement these new opcodes (0x4e and 0x4f for br_on_cast and br_on_cast_fail) directly? Binaryen hadn't yet implemented the previous encoding, so this will not be a breaking change for any Binaryen users.

[Liedtke]

@tlively Yes, because binaryen didn't implement it and this PR hasn't been merged yet, we went ahead and implemented the new opcode and updated decoding for 0x4f without a fallback today. (If required we could allow the old fail bit in the flags byte to "switch" the opcode from 0x4f to 0x4e.)