kwasm.validation.module

Kwasm.validation.module

package kwasm.validation.module

Classes

Name Description
object DataSegmentValidator

Validator of DataSegment nodes.

From the docs:

  • The memory C.mems[x] must be defined in the context.
  • The expression expr must be valid with result type [i32].
  • The expression expr must be constant.
  • Then the data segment is valid.

object ElementSegmentValidator

Validator of ElementSegment nodes.

From the docs:

  • The table C.tables[x] must be defined in the context.
  • Let limits elemtype be the table type C.tables[x].
  • The element type elemtype must be funcref.
  • The expression expr must be valid with result type [i32].
  • The expression expr must be constant.
  • For each y_i in y*, the function C.funcs[y] must be defined in the context.
  • Then the element segment is valid.

object ExportValidator

Validator of Export nodes.

From the docs:

  • The export description exportdesc must be valid with external type externtype.
  • Then the export is valid with external type externtype.

object ExportDescriptorValidator

Validator of ExportDescriptor nodes.

From the docs:


func x
  • The function C.funcs[x] must be defined in the context.
  • Then the export description is valid with external type func C.funcs[x].

table x
  • The table C.tables[x] must be defined in the context.
  • Then the export description is valid with external type table C.tables[x].

mem x
  • The memory C.mems[x] must be defined in the context.
  • Then the export description is valid with external type mem C.mems[x].

global x

  • The global C.globals\[x] must be defined in the context.
  • Then the export description is valid with external type global C.globals\[x].
object GlobalValidator

Validator of Global nodes.

From the docs:

  • The global type mut t must be valid.
  • The expression expr must be valid with result type [t].
  • The expression expr must be constant.
  • Then the global definition is valid with type mut t.

object ImportValidator

Validator of Import nodes.

From the docs:

  • The import description importdesc must be valid with type externtype.
  • Then the import is valid with type externtype.

object ImportDescriptorValidator

Validator of ImportDescriptor nodes.

From the docs:


func x
  • The function C.types[x] must be defined in the context.
  • Let [t*^1] => [t*^2] be the function type C.types[x].
  • Then the import description is valid with type func [t*^1] => [t*^2].

table tabletype
  • The table type tabletype must be valid.
  • Then the import description is valid with type table tabletype.

mem memtype
  • The memory type memtype must be valid.
  • Then the import description is valid with type mem memtype.

global globaltype

  • The global type globaltype must be valid.
  • Then the import description is valid with type global globaltype.
object MemoryValidator

Validator of Memory nodes.

From the docs:

  • The memory type memtype must be valid.
  • Then the memory definition is valid with type memtype.

object ModuleValidator

Validator of WasmModules.

From the docs:

Modules are classified by their mapping from the external types of their imports to those of their exports.

A module is entirely closed, that is, its components can only refer to definitions that appear in the module itself. Consequently, no initial context is required. Instead, the context C for validation of the module’s content is constructed from the definitions in the module.

KWasm Note: The validation context will be passed to the ModuleValidator

  • Let module be the module to validate.
  • Let C be a context where:

    • C.types is module.types,
    • C.funcs is funcs(it*) concatenated with ft*, with the import’s external types it* and the internal function types ft* as determined below,
    • C.tables is tables(it*) concatenated with tt*, with the import’s external types it* and the internal table types tt* as determined below,
    • C.mems is mems(it*) concatenated with mt*, with the import’s external types it* and the internal memory types mt* as determined below,
    • C.globals is globals(it*) concatenated with gt*, with the import’s external types it* and the internal global types gt* as determined below,
    • C.locals is empty,
    • C.labels is empty,
    • C.return is empty.
  • Let C′ be the context where C′.globals is the sequence globals(it*) and all other fields are empty.
  • Under the context C:
  • For each functype_i in module.types, the function type functype_i must be valid.
  • For each func_i in module.funcs, the definition func_i must be valid with a function type ft_i.
  • For each table_i in module.tables, the definition table_i must be valid with a table type tt_i.
  • For each mem_i in module.mems, the definition mem_i must be valid with a memory type mt_i.
  • For each global_i in module.globals: Under the context C′, the definition global_i must be valid with a global type gt_i.
  • For each elem_i in module.elem, the segment elem_i must be valid.
  • For each data_i in module.data, the segment data_i must be valid.
  • If module.start is non-empty, then module.start must be valid.
  • For each import_i in module.imports, the segment import_i must be valid with an external type it_i.
  • For each export_i in module.exports, the segment export_i must be valid with external type et_i.
  • The length of C.tables must not be larger than 1.
  • The length of C.mems must not be larger than 1.
  • All export names export_i.name must be different.
  • Let ft* be the concatenation of the internal function types ft_i, in index order.
  • Let tt* be the concatenation of the internal table types tt_i, in index order.
  • Let mt* be the concatenation of the internal memory types mt_i, in index order.
  • Let gt* be the concatenation of the internal global types gt_i, in index order.
  • Let it* be the concatenation of external types it_i of the imports, in index order.
  • Let et* be the concatenation of external types et_i of the exports, in index order.
  • Then the module is valid with external types it* => et*.

