diff --git a/document/core/syntax/instrindex.rst b/document/core/appendix/index-instructions.rst similarity index 99% rename from document/core/syntax/instrindex.rst rename to document/core/appendix/index-instructions.rst index d6230dbb27..f5811e024f 100644 --- a/document/core/syntax/instrindex.rst +++ b/document/core/appendix/index-instructions.rst @@ -1,10 +1,11 @@ -.. _instrindex: +.. index:: instruction +.. _index-instr: Index of Instructions --------------------- =================================== ================ ========================================== ======================================== =============================================================== -Instruction Opcode Type Validation Execution +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 ` diff --git a/document/core/appendix/index-rules.rst b/document/core/appendix/index-rules.rst new file mode 100644 index 0000000000..83d5d514d6 --- /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 \ok` +: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:`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 : \resulttype` +: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 : \name` +:ref:`Export description ` :math:`C \vdashexportdesc \exportdesc \ok` +:ref:`Import ` :math:`C \vdashimport \import : \externtype` +:ref:`Import description ` :math:`C \vdashimportdesc \importdesc : \externtype` +:ref:`Module ` :math:`\vdashmodule \module : \externtype^\ast` +=============================================== =============================================================================== + + +.. index:: runtime + +Typing of Runtime Constructs +~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +=============================================== =============================================================================== +Construct Judgement +=============================================== =============================================================================== +:ref:`Module instruction ` :math:`S \vdashmoduleinstr \moduleinstr \ok` +:ref:`Function instance ` :math:`S \vdashfuncinst \funcinst : \resulttype` +: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` +:ref:`Value ` :math:`\vdashval \val : \valtype` +:ref:`External value ` :math:`S \vdashexternval \externval : \externtype` +=============================================== =============================================================================== + + +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 \stepto S';F';{\instr'}^\ast` +:ref:`Expression ` :math:`S;F;\expr \stepto^\ast S';F';\val^\ast` +:ref:`Module instruction ` :math:`S;\moduleinstr \stepto S';{\moduleinstr'}^\ast` +=============================================== =============================================================================== diff --git a/document/core/appendix/index-types.rst b/document/core/appendix/index-types.rst new file mode 100644 index 0000000000..972ae6b49a --- /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{7C}` .. :math:`\hex{71}` +:ref:`Element type ` |ANYFUNC| :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/properties.rst b/document/core/appendix/properties.rst index 2a0c06e6df..2473df9d0c 100644 --- a/document/core/appendix/properties.rst +++ b/document/core/appendix/properties.rst @@ -1,17 +1,726 @@ -Formal Properties ------------------ +.. 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. + +* 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 behaviour, + 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 ` as well as :ref:`module instructions `. [#pldi2017]_ -.. _bijective: -Representation +.. _module-context: +.. _valid-store: + +Store Validity ~~~~~~~~~~~~~~ -.. todo:: bijection between abstract and binary +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. -.. _soundness: -Validation -~~~~~~~~~~ -.. todo:: progress, preservation +.. 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 optional :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 Instance ` :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:: table type, table instance, limits, function address +.. _valid-tableinst: + +:ref:`Table Instance ` :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^?\}~\ANYFUNC`. + +.. 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^?\}~\ANYFUNC + } + + +.. index:: memory type, memory instance, limits, byte +.. _valid-meminst: + +:ref:`Memory Instance ` :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 Instance ` :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 Instance ` :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 Instance ` :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 `. + +Threads may either be regular threads executing sequences of :ref:`instructions `, or module threads executing :ref:`module instructions ` that represent an ongoing module instantiation. +Regular threads are classified by their :ref:`result type `. +Module threads on the other hand have no result, not even an empty one. +Consequently, threads and configurations are cumutavily classified by an *optional* result type, where :math:`\epsilon` classifies the thread as a module computation. + +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 :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 optional :ref:`result type ` :math:`[t^?]^?`. + +* Then the configuration is valid with the optional :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:: thread, module instruction + +:ref:`Threads ` :math:`\moduleinstr^\ast` +........................................................ + +* The current allowed return type must be empty. + +* Each :ref:`module instruction ` :math:`\moduleinstr_i` in :math:`\moduleinstr^\ast` must be :ref:`valid `. + +* Then the thread is valid with no :ref:`result type `. + +.. math:: + \frac{ + (S \vdashmoduleinstr \moduleinstr \ok)^\ast + }{ + S; \epsilon \vdashthread \moduleinstr^\ast : \epsilon + } + + +.. 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:: value, value type +.. _valid-val: + +:ref:`Values ` :math:`t.\CONST~c` +............................................. + +* The value is valid with :ref:`value type ` :math:`t`. + +.. math:: + \frac{ + }{ + \vdashval t.\CONST~c : t + } + + +.. 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 new rules for :ref:`administrative instructions ` and :ref:`module 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:: 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:: module instruction, store +.. _valid-moduleinstr: + +Module Instructions +~~~~~~~~~~~~~~~~~~~ + +Typing rules for :ref:`module instructions ` are specified as follows. +Unlike regular instructions, module instructions do not use the operand stack, and consequently, are not classified by a type. + + +.. index:: instantiation, external value, external type + +:math:`\INSTANTIATE~\module~\externval^\ast` +............................................ + +* Each :ref:`external value ` :math:`\externval_i` in :math:`\externval^\ast` must be :ref:`valid ` with some :ref:`external type ` :math:`\externtype_i`. + +* Then the module instruction is valid. + +.. math:: + \frac{ + (S \vdashexternval \externval : \externtype)^\ast + }{ + S \vdashmoduleinstr \INSTANTIATE~\module~\externval^\ast \ok + } + + +.. index:: element, table, table address, module instance, function index + +:math:`\INITELEM~\tableaddr~o~\moduleinst~x^n` +.............................................. + +* The :ref:`external table value ` :math:`\EVTABLE~\tableaddr` must be :ref:`valid ` with some :ref:`external table type ` :math:`\ETTABLE~\limits~\ANYFUNC`. + +* 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 module instruction is valid. + +.. math:: + \frac{ + \begin{array}{@{}rl@{}} + S \vdashexternval \EVTABLE~\tableaddr : \ETTABLE~\limits~\ANYFUNC + \qquad& + o + n \leq \limits.\LMIN + \\ + S \vdashmoduleinst \moduleinst : C + \qquad& + (C.\CFUNCS[x] = \functype)^n + \end{array} + }{ + S \vdashmoduleinstr \INITELEM~\tableaddr~o~\moduleinst~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 module instruction is valid. + +.. math:: + \frac{ + S \vdashexternval \EVMEM~\memaddr : \ETMEM~\limits + \qquad + o + n \leq \limits.\LMIN \cdot 64\,\F{Ki} + }{ + S \vdashmoduleinstr \INITDATA~\memaddr~o~b^n \ok + } + + +.. index:: instruction, context + +:math:`\instr` +.............. + +* Under an empty :ref:`context `, + the :ref:`instruction ` :math:`\instr` must be valid with type :math:`[] \to []`. + +* Then the instruction is valid as a module instruction. + +.. math:: + \frac{ + S; \{\} \vdashinstr \instr : [] \to [] + }{ + S \vdashmoduleinstr \instr \ok + } + + + +.. 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 :ref:separately `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. + +**Theorem (Preservation).** +If the :ref:`configuration ` :math:`S;T` is :ref:`valid ` with optional :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 optional resulttype (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 either an empty sequence of :ref:`module instructions `, a |TRAP| instruction, or a sequence :math:`\val^\ast` of :ref:`values ` (paired with a :ref:`frame `). +A terminal configuration is a configuration whose thread is terminal. + +**Theorem (Progress).** +If the :ref:`configuration ` :math:`S;T` is :ref:`valid ` (i.e., :math:`\vdashconfig S;T : [t^\ast]^?` with some optional :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).** +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. + + +.. [#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. `Bringing the Web up to Speed with WebAssembly `_. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017. diff --git a/document/core/exec/conventions.rst b/document/core/exec/conventions.rst index d054e1919e..7c0df438df 100644 --- a/document/core/exec/conventions.rst +++ b/document/core/exec/conventions.rst @@ -13,7 +13,7 @@ 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. +2. In *formal notation*, describing the rule in mathematical form. [#pldi2017]_ .. note:: As with validation, the prose and formal rules are equivalent, @@ -54,7 +54,7 @@ The following conventions are adopted in stating these rules. * In various places the rules contain *assertions* expressing crucial invariants about the program state. -.. index:: ! reduction rules, ! configuration, evaluation context +.. index:: ! reduction rules, configuration, evaluation context .. _exec-notation: Formal Notation @@ -75,7 +75,8 @@ 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 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. +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. @@ -125,5 +126,9 @@ or if a :ref:`trap ` occurred. where :math:`x_4 = -x_2` and :math:`x_5 = -x_2 + x_3` and :math:`x_6 = x_1 \cdot (-x_2 + x_3)`. +.. [#pldi2017] + The semantics is derived from the following article: + Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman. `Bringing the Web up to Speed with WebAssembly `_. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017. + .. [#tapl] For example: Benjamin Pierce. `Types and Programming Languages `_. The MIT Press 2002 diff --git a/document/core/exec/instructions.rst b/document/core/exec/instructions.rst index 7d20577b12..6e433e89b7 100644 --- a/document/core/exec/instructions.rst +++ b/document/core/exec/instructions.rst @@ -1077,9 +1077,12 @@ Host Functions Invoking a :ref:`host function ` has non-deterministic behavior. It may either terminate with a :ref:`trap ` or return regularly. -However, in the latter case, it is assumed that it consumes and produces the right number and types of WebAssembly :ref:`values ` on the stack, +However, in the latter case, it must consume and produce the right number and types of WebAssembly :ref:`values ` on the stack, according to its :ref:`function type `. + A host function may also modify the :ref:`store `. +However, all store modifications must result in an :ref:`extension ` of the original store, i.e., they must only modify mutable contents and must not have instances removed. +Furthermore, the resulting store must be :ref:`valid `, i.e., all data and code in it is well-typed. .. math:: ~\\[-1ex] @@ -1092,7 +1095,8 @@ A host function may also modify the :ref:`store `. (\mbox{if} & S.\SFUNCS[a] = \{ \FITYPE~[t_1^n] \to [t_2^m], \FIHOSTCODE~\dots \} \\ \wedge & \val_1^n = (t_1.\CONST~c_1)^n \\ \wedge & \val_2^m = (t_2.\CONST~c_2)^m \\ - \wedge & S' \succ S) \\ + \wedge & \vdashstoreextends S \extendsto S' \\ + \wedge & \vdashstore S' \ok) \\ \end{array} \\[1ex] \begin{array}{lcl@{\qquad}l} @@ -1101,16 +1105,14 @@ A host function may also modify the :ref:`store `. \\ \qquad \begin{array}[t]{@{}r@{~}l@{}} (\mbox{if} & S.\SFUNCS[a] = \{ \FITYPE~\X{ft}, \FIHOSTCODE~\dots \} \\ - \wedge & S' \succ S) \\ + \wedge & \vdashstoreextends S \extendsto S' \\ + \wedge & \vdashstore S' \ok) \\ \end{array} \\ \end{array} -Here, :math:`S' \succ S` expresses that the new store :math:`S'` is *reachable* from :math:`S`. -Such a store must not contain fewer addresses than the original store, -it must not differ in elements that are not mutable, -and it must still be well-typed. - -.. todo:: Define this relation more precisely. +Here, :math:`S \extendsto S'` expresses that the new store :math:`S'` is an :ref:`extension ` of :math:`S`. +Moreover, :math:`\vdashstore S' \ok` restricts :math:`S'` to be a :ref:`valid ` store. +Both notions are defined in the :ref:`Appendix `. .. note:: A host function can call back into WebAssembly by :ref:`invoking ` a function :ref:`exported ` from a :ref:`module `. diff --git a/document/core/exec/modules.rst b/document/core/exec/modules.rst index c29355d33e..81db4a5040 100644 --- a/document/core/exec/modules.rst +++ b/document/core/exec/modules.rst @@ -14,7 +14,7 @@ External Typing For the purpose of checking :ref:`external values ` against :ref:`imports `, such values are classified by :ref:`external types `. -The following auxiliary typing rules specify this typing relation relative to a :ref:`store ` :math:`S` in which the external value lives. +The following auxiliary typing rules specify this typing relation relative to a :ref:`store ` :math:`S` in which the referenced instances live. .. index:: function type, function address @@ -31,7 +31,7 @@ The following auxiliary typing rules specify this typing relation relative to a \frac{ S.\SFUNCS[a] = \{\FITYPE~\functype, \dots\} }{ - S \vdash \EVFUNC~a : \ETFUNC~\functype + S \vdashexternval \EVFUNC~a : \ETFUNC~\functype } @@ -49,7 +49,7 @@ The following auxiliary typing rules specify this typing relation relative to a \frac{ S.\STABLES[a] = \{ \TIELEM~(\X{fa}^?)^n, \TIMAX~m^? \} }{ - S \vdash \EVTABLE~a : \ETTABLE~(\{\LMIN~n, \LMAX~m^?\}~\ANYFUNC) + S \vdashexternval \EVTABLE~a : \ETTABLE~(\{\LMIN~n, \LMAX~m^?\}~\ANYFUNC) } @@ -67,7 +67,7 @@ The following auxiliary typing rules specify this typing relation relative to a \frac{ S.\SMEMS[a] = \{ \MIDATA~b^{n\cdot64\,\F{Ki}}, \MIMAX~m^? \} }{ - S \vdash \EVMEM~a : \ETMEM~\{\LMIN~n, \LMAX~m^?\} + S \vdashexternval \EVMEM~a : \ETMEM~\{\LMIN~n, \LMAX~m^?\} } @@ -85,14 +85,13 @@ The following auxiliary typing rules specify this typing relation relative to a \frac{ S.\SGLOBALS[a] = \{ \GIVALUE~(t.\CONST~c), \GIMUT~\mut \} }{ - S \vdash \EVGLOBAL~a : \ETGLOBAL~(\mut~t) + S \vdashexternval \EVGLOBAL~a : \ETGLOBAL~(\mut~t) } - .. index:: ! matching, external type .. _exec-import: -.. _match-externtype: +.. _match: Import Matching ~~~~~~~~~~~~~~~ @@ -127,7 +126,7 @@ Limits \frac{ n_1 \geq n_2 }{ - \vdash \{ \LMIN~n_1, \LMAX~m_1^? \} \leq \{ \LMIN~n_2, \LMAX~\epsilon \} + \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1^? \} \matches \{ \LMIN~n_2, \LMAX~\epsilon \} } \quad \frac{ @@ -135,10 +134,12 @@ Limits \qquad m_1 \leq m_2 }{ - \vdash \{ \LMIN~n_1, \LMAX~m_1 \} \leq \{ \LMIN~n_2, \LMAX~m_2 \} + \vdashlimitsmatch \{ \LMIN~n_1, \LMAX~m_1 \} \matches \{ \LMIN~n_2, \LMAX~m_2 \} } +.. _match-externtype: + .. index:: function type .. _match-functype: @@ -153,7 +154,7 @@ An :ref:`external type ` :math:`\ETFUNC~\functype_1` matches ~\\[-1ex] \frac{ }{ - \vdash \ETFUNC~\functype \leq \ETFUNC~\functype + \vdashexterntypematch \ETFUNC~\functype \matches \ETFUNC~\functype } @@ -171,9 +172,9 @@ An :ref:`external type ` :math:`\ETTABLE~(\limits_1~\elemtype .. math:: \frac{ - \vdash \limits_1 \leq \limits_2 + \vdashlimitsmatch \limits_1 \matches \limits_2 }{ - \vdash \ETTABLE~(\limits_1~\elemtype) \leq \ETTABLE~(\limits_2~\elemtype) + \vdashexterntypematch \ETTABLE~(\limits_1~\elemtype) \matches \ETTABLE~(\limits_2~\elemtype) } @@ -189,9 +190,9 @@ An :ref:`external type ` :math:`\ETMEM~\limits_1` matches :ma .. math:: \frac{ - \vdash \limits_1 \leq \limits_2 + \vdashlimitsmatch \limits_1 \matches \limits_2 }{ - \vdash \ETMEM~\limits_1 \leq \ETMEM~\limits_2 + \vdashexterntypematch \ETMEM~\limits_1 \matches \ETMEM~\limits_2 } @@ -209,7 +210,7 @@ An :ref:`external type ` :math:`\ETGLOBAL~\globaltype_1` matc ~\\[-1ex] \frac{ }{ - \vdash \ETGLOBAL~\globaltype \leq \ETGLOBAL~\globaltype + \vdashexterntypematch \ETGLOBAL~\globaltype \matches \ETGLOBAL~\globaltype } @@ -219,7 +220,7 @@ An :ref:`external type ` :math:`\ETGLOBAL~\globaltype_1` matc Allocation ~~~~~~~~~~ -New instances of :ref:`functions `, :ref:`tables `, :ref:`memories `, :ref:`globals `, and :ref:`modules ` are *allocated* in a :ref:`store ` :math:`S`, as defined by the following auxiliary functions. +New instances of :ref:`functions `, :ref:`tables `, :ref:`memories `, and :ref:`globals ` are *allocated* in a :ref:`store ` :math:`S`, as defined by the following auxiliary functions. .. index:: function, function instance, function address, module instance, function type @@ -320,7 +321,7 @@ New instances of :ref:`functions `, :ref:`tables ` to allocate. -2. Let :math:`\{\LMIN~n, \LMAX~m^?\}` be the :ref:`table type ` :math:`\mem.\MTYPE`. +2. Let :math:`\{\LMIN~n, \LMAX~m^?\}` be the :ref:`memory type ` :math:`\mem.\MTYPE`. 3. Let :math:`a` be the first free :ref:`memory address ` in :math:`S`. @@ -347,13 +348,13 @@ New instances of :ref:`functions `, :ref:`tables ` .................................. -1. Let :math:`\global` be the :ref:`global ` to allocate. +1. Let :math:`\global` be the :ref:`global ` to allocate and :math:`\val` the :ref:`value ` to initialize it with. 2. Let :math:`\mut~t` be the :ref:`global type ` :math:`\global.\GTYPE`. 3. Let :math:`a` be the first free :ref:`global address ` in :math:`S`. -4. Let :math:`\globalinst` be the :ref:`global instance ` :math:`\{ \GIVALUE~(t.\CONST~0), \GIMUT~\mut \}` whose contents is a zero :ref:`value ` of :ref:`value type ` :math:`t`. +4. Let :math:`\globalinst` be the :ref:`global instance ` :math:`\{ \GIVALUE~\val, \GIMUT~\mut \}`. 5. Append :math:`\globalinst` to the |SGLOBALS| of :math:`S`. @@ -361,11 +362,11 @@ New instances of :ref:`functions `, :ref:`tables `, :ref:`tables ` .................................. -The allocation function for :ref:`modules ` requires a suitable list of :ref:`external values ` that are assumed to :ref:`match ` the :ref:`import ` vector of the module. +The allocation function for :ref:`modules ` requires a suitable list of :ref:`external values ` that are assumed to :ref:`match ` the :ref:`import ` vector of the module, +and a list of initialization :ref:`values ` for the module's :ref:`globals `. -1. Let :math:`\module` be the :ref:`module ` to allocate and :math:`\externval_{\F{im}}^\ast` the vector of :ref:`external values ` providing the module's imports. +1. Let :math:`\module` be the :ref:`module ` to allocate and :math:`\externval_{\F{im}}^\ast` the vector of :ref:`external values ` providing the module's imports, +and :math:`\val^\ast` the initialization :ref:`values ` of the module's :ref:`globals `. 2. For each :ref:`function ` :math:`\func_i` in :math:`\module.\MFUNCS`, do: @@ -394,7 +397,7 @@ The allocation function for :ref:`modules ` requires a suitable l 5. For each :ref:`global ` :math:`\global_i` in :math:`\module.\MGLOBALS`, do: - a. Let :math:`\globaladdr_i` be the :ref:`global address ` resulting from :ref:`allocating ` :math:`\global_i`. + a. Let :math:`\globaladdr_i` be the :ref:`global address ` resulting from :ref:`allocating ` :math:`\global_i` with initializer value :math:`\val^\ast[i]`. 6. Let :math:`\funcaddr^\ast` be the the concatenation of the :ref:`function addresses ` :math:`\funcaddr_i` in index order. @@ -434,7 +437,7 @@ The allocation function for :ref:`modules ` requires a suitable l .. math:: ~\\ \begin{array}{rlll} - \allocmodule(S, \module, \externval_{\F{im}}^\ast) &=& S', \moduleinst \end{array} + \allocmodule(S, \module, \externval_{\F{im}}^\ast, \val^\ast) &=& S', \moduleinst \end{array} where: @@ -452,7 +455,7 @@ where: S_1, \funcaddr^\ast &=& \allocfunc^\ast(S, \module.\MFUNCS, \moduleinst) \\ S_2, \tableaddr^\ast &=& \alloctable^\ast(S_1, \module.\MTABLES) \\ S_3, \memaddr^\ast &=& \allocmem^\ast(S_2, \module.\MMEMS) \\ - S', \globaladdr^\ast &=& \allocglobal^\ast(S_3, \module.\MGLOBALS) \\[1ex] + S', \globaladdr^\ast &=& \allocglobal^\ast(S_3, \module.\MGLOBALS, \val^\ast) \\[1ex] \exportinst^\ast &=& \{ \EINAME~(\export.\ENAME), \EIVALUE~\externval_{\F{ex}} \}^\ast \quad (\where \export^\ast = \module.\MEXPORTS) \\ \evfuncs(\externval_{\F{ex}}^\ast) &=& (\moduleinst.\MIFUNCS[x])^\ast @@ -465,15 +468,27 @@ where: \qquad\!\!\! (\where x^\ast = \edglobals(\module.\MEXPORTS)) \\ \end{array} -Here, the notation :math:`\F{allocX}^\ast` is shorthand for multiple :ref:`allocations ` of object kind :math:`X`, defined as follows: +.. scratch + Here, in slight abuse of notation, :math:(`\F{allocxyz}(S, \dots))^\ast` is taken to express multiple allocations with the updates to the store :math:`S` being threaded through, i.e., + + .. math:: + \begin{array}{rlll} + (\F{allocxyz}^\ast(S_0, \dots))^n &=& S_n, a^n \\[1ex] + \mbox{where for all $i < n$:} \hfill \\ + S_{i+1}, a^n[i] &=& \F{allocxyz}(S_i, \dots) + \end{array} + +Here, the notation :math:`\F{allocx}^\ast` is shorthand for multiple :ref:`allocations ` of object kind :math:`X`, defined as follows: .. math:: \begin{array}{rlll} - \F{allocX}^\ast(S_0, X^n, \dots) &=& S_n, a^n \\[1ex] + \F{allocx}^\ast(S_0, X^n, \dots) &=& S_n, a^n \\[1ex] \mbox{where for all $i < n$:} \hfill \\ - S_{i+1}, a^n[i] &=& \F{allocX}(S_i, X^n[i], \dots) + S_{i+1}, a^n[i] &=& \F{allocx}(S_i, X^n[i], \dots) \end{array} +Moreover, if the dots :math:`\dots` are a sequence :math:`A^n` (as for globals), then the elements of this sequence are passed to the allocation function pointwise. + .. note:: The definition of module allocation is mutually recursive with the allocation of its associated functions, because the resulting module instance :math:`\moduleinst` is passed to the function allocator as an argument, in order to form the necessary closures. In an implementation, this recursion is easily unraveled by mutating one or the other in a secondary step. @@ -481,6 +496,7 @@ Here, the notation :math:`\F{allocX}^\ast` is shorthand for multiple :ref:`alloc .. index:: ! instantiation, module, instance, store, trap .. _exec-module: +.. _exec-moduleinstr: .. _exec-instantiation: Instantiation @@ -510,77 +526,79 @@ It is up to the :ref:`embedder ` to define how such conditions are rep i. Fail. -5. Let :math:`\moduleinst` be a new module instance :ref:`allocated ` from :math:`\module` in store :math:`S`. +5. Let :math:`\moduleinst_{\F{im}}` be the auxiliary module instance :math:`\{\MIGLOBALS~\evglobals(\externval^\ast)\}` that only consists of the imported globals. -6. Let :math:`F` be the :ref:`frame ` :math:`\{ \AMODULE~\moduleinst, \ALOCALS~\epsilon \}`. +6. Let :math:`F` be the :ref:`frame ` :math:`\{ \AMODULE~\moduleinst_{\F{im}}, \ALOCALS~\epsilon \}`. 7. Push the frame :math:`F` to the stack. -8. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEM`, do: +8. Let :math:`\globalidx_{\F{new}}` be the :ref:`global index ` that corresponds to the number of global :ref:`imports ` in :math:`\module.\MIMPORTS` (i.e., the index of the first non-imported global). - a. Let :math:`\X{eoval}_i` be the result of :ref:`evaluating ` the expression :math:`\elem_i.\EOFFSET`. +9. For each :ref:`global ` :math:`\global_i` in :math:`\module.\MGLOBALS`, do: - b. Assert: due to :ref:`validation `, :math:`\X{eoval}_i` is of the form :math:`\I32.\CONST~\X{eo}_i`. + a. Let :math:`\val_i` be the result of :ref:`evaluating ` the initializer expression :math:`\global_i.\GINIT`. - c. Let :math:`\tableidx_i` be the :ref:`table index ` :math:`\elem_i.\ETABLE`. + b. Let :math:`\globalidx_i` be the :ref:`global index ` :math:`\globalidx_{\F{new}} + i`. - d. Assert: due to :ref:`validation `, :math:`\moduleinst.\MITABLES[\tableidx_i]` exists. + c. Assert: due to :ref:`validation `, :math:`\moduleinst.\MIGLOBALS[\globalidx_i]` exists. - e. Let :math:`\tableaddr_i` be the :ref:`table address ` :math:`\moduleinst.\MITABLES[\tableidx_i]`. + d. Let :math:`\globaladdr_i` be the :ref:`global address ` :math:`\moduleinst.\MIGLOBALS[\globalidx_i]`. - f. Assert: due to :ref:`validation `, :math:`S.\STABLES[\tableaddr_i]` exists. + e. Assert: due to :ref:`validation `, :math:`S.\SGLOBALS[\globaladdr_i]` exists. - g. Let :math:`\tableinst_i` be the :ref:`table instance ` :math:`S.\STABLES[\tableaddr_i]`. + f. Let :math:`\globalinst_i` be the :ref:`global instance ` :math:`S.\SGLOBALS[\globaladdr_i]`. - h. Let :math:`\X{eend}_i` be :math:`\X{eo}_i` plus the length of :math:`\elem_i.\EINIT`. +10. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEM`, do: - i. If :math:`\X{eend}_i` is larger than the length of :math:`\tableinst_i.\TIELEM`, then: + a. Let :math:`\X{eoval}_i` be the result of :ref:`evaluating ` the expression :math:`\elem_i.\EOFFSET`. - i. Fail. + b. Assert: due to :ref:`validation `, :math:`\X{eoval}_i` is of the form :math:`\I32.\CONST~\X{eo}_i`. -9. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATA`, do: + c. Let :math:`\tableidx_i` be the :ref:`table index ` :math:`\elem_i.\ETABLE`. - a. Let :math:`\X{doval}_i` be the result of :ref:`evaluating ` the expression :math:`\data_i.\DOFFSET`. + d. Assert: due to :ref:`validation `, :math:`\moduleinst.\MITABLES[\tableidx_i]` exists. - b. Assert: due to :ref:`validation `, :math:`\X{doval}_i` is of the form :math:`\I32.\CONST~\X{do}_i`. + e. Let :math:`\tableaddr_i` be the :ref:`table address ` :math:`\moduleinst.\MITABLES[\tableidx_i]`. - c. Let :math:`\memidx_i` be the :ref:`memory index ` :math:`\data_i.\DMEM`. + f. Assert: due to :ref:`validation `, :math:`S.\STABLES[\tableaddr_i]` exists. - d. Assert: due to :ref:`validation `, :math:`\moduleinst.\MIMEMS[\memidx_i]` exists. + g. Let :math:`\tableinst_i` be the :ref:`table instance ` :math:`S.\STABLES[\tableaddr_i]`. - e. Let :math:`\memaddr_i` be the :ref:`memory address ` :math:`\moduleinst.\MIMEMS[\memidx_i]`. + h. Let :math:`\X{eend}_i` be :math:`\X{eo}_i` plus the length of :math:`\elem_i.\EINIT`. - f. Assert: due to :ref:`validation `, :math:`S.\SMEMS[\memaddr_i]` exists. + i. If :math:`\X{eend}_i` is larger than the length of :math:`\tableinst_i.\TIELEM`, then: - g. Let :math:`\meminst_i` be the :ref:`memory instance ` :math:`S.\SMEMS[\memaddr_i]`. + i. Fail. - h. Let :math:`\X{dend}_i` be :math:`\X{do}_i` plus the length of :math:`\data_i.\DINIT`. +11. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATA`, do: - i. If :math:`\X{dend}_i` is larger than the length of :math:`\meminst_i.\MIDATA`, then: + a. Let :math:`\X{doval}_i` be the result of :ref:`evaluating ` the expression :math:`\data_i.\DOFFSET`. - i. Fail. + b. Assert: due to :ref:`validation `, :math:`\X{doval}_i` is of the form :math:`\I32.\CONST~\X{do}_i`. -10. Let :math:`\globalidx_{\F{new}}` be the :ref:`global index ` that corresponds to the number of global :ref:`imports ` in :math:`\module.\MIMPORTS` (i.e., the index of the first non-imported global). + c. Let :math:`\memidx_i` be the :ref:`memory index ` :math:`\data_i.\DMEM`. -11. For each :ref:`global ` :math:`\global_i` in :math:`\module.\MGLOBALS`, do: + d. Assert: due to :ref:`validation `, :math:`\moduleinst.\MIMEMS[\memidx_i]` exists. - a. Let :math:`\val_i` be the result of :ref:`evaluating ` the initializer expression :math:`\global_i.\GINIT`. + e. Let :math:`\memaddr_i` be the :ref:`memory address ` :math:`\moduleinst.\MIMEMS[\memidx_i]`. - b. Let :math:`\globalidx_i` be the :ref:`global index ` :math:`\globalidx_{\F{new}} + i`. + f. Assert: due to :ref:`validation `, :math:`S.\SMEMS[\memaddr_i]` exists. - c. Assert: due to :ref:`validation `, :math:`\moduleinst.\MIGLOBALS[\globalidx_i]` exists. + g. Let :math:`\meminst_i` be the :ref:`memory instance ` :math:`S.\SMEMS[\memaddr_i]`. - d. Let :math:`\globaladdr_i` be the :ref:`global address ` :math:`\moduleinst.\MIGLOBALS[\globalidx_i]`. + h. Let :math:`\X{dend}_i` be :math:`\X{do}_i` plus the length of :math:`\data_i.\DINIT`. - e. Assert: due to :ref:`validation `, :math:`S.\SGLOBALS[\globaladdr_i]` exists. + i. If :math:`\X{dend}_i` is larger than the length of :math:`\meminst_i.\MIDATA`, then: - f. Let :math:`\globalinst_i` be the :ref:`global instance ` :math:`S.\SGLOBALS[\globaladdr_i]`. + i. Fail. 12. Assert: due to :ref:`validation `, the frame :math:`F` is now on the top of the stack. 13. Pop the frame from the stack. -14. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEM`, do: +14. Let :math:`\moduleinst` be a new module instance :ref:`allocated ` from :math:`\module` in store :math:`S` with imports :math:`\externval^\ast` and glboal initializer values :math:`\val^\ast`. + +15. For each :ref:`element segment ` :math:`\elem_i` in :math:`\module.\MELEM`, do: a. For each :ref:`function index ` :math:`\funcidx_{ij}` in :math:`\elem_i.\EINIT` (starting with :math:`j = 0`), do: @@ -590,16 +608,12 @@ It is up to the :ref:`embedder ` to define how such conditions are rep iii. Replace :math:`\tableinst_i.\TIELEM[\X{eo}_i + j]` with :math:`\funcaddr_{ij}`. -15. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATA`, do: +16. For each :ref:`data segment ` :math:`\data_i` in :math:`\module.\MDATA`, do: a. For each :ref:`byte ` :math:`b_{ij}` in :math:`\data_i.\DINIT` (starting with :math:`j = 0`), do: i. Replace :math:`\meminst_i.\MIDATA[\X{do}_i + j]` with :math:`b_{ij}`. -16. For each :ref:`global ` :math:`\global_i` in :math:`\module.\MGLOBALS`, do: - - a. Replace :math:`\globalinst_i.\GIVALUE` with :math:`\val_i`. - 17. If the :ref:`start function ` :math:`\module.\MSTART` is not empty, then: a. Assert: due to :ref:`validation `, :math:`\moduleinst.\MIFUNCS[\module.\MSTART.\SFUNC]` exists. @@ -614,51 +628,46 @@ It is up to the :ref:`embedder ` to define how such conditions are rep \begin{array}{@{}rcll} S; \INSTANTIATE~\module~\externval^n &\stepto& S'; \begin{array}[t]{@{}l@{}} - (\INITTABLE~\tableaddr~\X{eo}~\moduleinst~\elem.\EINIT)^\ast \\ - (\INITMEM~\memaddr~\X{do}~\data.\DINIT)^\ast \\ - (\INITGLOBAL~\globaladdr~v)^\ast \\ + (\INITELEM~\tableaddr~\X{eo}~\moduleinst~\elem.\EINIT)^\ast \\ + (\INITDATA~\memaddr~\X{do}~\data.\DINIT)^\ast \\ (\INVOKE~\funcaddr)^? \\ - \moduleinst \\ \end{array} \\ &(\iff - & \vdash \module : \externtype^n \\ - &\wedge& (\vdash \externval : \externtype')^n \\ - &\wedge& (\vdash \externtype' \leq \externtype)^n \\[1ex] + & \vdashmodule \module : \externtype^n \\ + &\wedge& (\vdashexternval \externval : \externtype')^n \\ + &\wedge& (\vdashexterntypematch \externtype' \matches \externtype)^n \\[1ex] &\wedge& \module.\MGLOBALS = \global^k \\ &\wedge& \module.\MELEM = \elem^\ast \\ &\wedge& \module.\MDATA = \data^\ast \\ &\wedge& \module.\MSTART = \start^? \\[1ex] - &\wedge& S', \moduleinst = \F{allocmodule}(S, \module, \externval^n) \\ + &\wedge& S', \moduleinst = \F{allocmodule}(S, \module, \externval^n, v^\ast) \\ &\wedge& F = \{ \AMODULE~\moduleinst, \ALOCALS~\epsilon \} \\[1ex] + &\wedge& (S'; F; \global.\GINIT \stepto^\ast S'; F; v)^\ast \\ &\wedge& (S'; F; \elem.\EOFFSET \stepto^\ast S'; F; \I32.\CONST~\X{eo})^\ast \\ - &\wedge& (S'; F; \data.\DOFFSET \stepto^\ast S'; F; \I32.\CONST~\X{do})^\ast \\ - &\wedge& (S'; F; \global.\GINIT \stepto^\ast S'; F; v)^\ast \\[1ex] - &\wedge& (\tableaddr = \moduleinst.\MITABLES[\elem.\ETABLE])^\ast \\ - &\wedge& (\memaddr = \moduleinst.\MIMEMS[\data.\DMEM])^\ast \\ - &\wedge& \globaladdr^\ast = \moduleinst.\MIGLOBALS[|\moduleinst.\MIGLOBALS|-k \slice k] \\ - &\wedge& (\funcaddr = \moduleinst.\MIFUNCS[\start.\SFUNC])^? \\[1ex] + &\wedge& (S'; F; \data.\DOFFSET \stepto^\ast S'; F; \I32.\CONST~\X{do})^\ast \\[1ex] &\wedge& (\X{eo} + |\elem.\EINIT| \leq |S'.\STABLES[\tableaddr].\TIELEM|)^\ast \\ &\wedge& (\X{do} + |\data.\DINIT| \leq |S'.\SMEMS[\memaddr].\MIDATA|)^\ast ) + \\[1ex] + &\wedge& \globaladdr^\ast = \moduleinst.\MIGLOBALS[|\moduleinst.\MIGLOBALS|-k \slice k] \\ + &\wedge& (\tableaddr = \moduleinst.\MITABLES[\elem.\ETABLE])^\ast \\ + &\wedge& (\memaddr = \moduleinst.\MIMEMS[\data.\DMEM])^\ast \\ + &\wedge& (\funcaddr = \moduleinst.\MIFUNCS[\start.\SFUNC])^? \\[1ex] S; \INSTANTIATE~\module~\externval^n &\stepto& S'; \TRAP \qquad (\otherwise) \\[2ex] - S; \INITTABLE~a~i~m~\epsilon &\stepto& + S; \INITELEM~a~i~m~\epsilon &\stepto& S; \epsilon \\ - S; \INITTABLE~a~i~m~(x_0~x^\ast) &\stepto& - S'; \INITTABLE~a~(i+1)~m~x^\ast \\ && + S; \INITELEM~a~i~m~(x_0~x^\ast) &\stepto& + S'; \INITELEM~a~(i+1)~m~x^\ast \\ && (\iff S' = S \with \STABLES[a].\TIELEM[i] = m.\MIFUNCS[x_0]) \\[1ex] - S; \INITMEM~a~i~\epsilon &\stepto& + S; \INITDATA~a~i~\epsilon &\stepto& S; \epsilon \\ - S; \INITMEM~a~i~(b_0~b^\ast) &\stepto& - S'; \INITMEM~a~(i+1)~b^\ast \\ && + S; \INITDATA~a~i~(b_0~b^\ast) &\stepto& + S'; \INITDATA~a~(i+1)~b^\ast \\ && (\iff S' = S \with \SMEMS[a].\MIDATA[i] = b_0) - \\[1ex] - S; \INITGLOBAL~a~v &\stepto& - S'; \epsilon \\ && - (\iff S' = S \with \SGLOBALS[a] = v) \\ \end{array} .. note:: @@ -666,6 +675,8 @@ It is up to the :ref:`embedder ` to define how such conditions are rep Store mutation is not atomic; it happens in individual steps that may be interleaved with other threads. + Evaluation of :ref:`constant expressions ` does not affect the store. + .. index:: ! invocation, module, module instance, function, export, function address, function instance, function type, value, stack, trap, store .. _exec-invocation: diff --git a/document/core/exec/runtime.rst b/document/core/exec/runtime.rst index b721836e0d..5d81db128c 100644 --- a/document/core/exec/runtime.rst +++ b/document/core/exec/runtime.rst @@ -136,7 +136,7 @@ and collects runtime representations of all entities that are imported, defined, \MIFUNCS & \funcaddr^\ast, \\ \MITABLES & \tableaddr^\ast, \\ \MIMEMS & \memaddr^\ast, \\ - \MIGLOBALS & \globaladdr^\ast \\ + \MIGLOBALS & \globaladdr^\ast, \\ \MIEXPORTS & \exportinst^\ast ~\} \\ \end{array} \end{array} @@ -307,6 +307,7 @@ It filters out entries of a specific kind in an order-preserving fashion: * :math:`\evglobals(\externval^\ast) = [\globaladdr ~|~ (\EVGLOBAL~\globaladdr) \in \externval^\ast]` + .. index:: ! stack, ! frame, ! label, instruction, store, activation, function, call, local, module instance pair: abstract syntax; frame pair: abstract syntax; label @@ -492,51 +493,11 @@ This definition allows to index active labels surrounding a :ref:`branch ` :math:`l`, which corresponds to the number of surrounding |LABEL| instructions that must be hopped over -- which is exactly the count encoded in the index of a block context. -.. index:: ! evaluation context, instruction, trap, label, frame, value -.. _syntax-ctxt-eval: - -Evaluation Contexts -................... - -Finally, the following definition of *evaluation context* and associated structural rules enable reduction inside instruction sequences and administrative forms as well as the propagation of traps: - -.. math:: - \begin{array}{llll} - \production{(evaluation contexts)} & E &::=& - [\_] ~|~ - \val^\ast~E~\instr^\ast ~|~ - \LABEL_n\{\instr^\ast\}~E~\END ~|~ - \FRAME_n\{\frame\}~E~\END \\ - \end{array} - -.. math:: - \begin{array}{lcl@{\qquad}l} - S; F; E[\instr^\ast] &\stepto& S'; F'; E[{\instr'}^\ast] - & (\iff S; F; \instr^\ast \stepto S'; F'; {\instr'}^\ast) \\ - S; F; E[\TRAP] &\stepto& S; F; \TRAP - & (\iff E \neq [\_]) \\ - \end{array} - -.. note:: - For example, the following instruction sequence, - - .. math:: - (\F64.\CONST~x_1)~(\F64.\CONST~x_2)~\F64.\NEG~(\F64.\CONST~x_3)~\F64.\ADD~\F64.\MUL - - can be decomposed into :math:`E[(\F64.\CONST~x_2)~\F64.\NEG]` where - - .. math:: - E = (\F64.\CONST~x_1)~[\_]~(\F64.\CONST~x_3)~\F64.\ADD~\F64.\MUL - - Moreover, this is the *only* possible choice of evaluation context where the contents of the hole matches the left-hand side of a reduction rule. - - .. index:: ! module instructions, function, function instance, function address, label, frame, instruction, trap, global, global instance, memory, memory instance, table, table instance, invocation, start function pair:: abstract syntax; meta instruction .. _syntax-instantiate: -.. _syntax-init_table: -.. _syntax-init_mem: -.. _syntax-init_global: +.. _syntax-init_elem: +.. _syntax-init_data: .. _syntax-moduleinstr: Module Instructions @@ -548,18 +509,18 @@ It is hence expressed in terms of reduction into smaller steps expressed by a se .. math:: \begin{array}{llcl} \production{(module instruction)} & \moduleinstr &::=& - \instr \\ &&|& \INSTANTIATE~\module~\externval^\ast \\ &&|& - \INITTABLE~\tableaddr~\u32~\moduleinst~funcidx^\ast \\ &&|& - \INITMEM~\memaddr~\u32~\byte^\ast \\ &&|& - \INITGLOBAL~\globaladdr~\val \\ &&|& - \moduleinst \\ + \INITELEM~\tableaddr~\u32~\moduleinst~\funcidx^\ast \\ &&|& + \INITDATA~\memaddr~\u32~\byte^\ast \\ &&|& + \instr \\ \end{array} The |INSTANTIATE| instruction expresses instantiation of a :ref:`module ` itself, requiring a sequence of :ref:`external values ` for the expected imports. -It reduces into a sequence of initialization instructions for :ref:`tables `, :ref:`memories ` and :ref:`globals `, -and a possible :ref:`invocation ` of the :ref:`start function `. -The final instruction returns the newly created and initialized :ref:`module instance `. +It reduces into a sequence of initialization instructions for :ref:`element ` and :ref:`data ` segments, +and a possible :ref:`invocation ` of the :ref:`start function ` that reduces further to a sequence of regular instructions. + +.. comment out + The final instruction returns the newly created and initialized :ref:`module instance `. .. note:: The reason for splitting instantiation into individual reduction steps is to provide a semantics that is compatible with future extensions like threads. @@ -568,23 +529,80 @@ The final instruction returns the newly created and initialized :ref:`module ins module instructions *embed* ordinary instructions |instr| instead of extending them. Consequently, they can only occur at the top-level. -Evaluation contexts and additional structural reduction rules for module instructions are defined as follows: + +.. index:: ! configuration, ! thread, store, frame, instruction, module instruction +.. _syntax-thread: +.. _syntax-config: + +Configurations +.............. + +A *configuration* consists of the current :ref:`store ` and an executing *thread*. + +A thread can either be a regular computation over :ref:`instructions `, or a module instantiation, represented as a computation over :ref:`module instructions `. +Regular computation operates relative to a current :ref:`frame ` referring to their home :ref:`module instance `, +whereas module computations are not local to a module, and consequently require no frame. + +.. math:: + \begin{array}{llcl} + \production{(configuration)} & \config &::=& + \store; \thread \\ + \production{(thread)} & \thread &::=& + \frame; \instr^\ast ~|~ + \moduleinstr^\ast \\ + \end{array} + +.. note:: + The current version of WebAssembly is single-threaded, + but configurations with multiple threads may be supported in the future. + + +.. index:: ! evaluation context, instruction, trap, label, frame, value +.. _syntax-ctxt-eval: + +Evaluation Contexts +................... + +Finally, the following definition of *evaluation context* and associated structural rules enable reduction inside instruction sequences and administrative forms as well as the propagation of traps: .. math:: \begin{array}{llll} + \production{(evaluation contexts)} & E &::=& + [\_] ~|~ + \val^\ast~E~\instr^\ast ~|~ + \LABEL_n\{\instr^\ast\}~E~\END ~|~ + \FRAME_n\{\frame\}~E~\END \\ \production{(module evaluation contexts)} & M &::=& - E~~\moduleinstr^\ast~~\moduleinst \\ + [\_]~~\moduleinstr^\ast \\ \end{array} .. math:: \begin{array}{lcl@{\qquad}l} - S; M[\moduleinstr] &\stepto& S'; M[{\moduleinstr'}^\ast] - & (\iff S; \moduleinstr \stepto S'; {\moduleinstr'}^\ast) \\ + S; F; E[\instr^\ast] &\stepto& S'; F'; E[{\instr'}^\ast] + & (\iff S; F; \instr^\ast \stepto S'; F'; {\instr'}^\ast) \\ + S; F; E[\TRAP] &\stepto& S; F; \TRAP + & (\iff E \neq [\_]) \\ + S; M[E[\instr]] &\stepto& S'; M[E[{\instr'}^\ast]] + & (\iff S; F_0; \instr \stepto S'; F_0; {\instr'}^\ast) \\ S; M[\TRAP] &\stepto& S; \TRAP & (\iff M \neq [\_]) \\ \end{array} -Reduction terminates when the sequence has been reduced to a |moduleinst| or when a trap occurred. +where :math:`F_0 = \{\ALOCALS~\epsilon, \AMODULE~\{\}\}` is an empty dummy frame. + +Reduction terminates for a regular thread when its instruction sequence has been reduced to a sequence of :ref:`values ` or to a |TRAP|. +Reduction terminates for a module thread when its module instruction sequence has been reduced to an empty sequence or to a |TRAP|. + .. note:: - A trap may either arise from invocation of a :ref:`start function ` or indicate failure of the |INSTANTIATE| instruction itself. + For example, the following instruction sequence, + + .. math:: + (\F64.\CONST~x_1)~(\F64.\CONST~x_2)~\F64.\NEG~(\F64.\CONST~x_3)~\F64.\ADD~\F64.\MUL + + can be decomposed into :math:`E[(\F64.\CONST~x_2)~\F64.\NEG]` where + + .. math:: + E = (\F64.\CONST~x_1)~[\_]~(\F64.\CONST~x_3)~\F64.\ADD~\F64.\MUL + + Moreover, this is the *only* possible choice of evaluation context where the contents of the hole matches the left-hand side of a reduction rule. diff --git a/document/core/index.rst b/document/core/index.rst index 124f2f8c62..f6dca0a227 100644 --- a/document/core/index.rst +++ b/document/core/index.rst @@ -3,7 +3,7 @@ WebAssembly Specification .. only:: html - Release |release| (work in progress, last updated |today|) + Release |release| (Draft, last updated |today|) .. toctree:: :maxdepth: 3 @@ -20,10 +20,14 @@ WebAssembly Specification .. toctree:: - syntax/instrindex + appendix/index-types + appendix/index-instructions + appendix/index-rules .. only:: html - * :ref:`instrindex` + * :ref:`index-type` + * :ref:`index-instr` + * :ref:`index-rules` * :ref:`genindex` diff --git a/document/core/util/math.def b/document/core/util/math.def index ca6ea49e4b..ed2d48ff03 100644 --- a/document/core/util/math.def +++ b/document/core/util/math.def @@ -114,6 +114,8 @@ .. Types, terminals +.. |to| mathdef:: \xref{syntax/types}{syntax-functype}{\rightarrow} + .. |I8| mathdef:: \xref{exec/runtime}{syntax-storagetype}{\K{i8}} .. |I16| mathdef:: \xref{exec/runtime}{syntax-storagetype}{\K{i16}} .. |I32| mathdef:: \xref{syntax/types}{syntax-valtype}{\K{i32}} @@ -371,6 +373,7 @@ .. |Bu64| mathdef:: \xref{binary/values}{binary-int}{\BuX{\B{64}}} .. |BsN| mathdef:: \xref{binary/values}{binary-int}{\BsX{N}} +.. |Bs7| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{7}}} .. |Bs32| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{32}}} .. |Bs64| mathdef:: \xref{binary/values}{binary-int}{\BsX{\B{64}}} @@ -651,6 +654,7 @@ .. Notation .. |ok| mathdef:: \mathrel{\mbox{ok}} +.. |const| mathdef:: \xref{valid/instructions}{valid-constant}{\mathrel{\mbox{const}}} .. Contexts @@ -665,13 +669,42 @@ .. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}} +.. Judgments + +.. |vdashlimits| mathdef:: \xref{valid/types}{valid-limits}{\vdash} +.. |vdashfunctype| mathdef:: \xref{valid/types}{valid-functype}{\vdash} +.. |vdashtabletype| mathdef:: \xref{valid/types}{valid-tabletype}{\vdash} +.. |vdashmemtype| mathdef:: \xref{valid/types}{valid-memtype}{\vdash} +.. |vdashglobaltype| mathdef:: \xref{valid/types}{valid-globaltype}{\vdash} + +.. |vdashinstr| mathdef:: \xref{valid/instructions}{valid-instr}{\vdash} +.. |vdashinstrseq| mathdef:: \xref{valid/instructions}{valid-instr-seq}{\vdash} +.. |vdashexpr| mathdef:: \xref{valid/instructions}{valid-expr}{\vdash} +.. |vdashexprconst| mathdef:: \xref{valid/instructions}{valid-constant}{\vdash} +.. |vdashinstrconst| mathdef:: \xref{valid/instructions}{valid-constant}{\vdash} + +.. |vdashfunc| mathdef:: \xref{valid/modules}{valid-func}{\vdash} +.. |vdashtable| mathdef:: \xref{valid/modules}{valid-table}{\vdash} +.. |vdashmem| mathdef:: \xref{valid/modules}{valid-mem}{\vdash} +.. |vdashglobal| mathdef:: \xref{valid/modules}{valid-global}{\vdash} +.. |vdashelem| mathdef:: \xref{valid/modules}{valid-elem}{\vdash} +.. |vdashdata| mathdef:: \xref{valid/modules}{valid-data}{\vdash} +.. |vdashstart| mathdef:: \xref{valid/modules}{valid-start}{\vdash} +.. |vdashexport| mathdef:: \xref{valid/modules}{valid-export}{\vdash} +.. |vdashexportdesc| mathdef:: \xref{valid/modules}{valid-exportdesc}{\vdash} +.. |vdashimport| mathdef:: \xref{valid/modules}{valid-import}{\vdash} +.. |vdashimportdesc| mathdef:: \xref{valid/modules}{valid-importdesc}{\vdash} +.. |vdashmodule| mathdef:: \xref{valid/modules}{valid-module}{\vdash} + .. Execution .. --------- .. Notation -.. |stepto| mathdef:: \hookrightarrow +.. |stepto| mathdef:: \xref{exec/conventions}{formal-notation}{\hookrightarrow} +.. |extendsto| mathdef:: \xref{appendix/properties}{extend}{\preceq} +.. |matches| mathdef:: \xref{exec/modules}{match}{\leq} .. Allocation @@ -781,9 +814,9 @@ .. |TRAP| mathdef:: \xref{exec/runtime}{syntax-trap}{\K{trap}} .. |INVOKE| mathdef:: \xref{exec/runtime}{syntax-invoke}{\K{invoke}} .. |INSTANTIATE| mathdef:: \xref{exec/runtime}{syntax-instantiate}{\K{instantiate}} -.. |INITGLOBAL| mathdef:: \xref{exec/runtime}{syntax-init_global}{\K{init\_global}} -.. |INITTABLE| mathdef:: \xref{exec/runtime}{syntax-init_table}{\K{init\_table}} -.. |INITMEM| mathdef:: \xref{exec/runtime}{syntax-init_mem}{\K{init\_mem}} +.. |INITELEM| mathdef:: \xref{exec/runtime}{syntax-init_elem}{\K{init\_elem}} +.. |INITDATA| mathdef:: \xref{exec/runtime}{syntax-init_data}{\K{init\_data}} +.. |DO| mathdef:: \xref{exec/runtime}{syntax-do}{\K{do}} .. Values & Administrative Instructions, non-terminals @@ -795,6 +828,12 @@ .. |XB| mathdef:: \xref{exec/runtime}{syntax-ctxt-block}{B} +.. Configurations, non-terminals + +.. |config| mathdef:: \xref{exec/runtime}{syntax-config}{\X{config}} +.. |thread| mathdef:: \xref{exec/runtime}{syntax-thread}{\X{thread}} + + .. Numerics, operators .. |iadd| mathdef:: \xref{exec/numerics}{op-iadd}{\F{iadd}} @@ -883,6 +922,41 @@ .. |invoke| mathdef:: \xref{exec/modules}{exec-invocation}{\F{invoke}} +.. Judgements + +.. |vdashexternval| mathdef:: \xref{exec/modules}{valid-externval}{\vdash} + +.. |vdashlimitsmatch| mathdef:: \xref{exec/modules}{match-limits}{\vdash} +.. |vdashexterntypematch| mathdef:: \xref{exec/modules}{match-externtype}{\vdash} + + +.. Soundness +.. --------- + +.. Judgements + +.. |vdashadmininstr| mathdef:: \xref{appendix/properties}{valid-instr-admin}{\vdash} +.. |vdashmoduleinstr| mathdef:: \xref{appendix/properties}{valid-moduleinstr}{\vdash} + +.. |vdashfuncinst| mathdef:: \xref{appendix/properties}{valid-funcinst}{\vdash} +.. |vdashtableinst| mathdef:: \xref{appendix/properties}{valid-tableinst}{\vdash} +.. |vdashmeminst| mathdef:: \xref{appendix/properties}{valid-meminst}{\vdash} +.. |vdashglobalinst| mathdef:: \xref{appendix/properties}{valid-globalinst}{\vdash} +.. |vdashexportinst| mathdef:: \xref{appendix/properties}{valid-exportinst}{\vdash} +.. |vdashmoduleinst| mathdef:: \xref{appendix/properties}{valid-moduleinst}{\vdash} + +.. |vdashstore| mathdef:: \xref{appendix/properties}{valid-store}{\vdash} +.. |vdashconfig| mathdef:: \xref{appendix/properties}{valid-config}{\vdash} +.. |vdashthread| mathdef:: \xref{appendix/properties}{valid-thread}{\vdash} +.. |vdashframe| mathdef:: \xref{appendix/properties}{valid-frame}{\vdash} +.. |vdashval| mathdef:: \xref{appendix/properties}{valid-val}{\vdash} + +.. |vdashfuncinstextends| mathdef:: \xref{appendix/properties}{extend-funcinst}{\vdash} +.. |vdashtableinstextends| mathdef:: \xref{appendix/properties}{extend-tableinst}{\vdash} +.. |vdashmeminstextends| mathdef:: \xref{appendix/properties}{extend-meminst}{\vdash} +.. |vdashglobalinstextends| mathdef:: \xref{appendix/properties}{extend-globalinst}{\vdash} +.. |vdashstoreextends| mathdef:: \xref{appendix/properties}{extend-store}{\vdash} + .. Custom Sections .. --------------- diff --git a/document/core/valid/conventions.rst b/document/core/valid/conventions.rst index 1ff1104a20..5b0908817e 100644 --- a/document/core/valid/conventions.rst +++ b/document/core/valid/conventions.rst @@ -12,7 +12,7 @@ For each piece of abstract syntax, there is a typing rule that specifies the con All rules are given in two *equivalent* forms: 1. In *prose*, describing the meaning in intuitive form. -2. In *formal notation*, describing the rule in mathematical form. +2. In *formal notation*, describing the rule in mathematical form. [#pldi2017]_ .. note:: The prose and formal rules are equivalent, @@ -184,5 +184,9 @@ and there is one respective rule for each relevant construct :math:`A` of the ab which is expressed by extending the context :math:`C` with the additional label information for the premise. +.. [#pldi2017] + The semantics is derived from the following article: + Andreas Haas, Andreas Rossberg, Derek Schuff, Ben Titzer, Dan Gohman, Luke Wagner, Alon Zakai, JF Bastien, Michael Holman. `Bringing the Web up to Speed with WebAssembly `_. Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017). ACM 2017. + .. [#tapl] For example: Benjamin Pierce. `Types and Programming Languages `_. The MIT Press 2002 diff --git a/document/core/valid/instructions.rst b/document/core/valid/instructions.rst index 8d6aa30f00..3581cd0cb4 100644 --- a/document/core/valid/instructions.rst +++ b/document/core/valid/instructions.rst @@ -80,7 +80,7 @@ Numeric Instructions .. math:: \frac{ }{ - C \vdash t\K{.}\CONST~c : [] \to [t] + C \vdashinstr t\K{.}\CONST~c : [] \to [t] } @@ -94,7 +94,7 @@ Numeric Instructions .. math:: \frac{ }{ - C \vdash t\K{.}\unop : [t] \to [t] + C \vdashinstr t\K{.}\unop : [t] \to [t] } @@ -108,7 +108,7 @@ Numeric Instructions .. math:: \frac{ }{ - C \vdash t\K{.}\binop : [t~t] \to [t] + C \vdashinstr t\K{.}\binop : [t~t] \to [t] } @@ -122,7 +122,7 @@ Numeric Instructions .. math:: \frac{ }{ - C \vdash t\K{.}\testop : [t] \to [\I32] + C \vdashinstr t\K{.}\testop : [t] \to [\I32] } @@ -136,7 +136,7 @@ Numeric Instructions .. math:: \frac{ }{ - C \vdash t\K{.}\relop : [t~t] \to [\I32] + C \vdashinstr t\K{.}\relop : [t~t] \to [\I32] } @@ -150,7 +150,7 @@ Numeric Instructions .. math:: \frac{ }{ - C \vdash t_2\K{.}\cvtop/t_1 : [t_1] \to [t_2] + C \vdashinstr t_2\K{.}\cvtop/t_1 : [t_1] \to [t_2] } @@ -172,7 +172,7 @@ Parametric Instructions .. math:: \frac{ }{ - C \vdash \DROP : [t] \to [] + C \vdashinstr \DROP : [t] \to [] } @@ -186,7 +186,7 @@ Parametric Instructions .. math:: \frac{ }{ - C \vdash \SELECT : [t~t~\I32] \to [t] + C \vdashinstr \SELECT : [t~t~\I32] \to [t] } .. note:: @@ -216,7 +216,7 @@ Variable Instructions \frac{ C.\CLOCALS[x] = t }{ - C \vdash \GETLOCAL~x : [] \to [t] + C \vdashinstr \GETLOCAL~x : [] \to [t] } @@ -235,7 +235,7 @@ Variable Instructions \frac{ C.\CLOCALS[x] = t }{ - C \vdash \SETLOCAL~x : [t] \to [] + C \vdashinstr \SETLOCAL~x : [t] \to [] } @@ -254,7 +254,7 @@ Variable Instructions \frac{ C.\CLOCALS[x] = t }{ - C \vdash \TEELOCAL~x : [t] \to [t] + C \vdashinstr \TEELOCAL~x : [t] \to [t] } @@ -273,7 +273,7 @@ Variable Instructions \frac{ C.\CGLOBALS[x] = \mut~t }{ - C \vdash \GETGLOBAL~x : [] \to [t] + C \vdashinstr \GETGLOBAL~x : [] \to [t] } @@ -294,7 +294,7 @@ Variable Instructions \frac{ C.\CGLOBALS[x] = \MVAR~t }{ - C \vdash \SETGLOBAL~x : [t] \to [] + C \vdashinstr \SETGLOBAL~x : [t] \to [] } @@ -324,7 +324,7 @@ Memory Instructions \qquad 2^{\memarg.\ALIGN} \leq |t|/8 }{ - C \vdash t\K{.load}~\memarg : [\I32] \to [t] + C \vdashinstr t\K{.load}~\memarg : [\I32] \to [t] } @@ -345,12 +345,10 @@ Memory Instructions \qquad 2^{\memarg.\ALIGN} \leq N/8 }{ - C \vdash t\K{.load}N\K{\_}\sx~\memarg : [\I32] \to [t] + C \vdashinstr t\K{.load}N\K{\_}\sx~\memarg : [\I32] \to [t] } -.. _valid-store: - :math:`t\K{.}\STORE~\memarg` ............................ @@ -366,7 +364,7 @@ Memory Instructions \qquad 2^{\memarg.\ALIGN} \leq |t|/8 }{ - C \vdash t\K{.store}~\memarg : [\I32~t] \to [] + C \vdashinstr t\K{.store}~\memarg : [\I32~t] \to [] } @@ -387,7 +385,7 @@ Memory Instructions \qquad 2^{\memarg.\ALIGN} \leq N/8 }{ - C \vdash t\K{.store}N~\memarg : [\I32~t] \to [] + C \vdashinstr t\K{.store}N~\memarg : [\I32~t] \to [] } @@ -404,7 +402,7 @@ Memory Instructions \frac{ C.\CMEMS[0] = \memtype }{ - C \vdash \CURRENTMEMORY : [] \to [\I32] + C \vdashinstr \CURRENTMEMORY : [] \to [\I32] } @@ -421,7 +419,7 @@ Memory Instructions \frac{ C.\CMEMS[0] = \memtype }{ - C \vdash \GROWMEMORY : [\I32] \to [\I32] + C \vdashinstr \GROWMEMORY : [\I32] \to [\I32] } @@ -444,7 +442,7 @@ Control Instructions .. math:: \frac{ }{ - C \vdash \NOP : [] \to [] + C \vdashinstr \NOP : [] \to [] } @@ -458,7 +456,7 @@ Control Instructions .. math:: \frac{ }{ - C \vdash \UNREACHABLE : [t_1^\ast] \to [t_2^\ast] + C \vdashinstr \UNREACHABLE : [t_1^\ast] \to [t_2^\ast] } .. note:: @@ -479,9 +477,9 @@ Control Instructions .. math:: \frac{ - C,\CLABELS\,[t^?] \vdash \instr^\ast : [] \to [t^?] + C,\CLABELS\,[t^?] \vdashinstrseq \instr^\ast : [] \to [t^?] }{ - C \vdash \BLOCK~[t^?]~\instr^\ast~\END : [] \to [t^?] + C \vdashinstr \BLOCK~[t^?]~\instr^\ast~\END : [] \to [t^?] } .. note:: @@ -503,9 +501,9 @@ Control Instructions .. math:: \frac{ - C,\CLABELS\,[] \vdash \instr^\ast : [] \to [t^?] + C,\CLABELS\,[] \vdashinstrseq \instr^\ast : [] \to [t^?] }{ - C \vdash \LOOP~[t^?]~\instr^\ast~\END : [] \to [t^?] + C \vdashinstr \LOOP~[t^?]~\instr^\ast~\END : [] \to [t^?] } .. note:: @@ -530,11 +528,11 @@ Control Instructions .. math:: \frac{ - C,\CLABELS\,[t^?] \vdash \instr_1^\ast : [] \to [t^?] + C,\CLABELS\,[t^?] \vdashinstrseq \instr_1^\ast : [] \to [t^?] \qquad - C,\CLABELS\,[t^?] \vdash \instr_2^\ast : [] \to [t^?] + C,\CLABELS\,[t^?] \vdashinstrseq \instr_2^\ast : [] \to [t^?] }{ - C \vdash \IF~[t^?]~\instr_1^\ast~\ELSE~\instr_2^\ast~\END : [\I32] \to [t^?] + C \vdashinstr \IF~[t^?]~\instr_1^\ast~\ELSE~\instr_2^\ast~\END : [\I32] \to [t^?] } .. note:: @@ -557,7 +555,7 @@ Control Instructions \frac{ C.\CLABELS[l] = [t^?] }{ - C \vdash \BR~l : [t_1^\ast~t^?] \to [t_2^\ast] + C \vdashinstr \BR~l : [t_1^\ast~t^?] \to [t_2^\ast] } .. note:: @@ -579,7 +577,7 @@ Control Instructions \frac{ C.\CLABELS[l] = [t^?] }{ - C \vdash \BRIF~l : [t^?~\I32] \to [t^?] + C \vdashinstr \BRIF~l : [t^?~\I32] \to [t^?] } @@ -606,7 +604,7 @@ Control Instructions \qquad C.\CLABELS[l_N] = [t^?] }{ - C \vdash \BRTABLE~l^\ast~l_N : [t_1^\ast~t^?~\I32] \to [t_2^\ast] + C \vdashinstr \BRTABLE~l^\ast~l_N : [t_1^\ast~t^?~\I32] \to [t_2^\ast] } .. note:: @@ -628,7 +626,7 @@ Control Instructions \frac{ C.\CRETURN = [t^?] }{ - C \vdash \RETURN : [t_1^\ast~t^?] \to [t_2^\ast] + C \vdashinstr \RETURN : [t_1^\ast~t^?] \to [t_2^\ast] } .. note:: @@ -652,7 +650,7 @@ Control Instructions \frac{ C.\CFUNCS[x] = [t_1^\ast] \to [t_2^\ast] }{ - C \vdash \CALL~x : [t_1^\ast] \to [t_2^\ast] + C \vdashinstr \CALL~x : [t_1^\ast] \to [t_2^\ast] } @@ -677,7 +675,7 @@ Control Instructions \qquad C.\CTYPES[x] = [t_1^\ast] \to [t_2^\ast] }{ - C \vdash \CALLINDIRECT~x : [t_1^\ast] \to [t_2^\ast] + C \vdashinstr \CALLINDIRECT~x : [t_1^\ast] \to [t_2^\ast] } @@ -699,7 +697,7 @@ Empty Instruction Sequence: :math:`\epsilon` .. math:: \frac{ }{ - C \vdash \epsilon : [t^\ast] \to [t^\ast] + C \vdashinstrseq \epsilon : [t^\ast] \to [t^\ast] } @@ -719,11 +717,11 @@ Non-empty Instruction Sequence: :math:`\instr^\ast~\instr_N` .. math:: \frac{ - C \vdash \instr^\ast : [t_1^\ast] \to [t_0^\ast~t^\ast] + C \vdashinstrseq \instr^\ast : [t_1^\ast] \to [t_0^\ast~t^\ast] \qquad - C \vdash \instr_N : [t^\ast] \to [t_3^\ast] + C \vdashinstr \instr_N : [t^\ast] \to [t_3^\ast] }{ - C \vdash \instr^\ast~\instr_N : [t_1^\ast] \to [t_0^\ast~t_3^\ast] + C \vdashinstrseq \instr^\ast~\instr_N : [t_1^\ast] \to [t_0^\ast~t_3^\ast] } @@ -749,9 +747,9 @@ Expressions :math:`\expr` are classified by :ref:`result types \frac{ C.\CTYPES[x] = [t_1^\ast] \to [t_2^?] \qquad - C,\CLOCALS\,t_1^\ast~t^\ast,\CLABELS~[t_2^?],\CRETURN~[t_2^?] \vdash \expr : [t_2^?] + C,\CLOCALS\,t_1^\ast~t^\ast,\CLABELS~[t_2^?],\CRETURN~[t_2^?] \vdashexpr \expr : [t_2^?] }{ - C \vdash \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \} : [t_1^\ast] \to [t_2^?] + C \vdashfunc \{ \FTYPE~x, \FLOCALS~t^\ast, \FBODY~\expr \} : [t_1^\ast] \to [t_2^?] } .. note:: The restriction on the length of the result types :math:`t_2^\ast` may be lifted in future versions of WebAssembly. -.. index:: table, table type, limits, element type +.. index:: table, table type pair: validation; table single: abstract syntax; table .. _valid-table: @@ -59,27 +59,24 @@ Functions :math:`\func` are classified by :ref:`function types Tables ~~~~~~ -Tables :math:`\table` are classified by :ref:`table types ` of the form :math:`\limits~\elemtype`. - +Tables :math:`\table` are classified by :ref:`table types `. :math:`\{ \TTYPE~\tabletype \}` ............................... -* Let :math:`\limits~\elemtype` be the :ref:`table types ` :math:`\tabletype`. - -* The limits :math:`\limits` must be :ref:`valid `. +* The :ref:`table type ` :math:`\tabletype` must be :ref:`valid `. * Then the table definition is valid with type :math:`\tabletype`. .. math:: \frac{ - \vdash \limits\ok + \vdashtabletype \tabletype \ok }{ - C \vdash \{ \TTYPE~\limits~\elemtype \} : \limits~\elemtype + C \vdashtable \{ \TTYPE~\tabletype \} : \tabletype } -.. index:: memory, memory type, limits +.. index:: memory, memory type pair: validation; memory single: abstract syntax; memory .. _valid-mem: @@ -87,27 +84,24 @@ Tables :math:`\table` are classified by :ref:`table types ` of Memories ~~~~~~~~ -Memories :math:`\mem` are classified by :ref:`memory types ` of the form :math:`\limits`. - +Memories :math:`\mem` are classified by :ref:`memory types `. :math:`\{ \MTYPE~\memtype \}` ............................. -* Let :math:`\limits` be the :ref:`memory types ` :math:`\memtype`. - -* The limits :math:`\limits` must be :ref:`valid `. +* The :ref:`memory type ` :math:`\memtype` must be :ref:`valid `. * Then the memory definition is valid with type :math:`\memtype`. .. math:: \frac{ - \vdash \limits\ok + \vdashmemtype \memtype \ok }{ - C \vdash \{ \MTYPE~\limits \} : \limits~\elemtype + C \vdashmem \{ \MTYPE~\memtype \} : \memtype } -.. index:: global, global type, mutability, expression +.. index:: global, global type, expression pair: validation; global single: abstract syntax; global .. _valid-global: @@ -121,6 +115,8 @@ Globals :math:`\global` are classified by :ref:`global types :math:`\{ \GTYPE~\mut~t, \GINIT~\expr \}` ......................................... +* The :ref:`global type ` :math:`\mut~t` must be :ref:`valid `. + * The expression :math:`\expr` must be :ref:`valid ` with :ref:`result type ` :math:`[t]`. * The expression :math:`\expr` must be :ref:`constant `. @@ -129,11 +125,13 @@ Globals :math:`\global` are classified by :ref:`global types .. math:: \frac{ - C \vdash \expr : [t] + \vdashglobaltype \mut~t \ok \qquad - C \vdash \expr ~\F{const} + C \vdashexpr \expr : [t] + \qquad + C \vdashexprconst \expr ~\F{const} }{ - C \vdash \{ \GTYPE~\mut~t, \GINIT~\expr \} : \mut~t + C \vdashglobal \{ \GTYPE~\mut~t, \GINIT~\expr \} : \mut~t } @@ -172,13 +170,13 @@ Element segments :math:`\elem` are not classified by a type. \frac{ C.\CTABLES[x] = \limits~\ANYFUNC \qquad - C \vdash \expr : [\I32] + C \vdashexpr \expr : [\I32] \qquad - C \vdash \expr ~\F{const} + C \vdashexprconst \expr ~\F{const} \qquad (C.\CFUNCS[y] = \functype)^\ast }{ - C \vdash \{ \ETABLE~x, \EOFFSET~\expr, \EINIT~y^\ast \} \ok + C \vdashelem \{ \ETABLE~x, \EOFFSET~\expr, \EINIT~y^\ast \} \ok } @@ -210,11 +208,11 @@ Data segments :math:`\data` are not classified by any type. \frac{ C.\CMEMS[x] = \limits \qquad - C \vdash \expr : [\I32] + C \vdashexpr \expr : [\I32] \qquad - C \vdash \expr ~\F{const} + C \vdashexprconst \expr ~\F{const} }{ - C \vdash \{ \DMEM~x, \DOFFSET~\expr, \DINIT~b^\ast \} \ok + C \vdashdata \{ \DMEM~x, \DOFFSET~\expr, \DINIT~b^\ast \} \ok } @@ -242,13 +240,14 @@ Start function declarations :math:`\start` are not classified by any type. \frac{ C.\CFUNCS[x] = [] \to [] }{ - C \vdash \{ \SFUNC~x \} \ok + C \vdashstart \{ \SFUNC~x \} \ok } .. index:: export, name, index, function index, table index, memory index, global index pair: validation; export single: abstract syntax; export +.. _valid-exportdesc: .. _valid-export: Exports @@ -267,9 +266,9 @@ Export descriptions :math:`\exportdesc` are not classified by any type. .. math:: \frac{ - C \vdash \exportdesc \ok + C \vdashexportdesc \exportdesc \ok }{ - C \vdash \{ \ENAME~\name, \EDESC~\exportdesc \} : \name + C \vdashexport \{ \ENAME~\name, \EDESC~\exportdesc \} : \name } @@ -284,7 +283,7 @@ Export descriptions :math:`\exportdesc` are not classified by any type. \frac{ C.\CFUNCS[x] = \functype }{ - C \vdash \EDFUNC~x \ok + C \vdashexportdesc \EDFUNC~x \ok } @@ -299,7 +298,7 @@ Export descriptions :math:`\exportdesc` are not classified by any type. \frac{ C.\CTABLES[x] = \tabletype }{ - C \vdash \EDTABLE~x \ok + C \vdashexportdesc \EDTABLE~x \ok } @@ -314,7 +313,7 @@ Export descriptions :math:`\exportdesc` are not classified by any type. \frac{ C.\CMEMS[x] = \memtype }{ - C \vdash \EDMEM~x \ok + C \vdashexportdesc \EDMEM~x \ok } @@ -333,13 +332,14 @@ Export descriptions :math:`\exportdesc` are not classified by any type. \frac{ C.\CGLOBALS[x] = \MCONST~t }{ - C \vdash \EDGLOBAL~x \ok + C \vdashexportdesc \EDGLOBAL~x \ok } .. index:: import, name, function type, table type, memory type, global type pair: validation; import single: abstract syntax; import +.. _valid-importdesc: .. _valid-import: Imports @@ -357,9 +357,9 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi .. math:: \frac{ - C \vdash \importdesc : \externtype + C \vdashimportdesc \importdesc : \externtype }{ - C \vdash \{ \IMODULE~\name_1, \INAME~\name_2, \IDESC~\importdesc \} : \externtype + C \vdashimport \{ \IMODULE~\name_1, \INAME~\name_2, \IDESC~\importdesc \} : \externtype } @@ -376,51 +376,54 @@ Imports :math:`\import` and import descriptions :math:`\importdesc` are classifi \frac{ C.\CTYPES[x] = [t_1^\ast] \to [t_2^\ast] }{ - C \vdash \IDFUNC~x : \ETFUNC~[t_1^\ast] \to [t_2^\ast] + C \vdashimportdesc \IDFUNC~x : \ETFUNC~[t_1^\ast] \to [t_2^\ast] } -:math:`\IDTABLE~\limits~\elemtype` -.................................. +:math:`\IDTABLE~\tabletype` +........................... -* The limits :math:`\limits` must be valid. +* The table type :math:`\tabletype` must be :ref:`valid `. -* Then the import description is valid with type :math:`\ETTABLE~\limits~\elemtype`. +* Then the import description is valid with type :math:`\ETTABLE~\tabletype`. .. math:: \frac{ - \vdash \limits \ok + \vdashtable \tabletype \ok }{ - C \vdash \IDTABLE~\limits~\elemtype : \ETTABLE~\limits~\elemtype + C \vdashimportdesc \IDTABLE~\tabletype : \ETTABLE~\tabletype } -:math:`\IDMEM~\limits` -...................... +:math:`\IDMEM~\memtype` +....................... -* The limits :math:`\limits` must be valid. +* The memory type :math:`\memtype` must be :ref:`valid `. -* Then the import description is valid with type :math:`\ETMEM~\limits`. +* Then the import description is valid with type :math:`\ETMEM~\memtype`. .. math:: \frac{ - \vdash \limits \ok + \vdashmemtype \memtype \ok }{ - C \vdash \IDMEM~\limits : \ETMEM~\limits + C \vdashimportdesc \IDMEM~\memtype : \ETMEM~\memtype } -:math:`\IDGLOBAL~\mut~t` -........................ +:math:`\IDGLOBAL~\globaltype` +............................. -* The mutability :math:`\mut` must be |MCONST|. +* The global type :math:`\globaltype` must be :ref:`valid `. + +* The mutability of :math:`\globaltype` must be |MCONST|. -* Then the import description is valid with type :math:`\ETGLOBAL~t`. +* Then the import description is valid with type :math:`\ETGLOBAL~\globaltype`. .. math:: \frac{ + \vdashglobaltype \MCONST~t \ok }{ - C \vdash \IDGLOBAL~\MCONST~t : \ETGLOBAL~\MCONST~t + C \vdashimportdesc \IDGLOBAL~\MCONST~t : \ETGLOBAL~\MCONST~t } @@ -510,25 +513,25 @@ Instead, the context :math:`C` for validation of the module's content is constru .. math:: \frac{ \begin{array}{@{}c@{}} - (\vdash \functype \ok)^\ast + (\vdashfunctype \functype \ok)^\ast \quad - (C \vdash \func : \X{ft})^\ast + (C \vdashfunc \func : \X{ft})^\ast \quad - (C \vdash \table : \X{tt})^\ast + (C \vdashtable \table : \X{tt})^\ast \quad - (C \vdash \mem : \X{mt})^\ast + (C \vdashmem \mem : \X{mt})^\ast \quad - (C' \vdash \global : \X{gt})^\ast + (C' \vdashglobal \global : \X{gt})^\ast \\ - (C \vdash \elem \ok)^\ast + (C \vdashelem \elem \ok)^\ast \quad - (C \vdash \data \ok)^\ast + (C \vdashdata \data \ok)^\ast \quad - (C \vdash \start \ok)^? + (C \vdashstart \start \ok)^? \quad - (C \vdash \import : \X{it})^\ast + (C \vdashimport \import : \X{it})^\ast \quad - (C \vdash \export : \X{name})^\ast + (C \vdashexport \export : \X{name})^\ast \\ \X{ift}^\ast = \etfuncs(\X{it}^\ast) \qquad @@ -549,7 +552,7 @@ Instead, the context :math:`C` for validation of the module's content is constru \name^\ast ~\F{disjoint} \end{array} }{ - \vdash \{ + \vdashmodule \{ \begin{array}[t]{@{}l@{}} \MTYPES~\functype^\ast, \MFUNCS~\func^\ast, diff --git a/document/core/valid/types.rst b/document/core/valid/types.rst index b30008e7c4..8fbff90fca 100644 --- a/document/core/valid/types.rst +++ b/document/core/valid/types.rst @@ -2,7 +2,32 @@ Types ----- Most :ref:`types ` are universally valid. -However, restrictions apply to :ref:`function types ` and :ref:`limits `, which must be checked during validation. +However, restrictions apply to :ref:`function types ` as well as the :ref:`limits ` of :ref:`table types ` and :ref:`memory types `, which must be checked during validation. + + +.. index:: limits + pair: validation; limits + single: abstract syntax; limits +.. _valid-limits: + +Limits +~~~~~~ + +:ref:`Limits ` must have meaningful bounds. + +:math:`\{ \LMIN~n, \LMAX~m^? \}` +................................ + +* If the maximum :math:`m^?` is not empty, then its value must not be smaller than :math:`n`. + +* Then the limit is valid. + +.. math:: + \frac{ + (n \leq m)^? + }{ + \vdashlimits \{ \LMIN~n, \LMAX~m^? \} \ok + } .. index:: function type @@ -25,33 +50,74 @@ Function Types .. math:: \frac{ }{ - \vdash [t_1^\ast] \to [t_2^?] \ok + \vdashfunctype [t_1^\ast] \to [t_2^?] \ok } .. note:: This restriction may be removed in future versions of WebAssembly. -.. index:: limits - pair: validation; limits - single: abstract syntax; limits -.. _valid-limits: +.. index:: table type, element type, limits + pair: validation; table type + single: abstract syntax; table type +.. _valid-tabletype: -Limits -~~~~~~ +Table Types +~~~~~~~~~~~ -:ref:`Limits ` must have menaingful bounds. +:math:`\limits~\elemtype` +......................... -:math:`\{ \LMIN~n, \LMAX~m^? \}` -................................ +* The limits :math:`\limits` must be :ref:`valid `. -* If the maximum :math:`m^?` is not empty, then its value must not be smaller than :math:`n`. +* Then the table type is valid. -* Then the limit is valid. +.. math:: + \frac{ + \vdashlimits \limits \ok + }{ + \vdashtabletype \limits~\elemtype \ok + } + + +.. index:: memory type, limits + pair: validation; memory type + single: abstract syntax; memory type +.. _valid-memtype: + +Memory Types +~~~~~~~~~~~~ + +:math:`\limits` +............... + +* The limits :math:`\limits` must be :ref:`valid `. + +* Then the memory type is valid. + +.. math:: + \frac{ + \vdashlimits \limits \ok + }{ + \vdashmemtype \limits \ok + } + + +.. index:: global type, value type, mutability + pair: validation; global type + single: abstract syntax; global type +.. _valid-globaltype: + +Global Types +~~~~~~~~~~~~ + +:math:`\mut~\valtype` +..................... + +* Then the global type is valid. .. math:: \frac{ - (n \leq m)^? }{ - \vdash \{ \LMIN~n, \LMAX~m^? \} \ok + \vdashglobaltype \mut~\valtype \ok }