Add constant offsets to spec

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=<uint>
+align: align=(1|2|4|8|...)
 cvtop: trunc_s | trunc_u | extend_s | extend_u | ...
 
 expr:
@@ -145,8 +146,8 @@ expr:
   ( return <expr>? )                             ;; = (break <current_depth> <expr>?)
   ( get_local <var> )
   ( set_local <var> <expr> )
-  ( <type>.load((8|16)_<sign>)?(/<align>)? <expr> )
-  ( <type>.store(/<align>)? <expr> <expr> )
+  ( <type>.load((8|16)_<sign>)? <offset>? <align>? <expr> )
+  ( <type>.store <offset>? <align>? <expr> <expr> )
   ( <type>.const <value> )
   ( <type>.<unop> <expr> )
   ( <type>.<binop> <expr> <expr> )

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) }

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<Ast.memop> STORE
 %token<Ast.extop> LOAD_EXTEND
 %token<Ast.wrapop> STORE_WRAP
+%token<Memory.offset> OFFSET
+%token<int> 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) }

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 =

ml-proto/spec/check.ml

@@ -232,23 +232,25 @@ 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
 
 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"

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 ->

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,55 +97,59 @@ 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 =
   !mem.{i} <- (Int64.to_int v) land 255;
   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

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