Merge branch 'upstream'

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')
 

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 <exec-cvtop>`:
 
 .. 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 <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 <syntax-vec-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 <syntax-vec-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.
 
 

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 <valid-module>`, 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::

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 <syntax-testop>` 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}
 
 

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 <syntax-moduleinst>`
 .. 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 <syntax-blocktype>` and looks up the :ref:`instruction type <syntax-instrtype>` that it denotes in the current frame:
 
@@ -643,7 +646,7 @@ In order to express the reduction of :ref:`traps <trap>`, :ref:`calls <syntax-ca
      \INVOKE~\funcaddr \\ &&|&
      \RETURNINVOKE~\funcaddr \\ &&|&
      \LABEL_n\{\instr^\ast\}~\instr^\ast~\END \\ &&|&
-     \FRAME_n\{\frame\}~\instr^\ast~\END \\
+     \FRAME_n\{\framestate\}~\instr^\ast~\END \\
    \end{array}
 
 The |TRAP| instruction represents the occurrence of a trap.
@@ -732,14 +735,14 @@ Configurations
 A *configuration* consists of the current :ref:`store <syntax-store>` and an executing *thread*.
 
 A thread is a computation over :ref:`instructions <syntax-instr>`
-that operates relative to a current :ref:`frame <syntax-frame>` referring to the :ref:`module instance <syntax-moduleinst>` in which the computation runs, i.e., where the current function originates from.
+that operates relative to the state of a current :ref:`frame <syntax-framestate>` referring to the :ref:`module instance <syntax-moduleinst>` 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::

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 <text-token>`. 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 \\

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

interpreter/Makefile

@@ -33,7 +33,7 @@ zip:		$(ZIP)
 
 # Building
 
-.PHONY:                $(NAME) $(JSLIB)
+.PHONY:		$(NAME) $(JSLIB)
 
 $(NAME):
 	rm -f $@

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" }