64-bit floating point arithmetic fails on 32-bit machines

[IgnoredAmbience]

tests/test262/ch08/8.5/S8.5_A2.1.js
tests/test262/ch08/8.5/S8.5_A2.2.js

These tests were passing the nightlies up until Jul 12th 2013, when gds swapped the nightly test run onto a 32 bit machine.
This results in the discrepancy between 1796 test passes as reported by us in popl14 and the reproduction run of the tagged version popl14-results (1798 test passes).

[IgnoredAmbience]

Hmm, maybe not platform.
The OCaml language manual states:

Floating-point values are numbers in floating-point representation. The current implementation uses double-precision floating-point numbers conforming to the IEEE 754 standard, with 53 bits of mantissa and an exponent ranging from −1022 to 1023.

But, all OCaml versions since 3.07 have had this specified...

[IgnoredAmbience]

Progress! It's an x87 FPU bug, that OCaml helpfully dumps on us.
See http://www.vinc17.org/research/extended.en.html

[IgnoredAmbience]

OCaml doesn't support use of alternative FPU (SSE2) on x86, it only uses it for x64.
This bug probably doesn't affect Macs of either architecture.

The best solution for now is probably to explicitly not support JSCert under x86 Linux.

[IgnoredAmbience]

Reopening as we can probably do better than this -- does flocq give an extractable ieee754 implementation? It does highlight the assumption that ocaml confirms to its specification and that the CPU also does!

[IgnoredAmbience]

Content from gforge bug: https://gforge.inria.fr/tracker/index.php?func=detail&aid=16179&group_id=4179&atid=13867

Alan> tests/test262/ch08/8.5/S8.5_A2.1.js and
tests/test262/ch08/8.5/S8.5_A2.2.js are strange, they pass here.
Machine architecture?
gds> Did you ask that on Friday too? [10:45]
Alan> yes
gds> Possibly machine architecture then.
Alan> you told me it passed on your laptop
gds> They did...
gds> But I'm running the nightlies on a different machine.

[brabalan]

@edgemaster : regarding flocq extraction, I asked Xavier Leroy a while back about this (as they have the same issue with CompCert), here is what he said (in French, I can translate if necessary:

J'ai cru comprendre que vous utilisiez Flocq dans CompCert et que
pouviez faire de l'extraction. J'aimerais rendre plus robuste
l'extraction de flottants dans JSCert, et je me demande donc si votre
code est disponible.

Oui, tout à fait. À la base, il y a Flocq qui fait tout le boulot
difficile (http://flocq.gforge.inria.fr/ + une version intégrée dans
la distrib CompCert, les deux versions étant maintenues à peu près en
synchro).

Au dessus, une fine surcouche dans CompCert (module lib/Floats.v de la
distrib, http://compcert.inria.fr/doc/html/Floats.html) qui donne des
fonctions Coq calculables et "extractibles" pour:

• les opérations de base sur les flottants (arithmétique, conversions,
  comparaisons);
• encodage et décodage des flottants en vecteurs de bits
  (représentation en mémoire);
• de quoi calculer la valeur d'un littéral flottant à partir de
  sa représentation après parsing (base, mantisse entière, exposant).

Enfin, dans lib/Camlcoq.ml, il y a deux fonctions
coqfloat_of_camlfloat et camlfloat_of_coqfloat pour convertir entre
les flottants Flocq et les flottants "natifs" d'OCaml, si besoin est.

Tout cela est dispo sous double licence non-commerciale + GPL, donc
c'est librement réutilisable.

[IgnoredAmbience]

Paper on the previous: http://gallium.inria.fr/~xleroy/bibrefs/Boldo-Jourdan-Leroy-Melquiond-JAR.html