Iteration variable not set properly

[702fbtngus]

When running test-interpreter/spec-test-3/simd/simd_lane.wast, below failure comes out:

===== test-interpreter/spec-test-3/simd/simd_lane.wast =====
- Test failed at test-interpreter/spec-test-3/simd/simd_lane.wast:292.1-295.70 (Failure("Failed Array.get on base [] and index 0: IdxP (AccE (IterE (VarE (ci), [ci], *), IdxP (VarE (k)))) @"))

The test case and corresponding reduction rule is written as follows:

(assert_return (invoke "v8x16_swizzle"
  (v128.const i8x16 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31)
  (v128.const i8x16  0  1  2  3  4  5  6  7  8  9 10 11 12 13 14 15))
  (v128.const i8x16 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31))

rule Step_pure/vswizzle:
  (VCONST V128 c_1) (VCONST V128 c_2) (VSWIZZLE (pnn X N)) ~> (VCONST V128 c')
  -- var c : iN($lsize(pnn))
  -- if ci* = $lanes_(pnn X N, c_2)
  -- if c* = $lanes_(pnn X N, c_1) 0^(256 - N)
  -- if c' = $invlanes_(pnn X N, c*[$(ci*[k])]^(k<N))

The reason seems to be that usage of declared var as iteration from DSL is not elaborated correctly into il. Below code is elaborated version of reduction rule vswizzle:

  ;; spec/wasm-3.0/8-reduction.watsup:578.1-583.54
  rule vswizzle{c_1 : vec_(V128_vnn), c_2 : vec_(V128_vnn), pnn : pnn, N : N, c' : vec_(V128_vnn), c : iN($lsize((pnn : pnn <: lanetype))), ci* : lane_($lanetype(`%X%`((pnn : pnn <: lanetype), `%`(N))))*, k^N : nat^N}:
    `%~>%`([VCONST_admininstr(V128_vectype, c_1) VCONST_admininstr(V128_vectype, c_2) VSWIZZLE_admininstr(`%X%`((pnn : pnn <: imm), `%`(N)))], [VCONST_admininstr(V128_vectype, c')])
    -- if (ci*{ci : lane_($lanetype(`%X%`((pnn : pnn <: lanetype), `%`(N))))} = $lanes_(`%X%`((pnn : pnn <: lanetype), `%`(N)), c_2))
    -- if (c*{} = $lanes_(`%X%`((pnn : pnn <: lanetype), `%`(N)), c_1) :: `%`(0)^(256 - N){})
           ^^^^
    -- if (c' = $invlanes_(`%X%`((pnn : pnn <: lanetype), `%`(N)), c*{}[ci*{ci : lane_($lanetype(`%X%`((pnn : pnn <: lanetype), `%`(N))))}[k].`%`.0]^(k<N){k : nat}))

As seen here, c* is not set a proper iteration variable. Due to this, c* is evaluated to empty array to cause the failure.

It is elaborated properly without var declaration and 0^(256 - N) concatenation (which requires var declaration for type inference), as seen below, so usage of declared var as iteration should be the problem.

rule Step_pure/vswizzle:
  (VCONST V128 c_1) (VCONST V128 c_2) (VSWIZZLE (pnn X N)) ~> (VCONST V128 c')
  -- if ci* = $lanes_(pnn X N, c_2)
  -- if c* = $lanes_(pnn X N, c_1)
  -- if c' = $invlanes_(pnn X N, c*[$(ci*[k])]^(k<N))

  ;; spec/wasm-3.0/8-reduction.watsup:578.1-582.54
  rule vswizzle{c_1 : vec_(V128_vnn), c_2 : vec_(V128_vnn), pnn : pnn, N : N, c' : vec_(V128_vnn), ci* : lane_($lanetype(`%X%`((pnn : pnn <: lanetype), `%`(N))))*, c* : lane_($lanetype(`%X%`((pnn : pnn <: lanetype), `%`(N))))*, k^N : nat^N}:
    `%~>%`([VCONST_admininstr(V128_vectype, c_1) VCONST_admininstr(V128_vectype, c_2) VSWIZZLE_admininstr(`%X%`((pnn : pnn <: imm), `%`(N)))], [VCONST_admininstr(V128_vectype, c')])
    -- if (ci*{ci : lane_($lanetype(`%X%`((pnn : pnn <: lanetype), `%`(N))))} = $lanes_(`%X%`((pnn : pnn <: lanetype), `%`(N)), c_2))
    -- if (c*{c : lane_($lanetype(`%X%`((pnn : pnn <: lanetype), `%`(N))))} = $lanes_(`%X%`((pnn : pnn <: lanetype), `%`(N)), c_1))
    -- if (c' = $invlanes_(`%X%`((pnn : pnn <: lanetype), `%`(N)), c*{c : lane_($lanetype(`%X%`((pnn : pnn <: lanetype), `%`(N))))}[ci*{ci : lane_($lanetype(`%X%`((pnn : pnn <: lanetype), `%`(N))))}[k].`%`.0]^(k<N){k : nat}))

[rossberg]

Dimension inference probably assumes that c is a scalar variable. It will probably work if we wrap the var premise in (...)*, but the correct fix is that dimension inference should not take var declarations into account. I'll prepare a fix.

[rossberg]

Okay, I pushed a fix. That apparently fixed a bunch of tests, now at 99.14%.

Thanks for the find!