Using and defining external functions (host functions)

Dealing with the Stack

Given the following extern.wat file:

(module $extern

  (import "sausage" "fresh"
    (func $fresh (param i32) (result externref)))

  (import "sausage" "get_i32r"
    (func $get (param externref) (result i32)))

  (import "sausage" "set_i32r"
    (func $set (param externref) (param i32)))

  (import "sausage" "print_i32"
    (func $print_i32 (param i32)))

  (func $start (local $ref externref)

    ;; let ref = fresh 42
    (local.set $ref (call $fresh (i32.const 42)))

    ;; print_i32 (get ref)
    (call $print_i32 (call $get (local.get $ref)))

    ;; set ref 13
    (call $set (local.get $ref) (i32.const 13)  )

    ;; print_i32 (get ref)
    (call $print_i32 (call $get (local.get $ref)))

  )

  (start $start)
)

You can define the various required external functions in OCaml like this :

open Owi

(* an extern module that will be linked with a wasm module *)
let extern_module : Concrete_extern.Module.t =
  (* some custom functions *)
  let rint : Concrete_i32.t ref Type.Id.t = Type.Id.make () in
  let fresh i = Concrete_choice.return (ref i) in
  let set r (i : Concrete_i32.t) =
    r := i;
    Concrete_choice.return ()
  in
  let get r = Concrete_choice.return !r in
  let print_i32 (i : Concrete_i32.t) =
    Format.printf "%a\n%!" Concrete_i32.pp i;
    Concrete_choice.return ()
  in
  (* we need to describe their types *)
  let open Concrete_extern.Func in
  let open Concrete_extern.Func.Syntax in
  [ ("print_i32", Extern_func (i32 ^->. unit, print_i32))
  ; ("fresh", Extern_func (i32 ^->. externref rint, fresh))
  ; ("set_i32r", Extern_func (externref rint ^-> i32 ^->. unit, set))
  ; ("get_i32r", Extern_func (externref rint ^->. i32, get))
  ]

(* an environment that contains our custom module, available under the name `sausage` *)
let env =
  let env = Env.Concrete.empty ~context:() in
  Env.Concrete.link_extern_module ~env ~name:"sausage" extern_module
  |> Stdlib.Result.get_ok

(* a pure wasm module refering to `sausage` *)
let pure_wasm_module =
  Parse.Text.Module.from_file (Fpath.v "extern.wat") |> Stdlib.Result.get_ok

(* our pure wasm module, linked with `sausage` *)
let modul, env =
  Compile.Text.until_concrete_link env ~unsafe:false ~name:None pure_wasm_module
  |> Stdlib.Result.get_ok

module I = Interpret.Concrete (Interpret.Default_parameters)

let to_run = I.modul ~env ~modul

(* let's run it ! it will print the values as defined in the print_i32 function *)
let () =
  match Concrete_choice.run to_run Concrete_state.empty with
  | Error _o -> assert false
  | Ok (_env, _state) -> ()

You’ll get the expected result:

$ ./extern.exe
42
13

Dealing with the Linear Memory

Owi also allows interacting with linear memory through external functions. This is helpful because it enables the host system to communicate directly with a Wasm instance through its linear memory. Consider the tiny example below to illustrate this:

(module $extern_mem

  (import "chorizo" "memset" (func $memset (param i32 i32 i32)))

  (import "chorizo" "print_x64" (func $print_x64 (param i64)))

  (memory 1)

  (func $start

    ;; memset 0 0xAA 8
    (call $memset (i32.const 0) (i32.const 0xAA) (i32.const 8))

    ;; print_x64 (load 0)
    (call $print_x64 (i64.load (i32.const 0)))
  )

  (start $start)
)

In the module $extern_mem, we first import $memset and $print_x64. Then, in the $start function, we initialize the memory starting at address (i32.const 0) with a sequence of length (i32.const 8) with bytes of (i32.const 0xAA).

The definition of the external functions follows the same format as the [previous example]. The difference is that, now, in the GADT definition of memset to allow the memory to be passed to this function, we need to wrap the three I32 arguments in a Mem variant. That is, instead of writing memset as:

(Func (Arg (I32, (Arg (I32, (Arg (I32, Res))))), R0), memset)

One should use:

(Func (Mem (Arg (I32, (Arg (I32, (Arg (I32, Res)))))), R0), memset)

See the module below for the whole implementation:

open Owi

(* an extern module that will be linked with a wasm module *)
let extern_module : Concrete_extern.Module.t =
  (* some custom functions *)
  let memset m start byte length : _ Concrete_choice.t =
    let rec loop offset : _ Concrete_choice.t =
      let b = Concrete_i32.le offset length |> Concrete_boolean.to_bool in
      if b then
        let to_run =
          Concrete_memory.store_8 m ~addr:(Concrete_i32.add start offset) byte
        in
        begin match
          Concrete_choice.run_and_drop_state to_run Concrete_state.empty
        with
        | Error e -> Concrete_choice.trap e
        | Ok _mem -> loop (Concrete_i32.add offset (Concrete_i32.of_int 1))
        end
      else Concrete_choice.return ()
    in
    loop Concrete_i32.zero
  in
  let print_x64 (n : Concrete_i64.t) =
    let n = Concrete_i64.to_int64 n in
    Format.printf "0x%LX@\n" n;
    Concrete_choice.return ()
  in
  (* we need to describe their types *)
  let open Concrete_extern.Func in
  let open Concrete_extern.Func.Syntax in
  [ ("print_x64", Extern_func (i64 ^->. unit, print_x64))
  ; ("memset", Extern_func (memory 0 ^-> i32 ^-> i32 ^-> i32 ^->. unit, memset))
  ]

(* an environment that contains our custom module, available under the name `chorizo` *)
let env =
  let env = Env.Concrete.empty ~context:() in
  Env.Concrete.link_extern_module ~env ~name:"chorizo" extern_module
  |> Stdlib.Result.get_ok

(* a pure wasm module refering to `$extern_mem` *)
let pure_wasm_module =
  match Parse.Text.Module.from_file (Fpath.v "extern_mem.wat") with
  | Error _ -> assert false
  | Ok modul -> modul

(* our pure wasm module, linked with `chorizo` *)
let modul, env =
  match
    Compile.Text.until_concrete_link env ~unsafe:false ~name:None
      pure_wasm_module
  with
  | Error _ -> assert false
  | Ok v -> v

module I = Interpret.Concrete (Interpret.Default_parameters)

(* let's run it ! it will print the values as defined in the print_i64 function *)
let to_run = I.modul ~env ~modul

let () =
  match Concrete_choice.run to_run Concrete_state.empty with
  | Error _ -> assert false
  | Ok (_env, _state) -> ()

Running the above program should yield:

$ ./extern_mem.exe
0xAAAAAAAAAAAAAAAA