Use int64 for addresses and sizes, isolate BigArray int limitation

ml-proto/given/lib.ml

@@ -44,3 +44,10 @@ struct
     if x < 0 then failwith "is_power_of_two";
     x <> 0 && (x land (x - 1)) = 0
 end
+
+module Int64 =
+struct
+  let is_power_of_two x =
+    if x < 0L then failwith "is_power_of_two";
+    x <> 0L && (Int64.logand x (Int64.sub x 1L)) = 0L
+end

ml-proto/given/lib.mli

@@ -23,3 +23,8 @@ module Int :
 sig
   val is_power_of_two : int -> bool
 end
+
+module Int64 :
+sig
+  val is_power_of_two : int64 -> bool
+end

ml-proto/host/params.ml

@@ -1 +1 @@
-let page_size = 4096
+let page_size = 4096L

ml-proto/host/parser.mly

@@ -269,7 +269,7 @@ func :
 
 segment :
   | LPAR SEGMENT INT TEXT RPAR
-    { {Memory.addr = int_of_string $3; Memory.data = $4} @@ at() }
+    { {Memory.addr = Int64.of_string $3; Memory.data = $4} @@ at() }
 ;
 segment_list :
   | /* empty */ { [] }
@@ -278,10 +278,10 @@ segment_list :
 
 memory :
   | LPAR MEMORY INT INT segment_list RPAR
