diff --git a/.github/workflows/ci-interpreter.yml b/.github/workflows/ci-interpreter.yml index 3ce4327a1..6cd994f65 100644 --- a/.github/workflows/ci-interpreter.yml +++ b/.github/workflows/ci-interpreter.yml @@ -12,6 +12,9 @@ on: # Allows you to run this workflow manually from the Actions tab workflow_dispatch: +permissions: + contents: read + jobs: interpreter: runs-on: ubuntu-latest @@ -21,11 +24,9 @@ jobs: - name: Setup OCaml uses: ocaml/setup-ocaml@v3 with: - ocaml-compiler: 4.14.x - - name: Setup OCaml tools - run: opam install --yes ocamlfind.1.9.5 js_of_ocaml.4.0.0 js_of_ocaml-ppx.4.0.0 + ocaml-compiler: 5.04.x - name: Build interpreter - run: cd interpreter && opam exec make + run: cd interpreter && opam exec make jsdeps wasm # Neither V8 nor SpiderMonkey can currently handle all 3.0 tests, so we disable checking JS translation for now. #- name: Setup Node.js # uses: actions/setup-node@v4 diff --git a/.github/workflows/ci-spec.yml b/.github/workflows/ci-spec.yml index 1b32bcf54..fc2c8504d 100644 --- a/.github/workflows/ci-spec.yml +++ b/.github/workflows/ci-spec.yml @@ -2,37 +2,118 @@ name: CI for specs on: push: - branches: [ main, wasm-3.0 ] - paths: [ .github/**, document/**, spectec/**, specification/** ] + branches: [ main ] + paths: [ .github/**, document/**, spectec/src/**, specification/** ] pull_request: - branches: [ main, wasm-3.0 ] - paths: [ .github/**, document/**, spectec/**, specification/** ] + branches: [ main ] + paths: [ .github/**, document/**, spectec/src/**, specification/** ] # Allows you to run this workflow manually from the Actions tab workflow_dispatch: +permissions: + contents: read + +# Path within the published site recording the commit the baseline was rendered +# from, both as provenance and so a run can tell the copy is still current. +env: + BASELINE_STAMP: upstream/baseline-sha + jobs: ensure-wasm-latest: - if: ${{ github.repository == 'WebAssembly/spec' }} runs-on: ubuntu-latest steps: - name: Checkout repo uses: actions/checkout@v4 - name: Diff wasm-latest - run: bash .github/workflows/diff-wasm-latest.sh + if: ${{ github.repository == 'WebAssembly/spec' }} + run: cd specification && bash diff-wasm-latest.sh + + # Forks (i.e. proposal repos) also render the spec at the commit where they + # last diverged from their parent repo, so the proposal can be compared + # against an unmodified baseline. That baseline is published under /upstream. + resolve-baseline: + runs-on: ubuntu-latest + outputs: + variants: ${{ steps.resolve.outputs.variants }} + # The commit the baseline is rendered from, empty when there is none. A + # baseline absent from variants is one already published under /upstream. + base-sha: ${{ steps.resolve.outputs.base-sha }} + steps: + - name: Checkout repo + uses: actions/checkout@v4 + with: + # merge-base needs the full history + fetch-depth: 0 + - name: Resolve upstream baseline + id: resolve + env: + GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} + REPOSITORY: ${{ github.repository }} + run: | + set -euo pipefail + # Written once on whichever path exits below, so these defaults stand + # unless the checks further down replace them. + variants='["head"]' + base='' + write_outputs() { + echo "variants=$variants" >> "$GITHUB_OUTPUT" + echo "base-sha=$base" >> "$GITHUB_OUTPUT" + } + trap write_outputs EXIT + if [ "$REPOSITORY" = "WebAssembly/spec" ]; then + echo "Canonical repo, no upstream baseline." + exit 0 + fi + # A copy already on the site is left in place unless a newer baseline + # is rendered below. + published='' + if encoded=$(gh api "repos/$REPOSITORY/contents/$BASELINE_STAMP?ref=gh-pages" --jq .content 2>/dev/null); then + published=$(printf '%s' "$encoded" | base64 -d | tr -d '[:space:]') + fi + parent=$(gh api "repos/$REPOSITORY" --jq '.parent.full_name // ""' 2>/dev/null) || parent='' + if [ -z "$parent" ]; then + echo "::warning::Could not determine the parent repo, not rendering an upstream copy." + exit 0 + fi + if ! git fetch --no-tags --quiet "https://github.com/$parent.git" main; then + echo "::warning::Could not fetch $parent, not rendering an upstream copy." + exit 0 + fi + if ! merge_base=$(git merge-base HEAD FETCH_HEAD); then + echo "::warning::No common ancestor with $parent, no upstream copy." + exit 0 + fi + if [ "$merge_base" = "$(git rev-parse HEAD)" ]; then + echo "::notice::No divergence from $parent, no upstream copy." + exit 0 + fi + base=$merge_base + if [ "$base" = "$published" ]; then + echo "::notice::Baseline $base is already published, keeping that copy." + exit 0 + fi + echo "Upstream baseline: $base (from $parent)" + variants='["head","upstream"]' build-core-spec: runs-on: ubuntu-latest + needs: resolve-baseline + strategy: + fail-fast: false + matrix: + variant: ${{ fromJSON(needs.resolve-baseline.outputs.variants) }} steps: - name: Checkout repo uses: actions/checkout@v4 with: submodules: "recursive" + ref: ${{ matrix.variant == 'upstream' && needs.resolve-baseline.outputs.base-sha || '' }} - name: Setup OCaml uses: ocaml/setup-ocaml@v3 with: - ocaml-compiler: 4.14.x + ocaml-compiler: 5.04.x - name: Setup Dune run: opam install --yes dune menhir mdx zarith && opam exec dune --version - name: Setup Node.js @@ -51,110 +132,167 @@ jobs: run: cd document/core && opam exec make main - name: Run Bikeshed run: cd document/core && opam exec make bikeshed + - name: Stage artifact at its path on the site + run: mkdir -p _site && mv document/core/_build/html _site/core - name: Upload artifact uses: actions/upload-artifact@v4 with: - name: core-rendered - path: document/core/_build/html + name: core-rendered-${{ matrix.variant }} + path: _site build-js-api-spec: runs-on: ubuntu-latest + needs: resolve-baseline + strategy: + fail-fast: false + matrix: + variant: ${{ fromJSON(needs.resolve-baseline.outputs.variants) }} steps: - name: Checkout repo uses: actions/checkout@v4 + with: + ref: ${{ matrix.variant == 'upstream' && needs.resolve-baseline.outputs.base-sha || '' }} - name: Setup Bikeshed run: pip install bikeshed && bikeshed update - name: Run Bikeshed run: bikeshed spec "document/js-api/index.bs" "document/js-api/index.html" + - name: Stage artifact at its path on the site + run: mkdir -p _site/js-api && mv document/js-api/index.html _site/js-api/ - name: Upload artifact uses: actions/upload-artifact@v4 with: - name: js-api-rendered - path: document/js-api/index.html + name: js-api-rendered-${{ matrix.variant }} + path: _site build-web-api-spec: runs-on: ubuntu-latest + needs: resolve-baseline + strategy: + fail-fast: false + matrix: + variant: ${{ fromJSON(needs.resolve-baseline.outputs.variants) }} steps: - name: Checkout repo uses: actions/checkout@v4 + with: + ref: ${{ matrix.variant == 'upstream' && needs.resolve-baseline.outputs.base-sha || '' }} - name: Setup Bikeshed run: pip install bikeshed && bikeshed update - name: Run Bikeshed run: bikeshed spec "document/web-api/index.bs" "document/web-api/index.html" + - name: Stage artifact at its path on the site + run: mkdir -p _site/web-api && mv document/web-api/index.html _site/web-api/ - name: Upload artifact uses: actions/upload-artifact@v4 with: - name: web-api-rendered - path: document/web-api/index.html + name: web-api-rendered-${{ matrix.variant }} + path: _site build-code-metadata-spec: runs-on: ubuntu-latest + needs: resolve-baseline + strategy: + fail-fast: false + matrix: + variant: ${{ fromJSON(needs.resolve-baseline.outputs.variants) }} steps: - name: Checkout repo uses: actions/checkout@v4 with: submodules: "recursive" + ref: ${{ matrix.variant == 'upstream' && needs.resolve-baseline.outputs.base-sha || '' }} - 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==8.1.3 - name: Build main spec run: cd document/metadata/code && make main + - name: Stage artifact at its path on the site + run: mkdir -p _site/metadata && mv document/metadata/code/_build/html _site/metadata/code - name: Upload artifact uses: actions/upload-artifact@v4 with: - name: code-metadata-rendered - path: document/metadata/code/_build/html + name: code-metadata-rendered-${{ matrix.variant }} + path: _site build-legacy-exceptions-core-spec: runs-on: ubuntu-latest + needs: resolve-baseline + strategy: + fail-fast: false + matrix: + variant: ${{ fromJSON(needs.resolve-baseline.outputs.variants) }} steps: - name: Checkout repo uses: actions/checkout@v4 with: submodules: "recursive" + ref: ${{ matrix.variant == 'upstream' && needs.resolve-baseline.outputs.base-sha || '' }} - 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==8.1.3 - name: Build main spec run: cd document/legacy/exceptions/core && make main + - name: Stage artifact at its path on the site + run: mkdir -p _site/legacy/exceptions && mv document/legacy/exceptions/core/_build/html _site/legacy/exceptions/core - name: Upload artifact uses: actions/upload-artifact@v4 with: - name: legacy-exceptions-core-rendered - path: document/legacy/exceptions/core/_build/html + name: legacy-exceptions-core-rendered-${{ matrix.variant }} + path: _site build-legacy-exceptions-js-api-spec: runs-on: ubuntu-latest + needs: resolve-baseline + strategy: + fail-fast: false + matrix: + variant: ${{ fromJSON(needs.resolve-baseline.outputs.variants) }} steps: - name: Checkout repo uses: actions/checkout@v4 + with: + ref: ${{ matrix.variant == 'upstream' && needs.resolve-baseline.outputs.base-sha || '' }} - name: Setup Bikeshed run: pip install bikeshed && bikeshed update - name: Run Bikeshed run: bikeshed spec "document/legacy/exceptions/js-api/index.bs" "document/legacy/exceptions/js-api/index.html" + - name: Stage artifact at its path on the site + run: mkdir -p _site/legacy/exceptions/js-api && mv document/legacy/exceptions/js-api/index.html _site/legacy/exceptions/js-api/ - name: Upload artifact uses: actions/upload-artifact@v4 with: - name: legacy-exceptions-js-api-rendered - path: document/legacy/exceptions/js-api/index.html + name: legacy-exceptions-js-api-rendered-${{ matrix.variant }} + path: _site build-spec-versions: runs-on: ubuntu-latest + needs: resolve-baseline + strategy: + fail-fast: false + matrix: + variant: ${{ fromJSON(needs.resolve-baseline.outputs.variants) }} steps: - name: Checkout repo uses: actions/checkout@v4 + with: + ref: ${{ matrix.variant == 'upstream' && needs.resolve-baseline.outputs.base-sha || '' }} + - name: Stage artifact at its path on the site + run: mkdir -p _site && mv document/versions _site/versions - name: Upload artifacts uses: actions/upload-artifact@v4 with: - name: versions-rendered - path: document/versions/ + name: versions-rendered-${{ matrix.variant }} + path: _site publish-spec: runs-on: ubuntu-latest + permissions: + contents: write needs: - ensure-wasm-latest + - resolve-baseline - build-core-spec - build-js-api-spec - build-web-api-spec @@ -165,43 +303,40 @@ jobs: steps: - name: Checkout repo uses: actions/checkout@v4 + with: + # The baseline's index.html is read out of the history below + fetch-depth: 0 - name: Create output directory run: mkdir _output && cp document/index.html _output/index.html - - name: Download core spec artifact - uses: actions/download-artifact@v4 - with: - name: core-rendered - path: _output/core - - name: Download JS API spec artifact - uses: actions/download-artifact@v4 - with: - name: js-api-rendered - path: _output/js-api - - name: Download Web API spec artifact - uses: actions/download-artifact@v4 - with: - name: web-api-rendered - path: _output/web-api - - name: Download code metadata spec artifact - uses: actions/download-artifact@v4 - with: - name: code-metadata-rendered - path: _output/metadata/code - - name: Download legacy exceptions core spec artifact - uses: actions/download-artifact@v4 - with: - name: legacy-exceptions-core-rendered - path: _output/legacy/exceptions/core - - name: Download legacy exceptions JS API spec artifact + - name: Download rendered documents uses: actions/download-artifact@v4 with: - name: legacy-exceptions-js-api-rendered - path: _output/legacy/exceptions/js-api - - name: Download spec versions artifacts + pattern: '*-rendered-head' + merge-multiple: true + path: _output + - name: Download upstream baseline documents + if: contains(fromJSON(needs.resolve-baseline.outputs.variants), 'upstream') uses: actions/download-artifact@v4 with: - name: versions-rendered - path: _output/versions + pattern: '*-rendered-upstream' + merge-multiple: true + path: _output/upstream + - name: Record the upstream baseline + if: contains(fromJSON(needs.resolve-baseline.outputs.variants), 'upstream') + env: + BASE_SHA: ${{ needs.resolve-baseline.outputs.base-sha }} + run: | + set -euo pipefail + git show "$BASE_SHA:document/index.html" > _output/upstream/index.html + echo "$BASE_SHA" > "_output/$BASELINE_STAMP" + - name: Keep the upstream baseline copy already published + if: needs.resolve-baseline.outputs.base-sha != '' && !contains(fromJSON(needs.resolve-baseline.outputs.variants), 'upstream') + run: | + set -euo pipefail + # Publishing replaces the whole site, so the copy has to be carried + # over explicitly rather than just left in place. + git fetch --no-tags --depth 1 origin gh-pages + git archive FETCH_HEAD upstream | tar -x -C _output - name: Publish to GitHub Pages if: github.ref == 'refs/heads/main' uses: peaceiris/actions-gh-pages@v4 diff --git a/.github/workflows/ci-spectec.yml b/.github/workflows/ci-spectec.yml index cb56e2fff..b7ea336f0 100644 --- a/.github/workflows/ci-spectec.yml +++ b/.github/workflows/ci-spectec.yml @@ -12,6 +12,9 @@ on: # Allows you to run this workflow manually from the Actions tab workflow_dispatch: +permissions: + contents: read + jobs: spec-tec: runs-on: ubuntu-latest @@ -21,7 +24,7 @@ jobs: - name: Setup OCaml uses: ocaml/setup-ocaml@v3 with: - ocaml-compiler: 4.14.x + ocaml-compiler: 5.04.x - name: Setup Dune run: opam install --yes dune menhir mdx zarith - name: Setup Latex diff --git a/.github/workflows/w3c-publish.yml b/.github/workflows/w3c-publish.yml index d2efb1601..dee2bbe8f 100644 --- a/.github/workflows/w3c-publish.yml +++ b/.github/workflows/w3c-publish.yml @@ -5,8 +5,6 @@ on: # Disable on forks! branches: [ main ] paths: [ .github/**, document/**, specification/** ] - pull_request: - paths: [ .github/**, document/**, specification/** ] # Allows you to run this workflow manually from the Actions tab, gh CLI tool, # or REST API. THe w3c-status options correspond to the valid options for @@ -34,8 +32,12 @@ env: YARN_ENABLE_IMMUTABLE_INSTALLS: false W3C_STATUS: ${{ github.event_name == 'workflow_dispatch' && inputs.w3c-status || 'CRD' }} +permissions: + contents: read + jobs: publish-to-w3c-TR: + if: ${{ github.repository == 'WebAssembly/spec' }} strategy: fail-fast: false matrix: @@ -49,7 +51,7 @@ jobs: - name: Setup OCaml uses: ocaml/setup-ocaml@v3 with: - ocaml-compiler: 4.14.x + ocaml-compiler: 5.04.x - name: Setup Dune if: ${{ matrix.spec == 'core' }} run: opam install --yes dune menhir mdx zarith && opam exec dune --version diff --git a/LICENSE b/LICENSE index de2cac692..ce8035027 100644 --- a/LICENSE +++ b/LICENSE @@ -3,6 +3,8 @@ Please see the LICENSE file in each top-level directory for the terms applicable The relevant directories and licenses are: document/ - W3C Software and Document Notice and License +spectec/ - Apache License 2.0 interpreter/ - Apache License 2.0 test/ - Apache License 2.0 -papers/ - Creative Commons Attribution 4.0 International License +proposals/ - Creative Commons Universal 1.0 International License (CC0) +papers/ - Creative Commons Attribution 4.0 International License (CC BY 4.0) diff --git a/document/README.md b/document/README.md index ace0b7d2b..419fcac25 100644 --- a/document/README.md +++ b/document/README.md @@ -26,16 +26,16 @@ Please make sure to only use that once a change has approval. ### Prerequisites -You will need `python3.7`, and `pip`. `pip` should come with Python, if not follow [these installation instructions for `pip`](https://pip.pypa.io/en/stable/installing/), or check your system package manager for `pip3`. +You will need `python3.10`, and `pip`. `pip` should come with Python, if not follow [these installation instructions for `pip`](https://pip.pypa.io/en/stable/installing/), or check your system package manager for `pip3`. -> Important: you will need the version of pip that works with `python3.7`. +> Important: you will need the version of pip that works with `python3.10`. Use something like [`pipenv`](https://pipenv.pypa.io/) to keep your system installation of Python clean. ``` pip install pipenv -pipenv --python 3.7 +pipenv --python 3.10 pipenv shell ``` diff --git a/document/core/Makefile b/document/core/Makefile index 1f28a7480..e11e7894e 100644 --- a/document/core/Makefile +++ b/document/core/Makefile @@ -134,6 +134,7 @@ clean: rm -rf $(SPLICEDIR) rm -rf $(BUILDDIR) rm -rf $(STATICDIR) + rm -rf $(SPLICEDIR) rm -f $(GENERATED) .PHONY: html html-nested @@ -351,7 +352,7 @@ latex: latexpdf: $(GENERATED) $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex @echo "Running LaTeX files through pdflatex..." - $(MAKE) -C $(BUILDDIR)/latex LATEXMKOPTS=" $(BUILDDIR)/latex/LOG 2>&1 || cat $(BUILDDIR)/latex/LOG + $(MAKE) -C $(BUILDDIR)/latex LATEXMKOPTS=" -file-line-error -halt-on-error" all-pdf >$(BUILDDIR)/latex/LOG 2>&1 || cat $(BUILDDIR)/latex/LOG @echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex." .PHONY: latexpdfja diff --git a/document/core/appendix/changes.rst b/document/core/appendix/changes.rst index 61a7a54a7..0efcee2ae 100644 --- a/document/core/appendix/changes.rst +++ b/document/core/appendix/changes.rst @@ -338,7 +338,7 @@ Extended Constant Expressions Allowed basic numeric computations in constant expressions. [#proposal-extconst]_ -* Extended set of :ref:`constant instructions ` with: +* Extended set of :ref:`constant instructions ` with: - :math:`\K{i}\X{nn}\K{.add}` - :math:`\K{i}\X{nn}\K{.sub}` @@ -584,7 +584,7 @@ Added managed reference types. [#proposal-gc]_ - |ANYCONVERTEXTERN| - |EXTERNCONVERTANY| -* Extended set of :ref:`constant instructions ` with: +* Extended set of :ref:`constant instructions ` with: - |REFI31| - |STRUCTNEW| diff --git a/document/core/appendix/implementation.rst b/document/core/appendix/implementation.rst index 15fe69357..e40febbdc 100644 --- a/document/core/appendix/implementation.rst +++ b/document/core/appendix/implementation.rst @@ -56,6 +56,8 @@ An implementation may impose restrictions on the following dimensions of a modul * the nesting depth of :ref:`structured control instructions ` * the number of :ref:`label indices ` in a |BRTABLE| instruction * the number of instructions in a :ref:`constant ` :ref:`expression ` +* the number of instructions between a :ref:`branch instruction ` and its target +* the nesting depth of blocks between a :ref:`branch instruction ` and its target * the length of the array in a |ARRAYNEWFIXED| instruction * the length of an :ref:`element segment ` * the length of a :ref:`data segment ` @@ -63,7 +65,7 @@ An implementation may impose restrictions on the following dimensions of a modul * the range of :ref:`characters ` in a :ref:`name ` If the limits of an implementation are exceeded for a given module, -then the implementation may reject the :ref:`validation `, compilation, or :ref:`instantiation ` of that module with an embedder-specific error. +then the implementation may reject the :ref:`validation `, compilation, or :ref:`instantiation ` of that module with an implementation-specific error. .. note:: The last item allows :ref:`embedders ` that operate in limited environments without support for @@ -142,11 +144,14 @@ Restrictions on the following dimensions may be imposed during :ref:`execution < * the number of :ref:`frames ` on the :ref:`stack ` * the number of :ref:`labels ` on the :ref:`stack ` * the number of :ref:`values ` on the :ref:`stack ` +* the number of :ref:`handlers ` on the :ref:`stack ` +* the number of :ref:`labels ` dropped from the :ref:`stack ` by a :ref:`branch instruction ` +* the number of :ref:`values ` dropped from the :ref:`stack ` by a :ref:`branch instruction ` If the runtime limits of an implementation are exceeded during execution of a computation, -then it may terminate that computation and report an embedder-specific error to the invoking code. +then it may terminate that computation and report an implementation-specific error to the invoking code. -Some of the above limits may already be verified during instantiation, in which case an implementation may report exceedance in the same manner as for :ref:`syntactic limits `. +Some of the above limits may already be verified during :ref:`validation ` or :ref:`instantiation `, in which case an implementation may report exceedance in the same manner as for :ref:`syntactic limits `. .. note:: Concrete limits are usually not fixed but may be dependent on specifics, interdependent, vary over time, or depend on other implementation- or embedder-specific situations or events. diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py index e25af5964..0b0c126fb 100755 --- a/document/core/appendix/index-instructions.py +++ b/document/core/appendix/index-instructions.py @@ -117,10 +117,10 @@ def Instruction(version, name, opcode, type=None, validation=None, execution=Non Instruction(2.0, r'\TABLEGET~x', r'\hex{25}', r'[\X{at}] \to [t]', r'valid-table.get', r'exec-table.get'), Instruction(2.0, r'\TABLESET~x', r'\hex{26}', r'[\X{at}~t] \to []', r'valid-table.set', r'exec-table.set'), Instruction(0.0, None, r'\hex{27}'), - Instruction(1.0, r'\I32.\LOAD~x~\memarg', r'\hex{28}', r'[\X{at}] \to [\I32]', r'valid-load-val', r'exec-load-val'), - Instruction(1.0, r'\I64.\LOAD~x~\memarg', r'\hex{29}', r'[\X{at}] \to [\I64]', r'valid-load-val', r'exec-load-val'), - Instruction(1.0, r'\F32.\LOAD~x~\memarg', r'\hex{2A}', r'[\X{at}] \to [\F32]', r'valid-load-val', r'exec-load-val'), - Instruction(1.0, r'\F64.\LOAD~x~\memarg', r'\hex{2B}', r'[\X{at}] \to [\F64]', r'valid-load-val', r'exec-load-val'), + Instruction(1.0, r'\I32.\LOAD~x~\memarg', r'\hex{28}', r'[\X{at}] \to [\I32]', r'valid-load-num', r'exec-load-num'), + Instruction(1.0, r'\I64.\LOAD~x~\memarg', r'\hex{29}', r'[\X{at}] \to [\I64]', r'valid-load-num', r'exec-load-num'), + Instruction(1.0, r'\F32.\LOAD~x~\memarg', r'\hex{2A}', r'[\X{at}] \to [\F32]', r'valid-load-num', r'exec-load-num'), + Instruction(1.0, r'\F64.\LOAD~x~\memarg', r'\hex{2B}', r'[\X{at}] \to [\F64]', r'valid-load-num', r'exec-load-num'), Instruction(1.0, r'\I32.\LOAD\K{8\_s}~x~\memarg', r'\hex{2C}', r'[\X{at}] \to [\I32]', r'valid-load-pack', r'exec-load-pack'), Instruction(1.0, r'\I32.\LOAD\K{8\_u}~x~\memarg', r'\hex{2D}', r'[\X{at}] \to [\I32]', r'valid-load-pack', r'exec-load-pack'), Instruction(1.0, r'\I32.\LOAD\K{16\_s}~x~\memarg', r'\hex{2E}', r'[\X{at}] \to [\I32]', r'valid-load-pack', r'exec-load-pack'), @@ -131,10 +131,10 @@ def Instruction(version, name, opcode, type=None, validation=None, execution=Non Instruction(1.0, r'\I64.\LOAD\K{16\_u}~x~\memarg', r'\hex{33}', r'[\X{at}] \to [\I64]', r'valid-load-pack', r'exec-load-pack'), Instruction(1.0, r'\I64.\LOAD\K{32\_s}~x~\memarg', r'\hex{34}', r'[\X{at}] \to [\I64]', r'valid-load-pack', r'exec-load-pack'), Instruction(1.0, r'\I64.\LOAD\K{32\_u}~x~\memarg', r'\hex{35}', r'[\X{at}] \to [\I64]', r'valid-load-pack', r'exec-load-pack'), - Instruction(1.0, r'\I32.\STORE~x~\memarg', r'\hex{36}', r'[\X{at}~\I32] \to []', r'valid-store-val', r'exec-store-val'), - Instruction(1.0, r'\I64.\STORE~x~\memarg', r'\hex{37}', r'[\X{at}~\I64] \to []', r'valid-store-val', r'exec-store-val'), - Instruction(1.0, r'\F32.\STORE~x~\memarg', r'\hex{38}', r'[\X{at}~\F32] \to []', r'valid-store-val', r'exec-store-val'), - Instruction(1.0, r'\F64.\STORE~x~\memarg', r'\hex{39}', r'[\X{at}~\F64] \to []', r'valid-store-val', r'exec-store-val'), + Instruction(1.0, r'\I32.\STORE~x~\memarg', r'\hex{36}', r'[\X{at}~\I32] \to []', r'valid-store-num', r'exec-store-num'), + Instruction(1.0, r'\I64.\STORE~x~\memarg', r'\hex{37}', r'[\X{at}~\I64] \to []', r'valid-store-num', r'exec-store-num'), + Instruction(1.0, r'\F32.\STORE~x~\memarg', r'\hex{38}', r'[\X{at}~\F32] \to []', r'valid-store-num', r'exec-store-num'), + Instruction(1.0, r'\F64.\STORE~x~\memarg', r'\hex{39}', r'[\X{at}~\F64] \to []', r'valid-store-num', r'exec-store-num'), Instruction(1.0, r'\I32.\STORE\K{8}~x~\memarg', r'\hex{3A}', r'[\X{at}~\I32] \to []', r'valid-store-pack', r'exec-store-pack'), Instruction(1.0, r'\I32.\STORE\K{16}~x~\memarg', r'\hex{3B}', r'[\X{at}~\I32] \to []', r'valid-store-pack', r'exec-store-pack'), Instruction(1.0, r'\I64.\STORE\K{8}~x~\memarg', r'\hex{3C}', r'[\X{at}~\I64] \to []', r'valid-store-pack', r'exec-store-pack'), @@ -378,8 +378,8 @@ def Instruction(version, name, opcode, type=None, validation=None, execution=Non Instruction(2.0, r'\TABLEGROW~x', r'\hex{FC}~\hex{0F}', r'[t~\X{at}] \to [\X{at}]', r'valid-table.grow', r'exec-table.grow'), Instruction(2.0, r'\TABLESIZE~x', r'\hex{FC}~\hex{10}', r'[] \to [\X{at}]', r'valid-table.size', r'exec-table.size'), Instruction(2.0, r'\TABLEFILL~x', r'\hex{FC}~\hex{11}', r'[\X{at}~t~\X{at}] \to []', r'valid-table.fill', r'exec-table.fill'), - Instruction(0.0, None, r'\hex{FC}~\hex{1E} \dots'), - Instruction(2.0, r'\V128.\VLOAD~x~\memarg', r'\hex{FD}~~\hex{00}', r'[\X{at}] \to [\V128]', r'valid-vload-val', r'exec-vload-val'), + Instruction(0.0, None, r'\hex{FC}~\hex{12} \dots'), + Instruction(2.0, r'\V128.\VLOAD~x~\memarg', r'\hex{FD}~~\hex{00}', r'[\X{at}] \to [\V128]', r'valid-vload-num', r'exec-vload-num'), Instruction(2.0, r'\V128.\VLOAD\K{8x8\_s}~x~\memarg', r'\hex{FD}~~\hex{01}', r'[\X{at}] \to [\V128]', r'valid-vload-pack', r'exec-vload-pack'), Instruction(2.0, r'\V128.\VLOAD\K{8x8\_u}~x~\memarg', r'\hex{FD}~~\hex{02}', r'[\X{at}] \to [\V128]', r'valid-vload-pack', r'exec-vload-pack'), Instruction(2.0, r'\V128.\VLOAD\K{16x4\_s}~x~\memarg', r'\hex{FD}~~\hex{03}', r'[\X{at}] \to [\V128]', r'valid-vload-pack', r'exec-vload-pack'), diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst index c04d2be17..a09df66b9 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -27,13 +27,9 @@ Contexts ~~~~~~~~ In order to check :ref:`rolled up ` recursive types, -the :ref:`context ` is locally extended with an additional component that records the :ref:`sub type ` corresponding to each :ref:`recursive type index ` within the current :ref:`recursive type `: +the :ref:`context ` is locally extended with an additional component that records the :ref:`sub type ` corresponding to each :ref:`recursive type index ` within the current group of :ref:`recursive types `: -.. math:: - \begin{array}{llll} - \production{context} & C &::=& - \{~ \dots, \CRECS ~ \subtype^\ast ~\} \\ - \end{array} +$${syntax: context/sem} .. index:: value type, reference type, heap type, bottom type, sub type, recursive type, recursive type index @@ -44,164 +40,58 @@ Types Well-formedness for :ref:`extended type forms ` is defined as follows. +.. _valid-typeuse-ext: -.. _valid-heaptype-ext: +$${rule-prose: Typeuse_ok/rec} -:ref:`Heap Type ` :math:`\BOTH` -.................................................... +$${rule: Typeuse_ok/rec} -* The heap type is valid. -.. math:: - \frac{ - }{ - C \vdashheaptype \BOTH : \OKheaptype - } - -:ref:`Heap Type ` :math:`\REC~i` -..................................................... - -* The recursive type index :math:`i` must exist in :math:`C.\CRECS`. +.. _valid-heaptype-ext: -* Then the heap type is valid. +$${rule-prose: Heaptype_ok/bot} -.. math:: - \frac{ - C.\CRECS[i] = \subtype - }{ - C \vdashheaptype \REC~i : \OKheaptype - } +$${rule: Heaptype_ok/bot} .. _valid-valtype-ext: -:ref:`Value Type ` :math:`\BOT` -................................................... - -* The value type is valid. +$${rule-prose: Valtype_ok/bot} -.. math:: - \frac{ - }{ - C \vdashvaltype \BOT : \OKvaltype - } +$${rule: Valtype_ok/bot} .. _valid-rectype-ext: -:ref:`Recursive Types ` :math:`\TREC~\subtype^\ast` -................................................................... - -* Let :math:`C'` be the current :ref:`context ` :math:`C`, but where |CRECS| is :math:`\subtype^\ast`. - -* There must be a :ref:`type index ` :math:`x`, such that for each :ref:`sub type ` :math:`\subtype_i` in :math:`\subtype^\ast`: +$${rule-prose: Rectype_ok2} - * Under the context :math:`C'`, the :ref:`sub type ` :math:`\subtype_i` must be :ref:`valid ` for :ref:`type index ` :math:`x+i` and :ref:`recursive type index ` :math:`i`. - -* Then the recursive type is valid for the :ref:`type index ` :math:`x`. - -.. math:: - \frac{ - C,\CRECS~\subtype^\ast \vdashrectype \TREC~\subtype^\ast : {\OKrectype}(x,0) - }{ - C \vdashrectype \TREC~\subtype^\ast : {\OKrectype}(x) - } - -.. math:: - \frac{ - }{ - C \vdashrectype \TREC~\epsilon : {\OKrectype}(x,i) - } - \qquad - \frac{ - C \vdashsubtype \subtype : {\OKsubtype}(x,i) - \qquad - C \vdashrectype \TREC~{\subtype'}^\ast : {\OKrectype}(x+1,i+1) - }{ - C \vdashrectype \TREC~\subtype~{\subtype'}^\ast : {\OKrectype}(x,i) - } - -.. note:: - These rules are a generalisation of the ones :ref:`previously given `. +$${rule: {Rectype_ok2/empty Rectype_ok2/cons}} .. _valid-subtype-ext: -:ref:`Sub types ` :math:`\TSUB~\TFINAL^?~\X{ht}^\ast~\comptype` -............................................................................... - -* The :ref:`composite type ` :math:`\comptype` must be :ref:`valid `. +$${rule-prose: Subtype_ok2} -* The sequence :math:`\X{ht}^\ast` may be no longer than :math:`1`. +$${rule: Subtype_ok2} -* For every :ref:`heap type ` :math:`\X{ht}_k` in :math:`\X{ht}^\ast`: - - * The :ref:`heap type ` :math:`\X{ht}_k` must be ordered before a :ref:`type index ` :math:`x` and :ref:`recursive type index ` a :math:`i`, meaning: - - - Either :math:`\X{ht}_k` is a :ref:`defined type `. - - - Or :math:`\X{ht}_k` is a :ref:`type index ` :math:`y_k` that is smaller than :math:`x`. - - - Or :math:`\X{ht}_k` is a :ref:`recursive type index ` :math:`\REC~j_k` where :math:`j_k` is smaller than :math:`i`. - - * Let :ref:`sub type ` :math:`\subtype_k` be the :ref:`unrolling ` of the :ref:`heap type ` :math:`\X{ht}_k`, meaning: - - - Either :math:`\X{ht}_k` is a :ref:`defined type ` :math:`\deftype_k`, then :math:`\subtype_k` must be the :ref:`unrolling ` of :math:`\deftype_k`. - - - Or :math:`\X{ht}_k` is a :ref:`type index ` :math:`y_k`, then :math:`\subtype_k` must be the :ref:`unrolling ` of the :ref:`defined type ` :math:`C.\CTYPES[y_k]`. - - - Or :math:`\X{ht}_k` is a :ref:`recursive type index ` :math:`\REC~j_k`, then :math:`\subtype_k` must be :math:`C.\CRECS[j_k]`. - - * The :ref:`sub type ` :math:`\subtype_k` must not contain :math:`\TFINAL`. - - * Let :math:`\comptype'_k` be the :ref:`composite type ` in :math:`\subtype_k`. - - * The :ref:`composite type ` :math:`\comptype` must :ref:`match ` :math:`\comptype'_k`. - -* Then the sub type is valid for the :ref:`type index ` :math:`x` and :ref:`recursive type index ` :math:`i`. - -.. math:: - \frac{ - \begin{array}{@{}c@{}} - |\X{ht}^\ast| \leq 1 - \qquad - (\X{ht} \prec x,i)^\ast - \qquad - (\unrollht_{C}(\X{ht}) = \TSUB~{\X{ht}'}^\ast~\comptype')^\ast - \\ - C \vdashcomptype \comptype : \OKcomptype - \qquad - (C \vdashcomptypematch \comptype \subcomptypematch \comptype')^\ast - \end{array} - }{ - C \vdashsubtype \TSUB~\TFINAL^?~\X{ht}^\ast~\comptype : {\OKsubtype}(x,i) - } +where: .. _aux-unroll-heaptype: -where: - -.. math:: - \begin{array}{@{}lll@{}} - (\deftype \prec x,i) &=& {\F{true}} \\ - (y \prec x,i) &=& y < x \\ - (\REC~j \prec x,i) &=& j < i \\ - [2ex] - \unrollht_{C}(\deftype) &=& \unrolldt(\deftype) \\ - \unrollht_{C}(y) &=& \unrolldt(C.\CTYPES[y]) \\ - \unrollht_{C}(\REC~j) &=& C.\CRECS[j] \\ - \end{array} +$${definition: unrollht_ before} .. note:: - This rule is a generalisation of the ones :ref:`previously given `, which only allowed type indices as supertypes. + The new rules for :ref:`recursive types ` and :ref:`sub types ` complement the ones :ref:`previously given `, + which only allowed regular :ref:`type indices ` as supertypes. + They define validity of :ref:`rolled-up ` recursive types, + like they occur in :ref:`defined types `, + in turn needed to define :ref:`validity ` of :ref:`contexts `. + None of these rules are needed in the implementation of a validator. .. index:: defined type, recursive type, unroll, expand .. _valid-deftype: -:ref:`Defined types ` :math:`\rectype.i` -........................................................ - $${rule-prose: Deftype_ok} $${rule: Deftype_ok} @@ -213,21 +103,13 @@ $${rule: Deftype_ok} Subtyping ~~~~~~~~~ -In a :ref:`rolled-up ` :ref:`recursive type `, a :ref:`recursive type indices ` :math:`\REC~i` :ref:`matches ` another :ref:`heap type ` :math:`\X{ht}` if: +Inside a :ref:`rolled-up ` :ref:`recursive type `, a :ref:`recursive type index ` can :ref:`match ` another :ref:`heap type `. -* Let :math:`\TSUB~\TFINAL^?~{\X{ht}'}^\ast~\comptype` be the :ref:`sub type ` :math:`C.\CRECS[i]`. - -* The heap type :math:`\X{ht}` is contained in :math:`{\X{ht}'}^\ast`. - -.. math:: - \frac{ - C.\CRECS[i] = \TSUB~\TFINAL^?~(\X{ht}_1^\ast~\X{ht}~\X{ht}_2^\ast)~\comptype - }{ - C \vdashheaptypematch \REC~i \subheaptypematch \X{ht} - } +$${rule: Heaptype_sub/rec-*} .. note:: - This rule is only invoked when checking :ref:`validity ` of :ref:`rolled-up ` :ref:`recursive types `. + These rules complement the previously given rules for :ref:`matching heap types `. + They are only invoked when checking :ref:`validity ` of :ref:`rolled-up ` :ref:`recursive types `. .. index:: value, value type, result, result type, trap, exception, throw @@ -287,6 +169,14 @@ Results } +.. _valid-localtype: +.. _valid-context: + +.. todo + Context Validity + ~~~~~~~~~~~~~~~~ + + .. _module-context: .. _valid-store: @@ -845,7 +735,7 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow * Let :math:`m` be the length of :math:`\moduleinst.\MIFUNCS`. -* Let :math:`x^\ast` be the sequence of :ref:`function indices ` from :math:`0` to :math:`m-1`. +* Let :math:`x^\ast` be the sequence of :ref:`function indices ` from :math:`0` to :math:`k-1` for some :math:`k` that is smaller than or equal to the number of functions in the instance. * Then the module instance is valid with :ref:`context ` :math:`\{\CTYPES~\deftype^\ast,` :math:`\CTAGS~\tagtype^\ast,` :math:`\CGLOBALS~\globaltype^\ast,` :math:`\CMEMS~\memtype^\ast,` :math:`\CTABLES~\tabletype^\ast,` :math:`\CFUNCS~\deftype_{\K{F}}^\ast,` :math:`\CDATAS~\X{ok}^\ast,` :math:`\CELEMS~\reftype^\ast,` :math:`\CREFS~x^\ast\}`. @@ -873,6 +763,8 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow (S \vdashexportinst \exportinst : \OKexportinst)^\ast \qquad (\exportinst.\XINAME)^\ast ~\mbox{disjoint} + \\ + k \le |\funcaddr^\ast| \end{array} }{ S \vdashmoduleinst \{ @@ -895,11 +787,20 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow \CFUNCS & \deftype_{\K{F}}^\ast, \\ \CDATAS & \X{ok}^\ast, \\ \CELEMS & \reftype^\ast, \\ - \CREFS & 0 \dots (|\funcaddr^\ast|-1) ~\} + \CREFS & 0 \dots k-1 ~\} \end{array} \end{array} } +.. note:: + The field ${:C.REFS} from the resulting context is meant to be constructed to contain all :ref:`function indices ` from the module. + However, modules and their instances can contain more than ${:2^32} functions + (at most ${:2^32} definitions plus ${:2^32} imports), + while the highest representable function index is ${:$(2^32-1)}. + The variable ${:k} in the rule hence allows picking an upper limit for ${:C.REFS} that is smaller than the total number of functions, + in case that is necessary for ${:C.REFS} to be syntactically well-formed. + In practice, ${:k = $min(|funcaddr*|, 2^32)} always is the maximally permissive choice. + .. scratch .. index:: context, store, frame @@ -1123,7 +1024,7 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera .. math:: \frac{ - C \vdashresulttype [t^n] : \OKresulttype + \{\} \vdashresulttype [t^n] : \OKresulttype \qquad S; [t^n] \vdashinstrs F; \instr^\ast : [t^n] }{ @@ -1147,10 +1048,10 @@ To that end, all previous typing judgements :math:`C \vdash \X{prop}` are genera \begin{array}{c} (C \vdashcatch \catch : \OKcatch)^\ast \qquad - S; C \vdashinstrs \instr^\ast : [t_1^\ast] \to [t_2^\ast] \\ + S; C \vdashinstrs \instr^\ast : [] \to [t^\ast] \\ \end{array} }{ - S; C \vdashadmininstr \HANDLER_n\{\catch^\ast\}~\instr^\ast : [t_1^\ast] \to [t_2^\ast] + S; C \vdashadmininstr \HANDLER_n\{\catch^\ast\}~\instr^\ast : [] \to [t^\ast] } diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst index 5f99c745a..56f564b8e 100644 --- a/document/core/binary/modules.rst +++ b/document/core/binary/modules.rst @@ -42,7 +42,7 @@ All basic :ref:`indices ` are encoded with their respective value. $${grammar: { Btypeidx Bfuncidx Btableidx Bmemidx Bglobalidx Btagidx Belemidx Bdataidx - Blocalidx Blabelidx + Blocalidx Bfieldidx Blabelidx }} :ref:`External indices ` are encoded by a distiguishing byte followed by an encoding of their respective value. diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index 4ea3ce6a7..49043ed94 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -100,6 +100,7 @@ $${grammar: Bresulttype} pair: binary format; field type pair: binary format; storage type pair: binary format; packed type +.. _binary-mut: .. _binary-comptype: .. _binary-aggrtype: .. _binary-functype: @@ -163,7 +164,6 @@ $${grammar: Btagtype} .. index:: global type, mutability, value type pair: binary format; global type pair: binary format; mutability -.. _binary-mut: .. _binary-globaltype: Global Types diff --git a/document/core/conf.py b/document/core/conf.py index 25604d400..5e0d25f35 100644 --- a/document/core/conf.py +++ b/document/core/conf.py @@ -310,6 +310,7 @@ \setlist[enumerate,4]{label=\Alph*.} \setlist[enumerate,5]{label=\Roman*.} \renewcommand\sphinxcrossref[1]{#1} + \hypersetup{bookmarksnumbered=true,bookmarksdepth=2} ''', # Latex figure (float) alignment diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index ecf34f60b..04c53f82d 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -160,7 +160,7 @@ $${rule: {Step_read/call}} 6. :ref:`Invoke ` the function instance at address :math:`a`. -$${rule: {Step_read/call_ref-null}} +$${rule: {Step/call_ref-null}} .. note:: The formal rule for calling a non-null function reference is described :ref:`below `. @@ -330,27 +330,29 @@ and returning from it. Invocation of :ref:`function reference ` :math:`(\REFFUNCADDR~a)` .................................................................................. -1. Assert: due to :ref:`validation `, :math:`S.\SFUNCS[a]` exists. +1. Let :math:`z` be the current state. -2. Let :math:`f` be the :ref:`function instance `, :math:`S.\SFUNCS[a]`. +2. Assert: due to :ref:`validation `, :math:`z.\SFUNCS[a]` exists. -3. Let :math:`\TFUNC~[t_1^n] \Tarrow [t_2^m]` be the :ref:`composite type ` :math:`\expanddt(\X{f}.\FITYPE)`. +3. Let :math:`\X{fi}` be the :ref:`function instance `, :math:`z.\SFUNCS[a]`. -4. Let :math:`\FUNC~x~\local^\ast~\instr^\ast` be the :ref:`function ` :math:`f.\FICODE`. +4. Let :math:`\TFUNC~[t_1^n] \Tarrow [t_2^m]` be the :ref:`composite type ` :math:`\expanddt(\X{fi}.\FITYPE)`. -5. Assert: due to :ref:`validation `, :math:`n` values are on the top of the stack. +5. Let :math:`\FUNC~x~(\local~t)^\ast~\instr^\ast` be the :ref:`function ` :math:`\X{fi}.\FICODE`. -6. Pop the values :math:`\val^n` from the stack. +6. Assert: due to :ref:`validation `, :math:`n` values are on the top of the stack. -7. Let :math:`F` be the :ref:`frame ` :math:`\{ \AMODULE~F.\FIMODULE, \ALOCALS~\val^n~(\default_t)^\ast \}`. +7. Pop the values :math:`\val^n` from the stack. -8. Push the activation of :math:`f` with arity :math:`m` to the stack. +8. Let :math:`f` be the :ref:`frame ` :math:`\{ \ALOCALS~\val^n~(\default_t)^\ast, \AMODULE~\X{fi}.\FIMODULE \}`. -9. Let :math:`L` be the :ref:`label ` whose arity is :math:`m` and whose continuation is the end of the function. +9. Push the activation of :math:`f` with arity :math:`m` to the stack. -10. :ref:`Enter ` the instruction sequence :math:`\instr^\ast` with label :math:`L` and no values. +10. Let :math:`L` be the :ref:`label ` whose arity is :math:`m` and whose continuation is the end of the function. -$${rule: {Step_read/call_ref-func}} +11. :ref:`Enter ` the instruction sequence :math:`\instr^\ast` with label :math:`L` and no values. + +$${rule: {Step/call_ref-func}} .. note:: For non-defaultable types, the respective local is left uninitialized by these rules. @@ -397,39 +399,18 @@ A host function may also modify the :ref:`store `. However, all store modifications must result in an :ref:`extension ` of the original store, i.e., they must only modify mutable contents and must not have instances removed. Furthermore, the resulting store must be :ref:`valid `, i.e., all data and code in it is well-typed. -.. math:: - ~\\[-1ex] - \begin{array}{l} - \begin{array}{lcl@{\qquad}l} - S; \val^n~(\REFFUNCADDR~a)~\CALLREF &\stepto& S'; \result - \end{array} - \\ \qquad - \begin{array}[t]{@{}r@{~}l@{}} - \iff & S.\SFUNCS[a] = \{ \FITYPE~\deftype, \FIHOSTFUNC~\X{hf} \} \\ - \wedge & \deftype \approx \TFUNC~[t_1^n] \Tarrow [t_2^m] \\ - \wedge & (S'; \result) \in \X{hf}(S; \val^n) \\ - \end{array} \\ - \begin{array}{lcl@{\qquad}l} - S; \val^n~(\REFFUNCADDR~a)~\CALLREF &\stepto& S; \val^n~(\REFFUNCADDR~a)~\CALLREF - \end{array} - \\ \qquad - \begin{array}[t]{@{}r@{~}l@{}} - \iff & S.\SFUNCS[a] = \{ \FITYPE~\deftype, \FIHOSTFUNC~\X{hf} \} \\ - \wedge & \deftype \approx \TFUNC~[t_1^n] \Tarrow [t_2^m] \\ - \wedge & \bot \in \X{hf}(S; \val^n) \\ - \end{array} \\ - \end{array} +$${rule: {Step/call_ref-hostfunc-*}} -Here, :math:`\X{hf}(S; \val^n)` denotes the implementation-defined execution of host function :math:`\X{hf}` in current store :math:`S` with arguments :math:`\val^n`. -It yields a set of possible outcomes, where each element is either a pair of a modified store :math:`S'` and a :ref:`result ` -or the special value :math:`\bot` indicating divergence. +Here, ${:$hostcall(_HOSTFUNC hf, s, val^n)} denotes the implementation-defined execution of host function ${:hf} in current store ${:s} with arguments ${:val^n}. +It yields a set of possible outcomes, where each element is either a pair of a modified store ${:s'} and a :ref:`result ` +or the special value ${hostcallresult:BOT} indicating divergence. A host function is non-deterministic if there is at least one argument for which the set of outcomes is not singular. For a WebAssembly implementation to be :ref:`sound ` in the presence of host functions, every :ref:`host function instance ` must be :ref:`valid `, which means that it adheres to suitable pre- and post-conditions: -under a :ref:`valid store ` :math:`S`, and given arguments :math:`\val^n` matching the ascribed parameter types :math:`t_1^n`, -executing the host function must yield a non-empty set of possible outcomes each of which is either divergence or consists of a valid store :math:`S'` that is an :ref:`extension ` of :math:`S` and a result matching the ascribed return types :math:`t_2^m`. +under a :ref:`valid store ` ${:s}, and given arguments ${:val^n} matching the ascribed parameter types ${:t_1^n}, +executing the host function must yield a non-empty set of possible outcomes each of which is either divergence or consists of a valid store ${:s'} that is an :ref:`extension ` of ${:s} and a result matching the ascribed return types ${:t_2^m}. All these notions are made precise in the :ref:`Appendix `. .. note:: @@ -570,13 +551,25 @@ Memory Instructions However, it may be substantially slower on some hardware. -.. _exec-load-val: +.. _exec-load-num: + +$${rule-prose: Step_read/load-num-*} + +$${rule: {Step_read/load-num-*}} + + .. _exec-load-pack: -.. _exec-vload-val: -$${rule-prose: Step_read/load} +$${rule-prose: Step_read/load-pack-*} + +$${rule: {Step_read/load-pack-*}} + + +.. _exec-vload-num: + +$${rule-prose: Step_read/vload-num-*} -$${rule: {Step_read/load-*}} +$${rule: {Step_read/vload-num-*}} .. _exec-vload-pack: @@ -607,13 +600,19 @@ $${rule-prose: Step_read/vload_lane} $${rule: {Step_read/vload_lane-*}} -.. _exec-store-val: +.. _exec-store-num: .. _exec-store-pack: -.. _exec-vstore: $${rule-prose: Step/store} -$${rule: {Step/store-* Step/vstore-*}} +$${rule: {Step/store-*}} + + +.. _exec-vstore: + +$${rule-prose: Step/vstore} + +$${rule: {Step/vstore-*}} .. _exec-vstore_lane: @@ -684,22 +683,9 @@ Reference Instructions .. _exec-ref.null: -:math:`\REFNULL~x` -....................... +$${rule-prose: Step_read/ref.null} -1. Let :math:`F` be the :ref:`current ` :ref:`frame `. - -2. Assert: due to :ref:`validation `, the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]` exists. - -3. Let :math:`\deftype` be the :ref:`defined type ` :math:`F.\AMODULE.\MITYPES[x]`. - -4. Push the value :math:`\REFNULL~\deftype` to the stack. - -$${rule: {Step_read/ref.null-*}} - -.. note:: - No formal reduction rule is required for the case |REFNULL| |ABSHEAPTYPE|, - since the instruction form is already a :ref:`value `. +$${rule: {Step_read/ref.null}} .. _exec-ref.func: diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index 30cbc0a6e..430385446 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -182,6 +182,14 @@ $${definition: instantiate} where: +.. _eval-exprs: + +$${definition-prose: evalexprs} + +$${definition: evalexprs} + +and: + .. _eval-globals: $${definition-prose: evalglobals} diff --git a/document/core/exec/numerics.rst b/document/core/exec/numerics.rst index ce0e42fc8..d0180ab19 100644 --- a/document/core/exec/numerics.rst +++ b/document/core/exec/numerics.rst @@ -2162,7 +2162,7 @@ where: 3. Let :math:`(j_1~j_2)^m` be :math:`j^{2m}`, decomposed into pairwise elements. -4. For each :math:`i_{1k}` in :math:`i_1^m` and corresponding :math:`i_{2k}` in :math:`i_2^m`, let :math:`r_k` be :math:`\iaddsat_N(i_{1k}, i_{2k})`. +4. For each :math:`i_{1k}` in :math:`i_1^m` and corresponding :math:`i_{2k}` in :math:`i_2^m`, let :math:`r_k` be :math:`\iaddsats_N(i_{1k}, i_{2k})`. 5. Let :math:`r^m` be the concatenation of all :math:`r_k`. @@ -2170,7 +2170,7 @@ where: .. math:: \begin{array}{@{}lcll} - \ivdotsat_N(i_1^{2m}, i_2^{2m}) &=& (\iaddsat_N(j_1, j_2))^m + \ivdotsat_N(i_1^{2m}, i_2^{2m}) &=& (\iaddsats_N(j_1, j_2))^m & (\iff (\imul_N(i_1, i_2))^{2m} = (j_1~j_2)^m) \end{array} @@ -2206,9 +2206,9 @@ The previous operators are lifted to operators on arguments of vector type by wr \begin{array}[t]{@{}l} \iff i_1^\ast = \lanes_{\K{i}N_1\K{x}M_1}(c_1)[h \slice k] \\ \land~i_2^\ast = \lanes_{\K{i}N_1\K{x}M_1}(c_2)[h \slice k] \\ - \land~{i'_1}^\ast = \extend^{\sx}_{N_1, N_2}(i_1)^\ast \\ - \land~{i'_2}^\ast = \extend^{\sx}_{N_1, N_2}(i_2)^\ast \\ - \land~j^\ast = f_{N_2}({i'_1}^\ast, {i'_1}^\ast) \\ + \land~{i'_1}^\ast = \extend^{\sx_1}_{N_1, N_2}(i_1)^\ast \\ + \land~{i'_2}^\ast = \extend^{\sx_2}_{N_1, N_2}(i_2)^\ast \\ + \land~j^\ast = f_{N_2}({i'_1}^\ast, {i'_2}^\ast) \\ \end{array} \end{array} diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index cfa74500c..1143b82cb 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -12,7 +12,6 @@ Runtime Structure .. _syntax-num: .. _syntax-vec: .. _syntax-ref: -.. _syntax-addrref: .. _syntax-ref.i31num: .. _syntax-ref.struct: .. _syntax-ref.array: @@ -34,6 +33,7 @@ It is convenient to reuse the same notation as for the ${:CONST} :ref:`instructi References other than null are represented with additional :ref:`administrative instructions `. They either are *scalar references*, containing a 31-bit :ref:`integer `, +*null references*, *structure references*, pointing to a specific :ref:`structure address `, *array references*, pointing to a specific :ref:`array address `, *function references*, pointing to a specific :ref:`function address `, @@ -41,7 +41,7 @@ They either are *scalar references*, containing a 31-bit :ref:`integer ` defined by the :ref:`embedder `. Any of the aformentioned references can furthermore be wrapped up as an *external reference*. -$${syntax: val num vec ref addrref} +$${syntax: val num vec ref} .. note:: Future versions of WebAssembly may add additional forms of values. @@ -146,8 +146,8 @@ Convention .. _syntax-elemaddr: .. _syntax-dataaddr: .. _syntax-structaddr: -.. _syntax-exnaddr: .. _syntax-arrayaddr: +.. _syntax-exnaddr: .. _syntax-hostaddr: .. _syntax-addr: @@ -169,7 +169,7 @@ in the :ref:`store ` are referenced with abstract *addresses*. These are simply indices into the respective store component. In addition, an :ref:`embedder ` may supply an uninterpreted set of *host addresses*. -$${syntax: {addr funcaddr tableaddr memaddr globaladdr tagaddr elemaddr dataaddr structaddr arrayaddr hostaddr}} +$${syntax: {addr funcaddr tableaddr memaddr globaladdr tagaddr elemaddr dataaddr structaddr arrayaddr exnaddr hostaddr}} An :ref:`embedder ` may assign identity to :ref:`exported ` store objects corresponding to their addresses, even where this identity is not observable from within WebAssembly code itself @@ -590,7 +590,7 @@ In order to express the reduction of :ref:`traps `, :ref:`calls ` represents an allocated :ref:`reference ` value of respective form :ref:`"on the stack" `. +A :ref:`reference ` represents a :ref:`reference ` value of respective form :ref:`"on the stack" `. The ${:LABEL}, ${:FRAME}, and ${:HANDLER} instructions model :ref:`labels `, :ref:`frames `, and active :ref:`exception handlers `, respectively, :ref:`"on the stack" `. Moreover, the administrative syntax maintains the nesting structure of the original :ref:`structured control instruction ` or :ref:`function body ` and their :ref:`instruction sequences `. diff --git a/document/core/exec/values.rst b/document/core/exec/values.rst index ef2d01920..a6ee02be6 100644 --- a/document/core/exec/values.rst +++ b/document/core/exec/values.rst @@ -46,11 +46,6 @@ $${rule-prose: Ref_ok/null} $${rule: Ref_ok/null} -.. note:: - A null reference can be typed with any smaller type. - In particular, that allows it to be typed with the least type in its respective hierarchy. - That ensures that the value is compatible with any nullable type in that hierarchy. - .. _valid-ref.i31num: diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 74bbcc634..19840c61c 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -407,7 +407,8 @@ Instructions prefixed with ${:V128} do not involve a specific interpretation, an $${syntax: vvunop vvbinop vvternop vvtestop - vunop_ vbinop_ vternop_ vtestop_ vrelop_ vswizzlop_ vshiftop_ vextunop__ vextbinop__ vextternop__ vcvtop__ + vunop_ vbinop_ vternop_ vtestop_ vrelop_ vswizzlop_ vshiftop_ + vextunop__ vextbinop__ vextternop__ vcvtop__ } Vector instructions can be grouped into several subcategories: diff --git a/document/core/text/conventions.rst b/document/core/text/conventions.rst index 5aa3055bc..0b2222c99 100644 --- a/document/core/text/conventions.rst +++ b/document/core/text/conventions.rst @@ -42,8 +42,8 @@ In order to distinguish symbols of the textual syntax from symbols of the abstra * ${grammar-case: $(T)*} is a possibly empty sequence of iterations of ${:T}. (This is a shorthand for ${grammar-case: $(T)^n} used where ${:n} is not relevant.) -* ${grammar-case: $(T)+} is a possibly empty sequence of iterations of ${:T}. - (This is a shorthand for ${grammar-case: $(T)^n} used where ${:n} is not relevant.) +* ${grammar-case: $(T)+} is a non-empty sequence of iterations of ${:T}. + (This is a shorthand for ${grammar-case: $(T)^n} where ${:n >= 1}.) * ${grammar-case: $(T)?} is an optional occurrence of ${:T}. (This is a shorthand for ${grammar-case: $(T)^n} where ${:n<=1}.) diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index c4aab3a6c..36338aa3b 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -179,7 +179,9 @@ The offset and alignment immediates to memory instructions are optional. The offset defaults to ${:0}, the alignment to the storage size of the respective memory access, which is its *natural alignment*. Lexically, an ${grammar-case: Toffset} or ${grammar-case: Talign_} phrase is considered a single :ref:`keyword token `, so no :ref:`white space ` is allowed around the ${grammar-case: "="}. -$${grammar: {Tmemarg_ Toffset Talign_ Tlaneidx Tplaininstr_/memory-plain Tplaininstr_/data}} +$${grammar: {Tmemarg_ Toffset Talign_ Tlaneidx}} + +$${grammar: {Tplaininstr_/memory-plain Tplaininstr_/data}} Abbreviations @@ -403,6 +405,7 @@ $${grammar: { Tplaininstr_/vec-extbin-i16x8 Tplaininstr_/vec-extun-i32x4 Tplaininstr_/vec-extbin-i32x4 + Tplaininstr_/vec-exttern-i32x4 Tplaininstr_/vec-extbin-i64x2 }} diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index 167b4f451..2112cf416 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -257,6 +257,7 @@ $${grammar: Timport_/abbrev-func Texportfunc_} .. _text-datastring: .. _text-data: .. _text-memuse: +.. _text-offsetexpr: Data Segments ~~~~~~~~~~~~~ @@ -264,11 +265,7 @@ Data Segments Data segments allow for an optional :ref:`memory index ` to identify the memory to initialize. The data is written as a :ref:`string `, which may be split up into a possibly empty sequence of individual string literals. -$${grammar: Tdata_ Tdatastring {Tmemuse_/plain Toffset_/plain}} - -.. note:: - In the current version of WebAssembly, the only valid memory index is 0 - or a symbolic :ref:`memory identifier ` resolving to the same value. +$${grammar: Tdata_ Tdatastring {Tmemuse_/plain Toffsetexpr_/plain}} Abbreviations @@ -276,7 +273,7 @@ Abbreviations As an abbreviation, a single :ref:`folded instruction ` may occur in place of the offset of an active segment: -$${grammar: Toffset_/abbrev} +$${grammar: Toffsetexpr_/abbrev} Also, a memory use can be omitted, defaulting to ${:0}. @@ -434,6 +431,6 @@ $${definition-ignore: typesd importsd tagsd globalsd memsd tablesd funcsd datasd Abbreviations ............. -In a source file, the toplevel ${grammar-case: "(" "module" Tdecldots ")"} surrounding the module body may be omitted. +In a source file, the toplevel ${grammar-case: "(" "module" Tdecldots_(I) ")"} surrounding the module body may be omitted. $${grammar: Tmodule/abbrev} diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 35f85ec4b..44584df28 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -426,7 +426,7 @@ .. |module| mathdef:: \xref{syntax/modules}{syntax-module}{\X{module}} .. |decl| mathdef:: \xref{text/modules}{syntax-decl}{\X{decl}} -.. |type| mathdef:: \xref{syntax/types}{syntax-rectype}{\X{type}} +.. |type| mathdef:: \xref{syntax/modules}{syntax-type}{\X{type}} .. |func| mathdef:: \xref{syntax/modules}{syntax-func}{\X{func}} .. |local| mathdef:: \xref{syntax/modules}{syntax-local}{\X{local}} .. |table| mathdef:: \xref{syntax/modules}{syntax-table}{\X{table}} @@ -1088,6 +1088,7 @@ .. |Tlocals| mathdef:: \xref{text/modules}{text-local}{\T{locals}} .. |Tdata| mathdef:: \xref{text/modules}{text-data}{\T{data}} .. |Tdatastring| mathdef:: \xref{text/modules}{text-datastring}{\T{datastring}} +.. |Toffsetexpr| mathdef:: \xref{text/modules}{text-offsetexpr}{\T{offsetexpr}} .. |Tmemuse| mathdef:: \xref{text/modules}{text-memuse}{\T{memuse}} .. |Tstart| mathdef:: \xref{text/modules}{text-start}{\T{start}} @@ -1191,6 +1192,7 @@ .. |vdashtabletype| mathdef:: \xref{valid/types}{valid-tabletype}{\vdash} .. |vdashmemtype| mathdef:: \xref{valid/types}{valid-memtype}{\vdash} .. |vdashglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\vdash} +.. |vdashlocaltype| mathdef:: \xref{appendix/properties}{valid-localtype}{\vdash} .. |vdashtagtype| mathdef:: \xref{valid/types}{valid-tagtype}{\vdash} .. |vdashexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\vdash} .. |vdashdeftype| mathdef:: \xref{appendix/properties}{valid-deftype}{\vdash} @@ -1218,6 +1220,7 @@ .. |OKtabletype| mathdef:: \xref{valid/types}{valid-tabletype}{\K{ok}} .. |OKmemtype| mathdef:: \xref{valid/types}{valid-memtype}{\K{ok}} .. |OKglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\K{ok}} +.. |OKlocaltype| mathdef:: \xref{appendix/properties}{valid-localtype}{\K{ok}} .. |OKtagtype| mathdef:: \xref{valid/types}{valid-tagtype}{\K{ok}} .. |OKexterntype| mathdef:: \xref{valid/types}{valid-externtype}{\K{ok}} .. |OKlimits| mathdef:: \xref{valid/types}{valid-limits}{\K{ok}} @@ -1270,15 +1273,15 @@ .. |vdashinstrs| mathdef:: \xref{valid/instructions}{valid-instrs}{\vdash} .. |vdashcatch| mathdef:: \xref{valid/instructions}{valid-catch}{\vdash} .. |vdashexpr| mathdef:: \xref{valid/instructions}{valid-expr}{\vdash} -.. |vdashinstrconst| mathdef:: \xref{valid/instructions}{valid-const}{\vdash} -.. |vdashexprconst| mathdef:: \xref{valid/instructions}{valid-const}{\vdash} -.. |vdashexprokconst| mathdef:: \xref{valid/instructions}{valid-const}{\vdash} +.. |vdashinstrconst| mathdef:: \xref{valid/instructions}{valid-constant}{\vdash} +.. |vdashexprconst| mathdef:: \xref{valid/instructions}{valid-constant}{\vdash} +.. |vdashexprokconst| mathdef:: \xref{valid/instructions}{valid-constant}{\vdash} .. |OKcatch| mathdef:: \xref{valid/instructions}{valid-catch}{\K{ok}} -.. |CONSTinstrconst| mathdef:: \xref{valid/instructions}{valid-const}{\K{const}} -.. |CONSTexprconst| mathdef:: \xref{valid/instructions}{valid-const}{\K{const}} -.. |CONSTexprokconst| mathdef:: \xref{valid/instructions}{valid-const}{\K{const}} +.. |CONSTinstrconst| mathdef:: \xref{valid/instructions}{valid-constant}{\K{const}} +.. |CONSTexprconst| mathdef:: \xref{valid/instructions}{valid-constant}{\K{const}} +.. |CONSTexprokconst| mathdef:: \xref{valid/instructions}{valid-constant}{\K{const}} .. |vdashexternidx| mathdef:: \xref{valid/modules}{valid-externidx}{\vdash} @@ -1313,6 +1316,8 @@ .. |zeroop| mathdef:: \xref{syntax/instructions}{aux-zeroop}{\F{zeroop}} .. |halfop| mathdef:: \xref{syntax/instructions}{aux-halfop}{\F{halfop}} +.. |OKcontext| mathdef:: \xref{appendix/properties}{valid-context}{\K{ok}} + .. Execution .. --------- @@ -1542,6 +1547,7 @@ .. Administrative Instructions, terminals .. |REFI31NUM| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}i\scriptstyle31}} +.. |REFNULLADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}null}} .. |REFFUNCADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}func}} .. |REFSTRUCTADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}struct}} .. |REFARRAYADDR| mathdef:: \xref{exec/runtime}{syntax-ref}{\K{ref{.}array}} @@ -1556,7 +1562,6 @@ .. |num| mathdef:: \xref{exec/runtime}{syntax-num}{\X{num}} .. |vec| mathdef:: \xref{exec/runtime}{syntax-vec}{\X{vec}} .. |reff| mathdef:: \xref{exec/runtime}{syntax-ref}{\X{ref}} -.. |addrref| mathdef:: \xref{exec/runtime}{syntax-addrref}{\X{addrref}} .. |val| mathdef:: \xref{exec/runtime}{syntax-val}{\X{val}} .. |result| mathdef:: \xref{exec/runtime}{syntax-result}{\X{result}} diff --git a/document/core/util/mathjax2katex.py b/document/core/util/mathjax2katex.py index b840fced1..68e6d12bb 100755 --- a/document/core/util/mathjax2katex.py +++ b/document/core/util/mathjax2katex.py @@ -61,7 +61,7 @@ def HasBalancedTags(s): def ReplaceMath(cache, data): old = data - data = re.sub('[\\\\][\\\\]\\[([0-9]|-)', '\\\\DOUBLESLASH[\\1', data) # Messed up by Bikeshed + data = re.sub('[\\\\]\\[([0-9]|-)', '\\\\DOUBLESLASH[\\1', data) # Messed up by Bikeshed ("\\[" becomes "\[") data = data.replace('\\\\', '\\DOUBLESLASH') #data = data.replace('\\(', '') #data = data.replace('\\)', '') diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 7164062ed..418da737e 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -167,7 +167,6 @@ In addition, the following auxiliary relation denotes the *expansion* of a :ref: $${rule: Expand {Expand_use/*}} $${relation-ignore: Expand Expand_use} -$${definition-ignore: expanddt} .. index:: ! instruction type, value type, result type, instruction, local, local index @@ -219,7 +218,6 @@ Validity of an individual definition is specified relative to a *context*, which collects relevant information about the surrounding :ref:`module ` and the definitions in scope: * *Types*: the list of :ref:`types ` defined in the current module. -* *Recursive Types*: the list of :ref:`sub types ` in the current group of recursive types. * *Functions*: the list of :ref:`functions ` declared in the current module, represented by a :ref:`defined type ` that :ref:`expands ` to their :ref:`function type `. * *Tables*: the list of :ref:`tables ` declared in the current module, represented by their :ref:`table type `. * *Memories*: the list of :ref:`memories ` declared in the current module, represented by their :ref:`memory type `. @@ -239,7 +237,10 @@ The label stack is the only part of the context that changes as validation of an More concretely, contexts are defined as :ref:`records ` ${:C} with abstract syntax: -$${syntax: context} +$${syntax: context/syn} + +.. note:: + The definition of contexts needs to be :ref:`extended ` with additional fields for the purpose of proving :ref:`type soundness `. .. index:: ! type closure diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 6013d4de2..7c70bb580 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -33,7 +33,7 @@ Two degrees of polymorphism can be distinguished: the entire (or most of the) :ref:`instruction type ` ${instrtype: t_1* -> t_2*} of the instruction is unconstrained. That is the case for all :ref:`control instructions ` that perform an *unconditional control transfer*, such as ${:UNREACHABLE}, ${:BR}, or ${:RETURN}. -In both cases, the unconstrained types or type sequences can be chosen arbitrarily, as long as they meet the constraints imposed for the surrounding parts of the program. +In both cases, the unconstrained types or type sequences can be chosen arbitrarily, as long as they are valid in the current :ref:`context ` and meet the constraints imposed for the surrounding parts of the program. .. note:: For example, the ${:SELECT} instruction is valid with type ${instrtype: t t I32 -> t}, for any possible :ref:`number type ` ${:t}. @@ -43,7 +43,7 @@ In both cases, the unconstrained types or type sequences can be chosen arbitrari and - $${instr*: (CONST F64 $fnat(64, 1)) (CONST F64 $fnat(64, 2)) (CONST F64 $fnat(64, 3)) (SELECT)} + $${instr*: (CONST F64 $fnat(64, 1)) (CONST F64 $fnat(64, 2)) (CONST I32 3) (SELECT)} are valid, with ${:t} in the typing of ${:SELECT} being instantiated to ${:I32} or ${:F64}, respectively. @@ -575,14 +575,14 @@ $${rule-prose: Memarg_ok} $${rule: Memarg_ok} -.. _valid-load-val: +.. _valid-load-num: :math:`t\K{.}\LOAD~x~\memarg` ............................. -$${rule-prose: Instr_ok/load-val} +$${rule-prose: Instr_ok/load-num} -$${rule: Instr_ok/load-val} +$${rule: Instr_ok/load-num} .. _valid-load-pack: @@ -595,14 +595,14 @@ $${rule-prose: Instr_ok/load-pack} $${rule: Instr_ok/load-pack} -.. _valid-store-val: +.. _valid-store-num: :math:`t\K{.}\STORE~x~\memarg` .............................. -$${rule-prose: Instr_ok/store-val} +$${rule-prose: Instr_ok/store-num} -$${rule: Instr_ok/store-val} +$${rule: Instr_ok/store-num} .. _valid-store-pack: @@ -615,14 +615,14 @@ $${rule-prose: Instr_ok/store-pack} $${rule: Instr_ok/store-pack} -.. _valid-vload-val: +.. _valid-vload-num: :math:`\K{v128.}\LOAD~x~\memarg` -..................................... +................................ -$${rule-prose: Instr_ok/vload-val} +$${rule-prose: Instr_ok/vload-num} -$${rule: Instr_ok/vload-val} +$${rule: Instr_ok/vload-num} .. _valid-vload-pack: @@ -1359,31 +1359,33 @@ Instruction Sequences Typing of instruction sequences is defined recursively. - -Empty Instruction Sequence: :math:`\epsilon` -............................................ - $${rule-prose: Instrs_ok} $${rule: Instrs_ok/empty} +$${rule: Instrs_ok/instr} + $${rule: Instrs_ok/seq} -$${rule: {Instrs_ok/sub Instrs_ok/frame}} +$${rule: Instrs_ok/sub} .. note:: - In combination with the previous rule, - subsumption allows to compose instructions whose types would not directly fit otherwise. + This *subsumption rule* allows to weaken the type of an instruction sequence to a supertype, + which includes the ability to drop init variables ${:x*} from the instruction type in a context where they are not needed, for example, at the end of the body of a :ref:`block `. + +$${rule: Instrs_ok/frame} + +.. note:: + In combination with the previous two rules, + this *frame rule* allows to compose instructions whose types would not directly fit otherwise. For example, consider the instruction sequence $${instr*: (CONST I32 1) (CONST I32 2) (BINOP I32 ADD)} To type this sequence, its subsequence ${instr*: (CONST I32 2) (BINOP I32 ADD)} needs to be valid with an intermediate type. But the direct type of ${instr: (CONST I32 2)} is ${instrtype: eps -> I32}, not matching the two inputs expected by ${instr: $($(BINOP I32 ADD))}. - The subsumption rule allows to weaken the type of ${:(CONST I32 2)} to the supertype ${instrtype: I32 -> I32 I32}, such that it can be composed with ${instr: $($(BINOP I32 ADD))} and yields the intermediate type ${instrtype: I32 -> I32 I32} for the subsequence. That can in turn be composed with the first constant. - - Furthermore, subsumption allows to drop init variables ${:x*} from the instruction type in a context where they are not needed, for example, at the end of the body of a :ref:`block `. + The rule allows to weaken the type of ${instr: (CONST I32 2)} to the supertype ${instrtype: I32 -> I32 I32}, such that it can be composed with ${instr: $($(BINOP I32 ADD))} and yields the intermediate type ${instrtype: I32 -> I32 I32} for the subsequence. That can in turn be composed with the first constant. .. index:: expression, result type diff --git a/document/core/valid/matching.rst b/document/core/valid/matching.rst index 2b2a2e2b5..0043063d9 100644 --- a/document/core/valid/matching.rst +++ b/document/core/valid/matching.rst @@ -39,13 +39,12 @@ Heap Types $${rule-prose: Heaptype_sub} $${rule: - {Heaptype_sub/refl Heaptype_sub/exact-l} + {Heaptype_sub/refl} {Heaptype_sub/exact-l} {Heaptype_sub/trans} {Heaptype_sub/eq-any Heaptype_sub/i31-eq Heaptype_sub/struct-eq Heaptype_sub/array-eq} {Heaptype_sub/struct Heaptype_sub/array Heaptype_sub/func} {Heaptype_sub/typeidx-l Heaptype_sub/typeidx-r} - {Heaptype_sub/rec} - {Heaptype_sub/none Heaptype_sub/nofunc Heaptype_sub/noexn Heaptype_sub/noextern} + {Heaptype_sub/none Heaptype_sub/nofunc} {Heaptype_sub/noexn Heaptype_sub/noextern} {Heaptype_sub/bot} } $${rule-ignore: Heaptype_sub/def} diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index f53dfc44c..448e91eaa 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -289,4 +289,4 @@ $${rule: Module_ok} However, this recursion is just a specification device. All types needed to construct ${:C} can easily be determined from a simple pre-pass over the module that does not perform any actual validation. - Globals, however, are not recursive but evaluated sequentially, such that each :ref:`constant expressions ` only has access to imported or previously defined globals. + Globals, however, are not recursive but evaluated sequentially, such that each :ref:`constant expressions ` only has access to imported or previously defined globals. diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index a20422a57..b8c02667a 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -213,17 +213,10 @@ Recursive Types :ref:`Recursive types ` are validated with respect to the first :ref:`type index ` defined by the recursive group. -:math:`\TREC~\subtype^\ast` -........................... - $${rule-prose: Rectype_ok} $${rule: {Rectype_ok/empty Rectype_ok/cons}} - -:math:`\TSUB~\TFINAL^?~y^\ast~\desctype` -........................................ - $${rule-prose: Subtype_ok} $${rule: Subtype_ok} diff --git a/document/index.html b/document/index.html index 322b4d94f..8813e3253 100644 --- a/document/index.html +++ b/document/index.html @@ -112,7 +112,7 @@

