Modules

For modules, the execution semantics primarily defines instantiation, which allocates instances for a module and its contained definitions, initializes tables and memories from contained element and data segments, and invokes the start function if present. It also includes invocation of exported functions.

Instantiation depends on a number of auxiliary notions for type-checking imports and allocating instances.

External Typing

For the purpose of checking external values against imports, such values are classified by external types. The following auxiliary typing rules specify this typing relation relative to a store S in which the referenced instances live.

func a

  • The store entry S.funcs[a] must exist.

  • Then func a is valid with external type func S.funcs[a].type.

Sfunc a:func S.funcs[a].type

table a

  • The store entry S.tables[a] must exist.

  • Then table a is valid with external type table S.tables[a].type.

Stable a:table S.tables[a].type

mem a

  • The store entry S.mems[a] must exist.

  • Then mem a is valid with external type mem S.mems[a].type.

Smem a:mem S.mems[a].type

global a

  • The store entry S.globals[a] must exist.

  • Then global a is valid with external type global S.globals[a].type.

Sglobal a:global S.globals[a].type

Value Typing

For the purpose of checking argument values against the parameter types of exported functions, values are classified by value types. The following auxiliary typing rules specify this typing relation relative to a store S in which possibly referenced addresses live.

Numeric Values t.const c

St.const c:t

Null References ref.null t

Sref.null t:t

Function References ref a

Sfunc a:func functypeSref a:funcref

External References ref.extern a

Sref.extern a:externref

Allocation

New instances of functions, tables, memories, and globals are allocated in a store S, as defined by the following auxiliary functions.

Functions

  1. Let func be the function to allocate and moduleinst its module instance.

  2. Let a be the first free function address in S.

  3. Let functype be the function type moduleinst.types[func.type].

  4. Let funcinst be the function instance {type functype,module moduleinst,code func}.

  5. Append funcinst to the funcs of S.

  6. Return a.

 allocfunc(S,func,moduleinst)=S,funcaddrwhere:funcaddr=|S.funcs|functype=moduleinst.types[func.type]funcinst={type functype,module moduleinst,code func}S=S{funcs funcinst}

Host Functions

  1. Let hostfunc be the host function to allocate and functype its function type.

  2. Let a be the first free function address in S.

  3. Let funcinst be the function instance {type functype,hostcode hostfunc}.

  4. Append funcinst to the funcs of S.

  5. Return a.

 allochostfunc(S,functype,hostfunc)=S,funcaddrwhere:funcaddr=|S.funcs|funcinst={type functype,hostcode hostfunc}S=S{funcs funcinst}

Note

Host functions are never allocated by the WebAssembly semantics itself, but may be allocated by the embedder.

Tables

  1. Let tabletype be the table type to allocate and ref the initialization value.

  2. Let ({min n,max m?} reftype) be the structure of table type tabletype.

  3. Let a be the first free table address in S.

  4. Let tableinst be the table instance {type tabletype,elem refn} with n elements set to ref.

  5. Append tableinst to the tables of S.

  6. Return a.

alloctable(S,tabletype,ref)=S,tableaddrwhere:tabletype={min n,max m?} reftypetableaddr=|S.tables|tableinst={type tabletype,elem refn}S=S{tables tableinst}

Memories

  1. Let memtype be the memory type to allocate.

  2. Let {min n,max m?} be the structure of memory type memtype.

  3. Let a be the first free memory address in S.

  4. Let meminst be the memory instance {type memtype,data (0x00)n64Ki} that contains n pages of zeroed bytes.

  5. Append meminst to the mems of S.

  6. Return a.

allocmem(S,memtype)=S,memaddrwhere:memtype={min n,max m?}memaddr=|S.mems|meminst={type memtype,data (0x00)n64Ki}S=S{mems meminst}

Globals

  1. Let globaltype be the global type to allocate and val the value to initialize the global with.

  2. Let a be the first free global address in S.

  3. Let globalinst be the global instance {type globaltype,value val}.

  4. Append globalinst to the globals of S.

  5. Return a.

allocglobal(S,globaltype,val)=S,globaladdrwhere:globaladdr=|S.globals|globalinst={type globaltype,value val}S=S{globals globalinst}

Element segments

  1. Let reftype be the elements’ type and ref the vector of references to allocate.

  2. Let a be the first free element address in S.

  3. Let eleminst be the element instance {type reftype,elem ref}.

  4. Append eleminst to the elems of S.

  5. Return a.

