Skip to content

Commit 9d2d677

Browse files
committed
Merge branch 'funcref'
2 parents cd8b5c5 + ec004f6 commit 9d2d677

32 files changed

+527
-229
lines changed

.github/workflows/ci-interpreter.yml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ name: CI for interpreter & tests
33
on:
44
push:
55
branches: [ main ]
6-
paths: [ interpreter/**, test/** ]
6+
paths: [ .github/**, interpreter/**, test/** ]
77

88
pull_request:
99
branches: [ main ]
10-
paths: [ interpreter/**, test/** ]
10+
paths: [ .github/**, interpreter/**, test/** ]
1111

1212
# Allows you to run this workflow manually from the Actions tab
1313
workflow_dispatch:

.github/workflows/ci-spec.yml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,11 @@ name: CI for specs
33
on:
44
push:
55
branches: [ main ]
6-
paths: [ document/** ]
6+
paths: [ .github/**, document/** ]
77

88
pull_request:
99
branches: [ main ]
10-
paths: [ document/** ]
10+
paths: [ .github/**, document/** ]
1111

1212
# Allows you to run this workflow manually from the Actions tab
1313
workflow_dispatch:

.github/workflows/w3c-publish.yml

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
name: Publish to W3C TR space
2+
3+
on:
4+
push:
5+
branches: [ main ]
6+
paths: [ .github/**, document/** ]
7+
8+
# Allows you to run this workflow manually from the Actions tab
9+
workflow_dispatch:
10+
11+
jobs:
12+
publish-to-w3c-TR:
13+
if: github.repository == 'WebAssembly/spec'
14+
runs-on: ubuntu-latest
15+
steps:
16+
- name: Checkout repo
17+
uses: actions/checkout@v2
18+
with:
19+
submodules: "recursive"
20+
- name: Setup Node.js
21+
uses: actions/setup-node@v3
22+
with:
23+
node-version: 16
24+
- name: Setup Bikeshed
25+
run: pip install bikeshed && bikeshed update
26+
- name: Setup TexLive
27+
run: sudo apt-get update -y && sudo apt-get install -y latexmk texlive-latex-recommended texlive-latex-extra texlive-fonts-recommended
28+
- name: Setup Sphinx
29+
run: pip install six && pip install sphinx==5.1.0
30+
- name: Publish all specs to their https://www.w3.org/TR/ URLs
31+
run: cd document && make -e WD-echidna-CI
32+
env:
33+
STATUS: --md-status=WD
34+
W3C_ECHIDNA_TOKEN_CORE: ${{ secrets.W3C_ECHIDNA_TOKEN_CORE }}
35+
W3C_ECHIDNA_TOKEN_JSAPI: ${{ secrets.W3C_ECHIDNA_TOKEN_JSAPI }}
36+
W3C_ECHIDNA_TOKEN_WEBAPI: ${{ secrets.W3C_ECHIDNA_TOKEN_WEBAPI }}
37+
YARN_ENABLE_IMMUTABLE_INSTALLS: false

document/Makefile

Lines changed: 21 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
1-
DIRS = core js-api web-api
1+
DIRS = js-api web-api core
22
FILES = index.html
33
BUILDDIR = _build
4+
TAR = tar
45

56
# Global targets.
67

@@ -24,6 +25,25 @@ clean: $(DIRS:%=clean-%)
2425
.PHONY: diff
2526
diff: $(DIRS:%=diff-%)
2627

28+
# macOS: do “brew install tar” & run “make” as: TAR=gtar make -e WD-tar
29+
.PHONY: WD-tar
30+
WD-tar:
31+
for dir in $(DIRS); \
32+
do STATUS=--md-status=WD TAR=$(TAR) $(MAKE) -e -C $$dir $@;\
33+
done
34+
35+
# macOS: do “brew install tar” & run “make” as: TAR=gtar make -e WD-echidna
36+
.PHONY: WD-echidna
37+
WD-echidna:
38+
for dir in $(DIRS); \
39+
do $(MAKE) -e -C $$dir $@;\
40+
done
41+
42+
.PHONY: WD-echidna-CI
43+
WD-echidna-CI:
44+
for dir in $(DIRS); \
45+
do $(MAKE) -e -C $$dir $@;\
46+
done
2747

2848
# Directory-specific targets.
2949

document/core/Makefile

Lines changed: 25 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,8 @@ BUILDDIR = _build
99
STATICDIR = _static
1010
DOWNLOADDIR = _download
1111
NAME = WebAssembly
12+
DECISION_URL = https://github.com/WebAssembly/meetings/blob/main/main/2017/WG-12-06.md
13+
TAR = tar
1214

1315
# Internal variables.
1416
PAPEROPT_a4 = -D latex_paper_size=a4
@@ -78,7 +80,7 @@ publish-main: clean main bikeshed-keep deploy
7880
all: pdf html bikeshed
7981

8082
.PHONY: main
81-
main: pdf html
83+
main: macrosok pdf html
8284

8385
# Dirty hack to avoid rebuilding the Bikeshed version for every push.
8486
.PHONY: bikeshed-keep
@@ -95,6 +97,10 @@ GENERATED = appendix/index-instructions.rst
9597
%.rst: %.py
9698
(cd `dirname $@`; ./`basename $^`)
9799

100+
.PHONY: macrosok
101+
macrosok: $(GENERATED)
102+
sh util/check_macros.sh
103+
98104
.PHONY: pdf
99105
pdf: $(GENERATED) latexpdf
100106
mkdir -p $(BUILDDIR)/html/$(DOWNLOADDIR)
@@ -148,7 +154,7 @@ bikeshed: $(GENERATED)
148154
@echo
149155
@echo =========================================================================
150156
mkdir -p $(BUILDDIR)/bikeshed_mathjax/
151-
bikeshed spec index.bs $(BUILDDIR)/bikeshed_mathjax/index.html
157+
bikeshed spec $(STATUS) index.bs $(BUILDDIR)/bikeshed_mathjax/index.html
152158
mkdir -p $(BUILDDIR)/html/bikeshed/
153159
(cd util/katex/ && yarn && yarn build && npm install --only=prod)
154160
python3 util/mathjax2katex.py $(BUILDDIR)/bikeshed_mathjax/index.html \
@@ -163,9 +169,11 @@ bikeshed: $(GENERATED)
163169
@echo "Build finished. The HTML page is in $(BUILDDIR)/html/bikeshed/."
164170

165171
.PHONY: WD-tar
172+
# macOS tar has no “--transform” option (only GNU tar does), so on macOS,
173+
# do “brew install tar” & run “make” like this: “TAR=gtar make -e WD-tar”
166174
WD-tar: bikeshed
167175
@echo "Building tar file..."
168-
tar cvf \
176+
$(TAR) cvf \
169177
$(BUILDDIR)/WD.tar \
170178
--transform='s|$(BUILDDIR)/html/bikeshed/||' \
171179
--transform='s|index.html|Overview.html|' \
@@ -190,6 +198,20 @@ WD-echidna: WD-tar
190198
@echo
191199
@echo "Published working draft. Check its status at https://labs.w3.org/echidna/api/status?id=`cat $(BUILDDIR)/WD-echidna-id.txt`"
192200

201+
.PHONY: WD-echidna-CI
202+
WD-echidna-CI: WD-tar
203+
@if [ -z $(W3C_ECHIDNA_TOKEN_CORE) ] || \
204+
[ -z $(DECISION_URL) ] ; then \
205+
echo "Must provide W3C_ECHIDNA_TOKEN_CORE and DECISION_URL environment variables"; \
206+
exit 1; \
207+
fi
208+
curl 'https://labs.w3.org/echidna/api/request' \
209+
-F "tar=@$(BUILDDIR)/WD.tar" \
210+
-F "token=$(W3C_ECHIDNA_TOKEN_CORE)" \
211+
-F "decision=$(DECISION_URL)" | tee $(BUILDDIR)/WD-echidna-id.txt
212+
@echo
213+
@echo "Published working draft. Check its status at https://labs.w3.org/echidna/api/status?id=`cat $(BUILDDIR)/WD-echidna-id.txt`"
214+
193215
.PHONY: diff
194216
diff: bikeshed
195217
@echo "Downloading the old single-file html spec..."

document/core/appendix/index-instructions.py

Lines changed: 42 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -405,48 +405,48 @@ def Instruction(name, opcode, type=None, validation=None, execution=None, operat
405405
Instruction(r'\F32X4.\REPLACELANE~\laneidx', r'\hex{FD}~~\hex{20}', r'[\V128~\F32] \to [\V128]', r'valid-vec-replace_lane', r'exec-vec-replace_lane'),
406406
Instruction(r'\F64X2.\EXTRACTLANE~\laneidx', r'\hex{FD}~~\hex{21}', r'[\V128] \to [\F64]', r'valid-vec-extract_lane', r'exec-vec-extract_lane'),
407407
Instruction(r'\F64X2.\REPLACELANE~\laneidx', r'\hex{FD}~~\hex{22}', r'[\V128~\F64] \to [\V128]', r'valid-vec-replace_lane', r'exec-vec-replace_lane'),
408-
Instruction(r'\I8X16.\VEQ', r'\hex{FD}~~\hex{23}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ieq'),
409-
Instruction(r'\I8X16.\VNE', r'\hex{FD}~~\hex{24}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ine'),
410-
Instruction(r'\I8X16.\VLT\K{\_s}', r'\hex{FD}~~\hex{25}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ilt_s'),
411-
Instruction(r'\I8X16.\VLT\K{\_u}', r'\hex{FD}~~\hex{26}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ilt_u'),
412-
Instruction(r'\I8X16.\VGT\K{\_s}', r'\hex{FD}~~\hex{27}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-igt_s'),
413-
Instruction(r'\I8X16.\VGT\K{\_u}', r'\hex{FD}~~\hex{28}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-igt_u'),
414-
Instruction(r'\I8X16.\VLE\K{\_s}', r'\hex{FD}~~\hex{29}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ile_s'),
415-
Instruction(r'\I8X16.\VLE\K{\_u}', r'\hex{FD}~~\hex{2A}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ile_u'),
416-
Instruction(r'\I8X16.\VGE\K{\_s}', r'\hex{FD}~~\hex{2B}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ige_s'),
417-
Instruction(r'\I8X16.\VGE\K{\_u}', r'\hex{FD}~~\hex{2C}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ige_u'),
418-
Instruction(r'\I16X8.\VEQ', r'\hex{FD}~~\hex{2D}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ieq'),
419-
Instruction(r'\I16X8.\VNE', r'\hex{FD}~~\hex{2E}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ine'),
420-
Instruction(r'\I16X8.\VLT\K{\_s}', r'\hex{FD}~~\hex{2F}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ilt_s'),
421-
Instruction(r'\I16X8.\VLT\K{\_u}', r'\hex{FD}~~\hex{30}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ilt_u'),
422-
Instruction(r'\I16X8.\VGT\K{\_s}', r'\hex{FD}~~\hex{31}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-igt_s'),
423-
Instruction(r'\I16X8.\VGT\K{\_u}', r'\hex{FD}~~\hex{32}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-igt_u'),
424-
Instruction(r'\I16X8.\VLE\K{\_s}', r'\hex{FD}~~\hex{33}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ile_s'),
425-
Instruction(r'\I16X8.\VLE\K{\_u}', r'\hex{FD}~~\hex{34}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ile_u'),
426-
Instruction(r'\I16X8.\VGE\K{\_s}', r'\hex{FD}~~\hex{35}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ige_s'),
427-
Instruction(r'\I16X8.\VGE\K{\_u}', r'\hex{FD}~~\hex{36}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ige_u'),
428-
Instruction(r'\I32X4.\VEQ', r'\hex{FD}~~\hex{37}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ieq'),
429-
Instruction(r'\I32X4.\VNE', r'\hex{FD}~~\hex{38}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ine'),
430-
Instruction(r'\I32X4.\VLT\K{\_s}', r'\hex{FD}~~\hex{39}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ilt_s'),
431-
Instruction(r'\I32X4.\VLT\K{\_u}', r'\hex{FD}~~\hex{3A}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ilt_u'),
432-
Instruction(r'\I32X4.\VGT\K{\_s}', r'\hex{FD}~~\hex{3B}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-igt_s'),
433-
Instruction(r'\I32X4.\VGT\K{\_u}', r'\hex{FD}~~\hex{3C}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-igt_u'),
434-
Instruction(r'\I32X4.\VLE\K{\_s}', r'\hex{FD}~~\hex{3D}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ile_s'),
435-
Instruction(r'\I32X4.\VLE\K{\_u}', r'\hex{FD}~~\hex{3E}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ile_u'),
436-
Instruction(r'\I32X4.\VGE\K{\_s}', r'\hex{FD}~~\hex{3F}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ige_s'),
437-
Instruction(r'\I32X4.\VGE\K{\_u}', r'\hex{FD}~~\hex{40}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-ige_u'),
438-
Instruction(r'\F32X4.\VEQ', r'\hex{FD}~~\hex{41}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-feq'),
439-
Instruction(r'\F32X4.\VNE', r'\hex{FD}~~\hex{42}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fne'),
440-
Instruction(r'\F32X4.\VLT', r'\hex{FD}~~\hex{43}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-flt'),
441-
Instruction(r'\F32X4.\VGT', r'\hex{FD}~~\hex{44}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fgt'),
442-
Instruction(r'\F32X4.\VLE', r'\hex{FD}~~\hex{45}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fle'),
443-
Instruction(r'\F32X4.\VGE', r'\hex{FD}~~\hex{46}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fge'),
444-
Instruction(r'\F64X2.\VEQ', r'\hex{FD}~~\hex{47}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-feq'),
445-
Instruction(r'\F64X2.\VNE', r'\hex{FD}~~\hex{48}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fne'),
446-
Instruction(r'\F64X2.\VLT', r'\hex{FD}~~\hex{49}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-flt'),
447-
Instruction(r'\F64X2.\VGT', r'\hex{FD}~~\hex{4A}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fgt'),
448-
Instruction(r'\F64X2.\VLE', r'\hex{FD}~~\hex{4B}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fle'),
449-
Instruction(r'\F64X2.\VGE', r'\hex{FD}~~\hex{4C}', r'[\V128~\V128] \to [\V128]', r'valid-vbinop', r'exec-vbinop', r'op-fge'),
408+
Instruction(r'\I8X16.\VEQ', r'\hex{FD}~~\hex{23}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ieq'),
409+
Instruction(r'\I8X16.\VNE', r'\hex{FD}~~\hex{24}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ine'),
410+
Instruction(r'\I8X16.\VLT\K{\_s}', r'\hex{FD}~~\hex{25}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ilt_s'),
411+
Instruction(r'\I8X16.\VLT\K{\_u}', r'\hex{FD}~~\hex{26}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ilt_u'),
412+
Instruction(r'\I8X16.\VGT\K{\_s}', r'\hex{FD}~~\hex{27}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-igt_s'),
413+
Instruction(r'\I8X16.\VGT\K{\_u}', r'\hex{FD}~~\hex{28}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-igt_u'),
414+
Instruction(r'\I8X16.\VLE\K{\_s}', r'\hex{FD}~~\hex{29}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ile_s'),
415+
Instruction(r'\I8X16.\VLE\K{\_u}', r'\hex{FD}~~\hex{2A}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ile_u'),
416+
Instruction(r'\I8X16.\VGE\K{\_s}', r'\hex{FD}~~\hex{2B}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ige_s'),
417+
Instruction(r'\I8X16.\VGE\K{\_u}', r'\hex{FD}~~\hex{2C}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ige_u'),
418+
Instruction(r'\I16X8.\VEQ', r'\hex{FD}~~\hex{2D}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ieq'),
419+
Instruction(r'\I16X8.\VNE', r'\hex{FD}~~\hex{2E}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ine'),
420+
Instruction(r'\I16X8.\VLT\K{\_s}', r'\hex{FD}~~\hex{2F}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ilt_s'),
421+
Instruction(r'\I16X8.\VLT\K{\_u}', r'\hex{FD}~~\hex{30}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ilt_u'),
422+
Instruction(r'\I16X8.\VGT\K{\_s}', r'\hex{FD}~~\hex{31}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-igt_s'),
423+
Instruction(r'\I16X8.\VGT\K{\_u}', r'\hex{FD}~~\hex{32}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-igt_u'),
424+
Instruction(r'\I16X8.\VLE\K{\_s}', r'\hex{FD}~~\hex{33}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ile_s'),
425+
Instruction(r'\I16X8.\VLE\K{\_u}', r'\hex{FD}~~\hex{34}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ile_u'),
426+
Instruction(r'\I16X8.\VGE\K{\_s}', r'\hex{FD}~~\hex{35}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ige_s'),
427+
Instruction(r'\I16X8.\VGE\K{\_u}', r'\hex{FD}~~\hex{36}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ige_u'),
428+
Instruction(r'\I32X4.\VEQ', r'\hex{FD}~~\hex{37}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ieq'),
429+
Instruction(r'\I32X4.\VNE', r'\hex{FD}~~\hex{38}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ine'),
430+
Instruction(r'\I32X4.\VLT\K{\_s}', r'\hex{FD}~~\hex{39}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ilt_s'),
431+
Instruction(r'\I32X4.\VLT\K{\_u}', r'\hex{FD}~~\hex{3A}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ilt_u'),
432+
Instruction(r'\I32X4.\VGT\K{\_s}', r'\hex{FD}~~\hex{3B}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-igt_s'),
433+
Instruction(r'\I32X4.\VGT\K{\_u}', r'\hex{FD}~~\hex{3C}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-igt_u'),
434+
Instruction(r'\I32X4.\VLE\K{\_s}', r'\hex{FD}~~\hex{3D}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ile_s'),
435+
Instruction(r'\I32X4.\VLE\K{\_u}', r'\hex{FD}~~\hex{3E}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ile_u'),
436+
Instruction(r'\I32X4.\VGE\K{\_s}', r'\hex{FD}~~\hex{3F}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ige_s'),
437+
Instruction(r'\I32X4.\VGE\K{\_u}', r'\hex{FD}~~\hex{40}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-ige_u'),
438+
Instruction(r'\F32X4.\VEQ', r'\hex{FD}~~\hex{41}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-feq'),
439+
Instruction(r'\F32X4.\VNE', r'\hex{FD}~~\hex{42}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fne'),
440+
Instruction(r'\F32X4.\VLT', r'\hex{FD}~~\hex{43}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-flt'),
441+
Instruction(r'\F32X4.\VGT', r'\hex{FD}~~\hex{44}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fgt'),
442+
Instruction(r'\F32X4.\VLE', r'\hex{FD}~~\hex{45}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fle'),
443+
Instruction(r'\F32X4.\VGE', r'\hex{FD}~~\hex{46}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fge'),
444+
Instruction(r'\F64X2.\VEQ', r'\hex{FD}~~\hex{47}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-feq'),
445+
Instruction(r'\F64X2.\VNE', r'\hex{FD}~~\hex{48}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fne'),
446+
Instruction(r'\F64X2.\VLT', r'\hex{FD}~~\hex{49}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-flt'),
447+
Instruction(r'\F64X2.\VGT', r'\hex{FD}~~\hex{4A}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fgt'),
448+
Instruction(r'\F64X2.\VLE', r'\hex{FD}~~\hex{4B}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fle'),
449+
Instruction(r'\F64X2.\VGE', r'\hex{FD}~~\hex{4C}', r'[\V128~\V128] \to [\V128]', r'valid-vrelop', r'exec-vrelop', r'op-fge'),
450450
Instruction(r'\V128.\VNOT', r'\hex{FD}~~\hex{4D}', r'[\V128] \to [\V128]', r'valid-vvunop', r'exec-vvunop', r'op-inot'),
451451
Instruction(r'\V128.\VAND', r'\hex{FD}~~\hex{4E}', r'[\V128~\V128] \to [\V128]', r'valid-vvbinop', r'exec-vvbinop', r'op-iand'),
452452
Instruction(r'\V128.\VANDNOT', r'\hex{FD}~~\hex{4F}', r'[\V128~\V128] \to [\V128]', r'valid-vvbinop', r'exec-vvbinop', r'op-iandnot'),

document/core/appendix/properties.rst

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ In order to state and prove soundness precisely, the typing rules must be extend
2121

2222

2323
.. index:: context, recursive type, recursive type index
24-
.. context-rec:
24+
.. _context-ext:
2525

2626
Contexts
2727
~~~~~~~~
@@ -717,10 +717,14 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
717717

718718
* Let :math:`\reftype^\ast` be the concatenation of all :math:`\reftype_i` in order.
719719

720+
* Let :math:`m` be the length of :math:`\moduleinst.\MIFUNCS`.
721+
720722
* Let :math:`n` be the length of :math:`\moduleinst.\MIDATAS`.
721723

724+
* Let :math:`x^\ast` be the sequence of :ref:`function indices <syntax-funcidx>` from :math:`0` to :math:`m-1`.
725+
722726
* Then the module instance is valid with :ref:`context <context>`
723-
:math:`\{\CTYPES~\deftype^\ast,` :math:`\CFUNCS~\functype^\ast,` :math:`\CTABLES~\tabletype^\ast,` :math:`\CMEMS~\memtype^\ast,` :math:`\CGLOBALS~\globaltype^\ast,` :math:`\CELEMS~\reftype^\ast,` :math:`\CDATAS~{\ok}^n\}`.
727+
:math:`\{\CTYPES~\deftype^\ast,` :math:`\CFUNCS~\functype^\ast,` :math:`\CTABLES~\tabletype^\ast,` :math:`\CMEMS~\memtype^\ast,` :math:`\CGLOBALS~\globaltype^\ast,` :math:`\CELEMS~\reftype^\ast,` :math:`\CDATAS~{\ok}^n,` :math:`\CREFS~x^\ast\}`.
724728

725729
.. math::
726730
~\\[-1ex]
@@ -762,7 +766,8 @@ where :math:`\val_1 \gg^+_S \val_2` denotes the transitive closure of the follow
762766
\CMEMS & \memtype^\ast, \\
763767
\CGLOBALS & \globaltype^\ast, \\
764768
\CELEMS & \reftype^\ast, \\
765-
\CDATAS & {\ok}^n ~\}
769+
\CDATAS & {\ok}^n, \\
770+
\CREFS & 0 \dots (|\funcaddr^\ast|-1) ~\}
766771
\end{array}
767772
\end{array}
768773
}

document/core/binary/modules.rst

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -105,6 +105,9 @@ Id Section
105105
12 :ref:`data count section <binary-datacountsec>`
106106
== ===============================================
107107

108+
.. note::
109+
Section ids do not always correspond to the :ref:`order of sections <binary-module>` in the encoding of a module.
110+
108111

109112
.. index:: ! custom section
110113
pair: binary format; custom section

0 commit comments

Comments
 (0)