All Versions

diff --git a/document/js-api/index.bs b/document/js-api/index.bs index e5abc4ba3..64dfd22f7 100644 --- a/document/js-api/index.bs +++ b/document/js-api/index.bs @@ -9,6 +9,7 @@ TR: https://www.w3.org/TR/wasm-js-api-2/ ED: https://webassembly.github.io/spec/js-api/ Implementation Report: https://webassembly.org/features/ Editor: Ms2ger, w3cid 46309, Igalia +Editor: Ryan Hunt, w3cid 112030, Mozilla Foundation Repository: WebAssembly/spec Markup Shorthands: css no, markdown yes Abstract: This document provides an explicit JavaScript API for interacting with WebAssembly. @@ -34,7 +35,7 @@ Date: now
-urlPrefix: https://tc39.github.io/ecma262/; spec: ECMASCRIPT
+urlPrefix: https://tc39.es/ecma262/; spec: ECMASCRIPT
     type: interface; for: ECMAScript
         text: ArrayBuffer; url: sec-arraybuffer-objects
     type: exception; for: ECMAScript
@@ -67,14 +68,10 @@ urlPrefix: https://tc39.github.io/ecma262/; spec: ECMASCRIPT
             text: is an Object
             text: is not an Object
         text: current Realm; url: current-realm
