search

WebAssembly / multi-value

Proposal to add multi-values to WebAssembly
https://webassembly.github.io/multi-value/
Other
70 stars 24 forks source link

[spec] valid limit ok seems not well-defined #29

Closed Huxpro closed 5 years ago

Huxpro commented 5 years ago

In the https://webassembly.github.io/multi-value/core/appendix/properties.html#table-instances to validate tableinst, it use the rule 

\vdash limit ok

which seems to be undefined.

The vdash is linked to https://webassembly.github.io/multi-value/core/valid/types.html#valid-limits which is validated respect to some k.

The closest one is the https://webassembly.github.io/multi-value/core/valid/types.html#memory-types which conclude \vdash limit ok from \vdash limit : 2^16

rossberg commented 5 years ago

Ah, good find. This is actually wrong in the main spec. The judgement changed from the former to the form with the k at some point, but it seems like I forgot to adapt the occurrences in the rules for tableinst and moduleinst.

Care to create a PR against the main spec?

Huxpro commented 5 years ago

@rossberg will do! I couldn't find out the use of "valid limit" rule in the moduleinst. Could you point out? If I understood it correct, I could image two fixes for the tableinst:

  1. explicit say vdash limit 2^32.
  2. instantiate a valid tabletype judgement with funcref, i.e. vdash limit funcref ok.

I guess (2) is preferable?

rossberg commented 5 years ago

The minimal and direct fix is (1), i.e., to replace "\ok" with ": 2^K" in the two instance rules, where K is 32 for tables and 16 for memories. I would go for that.

The perhaps nicer but much more extensive fix would be to change the definition of tableinst and meminst to actually store tabletypes and memtypes instead of just limits. That's a change I had to make for the reference types proposal (along with the analogous change for globalinst). If you feel like it, you could backport that change, but I wouldn't necessarily recommend spending the time on it.

Huxpro commented 5 years ago

@rossberg two PRs respectively have been made against the main spec. Personally, I prefer (2) even more after looking at the reference-type proposal spec you mentioned. See reasons in https://github.com/WebAssembly/spec/pull/1094

Huxpro commented 5 years ago

Closed by https://github.com/WebAssembly/spec/pull/1093