Skip to content

Commit 7e5148c

Browse files
authored
Merge pull request #29 from Ms2ger/update
Update to upstream.
2 parents b57e66e + a36caad commit 7e5148c

File tree

179 files changed

+27867
-3365
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

179 files changed

+27867
-3365
lines changed

.travis.yml

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -6,16 +6,22 @@ dist: bionic
66
addons:
77
apt:
88
sources:
9+
- sourceline: 'ppa:avsm/ppa'
910
- sourceline: 'deb https://dl.yarnpkg.com/debian/ stable main'
1011
key_url: 'https://dl.yarnpkg.com/debian/pubkey.gpg'
12+
update: true
1113
packages:
12-
- ocaml
13-
- ocamlbuild
14+
- opam
1415
- texlive-full
1516
- yarn
1617

1718
install:
18-
- pip install Sphinx==2.4.4
19+
- opam init --auto-setup --compiler=4.07.1
20+
- eval $(opam env)
21+
- opam --version
22+
- ocaml --version
23+
- opam install --yes ocamlbuild.0.14.0
24+
- pip install Sphinx==3.5.2
1925
- git clone https://github.com/tabatkins/bikeshed.git
2026
- pip install --editable $PWD/bikeshed
2127
- bikeshed update

README.md

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,3 +28,7 @@ should take place in
2828
[the WebAssembly design repository](https://github.com/WebAssembly/design)
2929
first, so that this spec repository can remain focused. And please follow the
3030
[guidelines for contributing](Contributing.md).
31+
32+
# citing
33+
34+
For citing WebAssembly in LaTeX, use [this bibtex file](wasm-specs.bib).

document/README.md

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -21,3 +21,98 @@ To build everything and update [webassembly.github.io/spec](https://webassembly.
2121
make publish
2222
```
2323
Please make sure to only use that once a change has approval.
24+
25+
## Step by step guide to building the spec
26+
27+
### Prerequisites
28+
29+
You will need `python3.7`, and `pip`. `pip` should come with Python, if not follow [these installation instructions for `pip`](https://pip.pypa.io/en/stable/installing/), or check your system package manager for `pip3`.
30+
31+
> Important: you will need the version of pip that works with `python3.7`.
32+
33+
34+
Use something like [`pipenv`](https://pipenv.pypa.io/) to keep your system installation of Python clean.
35+
36+
```
37+
pip install pipenv
38+
pipenv --python 3.7
39+
pipenv shell
40+
```
41+
42+
Install Python dependencies:
43+
44+
```
45+
pipenv install Sphinx==3.5.2
46+
```
47+
48+
### Checking out the repository
49+
50+
Make sure this repository was cloned with `--recursive`:
51+
52+
```
53+
git clone --recursive https://github.com/WebAssembly/spec
54+
```
55+
56+
If you have already cloned but without `--recursive`, you can delete and re-clone, or `cd` into `spec` and run:
57+
58+
```
59+
git submodule update --init --recursive
60+
```
61+
62+
The rest of these instructions assume you are in the directory where is README is:
63+
64+
```
65+
cd spec/document
66+
```
67+
68+
### Building the multi-page HTML document
69+
70+
You can now build the [multi-page html document](https://webassembly.github.io/spec/core/):
71+
72+
```
73+
make -C core html
74+
```
75+
76+
### Building the single-page HTML document
77+
78+
To build the [single-page W3C version](https://webassembly.github.io/spec/core/bikeshed/), there are more dependencies to install. First, get [Bikeshed](https://github.com/tabatkins/bikeshed):
79+
80+
```
81+
# cd back to root of git directory
82+
git clone https://github.com/tabatkins/bikeshed.git
83+
pipenv install -e bikeshed
84+
bikeshed update
85+
```
86+
87+
You will also need `npm` and `yarn` for all the LaTeX goodness. `npm` might already be available on your system, you can also use something like [`nvm`](https://github.com/nvm-sh/nvm) to prevent messing with system packages:
88+
89+
```
90+
npm install -g yarn
91+
cd document
92+
make -C core bikeshed
93+
```
94+
95+
### Building the PDF
96+
97+
To build the [PDF](https://webassembly.github.io/spec/core/_download/WebAssembly.pdf), you will need `texlive-full`, install it using your system package manager:
98+
99+
```
100+
apt install texlive-full
101+
make -C core pdf
102+
```
103+
104+
### Building the JavaScript Embedding API
105+
106+
To build the [JavaScript Embedding API](https://webassembly.github.io/spec/js-api/index.html), you will need `bikeshed` as describe in the section [Building the single-page HTML document](#building-the-single-page-html-document):
107+
108+
```
109+
make -C js-api
110+
```
111+
112+
### Building the Web Embedding API
113+
114+
To build the [Web Embedding API](https://webassembly.github.io/spec/web-api/index.html), you will need `bikeshed` as describe in the section [Building the single-page HTML document](#building-the-single-page-html-document):
115+
116+
```
117+
make -C web-api
118+
```

document/core/Makefile

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -89,8 +89,12 @@ bikeshed-keep:
8989
echo Downloaded Bikeshed.
9090

9191

92+
.PHONY: index
93+
index:
94+
(cd appendix; ./gen-index-instructions.py)
95+
9296
.PHONY: pdf
93-
pdf: latexpdf
97+
pdf: index latexpdf
9498
mkdir -p $(BUILDDIR)/html/$(DOWNLOADDIR)
9599
ln -f $(BUILDDIR)/latex/$(NAME).pdf $(BUILDDIR)/html/$(DOWNLOADDIR)/$(NAME).pdf
96100

@@ -101,7 +105,7 @@ clean:
101105
rm -rf $(STATICDIR)
102106

103107
.PHONY: html
104-
html:
108+
html: index
105109
$(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html
106110
for file in `ls $(BUILDDIR)/html/*.html`; \
107111
do \

document/core/appendix/algorithm.rst

Lines changed: 73 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -21,15 +21,25 @@ The algorithm is expressed in typed pseudo code whose semantics is intended to b
2121
Data Structures
2222
~~~~~~~~~~~~~~~
2323

24-
The algorithm uses two separate stacks: the *operand stack* and the *control stack*.
24+
Types are representable as an enumeration.
25+
26+
.. code-block:: pseudo
27+
28+
type val_type = I32 | I64 | F32 | F64 | Funcref | Externref
29+
30+
func is_num(t : val_type | Unknown) : bool =
31+
return t = I32 || t = I64 || t = F32 || t = F64 || t = Unknown
32+
33+
func is_ref(t : val_type | Unknown) : bool =
34+
return t = Funcref || t = Externref || t = Unknown
35+
36+
The algorithm uses two separate stacks: the *value stack* and the *control stack*.
2537
The former tracks the :ref:`types <syntax-valtype>` of operand values on the :ref:`stack <stack>`,
2638
the latter surrounding :ref:`structured control instructions <syntax-instr-control>` and their associated :ref:`blocks <syntax-instr-control>`.
2739

2840
.. code-block:: pseudo
2941
30-
type val_type = I32 | I64 | F32 | F64
31-
32-
type opd_stack = stack(val_type | Unknown)
42+
type val_stack = stack(val_type | Unknown)
3343
3444
type ctrl_stack = stack(ctrl_frame)
3545
type ctrl_frame = {
@@ -40,79 +50,82 @@ the latter surrounding :ref:`structured control instructions <syntax-instr-contr
4050
unreachable : bool
4151
}
4252
43-
For each value, the operand stack records its :ref:`value type <syntax-valtype>`, or :code:`Unknown` when the type is not known.
53+
For each value, the value stack records its :ref:`value type <syntax-valtype>`, or :code:`Unknown` when the type is not known.
4454

4555
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).
4656

4757
For the purpose of presenting the algorithm, the operand and control stacks are simply maintained as global variables:
4858

4959
.. code-block:: pseudo
5060
51-
var opds : opd_stack
61+
var vals : val_stack
5262
var ctrls : ctrl_stack
5363
5464
However, these variables are not manipulated directly by the main checking function, but through a set of auxiliary functions:
5565

5666
.. code-block:: pseudo
5767
58-
func push_opd(type : val_type | Unknown) =
59-
opds.push(type)
68+
func push_val(type : val_type | Unknown) =
69+
vals.push(type)
6070
61-
func pop_opd() : val_type | Unknown =
62-
if (opds.size() = ctrls[0].height && ctrls[0].unreachable) return Unknown
63-
error_if(opds.size() = ctrls[0].height)
64-
return opds.pop()
71+
func pop_val() : val_type | Unknown =
72+
if (vals.size() = ctrls[0].height && ctrls[0].unreachable) return Unknown
73+
error_if(vals.size() = ctrls[0].height)
74+
return vals.pop()
6575
66-
func pop_opd(expect : val_type | Unknown) : val_type | Unknown =
67-
let actual = pop_opd()
76+
func pop_val(expect : val_type | Unknown) : val_type | Unknown =
77+
let actual = pop_val()
6878
if (actual = Unknown) return expect
6979
if (expect = Unknown) return actual
7080
error_if(actual =/= expect)
7181
return actual
7282
73-
func push_opds(types : list(val_type)) = foreach (t in types) push_opd(t)
74-
func pop_opds(types : list(val_type)) = foreach (t in reverse(types)) pop_opd(t)
83+
func push_vals(types : list(val_type)) = foreach (t in types) push_val(t)
84+
func pop_vals(types : list(val_type)) : list(val_type) =
85+
var popped := []
86+
foreach (t in reverse(types)) popped.append(pop_val(t))
87+
return popped
7588
76-
Pushing an operand simply pushes the respective type to the operand stack.
89+
Pushing an operand value simply pushes the respective type to the value stack.
7790

78-
Popping an operand checks that the operand stack does not underflow the current block and then removes one type.
79-
But first, a special case is handled where the block contains no known operands, but has been marked as unreachable.
91+
Popping an operand value checks that the value stack does not underflow the current block and then removes one type.
92+
But first, a special case is handled where the block contains no known values, but has been marked as unreachable.
8093
That can occur after an unconditional branch, when the stack is typed :ref:`polymorphically <polymorphism>`.
8194
In that case, an unknown type is returned.
8295

83-
A second function for popping an operand takes an expected type, which the actual operand type is checked against.
96+
A second function for popping an operand value takes an expected type, which the actual operand type is checked against.
8497
The types may differ in case one of them is Unknown.
85-
The more specific type is returned.
98+
The function returns the actual type popped from the stack.
8699

87100
Finally, there are accumulative functions for pushing or popping multiple operand types.
88101

89102
.. note::
90103
The notation :code:`stack[i]` is meant to index the stack from the top,
91-
so that :code:`ctrls[0]` accesses the element pushed last.
104+
so that, e.g., :code:`ctrls[0]` accesses the element pushed last.
92105

93106

94107
The control stack is likewise manipulated through auxiliary functions:
95108

96109
.. code-block:: pseudo
97110
98111
func push_ctrl(opcode : opcode, in : list(val_type), out : list(val_type)) =
99-
 let frame = ctrl_frame(opcode, in, out, opds.size(), false)
112+
 let frame = ctrl_frame(opcode, in, out, vals.size(), false)
100113
  ctrls.push(frame)
101-
push_opds(in)
114+
push_vals(in)
102115
103116
func pop_ctrl() : ctrl_frame =
104117
 error_if(ctrls.is_empty())
105118
 let frame = ctrls[0]
106-
  pop_opds(frame.end_types)
107-
  error_if(opds.size() =/= frame.height)
119+
  pop_vals(frame.end_types)
120+
  error_if(vals.size() =/= frame.height)
108121
ctrls.pop()
109122
  return frame
110123
111124
func label_types(frame : ctrl_frame) : list(val_types) =
112125
return (if frame.opcode == loop then frame.start_types else frame.end_types)
113126
114127
func unreachable() =
115-
  opds.resize(ctrls[0].height)
128+
  vals.resize(ctrls[0].height)
116129
  ctrls[0].unreachable := true
117130
118131
Pushing a control frame takes the types of the label and result values.
@@ -125,7 +138,7 @@ Afterwards, it checks that the stack has shrunk back to its initial height.
125138
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.
126139

127140
Finally, the current frame can be marked as unreachable.
128-
In that case, all existing operand types are purged from the operand stack, in order to allow for the :ref:`stack-polymorphism <polymorphism>` logic in :code:`pop_opd` to take effect.
141+
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.
129142

130143
.. note::
131144
Even with the unreachable flag set, consecutive operands are still pushed to and popped from the operand stack.
@@ -150,38 +163,46 @@ Other instructions are checked in a similar manner.
150163
func validate(opcode) =
151164
switch (opcode)
152165
case (i32.add)
153-
pop_opd(I32)
154-
pop_opd(I32)
155-
push_opd(I32)
166+
pop_val(I32)
167+
pop_val(I32)
168+
push_val(I32)
156169
157170
case (drop)
158-
pop_opd()
171+
pop_val()
159172
160173
case (select)
161-
pop_opd(I32)
162-
let t1 = pop_opd()
163-
let t2 = pop_opd(t1)
164-
push_opd(t2)
174+
pop_val(I32)
175+
let t1 = pop_val()
176+
let t2 = pop_val()
177+
error_if(not (is_num(t1) && is_num(t2)))
178+
error_if(t1 =/= t2 && t1 =/= Unknown && t2 =/= Unknown)
179+
push_val(if (t1 = Unknown) t2 else t1)
180+
181+
case (select t)
182+
pop_val(I32)
183+
pop_val(t)
184+
pop_val(t)
185+
push_val(t)
165186
166187
   case (unreachable)
167188
      unreachable()
168189
169190
case (block t1*->t2*)
170-
pop_opds([t1*])
191+
pop_vals([t1*])
171192
push_ctrl(block, [t1*], [t2*])
172193
173194
case (loop t1*->t2*)
174-
pop_opds([t1*])
195+
pop_vals([t1*])
175196
push_ctrl(loop, [t1*], [t2*])
176197
177198
case (if t1*->t2*)
178-
pop_opd(I32)
179-
pop_opds([t1*])
199+
pop_val(I32)
200+
pop_vals([t1*])
180201
push_ctrl(if, [t1*], [t2*])
181202
182203
case (end)
183204
let frame = pop_ctrl()
184-
push_opds(frame.end_types)
205+
push_vals(frame.end_types)
185206
186207
case (else)
187208
let frame = pop_ctrl()
@@ -190,23 +211,27 @@ Other instructions are checked in a similar manner.
190211
191212
case (br n)
192213
     error_if(ctrls.size() < n)
193-
      pop_opds(label_types(ctrls[n]))
214+
      pop_vals(label_types(ctrls[n]))
194215
      unreachable()
195216
196217
case (br_if n)
197218
     error_if(ctrls.size() < n)
198-
pop_opd(I32)
199-
      pop_opds(label_types(ctrls[n]))
200-
      push_opds(label_types(ctrls[n]))
219+
pop_val(I32)
220+
      pop_vals(label_types(ctrls[n]))
221+
      push_vals(label_types(ctrls[n]))
201222
202223
   case (br_table n* m)
224+
pop_val(I32)
203225
      error_if(ctrls.size() < m)
226+
let arity = label_types(ctrls[m]).size()
204227
      foreach (n in n*)
205-
        error_if(ctrls.size() < n || label_types(ctrls[n]) =/= label_types(ctrls[m]))
206-
pop_opd(I32)
207-
      pop_opds(label_types(ctrls[m]))
228+
        error_if(ctrls.size() < n)
229+
        error_if(label_types(ctrls[n]).size() =/= arity)
230+
push_vals(pop_vals(label_types(ctrls[n])))
231+
pop_vals(label_types(ctrls[m]))
208232
      unreachable()
209233
234+
210235
.. note::
211236
It is an invariant under the current WebAssembly instruction set that an operand of :code:`Unknown` type is never duplicated on the stack.
212237
This would change if the language were extended with stack instructions like :code:`dup`.

0 commit comments

Comments
 (0)