-        text: ObjectCreate; url: sec-objectcreate
         text: CreateBuiltinFunction; url: sec-createbuiltinfunction
-        text: SetFunctionName; url: sec-setfunctionname
-        text: SetFunctionLength; url: sec-setfunctionlength
         text: the Number value; url: sec-ecmascript-language-types-number-type
         text: is a Number; url: sec-ecmascript-language-types-number-type
         text: is a BigInt; url: sec-ecmascript-language-types-bigint-type
-        text: NumberToRawBytes; url: sec-numbertorawbytes
         text: Built-in Function Objects; url: sec-built-in-function-objects
         text: NativeError Object Structure; url: sec-nativeerror-object-structure
         text: CreateArrayFromList; url: sec-createarrayfromlist
@@ -84,8 +81,6 @@ urlPrefix: https://tc39.github.io/ecma262/; spec: ECMASCRIPT
         text: BigInt; url: #sec-ecmascript-language-types-bigint-type
         text: MakeBasicObject; url: #sec-makebasicobject
         text: ℝ; url: #ℝ
-        text: Built-in Function Objects; url: sec-built-in-function-objects
-        text: NativeError Object Structure; url: sec-nativeerror-object-structure
         text: 𝔽; url: #𝔽
         text: ℤ; url: #ℤ
         text: mathematical value; url: #mathematical-value
