-
Notifications
You must be signed in to change notification settings - Fork 746
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Proposal for new Binaryen IR type system #903
Comments
Thinking more about taking a node with I'm going to use
Is it always valid to transform this to:
My gut says yes. This is a form of DCE, and the bubbling out of Where can't we bubble out
, we can't rewrite the How does this interact with Presumably we want a single pass to propogate unreachability as far as it can go that we run early, followed by unreachable-DCE? |
Why is the first example, (Historical note: around the 0xc timeframe, the spec actually explicitly permitted implementations to ignore type errors in unreachable code, so implementations weren't wrong or non-compliant.) |
I believe that's a misunderstanding we had while drafting the post that wasn't fixed after the fact - we noticed for the next two examples and you're right it's not valid. |
@jgravelle-google the order doesn't flip, so
desugars to
which validates because the type stack at i32.add has [any, any]. The other order desugars to
which does not validate because the stack has [any, f32]. |
Does this mean emiting a proper wasm type for a block/if/loop when converting to wasm? Or something more?
Does this mean that a block has type
I'm not sure I understand what this propagation mechanism is. Would we need to propagate unreachability after each transformation? (I hope not?) On the general approach described in this issue: I think it sounds promising. I've also been moving in the direction of thinking we should keep the
then it is always valid to emit this wasm:
The first extra The second If that makes sense so far, then this can actually be taken a step further: again, if an unreachable block is one that cannot be exited, then we can just emit
i.e., don't emit a block at all! Just emit the block contents, then an unreachable. This is valid stacky wasm, I believe. (Also in fact the |
A shorter way to summarize the last part of my last comment is that, if we allow blocks with
which in effect puts a block on the stack, and makes it so it's ok to pop from the stack. So this can be seen as a wasm way to emit an unreachable block. Just instead of having the unreachable type as the block type, it's an extra byte afterwards. (And, while efficiency isn't the main issue here, we don't even need to waste a byte, as I think we can just not emit the block begin and end, it would still be valid stacky wasm, so we actually save a byte.) |
Let me add one other option to ponder. If there is an unreachable operator used deep in an expression then the expression can simply be split out into a series of live sub-expressions and the rest discarded. This can be done trivially when the IR is in a flat (no-expression) form in which all operators with a result set an SSA definition. I suspect this is why I did not find it necessary to propagate an Writing an explicit Here's another way to look at this: let blocks have no fall-through, so if there is one then the block must end in a I still have not got up to speed on the proposed validation rules, but cases such as the following illustrate some of my concerns, and could binaryen really read this into an AST, are values effectively materialized. Is this
|
Responding in order of original comments: First, (and to @kripken's question about reifying and @jgravelle-google's suggested transform) I guess we should be a little more precise with what that means, because I think it's actually 2 things. One is an IR->IR transformation, changing the type of a node with @sunfishcode re: @kripken's second question: yes, my proposal is your (1): when lowering, emit a proper wasm type based on the outside context. We still want to have validation rules which are defined entirely in terms of Binaryen AST; hence the 2 options I just mentioned for binary operators. Both possibilities allow straightforward lowering to wasm, I guess it's just a question of whether an asymmetric validation rule makes optimizations more difficult. I suppose you could just model it the way you model other side effects when deciding if a transformation like commuting operands is valid, so maybe it's not so bad. Adding I think |
On the |
Seems like overall we are pretty much in agreement here.
I think we should keep it symmetric as it currently is, because wasm's asymmetry is only due to the stack machine model (I believe?) and in our AST an asymmetry would be surprising. (Of course DCE makes this kind of a moot point anyhow.)
Is that about my proposal to emit an unreachable block as Now, maybe that doesn't matter if we can find the right i32/f32/etc. type for the block during lowering anyhow - if we can, then that's a nice clean solution. But I am not 100% sure we can. Another issue to consider is reading the output back into binaryen. If we emitted |
@Wllang my understanding is that your last example is valid because the polymorphic stack supplies (any number of) whatever types are needed. I'm not sure I'd want AST with default arguments though; I haven't really thought through the consequences of that but it seems like it would be surprising. WRT @kripken WRT symmetry: obviously symmetry would make some optimizations simpler, but it could leave performance on the table by defeating other optimizations; e.g. if we have WRT finding the right type during lowering for unreachable blocks: Every block is in some context, and has some parent. I think the type should be unambiguous in most cases (e.g. binops, conversions, etc). Possible exceptions might be cases like Wrt round-tripping (or just plain creating binaryen IR from wasm): not sure, it kind of ties in to whether we require blocks whose end is unreachable to have unreachable type. If so, then during wasm parsing it seems like we'd need to propagate unreachables outward through the scopes when we find an unreachable node (and likewise during optimizations that create unreachable nodes). In that case I think we'd end up with the same IR whether the extra |
Wrt symmetry: yeah, I see what you mean. I believe that is currently handled by DCE, though - it should remove all unneeded code including the toplevel add, where possible. So this is a little complexity but it seems worth it. Wrt finding the right type during lowering for unreachable blocks: Yeah, its those cases like if etc. that worry me. It's not enough to just look up the stack, in general, you may need to look up, reach an if, then go down into the ifs other arm, and so forth.
All operands but the last must be dropped, yes. (But if the last is unreachable, then we need to look at the Wrt round-tripping: yeah, maybe that isn't much different between the two proposals. Workable in either one, I suspect. |
I think for That leaves the more interesting case of parametric operators,
Thinking more about blocks: could say a block has type unreachable if any of its elements is unreachable, and if no br targets it (regardless of its last element). An example would be The alternative would be to say that a block is unreachable if no br targets it and its last element is unreachable. Then It kind of ties into the question of whether blocks or other elements which could have type unreachable must have that type. I think it could work either way for emitting wasm; for creating binaryen IR from wasm and for transformations, it would be a bit of extra work to potentially fix up the type of a node that is created or made unreachable by a transformation, but it sounds like that might be a property we want for round-tripping anyway. |
Yeah, thinking some more, that does sound right. (Except for
That does seem like a good way to define it.
I don't think that's necessary? If the block type is |
Exploring this issue, I implemented @dschuff's rule for block types (unreachable iff an element is unreachable, and no breaks), and the simple "emit unreachables to make stuff work" approach. I realize we haven't agreed here yet, I just wanted to see how this can work. Here is the diff.
|
mir2wasm does something similar to this. Rust has an unreachable type, |
Okay, I just finished reading this thread, so here are some thoughts of varying degrees of vagueness, relatedness, and self-consistency. Regarding symmetry, I think there's a higher level question of whether the binaryen IR defines an evaluation order (although I realize everyone else in the thread probably already knows if binaryen defines an order). If it does, then obviously you have to respect that, but if not then you have a lot more freedom. For example, if you don't define an evaluation order, the following transformation is always valid. (I'm using ⊥ to represent unreachable)
That obviously gives you a ton of freedom in eliminating dead code, although I expect these semantics would be surprising to binaryen users. I think the safest way to think of A consequence of this is that you don't get to propagate unreachable. So in our
where
is always illegal, because there's an Another way to think of I think With As far as when you go to reify an In the most general case, you'd have to do something like Hindley-Milner type inference. At the end you still might have type variables, but this means nothing observes that particular type and thus you can pick whatever you want (such as I'm not sure how helpful this is, but one way to think of type systems is that they define a logic that you can use to prove properties about programs. One way you might use this in binaryen is as a tool to decide whether it a particular optimization is correct and applicable. Going back to @dschuff's original requirements, here's the way I would think of the requirements.
If you were doing a paper on this, most of the paper would be focused on proving 6 and 7. It's good to be really precise and explicit about what is |
Good summary. Yeah, I think 1-8 are exactly what we want here. Earlier on we had hopes of having binaryen use pure wasm, so there wouldn't be two type systems, but we wasm evolved we've diverged. so formally, we do have two now. About unreachable being a type vs an effect, I'm not totally sure I see the difference in our case, but the changes proposed in this issue do make unreachable properly describe an ast node that is not "reachable" in the naive sense - you can't get exactly there (you can get out of it, though, if you branch to some outer scope). |
This was done in #911 (and followups mentioned above). |
Background: previous general discussion about Binaryen and wasm stack machine is at #663. It turns out Since Binary 0xc, Binaryen's type system has been subtly wrong with respect to the spec, and both V8 and SpiderMonkey were not spec compliant in that way and so nobody noticed. More concretely, @kripken tried to fix that in #899 and that led to some more general discussion about what to do. Probably that discussion should be in an issue and not in a PR, so here's an issue.
@jgravelle-google and I have been discussing it, and we have an idea which essentially carries the discussion in #899 to an end which we think we like, but maybe you can poke holes in it.
Also to recap, the goals are:
In short, we think we can allow blocks (and everything else in Binaryen IR) to have
unreachable
type, and basically freeze those types into block signatures (i.e. reify them) when converting to wasm proper. Here are the Binaryen IR properties:br
) is context-free; in other words a node is valid based on its type and it contents only (the consequence of this is that transforms are also context-free).unreachable
.a. all operand(s) (including those that follow unreachable nodes in blocks) are recursively valid, and
b. all operands type-check according to opcode-specific rules (
unreachable
always type-checks)c. A node with
unreachable
type must have at least oneunreachable
operandunreachable
nodes may be reified based on their context (see paragraph on conversion to wasm below), and the result remains valid.br
nodes are valid if their operand type matches the type of the target (br
s targetingunreachable
-typed nodes are invalid)On conversion to wasm, types of all
block
/loop
/if
must be inferred/reified to concrete types. Inference always happens from context (i.e. outside in) and not from e.g. inside-out. In other words (and in contrast to current Binaryen), block types are not inferred based on their last element, but based on their context; e.g. if they are the operand of areturn
or are implicitly fall-through-returned, then they are converted to the return type of the function. This happens for every block we emit; we check the context and if it requires a particular type, we emit that type; otherwise it can be void. When this happens, we do not need to reify anything inside (rule 3).There are a few non-intuitive consequences of these rules.
For example
(i32.add (f32.const 0) (br 0)))
is valid (and can have typeunreachable
) because of rule 3b.is valid and the
i32.add
must have typeunreachable
. It does not get reified.If the block is reified to
i32
then the add can stay unreachable, or have type i32. If the block is reified to something else then it's still valid (it's the first example again). In this nesting, it never needs to take a type (and it's beneficial).I think this also means that it's a valid transform to take a node with an
unreachable
child and make itunreachable
.I think this also has the optimization properties that we want, and that conversion from wasm is workable but we haven't thought about all the permutations yet, so... yeah, comments and we can see if it all holds up.
The text was updated successfully, but these errors were encountered: