Handle complex types in assertion wrapper modules#152
Conversation
Continuation types cannot be passed to JS, so `assert_return` actions must be implemented with WebAssembly wrapper modules when converting tests to JS. There is precedent for this with vector and exnref types. The difference for continuations is that they are defined types, so creating the wrapper modules with the correct import types requires arbitrarily complex type sections. Add code to traverse and topologically sort the rec groups reachable from the type of an exported function or global, then map them back to surface syntax that can be emitted.
|
Oh right, I hadn't realised that you need the type section, too! I appreciate that you implemented all the machinery to minimise it. :) But is that complexity actually needed? Why not just copy the type section as is? For just driving a test, I don't think it matters whether the wrapper has redundant definitions in it, and the type sections in the test suite won't be huge. |
|
Yes, I had the same thought. The problem is that the type section we have is in terms of recursive DefT, not type indices. Mapping the entire type section back to using type indices is no easier than just doing so for the types we need. (Or maybe there's a shortcut I didn't find?) |
|
I think the simplest solution would be to beef up the translation environment such that |
|
@rossberg, PTAL at the latest commit, which implements that simpler solution. |
| let locals, assertion = wrap_assertion at in | ||
| let _, orig_types, orig_dts = find_inst env x_opt at in | ||
| let n = Int32.of_int (List.length orig_types) in | ||
| (* TODO: Use List.find_index once we have OCaml 5.1.0 or later *) |
There was a problem hiding this comment.
On CI we already use 5.4, and it's required for SpecTec as well. I think it's okay at this point to update interpreter/dune-project to 5.4 as well.
| | dt' :: dts' -> if dt = dt' then Some (Int32.of_int i) else loop (i + 1) dts' | ||
| in loop 0 dts | ||
| in | ||
| let rec remap_ht = function |
There was a problem hiding this comment.
It might be worth syncing with upstream, where the Def case moved from heaptype to typeuse. Then you could simply use Type.subst_* for all the remapping, with the following substitution function:
let subst_of_types dts = function
| Def dt -> Idx (idx_of dt dts)
| tu -> tu
| ] @ | ||
| itypes' | ||
| in | ||
| let remap_global_type (GlobalT (mut, t)) = GlobalT (mut, remap_val t) in |
There was a problem hiding this comment.
Nit: move this before itypes' with the other remap functions..
2 participants
Continuation types cannot be passed to JS, so
assert_returnactions must be implemented with WebAssembly wrapper modules when converting tests to JS. There is precedent for this with vector and exnref types. The difference for continuations is that they are defined types, so creating the wrapper modules with the correct import types requires arbitrarily complex type sections.Add code to traverse and topologically sort the rec groups reachable from the type of an exported function or global, then map them back to surface syntax that can be emitted.