Understanding the post-drop block/br type system

[kripken]

Looks like the drop changes in 0xc change the block/br type system significantly. I've been trying to figure out what's going on from the new spec tests, but can't seem to. Is this documented somewhere?

For example, one source of puzzlement is that this should be invalid

(block $block1
  (br $block1
    (unreachable)
  )
) 

Intuitively that seems like it should be valid, as no value is sent to the block? So I can only guess it is invalid because the type of unreachable is unacceptable here. Yet, on the other hand this should be valid,

(block $block1
  (br $block1
    (br $block0
      (i32.const 8)
    )
  )
)

So somehow the type of br is different from the type of unreachable? That seems odd as both halt control flow.

[kripken]

To be specific, those examples are from the tests in the test repo's binary-0xc branch.

[kripken]

Which is identical to the spec repo's branch of the same name.

[binji]

Are you talking about the as-br-value tests in unreachable.wast and br.wast?

[kripken]

They are from br.wast. I go through them sequentially in alphabetical order. It'll be a while before I get to 'u' for unreachable ;) But I do have block.wast passing.

[binji]

Ah, I see. unreachable.wast has a similar test, but it validates:

  ;; unreachable.wast
  (func "as-br-value" (result i32)
    (block (br 0 (unreachable)))
  )
---
;; br.wast
(assert_invalid
  (module (func $type-arg-poly-vs-empty
    (block (br 0 (unreachable)))
  ))
  "arity mismatch"
)

AIUI, the idea is that if a br has a value argument, then the target block must either use the value or drop it. The fact that the value expression is unreachable doesn't matter, since unreachable can be used in place of any type.

(block $block1
  (br $block1
    (br $block0
      (i32.const 8)
    )
  )
)

This one doesn't make sense in isolation. Is there supposed to be a $block0 wrapping this, or is it a typo of this test from br.wast?

  (func "as-br-value" (result i32)
    (block (br 0 (br 0 (i32.const 9))))
  )

[kripken]

(The first example is from type-arg-poly-vs-empty, and the second is reduced from nested-br-value - yes, there is an outer block.)

Ok, thanks, the unreachable's type was confusing me perhaps. If I follow you, then it looks like the type system has gotten more complex and now an additional internal type is needed? What I mean is that before, binaryen had

• i32, etc., the "concrete" normal types
• unreachable, the type of unreachable, br, etc.. That is a type that vanishes when merged with other types, e.g. if one arm of an if is unreachable while the other is an i32, the combined merged type of the if is i32.
• none, the type of e.g. store and set_local (after we made them not return a value), values of this type must not be consumed. E.g. if one arm of an if has this type, then no matter the type of the other, the if will have this type (and must not be consumed).

Those types appear to no longer be sufficient, as if I understand things now, then (block (br 0 (unreachable))) must be dropped, and neither of unreachable and none require that? In other words a new type like this must be added,

• dropme, a type that can only be consumed by drop, and in fact must be consumed by it.

Is that correct?

[titzer]

For the stack machine, we made the decision not to typecheck unreachable code. That's not really an undue burden on the V8 and SM implementations, since they already modeled reachability for SSA renaming. For binaryen, I assume this is an additional thing to check.

I'm not entirely sure that one can easily model the reachability requirement with types alone. Instead it is state attached to each block and to the current "stack".

[kripken]

I see. In that case, maybe it makes more sense for binaryen to just jump to that state, instead of trying to get to where binary-0xc is right now? (which looks like post-drop but pre-full stack machine) Unless that's far off.

@rossberg-chromium, when do you expect ml-proto's binary-0xc branch to get to the final state of full stack machine / not typechecking unreachable code etc.?

[kripken]

(Or is there already another branch somewhere that is at that point?)

[titzer]

0xC will be updated to be the full stack machine over the next few days.

[titzer]

(in the design repo)

[binji]

I think I was confused about this too, not sure what the differences a "full stack machine" means for the type system.

[titzer]

Some details are available in this slide deck: https://docs.google.com/presentation/d/1dRsN5lKY60d3IOILi4bttJXOX4ge-2tA1PaEX-d5So0/edit#slide=id.p

But I think @rossberg-chromium 's rules will make it easier to see.

@titzer Interesting slide thank you. It claims to support multiple values, which is any area of concern for me.

So this seems to extend the break operators to be able to pick a number of values from the top of the stack and retain these at the exit of the target block while discarding the other values in the block?

The problem is that it is not possible to access the multiple values from a call. For example it is not possible to drop the top-of-stack value to expose the next value. Perhaps the proposal is to remove that restriction on drop too?

It is not even possible to store these values in local variables as the set_local operator returns no values so would be invalid while the other values are still on the stack.

Fwiw I believe that any re-arranging of values on the values stack is compatible with an expression based presentation. This can be demonstrated with a pick operator that chooses values from the values stack, popping them all, and then pushing some back in a different order.

The other show stopper is that the 's-expression syntax breaks down for stack machine', or in other words it is not presentable in an expression based format. There might be ways to work around that with canonicalization, but I have not worked through it all.

So it still appears to me that the proposal is not tenable and might not meet the expectations of the web community.

It really does not seem a big burden to keep the void values on the values stack. As I suggested long ago this could be done efficiently by keeping a counter of them in a stack location, so the stack entry would be void <n>. We could then adopt the get_value proposal and now have lexical scoped const variables, which are just values on the stack, and calls returning multiple values would simply be presented as destructing to multiple lexical scoped const variables. We might as well then define the function arguments as const variables too rather than local variables, so they could just be values on the values stack too. This is just one proposal, and at the other extreme would be the expressionless proposal using canonicalization to define a standard expression based presentation.