diff --git a/ml-proto/README.md b/ml-proto/README.md index 1fe4da5137..eaab702110 100644 --- a/ml-proto/README.md +++ b/ml-proto/README.md @@ -124,7 +124,8 @@ unop: ctz | clz | popcnt | ... binop: add | sub | mul | ... relop: eq | ne | lt | ... sign: s|u -align: 1|2|4|8|... +offset: offset= +align: align=(1|2|4|8|...) cvtop: trunc_s | trunc_u | extend_s | extend_u | ... expr: @@ -145,8 +146,8 @@ expr: ( return ? ) ;; = (break ?) ( get_local ) ( set_local ) - ( .load((8|16)_)?(/)? ) - ( .store(/)? ) + ( .load((8|16)_)? ? ? ) + ( .store ? ? ) ( .const ) ( . ) ( . ) diff --git a/ml-proto/host/lexer.mll b/ml-proto/host/lexer.mll index 7b98399493..f13e5537c1 100644 --- a/ml-proto/host/lexer.mll +++ b/ml-proto/host/lexer.mll @@ -60,8 +60,8 @@ let floatop t f32 f64 = | "f64" -> Values.Float64 f64 | _ -> assert false -let memop t a = - {ty = value_type t; align = if a = "" then None else Some (int_of_string a)} +let memop t = + {ty = value_type t; offset = 0L; align = None} let mem_size = function | "8" -> Memory.Mem8 @@ -74,11 +74,11 @@ let extension = function | 'u' -> Memory.ZX | _ -> assert false -let extendop t sz s a = - {memop = memop t a; sz = mem_size sz; ext = extension s} +let extop t sz s = + {memop = memop t; sz = mem_size sz; ext = extension s} -let wrapop t sz a = - {memop = memop t a; sz = mem_size sz} +let wrapop t sz = + {memop = memop t; sz = mem_size sz} } let space = [' ''\t'] @@ -109,7 +109,7 @@ let nxx = ixx | fxx let mixx = "i" ("8" | "16" | "32" | "64") let mfxx = "f" ("32" | "64") let sign = "s" | "u" -let align = digit+ +let digits = digit+ let mem_size = "8" | "16" | "32" rule token = parse @@ -143,19 +143,16 @@ rule token = parse | "get_local" { GET_LOCAL } | "set_local" { SET_LOCAL } - | (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) } + | (nxx as t)".load" { LOAD (memop t) } + | (nxx as t)".store" { STORE (memop t) } | (ixx as t)".load"(mem_size as sz)"_"(sign as s) - { LOAD_EXTEND (extendop t sz s "") } - | (ixx as t)".load"(mem_size as sz)"_"(sign as s)"/"(align as a) - { LOAD_EXTEND (extendop t sz s a) } + { LOAD_EXTEND (extop t sz s) } | (ixx as t)".store"(mem_size as sz) - { STORE_WRAP (wrapop t sz "") } - | (ixx as t)".store"(mem_size as sz)"/"(align as a) - { STORE_WRAP (wrapop t sz a) } + { STORE_WRAP (wrapop t sz) } + + | "offset="(digits as s) { OFFSET (Int64.of_string s) } + | "align="(digits as s) { ALIGN (int_of_string s) } | (nxx as t)".switch" { SWITCH (value_type t) } | (nxx as t)".const" { CONST (value_type t) } diff --git a/ml-proto/host/parser.mly b/ml-proto/host/parser.mly index 38b48ba0b3..a7286f678c 100644 --- a/ml-proto/host/parser.mly +++ b/ml-proto/host/parser.mly @@ -45,6 +45,24 @@ let literal s t = | _ -> Error.error s.at "constant out of range" +(* Memory operands *) + +let memop m offset align = + assert (m.offset = 0L); + assert (m.align = None); + {m with offset; align} + +let extop (e : extop) offset align = + assert (e.memop.offset = 0L); + assert (e.memop.align = None); + {e with memop = {e.memop with offset; align}} + +let wrapop (w : wrapop) offset align = + assert (w.memop.offset = 0L); + assert (w.memop.align = None); + {w with memop = {w.memop with offset; align}} + + (* Symbolic variables *) module VarMap = Map.Make(String) @@ -126,13 +144,12 @@ let implicit_decl c t at = | None -> let i = List.length c.types.tlist in anon_type c t; i @@ at | Some i -> i @@ at - %} %token INT FLOAT TEXT VAR VALUE_TYPE LPAR RPAR %token NOP BLOCK IF LOOP LABEL BREAK SWITCH CASE FALLTHROUGH %token CALL CALL_IMPORT CALL_INDIRECT RETURN -%token GET_LOCAL SET_LOCAL LOAD STORE +%token GET_LOCAL SET_LOCAL LOAD STORE LOAD_EXTEND STORE_WRAP OFFSET ALIGN %token CONST UNARY BINARY COMPARE CONVERT %token FUNC TYPE PARAM RESULT LOCAL %token MODULE MEMORY SEGMENT IMPORT EXPORT TABLE @@ -155,6 +172,8 @@ let implicit_decl c t at = %token STORE %token LOAD_EXTEND %token STORE_WRAP +%token OFFSET +%token ALIGN %nonassoc LOW %nonassoc VAR @@ -206,6 +225,15 @@ labeling : | bind_var { let at = at () in fun c -> bind_label c $1, Labelled @@ at } ; +offset : + | /* empty */ { 0L } + | OFFSET { $1 } +; +align : + | /* empty */ { None } + | ALIGN { Some $1 } +; + expr : | LPAR expr1 RPAR { let at = at () in fun c -> $2 c @@ at } ; @@ -234,10 +262,14 @@ expr1 : { fun c -> call_indirect ($2 c table, $3 c, $4 c) } | GET_LOCAL var { fun c -> get_local ($2 c local) } | SET_LOCAL var expr { fun c -> set_local ($2 c local, $3 c) } - | LOAD expr { fun c -> load ($1, $2 c) } - | STORE expr expr { fun c -> store ($1, $2 c, $3 c) } - | LOAD_EXTEND expr { fun c -> load_extend ($1, $2 c) } - | STORE_WRAP expr expr { fun c -> store_wrap ($1, $2 c, $3 c) } + | LOAD offset align expr + { fun c -> load (memop $1 $2 $3, $4 c) } + | STORE offset align expr expr + { fun c -> store (memop $1 $2 $3, $4 c, $5 c) } + | LOAD_EXTEND offset align expr + { fun c -> load_extend (extop $1 $2 $3, $4 c) } + | STORE_WRAP offset align expr expr + { fun c -> store_wrap (wrapop $1 $2 $3, $4 c, $5 c) } | CONST literal { fun c -> const (literal $2 $1) } | UNARY expr { fun c -> unary ($1, $2 c) } | BINARY expr expr { fun c -> binary ($1, $2 c, $3 c) } diff --git a/ml-proto/spec/ast.ml b/ml-proto/spec/ast.ml index a52fd5056f..a122ce82c1 100644 --- a/ml-proto/spec/ast.ml +++ b/ml-proto/spec/ast.ml @@ -62,7 +62,7 @@ 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 memop = {ty : value_type; align : int option} +type memop = {ty : value_type; offset : Memory.offset; align : int option} type extop = {memop : memop; sz : Memory.mem_size; ext : Memory.extension} type wrapop = {memop : memop; sz : Memory.mem_size} type hostop = diff --git a/ml-proto/spec/check.ml b/ml-proto/spec/check.ml index 0ce2e17fd0..1853a8b7d9 100644 --- a/ml-proto/spec/check.ml +++ b/ml-proto/spec/check.ml @@ -232,13 +232,13 @@ and check_case c t et case = and check_load c et memop e1 at = check_has_memory c at; - check_align memop.align at; + check_memop memop 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_memop memop at; check_expr c (Some Int32Type) e1; check_expr c (Some memop.ty) e2; check_type (Some memop.ty) et at @@ -246,9 +246,11 @@ and check_store c et memop e1 e2 at = and check_has_memory c at = require c.has_memory at "memory operators 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 +and check_memop memop at = + require (memop.offset >= 0L) at "negative offset"; + Lib.Option.app + (fun a -> require (Lib.Int.is_power_of_two a) at "non-power-of-two alignment") + memop.align and check_mem_type ty sz at = require (ty = Int64Type || sz <> Memory.Mem32) at "memory size too big" diff --git a/ml-proto/spec/eval.ml b/ml-proto/spec/eval.ml index 32d16ba0a9..6d4720f4e0 100644 --- a/ml-proto/spec/eval.ml +++ b/ml-proto/spec/eval.ml @@ -185,29 +185,32 @@ let rec eval_expr (c : config) (e : expr) = local c x := v1; Some v1 - | Load ({ty; align = _}, e1) -> + | Load ({ty; offset; align = _}, e1) -> let mem = some_memory c e.at in let v1 = mem_size (eval_expr c e1) e1.at in - (try Some (Memory.load mem v1 ty) with exn -> memory_error e.at exn) + (try Some (Memory.load mem v1 offset ty) + with exn -> memory_error e.at exn) - | Store ({ty = _; align = _}, e1, e2) -> + | Store ({ty = _; offset; align = _}, e1, e2) -> let mem = some_memory c e.at in let v1 = mem_size (eval_expr c e1) e1.at in let v2 = some (eval_expr c e2) e2.at in - (try Memory.store mem v1 v2 with exn -> memory_error e.at exn); + (try Memory.store mem v1 offset v2 + with exn -> memory_error e.at exn); Some v2 - | LoadExtend ({memop = {ty; align = _}; sz; ext}, e1) -> + | LoadExtend ({memop = {ty; offset; 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) + (try Some (Memory.load_extend mem v1 offset sz ext ty) with exn -> memory_error e.at exn) - | StoreWrap ({memop = {ty; align = _}; sz}, e1, e2) -> + | StoreWrap ({memop = {ty; offset; align = _}; sz}, e1, e2) -> let mem = some_memory c e.at in let v1 = mem_size (eval_expr c e1) e1.at in let v2 = some (eval_expr c e2) e2.at in - (try Memory.store_wrap mem v1 sz v2 with exn -> memory_error e.at exn); + (try Memory.store_wrap mem v1 offset sz v2 + with exn -> memory_error e.at exn); Some v2 | Const v -> diff --git a/ml-proto/spec/memory.ml b/ml-proto/spec/memory.ml index 1a508aec03..9f70257c0c 100644 --- a/ml-proto/spec/memory.ml +++ b/ml-proto/spec/memory.ml @@ -8,6 +8,7 @@ open Values type address = int64 type size = address +type offset = address type mem_size = Mem8 | Mem16 | Mem32 type extension = SX | ZX type segment = {addr : address; data : string} @@ -79,9 +80,14 @@ let grow mem n = Array1.blit (Array1.sub !mem 0 host_old_size) (Array1.sub after 0 host_old_size); mem := after -let rec loadn mem n a = +let effective_address a o = + let ea = Int64.add a o in + if I64.lt_u ea a then raise Bounds; + ea + +let rec loadn mem n ea = assert (n > 0 && n <= 8); - let i = host_index_of_int64 a n in + let i = host_index_of_int64 ea n in try loadn' mem n i with Invalid_argument _ -> raise Bounds and loadn' mem n i = @@ -91,9 +97,9 @@ and loadn' mem n i = else Int64.logor byte (Int64.shift_left (loadn' mem (n-1) (i+1)) 8) -let rec storen mem n a v = +let rec storen mem n ea v = assert (n > 0 && n <= 8); - let i = host_index_of_int64 a n in + let i = host_index_of_int64 ea n in try storen' mem n i v with Invalid_argument _ -> raise Bounds and storen' mem n i v = @@ -101,45 +107,49 @@ and storen' mem n i v = if (n > 1) then storen' mem (n-1) (i+1) (Int64.shift_right v 8) -let load mem a t = +let load mem a o t = + let ea = effective_address a o in 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)) + | Int32Type -> Int32 (Int64.to_int32 (loadn mem 4 ea)) + | Int64Type -> Int64 (loadn mem 8 ea) + | Float32Type -> Float32 (F32.of_bits (Int64.to_int32 (loadn mem 4 ea))) + | Float64Type -> Float64 (F64.of_bits (loadn mem 8 ea)) -let store mem a v = +let store mem a o v = + let ea = effective_address a o in 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) + | Int32 x -> storen mem 4 ea (Int64.of_int32 x) + | Int64 x -> storen mem 8 ea x + | Float32 x -> storen mem 4 ea (Int64.of_int32 (F32.to_bits x)) + | Float64 x -> storen mem 8 ea (F64.to_bits x) -let loadn_sx mem n a = +let loadn_sx mem n ea = assert (n > 0 && n <= 8); - let v = loadn mem n a in + let v = loadn mem n ea in let shift = 64 - (8 * n) in Int64.shift_right (Int64.shift_left v shift) shift -let load_extend mem a sz ext t = +let load_extend mem a o sz ext t = + let ea = effective_address a o in 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) + | Mem8, ZX, Int32Type -> Int32 (Int64.to_int32 (loadn mem 1 ea)) + | Mem8, SX, Int32Type -> Int32 (Int64.to_int32 (loadn_sx mem 1 ea)) + | Mem8, ZX, Int64Type -> Int64 (loadn mem 1 ea) + | Mem8, SX, Int64Type -> Int64 (loadn_sx mem 1 ea) + | Mem16, ZX, Int32Type -> Int32 (Int64.to_int32 (loadn mem 2 ea)) + | Mem16, SX, Int32Type -> Int32 (Int64.to_int32 (loadn_sx mem 2 ea)) + | Mem16, ZX, Int64Type -> Int64 (loadn mem 2 ea) + | Mem16, SX, Int64Type -> Int64 (loadn_sx mem 2 ea) + | Mem32, ZX, Int64Type -> Int64 (loadn mem 4 ea) + | Mem32, SX, Int64Type -> Int64 (loadn_sx mem 4 ea) | _ -> raise Type -let store_wrap mem a sz v = +let store_wrap mem a o sz v = + let ea = effective_address a o in 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 + | Mem8, Int32 x -> storen mem 1 ea (Int64.of_int32 x) + | Mem8, Int64 x -> storen mem 1 ea x + | Mem16, Int32 x -> storen mem 2 ea (Int64.of_int32 x) + | Mem16, Int64 x -> storen mem 2 ea x + | Mem32, Int64 x -> storen mem 4 ea x | _ -> raise Type diff --git a/ml-proto/spec/memory.mli b/ml-proto/spec/memory.mli index 25e804eec2..3f3a1cc7d5 100644 --- a/ml-proto/spec/memory.mli +++ b/ml-proto/spec/memory.mli @@ -6,6 +6,7 @@ type memory type t = memory type address = int64 type size = address +type offset = address type mem_size = Mem8 | Mem16 | Mem32 type extension = SX | ZX type segment = {addr : address; data : string} @@ -20,8 +21,8 @@ val create : size -> memory val init : memory -> segment list -> unit val size : memory -> size val grow : memory -> size -> unit -val load : memory -> address -> value_type -> value -val store : memory -> address -> value -> unit +val load : memory -> address -> offset -> value_type -> value +val store : memory -> address -> offset -> value -> unit val load_extend : - memory -> address -> mem_size -> extension -> value_type -> value -val store_wrap : memory -> address -> mem_size -> value -> unit + memory -> address -> offset -> mem_size -> extension -> value_type -> value +val store_wrap : memory -> address -> offset -> mem_size -> value -> unit diff --git a/ml-proto/test/address.wast b/ml-proto/test/address.wast new file mode 100644 index 0000000000..9a16ffd70e --- /dev/null +++ b/ml-proto/test/address.wast @@ -0,0 +1,35 @@ +(module + (memory 1024 (segment 0 "abcdefghijklmnopqrstuvwxyz")) + (import $print "stdio" "print" (param i32)) + + (func $good (param $i i32) + (call_import $print (i32.load8_u offset=0 (get_local $i))) ;; 97 'a' + (call_import $print (i32.load8_u offset=1 (get_local $i))) ;; 98 'b' + (call_import $print (i32.load8_u offset=2 (get_local $i))) ;; 99 'c' + (call_import $print (i32.load8_u offset=25 (get_local $i))) ;; 122 'z' + + (call_import $print (i32.load16_u offset=0 (get_local $i))) ;; 25185 'ab' + (call_import $print (i32.load16_u offset=1 align=1 (get_local $i))) ;; 25442 'bc' + (call_import $print (i32.load16_u offset=2 (get_local $i))) ;; 25699 'cd' + (call_import $print (i32.load16_u offset=25 align=1 (get_local $i))) ;; 122 'z\0' + + (call_import $print (i32.load offset=0 (get_local $i))) ;; 1684234849 'abcd' + (call_import $print (i32.load offset=1 align=1 (get_local $i))) ;; 1701077858 'bcde' + (call_import $print (i32.load offset=2 align=2 (get_local $i))) ;; 1717920867 'cdef' + (call_import $print (i32.load offset=25 align=1 (get_local $i))) ;; 122 'z\0\0\0' + ) + (export "good" $good) + + (func $bad1 (param $i i32) (i32.load offset=4294967296 (get_local $i))) + (export "bad1" $bad1) + (func $bad2 (param $i i32) (i32.load offset=4294967295 (get_local $i))) + (export "bad2" $bad2) +) + +(assert_return (invoke "good" (i32.const 0))) +(assert_return (invoke "good" (i32.const 995))) +(assert_trap (invoke "good" (i32.const 996)) "runtime: out of bounds memory access") +(assert_trap (invoke "bad1" (i32.const 0)) "runtime: out of bounds memory access") +(assert_trap (invoke "bad1" (i32.const 1)) "runtime: out of bounds memory access") +(assert_trap (invoke "bad2" (i32.const 0)) "runtime: out of bounds memory access") +(assert_trap (invoke "bad2" (i32.const 1)) "runtime: out of bounds memory access") diff --git a/ml-proto/test/memory.wast b/ml-proto/test/memory.wast index ee1c594943..b09cd1488e 100644 --- a/ml-proto/test/memory.wast +++ b/ml-proto/test/memory.wast @@ -35,29 +35,29 @@ ) ;; Test alignment annotation rules -(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)))) +(module (memory 0) (func (i32.load8_u align=2 (i32.const 0)))) +(module (memory 0) (func (i32.load16_u align=4 (i32.const 0)))) +(module (memory 0) (func (i32.load align=8 (i32.const 0)))) +(module (memory 0) (func (f32.load align=8 (i32.const 0)))) (assert_invalid - (module (memory 0) (func (i64.load/0 (i32.const 0)))) + (module (memory 0) (func (i64.load align=0 (i32.const 0)))) "non-power-of-two alignment" ) (assert_invalid - (module (memory 0) (func (i64.load/3 (i32.const 0)))) + (module (memory 0) (func (i64.load align=3 (i32.const 0)))) "non-power-of-two alignment" ) (assert_invalid - (module (memory 0) (func (i64.load/5 (i32.const 0)))) + (module (memory 0) (func (i64.load align=5 (i32.const 0)))) "non-power-of-two alignment" ) (assert_invalid - (module (memory 0) (func (i64.load/6 (i32.const 0)))) + (module (memory 0) (func (i64.load align=6 (i32.const 0)))) "non-power-of-two alignment" ) (assert_invalid - (module (memory 0) (func (i64.load/7 (i32.const 0)))) + (module (memory 0) (func (i64.load align=7 (i32.const 0)))) "non-power-of-two alignment" ) @@ -124,8 +124,8 @@ (break 0) ) (set_local 2 (f64.convert_s/i32 (get_local 0))) - (f64.store/1 (get_local 0) (get_local 2)) - (set_local 1 (f64.load/1 (get_local 0))) + (f64.store align=1 (get_local 0) (get_local 2)) + (set_local 1 (f64.load align=1 (get_local 0))) (if (f64.ne (get_local 2) (get_local 1)) (return (i32.const 0)) @@ -146,9 +146,9 @@ ) (return (f64.const 0)) ) - (i64.store/1 (i32.const 9) (i64.const 0)) - (i32.store16/1 (i32.const 15) (i32.const 16453)) - (return (f64.load/1 (i32.const 9))) + (i64.store align=1 (i32.const 9) (i64.const 0)) + (i32.store16 align=1 (i32.const 15) (i32.const 16453)) + (return (f64.load align=1 (i32.const 9))) ) ;; Sign and zero extending memory loads