Simd: Extend `assert_return_arithmetic_nan` and `assert_return_canonical_nan` for SIMD types

[abrown]

WAST has directives to check that NaNs returned by tests have the correct bits: assert_return_arithmetic_nan and assert_return_canonical_nan. With the inclusion of SIMD instructions, these directives need to understand what type of vector is returned by a test to correctly check whether NaNs in the vector lanes are correct (e.g. an f32x4 filled with NaNs is different than an f64x2 filled with NaNs). There are two proposals out there for extending the directive:

• create new directives with the expected type appended to the name: e.g., (assert_return_arithmetic_nan_f32x4 (invoke ...))
• add an optional parameter to the directive: e.g., (assert_return_canonical_nan (invoke ...) f64x2)

I am raising the issue here to solicit comments before the SIMD spec tests are merged that require this feature. @Honry has worked on this in https://github.com/WAVM/WAVM/issues/187 (see discusison by @AndrewScheidecker and @rossberg) and I have a PR ready to merge in https://github.com/bytecodealliance/wat/pull/24. Please tag whoever else might have an opinion on the issue.

[tlively]

I maintain that a type suffix on the assertion name itself makes most sense.

From @rossberg in https://github.com/WAVM/WAVM/issues/187#issuecomment-530707233:

In fact, the syntax should probably be

(assert_return_*_nan (...) f64x2)

to match the style of other assertions, where the specification of the result always goes last.

Other assert_return_*_nan assertions do not have results in the way assert_return assertions do, and that is true for their SIMD versions as well. For existing NaN assertions, the disjunction is baked into the assertion itself and not its arguments. The most consistent way to handle SIMD NaN assertions is therefore to create a new assertion for each disjunction of acceptable results, and that means baking the lane interpretation into the assertion name. This is exactly how we would name a collection of similar instructions as well. v128.const is a special case in that it is a single instruction with multiple text representations, whereas the SIMD NaN assertions are all semantically different.

Also I find that having the lane interpretation in the assertion name is more readable, but that doesn't seem worth arguing about since no one is going to change their mind over aesthetics.

[penzn]

This is going to be interpreter-only change for us, I believe. I have started on the interpreter in #138, still a long way to go. @tlively, @dtig, @arunetm can we tag this issue with something like "test" or "interpreter"?

[abrown]

The most consistent way to handle SIMD NaN assertions is therefore to create a new assertion for each disjunction of acceptable results

If I follow that correctly, then the other side of this argument is to move all of the distinguishing elements into the parameter list, like assert_return (...) canonical_nan_f64x2), effectively merging this directive under the assert_return directive. Looking at it now, that is actually what I would expect as the spec test writer (but maybe that is just me). @rossberg, any opinions since you last posted about this in https://github.com/WAVM/WAVM/issues/187#issuecomment-530707233?

[tlively]

@abrown I like that idea, but I wouldn't want to apply it to only SIMD asserts when we have a different convention for scalar asserts.

[abrown]

Ah, yeah; and perhaps it makes sense to keep it separate from assert_return. What about something like assert_return_nan (...) [nan type] [value type] where nan type can be one of canonical | arithmetic and value type can be one of f32 | f64 | f32x4 | f64x2?

[abrown]

That would seem to fit well with assert_return and assert_return_func and, importantly for me 😄, I can see a clear path to implement it in https://github.com/bytecodealliance/wat/pull/24.

[rossberg]

Interesting! I like the idea. Let's go further even, since the growing number of special variants of assert_return has already bothered me and does not really mesh with multiple returns either. It would be simpler and more consistent to refactor and unify all these assertions in assert_return with an enriched grammar for describing classes of individual result values. For example, something along the lines of

result ::= const | (t.arithmetic_nan fsimd?) | (t.canonical_nan fsimd?) | (ref.any) | (ref.func)
fsimd ::= f32x4 | f64x2

where fsimd must be present if t is v128.

[tlively]

SGTM. Would it be a problem to perform this refactoring across the existing test suite?

[rossberg]

Don't think so. The main bulk of the work would be the nan returns in the main spec repo. But they're concentrated in a few files and can be handled by a regexp.

Tools need to be adapted, though. How many tools are there now that consume .wast files?

[tlively]

I know Binaryen and WABT both have interpreters for running spec tests. My impression is that most engines also run spec tests. But updating the spec repo will only cause major headaches for projects that automatically pull in the tip-of-tree test suite, and I know that neither Binaryen nor WABT do that, so this change should be manageable at least for those two projects. I don't know about engines.

[abrown]

@tlively, @rossberg: I started to implement this in #142 and posted some questions there that I would appreciate feedback on. It is in a very early stage and I'm not familiar at all with the interpreter code so feel free to make sweeping suggestions.

[rossberg]

Thinking about this further, I think even my suggestion above is still not exactly right. For SIMD, you actually want to be able to specify NaNs per lane, e.g., to express the result of a div instruction that only has NaN in some of the lanes.

So the syntax for results should be a kind of "pattern" for values:

result ::= (t.const tsimd? litpat*) | (ref.any) | (ref.func)
tsimd ::= f32x4 | f64x2 | ...
litpat ::= literal | nan:canonical | nan:arithmetic

Here, litpat extends the syntax of literals in const instructions with additional patterns that extend the existing nan-with-payload syntax. This could be extended to other non-deterministic value classes.

With this you could e.g. write

(assert_return
  (invoke "f64x2.div" (v128.const f64x2 0 0) (v128.const f64x2 0 1))
  (v128.const f64x2 nan:arithmetic 0)
)

[tlively]

I like this scheme, but if there is an appetite for something simpler, extract_lane instructions could still be used for asserts with heterogeneous lanes.

[rossberg]

@tlively, fair enough, though of course, that would be arguing against extending assert_return_*_nan to SIMD in the first place. ;)

[tlively]

Not necessarily. Back on the original thread about this we had decided to use new SIMD asserts for homogeneous vectors and extract_lanes for heterogeneous vectors, because it wasn’t worth complicating the asserts to handle heterogeneous vectors themselves.

[abrown]

I think this is closed by https://github.com/WebAssembly/spec/pull/1104.