Module Mavryk_webassembly_interpreter.Decode

exception Code of Source.region * string
type state =
  1. | Byte_vector_step
  2. | Instr_step
  3. | Instr_block_step
  4. | Block_step
  5. | Name_step
  6. | Func_type_step
  7. | Import_step
  8. | Export_step
  9. | Code_step
  10. | Elem_step
  11. | Data_step
  12. | Module_step

States representation.

exception Step_error of state

Exception raised when the small-step parser evaluate an impossible state.

type 'a lazy_stack =
  1. | LazyStack of {
    1. length : int32;
    2. vector : 'a Vector.t;
    }

Lazy stack using an underlying lazy vector, and a pointer on the head of the stack.

val empty_stack : unit -> 'a lazy_stack

empty_stack () returns a new empty stack.

val push_stack : 'a -> 'a lazy_stack -> 'a lazy_stack

push_stack v s pushes value v on the stack s at index s.length and updates the length. If s.vector is full, it appends the value to the vector (growing it by 1), otherwise it set the value in the vector.

val push_rev_values : 'a list -> 'a lazy_stack -> 'a lazy_stack

push_rev_values vs s pushes values in vs on the stack s, starting from the end of the list.

val pop_stack : 'a lazy_stack -> ('a * 'a lazy_stack) option Lwt.t

pop_stack s returns the value at s.length - 1 and a new stack with length decreased by one.

val pop_at_most : int -> 'a lazy_stack -> ('a list * 'a lazy_stack) Lwt.t

pop_at_most n s returns at most the n values on top of the stack, and the resulting stack.

type instr_block_kont =
  1. | IKStop of Ast.block_label
    (*

    Final step of a block parsing.

    *)
  2. | IKNext of Ast.block_label
    (*

    Tag parsing, containing the accumulation of already parsed values.

    *)
  3. | IKBlock of Ast.block_type * int
    (*

    Block parsing step.

    *)
  4. | IKLoop of Ast.block_type * int
    (*

    Loop parsing step.

    *)
  5. | IKIf1 of Ast.block_type * int
    (*

    If parsing step.

    *)
  6. | IKIf2 of Ast.block_type * int * Ast.block_label
    (*

    If .. else parsing step.

    *)

Instruction parsing continuations.

type block_kont =
  1. | BlockStart
    (*

    Initial step of a block parsing, allocating the block in the block table.

    *)
  2. | BlockParse of instr_block_kont lazy_stack
    (*

    Parsing of a block, with the continuation stack.

    *)
  3. | BlockStop of Ast.block_label
    (*

    End of a block, returning the label corresponding to the allocated block at the beginning.

    *)

Block parsing continuations.

Vector and size continuations

type 'a lazy_vec_kont =
  1. | LazyVec of {
    1. offset : int32;
    2. vector : 'a Vector.t;
    }

Lazy vector accumulator, with the current offset to write the next value in the vector.

type pos = int

Position of a value on the stream.

type size = {
  1. size : int;
  2. start : pos;
}

Size checking version of sized for CPS-style parsing.

type byte_vector_kont =
  1. | VKStart
    (*

    Initial step.

    *)
  2. | VKRead of Ast.data_label * int64 * int64
    (*

    Reading step, containing the current position in the string and the length, reading byte per byte.

    *)
  3. | VKStop of Ast.data_label
    (*

    Final step, cannot reduce.

    *)

Incremental chunked byte vector creation (from implicit input).

type name_step =
  1. | NKStart
    (*

    UTF8 name starting point.

    *)
  2. | NKParse of pos * Stdlib.Buffer.t * int
    (*

    UTF8 char parsing.

    *)
  3. | NKStop of Ast.name
    (*

    UTF8 name final step.

    *)
type func_type_kont =
  1. | FKStart
  2. | FKIns of Types.value_type lazy_vec_kont
  3. | FKOut of Types.value_type Vector.t * Types.value_type lazy_vec_kont
  4. | FKStop of Types.func_type
type import_kont =
  1. | ImpKStart
    (*

    Import parsing starting point.

    *)
  2. | ImpKModuleName of name_step
    (*

    Import module name parsing UTF8 char per char step.

    *)
  3. | ImpKItemName of Ast.name * name_step
    (*

    Import item name parsing UTF8 char per char step.

    *)
  4. | ImpKStop of Ast.import'
    (*

    Import final step.

    *)
type export_kont =
  1. | ExpKStart
    (*

    Export parsing starting point.

    *)
  2. | ExpKName of name_step
    (*

    Export name parsing UTF8 char per char step.

    *)
  3. | ExpKStop of Ast.export'
    (*

    Export final step.

    *)
