diff --git a/ml-proto/host/parser.mly b/ml-proto/host/parser.mly index e8f4f239ce..814b15fc5e 100644 --- a/ml-proto/host/parser.mly +++ b/ml-proto/host/parser.mly @@ -200,9 +200,9 @@ expr1 : | BINARY expr expr { fun c -> binary ($1, $2 c, $3 c) } | COMPARE expr expr { fun c -> compare ($1, $2 c, $3 c) } | CONVERT expr { fun c -> convert ($1, $2 c) } - | PAGE_SIZE { fun c -> page_size } - | MEMORY_SIZE { fun c -> memory_size } - | RESIZE_MEMORY expr { fun c -> resize_memory ($2 c) } + | PAGE_SIZE { fun c -> host (PageSize, []) } + | MEMORY_SIZE { fun c -> host (MemorySize, []) } + | RESIZE_MEMORY expr { fun c -> host (ResizeMemory, [$2 c]) } ; expr_opt : | /* empty */ { fun c -> None } diff --git a/ml-proto/spec/ast.ml b/ml-proto/spec/ast.ml index 0bd14c35e6..425feff10e 100644 --- a/ml-proto/spec/ast.ml +++ b/ml-proto/spec/ast.ml @@ -66,6 +66,11 @@ type cvt = (Int32Op.cvt, Int64Op.cvt, Float32Op.cvt, Float64Op.cvt) op type memop = {ty : Types.value_type; align : int option} type extop = {memop : memop; sz : Memory.mem_size; ext : Memory.extension} type wrapop = {memop : memop; sz : Memory.mem_size} +type hostop = + | PageSize (* inquire host-defined page size *) + | MemorySize (* inquire current size of linear memory *) + | ResizeMemory (* resize linear memory *) + (* Expressions *) @@ -95,9 +100,7 @@ and expr' = | Binary of binop * expr * expr (* binary arithmetic operator *) | Compare of relop * expr * expr (* arithmetic comparison *) | Convert of cvt * expr (* conversion *) - | PageSize (* return host-defined page_size *) - | MemorySize (* return current size of linear memory *) - | ResizeMemory of expr (* resize linear memory *) + | Host of hostop * expr list (* host interaction *) and case = case' Source.phrase and case' = diff --git a/ml-proto/spec/check.ml b/ml-proto/spec/check.ml index 92a1cad6f3..00ebc651ad 100644 --- a/ml-proto/spec/check.ml +++ b/ml-proto/spec/check.ml @@ -89,6 +89,12 @@ let type_cvt at = function | DemoteFloat64 -> error at "invalid conversion" ), Float64Type +let type_hostop = function + | PageSize -> {ins = []; out = Some Int32Type} + | MemorySize -> {ins = []; out = Some Int32Type} + | ResizeMemory -> {ins = [Int32Type]; out = None} + + let type_func f = let {params; result; _} = f.it in {ins = List.map it params; out = Lib.Option.map it result} @@ -136,7 +142,7 @@ let rec check_expr c et e = check_expr c' et e1 | Break (x, eo) -> - check_expr_option c (label c x) eo e.at + check_expr_opt c (label c x) eo e.at | Switch (t, e1, cs, e2) -> require (t.it = Int32Type || t.it = Int64Type) t.at "invalid switch type"; @@ -208,25 +214,18 @@ let rec check_expr c et e = check_expr c (Some t1) e1; check_type (Some t) et e.at - | PageSize -> - check_has_memory c e.at; - check_type (Some Int32Type) et e.at - - | MemorySize -> + | Host (hostop, es) -> 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 + let {ins; out} = type_hostop hostop in + check_exprs c ins es; + check_type out et e.at and check_exprs c ts es = let ets = List.map (fun x -> Some x) ts in try List.iter2 (check_expr c) ets es with Invalid_argument _ -> error (Source.ats es) "arity mismatch" -and check_expr_option c et eo at = +and check_expr_opt c et eo at = match eo with | Some e -> check_expr c et e | None -> check_type None et at @@ -253,7 +252,7 @@ and check_store c et memop e1 e2 at = check_type (Some memop.ty) et at and check_has_memory c at = - require c.has_memory at "memory ops require a memory section"; + require c.has_memory at "memory operators require a memory section" and check_align align at = Lib.Option.app (fun a -> diff --git a/ml-proto/spec/eval.ml b/ml-proto/spec/eval.ml index a55ebcae51..16c60040aa 100644 --- a/ml-proto/spec/eval.ml +++ b/ml-proto/spec/eval.ml @@ -143,7 +143,7 @@ let rec eval_expr (c : config) (e : expr) = (try eval_expr c' e1 with L.Label vo -> vo) | Break (x, eo) -> - raise (label c x (eval_expr_option c eo)) + raise (label c x (eval_expr_opt c eo)) | Switch (_t, e1, cs, e2) -> let vo = some (eval_expr c e1) e1.at in @@ -189,7 +189,8 @@ let rec eval_expr (c : config) (e : expr) = | LoadExtend ({memop = {ty; align = _}; sz; ext}, e1) -> let mem = some_memory c e.at in let v1 = mem_size (eval_expr c e1) e1.at in - (try Some (Memory.load_extend mem v1 sz ext ty) with exn -> memory_error e.at exn) + (try Some (Memory.load_extend mem v1 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 @@ -233,25 +234,12 @@ let rec eval_expr (c : config) (e : expr) = | Arithmetic.TypeError (_, v, t) -> type_error e1.at v t | exn -> numerics_error e.at exn) - | PageSize -> - Some (Int32 (Int64.to_int32 c.instance.host.page_size)) - - | MemorySize -> + | Host (hostop, es) -> + let vs = List.map (eval_expr c) es in let mem = some_memory c e.at in - let i64 = Memory.size mem in - assert (i64 < Int64.of_int32 (Int32.max_int)); - Some (Int32 (Int64.to_int32 i64)) + eval_hostop c.instance.host mem hostop vs e.at - | ResizeMemory e -> - let mem = some_memory c e.at in - let sz = mem_size (eval_expr c e) e.at in - if (Int64.rem sz c.instance.host.page_size) <> 0L then - error e.at "runtime: resize_memory operand not multiple of page_size"; - Memory.resize mem sz; - None - -and eval_expr_option c eo = - match eo with +and eval_expr_opt c = function | Some e -> eval_expr c e | None -> None @@ -273,6 +261,28 @@ and eval_func (m : instance) (f : func) (evs : value list) = eval_expr c f.it.body +(* Host operators *) + +and eval_hostop host mem hostop vs at = + match hostop, vs with + | PageSize, [] -> + Some (Int32 (Int64.to_int32 host.page_size)) + + | MemorySize, [] -> + assert (Memory.size mem < Int64.of_int32 Int32.max_int); + Some (Int32 (Int64.to_int32 (Memory.size mem))) + + | ResizeMemory, [v] -> + let sz = mem_size v at in + if Int64.rem sz host.page_size <> 0L then + error at "runtime: resize_memory operand not multiple of page_size"; + Memory.resize mem sz; + None + + | _, _ -> + error at "runtime: invalid invocation of host operator" + + (* Modules *) let init_memory {it = {initial; segments; _}} = @@ -304,5 +314,5 @@ let host_eval e = let f = {params = []; result = None; locals = []; body = e} @@ no_region in let exports = ExportMap.singleton "eval" f in let host = {page_size = 1L} in - let m = {imports = []; exports; tables = []; funcs = [f]; memory = None; host} in - eval_func m f [] + let m = {imports = []; exports; tables = []; funcs = [f]; memory = None; host} + in eval_func m f [] diff --git a/ml-proto/spec/memory.ml b/ml-proto/spec/memory.ml index 336a36ffd5..9abd21b835 100644 --- a/ml-proto/spec/memory.ml +++ b/ml-proto/spec/memory.ml @@ -22,6 +22,7 @@ exception Type exception Bounds exception Address + (* * These limitations should be considered part of the host environment and not * part of the spec defined by this file. diff --git a/ml-proto/spec/memory.mli b/ml-proto/spec/memory.mli index 2b3320a00d..e830307fcc 100644 --- a/ml-proto/spec/memory.mli +++ b/ml-proto/spec/memory.mli @@ -22,5 +22,6 @@ val size : memory -> size val resize : memory -> size -> unit val load : memory -> address -> value_type -> value val store : memory -> address -> value -> unit -val load_extend : memory -> address -> mem_size -> extension -> value_type -> value +val load_extend : + memory -> address -> mem_size -> extension -> value_type -> value val store_wrap : memory -> address -> mem_size -> value -> unit diff --git a/ml-proto/spec/sugar.ml b/ml-proto/spec/sugar.ml index 134bb4dd1b..7d4b8946ba 100644 --- a/ml-proto/spec/sugar.ml +++ b/ml-proto/spec/sugar.ml @@ -85,14 +85,8 @@ let compare (relop, e1, e2) = let convert (cvt, e) = Convert (cvt, e) -let page_size = - PageSize - -let memory_size = - MemorySize - -let resize_memory e = - ResizeMemory e +let host (hostop, es) = + Host (hostop, es) let case (c, br) = diff --git a/ml-proto/spec/sugar.mli b/ml-proto/spec/sugar.mli index 2cb3cdf3ca..6e82ee8840 100644 --- a/ml-proto/spec/sugar.mli +++ b/ml-proto/spec/sugar.mli @@ -25,9 +25,7 @@ val unary : unop * expr -> expr' val binary : binop * expr * expr -> expr' val compare : relop * expr * expr -> expr' val convert : cvt * expr -> expr' -val page_size : expr' -val memory_size : expr' -val resize_memory : expr -> expr' +val host : hostop * expr list -> expr' val case : literal * (expr list * bool) option -> case'