allocelem(S,reftype,ref)=S,elemaddrwhere:elemaddr=|S.elems|eleminst={type reftype,elem ref}S=S{elems eleminst}

Data segments

  1. Let b be the vector of bytes to allocate.

  2. Let a be the first free data address in S.

  3. Let datainst be the data instance {data b}.

  4. Append datainst to the datas of S.

  5. Return a.

allocdata(S,b)=S,dataaddrwhere:dataaddr=|S.datas|datainst={data b}S=S{datas datainst}

Growing tables

  1. Let tableinst be the table instance to grow, n the number of elements by which to grow it, and ref the initialization value.

  2. Let len be n added to the length of tableinst.elem.

  3. If len is larger than or equal to 232, then fail.

  4. Let limits t be the structure of table type tableinst.type.

  5. Let limits be limits with min updated to len.

  6. If limits is not valid, then fail.

  7. Append refn to tableinst.elem.

  8. Set tableinst.type to the table type limits t.

growtable(tableinst,n,ref)=tableinstwithtype=limits twithelem=tableinst.elem refn(iflen=n+|tableinst.elem|len<232limits t=tableinst.typelimits=limitswithmin=lenlimitsok)

Growing memories

  1. Let meminst be the memory instance to grow and n the number of pages by which to grow it.

  2. Assert: The length of meminst.data is divisible by the page size 64Ki.

  3. Let len be n added to the length of meminst.data divided by the page size 64Ki.

  4. If len is larger than 216, then fail.

  5. Let limits be the structure of memory type meminst.type.

  6. Let limits be limits with min updated to len.

  7. If limits is not valid, then fail.

  8. Append n times 64Ki bytes with value 0x00 to meminst.data.

  9. Set meminst.type to the memory type limits.

growmem(meminst,n)=meminstwithtype=limitswithdata=meminst.data (0x00)n64Ki(iflen=n+|meminst.data|/64Kilen216limits=meminst.typelimits=limitswithmin=lenlimitsok)

Modules

The allocation function for modules requires a suitable list of external values that are assumed to match the import vector of the module, a list of initialization values for the module’s globals, and list of reference vectors for the module’s element segments.

  1. Let module be the module to allocate and externvalim the vector of external values providing the module’s imports, val the initialization values of the module’s globals, and (ref) the reference vectors of the module’s element segments.

  2. For each function funci in module.funcs, do:

    1. Let funcaddri be the function address resulting from allocating funci for the module instance moduleinst defined below.

  3. For each table tablei in module.tables, do:

    1. Let limitsi ti be the table type tablei.type.

    2. Let tableaddri be the table address resulting from allocating tablei.type with initialization value ref.null ti.

  4. For each memory memi in module.mems, do:

    1. Let memaddri be the memory address resulting from allocating memi.type.

  5. For each global globali in module.globals, do:

    1. Let globaladdri be the global address resulting from allocating globali.type with initializer value val[i].

  6. For each element segment elemi in module.elems, do:

    1. Let elemaddri be the element address resulting from allocating an element instance of reference type elemi.type with contents (ref)[i].

  7. For each data segment datai in module.datas, do:

    1. Let dataaddri be the data address resulting from allocating a data instance with contents datai.init.

  8. Let funcaddr be the concatenation of the function addresses funcaddri in index order.

  9. Let tableaddr be the concatenation of the table addresses tableaddri in index order.

  10. Let memaddr be the concatenation of the memory addresses memaddri in index order.

  11. Let globaladdr be the concatenation of the global addresses globaladdri in index order.

  12. Let elemaddr be the concatenation of the element addresses elemaddri in index order.

  13. Let dataaddr be the concatenation of the data addresses dataaddri in index order.

  14. Let funcaddrmod be the list of function addresses extracted from externvalim, concatenated with funcaddr.

  15. Let tableaddrmod be the list of table addresses extracted from externvalim, concatenated with tableaddr.

  16. Let memaddrmod be the list of memory addresses extracted from externvalim, concatenated with memaddr.

  17. Let globaladdrmod be the list of global addresses extracted from externvalim, concatenated with globaladdr.

  18. For each export exporti in module.exports, do:

    1. If exporti is a function export for function index x, then let externvali be the external value func (funcaddrmod[x]).

    2. Else, if exporti is a table export for table index x, then let externvali be the external value table (tableaddrmod[x]).

    3. Else, if exporti is a memory export for memory index x, then let externvali be the external value mem (memaddrmod[x]).

    4. Else, if exporti is a global export for global index x, then let externvali be the external value global (globaladdrmod[x]).

    5. Let exportinsti be the export instance {name (exporti.name),value externvali}.

  19. Let exportinst be the concatenation of the export instances exportinsti in index order.

  20. Let moduleinst be the module instance {types (module.types), funcaddrs funcaddrmod, tableaddrs tableaddrmod, memaddrs memaddrmod, globaladdrs globaladdrmod, exports exportinst}.

  21. Return moduleinst.

 allocmodule(S,module,externvalim,val,(ref))=S,moduleinst