-    { {initial = int_of_string $3; max = int_of_string $4; segments = $5 }
+    { {initial = Int64.of_string $3; max = Int64.of_string $4; segments = $5}
         @@ at() }
   | LPAR MEMORY INT segment_list RPAR
-    { {initial = int_of_string $3; max = int_of_string $3; segments = $4 }
+    { {initial = Int64.of_string $3; max = Int64.of_string $3; segments = $4}
         @@ at() }
 ;
 

ml-proto/host/script.ml

@@ -25,7 +25,7 @@ let trace name = if !Flags.trace then print_endline ("-- " ^ name)
 let current_module : Eval.instance option ref = ref None
 
 let eval_args es at =
-  let evs = List.map Eval.eval es in
+  let evs = List.map Eval.host_eval es in
   let reject_none = function
     | Some v -> v
     | None -> Error.error at "unexpected () value" in
@@ -88,7 +88,7 @@ let run_command cmd =
     let m = get_module cmd.at in
     let arg_vs = eval_args arg_es cmd.at in
     let got_v = Eval.invoke m name arg_vs in
-    let expect_v = Eval.eval expect_e in
+    let expect_v = Eval.host_eval expect_e in
     (match got_v, expect_v with
      | Some Int32 got_i32, Some Int32 expect_i32 ->
        if got_i32 <> expect_i32 then begin

ml-proto/spec/check.ml

@@ -22,13 +22,10 @@ type context =
   tables : func_type list;
   locals : value_type list;
   return : expr_type;
-  labels : expr_type list
+  labels : expr_type list;
+  has_memory : bool
 }
 
-let c0 =
-  {funcs = []; imports = []; tables = [];
-   locals = []; return = None; labels = []}
-
 let lookup category list x =
   try List.nth list x.it with Failure _ ->
     error x.at ("unknown " ^ category ^ " " ^ string_of_int x.it)
@@ -215,12 +212,15 @@ let rec check_expr c et e =
     check_type (Some t) et e.at
 
   | PageSize ->
+    check_has_memory c e.at;
     check_type (Some Int32Type) et e.at
 
   | MemorySize ->
+    check_has_memory c e.at;
     check_type (Some Int32Type) et e.at
 
   | ResizeMemory e ->
+    check_has_memory c e.at;
     check_expr c (Some Int32Type) e;
     check_type None et e.at
 
@@ -243,16 +243,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_has_memory c 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_has_memory c at;
   check_align memop.align 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 ops 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
@@ -281,14 +286,15 @@ let check_func c f =
                    return = Lib.Option.map it result} in
   check_expr c' (Lib.Option.map it result) e
 
-let check_table c tab =
+let check_table funcs tables tab =
   match tab.it with
   | [] ->
     error tab.at "empty table"
   | x::xs ->
-    let s = func c x in
-    List.iter (fun xI -> check_func_type (func c xI) s xI.at) xs;
-    {c with tables = c.tables @ [s]}
+    let func x = lookup "function" funcs x in
+    let s = func x in
+    List.iter (fun xI -> check_func_type (func xI) s xI.at) xs;
+    tables @ [s]
 
 module NameSet = Set.Make(String)
 
@@ -300,23 +306,32 @@ let check_export c set ex =
   NameSet.add name set
 
 let check_segment size prev_end seg =
-  let seg_end = seg.it.Memory.addr + String.length seg.it.Memory.data in
+  let seg_len = Int64.of_int (String.length seg.it.Memory.data) in
+  let seg_end = Int64.add seg.it.Memory.addr seg_len in
   require (seg.it.Memory.addr >= prev_end) seg.at
     "data segment not disjoint and ordered";
   require (size >= seg_end) seg.at
     "data segment does not fit memory";
   seg_end
 
 let check_memory memory =
-  require (memory.it.initial <= memory.it.max) memory.at
+  let mem = memory.it in
+  require (mem.initial <= mem.max) memory.at
     "initial memory size must be less than maximum";
-  ignore (List.fold_left (check_segment memory.it.initial) 0 memory.it.segments)
+  require (mem.max <= 4294967296L) memory.at
+    "linear memory size must be less or equal to 4GiB";
+  ignore (List.fold_left (check_segment mem.initial) Int64.zero mem.segments)
 
 let check_module m =
   let {imports; exports; tables; funcs; memory} = m.it in
   Lib.Option.app check_memory memory;
-  let c = {c0 with funcs = List.map type_func funcs;
-                 imports = List.map type_import imports} in
-  let c' = List.fold_left check_table c tables in
-  List.iter (check_func c') funcs;
-  ignore (List.fold_left (check_export c') NameSet.empty exports)
+  let func_types = List.map type_func funcs in
+  let c = {funcs = func_types;
+           imports = List.map type_import imports;
+           tables = List.fold_left (check_table func_types) [] tables;
+           locals = [];
+           return = None;
+           labels = [];
+           has_memory = memory <> None} in
+  List.iter (check_func c) funcs;
+  ignore (List.fold_left (check_export c) NameSet.empty exports)

ml-proto/spec/eval.ml

@@ -25,7 +25,7 @@ type instance =
   imports : import list;
   exports : export_map;
   tables : func list list;
-  memory : Memory.t;
+  memory : Memory.t option;
   host : host_params
 }
 
@@ -42,9 +42,6 @@ type config =
   return : label
 }
 
-let page_size c =
-  I32.of_int32 (Int32.of_int c.module_.host.page_size)
-
 let lookup category list x =
   try List.nth list x.it with Failure _ ->
     error x.at ("runtime: undefined " ^ category ^ " " ^ string_of_int x.it)
@@ -88,6 +85,11 @@ let numerics_error at = function
       error at "runtime: invalid conversion to integer"
   | exn -> raise exn
 
+let some_memory c at =
+  match c.module_.memory with
+  | Some m -> m
+  | _ -> error at "memory operation but no memory section"
+
 let some v at =
   match v with
   | Some v -> v
@@ -98,6 +100,11 @@ let int32 v at =
   | Int32 i -> i
   | v -> type_error at v Types.Int32Type
 
+let mem_size v at =
+  let i32 = int32 v at in
+  let i64 = Int64.of_int32 i32 in
+  Int64.shift_right_logical (Int64.shift_left i64 32) 32
+
 
 (* Evaluation *)
 
@@ -169,31 +176,27 @@ let rec eval_expr (c : config) (e : expr) =
     Some v1
 
   | Load ({ty; 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.module_.memory a ty)
-    with exn -> memory_error e.at exn)
+    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)
 
   | Store ({ty = _; align = _}, e1, e2) ->
-    let v1 = some (eval_expr c e1) e1.at in
+    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
-    let a = Memory.address_of_value v1 in
-    (try Memory.store c.module_.memory a v2
-    with exn -> memory_error e.at exn);
+    (try Memory.store mem v1 v2 with exn -> memory_error e.at exn);
     Some v2
 
   | 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.module_.memory a sz ext ty)
