[spec] First go at specification #3

rossberg · 2018-03-07T15:54:51Z

First go at specifying the baseline proposal, analogous to #2:

add types anyref and eqref (and internal nullref) and respective subtyping (splitting valtype into numtype and reftype)
add instructions ref.null, ref.isnull, ref.eq, get_table, set_table
allow multiple tables
validation, execution, binary format and text format
adjust appendix

This change should already be complete, but opcodes are preliminary; names of table instruction might also be subject to change, depending on pending main spec PR.

Edit: Rendered version

binji · 2018-03-07T23:20:56Z

document/core/exec/instructions.rst

+
+7. Pop the value :math:`\I32.\CONST~i` from the stack.
+
+8. If :math:`i` is larger than the length of :math:`\X{tab}.\TIELEM`, then:


Should be "is not smaller than", right? This matches the behavior in call_indirect.

binji · 2018-03-07T23:26:53Z

document/core/exec/instructions.rst

+
+9. Pop the value :math:`\I32.\CONST~i` from the stack.
+
+10. If :math:`i` is larger than the length of :math:`\X{tab}.\TIELEM`, then:


same here w/ "not smaller"

binji · 2018-03-07T23:31:12Z

document/core/exec/instructions.rst


-7. Let :math:`\X{ft}_{\F{expect}}` be the :ref:`function type <syntax-functype>` :math:`F.\AMODULE.\MITYPES[x]`.
+7. Let :math:`\X{ft}_{\F{expect}}` be the :ref:`function type <syntax-functype>` :math:`F.\AMODULE.\MITYPES[y]`.

 8. Assert: due to :ref:`validation <valid-call_indirect>`, a value with :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.


I can't mark the proper line, but shouldn't "if tab.elem[i] is uninitialized" be changed to "is REFNULL"?

Indeed. Also needed to change the consecutive line, since the table no longer contains a function address directly. The semantics of elem segments required a similar tweak.

binji · 2018-03-07T23:32:55Z

document/core/exec/runtime.rst

 .. _syntax-val:

 Values
 ~~~~~~

-WebAssembly computations manipulate *values* of the four basic :ref:`value types <syntax-valtype>`: :ref:`integers <syntax-int>` and :ref:`floating-point data <syntax-float>` of 32 or 64 bit width each, respectively.
+WebAssembly computations manipulate *values* of the four basic :ref:`value types <syntax-valtype>`: :ref:`integers <syntax-int>` and :ref:`floating-point data <syntax-float>` of 32 or 64 bit width each, or of references, respectively.


"respectively" sounds strange to me here.

Fixed the wording.

binji · 2018-03-07T23:33:36Z

document/core/exec/runtime.rst

+
+References other than null are represented with additional :ref:`administrative instructions <syntax-instr-admin>`.
+They either are *function references*, pointing to a specific :ref:`function address <syntax-funcaddr>`,
+or *host references* pointing to an unintrpreted form of :ref:`host address <syntax-hostaddr>` that can be defined by the :ref:`embedder <embedder>`.


sp: uninterpreted

binji · 2018-03-08T01:42:07Z

document/core/valid/instructions.rst

+
+* Let :math:`\limits~t` be the :ref:`table type <syntax-tabletype>` :math:`C.\CTABLES[x]`.
+
+* Then the instruction is valid with type :math:`[t] \to []`.


[\I32~t] \to []?

binji · 2018-03-08T01:42:22Z

document/core/valid/instructions.rst

+
+* Let :math:`\limits~t` be the :ref:`table type <syntax-tabletype>` :math:`C.\CTABLES[x]`.
+
+* Then the instruction is valid with type :math:`[] \to [t]`.


[\I32] \to [t]?

binji · 2018-03-08T01:47:37Z

document/core/syntax/types.rst

+Reference Types
+~~~~~~~~~~~~~~~
+
+*Reference types* classify 


remove newlines

Oops, this actually was a half-finished edit.

binji · 2018-03-08T01:49:51Z

document/core/syntax/types.rst

