Asymmetric handling of br_table and br_if with bot type #48

Activity

1. rossberg commented on Jun 3, 2019

   

   rossberg

   on Jun 3, 2019

   Member

   More actions

   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.
2. gahaas commented on Jun 3, 2019

   

   gahaas

   on Jun 3, 2019

   ContributorAuthor

   More actions

   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.
3. rossberg commented on Jun 3, 2019

   

   rossberg

   on Jun 3, 2019

   Member

   More actions

   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?
4. gahaas commented on Jun 3, 2019

   

   gahaas

   on Jun 3, 2019

   ContributorAuthor

   More actions

   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.
5. rossberg commented on Jun 4, 2019

   

   rossberg

   on Jun 4, 2019

   Member

   More actions

   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.
6. gahaas commented on Jun 4, 2019

   

   gahaas

   on Jun 4, 2019

   ContributorAuthor

   More actions

   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
)
)
7. rossberg commented on Jun 4, 2019

   

   rossberg

   on Jun 4, 2019

   Member

   More actions

   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.
8. gahaas commented on Jun 12, 2019

   

   gahaas

   on Jun 12, 2019

   ContributorAuthor

   More actions

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

   closed this as completedon Jun 12, 2019
10. rossberg

    added a commit that references this issue on Nov 20, 2019

    Clarify *.{init,copy,fill} w/ zero count (#48)

    ...

    e27277d