Recursive continuation type crashes the interpreter

[dhil]

Using a recursive continuation type triggers an assertion failure in the interpreter. Minimal repo:

(module
  (type $ct (cont $ct))
  (func (param $k (ref $ct))
    (cont.bind $ct $ct (local.get $k))
    (drop)
  )
)

Output:

./wasm: uncaught exception File "valid/valid.ml", line 107, characters 16-22: Assertion failed
Raised at Wasm__Valid.func_type_of_heap_type in file "valid/valid.ml", line 107, characters 16-28
Called from Wasm__Valid.func_type_of_cont_type in file "valid/valid.ml" (inlined), line 112, characters 2-32
Called from Wasm__Valid.check_instr in file "valid/valid.ml", line 630, characters 27-59
Called from Wasm__Valid.check_seq in file "valid/valid.ml", line 1025, characters 26-43
Called from Wasm__Valid.check_block in file "valid/valid.ml", line 1030, characters 15-41
Called from Stdlib__List.iter in file "list.ml", line 112, characters 12-15
Called from Wasm__Valid.check_module in file "valid/valid.ml", line 1214, characters 2-42
Called from Wasm__Run.run_command in file "script/run.ml", line 518, characters 6-26
Called from Stdlib__List.iter in file "list.ml", line 112, characters 12-15
Called from Wasm__Run.run_script in file "script/run.ml" (inlined), line 588, characters 2-30
Called from Wasm__Run.run_quote_script in file "script/run.ml", line 593, characters 7-24
Re-raised at Wasm__Run.run_quote_script in file "script/run.ml", line 593, characters 58-67
Called from Wasm__Run.input_from in file "script/run.ml", line 104, characters 4-14
Called from Wasm__Run.input_sexpr_file in file "script/run.ml", line 144, characters 18-39
Re-raised at Wasm__Run.input_sexpr_file in file "script/run.ml", line 147, characters 27-36
Called from Wasm__Run.run_meta in file "script/run.ml", line 565, characters 16-50
Called from Stdlib__List.iter in file "list.ml", line 112, characters 12-15
Called from Wasm__Run.input_from in file "script/run.ml", line 104, characters 4-14
Called from Dune__exe__Wasm.(fun) in file "wasm.ml", line 45, characters 33-53
Called from Stdlib__List.iter in file "list.ml", line 112, characters 12-15
Called from Dune__exe__Wasm in file "wasm.ml", line 45, characters 4-72

[dhil]

@rossberg, I would expect this program to fail due to $ct not being a well-formed type. A well-formed continuation type is always parameterised by a valid function type. But looking at the reference interpreter, we never seem to check whether types are well-formed.

I noticed it is possible to define a function type in terms of itself, e.g. the following program type checks and runs:

(module
  (type $ft (func (param (ref $ft))))
  (func $f (param $f (ref $ft))
    (call_ref $ft
      (local.get $f)
      (local.get $f)))
  (elem declare func $f)
  (func (export "main")
    (call $f (ref.func $f)))
)
(assert_exhaustion (invoke "main") "call stack exhausted")

This construction leads me to think that singly typedefs are implicitly recursive. Is this construction intended?

[rossberg]

A type without rec is simply a short-hand for a singleton recursion group, so the latter is well-typed.

As for the OP, I'm surprised the type definition passes validation. AFAICS, we do check type definitions, and we do check that cont is given a function type.

[rossberg]

I was looking at the version in the effect-handlers repo, the one here does indeed seem to miss that check:

specfx/interpreter/valid/valid.ml

Line 186 in 4310c76

| ContT ft -> check_heap_type c ft at

[rossberg]

Compare with https://github.com/effect-handlers/wasm-spec/blob/8c5d4f66db6405d57a7346ebbf2d207fe78d73fd/interpreter/valid/valid.ml#L133

[dhil]

aha, so this has been lost in a merge sometime ago. I will reinstall the check. Thanks!