Merge pull request #31 from dhil/wasmfx-merge

Merge with WebAssembly/spec

.github/workflows/w3c-publish.yml

@@ -10,6 +10,7 @@ on:
 
 jobs:
   publish-to-w3c-TR:
+    if: github.repository == 'WebAssembly/spec'
     runs-on: ubuntu-latest
     # TODO(dhil): The following effectively disables this workflow. It
     # should be removed before merging with upstream.

document/core/appendix/properties.rst

@@ -825,8 +825,12 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
 
 * Let :math:`\reftype^\ast` be the concatenation of all :math:`\reftype_i` in order.
 
+* Let :math:`m` be the length of :math:`\moduleinst.\MIFUNCS`.
+
 * Let :math:`n` be the length of :math:`\moduleinst.\MIDATAS`.
 
+* Let :math:`x^\ast` be the sequence of :ref:`function indices <syntax-funcidx>` from :math:`0` to :math:`m-1`.
+
 * Then the module instance is valid with :ref:`context <context>`
   :math:`\{\CTYPES~\deftype^\ast,` :math:`\CFUNCS~\functype^\ast,` :math:`\CTABLES~\tabletype^\ast,` :math:`\CMEMS~\memtype^\ast,` :math:`\CGLOBALS~\globaltype^\ast,` \CTAGS~\tagtype^\ast, :math:`\CELEMS~\reftype^\ast,` :math:`\CDATAS~{\ok}^n\}`.
 
@@ -874,7 +878,8 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
          \CGLOBALS & \globaltype^\ast, \\
          \CTAGS & \tagtype^\ast, \\
          \CELEMS & \reftype^\ast, \\
-         \CDATAS & {\ok}^n ~\}
+         \CDATAS & {\ok}^n, \\
+         \CREFS & 0 \dots (|\funcaddr^\ast|-1) ~\}
          \end{array}
        \end{array}
    }

document/core/exec/instructions.rst

@@ -1880,7 +1880,7 @@ Most other vector instructions are defined in terms of numeric operators that ar
 
 .. math::
    \begin{array}{lcl@{\qquad}l}
-   (\V128\K{.}\VCONST~c_1)~\V128\K{.}\vunop &\stepto& (\V128\K{.}\VCONST~c)
+   (\V128\K{.}\VCONST~c_1)~\shape\K{.}\vunop &\stepto& (\V128\K{.}\VCONST~c)
      & (\iff c = \vunop_{\shape}(c_1))
    \end{array}
 

document/core/valid/instructions.rst

@@ -961,7 +961,7 @@ The following auxiliary function denotes the number of lanes in a vector shape,
    \frac{
      \laneidx < \dim(\shape)
    }{
-     C \vdashinstr t\K{x}N\K{.}\EXTRACTLANE\K{\_}\sx^?~\laneidx : [\V128] \to [\unpacked(\shape)]
+     C \vdashinstr \shape\K{.}\EXTRACTLANE\K{\_}\sx^?~\laneidx : [\V128] \to [\unpacked(\shape)]
    }
 
 

document/core/valid/modules.rst

@@ -810,12 +810,26 @@ The :ref:`external types <syntax-externtype>` classifying a module may contain f
   * For each :math:`\tag_i` in :math:`\module.\MTAGS`,
     the definition :math:`\tag_i` must be :ref:`valid <valid-tag>` with a :ref:`tag type <syntax-tagtype>` :math:`\X{ht}_i`.
 
+  * For each :math:`\table_i` in :math:`\module.\MTABLES`,
+    the definition :math:`\table_i` must be :ref:`valid <valid-table>` with a :ref:`table type <syntax-tabletype>` :math:`\X{tt}_i`.
+
+  * For each :math:`\mem_i` in :math:`\module.\MMEMS`,
+    the definition :math:`\mem_i` must be :ref:`valid <valid-mem>` with a :ref:`memory type <syntax-memtype>` :math:`\X{mt}_i`.
+
+  * For each :math:`\global_i` in :math:`\module.\MGLOBALS`,
+    the definition :math:`\global_i` must be :ref:`valid <valid-global>` with a :ref:`global type <syntax-globaltype>` :math:`\X{gt}_i`.
+
   * For each :math:`\elem_i` in :math:`\module.\MELEMS`,
     the segment :math:`\elem_i` must be :ref:`valid <valid-elem>` with :ref:`reference type <syntax-reftype>` :math:`\X{rt}_i`.
 
   * For each :math:`\data_i` in :math:`\module.\MDATAS`,
     the segment :math:`\data_i` must be :ref:`valid <valid-data>`.
 
