[spec/interpreter/test] Add table bulk instructions missing from bulk op proposal #35

rossberg · 2019-04-02T08:40:32Z

Adds table.size, table.grow, table.fill to overview, spec, interpreter, and tests, as decided at recent CG meeting. Also adds a few more tests for table.get and table.set.

Edit: Also, change interpreter's segment encoding to match bulk ops proposal, addressing #18. (Not updated in spec yet, since corresponding spec text is still missing from bulk ops proposal.)

lars-t-hansen · 2019-04-03T06:30:29Z

proposals/reference-types/Overview.md

+  - `table.grow $x : [t i32] -> [i32]`
+    - iff `$x : table t`
+  - the first operand of `table.grow` is an initialisation value (for compatibility with future extensions to the type system, such as non-nullable references)
+


Any particular justification for the argument ordering for table.grow? I ask, since we chose the other ordering (init value on top of stack, delta underneath). I assume what you have here is compatible with v8?

Yes, I tried to follow the convention of the other bulk ops, which always have argument order (dest, source, length). In particular, this would most closely match table.fill, except for omitting the start index.
(AFAIAA, V8 does not implement these instructions yet.)

And table.fill follows memory.fill, fair enough. I'll file a bug to fix it on our end.

Though it's a bit odd that FF would be shipping features for which we don't even have a spec draft?

Well, shipping in Nightly only and it won't ride the trains until we're all aligned, but apart from this wrinkle I think we've anticipated the draft fairly well :)

lars-t-hansen · 2019-04-03T07:34:12Z

interpreter/binary/decode.ml

