diff --git a/ml-proto/src/host/lexer.mll b/ml-proto/src/host/lexer.mll index 69174e2ee1..7686927a2d 100644 --- a/ml-proto/src/host/lexer.mll +++ b/ml-proto/src/host/lexer.mll @@ -60,31 +60,25 @@ let floatop t f32 f64 = | "f64" -> Values.Float64 f64 | _ -> assert false -let mem_type mty = - let open Memory in - match mty with - | "i8" -> Int8Mem - | "i16" -> Int16Mem - | "i32" -> Int32Mem - | "i64" -> Int64Mem - | "f32" -> Float32Mem - | "f64" -> Float64Mem +let memop t a = + {ty = value_type t; align = if a = "" then None else Some (int_of_string a)} + +let mem_size = function + | "8" -> Memory.Mem8 + | "16" -> Memory.Mem16 + | "32" -> Memory.Mem32 + | _ -> assert false + +let extension = function + | 's' -> Memory.SX + | 'u' -> Memory.ZX | _ -> assert false -let loadop t sign a = - let mem = mem_type t in - let ext = match sign with - | ' ' -> Memory.NX - | 's' -> Memory.SX - | 'u' -> Memory.ZX - | _ -> assert false in - let align = if a = "" then Memory.mem_size mem else int_of_string a in - {mem; ext; align} - -let storeop t a = - let mem = mem_type t in - let align = if a = "" then Memory.mem_size mem else int_of_string a in - {mem; align} +let extendop t sz s a = + {memop = memop t a; sz = mem_size sz; ext = extension s} + +let truncop t sz a = + {memop = memop t a; sz = mem_size sz} } let space = [' ''\t'] @@ -110,7 +104,7 @@ let mixx = "i" ("8" | "16" | "32" | "64") let mfxx = "f" ("32" | "64") let sign = "s" | "u" let align = digit+ -let width = digit+ +let mem_size = "8" | "16" | "32" rule token = parse | "(" { LPAR } @@ -143,14 +137,19 @@ rule token = parse | "get_local" { GETLOCAL } | "set_local" { SETLOCAL } - | (nxx as t)".load" { LOAD (loadop t ' ' "") } - | (nxx as t)".load/"(align as a) { LOAD (loadop t ' ' a) } - | (ixx)".load"(width as w)"_"(sign as s) { LOAD (loadop ("i" ^ w) s "") } - | (ixx)".load"(width as w)"_"(sign as s)"/"(align as a) { LOAD (loadop ("i" ^ w) s a) } - | (nxx as t)".store" { STORE (storeop t "") } - | (nxx as t)".store/"(align as a) { STORE (storeop t a) } - | (ixx)".store"(width as w) { STORE (storeop ("i" ^ w) "") } - | (ixx)".store"(width as w)"/"(align as a) { STORE (storeop ("i" ^ w) a) } + | (nxx as t)".load" { LOAD (memop t "") } + | (nxx as t)".load/"(align as a) { LOAD (memop t a) } + | (nxx as t)".store" { STORE (memop t "") } + | (nxx as t)".store/"(align as a) { STORE (memop t a) } + + | (ixx as t)".load"(mem_size as sz)"_"(sign as s) + { LOADEXTEND (extendop t sz s "") } + | (ixx as t)".load"(mem_size as sz)"_"(sign as s)"/"(align as a) + { LOADEXTEND (extendop t sz s a) } + | (ixx as t)".store"(mem_size as sz) + { STORETRUNC (truncop t sz "") } + | (ixx as t)".store"(mem_size as sz)"/"(align as a) + { STORETRUNC (truncop t sz a) } | (nxx as t)".switch" { SWITCH (value_type t) } | (nxx as t)".const" { CONST (value_type t) } diff --git a/ml-proto/src/host/parser.mly b/ml-proto/src/host/parser.mly index 65ddf704fe..c671035a39 100644 --- a/ml-proto/src/host/parser.mly +++ b/ml-proto/src/host/parser.mly @@ -113,8 +113,10 @@ let anon_label c = {c with labels = VarMap.map ((+) 1) c.labels} %token BINARY %token COMPARE %token CONVERT -%token LOAD -%token STORE +%token LOAD +%token STORE +%token LOADEXTEND +%token STORETRUNC %start script %type script @@ -179,7 +181,9 @@ oper : | SETLOCAL var expr { fun c -> SetLocal ($2 c local, $3 c) } | LOAD expr { fun c -> Load ($1, $2 c) } | STORE expr expr { fun c -> Store ($1, $2 c, $3 c) } - | CONST literal { fun c -> Const (literal (ati 2) $2 $1) } + | LOADEXTEND expr { fun c -> LoadExtend ($1, $2 c) } + | STORETRUNC expr expr { fun c -> StoreTrunc ($1, $2 c, $3 c) } + | CONST literal { let at = at() in fun c -> Const (literal at $2 $1) } | UNARY expr { fun c -> Unary ($1, $2 c) } | BINARY expr expr { fun c -> Binary ($1, $2 c, $3 c) } | COMPARE expr expr { fun c -> Compare ($1, $2 c, $3 c) } diff --git a/ml-proto/src/spec/ast.ml b/ml-proto/src/spec/ast.ml index c6bb8cb927..1605f68b9b 100644 --- a/ml-proto/src/spec/ast.ml +++ b/ml-proto/src/spec/ast.ml @@ -63,9 +63,9 @@ type binop = (Int32Op.binop, Int64Op.binop, Float32Op.binop, Float64Op.binop) op type relop = (Int32Op.relop, Int64Op.relop, Float32Op.relop, Float64Op.relop) op type cvt = (Int32Op.cvt, Int64Op.cvt, Float32Op.cvt, Float64Op.cvt) op -type loadop = {mem : Memory.mem_type; ext : Memory.extension; align : int} -type storeop = {mem : Memory.mem_type; align : int} - +type memop = {ty : Types.value_type; align : int option} +type extendop = {memop : memop; sz : Memory.mem_size; ext : Memory.extension} +type truncop = {memop : memop; sz : Memory.mem_size} (* Expressions *) @@ -87,8 +87,10 @@ and expr' = | Return of expr option | GetLocal of var | SetLocal of var * expr - | Load of loadop * expr - | Store of storeop * expr * expr + | Load of memop * expr + | Store of memop * expr * expr + | LoadExtend of extendop * expr + | StoreTrunc of truncop * expr * expr | Const of literal | Unary of unop * expr | Binary of binop * expr * expr diff --git a/ml-proto/src/spec/check.ml b/ml-proto/src/spec/check.ml index e61cc58329..1ca52be718 100644 --- a/ml-proto/src/spec/check.ml +++ b/ml-proto/src/spec/check.ml @@ -53,14 +53,6 @@ let check_func_type actual expected at = (* Type Synthesis *) -let type_mem = function - | Memory.Int8Mem -> Int32Type - | Memory.Int16Mem -> Int32Type - | Memory.Int32Mem -> Int32Type - | Memory.Int64Mem -> Int64Type - | Memory.Float32Mem -> Float32Type - | Memory.Float64Mem -> Float64Type - let type_value = Values.type_of let type_unop = Values.type_of let type_binop = Values.type_of @@ -182,16 +174,19 @@ let rec check_expr c et e = check_expr c (Some (local c x)) e1; check_type None et e.at - | Load (loadop, e1) -> - check_align loadop.align e.at; - check_expr c (Some Int32Type) e1; - check_type (Some (type_mem loadop.mem)) et e.at + | Load (memop, e1) -> + check_load c et memop e1 e.at - | Store (storeop, e1, e2) -> - check_align storeop.align e.at; - check_expr c (Some Int32Type) e1; - check_expr c (Some (type_mem storeop.mem)) e2; - check_type None et e.at + | Store (memop, e1, e2) -> + check_store c et memop e1 e2 e.at + + | LoadExtend (extendop, e1) -> + check_mem_type extendop.memop.ty extendop.sz e.at; + check_load c et extendop.memop e1 e.at + + | StoreTrunc (truncop, e1, e2) -> + check_mem_type truncop.memop.ty truncop.sz e.at; + check_store c et truncop.memop e1 e2 e.at | Const v -> check_literal c et v @@ -246,8 +241,23 @@ and check_arm c t et arm = check_literal c (Some t) l; check_expr c (if fallthru then None else et) e +and check_load c et memop e1 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_align memop.align at; + check_expr c (Some Int32Type) e1; + check_expr c (Some memop.ty) e2; + check_type None et at + and check_align align at = - require (Lib.Int.is_power_of_two align) at "non-power-of-two alignment" + Lib.Option.app (fun a -> + require (Lib.Int.is_power_of_two a) at "non-power-of-two alignment") align + +and check_mem_type ty sz at = + require (ty = Int64Type || sz <> Memory.Mem32) at "memory size too big" (* diff --git a/ml-proto/src/spec/eval.ml b/ml-proto/src/spec/eval.ml index b125f6b435..16eab27afa 100644 --- a/ml-proto/src/spec/eval.ml +++ b/ml-proto/src/spec/eval.ml @@ -168,15 +168,31 @@ let rec eval_expr (c : config) (e : expr) = local c x := v1; None - | Load ({mem; ext; align = _}, e1) -> + | Load ({ty; align = _}, e1) -> let v1 = some (eval_expr c e1) e1.at in - (try Some (Memory.load c.modul.memory (Memory.address_of_value v1) mem ext) + let a = Memory.address_of_value v1 in + (try Some (Memory.load c.modul.memory a ty) with exn -> memory_error e.at exn) - | Store ({mem; align = _}, e1, e2) -> + | Store ({ty = _; align = _}, e1, e2) -> let v1 = some (eval_expr c e1) e1.at in let v2 = some (eval_expr c e2) e2.at in - (try Memory.store c.modul.memory (Memory.address_of_value v1) mem v2 + let a = Memory.address_of_value v1 in + (try Memory.store c.modul.memory a v2 + with exn -> memory_error e.at exn); + None + + | LoadExtend ({memop = {ty; align = _}; sz; ext}, e1) -> + let v1 = some (eval_expr c e1) e1.at in + let a = Memory.address_of_value v1 in + (try Some (Memory.load_extend c.modul.memory a sz ext ty) + with exn -> memory_error e.at exn) + + | StoreTrunc ({memop = {ty; align = _}; sz}, e1, e2) -> + 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_trunc c.modul.memory a sz v2 with exn -> memory_error e.at exn); None diff --git a/ml-proto/src/spec/memory.ml b/ml-proto/src/spec/memory.ml index 93afc3dc44..8b317c258d 100644 --- a/ml-proto/src/spec/memory.ml +++ b/ml-proto/src/spec/memory.ml @@ -3,35 +3,24 @@ *) open Bigarray +open Types +open Values (* Types and view types *) type address = int type size = address -type mem_size = int -type extension = SX | ZX | NX -type mem_type = - Int8Mem | Int16Mem | Int32Mem | Int64Mem | Float32Mem | Float64Mem - -type segment = -{ - addr : address; - data : string -} +type mem_size = Mem8 | Mem16 | Mem32 +type extension = SX | ZX +type segment = {addr : address; data : string} +type value_type = Types.value_type +type value = Values.value type memory' = (int, int8_unsigned_elt, c_layout) Array1.t type memory = memory' ref type t = memory -(* Queries *) - -let mem_size = function - | Int8Mem -> 1 - | Int16Mem -> 2 - | Int32Mem | Float32Mem -> 4 - | Int64Mem | Float64Mem -> 8 - (* Creation and initialization *) @@ -77,57 +66,60 @@ let address_of_value = function (* Load and store *) -let load8 mem a ext = - (match ext with - | SX -> Int32.shift_right (Int32.shift_left (Int32.of_int !mem.{a}) 24) 24 - | _ -> Int32.of_int !mem.{a}) - -let load16 mem a ext = - Int32.logor (load8 mem a NX) (Int32.shift_left (load8 mem (a+1) ext) 8) - -let load32 mem a = - Int32.logor (load16 mem a NX) (Int32.shift_left (load16 mem (a+2) NX) 16) - -let load64 mem a = - Int64.logor (Int64.of_int32 (load32 mem a)) (Int64.shift_left (Int64.of_int32 (load32 mem (a+4))) 32) - -let store8 mem a bits = - (* Store the lowest 8 bits of "bits" at byte index a, discarding the rest. *) - !mem.{a} <- Int32.to_int bits - -let store16 mem a bits = - store8 mem (a+0) bits; - store8 mem (a+1) (Int32.shift_right_logical bits 8) - -let store32 mem a bits = - store16 mem (a+0) bits; - store16 mem (a+2) (Int32.shift_right_logical bits 16) - -let store64 mem a bits = - store32 mem (a+0) (Int64.to_int32 bits); - store32 mem (a+4) (Int64.to_int32 (Int64.shift_right_logical bits 32)) - -let load mem a memty ext = - let open Types in - try - match memty, ext with - | Int8Mem, _ -> Int32 (I32.of_int32 (load8 mem a ext)) - | Int16Mem, _ -> Int32 (I32.of_int32 (load16 mem a ext)) - | Int32Mem, NX -> Int32 (I32.of_int32 (load32 mem a)) - | Int64Mem, NX -> Int64 (I64.of_int64 (load64 mem a)) - | Float32Mem, NX -> Float32 (F32.of_bits (load32 mem a)) - | Float64Mem, NX -> Float64 (F64.of_bits (load64 mem a)) - | _ -> raise Type - with Invalid_argument _ -> raise Bounds - -let store mem a memty v = - try - (match memty, v with - | Int8Mem, Int32 x -> store8 mem a (I32.to_int32 x) - | Int16Mem, Int32 x -> store16 mem a (I32.to_int32 x) - | Int32Mem, Int32 x -> store32 mem a (I32.to_int32 x) - | Int64Mem, Int64 x -> store64 mem a (I64.to_int64 x) - | Float32Mem, Float32 x -> store32 mem a (F32.to_bits x) - | Float64Mem, Float64 x -> store64 mem a (F64.to_bits x) - | _ -> raise Type) - with Invalid_argument _ -> raise Bounds +let rec loadn mem n a = + assert (n > 0 && n <= 8); + let byte = try Int64.of_int !mem.{a} with Invalid_argument _ -> raise Bounds in + if n = 1 then + byte + else + Int64.logor byte (Int64.shift_left (loadn mem (n-1) (a+1)) 8) + +let rec storen mem n a v = + assert (n > 0 && n <= 8); + let byte = (Int64.to_int v) land 255 in + (try !mem.{a} <- byte with Invalid_argument _ -> raise Bounds); + if (n > 1) then + storen mem (n-1) (a+1) (Int64.shift_right v 8) + +let load mem a t = + match t with + | Int32Type -> Int32 (Int64.to_int32 (loadn mem 4 a)) + | Int64Type -> Int64 (loadn mem 8 a) + | Float32Type -> Float32 (F32.of_bits (Int64.to_int32 (loadn mem 4 a))) + | Float64Type -> Float64 (F64.of_bits (loadn mem 8 a)) + +let store mem a v = + match v with + | Int32 x -> storen mem 4 a (Int64.of_int32 x) + | Int64 x -> storen mem 8 a x + | Float32 x -> storen mem 4 a (Int64.of_int32 (F32.to_bits x)) + | Float64 x -> storen mem 8 a (F64.to_bits x) + +let loadn_sx mem n a = + assert (n > 0 && n <= 8); + let v = loadn mem n a in + let shift = 64 - (8 * n) in + Int64.shift_right (Int64.shift_left v shift) shift + +let load_extend mem a sz ext t = + match sz, ext, t with + | Mem8, ZX, Int32Type -> Int32 (Int64.to_int32 (loadn mem 1 a)) + | Mem8, SX, Int32Type -> Int32 (Int64.to_int32 (loadn_sx mem 1 a)) + | Mem8, ZX, Int64Type -> Int64 (loadn mem 1 a) + | Mem8, SX, Int64Type -> Int64 (loadn_sx mem 1 a) + | Mem16, ZX, Int32Type -> Int32 (Int64.to_int32 (loadn mem 2 a)) + | Mem16, SX, Int32Type -> Int32 (Int64.to_int32 (loadn_sx mem 2 a)) + | Mem16, ZX, Int64Type -> Int64 (loadn mem 2 a) + | Mem16, SX, Int64Type -> Int64 (loadn_sx mem 2 a) + | Mem32, ZX, Int64Type -> Int64 (loadn mem 4 a) + | Mem32, SX, Int64Type -> Int64 (loadn_sx mem 4 a) + | _ -> raise Type + +let store_trunc mem a sz v = + match sz, v with + | Mem8, Int32 x -> storen mem 1 a (Int64.of_int32 x) + | Mem8, Int64 x -> storen mem 1 a x + | Mem16, Int32 x -> storen mem 2 a (Int64.of_int32 x) + | Mem16, Int64 x -> storen mem 2 a x + | Mem32, Int64 x -> storen mem 4 a x + | _ -> raise Type diff --git a/ml-proto/src/spec/memory.mli b/ml-proto/src/spec/memory.mli index 08cba1bc18..eda9fdd897 100644 --- a/ml-proto/src/spec/memory.mli +++ b/ml-proto/src/spec/memory.mli @@ -6,12 +6,11 @@ type memory type t = memory type address = int type size = address -type mem_size = int -type extension = SX | ZX | NX -type mem_type = - Int8Mem | Int16Mem | Int32Mem | Int64Mem | Float32Mem | Float64Mem - +type mem_size = Mem8 | Mem16 | Mem32 +type extension = SX | ZX type segment = {addr : address; data : string} +type value_type = Types.value_type +type value = Values.value exception Type exception Bounds @@ -21,8 +20,9 @@ val create : size -> memory val init : memory -> segment list -> unit val size : memory -> size val resize : memory -> size -> unit -val load : memory -> address -> mem_type -> extension -> Values.value -val store : memory -> address -> mem_type -> Values.value -> 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 store_trunc : memory -> address -> mem_size -> value -> unit -val mem_size : mem_type -> mem_size val address_of_value : Values.value -> address diff --git a/ml-proto/test/memory.wasm b/ml-proto/test/memory.wasm index 873d052ec0..d2a35f9744 100644 --- a/ml-proto/test/memory.wasm +++ b/ml-proto/test/memory.wasm @@ -140,31 +140,61 @@ ) ;; Sign and zero extending memory loads - (func $load8_s (param $i i32) (result i32) + (func $i32_load8_s (param $i i32) (result i32) (i32.store8 (i32.const 8) (get_local $i)) (return (i32.load8_s (i32.const 8))) ) - (func $load8_u (param $i i32) (result i32) + (func $i32_load8_u (param $i i32) (result i32) (i32.store8 (i32.const 8) (get_local $i)) (return (i32.load8_u (i32.const 8))) ) - (func $load16_s (param $i i32) (result i32) + (func $i32_load16_s (param $i i32) (result i32) (i32.store16 (i32.const 8) (get_local $i)) (return (i32.load16_s (i32.const 8))) ) - (func $load16_u (param $i i32) (result i32) + (func $i32_load16_u (param $i i32) (result i32) (i32.store16 (i32.const 8) (get_local $i)) (return (i32.load16_u (i32.const 8))) ) + (func $i64_load8_s (param $i i64) (result i64) + (i64.store8 (i32.const 8) (get_local $i)) + (return (i64.load8_s (i32.const 8))) + ) + (func $i64_load8_u (param $i i64) (result i64) + (i64.store8 (i32.const 8) (get_local $i)) + (return (i64.load8_u (i32.const 8))) + ) + (func $i64_load16_s (param $i i64) (result i64) + (i64.store16 (i32.const 8) (get_local $i)) + (return (i64.load16_s (i32.const 8))) + ) + (func $i64_load16_u (param $i i64) (result i64) + (i64.store16 (i32.const 8) (get_local $i)) + (return (i64.load16_u (i32.const 8))) + ) + (func $i64_load32_s (param $i i64) (result i64) + (i64.store32 (i32.const 8) (get_local $i)) + (return (i64.load32_s (i32.const 8))) + ) + (func $i64_load32_u (param $i i64) (result i64) + (i64.store32 (i32.const 8) (get_local $i)) + (return (i64.load32_u (i32.const 8))) + ) (export "data" $data) (export "aligned" $aligned) (export "unaligned" $unaligned) (export "cast" $cast) - (export "load8_s" $load8_s) - (export "load8_u" $load8_u) - (export "load16_s" $load16_s) - (export "load16_u" $load16_u) + (export "i32_load8_s" $i32_load8_s) + (export "i32_load8_u" $i32_load8_u) + (export "i32_load16_s" $i32_load16_s) + (export "i32_load16_u" $i32_load16_u) + (export "i64_load8_s" $i64_load8_s) + (export "i64_load8_u" $i64_load8_u) + (export "i64_load16_s" $i64_load16_s) + (export "i64_load16_u" $i64_load16_u) + (export "i64_load32_s" $i64_load32_s) + (export "i64_load32_u" $i64_load32_u) ) (assert_eq (invoke "data") (i32.const 1)) @@ -172,12 +202,26 @@ (assert_eq (invoke "unaligned") (i32.const 1)) (assert_eq (invoke "cast") (f64.const 42.0)) -(assert_eq (invoke "load8_s" (i32.const -1)) (i32.const -1)) -(assert_eq (invoke "load8_u" (i32.const -1)) (i32.const 255)) -(assert_eq (invoke "load16_s" (i32.const -1)) (i32.const -1)) -(assert_eq (invoke "load16_u" (i32.const -1)) (i32.const 65535)) +(assert_eq (invoke "i32_load8_s" (i32.const -1)) (i32.const -1)) +(assert_eq (invoke "i32_load8_u" (i32.const -1)) (i32.const 255)) +(assert_eq (invoke "i32_load16_s" (i32.const -1)) (i32.const -1)) +(assert_eq (invoke "i32_load16_u" (i32.const -1)) (i32.const 65535)) + +(assert_eq (invoke "i32_load8_s" (i32.const 100)) (i32.const 100)) +(assert_eq (invoke "i32_load8_u" (i32.const 200)) (i32.const 200)) +(assert_eq (invoke "i32_load16_s" (i32.const 20000)) (i32.const 20000)) +(assert_eq (invoke "i32_load16_u" (i32.const 40000)) (i32.const 40000)) + +(assert_eq (invoke "i64_load8_s" (i64.const -1)) (i64.const -1)) +(assert_eq (invoke "i64_load8_u" (i64.const -1)) (i64.const 255)) +(assert_eq (invoke "i64_load16_s" (i64.const -1)) (i64.const -1)) +(assert_eq (invoke "i64_load16_u" (i64.const -1)) (i64.const 65535)) +(assert_eq (invoke "i64_load32_s" (i64.const -1)) (i64.const -1)) +(assert_eq (invoke "i64_load32_u" (i64.const -1)) (i64.const 4294967295)) -(assert_eq (invoke "load8_s" (i32.const 100)) (i32.const 100)) -(assert_eq (invoke "load8_u" (i32.const 200)) (i32.const 200)) -(assert_eq (invoke "load16_s" (i32.const 20000)) (i32.const 20000)) -(assert_eq (invoke "load16_u" (i32.const 40000)) (i32.const 40000)) \ No newline at end of file +(assert_eq (invoke "i64_load8_s" (i64.const 100)) (i64.const 100)) +(assert_eq (invoke "i64_load8_u" (i64.const 200)) (i64.const 200)) +(assert_eq (invoke "i64_load16_s" (i64.const 20000)) (i64.const 20000)) +(assert_eq (invoke "i64_load16_u" (i64.const 40000)) (i64.const 40000)) +(assert_eq (invoke "i64_load32_s" (i64.const 20000)) (i64.const 20000)) +(assert_eq (invoke "i64_load32_u" (i64.const 40000)) (i64.const 40000))