Reinterpretation of NaNs does not follow the reference implementation

[agustinmista]

Hi!

I noticed that your implementation doesn't follow the reference one when it comes to reinterpreting NaNs.

Here is a small example:

m = Module 
  { types = [ FuncType {params = [], results = [I32]} ]
  , functions = [ 
      Function {  funcType = 0, localTypes = [I32], body = [
        F32Const (-1.0),
        FUnOp BS32 FSqrt,
        IReinterpretF BS32
    ]}]
  , tables = []
  , mems = []
  , globals = []
  , elems = []
  , datas = []
  , start = Nothing
  , imports = []
  , exports = [ Export {name = "foo", desc = ExportFunc 0} ]
}

After validation and instantiation, invoking "foo" using the Haskell interpreter returns [VI32 4290772992], whereas the reference implementation returns something else:

ghci> ByteString.writeFile "foo.wasm" (dumpModule m)
Leaving GHCi.
$ ./wasm foo.wasm -e '(invoke "foo")'
2_143_289_344 : i32

Now, according to the WebAssembly specification, reinterpreting NaNs is meant to be non-deterministic. However, since your implementation seems to follow the reference implementation quite closely, it is not clear whether this is a bug in haskell-wasm or if this behavior still lies under the specification.

In principle, I see no reason for not following the reference implementation as much as possible, but you might have a different point of view. Would you mind to clarify this?

Thanks!

/Agustín

[SPY]

Hi @agustinmista Thank you for a nice question. I enjoyed a journey into the spec interpreter codebase to find an answer and I'm ready to share some thoughts about it. First let's figure out why we see 2_143_289_344 as result in the spec interpreter case. Instead of using bare system functions for numeric operations with float number the spec interpreter defines wrappers. As a representation for F32 OCaml's built-in type Int32 is used with positive nan equals to 0x7fc0_0000l(or 2_143_289_344 in dec). Then lets look on sqrt op. It calls native sqrt on -1.0f and result is negative NaN(you could check by try in OCaml repl Int32.bits_of_float (Float.sqrt (-1.0));;. Result is -4194304l. It is 0xFFC00000 in hex). But instead of returning result as negative nan and store it as -4194304l unary wrapper checks if result is nan, and if it is it calls determine_unary_nan with initial argument (-1.0f in our case). If argument was NaN determine_unary_nan returns it as is, but as soon as it is not, it returns pos_nan or 2_143_289_344 for F32.

Second, lets look at Haskell implementation. It uses native Float as storage representation and honestly store result of native sqrt function. It returns -NaN or 0xFFC00000(4_290_772_992) in binary interpretation.

Now, when we understand why we have such results lets try to suppose why the spec interpreter chose this way of handling NaNs. My theory is to easer check for NaN equality in tests. In case of the spec interpreter is simple binary equality check. To support similar behaviour in haskell-wasm interpreter I had to implement NaN-independent equality check for float numbers.

Conclusions. I believe my approach is closer to the real world implementations(and if you check V8 you will see the same behaviour). I don't think compatibility with the spec interpreter in this aspect deserve efforts in this particular case.

[agustinmista]

Hi @SPY,

Thanks a lot for the detailed answer, IEEE754 is indeed a can of worms. I find it a bit sad to have a nice little language like WebAssembly being tainted by this source of non-determinism. For my particular purposes, differential testing across different implementations becomes unnecessarily complicated as there's not a single correct answer for some programs :(

I don't think compatibility with the spec interpreter in this aspect deserve efforts in this particular case.

This is a fair conclusion. I would add a comment in the documentation to make it explicit, though.

/Agustín