Clarification request: tail calls in unreachable code vs. multi-return

[jakobkummerow]

In reachable code the result types of any tail-called function must obviously match those of its tail-caller, i.e. there must be the same number of them, and they must be subtypes of them.

In unreachable code, I'm confused.

Interpretation 1

When starting with the understanding that "(return_call $x) is like (call $x) (return)" (which gives an accurate intuitive understanding in the common case, and has the nice property that it's a Wasm-to-Wasm transformation), it follows that the number of results of $x doesn't matter in unreachable code, since the polymorphic stack takes care of mismatches; but to the extent that they are present and overlap with the tail-calling function's result types, they must still be subtypes of those.

In other words:

(func $produce-i32 (result i32) (i32.const 0))
(func $valid
  unreachable
  return_call $produce-i32)
(func $valid-too (result f64) (result i32)
  unreachable
  return_call $produce-i32)
(func $invalid (result f64)
  unreachable
  return_call $produce-i32)
(func $invalid-too (result i32) (result f64)
  unreachable
  return_call $produce-i32)

This was my initial assumption, but after thinking about it for a while, I'm beginning to think that was a misunderstanding on my part.

Interpretation 2

When starting with the understanding that "return_call $x is like stashing away the call parameters (in a 'magical' way that isn't expressible in terms of other Wasm instructions), returning from the tail-calling function, restoring the call parameters on the value stack, and then calling $x", it follows that reachability inside the tail-calling function is irrelevant, and the result types of $x must always have the same arity as and be subtypes of the result types of the tail-calling function. Is that correct?

---

I would appreciate it if this was explicitly clarified in the spec text and/or tests. The current test suite in this repository passes with either of these two implementations of the validation algorithm.

I stumbled upon this because V8's implementation is slightly inconsistent. We implement return_call and return_call_indirect per Interpretation 2, but (for historical and possibly accidental reasons) have a single test case that requires Interpretation 1 for return_call_ref. Obviously that should be unified, and in order to do so, I'd like to get clarity on what the right behavior is.

(Side note: this is one more chapter in the story of unreachable code validation consuming annoying amounts of time and energy to get right, while having next to zero practical relevance.)

[tlively]

The spec supports interpretation 2. In particular, the typing rules for return_call require that the result of the function exactly matches the expected return type in the calling context. unreachable similar instructions do not modify the expected return type in the calling context in any way, although in principle they could if we wanted to spec interpretation 1 instead for some reason. And of course once we have subtyping, the "matches" relation will allow subtyping as well.

[rossberg]

What @tlively says. In general, the type system is designed such that reachability has the least possible interaction with other typing rules. There are no special cases for unreachable code whatsoever, it only produces a polymorphic stack. IOW, the only thing it relaxes is the number and types of values that can be popped from the stack. With that in mind, interpretation 1 would only make sense if the same was already allowed in reachable code.

[jakobkummerow]

Thanks for confirming. I'll fix V8's implementation accordingly.

I still think it would be good to clarify this in the spec text and/or tests.