Why are result types of control flow instructions arbitrary? (Especially `return`)

Question

I am trying to understand the type system of WebAssembly and confused by control flow instructions. I don't understand why the result type of br, result or unreachable is an arbitrary type sequence (t_2^*):

• https://webassembly.github.io/spec/core/valid/instructions.html#valid-return

• https://webassembly.github.io/spec/core/valid/instructions.html#valid-br

• https://webassembly.github.io/spec/core/valid/instructions.html#valid-unreachable

I ran the following two snippets in the reference interpreter:

 (module
   (func (result i32)
     (i32.const 1)
     (i32.const 2)
     (return)
     (return)
   )
 )

No type error is reported. However, this one:

 (module
   (func (result i32)
     (i32.const 1)
     (i32.const 2)
     (return)
     (f32.const 2)
   )
 )

Now I get type error: "test.wast:2.2-7.3: invalid module: type mismatch: operator requires [i32] but stack has [f32]".

But I can try and exploit the "arbitrary type sequence" and write weird programs that are still well-typed:

(module
 (func (result i32)
  (i32.const 1)
  (i32.const 2)
  (return)
  (i32.add)
  (i32.add)
  (i32.add)
  (i32.add)
  (i32.add)
  (i32.add)
  (i32.add)
 )
)

So what is the point of type checking after the return statement?

Answer 1

The Rationale section of the original Wasm design docs contains an extensive motivation of this feature.