[sanguineman]

Summary

array.copy reduces to a sequence of array.get and array.set instructions. The reduction rules determine the optional signedness annotation sx? of array.get from the source element type, using the auxiliary function $sx:

rule Step_read/array.copy-le:
  z; (REF.ARRAY_ADDR a_1) (CONST I32 i_1) (REF.ARRAY_ADDR a_2) (CONST I32 i_2) (CONST I32 n) (ARRAY.COPY x_1 x_2)  ~>
    (REF.ARRAY_ADDR a_1) (CONST I32 i_1)
    (REF.ARRAY_ADDR a_2) (CONST I32 i_2)
    (ARRAY.GET sx? x_2) (ARRAY.SET x_1)
    ...
  -- otherwise
  -- Expand: $type(z, x_2) ~~ ARRAY (mut? zt_2)
  -- if i_1 <= i_2
     /\ sx? = $sx(zt_2)

However, $sx only has cases for constant types and packed types:

def $sx(storagetype) : sx?
def $sx(consttype) = eps  ;; consttype = numtype | vectype
def $sx(packtype) = S

Since storagetype = valtype | packtype, $sx is undefined for reference types. Therefore, when the source array has a reference element type and n > 0, neither Step_read/array.copy-le nor Step_read/array.copy-gt applies, and no other array.copy rule applies either. Execution gets stuck.

For example, the following module is valid, since Instr_ok/array.copy only requires the source element type to be a subtype of the destination element type:

(module
  (type $a (array (mut funcref)))
  (func (export "copy") (result i32)
    (array.copy $a $a
      (array.new_default $a (i32.const 1)) (i32.const 0)
      (array.new_default $a (i32.const 1)) (i32.const 0)
      (i32.const 1))
    (i32.const 42)))
(assert_return (invoke "copy") (i32.const 42))

The OCaml reference interpreter runs it as expected, because it passes no sign extension for any non-packed element type:

let exto =
  match arraytype_of_comptype (expand_deftype (Aggr.type_of_array sa)) with
  | FieldT (_, PackStorageT _) -> Some U
  | _ -> None
in

The SpecTec interpreter, on the other hand, fails in $sx:

$sx: on expr `type(storagetype) == packtype` assertion fail

This case was not caught because test/core/gc/array_copy.wast only executes array.copy on i8 arrays. Arrays of reference type appear only in assert_invalid modules.

Fix

This PR replaces the consttype clause of $sx with a valtype clause, so that $sx returns eps for every non-packed storage type, including reference types:

def $sx(valtype) = eps
def $sx(packtype) = S

This is consistent with Instr_ok/array.get, which requires sx? =/= eps <=> $is_packtype(zt).

The change is applied to both wasm-3.0 and wasm-latest, and the SpecTec test expectations are updated accordingly.

A regression test copies an i31ref array, covering both Step_read/array.copy-le and Step_read/array.copy-gt.

Testing

• make -C interpreter test/gc/array_copy
• cd spectec && dune runtest test-frontend test-middlend test-latex test-prose test-splice
• spectec/spectec specification/wasm-3.0/*.spectec --interpreter test/core/gc/array_copy.wast (fails at the new test before this change, passes after)

[rossberg]

Thanks!

[rossberg]

@sanguineman, I'm afraid you need to join the CG to pass the IPC check.

[sanguineman]

@rossberg, thanks for the heads-up. I've joined the CG, and it passes the check now.