From aa9db85df9c30f9cca1940fd62bf52b761a01ea7 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Wed, 26 Apr 2017 16:08:35 +0200 Subject: [PATCH 1/8] [spec] Execution: conventions, runtime, instructions --- document/binary/instructions.rst | 32 ++--- document/binary/modules.rst | 77 +++++------ document/binary/types.rst | 18 +-- document/binary/values.rst | 22 ++-- document/execution/index.rst | 4 +- document/index.rst | 2 - document/instantiation/index.rst | 8 -- document/math.def | 161 ++++++++++++++++------- document/syntax/conventions.rst | 22 ++++ document/syntax/instructions.rst | 187 +++++++++++++++++---------- document/syntax/modules.rst | 52 +++++--- document/syntax/types.rst | 52 ++------ document/syntax/values.rst | 25 ++-- document/validation/conventions.rst | 44 ++++--- document/validation/instructions.rst | 94 +++----------- document/validation/modules.rst | 26 ++-- 16 files changed, 450 insertions(+), 376 deletions(-) delete mode 100644 document/instantiation/index.rst diff --git a/document/binary/instructions.rst b/document/binary/instructions.rst index 945b391e8b..fb64b6634c 100644 --- a/document/binary/instructions.rst +++ b/document/binary/instructions.rst @@ -37,7 +37,7 @@ Control Instructions .. math:: \begin{array}{llclll} - \production{instructions} & \Binstr &::=& + \production{instruction} & \Binstr &::=& \hex{00} &\Rightarrow& \UNREACHABLE \\ &&|& \hex{01} &\Rightarrow& \NOP \\ &&|& \hex{02}~~\X{rt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B} @@ -77,7 +77,7 @@ Parametric Instructions .. math:: \begin{array}{llclll} - \production{instructions} & \Binstr &::=& \dots \\ &&|& + \production{instruction} & \Binstr &::=& \dots \\ &&|& \hex{1A} &\Rightarrow& \DROP \\ &&|& \hex{1B} &\Rightarrow& \SELECT \\ \end{array} @@ -101,7 +101,7 @@ Variable Instructions .. math:: \begin{array}{llclll} - \production{instructions} & \Binstr &::=& \dots \\ &&|& + \production{instruction} & \Binstr &::=& \dots \\ &&|& \hex{20}~~x{:}\Blocalidx &\Rightarrow& \GETLOCAL~x \\ &&|& \hex{21}~~x{:}\Blocalidx &\Rightarrow& \SETLOCAL~x \\ &&|& \hex{22}~~x{:}\Blocalidx &\Rightarrow& \TEELOCAL~x \\ &&|& @@ -131,9 +131,9 @@ Each variant of :ref:`memory instruction ` is encoded with .. math:: \begin{array}{llclll} - \production{memory arguments} & \Bmemarg &::=& + \production{memory argument} & \Bmemarg &::=& a{:}\Bu32~~o{:}\Bu32 &\Rightarrow& \{ \ALIGN~a,~\OFFSET~o \} \\ - \production{instructions} & \Binstr &::=& \dots \\ &&|& + \production{instruction} & \Binstr &::=& \dots \\ &&|& \hex{28}~~m{:}\Bmemarg &\Rightarrow& \I32.\LOAD~m \\ &&|& \hex{29}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD~m \\ &&|& \hex{2A}~~m{:}\Bmemarg &\Rightarrow& \F32.\LOAD~m \\ &&|& @@ -181,7 +181,7 @@ The |CONST| instructions are followed by the respective literal. .. math:: \begin{array}{llclll} - \production{instructions} & \Binstr &::=& \dots \\&&|& + \production{instruction} & \Binstr &::=& \dots \\&&|& \hex{41}~~n{:}\Bi32 &\Rightarrow& \I32.\CONST~n \\ &&|& \hex{42}~~n{:}\Bi64 &\Rightarrow& \I64.\CONST~n \\ &&|& \hex{43}~~z{:}\Bf32 &\Rightarrow& \F32.\CONST~z \\ &&|& @@ -195,7 +195,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \production{instructions} & \Binstr &::=& \dots && \phantom{thisshouldbeenough} \\&&|& + \production{instruction} & \Binstr &::=& \dots && \phantom{thisshouldbeenough} \\&&|& \hex{45} &\Rightarrow& \I32.\EQZ \\ &&|& \hex{46} &\Rightarrow& \I32.\EQ \\ &&|& \hex{47} &\Rightarrow& \I32.\NE \\ &&|& @@ -211,7 +211,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{50} &\Rightarrow& \I64.\EQZ \\ &&|& \hex{51} &\Rightarrow& \I64.\EQ \\ &&|& \hex{52} &\Rightarrow& \I64.\NE \\ &&|& @@ -227,7 +227,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{5B} &\Rightarrow& \F32.\EQ \\ &&|& \hex{5C} &\Rightarrow& \F32.\NE \\ &&|& \hex{5D} &\Rightarrow& \F32.\LT \\ &&|& @@ -238,7 +238,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{61} &\Rightarrow& \F64.\EQ \\ &&|& \hex{62} &\Rightarrow& \F64.\NE \\ &&|& \hex{63} &\Rightarrow& \F64.\LT \\ &&|& @@ -252,7 +252,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{67} &\Rightarrow& \I32.\CLZ \\ &&|& \hex{68} &\Rightarrow& \I32.\CTZ \\ &&|& \hex{69} &\Rightarrow& \I32.\POPCNT \\ &&|& @@ -275,7 +275,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{79} &\Rightarrow& \I64.\CLZ \\ &&|& \hex{7A} &\Rightarrow& \I64.\CTZ \\ &&|& \hex{7B} &\Rightarrow& \I64.\POPCNT \\ &&|& @@ -298,7 +298,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{8B} &\Rightarrow& \F32.\ABS \\ &&|& \hex{8C} &\Rightarrow& \F32.\NEG \\ &&|& \hex{8D} &\Rightarrow& \F32.\CEIL \\ &&|& @@ -317,7 +317,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{99} &\Rightarrow& \F64.\ABS \\ &&|& \hex{9A} &\Rightarrow& \F64.\NEG \\ &&|& \hex{9B} &\Rightarrow& \F64.\CEIL \\ &&|& @@ -338,7 +338,7 @@ All other numeric instructions are plain opcodes without any immediates. .. math:: \begin{array}{llclll} - \phantom{\production{instructions}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& \hex{A7} &\Rightarrow& \I32.\WRAP\K{/}\I64 \\ &&|& \hex{A8} &\Rightarrow& \I32.\TRUNC\K{\_s/}\F32 \\ &&|& \hex{A9} &\Rightarrow& \I32.\TRUNC\K{\_u/}\F32 \\ &&|& @@ -380,6 +380,6 @@ Expressions .. math:: \begin{array}{llclll} - \production{instructions} & \Bexpr &::=& + \production{expression} & \Bexpr &::=& (\X{in}{:}\Binstr)^\ast~~\hex{0B} &\Rightarrow& \X{in}^\ast~\END \\ \end{array} diff --git a/document/binary/modules.rst b/document/binary/modules.rst index f520e7b88f..732d91375d 100644 --- a/document/binary/modules.rst +++ b/document/binary/modules.rst @@ -40,13 +40,13 @@ All :ref:`indices ` are encoded with their respective |U32| value. .. math:: \begin{array}{llclll} - \production{type indices} & \Btypeidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{function indices} & \Bfuncidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{table indices} & \Btableidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{memory indices} & \Bmemidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{global indices} & \Bglobalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{local indices} & \Blocalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ - \production{label indices} & \Blabelidx &::=& l{:}\Bu32 &\Rightarrow& l \\ + \production{type index} & \Btypeidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{function index} & \Bfuncidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{table index} & \Btableidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{memory index} & \Bmemidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{global index} & \Bglobalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{local index} & \Blocalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{label index} & \Blabelidx &::=& l{:}\Bu32 &\Rightarrow& l \\ \end{array} @@ -69,7 +69,7 @@ The following parameterized grammar rule defines the generic structure of a sect .. math:: \begin{array}{llclll@{\qquad}l} - \production{sections} & \Bsection_N(\B{B}) &::=& + \production{section} & \Bsection_N(\B{B}) &::=& N{:}\Bbyte~~\X{size}{:}\Bu32~~\X{cont}{:}\B{B} &\Rightarrow& \X{cont} & (\X{size} = ||\B{B}||) \\ &&|& \epsilon &\Rightarrow& \epsilon @@ -98,7 +98,7 @@ Their contents consist of a :ref:`name ` further identifying the cu .. math:: \begin{array}{llclll} - \production{custom sections} & \Bcustomsec &::=& + \production{custom section} & \Bcustomsec &::=& \Bsection_0(\Bcustom) \\ \production{custom data} & \Bcustom &::=& \Bname~~\Bbyte^\ast \\ @@ -123,7 +123,7 @@ It decodes into a vector of :ref:`function types ` that represe .. math:: \begin{array}{llclll} - \production{type sections} & \Btypesec &::=& + \production{type section} & \Btypesec &::=& \X{ft}^\ast{:\,}\Bsection_1(\Bfunctype^\ast) &\Rightarrow& \X{ft}^\ast \\ \end{array} @@ -143,12 +143,12 @@ It decodes into a vector of :ref:`imports ` that represent the |I .. math:: \begin{array}{llclll} - \production{import sections} & \Bimportsec &::=& + \production{import section} & \Bimportsec &::=& \X{im}^\ast{:}\Bsection_2(\Bimport^\ast) &\Rightarrow& \X{im}^\ast \\ - \production{imports} & \Bimport &::=& + \production{import} & \Bimport &::=& \X{mod}{:}\Bname~~\X{nm}{:}\Bname~~d{:}\Bimportdesc &\Rightarrow& \{ \MODULE~\X{mod}, \NAME~\X{nm}, \DESC~d \} \\ - \production{import descriptions} & \Bimportdesc &::=& + \production{import description} & \Bimportdesc &::=& \hex{00}~~x{:}\Btypeidx &\Rightarrow& \FUNC~x \\ &&|& \hex{01}~~\X{tt}{:}\Btabletype &\Rightarrow& \TABLE~\X{tt} \\ &&|& \hex{02}~~\X{mt}{:}\Bmemtype &\Rightarrow& \MEM~\X{mt} \\ &&|& @@ -172,7 +172,7 @@ The |LOCALS| and |BODY| fields of the respective functions are encoded separatel .. math:: \begin{array}{llclll} - \production{function sections} & \Bfuncsec &::=& + \production{function section} & \Bfuncsec &::=& x^\ast{:}\Bsection_3(\Btypeidx^\ast) &\Rightarrow& x^\ast \\ \end{array} @@ -192,9 +192,9 @@ It decodes into a vector of :ref:`tables ` that represent the |TAB .. math:: \begin{array}{llclll} - \production{table sections} & \Btablesec &::=& + \production{table section} & \Btablesec &::=& \X{tab}^\ast{:}\Bsection_4(\Btable^\ast) &\Rightarrow& \X{tab}^\ast \\ - \production{tables} & \Btable &::=& + \production{table} & \Btable &::=& \X{tt}{:}\Btabletype &\Rightarrow& \{ \TYPE~\X{tt} \} \\ \end{array} @@ -214,9 +214,9 @@ It decodes into a vector of :ref:`memories ` that represent the |MEM .. math:: \begin{array}{llclll} - \production{memory sections} & \Bmemsec &::=& + \production{memory section} & \Bmemsec &::=& \X{mem}^\ast{:}\Bsection_5(\Bmem^\ast) &\Rightarrow& \X{mem}^\ast \\ - \production{memories} & \Bmem &::=& + \production{memory} & \Bmem &::=& \X{mt}{:}\Bmemtype &\Rightarrow& \{ \TYPE~\X{mt} \} \\ \end{array} @@ -236,9 +236,9 @@ It decodes into a vector of :ref:`globals ` that represent the |G .. math:: \begin{array}{llclll} - \production{global sections} & \Bglobalsec &::=& + \production{global section} & \Bglobalsec &::=& \X{glob}^\ast{:}\Bsection_6(\Bglobal^\ast) &\Rightarrow& \X{glob}^\ast \\ - \production{globals} & \Bglobal &::=& + \production{global} & \Bglobal &::=& \X{gt}{:}\Bglobaltype~~e{:}\Bexpr &\Rightarrow& \{ \TYPE~\X{gt}, \INIT~e \} \\ \end{array} @@ -259,12 +259,12 @@ It decodes into a vector of :ref:`exports ` that represent the |E .. math:: \begin{array}{llclll} - \production{export sections} & \Bexportsec &::=& + \production{export section} & \Bexportsec &::=& \X{ex}^\ast{:}\Bsection_7(\Bexport^\ast) &\Rightarrow& \X{ex}^\ast \\ - \production{exports} & \Bexport &::=& + \production{export} & \Bexport &::=& \X{nm}{:}\Bname~~d{:}\Bexportdesc &\Rightarrow& \{ \NAME~\X{nm}, \DESC~d \} \\ - \production{export descriptions} & \Bexportdesc &::=& + \production{export description} & \Bexportdesc &::=& \hex{00}~~x{:}\Bfuncidx &\Rightarrow& \FUNC~x \\ &&|& \hex{01}~~x{:}\Btableidx &\Rightarrow& \TABLE~x \\ &&|& \hex{02}~~x{:}\Bmemidx &\Rightarrow& \MEM~x \\ &&|& @@ -288,9 +288,9 @@ It decodes into an optional :ref:`start function ` that represents .. math:: \begin{array}{llclll} - \production{start sections} & \Bstartsec &::=& + \production{start section} & \Bstartsec &::=& \X{st}^?{:}\Bsection_8(\Bstart) &\Rightarrow& \X{st}^? \\ - \production{start functions} & \Bstart &::=& + \production{start function} & \Bstart &::=& x{:}\Bfuncidx &\Rightarrow& \{ \FUNC~x \} \\ \end{array} @@ -312,9 +312,9 @@ It decodes into a vector of :ref:`element segments ` that represent .. math:: \begin{array}{llclll} - \production{element sections} & \Belemsec &::=& + \production{element section} & \Belemsec &::=& \X{seg}^\ast{:}\Bsection_9(\Belem^\ast) &\Rightarrow& \X{seg} \\ - \production{element segments} & \Belem &::=& + \production{element segment} & \Belem &::=& x{:}\Btableidx~~e{:}\Bexpr~~y^\ast{:}\Bvec(\Bfuncidx) &\Rightarrow& \{ \TABLE~x, \OFFSET~e, \INIT~y^\ast \} \\ \end{array} @@ -352,13 +352,13 @@ denoting *count* locals of the same value type. .. math:: \begin{array}{llclll@{\qquad}l} - \production{code sections} & \Bcodesec &::=& + \production{code section} & \Bcodesec &::=& \X{code}^\ast{:}\Bsection_{10}(\Bcode^\ast) &\Rightarrow& \X{code}^\ast \\ \production{code} & \Bcode &::=& \X{size}{:}\Bu32~~\X{code}{:}\Bfunc &\Rightarrow& \X{code} & (\X{size} = ||\Bfunc||) \\ - \production{functions} & \Bfunc &::=& + \production{function} & \Bfunc &::=& (t^\ast)^\ast{:}\Bvec(\Blocals)~~e{:}\Bexpr &\Rightarrow& \F{concat}((t^\ast)^\ast), e^\ast & (|\F{concat}((t^\ast)^\ast)| < 2^{32}) \\ @@ -368,13 +368,13 @@ denoting *count* locals of the same value type. .. math (commented out) \begin{array}{llclll} - \production{code sections} & \Bcodesec_{\typeidx^n} &::=& + \production{code section} & \Bcodesec_{\typeidx^n} &::=& \f^\ast{:}\Bsection_{10}(\Bcode_{\typeidx}^n) &\Rightarrow& \f^\ast \\ \production{code} & \Bcode_{\typeidx} &::=& \X{size}{:}\Bu32~~f{:}\Bfunc_{\typeidx} &\Rightarrow& f \qquad\qquad (\X{size} = |\Bfunc|) \\ - \production{functions} & \Bfunc_{\typeidx} &::=& + \production{function} & \Bfunc_{\typeidx} &::=& (t^\ast)^\ast{:}\Bvec(\Blocals)~~e{:}\Bexpr &\Rightarrow& \{ \TYPE~\typeidx, \LOCALS~\F{concat}((t^\ast)^\ast), \BODY~e^\ast \} \\ \production{locals} & \Blocals &::=& @@ -407,9 +407,9 @@ It decodes into a vector of :ref:`data segments ` that represent th .. math:: \begin{array}{llclll} - \production{data sections} & \Bdatasec &::=& + \production{data section} & \Bdatasec &::=& \X{seg}^\ast{:}\Bsection_{11}(\Bdata^\ast) &\Rightarrow& \X{seg} \\ - \production{data segments} & \Bdata &::=& + \production{data segment} & \Bdata &::=& x{:}\Bmemidx~~e{:}\Bexpr~~b^\ast{:}\Bvec(\Bbyte) &\Rightarrow& \{ \MEM~x, \OFFSET~e, \INIT~b^\ast \} \\ \end{array} @@ -440,7 +440,7 @@ The lengths of vectors produced by the (possibly empty) :ref:`function ` occurring in the binary format .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{result types} & \Bblocktype &::=& + \production{result type} & \Bblocktype &::=& \hex{40} &\Rightarrow& [] \\ &&|& t{:}\Bvaltype &\Rightarrow& [t] \\ \end{array} @@ -64,7 +64,7 @@ Function Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{function types} & \Bfunctype &::=& + \production{function type} & \Bfunctype &::=& \hex{60}~~t_1^\ast{:\,}\Bvec(\Bvaltype)~~t_2^\ast{:\,}\Bvec(\Bvaltype) &\Rightarrow& [t_1^\ast] \to [t_2^\ast] \\ \end{array} @@ -100,7 +100,7 @@ Memory Types .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{memory types} & \Bmemtype &::=& + \production{memory type} & \Bmemtype &::=& \X{lim}{:}\Blimits &\Rightarrow& \X{lim} \\ \end{array} @@ -120,9 +120,9 @@ Table Types .. math:: \begin{array}{llclll} - \production{table types} & \Btabletype &::=& + \production{table type} & \Btabletype &::=& \X{et}{:}\Belemtype~~\X{lim}{:}\Blimits &\Rightarrow& \X{lim}~\X{et} \\ - \production{element types} & \Belemtype &::=& + \production{element type} & \Belemtype &::=& \hex{70} &\Rightarrow& \ANYFUNC \\ \end{array} @@ -141,9 +141,9 @@ Global Types .. math:: \begin{array}{llclll} - \production{global types} & \Bglobaltype &::=& + \production{global type} & \Bglobaltype &::=& t{:}\Bvaltype~~m{:}\Bmut &\Rightarrow& m~t \\ \production{mutability} & \Bmut &::=& - \hex{00} &\Rightarrow& \CONST \\ &&|& - \hex{01} &\Rightarrow& \MUT \\ + \hex{00} &\Rightarrow& \MCONST \\ &&|& + \hex{01} &\Rightarrow& \MVAR \\ \end{array} diff --git a/document/binary/values.rst b/document/binary/values.rst index b2abed9ffa..6a1e98a4f0 100644 --- a/document/binary/values.rst +++ b/document/binary/values.rst @@ -19,7 +19,7 @@ Bytes .. math:: \begin{array}{llcll@{\qquad}l} - \production{bytes} & \Bbyte &::=& + \production{byte} & \Bbyte &::=& \hex{00} &\Rightarrow& \hex{00} \\ &&|&& \dots \\ &&|& \hex{FF} &\Rightarrow& \hex{FF} \\ @@ -49,9 +49,9 @@ As an additional constraint, the total number of bytes encoding a value of type .. math:: \begin{array}{llclll@{\qquad}l} - \production{unsigned integers} & \BuX{N} &::=& + \production{unsigned integer} & \BuX{N} &::=& n{:}\Bbyte &\Rightarrow& n & (n < 2^7 \wedge n < 2^N) \\ &&|& - n{:}\Bbyte~~m{:}\BuX{N-7} &\Rightarrow& + n{:}\Bbyte~~m{:}\BuX{(N\B{-7})} &\Rightarrow& 2^7\cdot m + (n-2^7) & (n \geq 2^7 \wedge N > 7) \\ \end{array} @@ -60,10 +60,10 @@ As an additional constraint, the total number of bytes encoding a value of type .. math:: \begin{array}{llclll@{\qquad}l} - \production{signed integers} & \BsX{N} &::=& + \production{signed integer} & \BsX{N} &::=& n{:}\Bbyte &\Rightarrow& n & (n < 2^6 \wedge n < 2^{N-1}) \\ &&|& n{:}\Bbyte &\Rightarrow& n-2^7 & (2^6 \leq n < 2^7 \wedge n \geq 2^7-2^{N-1}) \\ &&|& - n{:}\Bbyte~~m{:}\BsX{N-7} &\Rightarrow& + n{:}\Bbyte~~m{:}\BsX{(N\B{-7})} &\Rightarrow& 2^7\cdot m + (n-2^7) & (n \geq 2^7 \wedge N > 7) \\ \end{array} @@ -71,7 +71,7 @@ As an additional constraint, the total number of bytes encoding a value of type .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{uninterpreted integers} & \BiX{N} &::=& + \production{uninterpreted integer} & \BiX{N} &::=& n{:}\BsX{N} &\Rightarrow& n \end{array} @@ -99,7 +99,7 @@ Floating-Point .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{floating-point numbers} & \BfX{N} &::=& + \production{floating-point number} & \BfX{N} &::=& b^\ast{:\,}\Bbyte^{N/8} &\Rightarrow& \F{reverse}(b^\ast) \\ \end{array} @@ -118,7 +118,7 @@ Vectors .. math:: \begin{array}{llclll@{\qquad\qquad}l} - \production{vectors} & \Bvec(\B{B}) &::=& + \production{vector} & \Bvec(\B{B}) &::=& n{:}\Bu32~~(x{:}\B{B})^n &\Rightarrow& x^n \\ \end{array} @@ -135,13 +135,13 @@ Names .. math:: \begin{array}{llclll@{\qquad}l} - \production{names} & \Bname &::=& + \production{name} & \Bname &::=& n{:}\Bu32~~(\X{uc}{:}\Bcodepoint)^\ast &\Rightarrow& \X{uc}^\ast & (|\Bcodepoint^\ast| = n) \\ - \production{code points} & \Bcodepoint &::=& + \production{code point} & \Bcodepoint &::=& \X{uv}{:}\Bcodeval_N &\Rightarrow& \X{uv} & (\X{uv} \geq N \wedge (\X{uv} < \unicode{D800} \vee \unicode{E000} \leq \X{uv} < \unicode{110000})) \\ - \production{code values} & \Bcodeval_N &::=& + \production{code value} & \Bcodeval_N &::=& b_1{:}\Bbyte &\Rightarrow& b_1 & (b_1 < \hex{80} \wedge N = \unicode{00}) \\ &&|& diff --git a/document/execution/index.rst b/document/execution/index.rst index 628dbdc85d..caa7046cf1 100644 --- a/document/execution/index.rst +++ b/document/execution/index.rst @@ -5,5 +5,7 @@ Execution :maxdepth: 2 conventions - invocation + runtime + numerics instructions + modules diff --git a/document/index.rst b/document/index.rst index 6060619a7d..417975647c 100644 --- a/document/index.rst +++ b/document/index.rst @@ -11,9 +11,7 @@ WebAssembly Specification introduction/index syntax/index validation/index - instantiation/index execution/index - instructions/index binary/index appendix-properties/index appendix-algorithm/index diff --git a/document/instantiation/index.rst b/document/instantiation/index.rst deleted file mode 100644 index 2fdfe1ac10..0000000000 --- a/document/instantiation/index.rst +++ /dev/null @@ -1,8 +0,0 @@ -Instantiation -============= - -.. toctree:: - :maxdepth: 2 - - conventions - instantiation diff --git a/document/math.def b/document/math.def index d79f1fea3c..6d970bc711 100644 --- a/document/math.def +++ b/document/math.def @@ -20,6 +20,7 @@ .. Auxiliary definitions for grammars .. |production| mathdef:: \void +.. |with| mathdef:: ~\xref{syntax/conventions}{syntax-record}{\mbox{with}}~ .. Values, terminals @@ -32,31 +33,31 @@ .. |byte| mathdef:: \xref{syntax/values}{syntax-byte}{\X{byte}} -.. |uX#1| mathdef:: {\X{uint}_{#1}} -.. |sX#1| mathdef:: {\X{sint}_{#1}} -.. |iX#1| mathdef:: {\X{int}_{#1}} -.. |fX#1| mathdef:: {\X{float}_{#1}} +.. |uX#1| mathdef:: {\X{u}#1} +.. |sX#1| mathdef:: {\X{s}#1} +.. |iX#1| mathdef:: {\X{i}#1} +.. |fX#1| mathdef:: {\X{f}#1} .. |uN| mathdef:: \xref{syntax/values}{syntax-int}{\uX{N}} -.. |u1| mathdef:: \xref{syntax/values}{syntax-int}{\uX{1}} -.. |u8| mathdef:: \xref{syntax/values}{syntax-int}{\uX{8}} -.. |u16| mathdef:: \xref{syntax/values}{syntax-int}{\uX{16}} -.. |u32| mathdef:: \xref{syntax/values}{syntax-int}{\uX{32}} -.. |u64| mathdef:: \xref{syntax/values}{syntax-int}{\uX{64}} +.. |u1| mathdef:: \xref{syntax/values}{syntax-int}{\uX{\X{1}}} +.. |u8| mathdef:: \xref{syntax/values}{syntax-int}{\uX{\X{8}}} +.. |u16| mathdef:: \xref{syntax/values}{syntax-int}{\uX{\X{16}}} +.. |u32| mathdef:: \xref{syntax/values}{syntax-int}{\uX{\X{32}}} +.. |u64| mathdef:: \xref{syntax/values}{syntax-int}{\uX{\X{64}}} .. |sN| mathdef:: \xref{syntax/values}{syntax-int}{\sX{N}} -.. |s8| mathdef:: \xref{syntax/values}{syntax-int}{\sX{8}} -.. |s16| mathdef:: \xref{syntax/values}{syntax-int}{\sX{16}} -.. |s32| mathdef:: \xref{syntax/values}{syntax-int}{\sX{32}} -.. |s64| mathdef:: \xref{syntax/values}{syntax-int}{\sX{64}} +.. |s8| mathdef:: \xref{syntax/values}{syntax-int}{\sX{\X{8}}} +.. |s16| mathdef:: \xref{syntax/values}{syntax-int}{\sX{\X{16}}} +.. |s32| mathdef:: \xref{syntax/values}{syntax-int}{\sX{\X{32}}} +.. |s64| mathdef:: \xref{syntax/values}{syntax-int}{\sX{\X{64}}} .. |iN| mathdef:: \xref{syntax/values}{syntax-int}{\iX{N}} -.. |i32| mathdef:: \xref{syntax/values}{syntax-int}{\iX{32}} -.. |i64| mathdef:: \xref{syntax/values}{syntax-int}{\iX{64}} +.. |i32| mathdef:: \xref{syntax/values}{syntax-int}{\iX{\X{32}}} +.. |i64| mathdef:: \xref{syntax/values}{syntax-int}{\iX{\X{64}}} .. |fN| mathdef:: \xref{syntax/values}{syntax-float}{\fX{N}} -.. |f32| mathdef:: \xref{syntax/values}{syntax-float}{\fX{32}} -.. |f64| mathdef:: \xref{syntax/values}{syntax-float}{\fX{64}} +.. |f32| mathdef:: \xref{syntax/values}{syntax-float}{\fX{\X{32}}} +.. |f64| mathdef:: \xref{syntax/values}{syntax-float}{\fX{\X{64}}} .. |vec| mathdef:: \xref{syntax/values}{syntax-vec}{\X{vec}} .. |name| mathdef:: \xref{syntax/values}{syntax-name}{\X{name}} @@ -67,29 +68,29 @@ .. |Bbyte| mathdef:: \xref{binary/values}{binary-byte}{\B{byte}} -.. |BuX#1| mathdef:: {\B{uint}_{#1}} -.. |BsX#1| mathdef:: {\B{sint}_{#1}} -.. |BiX#1| mathdef:: {\B{int}_{#1}} -.. |BfX#1| mathdef:: {\B{float}_{#1}} +.. |BuX#1| mathdef:: {\B{u}#1} +.. |BsX#1| mathdef:: {\B{s}#1} +.. |BiX#1| mathdef:: {\B{i}#1} +.. |BfX#1| mathdef:: {\B{f}#1} .. |BuN| mathdef:: \xref{binary/values}{binary-int}{\BuX{N}} -.. |Bu1| mathdef:: \xref{binary/values}{binary-int}{\BuX{1}} -.. |Bu8| mathdef:: \xref{binary/values}{binary-int}{\BuX{8}} -.. |Bu16| mathdef:: \xref{binary/values}{binary-int}{\BuX{16}} -.. |Bu32| mathdef:: \xref{binary/values}{binary-int}{\BuX{32}} -.. |Bu64| mathdef:: \xref{binary/values}{binary-int}{\BuX{64}} +.. |Bu1| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{1}}} +.. |Bu8| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{8}}} +.. |Bu16| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{16}}} +.. |Bu32| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{32}}} +.. |Bu64| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{64}}} .. |BsN| mathdef:: \xref{binary/values}{binary-int}{\BsX{N}} -.. |Bs32| mathdef:: \xref{binary/values}{binary-int}{\BsX{32}} -.. |Bs64| mathdef:: \xref{binary/values}{binary-int}{\BsX{64}} +.. |Bs32| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{32}}} +.. |Bs64| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{64}}} .. |BiN| mathdef:: \xref{binary/values}{binary-int}{\BiX{N}} -.. |Bi32| mathdef:: \xref{binary/values}{binary-int}{\BiX{32}} -.. |Bi64| mathdef:: \xref{binary/values}{binary-int}{\BiX{64}} +.. |Bi32| mathdef:: \xref{binary/values}{binary-int}{\BiX{\B{32}}} +.. |Bi64| mathdef:: \xref{binary/values}{binary-int}{\BiX{\B{64}}} .. |BfN| mathdef:: \xref{binary/values}{binary-float}{\BfX{N}} -.. |Bf32| mathdef:: \xref{binary/values}{binary-float}{\BfX{32}} -.. |Bf64| mathdef:: \xref{binary/values}{binary-float}{\BfX{64}} +.. |Bf32| mathdef:: \xref{binary/values}{binary-float}{\BfX{\B{32}}} +.. |Bf64| mathdef:: \xref{binary/values}{binary-float}{\BfX{\B{64}}} .. |Bvec| mathdef:: \xref{binary/values}{binary-vec}{\B{vec}} .. |Bname| mathdef:: \xref{binary/values}{binary-name}{\B{name}} @@ -100,13 +101,16 @@ .. Types, terminals +.. |I8| mathdef:: \xref{execution/runtime}{syntax-storagetype}{\K{i8}} +.. |I16| mathdef:: \xref{execution/runtime}{syntax-storagetype}{\K{i16}} .. |I32| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{i32}} .. |I64| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{i64}} .. |F32| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{f32}} .. |F64| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{f64}} .. |ANYFUNC| mathdef:: \xref{syntax/types}{syntax-elemtype}{\K{anyfunc}} -.. |MUT| mathdef:: \xref{syntax/types}{syntax-mut}{\K{mut}} +.. |MVAR| mathdef:: \xref{syntax/types}{syntax-mut}{\K{var}} +.. |MCONST| mathdef:: \xref{syntax/types}{syntax-mut}{\K{var}} .. |MIN| mathdef:: \K{min} .. |MAX| mathdef:: \K{max} @@ -121,7 +125,6 @@ .. |tabletype| mathdef:: \xref{syntax/types}{syntax-tabletype}{\X{tabletype}} .. |elemtype| mathdef:: \xref{syntax/types}{syntax-elemtype}{\X{elemtype}} .. |memtype| mathdef:: \xref{syntax/types}{syntax-memtype}{\X{memtype}} -.. |externtype| mathdef:: \xref{syntax/types}{syntax-externtype}{\X{externtype}} .. |limits| mathdef:: \xref{syntax/types}{syntax-limits}{\X{limits}} .. |mut| mathdef:: \xref{syntax/types}{syntax-mut}{\X{mut}} @@ -136,7 +139,6 @@ .. |Btabletype| mathdef:: \xref{binary/types}{binary-tabletype}{\B{tabletype}} .. |Belemtype| mathdef:: \xref{binary/types}{binary-elemtype}{\B{elemtype}} .. |Bmemtype| mathdef:: \xref{binary/types}{binary-memtype}{\B{memtype}} -.. |Bexterntype| mathdef:: \xref{binary/types}{binary-externtype}{\B{externtype}} .. |Blimits| mathdef:: \xref{binary/types}{binary-limits}{\B{limits}} .. |Bmut| mathdef:: \xref{binary/types}{binary-mut}{\B{mut}} @@ -169,6 +171,7 @@ .. |GLOBALS| mathdef:: \K{globals} .. |LOCALS| mathdef:: \K{locals} .. |LABELS| mathdef:: \K{labels} +.. |LRETURN| mathdef:: \K{return} .. |IMPORTS| mathdef:: \K{imports} .. |EXPORTS| mathdef:: \K{exports} @@ -178,8 +181,6 @@ .. |TABLE| mathdef:: \K{table} .. |MEM| mathdef:: \K{mem} .. |GLOBAL| mathdef:: \K{global} -.. |LOCAL| mathdef:: \K{local} -.. |LABEL| mathdef:: \K{label} .. |IMPORT| mathdef:: \K{import} .. |EXPORT| mathdef:: \K{export} .. |CODE| mathdef:: \K{code} @@ -251,10 +252,10 @@ .. Modules, meta functions -.. |funcs| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{funcs}} -.. |tables| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{tables}} -.. |mems| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{mems}} -.. |globals| mathdef:: \xref{syntax/types}{syntax-externtype}{\F{globals}} +.. |funcs| mathdef:: \xref{execution/runtime}{syntax-externtype}{\F{funcs}} +.. |tables| mathdef:: \xref{execution/runtime}{syntax-externtype}{\F{tables}} +.. |mems| mathdef:: \xref{execution/runtime}{syntax-externtype}{\F{mems}} +.. |globals| mathdef:: \xref{execution/runtime}{syntax-externtype}{\F{globals}} .. Instructions, terminals @@ -331,14 +332,35 @@ .. |DEMOTE| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{demote}} .. |REINTERPRET| mathdef:: \xref{syntax/instructions}{syntax-instr-numeric}{\K{reinterpret}} +.. |TRAP| mathdef:: \xref{execution/runtime}{syntax-instr-admin}{\K{trap}} +.. |LABEL| mathdef:: \xref{execution/runtime}{syntax-instr-admin}{\K{label}} +.. |FRAME| mathdef:: \xref{execution/runtime}{syntax-instr-admin}{\K{frame}} + +.. |INVOKE| mathdef:: \xref{execution/instructions}{syntax-instr-admin}{\K{invoke}} +.. |INSTANTIATE| mathdef:: \xref{execution/modules}{syntax-instantiate}{\K{instantiate}} +.. |INITIALIZE| mathdef:: \xref{execution/modules}{syntax-instantiate}{\K{initialize}} +.. |INITGLOBAL| mathdef:: \xref{execution/modules}{syntax-instantiate}{\K{init\_global}} +.. |INITTABLE| mathdef:: \xref{execution/modules}{syntax-instantiate}{\K{init\_table}} +.. |INITMEM| mathdef:: \xref{execution/modules}{syntax-instantiate}{\K{init\_mem}} + .. Instructions, non-terminals -.. |unop| mathdef:: \X{unop} -.. |binop| mathdef:: \X{binop} -.. |testop| mathdef:: \X{testop} -.. |relop| mathdef:: \X{relop} -.. |cvtop| mathdef:: \X{cvtop} +.. |unop| mathdef:: \xref{syntax/instructions}{syntax-unop}{\X{unop}} +.. |binop| mathdef:: \xref{syntax/instructions}{syntax-binop}{\X{binop}} +.. |testop| mathdef:: \xref{syntax/instructions}{syntax-testop}{\X{testop}} +.. |relop| mathdef:: \xref{syntax/instructions}{syntax-relop}{\X{relop}} +.. |cvtop| mathdef:: \xref{syntax/instructions}{syntax-cvtop}{\X{cvtop}} + +.. |iunop| mathdef:: \xref{syntax/instructions}{syntax-iunop}{\X{iunop}} +.. |ibinop| mathdef:: \xref{syntax/instructions}{syntax-ibinop}{\X{ibinop}} +.. |itestop| mathdef:: \xref{syntax/instructions}{syntax-itestop}{\X{itestop}} +.. |irelop| mathdef:: \xref{syntax/instructions}{syntax-irelop}{\X{irelop}} + +.. |funop| mathdef:: \xref{syntax/instructions}{syntax-funop}{\X{funop}} +.. |fbinop| mathdef:: \xref{syntax/instructions}{syntax-fbinop}{\X{fbinop}} +.. |ftestop| mathdef:: \xref{syntax/instructions}{syntax-ftestop}{\X{ftestop}} +.. |frelop| mathdef:: \xref{syntax/instructions}{syntax-frelop}{\X{frelop}} .. |sx| mathdef:: \xref{syntax/instructions}{syntax-sx}{\X{sx}} .. |memarg| mathdef:: \xref{syntax/instructions}{syntax-memarg}{\X{memarg}} @@ -353,3 +375,50 @@ .. |Binstr| mathdef:: \xref{binary/instructions}{binary-instr}{\B{instr}} .. |Bexpr| mathdef:: \xref{binary/instructions}{binary-expr}{\B{expr}} + + +.. Runtime, terminals + +.. |MUT| mathdef:: \K{mut} + + +.. Runtime, non-terminals + +.. |val| mathdef:: \xref{execution/runtime}{syntax-val}{\X{val}} + +.. |addr| mathdef:: \xref{execution/runtime}{syntax-addr}{\X{addr}} +.. |funcaddr| mathdef:: \xref{execution/runtime}{syntax-funcaddr}{\X{funcaddr}} +.. |tableaddr| mathdef:: \xref{execution/runtime}{syntax-tableaddr}{\X{tableaddr}} +.. |memaddr| mathdef:: \xref{execution/runtime}{syntax-memaddr}{\X{memaddr}} +.. |globaladdr| mathdef:: \xref{execution/runtime}{syntax-globaladdr}{\X{globaladdr}} + +.. |moduleinst| mathdef:: \xref{execution/runtime}{syntax-moduleinst}{\X{moduleinst}} +.. |funcinst| mathdef:: \xref{execution/runtime}{syntax-funcinst}{\X{funcinst}} +.. |tableinst| mathdef:: \xref{execution/runtime}{syntax-tableinst}{\X{tableinst}} +.. |funcelem| mathdef:: \xref{execution/runtime}{syntax-funcelem}{\X{funcelem}} +.. |meminst| mathdef:: \xref{execution/runtime}{syntax-meminst}{\X{meminst}} +.. |globalinst| mathdef:: \xref{execution/runtime}{syntax-globalinst}{\X{globalinst}} +.. |exportinst| mathdef:: \xref{execution/runtime}{syntax-exportinst}{\X{exportinst}} + +.. |externval| mathdef:: \xref{execution/runtime}{syntax-externval}{\X{externval}} +.. |externtype| mathdef:: \xref{execution/runtime}{syntax-externtype}{\X{externtype}} +.. |storagetype| mathdef:: \xref{execution/runtime}{syntax-storagetype}{\X{storagetype}} + +.. |store| mathdef:: \xref{execution/runtime}{syntax-store}{\X{store}} +.. |frame| mathdef:: \xref{execution/runtime}{syntax-frame}{\X{frame}} +.. |label| mathdef:: \xref{execution/runtime}{syntax-label}{\X{label}} + +.. |XB| mathdef:: \xref{execution/runtime}{syntax-ctxt-block}{B} + + +.. Execution, notation + +.. |stepto| mathdef:: \hookrightarrow +.. |mod| mathdef:: \mathbin{\F{mod}} + +.. Numerics, meta functions + +.. |bytes| mathdef:: \xref{execution/numerics}{aux-bytes}{\F{bytes}} +.. |signed| mathdef:: \xref{execution/numerics}{aux-signed}{\F{signed}} +.. |extend| mathdef:: \xref{execution/numerics}{aux-extend}{\F{extend}} +.. |wrap| mathdef:: \xref{execution/numerics}{aux-wrap}{\F{wrap}} diff --git a/document/syntax/conventions.rst b/document/syntax/conventions.rst index 63413f5459..438b6b096a 100644 --- a/document/syntax/conventions.rst +++ b/document/syntax/conventions.rst @@ -30,6 +30,9 @@ The following conventions are adopted in defining grammar rules for abstract syn * :math:`A^\ast` is a possibly empty sequence of iterations of :math:`A`. (This is a shorthand for :math:`A^n` used where :math:`n` is not relevant.) +* :math:`A^+` is a possibly empty sequence of iterations of :math:`A`. + (This is a shorthand for :math:`A^n` where :math:`n \geq 1`.) + * :math:`A^?` is an optional occurrence of :math:`A`. (This is a shorthand for :math:`A^n` where :math:`n \leq 1`.) @@ -47,6 +50,14 @@ When dealing with syntactic constructs the following notation is also used: * :math:`s[i]` denotes the :math:`i`-th element of a sequence :math:`s`, starting from :math:`0`. +* :math:`s[i:n]` denotes the sub-sequence of length :math:`n` a sequence :math:`s` that consists of its :math:`i`-th to :math:`(i+n-1)`-the element. + +* :math:`s~\mbox{with}~[i] = x` denotes the same sequence as :math:`s`, + except that the :math:`i`-the element is replaced with :math:`x`. + +* :math:`s~\mbox{with}~[i:n] = x^n` denotes the same sequence as :math:`s`, + except that the sub-sequence :math:`s[i:n]` is replaced with :math:`x^n`. + Productions of the following form are interpreted as *records* that map a fixed set of fields :math:`\K{field}_i` to values :math:`x_i`, respectively: .. math:: @@ -55,3 +66,14 @@ Productions of the following form are interpreted as *records* that map a fixed The following notation is adopted for manipulating such records: * :math:`r.\K{field}` denotes the :math:`\K{field}` component of :math:`r`. + +* :math:`r~\mbox{with}~\K{field} = x` denotes the same record as :math:`r`, + except that the :math:`\K{field}` component is replaced with :math:`x`. + +The update notation for sequences and records generalizes recursively to nested components accessed by "paths" :math:`\X{pth} ::= ([\dots] \;| \;.\K{field})^+`: + +* :math:`s~\mbox{with}~[i]\X{pth} = x` denotes the same sequence as :math:`s`, + except that the :math:`s[i]` is replaced with :math:`s[i]~\mbox{with}~\X{pth} = x`. + +* :math:`r~\mbox{with}~\K{field}\X{pth} = x` denotes the same record as :math:`r`, + except that the :math:`\K{field}` component is replaced with :math:`r.\K{field}~\mbox{with}~\X{pth} = x`. diff --git a/document/syntax/instructions.rst b/document/syntax/instructions.rst index d1749c07a1..ce389bb6b6 100644 --- a/document/syntax/instructions.rst +++ b/document/syntax/instructions.rst @@ -25,6 +25,19 @@ The following sections group instructions into a number of different categories. .. _syntax-sx: .. _syntax-instr-numeric: +.. _syntax-const: +.. _syntax-unop: +.. _syntax-binop: +.. _syntax-testop: +.. _syntax-relop: +.. _syntax-iunop: +.. _syntax-ibinop: +.. _syntax-itestop: +.. _syntax-irelop: +.. _syntax-funop: +.. _syntax-fbinop: +.. _syntax-ftestop: +.. _syntax-frelop: .. index:: ! numeric instruction pair: abstract syntax; instruction @@ -40,59 +53,73 @@ These operations closely match respective operations available in hardware. \K{32} ~|~ \K{64} \\ \production{signedness} & \sx &::=& \K{u} ~|~ \K{s} \\ - \production{instructions} & \instr &::=& - \K{i}\X{nn}\K{.const}~\xref{syntax/values}{syntax-int}{\iX{\X{nn}}} ~|~ - \K{f}\X{nn}\K{.const}~\xref{syntax/values}{syntax-float}{\fX{\X{nn}}} ~|~ \\&&& - \K{i}\X{nn}\K{.eqz} ~|~ \\&&& - \K{i}\X{nn}\K{.eq} ~|~ - \K{i}\X{nn}\K{.ne} ~|~ - \K{i}\X{nn}\K{.lt\_}\sx ~|~ - \K{i}\X{nn}\K{.gt\_}\sx ~|~ - \K{i}\X{nn}\K{.le\_}\sx ~|~ - \K{i}\X{nn}\K{.ge\_}\sx ~|~ \\&&& - \K{f}\X{nn}\K{.eq} ~|~ - \K{f}\X{nn}\K{.ne} ~|~ - \K{f}\X{nn}\K{.lt} ~|~ - \K{f}\X{nn}\K{.gt} ~|~ - \K{f}\X{nn}\K{.le} ~|~ - \K{f}\X{nn}\K{.ge} ~|~ \\&&& - \K{i}\X{nn}\K{.clz} ~|~ - \K{i}\X{nn}\K{.ctz} ~|~ - \K{i}\X{nn}\K{.popcnt} ~|~ \\&&& - \K{i}\X{nn}\K{.add} ~|~ - \K{i}\X{nn}\K{.sub} ~|~ - \K{i}\X{nn}\K{.mul} ~|~ - \K{i}\X{nn}\K{.div\_}\sx ~|~ - \K{i}\X{nn}\K{.rem\_}\sx ~|~ \\&&& - \K{i}\X{nn}\K{.and} ~|~ - \K{i}\X{nn}\K{.or} ~|~ - \K{i}\X{nn}\K{.xor} ~|~ \\&&& - \K{i}\X{nn}\K{.shl} ~|~ - \K{i}\X{nn}\K{.shr\_}\sx ~|~ - \K{i}\X{nn}\K{.rotl} ~|~ - \K{i}\X{nn}\K{.rotr} ~|~ \\&&& - \K{f}\X{nn}\K{.abs} ~|~ - \K{f}\X{nn}\K{.neg} ~|~ - \K{f}\X{nn}\K{.sqrt} ~|~ \\&&& - \K{f}\X{nn}\K{.ceil} ~|~ - \K{f}\X{nn}\K{.floor} ~|~ - \K{f}\X{nn}\K{.trunc} ~|~ - \K{f}\X{nn}\K{.nearest} ~|~ \\&&& - \K{f}\X{nn}\K{.add} ~|~ - \K{f}\X{nn}\K{.sub} ~|~ - \K{f}\X{nn}\K{.mul} ~|~ - \K{f}\X{nn}\K{.div} ~|~ \\&&& - \K{f}\X{nn}\K{.min} ~|~ - \K{f}\X{nn}\K{.max} ~|~ - \K{f}\X{nn}\K{.copysign} ~|~ \\&&& - \K{i32.wrap/i64} ~|~ - \K{i64.extend\_}\sx/\K{i32} ~|~ - \K{i}\X{nn}\K{.trunc\_}\sx/\K{f}\X{mm} ~|~ \\&&& - \K{f32.demote/f64} ~|~ - \K{f64.promote/f32} ~|~ - \K{f}\X{nn}\K{.convert\_}\sx/\K{i}\X{mm} ~|~ \\&&& - \K{i}\X{nn}\K{.reinterpret/f}\X{nn} ~|~ - \K{f}\X{nn}\K{.reinterpret/i}\X{nn} \\ + \production{instruction} & \instr &::=& + \K{i}\X{nn}\K{.}\CONST~\xref{syntax/values}{syntax-int}{\iX{\X{nn}}} ~|~ + \K{f}\X{nn}\K{.}\CONST~\xref{syntax/values}{syntax-float}{\fX{\X{nn}}} ~|~ \\&&& + \K{i}\X{nn}\K{.}\iunop ~|~ + \K{f}\X{nn}\K{.}\funop ~|~ \\&&& + \K{i}\X{nn}\K{.}\ibinop ~|~ + \K{f}\X{nn}\K{.}\fbinop ~|~ \\&&& + \K{i}\X{nn}\K{.}\itestop ~|~ \\&&& + \K{i}\X{nn}\K{.}\irelop ~|~ + \K{f}\X{nn}\K{.}\frelop ~|~ \\&&& + \K{i32.}\WRAP\K{/i64} ~|~ + \K{i64.}\EXTEND\K{\_}\sx/\K{i32} ~|~ + \K{i}\X{nn}\K{.}\TRUNC\K{\_}\sx/\K{f}\X{mm} ~|~ \\&&& + \K{f32.}\TRUNC\K{/f64} ~|~ + \K{f64.}\PROMOTE\K{/f32} ~|~ + \K{f}\X{nn}\K{.}\CONVERT\K{\_}\sx/\K{i}\X{mm} ~|~ \\&&& + \K{i}\X{nn}\K{.}\REINTERPRET\K{/f}\X{nn} ~|~ + \K{f}\X{nn}\K{.}\REINTERPRET\K{/i}\X{nn} \\ + \production{integer unary operator} & \iunop &::=& + \K{clz} ~|~ + \K{ctz} ~|~ + \K{popcnt} \\ + \production{integer binary operator} & \ibinop &::=& + \K{add} ~|~ + \K{sub} ~|~ + \K{mul} ~|~ + \K{div\_}\sx ~|~ + \K{rem\_}\sx ~|~ \\&&& + \K{and} ~|~ + \K{or} ~|~ + \K{xor} ~|~ + \K{shl} ~|~ + \K{shr\_}\sx ~|~ + \K{rotl} ~|~ + \K{rotr} \\ + \production{floating-point unary operator} & \funop &::=& + \K{abs} ~|~ + \K{neg} ~|~ + \K{sqrt} ~|~ + \K{ceil} ~|~ + \K{floor} ~|~ + \K{trunc} ~|~ + \K{nearest} \\ + \production{floating-point binary operator} & \fbinop &::=& + \K{add} ~|~ + \K{sub} ~|~ + \K{mul} ~|~ + \K{div} ~|~ + \K{min} ~|~ + \K{max} ~|~ + \K{copysign} \\ + \production{integer test operator} & \itestop &::=& + \K{eqz} \\ + \production{integer relational operator} & \irelop &::=& + \K{eq} ~|~ + \K{ne} ~|~ + \K{lt\_}\sx ~|~ + \K{gt\_}\sx ~|~ + \K{le\_}\sx ~|~ + \K{ge\_}\sx \\ + \production{floating-point relational operator} & \frelop &::=& + \K{eq} ~|~ + \K{ne} ~|~ + \K{lt} ~|~ + \K{gt} ~|~ + \K{le} ~|~ + \K{ge} \\ \end{array} Numeric instructions are divided by :ref:`value type `. @@ -116,6 +143,28 @@ where a signedness annotation |sx| distinguishes whether the operands are to be For the other integer instructions, the use of 2's complement for the signed interpretation means that they behave the same regardless of signedness. +Conventions +........... + +Occasionally, it is convenient to group operators together according to the following grammar shorthands: + +.. math:: + \begin{array}{llll} + \production{unary operator} & \unop &::=& \iunop ~|~ \funop \\ + \production{binary operator} & \binop &::=& \ibinop ~|~ \fbinop \\ + \production{test operator} & \testop &::=& \itestop \\ + \production{relational operator} & \relop &::=& \irelop ~|~ \frelop \\ + \production{conversion operator} & \cvtop &::=& + \WRAP ~|~ + \EXTEND\K{\_}\sx ~|~ + \TRUNC\K{\_}\sx ~|~ + \CONVERT\K{\_}\sx ~|~ + \DEMOTE ~|~ + \PROMOTE ~|~ + \REINTERPRET \\ + \end{array} + + .. _syntax-instr-parametric: .. index:: ! parametric instruction pair: abstract syntax; instruction @@ -127,7 +176,7 @@ Instructions in this group can operate on operands of any :ref:`value type `. \begin{array}{llll} \production{memory immediate} & \memarg &::=& \{ \OFFSET~\u32, \ALIGN~\u32 \} \\ - \production{instructions} & \instr &::=& + \production{instruction} & \instr &::=& \dots ~|~ \\&&& - \K{i}\X{nn}\K{.load}~\memarg ~|~ - \K{f}\X{nn}\K{.load}~\memarg ~|~ \\&&& - \K{i}\X{nn}\K{.store}~\memarg ~|~ - \K{f}\X{nn}\K{.store}~\memarg ~|~ \\&&& - \K{i}\X{nn}\K{.load8\_}\sx~\memarg ~|~ - \K{i}\X{nn}\K{.load16\_}\sx~\memarg ~|~ - \K{i64.load32\_}\sx~\memarg ~|~ \\&&& - \K{i}\X{nn}\K{.store8}~\memarg ~|~ - \K{i}\X{nn}\K{.store16}~\memarg ~|~ - \K{i64.store32}~\memarg ~|~ \\&&& + \K{i}\X{nn}\K{.}\LOAD~\memarg ~|~ + \K{f}\X{nn}\K{.}\LOAD~\memarg ~|~ \\&&& + \K{i}\X{nn}\K{.}\STORE~\memarg ~|~ + \K{f}\X{nn}\K{.}\STORE~\memarg ~|~ \\&&& + \K{i}\X{nn}\K{.}\LOAD\K{8\_}\sx~\memarg ~|~ + \K{i}\X{nn}\K{.}\LOAD\K{16\_}\sx~\memarg ~|~ + \K{i64.}\LOAD\K{32\_}\sx~\memarg ~|~ \\&&& + \K{i}\X{nn}\K{.}\STORE\K{8}~\memarg ~|~ + \K{i}\X{nn}\K{.}\STORE\K{16}~\memarg ~|~ + \K{i64.}\STORE\K{32}~\memarg ~|~ \\&&& \CURRENTMEMORY ~|~ \\&&& \GROWMEMORY \\ \end{array} @@ -228,7 +279,7 @@ Instructions in this group affect the flow of control. .. math:: \begin{array}{llll} - \production{instructions} & \instr &::=& + \production{instruction} & \instr &::=& \dots ~|~ \\&&& \NOP ~|~ \\&&& \UNREACHABLE ~|~ \\&&& @@ -301,7 +352,7 @@ Expressions .. math:: \begin{array}{llll} - \production{expressions} & \expr &::=& + \production{expression} & \expr &::=& \instr^\ast~\END \\ \end{array} diff --git a/document/syntax/modules.rst b/document/syntax/modules.rst index 2b5036bdd6..d879612f92 100644 --- a/document/syntax/modules.rst +++ b/document/syntax/modules.rst @@ -13,7 +13,7 @@ and provide initialization logic in the form of :ref:`data ` and :r .. math:: \begin{array}{lllll} - \production{modules} & \module &::=& \{ & + \production{module} & \module &::=& \{ & \TYPES~\vec(\functype), \\&&&& \FUNCS~\vec(\func), \\&&&& \TABLES~\vec(\table), \\&&&& @@ -61,13 +61,13 @@ Each class of definition has its own *index space*, as distinguished by the foll .. math:: \begin{array}{llll} - \production{type indices} & \typeidx &::=& \u32 \\ - \production{function indices} & \funcidx &::=& \u32 \\ - \production{table indices} & \tableidx &::=& \u32 \\ - \production{memory indices} & \memidx &::=& \u32 \\ - \production{global indices} & \globalidx &::=& \u32 \\ - \production{local indices} & \localidx &::=& \u32 \\ - \production{label indices} & \labelidx &::=& \u32 \\ + \production{type index} & \typeidx &::=& \u32 \\ + \production{function index} & \funcidx &::=& \u32 \\ + \production{table index} & \tableidx &::=& \u32 \\ + \production{memory index} & \memidx &::=& \u32 \\ + \production{global index} & \globalidx &::=& \u32 \\ + \production{local index} & \localidx &::=& \u32 \\ + \production{label index} & \labelidx &::=& \u32 \\ \end{array} The index space for functions, tables, memories and globals includes respective imports declared in the same module. @@ -114,7 +114,7 @@ The |FUNCS| component of a module defines a vector of *functions* with the follo .. math:: \begin{array}{llll} - \production{functions} & \func &::=& + \production{function} & \func &::=& \{ \TYPE~\typeidx, \LOCALS~\vec(\valtype), \BODY~\expr \} \\ \end{array} @@ -142,7 +142,7 @@ The |TABLES| component of a module defines a vector of *tables* described by the .. math:: \begin{array}{llll} - \production{tables} & \table &::=& + \production{table} & \table &::=& \{ \TYPE~\tabletype \} \\ \end{array} @@ -172,7 +172,7 @@ The |MEMS| component of a module defines a vector of *linear memories* (or *memo .. math:: \begin{array}{llll} - \production{memories} & \mem &::=& + \production{memory} & \mem &::=& \{ \TYPE~\memtype \} \\ \end{array} @@ -203,7 +203,7 @@ The |GLOBALS| component of a module defines a vector of *global variables* (or * .. math:: \begin{array}{llll} - \production{globals} & \global &::=& + \production{global} & \global &::=& \{ \TYPE~\globaltype, \INIT~\expr \} \\ \end{array} @@ -229,7 +229,7 @@ The |ELEM| component of a module defines a vector of *element segments* that ini .. math:: \begin{array}{llll} - \production{element segments} & \elem &::=& + \production{element segment} & \elem &::=& \{ \TABLE~\tableidx, \OFFSET~\expr, \INIT~\vec(\funcidx) \} \\ \end{array} @@ -254,7 +254,7 @@ The |DATA| component of a module defines a vector of *data segments* that initia .. math:: \begin{array}{llll} - \production{data segments} & \data &::=& + \production{data segment} & \data &::=& \{ \MEM~\memidx, \OFFSET~\expr, \INIT~\vec(\byte) \} \\ \end{array} @@ -276,7 +276,7 @@ The |START| component of a module optionally declares the :ref:`function index < .. math:: \begin{array}{llll} - \production{start functions} & \start &::=& + \production{start function} & \start &::=& \{ \FUNC~\funcidx \} \\ \end{array} @@ -296,9 +296,9 @@ The |EXPORTS| component of a module defines a set of *exports* that become acces .. math:: \begin{array}{llll} - \production{exports} & \export &::=& + \production{export} & \export &::=& \{ \NAME~\name, \DESC~\exportdesc \} \\ - \production{export descriptions} & \exportdesc &::=& + \production{export description} & \exportdesc &::=& \FUNC~\funcidx ~|~ \\&&& \TABLE~\tableidx ~|~ \\&&& \MEM~\memidx ~|~ \\&&& @@ -313,6 +313,20 @@ which are referenced through a respective descriptor. In the current version of WebAssembly, only *immutable* globals may be exported. +Conventions +........... + +The following auxiliary notation is defined for sequences of exports, filtering out indices of a specific kind in an order-preserving fashion: + +* :math:`\funcs(\export^\ast) = [\funcidx ~|~ \FUNC~\funcidx \in (\export.\DESC)^\ast]` + +* :math:`\tables(\export^\ast) = [\tableidx ~|~ \TABLE~\tableidx \in (\export.\DESC)^\ast]` + +* :math:`\mems(\export^\ast) = [\memidx ~|~ \MEM~\memidx \in (\export.\DESC)^\ast]` + +* :math:`\globals(\export^\ast) = [\globalidx ~|~ \GLOBAL~\globalidx \in (\export.\DESC)^\ast]` + + .. _syntax-import: .. index:: ! import, name, function type, table type, memory type, global type, index, index space, type index, function index, table index, memory index, global index, function, table, memory, global, instantiation pair: abstract syntax; import @@ -328,9 +342,9 @@ The |IMPORTS| component of a module defines a set of *imports* that are required .. math:: \begin{array}{llll} - \production{imports} & \import &::=& + \production{import} & \import &::=& \{ \MODULE~\name, \NAME~\name, \DESC~\importdesc \} \\ - \production{import descriptions} & \importdesc &::=& + \production{import description} & \importdesc &::=& \FUNC~\typeidx ~|~ \\&&& \TABLE~\tabletype ~|~ \\&&& \MEM~\memtype ~|~ \\&&& diff --git a/document/syntax/types.rst b/document/syntax/types.rst index 262da63e24..bb8927d0ba 100644 --- a/document/syntax/types.rst +++ b/document/syntax/types.rst @@ -18,7 +18,7 @@ Value Types .. math:: \begin{array}{llll} - \production{value types} & \valtype &::=& + \production{value type} & \valtype &::=& \I32 ~|~ \I64 ~|~ \F32 ~|~ \F64 \\ \end{array} @@ -50,7 +50,7 @@ which is a sequence of values. .. math:: \begin{array}{llll} - \production{result types} & \resulttype &::=& + \production{result type} & \resulttype &::=& [\valtype^?] \\ \end{array} @@ -72,7 +72,7 @@ mapping a vector of parameters to a vector of results. .. math:: \begin{array}{llll} - \production{function types} & \functype &::=& + \production{function type} & \functype &::=& [\vec(\valtype)] \to [\vec(\valtype)] \\ \end{array} @@ -115,7 +115,7 @@ Memory Types .. math:: \begin{array}{llll} - \production{memory types} & \memtype &::=& + \production{memory type} & \memtype &::=& \limits \\ \end{array} @@ -139,9 +139,9 @@ Table Types .. math:: \begin{array}{llll} - \production{table types} & \tabletype &::=& + \production{table type} & \tabletype &::=& \limits~\elemtype \\ - \production{element types} & \elemtype &::=& + \production{element type} & \elemtype &::=& \ANYFUNC \\ \end{array} @@ -170,43 +170,9 @@ Global Types .. math:: \begin{array}{llll} - \production{global types} & \globaltype &::=& + \production{global type} & \globaltype &::=& \mut^?~\valtype \\ \production{mutability} & \mut &::=& - \CONST ~|~ - \MUT \\ + \MCONST ~|~ + \MVAR \\ \end{array} - - -.. _syntax-externtype: -.. index:: ! external type, function type, table type, memory type, global type - pair: abstract syntax; external type - pair: external; type - -External Types -~~~~~~~~~~~~~~ - -*External types* classify imports and exports and their respective types. - -.. math:: - \begin{array}{llll} - \production{external types} & \externtype &::=& - \FUNC~\functype ~|~ \\&&& - \TABLE~\tabletype ~|~ \\&&& - \MEM~\memtype ~|~ \\&&& - \GLOBAL~\globaltype \\ - \end{array} - - -Conventions -........... - -The following auxiliary notation is defined for sequences of external types, filtering out entries of a specific kind in an order-preserving fashion: - -* :math:`\funcs(\externtype^\ast) = [\functype ~|~ \FUNC~\functype \in \externtype^\ast]` - -* :math:`\tables(\externtype^\ast) = [\tabletype ~|~ \TABLE~\tabletype \in \externtype^\ast]` - -* :math:`\mems(\externtype^\ast) = [\memtype ~|~ \MEM~\memtype \in \externtype^\ast]` - -* :math:`\globals(\externtype^\ast) = [\globaltype ~|~ \GLOBAL~\globaltype \in \externtype^\ast]` diff --git a/document/syntax/values.rst b/document/syntax/values.rst index 6093043380..faa1aa2017 100644 --- a/document/syntax/values.rst +++ b/document/syntax/values.rst @@ -18,7 +18,7 @@ In the abstract syntax they are represented as hexadecimal literals. .. math:: \begin{array}{llll} - \production{bytes} & \byte &::=& + \production{byte} & \byte &::=& \hex{00} ~|~ \dots ~|~ \hex{FF} \\ \end{array} @@ -50,20 +50,17 @@ Different classes of *integers* with different value ranges are distinguished by .. math:: \begin{array}{llll} - \production{unsigned integers} & \uN &::=& + \production{unsigned integer} & \uN &::=& 0 ~|~ 1 ~|~ \dots ~|~ 2^N{-}1 \\ - \production{signed integers} & \sN &::=& + \production{signed integer} & \sN &::=& -2^{N-1} ~|~ \dots ~|~ {-}1 ~|~ 0 ~|~ 1 ~|~ \dots ~|~ 2^{N-1}{-}1 \\ - \production{uninterpreted integers} & \iN &::=& - \uN ~|~ \sN \\ + \production{uninterpreted integer} & \iN &::=& + \uN \\ \end{array} The latter class defines *uninterpreted* integers, whose signedness interpretation can vary depending on context. -In those contexts, a conversion based on 2's complement will be applied for values that are out-of-range for a chosen interpretation. -That is, semantically, when interpreted as unsigned, negative values :math:`-n` convert to :math:`2^N-n`, -and when interpreted as signed, positive values :math:`n \geq 2^{N-1}` convert to :math:`n-2^N`. - -.. todo:: once there, link to definition of conversion +In the abstract syntax, they are represented as unsigned. +However, some operations :ref:`convert ` them to signed based on a 2's complement interpretation. Conventions @@ -85,7 +82,7 @@ Floating-Point .. math:: \begin{array}{llll} - \production{floating-point numbers} & \fN &::=& + \production{floating-point number} & \fN &::=& \byte^{N/8} \\ \end{array} @@ -105,7 +102,7 @@ A vector can have at most :math:`2^{32}-1` elements. .. math:: \begin{array}{lllll} - \production{vectors} & \vec(A) &::=& + \production{vector} & \vec(A) &::=& A^n & (n < 2^{32})\\ \end{array} @@ -122,9 +119,9 @@ Names .. math:: \begin{array}{llll} - \production{names} & \name &::=& + \production{name} & \name &::=& \codepoint^\ast \\ - \production{code points} & \codepoint &::=& + \production{code point} & \codepoint &::=& \unicode{0000} ~|~ \dots ~|~ \unicode{D7FF} ~|~ \unicode{E000} ~|~ \dots ~|~ \unicode{10FFFF} \\ \end{array} diff --git a/document/validation/conventions.rst b/document/validation/conventions.rst index f05c46b2b2..d1f3633574 100644 --- a/document/validation/conventions.rst +++ b/document/validation/conventions.rst @@ -39,10 +39,11 @@ which collects relevant information about the surrounding :ref:`module ` for each :ref:`index space `, describing each defined entry in that space. -Locals and labels are only used for validating :ref:`instructions ` in :ref:`function bodies `, and are left empty elsewhere. +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: @@ -57,7 +58,8 @@ It is convenient to define contexts as :ref:`records ` :math:`C` & \MEMS & \memtype^\ast, \\ & \GLOBALS & \globaltype^\ast, \\ & \LOCALS & \valtype^\ast, \\ - & \LABELS & \resulttype^\ast ~\} \\ + & \LABELS & \resulttype^\ast, \\ + & \LRETURN & \resulttype^? ~\} \\ \end{array} \end{array} @@ -79,27 +81,35 @@ In addition to field access :math:`C.\K{field}` the following notation is adopte because the :ref:`label index ` space is indexed relatively, that is, in reverse order of addition. +.. _valid-notation-textual: + Textual Notation ~~~~~~~~~~~~~~~~ Validation is specified by stylised rules for each relevant part of the :ref:`abstract syntax `. The rules not only state constraints defining when a phrase is valid, they also classify it with a type. -A phrase :math:`A` is said to be "valid with type :math:`T`", -if all constraints expressed by the respective rules are met. -The form of :math:`T` depends on what :math:`A` is. +The following conventions are adopted in stating these rules. -.. note:: - For example, if :math:`A` is a :ref:`function `, - then :math:`T` is a :ref:`function type `; - for an :math:`A` that is a :ref:`global `, - :math:`T` is a :ref:`global type `; - and so on. +* A phrase :math:`A` is said to be "valid with type :math:`T`" + if and only if all constraints expressed by the respective rules are met. + The form of :math:`T` depends on what :math:`A` is. + + .. note:: + For example, if :math:`A` is a :ref:`function `, + then :math:`T` is a :ref:`function type `; + for an :math:`A` that is a :ref:`global `, + :math:`T` is a :ref:`global type `; + and so on. + +* The rules implicitly assume a given :ref:`context ` :math:`C`. + +* In some places, this context is locally extended to a context :math:`C'` with additional entries. + The formulation "Under context :math:`C'`, ... *statement* ..." is adopted to express that the following statement must apply under the assumptions embodied in the extended context. -The rules implicitly assume a given :ref:`context ` :math:`C`. -In some places, this context is locally extended to a context :math:`C'` with additional entries. -The formulation "Under context :math:`C'`, ... *statement* ..." is adopted to express that the following statement must apply under the assumptions embodied in the extended context. +.. _valid-notation: +.. index:: ! typing rules Formal Notation ~~~~~~~~~~~~~~~ @@ -129,7 +139,7 @@ The conclusion always is a judgment :math:`C \vdash A : T`, and there is one respective rule for each relevant construct :math:`A` of the abstract syntax. .. note:: - For example, the typing rule for the :ref:`instruction ` :math:`\I32.\ADD` can be given as an axiom: + For example, the typing rule for the :math:`\I32.\ADD` instruction can be given as an axiom: .. math:: \frac{ @@ -145,7 +155,7 @@ and there is one respective rule for each relevant construct :math:`A` of the ab .. math:: \frac{ - C.\LOCAL[x] = t + C.\LOCALS[x] = t }{ C \vdash \GETLOCAL~x : [] \to [t] } @@ -153,7 +163,7 @@ and there is one respective rule for each relevant construct :math:`A` of the ab Here, the premise enforces that the immediate :ref:`local index ` :math:`x` exists in the context. The instruction produces a value of its respective type :math:`t` (and does not consume any values). - If :math:`C.\LOCAL[x]` does not exist then the premise does not hold, + If :math:`C.\LOCALS[x]` does not exist then the premise does not hold, and the instruction is ill-typed. Finally, a :ref:`structured ` instruction requires diff --git a/document/validation/instructions.rst b/document/validation/instructions.rst index 918dd03cc2..3cd9d04a18 100644 --- a/document/validation/instructions.rst +++ b/document/validation/instructions.rst @@ -70,65 +70,9 @@ In both cases, the unconstrained types or type sequences can be chosen arbitrari Numeric Instructions ~~~~~~~~~~~~~~~~~~~~ -In this section, the following grammar shorthands are adopted: - -.. math:: - \begin{array}{llll} - \production{unary operators} & \unop &::=& - \CLZ ~|~ - \CTZ ~|~ - \POPCNT ~|~ - \ABS ~|~ - \NEG ~|~ - \SQRT ~|~ - \CEIL ~|~ - \FLOOR ~|~ - \TRUNC ~|~ - \NEAREST \\ - \production{binary operators} & \binop &::=& - \ADD ~|~ - \SUB ~|~ - \MUL ~|~ - \DIV ~|~ - \DIV\K{\_}\sx ~|~ - \REM\K{\_}\sx ~|~ - \FMIN ~|~ - \FMAX ~|~ - \COPYSIGN ~|~ \\&&& - \AND ~|~ - \OR ~|~ - \XOR ~|~ - \SHL ~|~ - \SHR\K{\_}\sx ~|~ - \ROTL ~|~ - \ROTR \\ - \production{test operators} & \testop &::=& - \EQZ \\ - \production{relational operators} & \relop &::=& - \EQ ~|~ - \NE ~|~ - \LT ~|~ - \GT ~|~ - \LE ~|~ - \GE ~|~ - \LT\K{\_}\sx ~|~ - \GT\K{\_}\sx ~|~ - \LE\K{\_}\sx ~|~ - \GE\K{\_}\sx \\ - \production{conversion operators} & \cvtop &::=& - \WRAP ~|~ - \EXTEND\K{\_}\sx ~|~ - \TRUNC\K{\_}\sx ~|~ - \CONVERT\K{\_}\sx ~|~ - \DEMOTE ~|~ - \PROMOTE ~|~ - \REINTERPRET \\ - \end{array} - - .. _valid-const: -:math:`t \K{.const}~c` +:math:`t\K{.}\CONST~c` ...................... * The instruction is valid with type :math:`[] \to [t]`. @@ -136,7 +80,7 @@ In this section, the following grammar shorthands are adopted: .. math:: \frac{ }{ - C \vdash t\K{.const}~c : [] \to [t] + C \vdash t\K{.}\CONST~c : [] \to [t] } @@ -321,7 +265,7 @@ Variable Instructions * The global :math:`C.\GLOBALS[x]` must be defined in the context. -* Let :math:`\mut~t` be the :ref:`value type ` :math:`C.\LOCALS[x]`. +* Let :math:`\mut~t` be the :ref:`global type ` :math:`C.\GLOBALS[x]`. * Then the instruction is valid with type :math:`[] \to [t]`. @@ -342,13 +286,13 @@ Variable Instructions * Let :math:`\mut~t` be the :ref:`global type ` :math:`C.\GLOBALS[x]`. -* The mutability :math:`\mut` must be |MUT|. +* The mutability :math:`\mut` must be |MVAR|. * Then the instruction is valid with type :math:`[t] \to []`. .. math:: \frac{ - C.\GLOBALS[x] = \MUT~t + C.\GLOBALS[x] = \MVAR~t }{ C \vdash \SETGLOBAL~x : [t] \to [] } @@ -365,8 +309,8 @@ Memory Instructions .. _valid-load: -:math:`t\K{.load}~\memarg` -.......................... +:math:`t\K{.}\LOAD~\memarg` +........................... * The memory :math:`C.\MEMS[0]` must be defined in the context. @@ -386,8 +330,8 @@ Memory Instructions .. _valid-loadn: -:math:`t\K{.load}N\K{\_}\sx~\memarg` -.................................... +:math:`t\K{.}\LOAD{N}\K{\_}\sx~\memarg` +....................................... * The memory :math:`C.\MEMS[0]` must be defined in the context. @@ -407,8 +351,8 @@ Memory Instructions .. _valid-store: -:math:`t\K{.store}~\memarg` -........................... +:math:`t\K{.}\STORE~\memarg` +............................ * The memory :math:`C.\MEMS[0]` must be defined in the context. @@ -428,8 +372,8 @@ Memory Instructions .. _valid-storen: -:math:`t\K{.store}N~\memarg` -............................ +:math:`t\K{.}\STORE{N}~\memarg` +............................... * The memory :math:`C.\MEMS[0]` must be defined in the context. @@ -674,15 +618,15 @@ Control Instructions :math:`\RETURN` ............... -* The label vector :math:`C.\LABELS` must not be empty in the context. +* The return type :math:`C.\LRETURN` must not be empty in the context. -* Let :math:`[t^?]` be the :ref:`result type ` that is the last element of :math:`C.\LABELS`. +* Let :math:`[t^?]` be the :ref:`result type ` of :math:`C.\LRETURN`. * Then the instruction is valid with type :math:`[t_1^\ast~t^?] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. .. math:: \frac{ - C.\LABELS[|C.\LABELS|-1] = [t^?] + C.\LRETURN = [t^?] }{ C \vdash \RETURN : [t_1^\ast~t^?] \to [t_2^\ast] } @@ -690,6 +634,10 @@ Control Instructions .. note:: The |RETURN| instruction is :ref:`stack-polymorphic `. + :math:`C.\LRETURN` is empty (:math:`\epsilon`) when validating an 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. + .. _valid-call: @@ -734,7 +682,7 @@ Control Instructions .. _valid-instr-seq: -.. index:: instruction +.. index:: instruction, instruction sequence Instruction Sequences ~~~~~~~~~~~~~~~~~~~~~ diff --git a/document/validation/modules.rst b/document/validation/modules.rst index a1e26da4a5..0fcab62e1d 100644 --- a/document/validation/modules.rst +++ b/document/validation/modules.rst @@ -51,9 +51,11 @@ Functions :math:`\func` are classified by :ref:`function types * Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with: - * the |LOCALS| set to the sequence of :ref:`value types ` :math:`t_1^\ast~t^\ast`, concatenating parameters and locals, + * |LOCALS| set to the sequence of :ref:`value types ` :math:`t_1^\ast~t^\ast`, concatenating parameters and locals, - * the |LABELS| set to the singular sequence containing only :ref:`result type ` :math:`[t_2^\ast]`. + * |LABELS| set to the singular sequence containing only :ref:`result type ` :math:`[t_2^\ast]`. + + * |LRETURN| set to the :ref:`result type ` :math:`[t_2^\ast]`. * Under the context :math:`C'`, the expression :math:`\expr` must be valid with type :math:`t_2^\ast`. @@ -64,7 +66,7 @@ Functions :math:`\func` are classified by :ref:`function types \frac{ C.\TYPES[x] = [t_1^\ast] \to [t_2^?] \qquad - C,\LOCALS\,t_1^\ast~t^\ast,\LABELS~[t_2^?] \vdash \expr : [t_2^?] + C,\LOCALS\,t_1^\ast~t^\ast,\LRETURN~[t_2^?] \vdash \expr : [t_2^?] }{ C \vdash \{ \TYPE~x, \LOCALS~t^\ast, \BODY~\expr \} : [t_1^\ast] \to [t_2^?] } @@ -343,13 +345,13 @@ Export descriptions :math:`\exportdesc` are not classified by any type. * Let :math:`\mut~t` be the :ref:`global type ` :math:`C.\GLOBALS[x]`. -* The mutability :math:`\mut` must be |CONST|. +* The mutability :math:`\mut` must be |MCONST|. * Then the export description is valid. .. math:: \frac{ - C.\GLOBALS[x] = \CONST~t + C.\GLOBALS[x] = \MCONST~t }{ C \vdash \GLOBAL~x ~\F{ok} } @@ -436,14 +438,14 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi :math:`\GLOBAL~\mut~t` ...................... -* The mutability :math:`\mut` must be |CONST|. +* The mutability :math:`\mut` must be |MCONST|. * Then the import description is valid with type :math:`\GLOBAL~t`. .. math:: \frac{ }{ - C \vdash \GLOBAL~\CONST~t : \GLOBAL~\CONST~t + C \vdash \GLOBAL~\MCONST~t : \GLOBAL~\MCONST~t } @@ -482,6 +484,8 @@ Instead, the context :math:`C` for validation of the module's content is constru * :math:`C.\LABELS` is empty. + * :math:`C.\LRETURN` is empty. + * Under the context :math:`C`: * For each :math:`\func_i` in :math:`\module.\FUNCS`, @@ -530,7 +534,7 @@ Instead, the context :math:`C` for validation of the module's content is constru \quad (C \vdash \mem : \X{mt})^\ast \quad - (C_i \vdash \global : \X{gt})_i^\ast + (C' \vdash \global : \X{gt})^\ast \\ (C \vdash \elem ~\F{ok})^\ast \quad @@ -552,13 +556,13 @@ Instead, the context :math:`C` for validation of the module's content is constru \\ C = \{ \TYPES~\functype^\ast, \FUNCS~\X{ift}^\ast~\X{ft}^\ast, \TABLES~\X{itt}^\ast~\X{tt}^\ast, \MEMS~\X{imt}^\ast~\X{mt}^\ast, \GLOBALS~\X{igt}^\ast~\X{gt}^\ast \} \\ + C' = \{ \GLOBALS~\X{igt}^\ast \} + \qquad |C.\TABLES| \leq 1 \qquad |C.\MEMS| \leq 1 \qquad \name^\ast ~\F{disjoint} - \qquad - (C_i = \{ \GLOBALS~[\X{igt}^\ast~\X{gt}^{i-1}] \})_i^\ast \end{array} }{ \vdash \{ @@ -585,7 +589,7 @@ Instead, the context :math:`C` for validation of the module's content is constru All types needed to construct :math:`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. - The effect of defining the limited contexts :math:`C_i` for validating the module's globals is that their initialization expressions can only access imported and previously defined globals and nothing else. + The effect of defining the limited context :math:`C'` for validating the module's globals is that their initialization expressions can only access imported globals and nothing else. .. note:: The restriction on the number of tables and memories may be lifted in future versions of WebAssembly. From 1a70dfe5636848228d079f6a5d77bb690807da25 Mon Sep 17 00:00:00 2001 From: rossberg-chromium Date: Thu, 27 Apr 2017 11:27:48 +0200 Subject: [PATCH 2/8] Tweaks --- document/binary/values.rst | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/document/binary/values.rst b/document/binary/values.rst index 6a1e98a4f0..8a4366501c 100644 --- a/document/binary/values.rst +++ b/document/binary/values.rst @@ -67,12 +67,12 @@ As an additional constraint, the total number of bytes encoding a value of type 2^7\cdot m + (n-2^7) & (n \geq 2^7 \wedge N > 7) \\ \end{array} -:ref:`Uninterpreted integers ` are always encoded as signed integers. +:ref:`Uninterpreted integers ` are encoded as signed integers. .. math:: \begin{array}{llclll@{\qquad\qquad}l} \production{uninterpreted integer} & \BiX{N} &::=& - n{:}\BsX{N} &\Rightarrow& n + n{:}\BsX{N} &\Rightarrow& i & (n = \signed_{\iX{N}}(i)) \end{array} .. note:: From 66c0af76d46cf9ae37d5f963a995577ec69d8ae1 Mon Sep 17 00:00:00 2001 From: Andreas Rossberg Date: Thu, 27 Apr 2017 19:27:35 +0200 Subject: [PATCH 3/8] Oops, forgot to add new files --- document/execution/conventions.rst | 131 ++++ document/execution/instructions.rst | 1051 +++++++++++++++++++++++++++ document/execution/modules.rst | 5 + document/execution/numerics.rst | 52 ++ document/execution/runtime.rst | 518 +++++++++++++ document/syntax/conventions.rst | 6 +- 6 files changed, 1759 insertions(+), 4 deletions(-) create mode 100644 document/execution/conventions.rst create mode 100644 document/execution/instructions.rst create mode 100644 document/execution/modules.rst create mode 100644 document/execution/numerics.rst create mode 100644 document/execution/runtime.rst diff --git a/document/execution/conventions.rst b/document/execution/conventions.rst new file mode 100644 index 0000000000..fb93b2a7b7 --- /dev/null +++ b/document/execution/conventions.rst @@ -0,0 +1,131 @@ +.. index:: ! execution, stack, store + +Conventions +----------- + +WebAssembly code is *executed* when :ref:`instantiating ` a module or :ref:`invoking ` a function on the resulting module instance. + +Execution behavior is defined in terms of an *abstract machine* that models the *program state*. +It includes a *stack*, which records operand values and control constructs, and an abstract *store* containing global state. + +For each instruction, there is a rule that specifies the effect of its execution on the program state. +Furthermore, there are rules describing the instantiation of a module. +As with :ref:`validation `, all rules are given in two *equivalent* forms: + +1. In *prose*, describing the execution in intuitive form. +2. In *formal notation*, describing the rule in mathematical form. + +.. note:: + As with validation, the prose and formal rules are equivalent, + so that understanding of the formal notation is *not* required to read this specification. + The formalism offers a more concise description in notation that is used widely in programming languages semantics and is readily amenable to mathematical proof. + +:ref:`Store `, :ref:`stack `, and other *runtime structure*, such as :ref:`module instances `, are made precise in terms of additional auxiliary :ref:`syntax `. + + +.. _exec-notation-textual: + +Textual Notation +~~~~~~~~~~~~~~~~ + +Execution is specified by stylised, step-wise rules for each :ref:`instruction ` of the :ref:`abstract syntax `. +The following conventions are adopted in stating these rules. + +* The execution rules implicitly assume a given :ref:`store ` :math:`S`. + +* The execution rules also assume the presence of an implicit :ref:`stack ` + that is modified by *pushing* or *popping* + :ref:`values `, :ref:`labels `, and :ref:`frames `. + +* Certain rules require the stack to contain at least one frame, + which is referred to as the *current* frame. + +* Both the store and the current frame are mutated by *replacing* some of its components. + Such replacement is assumed to apply globally. + +* The execution of an instruction may *trap*, + in which case the entire computation is aborted and no further modifications to the store are performed by it. + +* The execution of an instruction may also end in a *jump* to a designated target, + which defines the next instruction to execute. + +* Execution can *enter* and *exit* :ref:`instruction sequences ` in a block-like fashion. + +* :ref:`Instruction sequences ` are implicitly executed in order, unless a trap or jump occurs. + +* In various places the rules contain *assertions* expressing crucial invariants about the program state, with indications why these are known to hold. + + +.. _exec-notation: +.. index:: ! reduction rules, ! configuration + +Formal Notation +~~~~~~~~~~~~~~~ + +.. note:: + This section gives a brief explanation of the notation for specifying execution formally. + For the interested reader, a more thorough introduction can be found in respective text books. [#tapl]_ + +The formal execution rules use a standard approach for specifying operational semantics, rendering them into *reduction rules*. +Every rule has the following general form: + +.. math:: + \X{configuration} \quad\stepto\quad \X{configuration} + +A *configuration* is a syntactic description of a specific program state. +Each rule specifies one *step* of execution. +As long as there is at most one reduction rule applicable to a given configuration, reduction -- and thereby execution -- is *deterministic*. +WebAssembly has only very few exceptions to this, which are noted explicitly in this specification. + +For WebAssembly, a configuration is a tuple :math:`(S; F; \instr^\ast)` consisting of the current :ref:`store ` :math:`S`, the :ref:`call frame ` :math:`F` of the current function, and the sequence of :ref:`instructions ` that is to be executed. + +To avoid unnecessary clutter, the store :math:`S` and the frame :math:`F` are omitted from reduction rules that do not touch them. + +There is no separate representation of the :ref:`stack `. +Instead, it is conveniently represented as part of the configuration's instruction sequence. +In particular, :ref:`values ` are defined to coincide with |CONST| instructions, +and a sequence of |CONST| instructions can be interpreted as an operand "stack". + +.. note:: + For example, the :ref:`reduction rule ` for the :math:`\I32.\ADD` instruction could be given as follows: + + .. math:: + (\I32.\CONST~n_1)~(\I32.\CONST~n_2)~\I32.\ADD \quad\stepto\quad (\I32.\CONST~(n_1 + n_2) \mod 2^{32}) + + Per this rule, two |CONST| instructions and the |ADD| instruction itself are removed from the instruction stream and replaced with one new |CONST| instruction. + This can be interpreted as popping two value off the stack and pushing the result. + + When no result is produced, an instruction reduces to the empty sequence: + + .. math:: + \NOP \quad\stepto\quad \epsilon + +:ref:`Labels