From 3291e4b5feb697835501cbab67cfe2bafe3bff57 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 24 Jun 2021 20:57:12 +0200 Subject: [PATCH 1/3] [spec] Fix a bunch of minor issues --- document/core/binary/types.rst | 4 ++-- document/core/text/instructions.rst | 6 +++--- document/core/util/macros.def | 2 +- document/core/valid/instructions.rst | 6 +++--- 4 files changed, 9 insertions(+), 9 deletions(-) diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index 7c462e029c..8a2bf7e156 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -6,8 +6,8 @@ Types ----- .. note:: - In future versions of WebAssembly, value types may include types denoted by :ref:`type indices `. - Thus, the binary format for types corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, so that they can coexist with (positive) type indices in the future. + In some places, possible types include both type constructors or types denoted by :ref:`type indices `. + Thus, the binary format for most type constructors corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, such that they can unambiguously occur in the same place as (positive) type indices. .. index:: number type diff --git a/document/core/text/instructions.rst b/document/core/text/instructions.rst index 45c2a05979..6112a76677 100644 --- a/document/core/text/instructions.rst +++ b/document/core/text/instructions.rst @@ -74,13 +74,13 @@ However, the special case of a type use that is syntactically empty or consists x,I'{:}\Ttypeuse_I &\Rightarrow& x & (\iff I' = \{\ILOCALS~(\epsilon)^\ast\}) \\ \end{array} \\ \production{block instruction} & \Tblockinstr_I &::=& - \text{block}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\X{in}{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid^? + \text{block}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype_I~~(\X{in}{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid^? \\ &&&\qquad \Rightarrow\quad \BLOCK~\X{bt}~\X{in}^\ast~\END \qquad\quad~~ (\iff \Tid^? = \epsilon \vee \Tid^? = \Tlabel) \\ &&|& - \text{loop}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\X{in}{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid^? + \text{loop}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype_I~~(\X{in}{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid^? \\ &&&\qquad \Rightarrow\quad \LOOP~\X{bt}~\X{in}^\ast~\END \qquad\qquad (\iff \Tid^? = \epsilon \vee \Tid^? = \Tlabel) \\ &&|& - \text{if}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype~~(\X{in}_1{:}\Tinstr_{I'})^\ast~~ + \text{if}~~I'{:}\Tlabel_I~~\X{bt}{:}\Tblocktype_I~~(\X{in}_1{:}\Tinstr_{I'})^\ast~~ \text{else}~~\Tid_1^?~~(\X{in}_2{:}\Tinstr_{I'})^\ast~~\text{end}~~\Tid_2^? \\ &&&\qquad \Rightarrow\quad \IF~\X{bt}~\X{in}_1^\ast~\ELSE~\X{in}_2^\ast~\END \qquad (\iff \Tid_1^? = \epsilon \vee \Tid_1^? = \Tlabel, \Tid_2^? = \epsilon \vee \Tid_2^? = \Tlabel) \\ diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 42b310ddcf..cd1bf31d6e 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -308,7 +308,7 @@ .. Modules, non-terminals .. |module| mathdef:: \xref{syntax/modules}{syntax-module}{\X{module}} -.. |type| mathdef:: \xref{syntax/modules}{syntax-typedef}{\X{type}} +.. |type| mathdef:: \xref{syntax/types}{syntax-functype}{\X{type}} .. |func| mathdef:: \xref{syntax/modules}{syntax-func}{\X{func}} .. |table| mathdef:: \xref{syntax/modules}{syntax-table}{\X{table}} .. |mem| mathdef:: \xref{syntax/modules}{syntax-mem}{\X{mem}} diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index f329a67799..07e4921b69 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -599,7 +599,7 @@ Memory Instructions * The memory :math:`C.\CMEMS[0]` must be defined in the context. -* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. +* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. * Then the instruction is valid with type :math:`[\I32] \to [t]`. @@ -639,7 +639,7 @@ Memory Instructions * The memory :math:`C.\CMEMS[0]` must be defined in the context. -* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. +* The alignment :math:`2^{\memarg.\ALIGN}` must not be larger than the :ref:`bit width ` of :math:`t` divided by :math:`8`. * Then the instruction is valid with type :math:`[\I32~t] \to []`. @@ -1124,7 +1124,7 @@ Expressions :math:`\expr` are classified by :ref:`result types ` with some :ref:`stack type ` :math:`[] \to [t'^\ast]`. +* The instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with some :ref:`stack type ` :math:`[] \to [{t'}^\ast]`. * For each :ref:`operand type ` :math:`t'_i` in :math:`{t'}^\ast` and corresponding :ref:`value type ` type :math:`t_i` in :math:`t^\ast`, :math:`t'_i` :ref:`matches ` :math:`t_i`. From 16a2131ae154f1f21f0b6bbf44e7a16d4808f1b6 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 28 Jun 2021 09:02:11 +0200 Subject: [PATCH 2/3] more numtype bit width --- document/core/binary/instructions.rst | 3 ++- document/core/binary/types.rst | 2 +- document/core/exec/instructions.rst | 4 ++-- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst index d6a60d83f8..26e0b8fc79 100644 --- a/document/core/binary/instructions.rst +++ b/document/core/binary/instructions.rst @@ -82,7 +82,8 @@ Reference Instructions :ref:`Reference instructions ` are represented by single byte codes. .. _binary-ref.null: -.. _binary-ref.isnull: +.. _binary-ref.func: +.. _binary-ref.is_null: .. math:: \begin{array}{llclll} diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst index 8a2bf7e156..0d1dfec86d 100644 --- a/document/core/binary/types.rst +++ b/document/core/binary/types.rst @@ -7,7 +7,7 @@ Types .. note:: In some places, possible types include both type constructors or types denoted by :ref:`type indices `. - Thus, the binary format for most type constructors corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, such that they can unambiguously occur in the same place as (positive) type indices. + Thus, the binary format for type constructors corresponds to the encodings of small negative :math:`\xref{binary/values}{binary-sint}{\sN}` values, such that they can unambiguously occur in the same place as (positive) type indices. .. index:: number type diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 6f4c7dc740..78c43da796 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -978,7 +978,7 @@ Memory Instructions 9. If :math:`N` is not part of the instruction, then: - a. Let :math:`N` be the :ref:`bit width ` :math:`|t|` of :ref:`value type ` :math:`t`. + a. Let :math:`N` be the :ref:`bit width ` :math:`|t|` of :ref:`number type ` :math:`t`. 10. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: @@ -1058,7 +1058,7 @@ Memory Instructions 11. If :math:`N` is not part of the instruction, then: - a. Let :math:`N` be the :ref:`bit width ` :math:`|t|` of :ref:`value type ` :math:`t`. + a. Let :math:`N` be the :ref:`bit width ` :math:`|t|` of :ref:`number type ` :math:`t`. 12. If :math:`\X{ea} + N/8` is larger than the length of :math:`\X{mem}.\MIDATA`, then: From 09af00fd85daf4bea7ea7004d0f335b70bb03d8b Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Mon, 28 Jun 2021 09:05:49 +0200 Subject: [PATCH 3/3] more numtypes --- document/core/syntax/instructions.rst | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/document/core/syntax/instructions.rst b/document/core/syntax/instructions.rst index 039d4cfb2f..9c582d64ca 100644 --- a/document/core/syntax/instructions.rst +++ b/document/core/syntax/instructions.rst @@ -35,7 +35,7 @@ The following sections group instructions into a number of different categories. Numeric Instructions ~~~~~~~~~~~~~~~~~~~~ -Numeric instructions provide basic operations over numeric :ref:`values ` of specific :ref:`type `. +Numeric instructions provide basic operations over numeric :ref:`values ` of specific :ref:`type `. These operations closely match respective operations available in hardware. .. math:: @@ -118,7 +118,7 @@ These operations closely match respective operations available in hardware. \K{ge} \\ \end{array} -Numeric instructions are divided by :ref:`value type `. +Numeric instructions are divided by :ref:`number type `. For each type, several subcategories can be distinguished: * *Constants*: return a static constant. @@ -324,9 +324,9 @@ Instructions in this group are concerned with linear :ref:`memory `. \DATADROP~\dataidx \\ \end{array} -Memory is accessed with |LOAD| and |STORE| instructions for the different :ref:`value types `. +Memory is accessed with |LOAD| and |STORE| instructions for the different :ref:`number types `. They all take a *memory immediate* |memarg| that contains an address *offset* and the expected *alignment* (expressed as the exponent of a power of 2). -Integer loads and stores can optionally specify a *storage size* that is smaller than the :ref:`bit width ` of the respective value type. +Integer loads and stores can optionally specify a *storage size* that is smaller than the :ref:`bit width ` of the respective value type. In the case of loads, a sign extension mode |sx| is then required to select appropriate behavior. The static address offset is added to the dynamic address operand, yielding a 33 bit *effective address* that is the zero-based index at which the memory is accessed. @@ -351,7 +351,7 @@ The |DATADROP| instruction prevents further use of a passive data segment. This This restriction may be lifted in future versions. -.. index:: ! control instruction, ! structured control, ! label, ! block, ! block type, ! branch, ! unwinding, result type, label index, function index, type index, vector, trap, function, table, function type, value type, type index +.. index:: ! control instruction, ! structured control, ! label, ! block, ! block type, ! branch, ! unwinding, stack type, label index, function index, type index, vector, trap, function, table, function type, value type, type index pair: abstract syntax; instruction pair: abstract syntax; block type pair: block; type