-    with exn -> memory_error e.at exn)
+    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) with exn -> memory_error e.at exn)
 
   | StoreWrap ({memop = {ty; align = _}; sz}, e1, e2) ->
-    let v1 = some (eval_expr c e1) e1.at in
+    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
-    let a = Memory.address_of_value v1 in
-    (try Memory.store_wrap c.module_.memory a sz v2
-    with exn -> memory_error e.at exn);
+    (try Memory.store_wrap mem v1 sz v2 with exn -> memory_error e.at exn);
     Some v2
 
   | Const v ->
@@ -232,17 +235,20 @@ let rec eval_expr (c : config) (e : expr) =
       | exn -> numerics_error e.at exn)
 
   | PageSize ->
-    Some (Int32 (page_size c))
+    Some (Int32 (Int64.to_int32 c.module_.host.page_size))
 
   | MemorySize ->
-    Some (Int32 (I32.of_int32 (Int32.of_int (Memory.size c.module_.memory))))
+    let mem = some_memory c e.at in
+    let i64 = Memory.size mem in
+    assert (i64 < Int64.of_int32 (Int32.max_int));
+    Some (Int32 (Int64.to_int32 i64))
 
   | ResizeMemory e ->
-    let i = int32 (eval_expr c e) e.at in
-    if (I32.rem_u i (page_size c)) <> I32.zero then
+    let mem = some_memory c e.at in
+    let sz = mem_size (eval_expr c e) e.at in
+    if (Int64.rem sz c.module_.host.page_size) <> 0L then
       error e.at "runtime: resize_memory operand not multiple of page_size";
-    (* TODO: The conversion to int could overflow. *)
-    Memory.resize c.module_.memory (Int32.to_int i);
+    Memory.resize mem sz;
     None
 
 and eval_expr_option c eo =
@@ -272,36 +278,32 @@ and eval_func (m : instance) (f : func) (evs : value list) =
 
 (* Modules *)
 
-let init_memory ast =
-  match ast with
-  | None ->
-    Memory.create 0
-  | Some {it = {initial; segments; _}} ->
-    let mem = Memory.create initial in
-    Memory.init mem (List.map it segments);
-    mem
+let init_memory {it = {initial; segments; _}} =
+  let mem = Memory.create initial in
+  Memory.init mem (List.map it segments);
+  mem
 
 let init m imports host =
   assert (List.length imports = List.length m.it.Ast.imports);
-  assert (host.page_size > 0);
-  assert (Lib.Int.is_power_of_two host.page_size);
+  assert (host.page_size > 0L);
+  assert (Lib.Int64.is_power_of_two host.page_size);
   let {Ast.exports; tables; funcs; memory; _} = m.it in
-  let mem = init_memory memory in
+  let memory' = Lib.Option.map init_memory memory in
   let func x = List.nth funcs x.it in
   let export ex = ExportMap.add ex.it.name (func ex.it.func) in
   let exports = List.fold_right export exports ExportMap.empty in
   let tables = List.map (fun tab -> List.map func tab.it) tables in
-  {funcs; imports; exports; tables; memory = mem; host}
+  {funcs; imports; exports; tables; memory = memory'; host}
 
 let invoke m name vs =
   let f = export m (name @@ no_region) in
   assert (List.length vs = List.length f.it.params);
   eval_func m f vs
 
-let eval e =
+(* This function is not part of the spec. *)
+let host_eval e =
   let f = {params = []; result = None; locals = []; body = e} @@ no_region in
-  let memory = Memory.create 0 in
   let exports = ExportMap.singleton "eval" f in
-  let host = {page_size = 1} in
-  let m = {imports = []; exports; tables = []; funcs = [f]; memory; host} in
+  let host = {page_size = 1L} in
+  let m = {imports = []; exports; tables = []; funcs = [f]; memory = None; host} in
   eval_func m f []

ml-proto/spec/eval.mli

@@ -10,4 +10,6 @@ type host_params = {page_size : Memory.size}
 val init : Ast.module_ -> import list -> host_params -> instance
 val invoke : instance -> string -> value list -> value option
   (* raise Error.Error *)
-val eval : Ast.expr -> value option (* raise Error.Error *)
+
+(* This function is not part of the spec. *)
+val host_eval : Ast.expr -> value option (* raise Error.Error *)