stack-switching icon indicating copy to clipboard operation
stack-switching copied to clipboard

WasmFX reference interpreter: Errorenous treatment of non-final types

Open frank-emrich opened this issue 7 months ago • 2 comments

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.

frank-emrich avatar Jul 24 '24 14:07 frank-emrich