where:

table=module.tablesmem=module.memsglobal=module.globalselem=module.elemsdata=module.datasexport=module.exportsmoduleinst={ types module.types,funcaddrs funcs(externvalim) funcaddr,tableaddrs tables(externvalim) tableaddr,memaddrs mems(externvalim) memaddr,globaladdrs globals(externvalim) globaladdr,elemaddrs elemaddr,dataaddrs dataaddr,exports exportinst }S1,funcaddr=allocfunc(S,module.funcs,moduleinst)S2,tableaddr=alloctable(S1,(table.type),(ref.null t))(where(table.type)=(limits t))S3,memaddr=allocmem(S2,(mem.type))S4,globaladdr=allocglobal(S3,(global.type),val)S5,elemaddr=allocelem(S4,(elem.type),(ref))S,dataaddr=allocdata(S5,(data.init))exportinst={name (export.name),value externvalex}funcs(externvalex)=(moduleinst.funcaddrs[x]) (wherex=funcs(export))tables(externvalex)=(moduleinst.tableaddrs[x])(wherex=tables(export))mems(externvalex)=(moduleinst.memaddrs[x])(wherex=mems(export))globals(externvalex)=(moduleinst.globaladdrs[x])(wherex=globals(export))

Here, the notation allocx is shorthand for multiple allocations of object kind X, defined as follows:

allocx(S0,Xn,)=Sn,anwhere for all i<n:Si+1,an[i]=allocx(Si,Xn[i],)

Moreover, if the dots are a sequence An (as for globals or tables), 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 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.

Instantiation

Given a store S, a module module is instantiated with a list of external values externvaln supplying the required imports as follows.

Instantiation checks that the module is valid and the provided imports match the declared types, and may fail with an error otherwise. Instantiation can also result in a trap from initializing a table or memory from an active segment or from executing the start function. It is up to the embedder to define how such conditions are reported.

  1. If module is not valid, then:

    1. Fail.

  2. Assert: module is valid with external types externtypeimm classifying its imports.

  3. If the number m of imports is not equal to the number n of provided external values, then:

    1. Fail.

  4. For each external value externvali in externvaln and external type externtypei in externtypeimn, do:

    1. If externvali is not valid with an external type externtypei in store S, then:

      1. Fail.

    2. If externtypei does not match externtypei, then:

      1. Fail.

  1. Let moduleinstinit be the auxiliary module instance {globaladdrs globals(externvaln),funcaddrs moduleinst.funcaddrs} that only consists of the imported globals and the imported and allocated functions from the final module instance moduleinst, defined below.

  2. Let Finit be the auxiliary frame {module moduleinstinit,locals ϵ}.

  3. Push the frame Finit to the stack.

  4. Let val be the vector of global initialization values determined by module and externvaln. These may be calculated as follows.

    1. For each global globali in module.globals, do:

      1. Let vali be the result of evaluating the initializer expression globali.init.

    2. Assert: due to validation, the frame Finit is now on the top of the stack.

    3. Let val be the concatenation of vali in index order.

  5. Let (ref) be the list of reference vectors determined by the element segments in module. These may be calculated as follows.

    1. For each element segment elemi in module.elems, and for each element expression exprij in elemi.init, do:

      1. Let refij be the result of evaluating the initializer expression exprij.

    2. Let refi be the concatenation of function elements refij in order of index j.

    3. Let (ref) be the concatenation of function element vectors refi in order of index i.

  6. Pop the frame Finit from the stack.

  7. Let moduleinst be a new module instance allocated from module in store S with imports externvaln, global initializer values val, and element segment contents (ref), and let S be the extended store produced by module allocation.

  8. Let F be the auxiliary frame {module moduleinst,locals ϵ}.

  9. Push the frame F to the stack.

  10. For each element segment elemi in module.elems whose mode is of the form active {table tableidxi,offset einstri end}, do:

    1. Let n be the length of the vector elemi.init.

    2. Execute the instruction sequence einstri.

    3. Execute the instruction i32.const 0.

    4. Execute the instruction i32.const n.

    5. Execute the instruction table.init tableidxi i.

    6. Execute the instruction elem.drop i.

  11. For each element segment elemi in module.elems whose mode is of the form declarative, do:

    1. Execute the instruction elem.drop i.

  12. For each data segment datai in module.datas whose mode is of the form active {memory memidxi,offset dinstri end}, do:

    1. Let n be the length of the vector datai.init.

    2. Execute the instruction sequence dinstri.

    3. Execute the instruction i32.const 0.

    4. Execute the instruction i32.const n.

    5. Execute the instruction memory.init i.

    6. Execute the instruction data.drop i.

  13. If the start function module.start is not empty, then:

    1. Let start be the start function module.start.

    2. Execute the instruction call start.func.

  14. Assert: due to validation, the frame F is now on the top of the stack.

  15. Pop the frame F from the stack.

 instantiate(S,module,externvalk)=S;F;runelem0(elemn[0])  runelemn1(elemn[n1])rundata0(datam[0])  rundatam1(datam[m1])(call start.func)?(ifmodule:externtypeimkexterntypeex(Sexternval:externtype)k(externtypeexterntypeim)kmodule.globals=globalmodule.elems=elemnmodule.datas=datammodule.start=start?(exprg=global.init)(expre=elem.init)nS,moduleinst=allocmodule(S,module,externvalk,val,(ref)n)F={module moduleinst,locals ϵ}(S;F;exprgS;F;val end)((S;F;expreS;F;ref end))n)

