WasmFX reference interpreter: Errorenous treatment of non-final types

[frank-emrich]

There seems to be a validation problem when WasmFX instructions non-final types.

Consider the following program:

(module
  (type $ft1 (func (param i32)))
  (type $ct1 (sub (cont $ft1)))

  (type $ft0 (func))
  (type $ct0 (sub (cont $ft0)))

  (func $test (param $x (ref $ct1))
    (i32.const 123)
    (local.get $x)
    (cont.bind $ct1 $ct0)
    (drop)
  )
)

This should be accepted, but fails with the following error message:

invalid module: type mismatch: instruction requires [i32 (ref null (cont 0))] but stack has [i32 (ref 1)]

Removing the "sub" from the definitions of $ct0 and $ct1 makes the problem go away.

The culprit seems to be our usage of heap_type_of_str_type in valid.ml. This conversion function was introduced by us and is only used for the validation of WasmFX instructions. It turns a structural type into a heap type by turning it into a final subtype with an empty list of supertypes, and then puts that subtype definition into a singleton group of recursive types.

I suspect that this also affects code combining recursive types and WasmFX instruction, as it throws away information about the members of recursive type groups. We can probably get rid of heap_type_of_str_type altogether and obtain the desired heap types in a different way.

[dhil]

Thanks. I think before fixing this issue, we should make sure the reference interpreter is in sync with the wasm-3.0+exn on WebAssembly/spec.

[rossberg]

I agree, that function seems wrong and should never be used. Instead of heap_type_of_str_type (FuncT/ContT t), these rules should use VarHT (StatX x), where x is the type index from which the structural type was expanded before.

Note that the wasm-3.0+exn branch is no longer needed and now subsumed by wasm-3.0.

PS: I think syncing with wasm-3.0 is somewhat independent of this particular issue.

[dhil]

Fixed by #72.