@@ -101,7 +96,7 @@ urlPrefix: https://tc39.github.io/ecma262/; spec: ECMASCRIPT
         text: Array; url: sec-array-exotic-objects
         text: BigInt; url: sec-ecmascript-language-types-bigint-type
 urlPrefix: https://webassembly.github.io/spec/core/; spec: WebAssembly; type: dfn
-    text: embedding interface; url: appending/embedding.html
+    text: embedding interface; url: appendix/embedding.html
     text: scope; url: intro/introduction.html#scope
     url: valid/modules.html#valid-module
         text: valid
@@ -167,6 +162,7 @@ urlPrefix: https://webassembly.github.io/spec/core/; spec: WebAssembly; type: df
     text: match_valtype; url: appendix/embedding.html#embed-match-valtype
     text: match_externtype; url: appendix/embedding.html#embed-match-externtype
     text: error; url: appendix/embedding.html#embed-error
+    text: exception; url: appendix/embedding.html#embed-error
     text: store; url: exec/runtime.html#syntax-store
     text: address type; url: syntax/types.html#syntax-addrtype
     text: limits; url: syntax/types.html#syntax-limits
@@ -221,6 +217,10 @@ urlPrefix: https://webassembly.github.io/spec/core/; spec: WebAssembly; type: df
     url: exec/runtime.html#syntax-externval
         text: external value
         for: external value
