Kwasm.format.binary.module

From the docs:

The code section has the id 10. It decodes into a vector of code entries that are pairs of value type vectors and expressions. They represent the locals and body field of the functions in the funcs component of a module. The type fields of the respective functions are encoded separately in the function section.

The encoding of each code entry consists of

• the u32 size of the function code in bytes,
• the actual function code, which in turn consists of
• the declaration of locals,
• the function body as an expression.

Local declarations are compressed into a vector whose entries consist of

• a u32 count,
• a value type, denoting count locals of the same value type.

codesec ::= code*:section_10(vec(code)) => code*
code    ::= size:u32 code:func          => code (if size = ||func||)
func    ::= (t*):vec(locals) e:expr    => concat((t)), e (if |concat((t*)*)| < 2^32)
locals  ::= n:u32 t:valtype             => t^n

Here, code ranges over pairs (valtype*, expr). The meta function concat((t*)*) concatenates all sequences t*_i in (t*)*. Any code for which the length of the resulting sequence is out of bounds of the maximum size of a vector is malformed.

Note

Like with sections, the code size is not needed for decoding, but can be used to skip functions when navigating through a binary. The module is malformed if a size does not match the length of the respective function code.

From the docs:

Custom sections have the id 0. They are intended to be used for debugging information or third-party extensions, and are ignored by the WebAssembly semantics. Their contents consist of a name further identifying the custom section, followed by an uninterpreted sequence of bytes for custom use.

customsec   ::= section_0(custom)
custom      ::= name byte*

Note If an implementation interprets the data of a custom section, then errors in that data, or the placement of the section, must not invalidate the module.

From the docs:

The data section has the id 11. It decodes into a vector of data segments that represent the data component of a module.

datasec ::= seg*:section_11(vec(data))      => seg
data    ::= x:memidx e:expr b*:vec(byte)    => {data x, offset e, init b*}

From the docs:

The element section has the id 9. It decodes into a vector of element segments that represent the elem component of a module.

elemsec ::= seg*:section_9(vec(elem))           => seg
elem    ::= x:tableidx e:expr y*:vec(funcidx)   => {table x, offset e, init y*}

Reads an ElementSegment from a binary-encoded WebAssembly module's ElementSection.

From the docs:

The export section has the id 7. It decodes into a vector of exports that represent the exports component of a module.

exportsec   ::= ex*:section_7(vec(export))  => ex*
export      ::= nm:name d:exportdesc        => {name nm, desc d}
exportdesc  ::= 0x00 x:funcidx              => func x
0x01 x:tableidx             => table x
0x02 x:memidx               => mem x
0x03 x:globalidx            => global x

Encodes the receiving MemorySection as a sequence of Bytes.

From the docs:

The function section has the id 3. It decodes into a vector of type indices that represent the type fields of the functions in the funcs component of a module. The locals and body fields of the respective functions are encoded separately in the code section.

funcsec ::= x*:section_3(vec(typeidx))  => x*

From the docs:

The global section has the id 6. It decodes into a vector of globals that represent the globals component of a module.

globalsec   ::= glob*:section_6(vec(global))    => glob*
global      ::= gt:globaltype e:expr            => {type gt, init e}

From the docs:

The import section has the id 2. It decodes into a vector of imports that represent the imports component of a module.

importsec   ::= im*:section_2(vec(import))      => im*
import      ::= mod:name nm:name d:importdesc   => {module mod, name nm, desc d}
importdesc  ::= 0x00 x:typeidx                  => func x
0x01 tt:tabletype               => table tt
0x02 mt:memtype                 => mem mt
0x03 gt:globaltype              => global gt

From the docs:

All indices are encoded with their respective value.

typeidx     ::= x:u32 => x
funcidx     ::= x:u32 => x
tableidx    ::= x:u32 => x
memidx      ::= x:u32 => x
globalidx   ::= x:u32 => x
localidx    ::= x:u32 => x
labelidx    ::= l:u32 => l

From the code section docs:

Local declarations are compressed into a vector whose entries consist of

• a u32 count,
• a value type, denoting count locals of the same value type.

func    ::= (t*):vec(locals) e:expr    => concat((t)), e (if |concat((t*)*)| < 2^32)
locals  ::= n:u32 t:valtype             => tn

The meta function concat((t*)*) concatenates all sequences t*_i in (t*)*.

From the docs:

The memory section has the id 5. It decodes into a vector of memories that represent the mems component of a module.

memsec  ::= mem*:section_5(vec(mem))    => mem*
mem     ::= mt:memtype                  =>

Reads an Offset from a binary-encoded WebAssembly module.

Offsets are encoded as expressions.

From the docs:

Each section consists of

• a one-byte section id,
• theu32 size of the contents, in bytes,
• the actual contents, whose structure is depended on the section id.

Every section is optional; an omitted section is equivalent to the section being present with empty contents.

The following parameterized grammar rule defines the generic structure of a section with id N and contents described by the grammar B.

section_N(B)    ::= N:byte size:u32 cont:B  => cont (if size = ||B||)
ϵ                       => ϵ

Note Other than for unknown custom sections, the size is not required for decoding, but can be used to skip sections when navigating through a binary. The module is malformed if the size does not match the length of the binary contents B.

From the docs:

The start section has the id 8. It decodes into an optional start function that represents the start component of a module.

startsec    ::= st?:section_8(start)    => st?
start       ::= x:funcidx               =>

From the docs:

The table section has the id 4. It decodes into a vector of tables that represent the tables component of a module.

tablesec    ::= tab*:section_4(vec(table))  => tab*
table       ::= tt:tabletype                =>

From the docs:

The type section has the id 1. It decodes into a vector of function types that represent the 𝗍𝗒𝗉𝖾𝗌 component of a module.

typesec ::= ft*:section_1(vec(functype)) => ft*

From the docs:

The encoding of a module starts with a preamble containing a 4-byte magic number (the string ‘∖0asm’) and a version field. The current version of the WebAssembly binary format is 1.

The preamble is followed by a sequence of sections. Custom sections may be inserted at any place in this sequence, while other sections must occur at most once and in the prescribed order. All sections can be empty.

The lengths of vectors produced by the (possibly empty) function and code section must match up.

magic   ::= 0x00 0x61 0x73 0x6D
version ::= 0x01 0x00 0x00 0x00
module  ::= magic
version
customsec*
functype*:typesec
customsec*
import*:importsec
customsec*
typeidx^n:funcsec
customsec*
table*:tablesec
customsec*
mem*:memsec
customsec*
global*:globalsec
customsec*
export*:exportsec
customsec*
start?:startsec
customsec*
elem*:elemsec
customsec*
code^n:codesec
customsec*
data*:datasec
customsec*          => {types functype*,
funcs func^n,
tables table*,
mems mem*,
globals global*,
elem elem*,
data data*,
start start?,
imports import*,
exports export*}

Encodes a list of Locals to a sequence of bytes.