object StartFunctionValidator

Validator of StartFunction nodes.

From the docs:

  • The function C.funcs[x] must be defined in the context.
  • The type of C.funcs[x] must be [] => [].
  • Then the start function is valid.

object TableValidator

Validator of Table nodes.

From the docs:

  • The table type tabletype must be valid.
  • Then the table definition is valid with type tabletype.

object WasmFunctionValidator

Validator of WasmFunction nodes.

From the docs:

  • The type C.types[x] must be defined in the context.
  • Let [t*^1] => [t?^2] be the function type C.types[x].
  • Let C′ be the same context as C, but with:

    • locals set to the sequence of value types t*^1 t*, concatenating parameters and locals,
    • labels set to the singular sequence containing only result type [t?^2].
    • return set to the result type [t?^2].
  • Under the context C′, the expression expr must be valid with type t?^2.
  • Then the function definition is valid with type [t*^1] => [t?^2].

Methods

validate

fun DataSegment.validate(context: Module): Module

Validates the DataSegment node.

Receiver

Name Description
DataSegment

Parameters

Name Description
context: Module

ReturnValue

Name Description
Module

validate

fun ElementSegment.validate(context: Module): Module

Validates the ElementSegment node.

Receiver

Name Description
ElementSegment

Parameters

Name Description
context: Module

ReturnValue

Name Description
Module

validate

fun Export.validate(context: Module): Module

Validates the Export node.

Receiver

Name Description
Export

Parameters

Name Description
context: Module

ReturnValue

Name Description
Module

validate

fun ExportDescriptor<*>.validate(context: Module): Module

Validates the ExportDescriptor node.

Receiver

Name Description
ExportDescriptor<*>

Parameters

Name Description
context: Module

ReturnValue

Name Description
Module

validate

fun Global.validate(context: Module): Module

Validates the Global node.

Receiver

Name Description
Global

Parameters

Name Description
context: Module

ReturnValue

Name Description
Module

validate

fun Import.validate(context: Module): Module

Validates the Import node.

Receiver

Name Description
Import

Parameters

Name Description
context: Module

ReturnValue

Name Description
Module

validate

fun ImportDescriptor.validate(context: Module): Module

Validates the ImportDescriptor node.

Receiver

Name Description
ImportDescriptor

Parameters

Name Description
context: Module

ReturnValue

Name Description
Module

validate

fun Memory.validate(context: Module): Module

Validates the Memory node.

Receiver

Name Description
Memory

Parameters

Name Description
context: Module

ReturnValue

Name Description
Module

validate

fun WasmModule.validate(context: Module): Module

Validates a WasmModule.

This is the main entry point into the validation process.

Receiver

Name Description
WasmModule

Parameters

Name Description
context: Module

ReturnValue

Name Description
Module

validate

fun StartFunction.validate(context: Module): Module

Validates the StartFunction node.

Receiver

Name Description
StartFunction

Parameters

Name Description
context: Module

ReturnValue

Name Description
Module

validate

fun Table.validate(context: Module): Module

Validates the Table node.

Receiver

Name Description
Table

Parameters

Name Description
context: Module

ReturnValue

Name Description
Module

validate

fun WasmFunction.validate(context: Module): Module

Validates the WasmFunction node.

Receiver

Name Description
WasmFunction

Parameters

Name Description
context: Module

ReturnValue

Name Description
Module