+The type |ANYFUNC| denotes the infinite union of all references to :ref:`functions <syntax-func>`, regardless of their :ref:`function types <syntax-functype>`.
+
+The type |EQREF| denotes the infinite union of all references that can be compared for equality;
+in order to avoid exposing implementation details, some reference types, such as |ANYFUNC|, do not admit equality, and therefor are not :ref:`subtypes <match-reftype>` of |EQREF|.


sp: therefore

binji · 2018-03-08T01:59:04Z

document/core/syntax/modules.rst

@@ -147,7 +147,7 @@ The |MTABLES| component of a module defines a vector of *tables* described by th
     \{ \TTYPE~\tabletype \} \\
   \end{array}

-A table is a vector of opaque values of a particular table :ref:`element type <syntax-elemtype>`.
+A table is a vector of opaque values of a particular :ref:`reference type <syntax-reftype>`.


Just so I understand, of the instructions that operate on a table:

All table types allow use of get_table, set_table.

A table of ANYFUNC allows call_indirect.

A table of EQREF allows ref.eq.

A table of ANYREF allows no other instructions.

Is that correct?

Yes, that's right, except that ref.eq does not operate on tables but on references directly.

rossberg

Thanks for the review!

rossberg · 2018-03-08T07:09:33Z

document/core/exec/instructions.rst

+
+7. Pop the value :math:`\I32.\CONST~i` from the stack.
+
+8. If :math:`i` is larger than the length of :math:`\X{tab}.\TIELEM`, then:


rossberg · 2018-03-08T07:09:42Z

document/core/exec/instructions.rst

+
+9. Pop the value :math:`\I32.\CONST~i` from the stack.
+
+10. If :math:`i` is larger than the length of :math:`\X{tab}.\TIELEM`, then:


rossberg · 2018-03-08T07:22:51Z

document/core/exec/instructions.rst


-7. Let :math:`\X{ft}_{\F{expect}}` be the :ref:`function type <syntax-functype>` :math:`F.\AMODULE.\MITYPES[x]`.
+7. Let :math:`\X{ft}_{\F{expect}}` be the :ref:`function type <syntax-functype>` :math:`F.\AMODULE.\MITYPES[y]`.

 8. Assert: due to :ref:`validation <valid-call_indirect>`, a value with :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.


Indeed. Also needed to change the consecutive line, since the table no longer contains a function address directly. The semantics of elem segments required a similar tweak.

rossberg · 2018-03-08T07:25:48Z

document/core/exec/runtime.rst

 .. _syntax-val:

 Values
 ~~~~~~

-WebAssembly computations manipulate *values* of the four basic :ref:`value types <syntax-valtype>`: :ref:`integers <syntax-int>` and :ref:`floating-point data <syntax-float>` of 32 or 64 bit width each, respectively.
+WebAssembly computations manipulate *values* of the four basic :ref:`value types <syntax-valtype>`: :ref:`integers <syntax-int>` and :ref:`floating-point data <syntax-float>` of 32 or 64 bit width each, or of references, respectively.


Fixed the wording.

rossberg · 2018-03-08T07:26:03Z

document/core/exec/runtime.rst

+
+References other than null are represented with additional :ref:`administrative instructions <syntax-instr-admin>`.
+They either are *function references*, pointing to a specific :ref:`function address <syntax-funcaddr>`,
+or *host references* pointing to an unintrpreted form of :ref:`host address <syntax-hostaddr>` that can be defined by the :ref:`embedder <embedder>`.


rossberg · 2018-03-08T07:27:48Z

document/core/syntax/modules.rst

@@ -147,7 +147,7 @@ The |MTABLES| component of a module defines a vector of *tables* described by th
     \{ \TTYPE~\tabletype \} \\
   \end{array}

-A table is a vector of opaque values of a particular table :ref:`element type <syntax-elemtype>`.
+A table is a vector of opaque values of a particular :ref:`reference type <syntax-reftype>`.


Yes, that's right, except that ref.eq does not operate on tables but on references directly.

rossberg · 2018-03-08T07:30:30Z

