instruction-level block types declaration

[Laplace-Demon]

In binary_encoder.ml, we acquiesce block types should not have index. These indices are removed by function bt_some_to_raw in the rewriting phase, which checks inline types' correspondence with the type section.

let write_block_type buf (typ : binary block_type option) =
  match typ with
  | None | Some (Bt_raw (None, ([], []))) -> Buffer.add_char buf '\x40'
  | Some (Bt_raw (None, ([], [ vt ]))) -> write_valtype buf vt
  | Some (Bt_raw (None, (pt, _))) -> write_paramtype buf pt
  (* TODO: memo
     will this pattern matching be enough with the use of the new modul.types field?
  *)
  | _ -> assert false (* TODO: same, new pattern matching cases ? *)

 let bt_some_to_raw : text block_type -> binary block_type Result.t = function
    | Bt_ind ind -> begin
      let+ v = get (`Unknown_type ind) modul.typ ind in
      match Indexed.get v with
      | Def_func_t t' ->
        let idx = Indexed.get_index v in
        Bt_raw (Some (Raw idx), t')
      | _ -> assert false
    end
    | Bt_raw (type_use, t) -> (
      let* t = Binary_types.convert_func_type None t in
      match type_use with
      | None -> Ok (Bt_raw (None, t))
      | Some ind ->
        (* we check that the explicit type match the type_use, we have to remove parameters names to do so *)
        let* t' =
          let+ v = get (`Unknown_type ind) modul.typ ind in
          match Indexed.get v with Def_func_t t' -> t' | _ -> assert false
        in
        let ok = Types.func_type_eq t t' in
        if not ok then Error `Inline_function_type else Ok (Bt_raw (None, t)) )

This would make the encoding of inline function-like block types invalid. For example :

$ cat block_type.wat
(module
  (func
    i32.const 1
    (block (param i32) (result i32)
      i32.const 1
      i32.add
    )
    drop
  )
  (start 0)
)
$ owi wat2wasm block_type.wat
$ owi wasm2wat block_type.wasm
owi: internal error, uncaught exception:
     Invalid_argument("index out of bounds")

Here, block (param i32) (result i32) is encoded as 0x02 (for block) 0x01 0x7F (for param i32, but I think it should be 0x7F for representing the inline value type i32). And in reality, the first 0x01 would be parsed as type index, and the second 0x7F parsed as the instruction i64.div_s, making arraying indexing out of bounds.

In contrast, function types are added in the grouping phase by declare_func_type, and rewrited in the rewriting phase by rewrite_block_type, to assign them a type index. I think we should do the same thing to inline block types.

(In the reference interpreter, block types are also added to the types section :

$ cat block_type.wat
(module
  (func
    i32.const 1
    (loop (param i32) (result i32)
      i32.const 1
      i32.add
    )
    drop
  )
  (start 0)
)
$ ./wasm block_type.wat -o block_type.wasm
$ ./wasm block_type.wasm -o block_type.ref.wat
$ cat block_type.ref.wat 
(module
  (type $0 (func))
  (type $1 (func (param i32) (result i32)))
  (func $0
    (type 0)
    (i32.const 1)
    (loop (type 1) (i32.const 1) (i32.add))
    (drop)
  )
  (start 0)
)

)

[zapashcanon]

Thanks a lot for fixing this! I had a quick look but it seems quite good to me. Can you add a test ? The one in your PR description looks good to me. It may be worth to add one for loop and other instructions ?

[zapashcanon]

Thanks!