From b648a9940121280d5ad0b8cb3f3a4bb5764f4552 Mon Sep 17 00:00:00 2001 From: Luke Wagner Date: Tue, 29 Sep 2015 10:51:26 -0500 Subject: [PATCH] Add constant offsets to spec --- ml-proto/README.md | 14 ++-- ml-proto/src/host/lexer.mll | 49 ++++++++---- ml-proto/src/spec/ast.ml | 2 +- ml-proto/src/spec/check.ml | 12 +-- ml-proto/src/spec/eval.ml | 16 ++-- ml-proto/src/spec/memory.ml | 79 +++++++++++-------- ml-proto/src/spec/memory.mli | 9 ++- ml-proto/test/address.wasm | 17 ++++ .../test/expected-output/address.wasm.log | 3 + 9 files changed, 123 insertions(+), 78 deletions(-) create mode 100644 ml-proto/test/address.wasm create mode 100644 ml-proto/test/expected-output/address.wasm.log diff --git a/ml-proto/README.md b/ml-proto/README.md index 5627b75618..c60c98c8b9 100644 --- a/ml-proto/README.md +++ b/ml-proto/README.md @@ -126,10 +126,10 @@ type expr = | GetParam of var (* read parameter | GetLocal of var (* read local variable | SetLocal of var * expr (* write local variable - | LoadGlobal of var (* read global variable - | StoreGlobal of var * expr (* write global variable - | Load of loadop * expr (* read memory address - | Store of storeop * expr * expr (* write memory address + | Load of memop * expr (* read memory address + | Store of memop * expr * expr (* write memory address + | LoadExtend of extendop * expr (* read memory address with sign- or zero-extension + | StoreTrunc of truncop * expr * expr (* write memory address with truncation | Const of value (* constant | Unary of unop * expr (* unary arithmetic operator | Binary of binop * expr * expr (* binary arithmetic operator @@ -178,10 +178,8 @@ expr: ( return ? ) ( get_local ) ( set_local ) - ( load_global ) - ( store_global ) - ( .load((8|16)_)?(/)? ) - ( .store(/)? ) + ( .load((8|16)_)?(+)?(/)? ) + ( .store(+)?(/)? ) ( .const ) ( . ) ( . ) diff --git a/ml-proto/src/host/lexer.mll b/ml-proto/src/host/lexer.mll index 7686927a2d..f136f69228 100644 --- a/ml-proto/src/host/lexer.mll +++ b/ml-proto/src/host/lexer.mll @@ -60,8 +60,11 @@ 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 o a = + let ty = value_type t in + let offset = if o = "" then 0 else int_of_string o in + let align = if a = "" then None else Some (int_of_string a) in + {ty; offset; align} let mem_size = function | "8" -> Memory.Mem8 @@ -74,11 +77,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 extendop t sz s o a = + {memop = memop t o a; sz = mem_size sz; ext = extension s} -let truncop t sz a = - {memop = memop t a; sz = mem_size sz} +let truncop t sz o a = + {memop = memop t o a; sz = mem_size sz} } let space = [' ''\t'] @@ -103,7 +106,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 @@ -137,19 +140,31 @@ rule token = parse | "get_local" { GETLOCAL } | "set_local" { SETLOCAL } - | (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)".load+"(digits as o) { LOAD (memop t o "") } + | (nxx as t)".load/"(digits as a) { LOAD (memop t "" a) } + | (nxx as t)".load+"(digits as o)"/"(digits as a) { LOAD (memop t o a) } + | (nxx as t)".store" { STORE (memop t "" "") } + | (nxx as t)".store+"(digits as o) { STORE (memop t o "") } + | (nxx as t)".store/"(digits as a) { STORE (memop t "" a) } + | (nxx as t)".store+"(digits as o)"/"(digits as a) { STORE (memop t o 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) } + { LOADEXTEND (extendop t sz s "" "") } + | (ixx as t)".load"(mem_size as sz)"_"(sign as s)"+"(digits as o) + { LOADEXTEND (extendop t sz s o "") } + | (ixx as t)".load"(mem_size as sz)"_"(sign as s)"/"(digits as a) + { LOADEXTEND (extendop t sz s "" a) } + | (ixx as t)".load"(mem_size as sz)"_"(sign as s)"+"(digits as o)"/"(digits as a) + { LOADEXTEND (extendop t sz s o 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) } + { STORETRUNC (truncop t sz "" "") } + | (ixx as t)".store"(mem_size as sz)"+"(digits as o) + { STORETRUNC (truncop t sz o "") } + | (ixx as t)".store"(mem_size as sz)"/"(digits as a) + { STORETRUNC (truncop t sz "" a) } + | (ixx as t)".store"(mem_size as sz)"+"(digits as o)"/"(digits as a) + { STORETRUNC (truncop t sz o a) } | (nxx as t)".switch" { SWITCH (value_type t) } | (nxx as t)".const" { CONST (value_type t) } diff --git a/ml-proto/src/spec/ast.ml b/ml-proto/src/spec/ast.ml index 1605f68b9b..6e10d6416f 100644 --- a/ml-proto/src/spec/ast.ml +++ b/ml-proto/src/spec/ast.ml @@ -63,7 +63,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 : Types.value_type; align : int option} +type memop = {ty : Types.value_type; offset : Memory.offset; align : int option} type extendop = {memop : memop; sz : Memory.mem_size; ext : Memory.extension} type truncop = {memop : memop; sz : Memory.mem_size} diff --git a/ml-proto/src/spec/check.ml b/ml-proto/src/spec/check.ml index 1ca52be718..95839850aa 100644 --- a/ml-proto/src/spec/check.ml +++ b/ml-proto/src/spec/check.ml @@ -242,19 +242,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_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_align memop.align at; + check_memop memop at; check_expr c (Some Int32Type) e1; check_expr c (Some memop.ty) e2; check_type None et at -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 >= 0) 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/src/spec/eval.ml b/ml-proto/src/spec/eval.ml index 16eab27afa..13dc216082 100644 --- a/ml-proto/src/spec/eval.ml +++ b/ml-proto/src/spec/eval.ml @@ -168,31 +168,31 @@ let rec eval_expr (c : config) (e : expr) = local c x := v1; None - | Load ({ty; align = _}, e1) -> + | Load ({ty; offset; align = _}, e1) -> let v1 = some (eval_expr c e1) e1.at in let a = Memory.address_of_value v1 in - (try Some (Memory.load c.modul.memory a ty) + (try Some (Memory.load c.modul.memory a offset ty) with exn -> memory_error e.at exn) - | Store ({ty = _; align = _}, e1, e2) -> + | Store ({ty = _; offset; align = _}, 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 c.modul.memory a v2 + (try Memory.store c.modul.memory a offset v2 with exn -> memory_error e.at exn); None - | LoadExtend ({memop = {ty; align = _}; sz; ext}, e1) -> + | LoadExtend ({memop = {ty; offset; 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) + (try Some (Memory.load_extend c.modul.memory a offset sz ext ty) with exn -> memory_error e.at exn) - | StoreTrunc ({memop = {ty; align = _}; sz}, e1, e2) -> + | StoreTrunc ({memop = {ty; offset; 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 + (try Memory.store_trunc c.modul.memory a offset 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 8b317c258d..cfbe07767c 100644 --- a/ml-proto/src/spec/memory.ml +++ b/ml-proto/src/spec/memory.ml @@ -11,6 +11,7 @@ open Values type address = int type size = address +type offset = address type mem_size = Mem8 | Mem16 | Mem32 type extension = SX | ZX type segment = {addr : address; data : string} @@ -66,60 +67,68 @@ let address_of_value = function (* Load and store *) -let rec loadn mem n a = +let effective_address a o = + if max_int - a < o then raise Bounds; + a + o + +let rec loadn mem n ea = assert (n > 0 && n <= 8); - let byte = try Int64.of_int !mem.{a} with Invalid_argument _ -> raise Bounds in + let byte = try Int64.of_int !mem.{ea} 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) + Int64.logor byte (Int64.shift_left (loadn mem (n-1) (ea+1)) 8) -let rec storen mem n a v = +let rec storen mem n ea v = assert (n > 0 && n <= 8); let byte = (Int64.to_int v) land 255 in - (try !mem.{a} <- byte with Invalid_argument _ -> raise Bounds); + (try !mem.{ea} <- byte with Invalid_argument _ -> raise Bounds); if (n > 1) then - storen mem (n-1) (a+1) (Int64.shift_right v 8) + storen mem (n-1) (ea+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 o a 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_trunc mem a sz v = +let store_trunc 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/src/spec/memory.mli b/ml-proto/src/spec/memory.mli index eda9fdd897..951fbf9ddb 100644 --- a/ml-proto/src/spec/memory.mli +++ b/ml-proto/src/spec/memory.mli @@ -6,6 +6,7 @@ type memory type t = memory type address = int type size = address +type offset = address type mem_size = Mem8 | Mem16 | Mem32 type extension = SX | ZX type segment = {addr : address; data : string} @@ -20,9 +21,9 @@ val create : size -> memory val init : memory -> segment list -> unit 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 store_trunc : memory -> address -> mem_size -> value -> unit +val load : memory -> address -> offset -> value_type -> value +val store : memory -> address -> offset -> value -> unit +val load_extend : memory -> address -> offset -> mem_size -> extension -> value_type -> value +val store_trunc : memory -> address -> offset -> mem_size -> value -> unit val address_of_value : Values.value -> address diff --git a/ml-proto/test/address.wasm b/ml-proto/test/address.wasm new file mode 100644 index 0000000000..cd45862516 --- /dev/null +++ b/ml-proto/test/address.wasm @@ -0,0 +1,17 @@ +(module + (import $print "stdio" "print" (param i32)) + (memory 1024 (segment 0 "ab")) + (func $good + (call_import $print (i32.load8_u+0 (i32.const 0))) + (call_import $print (i32.load8_u+1 (i32.const 0))) + (call_import $print (i32.load8_u (i32.add (i32.const -1) (i32.const 1)))) + ) + (func $bad + (i32.load8_u+1 (i32.const -1)) + ) + (export "good" $good) + (export "bad" $bad) +) + +(invoke "good") +(assert_trap (invoke "bad") "runtime: out of bounds memory access") diff --git a/ml-proto/test/expected-output/address.wasm.log b/ml-proto/test/expected-output/address.wasm.log new file mode 100644 index 0000000000..af64bb0c52 --- /dev/null +++ b/ml-proto/test/expected-output/address.wasm.log @@ -0,0 +1,3 @@ +97 : i32 +98 : i32 +97 : i32