Proposal: Add type for unreachable states

[RossTate]

Problem

The current design of the unreachable instruction (and br and the like) imposes an additional decidability constraint on WebAssembly: for any instruction sequence, we need to be able to determine if there exists a typing for the sequence.

This problem will grow more difficult as WebAssembly grows (until we make it trivial with this proposal). Even just the small complexity introduced by adding reference types has caused a bug in the reference interpreter (WebAssembly/reference-types#111), imposing yet another layer of complexity on the reference interpreter solely for type-checking unreachable code. This will be made worse by br_on_null in the typed references proposal, which will require adding a "unknown reference type" case.

This decidability constraint seems to already be restricting the design of WebAssembly. For example, here in #1365 it is raised as an issue for adding a dup instruction. This is because (unannotated) dup and pick instructions would require you to reason that the duplicated type is used consistently across multiple instructions, requiring the type-checker to track constraints on type variables and ensure they're satisfiable, all for the sake of just type-checking unreachable code.

Short-Term Solution

A short-term solution is to add an unreachable type (it seems specifically to be a result type) to the typing rules but not to the grammar. Any (syntactically valid) instruction sequence would have type unreachable -> unreachable. Because this changes nothing besides validation and accepts strictly more programs, we could make this change to any proposal spec and it would be backwards compatible.

This solution does not seem to have been discussed in the design rationale. It also seems to be compatible with all the desirable properties provided there except for the following:

It is agnostic to reachability: neither the specification nor producers need to define, check, or otherwise care about reachability (unless they choose to, e.g. to perform dead code elimination).

However, this property seems to already not hold for even the original WebAssembly. In particular, select requires type-directed compilation, and without the relevant type information there is no guidance as to how it should be compiled. So WebAssembly compilers need to reason about unreachability already, likely by simply not compiling unreachable code (which addresses the attack vector mentioned here).

Long-Term Solution

A long-term solution would extend the grammar to account for an unreachable type. For example, a function could declare its type as [i32 i32] -> unreachable. WebAssembly compilers could even use this information to optimize calls to such functions, i.e. no need to save registers before the call if the call will never return! (Though of course you still have to consider exceptions.) This solution would involve many more design decisions, some of which might be informed by other discussions that are in flight, so it would probably be best to explore this option as part of some larger effort rather than as an isolated proposal.

[rossberg]

This exact type was previously introduced as part of the reference types proposal, for the reasons you mention, and some others (it wasn't needed for the MVP, because the type algebra was simple enough). However, as a bottom type, it relies on subtyping, so it got removed in response to the request to remove subtyping. I explicitly called out that this also axes the bottom type. I'm not surprised that we overlooked an implication like this.

Subtyping and the bottom type are currently reintroduced in the func-ref proposal. But it looks like we have to move it back to reftypes. :(

[conrad-watt]

I agree that at least the short-term solution is desirable (I sketched out the formal rules here).

FWIW, the design rationale you linked does explicitly address this:

Other solutions that have been discussed would lose most of the above properties. For example:
|...snip...|
Allowing but not type-checking unreachable code would break decomposability and requires the spec to provide a syntactic definition of reachability (which is unlikely to match the definition otherwise used by producers).

I think the concerns about the "syntactic definition of reachability" are overstated. To implement a type checker today, exactly the same set of instructions needs to be handled specially because of their polymorphic output types. I'm also not sure if anyone is relying on decompositionality (I could believe reliance on the converse).

The comparison to the JVM at the end of that rationale doesn't appear to be accurate. The analogy in Wasm for the JVM's approach would be to completely forbid syntactically dead code.
(Quote from the latest JVM standard (link))

It is illegal to have code after an unconditional branch without a stack map frame being provided for it.

So the JVM does not have to deal with any polymorphism issues in dead code. In an earlier version of the JVM (I think prior to the introduction of stack maps), return explicitly set the output type to empty (link).

FWIW, another "design smell" surrounding this - when I implemented a verified type checker for Wasm, easily 90% of the effort both in implementation and in correctness proof was concerned purely with handling the dead code case. This isn't precise but it's a rough indicator for the mental overhead this design decision is causing on type checking, even before typed objects are introduced.

EDIT: missed Andreas' response

This exact type was previously introduced as part of the reference types proposal, for the reasons you mention, and some others (it wasn't needed for the MVP, because the type algebra was simple enough). However, as a bottom type, it relies on subtyping, so it got removed in response to the request to remove subtyping.

I don't think this type should rely on subtyping. It's the type of the whole stack, not the type of an individual element. To allow dead code to skip validation, all you need are the typing rules

C ⊢ unreachable : t* -> ⊥
<similar for return, br, br_table>

C ⊢ e* : ⊥ -> t*

This should work even if t* can contain object types.

[RossTate]

My impression of the discussion about subtyping for reference types was that it was centered around a (near-)bottom heap type. I only just learned that there was a bottom value type in the proposal as well. As @conrad-watt points out, the suggestion here is a bottom state/result type, which avoids many of the problems of bottom heap/value types while providing a simpler solution to the same problem that the bottom value type seems to have been solving. (It's also simple enough that its rules can be formulated without explicitly adding subtyping.)

FWIW, the design rationale you linked does explicitly address this:

The solution here is slightly different because it gives a type to unreachable code. This, for example, makes it still decomposable. So same practical effect, but with slightly nicer theoretical properties.

[conrad-watt]

The solution here is slightly different because it gives a type to unreachable code. This, for example, makes it still decomposable. So same practical effect, but with slightly nicer theoretical properties.

In the short-term solution, the "type" is just a formal artefact to express skipping validation. If the "skipping validation" approach had been agreed on at an informal level, it would have almost certainly been formalised in this way. I agree that the approaches diverge when considering the long-term solution.

This, for example, makes it still decomposable.

I don't believe the resulting language would be decomposable in the same way that the current language is. I also don't believe this is a big deal :P

[RossTate]

Agreed. So do we have insights on reasons to not skip validation that have not been addressed above?

[conrad-watt]

It is agnostic to reachability: neither the specification nor producers need to define, check, or otherwise care about reachability (unless they choose to, e.g. to perform dead code elimination).

However, this property seems to already not hold for even the original WebAssembly. In particular, select requires type-directed compilation, and without the relevant type information there is no guidance as to how it should be compiled. So WebAssembly compilers need to reason about unreachability already, likely by simply not compiling unreachable code (which addresses the attack vector mentioned here).

I'd like to hear implementers' perspectives on how dead code is currently handled (e.g. in streaming compilation), and whether they'd have any concerns if it was no longer validated. The quoted point (from @RossTate's OP) seems very reasonable.

[rossberg]

@conrad-watt:

I think the concerns about the "syntactic definition of reachability" are overstated.

Not really. We actually had lengthy and heated discussions about the details of that at the time. For example, whether it should extend beyond a block's end. There is no canonical definition. At the same time, an impedance mismatch in the notion of unreachable would get in the way of codegen.

The analogy in Wasm for the JVM's approach would be to completely forbid syntactically dead code.

The relevant aspect of the analogy is that the JVM does not forbid dead code, and that's pretty important for producers. It merely requires it to be type-annotated.

I don't think this type should rely on subtyping.

If you want to keep checking dead code, then a simple bottom stack type would not be enough, since there can be known types on the top of the stack (it becomes more like a row variable). Either way, it's a separate, more complex extension. We could add that, too, but it seems less bang for the bucks, in the sense that it won't change engines, merely complicate the spec. Depending on the instruction set, it might not even replace the bottom value type (e.g., if you had pick without a stack type annotation).

FWIW, even on stack types, it would still be a form of subtyping (or something largely equivalent).

In the short-term solution, the "type" is just a formal artefact to express skipping validation.

That's not correct. The bottom value type does not "skip validation", it merely makes it more permissible. In particular, something like (unreachable) (i32.const 0) (i64.add) is still rejected.

I'm also not sure if anyone is relying on decompositionality

In general, it means that dead code is still type-checked to the extend that it could be executed. As I mentioned elsewhere, that e.g. addressed potential security concerns.

likely by simply not compiling unreachable code (which addresses the attack vector mentioned here)

Among other things, that work-around doesn't apply to interpreters.

[conrad-watt]

Not really. We actually had lengthy and heated discussions about the details of that at the time. For example, whether it should extend beyond a block's end. There is no canonical definition. At the same time, an impedance mismatch in the notion of unreachable would get in the way of codegen.

My point is that all implementations have converged around a set of instructions which, at validation time, must produce PolyStack [] as an output type. It is precisely these instructions that would be considered "syntactically dead", and now produce ⊥. I don't think there would be the same heated debate again. Deliberately or not, WebAssembly has effectively already adopted a definition of syntactic deadness through its non-deterministic output types.

If you want to keep checking dead code, then a simple bottom stack type would not be enough, since there can be known types on the top of the stack (it becomes more like a row variable).

I addressed this specifically with the additional typing rule C ⊢ e* : ⊥ -> t*. Generating a ⊥ type as output allows remaining instructions in a straight line to be skipped. This also confines the effects of ⊥ to within the current block, which seems the obvious choice.

Note that with @RossTate's extended proposal, which I'm not arguing for, block types could explicitly declare their output type as ⊥.

That's not correct. The bottom value type does not "skip validation", it merely makes it more permissible. In particular, something like (unreachable) (i32.const 0) (i64.add) is still rejected.

See above (also, in this proposal, ⊥ is the type of the whole stack, not of a single stack element - it's not the same as the bottom type from the earlier reference types draft).

Among other things, that work-around doesn't apply to interpreters.

I remember you saying that WebAssembly shouldn't be designed for interpreters! In any case, the code still has to be parsed; a security-conscious interpreter would have options to harden itself. But this all seems like a hypothetical.

EDIT:

The relevant aspect of the analogy is that the JVM does not forbid dead code, and that's pretty important for producers. It merely requires it to be type-annotated.

I was a little off with my analogy - I should have focussed on the point that, on the consumer side, the JVM has never had to handle this kind of polymorphic typing of dead code. I can almost believe that forbidding dead code could be annoying for some producers, but do they care about it being validated? Maybe Wasm could have been designed with input type annotations for dead code from the start, but we're now constrained by webcompat.

[RossTate]

My impression from @rossberg's first post and from @conrad-watt is that neither of y'all have objections to at least the short-term solution, so I'd like to hear directly from others about any objections they have.

[conrad-watt]

My impression from @rossberg's first post and from @conrad-watt is that neither of y'all have objections to at least the short-term solution, so I'd like to hear directly from others about any objections they have.

@rossberg's last comment was explicitly an objection to (his understanding of) the short-term solution. I hope he finds my arguments convincing, and I'm very interested to hear from implementers, but we shouldn't put words in his mouth.

[RossTate]

Ah, I see how I misread it. Thanks for correcting me.

[fitzgen]

Probably ~half the tricky fuzz bugs we've found in the wasmparser crate's validator (which powers wasmtime, cranelift, and aarch64 spidermonkey) and in cranelift's wasm-to-ir translator involve unreachable code, often with its interaction with new proposals (e.g. multi-value).

I've heard similar things from people who've hacked on spidermonkey's other wasm validator; hopefully those folks can speak up here as well.

The short term proposal (where we limit its effects to within a block) sounds like a great idea to me.

[tlively]

Binaryen has always had an explicit unreachable type in its IR that behaves almost like the proposed long-term solution, so the short-term solution would not require any meaningful changes to most of Binaryen and would allow some nice simplifications in some of Binaryen. It would also help reduce the cognitive overhead of working with Binaryen IR by making its unreachable handling more similar to Wasm's unreachable handling.

[binji]

Binaryen has always had an explicit unreachable type in its IR that behaves almost like the proposed long-term solution

Is that true? I was under the impression that binaryen's unreachable was quite a bit more complex than described here.

I addressed this specifically with the additional typing rule C ⊢ e* : ⊥ -> t*. Generating a ⊥ type as output allows remaining instructions in a straight line to be skipped.

It took me a bit to realize how this works. For others who were confused like me: the idea is that if ⊥ is on top of the type stack during validation, then this rule can consume any number of expressions (e*), and yield any number of result types (t*). This would allow it to match the expected results for that block.

EDIT: actually, ⊥ must be the entire type stack, see Conrad's comment below.

often with its interaction with new proposals (e.g. multi-value).

Agreed, I've found more cases where unreachability is complex in the newer proposals too (e.g. GC) when the annotations are removed. I believe this is essentially the same problem as select.