This series is mainly my notes on WASM research, which may be brief. The total includes:

  1. WebAssembly(1) Compilation
  2. The WebAssembly(2) Basic Api
  3. WebAssembly(3) Instructions
  4. WebAssembly(4) Validation
  5. WebAssembly(5) Memory
  6. WebAssembly(6) Binary Format
  7. WebAssembly(7) Future
  8. WebAssembly(8) Wasm in Rust (TODO)

Only authenticated modules can be initialized. Validation is done through a Type system that runs in the module AST and the content.

Contexts

Contexts specifies the context in which the type will run:


  1. Locals, labels, and return type are used only when validating statements inside the function body and are empty elsewhere.labelRepresents the current contextlabel stackRepresented by a series of ResultTypes, is the only part of the current context that changes with the order in which the statements are executed.
  2. Specific to the actual context, some empty fields will be omitted
  3. It means that in the same context C, it’s going toThe prepend to CfieldIn the
  4. We can useThis index syntax is used to represent the corresponding index space (index space). And context extends the tagMainly used to temporarily expand relative index space, for examplelabel indices. The new statement will be defined before all existing statements, taking the item with index 0 and adding one to the index of the other items of the previous definition

Formal Notation

  • Conventions

    Represents that A has the corresponding type TRepresents that in the context of C, A has the corresponding type T

In general, a validation rule can be written as follows:


Some rules can have no premises and are called axiom, such as i32.add:


For example, the local.get rule can be written as:


Another example is that the premise itself is a judgment:


Instructions

Instructions can pass through function typesTo classification. The function type describes how it operates on the operand virtual machine. Arguments for push and returns for POP. Such as instructionIs of type, means it can consume twoArgument, and generate a new one.

For some instructions, the type rule is not a strict type constraint, and polymorphism exists:

  1. The value of polymorphicvalue-polymorphic, some of the values or operands are unqualified, such as allParametric instructionsAll of them (drop, select)
  2. The stack of polymorphicstack-polymorphicThe state of the stack is unbounded, such as all control instructions, which provide unconditional flow control.unreachable.br.br_tableandreturn

For the SELECT directive, for example, the following two statements are legal:



In addition, type checking is also performed for unreachable statements under unreachable instructions. The check method is as follows: if there is a stack state that satisfies the current instruction block, it is valid; otherwise, it is illegal:


Is legal because when a stack state isThe time,unreachableThe statement can execute smoothly.


Is illegal because no stack can be found to allow the instruction block to execute properly.

Type definitions for common instructions

Instructions — WebAssembly 1.0