type code_kont =
  1. | CKStart
    (*

    Starting point of a function parsing.

    *)
  2. | CKLocalsParse of {
    1. left : pos;
    2. size : size;
    3. pos : pos;
    4. vec_kont : (int32 * Types.value_type) lazy_vec_kont;
    5. locals_size : Stdlib.Int64.t;
    }
    (*

    Parse a local value with its number of occurences.

    *)
  3. | CKLocalsAccumulate of {
    1. left : pos;
    2. size : size;
    3. pos : pos;
    4. type_vec : (int32 * Types.value_type) lazy_vec_kont;
    5. curr_type : (int32 * Types.value_type) option;
    6. vec_kont : Types.value_type lazy_vec_kont;
    }
    (*

    Accumulate local values.

    *)
  4. | CKBody of {
    1. left : pos;
    2. size : size;
    3. locals : Types.value_type Vector.t;
    4. const_kont : block_kont;
    }
    (*

    Parsing step of the body of a function.

    *)
  5. | CKStop of Ast.func
    (*

    Final step of a parsed function, irreducible.

    *)

Code section parsing.

type index_kind =
  1. | Indexed
  2. | Const
type elem_kont =
  1. | EKStart
    (*

    Starting point of an element segment parsing.

    *)
  2. | EKMode of {
    1. left : pos;
    2. index : int32 Source.phrase;
    3. index_kind : index_kind;
    4. early_ref_type : Types.ref_type option;
    5. offset_kont : pos * block_kont;
    }
    (*

    Element segment mode parsing step.

    *)
  3. | EKInitIndexed of {
    1. mode : Ast.segment_mode;
    2. ref_type : Types.ref_type;
    3. einit_vec : Ast.const lazy_vec_kont;
    }
    (*

    Element segment initialization code parsing step for referenced values.

    *)
  4. | EKInitConst of {
    1. mode : Ast.segment_mode;
    2. ref_type : Types.ref_type;
    3. einit_vec : Ast.const lazy_vec_kont;
    4. einit_kont : pos * block_kont;
    }
    (*

    Element segment initialization code parsing step for constant values.

    *)
  5. | EKStop of Ast.elem_segment'
    (*

    Final step of a segment parsing.

    *)
type data_kont =
  1. | DKStart
    (*

    Starting point of a data segment parsing.

    *)
  2. | DKMode of {
    1. left : pos;
    2. index : int32 Source.phrase;
    3. offset_kont : pos * block_kont;
    }
    (*

    Data segment mode parsing step.

    *)
  3. | DKInit of {
    1. dmode : Ast.segment_mode;
    2. init_kont : byte_vector_kont;
    }
  4. | DKStop of Ast.data_segment'
    (*

    Final step of a data segment parsing.

    *)
