Fix various SIMD constraints

[rossberg]

This PR adds various syntactic constraints on SIMD operators that were still missing. However, I ran into strange behaviour with the interpreter now failing some tests.

I added some extra checks in the interpreter backend to get a proper error and now have:

3-numerics.watsup:210.41-210.56: interpreter error: invlanes_: inverse_of
_lanes: [(F32, 0x4), [(POS (SUBNORM 0x0)), (POS (SUBNORM 0x0)), (POS (SUBN
ORM 0x0)), (POS (SUBNORM 0x0)), (POS (SUBNORM 0x0)), (POS (SUBNORM 0x0)), 
(POS (SUBNORM 0x0)), (POS (SUBNORM 0x0))]] (interpreting LetI (VarE (vc), 
CallE (inverse_of_lanes_, [ VarE (sh), IterE (VarE (c), [c], *) ])))

Apparently, this is while executing the test

(assert_return (invoke "f32x4.convert_i32x4_s" (v128.const i32x4 0 0 0 0))
                                               (v128.const f32x4 0.0 0.0 0.0 0.0))

at simd_conversions.wast:182, which invokes the simple function

  (func (export "f32x4.convert_i32x4_s") (param v128) (result v128)
    (f32x4.convert_i32x4_s (local.get 0)))

Something appears to go wrong with the interpretation of the reduction rules for VCVTOP. The prose for execution looks okay to me:

+execution_of_VCVTOP (lanet_u5 X n_u0) (lanet_u6 X n_u1) vcvtop half__u4? sx? zero__u13?
 1. Assert: Due to validation, a value is on the top of the stack.
 2. Pop the value (V128.CONST c_1) from the stack.
+3. If (half__u4? is not defined and zero__u13? is not defined), then:
+  a. Let Lnn_1 be lanet_u6.
+  b. Let Lnn_2 be lanet_u5.
+  c. Let M be n_u1.
+  d. If (n_u0 is M), then:
+    1) Let c'* be $lanes_((Lnn_1 X M), c_1).
+    2) Let c be $invlanes_((Lnn_2 X M), $vcvtop((Lnn_1 X M), (Lnn_2 X M), vcvtop, sx?, c')*).
+    3) Push the value (V128.CONST c) to the stack.
+4. If zero__u13? is not defined, then:
+  a. Let Lnn_1 be lanet_u6.
+  b. Let Lnn_2 be lanet_u5.
+  c. Let M_1 be n_u1.
+  d. Let M_2 be n_u0.
+  e. If half__u4? is defined, then:
+    1) Let ?(half) be half__u4?.
+    2) Let ci* be $lanes_((Lnn_1 X M_1), c_1)[$half((Lnn_1 X M_1), (Lnn_2 X M_2), half, 0, M_2) : M_2].
+    3) Let c be $invlanes_((Lnn_2 X M_2), $vcvtop((Lnn_1 X M_1), (Lnn_2 X M_2), vcvtop, sx?, ci)*).
     4) Push the value (V128.CONST c) to the stack.
+5. If half__u4? is not defined, then:
+  a. Let M_1 be n_u1.
+  b. Let M_2 be n_u0.
+  c. If the type of lanet_u6 is numtype, then:
+    1) Let nt_1 be lanet_u6.
+    2) If the type of lanet_u5 is numtype, then:
+      a) Let nt_2 be lanet_u5.
+      b) Let ci* be $lanes_((nt_1 X M_1), c_1).
+      c) Let c be $invlanes_((nt_2 X M_2), $vcvtop((nt_1 X M_1), (nt_2 X M_2), vcvtop, sx?, ci)* ++ $zero(nt_2)^M_1).
+      d) Push the value (V128.CONST c) to the stack.

But when interpreting the above instruction, it somehow seems to fall through to step 5. I don't understand why.

@ShinWonho, @f52985, any idea?

[f52985]

Here is the original condition for line 5:

