Merge pull request #22 from WebAssembly/merge

Merge with upstream ref-types

Author: rossberg

.travis.yml

@@ -1,19 +1,21 @@
-language: c++
 language: python
 python:
-  - "2.7"
+  - "3.7"
+dist: bionic
 
-sudo: on
-
-before_install:
-  - curl -sS https://dl.yarnpkg.com/debian/pubkey.gpg | sudo apt-key add -
-  - echo "deb https://dl.yarnpkg.com/debian/ stable main" | sudo tee /etc/apt/sources.list.d/yarn.list
-  - sudo apt-get update -qq
+addons:
+  apt:
+    sources:
+      - sourceline: 'deb https://dl.yarnpkg.com/debian/ stable main'
+        key_url: 'https://dl.yarnpkg.com/debian/pubkey.gpg'
+    packages:
+      - ocaml
+      - ocamlbuild
+      - texlive-full
+      - yarn
 
 install:
-  - ./interpreter/meta/travis/install-ocaml.sh
-  - sudo pip install sphinx==1.7.9
-  - sudo apt-get install texlive-full yarn
+  - pip install Sphinx==2.4.4
   - git clone https://github.com/tabatkins/bikeshed.git
   - pip install --editable $PWD/bikeshed
   - bikeshed update

document/core/Makefile

@@ -10,14 +10,10 @@ STATICDIR     = _static
 DOWNLOADDIR   = _download
 NAME          = WebAssembly
 
-# Hack until we have moved to more recent Sphinx.
-OLDMATHJAX    = https://cdn.mathjax.org/mathjax/latest/MathJax.js
-NEWMATHJAX    = https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.1/MathJax.js
-
 # Internal variables.
 PAPEROPT_a4     = -D latex_paper_size=a4
 PAPEROPT_letter = -D latex_paper_size=letter
-ALLSPHINXOPTS   = -d $(BUILDDIR)/doctrees $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) .
+ALLSPHINXOPTS   = -d $(BUILDDIR)/doctrees $(SPHINXOPTS) .
 # the i18n builder cannot share the environment and doctrees with the others
 I18NSPHINXOPTS  = $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) .
 
@@ -111,16 +107,10 @@ html:
 	do \
 	  sed s:BASEDIR:.:g <$$file >$$file.out; \
 	  mv -f $$file.out $$file; \
-	  sed s~$(OLDMATHJAX)~$(NEWMATHJAX)~g <$$file >$$file.out; \
-	  mv -f $$file.out $$file; \
 	done
 	for file in `ls $(BUILDDIR)/html/*/*.html`; \
 	do \
 	  sed s:BASEDIR:..:g <$$file >$$file.out; \
-	  sed 's;<body; <script type="text/javascript">MathJax.Hub.Config({TeX: {MAXBUFFER: 30*1024}})</script><body;' \
-	    <$$file.out >$$file; \
-	  rm -f $$file.out; \
-	  sed s~$(OLDMATHJAX)~$(NEWMATHJAX)~g <$$file >$$file.out; \
 	  mv -f $$file.out $$file; \
 	done
 	@echo

document/core/appendix/algorithm.rst

@@ -26,17 +26,16 @@ A simple subtyping check can be defined on these types.
 
 .. code-block:: pseudo
 
-   type val_type = I32 | I64 | F32 | F64 | Anyref | Funcref | Nullref | Bot
+   type val_type = I32 | I64 | F32 | F64 | Funcref | Externref | Bot
 
    func is_num(t : val_type) : bool =
      return t = I32 || t = I64 || t = F32 || t = F64 || t = Bot
 
    func is_ref(t : val_type) : bool =
-     return t = Anyref || t = Funcref || t = Nullref || t = Bot
+     return t = Funcref || t = Externref || t = Bot
 
    func matches(t1 : val_type, t2 : val_type) : bool =
-     return t1 = t2 || t1 = Bot ||
-       (t1 = Nullref && is_ref(t2)) || (is_ref(t1) && t2 = Anyref)
+     return t1 = t2 || t1 = Bot
 
 The algorithm uses two separate stacks: the *value stack* and the *control stack*.
 The former tracks the :ref:`types <syntax-valtype>` of operand values on the :ref:`stack <stack>`,
