stack-switching
stack-switching copied to clipboard
WasmFX reference interpreter: Errorenous treatment of non-final types
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.