From 8f411d5733a8c747f512d84f9e7ed5b1fc73e842 Mon Sep 17 00:00:00 2001 From: Luke Wagner Date: Sun, 1 May 2022 15:05:55 -0500 Subject: [PATCH] Revert component-model changes back to original core proposal --- .gitattributes | 7 + .gitignore | 5 + .gitmodules | 3 + .travis.yml | 25 + Contributing.md | 8 + LICENSE | 12 +- README.md | 36 +- deploy_key.enc | Bin 0 -> 3248 bytes design/README.md | 1 - design/high-level/Choices.md | 34 - design/high-level/FAQ.md | 26 - design/high-level/Goals.md | 55 - design/high-level/README.md | 5 - design/high-level/UseCases.md | 342 --- design/proposals/README.md | 5 - design/proposals/module-linking/Binary.md | 168 - .../Example-LinkTimeVirtualization.md | 93 - design/proposals/module-linking/Explainer.md | 948 ------ .../link-time-virtualization.svg | 1 - .../shared-everything-dynamic-linking.svg | 1 - document/Makefile | 76 + document/README.md | 23 + document/core/.gitignore | 3 + document/core/LICENSE | 50 + document/core/Makefile | 355 +++ document/core/README.md | 25 + document/core/appendix/algorithm.rst | 206 ++ document/core/appendix/custom.rst | 145 + document/core/appendix/embedding.rst | 622 ++++ document/core/appendix/implementation.rst | 137 + document/core/appendix/index-instructions.rst | 202 ++ document/core/appendix/index-rules.rst | 108 + document/core/appendix/index-types.rst | 24 + document/core/appendix/index.rst | 22 + document/core/appendix/properties.rst | 752 +++++ document/core/binary/conventions.rst | 118 + document/core/binary/index.rst | 13 + document/core/binary/instructions.rst | 381 +++ document/core/binary/modules.rst | 484 +++ document/core/binary/types.rst | 140 + document/core/binary/values.rst | 148 + document/core/conf.py | 480 +++ document/core/exec/conventions.rst | 134 + document/core/exec/index.rst | 13 + document/core/exec/instructions.rst | 1165 +++++++ document/core/exec/modules.rst | 799 +++++ document/core/exec/numerics.rst | 1551 ++++++++++ document/core/exec/runtime.rst | 594 ++++ document/core/index.bs | 29 + document/core/index.rst | 38 + document/core/intro/index.rst | 10 + document/core/intro/introduction.rst | 111 + document/core/intro/overview.rst | 143 + document/core/make.bat | 318 ++ document/core/static/custom.css | 72 + document/core/static/webassembly.png | Bin 0 -> 43955 bytes document/core/syntax/conventions.rst | 129 + document/core/syntax/index.rst | 13 + document/core/syntax/instructions.rst | 370 +++ document/core/syntax/modules.rst | 371 +++ document/core/syntax/types.rst | 216 ++ document/core/syntax/values.rst | 175 ++ document/core/text/conventions.rst | 157 + document/core/text/index.rst | 14 + document/core/text/instructions.rst | 478 +++ document/core/text/lexical.rst | 126 + document/core/text/modules.rst | 657 ++++ document/core/text/types.rst | 143 + document/core/text/values.rst | 253 ++ document/core/util/README.htmldiff.pl | 2 + document/core/util/bikeshed/conf.py | 470 +++ document/core/util/bikeshed_fixup.py | 61 + document/core/util/katex | 1 + document/core/util/katex_fix.patch | 42 + document/core/util/macros.def | 1041 +++++++ document/core/util/mathdef.py | 121 + document/core/util/mathdefbs.py | 126 + document/core/util/mathjax2katex.py | 265 ++ document/core/util/pseudo-lexer.py | 32 + document/core/valid/conventions.rst | 188 ++ document/core/valid/index.rst | 12 + document/core/valid/instructions.rst | 808 +++++ document/core/valid/modules.rst | 587 ++++ document/core/valid/types.rst | 198 ++ document/deploy.sh | 239 ++ document/index.html | 74 + document/js-api/Makefile | 44 + document/js-api/index.bs | 1131 +++++++ document/travis-deploy.sh | 80 + document/util/htmldiff.pl | 588 ++++ document/web-api/Makefile | 44 + document/web-api/index.bs | 233 ++ interpreter/.gitignore | 13 + {design => interpreter}/LICENSE | 0 interpreter/Makefile | 160 + interpreter/README.md | 408 +++ interpreter/binary/decode.ml | 671 ++++ interpreter/binary/decode.mli | 3 + interpreter/binary/encode.ml | 506 ++++ interpreter/binary/encode.mli | 5 + interpreter/binary/utf8.ml | 42 + interpreter/binary/utf8.mli | 4 + interpreter/exec/eval.ml | 451 +++ interpreter/exec/eval.mli | 10 + interpreter/exec/eval_numeric.ml | 197 ++ interpreter/exec/eval_numeric.mli | 9 + interpreter/exec/f32.ml | 14 + interpreter/exec/f32_convert.ml | 47 + interpreter/exec/f32_convert.mli | 8 + interpreter/exec/f64.ml | 9 + interpreter/exec/f64_convert.ml | 39 + interpreter/exec/f64_convert.mli | 8 + interpreter/exec/float.ml | 353 +++ interpreter/exec/i32.ml | 7 + interpreter/exec/i32_convert.ml | 45 + interpreter/exec/i32_convert.mli | 8 + interpreter/exec/i64.ml | 7 + interpreter/exec/i64_convert.ml | 51 + interpreter/exec/i64_convert.mli | 9 + interpreter/exec/int.ml | 301 ++ interpreter/exec/numeric_error.ml | 3 + interpreter/host/env.ml | 46 + interpreter/host/spectest.ml | 48 + interpreter/main/flags.ml | 7 + interpreter/main/main.ml | 55 + interpreter/meta/findlib/META | 4 + interpreter/meta/jslib/bsconfig.json | 6 + interpreter/meta/jslib/build.sh | 97 + interpreter/meta/jslib/wasm.ml | 9 + interpreter/meta/travis/build-test.sh | 12 + interpreter/meta/travis/install-ocaml.sh | 46 + interpreter/runtime/func.ml | 14 + interpreter/runtime/func.mli | 11 + interpreter/runtime/global.ml | 21 + interpreter/runtime/global.mli | 14 + interpreter/runtime/instance.ml | 41 + interpreter/runtime/memory.ml | 145 + interpreter/runtime/memory.mli | 44 + interpreter/runtime/table.ml | 54 + interpreter/runtime/table.mli | 23 + interpreter/script/import.ml | 20 + interpreter/script/import.mli | 8 + interpreter/script/js.ml | 416 +++ interpreter/script/js.mli | 1 + interpreter/script/run.ml | 513 ++++ interpreter/script/run.mli | 9 + interpreter/script/script.ml | 42 + interpreter/syntax/ast.ml | 257 ++ interpreter/syntax/operators.ml | 204 ++ interpreter/syntax/types.ml | 108 + interpreter/syntax/values.ml | 79 + interpreter/text/arrange.ml | 450 +++ interpreter/text/arrange.mli | 6 + interpreter/text/lexer.mli | 3 + interpreter/text/lexer.mll | 374 +++ interpreter/text/parse.ml | 28 + interpreter/text/parse.mli | 11 + interpreter/text/parser.mly | 838 +++++ interpreter/text/print.ml | 5 + interpreter/text/print.mli | 4 + interpreter/util/error.ml | 8 + interpreter/util/error.mli | 8 + interpreter/util/lib.ml | 194 ++ interpreter/util/lib.mli | 78 + interpreter/util/sexpr.ml | 32 + interpreter/util/sexpr.mli | 5 + interpreter/util/source.ml | 21 + interpreter/util/source.mli | 11 + interpreter/valid/valid.ml | 474 +++ interpreter/valid/valid.mli | 3 + interpreter/winmake.bat | 75 + papers/LICENSE | 1 + papers/pldi2017.pdf | Bin 0 -> 2501487 bytes proposals/module-linking/Binary.md | 198 ++ .../Example-LinkTimeVirtualization.md | 100 + .../Example-SharedEverythingDynamicLinking.md | 423 +-- proposals/module-linking/Explainer.md | 857 ++++++ .../module-linking/Subtyping.md | 48 +- .../link-time-virtualization.svg | 1 + .../shared-everything-dynamic-linking.svg | 1 + spec/README.md | 5 - test/LICENSE | 202 ++ test/README.md | 43 + test/Todo.md | 34 + test/build.py | 251 ++ test/core/.gitignore | 1 + test/core/README.md | 11 + test/core/address.wast | 589 ++++ test/core/align.wast | 866 ++++++ test/core/binary-leb128.wast | 963 ++++++ test/core/binary.wast | 781 +++++ test/core/block.wast | 1120 +++++++ test/core/br.wast | 606 ++++ test/core/br_if.wast | 665 ++++ test/core/br_table.wast | 1593 ++++++++++ test/core/break-drop.wast | 9 + test/core/call.wast | 451 +++ test/core/call_indirect.wast | 942 ++++++ test/core/comments.wast | Bin 0 -> 701 bytes test/core/const.wast | 802 +++++ test/core/conversions.wast | 499 +++ test/core/custom.wast | 120 + test/core/data.wast | 335 ++ test/core/elem.wast | 381 +++ test/core/endianness.wast | 217 ++ test/core/exports.wast | 198 ++ test/core/f32.wast | 2533 ++++++++++++++++ test/core/f32_bitwise.wast | 376 +++ test/core/f32_cmp.wast | 2422 +++++++++++++++ test/core/f64.wast | 2533 ++++++++++++++++ test/core/f64_bitwise.wast | 376 +++ test/core/f64_cmp.wast | 2422 +++++++++++++++ test/core/fac.wast | 89 + test/core/float_exprs.wast | 2570 ++++++++++++++++ test/core/float_literals.wast | 507 ++++ test/core/float_memory.wast | 157 + test/core/float_misc.wast | 678 +++++ test/core/forward.wast | 20 + test/core/func.wast | 661 ++++ test/core/func_ptrs.wast | 106 + test/core/globals.wast | 482 +++ test/core/i32.wast | 957 ++++++ test/core/i64.wast | 454 +++ test/core/if.wast | 933 ++++++ test/core/imports.wast | 593 ++++ test/core/inline-module.wast | 1 + test/core/int_exprs.wast | 350 +++ test/core/int_literals.wast | 151 + test/core/labels.wast | 328 ++ test/core/left-to-right.wast | 233 ++ test/core/linking.wast | 388 +++ test/core/load.wast | 567 ++++ test/core/local_get.wast | 226 ++ test/core/local_set.wast | 362 +++ test/core/local_tee.wast | 639 ++++ test/core/loop.wast | 469 +++ test/core/memory.wast | 212 ++ test/core/memory_grow.wast | 355 +++ test/core/memory_redundancy.wast | 65 + test/core/memory_size.wast | 85 + test/core/memory_trap.wast | 270 ++ test/core/names.wast | 1097 +++++++ test/core/nop.wast | 426 +++ test/core/return.wast | 479 +++ test/core/run.py | 109 + test/core/select.wast | 414 +++ test/core/skip-stack-guard-page.wast | 2284 ++++++++++++++ test/core/stack.wast | 220 ++ test/core/start.wast | 100 + test/core/store.wast | 417 +++ test/core/switch.wast | 150 + test/core/token.wast | 10 + test/core/traps.wast | 91 + test/core/type.wast | 59 + test/core/unreachable.wast | 299 ++ test/core/unreached-invalid.wast | 709 +++++ test/core/unwind.wast | 267 ++ test/core/utf8-custom-section-id.wast | 1792 +++++++++++ test/core/utf8-import-field.wast | 2672 ++++++++++++++++ test/core/utf8-import-module.wast | 2672 ++++++++++++++++ test/core/utf8-invalid-encoding.wast | 176 ++ test/harness/async_index.js | 375 +++ test/harness/sync_index.js | 339 +++ test/harness/testharness.css | 102 + test/harness/testharness.js | 2692 +++++++++++++++++ test/harness/testharnessreport.js | 17 + test/js-api/LICENSE.md | 33 + test/js-api/README.md | 71 + test/js-api/assertions.js | 73 + test/js-api/bad-imports.js | 152 + test/js-api/constructor/compile.any.js | 80 + .../instantiate-bad-imports.any.js | 22 + test/js-api/constructor/instantiate.any.js | 168 + test/js-api/constructor/validate.any.js | 99 + test/js-api/global/constructor.any.js | 127 + test/js-api/global/toString.any.js | 7 + test/js-api/global/value-get-set.any.js | 111 + test/js-api/global/valueOf.any.js | 28 + .../instance/constructor-bad-imports.any.js | 13 + test/js-api/instance/constructor.any.js | 54 + test/js-api/instance/exports.any.js | 66 + test/js-api/instance/toString.any.js | 9 + test/js-api/instanceTestFactory.js | 224 ++ test/js-api/interface.any.js | 160 + test/js-api/limits.any.js | 196 ++ test/js-api/memory/buffer.any.js | 64 + test/js-api/memory/constructor.any.js | 147 + test/js-api/memory/grow.any.js | 185 ++ test/js-api/memory/toString.any.js | 7 + test/js-api/module/constructor.any.js | 64 + test/js-api/module/customSections.any.js | 164 + test/js-api/module/exports.any.js | 131 + test/js-api/module/imports.any.js | 125 + test/js-api/module/toString.any.js | 8 + test/js-api/table/assertions.js | 13 + test/js-api/table/constructor.any.js | 179 ++ test/js-api/table/get-set.any.js | 225 ++ test/js-api/table/grow.any.js | 96 + test/js-api/table/length.any.js | 60 + test/js-api/table/toString.any.js | 7 + test/js-api/wasm-module-builder.js | 952 ++++++ w3c.json | 5 + 302 files changed, 86197 insertions(+), 1904 deletions(-) create mode 100644 .gitattributes create mode 100644 .gitignore create mode 100644 .gitmodules create mode 100644 .travis.yml create mode 100644 Contributing.md create mode 100644 deploy_key.enc delete mode 100644 design/README.md delete mode 100644 design/high-level/Choices.md delete mode 100644 design/high-level/FAQ.md delete mode 100644 design/high-level/Goals.md delete mode 100644 design/high-level/README.md delete mode 100644 design/high-level/UseCases.md delete mode 100644 design/proposals/README.md delete mode 100644 design/proposals/module-linking/Binary.md delete mode 100644 design/proposals/module-linking/Example-LinkTimeVirtualization.md delete mode 100644 design/proposals/module-linking/Explainer.md delete mode 100644 design/proposals/module-linking/link-time-virtualization.svg delete mode 100644 design/proposals/module-linking/shared-everything-dynamic-linking.svg create mode 100644 document/Makefile create mode 100644 document/README.md create mode 100644 document/core/.gitignore create mode 100644 document/core/LICENSE create mode 100644 document/core/Makefile create mode 100644 document/core/README.md create mode 100644 document/core/appendix/algorithm.rst create mode 100644 document/core/appendix/custom.rst create mode 100644 document/core/appendix/embedding.rst create mode 100644 document/core/appendix/implementation.rst create mode 100644 document/core/appendix/index-instructions.rst create mode 100644 document/core/appendix/index-rules.rst create mode 100644 document/core/appendix/index-types.rst create mode 100644 document/core/appendix/index.rst create mode 100644 document/core/appendix/properties.rst create mode 100644 document/core/binary/conventions.rst create mode 100644 document/core/binary/index.rst create mode 100644 document/core/binary/instructions.rst create mode 100644 document/core/binary/modules.rst create mode 100644 document/core/binary/types.rst create mode 100644 document/core/binary/values.rst create mode 100644 document/core/conf.py create mode 100644 document/core/exec/conventions.rst create mode 100644 document/core/exec/index.rst create mode 100644 document/core/exec/instructions.rst create mode 100644 document/core/exec/modules.rst create mode 100644 document/core/exec/numerics.rst create mode 100644 document/core/exec/runtime.rst create mode 100644 document/core/index.bs create mode 100644 document/core/index.rst create mode 100644 document/core/intro/index.rst create mode 100644 document/core/intro/introduction.rst create mode 100644 document/core/intro/overview.rst create mode 100644 document/core/make.bat create mode 100644 document/core/static/custom.css create mode 100644 document/core/static/webassembly.png create mode 100644 document/core/syntax/conventions.rst create mode 100644 document/core/syntax/index.rst create mode 100644 document/core/syntax/instructions.rst create mode 100644 document/core/syntax/modules.rst create mode 100644 document/core/syntax/types.rst create mode 100644 document/core/syntax/values.rst create mode 100644 document/core/text/conventions.rst create mode 100644 document/core/text/index.rst create mode 100644 document/core/text/instructions.rst create mode 100644 document/core/text/lexical.rst create mode 100644 document/core/text/modules.rst create mode 100644 document/core/text/types.rst create mode 100644 document/core/text/values.rst create mode 100644 document/core/util/README.htmldiff.pl create mode 100644 document/core/util/bikeshed/conf.py create mode 100755 document/core/util/bikeshed_fixup.py create mode 160000 document/core/util/katex create mode 100644 document/core/util/katex_fix.patch create mode 100644 document/core/util/macros.def create mode 100644 document/core/util/mathdef.py create mode 100644 document/core/util/mathdefbs.py create mode 100755 document/core/util/mathjax2katex.py create mode 100644 document/core/util/pseudo-lexer.py create mode 100644 document/core/valid/conventions.rst create mode 100644 document/core/valid/index.rst create mode 100644 document/core/valid/instructions.rst create mode 100644 document/core/valid/modules.rst create mode 100644 document/core/valid/types.rst create mode 100755 document/deploy.sh create mode 100644 document/index.html create mode 100644 document/js-api/Makefile create mode 100644 document/js-api/index.bs create mode 100755 document/travis-deploy.sh create mode 100755 document/util/htmldiff.pl create mode 100644 document/web-api/Makefile create mode 100644 document/web-api/index.bs create mode 100644 interpreter/.gitignore rename {design => interpreter}/LICENSE (100%) create mode 100644 interpreter/Makefile create mode 100644 interpreter/README.md create mode 100644 interpreter/binary/decode.ml create mode 100644 interpreter/binary/decode.mli create mode 100644 interpreter/binary/encode.ml create mode 100644 interpreter/binary/encode.mli create mode 100644 interpreter/binary/utf8.ml create mode 100644 interpreter/binary/utf8.mli create mode 100644 interpreter/exec/eval.ml create mode 100644 interpreter/exec/eval.mli create mode 100644 interpreter/exec/eval_numeric.ml create mode 100644 interpreter/exec/eval_numeric.mli create mode 100644 interpreter/exec/f32.ml create mode 100644 interpreter/exec/f32_convert.ml create mode 100644 interpreter/exec/f32_convert.mli create mode 100644 interpreter/exec/f64.ml create mode 100644 interpreter/exec/f64_convert.ml create mode 100644 interpreter/exec/f64_convert.mli create mode 100644 interpreter/exec/float.ml create mode 100644 interpreter/exec/i32.ml create mode 100644 interpreter/exec/i32_convert.ml create mode 100644 interpreter/exec/i32_convert.mli create mode 100644 interpreter/exec/i64.ml create mode 100644 interpreter/exec/i64_convert.ml create mode 100644 interpreter/exec/i64_convert.mli create mode 100644 interpreter/exec/int.ml create mode 100644 interpreter/exec/numeric_error.ml create mode 100644 interpreter/host/env.ml create mode 100644 interpreter/host/spectest.ml create mode 100644 interpreter/main/flags.ml create mode 100644 interpreter/main/main.ml create mode 100644 interpreter/meta/findlib/META create mode 100644 interpreter/meta/jslib/bsconfig.json create mode 100755 interpreter/meta/jslib/build.sh create mode 100644 interpreter/meta/jslib/wasm.ml create mode 100755 interpreter/meta/travis/build-test.sh create mode 100755 interpreter/meta/travis/install-ocaml.sh create mode 100644 interpreter/runtime/func.ml create mode 100644 interpreter/runtime/func.mli create mode 100644 interpreter/runtime/global.ml create mode 100644 interpreter/runtime/global.mli create mode 100644 interpreter/runtime/instance.ml create mode 100644 interpreter/runtime/memory.ml create mode 100644 interpreter/runtime/memory.mli create mode 100644 interpreter/runtime/table.ml create mode 100644 interpreter/runtime/table.mli create mode 100644 interpreter/script/import.ml create mode 100644 interpreter/script/import.mli create mode 100644 interpreter/script/js.ml create mode 100644 interpreter/script/js.mli create mode 100644 interpreter/script/run.ml create mode 100644 interpreter/script/run.mli create mode 100644 interpreter/script/script.ml create mode 100644 interpreter/syntax/ast.ml create mode 100644 interpreter/syntax/operators.ml create mode 100644 interpreter/syntax/types.ml create mode 100644 interpreter/syntax/values.ml create mode 100644 interpreter/text/arrange.ml create mode 100644 interpreter/text/arrange.mli create mode 100644 interpreter/text/lexer.mli create mode 100644 interpreter/text/lexer.mll create mode 100644 interpreter/text/parse.ml create mode 100644 interpreter/text/parse.mli create mode 100644 interpreter/text/parser.mly create mode 100644 interpreter/text/print.ml create mode 100644 interpreter/text/print.mli create mode 100644 interpreter/util/error.ml create mode 100644 interpreter/util/error.mli create mode 100644 interpreter/util/lib.ml create mode 100644 interpreter/util/lib.mli create mode 100644 interpreter/util/sexpr.ml create mode 100644 interpreter/util/sexpr.mli create mode 100644 interpreter/util/source.ml create mode 100644 interpreter/util/source.mli create mode 100644 interpreter/valid/valid.ml create mode 100644 interpreter/valid/valid.mli create mode 100644 interpreter/winmake.bat create mode 100644 papers/LICENSE create mode 100644 papers/pldi2017.pdf create mode 100644 proposals/module-linking/Binary.md create mode 100644 proposals/module-linking/Example-LinkTimeVirtualization.md rename {design/proposals => proposals}/module-linking/Example-SharedEverythingDynamicLinking.md (50%) create mode 100644 proposals/module-linking/Explainer.md rename {design/proposals => proposals}/module-linking/Subtyping.md (71%) create mode 100644 proposals/module-linking/link-time-virtualization.svg create mode 100644 proposals/module-linking/shared-everything-dynamic-linking.svg delete mode 100644 spec/README.md create mode 100644 test/LICENSE create mode 100644 test/README.md create mode 100644 test/Todo.md create mode 100755 test/build.py create mode 100644 test/core/.gitignore create mode 100644 test/core/README.md create mode 100644 test/core/address.wast create mode 100644 test/core/align.wast create mode 100644 test/core/binary-leb128.wast create mode 100644 test/core/binary.wast create mode 100644 test/core/block.wast create mode 100644 test/core/br.wast create mode 100644 test/core/br_if.wast create mode 100644 test/core/br_table.wast create mode 100644 test/core/break-drop.wast create mode 100644 test/core/call.wast create mode 100644 test/core/call_indirect.wast create mode 100644 test/core/comments.wast create mode 100644 test/core/const.wast create mode 100644 test/core/conversions.wast create mode 100644 test/core/custom.wast create mode 100644 test/core/data.wast create mode 100644 test/core/elem.wast create mode 100644 test/core/endianness.wast create mode 100644 test/core/exports.wast create mode 100644 test/core/f32.wast create mode 100644 test/core/f32_bitwise.wast create mode 100644 test/core/f32_cmp.wast create mode 100644 test/core/f64.wast create mode 100644 test/core/f64_bitwise.wast create mode 100644 test/core/f64_cmp.wast create mode 100644 test/core/fac.wast create mode 100644 test/core/float_exprs.wast create mode 100644 test/core/float_literals.wast create mode 100644 test/core/float_memory.wast create mode 100644 test/core/float_misc.wast create mode 100644 test/core/forward.wast create mode 100644 test/core/func.wast create mode 100644 test/core/func_ptrs.wast create mode 100644 test/core/globals.wast create mode 100644 test/core/i32.wast create mode 100644 test/core/i64.wast create mode 100644 test/core/if.wast create mode 100644 test/core/imports.wast create mode 100644 test/core/inline-module.wast create mode 100644 test/core/int_exprs.wast create mode 100644 test/core/int_literals.wast create mode 100644 test/core/labels.wast create mode 100644 test/core/left-to-right.wast create mode 100644 test/core/linking.wast create mode 100644 test/core/load.wast create mode 100644 test/core/local_get.wast create mode 100644 test/core/local_set.wast create mode 100644 test/core/local_tee.wast create mode 100644 test/core/loop.wast create mode 100644 test/core/memory.wast create mode 100644 test/core/memory_grow.wast create mode 100644 test/core/memory_redundancy.wast create mode 100644 test/core/memory_size.wast create mode 100644 test/core/memory_trap.wast create mode 100644 test/core/names.wast create mode 100644 test/core/nop.wast create mode 100644 test/core/return.wast create mode 100755 test/core/run.py create mode 100644 test/core/select.wast create mode 100644 test/core/skip-stack-guard-page.wast create mode 100644 test/core/stack.wast create mode 100644 test/core/start.wast create mode 100644 test/core/store.wast create mode 100644 test/core/switch.wast create mode 100644 test/core/token.wast create mode 100644 test/core/traps.wast create mode 100644 test/core/type.wast create mode 100644 test/core/unreachable.wast create mode 100644 test/core/unreached-invalid.wast create mode 100644 test/core/unwind.wast create mode 100644 test/core/utf8-custom-section-id.wast create mode 100644 test/core/utf8-import-field.wast create mode 100644 test/core/utf8-import-module.wast create mode 100644 test/core/utf8-invalid-encoding.wast create mode 100644 test/harness/async_index.js create mode 100644 test/harness/sync_index.js create mode 100644 test/harness/testharness.css create mode 100644 test/harness/testharness.js create mode 100644 test/harness/testharnessreport.js create mode 100644 test/js-api/LICENSE.md create mode 100644 test/js-api/README.md create mode 100644 test/js-api/assertions.js create mode 100644 test/js-api/bad-imports.js create mode 100644 test/js-api/constructor/compile.any.js create mode 100644 test/js-api/constructor/instantiate-bad-imports.any.js create mode 100644 test/js-api/constructor/instantiate.any.js create mode 100644 test/js-api/constructor/validate.any.js create mode 100644 test/js-api/global/constructor.any.js create mode 100644 test/js-api/global/toString.any.js create mode 100644 test/js-api/global/value-get-set.any.js create mode 100644 test/js-api/global/valueOf.any.js create mode 100644 test/js-api/instance/constructor-bad-imports.any.js create mode 100644 test/js-api/instance/constructor.any.js create mode 100644 test/js-api/instance/exports.any.js create mode 100644 test/js-api/instance/toString.any.js create mode 100644 test/js-api/instanceTestFactory.js create mode 100644 test/js-api/interface.any.js create mode 100644 test/js-api/limits.any.js create mode 100644 test/js-api/memory/buffer.any.js create mode 100644 test/js-api/memory/constructor.any.js create mode 100644 test/js-api/memory/grow.any.js create mode 100644 test/js-api/memory/toString.any.js create mode 100644 test/js-api/module/constructor.any.js create mode 100644 test/js-api/module/customSections.any.js create mode 100644 test/js-api/module/exports.any.js create mode 100644 test/js-api/module/imports.any.js create mode 100644 test/js-api/module/toString.any.js create mode 100644 test/js-api/table/assertions.js create mode 100644 test/js-api/table/constructor.any.js create mode 100644 test/js-api/table/get-set.any.js create mode 100644 test/js-api/table/grow.any.js create mode 100644 test/js-api/table/length.any.js create mode 100644 test/js-api/table/toString.any.js create mode 100644 test/js-api/wasm-module-builder.js create mode 100644 w3c.json diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 00000000..3171e903 --- /dev/null +++ b/.gitattributes @@ -0,0 +1,7 @@ +*.rst linguist-documentation=false +document/* linguist-documentation=false +document/*.rst linguist-documentation=false +document/*/*.rst linguist-documentation=false +test/harness/wast.js linguist-vendored +test/harness/testharness* linguist-vendored + diff --git a/.gitignore b/.gitignore new file mode 100644 index 00000000..6739bb2b --- /dev/null +++ b/.gitignore @@ -0,0 +1,5 @@ +**/*~ +**/*.tmproj +**/*.pyc +**/_build +**/_output diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 00000000..385b304b --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "document/core/util/katex"] + path = document/core/util/katex + url = https://github.com/KaTeX/KaTeX.git diff --git a/.travis.yml b/.travis.yml new file mode 100644 index 00000000..275b88e1 --- /dev/null +++ b/.travis.yml @@ -0,0 +1,25 @@ +language: c++ +language: python +python: + - "2.7" + +sudo: on + +install: + - ./interpreter/meta/travis/install-ocaml.sh + - sudo pip install sphinx==1.7.9 + - 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 + - bash ./document/travis-deploy.sh + +os: linux + +env: + global: + - ENCRYPTION_LABEL: "304454be9d6c" + - COMMIT_AUTHOR_EMAIL: "noreply@webassembly.org" diff --git a/Contributing.md b/Contributing.md new file mode 100644 index 00000000..1cc607fa --- /dev/null +++ b/Contributing.md @@ -0,0 +1,8 @@ +# Contributing to WebAssembly + +Interested in participating? Please follow +[the same contributing guidelines as the design repository][]. + + [the same contributing guidelines as the design repository]: https://github.com/WebAssembly/design/blob/master/Contributing.md + +Also, please be sure to read [the README.md](README.md) for this repository. diff --git a/LICENSE b/LICENSE index c5587c38..de2cac69 100644 --- a/LICENSE +++ b/LICENSE @@ -1,10 +1,8 @@ -Please see the LICENSE file for particular directories for the terms applicable -to that directory and its relative sub-directories. +Please see the LICENSE file in each top-level directory for the terms applicable to that directory and its relative sub-directories. The relevant directories and licenses are: -design/ - Apache License 2.0 - -(Other directories will be added when the [module-linking] repository merges.) - -[module-linking]: https://github.com/webassembly/module-linking/ +document/ - W3C Software and Document Notice and License +interpreter/ - Apache License 2.0 +test/ - Apache License 2.0 +papers/ - Creative Commons Attribution 4.0 International License diff --git a/README.md b/README.md index fd67bedb..eb3500c0 100644 --- a/README.md +++ b/README.md @@ -1,17 +1,27 @@ -# Module Linking proposal +[![Build Status](https://travis-ci.org/WebAssembly/spec.svg?branch=master)](https://travis-ci.org/WebAssembly/spec) -This repository contains the Module Linking proposal, which is the -first proposal of the [Component Model]. +# Module Linking Proposal for WebAssembly -Links: -* the general [explainer](design/proposals/module-linking/Explainer.md) for this proposal -* a sketch of the [binary format](design/proposals/module-linking/Binary.md) -* a description of [module subtyping](design/proposals/module-linking/Subtyping.md) +This repository is a clone of [github.com/WebAssembly/spec/](https://github.com/WebAssembly/spec/). +It is meant for discussion, prototype specification and implementation of a +proposal to add support for module linking to WebAssembly. -All Component Model work is done as part of the [W3C WebAssembly Community Group]. -To contribute to any of these repositories, see the Community Group's -[Contributing Guidelines]. +See the [explainer](proposals/module-linking/Explainer.md) for a summary of the +proposal. -[Component Model]: https://github.com/webassembly/component-model/ -[W3C WebAssembly Community Group]: https://www.w3.org/community/webassembly/ -[Contributing Guidelines]: https://webassembly.org/community/contributing/ +# spec + +This repository holds the sources for the WebAssembly draft specification +(to seed a future +[WebAssembly Working Group](https://lists.w3.org/Archives/Public/public-new-work/2017Jun/0005.html)), +a reference implementation, and the official testsuite. + +A formatted version of the spec is available here: +[webassembly.github.io/spec](https://webassembly.github.io/spec/), + +Participation is welcome. Discussions about new features, significant semantic +changes, or any specification change likely to generate substantial discussion +should take place in +[the WebAssembly design repository](https://github.com/WebAssembly/design) +first, so that this spec repository can remain focused. And please follow the +[guidelines for contributing](Contributing.md). diff --git a/deploy_key.enc b/deploy_key.enc new file mode 100644 index 0000000000000000000000000000000000000000..b6d3e2f19771652a9711760b1712a77fe1b4e579 GIT binary patch literal 3248 zcmV;h3{UeoaMr!6kTNmX>{8Y#<|(CVbO6TJr-;79Ag-eBM!B~g(FTQ5ldW}>C6w#F z7?FSyFeYZ$v_V^lQFEF>+7k9B7m`7vS_SQ$;wWv|QOclL{NpaXb;g5ti(%WUt|3;5 z3CA#OrS)XS){2AUta7q}MSmhTJq zo{c?28()!ibPsqvTfOAA!4zOONU^F*gLcD(DrJbnNphXRZ3yC#LaPJi{CC$C(2A_7 zNaF$Iwo+ftMAzTpRFW1@B>=0mk{V^}DS!4rt3&v*?r8!}EfiTzY#jX?%ckauU9h@W zx(fD`Pk=~T7D1zi5Xgo-F3df<=bCbjU0(ZD&z`12ST)Xxn<2-%!cB^F0IoG~-*{lROB{l$8;> zQYD6uvZB!WjR97=Gm5k(nd?fS-skc&EK?_V8WnS+v(_4N1NbVfWy{T9c3+w+eKW@y z`gzb1V%Tr>ul(ay+I}7y2o4<>nNeC`_9<4dQwbaZcv=lR5j&@)QY$OIg__IEl?CzP zj*w)N-7!X;zax-wu2%HYpX17nK^l2cLppXhM>Q8<9AmF4V+?wF~S-rGWRU;<& zEfi}`>wt%Un_w@H!oNoZ>x+M|o6OWL0ZWAvCDS3ci~T8hKI0BHLyhmaX>a@YdQNK^9SJORstB zfvrm3TfM$`MMQQXp+4m=U~?Y#8>LXJEJKe+QT3ai?lI{90Zbd!SJdk4H(U1tebkQS zElH@QyluL-tMcF~ED_;l>!0Ijv*4gtnDwmLYV{a3@tjZ`D zFgG=OkZ90lfbv6>Fy&2v?b=c~Y_N9G zUi9};vfpk;9dPn4FMkaR{o~nn&h!a-?Sdb%SZ)!fI~GWnk~X{F~0*MZTR*=jmm-h1@t zDL!$f-TC0j9#3k6yGm=yVm`^%@wfi3bq#*03KSe>$d+&xjHOcMc8uJt8)hN2{SBal z4ob$b$`dj=o#p1YnW?UI^yZ;rkMjLI{F#<8G09bp2NC-f7?!MtUZ(JwIdFlSzu%EdX7u+as(dHl z58QQZ`uk&2UcuOD{=l^SW7lbUC)YQxLZoD(4yfjbALj)ocgYIM0ZYz?(TpdH^*N^lP&fD?>5S3l5d9vDe0MYX}=L@v0ac*d^h zMC3X&i8_TGc*nis1+Hbb@FGCYM0^b7+Ks%np4Yi`?%nMjTjK}kiD^peA^u+*e>(aKEP(B~>~mZq#KO^e z%~M*@SsY^h6(tY`GdMou`@})%F*bIbRNZ>mC~Kmlo-i?%UtfW#dT*z*RcdL zpk60TCgJqxKBvX~s$%Shh(AI%*I`@P2!X_@lhC_lv0_yIg6%&*TKAQRPZQNW>=_H-#1pBvjD+m{Zb}zcH8nbpNqr9whn4 zA=y)BHKQ-DrD~ATW$s5sLj-tJ#cf~=mO{+4YNwZc;4(}zeG0i5iXTW*#VVOL90%~C zVKMQHgk?j=XH43>K+-CeY3%JXI)VIB$Ad;DSsk-VJs=GfjP+|s{r){_ozCKbFDNi| zfEk3yUlIo}(x+SiFz(8%;%1%!B5`O|M9Tgg3bui&lu)v`(ydUn{aib=ktlW8MU&;r zQ+2LIr_4e3%GTLQ5?58orh7HmWd&Z&T0Uz!9~Ha`K^gp=fQ`FR=0~z|>MuzT4#e%& zBXJPHh`^tE;|zIgNiR(*kU@PB&}J%3Coh;M^QnC8vP7h%*_Gozd?$RZWr_#dXYF>u zT>^8L;b}KO+gPONfMBv1ae%Hy6R+;S^w+Ng{zo&nGB`o<^fxC>{v`=!WnoSACN9e? z!P}dgK-N^z=5p%- zjAkKdA-dFrZxs{<7wntcycPzJOC})W{%YX>7&0{p8S%XXI0{sJi2me-X!z#kb@^(L zIrTxbTFMXTi!+maqh2OdhC54A&#rQ{4~>UL|6E*af1FP^b#OX~#=VRt;}}z+FhX7& z(?0)PAKjGZ*g(dZNg81514!QK;bQWS0-qDq&xgnv8vdcEkLzW9YdU7Q`jSwWHd*~b zqQ?O;jM%iLY>Zw*$r*lZ~?dz)vtCi6GqzmKd+b z!(zZgpXf?*+wbzsxQ&XJ3)2p#3|IEa$pe0b>QbH=rr|j)yS-i=SFADE7tJ`oCmN@} zL{UA^mr)_ZWdcbz>BGLSKFnFY^oV4EXulUCv6iQUG?d~nuNbxQiWI`F1pbLxAfG^h iY#Pu|2q&8>`3}#6q-2Cz`ZEbT?K&=q;2asiqpF?e?>4gl literal 0 HcmV?d00001 diff --git a/design/README.md b/design/README.md deleted file mode 100644 index b9032baa..00000000 --- a/design/README.md +++ /dev/null @@ -1 +0,0 @@ -See the [parent README](../README.md). diff --git a/design/high-level/Choices.md b/design/high-level/Choices.md deleted file mode 100644 index ff48a3b9..00000000 --- a/design/high-level/Choices.md +++ /dev/null @@ -1,34 +0,0 @@ -# Component Model High-Level Design Choices - -Based on the [goals](Goals.md) and [use cases](UseCases.md), the component -model makes several high-level design choices that permeate the rest of the -component model. - -1. The component model adopts a shared-nothing architecture in which component - instances fully encapsulate their linear memories, tables, globals and, in - the future, GC memory. Component interfaces contain only immutable copied - values, opaque typed handles and immutable uninstantiated modules/components. - While handles and imports can be used as an indirect form of sharing, the - [dependency use cases](UseCases.md#component-dependencies) enable this degree - of sharing to be finely controlled. - -2. The component model introduces no global singletons, namespaces, registries, - locator services or frameworks through which components are configured or - linked. Instead, all related use cases are addressed through explicit - parametrization of components via imports (of data, functions, and types) - with every client of a component having the option to independently - instantiate the component with its own chosen import values. - -3. The component model assumes no global inter-component garbage or cycle - collector that is able to trace through cross-component cycles. Instead - resources have lifetimes and require explicit acyclic ownership through - handles. The explicit lifetimes allow resources to have destructors that are - called deterministically and can be used to release linear memory - allocations in non-garbage-collected languages. - -4. The component model assumes that Just-In-Time compilation is not available - at runtime and thus only provides declarative linking features that admit - Ahead-of-Time compilation, optimization and analysis. While component instances - can be created at runtime, the components being instantiated as well as their - dependencies and clients are known before execution begins. - (See also [this slide](https://docs.google.com/presentation/d/1PSC3Q5oFsJEaYyV5lNJvVgh-SNxhySWUqZ6puyojMi8/edit#slide=id.gceaf867ebf_0_10).) diff --git a/design/high-level/FAQ.md b/design/high-level/FAQ.md deleted file mode 100644 index f403f8ec..00000000 --- a/design/high-level/FAQ.md +++ /dev/null @@ -1,26 +0,0 @@ -# FAQ - -### How does WASI relate to the Component Model? - -[WASI] is layered on top of the Component Model, with the Component Model -providing the foundational building blocks used to define WASI's interfaces, -including: -* the grammar of types that can be used in WASI interfaces; -* the linking functionality that WASI can assume is used to compose separate - modules of code, isolate their capabilities and virtualize WASI interfaces; -* the core wasm ABI that core wasm toolchains can compile against when targeting WASI. - -By way of comparison to traditional Operating Systems, the Component Model -fills the role of an OS's process model (defining how processes start up and -communicate with each other) while WASI fills the role of an OS's many I/O -interfaces. - -Use of WASI does not force the client to target the Component Model, however. -Any core wasm producer can simply target the core wasm ABI defined by the -Component Model for a given WASI interface's signature. This approach reopens -many questions that are answered by the Component Model, particularly when more -than one wasm module is involved, but for single-module scenarios or highly -custom scenarios, this might be appropriate. - - -[WASI]: https://github.com/WebAssembly/WASI/blob/main/README.md diff --git a/design/high-level/Goals.md b/design/high-level/Goals.md deleted file mode 100644 index 200c3c21..00000000 --- a/design/high-level/Goals.md +++ /dev/null @@ -1,55 +0,0 @@ -# Component Model High-Level Goals - -(For comparison, see WebAssembly's [original High-Level Goals].) - -1. Define a portable, load- and run-time-efficient binary format for - separately-compiled components built from WebAssembly core modules that - enable portable, cross-language composition. -2. Support the definition of portable, virtualizable, statically-analyzable, - capability-safe, language-agnostic interfaces, especially those being - defined by [WASI]. -3. Maintain and enhance WebAssembly's unique value proposition: - * *Language neutrality*: avoid biasing the component model toward just one - language or family of languages. - * *Embeddability*: design components to be embedded in a diverse set of - host execution environments, including browsers, servers, intermediaries, - small devices and data-intensive systems. - * *Optimizability*: maximize the static information available to - Ahead-of-Time compilers to minimize the cost of instantiation and - startup. - * *Formal semantics*: define the component model within the same semantic - framework as core wasm. - * *Web platform integration*: ensure components can be natively supported - in browsers by extending the existing WebAssembly integration points: the - [JS API], [Web API] and [ESM-integration]. Before native support is - implemented, ensure components can be polyfilled in browsers via - Ahead-of-Time compilation to currently-supported browser functionality. -4. Define the component model *incrementally*: starting from a set of - [initial use cases] and expanding the set of use cases over time, - prioritized by feedback and experience. - -## Non-goals - -1. Don't attempt to solve 100% of WebAssembly embedding scenarios. - * Some scenarios will require features in conflict with the above-mentioned goal. - * With the layered approach to specification, unsupported embedding - scenarios can be solved via alternative layered specifications or by - directly embedding the existing WebAssembly core specification. -2. Don't attempt to solve problems that are better solved by some combination - of the toolchain, the platform or higher layer specifications, including: - * package management and version control; - * deployment and live upgrade / dynamic reconfiguration; - * persistence and storage; and - * distributed computing and partial failure. -2. Don't specify a set of "component services". - * Specifying services that may be implemented by a host and exposed to - components is the domain of WASI and out of scope of the component model. - * See also the [WASI FAQ entry](FAQ.md#how-does-wasi-relate-to-the-component-model). - - -[original High-Level Goals]: https://github.com/WebAssembly/design/blob/main/HighLevelGoals.md -[WASI]: https://github.com/WebAssembly/WASI/blob/main/README.md -[JS API]: https://webassembly.github.io/spec/js-api/index.html -[Web API]: https://webassembly.github.io/spec/web-api/index.html -[ESM-integration]: https://github.com/WebAssembly/esm-integration/tree/main/proposals/esm-integration -[initial use cases]: UseCases.md#Initial-MVP diff --git a/design/high-level/README.md b/design/high-level/README.md deleted file mode 100644 index 5abbd287..00000000 --- a/design/high-level/README.md +++ /dev/null @@ -1,5 +0,0 @@ -# Component Model High-Level Design Documents - -This directory contains design documents describing the component model's -[goals](Goals.md), [use cases](UseCases.md), [design choices](Choices.md) -and [FAQ](FAQ.md). diff --git a/design/high-level/UseCases.md b/design/high-level/UseCases.md deleted file mode 100644 index 608e6d06..00000000 --- a/design/high-level/UseCases.md +++ /dev/null @@ -1,342 +0,0 @@ -# Component Model Use Cases - -## Initial (MVP) - -This section describes a collection of use cases that characterize active and -developing embeddings of wasm and the limitations of the core wasm -specification that they run into outside of a browser context. The use cases -have a high degree of overlap in their required features and help to define the -scope of an "MVP" (Minimum Viable Product) for the Component Model. - -### Hosts embedding components - -One way that components are to be used is by being directly instantiated and -executed by a host (an application, system or service embedding a wasm -runtime), using the component model to provide a common format and toolchain so -that each distinct host doesn't have to define its own custom conventions and -sets of tools for solving the same problems. - -#### Value propositions to hosts for embedding components - -First, it's useful to enumerate some use cases for why the host wants to run -wasm in the first place (instead of using an alternative virtualization or -sandboxing technology): - -1. A native language runtime (like node.js or CPython) uses components as a - portable, sandboxed alternative to the runtime's native plugins, avoiding the - portability and security problems of native plugins. -2. A serverless platform wishing to move code closer to data or clients uses - wasm components in place of a fixed scripting language, leveraging wasm's - strong sandboxing and language neutrality. -3. A serverless platform wishing to spin up fresh execution contexts at high - volume with low latency uses wasm components due to their low overhead and fast - instantiation. -4. A system or service adds support for efficient, multi-language "scripting" - with only a modest amount of engineering effort by embedding an existing - component runtime, reusing existing WASI standards support where applicable. -5. A large application decouples the updating of modular pieces of the - application from the updating of the natively-installed base application, - by distributing and running the modular pieces as wasm components. -6. A monolithic application sandboxes an unsafe library by compiling it into a - wasm component and then AOT-compiling the wasm component into native code - linked into the monolithic application (e.g., [RLBox]). -7. A large application practices [Principle of Least Authority] and/or - [Modular Programming] by decomposing the application into wasm components, - leveraging the lightweight sandboxing model of wasm to avoid the overhead of - traditional process-based decomposition. - -#### Invoking component exports from the host - -Once a host chooses to embed wasm (for one of the preceding reasons), the first -design choice is how host executes the wasm code. The core wasm [start function] -is sometimes used for this purpose, however the lack of parameters or results -miss out on several use cases listed below, which suggest the use of exported -wasm functions with typed signatures instead. However, there are a number of -use cases that go beyond the ability of core wasm: - -1. A JS developer `import`s a component (via [ESM-integration]) and calls the - component's exports as JS functions, passing high-level JS values like strings, - objects and arrays which are automatically coerced according to the high-level, - typed interface of the invoked component. -2. A generic wasm runtime CLI allows the user to invoke the exports of a - component directly from the command-line, automatically parsing argv and env - vars according to the high-level, typed interface of the invoked component. -3. A generic wasm runtime HTTP server maps HTTP endpoints onto the exports of a - component, automatically parsing request params, headers and body and - generating response headers and body according to the high-level, typed - interface of the invoked component. -4. A host implements a wasm execution platform by invoking wasm component - exports in response to domain-specific events (e.g., on new request, on new - chunk of data available for processing, on trigger firing) through a fixed - interface that is either standardized (e.g., via WASI) or specific to the host. - -The first three use cases demonstrate a more general use case of generically -reflecting typed component exports in terms of host-native concepts. - -#### Exposing host functionality to components as imports - -Once wasm has been invoked by the host, the next design choice is how to expose -the host's native functionality and resources to the wasm code while it executes. -Imports are the natural choice and already used for this purpose, but there are -a number of use cases that go beyond what can be expressed with core wasm -imports: - -1. A host defines imports in terms of explicit high-level value types (e.g., - numbers, strings, lists, records and variants) that can be automatically - bound to the calling component's source-language values. -2. A host returns non-value, non-copied resources (like files, storage - connections and requests/responses) to components via unforgeable handles - (analogous to Unix file descriptors). -3. A host exposes non-blocking and/or streaming I/O to components through - language-neutral interfaces that can be bound to different components' - source languages' concurrency features (such as promises, futures, - async/await and coroutines). -4. A host passes configuration (e.g., values from config files and secrets) to - a component through imports of typed high-level values and handles. -5. A component declares that a particular import is "optional", allowing that - component to execute on hosts with or without the imported functionality. -6. A developer instantiates a component with native host imports in production - and with mock or emulated imports in local development and testing. - -#### Host-determined component lifecycles and associativity - -Another design choice when a host embeds wasm is when to create new instances, -when to route events to existing instances, when existing instances are -destroyed, and how, if there are multiple live instances, do they interact with -each other, if at all. Some use cases include: - -1. A host creates many ephemeral, concurrent component instances, each of which - is tied to a particular host-domain-specific entity's lifecycle (e.g. a - request-response pair, connection, session, job, client or tenant), with a - component instance being destroyed when the associated entity's - domain-specified lifecycle completes. -2. A host delivers fine-grained events, for which component instantiation would - have too much overhead if performed per-event or for which retained mutable - state is desired, by making multiple export calls on the same component - instance over time. Export calls can be asynchronous, allowing multiple - fine-grained events to be processed concurrently. For example, multiple - packets could be delivered as multiple export calls to the component instance - for a connection. -3. A host represents associations between longer- and shorter-lived - host-domain-specific entities (e.g., a "connection's session" or a "session's - user") by having the shorter-lived component instances (e.g., "connections") - import the exports of the longer-lived component instances (e.g., "sessions"). - -### Component composition - -The other way components are to be used (other than via direct execution by the -host) is by other components, through component composition. - -#### Value propositions to developers for composing components - -Enumerating some of the reasons why we might want to compose components in the -first place (instead of simply using the module/package mechanisms built into -the programming language): - -1. A component developer reuses code already written in another language - instead of having to reimplement the functionality from scratch. -2. A component developer writing code in a high-level scripting language (e.g., - JS or Python) reuses high-performance code written in a lower-level language - (e.g., C++ or Rust). -3. A component developer mitigates the impact of supply-chain attacks by - putting their dependencies into several components and controlling the - capabilities delegated to each, taking advantage of the strong sandboxing model - of components. -4. A component runtime implements built-in host functionality as wasm - components to reduce the [Trusted Computing Base]. -5. An application developer applies the Unix philosophy without incurring the - full cost and OS-dependency of splitting their program into multiple processes - by instead having each component do one thing well and using the component - model to compose their program as a hierarchy of components. -6. An application developer composes multiple independently-developed - components that import and export the same interface (e.g., a HTTP - request-handling interface) by linking them together, exports-to-imports, being - able to create recursive, branching DAGs of linked components not otherwise - expressible with classic Unix-style pipelines. - -In all the above use cases, the developer has an additional goal of keeping the -component reuse as a private, fully-encapsulated implementation detail that -their client doesn't need to be aware of (either directly in code, or -indirectly in the developer workflow). - -#### Composition primitives - -Core wasm already provides the fundamental composition primitives of: imports, -exports and functions, allowing a module to export a function that is imported -by another module. Building from this starting point, there are a number of -use cases that require additional features: - -1. Developers importing or exporting functions use high-level value types in - their function signatures that include strings, lists, records, variants and - arbitrarily-nested combinations of these. Both developers (the caller and - callee) get to use the idiomatic values of their respective languages. - Values are passed by copy so that there is no shared mutation, ownership or - management of these values before or after the call that either developer - needs to worry about. -2. Developers importing or exporting functions use opaque typed handles in - their function signatures to pass resources that cannot or should not be copied - at the callsite. Both developers (the caller and callee) use their respective - languages' abstract data type support for interacting with resources. Handles - can encapsulate `i32` pointers to linear memory allocations that need to be - safely freed when the last handle goes away. -3. Developers import or export functions with signatures containing - concurrency-oriented types (e.g., async, future and stream) to address - concurrency use cases like non-blocking I/O, early return and streaming. Both - developers (the caller and callee) are able to use their respective languages' - native concurrency support, if it exists, using the concurrency-oriented types - to establish a deterministic communication protocol that defines how the - cross-language composition behaves. -4. A component developer makes a minor [semver] update which changes the - component's type in a logically backwards-compatible manner (e.g., adding a new - case to a variant parameter type). The component model ensures that the new - component stays valid (at link-time and run-time) for use by existing clients - compiled against the older signature. -5. A component developer uses their language, toolchain and memory - representation of choice (including, in the future, [GC memory]), with these - implementation choices fully encapsulated by the component and thus hidden from - the client. The component developer can switch languages, toolchains or memory - representations in the future without breaking existing clients. - -The above use cases roughly correspond to the use cases of an [RPC] framework, -which have similar goals of crossing language boundaries. The major difference -is the dropping of the distributed computing goals (see [non-goals](Goals.md#non-goals)) -and the additional performance goals mentioned [below](#performance). - -#### Component dependencies - -When a client component imports another component as a dependency, there are a -number of use cases for how the dependency's instance is configured and shared -or not shared with other clients of the same dependency. These use cases -require a greater degree of programmer control than allowed by most languages' -native module systems and most native code linking systems while not requiring -fully dynamic linking (e.g., as provided by the [JS API]). - -1. A component developer exposes their component's configuration to clients as - imports that are supplied when the component is instantiated by the client. -2. A component developer configures a dependency independently of any other - clients of the same dependency by creating a fresh private instance of the - dependency and supplying the desired configuration values at instantiation. -3. A component developer imports a dependency as an already-created instance, - giving the component's clients the responsibility to configure the - dependency and the freedom to share it with others. -4. A component developer creates a fresh private instance of a dependency to - isolate the dependency's mutable instance state in order to minimize the - damage that can be caused in the event of a supply chain attack or - exploitable bug in the dependency. -5. A component developer imports an already-created instance of a dependency, - allowing the dependency to use mutable instance state to deduplicate data or - cache common results, optimizing overall app performance. -6. A component developer imports a WASI interface and does not explicitly pass - the WASI interface to a privately-created dependency. The developer knows, - without manually auditing the code of the dependency, that the dependency - cannot access the WASI interface. -7. A component developer creates a private dependency instance, supplying it a - virtualized implementation of a WASI interface. The developer knows, without - manually auditing the code of the dependency, that the dependency exclusively - uses the virtualized implementation. -8. A component developer creates a fresh private instance of a dependency, - supplying the component's own functions as imports to the dependency. The - component does this to parameterize the dependency's behavior with the - component's own logic or implementation choices (achieving the goals usually - accomplished using callback registration or [dependency injection]). - -### Performance - -In pursuit of the above functional use cases, it's important that the component -model not sacrifice the performance properties that motivate the use of wasm in -the first place. Thus, the new features mentioned above should be consistent -with the predictable performance model established by core wasm by supporting -the following use cases: - -1. A component runtime implements cross-component calls with efficient, direct - control flow transfer without thread context switching or synchronization. -2. A component runtime implements component instances without needing to give - each instance its own event loop, green thread or message queue. -3. A component runtime or optimizing AOT compiler compiles all import and - export names into indices or more direct forms of reference (up to and - including direct inlining of cross-component definitions into uses). -4. A component runtime implements value passing between component instances - without ever creating an intermediate O(n) copy of aggregate data types, - outside of either component instance's explicitly-allocated linear memory. -5. A component runtime shares the compiled machine code of a component across - many instances of that component. -6. A component is composed of several core wasm modules that operate on a - single shared linear memory, some of which contain langauge runtime code - that is shared by all components produced from the same language toolchain. - A component runtime shares the compiled machine code of the shared language - runtime module. -7. A component runtime implements the component model and achieves expected - performance without using any runtime code generation or Just-in-Time - compilation. - -## Post-MVP - -The following are a list of use cases that make sense to support eventually, -but not necessarily in the initial release. - -### Runtime dynamic linking - -* A component lazily creates an instance of its dependency on the first call - to its exports. -* A component dynamically instantiates, calls, then destroys its dependency, - avoiding persistent resource usage by the dependency if the dependency is used - infrequently and/or preventing the dependency from accumulating state across - calls which could create supply chain attack risk. -* A component creates a fresh internal instance every time one of its exports - is called, avoiding any residual state between export calls and aligning with - the usual assumptions of C programs with a `main()`. - -### Parallelism - -* A component creates a new (green) thread to execute an export call to a - dependency, achieving task parallelism while avoiding low-level data races due - to the absence of shared mutable state between the component and the - dependency. -* Two component instances connected via stream execute in separate (green) - threads, achieving pipeline parallelism while preserving determinism due to the - absence of shared mutable state. - -### Copy Minimization - -* A component produces or consumes the high-level abstract value types using - its own arbitrary linear memory representation or procedural interface (like - iterator or generator) without having to make an intermediate copy in linear - memory or copy unwanted elements. -* A component is given a "blob" resource representing an immutable array of - bytes living outside any linear memory that can be semantically copied into - linear memory in a way that, if supported by the host, can be implemented via - copy-on-write memory-mapping. -* A component creates a stream directly from a data segment, avoiding the cost - of first copying the data segment into linear memory and then streaming from - linear memory. - -### Component-level multi-threading - -In the absence of these features, a component can assume its exports are -called in a single-threaded manner (just like core wasm). If and when core wasm -gets a primitive [`fork`] instruction, a component may, as a private -implementation detail, have its internal `shared` memory accessed by multiple -component-internal threads. However, these `fork`ed threads would not be able -to call imports, which could break other components' single-threaded assumptions. - -* A component explicitly annotates a function export with [`shared`], - opting in to it being called simultaneously from multiple threads. -* A component explicitly annotates a function import with `shared`, requiring - the imported function to have been explicitly `shared` and thus callable from - any `fork`ed thread. - - - -[RLBox]: https://plsyssec.github.io/rlbox_sandboxing_api/sphinx/ -[Principle of Least Authority]: https://en.wikipedia.org/wiki/Principle_of_least_privilege -[Modular Programming]: https://en.wikipedia.org/wiki/Modular_programming -[start function]: https://webassembly.github.io/spec/core/intro/overview.html#semantic-phases -[ESM-integration]: https://github.com/WebAssembly/esm-integration/tree/main/proposals/esm-integration -[Trusted Computing Base]: https://en.wikipedia.org/wiki/Trusted_computing_base -[semver]: https://en.wikipedia.org/wiki/Software_versioning -[RPC]: https://en.wikipedia.org/wiki/Remote_procedure_call -[GC memory]: https://github.com/WebAssembly/gc/blob/master/proposals/gc/Overview.md -[JS API]: https://webassembly.github.io/spec/js-api/index.html -[dependency injection]: https://en.wikipedia.org/wiki/Dependency_injection -[`fork`]: https://dl.acm.org/doi/pdf/10.1145/3360559 -[`shared`]: https://dl.acm.org/doi/pdf/10.1145/3360559 diff --git a/design/proposals/README.md b/design/proposals/README.md deleted file mode 100644 index 36725210..00000000 --- a/design/proposals/README.md +++ /dev/null @@ -1,5 +0,0 @@ -This subdirectory will contain the explainers specific to each proposal, -starting initially with [module-linking] and [interface-types]. - -[module-linking]: https://github.com/webassembly/module-linking/ -[interface-types]: https://github.com/webassembly/interface-types/ diff --git a/design/proposals/module-linking/Binary.md b/design/proposals/module-linking/Binary.md deleted file mode 100644 index a450b14f..00000000 --- a/design/proposals/module-linking/Binary.md +++ /dev/null @@ -1,168 +0,0 @@ -# Module Linking Binary Format - -This document presents the binary format of the adapter modules in the -[attribute grammar] style of the Core WebAssembly [text format]. Additionally, -key validation rules are roughly sketched out. For explanations of what the -different AST productions mean, consult the respective sections in the -[explainer](Explainer.md). The overall plan for the binary format is -described in the explainer's [Binary Format Considerations section](Explainer.md#binary-format-considerations). - - -## Module Definitions - -(See [module definitions](Explainer.md#module-definitions) in the explainer.) -``` -magic ::= 0x00 0x61 0x73 0x6D -adapter-version ::= 0x0a 0x00 0x01 0x00 -adapter-preamble ::= -adapter-module ::= s*:
* => (adapter module flatten(s*)) -section ::= t*:section_1(vec()) => t* - | i*:section_2(vec()) => i* - | m*:section_3(vec()) => m* - | i*:section_4(vec()) => i* - | a*:section_5(vec()) => a* - | e*:section_6(vec()) => e* -module ::= size:u32 m: => m (if size = ||m||) - | size:u32 m: => m (if size = ||m||) -``` -Notes: -* The first `u16` of `adapter-version` is the pre-release version, `0xa`. The - idea is that, before final standardization, this pre-release version will be - bumped to coordinate spec changes in the prototypes. When the standard is - finalized, the version will be changed one last time to `0x1`. This mirrors - what happened during the path to Core WebAssembly 1.0. -* The second `u16` of `adapter-version` is the "module kind" which is `0x1` for - adapter modules and `0x0` for core modules. -* The `section_X`'s refer to Core WebAssembly's [`section`] parameterized rule. - The `X` numbers (and all other magic constants in the adapter module binary - format) do not attempt to be distinct from or align with the core module - binary format since, over time, this distinction/alignment will be lost as - both formats may grow independently. -* `core:module` refers to Core WebAssembly's [`module`] rule. - -One general note with respect to the binary format and validation is that each -definition is validated in an environment defined containing only the preceding -definitions. Thus, the index spaces are built and validated incrementally as -each definition of the module is decoded and validated. For validation -purposes, the `section` boundaries are not significant; all that matters is the -individual definitions (`type`, `import`, `export`, `module`, `instance` and -`alias`) contained within the sections. - - -## Instance Definitions - -(See [instance definitions](Explainer.md#instance-definitions) in the explainer.) -``` -instance ::= ie: => (instance ie) -instance-expr ::= 0x00 m: nd*:vec() => (instantiate m (import nd)*) - | 0x01 nd*:vec() => (export nd)* -named-def ::= nm: dr: => nm dr -def-ref ::= 0x00 x: => (instance x) - | 0x01 x: => (module x) - | 0x02 x: => (func x) - | 0x03 x: => (table x) - | 0x04 x: => (memory x) - | 0x05 x: => (global x) -``` -Notes: -* The indices in the `def-ref`s are validated according to the respective index - space. As mentioned above, index spaces are built incrementally as each - definition is validated. -* The `import` arguments supplied by `instantiate` are validated against the - module `m` according to [module subtyping](Subtyping.md#instantiation) rules. -* The `def-ref` codes are chosen to keep the shared-nothing kinds contiguous - (with room for future additions by Interface Types) and separate from the - shared-everything core module kinds. -* `name` refers to the Core WebAssembly's [`name`] rule. - - -## Import Definitions - -(See [import definitions](Explainer.md#import-definitions) in the explainer.) -``` -import ::= nm: dt: => (import nm dt) -deftype ::= 0x00 i: => type-index-space[i] (must be (instance) type) - | 0x01 i: => type-index-space[i] (must be (module) type) - | 0x02 i: => type-index-space[i] (must be (func) type) - | 0x03 tt: => tt - | 0x04 mt: => mt - | 0x05 gt: => gt -``` -Notes: -* Unlike the text format, which allows module/instance/function types to be - written "inline", the binary format requires these compound types be defined - separately as a type definition, referred to be type index. -* The `nm` are validated to be unique; duplicate import names are not allowed - in adapter modules. - - -## Export Definitions - -(See [export definitions](Explainer.md#export-definitions) in the explainer.) -``` -export ::= nm: dr: => (export nm dr) -``` -Notes: -* As with import definitions, the `nm` are validated to be unique. -* As with instance definitions, the indices of `dt` are validated to be - be valid in the associated index space at the point of the export. - - -## Alias Definitions - -(See [alias definitions](Explainer.md#alias-definitions) in the explainer.) -``` -alias ::= 0x00 i: nm: 0x00 => (alias i nm (instance)) - | 0x00 i: nm: 0x01 => (alias i nm (module)) - | 0x00 i: nm: 0x02 => (alias i nm (func)) - | 0x00 i: nm: 0x03 => (alias i nm (table)) - | 0x00 i: nm: 0x04 => (alias i nm (memory)) - | 0x00 i: nm: 0x05 => (alias i nm (global)) - | 0x01 ct: i: 0x01 => (alias outer ct i (module)) - | 0x01 ct: i: 0x06 => (alias outer ct i (type)) -``` -Notes: -* For instance-export aliases, `i` is validated to refer to an instance in the - instance index space that actually exports `nm` with the specified definition - kind. -* For outer aliases, `ct` is validated to be *less or equal than* the number - of enclosing modules and `i` is validated to be a valid index in the - specified definition's index space of the enclosing adapter module indicated - by `ct` (counting outward, starting with `0` referring to the current adapter - module). - - -## Type Definitions - -(See [type definitions](Explainer.md#type-definitions) in the explainer.) -``` -type ::= 0x7f it: => it - | 0x7e mt: => mt - | 0x7d ft: => ft -instancetype ::= itd*:vec() => (instance itd*) -instancetype-def ::= 0x01 t: => t - | 0x05 a: => a - | 0x06 nm: dt: => (export nm dt) -moduletype ::= mtd*:vec() => (module mtd*) -moduletype-def ::= itd: => itd - | 0x02 i: => i -``` -Notes: -* Instance and modules types create fresh type index spaces that are - populated and referenced by their contents. E.g., for a module type that - imports a function, the `import` `moduletype-def` must be preceded by - either a `type` or `alias` `moduletype-def` that adds the function type to - the type index space. -* Currently, the only allowed form of `alias` in instance and module types - is `(alias outer ct li (type))`. In the future, other kinds of aliases - will be needed and this restriction will be relaxed. -* The normal index space validation rules for adapter modules described above - ensure that module and instance type definitions are acyclic. - - - -[Attribute Grammar]: https://en.wikipedia.org/wiki/Attribute_grammar -[Text Format]: https://webassembly.github.io/spec/core/text/conventions.html -[`section`]: https://webassembly.github.io/spec/core/binary/modules.html#sections -[`module`]: https://webassembly.github.io/spec/core/binary/modules.html#binary-module -[`name`]: https://webassembly.github.io/spec/core/binary/values.html#binary-name diff --git a/design/proposals/module-linking/Example-LinkTimeVirtualization.md b/design/proposals/module-linking/Example-LinkTimeVirtualization.md deleted file mode 100644 index ee823f34..00000000 --- a/design/proposals/module-linking/Example-LinkTimeVirtualization.md +++ /dev/null @@ -1,93 +0,0 @@ -# Link-Time Virtualization Example - -This document walks through the -[Link-time Virtualization](Explainer.md#link-time-virtualization) -use case. - -We start with a child module that has been written and compiled separately, -without regard to the parent module. It imports `wasi:filesystem` to do file I/O: -```wasm -(module $Child - (import "wasi:filesystem" "read" (func (param i32 i32 i32) (result i32))) - (import "wasi:filesystem" "write" (func (param i32 i32 i32) (result i32))) - (func $play (export "play") - ... - ) -) -``` - -We want to write a parent module that reuses the child module, but we don't -want to give it real file operations, but rather some virtual filesystem. -This virtual filesystem can be factored out and reused as a separate module -that imports the "real" `wasi:filesystem` and exports a virtualized -implementation of all the `wasi:filesystem` operations: -```wasm -(module $VirtualFS - (import "wasi:filesystem" "read" (func (param i32 i32 i32) (result i32))) - (import "wasi:filesystem" "write" (func (param i32 i32 i32) (result i32))) - - (func (export "read") (param i32 i32 i32) (result i32) - ... - ) - (func (export "write") (param i32 i32 i32) (result i32) - ... - ) -) -``` - -We can now write the parent module as an adapter module that composes `$Child` -and `$VirtualFS`: -```wasm -(adapter module $Parent - (type $FSInstance (instance - (export "read" (func (param i32 i32 i32) (result i32))) - (export "write" (func (param i32 i32 i32) (result i32))) - )) - (import "wasi:filesystem" (instance $real-fs (type $FSInstance))) - - (import "./virtualize.wasm" (module $VirtualFS - (import "wasi:filesystem" (instance (type $FSInstance))) - (export (type $FSInstance)) - )) - (import "./child.wasm" (module $Child - (import "wasi:filesystem" (instance (type $FSInstance))) - (export "play" (func)) - )) - - (instance $virt-fs (instantiate $VirtualFS (import "wasi:filesystem" (instance $real-fs)))) - (instance $child (instantiate $Child (import "wasi:filesystem" (instance $virt-fs)))) -) -``` -This example demonstrates several features of the Module Linking proposal: -* The first line of the module is a [type definition](Explainer.md#type-definitions), - factoring out an instance type so it can be reused four times below. -* The next line is an [import definition](Explainer.md#import-definitions), - importing an instance of `wasi:filesystem`. This instance import is logically - equivalent to two two-level imports in a core module with `wasi:filesystem` as the - "module" name and `read`/`write` as the "field" name. -* The following two imports import *modules*, which is the other new importable - type (after instances). -* The final two lines are [instance definitions](Explainer.md#instance-definitions), - instantiating and wiring up the `VirtualizeFS` and `Child` modules. - -Here, we assume that the host understands relative file paths. To remove this host -assumption, a tool could replace the imports definitions in `$Parent` with -[module definitions](Explainer.md#module-definitions): -```wasm -(adapter module $Parent - (type $FSInstance ... same as above) - (import "wasi:filesystem" ... same as above) - - (module $VirtualizeFS ... copied inline) - (module $Child ... copied inline) - - (instance $virt-fs ... same as above) - (instance $child ... same as above) -) -``` - -In general, a tool can trivially go between nested modules and module imports -without any understanding of their contents which allows bundling tools to -optimize for the deployment target. For example, on the Web, the choice to -import vs. nest modules can be based on the usual bundling considerations of -caching, reuse and minimizing fetches. diff --git a/design/proposals/module-linking/Explainer.md b/design/proposals/module-linking/Explainer.md deleted file mode 100644 index be4e8a72..00000000 --- a/design/proposals/module-linking/Explainer.md +++ /dev/null @@ -1,948 +0,0 @@ -# Module Linking Explainer - -This explainer introduces the Module Linking proposal, as the first proposal -of the [Component Model] specification. Module Linking enables multiple Core -WebAssembly modules to be linked together without relying on imported host -functionality. - -1. [Problem](#problem) -2. [Use Cases](#use-cases) -3. [Additional Requirements](#additional-requirements) -4. [Walkthrough](#walkthrough) - 1. [Module Definitions](#module-definitions) - 2. [Instance Definitions](#instance-definitions) - 3. [Import Definitions](#import-definitions) - 4. [Export Definitions](#export-definitions) - 5. [Alias Definitions](#alias-definitions) - 6. [Type Definitions](#type-definitions) -5. [Binary Format Considerations](#binary-format-considerations) -6. [Web Platform Integration](#web-platform-integration) - - -## Problem - -Currently, WebAssembly modules have no way to define how they are to be -instantiated and linked together without relying on host-specific functionality -such as the [JS API]. Consequently, the only portable way to link modules today -is to [statically link] them using toolchain-specific conventions. This leads -to code duplication in production and inhibits cross-language reuse. A number -of [Component Model use cases] require support for more dynamic forms of -linking that enable the sharing of separately-compiled modules written in -different languages. - - -## Use Cases - -To motivate the proposed solution, we consider 2 use cases whose requirements -aren't satisfied by simpler solutions. - - -### Link-time Virtualization - -When using a first-class instantiation API like the JS API's -[`WebAssembly.instantiate()`], the imports of the module-to-be-instantiated -appear as explicit arguments supplied by the caller. This has several useful -properties that should be preserved by a pure-wasm linking solution: - -First, it enables applications to easily enforce the [Principle of Least Authority], -passing modules only the imports necessary to do their job. There are currently -[cases][Figma plugins] of Web applications relying on this property to sandbox -untrusted plugins. - -Second, it enables client modules to fully or partially [virtualize] the imports -of their dependencies without extraordinary challenge or performance overhead. -For example, if a module imports a set of file operations and a client wants to -reuse this module on a system without builtin file I/O, the client should be -able to virtualize the file operations with an in-memory implementation. -Virtualization also enhances the ability of developers to apply the Principle of -Least Authority, by allowing a client module to not only pass *subsets* of -capabilities, but to also dynamically [attenuate] capabilities. Lastly, -virtualization allows developers to locally test modules intended for later -deployment by [mocking] deployment APIs with local implementations. In general, -if virtualization is well-supported and efficient, software reusability and -composability are increased. - -While it is possible to perform virtualization at run-time, e.g., passing -function references for all virtualizable operations, this approach would be -problematic as a basis for a highly-virtualizable ecosystem since it would -require modules to intentionally opt into virtualization by choosing to receive -first-class function references instead of using function imports. In the limit, -to provide maximum flexibility to client code, toolchains would need to avoid -*all* use of imports, effectively annulling a core part of wasm. Because of -their more-static nature, imports are inherently more efficient and optimizable -than first-class function references, so this would also have a negative -performance impact. - -Thus, to avoid the problems of run-time virtualization, a wasm linking solution -should enable **link-time virtualization** such that a parent module can -specify all the imports of its dependencies (without any explicit opt-in on the -part of those dependencies), just as with the JS API's [`instantiate`]. Note -that it's possible to achieve run-time virtualization by supplying link-time -function imports that perform dynamic dispatch on their parameters. Link-time -virtualization is thus a fairly general mechanism to enable multiple styles of -virtualization. - -As an example, given the static dependency graph on the left (where all 3 -modules import a host-supplied instance of `wasi:filesystem`), it should be -possible for `parent.wasm` to generate the linked instance graph on the right, -where the `parent` instance has created a `virtualized` instance and supplied -it to a new `child` instance as an implementation of the `wasi:filesystem` -interface: - -

- -Importantly, the `child` instance has no access to the `wasi:filesystem` -instance imported by the `parent` instance. - -A worked example of this use case is given [here](Example-LinkTimeVirtualization.md). - - -### Shared-Everything C-family Dynamic Linking - -"Dynamic Linking" refers to keeping modules separate until load-time so that -common modules can be shared by multiple independent clients. This avoids the -need to [statically link] (thereby duplicating) the shared modules into each -client. "Shared-Everything" linking refers to the case where the linked modules -share memory and tables, effectively emulating [native dynamic linking]. -Lastly, "C-family" refers to the family of languages that can interoperate -through a traditional C ABI (e.g., C, C++, FORTRAN and Rust). - -Two modules are dynamically linked by having one module import the functions, -memories, tables and globals exported by another module. One challenge for -dynamic linking is controlling which module instances share a linear memory and -which have separate linear memories. In the [shared-nothing] context of the -Component Model, we want all the core modules used by a single component to -share a single linear memory while we want each distinct component instance to -get a distinct linear memory. - -For example, it should be possible to take the static dependency graph of the -application on the left, which is built from two components (`zipper` and -`imgmgk`) and three shared core modules (`libc`, `libzip` and `libimg`), and -create the dynamically-linked instance graph on the right at load-time: - -

- -Here, `libc` defines and exports a linear memory that is imported by the other -core instances contained within the same component instance. The whole -application uses the `libc` module three times, sharing *code*, but with each -usage getting a distinct instance and thus not sharing *data*. Module systems -where sharing a module forces sharing a module instance are common in existing -programming languages but break shared-nothing isolation and this use case. - -A worked example of this use case is given [here](Example-SharedEverythingDynamicLinking.md). - - -## Additional Requirements - -Additionally, the following high-level Component Model [design choices] are -relevant: - -* **No GC dependency**: Since we wish to use this feature to implement dynamic - linking of C/C++/Rust programs, and since C/C++/Rust programs aim to run on - hosts that don't contain a GC, this proposal should not require a general - garbage collection algorithm to implement. - -* **No JIT dependency**: Today, using static linking of libraries, wasm - hosts are able to use a simple, Ahead-of-Time compilation model to generate - high-performance machine code images that can be immediately instantiated and - run. Switching to dynamic linking should not hurt hosts' ability to perform - the same degree of optimization. - -* **No global registries at runtime**: A number of existing dependency - resolution mechanisms with similar use cases as Module Linking depend on a - shared mutable registry into which, at runtime, modules are registered and - names are resolved. - - -## Walkthrough - -This proposal bootstraps the Component Model by defining a new "adapter module" -concept. Adapter modules *contain* Core WebAssembly ("core") modules as well as -several new definition kinds that address the use cases listed above. Just like -core modules, adapter modules have abstract syntax with both text- and -binary-format representations. Similarly, adapter modules are meant to be -distributable binaries that can be directly loaded and executed by a supporting -runtime. - -(As a spoiler: adapter modules are extended by the [Interface Types] proposal -with the additional features necessary to achieve the [shared-nothing] goals of -the Component Model. The Interface Types proposal also defines a *restricted* -form of adapter modules called **components** which are adapter modules whose -public interfaces (imports and exports) *only* use interface types, thereby -ensuring shared-nothing isolation of their contained shared mutable state. -Ultimately, both definitions—adapter modules and components—are -necessary for different scenarios.) - -This walkthrough section introduces adapter modules via their text format. The -[next section](#binary-format-considerations) discusses the high-level -considerations for the binary format of adapter modules while a -[sibling document](Binary.md) provides a detailed binary format description. - - -### Module Definitions - -Like core modules, adapter modules are composed of sequences of definitions. -This proposal includes 6 definition kinds: -``` -adapter-module ::= (adapter module ? * ) -definition ::= - | - | - | - | - | -module ::= - | -``` -From this grammar fragment we can see that the `adapter-module` production is -recursive and thus adapter modules can contain other adapter modules. The -`core:module` production refers to the Core WebAssembly's [`module`] -parse rule. Together, this means that adapter modules can form trees with core -modules appearing only at leaves. - -For example, the following adapter module contains one adapter module and two -core modules: -```wasm -(adapter module - (adapter module $A - (module $B - (func (export "one") (result i32) (i32.const 1)) - ) - ) - (module $C - (func (export "two") (result i32) (i32.const 2)) - ) -) -``` -Just like other definitions, adapter and core module definitions go into an -[index space] called the *module index space* which can be referenced by other -definitions (in the text format, via symbolic identifiers like `$A`, `$B` and -`$C` above). Notably, adapter and core modules go into the *same* module index -space since the users of the module index space don't distinguish between -adapter and core modules; after definition, both kinds of modules simply have a -*module type* against which uses are checked (more on module types below). - -Unlike core modules, the definitions inside an adapter module are inherently -*ordered*: definitions can only reference preceding definitions so that adapter -module definitions are acyclic by nature. This acyclicy reflects the acyclic -nature of Core WebAssembly's [module instantiation], which adapter modules can -perform (as described below). - -Lastly, the syntax and semantics of core modules are not modified by adapter -modules; all interaction with core modules happens through imports and exports -and thus, from the Core WebAssembly's point of view, the Component Model is -just another [WebAssembly embedder][core concepts]. - - -### Instance Definitions - -Instance definitions are the central feature of the Module Linking proposal, -allowing adapter modules to create and link module instances. Whenever an -adapter module is instantiated, all of its contained instance definitions are -executed, creating new module instances according to the contained -`instance-expr` expressions. The syntax of instance definitions is: -``` -instance ::= (instance ? ) -instance-expr ::= (instantiate (import )*) - | (export )* -def-ref ::= (instance ) - | (module ) - | (func ) - | (table ) - | (memory ) - | (global ) -``` -As an example, the following `$Parent` adapter module creates a new `$Child` -module instance every time `$Parent` is instantiated: -```wasm -(adapter module $Parent - (module $Child - (memory 1) - ) - (instance $child (instantiate $Child)) - ... -) -``` -The fresh `$Child` instance is added to the *instance index space* which other -definitions (in the `...`) can refer to via the identifier `$child`. Without -the `instance` definition, no instance of `$Child` would be created. If there -were a second `instance` definition of `$Child`, two instances would be -created. Thus, this proposal Module Linking separates the concepts of *defining -a module* from *creating an instance* of a module. - -A more interesting example uses instance definitions to link two core modules -together: -```wasm -(adapter module - (module $A - (func (export "answer") (result i32) (i32.const 42)) - ) - (module $B - (func (import "the" "answer") (result i32)) - ) - (instance $a (instantiate $A)) - (instance $b (instantiate $B (import "the" (instance $a)))) -) -``` -Here, the two-level import names of core modules are resolved by using the -first name (`"the"`) as a named parameter supplied by `instantiate` and the -second name (`"answer"`) as the name of an export. - -The static validation rules for `instantiate` ensure that: -* every `name` imported by the instantiated module is supplied exactly once by - an `import` in the list; -* the indices in the `def-ref`s refer to a preceding definitions of matching - type. - -One reason to have explicit instance definitions is to allow code generators -and developers to construct arbitrary DAGs of module instances where individual -modules can be instantiated multiple times in the DAG. For example, the -following adapter module creates two instances of `$Libc` for two non-[PIC] -modules that would otherwise clobber each other if they shared a linear memory: -```wasm -(adapter module - (module $Libc - (memory (export "memory") 1) - (func (export "malloc") (param i32) (result i32) ...) - ) - - (module $A - (memory (import "libc" "memory") 1) - (func (import "libc" "malloc") (param i32) (result i32)) - (func (export "run") ...) - ) - (instance $libcA (instantiate $Libc)) - (instance $a (instantiate $A (import "libc" (instance $libcA)))) - - (module $B - (memory (import "libc" "memory") 1) - (func (import "libc" "malloc") (param i32) (result i32)) - (func (export "run") ...) - ) - (instance $libcB (instantiate $Libc)) - (instance $b (instantiate $B (import "libc" (instance $libcB)))) -) -``` -This adapter module contains 3 child modules but creates 4 module instances at -instantiation-time. This works because the import string `"libc"` in `$A` and -`$B` is not looked up in a global namespace; it's a named parameter supplied -directly by the outer adapter module. - -Lastly, `instance-expr` offers an alternative to `instantiate` for creating -instances: instances can be synthesized by "tupling" together existing -definitions. For example, the following adapter module creates an instance that -pairs together two existing instances: -```wasm -(adapter module - (module $Inner ...) - (instance $left (instantiate $Inner)) - (instance $right (instantiate $Inner)) - (instance $pair - (export "left" (instance $left)) - (export "right" (instance $right)) - ) -) -``` -Technically, this tupling instance definition is just shorthand for an -auxiliary adapter module that reexports all its imports. This shorthand will -become more evidently useful once other definitions are presented (below). - - -### Import Definitions - -Imports in adapter modules serve the same role as in core modules, but with an -expanded set of importable types that allow whole modules and instances to be -imported: -``` -import ::= (import ) -deftype ::= - | - | - | - | - | -instancetype ::= (instance ? (export )*) -moduletype ::= (module ? (import )* (export )*) -``` -The `core:`-prefixed productions refer to Core WebAssembly's [`functype`], -[`tabletype`], [`memtype`] and [`globaltype`] productions. - -Unlike core modules, adapter module imports do not allow duplicate names. -This is necessary to ensure that the named arguments passed by `instantiate` -unambiguously match a single import. - -Also unlike core modules, adapter module imports only have a single name -(whereas core imports have two names). The reason for this is that, with the -ability to import instances, the *exports* of an imported instance take on the -role of the second-level name. Thus, always requiring two names would force -extra, unnecessary names to be invented. - -As an example, the following adapter module instantiates its contained core -module with imported `libc` module, matching the second-level name `malloc` -against the declared exports of `libc`: -```wasm -(adapter module $M - (import "libc" (module $Libc - (export "malloc" (func (param i32) (result i32))) - )) - (module $Core - (func (import "libc" "malloc") (param i32) (result i32)) - ... - ) - (instance $libc (instantiate $Libc)) - (instance $core (instantiate $Core (import "libc" (instance $libc)))) -) -``` -Note that, by importing `libc` as a *module*, instead of as an *instance*, `$M` -is able to create a new instance of `libc` with a fresh, private linear memory. -This allows `$M` to share the *code* of `libc` with other adapter modules -without being forced to share linear memory (which could, e.g., lead to one -module's static global data clobbering another's). - -Adapter modules can also import whole instances, as a replacement for two-level -imports. For example: -```wasm -(adapter module $N - (import "wasi:filesystem" (instance $libc - (export "path_open" (func ... )) - (export "read" (func ...)) - )) - ... -) -``` -Here, `$N` imports an instance of the `wasi:filesystem` interface, which means -that *someone else* has already created the instance and `$N` cannot do so -itself. - -For the same reason that `instantiate` operates uniformly on modules, imports -do not distinguish between core modules and adapter modules; all that matters -is that the (core|adapter) module have the expected import and export types. -That being said, since adapter modules have a larger available set of -importable types (viz., module and instance types and, later, interface types), -certain signatures will only be implementable by adapter modules in practice. - -To deal with the two-level imports of core modules, the Component Model assigns -a module type using single-level imports of instances with the second-level -names as exports. For example, the following core module: -```wasm -(module - (import "one" "foo" (func)) - (import "two" "bar" (func)) - (import "one" "baz" (func)) - ... -) -``` -would be assigned the following module type: -```wasm -(module - (import "one" (instance - (export "foo" (func)) - (export "baz" (func)) - )) - (import "two" (instance - (export "bar" (func)) - )) -) -``` -Since module types do not allow duplicate import or export names, not all core -modules can be assigned a module type. Thus, adapter modules do not allow the -nesting or importing of core modules with duplicate imports. - -Module and instance types also support subtyping, so that superfluous imports -and exports can be ignored. For example, the following adapter module -validates, with the superfluous import `a` being ignored by `$N` and the -superfluous export `d` being ignored by `$M`. -```wasm -(adapter module - (adapter module $M - (import "i" (module - (import "a" (func)) - (import "b" (func)) - (export "c" (func)) - )) - ) - (adapter module $N - (import "b" (func)) - (func (export "c") ...) - (func (export "d") ...) - ) - (instance (instantiate $M (import "i" (module $N)))) -) -``` -Additionally, since imports and exports are matched by name, module and -instance subtyping ignores import/export declaration order. - - -### Export Definitions - -Exports in adapter modules serve the same role as in core modules, but with an -expanded set of exportable types that allow whole modules and instances to be -exported: -``` -export ::= (export ) -``` -(Note: `def-ref` is defined [above](#instance-definitions).) - -As an example, the following adapter module implements the WASI filesystem -interface, exporting the instance with the name `wasi:filesystem` to provide a -clear semantic connection between the implementation and the interface. -```wasm -(adapter module - (module $Core - (func (export "path_open") ...) - (func (export "read") ...) - ) - (instance $core (instantiate $Core)) - (export "wasi:filesystem" (instance $core)) -) -``` -To show an example of exporting individual functions, memories, tables, etc, -we first need the ability to extract these from core instances via Alias -Definitions. - - -### Alias Definitions - -Alias definitions inject other modules' definitions into the current module's -index spaces. Aliases can target either instance exports or the local -definitions of an outer adapter module: -``` -alias ::= (alias ) -alias-target ::= - | -alias-name ::= (instance ?) - | (module ?) - | (func ?) - | (type ?) - | (table ?) - | (memory ?) - | (global ?) -``` -As an example of an instance-export alias, the following adapter module -aliases the `f` export of `i` in order to pass it as the `foo` import of `M`: -```wasm -(adapter module - (import "M" (module $M - (import "foo" (func)) - )) - (import "i" (instance $i - (export "f" (func)) - (export "g" (func)) - )) - (alias $i "f" (func $f)) - (instance $m (instantiate $M (import "foo" (func $f)))) -) -``` -As an example of an outer alias, in the following adapter module, `$Inner` -aliases `$Outer`'s `$Libc` module, avoiding the need to manually import it: -```wasm -(adapter module $Outer - (module $Libc - ... - ) - (adapter module $Inner - (alias $Outer $Libc (module $InnerLibc)) - (instance (instantiate $InnerLibc)) - ... - ) -) -``` -Here, `$Outer` and `$Libc` serve as symbolic [de Bruijn indices], ultimately -resolving to a pair of integers: the number of enclosing adapter modules to -skip, and the index of the target definition. In particular, this number can be -0, in which case the outer alias refers to the current module, allowing a -single module to alias its own definitions at multiple indices in the index -space (which can be [useful to tools][Issue-30]). - -Adapter module definitions containing outer aliases effectively produce a -module [closure] at instantiation time, including a copy of the outer-aliased -definitions in the module value. Because of the prevalent assumption that -module values are stateless, outer aliases are restricted to only refer to -stateless module and type definitions. (In the future, outer aliases to all -kinds of definitions could be allowed by recording the "statefulness" of the -resulting bound module in the resulting bound module's type.) - -Additionally, to maintain the acyclicy of module instantiation, outer aliases -are only allowed to refer to preceding outer definitions. Otherwise, modules -could easily create incoherent (or coherent, but mind-bending) recursive -definitions which would complicate tools and implementations. - -With both instance and outer aliases, the alias definition inserts the target -definition into the index space of the `alias-name` (so, e.g., -`(alias $i "foo" (func $f))` inserts `foo` into the function index space, with -`$f` resolving to the new function index). The target definition kind is -validated to actually match the kind of the index space. After that, the -aliased definition can be used in all the same ways as a normal imported or -internal definition. - -For symmetry with [imports][func-import-abbrev], aliases can be written -in an inverted form that puts the definition kind first: -```wasm -(func $f (import "i" "f")) ≡ (import "i" "f" (func $f)) ;; (existing) -(func $g (alias $i "g1")) ≡ (alias $i "g1" (func $g)) ;; (new) -``` - -To reduce the syntactic burden in the text format, aliases come with syntactic -sugar for implicitly declaring aliases inline, in the same manner as the Core -WebAssembly's [`typeuse`] sugar. - -For instance-export aliases, the inline sugar has the form: -``` -(kind +) -``` -where the `+` is a sequence of exports projected from the ``. -For example, the following snippet using inline alias sugar: -```wasm -(instance $j (instantiate $J (import "f" (func $i "f")))) -(export "x" (func $j "g" "h")) -``` -is equivalent to the expanded explicit aliases: -```wasm -(alias $i "f" (func $f_alias)) -(instance $j (instantiate $J (import "f" (func $f_alias)))) -(alias $j "g" (instance $g_alias)) -(alias $g_alias "h" (func $h_alias)) -(export "x" (func $h_alias)) -``` - -For outer aliases, the inline sugar is simply the identifier of the outer -definition, resolved using normal lexical scoping rules. For example, the -following adapter module: -```wasm -(adapter module $M - (module $N ...) - (adapter module - (alias $M $N (module $N)) - (instance (instantiate $N)) - ) -) -``` -can be equivalently written: -```wasm -(adapter module - (module $N ...) - (adapter module - (instance (instantiate $N)) - ) -) -``` - -Using aliases, an adapter module can re-export individual functions: -```wasm -(adapter module - (module $Core1 - (func (export "foo") ...) - ) - (instance $core1 (instantiate $Core1)) - (module $Core2 - (func (export "bar") ...) - ) - (instance $core2 (instantiate $Core2)) - (export "a" (func $core1 "foo")) - (export "b" (func $core2 "bar")) -) -``` -This example uses the inline alias sugar to alias `foo` and `bar`, -exporting them with the names `a` and `b`, resp. - -Addititionally, aliases are useful in combination with instance -definitions for being able to synthesize instances from individual -definitions. For example: -```wasm -(adapter module - (import "x" (instance $x - (export "foo" (func)) - (export "bar" (func)) - )) - (instance $y - (export "a" (func $x "foo")) - (export "b" (func $x "bar")) - ) - ... -) -``` -Here, the imported instance `x` is transformed into a new instance `y` by -aliasing `x`'s exports and tupling them back together with new names. The new -instance `y` can then be passed to `instantiate` or `export`. In this way, -instances can be easily renamed and recombined via aliases. Due to the -declarativity of Module Linking, all this instance and name manipulation is -resolved at compile time and thus incurs no runtime penalty. - - -### Type Definitions - -Type definitions in adapter modules serve the same role as they do in core -modules, but with an expanded set of definable types that allow module and -instance types. Type definitions allow these compound types to be reused to -avoid duplication. -``` -type ::= (type $id? ) -``` -(Note: `deftype` is defined [above](#import-definitions).) - -For example, using both type and alias definitions, the type of `$Libc` -is deduplicated in the following adapter module: -```wasm -(adapter module - (type $LibcModule (module - (export "memory" (memory 1)) - (export "malloc" (func (param i32) (result i32))) - )) - (import "Libc" (module $Libc (type $LibcModule))) - (import "A" (module $A - (import "Libc" (module $Libc (type $LibcModule))) - ... - )) - (import "B" (module $B - (import "Libc" (module $Libc (type $LibcModule))) - ... - )) - ... -) -``` -Here, `(type ...)` is used to refer to a type definition, inheriting Core -WebAssembly's [`typeuse`] syntax. This adapter module is an example of the -kind of thing that a bundler might produce to link together modules `A` and `B` -sharing common `Libc` code. - -Frequently an adapter module will need to define both a module type and an -instance type that is the result of instantiating the module type. To avoid -duplicating the list of exports in both the module and instance types, a -bit of syntactic sugar is added, allowing an instance's exports to be injected -into a module by writing `(export $InstanceType)` (without a `` before -the `$InstanceType`). For example, this sugar could be used to share between -the `Libc` instance and module types: -```wasm -(adapter module - (type $LibcInstance (instance - (export "memory" (memory 1)) - (export "malloc" (func (param i32) (result i32))) - )) - (type $LibcModule (module - (export $LibcInstance) - )) - ... -) -``` -In this example, `$LibcInstance` is the type of already-created instances while -`$LibcModule` is the type of modules that can be instantiated to create -`$LibcInstance`-compatible instances. - - -## Binary Format Considerations - -The basic idea of the binary format for adapter modules is to replicate the -conventions of the core module binary format to the extent possible. At the -top-level, an adapter module has a [preamble][Module Binary] followed by a -sequence of [sections]. - -To distinguish core modules from adapter modules, the [`version`][Module -Binary] field is split into two `u16` fields: a `version` field and a `layer` -field, where core modules implicitly already have the `layer` set to 0 and -adapter modules would have the `layer` set to 1. Thus the `layer` field would -allow runtimes to load both kinds of modules through a single entry point -(e.g., the existing JS API or ESM-integration), unambiguously determining how -to interpret the bytes by looking at the premable. - -Like core modules, different definition kinds are encoded in different binary -section kinds (e.g., "modules" go into a "module section", "instances" go in -an "instance section", etc). - -Unlike core modules, adapter module sections can go in any order and there can -be multiple sections of a given kind (e.g., multiple module sections). The -reason for this is to align the binary format order with the definition order, -where any definition can refer back to any preceding definition, so that -acyclicy can be enforced by simply requiring that all referenced indices are -less-than the current definition's index. - -When core modules are embedded in adapter modules, this is done by literally -embedding a [core module binary] in-line in the module section. Thus, a -runtime can implement adapter modules in terms of an existing core engine -by recursively invoking the engine's binary decoding logic when a core module -definition is encountered. More generally, just as the Component Model spec is -layered in top of the Core WebAssembly spec, a Component Model implementation -is meant to be layered on top of a Core WebAssembly implementation. - -As an example, this adapter module: -```wasm -(adapter module - (import "a" (instance $a (export "f" (func)))) - (module $M - (import "a" "f" (func)) - (func (export "f"))) - (instance $m1 (instantiate $M (import "a" (instance $a)))) - (instance $m2 (instantiate $M (import "a" (instance $m1)))) - (alias $m2 "f" (func $f)) - (export "g" (func $f)) -) -``` -could be encoded with the binary section sequence: -1. Type Section, defining an instance type (for `$a`) and function type (for `f`) -2. Import Section, defining the import `$a`, referencing the instance type in (1) -3. Module Section, defining the module `$M` by embedding the core module binary - format of `$M` inline -4. Instance Section, defining the instance `$m1`, referencing (3) and (2) -5. Instance Section, defining the instance `$m2`, referencing (3) and (4) -8. Alias Section, adding `f` to the function index space, referencing (5) -9. Export section, exporting `g`, referencing (8) - -This repository also contains a [detailed binary format sketch](./Binary.md). - - -## Web Platform Integration - -### JS API - -The [JS API] currently provides functions like `WebAssembly.compile()` and -`WebAssembly.compileStreaming()` which take raw bytes from an `ArrayBuffer` or -`Response` object and compile them into core modules that are wrapped in a -`WebAssembly.Module` objects. - -To natively support the Component Model, the JS API would be extended to allow -the existing JS API functions (`WebAssembly.compile()` et al) to accept adapter -module binaries. As described [above](#binary-format-considerations), an engine -can determine whether a given binary is a core or adapter module by examining -the `layer` field in the first 8 bytes. - -Since adapter modules have the same outward-facing structure as core modules, -the result of loading an adapter module with the JS API would just be a -`WebAssembly.Module` object. One area where the JS API would have to be -extended is in the [*read the imports*] logic, to support single-level imports, -instance imports and module imports. There is a fairly natural exension for all -of these features. For example, the adapter module: -```wasm -;; a.wasm -(adapter module - (import "one" (func)) - (import "two" (instance - (export "three" (instance - (export "four" (module - (import "five" (func)) - (export "six" (func)) - )) - )) - )) -) -``` -could be successfully instantiated via: -```js -WebAssembly.instantiateStreaming(fetch('./a.wasm'), { - one: () => (), - two: { - three: { - four: new WebAssembly.Module(code) - } - } -}); -``` -where `instantiateStreaming` checks that the module created from `code` exports -a function `six` (and *may* import a function `five`). - -Additionally, the JS API `WebAssembly.Module.imports()` and `exports()` -functions would need to be extended to include the new instance and module -types in the `kind` fields. - -Lastly, considering the new exportable types, a module export would naturally -produce a `WebAssembly.Module` object. For an instance export, the JavaScript -correspondence already established by [ESM-integration] is a [Namespace Object]. - - -### ESM-integration - -Like the JS API, [ESM-integration] can be extended to load adapter module -binaries in all the same places where core module binaries can be loaded today, -branching on the `layer` field in the binary format to determine the kind of -module to decode. - -As with the JS API, the main question for ESM-integration is how to deal with -all imports having a single string as well as the new instance and module -import/export types. Going through these: - -For adapter module imports of module type, we need a fundamentally new way to -request that the ESM loader parse or decode a module without *also* -instantiating that module. Recognizing this same need from JavaScript, there is -already a TC39 proposal called [Import Reflection] that adds the ability to -write, in JavaScript: -```js -import Foo from "./foo.wasm" as "wasm-module"; -assert(Foo instanceof WebAssembly.Module); -``` -With this extension to JavaScript and the ESM loader, an adapter module import -of module type can be treated like an `as "wasm-module"` import by -ESM-integration. - -In all other cases, the (single) string imported by an adapter module import is -first resolved to a [Module Record] using the same process as resolving the -[Module Specifier] of a JavaScript `import`. After this, the handling of the -imported Module Record is determined by the import type: - -For imports of instance type, the ESM loader would treat the exports of the -instance type as if they were the [Named Imports] of a JavaScript `import`. -Thus, single-level imports of instance type mirror the behavior of core -two-level imports with existing ESM-integration. Since the exports of an -instance type can themselves be instance types, this process must be performed -recursively. - -Otherwise, the import is treated like a JavaScript [Imported Default Binding] -and the Module Record is converted to its default value. This allows, for -example, a single level import of a function: -```wasm -(adapter module - (import "./foo.js" (func (result i32))) -) -``` -to be satisfied by a JavaScript module via ESM-integration: -```js -// foo.js -export default () => 42; -``` -Lastly, for exports, ESM-integration would produce the same JavaScript -objects for exports as described above for the JS API. - - - -[Component Model]: ../../high-level -[Component Model use cases]: ../../high-level/UseCases.md -[Design Choices]: ../../high-level/Choices.md -[Shared-Nothing]: ../../high-level/Choices.md - -[Interface Types]: https://github.com/WebAssembly/interface-types - -[ESM-integration]: https://github.com/WebAssembly/esm-integration -[Namespace Object]: https://tc39.es/ecma262/multipage/reflection.html#sec-module-namespace-objects -[Import Reflection]: https://github.com/tc39-transfer/proposal-import-reflection -[Module Record]: https://tc39.es/ecma262/#sec-abstract-module-records -[Module Specifier]: https://tc39.es/ecma262/multipage/ecmascript-language-scripts-and-modules.html#prod-ModuleSpecifier -[Named Imports]: https://tc39.es/ecma262/multipage/ecmascript-language-scripts-and-modules.html#prod-NamedImports -[Imported Default Binding]: https://tc39.es/ecma262/multipage/ecmascript-language-scripts-and-modules.html#prod-ImportedDefaultBinding - -[Core Concepts]: https://webassembly.github.io/spec/core/intro/overview.html#concepts -[`typeuse`]: https://webassembly.github.io/spec/core/text/modules.html#type-uses -[Index Space]: https://webassembly.github.io/spec/core/syntax/modules.html#indices -[`module`]: https://webassembly.github.io/spec/core/text/modules.html#text-module -[`import`]: https://webassembly.github.io/spec/core/text/modules.html#imports -[`functype`]: https://webassembly.github.io/spec/core/text/types.html#function-types -[`tabletype`]: https://webassembly.github.io/spec/core/text/types.html#table-types -[`memtype`]: https://webassembly.github.io/spec/core/text/types.html#memory-types -[`globaltype`]: https://webassembly.github.io/spec/core/text/types.html#global-types -[func-import-abbrev]: https://webassembly.github.io/spec/core/text/modules.html#text-func-abbrev -[Module Binary]: https://webassembly.github.io/spec/core/binary/modules.html#binary-module -[Sections]: https://webassembly.github.io/spec/core/binary/modules.html#sections -[Module Instantiation]: https://webassembly.github.io/spec/core/appendix/embedding.html#mathrm-module-instantiate-xref-exec-runtime-syntax-store-mathit-store-xref-syntax-modules-syntax-module-mathit-module-xref-exec-runtime-syntax-externval-mathit-externval-ast-xref-exec-runtime-syntax-store-mathit-store-xref-exec-runtime-syntax-moduleinst-mathit-moduleinst-xref-appendix-embedding-embed-error-mathit-error -[JS API]: https://webassembly.github.io/spec/js-api/index.html -[`WebAssembly.instantiate()`]: https://webassembly.github.io/spec/js-api/index.html#dom-webassembly-instantiate-moduleobject-importobject -[*read the imports*]: https://webassembly.github.io/spec/js-api/index.html#read-the-imports - -[Statically link]: https://en.wikipedia.org/wiki/Static_library -[Native Dynamic Linking]: https://en.wikipedia.org/wiki/Dynamic_loading -[Principle of Least Authority]: https://en.wikipedia.org/wiki/Principle_of_least_privilege -[Virtualize]: https://en.wikipedia.org/wiki/Virtualization -[Mocking]: https://en.wikipedia.org/wiki/Mock_object -[De Bruijn Indices]: https://en.wikipedia.org/wiki/De_Bruijn_index -[Closure]: https://en.wikipedia.org/wiki/Closure_(computer_programming) -[PIC]: https://en.wikipedia.org/wiki/Position-independent_code - -[Figma plugins]: https://www.figma.com/blog/an-update-on-plugin-security/ -[Attenuate]: http://cap-lore.com/CapTheory/Patterns/Attenuation.html - -[Issue-30]: https://github.com/WebAssembly/module-linking/issues/30 diff --git a/design/proposals/module-linking/link-time-virtualization.svg b/design/proposals/module-linking/link-time-virtualization.svg deleted file mode 100644 index 19b8bae4..00000000 --- a/design/proposals/module-linking/link-time-virtualization.svg +++ /dev/null @@ -1 +0,0 @@ - \ No newline at end of file diff --git a/design/proposals/module-linking/shared-everything-dynamic-linking.svg b/design/proposals/module-linking/shared-everything-dynamic-linking.svg deleted file mode 100644 index 294acc87..00000000 --- a/design/proposals/module-linking/shared-everything-dynamic-linking.svg +++ /dev/null @@ -1 +0,0 @@ - \ No newline at end of file diff --git a/document/Makefile b/document/Makefile new file mode 100644 index 00000000..875efc72 --- /dev/null +++ b/document/Makefile @@ -0,0 +1,76 @@ +DIRS = core js-api web-api +FILES = index.html +BUILDDIR = _build + +# Global targets. + +.PHONY: all +all: $(BUILDDIR) root $(DIRS) + +$(BUILDDIR): + mkdir -p $@ + +.PHONY: deploy +deploy: + GIT_DEPLOY_DIR=$(BUILDDIR) bash deploy.sh + +.PHONY: publish +publish: all deploy + +.PHONY: clean +clean: $(DIRS:%=clean-%) + rm -rf $(BUILDDIR) + +.PHONY: diff +diff: $(DIRS:%=diff-%) + + +# Directory-specific targets. + +.PHONY: root +root: $(BUILDDIR) + touch $(BUILDDIR)/.nojekyll + cp -f $(FILES) $(BUILDDIR)/ + +.PHONY: $(DIRS) +$(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-%): deploy-%: + GIT_DEPLOY_DIR=$(BUILDDIR) GIT_DEPLOY_SUBDIR=$(@:deploy-%=%) bash deploy.sh + +.PHONY: $(DIRS:%=publish-%) +$(DIRS:%=publish-%): publish-%: % deploy-% + +.PHONY: $(DIRS:%=clean-%) +$(DIRS:%=clean-%): clean-%: + (cd $(@:clean-%=%); make BUILDDIR=$(BUILDDIR) clean) + rm -rf $(BUILDDIR)/$(@:clean-%=%) + +.PHONY: $(DIRS:%=diff-%) +$(DIRS:%=diff-%): diff-%: + (cd $(@:diff-%=%); make BUILDDIR=$(BUILDDIR) diff) + + +# Help. + +.PHONY: help +help: + @echo "Please use \`make ' where is one of" + @echo " all to build all documents" + @echo " publish to make all and push to gh-pages" + @echo " to build a specific subdirectory" + @echo " publish- to build and push a specific subdirectory" + +.PHONY: usage +usage: help diff --git a/document/README.md b/document/README.md new file mode 100644 index 00000000..e8312f42 --- /dev/null +++ b/document/README.md @@ -0,0 +1,23 @@ +# WebAssembly Specifications + +This directory contains the source code for the WebAssembly spec documents, as served from the [webassembly.github.io/spec](https://webassembly.github.io/spec) pages. +It uses [Sphinx](http://www.sphinx-doc.org/) and [Bikeshed](https://github.com/tabatkins/bikeshed). + +To install Sphinx: +``` +pip install sphinx +``` + +To install Bikeshed, see the instructions [here](https://tabatkins.github.io/bikeshed/#installing). + + +To build everything locally (result appears in `_build/`): +``` +make all +``` + +To build everything and update [webassembly.github.io/spec](https://webassembly.github.io/spec) with it: +``` +make publish +``` +Please make sure to only use that once a change has approval. diff --git a/document/core/.gitignore b/document/core/.gitignore new file mode 100644 index 00000000..b932ec28 --- /dev/null +++ b/document/core/.gitignore @@ -0,0 +1,3 @@ +_build +_static +document/*.pyc diff --git a/document/core/LICENSE b/document/core/LICENSE new file mode 100644 index 00000000..795b406e --- /dev/null +++ b/document/core/LICENSE @@ -0,0 +1,50 @@ +W3C SOFTWARE AND DOCUMENT NOTICE AND LICENSE + +This work is being provided by the copyright holders under the following +license. + + +LICENSE + +By obtaining and/or copying this work, you (the licensee) agree that you have +read, understood, and will comply with the following terms and conditions. + +Permission to copy, modify, and distribute this work, with or without +modification, for any purpose and without fee or royalty is hereby granted, +provided that you include the following on ALL copies of the work or portions +thereof, including modifications: + +* The full text of this NOTICE in a location viewable to users of the + redistributed or derivative work. + +* Any pre-existing intellectual property disclaimers, notices, or terms and + conditions. If none exist, the W3C Software and Document Short Notice + (https://www.w3.org/Consortium/Legal/copyright-software-short-notice) should + be included. + +* Notice of any changes or modifications, through a copyright statement on the + new code or document such as "This software or document includes material + copied from or derived from [title and URI of the W3C document]. Copyright © [YEAR] W3C® (MIT, ERCIM, Keio, Beihang)." + + +DISCLAIMERS + +THIS WORK IS PROVIDED "AS IS," AND COPYRIGHT HOLDERS MAKE NO REPRESENTATIONS +OR WARRANTIES, EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO, WARRANTIES OF +MERCHANTABILITY OR FITNESS FOR ANY PARTICULAR PURPOSE OR THAT THE USE OF THE +SOFTWARE OR DOCUMENT WILL NOT INFRINGE ANY THIRD PARTY PATENTS, COPYRIGHTS, +TRADEMARKS OR OTHER RIGHTS. + +COPYRIGHT HOLDERS WILL NOT BE LIABLE FOR ANY DIRECT, INDIRECT, SPECIAL OR +CONSEQUENTIAL DAMAGES ARISING OUT OF ANY USE OF THE SOFTWARE OR DOCUMENT. + +The name and trademarks of copyright holders may NOT be used in advertising or +publicity pertaining to the work without specific, written prior permission. +Title to copyright in this work will at all times remain with copyright +holders. + + +NOTES + +This version: +http://www.w3.org/Consortium/Legal/2015/copyright-software-and-document diff --git a/document/core/Makefile b/document/core/Makefile new file mode 100644 index 00000000..da65b10a --- /dev/null +++ b/document/core/Makefile @@ -0,0 +1,355 @@ +# Makefile for Sphinx documentation +# + +# You can set these variables from the command line. +SPHINXOPTS = +SPHINXBUILD = sphinx-build +PAPER = a4 +BUILDDIR = _build +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) . +# the i18n builder cannot share the environment and doctrees with the others +I18NSPHINXOPTS = $(PAPEROPT_$(PAPER)) $(SPHINXOPTS) . + +.PHONY: usage +usage: + @echo "Please use \`make ' where is one of" + @echo " html to make standalone HTML files" + @echo " pdf to make standalone PDF file" + @echo " bikeshed to make a bikeshed wrapped single large HTML file" + @echo " diff to make a diff of the bikeshed HTML file with the latest TR" + @echo " WD-tar generate tar file for updating the Working Draft" + @echo " WD-echidna publish the Working Draft tar file via Echidna" + @echo " all to make all 3" + @echo " publish to make all and push to gh-pages" + @echo " help to see more options" + +.PHONY: help +help: + @echo "Usage: \`make ' where is one of" + @echo " html to make standalone HTML files" + @echo " pdf to make standalone PDF file" + @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" + @echo " pickle to make pickle files" + @echo " json to make JSON files" + @echo " htmlhelp to make HTML files and a HTML help project" + @echo " qthelp to make HTML files and a qthelp project" + @echo " applehelp to make an Apple Help Book" + @echo " devhelp to make HTML files and a Devhelp project" + @echo " epub to make an epub" + @echo " epub3 to make an epub3" + @echo " latex to make LaTeX files, you can set PAPER=a4 or PAPER=letter" + @echo " latexpdf to make LaTeX files and run them through pdflatex" + @echo " latexpdfja to make LaTeX files and run them through platex/dvipdfmx" + @echo " text to make text files" + @echo " man to make manual pages" + @echo " texinfo to make Texinfo files" + @echo " info to make Texinfo files and run them through makeinfo" + @echo " gettext to make PO message catalogs" + @echo " changes to make an overview of all changed/added/deprecated items" + @echo " xml to make Docutils-native XML files" + @echo " pseudoxml to make pseudoxml-XML files for display purposes" + @echo " linkcheck to check all external links for integrity" + @echo " doctest to run all doctests embedded in the documentation (if enabled)" + @echo " coverage to run coverage check of the documentation (if enabled)" + @echo " dummy to check syntax errors of document sources" + +.PHONY: deploy +deploy: + (cd ..; make dir-core deploy-core) + +.PHONY: publish +publish: clean all deploy + +.PHONY: publish-main +publish-main: clean main bikeshed-keep deploy + +.PHONY: all +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 + mkdir -p $(BUILDDIR)/html/$(DOWNLOADDIR) + ln -f $(BUILDDIR)/latex/$(NAME).pdf $(BUILDDIR)/html/$(DOWNLOADDIR)/$(NAME).pdf + + +.PHONY: clean +clean: + rm -rf $(BUILDDIR) + rm -rf $(STATICDIR) + +.PHONY: html +html: + $(SPHINXBUILD) -b html $(ALLSPHINXOPTS) $(BUILDDIR)/html + for file in `ls $(BUILDDIR)/html/*.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;MathJax.Hub.Config({TeX: {MAXBUFFER: 30*1024}})$$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/." + +.PHONY: dirhtml +dirhtml: + $(SPHINXBUILD) -b dirhtml $(ALLSPHINXOPTS) $(BUILDDIR)/dirhtml + @echo + @echo "Build finished. The HTML pages are in $(BUILDDIR)/dirhtml." + +.PHONY: singlehtml +singlehtml: + $(SPHINXBUILD) -b singlehtml $(ALLSPHINXOPTS) $(BUILDDIR)/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/ + (cd util/katex/ && npm install --only=prod) + 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 + cp $(BUILDDIR)/bikeshed_singlehtml/_static/pygments.css \ + $(BUILDDIR)/html/bikeshed/ + @echo + @echo "Build finished. The HTML page is in $(BUILDDIR)/html/bikeshed/." + +.PHONY: WD-tar +WD-tar: bikeshed + @echo "Building tar file..." + tar cvf \ + $(BUILDDIR)/WD.tar \ + --transform='s|$(BUILDDIR)/html/bikeshed/||' \ + --transform='s|index.html|Overview.html|' \ + $(BUILDDIR)/html/bikeshed/index.html \ + $(BUILDDIR)/html/bikeshed/pygments.css \ + $(BUILDDIR)/html/bikeshed/katex/dist/katex.css \ + $(BUILDDIR)/html/bikeshed/katex/dist/fonts + @echo "Built $(BUILDDIR)/WD.tar." + +.PHONY: WD-echidna +WD-echidna: WD-tar + @if [ -z $(W3C_USERNAME) ] || \ + [ -z $(W3C_PASSWORD) ] || \ + [ -z $(DECISION_URL) ] ; then \ + echo "Must provide W3C_USERNAME, W3C_PASSWORD, and DECISION_URL environment variables"; \ + exit 1; \ + fi + curl 'https://labs.w3.org/echidna/api/request' \ + --user '$(W3C_USERNAME):$(W3C_PASSWORD)' \ + -F "tar=@$(BUILDDIR)/WD.tar" \ + -F "decision=$(DECISION_URL)" | tee $(BUILDDIR)/WD-echidna-id.txt + @echo + @echo "Published working draft. Check its status at https://labs.w3.org/echidna/api/status?id=`cat $(BUILDDIR)/WD-echidna-id.txt`" + +.PHONY: diff +diff: bikeshed + @echo "Downloading the old single-file html spec..." + curl `grep "^TR" index.bs | cut -d' ' -f2` -o $(BUILDDIR)/html/bikeshed/old.html + @echo "Done." + @echo "Diffing new against old (go get a coffee)..." + perl ../util/htmldiff.pl $(BUILDDIR)/html/bikeshed/old.html $(BUILDDIR)/html/bikeshed/index.html $(BUILDDIR)/html/bikeshed/diff.html + @echo "Done. The diff is at $(BUILDDIR)/html/bikeshed/diff.html" + +.PHONY: pickle +pickle: + $(SPHINXBUILD) -b pickle $(ALLSPHINXOPTS) $(BUILDDIR)/pickle + @echo + @echo "Build finished; now you can process the pickle files." + +.PHONY: json +json: + $(SPHINXBUILD) -b json $(ALLSPHINXOPTS) $(BUILDDIR)/json + @echo + @echo "Build finished; now you can process the JSON files." + +.PHONY: htmlhelp +htmlhelp: + $(SPHINXBUILD) -b htmlhelp $(ALLSPHINXOPTS) $(BUILDDIR)/htmlhelp + @echo + @echo "Build finished; now you can run HTML Help Workshop with the" \ + ".hhp project file in $(BUILDDIR)/htmlhelp." + +.PHONY: qthelp +qthelp: + $(SPHINXBUILD) -b qthelp $(ALLSPHINXOPTS) $(BUILDDIR)/qthelp + @echo + @echo "Build finished; now you can run "qcollectiongenerator" with the" \ + ".qhcp project file in $(BUILDDIR)/qthelp, like this:" + @echo "# qcollectiongenerator $(BUILDDIR)/qthelp/WebAssembly.qhcp" + @echo "To view the help file:" + @echo "# assistant -collectionFile $(BUILDDIR)/qthelp/WebAssembly.qhc" + +.PHONY: applehelp +applehelp: + $(SPHINXBUILD) -b applehelp $(ALLSPHINXOPTS) $(BUILDDIR)/applehelp + @echo + @echo "Build finished. The help book is in $(BUILDDIR)/applehelp." + @echo "N.B. You won't be able to view it unless you put it in" \ + "~/Library/Documentation/Help or install it in your application" \ + "bundle." + +.PHONY: devhelp +devhelp: + $(SPHINXBUILD) -b devhelp $(ALLSPHINXOPTS) $(BUILDDIR)/devhelp + @echo + @echo "Build finished." + @echo "To view the help file:" + @echo "# mkdir -p $$HOME/.local/share/devhelp/WebAssembly" + @echo "# ln -s $(BUILDDIR)/devhelp $$HOME/.local/share/devhelp/WebAssembly" + @echo "# devhelp" + +.PHONY: epub +epub: + $(SPHINXBUILD) -b epub $(ALLSPHINXOPTS) $(BUILDDIR)/epub + @echo + @echo "Build finished. The epub file is in $(BUILDDIR)/epub." + +.PHONY: epub3 +epub3: + $(SPHINXBUILD) -b epub3 $(ALLSPHINXOPTS) $(BUILDDIR)/epub3 + @echo + @echo "Build finished. The epub3 file is in $(BUILDDIR)/epub3." + +.PHONY: latex +latex: + $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex + @echo + @echo "Build finished; the LaTeX files are in $(BUILDDIR)/latex." + @echo "Run \`make' in that directory to run these through (pdf)latex" \ + "(use \`make latexpdf' here to do that automatically)." + +.PHONY: latexpdf +latexpdf: + $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex + @echo "Running LaTeX files through pdflatex..." + $(MAKE) -C $(BUILDDIR)/latex all-pdf + @echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex." + +.PHONY: latexpdfja +latexpdfja: + $(SPHINXBUILD) -b latex $(ALLSPHINXOPTS) $(BUILDDIR)/latex + @echo "Running LaTeX files through platex and dvipdfmx..." + $(MAKE) -C $(BUILDDIR)/latex all-pdf-ja + @echo "pdflatex finished; the PDF files are in $(BUILDDIR)/latex." + +.PHONY: text +text: + $(SPHINXBUILD) -b text $(ALLSPHINXOPTS) $(BUILDDIR)/text + @echo + @echo "Build finished. The text files are in $(BUILDDIR)/text." + +.PHONY: man +man: + $(SPHINXBUILD) -b man $(ALLSPHINXOPTS) $(BUILDDIR)/man + @echo + @echo "Build finished. The manual pages are in $(BUILDDIR)/man." + +.PHONY: texinfo +texinfo: + $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo + @echo + @echo "Build finished. The Texinfo files are in $(BUILDDIR)/texinfo." + @echo "Run \`make' in that directory to run these through makeinfo" \ + "(use \`make info' here to do that automatically)." + +.PHONY: info +info: + $(SPHINXBUILD) -b texinfo $(ALLSPHINXOPTS) $(BUILDDIR)/texinfo + @echo "Running Texinfo files through makeinfo..." + make -C $(BUILDDIR)/texinfo info + @echo "makeinfo finished; the Info files are in $(BUILDDIR)/texinfo." + +.PHONY: gettext +gettext: + $(SPHINXBUILD) -b gettext $(I18NSPHINXOPTS) $(BUILDDIR)/locale + @echo + @echo "Build finished. The message catalogs are in $(BUILDDIR)/locale." + +.PHONY: changes +changes: + $(SPHINXBUILD) -b changes $(ALLSPHINXOPTS) $(BUILDDIR)/changes + @echo + @echo "The overview file is in $(BUILDDIR)/changes." + +.PHONY: linkcheck +linkcheck: + $(SPHINXBUILD) -b linkcheck $(ALLSPHINXOPTS) $(BUILDDIR)/linkcheck + @echo + @echo "Link check complete; look for any errors in the above output " \ + "or in $(BUILDDIR)/linkcheck/output.txt." + +.PHONY: doctest +doctest: + $(SPHINXBUILD) -b doctest $(ALLSPHINXOPTS) $(BUILDDIR)/doctest + @echo "Testing of doctests in the sources finished, look at the " \ + "results in $(BUILDDIR)/doctest/output.txt." + +.PHONY: coverage +coverage: + $(SPHINXBUILD) -b coverage $(ALLSPHINXOPTS) $(BUILDDIR)/coverage + @echo "Testing of coverage in the sources finished, look at the " \ + "results in $(BUILDDIR)/coverage/python.txt." + +.PHONY: xml +xml: + $(SPHINXBUILD) -b xml $(ALLSPHINXOPTS) $(BUILDDIR)/xml + @echo + @echo "Build finished. The XML files are in $(BUILDDIR)/xml." + +.PHONY: pseudoxml +pseudoxml: + $(SPHINXBUILD) -b pseudoxml $(ALLSPHINXOPTS) $(BUILDDIR)/pseudoxml + @echo + @echo "Build finished. The pseudo-XML files are in $(BUILDDIR)/pseudoxml." + +.PHONY: dummy +dummy: + $(SPHINXBUILD) -b dummy $(ALLSPHINXOPTS) $(BUILDDIR)/dummy + @echo + @echo "Build finished. Dummy builder generates no files." diff --git a/document/core/README.md b/document/core/README.md new file mode 100644 index 00000000..299b7a3a --- /dev/null +++ b/document/core/README.md @@ -0,0 +1,25 @@ +# WebAssembly Core Specification + +This is the official WebAssembly "language" specification. + +It uses [Sphinx](http://www.sphinx-doc.org/). To install that: +``` +pip install sphinx +``` +To make HTML (result in `_build/html`): +``` +make html +``` +To make PDF (result in `_build/latex`, requires LaTeX): +``` +make pdf +``` +To make all: +``` +make all +``` +Finally, to make all and update webassembly.github.io/spec with it: +``` +make publish +``` +Please make sure to only use that once a change has approval. diff --git a/document/core/appendix/algorithm.rst b/document/core/appendix/algorithm.rst new file mode 100644 index 00000000..feede049 --- /dev/null +++ b/document/core/appendix/algorithm.rst @@ -0,0 +1,206 @@ +.. index:: validation, algorithm, instruction, module, binary format, opcode +.. _algo-valid: + +Validation Algorithm +-------------------- + +The specification of WebAssembly :ref:`validation ` is purely *declarative*. +It describes the constraints that must be met by a :ref:`module ` or :ref:`instruction ` sequence to be valid. + +This section sketches the skeleton of a sound and complete *algorithm* for effectively validating code, i.e., sequences of :ref:`instructions `. +(Other aspects of validation are straightforward to implement.) + +In fact, the algorithm is expressed over the flat sequence of opcodes as occurring in the :ref:`binary format `, and performs only a single pass over it. +Consequently, it can be integrated directly into a decoder. + +The algorithm is expressed in typed pseudo code whose semantics is intended to be self-explanatory. + + +.. index:: value type, stack, label, frame, instruction + +Data Structures +~~~~~~~~~~~~~~~ + +The algorithm uses two separate stacks: the *operand stack* and the *control stack*. +The former tracks the :ref:`types ` of operand values on the :ref:`stack `, +the latter surrounding :ref:`structured control instructions ` and their associated :ref:`blocks `. + +.. code-block:: pseudo + + type val_type = I32 | I64 | F32 | F64 + + type opd_stack = stack(val_type | Unknown) + + type ctrl_stack = stack(ctrl_frame) + type ctrl_frame = { + label_types : list(val_type) + end_types : list(val_type) + height : nat + unreachable : bool + } + +For each value, the operand stack records its :ref:`value type `, or :code:`Unknown` when the type is not known. + +For each entered block, the control stack records a *control frame* with the type of the associated :ref:`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 ` typing after branches). + +.. note:: + In the presentation of this algorithm, multiple values are supported for the :ref:`result types ` classifying blocks and labels. + With the current version of WebAssembly, the :code:`list` could be simplified to an optional value. + +For the purpose of presenting the algorithm, the operand and control stacks are simply maintained as global variables: + +.. code-block:: pseudo + + var opds : opd_stack + var ctrls : ctrl_stack + +However, these variables are not manipulated directly by the main checking function, but through a set of auxiliary functions: + +.. code-block:: pseudo + + func push_opd(type : val_type | Unknown) = + opds.push(type) + + func pop_opd() : val_type | Unknown = + if (opds.size() = ctrls[0].height && ctrls[0].unreachable) return Unknown + error_if(opds.size() = ctrls[0].height) + return opds.pop() + + func pop_opd(expect : val_type | Unknown) : val_type | Unknown = + let actual = pop_opd() + if (actual = Unknown) return expect + if (expect = Unknown) return actual + error_if(actual =/= expect) + return actual + + func push_opds(types : list(val_type)) = foreach (t in types) push_opd(t) + func pop_opds(types : list(val_type)) = foreach (t in reverse(types)) pop_opd(t) + +Pushing an operand simply pushes the respective type to the operand stack. + +Popping an operand checks that the operand stack does not underflow the current block and then removes one type. +But first, a special case is handled where the block contains no known operands, but has been marked as unreachable. +That can occur after an unconditional branch, when the stack is typed :ref:`polymorphically `. +In that case, an unknown type is returned. + +A second function for popping an operand takes an expected type, which the actual operand type is checked against. +The types may differ in case one of them is Unknown. +The more specific type is returned. + +Finally, there are accumulative functions for pushing or popping multiple operand types. + +.. note:: + The notation :code:`stack[i]` is meant to index the stack from the top, + so that :code:`ctrls[0]` accesses the element pushed last. + + +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, opds.size(), false) +   ctrls.push(frame) + + func pop_ctrl() : list(val_type) = +  error_if(ctrls.is_empty()) +  let frame = ctrls[0] +   pop_opds(frame.end_types) +   error_if(opds.size() =/= frame.height) + ctrls.pop() +   return frame.end_types + + func unreachable() = +   opds.resize(ctrls[0].height) +   ctrls[0].unreachable := true + +Pushing a control frame takes the types of the label and result values. +It allocates a new frame record recording them along with the current height of the operand stack and marks the block as reachable. + +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. + +Finally, the current frame can be marked as unreachable. +In that case, all existing operand types are purged from the operand stack, in order to allow for the :ref:`stack-polymorphism ` logic in :code:`pop_opd` to take effect. + +.. note:: + Even with the unreachable flag set, consecutive operands are still pushed to and popped from the operand stack. + That is necessary to detect invalid :ref:`examples ` like :math:`(\UNREACHABLE~(\I32.\CONST)~\I64.\ADD)`. + However, a polymorphic stack cannot underflow, but instead generates :code:`Unknown` types as needed. + + +.. index:: opcode + +Validation of Opcode Sequences +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The following function shows the validation of a number of representative instructions that manipulate the stack. +Other instructions are checked in a similar manner. + +.. note:: + Various instructions not shown here will additionally require the presence of a validation :ref:`context ` for checking uses of :ref:`indices `. + That is an easy addition and therefore omitted from this presentation. + +.. code-block:: pseudo + + func validate(opcode) = + switch (opcode) + case (i32.add) + pop_opd(I32) + pop_opd(I32) + push_opd(I32) + + case (drop) + pop_opd() + + case (select) + pop_opd(I32) + let t1 = pop_opd() + let t2 = pop_opd(t1) + push_opd(t2) + +    case (unreachable) +       unreachable() + + case (block t*) + push_ctrl([t*], [t*]) + + case (loop t*) + push_ctrl([], [t*]) + + case (if t*) + pop_opd(I32) + push_ctrl([t*], [t*]) + + case (end) + let results = pop_ctrl() + push_opds(results) + + case (else) + let results = pop_ctrl() + push_ctrl(results, results) + + case (br n) +      error_if(ctrls.size() < n) +       pop_opds(ctrls[n].label_types) +       unreachable() + + case (br_if n) +      error_if(ctrls.size() < n) + pop_opd(I32) +       pop_opds(ctrls[n].label_types) +       push_opds(ctrls[n].label_types) + +    case (br_table n* m) +       error_if(ctrls.size() < m) +       foreach (n in n*) +         error_if(ctrls.size() < n || ctrls[n].label_types =/= ctrls[m].label_types) + pop_opd(I32) +       pop_opds(ctrls[m].label_types) +       unreachable() + +.. note:: + It is an invariant under the current WebAssembly instruction set that an operand of :code:`Unknown` type is never duplicated on the stack. + This would change if the language were extended with stack instructions like :code:`dup`. + Under such an extension, the above algorithm would need to be refined by replacing the :code:`Unknown` type with proper *type variables* to ensure that all uses are consistent. diff --git a/document/core/appendix/custom.rst b/document/core/appendix/custom.rst new file mode 100644 index 00000000..bea81d61 --- /dev/null +++ b/document/core/appendix/custom.rst @@ -0,0 +1,145 @@ +.. index:: custom section, section, binary format + +Custom Sections +--------------- + +This appendix defines dedicated :ref:`custom sections ` for WebAssembly's :ref:`binary format `. +Such sections do not contribute to, or otherwise affect, the WebAssembly semantics, and like any custom section they may be ignored by an implementation. +However, they provide useful meta data that implementations can make use of to improve user experience or take compilation hints. + +Currently, only one dedicated custom section is defined, the :ref:`name section`. + + +.. index:: ! name section, name, Unicode UTF-8 +.. _binary-namesec: + +Name Section +~~~~~~~~~~~~ + +The *name section* is a :ref:`custom section ` whose name string is itself :math:`\text{name}`. +The name section should appear only once in a module, and only after the :ref:`data section `. + +The purpose of this section is to attach printable names to definitions in a module, which e.g. can be used by a debugger or when parts of the module are to be rendered in :ref:`text form `. + +.. note:: + All :ref:`names ` are represented in |Unicode|_ encoded in UTF-8. + Names need not be unique. + + +.. _binary-namesubsection: + +Subsections +........... + +The :ref:`data ` of a name section consists of a sequence of *subsections*. +Each subsection consists of a + +* a one-byte subsection *id*, +* the |U32| *size* of the contents, in bytes, +* the actual *contents*, whose structure is depended on the subsection id. + +.. math:: + \begin{array}{llcll} + \production{name section} & \Bnamesec &::=& + \Bsection_0(\Bnamedata) \\ + \production{name data} & \Bnamedata &::=& + n{:}\Bname & (\iff n = \text{name}) \\ &&& + \Bmodulenamesubsec^? \\ &&& + \Bfuncnamesubsec^? \\ &&& + \Blocalnamesubsec^? \\ + \production{name subsection} & \Bnamesubsection_N(\B{B}) &::=& + N{:}\Bbyte~~\X{size}{:}\Bu32~~\B{B} + & (\iff \X{size} = ||\B{B}||) \\ + \end{array} + +The following subsection ids are used: + +== =========================================== +Id Subsection +== =========================================== + 0 :ref:`module name ` + 1 :ref:`function names ` + 2 :ref:`local names ` +== =========================================== + +Each subsection may occur at most once, and in order of increasing id. + + +.. index:: ! name map, index, index space +.. _binary-indirectnamemap: +.. _binary-namemap: + +Name Maps +......... + +A *name map* assigns :ref:`names ` to :ref:`indices ` in a given :ref:`index space `. +It consists of a :ref:`vector ` of index/name pairs in order of increasing index value. +Each index must be unique, but the assigned names need not be. + +.. math:: + \begin{array}{llclll} + \production{name map} & \Bnamemap &::=& + \Bvec(\Bnameassoc) \\ + \production{name association} & \Bnameassoc &::=& + \Bidx~\Bname \\ + \end{array} + +An *indirect name map* assigns :ref:`names ` to a two-dimensional :ref:`index space `, where secondary indices are *grouped* by primary indices. +It consists of a vector of primary index/name map pairs in order of increasing index value, where each name map in turn maps secondary indices to names. +Each primary index must be unique, and likewise each secondary index per individual name map. + +.. math:: + \begin{array}{llclll} + \production{indirect name map} & \Bindirectnamemap &::=& + \Bvec(\Bindirectnameassoc) \\ + \production{indirect name association} & \Bindirectnameassoc &::=& + \Bidx~\Bnamemap \\ + \end{array} + + +.. index:: module +.. _binary-modulenamesec: + +Module Names +............ + +The *module name subsection* has the id 0. +It simply consists of a single :ref:`name ` that is assigned to the module itself. + +.. math:: + \begin{array}{llclll} + \production{module name subsection} & \Bmodulenamesubsec &::=& + \Bnamesubsection_0(\Bname) \\ + \end{array} + + +.. index:: function, function index +.. _binary-funcnamesec: + +Function Names +.............. + +The *function name subsection* has the id 1. +It consists of a :ref:`name map ` assigning function names to :ref:`function indices `. + +.. math:: + \begin{array}{llclll} + \production{function name subsection} & \Bfuncnamesubsec &::=& + \Bnamesubsection_1(\Bnamemap) \\ + \end{array} + + +.. index:: function, local, function index, local index +.. _binary-localnamesec: + +Local Names +........... + +The *local name subsection* has the id 2. +It consists of an :ref:`indirect name map ` assigning local names to :ref:`local indices ` grouped by :ref:`function indices `. + +.. math:: + \begin{array}{llclll} + \production{local name subsection} & \Blocalnamesubsec &::=& + \Bnamesubsection_2(\Bindirectnamemap) \\ + \end{array} diff --git a/document/core/appendix/embedding.rst b/document/core/appendix/embedding.rst new file mode 100644 index 00000000..70866c72 --- /dev/null +++ b/document/core/appendix/embedding.rst @@ -0,0 +1,622 @@ +.. index:: ! embedding, embedder, implementation, host +.. _embed: + +Embedding +--------- + +A WebAssembly implementation will typically be *embedded* into a *host* environment. +An *embedder* implements the connection between such a host environment and the WebAssembly semantics as defined in the main body of this specification. +An embedder is expected to interact with the semantics in well-defined ways. + +This section defines a suitable interface to the WebAssembly semantics in the form of entry points through which an embedder can access it. +The interface is intended to be complete, in the sense that an embedder does not need to reference other functional parts of the WebAssembly specification directly. + +.. note:: + On the other hand, an embedder does not need to provide the host environment with access to all functionality defined in this interface. + For example, an implementation may not support :ref:`parsing ` of the :ref:`text format `. + +Types +~~~~~ + +In the description of the embedder interface, syntactic classes from the :ref:`abstract syntax ` and the :ref:`runtime's abstract machine ` are used as names for variables that range over the possible objects from that class. +Hence, these syntactic classes can also be interpreted as types. + +For numeric parameters, notation like :math:`n:\u32` is used to specify a symbolic name in addition to the respective value range. + + +.. _embed-error: + +Errors +~~~~~~ + +Failure of an interface operation is indicated by an auxiliary syntactic class: + +.. math:: + \begin{array}{llll} + \production{(error)} & \error &::=& \ERROR \\ + \end{array} + +In addition to the error conditions specified explicitly in this section, implementations may also return errors when specific :ref:`implementation limitations ` are reached. + +.. note:: + Errors are abstract and unspecific with this definition. + Implementations can refine it to carry suitable classifications and diagnostic messages. + + +Pre- and Post-Conditions +~~~~~~~~~~~~~~~~~~~~~~~~ + +Some operations state *pre-conditions* about their arguments or *post-conditions* about their results. +It is the embedder's responsibility to meet the pre-conditions. +If it does, the post conditions are guaranteed by the semantics. + +In addition to pre- and post-conditions explicitly stated with each operation, the specification adopts the following conventions for :ref:`runtime objects ` (:math:`store`, :math:`\moduleinst`, :math:`\externval`, :ref:`addresses `): + +* Every runtime object passed as a parameter must be :ref:`valid ` per an implicit pre-condition. + +* Every runtime object returned as a result is :ref:`valid ` per an implicit post-condition. + +.. note:: + As long as an embedder treats runtime objects as abstract and only creates and manipulates them through the interface defined here, all implicit pre-conditions are automatically met. + + + +.. index:: allocation, store +.. _embed-store: + +Store +~~~~~ + +.. _embed-store-init: + +:math:`\F{store\_init}() : \store` +.................................. + +1. Return the empty :ref:`store `. + +.. math:: + \begin{array}{lclll} + \F{store\_init}() &=& \{ \SFUNCS~\epsilon,~ \SMEMS~\epsilon,~ \STABLES~\epsilon,~ \SGLOBALS~\epsilon \} \\ + \end{array} + + + +.. index:: module +.. _embed-module: + +Modules +~~~~~~~ + +.. index:: binary format +.. _embed-module-decode: + +:math:`\F{module\_decode}(\byte^\ast) : \module ~|~ \error` +........................................................... + +1. If there exists a derivation for the :ref:`byte ` sequence :math:`\byte^\ast` as a :math:`\Bmodule` according to the :ref:`binary grammar for modules `, yielding a :ref:`module ` :math:`m`, then return :math:`m`. + +2. Else, return :math:`\ERROR`. + +.. math:: + \begin{array}{lclll} + \F{module\_decode}(b^\ast) &=& m && (\iff \Bmodule \stackrel\ast\Longrightarrow m{:}b^\ast) \\ + \F{module\_decode}(b^\ast) &=& \ERROR && (\otherwise) \\ + \end{array} + + +.. index:: text format +.. _embed-module-parse: + +:math:`\F{module\_parse}(\char^\ast) : \module ~|~ \error` +.......................................................... + +1. If there exists a derivation for the :ref:`source ` :math:`\char^\ast` as a :math:`\Tmodule` according to the :ref:`text grammar for modules `, yielding a :ref:`module ` :math:`m`, then return :math:`m`. + +2. Else, return :math:`\ERROR`. + +.. math:: + \begin{array}{lclll} + \F{module\_parse}(c^\ast) &=& m && (\iff \Tmodule \stackrel\ast\Longrightarrow m{:}c^\ast) \\ + \F{module\_parse}(c^\ast) &=& \ERROR && (\otherwise) \\ + \end{array} + + +.. index:: validation +.. _embed-module-validate: + +:math:`\F{module\_validate}(\module) : \error^?` +................................................ + +1. If :math:`\module` is :ref:`valid `, then return nothing. + +2. Else, return :math:`\ERROR`. + +.. math:: + \begin{array}{lclll} + \F{module\_validate}(m) &=& \epsilon && (\iff {} \vdashmodule m : \externtype^\ast \to {\externtype'}^\ast) \\ + \F{module\_validate}(m) &=& \ERROR && (\otherwise) \\ + \end{array} + + +.. index:: instantiation, module instance +.. _embed-module-instantiate: + +:math:`\F{module\_instantiate}(\store, \module, \externval^\ast) : (\store, \moduleinst ~|~ \error)` +.................................................................................................... + +1. Try :ref:`instantiating ` :math:`\module` in :math:`\store` with :ref:`external values ` :math:`\externval^\ast` as imports: + + a. If it succeeds with a :ref:`module instance ` :math:`\moduleinst`, then let :math:`\X{result}` be :math:`\moduleinst`. + + b. Else, let :math:`\X{result}` be :math:`\ERROR`. + +2. Return the new store paired with :math:`\X{result}`. + +.. math:: + \begin{array}{lclll} + \F{module\_instantiate}(S, m, \X{ev}^\ast) &=& (S', F.\AMODULE) && (\iff \instantiate(S, m, \X{ev}^\ast) \stepto^\ast S'; F; \epsilon) \\ + \F{module\_instantiate}(S, m, \X{ev}^\ast) &=& (S', \ERROR) && (\iff \instantiate(S, m, \X{ev}^\ast) \stepto^\ast S'; F; \TRAP) \\ + \end{array} + +.. note:: + The store may be modified even in case of an error. + + +.. index:: import +.. _embed-module-imports: + +:math:`\F{module\_imports}(\module) : (\name, \name, \externtype)^\ast` +....................................................................... + +1. Pre-condition: :math:`\module` is :ref:`valid ` with external import types :math:`\externtype^\ast` and external export types :math:`{\externtype'}^\ast`. + +2. Let :math:`\import^\ast` be the :ref:`imports ` :math:`\module.\MIMPORTS`. + +3. Assert: the length of :math:`\import^\ast` equals the length of :math:`\externtype^\ast`. + +4. For each :math:`\import_i` in :math:`\import^\ast` and corresponding :math:`\externtype_i` in :math:`\externtype^\ast`, do: + + a. Let :math:`\X{result}_i` be the triple :math:`(\import_i.\IMODULE, \import_i.\INAME, \externtype_i)`. + +5. Return the concatenation of all :math:`\X{result}_i`, in index order. + +6. Post-condition: each :math:`\externtype_i` is :ref:`valid `. + +.. math:: + ~ \\ + \begin{array}{lclll} + \F{module\_imports}(m) &=& (\X{im}.\IMODULE, \X{im}.\INAME, \externtype)^\ast \\ + && \qquad (\iff \X{im}^\ast = m.\MIMPORTS \wedge {} \vdashmodule m : \externtype^\ast \to {\externtype'}^\ast) \\ + \end{array} + + +.. index:: export +.. _embed-module-exports: + +:math:`\F{module\_exports}(\module) : (\name, \externtype)^\ast` +................................................................ + +1. Pre-condition: :math:`\module` is :ref:`valid ` with external import types :math:`\externtype^\ast` and external export types :math:`{\externtype'}^\ast`. + +2. Let :math:`\export^\ast` be the :ref:`exports ` :math:`\module.\MEXPORTS`. + +3. Assert: the length of :math:`\export^\ast` equals the length of :math:`{\externtype'}^\ast`. + +4. For each :math:`\export_i` in :math:`\export^\ast` and corresponding :math:`\externtype'_i` in :math:`{\externtype'}^\ast`, do: + + a. Let :math:`\X{result}_i` be the pair :math:`(\export_i.\ENAME, \externtype'_i)`. + +5. Return the concatenation of all :math:`\X{result}_i`, in index order. + +6. Post-condition: each :math:`\externtype'_i` is :ref:`valid `. + +.. math:: + ~ \\ + \begin{array}{lclll} + \F{module\_exports}(m) &=& (\X{ex}.\ENAME, \externtype')^\ast \\ + && \qquad (\iff \X{ex}^\ast = m.\MEXPORTS \wedge {} \vdashmodule m : \externtype^\ast \to {\externtype'}^\ast) \\ + \end{array} + + +.. index:: module, module instance +.. _embed-instance: + +Module Instances +~~~~~~~~~~~~~~~~ + +.. index:: export, export instance + +.. _embed-instance-export: + +:math:`\F{instance\_export}(\moduleinst, \name) : \externval ~|~ \error` +........................................................................ + +1. Assert: due to :ref:`validity ` of the :ref:`module instance ` :math:`\moduleinst`, all its :ref:`export names ` are different. + +2. If there exists an :math:`\exportinst_i` in :math:`\moduleinst.\MIEXPORTS` such that :ref:`name ` :math:`\exportinst_i.\EINAME` equals :math:`\name`, then: + + a. Return the :ref:`external value ` :math:`\exportinst_i.\EIVALUE`. + +3. Else, return :math:`\ERROR`. + +.. math:: + ~ \\ + \begin{array}{lclll} + \F{instance\_export}(m, \name) &=& m.\MIEXPORTS[i].\EIVALUE && (\iff m.\MEXPORTS[i].\EINAME = \name) \\ + \F{instance\_export}(m, \name) &=& \ERROR && (\otherwise) \\ + \end{array} + + +.. index:: function, host function, function address, function instance, function type, store +.. _embed-func: + +Functions +~~~~~~~~~ + +.. _embed-func-alloc: + +:math:`\F{func\_alloc}(\store, \functype, \hostfunc) : (\store, \funcaddr)` +........................................................................... + +1. Pre-condition: :math:`\functype` is :math:`valid `. + +2. Let :math:`\funcaddr` be the result of :ref:`allocating a host function ` in :math:`\store` with :ref:`function type ` :math:`\functype` and host function code :math:`\hostfunc`. + +3. Return the new store paired with :math:`\funcaddr`. + +.. math:: + \begin{array}{lclll} + \F{func\_alloc}(S, \X{ft}, \X{code}) &=& (S', \X{a}) && (\iff \allochostfunc(S, \X{ft}, \X{code}) = S', \X{a}) \\ + \end{array} + +.. note:: + This operation assumes that :math:`\hostfunc` satisfies the :ref:`pre- and post-conditions ` required for a function instance with type :math:`\functype`. + + Regular (non-host) function instances can only be created indirectly through :ref:`module instantiation `. + + +.. _embed-func-type: + +:math:`\F{func\_type}(\store, \funcaddr) : \functype` +..................................................... + +1. Assert: the :ref:`external value ` :math:`\EVFUNC~\funcaddr` is :ref:`valid ` with :ref:`external type ` :math:`\ETFUNC~\functype`. + +2. Return :math:`\functype`. + +3. Post-condition: :math:`\functype` is :ref:`valid `. + +.. math:: + \begin{array}{lclll} + \F{func\_type}(S, a) &=& \X{ft} && (\iff S \vdashexternval \EVFUNC~a : \ETFUNC~\X{ft}) \\ + \end{array} + + +.. index:: invocation, value, result +.. _embed-func-invoke: + +:math:`\F{func\_invoke}(\store, \funcaddr, \val^\ast) : (\store, \val^\ast ~|~ \error)` +........................................................................................ + +1. Try :ref:`invoking ` the function :math:`\funcaddr` in :math:`\store` with :ref:`values ` :math:`\val^\ast` as arguments: + + a. If it succeeds with :ref:`values ` :math:`{\val'}^\ast` as results, then let :math:`\X{result}` be :math:`{\val'}^\ast`. + + b. Else it has trapped, hence let :math:`\X{result}` be :math:`\ERROR`. + +2. Return the new store paired with :math:`\X{result}`. + +.. math:: + ~ \\ + \begin{array}{lclll} + \F{func\_invoke}(S, a, v^\ast) &=& (S', {v'}^\ast) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; {v'}^\ast) \\ + \F{func\_invoke}(S, a, v^\ast) &=& (S', \ERROR) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \TRAP) \\ + \end{array} + +.. note:: + The store may be modified even in case of an error. + + +.. index:: table, table address, store, table instance, table type, element, function address +.. _embed-table: + +Tables +~~~~~~ + +.. _embed-table-alloc: + +:math:`\F{table\_alloc}(\store, \tabletype) : (\store, \tableaddr)` +................................................................... + +1. Pre-condition: :math:`\tabletype` is :math:`valid `. + +2. Let :math:`\tableaddr` be the result of :ref:`allocating a table ` in :math:`\store` with :ref:`table type ` :math:`\tabletype`. + +3. Return the new store paired with :math:`\tableaddr`. + +.. math:: + \begin{array}{lclll} + \F{table\_alloc}(S, \X{tt}) &=& (S', \X{a}) && (\iff \alloctable(S, \X{tt}) = S', \X{a}) \\ + \end{array} + + +.. _embed-table-type: + +:math:`\F{table\_type}(\store, \tableaddr) : \tabletype` +........................................................ + +1. Assert: the :ref:`external value ` :math:`\EVTABLE~\tableaddr` is :ref:`valid ` with :ref:`external type ` :math:`\ETTABLE~\tabletype`. + +2. Return :math:`\tabletype`. + +3. Post-condition: :math:`\tabletype` is :math:`valid `. + +.. math:: + \begin{array}{lclll} + \F{table\_type}(S, a) &=& \X{tt} && (\iff S \vdashexternval \EVTABLE~a : \ETTABLE~\X{tt}) \\ + \end{array} + + +.. _embed-table-read: + +:math:`\F{table\_read}(\store, \tableaddr, i:\u32) : \funcaddr^? ~|~ \error` +............................................................................ + +1. Let :math:`\X{ti}` be the :ref:`table instance ` :math:`\store.\STABLES[\tableaddr]`. + +2. If :math:`i` is larger than or equal to the length of :math:`\X{ti}.\TIELEM`, then return :math:`\ERROR`. + +3. Else, return :math:`\X{ti}.\TIELEM[i]`. + +.. math:: + \begin{array}{lclll} + \F{table\_read}(S, a, i) &=& \X{fa}^? && (\iff S.\STABLES[a].\TIELEM[i] = \X{fa}^?) \\ + \F{table\_read}(S, a, i) &=& \ERROR && (\otherwise) \\ + \end{array} + + +.. _embed-table-write: + +:math:`\F{table\_write}(\store, \tableaddr, i:\u32, \funcaddr^?) : \store ~|~ \error` +....................................................................................... + +1. Let :math:`\X{ti}` be the :ref:`table instance ` :math:`\store.\STABLES[\tableaddr]`. + +2. If :math:`i` is larger than or equal to the length of :math:`\X{ti}.\TIELEM`, then return :math:`\ERROR`. + +3. Replace :math:`\X{ti}.\TIELEM[i]` with the optional :ref:`function address ` :math:`\X{fa}^?`. + +4. Return the updated store. + +.. math:: + \begin{array}{lclll} + \F{table\_write}(S, a, i, \X{fa}^?) &=& S' && (\iff S' = S \with \STABLES[a].\TIELEM[i] = \X{fa}^?) \\ + \F{table\_write}(S, a, i, \X{fa}^?) &=& \ERROR && (\otherwise) \\ + \end{array} + + +.. _embed-table-size: + +:math:`\F{table\_size}(\store, \tableaddr) : \u32` +.................................................. + +1. Return the length of :math:`\store.\STABLES[\tableaddr].\TIELEM`. + +.. math:: + ~ \\ + \begin{array}{lclll} + \F{table\_size}(S, a) &=& n && + (\iff |S.\STABLES[a].\TIELEM| = n) \\ + \end{array} + + + +.. _embed-table-grow: + +:math:`\F{table\_grow}(\store, \tableaddr, n:\u32) : \store ~|~ \error` +....................................................................... + +1. Try :ref:`growing ` the :ref:`table instance ` :math:`\store.\STABLES[\tableaddr]` by :math:`n` elements: + + a. If it succeeds, return the updated store. + + b. Else, return :math:`\ERROR`. + +.. math:: + ~ \\ + \begin{array}{lclll} + \F{table\_grow}(S, a, n) &=& S' && + (\iff S' = S \with \STABLES[a] = \growtable(S.\STABLES[a], n)) \\ + \F{table\_grow}(S, a, n) &=& \ERROR && (\otherwise) \\ + \end{array} + + +.. index:: memory, memory address, store, memory instance, memory type, byte +.. _embed-mem: + +Memories +~~~~~~~~ + +.. _embed-mem-alloc: + +:math:`\F{mem\_alloc}(\store, \memtype) : (\store, \memaddr)` +................................................................ + +1. Pre-condition: :math:`\memtype` is :math:`valid `. + +2. Let :math:`\memaddr` be the result of :ref:`allocating a memory ` in :math:`\store` with :ref:`memory type ` :math:`\memtype`. + +3. Return the new store paired with :math:`\memaddr`. + +.. math:: + \begin{array}{lclll} + \F{mem\_alloc}(S, \X{mt}) &=& (S', \X{a}) && (\iff \allocmem(S, \X{mt}) = S', \X{a}) \\ + \end{array} + + +.. _embed-mem-type: + +:math:`\F{mem\_type}(\store, \memaddr) : \memtype` +.................................................. + +1. Assert: the :ref:`external value ` :math:`\EVMEM~\memaddr` is :ref:`valid ` with :ref:`external type ` :math:`\ETMEM~\memtype`. + +2. Return :math:`\memtype`. + +3. Post-condition: :math:`\memtype` is :math:`valid `. + +.. math:: + \begin{array}{lclll} + \F{mem\_type}(S, a) &=& \X{mt} && (\iff S \vdashexternval \EVMEM~a : \ETMEM~\X{mt}) \\ + \end{array} + + +.. _embed-mem-read: + +:math:`\F{mem\_read}(\store, \memaddr, i:\u32) : \byte ~|~ \error` +.................................................................. + +1. Let :math:`\X{mi}` be the :ref:`memory instance ` :math:`\store.\SMEMS[\memaddr]`. + +2. If :math:`i` is larger than or equal to the length of :math:`\X{mi}.\MIDATA`, then return :math:`\ERROR`. + +3. Else, return the :ref:`byte ` :math:`\X{mi}.\MIDATA[i]`. + +.. math:: + \begin{array}{lclll} + \F{mem\_read}(S, a, i) &=& b && (\iff S.\SMEMS[a].\MIDATA[i] = b) \\ + \F{mem\_read}(S, a, i) &=& \ERROR && (\otherwise) \\ + \end{array} + + +.. _embed-mem-write: + +:math:`\F{mem\_write}(\store, \memaddr, i:\u32, \byte) : \store ~|~ \error` +........................................................................... + +1. Let :math:`\X{mi}` be the :ref:`memory instance ` :math:`\store.\SMEMS[\memaddr]`. + +2. If :math:`\u32` is larger than or equal to the length of :math:`\X{mi}.\MIDATA`, then return :math:`\ERROR`. + +3. Replace :math:`\X{mi}.\MIDATA[i]` with :math:`\byte`. + +4. Return the updated store. + +.. math:: + \begin{array}{lclll} + \F{mem\_write}(S, a, i, b) &=& S' && (\iff S' = S \with \SMEMS[a].\MIDATA[i] = b) \\ + \F{mem\_write}(S, a, i, b) &=& \ERROR && (\otherwise) \\ + \end{array} + + +.. _embed-mem-size: + +:math:`\F{mem\_size}(\store, \memaddr) : \u32` +.............................................. + +1. Return the length of :math:`\store.\SMEMS[\memaddr].\MIDATA` divided by the :ref:`page size `. + +.. math:: + ~ \\ + \begin{array}{lclll} + \F{mem\_size}(S, a) &=& n && + (\iff |S.\SMEMS[a].\MIDATA| = n \cdot 64\,\F{Ki}) \\ + \end{array} + + + +.. _embed-mem-grow: + +:math:`\F{mem\_grow}(\store, \memaddr, n:\u32) : \store ~|~ \error` +................................................................... + +1. Try :ref:`growing ` the :ref:`memory instance ` :math:`\store.\SMEMS[\memaddr]` by :math:`n` :ref:`pages `: + + a. If it succeeds, return the updated store. + + b. Else, return :math:`\ERROR`. + +.. math:: + ~ \\ + \begin{array}{lclll} + \F{mem\_grow}(S, a, n) &=& S' && + (\iff S' = S \with \SMEMS[a] = \growmem(S.\SMEMS[a], n)) \\ + \F{mem\_grow}(S, a, n) &=& \ERROR && (\otherwise) \\ + \end{array} + + + +.. index:: global, global address, store, global instance, global type, value +.. _embed-global: + +Globals +~~~~~~~ + +.. _embed-global-alloc: + +:math:`\F{global\_alloc}(\store, \globaltype, \val) : (\store, \globaladdr)` +............................................................................ + +1. Pre-condition: :math:`\globaltype` is :math:`valid `. + +2. Let :math:`\globaladdr` be the result of :ref:`allocating a global ` in :math:`\store` with :ref:`global type ` :math:`\globaltype` and initialization value :math:`\val`. + +3. Return the new store paired with :math:`\globaladdr`. + +.. math:: + \begin{array}{lclll} + \F{global\_alloc}(S, \X{gt}, v) &=& (S', \X{a}) && (\iff \allocglobal(S, \X{gt}, v) = S', \X{a}) \\ + \end{array} + + +.. _embed-global-type: + +:math:`\F{global\_type}(\store, \globaladdr) : \globaltype` +........................................................... + +1. Assert: the :ref:`external value ` :math:`\EVGLOBAL~\globaladdr` is :ref:`valid ` with :ref:`external type ` :math:`\ETGLOBAL~\globaltype`. + +2. Return :math:`\globaltype`. + +3. Post-condition: :math:`\globaltype` is :math:`valid `. + +.. math:: + \begin{array}{lclll} + \F{global\_type}(S, a) &=& \X{gt} && (\iff S \vdashexternval \EVGLOBAL~a : \ETGLOBAL~\X{gt}) \\ + \end{array} + + +.. _embed-global-read: + +:math:`\F{global\_read}(\store, \globaladdr) : \val` +.................................................... + +1. Let :math:`\X{gi}` be the :ref:`global instance ` :math:`\store.\SGLOBALS[\globaladdr]`. + +2. Return the :ref:`value ` :math:`\X{gi}.\GIVALUE`. + +.. math:: + \begin{array}{lclll} + \F{global\_read}(S, a) &=& v && (\iff S.\SGLOBALS[a].\GIVALUE = v) \\ + \end{array} + + +.. _embed-global-write: + +:math:`\F{global\_write}(\store, \globaladdr, \val) : \store ~|~ \error` +........................................................................ + +1. Let :math:`\X{gi}` be the :ref:`global instance ` :math:`\store.\SGLOBALS[\globaladdr]`. + +2. If :math:`\X{gi}.\GIMUT` is not :math:`\MVAR`, then return :math:`\ERROR`. + +3. Replace :math:`\X{gi}.\GIVALUE` with the :ref:`value ` :math:`\val`. + +4. Return the updated store. + +.. math:: + ~ \\ + \begin{array}{lclll} + \F{global\_write}(S, a, v) &=& S' && (\iff S.\SGLOBALS[a].\GIMUT = \MVAR \wedge S' = S \with \SGLOBALS[a].\GIVALUE = v) \\ + \F{global\_write}(S, a, v) &=& \ERROR && (\otherwise) \\ + \end{array} diff --git a/document/core/appendix/implementation.rst b/document/core/appendix/implementation.rst new file mode 100644 index 00000000..df2885cc --- /dev/null +++ b/document/core/appendix/implementation.rst @@ -0,0 +1,137 @@ +.. index:: ! implementation limitations, implementation +.. _impl: + +Implementation Limitations +-------------------------- + +Implementations typically impose additional restrictions on a number of aspects of a WebAssembly module or execution. +These may stem from: + +* physical resource limits, +* constraints imposed by the embedder or its environment, +* limitations of selected implementation strategies. + +This section lists allowed limitations. +Where restrictions take the form of numeric limits, no minimum requirements are given, +nor are the limits assumed to be concrete, fixed numbers. +However, it is expected that all implementations have "reasonably" large limits to enable common applications. + +.. note:: + A conforming implementation is not allowed to leave out individual *features*. + However, designated subsets of WebAssembly may be specified in the future. + + +Syntactic Limits +~~~~~~~~~~~~~~~~ + +.. index:: abstract syntax, module, type, function, table, memory, global, element, data, import, export, parameter, result, local, structured control instruction, instruction, name, Unicode, character +.. _impl-syntax: + +Structure +......... + +An implementation may impose restrictions on the following dimensions of a module: + +* the number of :ref:`types ` in a :ref:`module ` +* the number of :ref:`functions ` in a :ref:`module `, including imports +* the number of :ref:`tables ` in a :ref:`module `, including imports +* the number of :ref:`memories ` in a :ref:`module `, including imports +* the number of :ref:`globals ` in a :ref:`module `, including imports +* the number of :ref:`element segments ` in a :ref:`module ` +* the number of :ref:`data segments ` in a :ref:`module ` +* the number of :ref:`imports ` to a :ref:`module ` +* the number of :ref:`exports ` from a :ref:`module ` +* the number of parameters in a :ref:`function type ` +* the number of results in a :ref:`function type ` +* the number of :ref:`locals ` in a :ref:`function ` +* the size of a :ref:`function ` body +* the size of a :ref:`structured control instruction ` +* the number of :ref:`structured control instructions ` in a :ref:`function ` +* the nesting depth of :ref:`structured control instructions ` +* the number of :ref:`label indices ` in a |brtable| instruction +* the length of an :ref:`element segment ` +* the length of a :ref:`data segment ` +* the length of a :ref:`name ` +* the range of :ref:`characters ` in a :ref:`name ` + +If the limits of an implementation are exceeded for a given module, +then the implementation may reject the :ref:`validation `, compilation, or :ref:`instantiation ` of that module with an embedder-specific error. + +.. note:: + The last item allows :ref:`embedders ` that operate in limited environments without support for + |Unicode|_ to limit the + names of :ref:`imports ` and :ref:`exports ` + to common subsets like |ASCII|_. + + +.. index:: binary format, module, section, function, code +.. _impl-binary: + +Binary Format +............. + +For a module given in :ref:`binary format `, additional limitations may be imposed on the following dimensions: + +* the size of a :ref:`module ` +* the size of any :ref:`section ` +* the size of an individual function's :ref:`code ` +* the number of :ref:`sections ` + + +.. index:: text format, source text, token, identifier, character, unicode +.. _impl-text: + +Text Format +........... + +For a module given in :ref:`text format `, additional limitations may be imposed on the following dimensions: + +* the size of the :ref:`source text ` +* the size of any syntactic element +* the size of an individual :ref:`token ` +* the nesting depth of :ref:`folded instructions ` +* the length of symbolic :ref:`identifiers ` +* the range of literal :ref:`characters ` allowed in the :ref:`source text ` + + +.. index:: validation, function +.. _impl-valid: + +Validation +~~~~~~~~~~ + +An implementation may defer :ref:`validation ` of individual :ref:`functions ` until they are first :ref:`invoked `. + +If a function turns out to be invalid, then the invocation, and every consecutive call to the same function, results in a :ref:`trap `. + +.. note:: + This is to allow implementations to use interpretation or just-in-time compilation for functions. + The function must still be fully validated before execution of its body begins. + + +.. index:: execution, module instance, function instance, table instance, memory instance, global instance, allocation, frame, label, value +.. _impl-exec: + +Execution +~~~~~~~~~ + +Restrictions on the following dimensions may be imposed during :ref:`execution ` of a WebAssembly program: + +* the number of allocated :ref:`module instances ` +* the number of allocated :ref:`function instances ` +* the number of allocated :ref:`table instances ` +* the number of allocated :ref:`memory instances ` +* the number of allocated :ref:`global instances ` +* the size of a :ref:`table instance ` +* the size of a :ref:`memory instance ` +* the number of :ref:`frames ` on the :ref:`stack ` +* the number of :ref:`labels ` on the :ref:`stack ` +* the number of :ref:`values ` on the :ref:`stack ` + +If the runtime limits of an implementation are exceeded during execution of a computation, +then it may terminate that computation and report an embedder-specific error to the invoking code. + +Some of the above limits may already be verified during instantiation, in which case an implementation may report exceedance in the same manner as for :ref:`syntactic limits `. + +.. note:: + Concrete limits are usually not fixed but may be dependent on specifics, interdependent, vary over time, or depend on other implementation- or embedder-specific situations or events. diff --git a/document/core/appendix/index-instructions.rst b/document/core/appendix/index-instructions.rst new file mode 100644 index 00000000..788915a9 --- /dev/null +++ b/document/core/appendix/index-instructions.rst @@ -0,0 +1,202 @@ +.. index:: instruction +.. _index-instr: + +Index of Instructions +--------------------- + +====================================== ================ ========================================== ======================================== =============================================================== +Instruction Binary Opcode Type Validation Execution +====================================== ================ ========================================== ======================================== =============================================================== +:math:`\UNREACHABLE` :math:`\hex{00}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\NOP` :math:`\hex{01}` :math:`[] \to []` :ref:`validation ` :ref:`execution ` +:math:`\BLOCK~[t^?]` :math:`\hex{02}` :math:`[] \to [t^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\LOOP~[t^?]` :math:`\hex{03}` :math:`[] \to [t^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\IF~[t^?]` :math:`\hex{04}` :math:`[\I32] \to [t^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\ELSE` :math:`\hex{05}` +(reserved) :math:`\hex{06}` +(reserved) :math:`\hex{07}` +(reserved) :math:`\hex{08}` +(reserved) :math:`\hex{09}` +(reserved) :math:`\hex{0A}` +:math:`\END` :math:`\hex{0B}` +:math:`\BR~l` :math:`\hex{0C}` :math:`[t_1^\ast~t^?] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\BRIF~l` :math:`\hex{0D}` :math:`[t^?~\I32] \to [t^?]` :ref:`validation ` :ref:`execution ` +:math:`\BRTABLE~l^\ast~l` :math:`\hex{0E}` :math:`[t_1^\ast~t^?~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\RETURN` :math:`\hex{0F}` :math:`[t_1^\ast~t^?] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\CALL~x` :math:`\hex{10}` :math:`[t_1^\ast] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +:math:`\CALLINDIRECT~x` :math:`\hex{11}` :math:`[t_1^\ast~\I32] \to [t_2^\ast]` :ref:`validation ` :ref:`execution ` +(reserved) :math:`\hex{12}` +(reserved) :math:`\hex{13}` +(reserved) :math:`\hex{14}` +(reserved) :math:`\hex{15}` +(reserved) :math:`\hex{16}` +(reserved) :math:`\hex{17}` +(reserved) :math:`\hex{18}` +(reserved) :math:`\hex{19}` +:math:`\DROP` :math:`\hex{1A}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` +:math:`\SELECT` :math:`\hex{1B}` :math:`[t~t~\I32] \to [t]` :ref:`validation ` :ref:`execution ` +(reserved) :math:`\hex{1C}` +(reserved) :math:`\hex{1D}` +(reserved) :math:`\hex{1E}` +(reserved) :math:`\hex{1F}` +:math:`\LOCALGET~x` :math:`\hex{20}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\LOCALSET~x` :math:`\hex{21}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` +:math:`\LOCALTEE~x` :math:`\hex{22}` :math:`[t] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\GLOBALGET~x` :math:`\hex{23}` :math:`[] \to [t]` :ref:`validation ` :ref:`execution ` +:math:`\GLOBALSET~x` :math:`\hex{24}` :math:`[t] \to []` :ref:`validation ` :ref:`execution ` +(reserved) :math:`\hex{25}` +(reserved) :math:`\hex{26}` +(reserved) :math:`\hex{27}` +:math:`\I32.\LOAD~\memarg` :math:`\hex{28}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD~\memarg` :math:`\hex{29}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\F32.\LOAD~\memarg` :math:`\hex{2A}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution ` +:math:`\F64.\LOAD~\memarg` :math:`\hex{2B}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\LOAD\K{8\_s}~\memarg` :math:`\hex{2C}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\LOAD\K{8\_u}~\memarg` :math:`\hex{2D}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\LOAD\K{16\_s}~\memarg` :math:`\hex{2E}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\LOAD\K{16\_u}~\memarg` :math:`\hex{2F}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{8\_s}~\memarg` :math:`\hex{30}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{8\_u}~\memarg` :math:`\hex{31}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{16\_s}~\memarg` :math:`\hex{32}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{16\_u}~\memarg` :math:`\hex{33}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{32\_s}~\memarg` :math:`\hex{34}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\LOAD\K{32\_u}~\memarg` :math:`\hex{35}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\STORE~\memarg` :math:`\hex{36}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I64.\STORE~\memarg` :math:`\hex{37}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` +:math:`\F32.\STORE~\memarg` :math:`\hex{38}` :math:`[\I32~\F32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\F64.\STORE~\memarg` :math:`\hex{39}` :math:`[\I32~\F64] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I32.\STORE\K{8}~\memarg` :math:`\hex{3A}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I32.\STORE\K{16}~\memarg` :math:`\hex{3B}` :math:`[\I32~\I32] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I64.\STORE\K{8}~\memarg` :math:`\hex{3C}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I64.\STORE\K{16}~\memarg` :math:`\hex{3D}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` +:math:`\I64.\STORE\K{32}~\memarg` :math:`\hex{3E}` :math:`[\I32~\I64] \to []` :ref:`validation ` :ref:`execution ` +:math:`\MEMORYSIZE` :math:`\hex{3F}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\MEMORYGROW` :math:`\hex{40}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\CONST~\i32` :math:`\hex{41}` :math:`[] \to [\I32]` :ref:`validation ` :ref:`execution ` +:math:`\I64.\CONST~\i64` :math:`\hex{42}` :math:`[] \to [\I64]` :ref:`validation ` :ref:`execution ` +:math:`\F32.\CONST~\f32` :math:`\hex{43}` :math:`[] \to [\F32]` :ref:`validation ` :ref:`execution ` +:math:`\F64.\CONST~\f64` :math:`\hex{44}` :math:`[] \to [\F64]` :ref:`validation ` :ref:`execution ` +:math:`\I32.\EQZ` :math:`\hex{45}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\EQ` :math:`\hex{46}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\NE` :math:`\hex{47}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\LT\K{\_s}` :math:`\hex{48}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\LT\K{\_u}` :math:`\hex{49}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\GT\K{\_s}` :math:`\hex{4A}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\GT\K{\_u}` :math:`\hex{4B}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\LE\K{\_s}` :math:`\hex{4C}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\LE\K{\_u}` :math:`\hex{4D}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\GE\K{\_s}` :math:`\hex{4E}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\GE\K{\_u}` :math:`\hex{4F}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EQZ` :math:`\hex{50}` :math:`[\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EQ` :math:`\hex{51}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\NE` :math:`\hex{52}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\LT\K{\_s}` :math:`\hex{53}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\LT\K{\_u}` :math:`\hex{54}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\GT\K{\_s}` :math:`\hex{55}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\GT\K{\_u}` :math:`\hex{56}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\LE\K{\_s}` :math:`\hex{57}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\LE\K{\_u}` :math:`\hex{58}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\GE\K{\_s}` :math:`\hex{59}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\GE\K{\_u}` :math:`\hex{5A}` :math:`[\I64~\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\EQ` :math:`\hex{5B}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\NE` :math:`\hex{5C}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\LT` :math:`\hex{5D}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\GT` :math:`\hex{5E}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\LE` :math:`\hex{5F}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\GE` :math:`\hex{60}` :math:`[\F32~\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\EQ` :math:`\hex{61}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\NE` :math:`\hex{62}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\LT` :math:`\hex{63}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\GT` :math:`\hex{64}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\LE` :math:`\hex{65}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\GE` :math:`\hex{66}` :math:`[\F64~\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\CLZ` :math:`\hex{67}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\CTZ` :math:`\hex{68}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\POPCNT` :math:`\hex{69}` :math:`[\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\ADD` :math:`\hex{6A}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\SUB` :math:`\hex{6B}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\MUL` :math:`\hex{6C}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\DIV\K{\_s}` :math:`\hex{6D}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\DIV\K{\_u}` :math:`\hex{6E}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\REM\K{\_s}` :math:`\hex{6F}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\REM\K{\_u}` :math:`\hex{70}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\AND` :math:`\hex{71}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\OR` :math:`\hex{72}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\XOR` :math:`\hex{73}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\SHL` :math:`\hex{74}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\SHR\K{\_s}` :math:`\hex{75}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\SHR\K{\_u}` :math:`\hex{76}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\ROTL` :math:`\hex{77}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\ROTR` :math:`\hex{78}` :math:`[\I32~\I32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\CLZ` :math:`\hex{79}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\CTZ` :math:`\hex{7A}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\POPCNT` :math:`\hex{7B}` :math:`[\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\ADD` :math:`\hex{7C}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\SUB` :math:`\hex{7D}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\MUL` :math:`\hex{7E}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\DIV\K{\_s}` :math:`\hex{7F}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\DIV\K{\_u}` :math:`\hex{80}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\REM\K{\_s}` :math:`\hex{81}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\REM\K{\_u}` :math:`\hex{82}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\AND` :math:`\hex{83}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\OR` :math:`\hex{84}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\XOR` :math:`\hex{85}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\SHL` :math:`\hex{86}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\SHR\K{\_s}` :math:`\hex{87}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\SHR\K{\_u}` :math:`\hex{88}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\ROTL` :math:`\hex{89}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\ROTR` :math:`\hex{8A}` :math:`[\I64~\I64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\ABS` :math:`\hex{8B}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\NEG` :math:`\hex{8C}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CEIL` :math:`\hex{8D}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\FLOOR` :math:`\hex{8E}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\TRUNC` :math:`\hex{8F}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\NEAREST` :math:`\hex{90}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\SQRT` :math:`\hex{91}` :math:`[\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\ADD` :math:`\hex{92}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\SUB` :math:`\hex{93}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\MUL` :math:`\hex{94}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\DIV` :math:`\hex{95}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\FMIN` :math:`\hex{96}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\FMAX` :math:`\hex{97}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\COPYSIGN` :math:`\hex{98}` :math:`[\F32~\F32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\ABS` :math:`\hex{99}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\NEG` :math:`\hex{9A}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CEIL` :math:`\hex{9B}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\FLOOR` :math:`\hex{9C}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\TRUNC` :math:`\hex{9D}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\NEAREST` :math:`\hex{9E}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\SQRT` :math:`\hex{9F}` :math:`[\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\ADD` :math:`\hex{A0}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\SUB` :math:`\hex{A1}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\MUL` :math:`\hex{A2}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\DIV` :math:`\hex{A3}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\FMIN` :math:`\hex{A4}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\FMAX` :math:`\hex{A5}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\COPYSIGN` :math:`\hex{A6}` :math:`[\F64~\F64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\WRAP\K{\_}\I64` :math:`\hex{A7}` :math:`[\I64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_}\F32\K{\_s}` :math:`\hex{A8}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_}\F32\K{\_u}` :math:`\hex{A9}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_}\F64\K{\_s}` :math:`\hex{AA}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\TRUNC\K{\_}\F64\K{\_u}` :math:`\hex{AB}` :math:`[\F64] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EXTEND\K{\_}\I32\K{\_s}` :math:`\hex{AC}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\EXTEND\K{\_}\I32\K{\_u}` :math:`\hex{AD}` :math:`[\I32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_}\F32\K{\_s}` :math:`\hex{AE}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_}\F32\K{\_u}` :math:`\hex{AF}` :math:`[\F32] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_}\F64\K{\_s}` :math:`\hex{B0}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\TRUNC\K{\_}\F64\K{\_u}` :math:`\hex{B1}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_}\I32\K{\_s}` :math:`\hex{B2}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_}\I32\K{\_u}` :math:`\hex{B3}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_}\I64\K{\_s}` :math:`\hex{B4}` :math:`[\I64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\CONVERT\K{\_}\I64\K{\_u}` :math:`\hex{B5}` :math:`[\I64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\DEMOTE\K{\_}\F64` :math:`\hex{B6}` :math:`[\F64] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CONVERT\K{\_}\I32\K{\_s}` :math:`\hex{B7}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CONVERT\K{\_}\I32\K{\_u}` :math:`\hex{B8}` :math:`[\I32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CONVERT\K{\_}\I64\K{\_s}` :math:`\hex{B9}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\CONVERT\K{\_}\I64\K{\_u}` :math:`\hex{BA}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\PROMOTE\K{\_}\F32` :math:`\hex{BB}` :math:`[\F32] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I32.\REINTERPRET\K{\_}\F32` :math:`\hex{BC}` :math:`[\F32] \to [\I32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\I64.\REINTERPRET\K{\_}\F64` :math:`\hex{BD}` :math:`[\F64] \to [\I64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F32.\REINTERPRET\K{\_}\I32` :math:`\hex{BE}` :math:`[\I32] \to [\F32]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +:math:`\F64.\REINTERPRET\K{\_}\I64` :math:`\hex{BF}` :math:`[\I64] \to [\F64]` :ref:`validation ` :ref:`execution `, :ref:`operator ` +====================================== ================ ========================================== ======================================== =============================================================== diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst new file mode 100644 index 00000000..4d610e09 --- /dev/null +++ b/document/core/appendix/index-rules.rst @@ -0,0 +1,108 @@ +.. _index-rules: + +Index of Semantic Rules +----------------------- + + +.. index:: validation +.. _index-valid: + +Typing of Static Constructs +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +=============================================== =============================================================================== +Construct Judgement +=============================================== =============================================================================== +:ref:`Limits ` :math:`\vdashlimits \limits : k` +:ref:`Function type ` :math:`\vdashfunctype \functype \ok` +:ref:`Table type ` :math:`\vdashtabletype \tabletype \ok` +:ref:`Memory type ` :math:`\vdashmemtype \memtype \ok` +:ref:`Global type ` :math:`\vdashglobaltype \globaltype \ok` +:ref:`External type ` :math:`\vdashexterntype \externtype \ok` +:ref:`Instruction ` :math:`S;C \vdashinstr \instr : \functype` +:ref:`Instruction sequence ` :math:`S;C \vdashinstrseq \instr^\ast : \functype` +:ref:`Expression ` :math:`C \vdashexpr \expr : \resulttype` +:ref:`Function ` :math:`C \vdashfunc \func : \functype` +:ref:`Table ` :math:`C \vdashtable \table : \tabletype` +:ref:`Memory ` :math:`C \vdashmem \mem : \memtype` +:ref:`Global ` :math:`C \vdashglobal \global : \globaltype` +:ref:`Element segment ` :math:`C \vdashelem \elem \ok` +:ref:`Data segment ` :math:`C \vdashdata \data \ok` +:ref:`Start function ` :math:`C \vdashstart \start \ok` +:ref:`Export ` :math:`C \vdashexport \export : \externtype` +:ref:`Export description ` :math:`C \vdashexportdesc \exportdesc : \externtype` +:ref:`Import ` :math:`C \vdashimport \import : \externtype` +:ref:`Import description ` :math:`C \vdashimportdesc \importdesc : \externtype` +:ref:`Module ` :math:`\vdashmodule \module : \externtype^\ast \to \externtype^\ast` +=============================================== =============================================================================== + + +.. index:: runtime + +Typing of Runtime Constructs +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +=============================================== =============================================================================== +Construct Judgement +=============================================== =============================================================================== +:ref:`Value ` :math:`\vdashval \val : \valtype` +:ref:`Result ` :math:`\vdashresult \result : \resulttype` +:ref:`External value ` :math:`S \vdashexternval \externval : \externtype` +:ref:`Function instance ` :math:`S \vdashfuncinst \funcinst : \functype` +:ref:`Table instance ` :math:`S \vdashtableinst \tableinst : \tabletype` +:ref:`Memory instance ` :math:`S \vdashmeminst \meminst : \memtype` +:ref:`Global instance ` :math:`S \vdashglobalinst \globalinst : \globaltype` +:ref:`Export instance ` :math:`S \vdashexportinst \exportinst \ok` +:ref:`Module instance ` :math:`S \vdashmoduleinst \moduleinst : C` +:ref:`Store ` :math:`\vdashstore \store \ok` +:ref:`Configuration ` :math:`\vdashconfig \config \ok` +:ref:`Thread ` :math:`S;\resulttype^? \vdashthread \thread : \resulttype` +:ref:`Frame ` :math:`S \vdashframe \frame : C` +=============================================== =============================================================================== + + +Constantness +~~~~~~~~~~~~ + +=============================================== =============================================================================== +Construct Judgement +=============================================== =============================================================================== +:ref:`Constant expression ` :math:`C \vdashexprconst \expr \const` +:ref:`Constant instruction ` :math:`C \vdashinstrconst \instr \const` +=============================================== =============================================================================== + + +Import Matching +~~~~~~~~~~~~~~~ + +=============================================== =============================================================================== +Construct Judgement +=============================================== =============================================================================== +:ref:`Limits ` :math:`\vdashlimitsmatch \limits_1 \matches \limits_2` +:ref:`External type ` :math:`\vdashexterntypematch \externtype_1 \matches \externtype_2` +=============================================== =============================================================================== + + +Store Extension +~~~~~~~~~~~~~~~ + +=============================================== =============================================================================== +Construct Judgement +=============================================== =============================================================================== +:ref:`Function instance ` :math:`\vdashfuncinstextends \funcinst_1 \extendsto \funcinst_2` +:ref:`Table instance ` :math:`\vdashtableinstextends \tableinst_1 \extendsto \tableinst_2` +:ref:`Memory instance ` :math:`\vdashmeminstextends \meminst_1 \extendsto \meminst_2` +:ref:`Global instance ` :math:`\vdashglobalinstextends \globalinst_1 \extendsto \globalinst_2` +:ref:`Store ` :math:`\vdashstoreextends \store_1 \extendsto \store_2` +=============================================== =============================================================================== + + +Execution +~~~~~~~~~ + +=============================================== =============================================================================== +Construct Judgement +=============================================== =============================================================================== +:ref:`Instruction ` :math:`S;F;\instr^\ast \stepto S';F';{\instr'}^\ast` +:ref:`Expression ` :math:`S;F;\expr \stepto S';F';\expr'` +=============================================== =============================================================================== diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst new file mode 100644 index 00000000..55787782 --- /dev/null +++ b/document/core/appendix/index-types.rst @@ -0,0 +1,24 @@ +.. index:: type +.. _index-type: + +Index of Types +-------------- + +======================================== =========================================== =============================================================================== +Category Constructor Binary Opcode +======================================== =========================================== =============================================================================== +:ref:`Type index ` :math:`x` (positive number as |Bs32| or |Bu32|) +:ref:`Value type ` |I32| :math:`\hex{7F}` (-1 as |Bs7|) +:ref:`Value type ` |I64| :math:`\hex{7E}` (-2 as |Bs7|) +:ref:`Value type ` |F32| :math:`\hex{7D}` (-3 as |Bs7|) +:ref:`Value type ` |F64| :math:`\hex{7C}` (-4 as |Bs7|) +(reserved) :math:`\hex{7B}` .. :math:`\hex{71}` +:ref:`Element type ` |FUNCREF| :math:`\hex{70}` (-16 as |Bs7|) +(reserved) :math:`\hex{6F}` .. :math:`\hex{61}` +:ref:`Function type ` :math:`[\valtype^\ast] \to [\valtype^\ast]` :math:`\hex{60}` (-32 as |Bs7|) +(reserved) :math:`\hex{5F}` .. :math:`\hex{41}` +:ref:`Result type ` :math:`[\epsilon]` :math:`\hex{40}` (-64 as |Bs7|) +:ref:`Table type ` :math:`\limits~\elemtype` (none) +:ref:`Memory type ` :math:`\limits` (none) +:ref:`Global type ` :math:`\mut~\valtype` (none) +======================================== =========================================== =============================================================================== diff --git a/document/core/appendix/index.rst b/document/core/appendix/index.rst new file mode 100644 index 00000000..789d2140 --- /dev/null +++ b/document/core/appendix/index.rst @@ -0,0 +1,22 @@ +.. _appendix: + +Appendix +======== + +.. toctree:: + :maxdepth: 2 + + embedding + implementation + algorithm + custom + properties + +.. only:: singlehtml + + .. toctree:: + + index-types + index-instructions + index-rules + diff --git a/document/core/appendix/properties.rst b/document/core/appendix/properties.rst new file mode 100644 index 00000000..330f42dc --- /dev/null +++ b/document/core/appendix/properties.rst @@ -0,0 +1,752 @@ +.. index:: ! soundness, type system +.. _soundness: + +Soundness +--------- + +The :ref:`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 ` or :ref:`global ` variable will only contain type-correct values, every :ref:`instruction ` will only be applied to operands of the expected type, and every :ref:`function ` :ref:`invocation ` always evaluates to a result of the right type (if it does not :ref:`trap ` or diverge). + +* No memory location will be read or written except those explicitly defined by the program, i.e., as a :ref:`local `, a :ref:`global `, an element in a :ref:`table `, or a location within a linear :ref:`memory `. + +* There is no undefined behavior, + i.e., the :ref:`execution rules ` cover all possible cases that can occur in a :ref:`valid ` program, and the rules are mutually consistent. + +Soundness also is instrumental in ensuring additional properties, most notably, *encapsulation* of function and module scopes: no :ref:`locals ` can be accessed outside their own function and no :ref:`module ` components can be accessed outside their own module unless they are explicitly :ref:`exported ` or :ref:`imported `. + +The typing rules defining WebAssembly :ref:`validation ` only cover the *static* components of a WebAssembly program. +In order to state and prove soundness precisely, the typing rules must be extended to the *dynamic* components of the abstract :ref:`runtime `, that is, the :ref:`store `, :ref:`configurations `, and :ref:`administrative instructions `. [#cite-pldi2017]_ + + +.. index:: value, value type, result, result type, trap +.. _valid-val: +.. _valid-result: + +Values and Results +~~~~~~~~~~~~~~~~~~ + +:ref:`Values ` and :ref:`results ` can be classified by :ref:`value types ` and :ref:`result types ` as follows. + +:ref:`Values ` :math:`t.\CONST~c` +............................................. + +* The value is valid with :ref:`value type ` :math:`t`. + +.. math:: + \frac{ + }{ + \vdashval t.\CONST~c : t + } + + +:ref:`Results ` :math:`\val^\ast` +................................................ + +* For each :ref:`value ` :math:`\val_i` in :math:`\val^\ast`: + + * The value :math:`\val_i` is :ref:`valid ` with some :ref:`value type ` :math:`t_i`. + +* Let :math:`t^\ast` be the concatenation of all :math:`t_i`. + +* Then the result is valid with :ref:`result type ` :math:`[t^\ast]`. + +.. math:: + \frac{ + (\vdashval \val : t)^\ast + }{ + \vdashresult \val^\ast : [t^\ast] + } + + +:ref:`Results ` :math:`\TRAP` +............................................ + +* The result is valid with :ref:`result type ` :math:`[t^\ast]`, for any sequence :math:`t^\ast` of :ref:`value types `. + +.. math:: + \frac{ + }{ + \vdashresult \TRAP : [t^\ast] + } + + +.. _module-context: +.. _valid-store: + +Store Validity +~~~~~~~~~~~~~~ + +The following typing rules specify when a runtime :ref:`store ` :math:`S` is *valid*. +A valid store must consist of +:ref:`function `, :ref:`table `, :ref:`memory `, :ref:`global `, and :ref:`module ` instances that are themselves valid, relative to :math:`S`. + +To that end, each kind of instance is classified by a respective :ref:`function `, :ref:`table `, :ref:`memory `, or :ref:`global ` type. +Module instances are classified by *module contexts*, which are regular :ref:`contexts ` repurposed as module types describing the :ref:`index spaces ` defined by a module. + + + +.. index:: store, function instance, table instance, memory instance, global instance, function type, table type, memory type, global type + +:ref:`Store ` :math:`S` +..................................... + +* Each :ref:`function instance ` :math:`\funcinst_i` in :math:`S.\SFUNCS` must be :ref:`valid ` with some :ref:`function type ` :math:`\functype_i`. + +* Each :ref:`table instance ` :math:`\tableinst_i` in :math:`S.\STABLES` must be :ref:`valid ` with some :ref:`table type ` :math:`\tabletype_i`. + +* Each :ref:`memory instance ` :math:`\meminst_i` in :math:`S.\SMEMS` must be :ref:`valid ` with some :ref:`memory type ` :math:`\memtype_i`. + +* Each :ref:`global instance ` :math:`\globalinst_i` in :math:`S.\SGLOBALS` must be :ref:`valid ` with some :ref:`global type ` :math:`\globaltype_i`. + +* Then the store is valid. + +.. math:: + ~\\[-1ex] + \frac{ + \begin{array}{@{}c@{}} + (S \vdashfuncinst \funcinst : \functype)^\ast + \qquad + (S \vdashtableinst \tableinst : \tabletype)^\ast + \\ + (S \vdashmeminst \meminst : \memtype)^\ast + \qquad + (S \vdashglobalinst \globalinst : \globaltype)^\ast + \\ + S = \{ + \SFUNCS~\funcinst^\ast, + \STABLES~\tableinst^\ast, + \SMEMS~\meminst^\ast, + \SGLOBALS~\globalinst^\ast \} + \end{array} + }{ + \vdashstore S \ok + } + + +.. index:: function type, function instance +.. _valid-funcinst: + +:ref:`Function Instances ` :math:`\{\FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func\}` +....................................................................................................................... + +* The :ref:`function type ` :math:`\functype` must be :ref:`valid `. + +* The :ref:`module instance ` :math:`\moduleinst` must be :ref:`valid ` with some :ref:`context ` :math:`C`. + +* Under :ref:`context ` :math:`C`, the :ref:`function ` :math:`\func` must be :ref:`valid ` with :ref:`function type ` :math:`\functype`. + +* Then the function instance is valid with :ref:`function type ` :math:`\functype`. + +.. math:: + \frac{ + \vdashfunctype \functype \ok + \qquad + S \vdashmoduleinst \moduleinst : C + \qquad + C \vdashfunc \func : \functype + }{ + S \vdashfuncinst \{\FITYPE~\functype, \FIMODULE~\moduleinst, \FICODE~\func\} : \functype + } + + +.. index:: function type, function instance, host function +.. _valid-hostfuncinst: + +:ref:`Host Function Instances ` :math:`\{\FITYPE~\functype, \FIHOSTCODE~\X{hf}\}` +.................................................................................................. + +* The :ref:`function type ` :math:`\functype` must be :ref:`valid `. + +* Let :math:`[t_1^\ast] \to [t_2^\ast]` be the :ref:`function type ` :math:`\functype`. + +* For every :ref:`valid ` :ref:`store ` :math:`S_1` :ref:`extending ` :math:`S` and every sequence :math:`\val^\ast` of :ref:`values ` whose :ref:`types ` coincide with :math:`t_1^\ast`: + + * :ref:`Executing ` :math:`\X{hf}` in store :math:`S_1` with arguments :math:`\val^\ast` has a non-empty set of possible outcomes. + + * For every element :math:`R` of this set: + + * Either :math:`R` must be :math:`\bot` (i.e., divergence). + + * Or :math:`R` consists of a :ref:`valid ` :ref:`store ` :math:`S_2` :ref:`extending ` :math:`S_1` and a :ref:`result ` :math:`\result` whose :ref:`type ` coincides with :math:`[t_2^\ast]`. + +* Then the function instance is valid with :ref:`function type ` :math:`\functype`. + +.. math:: + \frac{ + \begin{array}[b]{@{}l@{}} + \vdashfunctype [t_1^\ast] \to [t_2^\ast] \ok \\ + \end{array} + \quad + \begin{array}[b]{@{}l@{}} + \forall S_1, \val^\ast,~ + {\vdashstore S_1 \ok} \wedge + {\vdashstoreextends S \extendsto S_1} \wedge + {\vdashresult \val^\ast : [t_1^\ast]} + \Longrightarrow {} \\ \qquad + \X{hf}(S_1; \val^\ast) \supset \emptyset \wedge {} \\ \qquad + \forall R \in \X{hf}(S_1; \val^\ast),~ + R = \bot \vee {} \\ \qquad\qquad + \exists S_2, \result,~ + {\vdashstore S_2 \ok} \wedge + {\vdashstoreextends S_1 \extendsto S_2} \wedge + {\vdashresult \result : [t_2^\ast]} \wedge + R = (S_2; \result) + \end{array} + }{ + S \vdashfuncinst \{\FITYPE~[t_1^\ast] \to [t_2^\ast], \FIHOSTCODE~\X{hf}\} : [t_1^\ast] \to [t_2^\ast] + } + +.. note:: + This rule states that, if appropriate pre-conditions about store and arguments are satisfied, then executing the host function must satisfy appropriate post-conditions about store and results. + The post-conditions match the ones in the :ref:`execution rule ` for invoking host functions. + + Any store under which the function is invoked is assumed to be an extension of the current store. + That way, the function itself is able to make sufficient assumptions about future stores. + + +.. index:: table type, table instance, limits, function address +.. _valid-tableinst: + +:ref:`Table Instances ` :math:`\{ \TIELEM~(\X{fa}^?)^n, \TIMAX~m^? \}` +.............................................................................................. + +* For each optional :ref:`function address ` :math:`\X{fa}^?_i` in the table elements :math:`(\X{fa}^?)^n`: + + * Either :math:`\X{fa}^?_i` is empty. + + * Or the :ref:`external value ` :math:`\EVFUNC~\X{fa}` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETFUNC~\X{ft}`. + +* The :ref:`limits ` :math:`\{\LMIN~n, \LMAX~m^?\}` must be :ref:`valid `. + +* Then the table instance is valid with :ref:`table type ` :math:`\{\LMIN~n, \LMAX~m^?\}~\FUNCREF`. + +.. math:: + \frac{ + ((S \vdash \EVFUNC~\X{fa} : \ETFUNC~\functype)^?)^n + \qquad + \vdashlimits \{\LMIN~n, \LMAX~m^?\} \ok + }{ + S \vdashtableinst \{ \TIELEM~(\X{fa}^?)^n, \TIMAX~m^? \} : \{\LMIN~n, \LMAX~m^?\}~\FUNCREF + } + + +.. index:: memory type, memory instance, limits, byte +.. _valid-meminst: + +:ref:`Memory Instances ` :math:`\{ \MIDATA~b^n, \MIMAX~m^? \}` +.............................................................................. + +* The :ref:`limits ` :math:`\{\LMIN~n, \LMAX~m^?\}` must be :ref:`valid `. + +* Then the memory instance is valid with :ref:`memory type ` :math:`\{\LMIN~n, \LMAX~m^?\}`. + +.. math:: + \frac{ + \vdashlimits \{\LMIN~n, \LMAX~m^?\} \ok + }{ + S \vdashmeminst \{ \MIDATA~b^n, \MIMAX~m^? \} : \{\LMIN~n, \LMAX~m^?\} + } + + +.. index:: global type, global instance, value, mutability +.. _valid-globalinst: + +:ref:`Global Instances ` :math:`\{ \GIVALUE~(t.\CONST~c), \GIMUT~\mut \}` +............................................................................................ + +* The global instance is valid with :ref:`global type ` :math:`\mut~t`. + +.. math:: + \frac{ + }{ + S \vdashglobalinst \{ \GIVALUE~(t.\CONST~c), \GIMUT~\mut \} : \mut~t + } + + +.. index:: external type, export instance, name, external value +.. _valid-exportinst: + +:ref:`Export Instances ` :math:`\{ \EINAME~\name, \EIVALUE~\externval \}` +....................................................................................................... + +* The :ref:`external value ` :math:`\externval` must be :ref:`valid ` with some :ref:`external type ` :math:`\externtype`. + +* Then the export instance is valid. + +.. math:: + \frac{ + S \vdashexternval \externval : \externtype + }{ + S \vdashexportinst \{ \EINAME~\name, \EIVALUE~\externval \} \ok + } + + +.. index:: module instance, context +.. _valid-moduleinst: + +:ref:`Module Instances ` :math:`\moduleinst` +............................................................... + +* Each :ref:`function type ` :math:`\functype_i` in :math:`\moduleinst.\MITYPES` must be :ref:`valid `. + +* For each :ref:`function address ` :math:`\funcaddr_i` in :math:`\moduleinst.\MIFUNCS`, the :ref:`external value ` :math:`\EVFUNC~\funcaddr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETFUNC~\functype'_i`. + +* For each :ref:`table address ` :math:`\tableaddr_i` in :math:`\moduleinst.\MITABLES`, the :ref:`external value ` :math:`\EVTABLE~\tableaddr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETTABLE~\tabletype_i`. + +* For each :ref:`memory address ` :math:`\memaddr_i` in :math:`\moduleinst.\MIMEMS`, the :ref:`external value ` :math:`\EVMEM~\memaddr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETMEM~\memtype_i`. + +* For each :ref:`global address ` :math:`\globaladdr_i` in :math:`\moduleinst.\MIGLOBALS`, the :ref:`external value ` :math:`\EVGLOBAL~\globaladdr_i` must be :ref:`valid ` with some :ref:`external type ` :math:`\ETGLOBAL~\globaltype_i`. + +* Each :ref:`export instance ` :math:`\exportinst_i` in :math:`\moduleinst.\MIEXPORTS` must be :ref:`valid `. + +* For each :ref:`export instance ` :math:`\exportinst_i` in :math:`\moduleinst.\MIEXPORTS`, the :ref:`name ` :math:`\exportinst_i.\EINAME` must be different from any other name occurring in :math:`\moduleinst.\MIEXPORTS`. + +* Let :math:`{\functype'}^\ast` be the concatenation of all :math:`\functype'_i` in order. + +* Let :math:`\tabletype^\ast` be the concatenation of all :math:`\tabletype_i` in order. + +* Let :math:`\memtype^\ast` be the concatenation of all :math:`\memtype_i` in order. + +* Let :math:`\globaltype^\ast` be the concatenation of all :math:`\globaltype_i` in order. + +* Then the module instance is valid with :ref:`context ` :math:`\{\CTYPES~\functype^\ast, \CFUNCS~{\functype'}^\ast, \CTABLES~\tabletype^\ast, \CMEMS~\memtype^\ast, \CGLOBALS~\globaltype^\ast\}`. + +.. math:: + ~\\[-1ex] + \frac{ + \begin{array}{@{}c@{}} + (\vdashfunctype \functype \ok)^\ast + \\ + (S \vdashexternval \EVFUNC~\funcaddr : \ETFUNC~\functype')^\ast + \qquad + (S \vdashexternval \EVTABLE~\tableaddr : \ETTABLE~\tabletype)^\ast + \\ + (S \vdashexternval \EVMEM~\memaddr : \ETMEM~\memtype)^\ast + \qquad + (S \vdashexternval \EVGLOBAL~\globaladdr : \ETGLOBAL~\globaltype)^\ast + \\ + (S \vdashexportinst \exportinst \ok)^\ast + \qquad + (\exportinst.\EINAME)^\ast ~\mbox{disjoint} + \end{array} + }{ + S \vdashmoduleinst \{ + \begin{array}[t]{@{}l@{~}l@{}} + \MITYPES & \functype^\ast, \\ + \MIFUNCS & \funcaddr^\ast, \\ + \MITABLES & \tableaddr^\ast, \\ + \MIMEMS & \memaddr^\ast, \\ + \MIGLOBALS & \globaladdr^\ast \\ + \MIEXPORTS & \exportinst^\ast ~\} : \{ + \begin{array}[t]{@{}l@{~}l@{}} + \CTYPES & \functype^\ast, \\ + \CFUNCS & {\functype'}^\ast, \\ + \CTABLES & \tabletype^\ast, \\ + \CMEMS & \memtype^\ast, \\ + \CGLOBALS & \globaltype^\ast ~\} + \end{array} + \end{array} + } + + +.. index:: configuration, administrative instruction, store, frame +.. _frame-context: +.. _valid-config: + +Configuration Validity +~~~~~~~~~~~~~~~~~~~~~~ + +To relate the WebAssembly :ref:`type system ` to its :ref:`execution semantics `, the :ref:`typing rules for instructions ` must be extended to :ref:`configurations ` :math:`S;T`, +which relates the :ref:`store ` to execution :ref:`threads `. + +Configurations and threads are classified by their :ref:`result type `. +In addition to the store :math:`S`, threads are typed under a *return type* :math:`\resulttype^?`, which controls whether and with which type a |return| instruction is allowed. +This type is absent (:math:`\epsilon`) except for instruction sequences inside an administrative |FRAME| instruction. + +Finally, :ref:`frames ` are classified with *frame contexts*, which extend the :ref:`module contexts ` of a frame's associated :ref:`module instance ` with the :ref:`locals ` that the frame contains. + + +.. index:: result type, thread + +:ref:`Configurations ` :math:`S;T` +................................................. + +* The :ref:`store ` :math:`S` must be :ref:`valid `. + +* Under no allowed return type, + the :ref:`thread ` :math:`T` must be :ref:`valid ` with some :ref:`result type ` :math:`[t^?]`. + +* Then the configuration is valid with the :ref:`result type ` :math:`[t^?]`. + +.. math:: + \frac{ + \vdashstore S \ok + \qquad + S; \epsilon \vdashthread T : [t^?] + }{ + \vdashconfig S; T : [t^?] + } + + +.. index:: thread, frame, instruction, result type, context +.. _valid-thread: + +:ref:`Threads ` :math:`F;\instr^\ast` +.................................................... + +* Let :math:`\resulttype^?` be the current allowed return type. + +* The :ref:`frame ` :math:`F` must be :ref:`valid ` with a :ref:`context ` :math:`C`. + +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with |CRETURN| set to :math:`\resulttype^?`. + +* Under context :math:`C'`, + the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with some type :math:`[] \to [t^?]`. + +* Then the thread is valid with the :ref:`result type ` :math:`[t^?]`. + +.. math:: + \frac{ + S \vdashframe F : C + \qquad + S; C,\CRETURN~\resulttype^? \vdashinstrseq \instr^\ast : [] \to [t^?] + }{ + S; \resulttype^? \vdashthread F; \instr^\ast : [t^?] + } + + +.. index:: frame, local, module instance, value, value type, context +.. _valid-frame: + +:ref:`Frames ` :math:`\{\ALOCALS~\val^\ast, \AMODULE~\moduleinst\}` +................................................................................. + +* The :ref:`module instance ` :math:`\moduleinst` must be :ref:`valid ` with some :ref:`module context ` :math:`C`. + +* Each :ref:`value ` :math:`\val_i` in :math:`\val^\ast` must be :ref:`valid ` with some :ref:`value type ` :math:`t_i`. + +* Let :math:`t^\ast` the concatenation of all :math:`t_i` in order. + +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`value types ` :math:`t^\ast` prepended to the |CLOCALS| vector. + +* Then the frame is valid with :ref:`frame context ` :math:`C'`. + +.. math:: + \frac{ + S \vdashmoduleinst \moduleinst : C + \qquad + (\vdashval \val : t)^\ast + }{ + S \vdashframe \{\ALOCALS~\val^\ast, \AMODULE~\moduleinst\} : (C, \CLOCALS~t^\ast) + } + + +.. index:: administrative instruction, value type, context, store +.. _valid-instr-admin: + +Administrative Instructions +~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Typing rules for :ref:`administrative instructions ` are specified as follows. +In addition to the :ref:`context ` :math:`C`, typing of these instructions is defined under a given :ref:`store ` :math:`S`. +To that end, all previous typing judgements :math:`C \vdash \X{prop}` are generalized to include the store, as in :math:`S; C \vdash \X{prop}`, by implicitly adding :math:`S` to all rules -- :math:`S` is never modified by the pre-existing rules, but it is accessed in the extra rules for :ref:`administrative instructions ` given below. + + +.. index:: trap + +:math:`\TRAP` +............. + +* The instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`, for any sequences of :ref:`value types ` :math:`t_1^\ast` and :math:`t_2^\ast`. + +.. math:: + \frac{ + }{ + S; C \vdashadmininstr \TRAP : [t_1^\ast] \to [t_2^\ast] + } + + +.. index:: function address, extern value, extern type, function type + +:math:`\INVOKE~\funcaddr` +......................... + +* The :ref:`external function value ` :math:`\EVFUNC~\funcaddr` must be :ref:`valid ` with :ref:`external function type ` :math:`\ETFUNC ([t_1^\ast] \to [t_2^\ast])`. + +* Then the instruction is valid with type :math:`[t_1^\ast] \to [t_2^\ast]`. + +.. math:: + \frac{ + S \vdashexternval \EVFUNC~\funcaddr : \ETFUNC~[t_1^\ast] \to [t_2^\ast] + }{ + S; C \vdashadmininstr \INVOKE~\funcaddr : [t_1^\ast] \to [t_2^\ast] + } + + +.. index:: element, table, table address, module instance, function index + +:math:`\INITELEM~\tableaddr~o~x^n` +.................................. + +* The :ref:`external table value ` :math:`\EVTABLE~\tableaddr` must be :ref:`valid ` with some :ref:`external table type ` :math:`\ETTABLE~\limits~\FUNCREF`. + +* The index :math:`o + n` must be smaller than or equal to :math:`\limits.\LMIN`. + +* The :ref:`module instance ` :math:`\moduleinst` must be :ref:`valid ` with some :ref:`context ` :math:`C`. + +* Each :ref:`function index ` :math:`x_i` in :math:`x^n` must be defined in the context :math:`C`. + +* Then the instruction is valid. + +.. math:: + \frac{ + S \vdashexternval \EVTABLE~\tableaddr : \ETTABLE~\limits~\FUNCREF + \qquad + o + n \leq \limits.\LMIN + \qquad + (C.\CFUNCS[x] = \functype)^n + }{ + S; C \vdashadmininstr \INITELEM~\tableaddr~o~x^n \ok + } + + +.. index:: data, memory, memory address, byte + +:math:`\INITDATA~\memaddr~o~b^n` +................................ + +* The :ref:`external memory value ` :math:`\EVMEM~\memaddr` must be :ref:`valid ` with some :ref:`external memory type ` :math:`\ETMEM~\limits`. + +* The index :math:`o + n` must be smaller than or equal to :math:`\limits.\LMIN` divided by the :ref:`page size ` :math:`64\,\F{Ki}`. + +* Then the instruction is valid. + +.. math:: + \frac{ + S \vdashexternval \EVMEM~\memaddr : \ETMEM~\limits + \qquad + o + n \leq \limits.\LMIN \cdot 64\,\F{Ki} + }{ + S; C \vdashadmininstr \INITDATA~\memaddr~o~b^n \ok + } + + +.. index:: label, instruction, result type + +:math:`\LABEL_n\{\instr_0^\ast\}~\instr^\ast~\END` +.................................................. + +* The instruction sequence :math:`\instr_0^\ast` must be :ref:`valid ` with some type :math:`[t_1^n] \to [t_2^?]`. + +* Let :math:`C'` be the same :ref:`context ` as :math:`C`, but with the :ref:`result type ` :math:`[t_1^n]` prepended to the |CLABELS| vector. + +* Under context :math:`C'`, + the instruction sequence :math:`\instr^\ast` must be :ref:`valid ` with type :math:`[] \to [t_2^?]`. + +* Then the compound instruction is valid with type :math:`[] \to [t_2^?]`. + +.. math:: + \frac{ + S; C \vdashinstrseq \instr_0^\ast : [t_1^n] \to [t_2^?] + \qquad + S; C,\CLABELS\,[t_1^n] \vdashinstrseq \instr^\ast : [] \to [t_2^?] + }{ + S; C \vdashadmininstr \LABEL_n\{\instr_0^\ast\}~\instr^\ast~\END : [] \to [t_2^?] + } + + +.. index:: frame, instruction, result type + +:math:`\FRAME_n\{F\}~\instr^\ast~\END` +........................................... + +* Under the return type :math:`[t^n]`, + the :ref:`thread ` :math:`F; \instr^\ast` must be :ref:`valid ` with :ref:`result type ` :math:`[t^n]`. + +* Then the compound instruction is valid with type :math:`[] \to [t^n]`. + +.. math:: + \frac{ + S; [t^n] \vdashinstrseq F; \instr^\ast : [t^n] + }{ + S; C \vdashadmininstr \FRAME_n\{F\}~\instr^\ast~\END : [] \to [t^n] + } + + +.. index:: ! store extension, store +.. _extend: + +Store Extension +~~~~~~~~~~~~~~~ + +Programs can mutate the :ref:`store ` and its contained instances. +Any such modification must respect certain invariants, such as not removing allocated instances or changing immutable definitions. +While these invariants are inherent to the execution semantics of WebAssembly :ref:`instructions ` and :ref:`modules `, +:ref:`host functions ` do not automatically adhere to them. Consequently, the required invariants must be stated as explicit constraints on the :ref:`invocation ` of host functions. +Soundness only holds when the :ref:`embedder ` ensures these constraints. + +The necessary constraints are codified by the notion of store *extension*: +a store state :math:`S'` extends state :math:`S`, written :math:`S \extendsto S'`, when the following rules hold. + +.. note:: + Extension does not imply that the new store is valid, which is defined separately :ref:`above `. + + +.. index:: store, function instance, table instance, memory instance, global instance +.. _extend-store: + +:ref:`Store ` :math:`S` +..................................... + +* The length of :math:`S.\SFUNCS` must not shrink. + +* The length of :math:`S.\STABLES` must not shrink. + +* The length of :math:`S.\SMEMS` must not shrink. + +* The length of :math:`S.\SGLOBALS` must not shrink. + +* For each :ref:`function instance ` :math:`\funcinst_i` in the original :math:`S.\SFUNCS`, the new function instance must be an :ref:`extension ` of the old. + +* For each :ref:`table instance ` :math:`\tableinst_i` in the original :math:`S.\STABLES`, the new table instance must be an :ref:`extension ` of the old. + +* For each :ref:`memory instance ` :math:`\meminst_i` in the original :math:`S.\SMEMS`, the new memory instance must be an :ref:`extension ` of the old. + +* For each :ref:`global instance ` :math:`\globalinst_i` in the original :math:`S.\SGLOBALS`, the new global instance must be an :ref:`extension ` of the old. + +.. math:: + \frac{ + \begin{array}{@{}ccc@{}} + S_1.\SFUNCS = \funcinst_1^\ast & + S_2.\SFUNCS = {\funcinst'_1}^\ast~\funcinst_2^\ast & + (\funcinst_1 \extendsto \funcinst'_1)^\ast \\ + S_1.\STABLES = \tableinst_1^\ast & + S_2.\STABLES = {\tableinst'_1}^\ast~\tableinst_2^\ast & + (\tableinst_1 \extendsto \tableinst'_1)^\ast \\ + S_1.\SMEMS = \meminst_1^\ast & + S_2.\SMEMS = {\meminst'_1}^\ast~\meminst_2^\ast & + (\meminst_1 \extendsto \meminst'_1)^\ast \\ + S_1.\SGLOBALS = \globalinst_1^\ast & + S_2.\SGLOBALS = {\globalinst'_1}^\ast~\globalinst_2^\ast & + (\globalinst_1 \extendsto \globalinst'_1)^\ast \\ + \end{array} + }{ + \vdashstoreextends S_1 \extendsto S_2 + } + + +.. index:: function instance +.. _extend-funcinst: + +:ref:`Function Instance ` :math:`\funcinst` +............................................................ + +* A function instance must remain unchanged. + +.. math:: + \frac{ + }{ + \vdashfuncinstextends \funcinst \extendsto \funcinst + } + + +.. index:: table instance +.. _extend-tableinst: + +:ref:`Table Instance ` :math:`\tableinst` +........................................................... + +* The length of :math:`\tableinst.\TIELEM` must not shrink. + +* The value of :math:`\tableinst.\TIMAX` must remain unchanged. + +.. math:: + \frac{ + n_1 \leq n_2 + }{ + \vdashtableinstextends \{\TIELEM~(\X{fa}_1^?)^{n_1}, \TIMAX~m\} \extendsto \{\TIELEM~(\X{fa}_2^?)^{n_2}, \TIMAX~m\} + } + + +.. index:: memory instance +.. _extend-meminst: + +:ref:`Memory Instance ` :math:`\meminst` +........................................................ + +* The length of :math:`\meminst.\MIDATA` must not shrink. + +* The value of :math:`\meminst.\MIMAX` must remain unchanged. + +.. math:: + \frac{ + n_1 \leq n_2 + }{ + \vdashmeminstextends \{\MIDATA~b_1^{n_1}, \MIMAX~m\} \extendsto \{\MIDATA~b_2^{n_2}, \MIMAX~m\} + } + + +.. index:: global instance, value, mutability +.. _extend-globalinst: + +:ref:`Global Instance ` :math:`\globalinst` +.............................................................. + +* The :ref:`mutability ` :math:`\globalinst.\GIMUT` must remain unchanged. + +* The :ref:`value type ` of the :ref:`value ` :math:`\globalinst.\GIVALUE` must remain unchanged. + +* If :math:`\globalinst.\GIMUT` is |MCONST|, then the :ref:`value ` :math:`\globalinst.\GIVALUE` must remain unchanged. + +.. math:: + \frac{ + \mut = \MVAR \vee c_1 = c_2 + }{ + \vdashglobalinstextends \{\GIVALUE~(t.\CONST~c_1), \GIMUT~\mut\} \extendsto \{\GIVALUE~(t.\CONST~c_2), \GIMUT~\mut\} + } + + + +.. index:: ! preservation, ! progress, soundness, configuration, thread, terminal configuration, instantiation, invocation, validity, module +.. _soundness-statement: + +Theorems +~~~~~~~~ + +Given the definition of :ref:`valid configurations `, +the standard soundness theorems hold. [#cite-cpp2018]_ + +**Theorem (Preservation).** +If a :ref:`configuration ` :math:`S;T` is :ref:`valid ` with :ref:`result type ` :math:`[t^\ast]` (i.e., :math:`\vdashconfig S;T : [t^\ast]`), +and steps to :math:`S';T'` (i.e., :math:`S;T \stepto S';T'`), +then :math:`S';T'` is a valid configuration with the same result type (i.e., :math:`\vdashconfig S';T' : [t^\ast]`). +Furthermore, :math:`S'` is an :ref:`extension ` of :math:`S` (i.e., :math:`\vdashstoreextends S \extendsto S'`). + +A *terminal* :ref:`thread ` is one whose sequence of :ref:`instructions ` is a :ref:`result `. +A terminal configuration is a configuration whose thread is terminal. + +**Theorem (Progress).** +If a :ref:`configuration ` :math:`S;T` is :ref:`valid ` (i.e., :math:`\vdashconfig S;T : [t^\ast]` for some :ref:`result type ` :math:`[t^\ast]`), +then either it is terminal, +or it can step to some configuration :math:`S';T'` (i.e., :math:`S;T \stepto S';T'`). + +From Preservation and Progress the soundness of the WebAssembly type system follows directly. + +**Corollary (Soundness).** +If a :ref:`configuration ` :math:`S;T` is :ref:`valid ` (i.e., :math:`\vdashconfig S;T : [t^\ast]` for some :ref:`result type ` :math:`[t^\ast]`), +then it either diverges or takes a finite number of steps to reach a terminal configuration :math:`S';T'` (i.e., :math:`S;T \stepto^\ast S';T'`) that is valid with the same result type (i.e., :math:`\vdashconfig S';T' : [t^\ast]`) +and where :math:`S'` is an :ref:`extension ` of :math:`S` (i.e., :math:`\vdashstoreextends S \extendsto S'`). + +In other words, every thread in a valid configuration either runs forever, traps, or terminates with a result that has the expected type. +Consequently, given a :ref:`valid store `, no computation defined by :ref:`instantiation ` or :ref:`invocation ` of a valid module can "crash" or otherwise (mis)behave in ways not covered by the :ref:`execution ` semantics given in this specification. + + +.. [#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. diff --git a/document/core/binary/conventions.rst b/document/core/binary/conventions.rst new file mode 100644 index 00000000..8d383997 --- /dev/null +++ b/document/core/binary/conventions.rst @@ -0,0 +1,118 @@ +.. index:: ! binary format, module, byte, file extension, abstract syntax + +Conventions +----------- + +The binary format for WebAssembly :ref:`modules ` is a dense linear *encoding* of their :ref:`abstract syntax `. +[#compression]_ + +The format is defined by an *attribute grammar* whose only terminal symbols are :ref:`bytes `. +A byte sequence is a well-formed encoding of a module if and only if it is generated by the grammar. + +Each production of this grammar has exactly one synthesized attribute: the abstract syntax that the respective byte sequence encodes. +Thus, the attribute grammar implicitly defines a *decoding* function +(i.e., a parsing function for the binary format). + +Except for a few exceptions, the binary grammar closely mirrors the grammar of the abstract syntax. + +.. note:: + Some phrases of abstract syntax have multiple possible encodings in the binary format. + For example, numbers may be encoded as if they had optional leading zeros. + Implementations of decoders must support all possible alternatives; + implementations of encoders can pick any allowed encoding. + +The recommended extension for files containing WebAssembly modules in binary format is ":math:`\T{.wasm}`" +and the recommended |MediaType|_ is ":math:`\T{application/wasm}`". + +.. [#compression] + Additional encoding layers -- for example, introducing compression -- may be defined on top of the basic representation defined here. + However, such layers are outside the scope of the current specification. + + +.. index:: grammar notation, notation, byte + single: binary format; grammar + pair: binary format; notation +.. _binary-grammar: + +Grammar +~~~~~~~ + +The following conventions are adopted in defining grammar rules for the binary format. +They mirror the conventions used for :ref:`abstract syntax `. +In order to distinguish symbols of the binary syntax from symbols of the abstract syntax, :math:`\mathtt{typewriter}` font is adopted for the former. + +* Terminal symbols are :ref:`bytes ` expressed in hexadecimal notation: :math:`\hex{0F}`. + +* Nonterminal symbols are written in typewriter font: :math:`\B{valtype}, \B{instr}`. + +* :math:`B^n` is a sequence of :math:`n\geq 0` iterations of :math:`B`. + +* :math:`B^\ast` is a possibly empty sequence of iterations of :math:`B`. + (This is a shorthand for :math:`B^n` used where :math:`n` is not relevant.) + +* :math:`B^?` is an optional occurrence of :math:`B`. + (This is a shorthand for :math:`B^n` where :math:`n \leq 1`.) + +* :math:`x{:}B` denotes the same language as the nonterminal :math:`B`, but also binds the variable :math:`x` to the attribute synthesized for :math:`B`. + +* Productions are written :math:`\B{sym} ::= B_1 \Rightarrow A_1 ~|~ \dots ~|~ B_n \Rightarrow A_n`, where each :math:`A_i` is the attribute that is synthesized for :math:`\B{sym}` in the given case, usually from attribute variables bound in :math:`B_i`. + +* Some productions are augmented by side conditions in parentheses, which restrict the applicability of the production. They provide a shorthand for a combinatorial expansion of the production into many separate cases. + +.. note:: + For example, the :ref:`binary grammar ` for :ref:`value types ` is given as follows: + + .. math:: + \begin{array}{llcll@{\qquad\qquad}l} + \production{value types} & \Bvaltype &::=& + \hex{7F} &\Rightarrow& \I32 \\ &&|& + \hex{7E} &\Rightarrow& \I64 \\ &&|& + \hex{7D} &\Rightarrow& \F32 \\ &&|& + \hex{7C} &\Rightarrow& \F64 \\ + \end{array} + + Consequently, the byte :math:`\hex{7F}` encodes the type |I32|, + :math:`\hex{7E}` encodes the type |I64|, and so forth. + No other byte value is allowed as the encoding of a value type. + + The :ref:`binary grammar ` for :ref:`limits ` is defined as follows: + + .. math:: + \begin{array}{llclll} + \production{limits} & \Blimits &::=& + \hex{00}~~n{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~\epsilon \} \\ &&|& + \hex{01}~~n{:}\Bu32~~m{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~m \} \\ + \end{array} + + That is, a limits pair is encoded as either the byte :math:`\hex{00}` followed by the encoding of a |U32| value, + or the byte :math:`\hex{01}` followed by two such encodings. + The variables :math:`n` and :math:`m` name the attributes of the respective |Bu32| nonterminals, which in this case are the actual :ref:`unsigned integers ` those decode into. + The attribute of the complete production then is the abstract syntax for the limit, expressed in terms of the former values. + + +.. _binary-notation: + +Auxiliary Notation +~~~~~~~~~~~~~~~~~~ + +When dealing with binary encodings the following notation is also used: + +* :math:`\epsilon` denotes the empty byte sequence. + +* :math:`||B||` is the length of the byte sequence generated from the production :math:`B` in a derivation. + + +.. index:: vector + pair: binary format; vector +.. _binary-vec: + +Vectors +~~~~~~~ + +:ref:`Vectors ` are encoded with their |Bu32| length followed by the encoding of their element sequence. + +.. math:: + \begin{array}{llclll@{\qquad\qquad}l} + \production{vector} & \Bvec(\B{B}) &::=& + n{:}\Bu32~~(x{:}\B{B})^n &\Rightarrow& x^n \\ + \end{array} diff --git a/document/core/binary/index.rst b/document/core/binary/index.rst new file mode 100644 index 00000000..b47e6647 --- /dev/null +++ b/document/core/binary/index.rst @@ -0,0 +1,13 @@ +.. _binary: + +Binary Format +============= + +.. toctree:: + :maxdepth: 2 + + conventions + values + types + instructions + modules diff --git a/document/core/binary/instructions.rst b/document/core/binary/instructions.rst new file mode 100644 index 00000000..1d4a8af8 --- /dev/null +++ b/document/core/binary/instructions.rst @@ -0,0 +1,381 @@ +.. index:: instruction, ! opcode +.. _binary-instr: + +Instructions +------------ + +:ref:`Instructions ` are encoded by *opcodes*. +Each opcode is represented by a single byte, +and is followed by the instruction's immediate arguments, where present. +The only exception are :ref:`structured control instructions `, which consist of several opcodes bracketing their nested instruction sequences. + +.. note:: + Gaps in the byte code ranges for encoding instructions are reserved for future extensions. + + +.. index:: control instructions, structured control, label, block, branch, result type, label index, function index, type index, vector, polymorphism + pair: binary format; instruction +.. _binary-instr-control: + +Control Instructions +~~~~~~~~~~~~~~~~~~~~ + +:ref:`Control instructions ` have varying encodings. For structured instructions, the instruction sequences forming nested blocks are terminated with explicit opcodes for |END| and |ELSE|. + +.. _binary-nop: +.. _binary-unreachable: +.. _binary-block: +.. _binary-loop: +.. _binary-if: +.. _binary-br: +.. _binary-br_if: +.. _binary-br_table: +.. _binary-return: +.. _binary-call: +.. _binary-call_indirect: + +.. math:: + \begin{array}{llclll} + \production{instruction} & \Binstr &::=& + \hex{00} &\Rightarrow& \UNREACHABLE \\ &&|& + \hex{01} &\Rightarrow& \NOP \\ &&|& + \hex{02}~~\X{rt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B} + &\Rightarrow& \BLOCK~\X{rt}~\X{in}^\ast~\END \\ &&|& + \hex{03}~~\X{rt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B} + &\Rightarrow& \LOOP~\X{rt}~\X{in}^\ast~\END \\ &&|& + \hex{04}~~\X{rt}{:}\Bblocktype~~(\X{in}{:}\Binstr)^\ast~~\hex{0B} + &\Rightarrow& \IF~\X{rt}~\X{in}^\ast~\ELSE~\epsilon~\END \\ &&|& + \hex{04}~~\X{rt}{:}\Bblocktype~~(\X{in}_1{:}\Binstr)^\ast~~ + \hex{05}~~(\X{in}_2{:}\Binstr)^\ast~~\hex{0B} + &\Rightarrow& \IF~\X{rt}~\X{in}_1^\ast~\ELSE~\X{in}_2^\ast~\END \\ &&|& + \hex{0C}~~l{:}\Blabelidx &\Rightarrow& \BR~l \\ &&|& + \hex{0D}~~l{:}\Blabelidx &\Rightarrow& \BRIF~l \\ &&|& + \hex{0E}~~l^\ast{:}\Bvec(\Blabelidx)~~l_N{:}\Blabelidx + &\Rightarrow& \BRTABLE~l^\ast~l_N \\ &&|& + \hex{0F} &\Rightarrow& \RETURN \\ &&|& + \hex{10}~~x{:}\Bfuncidx &\Rightarrow& \CALL~x \\ &&|& + \hex{11}~~x{:}\Btypeidx~~\hex{00} &\Rightarrow& \CALLINDIRECT~x \\ + \end{array} + +.. note:: + The |ELSE| opcode :math:`\hex{05}` in the encoding of an |IF| instruction can be omitted if the following instruction sequence is empty. + +.. note:: + In future versions of WebAssembly, the zero byte occurring in the encoding + of the |CALLINDIRECT| instruction may be used to index additional tables. + +.. index:: value type, polymorphism + pair: binary format; instruction +.. _binary-instr-parametric: + +Parametric Instructions +~~~~~~~~~~~~~~~~~~~~~~~ + +:ref:`Parametric instructions ` are represented by single byte codes. + +.. _binary-drop: +.. _binary-select: + +.. math:: + \begin{array}{llclll} + \production{instruction} & \Binstr &::=& \dots \\ &&|& + \hex{1A} &\Rightarrow& \DROP \\ &&|& + \hex{1B} &\Rightarrow& \SELECT \\ + \end{array} + + +.. index:: variable instructions, local index, global index + pair: binary format; instruction +.. _binary-instr-variable: + +Variable Instructions +~~~~~~~~~~~~~~~~~~~~~ + +:ref:`Variable instructions ` are represented by byte codes followed by the encoding of the respective :ref:`index `. + +.. _binary-local.get: +.. _binary-local.set: +.. _binary-local.tee: +.. _binary-global.get: +.. _binary-global.set: + +.. math:: + \begin{array}{llclll} + \production{instruction} & \Binstr &::=& \dots \\ &&|& + \hex{20}~~x{:}\Blocalidx &\Rightarrow& \LOCALGET~x \\ &&|& + \hex{21}~~x{:}\Blocalidx &\Rightarrow& \LOCALSET~x \\ &&|& + \hex{22}~~x{:}\Blocalidx &\Rightarrow& \LOCALTEE~x \\ &&|& + \hex{23}~~x{:}\Bglobalidx &\Rightarrow& \GLOBALGET~x \\ &&|& + \hex{24}~~x{:}\Bglobalidx &\Rightarrow& \GLOBALSET~x \\ + \end{array} + + +.. index:: memory instruction, memory index + pair: binary format; instruction +.. _binary-instr-memory: + +Memory Instructions +~~~~~~~~~~~~~~~~~~~ + +Each variant of :ref:`memory instruction ` is encoded with a different byte code. Loads and stores are followed by the encoding of their |memarg| immediate. + +.. _binary-memarg: +.. _binary-load: +.. _binary-loadn: +.. _binary-store: +.. _binary-storen: +.. _binary-memory.size: +.. _binary-memory.grow: + +.. math:: + \begin{array}{llclll} + \production{memory argument} & \Bmemarg &::=& + a{:}\Bu32~~o{:}\Bu32 &\Rightarrow& \{ \ALIGN~a,~\OFFSET~o \} \\ + \production{instruction} & \Binstr &::=& \dots \\ &&|& + \hex{28}~~m{:}\Bmemarg &\Rightarrow& \I32.\LOAD~m \\ &&|& + \hex{29}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD~m \\ &&|& + \hex{2A}~~m{:}\Bmemarg &\Rightarrow& \F32.\LOAD~m \\ &&|& + \hex{2B}~~m{:}\Bmemarg &\Rightarrow& \F64.\LOAD~m \\ &&|& + \hex{2C}~~m{:}\Bmemarg &\Rightarrow& \I32.\LOAD\K{8\_s}~m \\ &&|& + \hex{2D}~~m{:}\Bmemarg &\Rightarrow& \I32.\LOAD\K{8\_u}~m \\ &&|& + \hex{2E}~~m{:}\Bmemarg &\Rightarrow& \I32.\LOAD\K{16\_s}~m \\ &&|& + \hex{2F}~~m{:}\Bmemarg &\Rightarrow& \I32.\LOAD\K{16\_u}~m \\ &&|& + \hex{30}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD\K{8\_s}~m \\ &&|& + \hex{31}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD\K{8\_u}~m \\ &&|& + \hex{32}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD\K{16\_s}~m \\ &&|& + \hex{33}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD\K{16\_u}~m \\ &&|& + \hex{34}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD\K{32\_s}~m \\ &&|& + \hex{35}~~m{:}\Bmemarg &\Rightarrow& \I64.\LOAD\K{32\_u}~m \\ &&|& + \hex{36}~~m{:}\Bmemarg &\Rightarrow& \I32.\STORE~m \\ &&|& + \hex{37}~~m{:}\Bmemarg &\Rightarrow& \I64.\STORE~m \\ &&|& + \hex{38}~~m{:}\Bmemarg &\Rightarrow& \F32.\STORE~m \\ &&|& + \hex{39}~~m{:}\Bmemarg &\Rightarrow& \F64.\STORE~m \\ &&|& + \hex{3A}~~m{:}\Bmemarg &\Rightarrow& \I32.\STORE\K{8}~m \\ &&|& + \hex{3B}~~m{:}\Bmemarg &\Rightarrow& \I32.\STORE\K{16}~m \\ &&|& + \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& \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 |MEMORYSIZE| and |MEMORYGROW| instructions may be used to index additional memories. + + +.. index:: numeric instruction + pair: binary format; instruction +.. _binary-instr-numeric: + +Numeric Instructions +~~~~~~~~~~~~~~~~~~~~ + +All variants of :ref:`numeric instructions ` are represented by separate byte codes. + +The |CONST| instructions are followed by the respective literal. + +.. _binary-const: + +.. math:: + \begin{array}{llclll} + \production{instruction} & \Binstr &::=& \dots \\&&|& + \hex{41}~~n{:}\Bi32 &\Rightarrow& \I32.\CONST~n \\ &&|& + \hex{42}~~n{:}\Bi64 &\Rightarrow& \I64.\CONST~n \\ &&|& + \hex{43}~~z{:}\Bf32 &\Rightarrow& \F32.\CONST~z \\ &&|& + \hex{44}~~z{:}\Bf64 &\Rightarrow& \F64.\CONST~z \\ + \end{array} + +All other numeric instructions are plain opcodes without any immediates. + +.. _binary-testop: +.. _binary-relop: + +.. math:: + \begin{array}{llclll} + \production{instruction} & \Binstr &::=& \dots && \phantom{thisshouldbeenough} \\&&|& + \hex{45} &\Rightarrow& \I32.\EQZ \\ &&|& + \hex{46} &\Rightarrow& \I32.\EQ \\ &&|& + \hex{47} &\Rightarrow& \I32.\NE \\ &&|& + \hex{48} &\Rightarrow& \I32.\LT\K{\_s} \\ &&|& + \hex{49} &\Rightarrow& \I32.\LT\K{\_u} \\ &&|& + \hex{4A} &\Rightarrow& \I32.\GT\K{\_s} \\ &&|& + \hex{4B} &\Rightarrow& \I32.\GT\K{\_u} \\ &&|& + \hex{4C} &\Rightarrow& \I32.\LE\K{\_s} \\ &&|& + \hex{4D} &\Rightarrow& \I32.\LE\K{\_u} \\ &&|& + \hex{4E} &\Rightarrow& \I32.\GE\K{\_s} \\ &&|& + \hex{4F} &\Rightarrow& \I32.\GE\K{\_u} \\ + \end{array} + +.. math:: + \begin{array}{llclll} + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \hex{50} &\Rightarrow& \I64.\EQZ \\ &&|& + \hex{51} &\Rightarrow& \I64.\EQ \\ &&|& + \hex{52} &\Rightarrow& \I64.\NE \\ &&|& + \hex{53} &\Rightarrow& \I64.\LT\K{\_s} \\ &&|& + \hex{54} &\Rightarrow& \I64.\LT\K{\_u} \\ &&|& + \hex{55} &\Rightarrow& \I64.\GT\K{\_s} \\ &&|& + \hex{56} &\Rightarrow& \I64.\GT\K{\_u} \\ &&|& + \hex{57} &\Rightarrow& \I64.\LE\K{\_s} \\ &&|& + \hex{58} &\Rightarrow& \I64.\LE\K{\_u} \\ &&|& + \hex{59} &\Rightarrow& \I64.\GE\K{\_s} \\ &&|& + \hex{5A} &\Rightarrow& \I64.\GE\K{\_u} \\ + \end{array} + +.. math:: + \begin{array}{llclll} + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \hex{5B} &\Rightarrow& \F32.\EQ \\ &&|& + \hex{5C} &\Rightarrow& \F32.\NE \\ &&|& + \hex{5D} &\Rightarrow& \F32.\LT \\ &&|& + \hex{5E} &\Rightarrow& \F32.\GT \\ &&|& + \hex{5F} &\Rightarrow& \F32.\LE \\ &&|& + \hex{60} &\Rightarrow& \F32.\GE \\ + \end{array} + +.. math:: + \begin{array}{llclll} + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \hex{61} &\Rightarrow& \F64.\EQ \\ &&|& + \hex{62} &\Rightarrow& \F64.\NE \\ &&|& + \hex{63} &\Rightarrow& \F64.\LT \\ &&|& + \hex{64} &\Rightarrow& \F64.\GT \\ &&|& + \hex{65} &\Rightarrow& \F64.\LE \\ &&|& + \hex{66} &\Rightarrow& \F64.\GE \\ + \end{array} + +.. _binary-unop: +.. _binary-binop: + +.. math:: + \begin{array}{llclll} + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \hex{67} &\Rightarrow& \I32.\CLZ \\ &&|& + \hex{68} &\Rightarrow& \I32.\CTZ \\ &&|& + \hex{69} &\Rightarrow& \I32.\POPCNT \\ &&|& + \hex{6A} &\Rightarrow& \I32.\ADD \\ &&|& + \hex{6B} &\Rightarrow& \I32.\SUB \\ &&|& + \hex{6C} &\Rightarrow& \I32.\MUL \\ &&|& + \hex{6D} &\Rightarrow& \I32.\DIV\K{\_s} \\ &&|& + \hex{6E} &\Rightarrow& \I32.\DIV\K{\_u} \\ &&|& + \hex{6F} &\Rightarrow& \I32.\REM\K{\_s} \\ &&|& + \hex{70} &\Rightarrow& \I32.\REM\K{\_u} \\ &&|& + \hex{71} &\Rightarrow& \I32.\AND \\ &&|& + \hex{72} &\Rightarrow& \I32.\OR \\ &&|& + \hex{73} &\Rightarrow& \I32.\XOR \\ &&|& + \hex{74} &\Rightarrow& \I32.\SHL \\ &&|& + \hex{75} &\Rightarrow& \I32.\SHR\K{\_s} \\ &&|& + \hex{76} &\Rightarrow& \I32.\SHR\K{\_u} \\ &&|& + \hex{77} &\Rightarrow& \I32.\ROTL \\ &&|& + \hex{78} &\Rightarrow& \I32.\ROTR \\ + \end{array} + +.. math:: + \begin{array}{llclll} + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \hex{79} &\Rightarrow& \I64.\CLZ \\ &&|& + \hex{7A} &\Rightarrow& \I64.\CTZ \\ &&|& + \hex{7B} &\Rightarrow& \I64.\POPCNT \\ &&|& + \hex{7C} &\Rightarrow& \I64.\ADD \\ &&|& + \hex{7D} &\Rightarrow& \I64.\SUB \\ &&|& + \hex{7E} &\Rightarrow& \I64.\MUL \\ &&|& + \hex{7F} &\Rightarrow& \I64.\DIV\K{\_s} \\ &&|& + \hex{80} &\Rightarrow& \I64.\DIV\K{\_u} \\ &&|& + \hex{81} &\Rightarrow& \I64.\REM\K{\_s} \\ &&|& + \hex{82} &\Rightarrow& \I64.\REM\K{\_u} \\ &&|& + \hex{83} &\Rightarrow& \I64.\AND \\ &&|& + \hex{84} &\Rightarrow& \I64.\OR \\ &&|& + \hex{85} &\Rightarrow& \I64.\XOR \\ &&|& + \hex{86} &\Rightarrow& \I64.\SHL \\ &&|& + \hex{87} &\Rightarrow& \I64.\SHR\K{\_s} \\ &&|& + \hex{88} &\Rightarrow& \I64.\SHR\K{\_u} \\ &&|& + \hex{89} &\Rightarrow& \I64.\ROTL \\ &&|& + \hex{8A} &\Rightarrow& \I64.\ROTR \\ + \end{array} + +.. math:: + \begin{array}{llclll} + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \hex{8B} &\Rightarrow& \F32.\ABS \\ &&|& + \hex{8C} &\Rightarrow& \F32.\NEG \\ &&|& + \hex{8D} &\Rightarrow& \F32.\CEIL \\ &&|& + \hex{8E} &\Rightarrow& \F32.\FLOOR \\ &&|& + \hex{8F} &\Rightarrow& \F32.\TRUNC \\ &&|& + \hex{90} &\Rightarrow& \F32.\NEAREST \\ &&|& + \hex{91} &\Rightarrow& \F32.\SQRT \\ &&|& + \hex{92} &\Rightarrow& \F32.\ADD \\ &&|& + \hex{93} &\Rightarrow& \F32.\SUB \\ &&|& + \hex{94} &\Rightarrow& \F32.\MUL \\ &&|& + \hex{95} &\Rightarrow& \F32.\DIV \\ &&|& + \hex{96} &\Rightarrow& \F32.\FMIN \\ &&|& + \hex{97} &\Rightarrow& \F32.\FMAX \\ &&|& + \hex{98} &\Rightarrow& \F32.\COPYSIGN \\ + \end{array} + +.. math:: + \begin{array}{llclll} + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \hex{99} &\Rightarrow& \F64.\ABS \\ &&|& + \hex{9A} &\Rightarrow& \F64.\NEG \\ &&|& + \hex{9B} &\Rightarrow& \F64.\CEIL \\ &&|& + \hex{9C} &\Rightarrow& \F64.\FLOOR \\ &&|& + \hex{9D} &\Rightarrow& \F64.\TRUNC \\ &&|& + \hex{9E} &\Rightarrow& \F64.\NEAREST \\ &&|& + \hex{9F} &\Rightarrow& \F64.\SQRT \\ &&|& + \hex{A0} &\Rightarrow& \F64.\ADD \\ &&|& + \hex{A1} &\Rightarrow& \F64.\SUB \\ &&|& + \hex{A2} &\Rightarrow& \F64.\MUL \\ &&|& + \hex{A3} &\Rightarrow& \F64.\DIV \\ &&|& + \hex{A4} &\Rightarrow& \F64.\FMIN \\ &&|& + \hex{A5} &\Rightarrow& \F64.\FMAX \\ &&|& + \hex{A6} &\Rightarrow& \F64.\COPYSIGN \\ + \end{array} + +.. _binary-cvtop: + +.. math:: + \begin{array}{llclll} + \phantom{\production{instruction}} & \phantom{\Binstr} &\phantom{::=}& \phantom{\dots} && \phantom{thisshouldbeenough} \\[-2ex] &&|& + \hex{A7} &\Rightarrow& \I32.\WRAP\K{\_}\I64 \\ &&|& + \hex{A8} &\Rightarrow& \I32.\TRUNC\K{\_}\F32\K{\_s} \\ &&|& + \hex{A9} &\Rightarrow& \I32.\TRUNC\K{\_}\F32\K{\_u} \\ &&|& + \hex{AA} &\Rightarrow& \I32.\TRUNC\K{\_}\F64\K{\_s} \\ &&|& + \hex{AB} &\Rightarrow& \I32.\TRUNC\K{\_}\F64\K{\_u} \\ &&|& + \hex{AC} &\Rightarrow& \I64.\EXTEND\K{\_}\I32\K{\_s} \\ &&|& + \hex{AD} &\Rightarrow& \I64.\EXTEND\K{\_}\I32\K{\_u} \\ &&|& + \hex{AE} &\Rightarrow& \I64.\TRUNC\K{\_}\F32\K{\_s} \\ &&|& + \hex{AF} &\Rightarrow& \I64.\TRUNC\K{\_}\F32\K{\_u} \\ &&|& + \hex{B0} &\Rightarrow& \I64.\TRUNC\K{\_}\F64\K{\_s} \\ &&|& + \hex{B1} &\Rightarrow& \I64.\TRUNC\K{\_}\F64\K{\_u} \\ &&|& + \hex{B2} &\Rightarrow& \F32.\CONVERT\K{\_}\I32\K{\_s} \\ &&|& + \hex{B3} &\Rightarrow& \F32.\CONVERT\K{\_}\I32\K{\_u} \\ &&|& + \hex{B4} &\Rightarrow& \F32.\CONVERT\K{\_}\I64\K{\_s} \\ &&|& + \hex{B5} &\Rightarrow& \F32.\CONVERT\K{\_}\I64\K{\_u} \\ &&|& + \hex{B6} &\Rightarrow& \F32.\DEMOTE\K{\_}\F64 \\ &&|& + \hex{B7} &\Rightarrow& \F64.\CONVERT\K{\_}\I32\K{\_s} \\ &&|& + \hex{B8} &\Rightarrow& \F64.\CONVERT\K{\_}\I32\K{\_u} \\ &&|& + \hex{B9} &\Rightarrow& \F64.\CONVERT\K{\_}\I64\K{\_s} \\ &&|& + \hex{BA} &\Rightarrow& \F64.\CONVERT\K{\_}\I64\K{\_u} \\ &&|& + \hex{BB} &\Rightarrow& \F64.\PROMOTE\K{\_}\F32 \\ &&|& + \hex{BC} &\Rightarrow& \I32.\REINTERPRET\K{\_}\F32 \\ &&|& + \hex{BD} &\Rightarrow& \I64.\REINTERPRET\K{\_}\F64 \\ &&|& + \hex{BE} &\Rightarrow& \F32.\REINTERPRET\K{\_}\I32 \\ &&|& + \hex{BF} &\Rightarrow& \F64.\REINTERPRET\K{\_}\I64 \\ + \end{array} + + +.. index:: expression + pair: binary format; expression + single: expression; constant +.. _binary-expr: + +Expressions +~~~~~~~~~~~ + +:ref:`Expressions ` are encoded by their instruction sequence terminated with an explicit :math:`\hex{0B}` opcode for |END|. + +.. math:: + \begin{array}{llclll} + \production{expression} & \Bexpr &::=& + (\X{in}{:}\Binstr)^\ast~~\hex{0B} &\Rightarrow& \X{in}^\ast~\END \\ + \end{array} diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst new file mode 100644 index 00000000..9c44b95c --- /dev/null +++ b/document/core/binary/modules.rst @@ -0,0 +1,484 @@ +Modules +------- + +The binary encoding of modules is organized into *sections*. +Most sections correspond to one component of a :ref:`module ` record, +except that :ref:`function definitions ` are split into two sections, separating their type declarations in the :ref:`function section ` from their bodies in the :ref:`code section `. + +.. note:: + This separation enables *parallel* and *streaming* compilation of the functions in a module. + + +.. index:: index, type index, function index, table index, memory index, global index, local index, label index + pair: binary format; type index + pair: binary format; function index + pair: binary format; table index + pair: binary format; memory index + pair: binary format; global index + pair: binary format; local index + pair: binary format; label index +.. _binary-typeidx: +.. _binary-funcidx: +.. _binary-tableidx: +.. _binary-memidx: +.. _binary-globalidx: +.. _binary-localidx: +.. _binary-labelidx: +.. _binary-index: + +Indices +~~~~~~~ + +All :ref:`indices ` are encoded with their respective value. + +.. math:: + \begin{array}{llclll} + \production{type index} & \Btypeidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{function index} & \Bfuncidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{table index} & \Btableidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{memory index} & \Bmemidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{global index} & \Bglobalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{local index} & \Blocalidx &::=& x{:}\Bu32 &\Rightarrow& x \\ + \production{label index} & \Blabelidx &::=& l{:}\Bu32 &\Rightarrow& l \\ + \end{array} + + +.. index:: ! section + pair: binary format; section +.. _binary-section: + +Sections +~~~~~~~~ + +Each section consists of + +* a one-byte section *id*, +* the |U32| *size* of the contents, in bytes, +* the actual *contents*, whose structure is depended on the section id. + +Every section is optional; an omitted section is equivalent to the section being present with empty contents. + +The following parameterized grammar rule defines the generic structure of a section with id :math:`N` and contents described by the grammar :math:`\B{B}`. + +.. math:: + \begin{array}{llclll@{\qquad}l} + \production{section} & \Bsection_N(\B{B}) &::=& + N{:}\Bbyte~~\X{size}{:}\Bu32~~\X{cont}{:}\B{B} + &\Rightarrow& \X{cont} & (\iff \X{size} = ||\B{B}||) \\ &&|& + \epsilon &\Rightarrow& \epsilon + \end{array} + +For most sections, the contents :math:`\B{B}` encodes a :ref:`vector `. +In these cases, the empty result :math:`\epsilon` is interpreted as the empty vector. + +.. note:: + Other than for unknown :ref:`custom sections `, + the :math:`\X{size}` is not required for decoding, but can be used to skip sections when navigating through a binary. + The module is malformed if the size does not match the length of the binary contents :math:`\B{B}`. + +The following section ids are used: + +== ======================================== +Id Section +== ======================================== + 0 :ref:`custom section ` + 1 :ref:`type section ` + 2 :ref:`import section ` + 3 :ref:`function section ` + 4 :ref:`table section ` + 5 :ref:`memory section ` + 6 :ref:`global section ` + 7 :ref:`export section ` + 8 :ref:`start section ` + 9 :ref:`element section ` +10 :ref:`code section ` +11 :ref:`data section ` +== ======================================== + + +.. index:: ! custom section + pair: binary format; custom section + single: section; custom +.. _binary-customsec: + +Custom Section +~~~~~~~~~~~~~~ + +*Custom sections* have the id 0. +They are intended to be used for debugging information or third-party extensions, and are ignored by the WebAssembly semantics. +Their contents consist of a :ref:`name ` further identifying the custom section, followed by an uninterpreted sequence of bytes for custom use. + +.. math:: + \begin{array}{llclll} + \production{custom section} & \Bcustomsec &::=& + \Bsection_0(\Bcustom) \\ + \production{custom data} & \Bcustom &::=& + \Bname~~\Bbyte^\ast \\ + \end{array} + +.. note:: + If an implementation interprets the contents of a custom section, then errors in that contents, or the placement of the section, must not invalidate the module. + + +.. index:: ! type section, type definition + pair: binary format; type section + pair: section; type +.. _binary-typedef: +.. _binary-typesec: + +Type Section +~~~~~~~~~~~~ + +The *type section* has the id 1. +It decodes into a vector of :ref:`function types ` that represent the |MTYPES| component of a :ref:`module `. + +.. math:: + \begin{array}{llclll} + \production{type section} & \Btypesec &::=& + \X{ft}^\ast{:\,}\Bsection_1(\Bvec(\Bfunctype)) &\Rightarrow& \X{ft}^\ast \\ + \end{array} + + +.. index:: ! import section, import, name, function type, table type, memory type, global type + pair: binary format; import + pair: section; import +.. _binary-import: +.. _binary-importdesc: +.. _binary-importsec: + +Import Section +~~~~~~~~~~~~~~ + +The *import section* has the id 2. +It decodes into a vector of :ref:`imports ` that represent the |MIMPORTS| component of a :ref:`module `. + +.. math:: + \begin{array}{llclll} + \production{import section} & \Bimportsec &::=& + \X{im}^\ast{:}\Bsection_2(\Bvec(\Bimport)) &\Rightarrow& \X{im}^\ast \\ + \production{import} & \Bimport &::=& + \X{mod}{:}\Bname~~\X{nm}{:}\Bname~~d{:}\Bimportdesc + &\Rightarrow& \{ \IMODULE~\X{mod}, \INAME~\X{nm}, \IDESC~d \} \\ + \production{import description} & \Bimportdesc &::=& + \hex{00}~~x{:}\Btypeidx &\Rightarrow& \IDFUNC~x \\ &&|& + \hex{01}~~\X{tt}{:}\Btabletype &\Rightarrow& \IDTABLE~\X{tt} \\ &&|& + \hex{02}~~\X{mt}{:}\Bmemtype &\Rightarrow& \IDMEM~\X{mt} \\ &&|& + \hex{03}~~\X{gt}{:}\Bglobaltype &\Rightarrow& \IDGLOBAL~\X{gt} \\ + \end{array} + + +.. index:: ! function section, function, type index, function type + pair: binary format; function + pair: section; function +.. _binary-funcsec: + +Function Section +~~~~~~~~~~~~~~~~ + +The *function section* has the id 3. +It decodes into a vector of :ref:`type indices ` that represent the |FTYPE| fields of the :ref:`functions ` in the |MFUNCS| component of a :ref:`module `. +The |FLOCALS| and |FBODY| fields of the respective functions are encoded separately in the :ref:`code section `. + +.. math:: + \begin{array}{llclll} + \production{function section} & \Bfuncsec &::=& + x^\ast{:}\Bsection_3(\Bvec(\Btypeidx)) &\Rightarrow& x^\ast \\ + \end{array} + + +.. index:: ! table section, table, table type + pair: binary format; table + pair: section; table +.. _binary-table: +.. _binary-tablesec: + +Table Section +~~~~~~~~~~~~~ + +The *table section* has the id 4. +It decodes into a vector of :ref:`tables ` that represent the |MTABLES| component of a :ref:`module `. + +.. math:: + \begin{array}{llclll} + \production{table section} & \Btablesec &::=& + \X{tab}^\ast{:}\Bsection_4(\Bvec(\Btable)) &\Rightarrow& \X{tab}^\ast \\ + \production{table} & \Btable &::=& + \X{tt}{:}\Btabletype &\Rightarrow& \{ \TTYPE~\X{tt} \} \\ + \end{array} + + +.. index:: ! memory section, memory, memory type + pair: binary format; memory + pair: section; memory +.. _binary-mem: +.. _binary-memsec: + +Memory Section +~~~~~~~~~~~~~~ + +The *memory section* has the id 5. +It decodes into a vector of :ref:`memories ` that represent the |MMEMS| component of a :ref:`module `. + +.. math:: + \begin{array}{llclll} + \production{memory section} & \Bmemsec &::=& + \X{mem}^\ast{:}\Bsection_5(\Bvec(\Bmem)) &\Rightarrow& \X{mem}^\ast \\ + \production{memory} & \Bmem &::=& + \X{mt}{:}\Bmemtype &\Rightarrow& \{ \MTYPE~\X{mt} \} \\ + \end{array} + + +.. index:: ! global section, global, global type, expression + pair: binary format; global + pair: section; global +.. _binary-global: +.. _binary-globalsec: + +Global Section +~~~~~~~~~~~~~~ + +The *global section* has the id 6. +It decodes into a vector of :ref:`globals ` that represent the |MGLOBALS| component of a :ref:`module `. + +.. math:: + \begin{array}{llclll} + \production{global section} & \Bglobalsec &::=& + \X{glob}^\ast{:}\Bsection_6(\Bvec(\Bglobal)) &\Rightarrow& \X{glob}^\ast \\ + \production{global} & \Bglobal &::=& + \X{gt}{:}\Bglobaltype~~e{:}\Bexpr + &\Rightarrow& \{ \GTYPE~\X{gt}, \GINIT~e \} \\ + \end{array} + + +.. index:: ! export section, export, name, index, function index, table index, memory index, global index + pair: binary format; export + pair: section; export +.. _binary-export: +.. _binary-exportdesc: +.. _binary-exportsec: + +Export Section +~~~~~~~~~~~~~~ + +The *export section* has the id 7. +It decodes into a vector of :ref:`exports ` that represent the |MEXPORTS| component of a :ref:`module `. + +.. math:: + \begin{array}{llclll} + \production{export section} & \Bexportsec &::=& + \X{ex}^\ast{:}\Bsection_7(\Bvec(\Bexport)) &\Rightarrow& \X{ex}^\ast \\ + \production{export} & \Bexport &::=& + \X{nm}{:}\Bname~~d{:}\Bexportdesc + &\Rightarrow& \{ \ENAME~\X{nm}, \EDESC~d \} \\ + \production{export description} & \Bexportdesc &::=& + \hex{00}~~x{:}\Bfuncidx &\Rightarrow& \EDFUNC~x \\ &&|& + \hex{01}~~x{:}\Btableidx &\Rightarrow& \EDTABLE~x \\ &&|& + \hex{02}~~x{:}\Bmemidx &\Rightarrow& \EDMEM~x \\ &&|& + \hex{03}~~x{:}\Bglobalidx &\Rightarrow& \EDGLOBAL~x \\ + \end{array} + + +.. index:: ! start section, start function, function index + pair: binary format; start function + single: section; start + single: start function; section +.. _binary-start: +.. _binary-startsec: + +Start Section +~~~~~~~~~~~~~ + +The *start section* has the id 8. +It decodes into an optional :ref:`start function ` that represents the |MSTART| component of a :ref:`module `. + +.. math:: + \begin{array}{llclll} + \production{start section} & \Bstartsec &::=& + \X{st}^?{:}\Bsection_8(\Bstart) &\Rightarrow& \X{st}^? \\ + \production{start function} & \Bstart &::=& + x{:}\Bfuncidx &\Rightarrow& \{ \SFUNC~x \} \\ + \end{array} + + +.. index:: ! element section, element, table index, expression, function index + pair: binary format; element + pair: section; element + single: table; element + single: element; segment +.. _binary-elem: +.. _binary-elemsec: + +Element Section +~~~~~~~~~~~~~~~ + +The *element section* has the id 9. +It decodes into a vector of :ref:`element segments ` that represent the |MELEM| component of a :ref:`module `. + +.. math:: + \begin{array}{llclll} + \production{element section} & \Belemsec &::=& + \X{seg}^\ast{:}\Bsection_9(\Bvec(\Belem)) &\Rightarrow& \X{seg} \\ + \production{element segment} & \Belem &::=& + x{:}\Btableidx~~e{:}\Bexpr~~y^\ast{:}\Bvec(\Bfuncidx) + &\Rightarrow& \{ \ETABLE~x, \EOFFSET~e, \EINIT~y^\ast \} \\ + \end{array} + + +.. index:: ! code section, function, local, type index, function type + pair: binary format; function + pair: binary format; local + pair: section; code +.. _binary-code: +.. _binary-func: +.. _binary-local: +.. _binary-codesec: + +Code Section +~~~~~~~~~~~~ + +The *code section* has the id 10. +It decodes into a vector of *code* entries that are pairs of :ref:`value type ` vectors and :ref:`expressions `. +They represent the |FLOCALS| and |FBODY| field of the :ref:`functions ` in the |MFUNCS| component of a :ref:`module `. +The |FTYPE| fields of the respective functions are encoded separately in the :ref:`function section `. + +The encoding of each code entry consists of + +* the |U32| *size* of the function code in bytes, +* the actual *function code*, which in turn consists of + + * the declaration of *locals*, + * the function *body* as an :ref:`expression `. + +Local declarations are compressed into a vector whose entries consist of + +* a |U32| *count*, +* a :ref:`value type `, + +denoting *count* locals of the same value type. + +.. math:: + \begin{array}{llclll@{\qquad}l} + \production{code section} & \Bcodesec &::=& + \X{code}^\ast{:}\Bsection_{10}(\Bvec(\Bcode)) + &\Rightarrow& \X{code}^\ast \\ + \production{code} & \Bcode &::=& + \X{size}{:}\Bu32~~\X{code}{:}\Bfunc + &\Rightarrow& \X{code} & (\iff \X{size} = ||\Bfunc||) \\ + \production{function} & \Bfunc &::=& + (t^\ast)^\ast{:}\Bvec(\Blocals)~~e{:}\Bexpr + &\Rightarrow& \concat((t^\ast)^\ast), e^\ast + & (\iff |\concat((t^\ast)^\ast)| < 2^{32}) \\ + \production{locals} & \Blocals &::=& + n{:}\Bu32~~t{:}\Bvaltype &\Rightarrow& t^n \\ + \end{array} + +Here, :math:`\X{code}` ranges over pairs :math:`(\valtype^\ast, \expr)`. +The meta function :math:`\concat((t^\ast)^\ast)` concatenates all sequences :math:`t_i^\ast` in :math:`(t^\ast)^\ast`. +Any code for which the length of the resulting sequence is out of bounds of the maximum size of a :ref:`vector ` is malformed. + +.. note:: + Like with :ref:`sections `, the code :math:`\X{size}` is not needed for decoding, but can be used to skip functions when navigating through a binary. + The module is malformed if a size does not match the length of the respective function code. + + +.. index:: ! data section, data, memory, memory index, expression, byte + pair: binary format; data + pair: section; data + single: memory; data + single: data; segment +.. _binary-data: +.. _binary-datasec: + +Data Section +~~~~~~~~~~~~ + +The *data section* has the id 11. +It decodes into a vector of :ref:`data segments ` that represent the |MDATA| component of a :ref:`module `. + +.. math:: + \begin{array}{llclll} + \production{data section} & \Bdatasec &::=& + \X{seg}^\ast{:}\Bsection_{11}(\Bvec(\Bdata)) &\Rightarrow& \X{seg} \\ + \production{data segment} & \Bdata &::=& + x{:}\Bmemidx~~e{:}\Bexpr~~b^\ast{:}\Bvec(\Bbyte) + &\Rightarrow& \{ \DMEM~x, \DOFFSET~e, \DINIT~b^\ast \} \\ + \end{array} + + +.. index:: module, section, type definition, function type, function, table, memory, global, element, data, start function, import, export, context, version + pair: binary format; module +.. _binary-magic: +.. _binary-version: +.. _binary-module: + +Modules +~~~~~~~ + +The encoding of a :ref:`module ` starts with a preamble containing a 4-byte magic number (the string :math:`\text{\backslash0asm}`) and a version field. +The current version of the WebAssembly binary format is 1. + +The preamble is followed by a sequence of :ref:`sections `. +:ref:`Custom sections ` may be inserted at any place in this sequence, +while other sections must occur at most once and in the prescribed order. +All sections can be empty. + +The lengths of vectors produced by the (possibly empty) :ref:`function ` and :ref:`code ` section must match up. + +.. math:: + \begin{array}{llcllll} + \production{magic} & \Bmagic &::=& + \hex{00}~\hex{61}~\hex{73}~\hex{6D} \\ + \production{version} & \Bversion &::=& + \hex{01}~\hex{00}~\hex{00}~\hex{00} \\ + \production{module} & \Bmodule &::=& + \Bmagic \\ &&& + \Bversion \\ &&& + \Bcustomsec^\ast \\ &&& + \functype^\ast{:\,}\Btypesec \\ &&& + \Bcustomsec^\ast \\ &&& + \import^\ast{:\,}\Bimportsec \\ &&& + \Bcustomsec^\ast \\ &&& + \typeidx^n{:\,}\Bfuncsec \\ &&& + \Bcustomsec^\ast \\ &&& + \table^\ast{:\,}\Btablesec \\ &&& + \Bcustomsec^\ast \\ &&& + \mem^\ast{:\,}\Bmemsec \\ &&& + \Bcustomsec^\ast \\ &&& + \global^\ast{:\,}\Bglobalsec \\ &&& + \Bcustomsec^\ast \\ &&& + \export^\ast{:\,}\Bexportsec \\ &&& + \Bcustomsec^\ast \\ &&& + \start^?{:\,}\Bstartsec \\ &&& + \Bcustomsec^\ast \\ &&& + \elem^\ast{:\,}\Belemsec \\ &&& + \Bcustomsec^\ast \\ &&& + \X{code}^n{:\,}\Bcodesec \\ &&& + \Bcustomsec^\ast \\ &&& + \data^\ast{:\,}\Bdatasec \\ &&& + \Bcustomsec^\ast + \quad\Rightarrow\quad \{~ + \begin{array}[t]{@{}l@{}} + \MTYPES~\functype^\ast, \\ + \MFUNCS~\func^n, \\ + \MTABLES~\table^\ast, \\ + \MMEMS~\mem^\ast, \\ + \MGLOBALS~\global^\ast, \\ + \MELEM~\elem^\ast, \\ + \MDATA~\data^\ast, \\ + \MSTART~\start^?, \\ + \MIMPORTS~\import^\ast, \\ + \MEXPORTS~\export^\ast ~\} \\ + \end{array} \\ + \end{array} + +where for each :math:`t_i^\ast, e_i` in :math:`\X{code}^n`, + +.. math:: + \func^n[i] = \{ \FTYPE~\typeidx^n[i], \FLOCALS~t_i^\ast, \FBODY~e_i \} ) \\ + +.. note:: + The version of the WebAssembly binary format may increase in the future + if backward-incompatible changes have to be made to the format. + However, such changes are expected to occur very infrequently, if ever. + The binary format is intended to be forward-compatible, + such that future extensions can be made without incrementing its version. diff --git a/document/core/binary/types.rst b/document/core/binary/types.rst new file mode 100644 index 00000000..c114211b --- /dev/null +++ b/document/core/binary/types.rst @@ -0,0 +1,140 @@ +.. index:: type + pair: binary format; type +.. _binary-type: + +Types +----- + +.. index:: value type + pair: binary format; value type +.. _binary-valtype: + +Value Types +~~~~~~~~~~~ + +:ref:`Value types ` are encoded by a single byte. + +.. math:: + \begin{array}{llclll@{\qquad\qquad}l} + \production{value type} & \Bvaltype &::=& + \hex{7F} &\Rightarrow& \I32 \\ &&|& + \hex{7E} &\Rightarrow& \I64 \\ &&|& + \hex{7D} &\Rightarrow& \F32 \\ &&|& + \hex{7C} &\Rightarrow& \F64 \\ + \end{array} + +.. note:: + In future versions of WebAssembly, value types may include types denoted by :ref:`type indices `. + Thus, the binary format for types corresponds to the |SignedLEB128|_ :ref:`encoding ` of small negative :math:`\sN` values, so that they can coexist with (positive) type indices in the future. + + +.. index:: result type, value type + pair: binary format; result type +.. _binary-blocktype: +.. _binary-resulttype: + +Result Types +~~~~~~~~~~~~ + +The only :ref:`result types ` occurring in the binary format are the types of blocks. These are encoded in special compressed form, by either the byte :math:`\hex{40}` indicating the empty type or as a single :ref:`value type `. + +.. math:: + \begin{array}{llclll@{\qquad\qquad}l} + \production{result type} & \Bblocktype &::=& + \hex{40} &\Rightarrow& [] \\ &&|& + t{:}\Bvaltype &\Rightarrow& [t] \\ + \end{array} + +.. note:: + In future versions of WebAssembly, this scheme may be extended to support multiple results or more general block types. + + +.. index:: function type, value type, result type + pair: binary format; function type +.. _binary-functype: + +Function Types +~~~~~~~~~~~~~~ + +:ref:`Function types ` are encoded by the byte :math:`\hex{60}` followed by the respective :ref:`vectors ` of parameter and result types. + +.. math:: + \begin{array}{llclll@{\qquad\qquad}l} + \production{function type} & \Bfunctype &::=& + \hex{60}~~t_1^\ast{:\,}\Bvec(\Bvaltype)~~t_2^\ast{:\,}\Bvec(\Bvaltype) + &\Rightarrow& [t_1^\ast] \to [t_2^\ast] \\ + \end{array} + + +.. index:: limits + pair: binary format; limits +.. _binary-limits: + +Limits +~~~~~~ + +:ref:`Limits ` are encoded with a preceding flag indicating whether a maximum is present. + +.. math:: + \begin{array}{llclll} + \production{limits} & \Blimits &::=& + \hex{00}~~n{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~\epsilon \} \\ &&|& + \hex{01}~~n{:}\Bu32~~m{:}\Bu32 &\Rightarrow& \{ \LMIN~n, \LMAX~m \} \\ + \end{array} + + +.. index:: memory type, limits, page size + pair: binary format; memory type +.. _binary-memtype: + +Memory Types +~~~~~~~~~~~~ + +:ref:`Memory types ` are encoded with their :ref:`limits `. + +.. math:: + \begin{array}{llclll@{\qquad\qquad}l} + \production{memory type} & \Bmemtype &::=& + \X{lim}{:}\Blimits &\Rightarrow& \X{lim} \\ + \end{array} + + +.. index:: table type, element type, limits + pair: binary format; table type + pair: binary format; element type +.. _binary-elemtype: +.. _binary-tabletype: + +Table Types +~~~~~~~~~~~ + +:ref:`Table types ` are encoded with their :ref:`limits ` and a constant byte indicating their :ref:`element type `. + +.. math:: + \begin{array}{llclll} + \production{table type} & \Btabletype &::=& + \X{et}{:}\Belemtype~~\X{lim}{:}\Blimits &\Rightarrow& \X{lim}~\X{et} \\ + \production{element type} & \Belemtype &::=& + \hex{70} &\Rightarrow& \FUNCREF \\ + \end{array} + + +.. index:: global type, mutability, value type + pair: binary format; global type + pair: binary format; mutability +.. _binary-mut: +.. _binary-globaltype: + +Global Types +~~~~~~~~~~~~ + +:ref:`Global types ` are encoded by their :ref:`value type ` and a flag for their :ref:`mutability `. + +.. math:: + \begin{array}{llclll} + \production{global type} & \Bglobaltype &::=& + t{:}\Bvaltype~~m{:}\Bmut &\Rightarrow& m~t \\ + \production{mutability} & \Bmut &::=& + \hex{00} &\Rightarrow& \MCONST \\ &&|& + \hex{01} &\Rightarrow& \MVAR \\ + \end{array} diff --git a/document/core/binary/values.rst b/document/core/binary/values.rst new file mode 100644 index 00000000..c6268624 --- /dev/null +++ b/document/core/binary/values.rst @@ -0,0 +1,148 @@ +.. index:: value + pair: binary format; value +.. _binary-value: + +Values +------ + + +.. index:: byte + pair: binary format; byte +.. _binary-byte: + +Bytes +~~~~~ + +:ref:`Bytes ` encode themselves. + +.. math:: + \begin{array}{llcll@{\qquad}l} + \production{byte} & \Bbyte &::=& + \hex{00} &\Rightarrow& \hex{00} \\ &&|&& + \dots \\ &&|& + \hex{FF} &\Rightarrow& \hex{FF} \\ + \end{array} + + +.. index:: integer, unsigned integer, signed integer, uninterpreted integer, LEB128, two's complement + pair: binary format; integer + pair: binary format; unsigned integer + pair: binary format; signed integer + pair: binary format; uninterpreted integer +.. _binary-sint: +.. _binary-uint: +.. _binary-int: + +Integers +~~~~~~~~ + +All :ref:`integers ` are encoded using the |LEB128|_ variable-length integer encoding, in either unsigned or signed variant. + +:ref:`Unsigned integers ` are encoded in |UnsignedLEB128|_ format. +As an additional constraint, the total number of bytes encoding a value of type :math:`\uN` must not exceed :math:`\F{ceil}(N/7)` bytes. + +.. math:: + \begin{array}{llclll@{\qquad}l} + \production{unsigned integer} & \BuN &::=& + n{:}\Bbyte &\Rightarrow& n & (\iff n < 2^7 \wedge n < 2^N) \\ &&|& + n{:}\Bbyte~~m{:}\BuX{(N\B{-7})} &\Rightarrow& + 2^7\cdot m + (n-2^7) & (\iff n \geq 2^7 \wedge N > 7) \\ + \end{array} + +:ref:`Signed integers ` are encoded in |SignedLEB128|_ format, which uses a two's complement representation. +As an additional constraint, the total number of bytes encoding a value of type :math:`\sN` must not exceed :math:`\F{ceil}(N/7)` bytes. + +.. math:: + \begin{array}{llclll@{\qquad}l} + \production{signed integer} & \BsN &::=& + n{:}\Bbyte &\Rightarrow& n & (\iff n < 2^6 \wedge n < 2^{N-1}) \\ &&|& + n{:}\Bbyte &\Rightarrow& n-2^7 & (\iff 2^6 \leq n < 2^7 \wedge n \geq 2^7-2^{N-1}) \\ &&|& + n{:}\Bbyte~~m{:}\BsX{(N\B{-7})} &\Rightarrow& + 2^7\cdot m + (n-2^7) & (\iff n \geq 2^7 \wedge N > 7) \\ + \end{array} + +:ref:`Uninterpreted integers ` are encoded as signed integers. + +.. math:: + \begin{array}{llclll@{\qquad\qquad}l} + \production{uninterpreted integer} & \BiN &::=& + n{:}\BsN &\Rightarrow& i & (\iff n = \signed_{\iN}(i)) + \end{array} + +.. note:: + The side conditions :math:`N > 7` in the productions for non-terminal bytes of the :math:`\uX{}` and :math:`\sX{}` encodings restrict the encoding's length. + However, "trailing zeros" are still allowed within these bounds. + For example, :math:`\hex{03}` and :math:`\hex{83}~\hex{00}` are both well-formed encodings for the value :math:`3` as a |u8|. + Similarly, either of :math:`\hex{7e}` and :math:`\hex{FE}~\hex{7F}` and :math:`\hex{FE}~\hex{FF}~\hex{7F}` are well-formed encodings of the value :math:`-2` as a |s16|. + + The side conditions on the value :math:`n` of terminal bytes further enforce that + any unused bits in these bytes must be :math:`0` for positive values and :math:`1` for negative ones. + For example, :math:`\hex{83}~\hex{10}` is malformed as a |u8| encoding. + Similarly, both :math:`\hex{83}~\hex{3E}` and :math:`\hex{FF}~\hex{7B}` are malformed as |s8| encodings. + + +.. index:: floating-point number, little endian + pair: binary format; floating-point number +.. _binary-float: + +Floating-Point +~~~~~~~~~~~~~~ + +:ref:`Floating-point ` values are encoded directly by their |IEEE754|_ (Section 3.4) bit pattern in |LittleEndian|_ byte order: + +.. math:: + \begin{array}{llclll@{\qquad\qquad}l} + \production{floating-point value} & \BfN &::=& + b^\ast{:\,}\Bbyte^{N/8} &\Rightarrow& \bytes_{\fN}^{-1}(b^\ast) \\ + \end{array} + + +.. index:: name, byte, Unicode, ! UTF-8 + pair: binary format; name +.. _binary-utf8: +.. _binary-name: + +Names +~~~~~ + +:ref:`Names ` are encoded as a :ref:`vector ` of bytes containing the |Unicode|_ (Section 3.9) UTF-8 encoding of the name's character sequence. + +.. math:: + \begin{array}{llclllll} + \production{name} & \Bname &::=& + b^\ast{:}\Bvec(\Bbyte) &\Rightarrow& \name + && (\iff \utf8(\name) = b^\ast) \\ + \end{array} + +The auxiliary |utf8| function expressing this encoding is defined as follows: + +.. math:: + \begin{array}{@{}l@{}} + \begin{array}{@{}lcl@{\qquad}l@{}} + \utf8(c^\ast) &=& (\utf8(c))^\ast \\[1ex] + \utf8(c) &=& b & + (\begin{array}[t]{@{}c@{~}l@{}} + \iff & c < \unicode{80} \\ + \wedge & c = b) \\ + \end{array} \\ + \utf8(c) &=& b_1~b_2 & + (\begin{array}[t]{@{}c@{~}l@{}} + \iff & \unicode{80} \leq c < \unicode{800} \\ + \wedge & c = 2^6(b_1-\hex{C0})+(b_2-\hex{80})) \\ + \end{array} \\ + \utf8(c) &=& b_1~b_2~b_3 & + (\begin{array}[t]{@{}c@{~}l@{}} + \iff & \unicode{800} \leq c < \unicode{D800} \vee \unicode{E000} \leq c < \unicode{10000} \\ + \wedge & c = 2^{12}(b_1-\hex{E0})+2^6(b_2-\hex{80})+(b_3-\hex{80})) \\ + \end{array} \\ + \utf8(c) &=& b_1~b_2~b_3~b_4 & + (\begin{array}[t]{@{}c@{~}l@{}} + \iff & \unicode{10000} \leq c < \unicode{110000} \\ + \wedge & c = 2^{18}(b_1-\hex{F0})+2^{12}(b_2-\hex{80})+2^6(b_3-\hex{80})+(b_4-\hex{80})) \\ + \end{array} \\ + \end{array} \\ + \where b_2, b_3, b_4 < \hex{C0} \\ + \end{array} + +.. note:: + Unlike in some other formats, name strings are not 0-terminated. diff --git a/document/core/conf.py b/document/core/conf.py new file mode 100644 index 00000000..d410ee04 --- /dev/null +++ b/document/core/conf.py @@ -0,0 +1,480 @@ +# -*- coding: utf-8 -*- +# +# WebAssembly documentation build configuration file, created by +# sphinx-quickstart on Mon Nov 21 11:32:49 2016. +# +# This file is execfile()d with the current directory set to its +# containing dir. +# +# Note that not all possible configuration values are present in this +# autogenerated file. +# +# All configuration values have a default; values that are commented out +# serve to show the default. + +# If extensions (or modules to document with autodoc) are in another directory, +# add these directories to sys.path here. If the directory is relative to the +# documentation root, use os.path.abspath to make it absolute, like shown here. +import os +import sys +pwd = os.path.abspath('.') +sys.path.insert(0, pwd + '/util') + +# -- General configuration ------------------------------------------------ + +# If your documentation needs a minimal Sphinx version, state it here. +# +needs_sphinx = '1.4' + +# Add any Sphinx extension module names here, as strings. They can be +# extensions coming with Sphinx (named 'sphinx.ext.*') or your custom +# ones. +extensions = [ + 'sphinx.ext.todo', + 'sphinx.ext.coverage', + 'sphinx.ext.mathjax', + 'sphinx.ext.ifconfig', + 'sphinx.ext.githubpages', + 'mathdef', + 'pseudo-lexer' +] + +# Add any paths that contain templates here, relative to this directory. +templates_path = ['_templates'] + +# The suffix(es) of source filenames. +# You can specify multiple suffix as a list of string: +# +source_suffix = ['.rst'] + +# The encoding of source files. +# +# source_encoding = 'utf-8-sig' + +# The master toctree document. +master_doc = 'index' + +# General information about the project. +name = 'WebAssembly' +project = u'WebAssembly' +title = u'WebAssembly Specification' +copyright = u'2017, WebAssembly Community Group' +author = u'WebAssembly Community Group' +editor = u'Andreas Rossberg (editor)' +logo = 'static/webassembly.png' + +# The version info for the project you're documenting, acts as replacement for +# |version| and |release|, also used in various other places throughout the +# built documents. +# +# The short X.Y version. +version = u'1.0' +# The full version, including alpha/beta/rc tags. +release = version + '' + +# The language for content autogenerated by Sphinx. Refer to documentation +# for a list of supported languages. +# +# This is also used if you do content translation via gettext catalogs. +# Usually you set "language" from the command line for these cases. +language = None + +# There are two options for replacing |today|: either, you set today to some +# non-false value, then it is used: +# +# today = '' +# +# Else, today_fmt is used as the format for a strftime call. +# +# today_fmt = '%B %d, %Y' + +# List of patterns, relative to source directory, that match files and +# directories to ignore when looking for source files. +# This patterns also effect to html_static_path and html_extra_path +exclude_patterns = ['_build', 'Thumbs.db', '.DS_Store'] + +# The reST default role (used for this markup: `text`) to use for all +# documents. +# +# default_role = None + +# If true, '()' will be appended to :func: etc. cross-reference text. +# +# add_function_parentheses = True + +# If true, the current module name will be prepended to all description +# unit titles (such as .. function::). +# +# add_module_names = True + +# If true, sectionauthor and moduleauthor directives will be shown in the +# output. They are ignored by default. +# +# show_authors = False + +# The name of the Pygments (syntax highlighting) style to use. +pygments_style = 'sphinx' + +# A list of ignored prefixes for module index sorting. +# modindex_common_prefix = [] + +# If true, keep warnings as "system message" paragraphs in the built documents. +# keep_warnings = False + +# If true, `todo` and `todoList` produce output, else they produce nothing. +todo_include_todos = True + + +# -- Options for HTML output ---------------------------------------------- + +# The theme to use for HTML and HTML Help pages. See the documentation for +# a list of builtin themes. +# +html_theme = 'alabaster' + +# Theme options are theme-specific and customize the look and feel of a theme +# further. For a list of options available for each theme, see the +# documentation. +# +html_theme_options = { + 'logo': logo, + 'logo_name': 'WebAssembly', + 'description': 'WebAssembly Specification', + 'fixed_sidebar': True, + 'sidebar_width': '260px', + 'sidebar_collapse': True, + 'show_powered_by': False, + 'extra_nav_links': { + 'Index': 'BASEDIR/genindex.html', + 'Download as PDF': 'BASEDIR/_download/' + name + '.pdf' + }, +} + +html_sidebars = { + '**': [ + # 'about.html', + 'navigation.html', + # 'relations.html', + 'searchbox.html', + ] +} + + +# Add any paths that contain custom themes here, relative to this directory. +# html_theme_path = [] + +# The name for this set of Sphinx documents. +# " v documentation" by default. +# +html_title = project + u' ' + release + +# A shorter title for the navigation bar. Default is the same as html_title. +# +# html_short_title = None + +# The name of an image file (relative to this directory) to place at the top +# of the sidebar. +# +html_logo = logo + +# The name of an image file (relative to this directory) to use as a favicon of +# the docs. This file should be a Windows icon file (.ico) being 16x16 or 32x32 +# pixels large. +# +# html_favicon = None + +# Add any paths that contain custom static files (such as style sheets) here, +# relative to this directory. They are copied after the builtin static files, +# so a file named "default.css" will overwrite the builtin "default.css". +html_static_path = ['_static', 'static/custom.css'] + +# Add any extra paths that contain custom files (such as robots.txt or +# .htaccess) here, relative to this directory. These files are copied +# directly to the root of the documentation. +# +# html_extra_path = [] + +# If not None, a 'Last updated on:' timestamp is inserted at every page +# bottom, using the given strftime format. +# The empty string is equivalent to '%b %d, %Y'. +# +# html_last_updated_fmt = None + +# If true, SmartyPants will be used to convert quotes and dashes to +# typographically correct entities. +# +# html_use_smartypants = True + +# Additional templates that should be rendered to pages, maps page names to +# template names. +# +# html_additional_pages = {} + +# If false, no module index is generated. +# +html_domain_indices = False + +# If false, no index is generated. +# +html_use_index = True + +# If true, the index is split into individual pages for each letter. +# +html_split_index = False + +# If true, the reST sources are included in the HTML build as _sources/name. The default is True. +# +html_copy_source = False + +# If true, links to the reST sources are added to the pages. +# +html_show_sourcelink = False + +# If true, "Created using Sphinx" is shown in the HTML footer. Default is True. +# +html_show_sphinx = False + +# If true, "(C) Copyright ..." is shown in the HTML footer. Default is True. +# +html_show_copyright = True + +# If this is not None, a ‘Last updated on:’ timestamp is inserted at every +# page bottom, using the given strftime() format. +# +html_last_updated_fmt = '%F' + +# If true, an OpenSearch description file will be output, and all pages will +# contain a tag referring to it. The value of this option must be the +# base URL from which the finished HTML is served. +# +# html_use_opensearch = '' + +# This is the file name suffix for HTML files (e.g. ".xhtml"). +# +# html_file_suffix = None + +# Language to be used for generating the HTML full-text search index. +# Sphinx supports the following languages: +# 'da', 'de', 'en', 'es', 'fi', 'fr', 'hu', 'it', 'ja' +# 'nl', 'no', 'pt', 'ro', 'ru', 'sv', 'tr', 'zh' +# +# html_search_language = 'en' + +# A dictionary with options for the search language support, empty by default. +# 'ja' uses this config value. +# 'zh' user can custom change `jieba` dictionary path. +# +# html_search_options = {'type': 'default'} + +# The name of a javascript file (relative to the configuration directory) that +# implements a search results scorer. If empty, the default will be used. +# +# html_search_scorer = 'scorer.js' + +# Output file base name for HTML help builder. +# +htmlhelp_basename = 'WebAssemblydoc' + + +# -- Options for LaTeX output --------------------------------------------- + +latex_elements = { + # The paper size ('a4paper' or 'letterpaper'). + 'papersize': 'a4paper', + + # The font size ('10pt', '11pt' or '12pt'). + 'pointsize': '10pt', + + # Additional stuff for the LaTeX preamble. + 'preamble': '', + + # Latex figure (float) alignment + 'figure_align': 'htbp', + + # Fancy chapters [Bjarne, Sonny, Lenny, Glenn, Conny, Rejne] + 'fncychap': '\\usepackage[Sonny]{fncychap}', +} + +# Grouping the document tree into LaTeX files. List of tuples +# (source start file, target name, title, +# author, documentclass [howto, manual, or own class]). +latex_documents = [ + ( master_doc, + name + '.tex', + title, + author + '\\\\ \\hfill\\large ' + editor, + 'manual' + ), +] + +# The name of an image file (relative to this directory) to place at the top of +# the title page. +# +latex_logo = logo + +# For "manual" documents [part, chapter, or section]. +# +latex_toplevel_sectioning = 'chapter' + +# If true, show page references after internal links. +# +latex_show_pagerefs = False + +# How to show URL addresses after external links [no, footnote, inline]. +# +latex_show_urls = 'footnote' + +# Documents to append as an appendix to all manuals. +# +# latex_appendices = [] + +# It false, will not define \strong, \code, \titleref, \crossref ... but only +# \sphinxstrong, ..., \sphinxtitleref, ... To help avoid clash with user added +# packages. +# +# latex_keep_old_macro_names = True + +# If false, no module index is generated. +# +latex_domain_indices = False + + +# -- Options for manual page output --------------------------------------- + +# One entry per manual page. List of tuples +# (source start file, name, description, authors, manual section). +man_pages = [ + ( master_doc, + name, + title, + [author], + 1 + ) +] + +# If true, show URL addresses after external links. +# +# man_show_urls = False + + +# -- Options for Texinfo output ------------------------------------------- + +# Grouping the document tree into Texinfo files. List of tuples +# (source start file, target name, title, author, +# dir menu entry, description, category) +texinfo_documents = [ + ( master_doc, + name, + title, + author, + name, + 'A portable low-level execution format.', + 'Virtual Machine' + ), +] + +# Documents to append as an appendix to all manuals. +# +# texinfo_appendices = [] + +# If false, no module index is generated. +# +texinfo_domain_indices = False + +# How to display URL addresses: 'footnote', 'no', or 'inline'. +# +# texinfo_show_urls = 'footnote' + +# If true, do not generate a @detailmenu in the "Top" node's menu. +# +# texinfo_no_detailmenu = False + + +# -- Options for Epub output ---------------------------------------------- + +# Bibliographic Dublin Core info. +epub_title = project +epub_author = author +epub_publisher = author +epub_copyright = copyright + +# The basename for the epub file. It defaults to the project name. +# epub_basename = project + +# The HTML theme for the epub output. Since the default themes are not +# optimized for small screen space, using the same theme for HTML and epub +# output is usually not wise. This defaults to 'epub', a theme designed to save +# visual space. +# +# epub_theme = 'epub' + +# The language of the text. It defaults to the language option +# or 'en' if the language is not set. +# +# epub_language = '' + +# The scheme of the identifier. Typical schemes are ISBN or URL. +# epub_scheme = '' + +# The unique identifier of the text. This can be a ISBN number +# or the project homepage. +# +# epub_identifier = '' + +# A unique identification for the text. +# +# epub_uid = '' + +# A tuple containing the cover image and cover page html template filenames. +# +# epub_cover = () + +# A sequence of (type, uri, title) tuples for the guide element of content.opf. +# +# epub_guide = () + +# HTML files that should be inserted before the pages created by sphinx. +# The format is a list of tuples containing the path and title. +# +# epub_pre_files = [] + +# HTML files that should be inserted after the pages created by sphinx. +# The format is a list of tuples containing the path and title. +# +# epub_post_files = [] + +# A list of files that should not be packed into the epub file. +epub_exclude_files = ['search.html'] + +# The depth of the table of contents in toc.ncx. +# +# epub_tocdepth = 3 + +# Allow duplicate toc entries. +# +# epub_tocdup = True + +# Choose between 'default' and 'includehidden'. +# +# epub_tocscope = 'default' + +# Fix unsupported image types using the Pillow. +# +# epub_fix_images = False + +# Scale large images. +# +# epub_max_image_width = 0 + +# How to display URL addresses: 'footnote', 'no', or 'inline'. +# +# epub_show_urls = 'inline' + +# If false, no index is generated. +# +# epub_use_index = True + +# Macros +rst_prolog = """ +.. include:: /""" + pwd + """/util/macros.def +""" diff --git a/document/core/exec/conventions.rst b/document/core/exec/conventions.rst new file mode 100644 index 00000000..807239b0 --- /dev/null +++ b/document/core/exec/conventions.rst @@ -0,0 +1,134 @@ +.. index:: ! execution, stack, store + +Conventions +----------- + +WebAssembly code is *executed* when :ref:`instantiating ` a module or :ref:`invoking ` an :ref:`exported ` function on the resulting module :ref:`instance `. + +Execution behavior is defined in terms of an *abstract machine* that models the *program state*. +It includes a *stack*, which records operand values and control constructs, and an abstract *store* containing global state. + +For each instruction, there is a rule that specifies the effect of its execution on the program state. +Furthermore, there are rules describing the instantiation of a module. +As with :ref:`validation `, all rules are given in two *equivalent* forms: + +1. In *prose*, describing the execution in intuitive form. +2. In *formal notation*, describing the rule in mathematical form. [#cite-pldi2017]_ + +.. note:: + As with validation, the prose and formal rules are equivalent, + so that understanding of the formal notation is *not* required to read this specification. + The formalism offers a more concise description in notation that is used widely in programming languages semantics and is readily amenable to mathematical proof. + + +.. _exec-notation-textual: + +Prose Notation +~~~~~~~~~~~~~~ + +Execution is specified by stylised, step-wise rules for each :ref:`instruction ` of the :ref:`abstract syntax `. +The following conventions are adopted in stating these rules. + +* The execution rules implicitly assume a given :ref:`store ` :math:`S`. + +* The execution rules also assume the presence of an implicit :ref:`stack ` + that is modified by *pushing* or *popping* + :ref:`values `, :ref:`labels `, and :ref:`frames `. + +* Certain rules require the stack to contain at least one frame. + The most recent frame is referred to as the *current* frame. + +* Both the store and the current frame are mutated by *replacing* some of their components. + Such replacement is assumed to apply globally. + +* The execution of an instruction may *trap*, + in which case the entire computation is aborted and no further modifications to the store are performed by it. (Other computations can still be initiated afterwards.) + +* The execution of an instruction may also end in a *jump* to a designated target, + which defines the next instruction to execute. + +* Execution can *enter* and *exit* :ref:`instruction sequences ` that form :ref:`blocks `. + +* :ref:`Instruction sequences ` are implicitly executed in order, unless a trap or jump occurs. + +* In various places the rules contain *assertions* expressing crucial invariants about the program state. + + +.. index:: ! reduction rules, configuration, evaluation context +.. _exec-notation: + +Formal Notation +~~~~~~~~~~~~~~~ + +.. note:: + This section gives a brief explanation of the notation for specifying execution formally. + For the interested reader, a more thorough introduction can be found in respective text books. [#cite-tapl]_ + +The formal execution rules use a standard approach for specifying operational semantics, rendering them into *reduction rules*. +Every rule has the following general form: + +.. math:: + \X{configuration} \quad\stepto\quad \X{configuration} + +A *configuration* is a syntactic description of a program state. +Each rule specifies one *step* of execution. +As long as there is at most one reduction rule applicable to a given configuration, reduction -- and thereby execution -- is *deterministic*. +WebAssembly has only very few exceptions to this, which are noted explicitly in this specification. + +For WebAssembly, a configuration typically is a tuple :math:`(S; F; \instr^\ast)` consisting of the current :ref:`store ` :math:`S`, the :ref:`call frame ` :math:`F` of the current function, and the sequence of :ref:`instructions ` that is to be executed. +(A more precise definition is given :ref:`later `.) + +To avoid unnecessary clutter, the store :math:`S` and the frame :math:`F` are omitted from reduction rules that do not touch them. + +There is no separate representation of the :ref:`stack `. +Instead, it is conveniently represented as part of the configuration's instruction sequence. +In particular, :ref:`values ` are defined to coincide with |CONST| instructions, +and a sequence of |CONST| instructions can be interpreted as an operand "stack" that grows to the right. + +.. note:: + For example, the :ref:`reduction rule ` for the :math:`\I32.\ADD` instruction can be given as follows: + + .. math:: + (\I32.\CONST~n_1)~(\I32.\CONST~n_2)~\I32.\ADD \quad\stepto\quad (\I32.\CONST~(n_1 + n_2) \mod 2^{32}) + + Per this rule, two |CONST| instructions and the |ADD| instruction itself are removed from the instruction stream and replaced with one new |CONST| instruction. + This can be interpreted as popping two value off the stack and pushing the result. + + When no result is produced, an instruction reduces to the empty sequence: + + .. math:: + \NOP \quad\stepto\quad \epsilon + +:ref:`Labels