[interpreter] Validate offsets against the selected memory

[sanguineman]

Summary

WebAssembly load instructions consume a base address from the operand stack, add the static offset encoded in the instruction, and read a value from the resulting address in the selected linear memory.

The selected memory's address type determines both the type of the base address and the valid range of the static offset. A memory32 instruction consumes an i32 base address and requires its offset to be less than 2^32. A memory64 instruction consumes an i64 base address and permits offsets in the wider u64 range.

The validation specification written in SpecTec checks these conditions using the address type of the selected memory.

However, the OCaml reference interpreter uses two different memories while validating a memory instruction. The instruction validator obtains the stack address type from the selected memory x, but check_memop obtains the address type used for offset validation from memory 0.

(* valid.ml *)
let rec check_instr (c : context) (e : instr) (s : infer_resulttype) : infer_instrtype =
  match e.it with
  (* ... *)
  | Load (x, memop) ->
    let MemoryT (at, _lim) = memory c x in (* address type from the memory at index x *)
    let t = check_memop c memop num_size (Lib.Option.map fst) e.at in
    [NumT (numtype_of_addrtype at)] --> [NumT t], []

(* valid.ml *)
let check_memop (c : context) (memop : ('t, 's) memop) ty_size get_sz at =
  let size =
    match get_sz memop.pack with
    | None -> ty_size memop.ty
    | Some sz ->
      check_pack sz (ty_size memop.ty) at;
      Pack.packed_size sz
  in
  require (1 lsl memop.align >= 1 && 1 lsl memop.align <= size) at
    "alignment must not be larger than natural";
  let MemoryT (at_, _lim) = memory c (0l @@ at) in (* address type from the memory at index 0, not x *) 
  if at_ = I32AT then
    require (I64.lt_u memop.offset 0x1_0000_0000L) at
      "offset out of range";
  memop.ty

As a result, offset validation can use the wrong address type when the selected memory and memory 0 have different address types.

For example, consider a module where memory 0 is a memory64 and memory 1 is a memory32:

(assert_invalid
  (module
    (memory i64 0)
    (memory 0)
    (func
      i32.const 0
      i32.load 1 offset=4294967296
      drop)
  )
  "offset out of range"
)

A load from memory 1 with an offset of 4294967296 must be rejected because the selected memory is a memory32 and the offset is equal to 2^32.

The reference interpreter instead checks the offset against the address type of memory 0. Because memory 0 is a memory64, it skips the memory32 offset bound and accepts the invalid instruction.

The declarative SpecTec validation rule does not have this mismatch. It obtains the address type at from C.MEMS[x] and passes the same address type to Memarg_ok:

rule Instr_ok/load-val:
  C |- LOAD nt x memarg : at -> nt
  -- if C.MEMS[x] = at lim PAGE
  -- Memarg_ok: |- memarg : at -> $size(nt)

Fix

This PR passes the selected memory index x to check_memop and uses that memory to validate the offset. The stack address type and the offset bound are therefore derived from the same selected memory.

Because check_memop is shared by numeric and vector load/store instructions, the correction applies consistently to Load, Store, VecLoad, VecStore, VecLoadLane, and VecStoreLane.

A regression test declares memory 0 as memory64 and memory 1 as memory32, then verifies that a load from memory 1 with an offset of 2^32 is rejected with offset out of range.

Testing

• make -C interpreter test/memory64/load64
• make -C interpreter unittest

[rossberg]

Thanks!