diff --git a/ml-proto/host/script.ml b/ml-proto/host/script.ml index 1fe8bb512b..53804fcfe9 100644 --- a/ml-proto/host/script.ml +++ b/ml-proto/host/script.ml @@ -25,7 +25,7 @@ let trace name = if !Flags.trace then print_endline ("-- " ^ name) let current_module : Eval.instance option ref = ref None let eval_args es at = - let evs = List.map Eval.eval es in + let evs = List.map Eval.host_eval es in let reject_none = function | Some v -> v | None -> Error.error at "unexpected () value" in @@ -88,7 +88,7 @@ let run_command cmd = let m = get_module cmd.at in let arg_vs = eval_args arg_es cmd.at in let got_v = Eval.invoke m name arg_vs in - let expect_v = Eval.eval expect_e in + let expect_v = Eval.host_eval expect_e in (match got_v, expect_v with | Some Int32 got_i32, Some Int32 expect_i32 -> if got_i32 <> expect_i32 then begin diff --git a/ml-proto/spec/check.ml b/ml-proto/spec/check.ml index d42de9d2fc..921dcb8766 100644 --- a/ml-proto/spec/check.ml +++ b/ml-proto/spec/check.ml @@ -22,13 +22,10 @@ type context = tables : func_type list; locals : value_type list; return : expr_type; - labels : expr_type list + labels : expr_type list; + has_memory : bool } -let c0 = - {funcs = []; imports = []; tables = []; - locals = []; return = None; labels = []} - let lookup category list x = try List.nth list x.it with Failure _ -> error x.at ("unknown " ^ category ^ " " ^ string_of_int x.it) @@ -215,12 +212,15 @@ let rec check_expr c et e = check_type (Some t) et e.at | PageSize -> + check_has_memory c e.at; check_type (Some Int32Type) et e.at | MemorySize -> + check_has_memory c e.at; check_type (Some Int32Type) et e.at | ResizeMemory e -> + check_has_memory c e.at; check_expr c (Some Int32Type) e; check_type None et e.at @@ -243,16 +243,21 @@ and check_arm c t et arm = check_expr c (if fallthru then None else et) e and check_load c et memop e1 at = + check_has_memory c at; check_align memop.align at; check_expr c (Some Int32Type) e1; check_type (Some memop.ty) et at and check_store c et memop e1 e2 at = + check_has_memory c at; check_align memop.align at; check_expr c (Some Int32Type) e1; check_expr c (Some memop.ty) e2; check_type (Some memop.ty) et at +and check_has_memory c at = + require c.has_memory at "memory ops require a memory section"; + and check_align align at = Lib.Option.app (fun a -> require (Lib.Int.is_power_of_two a) at "non-power-of-two alignment") align @@ -281,14 +286,15 @@ let check_func c f = return = Lib.Option.map it result} in check_expr c' (Lib.Option.map it result) e -let check_table c tab = +let check_table funcs tables tab = match tab.it with | [] -> error tab.at "empty table" | x::xs -> - let s = func c x in - List.iter (fun xI -> check_func_type (func c xI) s xI.at) xs; - {c with tables = c.tables @ [s]} + let func x = lookup "function" funcs x in + let s = func x in + List.iter (fun xI -> check_func_type (func xI) s xI.at) xs; + tables @ [s] module NameSet = Set.Make(String) @@ -315,8 +321,13 @@ let check_memory memory = let check_module m = let {imports; exports; tables; funcs; memory} = m.it in Lib.Option.app check_memory memory; - let c = {c0 with funcs = List.map type_func funcs; - imports = List.map type_import imports} in - let c' = List.fold_left check_table c tables in - List.iter (check_func c') funcs; - ignore (List.fold_left (check_export c') NameSet.empty exports) + let func_types = List.map type_func funcs in + let c = {funcs = func_types; + imports = List.map type_import imports; + tables = List.fold_left (check_table func_types) [] tables; + locals = []; + return = None; + labels = []; + has_memory = memory <> None} in + List.iter (check_func c) funcs; + ignore (List.fold_left (check_export c) NameSet.empty exports) diff --git a/ml-proto/spec/eval.ml b/ml-proto/spec/eval.ml index 0a074e6c1b..61e011a112 100644 --- a/ml-proto/spec/eval.ml +++ b/ml-proto/spec/eval.ml @@ -25,7 +25,7 @@ type instance = imports : import list; exports : export_map; tables : func list list; - memory : Memory.t; + memory : Memory.t option; host : host_params } @@ -88,6 +88,11 @@ let numerics_error at = function error at "runtime: invalid conversion to integer" | exn -> raise exn +let some_memory c at = + match c.module_.memory with + | Some m -> m + | _ -> error at "memory operation but no memory section" + let some v at = match v with | Some v -> v @@ -169,31 +174,31 @@ let rec eval_expr (c : config) (e : expr) = Some v1 | Load ({ty; align = _}, e1) -> + let mem = some_memory c e.at in let v1 = some (eval_expr c e1) e1.at in let a = Memory.address_of_value v1 in - (try Some (Memory.load c.module_.memory a ty) - with exn -> memory_error e.at exn) + (try Some (Memory.load mem a ty) with exn -> memory_error e.at exn) | Store ({ty = _; align = _}, e1, e2) -> + let mem = some_memory c e.at in let v1 = some (eval_expr c e1) e1.at in let v2 = some (eval_expr c e2) e2.at in let a = Memory.address_of_value v1 in - (try Memory.store c.module_.memory a v2 - with exn -> memory_error e.at exn); + (try Memory.store mem a v2 with exn -> memory_error e.at exn); Some v2 | LoadExtend ({memop = {ty; align = _}; sz; ext}, e1) -> + let mem = some_memory c e.at in let v1 = some (eval_expr c e1) e1.at in let a = Memory.address_of_value v1 in - (try Some (Memory.load_extend c.module_.memory a sz ext ty) - with exn -> memory_error e.at exn) + (try Some (Memory.load_extend mem a sz ext ty) with exn -> memory_error e.at exn) | StoreWrap ({memop = {ty; align = _}; sz}, e1, e2) -> + let mem = some_memory c e.at in let v1 = some (eval_expr c e1) e1.at in let v2 = some (eval_expr c e2) e2.at in let a = Memory.address_of_value v1 in - (try Memory.store_wrap c.module_.memory a sz v2 - with exn -> memory_error e.at exn); + (try Memory.store_wrap mem a sz v2 with exn -> memory_error e.at exn); Some v2 | Const v -> @@ -235,14 +240,16 @@ let rec eval_expr (c : config) (e : expr) = Some (Int32 (page_size c)) | MemorySize -> - Some (Int32 (I32.of_int32 (Int32.of_int (Memory.size c.module_.memory)))) + let mem = some_memory c e.at in + Some (Int32 (I32.of_int32 (Int32.of_int (Memory.size mem)))) | ResizeMemory e -> + let mem = some_memory c e.at in let i = int32 (eval_expr c e) e.at in if (I32.rem_u i (page_size c)) <> I32.zero then error e.at "runtime: resize_memory operand not multiple of page_size"; (* TODO: The conversion to int could overflow. *) - Memory.resize c.module_.memory (Int32.to_int i); + Memory.resize mem (Int32.to_int i); None and eval_expr_option c eo = @@ -272,36 +279,32 @@ and eval_func (m : instance) (f : func) (evs : value list) = (* Modules *) -let init_memory ast = - match ast with - | None -> - Memory.create 0 - | Some {it = {initial; segments; _}} -> - let mem = Memory.create initial in - Memory.init mem (List.map it segments); - mem +let init_memory {it = {initial; segments; _}} = + let mem = Memory.create initial in + Memory.init mem (List.map it segments); + mem let init m imports host = assert (List.length imports = List.length m.it.Ast.imports); assert (host.page_size > 0); assert (Lib.Int.is_power_of_two host.page_size); let {Ast.exports; tables; funcs; memory; _} = m.it in - let mem = init_memory memory in + let memory' = Lib.Option.map init_memory memory in let func x = List.nth funcs x.it in let export ex = ExportMap.add ex.it.name (func ex.it.func) in let exports = List.fold_right export exports ExportMap.empty in let tables = List.map (fun tab -> List.map func tab.it) tables in - {funcs; imports; exports; tables; memory = mem; host} + {funcs; imports; exports; tables; memory = memory'; host} let invoke m name vs = let f = export m (name @@ no_region) in assert (List.length vs = List.length f.it.params); eval_func m f vs -let eval e = +(* This function is not part of the spec. *) +let host_eval e = let f = {params = []; result = None; locals = []; body = e} @@ no_region in - let memory = Memory.create 0 in let exports = ExportMap.singleton "eval" f in let host = {page_size = 1} in - let m = {imports = []; exports; tables = []; funcs = [f]; memory; host} in + let m = {imports = []; exports; tables = []; funcs = [f]; memory = None; host} in eval_func m f [] diff --git a/ml-proto/spec/eval.mli b/ml-proto/spec/eval.mli index 4c737a0103..2442bfe13f 100644 --- a/ml-proto/spec/eval.mli +++ b/ml-proto/spec/eval.mli @@ -10,4 +10,6 @@ type host_params = {page_size : Memory.size} val init : Ast.module_ -> import list -> host_params -> instance val invoke : instance -> string -> value list -> value option (* raise Error.Error *) -val eval : Ast.expr -> value option (* raise Error.Error *) + +(* This function is not part of the spec. *) +val host_eval : Ast.expr -> value option (* raise Error.Error *) diff --git a/ml-proto/test/memory.wast b/ml-proto/test/memory.wast index 2ec068f3c0..f27a8b82cb 100644 --- a/ml-proto/test/memory.wast +++ b/ml-proto/test/memory.wast @@ -35,29 +35,29 @@ ) ;; Test alignment annotation rules -(module (func (i32.load8_u/2 (i32.const 0)))) -(module (func (i32.load16_u/4 (i32.const 0)))) -(module (func (i32.load/8 (i32.const 0)))) -(module (func (f32.load/8 (i32.const 0)))) +(module (memory 0) (func (i32.load8_u/2 (i32.const 0)))) +(module (memory 0) (func (i32.load16_u/4 (i32.const 0)))) +(module (memory 0) (func (i32.load/8 (i32.const 0)))) +(module (memory 0) (func (f32.load/8 (i32.const 0)))) (assert_invalid - (module (func (i64.load/0 (i32.const 0)))) + (module (memory 0) (func (i64.load/0 (i32.const 0)))) "non-power-of-two alignment" ) (assert_invalid - (module (func (i64.load/3 (i32.const 0)))) + (module (memory 0) (func (i64.load/3 (i32.const 0)))) "non-power-of-two alignment" ) (assert_invalid - (module (func (i64.load/5 (i32.const 0)))) + (module (memory 0) (func (i64.load/5 (i32.const 0)))) "non-power-of-two alignment" ) (assert_invalid - (module (func (i64.load/6 (i32.const 0)))) + (module (memory 0) (func (i64.load/6 (i32.const 0)))) "non-power-of-two alignment" ) (assert_invalid - (module (func (i64.load/7 (i32.const 0)))) + (module (memory 0) (func (i64.load/7 (i32.const 0)))) "non-power-of-two alignment" )