From 5c2ab5a3b5ac4f10d9a9d39e0c1e750fa830377f Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Fri, 16 Mar 2018 09:32:15 +0100 Subject: [PATCH 1/5] [spec] Address comments by Luke --- document/core/intro/introduction.rst | 2 +- document/core/syntax/types.rst | 4 +-- document/core/text/modules.rst | 30 ++++++++++++---- document/core/util/macros.def | 2 ++ document/core/valid/conventions.rst | 13 +++---- document/core/valid/instructions.rst | 12 +++---- document/core/valid/modules.rst | 52 ++++++++++++++++++---------- document/core/valid/types.rst | 2 +- 8 files changed, 73 insertions(+), 44 deletions(-) diff --git a/document/core/intro/introduction.rst b/document/core/intro/introduction.rst index 6c9b058974..4819dbdd76 100644 --- a/document/core/intro/introduction.rst +++ b/document/core/intro/introduction.rst @@ -5,7 +5,7 @@ WebAssembly (abbreviated Wasm [#wasm]_) is a *safe, portable, low-level code for designed for efficient execution and compact representation. Its main goal is to enable high performance applications on the Web, but it does not make any Web-specific assumptions or provide Web-specific features, so it can be employed in other environments as well. -WebAssembly is an open standard developed by a `W3C Community Group `_ that includes representatives of all major browser vendors. +WebAssembly is an open standard developed by a `W3C Community Group `_. This document describes version |release| of the :ref:`core ` WebAssembly standard. It is intended that it will be superseded by new incremental releases with additional features in the future. diff --git a/document/core/syntax/types.rst b/document/core/syntax/types.rst index 6898fb59ee..012eff4c33 100644 --- a/document/core/syntax/types.rst +++ b/document/core/syntax/types.rst @@ -49,7 +49,7 @@ Result Types ~~~~~~~~~~~~ *Result types* classify the result of :ref:`executing ` :ref:`instructions ` or :ref:`blocks `, -which is a sequence of values. +which is a sequence of values written with brackets. .. math:: \begin{array}{llll} @@ -71,7 +71,7 @@ Function Types ~~~~~~~~~~~~~~ *Function types* classify the signature of :ref:`functions `, -mapping a vector of parameters to a vector of results. +mapping a vector of parameters to a vector of results, written as follows. .. math:: \begin{array}{llll} diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst index d649bd2911..c52a3872c7 100644 --- a/document/core/text/modules.rst +++ b/document/core/text/modules.rst @@ -476,9 +476,8 @@ When omitted, :math:`\T{0}` is assumed. .. math:: \begin{array}{llclll} \production{element segment} & \Telem_I &::=& - \text{(}~\text{elem}~~(x{:}\Ttableidx_I)^?~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~y^\ast{:}\Tvec(\Tfuncidx_I)~\text{)} \\ &&& \qquad - \Rightarrow\quad \{ \ETABLE~x', \EOFFSET~e, \EINIT~y^\ast \} \\ - &&& \qquad\qquad\qquad (\iff x' = x^? \neq \epsilon \vee x' = 0) \\ + \text{(}~\text{elem}~~x{:}\Ttableidx_I~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~y^\ast{:}\Tvec(\Tfuncidx_I)~\text{)} \\ &&& \qquad + \Rightarrow\quad \{ \ETABLE~x, \EOFFSET~e, \EINIT~y^\ast \} \\ \end{array} .. note:: @@ -498,6 +497,16 @@ As an abbreviation, a single instruction may occur in place of the offset: \text{(}~\text{offset}~~\Tinstr~\text{)} \end{array} +Also, the table index can be omitted, defaulting to :math:`0`. + +.. math:: + \begin{array}{llclll} + \production{element segment} & + \text{(}~\text{elem}~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)} + &\equiv& + \text{(}~\text{elem}~~0~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)} + \end{array} + As another abbreviation, element segments may also be specified inline with :ref:`table ` definitions; see the respective section. @@ -518,9 +527,8 @@ The data is written as a :ref:`string `, which may be split up into .. math:: \begin{array}{llclll} \production{data segment} & \Tdata_I &::=& - \text{(}~\text{data}~~(x{:}\Tmemidx_I)^?~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~b^\ast{:}\Tdatastring~\text{)} \\ &&& \qquad - \Rightarrow\quad \{ \DMEM~x', \DOFFSET~e, \DINIT~b^\ast \} \\ - &&& \qquad\qquad\qquad (\iff x' = x^? \neq \epsilon \vee x' = 0) \\[1ex] + \text{(}~\text{data}~~x{:}\Tmemidx_I~~\text{(}~\text{offset}~~e{:}\Texpr_I~\text{)}~~b^\ast{:}\Tdatastring~\text{)} \\ &&& \qquad + \Rightarrow\quad \{ \DMEM~x', \DOFFSET~e, \DINIT~b^\ast \} \\[1ex] \production{data string} & \Tdatastring &::=& (b^\ast{:}\Tstring)^\ast \quad\Rightarrow\quad \concat((b^\ast)^\ast) \\ \end{array} @@ -542,6 +550,16 @@ As an abbreviation, a single instruction may occur in place of the offset: \text{(}~\text{offset}~~\Tinstr~\text{)} \end{array} +Also, the memory index can be omitted, defaulting to :math:`0`. + +.. math:: + \begin{array}{llclll} + \production{data segment} & + \text{(}~\text{data}~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)} + &\equiv& + \text{(}~\text{data}~~0~~\text{(}~\text{offset}~~\Texpr_I~\text{)}~~\dots~\text{)} + \end{array} + As another abbreviation, data segments may also be specified inline with :ref:`memory ` definitions; see the respective section. diff --git a/document/core/util/macros.def b/document/core/util/macros.def index 2216694b13..cf372d341a 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -717,6 +717,8 @@ .. |CLABELS| mathdef:: \xref{valid/conventions}{context}{\K{labels}} .. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}} +.. |NORETURN| mathdef:: \xref{valid/conventions}{context}{\K{noreturn}} + .. Judgments diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 5ed7789a7c..c61e93b6e9 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -40,14 +40,14 @@ which collects relevant information about the surrounding :ref:`module ` for each :ref:`index space `, describing each defined entry in that space. Locals, labels and return type are only used for validating :ref:`instructions ` in :ref:`function bodies `, and are left empty elsewhere. The label stack is the only part of the context that changes as validation of an instruction sequence proceeds. -It is convenient to define contexts as :ref:`records ` :math:`C` with abstract syntax: +More concretely, contexts are defined as :ref:`records ` :math:`C` with abstract syntax: .. math:: \begin{array}{llll} @@ -60,17 +60,14 @@ It is convenient to define contexts as :ref:`records ` :math:`C & \CGLOBALS & \globaltype^\ast, \\ & \CLOCALS & \valtype^\ast, \\ & \CLABELS & \resulttype^\ast, \\ - & \CRETURN & \resulttype^? ~\} \\ + & \CRETURN & (\resulttype ~|~ \NORETURN) ~\} \\ \end{array} \end{array} -.. note:: - The fields of a context are not defined as :ref:`vectors `, - since their lengths are not bounded by the maximum vector size. - -In addition to field access :math:`C.\K{field}` the following notation is adopted for manipulating contexts: +In addition to field access written :math:`C.\K{field}` the following notation is adopted for manipulating contexts: * When spelling out a context, empty fields are omitted. + Likewise, the |CRETURN| field may be omitted when it is |NORETURN|. * :math:`C,\K{field}\,A^\ast` denotes the same context as :math:`C` but with the elements :math:`A^\ast` prepended to its :math:`\K{field}` component sequence. diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index ffc308ff29..77e5fddd49 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -314,7 +314,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:`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]`. @@ -354,7 +354,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:`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 []`. @@ -616,7 +616,7 @@ Control Instructions :math:`\RETURN` ............... -* The return type :math:`C.\CRETURN` must not be empty in the context. +* The return type :math:`C.\CRETURN` must not be |NORETURN| in the context. * Let :math:`[t^?]` be the :ref:`result type ` of :math:`C.\CRETURN`. @@ -632,9 +632,7 @@ Control Instructions .. note:: The |RETURN| instruction is :ref:`stack-polymorphic `. - :math:`C.\CRETURN` is empty (:math:`\epsilon`) when validating an :ref:`expression ` that is not a function body. - This differs from it being set to the empty result type (:math:`[]`), - which is the case for functions not returning anything. + :math:`C.\CRETURN` is |NORETURN| when validating an :ref:`expression ` that is not a function body. .. _valid-call: @@ -773,7 +771,7 @@ Constant Expressions \frac{ (C \vdashinstrconst \instr \const)^\ast }{ - C \vdashexprconst \instr~\END \const + C \vdashexprconst \instr^\ast~\END \const } .. math:: diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 6dc45a687b..6130cab2c7 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -334,6 +334,9 @@ Exports :math:`\export` and export descriptions :math:`\exportdesc` are classifi C \vdashexportdesc \EDGLOBAL~x : \ETGLOBAL~(\MCONST~t) } +.. note:: + In future versions of WebAssembly, the restriction to exporting only immutable globals may be removed. + .. index:: import, name, function type, table type, memory type, global type pair: validation; import @@ -425,6 +428,9 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi C \vdashimportdesc \IDGLOBAL~\MCONST~t : \ETGLOBAL~\MCONST~t } +.. note:: + In future versions of WebAssembly, the restriction to importing only immutable globals may be removed. + .. index:: module, type definition, function type, function, table, memory, global, element, data, start function, import, export, context pair: validation; module @@ -447,25 +453,25 @@ Instead, the context :math:`C` for validation of the module's content is constru * :math:`C.\CTYPES` is :math:`\module.\MTYPES`, - * :math:`C.\CFUNCS` is :math:`\etfuncs(\externtype_i^\ast)` concatenated with :math:`\functype_i^\ast`, - with the type sequences :math:`\externtype_i^\ast` and :math:`\functype_i^\ast` as determined below, + * :math:`C.\CFUNCS` is :math:`\etfuncs(\X{it}^\ast)` concatenated with :math:`\X{ft}^\ast`, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`function types ` :math:`\X{ft}^\ast` as determined below, - * :math:`C.\CTABLES` is :math:`\ettables(\externtype_i^\ast)` concatenated with :math:`\tabletype_i^\ast`, - with the type sequences :math:`\externtype_i^\ast` and :math:`\tabletype_i^\ast` as determined below, + * :math:`C.\CTABLES` is :math:`\ettables(\X{it}^\ast)` concatenated with :math:`\X{tt}^\ast`, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`table types ` :math:`\X{tt}^\ast` as determined below, - * :math:`C.\CMEMS` is :math:`\etmems(\externtype_i^\ast)` concatenated with :math:`\memtype_i^\ast`, - with the type sequences :math:`\externtype_i^\ast` and :math:`\memtype_i^\ast` as determined below, + * :math:`C.\CMEMS` is :math:`\etmems(\X{it}^\ast)` concatenated with :math:`\X{mt}^\ast`, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`memory types ` :math:`\X{mt}^\ast` as determined below, - * :math:`C.\CGLOBALS` is :math:`\etglobals(\externtype_i^\ast)` concatenated with :math:`\globaltype_i^\ast`, - with the type sequences :math:`\externtype_i^\ast` and :math:`\globaltype_i^\ast` as determined below. + * :math:`C.\CGLOBALS` is :math:`\etglobals(\X{it}^\ast)` concatenated with :math:`\X{gt}^\ast`, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`global types ` :math:`\X{gt}^\ast` as determined below, * :math:`C.\CLOCALS` is empty, - * :math:`C.\CLABELS` is empty. + * :math:`C.\CLABELS` is empty, - * :math:`C.\CRETURN` is empty. + * :math:`C.\CRETURN` is |NORETURN|. -* Let :math:`C'` be the :ref:`context ` where :math:`C'.\CGLOBALS` is the sequence :math:`\etglobals(\externtype_i^\ast)` and all other fields are empty. +* Let :math:`C'` be the :ref:`context ` where :math:`C'.\CGLOBALS` is the sequence :math:`\etglobals(\externtype_i^\ast)`, :math:`C.\CRETURN` is |NORETURN| and all other fields are empty. * Under the context :math:`C`: @@ -476,15 +482,15 @@ Instead, the context :math:`C` for validation of the module's content is constru the definition :math:`\func_i` must be :ref:`valid ` with a :ref:`function type ` :math:`\X{ft}_i`. * For each :math:`\table_i` in :math:`\module.\MTABLES`, - the definition :math:`\table_i` must be :ref:`valid ` with a :ref:`table type ` :math:`\tabletype_i`. + the definition :math:`\table_i` must be :ref:`valid ` with a :ref:`table type ` :math:`\X{tt}_i`. * For each :math:`\mem_i` in :math:`\module.\MMEMS`, - the definition :math:`\mem_i` must be :ref:`valid ` with a :ref:`memory type ` :math:`\memtype_i`. + the definition :math:`\mem_i` must be :ref:`valid ` with a :ref:`memory type ` :math:`\X{mt}_i`. * For each :math:`\global_i` in :math:`\module.\MGLOBALS`: * Under the context :math:`C'`, - the definition :math:`\global_i` must be :ref:`valid ` with a :ref:`global type ` :math:`\globaltype_i`. + the definition :math:`\global_i` must be :ref:`valid ` with a :ref:`global type ` :math:`\X{gt}_i`. * For each :math:`\elem_i` in :math:`\module.\MELEM`, the segment :math:`\elem_i` must be :ref:`valid `. @@ -496,10 +502,10 @@ Instead, the context :math:`C` for validation of the module's content is constru then :math:`\module.\MSTART` must be :ref:`valid `. * For each :math:`\import_i` in :math:`\module.\MIMPORTS`, - the segment :math:`\import_i` must be :ref:`valid ` with an :ref:`external type ` :math:`\externtype_i`. + the segment :math:`\import_i` must be :ref:`valid ` with an :ref:`external type ` :math:`\X{it}_i`. * For each :math:`\export_i` in :math:`\module.\MEXPORTS`, - the segment :math:`\import_i` must be :ref:`valid ` with :ref:`external type ` :math:`\externtype'_i`. + the segment :math:`\import_i` must be :ref:`valid ` with :ref:`external type ` :math:`\X{et}_i`. * The length of :math:`C.\CTABLES` must not be larger than :math:`1`. @@ -507,11 +513,19 @@ Instead, the context :math:`C` for validation of the module's content is constru * All export names :math:`\export_i.\ENAME` must be different. -* Let :math:`\externtype^\ast` be the concatenation of :ref:`external types ` :math:`\externtype_i` of the imports, in index order. +* Let :math:`\X{ft}^\ast` be the concatenation of the internal :ref:`function types ` :math:`\X{ft}_i`, in index order. + +* Let :math:`\X{tt}^\ast` be the concatenation of the internal :ref:`table types ` :math:`\X{tt}_i`, in index order. + +* Let :math:`\X{mt}^\ast` be the concatenation of the internal :ref:`memory types ` :math:`\X{mt}_i`, in index order. + +* Let :math:`\X{gt}^\ast` be the concatenation of the internal :ref:`global types ` :math:`\X{gt}_i`, in index order. + +* Let :math:`\X{it}^\ast` be the concatenation of :ref:`external types ` :math:`\X{it}_i` of the imports, in index order. -* Let :math:`{\externtype'}^\ast` be the concatenation of :ref:`external types ` :math:`\externtype'_i` of the exports, in index order. +* Let :math:`\X{et}^\ast` be the concatenation of :ref:`external types ` :math:`\X{et}_i` of the exports, in index order. -* Then the module is valid with :ref:`external types ` :math:`\externtype^\ast \to {\externtype'}^\ast`. +* Then the module is valid with :ref:`external types ` :math:`\X{it}^\ast \to \X{et}^\ast`. .. math:: \frac{ diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index 76c6c70211..89b79a4187 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -54,7 +54,7 @@ Function Types } .. note:: - This restriction may be removed in future versions of WebAssembly. + The restriction to at most one result may be removed in future versions of WebAssembly. .. index:: table type, element type, limits From c05f73cc6711af698d2874a892cf5106d8fde7da Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Sat, 24 Mar 2018 08:47:10 +0100 Subject: [PATCH 2/5] Context extension notation --- document/core/valid/conventions.rst | 8 +++----- document/core/valid/instructions.rst | 11 +++++++---- document/core/valid/modules.rst | 10 +++++----- 3 files changed, 15 insertions(+), 14 deletions(-) diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index c61e93b6e9..d8175a8c33 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -69,14 +69,12 @@ In addition to field access written :math:`C.\K{field}` the following notation i * When spelling out a context, empty fields are omitted. Likewise, the |CRETURN| field may be omitted when it is |NORETURN|. -* :math:`C,\K{field}\,A^\ast` denotes the same context as :math:`C` but with the elements :math:`A^\ast` prepended to its :math:`\K{field}` component sequence. +* The notation :math:`\K{field}\,A^\ast, C` denotes the same context as :math:`C` but with the elements :math:`A^\ast` prepended to its :math:`\K{field}` component sequence. .. note:: - This notation is defined to *prepend* not *append*. - It is only used in situations where the original :math:`C.\K{field}` is either empty + The notation for context extension is only used in situations where the original :math:`C.\K{field}` is either empty or :math:`\K{field}` is :math:`\K{labels}`. - In the latter case adding to the front is desired - because the :ref:`label index ` space is indexed relatively, that is, in reverse order of addition. + It is reversed from usual conventions because it *prepends* not *appends*, in accordance with the use of relative indexing to look up a label in the context's label list. .. _valid-notation-textual: diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 77e5fddd49..f36988e9a2 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -477,7 +477,7 @@ Control Instructions .. math:: \frac{ - C,\CLABELS\,[t^?] \vdashinstrseq \instr^\ast : [] \to [t^?] + \CLABELS\,[t^?], C \vdashinstrseq \instr^\ast : [] \to [t^?] }{ C \vdashinstr \BLOCK~[t^?]~\instr^\ast~\END : [] \to [t^?] } @@ -501,7 +501,7 @@ Control Instructions .. math:: \frac{ - C,\CLABELS\,[] \vdashinstrseq \instr^\ast : [] \to [t^?] + \CLABELS\,[], C \vdashinstrseq \instr^\ast : [] \to [t^?] }{ C \vdashinstr \LOOP~[t^?]~\instr^\ast~\END : [] \to [t^?] } @@ -528,9 +528,9 @@ Control Instructions .. math:: \frac{ - C,\CLABELS\,[t^?] \vdashinstrseq \instr_1^\ast : [] \to [t^?] + \CLABELS\,[t^?], C \vdashinstrseq \instr_1^\ast : [] \to [t^?] \qquad - C,\CLABELS\,[t^?] \vdashinstrseq \instr_2^\ast : [] \to [t^?] + \CLABELS\,[t^?], C \vdashinstrseq \instr_2^\ast : [] \to [t^?] }{ C \vdashinstr \IF~[t^?]~\instr_1^\ast~\ELSE~\instr_2^\ast~\END : [\I32] \to [t^?] } @@ -787,4 +787,7 @@ Constant Expressions } .. note:: + Currently, constant expressions occurring as initializers of :ref:`globals ` are further constrained in that contained |GETGLOBAL| instructions are only allowed to refer to *imported* globals. + This is enforced in the :ref:`validation rule for modules ` by constraining the context :math:`C` accordingly. + The definition of constant expression may be extended in future versions of WebAssembly. diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 6130cab2c7..329eb320fb 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -42,7 +42,7 @@ Functions :math:`\func` are classified by :ref:`function types \frac{ C.\CTYPES[x] = [t_1^\ast] \to [t_2^?] \qquad - C,\CLOCALS\,t_1^\ast~t^\ast,\CLABELS~[t_2^?],\CRETURN~[t_2^?] \vdashexpr \expr : [t_2^?] + \CLOCALS\,t_1^\ast~t^\ast,\CLABELS~[t_2^?],\CRETURN~[t_2^?], C \vdashexpr \expr : [t_2^?] }{ C \vdashfunc \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \} : [t_1^\ast] \to [t_2^?] } @@ -454,16 +454,16 @@ Instead, the context :math:`C` for validation of the module's content is constru * :math:`C.\CTYPES` is :math:`\module.\MTYPES`, * :math:`C.\CFUNCS` is :math:`\etfuncs(\X{it}^\ast)` concatenated with :math:`\X{ft}^\ast`, - with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`function types ` :math:`\X{ft}^\ast` as determined below, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`function types ` :math:`\X{ft}^\ast` as determined below, * :math:`C.\CTABLES` is :math:`\ettables(\X{it}^\ast)` concatenated with :math:`\X{tt}^\ast`, - with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`table types ` :math:`\X{tt}^\ast` as determined below, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`table types ` :math:`\X{tt}^\ast` as determined below, * :math:`C.\CMEMS` is :math:`\etmems(\X{it}^\ast)` concatenated with :math:`\X{mt}^\ast`, - with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`memory types ` :math:`\X{mt}^\ast` as determined below, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`memory types ` :math:`\X{mt}^\ast` as determined below, * :math:`C.\CGLOBALS` is :math:`\etglobals(\X{it}^\ast)` concatenated with :math:`\X{gt}^\ast`, - with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`global types ` :math:`\X{gt}^\ast` as determined below, + with the import's :ref:`external types ` :math:`\X{it}^\ast` and the internal :math:`global types ` :math:`\X{gt}^\ast` as determined below, * :math:`C.\CLOCALS` is empty, From baf92f5e31f33b4caafc083effae5583721443ef Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Sat, 24 Mar 2018 08:58:43 +0100 Subject: [PATCH 3/5] Drop noreturn --- document/core/util/macros.def | 2 -- document/core/valid/conventions.rst | 5 ++--- document/core/valid/instructions.rst | 6 ++++-- document/core/valid/modules.rst | 4 ++-- 4 files changed, 8 insertions(+), 9 deletions(-) diff --git a/document/core/util/macros.def b/document/core/util/macros.def index cf372d341a..2216694b13 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -717,8 +717,6 @@ .. |CLABELS| mathdef:: \xref{valid/conventions}{context}{\K{labels}} .. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}} -.. |NORETURN| mathdef:: \xref{valid/conventions}{context}{\K{noreturn}} - .. Judgments diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index d8175a8c33..5f1d455d4a 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -40,7 +40,7 @@ which collects relevant information about the surrounding :ref:`module ` for each :ref:`index space `, describing each defined entry in that space. @@ -60,14 +60,13 @@ More concretely, contexts are defined as :ref:`records ` :math: & \CGLOBALS & \globaltype^\ast, \\ & \CLOCALS & \valtype^\ast, \\ & \CLABELS & \resulttype^\ast, \\ - & \CRETURN & (\resulttype ~|~ \NORETURN) ~\} \\ + & \CRETURN & \resulttype^? ~\} \\ \end{array} \end{array} In addition to field access written :math:`C.\K{field}` the following notation is adopted for manipulating contexts: * When spelling out a context, empty fields are omitted. - Likewise, the |CRETURN| field may be omitted when it is |NORETURN|. * The notation :math:`\K{field}\,A^\ast, C` denotes the same context as :math:`C` but with the elements :math:`A^\ast` prepended to its :math:`\K{field}` component sequence. diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index f36988e9a2..cd4127cb28 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -616,7 +616,7 @@ Control Instructions :math:`\RETURN` ............... -* The return type :math:`C.\CRETURN` must not be |NORETURN| in the context. +* The return type :math:`C.\CRETURN` must not be absent in the context. * Let :math:`[t^?]` be the :ref:`result type ` of :math:`C.\CRETURN`. @@ -632,7 +632,9 @@ Control Instructions .. note:: The |RETURN| instruction is :ref:`stack-polymorphic `. - :math:`C.\CRETURN` is |NORETURN| when validating an :ref:`expression ` that is not a function body. + :math:`C.\CRETURN` is absent (set to :math:`\epsilon`) when validating an :ref:`expression ` that is not a function body. + This differs from it being set to the empty result type (:math:`[\epsilon]`), + which is the case for functions not returning anything. .. _valid-call: diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 329eb320fb..b54d6560c6 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -469,9 +469,9 @@ Instead, the context :math:`C` for validation of the module's content is constru * :math:`C.\CLABELS` is empty, - * :math:`C.\CRETURN` is |NORETURN|. + * :math:`C.\CRETURN` is empty. -* Let :math:`C'` be the :ref:`context ` where :math:`C'.\CGLOBALS` is the sequence :math:`\etglobals(\externtype_i^\ast)`, :math:`C.\CRETURN` is |NORETURN| and all other fields are empty. +* Let :math:`C'` be the :ref:`context ` where :math:`C'.\CGLOBALS` is the sequence :math:`\etglobals(\externtype_i^\ast)` and all other fields are empty. * Under the context :math:`C`: From 6299fc3c74ed1a6f52c0aba35373a0100886d9cb Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Tue, 3 Apr 2018 15:42:27 +0200 Subject: [PATCH 4/5] eps --- document/core/valid/modules.rst | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index b54d6560c6..79d5530572 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -129,7 +129,7 @@ Globals :math:`\global` are classified by :ref:`global types \qquad C \vdashexpr \expr : [t] \qquad - C \vdashexprconst \expr ~\F{const} + C \vdashexprconst \expr \const }{ C \vdashglobal \{ \GTYPE~\mut~t, \GINIT~\expr \} : \mut~t } @@ -172,7 +172,7 @@ Element segments :math:`\elem` are not classified by a type. \qquad C \vdashexpr \expr : [\I32] \qquad - C \vdashexprconst \expr ~\F{const} + C \vdashexprconst \expr \const \qquad (C.\CFUNCS[y] = \functype)^\ast }{ @@ -210,7 +210,7 @@ Data segments :math:`\data` are not classified by any type. \qquad C \vdashexpr \expr : [\I32] \qquad - C \vdashexprconst \expr ~\F{const} + C \vdashexprconst \expr \const }{ C \vdashdata \{ \DMEM~x, \DOFFSET~\expr, \DINIT~b^\ast \} \ok } From c90608ffc6e2d0853697a0774ddf636f1a415d20 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 4 Apr 2018 08:24:15 +0200 Subject: [PATCH 5/5] Revert context extension notation --- document/core/syntax/conventions.rst | 4 ++++ document/core/valid/conventions.rst | 10 ++++++---- document/core/valid/instructions.rst | 21 +++++++++++++++++---- document/core/valid/modules.rst | 2 +- 4 files changed, 28 insertions(+), 9 deletions(-) diff --git a/document/core/syntax/conventions.rst b/document/core/syntax/conventions.rst index bb1fba797c..a1aec4214f 100644 --- a/document/core/syntax/conventions.rst +++ b/document/core/syntax/conventions.rst @@ -41,9 +41,13 @@ The following conventions are adopted in defining grammar rules for abstract syn +.. _notation-epsilon: +.. _notation-length: +.. _notation-index: .. _notation-slice: .. _notation-replace: .. _notation-record: +.. _notation-project: .. _notation-concat: .. _notation-compose: diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 5f1d455d4a..9e5f6f182b 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -64,16 +64,18 @@ More concretely, contexts are defined as :ref:`records ` :math: \end{array} \end{array} +.. _notation-extend: + In addition to field access written :math:`C.\K{field}` the following notation is adopted for manipulating contexts: * When spelling out a context, empty fields are omitted. -* The notation :math:`\K{field}\,A^\ast, C` denotes the same context as :math:`C` but with the elements :math:`A^\ast` prepended to its :math:`\K{field}` component sequence. +* :math:`C,\K{field}\,A^\ast` denotes the same context as :math:`C` but with the elements :math:`A^\ast` prepended to its :math:`\K{field}` component sequence. .. note:: - The notation for context extension is only used in situations where the original :math:`C.\K{field}` is either empty - or :math:`\K{field}` is :math:`\K{labels}`. - It is reversed from usual conventions because it *prepends* not *appends*, in accordance with the use of relative indexing to look up a label in the context's label list. + We use :ref:`indexing notation ` like :math:`C.\CLABELS[i]` to look up indices in their respective :ref:`index space ` in the context. + Context extension notation :math:`C,\K{field}\,A` is primarily used to locally extend *relative* index spaces, such as :ref:`label indices `. + Accordingly, the notation is defined to append at the *front* of the respective sequence, introducing a new relative index :math:`0` and shifting the existing ones. .. _valid-notation-textual: diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index cd4127cb28..a6e3845cd0 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -477,12 +477,14 @@ Control Instructions .. math:: \frac{ - \CLABELS\,[t^?], C \vdashinstrseq \instr^\ast : [] \to [t^?] + C,\CLABELS\,[t^?] \vdashinstrseq \instr^\ast : [] \to [t^?] }{ C \vdashinstr \BLOCK~[t^?]~\instr^\ast~\END : [] \to [t^?] } .. note:: + The :ref:`notation ` :math:`C,\CLABELS\,[t^?]` inserts the new label type at index :math:`0`, shifting all others. + The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the block was entered. This may be generalized in future versions of WebAssembly. @@ -501,12 +503,14 @@ Control Instructions .. math:: \frac{ - \CLABELS\,[], C \vdashinstrseq \instr^\ast : [] \to [t^?] + C,\CLABELS\,[] \vdashinstrseq \instr^\ast : [] \to [t^?] }{ C \vdashinstr \LOOP~[t^?]~\instr^\ast~\END : [] \to [t^?] } .. note:: + The :ref:`notation ` :math:`C,\CLABELS\,[t^?]` inserts the new label type at index :math:`0`, shifting all others. + The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the loop was entered. This may be generalized in future versions of WebAssembly. @@ -528,14 +532,16 @@ Control Instructions .. math:: \frac{ - \CLABELS\,[t^?], C \vdashinstrseq \instr_1^\ast : [] \to [t^?] + C,\CLABELS\,[t^?] \vdashinstrseq \instr_1^\ast : [] \to [t^?] \qquad - \CLABELS\,[t^?], C \vdashinstrseq \instr_2^\ast : [] \to [t^?] + C,\CLABELS\,[t^?] \vdashinstrseq \instr_2^\ast : [] \to [t^?] }{ C \vdashinstr \IF~[t^?]~\instr_1^\ast~\ELSE~\instr_2^\ast~\END : [\I32] \to [t^?] } .. note:: + The :ref:`notation ` :math:`C,\CLABELS\,[t^?]` inserts the new label type at index :math:`0`, shifting all others. + The fact that the nested instruction sequence :math:`\instr^\ast` must have type :math:`[] \to [t^?]` implies that it cannot access operands that have been pushed on the stack before the conditional was entered. This may be generalized in future versions of WebAssembly. @@ -559,6 +565,8 @@ Control Instructions } .. note:: + The :ref:`label index ` space in the :ref:`context ` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected. + The |BR| instruction is :ref:`stack-polymorphic `. @@ -580,6 +588,9 @@ Control Instructions C \vdashinstr \BRIF~l : [t^?~\I32] \to [t^?] } +.. note:: + The :ref:`label index ` space in the :ref:`context ` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l]` performs a relative lookup as expected. + .. _valid-br_table: @@ -608,6 +619,8 @@ Control Instructions } .. note:: + The :ref:`label index ` space in the :ref:`context ` :math:`C` contains the most recent label first, so that :math:`C.\CLABELS[l_i]` performs a relative lookup as expected. + The |BRTABLE| instruction is :ref:`stack-polymorphic `. diff --git a/document/core/valid/modules.rst b/document/core/valid/modules.rst index 79d5530572..78e99e77ea 100644 --- a/document/core/valid/modules.rst +++ b/document/core/valid/modules.rst @@ -42,7 +42,7 @@ Functions :math:`\func` are classified by :ref:`function types \frac{ C.\CTYPES[x] = [t_1^\ast] \to [t_2^?] \qquad - \CLOCALS\,t_1^\ast~t^\ast,\CLABELS~[t_2^?],\CRETURN~[t_2^?], C \vdashexpr \expr : [t_2^?] + C,\CLOCALS\,t_1^\ast~t^\ast,\CLABELS~[t_2^?],\CRETURN~[t_2^?] \vdashexpr \expr : [t_2^?] }{ C \vdashfunc \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \} : [t_1^\ast] \to [t_2^?] }