5. If (half__u0? is not defined and ((zero__u7? is ?(ZERO)) and the type of lanet_u2 is numtype)), then:

and the main difference seems to be the absence of the condition zero__u7? is ?(ZERO). Due to this absence, the execution seems to fall through step 5 even if it should not.

The real question though, is "why that condition disappeared". One thing I noticed is that the reduction rule originally used upper case ZERO, while the new reduction rule uses lower case zero. That may have confused the translation I guess. I'll try looking into it more deeper.

[rossberg]

One thing I don't understand: why are these actually independent if-conditions, and not else-if branches? At most one of the original reduction rules can apply, so shouldn't they be translated into mutually exclusive code paths?

[f52985]

The main reason was that there are some cases where:

the prose for first reduction rule looks like:

1. If A, then:
  a. If B, then:
    ...

and the prose for second reduction rule looks like:

1. If A, then:
  a. If C, then:
    ...

Inserting the second prose as the else-branch of the top level if-branch for first prose would make a wrong prose, and coming up with a correct, general mechanism (that can automatically inserts the else-branch into the second-level if branch for this case) was be a bit challenging.

Instead, it was implemented as the simple concatenation of independent if-branches for now, since it should generate correct prose anyway, under the assumption that each reduction rules are mutually exclusive.

[rossberg]

I see. But that seems quite problematic, because it now requires negating and spelling out all previous (implicit & explicit) conditions for every consecutive case, which is brittle and makes the prose more verbose and less faithful to the formal rules — one goal of the spec was to keep them as close as possible.

Do you have an example of the scenario you describe? How often does that come up?

[f52985]

Do you have an example of the scenario you describe? How often does that come up?

I think it was related to an automatically inferred side condition, though I can't recall the exact scenario. I believe that happened quite rarely anyway, so I would try making every branches as else-branches, see if there's any problem with that, and see if I can handle that.

[f52985]

By the way, it seems that the current reductions rules for VCVTOP is indeed, non-mutually exclusive.

This is the parsed IL for the previous version:

VCVTOP_instr(
  `%X%`_shape((nt_2 : numtype <: lanetype),`%`_dim(N_2)),
  `%X%`_shape((nt_1 : numtype <: lanetype),`%`_dim(N_1)),
  vcvtop,
  ?(),
  sx?{sx : sx},
  ?(ZERO_zero_)
)

and here is the parsed IL for the new version:

VCVTOP_instr(
  `%X%`_shape((nt_2 : numtype <: lanetype), `%`_dim(M_2)),
  `%X%`_shape((nt_1 : numtype <: lanetype), `%`_dim(M_1)),
  vcvtop,
  ?(),
  sx?{sx : sx},
  zero
)

The main difference is the last argument (which has type zero?). The previous version explicitly uses ?(...) to indicate that it should be defined, while the new version uses a simple variable zero, meaning both defined and undefined option value can be matched.

(And if the prose-generation was "perfect", these rules should be translated as a prose containing Either:, ... which is certainly out of the scope, I believe)

So, the fundamental reason for test failure seems to be the non-deterministic reduction rules.

Whether the prose uses else-branch or not seems to be an orthogonal issue. (And considering this case, perhaps it rather makes sense NOT to insert the else-branches, so that non-deterministic rules can be detected?)

[rossberg]

That's an excellent point. The intuition was that a meta variable never has an iterated type by itself (so that we have to write x? or x*), which arguably is what one would expect given this notation. But the elaborator happily inferred iterated types, so indeed the rules were interpreted as overlapping. I changed it to not do that, and after that, these are now correctly recognised as singletons and the tests pass again. That also produced more natural translations for various other rules (see commit) and uncovered a bug where I still used epsilon instead of eps. :)

Thanks for the help! That unblocks this PR. I'm still uneasy about not using else-branches (which is closely related to the assumption of full coverage and turning the last condition into an assertion that we discussed last week — I don't think that even works without if-else), but we can resolve that separately.