+    (match op s with
+    | 0x0f -> table_fill (at var s)
+    | 0x10 -> table_size (at var s)
+    | 0x11 -> table_grow (at var s)


These encodings contradict the table in #29 (first and last comments), which we have used as the basis for the decoder in Firefox. If possible I'd like these to change here since we're shipping already. Proposed encodings there are table_grow == 0x0f, table_size == 0x10, table_fill == 0x11. Ditto the encoder and any other spots.

Ah, sorry, I completely forgot about #29. Changed. (Though it's a bit odd that FF would be shipping features for which we don't even have a spec draft?)

lars-t-hansen · 2019-04-03T07:35:31Z

interpreter/binary/encode.ml

      | TableGet x -> op 0x25; var x
      | TableSet x -> op 0x26; var x
+      | TableSize x -> op 0xfc; op 0x10; var x
+      | TableGrow x -> op 0xfc; op 0x11; var x
+      | TableFill x -> op 0xfc; op 0x0f; var x


See comments in decode.ml re the encodings here.

lars-t-hansen · 2019-04-03T07:53:07Z

interpreter/runtime/table.mli

 val type_of : table -> table_type
 val size : table -> size
-val grow : table -> size -> unit (* raises SizeOverflow, SizeLimit *)
+val grow : table -> size -> ref_ -> unit (* raises SizeOverflow, SizeLimit *)


Nit: add OutOfMemory to the comment here?

lars-t-hansen · 2019-04-03T07:53:36Z

interpreter/runtime/table.mli


-val alloc : table_type -> table
+val alloc : table_type -> ref_ -> table


Nit: add comment that this can raise OutOfMemory?

lars-t-hansen · 2019-04-03T08:02:22Z

test/core/table_fill.wast

+
+(assert_trap
+  (invoke "fill" (i32.const 8) (ref.host 6) (i32.const 3))
+  "out of bounds"


In this case we also want to check that there was initialization of the elements up to the bound.

Isn't that what the next 3 asserts are doing, or did you mean something else?

Sorry, my oversight - eyes glazing over...

lars-t-hansen · 2019-04-03T08:07:23Z

document/core/binary/instructions.rst


 .. math::
   \begin{array}{llclll}
   \production{instruction} & \Binstr &::=& \dots \\ &&|&
     \hex{25}~~x{:}\Btableidx &\Rightarrow& \TABLEGET~x \\ &&|&
-     \hex{26}~~x{:}\Btableidx &\Rightarrow& \TABLESET~x \\
+     \hex{26}~~x{:}\Btableidx &\Rightarrow& \TABLESET~x \\ &&|&
+     \hex{FC}~\hex{0F}~~x{:}\Btableidx &\Rightarrow& \TABLEFILL~x \\ &&|&


See notes later about encodings here.

lars-t-hansen · 2019-04-03T08:11:30Z

document/core/exec/instructions.rst

+7. Assert: due to :ref:`validation <valid-table.grow>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
+
+8. Pop the value :math:`\I32.\CONST~n` from the stack.
+


I think we're missing any handling of the initializer argument here?

Good catch, fixed. That meant also adjusting the meta function and the embedding interface accordingly to support an initialisation value.

lars-t-hansen · 2019-04-03T08:16:54Z

document/core/exec/instructions.rst

+
+5. Let :math:`\X{tab}` be the :ref:`table instance <syntax-tableinst>` :math:`S.\STABLES[a]`.
+
+6. Assert: due to :ref:`validation <valid-table.fill>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.


Technically this is possibly a little dodgy (ditto subsequent clauses, ditto clauses for TABLESET): since we're directly manipulating the stack in the recursive call below, asserting that this is true as a consequence of validation is questionable. I'm not sure it's worth fixing though.

Yes, fair point. I think there are actually a few other such assertions already where, strictly speaking, having the right value on the stack is rather a consequence of soundness.

lars-t-hansen

Looks good in general, thanks for doing this. I'd like to see the opcode encodings changed to values previously agreed upon in #29. I'd like to have a discussion about argument ordering for table.grow, as Firefox is now in conflict with this spec.

rossberg

Comments addresses. Also applied some minor adaptation to JS API.

See comment below regarding operand order for table.grow.

rossberg · 2019-04-03T08:12:41Z

interpreter/binary/decode.ml

+    (match op s with
+    | 0x0f -> table_fill (at var s)
+    | 0x10 -> table_size (at var s)
+    | 0x11 -> table_grow (at var s)


Ah, sorry, I completely forgot about #29. Changed. (Though it's a bit odd that FF would be shipping features for which we don't even have a spec draft?)

rossberg · 2019-04-03T08:15:06Z

interpreter/runtime/table.mli


-val alloc : table_type -> table
+val alloc : table_type -> ref_ -> table


rossberg · 2019-04-03T08:15:44Z

interpreter/runtime/table.mli

 val type_of : table -> table_type
 val size : table -> size
-val grow : table -> size -> unit (* raises SizeOverflow, SizeLimit *)
+val grow : table -> size -> ref_ -> unit (* raises SizeOverflow, SizeLimit *)


rossberg · 2019-04-03T08:16:25Z

proposals/reference-types/Overview.md

+  - `table.grow $x : [t i32] -> [i32]`
+    - iff `$x : table t`
+  - the first operand of `table.grow` is an initialisation value (for compatibility with future extensions to the type system, such as non-nullable references)
+


Yes, I tried to follow the convention of the other bulk ops, which always have argument order (dest, source, length). In particular, this would most closely match table.fill, except for omitting the start index.
(AFAIAA, V8 does not implement these instructions yet.)

rossberg · 2019-04-03T08:18:27Z

test/core/table_fill.wast

+
+(assert_trap
+  (invoke "fill" (i32.const 8) (ref.host 6) (i32.const 3))
+  "out of bounds"


Isn't that what the next 3 asserts are doing, or did you mean something else?

rossberg · 2019-04-03T08:37:27Z

document/core/exec/instructions.rst

+7. Assert: due to :ref:`validation <valid-table.grow>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
+
+8. Pop the value :math:`\I32.\CONST~n` from the stack.
+


Good catch, fixed. That meant also adjusting the meta function and the embedding interface accordingly to support an initialisation value.

rossberg · 2019-04-03T08:42:42Z

document/core/exec/instructions.rst

+
+5. Let :math:`\X{tab}` be the :ref:`table instance <syntax-tableinst>` :math:`S.\STABLES[a]`.
+
+6. Assert: due to :ref:`validation <valid-table.fill>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.


Yes, fair point. I think there are actually a few other such assertions already where, strictly speaking, having the right value on the stack is rather a consequence of soundness.

rossberg · 2019-04-03T09:15:04Z

Thanks for reviewing!

This commit fixes #34 by specifying that the flags field (which indicates if a segment is passive) is a `varuint32` instead of a `uint8`. It was discovered in #34 that the memory index located at that position today is a `varuint32`, which can be validly encoded as `0x80 0x00` in addition to `0x00` (in addition to a number of other encodings). This means that if the first field were repurposed as a single byte of flags, it would break these existing modules that work today. It's not currently known how many modules in the wild actually take advantage of such an encoding, but it's probably better to be safe than sorry! Closes #34

rossberg added 4 commits March 31, 2019 01:13

Interpreter

4fd1af5

[spec] Add table.size/grow/fill

405a5fa

[test] More tests for table instructions

dd03821

Eps

31574fb

rossberg requested a review from lars-t-hansen April 2, 2019 08:40

rossberg added 2 commits April 2, 2019 10:53

Reorder byte codes for slightly more consistency

fa45692

[interpreter] Adjust segment encoding to match bulk proposal

10e7345

lars-t-hansen reviewed Apr 3, 2019

View reviewed changes

lars-t-hansen suggested changes Apr 3, 2019

View reviewed changes

Comments and tweaks to JS API

daeaa93

rossberg commented Apr 3, 2019

View reviewed changes

lars-t-hansen approved these changes Apr 3, 2019

View reviewed changes

rossberg merged commit c3d5cbc into master Apr 3, 2019

rossberg mentioned this pull request Apr 3, 2019

Coordinate with bulk table ops / clarify encoding of the table index #18

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[spec/interpreter/test] Add table bulk instructions missing from bulk op proposal #35

[spec/interpreter/test] Add table bulk instructions missing from bulk op proposal #35

rossberg commented Apr 2, 2019 •

edited

Loading

lars-t-hansen Apr 3, 2019

rossberg Apr 3, 2019

lars-t-hansen Apr 3, 2019

lars-t-hansen Apr 3, 2019

rossberg Apr 3, 2019

lars-t-hansen Apr 3, 2019

lars-t-hansen Apr 3, 2019

rossberg Apr 3, 2019

lars-t-hansen Apr 3, 2019

rossberg Apr 3, 2019

lars-t-hansen Apr 3, 2019 •

edited

Loading

rossberg Apr 3, 2019

lars-t-hansen Apr 3, 2019

lars-t-hansen Apr 3, 2019

lars-t-hansen Apr 3, 2019

rossberg Apr 3, 2019

lars-t-hansen Apr 3, 2019

rossberg Apr 3, 2019

lars-t-hansen left a comment

rossberg left a comment

rossberg Apr 3, 2019

rossberg Apr 3, 2019

rossberg Apr 3, 2019

rossberg Apr 3, 2019

rossberg Apr 3, 2019

rossberg Apr 3, 2019

rossberg Apr 3, 2019

rossberg commented Apr 3, 2019


		val alloc : table_type -> table
		val alloc : table_type -> ref_ -> table

		7. Assert: due to :ref:`validation <valid-table.grow>`, a value of :ref:`value type <syntax-valtype>` \|I32\| is on the top of the stack.

		8. Pop the value :math:`\I32.\CONST~n` from the stack.


		5. Let :math:`\X{tab}` be the :ref:`table instance <syntax-tableinst>` :math:`S.\STABLES[a]`.

		6. Assert: due to :ref:`validation <valid-table.fill>`, a value of :ref:`value type <syntax-valtype>` \|I32\| is on the top of the stack.

[spec/interpreter/test] Add table bulk instructions missing from bulk op proposal #35

[spec/interpreter/test] Add table bulk instructions missing from bulk op proposal #35

Conversation

rossberg commented Apr 2, 2019 • 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

lars-t-hansen Apr 3, 2019 • 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

lars-t-hansen left a 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

rossberg commented Apr 3, 2019

rossberg commented Apr 2, 2019 •

edited

Loading

lars-t-hansen Apr 3, 2019 •

edited

Loading