document/core/syntax/types.rst

+Reference Types
+~~~~~~~~~~~~~~~
+
+*Reference types* classify 


Oops, this actually was a half-finished edit.

rossberg · 2018-03-08T07:34:41Z

document/core/valid/instructions.rst

+
+* Let :math:`\limits~t` be the :ref:`table type <syntax-tabletype>` :math:`C.\CTABLES[x]`.
+
+* Then the instruction is valid with type :math:`[] \to [t]`.


rossberg · 2018-03-08T07:34:48Z

document/core/valid/instructions.rst

+
+* Let :math:`\limits~t` be the :ref:`table type <syntax-tabletype>` :math:`C.\CTABLES[x]`.
+
+* Then the instruction is valid with type :math:`[t] \to []`.


rossberg · 2018-03-08T07:45:09Z

document/core/valid/instructions.rst

-     C \vdashinstrseq \instr^\ast : [t_1^\ast] \to [t_0^\ast~t^\ast]
+     C \vdashinstrseq \instr^\ast : [t_1^\ast] \to [t_0^\ast~{t'}^\ast]
+     \qquad
+     (\vdashvaltypematch t' \leq t)^\ast


Replaced it with a hyperlinked version.

bnjbvr · 2018-03-13T14:02:55Z

document/core/appendix/algorithm.rst

+
+   type val_type = I32 | I64 | F32 | F64 | Anyref | Anyfunc | Eqref | Nullref
+
+   func is_ref(t : valtype) : bool =


nit: val_type (function parameter)

lukewagner · 2018-03-14T16:45:46Z

document/core/text/modules.rst


 .. math::
   \begin{array}{llclll}
   \production{element segment} & \Telem_I &::=&
-     \text{(}~\text{elem}~~(x{:}\Ttableidx_I)^?~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~y^\ast{:}\Tvec(\Tfuncidx_I)~\text{)} \\ &&& \qquad
-       \Rightarrow\quad \{ \ETABLE~x', \EOFFSET~e, \EINIT~y^\ast \} \\
-       &&& \qquad\qquad\qquad (\iff x' = x^? \neq \epsilon \vee x' = 0) \\


Might want to uplift this change to the v.1 spec as an editorial fix. The new way is much cleaner and I'm not even sure if the original expression parses...

Good point, will do.

lukewagner · 2018-03-14T17:21:09Z

document/core/appendix/algorithm.rst

@@ -70,7 +81,7 @@ However, these variables are not manipulated directly by the main checking funct
     let actual = pop_opd()
     if (actual = Unknown) return expect
     if (expect = Unknown) return actual
-     error_if(actual =/= expect)
+     error_if(not matches(actual, expect))


IIUC, according to the validation rules, (select (ref.null) (get_table ...) (...)) is supposed to validate, since subtyping is applied to ref.null when validating select with t = anyref. To implement this, I think select now needs special treatment below; I expect taking a meet of the two pop_opd()s.

Ah, good catch! This is not just for nullref, subtyping generally changes the way select needs to be handled. To simplify things, I refactored the pseudo code somewhat to make Unknown act more like a bottom type (which has been your view all along, I think :) ).

While fixing this I realised that subtyping also affects how br_table needs to be handled, so I incorporated respective changes as well.

lukewagner · 2018-03-14T18:48:04Z

document/core/syntax/types.rst

+
+The type |ANYFUNC| denotes the infinite union of all references to :ref:`functions <syntax-func>`, regardless of their :ref:`function types <syntax-functype>`.
+
+The type |EQREF| denotes the infinite union of all references that can be compared for equality;


Bikeshed: for symmetry with the other any*, could this perhaps be anyeqref?

lukewagner · 2018-03-14T18:55:39Z

document/core/syntax/types.rst

+
+The type |NULLREF| only contains a single value: the :ref:`null <syntax-ref_null>` reference.
+It is a :ref:`subtype <match-reftype>` of all other reference types.
+The |NULLREF| type cannot be used in a program, it only occurs during :ref:`validation <valid>`.


I'm trying to see how this is the case: as is, it appears that nullref is a valtype which means it can appear in function signatures and as the type of locals. So you can have silly expressions like:

(local $x nulltype) (call $foo (tee_local $x (get_local $x)))

Instead of trying to introduce a validation-only type, can't we just have an operator reftype.null where reftype is later constrained by validation to only allow nullable types?

That is prevented simply by not making nullref part of the "concrete" syntax, i.e., it cannot be expressed in either the binary or the text format. That could be made more explicit by separating it out from value types into a separate class used only for validation, but is it worth it? Alternatively, would a respective note suffice?

A syntax like <reftype>.null cannot nicely be generalised to less primitive reference types. And it seems a bit wasteful to have separate null instructions for each type constructor, especially when they all necessarily produce the same value per subtyping.

We could type-annotate the instruction instead, but that also just seems unnecessary given that we're already buying into subtyping anyway. What the proposed semantics does mirrors the treatment of null expressions in most languages, e.g. Java or C++.

This seems like a point worth discussing at the April meeting.

Ah hah, I hadn't noticed nullref wasn't part of concrete syntax! Yes, that does solve the problem rather elegantly in the spec. In the implementation, though, what will still be annoying is that we'll probably need separate valtype enums for what can appear in locals/signatures (the latter of which takes part in serialization and indirect call ABI matching so we need to be crystal clear about what the cases are) and for what can appear as part of validation. And we'll have to go back and forth between them and ask "which valtype enum do I use here?" and it's not a huge deal, but it'd be nice to avoid if there's not a downside.

And it seems a bit wasteful to have separate null instructions for each type constructor

For this I was assuming a single bytecode "null" followed by the reftype as an immediate (which handles both the primitive and compound types in the encoding)...

We could type-annotate the instruction instead, but that also just seems unnecessary given that we're already buying into subtyping anyway.

... which is what I think you mean here. Agreed we are necessarily buying into subtyping, the only difference here is that the other types will be present in the concrete syntax and so there's not really another option (other than, I suppose, removing subtyping in lieu of a static upcast operator). With null, it seems like we have an option and the non-subtype route seems mildly simpler.

This seems like a point worth discussing at the April meeting.

Yeah, happy to discuss in the group. In the short-term, we were wanting to get going on a prototype impl of this proposal and, because of aforementioned valtype warts, we'd prefer to implement the type-parameterized null. Could you perhaps flip the proposal to that so we can directly implement the proposal (knowing we might have to change if the proposal flips back)?

Well, it's a few hours work on tests and interpreter, too, that I probably want to postpone until it's clear that I won't have to undo it shortly after. But I'm happy to hold back landing these PRs until the meeting. I don’t think that needs to block you from prototyping either version.

rossberg

Thanks for the review!

rossberg · 2018-03-15T09:19:49Z

document/core/appendix/algorithm.rst

@@ -70,7 +81,7 @@ However, these variables are not manipulated directly by the main checking funct
     let actual = pop_opd()
     if (actual = Unknown) return expect
     if (expect = Unknown) return actual
-     error_if(actual =/= expect)
+     error_if(not matches(actual, expect))


Ah, good catch! This is not just for nullref, subtyping generally changes the way select needs to be handled. To simplify things, I refactored the pseudo code somewhat to make Unknown act more like a bottom type (which has been your view all along, I think :) ).

While fixing this I realised that subtyping also affects how br_table needs to be handled, so I incorporated respective changes as well.

rossberg · 2018-03-15T09:20:55Z

document/core/syntax/types.rst

+
+The type |ANYFUNC| denotes the infinite union of all references to :ref:`functions <syntax-func>`, regardless of their :ref:`function types <syntax-functype>`.
+
+The type |EQREF| denotes the infinite union of all references that can be compared for equality;


rossberg · 2018-03-15T09:21:21Z

document/core/text/modules.rst


 .. math::
   \begin{array}{llclll}
   \production{element segment} & \Telem_I &::=&
-     \text{(}~\text{elem}~~(x{:}\Ttableidx_I)^?~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~y^\ast{:}\Tvec(\Tfuncidx_I)~\text{)} \\ &&& \qquad
-       \Rightarrow\quad \{ \ETABLE~x', \EOFFSET~e, \EINIT~y^\ast \} \\
-       &&& \qquad\qquad\qquad (\iff x' = x^? \neq \epsilon \vee x' = 0) \\


Good point, will do.

rossberg · 2018-03-15T09:39:49Z

document/core/syntax/types.rst

+
+The type |NULLREF| only contains a single value: the :ref:`null <syntax-ref_null>` reference.
+It is a :ref:`subtype <match-reftype>` of all other reference types.
+The |NULLREF| type cannot be used in a program, it only occurs during :ref:`validation <valid>`.


That is prevented simply by not making nullref part of the "concrete" syntax, i.e., it cannot be expressed in either the binary or the text format. That could be made more explicit by separating it out from value types into a separate class used only for validation, but is it worth it? Alternatively, would a respective note suffice?

A syntax like <reftype>.null cannot nicely be generalised to less primitive reference types. And it seems a bit wasteful to have separate null instructions for each type constructor, especially when they all necessarily produce the same value per subtyping.

We could type-annotate the instruction instead, but that also just seems unnecessary given that we're already buying into subtyping anyway. What the proposed semantics does mirrors the treatment of null expressions in most languages, e.g. Java or C++.

This seems like a point worth discussing at the April meeting.

See issue #3.

[spec] First go at specification

2bed427

rossberg requested review from binji, flagxor and lukewagner March 7, 2018 15:54

binji reviewed Mar 8, 2018

View reviewed changes

Comments and fixes

472ff1f

rossberg commented Mar 8, 2018

View reviewed changes

Define default values

684e016

bnjbvr reviewed Mar 13, 2018

View reviewed changes

Typo

15762fc

lukewagner reviewed Mar 14, 2018

View reviewed changes

Comments by Luke

71435f4

rossberg commented Mar 15, 2018

View reviewed changes

Fix br_table

29c91d0

rossberg mentioned this pull request Mar 16, 2018

[spec] Address comments by Luke WebAssembly/spec#752

Merged

rossberg added 2 commits March 23, 2018 13:37

Tweak

3e99426

Fix globaltype matching

b302023

rossberg merged commit 1f29a8e into master Apr 4, 2018

aheejin mentioned this pull request Nov 16, 2019

Why is nullref not allowed in binary and text format? #60

Closed

rossberg pushed a commit that referenced this pull request Nov 20, 2019

Include link to gist for benchmark

107c4cc

See issue #3.

taralx mentioned this pull request Jun 12, 2020

Remove type annotations on ref.as_non_null and br_on_null WebAssembly/function-references#31

Merged


		7. Pop the value :math:`\I32.\CONST~i` from the stack.

		8. If :math:`i` is larger than the length of :math:`\X{tab}.\TIELEM`, then:


		9. Pop the value :math:`\I32.\CONST~i` from the stack.

		10. If :math:`i` is larger than the length of :math:`\X{tab}.\TIELEM`, then:


		* Let :math:`\limits~t` be the :ref:`table type <syntax-tabletype>` :math:`C.\CTABLES[x]`.

		* Then the instruction is valid with type :math:`[t] \to []`.


		type val_type = I32 \| I64 \| F32 \| F64 \| Anyref \| Anyfunc \| Eqref \| Nullref

		func is_ref(t : valtype) : bool =


		The type \|ANYFUNC\| denotes the infinite union of all references to :ref:`functions <syntax-func>`, regardless of their :ref:`function types <syntax-functype>`.

		The type \|EQREF\| denotes the infinite union of all references that can be compared for equality;

[spec] First go at specification #3

[spec] First go at specification #3

Conversation

rossberg commented Mar 7, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

rossberg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

lukewagner Mar 14, 2018 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

rossberg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

rossberg commented Mar 7, 2018 •

edited

Loading

lukewagner Mar 14, 2018 •

edited

Loading