+            text: func
+            text: table
+            text: mem
+            text: global
             text: tag
     text: host function; url: exec/runtime.html#syntax-hostfunc
     text: the instantiation algorithm; url: exec/modules.html#instantiation
@@ -250,7 +250,7 @@ urlPrefix: https://webassembly.github.io/spec/core/; spec: WebAssembly; type: df
     text: signed_64; url: exec/numerics.html#aux-signed
     text: sequence; url: syntax/conventions.html#grammar-notation
     text: exception; for: tagtype/attribute; url: syntax/types.html#syntax-tagtype
-urlPrefix: https://heycam.github.io/webidl/; spec: WebIDL
+urlPrefix: https://webidl.spec.whatwg.org/; spec: WebIDL
     type: dfn
         text: create a namespace object; url: create-a-namespace-object
         text: [EnforceRange]; url: #EnforceRange
@@ -352,7 +352,7 @@ Each [=agent=] is associated with the following [=ordered map=]s:
     * The Exported Function cache, mapping [=function address=]es to [=Exported Function=] objects.
     * The Exported GC Object cache, mapping [=struct address=]es and [=array address=]es to [=Exported GC Object=] objects.
     * The Global object cache, mapping [=global address=]es to {{Global}} objects.
-    * The Tag object cache, mapping [=tag addresses=] to {{Tag}} objects.
+    * The Tag object cache, mapping [=tag address=]es to {{Tag}} objects.
     * The Exception object cache, mapping [=exception address=]es to {{Exception}} objects.
     * The Host value cache, mapping [=host address=]es to values.
 
