1(* This module exposes an [interpret] function to Rust. It wraps several
2different calls from the WebAssembly specification interpreter in a way that we
3can access across the FFI boundary. To understand this better, see:
4 - the OCaml manual documentation re: calling OCaml from C,
5 https://ocaml.org/manual/intfc.html#s%3Ac-advexample
6 - the [ocaml-interop] example,
7 https://github.com/tezedge/ocaml-interop/blob/master/testing/rust-caller/ocaml/callable.ml
8*)
9
10(** Enumerate the types of values we pass across the FFI boundary. This must
11match `Value` in `src/lib.rs` *)
12type ffi_value =
13  | I32 of int32
14  | I64 of int64
15  | F32 of int32
16  | F64 of int64
17  | V128 of Bytes.t
18
19(** Enumerate the kinds of exported values the interpreter can retrieve. *)
20type ffi_export_value =
21  | Global of ffi_value
22  | Memory of Bytes.t
23
24(* Here we access the WebAssembly specification interpreter; this must be linked
25in. *)
26open Wasm
27open Wasm.WasmRef_Isa_m.WasmRef_Isa
28
29type spec_instance = (unit module_export_ext list * ((unit s_m_ext) ref))
30
31(** Helper for converting the FFI values to their spec interpreter type. *)
32let convert_to_wasm (v: ffi_value) : v = match v with
33| I32 n -> V_num (ConstInt32 (I32_impl_abs n))
34| I64 n -> V_num (ConstInt64 (I64_impl_abs n))
35| F32 n -> V_num (ConstFloat32 (F32.of_bits n))
36| F64 n -> V_num (ConstFloat64 (F64.of_bits n))
37| V128 n -> V_vec (ConstVec128 (V128.of_bits (Bytes.to_string n)))
38
39(** Helper for converting the spec interpreter values to their FFI type. *)
40let convert_from_wasm (v: v) : ffi_value = match v with
41| V_num ((ConstInt32 (I32_impl_abs n))) -> I32 n
42| V_num ((ConstInt64 (I64_impl_abs n))) -> I64 n
43| V_num ((ConstFloat32 n)) -> F32 (F32.to_bits n)
44| V_num ((ConstFloat64 n)) -> F64 (F64.to_bits n)
45| V_vec ((ConstVec128 n)) -> V128 (Bytes.of_string (V128.to_bits n))
46
47(** Parse the given WebAssembly module binary into an Ast.module_. At some point
48in the future this should also be able to parse the textual form (TODO). *)
49let parse bytes =
50  (* Optionally, use Bytes.unsafe_to_string here to avoid the copy *)
51  let bytes_as_str = Bytes.to_string bytes in
52  (Decode.decode "default" bytes_as_str)
53
54(** Construct an instance from a sequence of WebAssembly bytes. This clears the
55previous contents of the global store *)
56let instantiate_exn module_bytes : spec_instance =
57  let s = (make_empty_store_m ()) in
58  let module_ = parse module_bytes in
59  let m_isa = Ast_convert.convert_module (module_.it) in
60  (match interp_instantiate_init_m s m_isa [] () with
61  | (s', (RI_res_m(inst,v_exps,_))) -> (v_exps, ref s')
62  | (s', (RI_trap_m str)) -> raise (Eval.Trap (Source.no_region, "(Isabelle) trap: " ^ str))
63  | (s', (RI_crash_m (Error_exhaustion str))) -> raise (Eval.Exhaustion (Source.no_region, "(Isabelle) call stack exhausted"))
64  | (s', (RI_crash_m (Error_invalid str))) -> raise (Eval.Crash (Source.no_region, "(Isabelle) error: " ^ str))
65  | (s', (RI_crash_m (Error_invariant str))) -> raise (Eval.Crash (Source.no_region, "(Isabelle) error: " ^ str))
66  )
67
68let instantiate module_bytes =
69  try Ok(instantiate_exn module_bytes) with
70  | _ as e -> Error(Printexc.to_string e)
71
72(** Retrieve the value of an export by name from a WebAssembly instance. *)
73let export_exn (inst_s : spec_instance) (name : string) : ffi_export_value =
74  let (inst, s_ref) = inst_s in
75  match (e_desc (List.find (fun exp -> String.equal (e_name exp) name) inst)) with
76    Ext_func _ -> raise Not_found
77  | Ext_tab _ -> raise Not_found
78  | Ext_mem i -> Memory (fst (Array.get (mems (!s_ref)) (Z.to_int (integer_of_nat i))))
79  | Ext_glob i -> Global (convert_from_wasm (g_val (Array.get (globs (!s_ref)) (Z.to_int (integer_of_nat i)))))
80
81let export inst name =
82  try Ok(export_exn inst name) with
83  | _ as e -> Error(Printexc.to_string e)
84
85(** Interpret the first exported function and return the result. Use provided
86parameters if they exist, otherwise use default (zeroed) values. *)
87let interpret_legacy_exn module_bytes opt_params =
88  let opt_params_ = Option.map (List.rev_map convert_to_wasm) opt_params in
89  let module_ = parse module_bytes in
90  let m_isa = Ast_convert.convert_module (module_.it) in
91  let fuel = Z.of_string "4611686018427387904" in
92  let max_call_depth = Z.of_string "300" in
93  (match run_fuzz (nat_of_integer fuel) (nat_of_integer max_call_depth) (make_empty_store_m ()) m_isa [] opt_params_ () with
94  | (s', RValue vs_isa') -> List.rev_map convert_from_wasm vs_isa'
95  | (s', RTrap str) -> raise (Eval.Trap (Source.no_region, "(Isabelle) trap: " ^ str))
96  | (s', (RCrash (Error_exhaustion str))) -> raise (Eval.Exhaustion (Source.no_region, "(Isabelle) call stack exhausted"))
97  | (s', (RCrash (Error_invalid str))) -> raise (Eval.Crash (Source.no_region, "(Isabelle) error: " ^ str))
98  | (s', (RCrash (Error_invariant str))) -> raise (Eval.Crash (Source.no_region, "(Isabelle) error: " ^ str))
99  )
100
101let interpret_legacy module_bytes opt_params =
102  try Ok(interpret_legacy_exn module_bytes opt_params) with
103  | _ as e -> Error(Printexc.to_string e)
104
105(* process an optional list of params, generating default params if necessary *)
106(* TODO: this should be done in the Isabelle model *)
107let get_param_vs s_ref (vs_opt :(ffi_value list) option) i =
108  (match vs_opt with
109   | None -> (match cl_m_type ((array_nth heap_cl_m (funcs !s_ref) i) ()) with Tf (t1, _) -> map bitzero t1)
110   | Some vs -> List.map convert_to_wasm vs)
111
112(** Interpret the function exported at name. Use provided
113parameters if they exist, otherwise use default (zeroed) values. *)
114let interpret_exn (inst_s : spec_instance) (name : string) opt_params =
115  (let fuel = Z.of_string "4611686018427387904" in
116   let max_call_depth = Z.of_string "300" in
117   let (inst, s_ref) = inst_s in
118   match (e_desc (List.find (fun exp -> String.equal (e_name exp) name) inst)) with
119   | Ext_func i ->
120       (let params = get_param_vs s_ref opt_params i in
121        let (s', res) = run_invoke_v_m (nat_of_integer fuel) (nat_of_integer max_call_depth) ((!s_ref), (params, i)) () in
122        s_ref := s';
123        (match res with
124         | RValue vs_isa' -> List.rev_map convert_from_wasm vs_isa'
125         | RTrap str -> raise (Eval.Trap (Source.no_region, "(Isabelle) trap: " ^ str))
126         | (RCrash (Error_exhaustion str)) -> raise (Eval.Exhaustion (Source.no_region, "(Isabelle) call stack exhausted"))
127         | (RCrash (Error_invalid str)) -> raise (Eval.Crash (Source.no_region, "(Isabelle) error: " ^ str))
128         | (RCrash (Error_invariant str)) -> raise (Eval.Crash (Source.no_region, "(Isabelle) error: " ^ str))
129        ))
130   | _ -> raise Not_found)
131
132let interpret inst name opt_params =
133  try Ok(interpret_exn inst name opt_params) with
134  | _ as e -> Error(Printexc.to_string e)
135
136let () =
137  Callback.register "instantiate" instantiate;
138  Callback.register "interpret_legacy" interpret_legacy;
139  Callback.register "interpret" interpret;
140  Callback.register "export" export;
141