Skip to content

Commit b648a99

Browse files
lukewagnerlukewagner
committed
Add constant offsets to spec
1 parent ae419ca commit b648a99

File tree

9 files changed

+123
-78
lines changed

9 files changed

+123
-78
lines changed

‎ml-proto/README.md

Lines changed: 6 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -126,10 +126,10 @@ type expr =
126126
| GetParam of var (* read parameter
127127
| GetLocal of var (* read local variable
128128
| SetLocal of var * expr (* write local variable
129-
| LoadGlobal of var (* read global variable
130-
| StoreGlobal of var * expr (* write global variable
131-
| Load of loadop * expr (* read memory address
132-
| Store of storeop * expr * expr (* write memory address
129+
| Load of memop * expr (* read memory address
130+
| Store of memop * expr * expr (* write memory address
131+
| LoadExtend of extendop * expr (* read memory address with sign- or zero-extension
132+
| StoreTrunc of truncop * expr * expr (* write memory address with truncation
133133
| Const of value (* constant
134134
| Unary of unop * expr (* unary arithmetic operator
135135
| Binary of binop * expr * expr (* binary arithmetic operator
@@ -178,10 +178,8 @@ expr:
178178
( return <expr>? )
179179
( get_local <var> )
180180
( set_local <var> <expr> )
181-
( load_global <var> )
182-
( store_global <var> <expr> )
183-
( <type>.load((8|16)_<sign>)?(/<align>)? <expr> )
184-
( <type>.store(/<align>)? <expr> <expr> )
181+
( <type>.load((8|16)_<sign>)?(+<offset>)?(/<align>)? <expr> )
182+
( <type>.store(+<offset>)?(/<align>)? <expr> <expr> )
185183
( <type>.const <value> )
186184
( <type>.<unop> <expr> )
187185
( <type>.<binop> <expr> <expr> )

‎ml-proto/src/host/lexer.mll

Lines changed: 32 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -60,8 +60,11 @@ let floatop t f32 f64 =
6060
| "f64" -> Values.Float64 f64
6161
| _ -> assert false
6262

63-
let memop t a =
64-
{ty = value_type t; align = if a = "" then None else Some (int_of_string a)}
63+
let memop t o a =
64+
let ty = value_type t in
65+
let offset = if o = "" then 0 else int_of_string o in
66+
let align = if a = "" then None else Some (int_of_string a) in
67+
{ty; offset; align}
6568

6669
let mem_size = function
6770
| "8" -> Memory.Mem8
@@ -74,11 +77,11 @@ let extension = function
7477
| 'u' -> Memory.ZX
7578
| _ -> assert false
7679

77-
let extendop t sz s a =
78-
{memop = memop t a; sz = mem_size sz; ext = extension s}
80+
let extendop t sz s o a =
81+
{memop = memop t o a; sz = mem_size sz; ext = extension s}
7982

80-
let truncop t sz a =
81-
{memop = memop t a; sz = mem_size sz}
83+
let truncop t sz o a =
84+
{memop = memop t o a; sz = mem_size sz}
8285
}
8386

8487
let space = [' ''\t']
@@ -103,7 +106,7 @@ let nxx = ixx | fxx
103106
let mixx = "i" ("8" | "16" | "32" | "64")
104107
let mfxx = "f" ("32" | "64")
105108
let sign = "s" | "u"
106-
let align = digit+
109+
let digits = digit+
107110
let mem_size = "8" | "16" | "32"
108111

109112
rule token = parse
@@ -137,19 +140,31 @@ rule token = parse
137140
| "get_local" { GETLOCAL }
138141
| "set_local" { SETLOCAL }
139142

140-
| (nxx as t)".load" { LOAD (memop t "") }
141-
| (nxx as t)".load/"(align as a) { LOAD (memop t a) }
142-
| (nxx as t)".store" { STORE (memop t "") }
143-
| (nxx as t)".store/"(align as a) { STORE (memop t a) }
143+
| (nxx as t)".load" { LOAD (memop t "" "") }
144+
| (nxx as t)".load+"(digits as o) { LOAD (memop t o "") }
145+
| (nxx as t)".load/"(digits as a) { LOAD (memop t "" a) }
146+
| (nxx as t)".load+"(digits as o)"/"(digits as a) { LOAD (memop t o a) }
147+
| (nxx as t)".store" { STORE (memop t "" "") }
148+
| (nxx as t)".store+"(digits as o) { STORE (memop t o "") }
149+
| (nxx as t)".store/"(digits as a) { STORE (memop t "" a) }
150+
| (nxx as t)".store+"(digits as o)"/"(digits as a) { STORE (memop t o a) }
144151

145152
| (ixx as t)".load"(mem_size as sz)"_"(sign as s)
146-
{ LOADEXTEND (extendop t sz s "") }
147-
| (ixx as t)".load"(mem_size as sz)"_"(sign as s)"/"(align as a)
148-
{ LOADEXTEND (extendop t sz s a) }
153+
{ LOADEXTEND (extendop t sz s "" "") }
154+
| (ixx as t)".load"(mem_size as sz)"_"(sign as s)"+"(digits as o)
155+
{ LOADEXTEND (extendop t sz s o "") }
156+
| (ixx as t)".load"(mem_size as sz)"_"(sign as s)"/"(digits as a)
157+
{ LOADEXTEND (extendop t sz s "" a) }
158+
| (ixx as t)".load"(mem_size as sz)"_"(sign as s)"+"(digits as o)"/"(digits as a)
159+
{ LOADEXTEND (extendop t sz s o a) }
149160
| (ixx as t)".store"(mem_size as sz)
150-
{ STORETRUNC (truncop t sz "") }
151-
| (ixx as t)".store"(mem_size as sz)"/"(align as a)
152-
{ STORETRUNC (truncop t sz a) }
161+
{ STORETRUNC (truncop t sz "" "") }
162+
| (ixx as t)".store"(mem_size as sz)"+"(digits as o)
163+
{ STORETRUNC (truncop t sz o "") }
164+
| (ixx as t)".store"(mem_size as sz)"/"(digits as a)
165+
{ STORETRUNC (truncop t sz "" a) }
166+
| (ixx as t)".store"(mem_size as sz)"+"(digits as o)"/"(digits as a)
167+
{ STORETRUNC (truncop t sz o a) }
153168

154169
| (nxx as t)".switch" { SWITCH (value_type t) }
155170
| (nxx as t)".const" { CONST (value_type t) }

‎ml-proto/src/spec/ast.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -63,7 +63,7 @@ type binop = (Int32Op.binop, Int64Op.binop, Float32Op.binop, Float64Op.binop) op
6363
type relop = (Int32Op.relop, Int64Op.relop, Float32Op.relop, Float64Op.relop) op
6464
type cvt = (Int32Op.cvt, Int64Op.cvt, Float32Op.cvt, Float64Op.cvt) op
6565

66-
type memop = {ty : Types.value_type; align : int option}
66+
type memop = {ty : Types.value_type; offset : Memory.offset; align : int option}
6767
type extendop = {memop : memop; sz : Memory.mem_size; ext : Memory.extension}
6868
type truncop = {memop : memop; sz : Memory.mem_size}
6969

‎ml-proto/src/spec/check.ml

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -242,19 +242,21 @@ and check_arm c t et arm =
242242
check_expr c (if fallthru then None else et) e
243243

244244
and check_load c et memop e1 at =
245-
check_align memop.align at;
245+
check_memop memop at;
246246
check_expr c (Some Int32Type) e1;
247247
check_type (Some memop.ty) et at
248248

249249
and check_store c et memop e1 e2 at =
250-
check_align memop.align at;
250+
check_memop memop at;
251251
check_expr c (Some Int32Type) e1;
252252
check_expr c (Some memop.ty) e2;
253253
check_type None et at
254254

255-
and check_align align at =
256-
Lib.Option.app (fun a ->
257-
require (Lib.Int.is_power_of_two a) at "non-power-of-two alignment") align
255+
and check_memop memop at =
256+
require (memop.offset >= 0) at "negative offset";
257+
Lib.Option.app
258+
(fun a -> require (Lib.Int.is_power_of_two a) at "non-power-of-two alignment")
259+
memop.align
258260

259261
and check_mem_type ty sz at =
260262
require (ty = Int64Type || sz <> Memory.Mem32) at "memory size too big"

‎ml-proto/src/spec/eval.ml

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -168,31 +168,31 @@ let rec eval_expr (c : config) (e : expr) =
168168
local c x := v1;
169169
None
170170

171-
| Load ({ty; align = _}, e1) ->
171+
| Load ({ty; offset; align = _}, e1) ->
172172
let v1 = some (eval_expr c e1) e1.at in
173173
let a = Memory.address_of_value v1 in
174-
(try Some (Memory.load c.modul.memory a ty)
174+
(try Some (Memory.load c.modul.memory a offset ty)
175175
with exn -> memory_error e.at exn)
176176

177-
| Store ({ty = _; align = _}, e1, e2) ->
177+
| Store ({ty = _; offset; align = _}, e1, e2) ->
178178
let v1 = some (eval_expr c e1) e1.at in
179179
let v2 = some (eval_expr c e2) e2.at in
180180
let a = Memory.address_of_value v1 in
181-
(try Memory.store c.modul.memory a v2
181+
(try Memory.store c.modul.memory a offset v2
182182
with exn -> memory_error e.at exn);
183183
None
184184

185-
| LoadExtend ({memop = {ty; align = _}; sz; ext}, e1) ->
185+
| LoadExtend ({memop = {ty; offset; align = _}; sz; ext}, e1) ->
186186
let v1 = some (eval_expr c e1) e1.at in
187187
let a = Memory.address_of_value v1 in
188-
(try Some (Memory.load_extend c.modul.memory a sz ext ty)
188+
(try Some (Memory.load_extend c.modul.memory a offset sz ext ty)
189189
with exn -> memory_error e.at exn)
190190

191-
| StoreTrunc ({memop = {ty; align = _}; sz}, e1, e2) ->
191+
| StoreTrunc ({memop = {ty; offset; align = _}; sz}, e1, e2) ->
192192
let v1 = some (eval_expr c e1) e1.at in
193193
let v2 = some (eval_expr c e2) e2.at in
194194
let a = Memory.address_of_value v1 in
195-
(try Memory.store_trunc c.modul.memory a sz v2
195+
(try Memory.store_trunc c.modul.memory a offset sz v2
196196
with exn -> memory_error e.at exn);
197197
None
198198

‎ml-proto/src/spec/memory.ml

Lines changed: 44 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ open Values
1111

1212
type address = int
1313
type size = address
14+
type offset = address
1415
type mem_size = Mem8 | Mem16 | Mem32
1516
type extension = SX | ZX
1617
type segment = {addr : address; data : string}
@@ -66,60 +67,68 @@ let address_of_value = function
6667

6768
(* Load and store *)
6869

69-
let rec loadn mem n a =
70+
let effective_address a o =
71+
if max_int - a < o then raise Bounds;
72+
a + o
73+
74+
let rec loadn mem n ea =
7075
assert (n > 0 && n <= 8);
71-
let byte = try Int64.of_int !mem.{a} with Invalid_argument _ -> raise Bounds in
76+
let byte = try Int64.of_int !mem.{ea} with Invalid_argument _ -> raise Bounds in
7277
if n = 1 then
7378
byte
7479
else
75-
Int64.logor byte (Int64.shift_left (loadn mem (n-1) (a+1)) 8)
80+
Int64.logor byte (Int64.shift_left (loadn mem (n-1) (ea+1)) 8)
7681

77-
let rec storen mem n a v =
82+
let rec storen mem n ea v =
7883
assert (n > 0 && n <= 8);
7984
let byte = (Int64.to_int v) land 255 in
80-
(try !mem.{a} <- byte with Invalid_argument _ -> raise Bounds);
85+
(try !mem.{ea} <- byte with Invalid_argument _ -> raise Bounds);
8186
if (n > 1) then
82-
storen mem (n-1) (a+1) (Int64.shift_right v 8)
87+
storen mem (n-1) (ea+1) (Int64.shift_right v 8)
8388

84-
let load mem a t =
89+
let load mem a o t =
90+
let ea = effective_address a o in
8591
match t with
86-
| Int32Type -> Int32 (Int64.to_int32 (loadn mem 4 a))
87-
| Int64Type -> Int64 (loadn mem 8 a)
88-
| Float32Type -> Float32 (F32.of_bits (Int64.to_int32 (loadn mem 4 a)))
89-
| Float64Type -> Float64 (F64.of_bits (loadn mem 8 a))
92+
| Int32Type -> Int32 (Int64.to_int32 (loadn mem 4 ea))
93+
| Int64Type -> Int64 (loadn mem 8 ea)
94+
| Float32Type -> Float32 (F32.of_bits (Int64.to_int32 (loadn mem 4 ea)))
95+
| Float64Type -> Float64 (F64.of_bits (loadn mem 8 ea))
9096

91-
let store mem a v =
97+
let store mem o a v =
98+
let ea = effective_address a o in
9299
match v with
93-
| Int32 x -> storen mem 4 a (Int64.of_int32 x)
94-
| Int64 x -> storen mem 8 a x
95-
| Float32 x -> storen mem 4 a (Int64.of_int32 (F32.to_bits x))
96-
| Float64 x -> storen mem 8 a (F64.to_bits x)
100+
| Int32 x -> storen mem 4 ea (Int64.of_int32 x)
101+
| Int64 x -> storen mem 8 ea x
102+
| Float32 x -> storen mem 4 ea (Int64.of_int32 (F32.to_bits x))
103+
| Float64 x -> storen mem 8 ea (F64.to_bits x)
97104

98-
let loadn_sx mem n a =
105+
let loadn_sx mem n ea =
99106
assert (n > 0 && n <= 8);
100-
let v = loadn mem n a in
107+
let v = loadn mem n ea in
101108
let shift = 64 - (8 * n) in
102109
Int64.shift_right (Int64.shift_left v shift) shift
103110

104-
let load_extend mem a sz ext t =
111+
let load_extend mem a o sz ext t =
112+
let ea = effective_address a o in
105113
match sz, ext, t with
106-
| Mem8, ZX, Int32Type -> Int32 (Int64.to_int32 (loadn mem 1 a))
107-
| Mem8, SX, Int32Type -> Int32 (Int64.to_int32 (loadn_sx mem 1 a))
108-
| Mem8, ZX, Int64Type -> Int64 (loadn mem 1 a)
109-
| Mem8, SX, Int64Type -> Int64 (loadn_sx mem 1 a)
110-
| Mem16, ZX, Int32Type -> Int32 (Int64.to_int32 (loadn mem 2 a))
111-
| Mem16, SX, Int32Type -> Int32 (Int64.to_int32 (loadn_sx mem 2 a))
112-
| Mem16, ZX, Int64Type -> Int64 (loadn mem 2 a)
113-
| Mem16, SX, Int64Type -> Int64 (loadn_sx mem 2 a)
114-
| Mem32, ZX, Int64Type -> Int64 (loadn mem 4 a)
115-
| Mem32, SX, Int64Type -> Int64 (loadn_sx mem 4 a)
114+
| Mem8, ZX, Int32Type -> Int32 (Int64.to_int32 (loadn mem 1 ea))
115+
| Mem8, SX, Int32Type -> Int32 (Int64.to_int32 (loadn_sx mem 1 ea))
116+
| Mem8, ZX, Int64Type -> Int64 (loadn mem 1 ea)
117+
| Mem8, SX, Int64Type -> Int64 (loadn_sx mem 1 ea)
118+
| Mem16, ZX, Int32Type -> Int32 (Int64.to_int32 (loadn mem 2 ea))
119+
| Mem16, SX, Int32Type -> Int32 (Int64.to_int32 (loadn_sx mem 2 ea))
120+
| Mem16, ZX, Int64Type -> Int64 (loadn mem 2 ea)
121+
| Mem16, SX, Int64Type -> Int64 (loadn_sx mem 2 ea)
122+
| Mem32, ZX, Int64Type -> Int64 (loadn mem 4 ea)
123+
| Mem32, SX, Int64Type -> Int64 (loadn_sx mem 4 ea)
116124
| _ -> raise Type
117125

118-
let store_trunc mem a sz v =
126+
let store_trunc mem a o sz v =
127+
let ea = effective_address a o in
119128
match sz, v with
120-
| Mem8, Int32 x -> storen mem 1 a (Int64.of_int32 x)
121-
| Mem8, Int64 x -> storen mem 1 a x
122-
| Mem16, Int32 x -> storen mem 2 a (Int64.of_int32 x)
123-
| Mem16, Int64 x -> storen mem 2 a x
124-
| Mem32, Int64 x -> storen mem 4 a x
129+
| Mem8, Int32 x -> storen mem 1 ea (Int64.of_int32 x)
130+
| Mem8, Int64 x -> storen mem 1 ea x
131+
| Mem16, Int32 x -> storen mem 2 ea (Int64.of_int32 x)
132+
| Mem16, Int64 x -> storen mem 2 ea x
133+
| Mem32, Int64 x -> storen mem 4 ea x
125134
| _ -> raise Type

‎ml-proto/src/spec/memory.mli

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ type memory
66
type t = memory
77
type address = int
88
type size = address
9+
type offset = address
910
type mem_size = Mem8 | Mem16 | Mem32
1011
type extension = SX | ZX
1112
type segment = {addr : address; data : string}
@@ -20,9 +21,9 @@ val create : size -> memory
2021
val init : memory -> segment list -> unit
2122
val size : memory -> size
2223
val resize : memory -> size -> unit
23-
val load : memory -> address -> value_type -> value
24-
val store : memory -> address -> value -> unit
25-
val load_extend : memory -> address -> mem_size -> extension -> value_type -> value
26-
val store_trunc : memory -> address -> mem_size -> value -> unit
24+
val load : memory -> address -> offset -> value_type -> value
25+
val store : memory -> address -> offset -> value -> unit
26+
val load_extend : memory -> address -> offset -> mem_size -> extension -> value_type -> value
27+
val store_trunc : memory -> address -> offset -> mem_size -> value -> unit
2728

2829
val address_of_value : Values.value -> address

‎ml-proto/test/address.wasm

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
(module
2+
(import $print "stdio" "print" (param i32))
3+
(memory 1024 (segment 0 "ab"))
4+
(func $good
5+
(call_import $print (i32.load8_u+0 (i32.const 0)))
6+
(call_import $print (i32.load8_u+1 (i32.const 0)))
7+
(call_import $print (i32.load8_u (i32.add (i32.const -1) (i32.const 1))))
8+
)
9+
(func $bad
10+
(i32.load8_u+1 (i32.const -1))
11+
)
12+
(export "good" $good)
13+
(export "bad" $bad)
14+
)
15+
16+
(invoke "good")
17+
(assert_trap (invoke "bad") "runtime: out of bounds memory access")

‎ml-proto/test/expected-output/address.wasm.log

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
97 : i32
2+
98 : i32
3+
97 : i32

0 commit comments

Comments
 (0)