@@ -48,19 +47,16 @@ the latter surrounding :ref:`structured control instructions <syntax-instr-contr
 
    type ctrl_stack = stack(ctrl_frame)
    type ctrl_frame = {
-     label_types : list(val_type)
+     opcode : opcode
+     start_types : list(val_type)
      end_types : list(val_type)
      height : nat
      unreachable : bool
    }
 
 For each value, the value stack records its :ref:`value type <syntax-valtype>`.
 
-For each entered block, the control stack records a *control frame* with the type of the associated :ref:`label <syntax-label>` (used to type-check branches), the result type of the block (used to check its result), the height of the operand stack at the start of the block (used to check that operands do not underflow the current block), and a flag recording whether the remainder of the block is unreachable (used to handle :ref:`stack-polymorphic <polymorphism>` typing after branches).
-
-.. note::
-   In the presentation of this algorithm, multiple values are supported for the :ref:`result types <syntax-resulttype>` classifying blocks and labels.
-   With the current version of WebAssembly, the :code:`list` could be simplified to an optional value.
+For each entered block, the control stack records a *control frame* with the originating opcode, the types on the top of the operand stack at the start and end of the block (used to check its result as well as branches), the height of the operand stack at the start of the block (used to check that operands do not underflow the current block), and a flag recording whether the remainder of the block is unreachable (used to handle :ref:`stack-polymorphic <polymorphism>` typing after branches).
 
 For the purpose of presenting the algorithm, the operand and control stacks are simply maintained as global variables:
 
@@ -76,7 +72,7 @@ However, these variables are not manipulated directly by the main checking funct
    func push_val(type : val_type) =
      vals.push(type)
 
-   func pop_val() : val_type =
+   func pop_val() : val_type | Unknown =
      if (vals.size() = ctrls[0].height && ctrls[0].unreachable) return Bot
      error_if(vals.size() = ctrls[0].height)
      return vals.pop()
@@ -114,17 +110,21 @@ The control stack is likewise manipulated through auxiliary functions:
 
 .. code-block:: pseudo
 
-   func push_ctrl(label : list(val_type), out : list(val_type)) =
-     let frame = ctrl_frame(label, out, vals.size(), false)
+   func push_ctrl(opcode : opcode, in : list(val_type), out : list(val_type)) =
+     let frame = ctrl_frame(opcode, in, out, vals.size(), false)
      ctrls.push(frame)
+     push_vals(in)
 
-   func pop_ctrl() : list(val_type) =
+   func pop_ctrl() : ctrl_frame =
      error_if(ctrls.is_empty())
      let frame = ctrls[0]
      pop_vals(frame.end_types)
      error_if(vals.size() =/= frame.height)
      ctrls.pop()
-     return frame.end_types
+     return frame
+
+   func label_types(frame : ctrl_frame) : list(val_types) =
+     return (if frame.opcode == loop then frame.start_types else frame.end_types)
 
    func unreachable() =
      vals.resize(ctrls[0].height)
@@ -137,6 +137,8 @@ Popping a frame first checks that the control stack is not empty.
 It then verifies that the operand stack contains the right types of values expected at the end of the exited block and pops them off the operand stack.
 Afterwards, it checks that the stack has shrunk back to its initial height.
 
+The type of the :ref:`label <syntax-label>` associated with a control frame is either that of the stack at the start or the end of the frame, determined by the opcode that it originates from.
+
 Finally, the current frame can be marked as unreachable.
 In that case, all existing operand types are purged from the value stack, in order to allow for the :ref:`stack-polymorphism <polymorphism>` logic in :code:`pop_val` to take effect.
 
@@ -187,44 +189,48 @@ Other instructions are checked in a similar manner.
        case (unreachable)
          unreachable()
 
-       case (block t*)
-         push_ctrl([t*], [t*])
+       case (block t1*->t2*)
+         pop_vals([t1*])
+         push_ctrl(block, [t1*], [t2*])
 
-       case (loop t*)
-         push_ctrl([], [t*])
+       case (loop t1*->t2*)
+         pop_vals([t1*])
+         push_ctrl(loop, [t1*], [t2*])
 
-       case (if t*)
+       case (if t1*->t2*)
          pop_val(I32)
-         push_ctrl([t*], [t*])
+         pop_vals([t1*])
+         push_ctrl(if, [t1*], [t2*])
 
        case (end)
-         let results = pop_ctrl()
-         push_vals(results)
+         let frame = pop_ctrl()
+         push_vals(frame.end_types)
 
        case (else)
-         let results = pop_ctrl()
-         push_ctrl(results, results)
+         let frame = pop_ctrl()
+         error_if(frame.opcode =/= if)
+         push_ctrl(else, frame.start_types, frame.end_types)
 
        case (br n)
          error_if(ctrls.size() < n)
-         pop_vals(ctrls[n].label_types)
+         pop_vals(label_types(ctrls[n]))
          unreachable()
 
        case (br_if n)
          error_if(ctrls.size() < n)
          pop_val(I32)
-         pop_vals(ctrls[n].label_types)
-         push_vals(ctrls[n].label_types)
+         pop_vals(label_types(ctrls[n]))
+         push_vals(label_types(ctrls[n]))
 
        case (br_table n* m)
          pop_val(I32)
          error_if(ctrls.size() < m)
-         let arity = ctrls[m].label_types.size()
+         let arity = label_types(ctrls[m]).size()
          foreach (n in n*)
            error_if(ctrls.size() < n)
-           error_if(ctrls[n].label_types.size() =/= arity)
-           push_vals(pop_vals(ctrls[n].label_types))
-         pop_vals(ctrls[m].label_types)
+           error_if(label_types(ctrls[n]).size() =/= arity)
+           push_vals(pop_vals(label_types(ctrls[n])))
+         pop_vals(label_types(ctrls[m]))
          unreachable()
 
 .. note::

document/core/appendix/implementation.rst

@@ -43,6 +43,8 @@ An implementation may impose restrictions on the following dimensions of a modul
 * the number of :ref:`exports <syntax-export>` from a :ref:`module <syntax-module>`
 * the number of parameters in a :ref:`function type <syntax-functype>`
 * the number of results in a :ref:`function type <syntax-functype>`
+* the number of parameters in a :ref:`block type <syntax-blocktype>`
+* the number of results in a :ref:`block type <syntax-blocktype>`
 * the number of :ref:`locals <syntax-local>` in a :ref:`function <syntax-func>`
 * the size of a :ref:`function <syntax-func>` body
 * the size of a :ref:`structured control instruction <syntax-instr-control>`