Merge remote-tracking branch 'spec/master' into HEAD

.gitmodules

@@ -0,0 +1,3 @@
+[submodule "document/core/util/katex"]
+	path = document/core/util/katex
+	url = https://github.com/Khan/KaTeX.git

.travis.yml

@@ -1,11 +1,17 @@
 language: c++
+language: python
+python:
+  - "2.7"
 
 sudo: on
 
 install:
   - ./interpreter/meta/travis/install-ocaml.sh
   - sudo pip install sphinx
   - sudo apt-get install texlive-full
+  - git clone https://github.com/tabatkins/bikeshed.git
+  - pip install --editable $PWD/bikeshed
+  - bikeshed update
 
 script:
   - ./interpreter/meta/travis/build-test.sh

document/Makefile

@@ -30,20 +30,27 @@ root: $(BUILDDIR)
 	cp -f $(FILES) $(BUILDDIR)/
 
 .PHONY: $(DIRS)
-$(DIRS): %: $(BUILDDIR)
-	(cd $@; make BUILDDIR=$(BUILDDIR) all)
-	mkdir -p $(BUILDDIR)/$@
-	cp -R $@/$(BUILDDIR)/html/* $(BUILDDIR)/$@/
+$(DIRS): %: $(BUILDDIR) $(DIRS:%=build-%) $(DIRS:%=dir-%)
+
+.PHONY: $(DIRS:%=build-%)
+$(DIRS:%=build-%): build-%:
+	(cd $(@:build-%=%); make BUILDDIR=$(BUILDDIR) all)
+
+.PHONY: $(DIRS:%=dir-%)
+$(DIRS:%=dir-%): dir-%:
+	mkdir -p $(BUILDDIR)/$(@:dir-%=%)
+	rm -rf $(BUILDDIR)/$(@:dir-%=%)/*
+	cp -R $(@:dir-%=%)/$(BUILDDIR)/html/* $(BUILDDIR)/$(@:dir-%=%)/
 
 .PHONY: $(DIRS:%=deploy-%)
-$(DIRS:%=deploy-%):
+$(DIRS:%=deploy-%): deploy-%:
 	GIT_DEPLOY_DIR=$(BUILDDIR) GIT_DEPLOY_SUBDIR=$(@:deploy-%=%) bash deploy.sh
 
 .PHONY: $(DIRS:%=publish-%)
 $(DIRS:%=publish-%): publish-%: % deploy-%
 
 .PHONY: $(DIRS:%=clean-%)
-$(DIRS:%=clean-%):
+$(DIRS:%=clean-%): clean-%:
 	(cd $(@:clean-%=%); make BUILDDIR=$(BUILDDIR) clean)
 	rm -rf $(BUILDDIR)/$(@:clean-%=%)
 

document/core/Makefile

@@ -26,7 +26,8 @@ usage:
 	@echo "Please use \`make <target>' where <target> is one of"
 	@echo "  html       to make standalone HTML files"
 	@echo "  pdf        to make standalone PDF file"
-	@echo "  all        to make both"
+	@echo "  bikeshed   to make a bikeshed wrapped single large HTML file"
+	@echo "  all        to make all 3"
 	@echo "  publish    to make all and push to gh-pages"
 	@echo "  help       to see more options"
 
@@ -35,7 +36,8 @@ help:
 	@echo "Usage: \`make <target>' where <target> is one of"
 	@echo "  html       to make standalone HTML files"
 	@echo "  pdf        to make standalone PDF file"
-	@echo "  all        to make both"
+	@echo "  bikeshed   to make a bikeshed wrapped single large HTML file"
+	@echo "  all        to make all 3"
 	@echo "  publish    to make all and push to gh-pages"
 	@echo "  dirhtml    to make HTML files named index.html in directories"
 	@echo "  singlehtml to make a single large HTML file"
@@ -65,14 +67,28 @@ help:
 
 .PHONY: deploy
 deploy:
-	(cd ..; make deploy-core)
+	(cd ..; make dir-core deploy-core)
 
 .PHONY: publish
-publish:
-	(cd ..; make publish-core)
+publish: clean all deploy
+
+.PHONY: publish-main
+publish-main: clean main bikeshed-keep deploy
 
 .PHONY: all
-all:	pdf html
+all:	pdf html bikeshed
+
+.PHONY: main
+main:	pdf html
+
+# Dirty hack to avoid rebuilding the Bikeshed version for every push.
+.PHONY: bikeshed-keep
+bikeshed-keep:
+	test -e $(BUILDDIR)/html/bikeshed || \
+	  wget -r -nH --cut-dirs=2 -P $(BUILDDIR)/html --no-check-certificate \
+	    https://webassembly.github.io/spec/core/bikeshed || \
+	  echo Downloaded Bikeshed.
+
 
 .PHONY: pdf
 pdf:	latexpdf
@@ -98,14 +114,14 @@ html:
 	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;' \
+	  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
-	@echo "Build finished. The HTML pages are in `pwd`/$(BUILDDIR)/html."
+	@echo "Build finished. The HTML pages are in `pwd`/$(BUILDDIR)/html/."
 
 .PHONY: dirhtml
 dirhtml:
@@ -119,6 +135,24 @@ singlehtml:
 	@echo
 	@echo "Build finished. The HTML page is in $(BUILDDIR)/singlehtml."
 
+.PHONY: bikeshed
+bikeshed:
+	$(SPHINXBUILD) -b singlehtml -c util/bikeshed \
+		$(ALLSPHINXOPTS) $(BUILDDIR)/bikeshed_singlehtml
+	python util/bikeshed_fixup.py $(BUILDDIR)/bikeshed_singlehtml/index.html \
+		>$(BUILDDIR)/bikeshed_singlehtml/index_fixed.html
+	mkdir -p $(BUILDDIR)/bikeshed_mathjax/
+	bikeshed spec index.bs $(BUILDDIR)/bikeshed_mathjax/index.html
+	mkdir -p $(BUILDDIR)/html/bikeshed/
+	python util/mathjax2katex.py $(BUILDDIR)/bikeshed_mathjax/index.html \
+		>$(BUILDDIR)/html/bikeshed/index.html
+	mkdir -p $(BUILDDIR)/html/bikeshed/katex/dist/
+	cp -r util/katex/dist/* $(BUILDDIR)/html/bikeshed/katex/dist/
+	patch -p0 $(BUILDDIR)/html/bikeshed/katex/dist/katex.css \
+		< util/katex_fix.patch
+	@echo
+	@echo "Build finished. The HTML page is in $(BUILDDIR)/html/bikeshed/."
+
 .PHONY: pickle
 pickle:
 	$(SPHINXBUILD) -b pickle $(ALLSPHINXOPTS) $(BUILDDIR)/pickle

document/core/appendix/algorithm.rst

@@ -169,6 +169,7 @@ Other instructions are checked in a similar manner.
          push_ctrl([], [t*])
 
        case (if t*)
+         pop_opd(I32)
          push_ctrl([t*], [t*])
 
        case (end)

document/core/appendix/index-instructions.rst

@@ -70,8 +70,8 @@ Instruction                          Binary Opcode     Type
 :math:`\I64.\STORE\K{8}~\memarg`     :math:`\hex{3C}`  :math:`[\I32~\I64] \to []`                  :ref:`validation <valid-storen>`          :ref:`execution <exec-storen>`
 :math:`\I64.\STORE\K{16}~\memarg`    :math:`\hex{3D}`  :math:`[\I32~\I64] \to []`                  :ref:`validation <valid-storen>`          :ref:`execution <exec-storen>`
 :math:`\I64.\STORE\K{32}~\memarg`    :math:`\hex{3E}`  :math:`[\I32~\I64] \to []`                  :ref:`validation <valid-storen>`          :ref:`execution <exec-storen>`
-:math:`\CURRENTMEMORY`               :math:`\hex{3F}`  :math:`[] \to [\I32]`                       :ref:`validation <valid-current_memory>`  :ref:`execution <exec-current_memory>`
-:math:`\GROWMEMORY`                  :math:`\hex{40}`  :math:`[\I32] \to [\I32]`                   :ref:`validation <valid-grow_memory>`     :ref:`execution <exec-grow_memory>`
+:math:`\MEMORYSIZE`                  :math:`\hex{3F}`  :math:`[] \to [\I32]`                       :ref:`validation <valid-memory.size>`     :ref:`execution <exec-memory.size>`
+:math:`\MEMORYGROW`                  :math:`\hex{40}`  :math:`[\I32] \to [\I32]`                   :ref:`validation <valid-memory.grow>`     :ref:`execution <exec-memory.grow>`
 :math:`\I32.\CONST~\i32`             :math:`\hex{41}`  :math:`[] \to [\I32]`                       :ref:`validation <valid-const>`           :ref:`execution <exec-const>`
 :math:`\I64.\CONST~\i64`             :math:`\hex{42}`  :math:`[] \to [\I64]`                       :ref:`validation <valid-const>`           :ref:`execution <exec-const>`
 :math:`\F32.\CONST~\f32`             :math:`\hex{43}`  :math:`[] \to [\F32]`                       :ref:`validation <valid-const>`           :ref:`execution <exec-const>`

document/core/appendix/index-rules.rst

@@ -102,6 +102,6 @@ Execution
 ===============================================  ===============================================================================
 Construct                                        Judgement
 ===============================================  ===============================================================================
-:ref:`Instruction <exec-instr>`                  :math:`S;F;\instr \stepto S';F';{\instr'}^\ast`
-:ref:`Expression <exec-expr>`                    :math:`S;F;\expr \stepto^\ast S';F';\val^\ast`
+:ref:`Instruction <exec-instr>`                  :math:`S;F;\instr^\ast \stepto S';F';{\instr'}^\ast`
+:ref:`Expression <exec-expr>`                    :math:`S;F;\expr \stepto  S';F';\expr'`
 ===============================================  ===============================================================================

document/core/appendix/index.rst

@@ -11,3 +11,13 @@ Appendix
    algorithm
    custom
    properties
+
+.. only:: singlehtml
+
+   .. toctree::
+
+      :maxdepth: 2
+      index-types
+      index-instructions
+      index-rules
+

document/core/appendix/properties.rst

@@ -7,7 +7,7 @@ Soundness
 The :ref:`type system <type-system>` of WebAssembly is *sound*, implying both *type safety* and *memory safety* with respect to the WebAssembly semantics. For example:
 
 * All types declared and derived during validation are respected at run time;
-  e.g., every :ref:`local <syntax-local>` or :ref:`global <syntax-global>` variable will only contain type-correct values, every :ref:`instruction <syntax-instr>` will only be applied to operands of the expected type, and every :ref:`function <syntax-func>` :ref:`invocation <exec-invocation>` always evaluates to a result of the right type.
+  e.g., every :ref:`local <syntax-local>` or :ref:`global <syntax-global>` variable will only contain type-correct values, every :ref:`instruction <syntax-instr>` will only be applied to operands of the expected type, and every :ref:`function <syntax-func>` :ref:`invocation <exec-invocation>` always evaluates to a result of the right type (if it does not :ref:`trap <trap>`).
 
 * No memory location will be read or written except those explicitly defined by the program, i.e., as a :ref:`local <syntax-local>`, a :ref:`global <syntax-global>`, an element in a :ref:`table <syntax-table>`, or a location within a linear :ref:`memory <syntax-mem>`.
 
@@ -709,7 +709,7 @@ Theorems
 ~~~~~~~~
 
 Given the definition of :ref:`valid configurations <valid-config>`,
-the standard soundness theorems hold.
+the standard soundness theorems hold. [#cite-cpp2018]_
 
 **Theorem (Preservation).**
 If a :ref:`configuration <syntax-config>` :math:`S;T` is :ref:`valid <valid-config>` with :ref:`result type <syntax-resulttype>` :math:`[t^\ast]` (i.e., :math:`\vdashconfig S;T : [t^\ast]`),
@@ -739,3 +739,7 @@ Consequently, given a :ref:`valid store <valid-store>`, no computation defined b
 .. [#cite-pldi2017]
    The formalization and theorems are derived from the following article:
    Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman. |PLDI2017|_. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017.
+
+.. [#cite-cpp2018]
+   A machine-verified version of the formalization and soundness proof is described in the following article:
+   Conrad Watt. |CPP2018|_. Proceedings of the 7th ACM SIGPLAN Conference on Certified Programs and Proofs (CPP 2018). ACM 2018.

document/core/binary/instructions.rst

@@ -124,8 +124,8 @@ Each variant of :ref:`memory instruction <syntax-instr-memory>` is encoded with
 .. _binary-loadn:
 .. _binary-store:
 .. _binary-storen:
-.. _binary-current_memory:
-.. _binary-grow_memory:
+.. _binary-memory.size:
+.. _binary-memory.grow:
 
 .. math::
    \begin{array}{llclll}
@@ -155,12 +155,12 @@ Each variant of :ref:`memory instruction <syntax-instr-memory>` is encoded with
      \hex{3C}~~m{:}\Bmemarg &\Rightarrow& \I64.\STORE\K{8}~m \\ &&|&
      \hex{3D}~~m{:}\Bmemarg &\Rightarrow& \I64.\STORE\K{16}~m \\ &&|&
      \hex{3E}~~m{:}\Bmemarg &\Rightarrow& \I64.\STORE\K{32}~m \\ &&|&
-     \hex{3F}~~\hex{00} &\Rightarrow& \CURRENTMEMORY \\ &&|&
-     \hex{40}~~\hex{00} &\Rightarrow& \GROWMEMORY \\
+     \hex{3F}~~\hex{00} &\Rightarrow& \MEMORYSIZE \\ &&|&
+     \hex{40}~~\hex{00} &\Rightarrow& \MEMORYGROW \\
    \end{array}
 
 .. note::
-   In future versions of WebAssembly, the additional zero bytes occurring in the encoding of the |CURRENTMEMORY| and |GROWMEMORY| instructions may be used to index additional memories.
+   In future versions of WebAssembly, the additional zero bytes occurring in the encoding of the |MEMORYSIZE| and |MEMORYGROW| instructions may be used to index additional memories.
 
 
 .. index:: numeric instruction

document/core/exec/instructions.rst

@@ -533,18 +533,18 @@ Memory Instructions
    \end{array}
 
 
-.. _exec-current_memory:
+.. _exec-memory.size:
 
-:math:`\CURRENTMEMORY`
-......................
+:math:`\MEMORYSIZE`
+...................
 
 1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
 
-2. Assert: due to :ref:`validation <valid-current_memory>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.
+2. Assert: due to :ref:`validation <valid-memory.size>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.
 
 3. Let :math:`a` be the :ref:`memory address <syntax-memaddr>` :math:`F.\AMODULE.\MIMEMS[0]`.
 
-4. Assert: due to :ref:`validation <valid-current_memory>`, :math:`S.\SMEMS[a]` exists.
+4. Assert: due to :ref:`validation <valid-memory.size>`, :math:`S.\SMEMS[a]` exists.
 
 5. Let :math:`\X{mem}` be the :ref:`memory instance <syntax-meminst>` :math:`S.\SMEMS[a]`.
 
@@ -555,31 +555,31 @@ Memory Instructions
 .. math::
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   S; F; \CURRENTMEMORY &\stepto& S; F; (\I32.\CONST~\X{sz})
+   S; F; \MEMORYSIZE &\stepto& S; F; (\I32.\CONST~\X{sz})
    \end{array}
    \\ \qquad
      (\iff |S.\SMEMS[F.\AMODULE.\MIMEMS[0]].\MIDATA| = \X{sz}\cdot64\,\F{Ki}) \\
    \end{array}
 
 
-.. _exec-grow_memory:
+.. _exec-memory.grow:
 
-:math:`\GROWMEMORY`
+:math:`\MEMORYGROW`
 ...................
 
 1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
 
-2. Assert: due to :ref:`validation <valid-grow_memory>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.
+2. Assert: due to :ref:`validation <valid-memory.grow>`, :math:`F.\AMODULE.\MIMEMS[0]` exists.
 
 3. Let :math:`a` be the :ref:`memory address <syntax-memaddr>` :math:`F.\AMODULE.\MIMEMS[0]`.
 
-4. Assert: due to :ref:`validation <valid-grow_memory>`, :math:`S.\SMEMS[a]` exists.
+4. Assert: due to :ref:`validation <valid-memory.grow>`, :math:`S.\SMEMS[a]` exists.
 
 5. Let :math:`\X{mem}` be the :ref:`memory instance <syntax-meminst>` :math:`S.\SMEMS[a]`.
 
 6. Let :math:`\X{sz}` be the length of :math:`S.\SMEMS[a]` divided by the :ref:`page size <page-size>`.
 
-7. Assert: due to :ref:`validation <valid-grow_memory>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
+7. Assert: due to :ref:`validation <valid-memory.grow>`, a value of :ref:`value type <syntax-valtype>` |I32| is on the top of the stack.
 
 8. Pop the value :math:`\I32.\CONST~n` from the stack.
 
@@ -595,7 +595,7 @@ Memory Instructions
    ~\\[-1ex]
    \begin{array}{l}
    \begin{array}{lcl@{\qquad}l}
-   S; F; (\I32.\CONST~n)~\GROWMEMORY &\stepto& S'; F; (\I32.\CONST~\X{sz})
+   S; F; (\I32.\CONST~n)~\MEMORYGROW &\stepto& S'; F; (\I32.\CONST~\X{sz})
    \end{array}
    \\ \qquad
      \begin{array}[t]{@{}r@{~}l@{}}
@@ -605,12 +605,12 @@ Memory Instructions
      \end{array}
    \\[1ex]
    \begin{array}{lcl@{\qquad}l}
-   S; F; (\I32.\CONST~n)~\GROWMEMORY &\stepto& S; F; (\I32.\CONST~{-1})
+   S; F; (\I32.\CONST~n)~\MEMORYGROW &\stepto& S; F; (\I32.\CONST~{-1})
    \end{array}
    \end{array}
 
 .. note::
-   The |GROWMEMORY| instruction is non-deterministic.
+   The |MEMORYGROW| instruction is non-deterministic.
    It may either succeed, returning the old memory size :math:`\X{sz}`,
    or fail, returning :math:`{-1}`.
    Failure *must* occur if the referenced memory instance has a maximum size defined that would be exceeded.
@@ -823,7 +823,7 @@ Control Instructions
 
 2. Let :math:`n` be the arity of :math:`F`.
 
-3. Assert: due to :ref:`validation <valid-br>`, there are at least :math:`n` values on the top of the stack.
+3. Assert: due to :ref:`validation <valid-return>`, there are at least :math:`n` values on the top of the stack.
 
 4. Pop the results :math:`\val^n` from the stack.
 
@@ -1049,7 +1049,7 @@ Invocation of :ref:`function address <syntax-funcaddr>` :math:`a`
 Returning from a function
 .........................
 
-When the end of a funtion is reached without a jump (i.e., |RETURN|) or trap aborting it, then the following steps are performed.
+When the end of a function is reached without a jump (i.e., |RETURN|) or trap aborting it, then the following steps are performed.
 
 1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
 
@@ -1130,17 +1130,21 @@ An :ref:`expression <syntax-expr>` is *evaluated* relative to a :ref:`current <e
 
 1. Jump to the start of the instruction sequence :math:`\instr^\ast` of the expression.
 
-2. Execute of the instruction sequence.
+2. Execute the instruction sequence.
 
 3. Assert: due to :ref:`validation <valid-expr>`, the top of the stack contains a :ref:`value <syntax-val>`.
 
-4. Pop the the :ref:`value <syntax-val>` :math:`\val` from the stack.
+4. Pop the :ref:`value <syntax-val>` :math:`\val` from the stack.
 
 The value :math:`\val` is the result of the evaluation.
 
 .. math::
    \frac{
-     S; F; \instr^\ast \stepto^\ast S'; F'; v
+     S; F; \instr^\ast \stepto S'; F'; \instr'^\ast
    }{
-     S; F; \instr^\ast~\END \stepto^\ast S'; F'; v
+     S; F; \instr^\ast~\END \stepto S'; F'; \instr'^\ast~\END
    }
+
+.. note::
+   Evaluation iterates this reduction rule until reaching a value.
+   Expressions constituting :ref:`function <syntax-func>` bodies are executed during function :ref:`invocation <exec-invoke>`.