type section_tag = [
  1. | `CodeSection
  2. | `CustomSection
  3. | `DataCountSection
  4. | `DataSection
  5. | `ElemSection
  6. | `ExportSection
  7. | `FuncSection
  8. | `GlobalSection
  9. | `ImportSection
  10. | `MemorySection
  11. | `StartSection
  12. | `TableSection
  13. | `TypeSection
]

Representation of a section tag.

type vec_repr =
  1. | VecRepr

Type witness for a LazyVector.

type opt_repr =
  1. | OptRepr

Type witness for an option.

type (_, _) field_type =
  1. | TypeField : (Ast.type_, vec_repr) field_type
  2. | ImportField : (Ast.import, vec_repr) field_type
  3. | FuncField : (Ast.var, vec_repr) field_type
  4. | TableField : (Ast.table, vec_repr) field_type
  5. | MemoryField : (Ast.memory, vec_repr) field_type
  6. | GlobalField : (Ast.global, vec_repr) field_type
  7. | ExportField : (Ast.export, vec_repr) field_type
  8. | StartField : (Ast.start, opt_repr) field_type
  9. | ElemField : (Ast.elem_segment, vec_repr) field_type
  10. | DataCountField : (int32, opt_repr) field_type
  11. | CodeField : (Ast.func, vec_repr) field_type
  12. | DataField : (Ast.data_segment, vec_repr) field_type

Sections representation.

type field =
  1. | VecField : ('a, vec_repr) field_type * 'a Vector.t -> field
  2. | SingleField : ('a, opt_repr) field_type * 'a option -> field

Result of a section parsing, being either a single value or a vector.

type module_kont =
  1. | MKStart
    (*

    Initial state of a module parsing

    *)
  2. | MKSkipCustom : ('a, 'repr) field_type option -> module_kont
    (*

    Custom section which are skipped, with the next section to parse.

    *)
  3. | MKFieldStart : ('a, 'repr) field_type -> module_kont
    (*

    Starting point of a section, handles parsing generic section header.

    *)
  4. | MKField : ('a, vec_repr) field_type * size * 'a lazy_vec_kont -> module_kont
    (*

    Section currently parsed, accumulating each element from the underlying vector.

    *)
  5. | MKElaborateFunc : Ast.var Vector.t * Ast.func Vector.t * Ast.func lazy_vec_kont * Ast.instr lazy_vec_kont lazy_vec_kont option * bool -> module_kont
    (*

    Elaboration of functions from the code section with their declared type in the func section, and accumulating invariants conditions associated to functions.

    *)
  6. | MKBuild of Ast.func Vector.t option * bool
    (*

    Accumulating the parsed sections vectors into a module and checking invariants.

    *)
  7. | MKStop of Ast.module_
    (*

    Final step of the parsing, cannot reduce.

    *)
  8. | MKTypes of func_type_kont * pos * size * Ast.type_ lazy_vec_kont
    (*

    Function types section parsing.

    *)
  9. | MKImport of import_kont * pos * size * Ast.import lazy_vec_kont
    (*

    Import section parsing.

    *)
  10. | MKExport of export_kont * pos * size * Ast.export lazy_vec_kont
    (*

    Export section parsing.

    *)
  11. | MKGlobal of Types.global_type * int * block_kont * size * Ast.global lazy_vec_kont
    (*

    Globals section parsing, containing the starting position, the continuation of the current global block instruction, and the size of the section.

    *)
  12. | MKElem of elem_kont * int * size * Ast.elem_segment lazy_vec_kont
    (*

    Element segments section parsing, containing the current element parsing continuation, the starting position of the current element, the size of the section.

    *)
  13. | MKData of data_kont * int * size * Ast.data_segment lazy_vec_kont
    (*

    Data segments section parsing, containing the current data parsing continuation, the starting position of the current data, the size of the section.

    *)
  14. | MKCode of code_kont * int * size * Ast.func lazy_vec_kont
    (*

    Code section parsing, containing the current function parsing continuation, the starting position of the current function, the size of the section.

    *)

Module parsing steps

type stream = {
  1. name : string;
  2. bytes : Mavryk_lazy_containers.Chunked_byte_vector.t;
  3. mutable pos : int;
}

Parsed bytes with the current reading position.

type building_state = {
  1. types : Ast.type_ Vector.t;
  2. imports : Ast.import Vector.t;
  3. vars : Ast.var Vector.t;
  4. tables : Ast.table Vector.t;
  5. memories : Ast.memory Vector.t;
  6. globals : Ast.global Vector.t;
  7. exports : Ast.export Vector.t;
  8. start : Ast.start option;
  9. elems : Ast.elem_segment Vector.t;
  10. data_count : int32 option;
  11. code : Ast.func Vector.t;
  12. datas : Ast.data_segment Vector.t;
}

Accumulator of parsed fields

type decode_kont = {
  1. building_state : building_state;
    (*

    Accumulated parsed sections, used to build the final module.

    *)
  2. module_kont : module_kont;
    (*

    Module continuation.

    *)
  3. allocation_state : Ast.allocations;
    (*

    Basic blocks allocated.

    *)
  4. stream_pos : int;
  5. stream_name : string;
}

Decoding continuation step.

val make_stream : name:string -> bytes:Mavryk_lazy_containers.Chunked_byte_vector.t -> stream

make_stream filename bytes returns a new stream to decode.

val initial_decode_kont : name:string -> decode_kont

initial_decode_kont ~name returns the initial tick state to be fed to module_step, such that name is the name of the input (generally the name of the file that contains said input).

val module_step : allow_floats:bool -> Mavryk_lazy_containers.Chunked_byte_vector.t -> decode_kont -> decode_kont Lwt.t

module_step ~allow_floats stream kont takes one step of parsing from a continuation and returns a new continuation. Fails when the continuation of the module is MKStop since it cannot reduce.

  • raises Floating_point.Error

    if it decodes a float instruction or type and allow_floats is false.

val decode : allow_floats:bool -> name:string -> bytes:Mavryk_lazy_containers.Chunked_byte_vector.t -> Ast.module_ Lwt.t

decode ~name ~bytes decodes a module name from its bytes encoding.

  • raises Code

    on parsing errors.

  • raises Floating_point.Error

    if it decodes a float instruction or type and allow_floats is false.

val decode_custom : Ast.name -> name:string -> bytes:Mavryk_lazy_containers.Chunked_byte_vector.t -> string list Lwt.t

decode ~name ~bytes decodes a custom section of name name from its bytes encoding.

  • raises Code

    on parsing errors.