Asymmetric handling of br_table and br_if with bot type

[gahaas]

With the recent change to introduce the bottom type, the validation rules for br_table changed. However, br_if did not get changed accordingly.

Consider the following two functions, the first function uses br_table, with one additional block to simulate the fall-through of br_if. The second function uses br_if directly.
(func (result f32)
(block (result f32)
(block (result i32)
unreachable
br_table 0 1 1
)
f32.convert_i32_u
)
)

(func (result f32)
(block (result f32)
unreachable
br_if 0
f32.convert_i32_u
)
)

The function with br_table validates, because the result type of the br_table instruction is BOT. The function with br_if, however, does not validate. For br_if the result type of the fall-through case is not considered when its result type is calculated.

Should we adjust the validation of br_if to match the validation of br_table?

[rossberg]

This is not specific to bottom, it applies to any subtyping.

The difference comes from the fact that br_table has (via the labels' blocks) an explicit type annotation for each of its continuations. For br_if there is no separate one for the fall-through case, so the one available is used for both out edges.

The same applies to other instructions that "fork" an operand from the stack, such as local.tee. We could relax all their typing rules and make them return the "original" type of the input, but it makes the rules slightly less simple. More importantly, by the same token we would then want to have an instruction like select return the lub of its inputs -- but that defeats the purpose of this change, so cannot be done.

So in a way, you'd be trading one small difference for a larger inconsistency.

[gahaas]

Would it be possible to define the result type of br_if and br_table not based on the types of the target blocks, but based on the input value that is popped from the stack? This type is always known, so we would not have to do a sub-type calculation.

[rossberg]

That's the alternative I just described, probably a bit obscured. That wouldn't work in all similar cases (esp. select), so would ultimately lead to a more severe inconsistency than the one you're pointing out.

Do you have a use case for this?

[gahaas]

Sorry, I should have read your reply more carefully.

I don't understand though why the validation rules of select should influence the validation rules of br_if. Also, with the introduction of the typed version of select I don't see why select is still a problem.

I don't have a use case for this. However, the difference between br_if and br_table seems un-intuitive. It's also a bit awkward to implement in V8. At the moment these instructions share the type checking. With the current proposal though we would have to treat these instructions differently,although intuitively they should just behave the same.

[rossberg]

The general scheme are instructions with typing rules of the form

C(...) = t
---------------------------------
C |- xxx : [...t...] -> [...t...]

This includes br_if but also local.tee, select, and probably a few others. Your proposal would be to change such rules to be covariant:

C(...) = t
t' <: t
-----------------------------------
C |- xxx : [...t'...] -> [...t'...]

However, this breaks down as soon as there are multiple occurrences of t' in the input type, as is the case with select. To remain consistent, the output type would then have to be their lub, avoiding which was the point of the exercise.

I'm not sure I see the problem with the V8 implementation. Looking at the code, it seems like all you'd have to do is popping the old argument(s) and pushing the refined type(s) at the end of the ExprBrIf case (see also the algorithm in the spec appendix). That may seem unnecessary from the perspective of your particular algorithm, but only when viewing the wider question through that particular lense.

[gahaas]

I have two use-cases for you. Assume you have 3 types A, B, C, with A is a sub-type of B, and B is a sub-type of C.
The following function with br_table should validate nicely.
(func (param A)(result C)
(block (result C)
(block (result B)
local.get 0
i32.const 0
br_table 0 1 1
)
B.someOp
)
)

The same function implemented with br_if does not validate.

(func (param A)(result C)
(block (result C)
local.get 0
i32.const 0
br_if 0
B.someOp
)
)

From a stack point of view, both version should validate. On top of the stack is a value of type A, which can be consumed both as type B and as type C.

Another use case is multi-inheritance. Assume types A, B, C, with A being a sub-type of B and C, but B and C are unrelated. Then the following function would not validate with the current proposal, although from a stack point of view it should. This is just a generalization of the current case with the BOT type I guess.

(func (param A)(result C)
(block (result C)
local.get 0
i32.const 0
br_if 0
B.someOp
)
)

[rossberg]

Sure, but these are synthetic use cases. I can easily construct analogous examples for the other instructions mentioned before, including select. But you don't seem to have issues with those. :)

From the point of view of the type system, this form of "covariance" is more involved, and it seems undesirable to introduce it in some cases but not the others, which is what we would have to do. So I prefer to stay on the conservative side, until it really proves too limited in practice.

[gahaas]

Thank you for the information. I adjusted my implementation now accordingly.