+* Under the context :math:`C`:
+
+  * For each :math:`\func_i` in :math:`\module.\MFUNCS`,
+    the definition :math:`\func_i` must be :ref:`valid <valid-func>` with a :ref:`function type <syntax-functype>` :math:`\X{ft}_i`.
+
   * If :math:`\module.\MSTART` is non-empty,
     then :math:`\module.\MSTART` must be :ref:`valid <valid-start>`.
 
@@ -825,7 +839,11 @@ The :ref:`external types <syntax-externtype>` classifying a module may contain f
   * For each :math:`\export_i` in :math:`\module.\MEXPORTS`,
     the segment :math:`\export_i` must be :ref:`valid <valid-export>` with :ref:`external type <syntax-externtype>` :math:`\X{et}_i`.
 
-* Let :math:`\X{dt}^\ast` be the concatenation of the internal :ref:`function types <syntax-functype>` :math:`\X{dt}_i`, in index order.
+* The length of :math:`C.\CMEMS` must not be larger than :math:`1`.
+
+* All export names :math:`\export_i.\ENAME` must be different.
+
+* Let :math:`\X{ft}^\ast` be the concatenation of the internal :ref:`function types <syntax-functype>` :math:`\X{ft}_i`, in index order.
 
 * Let :math:`\X{tt}^\ast` be the concatenation of the internal :ref:`table types <syntax-tabletype>` :math:`\X{tt}_i`, in index order.
 
@@ -894,6 +912,9 @@ The :ref:`external types <syntax-externtype>` classifying a module may contain f
        \CREFS~x^\ast \}
      \\
      C' = \{ \CTYPES~C_0.\CTYPES, \CGLOBALS~\X{igt}^\ast, \CFUNCS~(C.\CFUNCS), \CTABLES~(C.\CTABLES), \CMEMS~(C.\CMEMS), \CREFS~(C.\CREFS) \}
+     %C' = C \with \CGLOBALS = \X{igt}^\ast
+     %\qquad
+     %|C.\CMEMS| \leq 1
      \qquad
      (\export.\ENAME)^\ast ~\F{disjoint}
      \\

document/js-api/index.bs

@@ -61,6 +61,7 @@ urlPrefix: https://tc39.github.io/ecma262/; spec: ECMASCRIPT
         text: NativeError Object Structure; url: sec-nativeerror-object-structure
         text: 𝔽; url: #𝔽
         text: ℤ; url: #ℤ
+        text: SameValue; url: sec-samevalue
     type: abstract-op
         text: CreateMethodProperty; url: sec-createmethodproperty
 urlPrefix: https://webassembly.github.io/spec/core/; spec: WebAssembly; type: dfn
@@ -129,6 +130,8 @@ urlPrefix: https://webassembly.github.io/spec/core/; spec: WebAssembly; type: df
     text: struct address; url: exec/runtime.html#syntax-structaddr
     text: array address; url: exec/runtime.html#syntax-arrayaddr
     text: host address; url: exec/runtime.html#syntax-hostaddr
+    text: extern address; url: exec/runtime.html#syntax-externaddr
+    text: page size; url: exec/runtime.html#page-size
     url: syntax/types.html#syntax-numtype
         text: i32
         text: i64
@@ -191,6 +194,11 @@ urlPrefix: https://heycam.github.io/webidl/; spec: WebIDL
         text: create a namespace object; url: create-a-namespace-object
 urlPrefix: https://webassembly.github.io/js-types/js-api/; spec: WebAssembly JS API (JS Type Reflection)
     type: abstract-op; text: FromValueType; url: abstract-opdef-fromvaluetype
+urlPrefix: https://tc39.es/proposal-resizablearraybuffer/; spec: ResizableArrayBuffer proposal
+    type: dfn
+        text: handled; url: sec-hostresizearraybuffer
+        text: IsFixedLengthArrayBuffer; url: sec-isfixedarraybuffer
+        text: HostResizeArrayBuffer; url: sec-hostresizearraybuffer
 </pre>
 
 <pre class='link-defaults'>
