Skip to content

Commit

Permalink
Merge branch 'wasm3'
Browse files Browse the repository at this point in the history
  • Loading branch information
rossberg committed Apr 12, 2024
2 parents ff7ca55 + 24ab598 commit 3ec1e39
Show file tree
Hide file tree
Showing 8 changed files with 164 additions and 60 deletions.
37 changes: 37 additions & 0 deletions .github/workflows/w3c-publish.yml
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
name: Publish to W3C TR space

on:
push:
branches: [ main ]
paths: [ .github/**, document/** ]

# Allows you to run this workflow manually from the Actions tab
workflow_dispatch:

jobs:
publish-to-w3c-TR:
if: github.repository == 'WebAssembly/spec'
runs-on: ubuntu-latest
steps:
- name: Checkout repo
uses: actions/checkout@v2
with:
submodules: "recursive"
- name: Setup Node.js
uses: actions/setup-node@v3
with:
node-version: 16
- name: Setup Bikeshed
run: pip install bikeshed && bikeshed update
- name: Setup TexLive
run: sudo apt-get update -y && sudo apt-get install -y latexmk texlive-latex-recommended texlive-latex-extra texlive-fonts-recommended
- name: Setup Sphinx
run: pip install six && pip install sphinx==5.1.0
- name: Publish all specs to their https://www.w3.org/TR/ URLs
run: cd document && make -e WD-echidna-CI
env:
STATUS: --md-status=WD
W3C_ECHIDNA_TOKEN_CORE: ${{ secrets.W3C_ECHIDNA_TOKEN_CORE }}
W3C_ECHIDNA_TOKEN_JSAPI: ${{ secrets.W3C_ECHIDNA_TOKEN_JSAPI }}
W3C_ECHIDNA_TOKEN_WEBAPI: ${{ secrets.W3C_ECHIDNA_TOKEN_WEBAPI }}
YARN_ENABLE_IMMUTABLE_INSTALLS: false
9 changes: 7 additions & 2 deletions document/core/appendix/properties.rst
Original file line number Diff line number Diff line change
Expand Up @@ -825,10 +825,14 @@ 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\}`.
: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,` :math:`\CREFS~x^\ast\}`.

.. math::
~\\[-1ex]
Expand Down Expand Up @@ -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}
}
Expand Down
2 changes: 1 addition & 1 deletion document/core/exec/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down
2 changes: 1 addition & 1 deletion document/core/valid/instructions.rst
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
}
Expand Down
111 changes: 99 additions & 12 deletions document/js-api/index.bs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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'>
Expand Down Expand Up @@ -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>
Expand All @@ -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>
Expand All @@ -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|.
Expand Down Expand Up @@ -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>
Expand Down
29 changes: 8 additions & 21 deletions interpreter/dune
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Expand Down
9 changes: 4 additions & 5 deletions interpreter/dune-project
Original file line number Diff line number Diff line change
@@ -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")
Expand Down
25 changes: 7 additions & 18 deletions interpreter/text/parse.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down

0 comments on commit 3ec1e39

Please sign in to comment.