@@ -372,11 +372,11 @@ dictionary WebAssemblyCompileOptions {
 
 [Exposed=*]
 namespace WebAssembly {
-    boolean validate(BufferSource bytes, optional WebAssemblyCompileOptions options = {});
-    Promise<Module> compile(BufferSource bytes, optional WebAssemblyCompileOptions options = {});
+    boolean validate([AllowResizable] AllowSharedBufferSource bytes, optional WebAssemblyCompileOptions options = {});
+    Promise<Module> compile([AllowResizable] AllowSharedBufferSource bytes, optional WebAssemblyCompileOptions options = {});
 
     Promise<WebAssemblyInstantiatedSource> instantiate(
-        BufferSource bytes, optional object importObject, optional WebAssemblyCompileOptions options = {});
+        [AllowResizable] AllowSharedBufferSource bytes, optional object importObject, optional WebAssemblyCompileOptions options = {});
 
     Promise<Instance> instantiate(
         Module moduleObject, optional object importObject);
@@ -412,7 +412,7 @@ To validate builtins and imported string for a WebAssembly module fro
         1. Let |stringExternType| be `global const (ref extern)`.
         1. If [=match_externtype=](|stringExternType|, |importExternType|) is false, return false
     1. Else,
-        1. If [=validate an import for builtins|validating a import for builtin=] with |import| and |builtinSetNames| is false, return false.
+        1. If [=validate an import for builtins|validating an import for builtins=] with |import| and |builtinSetNames| is false, return false.
 1. Return true.
 
 
@@ -438,7 +438,7 @@ A {{Module}} object represents a single WebAssembly module. Each {{Module}} obje
 
To construct a WebAssembly module object from a module |module|, source bytes |bytes|, enabled builtins |builtinSetNames|, and |importedStringModule|, perform the following steps: - 1. Let |moduleObject| be a new {{Module}} object. + 1. Let |moduleObject| be a [=/new=] {{Module}}. 1. Set |moduleObject|.\[[Module]] to |module|. 1. Set |moduleObject|.\[[Bytes]] to |bytes|. 1. Set |moduleObject|.\[[BuiltinSets]] to |builtinSetNames|. @@ -452,11 +452,11 @@ A {{Module}} object represents a single WebAssembly module. Each {{Module}} obje 1. Let |promise| be [=a new promise=]. 1. Run the following steps [=in parallel=]: 1. [=compile a WebAssembly module|Compile the WebAssembly module=] |bytes| and store the result as |module|. - 1. [=Queue a task=] to perform the following steps. If |taskSource| was provided, queue the task on that task source. - 1. If |module| is [=error=], reject |promise| with a {{CompileError}} exception. + 1. [=Queue a task=] on |taskSource|, if provided, to perform the following steps: + 1. If |module| is [=error=], [=reject=] |promise| with a {{CompileError}} exception and return. 1. Let |builtinSetNames| be |options|["builtins"]. 1. Let |importedStringModule| be |options|["importedStringConstants"]. - 1. If [=validate builtins and imported string for a WebAssembly module|validating builtins and imported strings=] for |module| with |builtinSetNames| and |importedStringModule| is false, reject |promise| with a {{CompileError}} exception. + 1. If [=validate builtins and imported string for a WebAssembly module|validating builtins and imported strings=] for |module| with |builtinSetNames| and |importedStringModule| is false, [=reject=] |promise| with a {{CompileError}} exception. 1. Otherwise, 1. [=Construct a WebAssembly module object=] from |module|, |bytes|, |builtinSetNames|, |importedStringModule|, and let |moduleObject| be the result. 1. [=Resolve=] |promise| with |moduleObject|. @@ -474,7 +474,7 @@ A {{Module}} object represents a single WebAssembly module. Each {{Module}} obje To instantiate imported strings with module |module| and |importedStringModule|, perform the following steps: 1. Assert: |importedStringModule| is not null. -1. Let |exportsObject| be [=!=] [$OrdinaryObjectCreate$](null). +1. Let |exportsObject| be [$OrdinaryObjectCreate$](null). 1. [=list/iterate|For each=] (|moduleName|, |componentName|, |externtype|) of [=module_imports=](|module|), 1. If |moduleName| does not equal |importedStringModule|, then [=iteration/continue=]. 1. Let |stringConstant| be |componentName|. @@ -486,22 +486,22 @@ To instantiate imported strings with module |module| and |importedStr
To read the imports from a WebAssembly module |module| from imports object |importObject|, enabled builtins |builtinSetNames|, and |importedStringModule|, perform the following steps: - 1. If |module|.[=imports=] [=list/is empty|is not empty=], and |importObject| is undefined, throw a {{TypeError}} exception. - 1. Let |builtinOrStringImports| be the ordered map « ». + 1. If [=module_imports=](|module|) [=list/is empty|is not empty=], and |importObject| is missing, throw a {{TypeError}} exception. + 1. Let |builtinOrStringImports| be the ordered map «[ ]». 1. [=list/iterate|For each=] |builtinSetName| of |builtinSetNames|, - 1. Assert: |builtinOrStringImports| does not contain |builtinSetName| + 1. Let |builtinSetQualifiedName| be |builtinSetName| prefixed with "wasm:" + 1. Assert: |builtinOrStringImports| does not contain |builtinSetQualifiedName| 1. If |builtinSetName| does not refer to a builtin set, then [=iteration/continue=]. 1. Let |exportsObject| be the result of [=instantiate a builtin set=] with |builtinSetName| - 1. Let |builtinSetQualifiedName| be |builtinSetName| prefixed with "wasm:" 1. [=map/set|Set=] |builtinOrStringImports|[|builtinSetQualifiedName|] to |exportsObject| 1. If |importedStringModule| is not null, 1. Let |exportsObject| be the result of [=instantiate imported strings=] with |module| and |importedStringModule| 1. [=map/set|Set=] |builtinOrStringImports|[|importedStringModule|] to |exportsObject| 1. Let |imports| be « ». 1. [=list/iterate|For each=] (|moduleName|, |componentName|, |externtype|) of [=module_imports=](|module|), - 1. If |builtinOrStringImports| [=map/exist|contains=] |moduleName|, + 1. If |builtinOrStringImports|[|moduleName|] [=map/exists=], 1. Let |o| be |builtinOrStringImports|[|moduleName|]. - 1. If |o| [=is not an Object=] or if |o| [=map/exist|does not contain=] |componentName|, + 1. If |o| [=is not an Object=] or if [=?=] [$HasProperty$](|o|, |componentName|) is false, 1. Set |o| to [=?=] [$Get$](|importObject|, |moduleName|). 1. Else, 1. Let |o| be [=?=] [$Get$](|importObject|, |moduleName|). @@ -514,7 +514,7 @@ To instantiate imported strings with module |module| and |importedStr 1. Otherwise, 1. [=Create a host function=] from |v| and |functype|, and let |funcaddr| be the result. 1. Let |index| be the number of external functions in |imports|. This value |index| is known as the index of the host function |funcaddr|. - 1. Let |externfunc| be the [=external value=] [=external value|func=] |funcaddr|. + 1. Let |externfunc| be the [=external value=] [=external value/func=] |funcaddr|. 1. [=list/Append=] |externfunc| to |imports|. 1. If |externtype| is of the form [=external-type/global=] mut |valtype|, 1. If |v| [=implements=] {{Global}}, @@ -530,19 +530,18 @@ To instantiate imported strings with module |module| and |importedStr 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let (|store|, |globaladdr|) be [=global_alloc=](|store|, [=const=] |valtype|, |value|). 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. - 1. Let |externglobal| be [=external value|global=] |globaladdr|. + 1. Let |externglobal| be [=external value/global=] |globaladdr|. 1. [=list/Append=] |externglobal| to |imports|. 1. If |externtype| is of the form [=external-type/mem=] memtype, 1. If |v| does not [=implement=] {{Memory}}, throw a {{LinkError}} exception. - 1. Let |externmem| be the [=external value=] [=external value|mem=] |v|.\[[Memory]]. + 1. Let |externmem| be the [=external value=] [=external value/mem=] |v|.\[[Memory]]. 1. [=list/Append=] |externmem| to |imports|. 1. If |externtype| is of the form [=external-type/table=] tabletype, 1. If |v| does not [=implement=] {{Table}}, throw a {{LinkError}} exception. 1. Let |tableaddr| be |v|.\[[Table]]. - 1. Let |externtable| be the [=external value=] [=external value|table=] |tableaddr|. + 1. Let |externtable| be the [=external value=] [=external value/table=] |tableaddr|. 1. [=list/Append=] |externtable| to |imports|. - 1. If |externtype| is of the form [=external-type/tag=] |attribute| functype, - 1. Assert: |attribute| is [=tagtype/attribute/exception=]. + 1. If |externtype| is of the form [=external-type/tag=] functype, 1. If |v| does not [=implement=] {{Tag}}, throw a {{LinkError}} exception. 1. Let |tagaddr| be |v|.\[[Address]]. 1. Let |externtag| be the [=external value=] [=external value/tag=] |tagaddr|. @@ -556,32 +555,31 @@ The verification of WebAssembly type requirements is deferred to the
To create an exports object from a WebAssembly module |module| and instance |instance|, perform the following steps: - 1. Let |exportsObject| be [=!=] [$OrdinaryObjectCreate$](null). + 1. Let |exportsObject| be [$OrdinaryObjectCreate$](null). 1. [=list/iterate|For each=] (|name|, |externtype|) of [=module_exports=](|module|), 1. Let |externval| be [=instance_export=](|instance|, |name|). 1. Assert: |externval| is not [=error=]. 1. If |externtype| is of the form [=external-type/func=] functype, - 1. Assert: |externval| is of the form [=external value|func=] |funcaddr|. - 1. Let [=external value|func=] |funcaddr| be |externval|. + 1. Assert: |externval| is of the form [=external value/func=] |funcaddr|. + 1. Let [=external value/func=] |funcaddr| be |externval|. 1. Let |func| be the result of creating [=a new Exported Function=] from |funcaddr|. 1. Let |value| be |func|. 1. If |externtype| is of the form [=external-type/global=] mut globaltype, - 1. Assert: |externval| is of the form [=external value|global=] |globaladdr|. - 1. Let [=external value|global=] |globaladdr| be |externval|. + 1. Assert: |externval| is of the form [=external value/global=] |globaladdr|. + 1. Let [=external value/global=] |globaladdr| be |externval|. 1. Let |global| be [=create a global object|a new Global object=] created from |globaladdr|. 1. Let |value| be |global|. 1. If |externtype| is of the form [=external-type/mem=] memtype, - 1. Assert: |externval| is of the form [=external value|mem=] |memaddr|. - 1. Let [=external value|mem=] |memaddr| be |externval|. + 1. Assert: |externval| is of the form [=external value/mem=] |memaddr|. + 1. Let [=external value/mem=] |memaddr| be |externval|. 1. Let |memory| be [=create a memory object|a new Memory object=] created from |memaddr|. 1. Let |value| be |memory|. 1. If |externtype| is of the form [=external-type/table=] tabletype, - 1. Assert: |externval| is of the form [=external value|table=] |tableaddr|. - 1. Let [=external value|table=] |tableaddr| be |externval|. + 1. Assert: |externval| is of the form [=external value/table=] |tableaddr|. + 1. Let [=external value/table=] |tableaddr| be |externval|. 1. Let |table| be [=create a Table object|a new Table object=] created from |tableaddr|. 1. Let |value| be |table|. - 1. If |externtype| is of the form [=external-type/tag=] |attribute| functype, - 1. Assert: |attribute| is [=tagtype/attribute/exception=]. + 1. If |externtype| is of the form [=external-type/tag=] functype, 1. Assert: |externval| is of the form [=external value/tag=] |tagaddr|. 1. Let [=external value/tag=] |tagaddr| be |externval|. 1. Let |tag| be [=create a Tag object|a new Tag object=] created from |tagaddr|. @@ -605,14 +603,13 @@ The verification of WebAssembly type requirements is deferred to the
To instantiate the core of a WebAssembly module from a module |module| and imports |imports|, perform the following steps: 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. - 1. Let |result| be [=module_instantiate=](|store|, |module|, |imports|). + 1. Let (|store|, |result|) be [=module_instantiate=](|store|, |module|, |imports|). 1. If |result| is [=error=], throw an appropriate exception type: * A {{LinkError}} exception for most cases which occur during linking. * If the error came when running the start function, throw a {{RuntimeError}} for most errors which occur from WebAssembly, or the error object propagated from inner ECMAScript code. * Another error type if appropriate, for example an out-of-memory exception, as documented in the WebAssembly error mapping. - 1. Let (|store|, |instance|) be |result|. 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. - 1. Return |instance|. + 1. Return |result|.
@@ -667,10 +664,13 @@ The verification of WebAssembly type requirements is deferred to the Note: A follow-on streaming API is documented in the WebAssembly Web API. +
+ The getter of the JSTag attribute of the {{WebAssembly}} Namespace, when invoked, performs the following steps: 1. Let |JSTagAddr| be the result of [=get the JavaScript exception tag|getting the JavaScript exception tag=]. 1. Let |JSTagObject| be the result of [=create a Tag object|creating a Tag object=] from |JSTagAddr|. 1. Return |JSTagObject|. +

Modules

@@ -704,7 +704,7 @@ dictionary ModuleImportDescriptor { [LegacyNamespace=WebAssembly, Exposed=*] interface Module { - constructor(BufferSource bytes, optional WebAssemblyCompileOptions options = {}); + constructor([AllowResizable] AllowSharedBufferSource bytes, optional WebAssemblyCompileOptions options = {}); static sequence<ModuleExportDescriptor> exports(Module moduleObject); static sequence<ModuleImportDescriptor> imports(Module moduleObject); static sequence<ArrayBuffer> customSections(Module moduleObject, DOMString sectionName); @@ -786,10 +786,10 @@ interface Instance {
- The Instance(|module|, |importObject|) constructor, when invoked, runs the following steps: - 1. Let |module| be |module|.\[[Module]]. - 1. Let |builtinSetNames| be |module|.\[[BuiltinSets]]. - 1. Let |importedStringModule| be |module|.\[[ImportedStringModule]]. + The Instance(|moduleObject|, |importObject|) constructor, when invoked, runs the following steps: + 1. Let |builtinSetNames| be |moduleObject|.\[[BuiltinSets]]. + 1. Let |importedStringModule| be |moduleObject|.\[[ImportedStringModule]]. + 1. Let |module| be |moduleObject|.\[[Module]]. 1. [=Read the imports=] of |module| with imports |importObject|, |builtinSetNames|, and |importedStringModule|, and let |imports| be the result. 1. [=Instantiate the core of a WebAssembly module=] |module| with |imports|, and let |instance| be the result. 1. [=initialize an instance object|Initialize=] **this** from |module| and |instance|. @@ -846,7 +846,7 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each 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|.\[[ArrayBufferMaxByteLength]] to |maxsize|. 1. Set |buffer|.\[[ArrayBufferDetachKey]] to "WebAssembly.Memory". 1. Return |buffer|.
@@ -874,7 +874,7 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each
The Memory(|descriptor|) constructor, when invoked, performs the following steps: - 1. If |descriptor|["address"] [=map/exists=], let |addrtype| be |descriptor|["address"]; otherwise, let |addrtype| be "i32". + 1. If |descriptor|["address"] [=map/exists=], let |addrtype| be [=ToValueType=](|descriptor|["address"]); otherwise, let |addrtype| be [=i32=]. 1. Let |initial| be [=?=] [=AddressValueToU64=](|descriptor|["initial"], |addrtype|). 1. If |descriptor|["maximum"] [=map/exists=], let |maximum| be [=?=] [=AddressValueToU64=](|descriptor|["maximum"], |addrtype|); otherwise, let |maximum| be empty. 1. Let |memtype| be [=memory type=] |addrtype| { **min** |initial|, **max** |maximum| }. @@ -906,7 +906,7 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each To grow the memory buffer associated with a [=memory address=] |memaddr| by |delta|, perform the following steps: 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. - 1. Let |ret| be the [=mem_size=](|store|, |memaddr|). + 1. Let |ret| be [=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|. @@ -924,13 +924,13 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each 1. Return [=U64ToAddressValue=](|ret|, |addrtype|).
-Immediately after a WebAssembly [=memory.grow=] instruction executes, perform the following steps: +Immediately after a WebAssembly [=memory.grow=] |x| instruction executes, perform the following steps:
- 1. If the top of the stack is not [=i32.const=] (−1), + 1. If the top of the stack is not [=i32.const=] (−1) and the top of the stack is not [=i64.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. Assert: due to validation, |frame|.[=frame/module=].[=moduleinst/memaddrs=][|x|] exists. + 1. Let |memaddr| be the [=memory address=] |frame|.[=frame/module=].[=moduleinst/memaddrs=][|x|]. 1. [=Refresh the memory buffer=] of |memaddr|.
@@ -979,7 +979,7 @@ Immediately after a WebAssembly [=memory.grow=] instruction executes, perform th 1. Throw a {{RangeError}} exception. 1. Let |delta| be |lengthDelta| ÷ 65536. 1. [=Grow the memory buffer=] associated with |memaddr| by |delta|. - 1. Return handled. + 1. Return handled. 1. Otherwise, return unhandled. @@ -1041,16 +1041,16 @@ Each {{Table}} object has a \[[Table]] internal slot, which is a [=table address 1. Let |elementtype| be [=ToValueType=](|descriptor|["element"]). 1. If |elementtype| is not a [=reftype=], 1. [=Throw=] a {{TypeError}} exception. - 1. If |descriptor|["address"] [=map/exists=], let |addrtype| be |descriptor|["address"]; otherwise, let |addrtype| be "i32". + 1. If |descriptor|["address"] [=map/exists=], let |addrtype| be [=ToValueType=](|descriptor|["address"]); otherwise, let |addrtype| be [=i32=]. 1. Let |initial| be [=?=] [=AddressValueToU64=](|descriptor|["initial"], |addrtype|). 1. If |descriptor|["maximum"] [=map/exists=], let |maximum| be [=?=] [=AddressValueToU64=](|descriptor|["maximum"], |addrtype|); otherwise, let |maximum| be empty. - 1. Let |type| be the [=table type=] |addrtype| { [=limits|min=] |initial|, [=limits|max=] |maximum| } |elementType|. + 1. Let |type| be the [=table type=] |addrtype| { [=limits|min=] |initial|, [=limits|max=] |maximum| } |elementtype|. 1. If |type| is not [=valid tabletype|valid=], throw a {{RangeError}} exception. 1. If |value| is missing, 1. Let |ref| be [=DefaultValue=](|elementtype|). 1. Assert: |ref| is not [=error=]. 1. Otherwise, - 1. Let |ref| be [=?=] [=ToWebAssemblyValue=](|value|, |elementType|). + 1. Let |ref| be [=?=] [=ToWebAssemblyValue=](|value|, |elementtype|). 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let (|store|, |tableaddr|) be [=table_alloc=](|store|, |type|, |ref|). If allocation fails, throw a {{RangeError}} exception. 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. @@ -1075,7 +1075,7 @@ Each {{Table}} object has a \[[Table]] internal slot, which is a [=table address Note: The above exception can happen due to either insufficient memory or an invalid size parameter. 1. Set the [=surrounding agent=]'s [=associated store=] to |result|. - 1. Return |initialSize|. + 1. Return [=U64ToAddressValue=](|initialSize|, |addrtype|).
@@ -1186,7 +1186,7 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each
The algorithm DefaultValue(|valuetype|) performs the following steps: - 1. If |valuetype| equals [=externref=], return [=ToWebAssemblyValue=](undefined, |valuetype|). + 1. If |valuetype| equals [=externref=], return [=!=] [=ToWebAssemblyValue=](undefined, |valuetype|). 1. Return [=val_default=](|valuetype|).
@@ -1200,17 +1200,17 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each 1. Let |value| be [=DefaultValue=](|valuetype|). 1. Assert: |value| is not [=error=]. 1. Otherwise, - 1. Let |value| be [=ToWebAssemblyValue=](|v|, |valuetype|). + 1. Let |value| be [=?=] [=ToWebAssemblyValue=](|v|, |valuetype|). 1. If |mutable| is true, let |globaltype| be [=var=] |valuetype|; otherwise, let |globaltype| be [=const=] |valuetype|. - 1. Let |store| be the current agent's [=associated store=]. + 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let (|store|, |globaladdr|) be [=global_alloc=](|store|, |globaltype|, |value|). - 1. Set the current agent's [=associated store=] to |store|. + 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. 1. [=initialize a global object|Initialize=] **this** from |globaladdr|.
The algorithm GetGlobalValue({{Global}} |global|) performs the following steps: - 1. Let |store| be the current agent's [=associated store=]. + 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let |globaladdr| be |global|.\[[Global]]. 1. Let |globaltype| be [=global_type=](|store|, |globaladdr|). 1. If |globaltype| is of the form mut |valuetype| where |valuetype| [=matches/valtype|matches=] [=v128=] or [=exnref=], throw a {{TypeError}}. @@ -1218,20 +1218,22 @@ which can be simultaneously referenced by multiple {{Instance}} objects. Each 1. Return [=ToJSValue=](|value|).
-
+
The getter of the value attribute of {{Global}}, when invoked, performs the following steps: 1. Return [=GetGlobalValue=](**this**). +
+
The setter of the value attribute of {{Global}}, when invoked, performs the following steps: - 1. Let |store| be the current agent's [=associated store=]. + 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let |globaladdr| be **this**.\[[Global]]. 1. Let |mut| |valuetype| be [=global_type=](|store|, |globaladdr|). 1. If |valuetype| [=matches/valtype|matches=] [=v128=] or [=exnref=], throw a {{TypeError}}. 1. If |mut| is [=const=], throw a {{TypeError}}. - 1. Let |value| be [=ToWebAssemblyValue=](**the given value**, |valuetype|). + 1. Let |value| be [=?=] [=ToWebAssemblyValue=](**the given value**, |valuetype|). 1. Let |store| be [=global_write=](|store|, |globaladdr|, |value|). 1. If |store| is [=error=], throw a {{RangeError}} exception. - 1. Set the current agent's [=associated store=] to |store|. + 1. Set the [=surrounding agent=]'s [=associated store=] to |store|.
@@ -1255,8 +1257,8 @@ This slot holds a [=function address=] relative to the [=surrounding agent=]'s [ 1. Let |index| be the [=index of the host function=] |funcaddr|. 1. Otherwise, 1. Let |moduleinst| be |funcinst|.module. - 1. Assert: |funcaddr| is contained in |moduleinst|.funcaddrs. - 1. Let |index| be the index of |moduleinst|.funcaddrs where |funcaddr| is found. + 1. Assert: |funcaddr| is contained in |moduleinst|.funcs. + 1. Let |index| be the index of |moduleinst|.funcs where |funcaddr| is found. 1. Return [=!=] [$ToString$](|index|).
@@ -1273,7 +1275,7 @@ This slot holds a [=function address=] relative to the [=surrounding agent=]'s [ 1. Let [|paramTypes|] → [resultTypes] be |functype|. 1. Let |arity| be |paramTypes|'s [=list/size=]. 1. Let |name| be the [=name of the WebAssembly function=] |funcaddr|. - 1. Let |function| be [=!=] [$CreateBuiltinFunction$](|steps|, |arity|, |name|, « \[[FunctionAddress]] », |realm|). + 1. Let |function| be [$CreateBuiltinFunction$](|steps|, |arity|, |name|, « \[[FunctionAddress]] », |realm|). 1. Set |function|.\[[FunctionAddress]] to |funcaddr|. 1. [=map/Set=] |map|[|funcaddr|] to |function|. 1. Return |function|. @@ -1293,17 +1295,17 @@ This slot holds a [=function address=] relative to the [=surrounding agent=]'s [ 1. [=list/iterate|For each=] |t| of |parameters|, 1. If |argValues|'s [=list/size=] > |i|, let |arg| be |argValues|[|i|]. 1. Otherwise, let |arg| be undefined. - 1. [=list/Append=] [=ToWebAssemblyValue=](|arg|, |t|) to |args|. + 1. [=list/Append=] [=?=] [=ToWebAssemblyValue=](|arg|, |t|) to |args|. 1. Set |i| to |i| + 1. 1. Let (|store|, |ret|) be the result of [=func_invoke=](|store|, |funcaddr|, |args|). 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. 1. If |ret| is [=error=], throw an exception. This exception should be a WebAssembly {{RuntimeError}} exception, unless otherwise indicated by the WebAssembly error mapping. - 1. If |ret| is [=THROW=] [=ref.exn=] |exnaddr|, then + 1. If |ret| is of the form [=/exception=] |exnaddr|, then 1. Let |tagaddr| be [=exn_tag=](|store|, |exnaddr|). 1. Let |payload| be [=exn_read=](|store|, |exnaddr|). - 1. Let |jsTagAddr| be the result of [=get the JavaScript exception tag |getting the JavaScript exception tag=]. + 1. Let |jsTagAddr| be the result of [=get the JavaScript exception tag|getting the JavaScript exception tag=]. 1. If |tagaddr| is equal to |jsTagAddr|, - 1. Throw the result of [=retrieving a host value=] from |payload|[0]. + 1. Throw [=ToJSValue=](|payload|[0]). 1. Otherwise, 1. Let |exception| be [=create an Exception object|a new Exception=] created from |exnaddr|. 1. Throw |exception|. @@ -1328,7 +1330,7 @@ Note: Exported Functions do not have a \[[Construct]] method and thus it is not 1. If any type in |parameters| or |results| [=matches/valtype|matches=] [=v128=] or [=exnref=], throw a {{TypeError}}. 1. Let |jsArguments| be « ». 1. [=list/iterate|For each=] |arg| of |arguments|, - 1. [=list/Append=] [=!=] [=ToJSValue=](|arg|) to |jsArguments|. + 1. [=list/Append=] [=ToJSValue=](|arg|) to |jsArguments|. 1. Let |ret| be [=?=] [$Call$](|func|, undefined, |jsArguments|). 1. Let |resultsSize| be |results|'s [=list/size=]. 1. If |resultsSize| is 0, return « ». @@ -1340,7 +1342,7 @@ Note: Exported Functions do not have a \[[Construct]] method and thus it is not 1. Let |wasmValues| be a new, empty [=list=]. 1. If |values|'s [=list/size=] is not |resultsSize|, throw a {{TypeError}} exception. 1. For each |value| and |resultType| in |values| and |results|, paired linearly, - 1. [=list/Append=] [=ToWebAssemblyValue=](|value|, |resultType|) to |wasmValues|. + 1. [=list/Append=] [=?=] [=ToWebAssemblyValue=](|value|, |resultType|) to |wasmValues|. 1. Return |wasmValues|.
@@ -1364,12 +1366,13 @@ Note: Exported Functions do not have a \[[Construct]] method and thus it is not 1. If |v| [=implements=] {{Exception}}, 1. Let |address| be |v|.\[[Address]]. 1. Otherwise, - 1. Let |type| be the result of [=get the JavaScript exception tag |getting the JavaScript exception tag=]. + 1. Let |type| be the result of [=get the JavaScript exception tag|getting the JavaScript exception tag=]. 1. Let |payload| be [=!=] [=ToWebAssemblyValue=](|v|, [=externref=]). 1. Let (|store|, |address|) be [=exn_alloc=](|store|, |type|, « |payload| »). 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. 1. Execute the WebAssembly instructions ([=ref.exn=] |address|) ([=throw_ref=]). 1. Otherwise, return |result|.\[[Value]]. + 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let (|store|, |funcaddr|) be [=func_alloc=](|store|, |functype|, |hostfunc|). 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. 1. Return |funcaddr|. @@ -1385,7 +1388,7 @@ The algorithm ToJSValue(|w|) coerces a [=WebAssembly value=] to a Jav 1. Return [=ℤ=](|i64| interpreted as a [=mathematical value=]). 1. If |w| is of the form [=i32.const=] |u32|, 1. Let |i32| be [=signed_32=](|u32|). - 2. Return [=𝔽=](|i32| interpreted as a [=mathematical value=]). + 1. Return [=𝔽=](|i32| interpreted as a [=mathematical value=]). 1. If |w| is of the form [=f32.const=] |f32|, 1. If |f32| is [=+∞=] or [=−∞=], return **+∞**𝔽 or **-∞**𝔽, respectively. 1. If |f32| is [=nan=], return **NaN**. @@ -1394,10 +1397,10 @@ The algorithm ToJSValue(|w|) coerces a [=WebAssembly value=] to a Jav 1. If |f64| is [=+∞=] or [=−∞=], return **+∞**𝔽 or **-∞**𝔽, respectively. 1. If |f64| is [=nan=], return **NaN**. 1. Return [=𝔽=](|f64| interpreted as a [=mathematical value=]). -1. If |w| is of the form [=ref.null=] t, return null. +1. If |w| is of the form [=ref.null=], return null. 1. If |w| is of the form [=ref.i31=] |u31|, 1. Let |i31| be [=signed_31=](|u31|). - 1. Let return [=𝔽=](|i31|). + 1. Return [=𝔽=](|i31| interpreted as a [=mathematical value=]). 1. If |w| is of the form [=ref.struct=] |structaddr|, return the result of creating [=a new Exported GC Object=] from |structaddr| and "struct". 1. If |w| is of the form [=ref.array=] |arrayaddr|, return the result of creating [=a new Exported GC Object=] from |arrayaddr| and "array". 1. If |w| is of the form [=ref.func=] |funcaddr|, return the result of creating [=a new Exported Function=] from |funcaddr|. @@ -1447,34 +1450,34 @@ The algorithm ToWebAssemblyValue(|v|, |type|) coerces a JavaScript va 1. Otherwise, 1. Let |f64| be |number|. 1. Return [=f64.const=] |f64|. -1. If |type| is of the form [=ref=] |null| |heaptype|, +1. If |type| is of the form [=ref=] |null| heaptype, 1. If |v| is null, - 1. Let |r| be [=ref.null=] |heaptype|. - 1. Else if [=match_valtype=](|type|, [=ref=] |null| [=heap-type/extern=]), - 1. Let |ref| be [=ToWebAssemblyValue=](|v|, [=ref=] [=heap-type/any=]). + 1. Let |r| be [=ref.null=]. + 1. Else if [=match_valtype=](|type|, [=ref=] |null| [=heap-type/extern=]) is true, + 1. Let |ref| be [=!=] [=ToWebAssemblyValue=](|v|, [=ref=] [=heap-type/any=]). 1. Let |r| be [=ref.extern=] |ref|. - 1. Else if |v| is an [=Exported Function=] and [=match_valtype=](|type|, [=ref=] |null| [=heap-type/func=]), + 1. Else if |v| is an [=Exported Function=] and [=match_valtype=](|type|, [=ref=] |null| [=heap-type/func=]) is true, 1. Let |funcaddr| be the value of |v|'s \[[FunctionAddress]] internal slot. 1. Let |r| be [=ref.func=] |funcaddr|. 1. Else if |v| [=is a Number=] and |v| is equal to [=?=] [$ToInt32$](|v|) and [=ℝ=](|v|) < 230 and [=ℝ=](|v|) ⩾ -230, - 1. Let |i31| [=?=] [$ToInt32$](|v|). - 1. Let |u31| be the unsigned integer such that |i31| is [=signed_31=](|i31|). + 1. Let |i31| be [=?=] [$ToInt32$](|v|). + 1. Let |u31| be the unsigned integer such that |i31| is [=signed_31=](|u31|). 1. Let |r| be [=ref.i31=] |u31|. 1. Else if |v| is an [=Exported GC Object=], 1. Let |objectaddr| be the value of |v|'s \[[ObjectAddress]] internal slot. 1. Let |objectkind| be the value of |v|'s \[[ObjectKind]] internal slot. 1. If |objectkind| is "array", 1. Let |r| be [=ref.array=] |objectaddr|. - 1. If |objectkind| is "struct", + 1. Else if |objectkind| is "struct", 1. Let |r| be [=ref.struct=] |objectaddr|. 1. Else, 1. Let |map| be the [=surrounding agent=]'s associated [=host value cache=]. 1. If a [=host address=] |hostaddr| exists such that |map|[|hostaddr|] is the same as |v|, 1. Return [=ref.host=] |hostaddr|. - 1. Let [=host address=] |hostaddr| be the smallest address such that |map|[|hostaddr|] [=map/exists=] is false. + 1. Let |hostaddr| be the smallest [=host address=] such that |map|[|hostaddr|] [=map/exists=] is false. 1. [=map/Set=] |map|[|hostaddr|] to |v|. 1. Let |r| be [=ref.host=] |hostaddr|. - 1. Let |store| be the current agent's [=associated store=]. + 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let |actualtype| be [=ref_type=](|store|, |r|). 1. If [=match_valtype=](|actualtype|, |type|) is false, 1. Throw a {{TypeError}}. @@ -1486,12 +1489,12 @@ The algorithm ToWebAssemblyValue(|v|, |type|) coerces a JavaScript va
The algorithm AddressValueToU64(|v|, |addrtype|) converts a JavaScript value to a WebAssembly [=u64=] for use in embedding operations. It is designed to act like [=[EnforceRange]=] [=unsigned long=] for {{AddressType}} "i32", and to extend these semantics to {{AddressType}} "i64", by performing the following steps: -1. If |addrtype| is "i32", +1. If |addrtype| is [=i32=], 1. Let |n| be [=?=] [$ConvertToInt$](|v|, 32, "unsigned"), where the destination type is associated with [=[EnforceRange]=]. Note: This is equivalent to the [=js-unsigned-long|JS conversion rules=] for [=[EnforceRange]=] [=unsigned long=]. 1. Return [=ℝ=](|n|) as a WebAssembly [=u64=]. -1. If |addrtype| is "i64", +1. If |addrtype| is [=i64=], 1. Let |n| be [=?=] [$ToBigInt$](|v|). 1. If |n| < 0 or |n| > 264 − 1, [=throw=] a {{TypeError}}. @@ -1504,16 +1507,14 @@ The algorithm AddressValueToU64(|v|, |addrtype|) converts a JavaScrip
The algorithm U64ToAddressValue(|v|, |addrtype|) converts a [=u64=] value from a WebAssembly embedding operation to the correct variant of {{AddressValue}} for an {{AddressType}}, by performing the following steps: -1. If |addrtype| is "i32", return [=𝔽=](|v| interpreted as a [=mathematical value=]). -1. Else if |addrtype| is "i64", return [=ℤ=](|v| interpreted as a [=mathematical value=]). +1. If |addrtype| is [=i32=], return [=𝔽=](|v| interpreted as a [=mathematical value=]). +1. Else if |addrtype| is [=i64=], return [=ℤ=](|v| interpreted as a [=mathematical value=]). 1. Assert: This step is not reached.

Tags

-The tag_alloc(|store|, |parameters|) algorithm creates a new [=tag address=] for |parameters| in |store| and returns the updated store and the [=tag address=]. -

Tag types

@@ -1521,7 +1522,7 @@ dictionary TagType {
   required sequence<ValueType> parameters;
 };
 
-[LegacyNamespace=WebAssembly, Exposed=(Window,Worker,Worklet)]
+[LegacyNamespace=WebAssembly, Exposed=*]
 interface Tag {
   constructor(TagType type);
 };
@@ -1546,7 +1547,7 @@ To create a Tag object from a [=tag address=] |tagAddress|, perform t
 1. Let |map| be the [=surrounding agent=]'s associated [=Tag object cache=].
 1. If |map|[|tagAddress|] [=map/exists=],
     1. Return |map|[|tagAddress|].
-1. Let |tag| be a [=new=] {{Tag}}.
+1. Let |tag| be a [=/new=] {{Tag}}.
 1. [=initialize a Tag object|Initialize=] |tag| from |tagAddress|.
 1. Return |tag|.
 
@@ -1558,11 +1559,11 @@ The new Tag(|type|) constructor
 
 1. Let |parameters| be |type|["parameters"].
 1. Let |wasmParameters| be «».
-1. [=list/iterate|For each=] |type| of |parameters|,
-    1. [=list/Append=] [=ToValueType=](|type|) to |wasmParameters|.
-1. Let |store| be the current agent's [=associated store=].
-1. Let (|store|, |tagAddress|) be [=tag_alloc=](|store|, |wasmParameters|).
-1. Set the current agent's [=associated store=] to |store|.
+1. [=list/iterate|For each=] |paramType| of |parameters|,
+    1. [=list/Append=] [=ToValueType=](|paramType|) to |wasmParameters|.
+1. Let |store| be the [=surrounding agent=]'s [=associated store=].
+1. Let (|store|, |tagAddress|) be [=tag_alloc=](|store|, |wasmParameters| → « »).
+1. Set the [=surrounding agent=]'s [=associated store=] to |store|.
 1. [=initialize a Tag object|Initialize=] **this** from |tagAddress|.
 
 
@@ -1644,8 +1645,7 @@ The internal methods of an [=Exported GC Object=] use the following implementati
The \[[OwnPropertyKeys]] internal method of an Exported GC Object O takes no arguments and returns a list. It performs the following steps when called: - 1. Let keys be a new empty list. - 1. Return keys. + 1. Return « ».
@@ -1655,7 +1655,7 @@ The internal methods of an [=Exported GC Object=] use the following implementati 1. Let |map| be the [=surrounding agent=]'s associated [=exported GC object cache=]. 1. If |map|[|objectaddr|] [=map/exists=], 1. Return |map|[|objectaddr|]. - 1. Let |object| be [=MakeBasicObject=](« \[[ObjectAddress]] »). + 1. Let |object| be [=MakeBasicObject=](« \[[ObjectAddress]], \[[ObjectKind]] »). 1. Set |object|.\[[ObjectAddress]] to |objectaddr|. 1. Set |object|.\[[ObjectKind]] to |objectkind|. 1. Set |object|.\[[GetPrototypeOf]] as specified in [=[[GetPrototypeOf]] internal method of an Exported GC Object=]. @@ -1680,10 +1680,10 @@ dictionary ExceptionOptions { boolean traceStack = false; }; -[LegacyNamespace=WebAssembly, Exposed=(Window,Worker,Worklet)] +[LegacyNamespace=WebAssembly, Exposed=*] interface Exception { constructor(Tag exceptionTag, sequence<any> payload, optional ExceptionOptions options = {}); - any getArg([EnforceRange] unsigned long index); + any getArg(Tag exceptionTag, [EnforceRange] unsigned long index); boolean is(Tag exceptionTag); readonly attribute (DOMString or undefined) stack; }; @@ -1715,7 +1715,7 @@ To create an Exception object from a [=exception address=] |exnAddres 1. Let |map| be the [=surrounding agent=]'s associated [=Exception object cache=]. 1. If |map|[|exnAddress|] [=map/exists=], 1. Return |map|[|exnAddress|]. -1. Let |exn| be a [=new=] {{Exception}}. +1. Let |exn| be a [=/new=] {{Exception}}. 1. [=initialize an Exception object|Initialize=] |exn| from |exnAddress|. 1. Return |exn|. @@ -1740,7 +1740,7 @@ constructor steps are: 1. If |resultType| [=matches/valtype|matches=] [=v128=] or [=exnref=], 1. Throw a {{TypeError}}. 1. [=list/Append=] [=?=] [=ToWebAssemblyValue=](|value|, |resultType|) to |wasmPayload|. -1. Let (|store|, |exceptionAddr|) be [=exn_alloc=](|store|, |exceptionTag|.\[[Address]], |wasmPayload|) +1. Let (|store|, |exceptionAddr|) be [=exn_alloc=](|store|, |exceptionTag|.\[[Address]], |wasmPayload|). 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. 1. [=initialize an Exception object|Initialize=] **this** from |exceptionAddr|. 1. If |options|["traceStack"] is true, @@ -1751,9 +1751,11 @@ constructor steps are:
-The getArg(|index|) method steps are: +The getArg(|exceptionTag|, |index|) method steps are: 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. +1. If **this**.\[[Type]] is not equal to |exceptionTag|.\[[Address]], + 1. Throw a {{TypeError}}. 1. Let |tagaddr| be [=exn_tag=](|store|, **this**.\[[Address]]). 1. Let |payload| be [=exn_read=](|store|, **this**.\[[Address]]). 1. Assert: |tagaddr| is equal to **this**.\[[Type]]. @@ -1799,8 +1801,8 @@ To get the JavaScript exception tag, perform the following steps: 1. return the [=surrounding agent=]'s associated [=JavaScript exception tag=] 1. Let |store| be the [=surrounding agent=]'s [=associated store=]. 1. Let (|store|, |tagAddress|) be [=tag_alloc=](|store|, « [=externref=] » → « »). - 1. Set the current agent's [=associated store=] to |store|. - 1. Set the current agent's associated [=JavaScript exception tag=] to |tagAddress|. + 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. + 1. Set the [=surrounding agent=]'s associated [=JavaScript exception tag=] to |tagAddress|. 1. return |tagAddress|. @@ -1873,7 +1875,8 @@ To validate builtin set names with |builtinSetNames|, perform the fol To create a builtin function from type |funcType| and execution steps |steps|, perform the following steps: 1. Let |hostfunc| be a [=host function=] which executes |steps| when called. -1. Let (|store|, |funcaddr|) be [=func_alloc=](|store|, |functype|, |hostfunc|). +1. Let |store| be the [=surrounding agent=]'s [=associated store=]. +1. Let (|store|, |funcaddr|) be [=func_alloc=](|store|, |funcType|, |hostfunc|). 1. Set the [=surrounding agent=]'s [=associated store=] to |store|. 1. Return |funcaddr|. @@ -1884,9 +1887,9 @@ To create a builtin function from type |funcType| and execution steps To instantiate a builtin set with name |builtinSetName|, perform the following steps: 1. Let |builtins| be the result of [=get the builtins for a builtin set=] |builtinSetName|. -1. Let |exportsObject| be [=!=] [$OrdinaryObjectCreate$](null). +1. Let |exportsObject| be [$OrdinaryObjectCreate$](null). 1. [=list/iterate|For each=] (|name|, |funcType|, |steps|) of |builtins|, - 1. Let |funcaddr| be the result fo [=create a builtin function=] with |funcType| and |steps|. + 1. Let |funcaddr| be the result of [=create a builtin function=] with |funcType| and |steps|. 1. Let |func| be the result of creating [=a new Exported Function=] from |funcaddr|. 1. Let |value| be |func|. 1. Let |status| be [=!=] [$CreateDataProperty$](|exportsObject|, |name|, |value|). @@ -1903,7 +1906,7 @@ To validate an import for builtins with |import|, enabled builtins |b 1. Let |maybeBuiltin| be the result of [=find a builtin|finding a builtin=] for |import| and |builtinSetNames|. 1. If |maybeBuiltin| is null, return true. 1. Let |importExternType| be |import|[2]. -1. Let |builtinFuncType| be |maybeBuiltin|[0][1]. +1. Let |builtinFuncType| be |maybeBuiltin|[1][1]. 1. Let |builtinExternType| be `func |builtinFuncType|`. 1. Return [=match_externtype=](|builtinExternType|, |importExternType|). @@ -2018,7 +2021,7 @@ When this builtin is invoked with parameters |string|, |array|, and |start|, the 1. Let |i| be 0. 1. While |i| < |stringLength|: 1. Let |charCode| be [$CharCodeAt$](|string|, |i|). - 1. Set the element at index |start| + |i| in |array| to [=ToWebAssemblyValue=](|charCode|). + 1. Set the element at index |start| + |i| in |array| to [=ToWebAssemblyValue=](|charCode|, [=i32=]). 1. Set |i| to |i| + 1. 1. Return |stringLength|. @@ -2140,7 +2143,7 @@ When this builtin is invoked with parameters |first| and |second|, the following 1. Throw a {{RuntimeError}} exception as if a [=trap=] was executed. 1. If |second| is not null and |second| [=is not a String=], 1. Throw a {{RuntimeError}} exception as if a [=trap=] was executed. -1. If [=!=] [=IsStrictlyEqual=](|first|, |second|) is true, +1. If [=IsStrictlyEqual=](|first|, |second|) is true, 1. Return 1. 1. Return 0. @@ -2156,7 +2159,7 @@ When this builtin is invoked with parameters |first| and |second|, the following 1. Let |first| be [=?=] [$UnwrapString$](|first|). 1. Let |second| be [=?=] [$UnwrapString$](|second|). -1. If [=!=] [=IsStrictlyEqual=](|first|, |second|) is true, +1. If [=IsStrictlyEqual=](|first|, |second|) is true, 1. Return 0. 1. If [=!=] [=IsLessThan=](|first|, |second|, true) is true, 1. Return -1. diff --git a/document/legacy/exceptions/js-api/index.bs b/document/legacy/exceptions/js-api/index.bs index e7db14074..6eaf8dac8 100644 --- a/document/legacy/exceptions/js-api/index.bs +++ b/document/legacy/exceptions/js-api/index.bs @@ -1213,8 +1213,8 @@ The new Tag(|type|) constructor 1. Let |parameters| be |type|["parameters"]. 1. Let |wasmParameters| be «». -1. [=list/iterate|For each=] |type| of |parameters|, - 1. [=list/Append=] [=ToValueType=](|type|) to |wasmParameters|. +1. [=list/iterate|For each=] |paramType| of |parameters|, + 1. [=list/Append=] [=ToValueType=](|paramType|) to |wasmParameters|. 1. Let |store| be the current agent's [=associated store=]. 1. Let (|store|, |tagAddress|) be [=tag_alloc=](|store|, |wasmParameters|). 1. Set the current agent's [=associated store=] to |store|. diff --git a/document/versions/core/WebAssembly-3.0.pdf b/document/versions/core/WebAssembly-3.0.pdf new file mode 100644 index 000000000..afaee0b60 Binary files /dev/null and b/document/versions/core/WebAssembly-3.0.pdf differ diff --git a/document/web-api/index.bs b/document/web-api/index.bs index 09c0d975b..aa58250d5 100644 --- a/document/web-api/index.bs +++ b/document/web-api/index.bs @@ -9,6 +9,7 @@ TR: https://www.w3.org/TR/wasm-web-api-2/ ED: https://webassembly.github.io/spec/web-api/ Implementation Report: https://webassembly.org/features/ Editor: Ms2ger, w3cid 46309, Igalia +Editor: Ryan Hunt, w3cid 112030, Mozilla Foundation Repository: WebAssembly/spec Abstract: This document describes the integration of WebAssembly with the broader web platform. Markup Shorthands: css no, markdown yes @@ -40,7 +41,7 @@ Date: now
-urlPrefix: https://tc39.github.io/ecma262/; spec: ECMASCRIPT
+urlPrefix: https://tc39.es/ecma262/; spec: ECMASCRIPT
     type: exception; for: ECMAScript
         text: TypeError; url: sec-native-error-types-used-in-this-standard-typeerror
     type: interface
@@ -61,7 +62,6 @@ urlPrefix: https://webassembly.github.io/spec/js-api/; spec: WASMJS
         text: WebAssemblyInstantiatedSource; url: #dictdef-webassemblyinstantiatedsource
     type: dfn
         text: compile a WebAssembly module; url: #compile-a-webassembly-module
-        text: instantiate a WebAssembly module; url: #instantiate-a-webassembly-module
         text: instantiate; url: #dom-webassembly-instantiate
         text: asynchronously compile a webassembly module; url: #asynchronously-compile-a-webassembly-module
         text: instantiate a promise of a module; url: #instantiate-a-promise-of-a-module
diff --git a/interpreter/Makefile b/interpreter/Makefile
index de0f99cf1..94cdb5ded 100644
--- a/interpreter/Makefile
+++ b/interpreter/Makefile
@@ -14,6 +14,9 @@ LIB =		$(NAME)
 JSLIB =		wast.js
 ZIP =		$(NAME).zip
 
+DEPS =		dune menhir
+JSDEPS =	ocamlfind js_of_ocaml js_of_ocaml-ppx
+
 BUILDDIR =	_build/default
 
 JS =		# set to JS shell command to run JS tests, empty to skip
@@ -26,6 +29,7 @@ JS =		# set to JS shell command to run JS tests, empty to skip
 default:	$(NAME)
 all:		default alltest
 alltest:	unittest partest custompartest
+alldeps:	$(NAME)-deps $(JSLIB)-deps
 ci:		all jslib zip
 
 jslib:		$(JSLIB)
@@ -36,11 +40,17 @@ zip:		$(ZIP)
 
 .PHONY:		$(NAME) $(JSLIB)
 
+deps:
+	opam install --yes $(DEPS)
+
 $(NAME):
 	rm -f $@
 	dune build $@.exe
 	ln $(BUILDDIR)/$@.exe $@
 
+jsdeps:	deps
+	opam install --yes $(JSDEPS)
+
 $(JSLIB):
 	rm -f $@
 	dune build $(@:%.js=%.bc.js)
@@ -121,7 +131,7 @@ customquiettest/%:	$(NAME)
 		  $(TESTDIR)/run.py 2>$(@F).out --wasm `pwd`/$(NAME) --opts '$(CUSTOMOPTS)' $(if $(JS),--js '$(JS)',) $(CUSTOMTESTDIR)/$*.wast && \
 		  rm $(@F).out \
 		) || \
-		cat $(@F).out || rm $(@F).out || exit 1
+		(cat $(@F).out && rm $(@F).out && exit 1)
 
 
 # Packaging
diff --git a/interpreter/README.md b/interpreter/README.md
index cade09865..2ede808da 100644
--- a/interpreter/README.md
+++ b/interpreter/README.md
@@ -431,14 +431,14 @@ script: *
 
 cmd:
                                      ;; define, validate, and possibly instantiate module
-  
+                                   ;; instantiate module
   ( register  ? )              ;; register module instance for imports
                                      ;; perform action and print results
                                   ;; assert result of an action
                                        ;; meta command
 
 module:
-  ...
+  ...                                        ;; ordinary module syntax (see above)
   ( module ? binary * )        ;; module in binary format (may be malformed)
   ( module ? quote * )         ;; module quoted in text (may be malformed)
   ( module definition ? binary ... )   ;; uninstantiated module
@@ -453,7 +453,7 @@ action:
 const:
   ( .const  )                 ;; number value
   (   + )          ;; vector value
-  ( ref.null  )                    ;; null reference
+  ( ref.null  )                   ;; null reference
   ( ref.host  )                         ;; host reference
   ( ref.extern  )                       ;; external host reference
 
@@ -485,7 +485,7 @@ num_pat:
 meta:
   ( script ?