Wasm: try..finally with non-nullable reference type produces invalid code

[sjrd]

Reproduction:

  def test(): Unit = {
    var a = 1
    val some = try {
      Some(a)
    } finally {
      a = 2
    }
    assert(some.value == 1)
  }

produces invalid Wasm code. Trying to run the program yields

[CompileError: WebAssembly.instantiate():
Compiling function #165:"f.helloworld.Main$.test;V" failed:
uninitialized non-defaultable local: 2 @+28176]

The pretty-printed code for the function is

  (func $f.helloworld.Main$.test_V (type $128)
     (param $this (ref $c.helloworld.Main$))
     (local $a i32) (local $1 (ref $c.scala.Some)) (local $2 (ref $c.scala.Some)) (local $some (ref $c.scala.Some))
     i32.const 1
     local.set $a
     block $1
       block $2 (result exnref)
         try_table (catch_all_ref $2)
           call $new.scala.Some
           local.tee $2
           local.get $a
           call $bI
           call $ct.scala.Some.<init>_Ljava.lang.Object_V
           local.get $2
           local.set $1
         end
         ref.null exn
       end
       i32.const 2
       local.set $a
       br_on_null $1
       throw_ref
     end
     local.get $1
     local.set $some
     call $m.scala.Predef$
     ref.as_non_null
     local.get $some
     struct.get $c.scala.Some $f.scala.Some.value
     call $as.int
     i32.const 1
     i32.eq
     call $f.scala.Predef$.assert_Z_V)

Wasm cannot prove that, in all the code paths that lead to reading local.get $1 after the big block $1, the variable was initialized. That's fair, since it wouldn't be initialized if we caught an exception; we know that we cannot reach there in that case (because of the re-throw) but Wasm validation cannot prove it. Since $1 has a non-nullable reference type (ref $c.Some), that is not valid code.

We have to always use a defaultable type for the partial results involved in try..finallys (which means we have to cast away nullability when we read them).