moving mem existence and alignment from rewrite to typecheck

CHANGES.md

@@ -9,6 +9,7 @@
 - start benchmarking against test-comp
 - fix handling of `select` and `call_indirect` in the text format
 - add `owi wat2wasm` subcommand
+- moving memory existence and alignment from rewrite module to typecheck module
 
 ## 0.2 - 2024-04-24
 

src/text_to_binary/rewrite.ml

@@ -248,55 +248,17 @@ let rewrite_expr (modul : Assigned.t) (locals : binary param list)
     | Elem_drop id ->
       let* id = find_elem (Some id) in
       ok @@ Elem_drop id
-    (* TODO: should we check alignment or memory existence first ? is it tested in the reference implementation ? *)
-    | I_load8 (nn, sx, memarg) ->
-      if List.length modul.mem.values < 1 then Error (`Unknown_memory 0)
-      else if memarg.align >= 1l then Error `Alignment_too_large
-      else Ok (I_load8 (nn, sx, memarg))
-    | I_store8 (nn, memarg) ->
-      if List.length modul.mem.values < 1 then Error (`Unknown_memory 0)
-      else if memarg.align >= 1l then Error `Alignment_too_large
-      else ok @@ I_store8 (nn, memarg)
-    | I_load16 (nn, sx, memarg) ->
-      if List.length modul.mem.values < 1 then Error (`Unknown_memory 0)
-      else if memarg.align >= 2l then Error `Alignment_too_large
-      else ok @@ I_load16 (nn, sx, memarg)
-    | I_store16 (nn, memarg) ->
-      if List.length modul.mem.values < 1 then Error (`Unknown_memory 0)
-      else if memarg.align >= 2l then Error `Alignment_too_large
-      else ok @@ I_store16 (nn, memarg)
-    | I64_load32 (nn, memarg) ->
-      if List.length modul.mem.values < 1 then Error (`Unknown_memory 0)
-      else if memarg.align >= 4l then Error `Alignment_too_large
-      else ok @@ I64_load32 (nn, memarg)
-    | I64_store32 memarg ->
-      if List.length modul.mem.values < 1 then Error (`Unknown_memory 0)
-      else if memarg.align >= 4l then Error `Alignment_too_large
-      else ok @@ I64_store32 memarg
-    | I_load (nn, memarg) ->
-      if List.length modul.mem.values < 1 then Error (`Unknown_memory 0)
-      else
-        let max_allowed = match nn with S32 -> 4l | S64 -> 8l in
-        if memarg.align >= max_allowed then Error `Alignment_too_large
-        else ok @@ I_load (nn, memarg)
-    | F_load (nn, memarg) ->
-      if List.length modul.mem.values < 1 then Error (`Unknown_memory 0)
-      else
-        let max_allowed = match nn with S32 -> 4l | S64 -> 8l in
-        if memarg.align >= max_allowed then Error `Alignment_too_large
-        else ok @@ F_load (nn, memarg)
-    | F_store (nn, memarg) ->
-      if List.length modul.mem.values < 1 then Error (`Unknown_memory 0)
-      else
-        let max_allowed = match nn with S32 -> 4l | S64 -> 8l in
-        if memarg.align >= max_allowed then Error `Alignment_too_large
-        else ok @@ F_store (nn, memarg)
-    | I_store (nn, memarg) ->
-      if List.length modul.mem.values < 1 then Error (`Unknown_memory 0)
-      else
-        let max_allowed = match nn with S32 -> 4l | S64 -> 8l in
-        if memarg.align >= max_allowed then Error `Alignment_too_large
-        else ok @@ I_store (nn, memarg)
+    (* alignment and memory existence checks have been moved in typecheck ? TODO: is it tested in the reference implementation ? *)
+    | I_load8 (nn, sx, memarg) -> ok @@ I_load8 (nn, sx, memarg)
+    | I_store8 (nn, memarg) -> ok @@ I_store8 (nn, memarg)
+    | I_load16 (nn, sx, memarg) -> ok @@ I_load16 (nn, sx, memarg)
+    | I_store16 (nn, memarg) -> ok @@ I_store16 (nn, memarg)
+    | I64_load32 (nn, memarg) -> ok @@ I64_load32 (nn, memarg)
+    | I64_store32 memarg -> ok @@ I64_store32 memarg
+    | I_load (nn, memarg) -> ok @@ I_load (nn, memarg)
+    | F_load (nn, memarg) -> ok @@ F_load (nn, memarg)
+    | F_store (nn, memarg) -> ok @@ F_store (nn, memarg)
+    | I_store (nn, memarg) -> ok @@ I_store (nn, memarg)
     | (Memory_copy | Memory_size | Memory_fill | Memory_grow) as i ->
       if List.length modul.mem.values < 1 then Error (`Unknown_memory 0)
       else Ok i

src/validate/typecheck.ml

@@ -36,6 +36,7 @@ end
 module Env = struct
   type t =
     { locals : typ Index.Map.t
+    ; mem : (mem, limits) Runtime.t Named.t
     ; globals : (global, binary global_type) Runtime.t Named.t
     ; result_type : binary result_type
     ; funcs : (binary func, binary block_type) Runtime.t Named.t
@@ -85,7 +86,8 @@ module Env = struct
     let value = Indexed.get_at_exn i env.elems.values in
     value.typ
 
-  let make ~params ~locals ~globals ~funcs ~result_type ~tables ~elems ~refs =
+  let make ~params ~locals ~mem ~globals ~funcs ~result_type ~tables ~elems
+    ~refs =
     let l = List.mapi (fun i v -> (i, v)) (params @ locals) in
     let locals =
       List.fold_left
@@ -94,7 +96,16 @@ module Env = struct
           Index.Map.add i typ locals )
         Index.Map.empty l
     in
-    { locals; globals; result_type; funcs; tables; elems; blocks = []; refs }
+    { locals
+    ; mem
+    ; globals
+    ; result_type
+    ; funcs
+    ; tables
+    ; elems
+    ; blocks = []
+    ; refs
+    }
 end
 
 type env = Env.t
@@ -223,6 +234,11 @@ end
 
 let rec typecheck_instr (env : env) (stack : stack) (instr : binary instr) :
   stack Result.t =
+  let check_mem memarg_align align =
+    if List.length env.mem.values < 1 then Error (`Unknown_memory 0)
+    else if memarg_align >= align then Error `Alignment_too_large
+    else Ok ()
+  in
   match instr with
   | Nop -> Ok stack
   | Drop -> Stack.drop stack
@@ -281,19 +297,45 @@ let rec typecheck_instr (env : env) (stack : stack) (instr : binary instr) :
     let* stack_e1 = typecheck_expr env e1 ~is_loop:false block_type ~stack in
     let+ _stack_e2 = typecheck_expr env e2 ~is_loop:false block_type ~stack in
     stack_e1
-  | I_load (nn, _) | I_load16 (nn, _, _) | I_load8 (nn, _, _) ->
+  | I_load8 (nn, _, memarg) ->
+    let* () = check_mem memarg.align 1l in
+    let* stack = Stack.pop [ i32 ] stack in
+    Stack.push [ itype nn ] stack
+  | I_load16 (nn, _, memarg) ->
+    let* () = check_mem memarg.align 2l in
     let* stack = Stack.pop [ i32 ] stack in
     Stack.push [ itype nn ] stack
-  | I64_load32 _ ->
+  | I_load (nn, memarg) ->
+    let max_allowed = match nn with S32 -> 4l | S64 -> 8l in
+    let* () = check_mem memarg.align max_allowed in
+    let* stack = Stack.pop [ i32 ] stack in
+    Stack.push [ itype nn ] stack
+  | I64_load32 (_, memarg) ->
+    let* () = check_mem memarg.align 4l in
     let* stack = Stack.pop [ i32 ] stack in
     Stack.push [ i64 ] stack
-  | I_store8 (nn, _) | I_store16 (nn, _) | I_store (nn, _) ->
+  | I_store8 (nn, memarg) ->
+    let* () = check_mem memarg.align 1l in
+    Stack.pop [ itype nn; i32 ] stack
+  | I_store16 (nn, memarg) ->
+    let* () = check_mem memarg.align 2l in
+    Stack.pop [ itype nn; i32 ] stack
+  | I_store (nn, memarg) ->
+    let max_allowed = match nn with S32 -> 4l | S64 -> 8l in
+    let* () = check_mem memarg.align max_allowed in
     Stack.pop [ itype nn; i32 ] stack
-  | I64_store32 _ -> Stack.pop [ i64; i32 ] stack
-  | F_load (nn, _) ->
+  | I64_store32 memarg ->
+    let* () = check_mem memarg.align 4l in
+    Stack.pop [ i64; i32 ] stack
+  | F_load (nn, memarg) ->
+    let max_allowed = match nn with S32 -> 4l | S64 -> 8l in
+    let* () = check_mem memarg.align max_allowed in
     let* stack = Stack.pop [ i32 ] stack in
     Stack.push [ ftype nn ] stack
-  | F_store (nn, _) -> Stack.pop [ ftype nn; i32 ] stack
+  | F_store (nn, memarg) ->
+    let max_allowed = match nn with S32 -> 4l | S64 -> 8l in
+    let* () = check_mem memarg.align max_allowed in
+    Stack.pop [ ftype nn; i32 ] stack
   | I_reinterpret_f (inn, fnn) ->
     let* stack = Stack.pop [ ftype fnn ] stack in
     Stack.push [ itype inn ] stack
@@ -504,7 +546,7 @@ let typecheck_function (modul : modul) func refs =
   | Local func ->
     let (Bt_raw ((None | Some _), (params, result))) = func.type_f in
     let env =
-      Env.make ~params ~funcs:modul.func ~locals:func.locals
+      Env.make ~params ~funcs:modul.func ~locals:func.locals ~mem:modul.mem
         ~globals:modul.global ~result_type:result ~tables:modul.table
         ~elems:modul.elem ~refs
     in

test/script/gc.t

@@ -21,7 +21,7 @@
   [23]
   $ owi script --no-exhaustion reference/proposals/gc/ref_eq.wast
   owi: internal error, uncaught exception:
-       File "src/validate/typecheck.ml", line 478, characters 4-10: Assertion failed
+       File "src/validate/typecheck.ml", line 520, characters 4-10: Assertion failed
 
   [125]
   $ owi script --no-exhaustion reference/proposals/gc/ref_test.wast