@@ -643,6 +651,8 @@ dictionary MemoryDescriptor {
 interface Memory {
   constructor(MemoryDescriptor descriptor);
   unsigned long grow([EnforceRange] unsigned long delta);
+  ArrayBuffer toFixedLengthBuffer();
+  ArrayBuffer toResizableBuffer();
   readonly attribute ArrayBuffer buffer;
 };
 </pre>
@@ -655,10 +665,27 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each
     * \[[BufferObject]] : an {{ArrayBuffer}} whose [=Data Block=] is [=identified with=] the above memory address
 
 <div algorithm>
-    To <dfn>create a memory buffer</dfn> from a [=memory address=] |memaddr|, perform the following steps:
+    To <dfn>create a fixed length memory buffer</dfn> from a [=memory address=] |memaddr|, perform the following steps:
+
+    1. Let |block| be a [=Data Block=] which is [=identified with=] the underlying memory of |memaddr|.
+    1. Let |buffer| be a new {{ArrayBuffer}} with the internal slots \[[ArrayBufferData]], \[[ArrayBufferByteLength]], and \[[ArrayBufferDetachKey]].
+    1. Set |buffer|.\[[ArrayBufferData]] to |block|.
+    1. Set |buffer|.\[[ArrayBufferByteLength]] to the length of |block|.
+    1. Set |buffer|.\[[ArrayBufferDetachKey]] to "WebAssembly.Memory".
+    1. Return |buffer|.
+</div>
+
+<div algorithm>
+    To <dfn>create a resizable memory buffer</dfn> from a [=memory address=] |memaddr| and a |maxsize|, perform the following steps:
 
     1. Let |block| be a [=Data Block=] which is [=identified with=] the underlying memory of |memaddr|.
-    1. Let |buffer| be a new {{ArrayBuffer}} whose \[[ArrayBufferData]] is |block| and \[[ArrayBufferByteLength]] is set to the length of |block|.
+    1. Let |length| be the length of |block|.
+    1. If |maxsize| &gt; (65536 &times; 65536),
+        1. Throw a {{RangeError}} exception.
+    1. Let |buffer| be a new {{ArrayBuffer}} with the internal slots \[[ArrayBufferData]], \[[ArrayBufferByteLength]], \[[ArrayBufferMaxByteLength]], and \[[ArrayBufferDetachKey]].
+    1. Set |buffer|.\[[ArrayBufferData]] to |block|.
+    1. Set |buffer|.\[[ArrayBufferByteLength]] to |length|.
+    1. Set |buffer|.\[[ArrayBufferMaxByteLength]] is |maxsize|.
     1. Set |buffer|.\[[ArrayBufferDetachKey]] to "WebAssembly.Memory".
     1. Return |buffer|.
 </div>
@@ -667,7 +694,7 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each
     To <dfn>initialize a memory object</dfn> |memory| from a [=memory address=] |memaddr|, perform the following steps:
     1. Let |map| be the [=surrounding agent=]'s associated [=Memory object cache=].
     1. Assert: |map|[|memaddr|] doesn't [=map/exist=].
-    1. Let |buffer| be the result of [=create a memory buffer|creating a memory buffer=] from |memaddr|.
+    1. Let |buffer| be the result of [=create a fixed length memory buffer|creating a fixed length memory buffer=] from |memaddr|.
     1. Set |memory|.\[[Memory]] to |memaddr|.
     1. Set |memory|.\[[BufferObject]] to |buffer|.
     1. [=map/Set=] |map|[|memaddr|] to |memory|.
@@ -697,36 +724,96 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each
 </div>
 
 <div algorithm>
-    To <dfn>reset the Memory buffer</dfn> of |memaddr|, perform the following steps:
+    To <dfn>refresh the Memory buffer</dfn> of |memaddr|, perform the following steps:
 
     1. Let |map| be the [=surrounding agent=]'s associated [=Memory object cache=].
     1. Assert: |map|[|memaddr|] [=map/exists=].
     1. Let |memory| be |map|[|memaddr|].
-    1. Perform [=!=] [$DetachArrayBuffer$](|memory|.\[[BufferObject]], "WebAssembly.Memory").
-    1. Let |buffer| be the result of [=create a memory buffer|creating a memory buffer=] from |memaddr|.
-    1. Set |memory|.\[[BufferObject]] to |buffer|.
+    1. Let |buffer| be |memory|.\[[BufferObject]].
+    1. If [=IsFixedLengthArrayBuffer=](|buffer|) is true,
+        1. Perform [=!=] [$DetachArrayBuffer$](|buffer|, "WebAssembly.Memory").
+        1. Let |buffer| be the result of [=create a fixed length memory buffer|creating a fixed length memory buffer=] from |memaddr|.
+        1. Set |memory|.\[[BufferObject]] to |buffer|.
+    1. Otherwise,
+        1. Let |block| be a [=Data Block=] which is [=identified with=] the underlying memory of |memaddr|.
+        1. Set |buffer|.\[[ArrayBufferData]] to |block|.
+        1. Set |buffer|.\[[ArrayBufferByteLength]] to the length of |block|.
 </div>
 
-<div algorithm=dom-Memory-grow>
-    The <dfn method for="Memory">grow(|delta|)</dfn> method, when invoked, performs the following steps:
+<div algorithm>
+    To <dfn>grow the memory buffer</dfn> associated with a [=memory address=] |memaddr| by |delta|, perform the following steps:
+
     1. Let |store| be the [=surrounding agent=]'s [=associated store=].
-    1. Let |memaddr| be **this**.\[[Memory]].
     1. Let |ret| be the [=mem_size=](|store|, |memaddr|).
     1. Let |store| be [=mem_grow=](|store|, |memaddr|, |delta|).
     1. If |store| is [=error=], throw a {{RangeError}} exception.
     1. Set the [=surrounding agent=]'s [=associated store=] to |store|.
-    1. [=Reset the memory buffer=] of |memaddr|.
+    1. [=Refresh the memory buffer=] of |memaddr|.
     1. Return |ret|.
 </div>
 
+<div algorithm=dom-Memory-grow>
+    The <dfn method for="Memory">grow(|delta|)</dfn> method, when invoked, performs the following steps:
+    1. Let |memaddr| be **this**.\[[Memory]].
+    1. Return the result of [=grow the memory buffer|growing the memory buffer=] associated with |memaddr| by |delta|.
+</div>
+
 Immediately after a WebAssembly [=memory.grow=] instruction executes, perform the following steps:
 
 <div algorithm="memory.grow">
     1. If the top of the stack is not [=i32.const=] (−1),
         1. Let |frame| be the [=current frame=].
         1. Assert: due to validation, |frame|.[=frame/module=].[=moduleinst/memaddrs=][0] exists.
         1. Let |memaddr| be the memory address |frame|.[=frame/module=].[=moduleinst/memaddrs=][0].
-        1. [=Reset the memory buffer=] of |memaddr|.
+        1. [=Refresh the memory buffer=] of |memaddr|.
+</div>
+
+<div algorithm=dom-Memory-toFixedLengthBuffer>
+    The <dfn method for="Memory">toFixedLengthBuffer()</dfn> method, when invoked, performs the following steps:
+    1. Let |buffer| be **this**.\[[BufferObject]].
+    1. If [=IsFixedLengthArrayBuffer=](|buffer|) is true, return |buffer|.
+    1. Let |memaddr| be **this**.\[[Memory]].
+    1. Let |fixedBuffer| be the result of [=create a fixed length memory buffer|creating a fixed length memory buffer=] from |memaddr|.
+    1. Perform [=!=] [$DetachArrayBuffer$](|buffer|, "WebAssembly.Memory").
+    1. Set **this**.\[[BufferObject]] to |fixedBuffer|.
+    1. Return |fixedBuffer|.
+</div>
+
+<div algorithm=dom-Memory-toResizableBuffer>
+    The <dfn method for="Memory">toResizableBuffer()</dfn> method, when invoked, performs the following steps:
+    1. Let |buffer| be **this**.\[[BufferObject]].
+    1. If [=IsFixedLengthArrayBuffer=](|buffer|) is false, return |buffer|.
+    1. Let |memaddr| be **this**.\[[Memory]].
+    1. Let |store| be the [=surrounding agent=]'s [=associated store=].
+    1. Let |memtype| be [=mem_type=](|store|, |memaddr|).
+    1. If |memtype| has a max,
+        1. Let |maxsize| be the max value in |memtype|.
+    1. Otherwise,
+        1. Let |maxsize| be 65536 &times; 65536.
+    1. Let |resizableBuffer| be the result of [=create a resizable memory buffer|creating a resizable memory buffer=] from |memaddr| and |maxsize|.
+    1. Perform [=!=] [$DetachArrayBuffer$](|buffer|, "WebAssembly.Memory").
+    1. Set **this**.\[[BufferObject]] to |resizableBuffer|.
+    1. Return |resizableBuffer|.
+</div>
+
+{{ArrayBuffer}} objects returned by a {{Memory}} object must have a size that is a multiple of a WebAssembly [=page size=] (the constant 65536). For this reason [=HostResizeArrayBuffer=] is redefined as follows.
+
+<div algorithm>
+    The <dfn>abstract operation [=HostResizeArrayBuffer=]</dfn> takes arguments |buffer| (an {{ArrayBuffer}}) and |newLength|. It performs the following steps when called.
+
+    1. If |buffer|.\[[ArrayBufferDetachKey]] is "WebAssembly.Memory",
+        1. Let |map| be the [=surrounding agent=]'s associated [=Memory object cache=].
+        1. Assert: |buffer| is the \[[BufferObject]] of exactly one value in |map|.
+        1. [=map/iterate|For each=] |memaddr| &rarr; |mem| in |map|,
+            1. If [=SameValue=](|mem|.\[[BufferObject]], |buffer|) is true,
+                1. Assert: |buffer|.\[[ArrayBufferByteLength]] modulo 65536 is 0.
+                1. Let |lengthDelta| be |newLength| - |buffer|.\[[ArrayBufferByteLength]].
+                1. If |lengthDelta| &lt; 0 or |lengthDelta| modulo 65536 is not 0,
+                    1. Throw a {{RangeError}} exception.
+                1. Let |delta| be |lengthDelta| &div; 65536.
+                1. [=Grow the memory buffer=] associated with |memaddr| by |delta|.
+         1. Return <emu-const>handled</emu-const>.
+    1. Otherwise, return <emu-const>unhandled</emu-const>.
 </div>
 
 <div algorithm>

interpreter/dune

@@ -2,12 +2,7 @@
 
 (library
   (public_name wasm)
-  ; The 'wasm' module shall not be part of the library, as it would start the
-  ; Wasm REPL every time in all the dependencies.
-  ; We exclude the 'wast' module as it is only used for the JS build.
-  ; 'smallint' is a separate test module.
-  (modules :standard \ main wasm smallint wast)
-  (libraries menhirLib)
+  (modules :standard \ main wasm wast smallint)
 )
 
 (executable
@@ -32,26 +27,18 @@
   (preprocess (pps js_of_ocaml-ppx))
 )
 
-(rule
-  (targets wasm.ml)
-  (deps main/main.ml)
-  (action (copy main/main.ml wasm.ml))
-)
+(env (_ (flags (-w +a-4-27-42-44-45-70 -warn-error +a-3))))
 
 (subdir text
-  (rule
-    (target lexer.ml)
-    (deps lexer.mll)
-    (action
-      (chdir %{workspace_root}
-        (run %{bin:ocamllex} -ml -q -o %{target} %{deps})
-      )
-    )
-  )
+  (ocamllex (modules lexer))
   (menhir (modules parser))
 )
 
-(env (_ (flags (-w +a-4-27-42-44-45-70 -warn-error +a-3))))
+(rule
+  (targets wasm.ml)
+  (deps main/main.ml)
+  (action (copy main/main.ml wasm.ml))
+)
 
 (rule
   (alias runtest)

interpreter/dune-project

@@ -1,17 +1,16 @@
 (lang dune 2.9)
 
 (name wasm)
-
-(generate_opam_files true)
-(using menhir 2.1)
-(implicit_transitive_deps false)
-
 (license Apache-2.0)
 (source (github WebAssembly/spec))
 
 (authors "Andreas Rossberg <[email protected]")
 (maintainers "Andreas Rossberg <[email protected]")
 
+(generate_opam_files true)
+(using menhir 2.1)
+(implicit_transitive_deps false)
+
 (package
   (name wasm)
   (synopsis "Library to read and write WebAssembly (Wasm) files and manipulate their AST")

interpreter/text/parse.ml

@@ -9,30 +9,19 @@ sig
   val parse_channel : in_channel -> t
 end
 
-let provider buf () =
-  let tok = Lexer.token buf in
-  let start = Lexing.lexeme_start_p buf in
-  let stop = Lexing.lexeme_end_p buf in
-  tok, start, stop
-
-let convert_pos buf =
-  { Source.left = Lexer.convert_pos buf.Lexing.lex_start_p;
-    Source.right = Lexer.convert_pos buf.Lexing.lex_curr_p
+let convert_pos lexbuf =
+  { Source.left = Lexer.convert_pos lexbuf.Lexing.lex_start_p;
+    Source.right = Lexer.convert_pos lexbuf.Lexing.lex_curr_p
   }
 
 let make (type a) (start : _ -> _ -> a) : (module S with type t = a) =
   (module struct
     type t = a
 
-    let parse name buf =
-      Lexing.set_filename buf name;
-      try
-        MenhirLib.Convert.Simplified.traditional2revised start (provider buf)
-      with
-      | Parser.Error ->
-        raise (Syntax (convert_pos buf, "unexpected token"))
-      | Syntax (region, s) when region <> Source.no_region ->
-        raise (Syntax (convert_pos buf, s))
+    let parse name lexbuf =
+      Lexing.set_filename lexbuf name;
+      try start Lexer.token lexbuf with Parser.Error ->
+        raise (Syntax (convert_pos lexbuf, "unexpected token"))
 
     let parse_string s =
       parse "string" (Lexing.from_string ~with_positions:true s)