where:

runelemi({type et,init exprn,mode passive})=ϵrunelemi({type et,init exprn,mode active{table x,offset instr end}})=instr (i32.const 0) (i32.const n) (table.init x i) (elem.drop i)runelemi({type et,init exprn,mode declarative})=(elem.drop i)rundatai({init bn,mode passive})=ϵrundatai({init bn,mode active{memory x,offset instr end}})=instr (i32.const 0) (i32.const n) (memory.init x i) (data.drop i)

Note

Module allocation and the evaluation of global initializers and element segments are mutually recursive because the global initialization values val and element segment contents (ref) are passed to the module allocator while depending on the module instance moduleinst and store S returned by allocation. However, this recursion is just a specification device. In practice, the initialization values can be determined beforehand by staging module allocation such that first, the module’s own function instances are pre-allocated in the store, then the initializer expressions are evaluated, then the rest of the module instance is allocated, and finally the new function instances’ module fields are set to that module instance. This is possible because validation ensures that initialization expressions cannot actually call a function, only take their reference.

All failure conditions are checked before any observable mutation of the store takes place. Store mutation is not atomic; it happens in individual steps that may be interleaved with other threads.

Evaluation of constant expressions does not affect the store.

Invocation

Once a module has been instantiated, any exported function can be invoked externally via its function address funcaddr in the store S and an appropriate list val of argument values.

Invocation may fail with an error if the arguments do not fit the function type. Invocation can also result in a trap. It is up to the embedder to define how such conditions are reported.

Note

If the embedder API performs type checks itself, either statically or dynamically, before performing an invocation, then no failure other than traps can occur.

The following steps are performed:

  1. Assert: S.funcs[funcaddr] exists.

  2. Let funcinst be the function instance S.funcs[funcaddr].

  3. Let [t1n][t2m] be the function type funcinst.type.

  4. If the length |val| of the provided argument values is different from the number n of expected arguments, then:

    1. Fail.

  5. For each value type ti in t1n and corresponding value vali in val, do:

    1. If vali is not valid with value type ti, then:

      1. Fail.

  6. Let F be the dummy frame {module {},locals ϵ}.

  7. Push the frame F to the stack.

  8. Push the values val to the stack.

  9. Invoke the function instance at address funcaddr.

Once the function has returned, the following steps are executed:

  1. Assert: due to validation, m values are on the top of the stack.

  2. Pop valresm from the stack.

  3. Assert: due to validation, the frame F is now on the top of the stack.

  4. Pop the frame F from the stack.

The values valresm are returned as the results of the invocation.

 invoke(S,funcaddr,valn)=S;F;valn (invoke funcaddr)(ifS.funcs[funcaddr].type=[t1n][t2m](Sval:t1)nF={module {},locals ϵ})