diff --git a/document/core/appendix/index-instructions.py b/document/core/appendix/index-instructions.py index a433bf5b4..9de5a110f 100755 --- a/document/core/appendix/index-instructions.py +++ b/document/core/appendix/index-instructions.py @@ -54,8 +54,7 @@ def RefWrap(s, kind): def Instruction(name, opcode, type=None, validation=None, execution=None, operator=None): if operator: - execution_str = ', '.join([RefWrap(execution, 'execution'), - RefWrap(operator, 'operator')]) + execution_str = RefWrap(execution, 'execution') + ' (' + RefWrap(operator, 'operator') + ')' else: execution_str = RefWrap(execution, 'execution') diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index c3ac55001..637b002d8 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -20,16 +20,15 @@ The mapping of numeric instructions to their underlying operators is expressed b .. math:: \begin{array}{lll@{\qquad}l} - \X{op}_{\IN}(i_1,\dots,i_k) &=& \F{i}\X{op}_N(i_1,\dots,i_k) \\ - \X{op}_{\FN}(z_1,\dots,z_k) &=& \F{f}\X{op}_N(z_1,\dots,z_k) \\ - \X{op}_{\VN}(i_1,\dots,i_k) &=& \F{i}\X{op}_N(i_1,\dots,i_k) \\ + \X{op}_{\IN}(i_1,\dots,i_k) &=& \xref{exec/numerics}{int-ops}{\F{i}\X{op}}_N(i_1,\dots,i_k) \\ + \X{op}_{\FN}(z_1,\dots,z_k) &=& \xref{exec/numerics}{float-ops}{\F{f}\X{op}}_N(z_1,\dots,z_k) \\ \end{array} And for :ref:`conversion operators `: .. math:: \begin{array}{lll@{\qquad}l} - \X{cvtop}^{\sx^?}_{t_1,t_2}(c) &=& \X{cvtop}^{\sx^?}_{|t_1|,|t_2|}(c) \\ + \cvtop^{\sx^?}_{t_1,t_2}(c) &=& \xref{exec/numerics}{convert-ops}{\X{cvtop}}^{\sx^?}_{|t_1|,|t_2|}(c) \\ \end{array} Where the underlying operators are partial, the corresponding instruction will :ref:`trap ` when the result is not defined. @@ -64,9 +63,9 @@ Where the underlying operators are non-deterministic, because they may return on 2. Pop the value :math:`t.\CONST~c_1` from the stack. -3. If :math:`\unop_t(c_1)` is defined, then: +3. If :math:`\unopF_t(c_1)` is defined, then: - a. Let :math:`c` be a possible result of computing :math:`\unop_t(c_1)`. + a. Let :math:`c` be a possible result of computing :math:`\unopF_t(c_1)`. b. Push the value :math:`t.\CONST~c` to the stack. @@ -77,9 +76,9 @@ Where the underlying operators are non-deterministic, because they may return on .. math:: \begin{array}{lcl@{\qquad}l} (t\K{.}\CONST~c_1)~t\K{.}\unop &\stepto& (t\K{.}\CONST~c) - & (\iff c \in \unop_t(c_1)) \\ + & (\iff c \in \unopF_t(c_1)) \\ (t\K{.}\CONST~c_1)~t\K{.}\unop &\stepto& \TRAP - & (\iff \unop_{t}(c_1) = \{\}) + & (\iff \unopF_{t}(c_1) = \{\}) \end{array} @@ -94,9 +93,9 @@ Where the underlying operators are non-deterministic, because they may return on 3. Pop the value :math:`t.\CONST~c_1` from the stack. -4. If :math:`\binop_t(c_1, c_2)` is defined, then: +4. If :math:`\binopF_t(c_1, c_2)` is defined, then: - a. Let :math:`c` be a possible result of computing :math:`\binop_t(c_1, c_2)`. + a. Let :math:`c` be a possible result of computing :math:`\binopF_t(c_1, c_2)`. b. Push the value :math:`t.\CONST~c` to the stack. @@ -107,9 +106,9 @@ Where the underlying operators are non-deterministic, because they may return on .. math:: \begin{array}{lcl@{\qquad}l} (t\K{.}\CONST~c_1)~(t\K{.}\CONST~c_2)~t\K{.}\binop &\stepto& (t\K{.}\CONST~c) - & (\iff c \in \binop_t(c_1,c_2)) \\ + & (\iff c \in \binopF_t(c_1,c_2)) \\ (t\K{.}\CONST~c_1)~(t\K{.}\CONST~c_2)~t\K{.}\binop &\stepto& \TRAP - & (\iff \binop_{t}(c_1,c_2) = \{\}) + & (\iff \binopF_{t}(c_1,c_2) = \{\}) \end{array} @@ -122,14 +121,14 @@ Where the underlying operators are non-deterministic, because they may return on 2. Pop the value :math:`t.\CONST~c_1` from the stack. -3. Let :math:`c` be the result of computing :math:`\testop_t(c_1)`. +3. Let :math:`c` be the result of computing :math:`\testopF_t(c_1)`. 4. Push the value :math:`\I32.\CONST~c` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} (t\K{.}\CONST~c_1)~t\K{.}\testop &\stepto& (\I32\K{.}\CONST~c) - & (\iff c = \testop_t(c_1)) \\ + & (\iff c = \testopF_t(c_1)) \\ \end{array} @@ -144,14 +143,14 @@ Where the underlying operators are non-deterministic, because they may return on 3. Pop the value :math:`t.\CONST~c_1` from the stack. -4. Let :math:`c` be the result of computing :math:`\relop_t(c_1, c_2)`. +4. Let :math:`c` be the result of computing :math:`\relopF_t(c_1, c_2)`. 5. Push the value :math:`\I32.\CONST~c` to the stack. .. math:: \begin{array}{lcl@{\qquad}l} (t\K{.}\CONST~c_1)~(t\K{.}\CONST~c_2)~t\K{.}\relop &\stepto& (\I32\K{.}\CONST~c) - & (\iff c = \relop_t(c_1,c_2)) \\ + & (\iff c = \relopF_t(c_1,c_2)) \\ \end{array} @@ -1548,20 +1547,27 @@ Where: Vector Instructions ~~~~~~~~~~~~~~~~~~~ -Most vector instructions are defined in terms of generic numeric operators applied lane-wise based on the :ref:`shape `. +Vector instructions that operate bitwise are handled as integer operations of respective width. .. math:: \begin{array}{lll@{\qquad}l} + \X{op}_{\VN}(i_1,\dots,i_k) &=& \xref{exec/numerics}{int-ops}{\F{i}\X{op}}_N(i_1,\dots,i_k) \\ + \end{array} + +Most other vector instructions are defined in terms of numeric operators that are applied lane-wise according to the given :ref:`shape `. + +.. math:: + \begin{array}{llll} \X{op}_{t\K{x}N}(n_1,\dots,n_k) &=& - \lanes^{-1}_{t\K{x}N}(op_t(\lanes_{t\K{x}N}(n_1) ~\dots~ \lanes_{t\K{x}N}(n_k)) + \lanes^{-1}_{t\K{x}N}(\xref{exec/instructions}{exec-instr-numeric}{\X{op}}_t(i_1,\dots,i_k)^\ast) & \qquad(\iff i_1^\ast = \lanes_{t\K{x}N}(n_1) \land \dots \land i_k^\ast = \lanes_{t\K{x}N}(n_k) \\ \end{array} .. note:: - For example, the result of instruction :math:`\K{i32x4}.\ADD` applied to operands :math:`i_1, i_2` - invokes :math:`\ADD_{\K{i32x4}}(i_1, i_2)`, which maps to - :math:`\lanes^{-1}_{\K{i32x4}}(\ADD_{\I32}(i_1^+, i_2^+))`, - where :math:`i_1^+` and :math:`i_2^+` are sequences resulting from invoking - :math:`\lanes_{\K{i32x4}}(i_1)` and :math:`\lanes_{\K{i32x4}}(i_2)` + For example, the result of instruction :math:`\K{i32x4}.\ADD` applied to operands :math:`v_1, v_2` + invokes :math:`\ADD_{\K{i32x4}}(v_1, v_2)`, which maps to + :math:`\lanes^{-1}_{\K{i32x4}}(\ADD_{\I32}(i_1, i_2)^\ast)`, + where :math:`i_1^\ast` and :math:`i_2^\ast` are sequences resulting from invoking + :math:`\lanes_{\K{i32x4}}(v_1)` and :math:`\lanes_{\K{i32x4}}(v_2)` respectively. diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index a16e1ecc7..895789ba2 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -715,6 +715,10 @@ Once the function has returned, the following steps are executed: 2. Pop :math:`\val_{\F{res}}^m` from the stack. +3. Assert: due to :ref:`validation `, the frame :math:`F` is now on the top of the stack. + +4. Pop the frame :math:`F` from the stack. + The values :math:`\val_{\F{res}}^m` are returned as the results of the invocation. .. math:: diff --git a/document/core/exec/numerics.rst b/document/core/exec/numerics.rst index 1655f3770..093258e0a 100644 --- a/document/core/exec/numerics.rst +++ b/document/core/exec/numerics.rst @@ -171,24 +171,25 @@ where :math:`M = \significand(N)` and :math:`E = \exponent(N)`. Vectors ....... -Numeric vectors have the same underlying representation as an |i128|. -They can also be interpreted as a sequence of numeric values packed into a |V128| with a particular |shape|. +Numeric vectors of type |VN| have the same underlying representation as an |IN|. +They can also be interpreted as a sequence of numeric values packed into a |VN| with a particular |shape| :math:`t\K{x}M`, +provided that :math:`N = |t|\cdot M`. .. math:: \begin{array}{l} \begin{array}{lll@{\qquad}l} - \lanes_{t\K{x}N}(c) &=& - c_0~\dots~c_{N-1} \\ + \lanes_{t\K{x}M}(c) &=& + c_0~\dots~c_{M-1} \\ \end{array} \\ \qquad \begin{array}[t]{@{}r@{~}l@{}l@{~}l@{~}l} - (\where & B &=& |t| / 8 \\ - \wedge & b^{16} &=& \bytes_{\i128}(c) \\ - \wedge & c_i &=& \bytes_{t}^{-1}(b^{16}[i \cdot B \slice B])) + (\where & w &=& |t| / 8 \\ + \wedge & b^\ast &=& \bytes_{\IN}(c) \\ + \wedge & c_i &=& \bytes_{t}^{-1}(b^\ast[i \cdot w \slice w])) \end{array} \end{array} -These functions are bijections, so they are invertible. +This function is a bijection on |IN|, hence it is invertible. .. index:: byte, little endian, memory @@ -717,11 +718,13 @@ The integer result of predicates -- i.e., :ref:`tests ` and :ref: :math:`\iextendMs_N(i)` ....................... -* Return :math:`\extends_{M,N}(i)`. +* Let :math:`j` be the result of computing :math:`\wrap_{N,M}(i)`. + +* Return :math:`\extends_{M,N}(j)`. .. math:: \begin{array}{lll@{\qquad}l} - \iextendMs_{N}(i) &=& \extends_{M,N}(i) \\ + \iextendMs_{N}(i) &=& \extends_{M,N}(\wrap_{N,M}(i)) \\ \end{array} diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index 681a4f89d..e0f075373 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -522,6 +522,7 @@ Conventions pair: abstract syntax; frame pair: abstract syntax; label .. _syntax-frame: +.. _syntax-framestate: .. _syntax-label: .. _frame: .. _label: @@ -589,6 +590,8 @@ and a reference to the function's own :ref:`module instance ` .. math:: \begin{array}{llll} \production{frame} & \frame &::=& + \FRAME_n\{ \framestate \} \\ + \production{frame state} & \framestate &::=& \{ \ALOCALS~(\val^?)^\ast, \AMODULE~\moduleinst \} \\ \end{array} @@ -603,7 +606,7 @@ Conventions * The meta variable :math:`L` ranges over labels where clear from context. -* The meta variable :math:`F` ranges over frames where clear from context. +* The meta variable :math:`F` ranges over frame states where clear from context. * The following auxiliary definition takes a :ref:`block type ` and looks up the :ref:`instruction type ` that it denotes in the current frame: @@ -643,7 +646,7 @@ In order to express the reduction of :ref:`traps `, :ref:`calls ` and an executing *thread*. A thread is a computation over :ref:`instructions ` -that operates relative to a current :ref:`frame ` referring to the :ref:`module instance ` in which the computation runs, i.e., where the current function originates from. +that operates relative to the state of a current :ref:`frame ` referring to the :ref:`module instance ` in which the computation runs, i.e., where the current function originates from. .. math:: \begin{array}{llcl} \production{configuration} & \config &::=& \store; \thread \\ \production{thread} & \thread &::=& - \frame; \instr^\ast \\ + \framestate; \instr^\ast \\ \end{array} .. note:: diff --git a/document/core/text/lexical.rst b/document/core/text/lexical.rst index 1dd34c863..4584b0c42 100644 --- a/document/core/text/lexical.rst +++ b/document/core/text/lexical.rst @@ -85,7 +85,9 @@ The allowed formatting characters correspond to a subset of the |ASCII|_ *format \production{white space} & \Tspace &::=& (\text{~~} ~|~ \Tformat ~|~ \Tcomment)^\ast \\ \production{format} & \Tformat &::=& - \unicode{09} ~|~ \unicode{0A} ~|~ \unicode{0D} \\ + \Tnewline ~|~ \unicode{09} \\ + \production{newline} & \Tnewline &::=& + \unicode{0A} ~|~ \unicode{0D} ~|~ \unicode{0D}~\unicode{0A} \\ \end{array} The only relevance of white space is to separate :ref:`tokens `. It is otherwise ignored. @@ -107,13 +109,13 @@ Block comments can be nested. \production{comment} & \Tcomment &::=& \Tlinecomment ~|~ \Tblockcomment \\ \production{line comment} & \Tlinecomment &::=& - \Tcommentd~~\Tlinechar^\ast~~(\unicode{0A} ~|~ \T{eof}) \\ + \Tcommentd~~\Tlinechar^\ast~~(\Tnewline ~|~ \T{eof}) \\ \production{line character} & \Tlinechar &::=& - c{:}\Tchar & (\iff c \neq \unicode{0A}) \\ + c{:}\Tchar & (\iff c \neq \unicode{0A} \land c \neq \unicode{0D}) \\ \production{block comment} & \Tblockcomment &::=& \Tcommentl~~\Tblockchar^\ast~~\Tcommentr \\ \production{block character} & \Tblockchar &::=& - c{:}\Tchar & (\iff c \neq \text{;} \wedge c \neq \text{(}) \\ &&|& + c{:}\Tchar & (\iff c \neq \text{;} \land c \neq \text{(}) \\ &&|& \text{;} & (\iff~\mbox{the next character is not}~\text{)}) \\ &&|& \text{(} & (\iff~\mbox{the next character is not}~\text{;}) \\ &&|& \Tblockcomment \\ diff --git a/document/core/util/macros.def b/document/core/util/macros.def index d290002f7..2871f58d6 100644 --- a/document/core/util/macros.def +++ b/document/core/util/macros.def @@ -609,6 +609,12 @@ .. |relop| mathdef:: \xref{syntax/instructions}{syntax-relop}{\X{relop}} .. |cvtop| mathdef:: \xref{syntax/instructions}{syntax-cvtop}{\X{cvtop}} +.. |unopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{unop}} +.. |binopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{binop}} +.. |testopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{testop}} +.. |relopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\X{relop}} +.. |cvtopF| mathdef:: \xref{exec/instructions}{exec-instr-numeric}{\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}} @@ -827,6 +833,7 @@ .. |Tchar| mathdef:: \xref{text/lexical}{text-char}{\T{char}} .. |Tspace| mathdef:: \xref{text/lexical}{text-space}{\T{space}} .. |Tformat| mathdef:: \xref{text/lexical}{text-format}{\T{format}} +.. |Tnewline| mathdef:: \xref{text/lexical}{text-newline}{\T{newline}} .. |Ttoken| mathdef:: \xref{text/lexical}{text-token}{\T{token}} .. |Tkeyword| mathdef:: \xref{text/lexical}{text-keyword}{\T{keyword}} @@ -1291,6 +1298,7 @@ .. |label| mathdef:: \xref{exec/runtime}{syntax-label}{\X{label}} .. |frame| mathdef:: \xref{exec/runtime}{syntax-frame}{\X{frame}} +.. |framestate| mathdef:: \xref{exec/runtime}{syntax-framestate}{\X{framestate}} .. Stack, meta functions diff --git a/interpreter/Makefile b/interpreter/Makefile index 5939f838e..dfd9064bb 100644 --- a/interpreter/Makefile +++ b/interpreter/Makefile @@ -33,7 +33,7 @@ zip: $(ZIP) # Building -.PHONY: $(NAME) $(JSLIB) +.PHONY: $(NAME) $(JSLIB) $(NAME): rm -f $@ diff --git a/interpreter/text/lexer.mll b/interpreter/text/lexer.mll index 4e3e27bc4..a374eaf03 100644 --- a/interpreter/text/lexer.mll +++ b/interpreter/text/lexer.mll @@ -27,9 +27,9 @@ let string s = while !i < String.length s - 1 do let c = if s.[!i] <> '\\' then s.[!i] else match (incr i; s.[!i]) with - | 'n' -> '\n' - | 'r' -> '\r' - | 't' -> '\t' + | 'n' -> '\x0a' + | 'r' -> '\x0d' + | 't' -> '\x09' | '\\' -> '\\' | '\'' -> '\'' | '\"' -> '\"' @@ -61,10 +61,12 @@ let letter = ['a'-'z''A'-'Z'] let symbol = ['+''-''*''/''\\''^''~''=''<''>''!''?''@''#''$''%''&''|'':''`''.''\''] -let space = [' ''\t''\n''\r'] +let ascii_newline = ['\x0a''\x0d'] +let newline = ascii_newline | "\x0a\x0d" +let space = [' ''\x09''\x0a''\x0d'] let control = ['\x00'-'\x1f'] # space let ascii = ['\x00'-'\x7f'] -let ascii_no_nl = ascii # '\x0a' +let ascii_no_nl = ascii # ascii_newline let utf8cont = ['\x80'-'\xbf'] let utf8enc = ['\xc2'-'\xdf'] utf8cont @@ -128,8 +130,8 @@ rule token = parse | float as s { FLOAT s } | string as s { STRING (string s) } - | '"'character*('\n'|eof) { error lexbuf "unclosed string literal" } - | '"'character*['\x00'-'\x09''\x0b'-'\x1f''\x7f'] + | '"'character*(newline|eof) { error lexbuf "unclosed string literal" } + | '"'character*(control#ascii_newline) { error lexbuf "illegal control character in string literal" } | '"'character*'\\'_ { error_nest (Lexing.lexeme_end_p lexbuf) lexbuf "illegal escape" } @@ -769,11 +771,11 @@ rule token = parse | id as s { VAR s } | ";;"utf8_no_nl*eof { EOF } - | ";;"utf8_no_nl*'\n' { Lexing.new_line lexbuf; token lexbuf } + | ";;"utf8_no_nl*newline { Lexing.new_line lexbuf; token lexbuf } | ";;"utf8_no_nl* { token lexbuf (* causes error on following position *) } | "(;" { comment (Lexing.lexeme_start_p lexbuf) lexbuf; token lexbuf } - | space#'\n' { token lexbuf } - | '\n' { Lexing.new_line lexbuf; token lexbuf } + | space#ascii_newline { token lexbuf } + | newline { Lexing.new_line lexbuf; token lexbuf } | eof { EOF } | reserved { unknown lexbuf } @@ -784,7 +786,7 @@ rule token = parse and comment start = parse | ";)" { () } | "(;" { comment (Lexing.lexeme_start_p lexbuf) lexbuf; comment start lexbuf } - | '\n' { Lexing.new_line lexbuf; comment start lexbuf } + | newline { Lexing.new_line lexbuf; comment start lexbuf } | utf8_no_nl { comment start lexbuf } | eof { error_nest start lexbuf "unclosed comment" } | _ { error lexbuf "malformed UTF-8 encoding" } diff --git a/test/core/comments.wast b/test/core/comments.wast index c291370fa..5ef64a6c1 100644 Binary files a/test/core/comments.wast and b/test/core/comments.wast differ