Introduce float_conversion_default_nan parameter for float-float conversions

For RISC-V we need to return the canonical NaN value if the argument of
a float32->float64 or float64->float32 conversion is any NaN.
This is in line with 11.3 from the RISC-V manual, the description of
the conversion operations as well as what the spike ISA simulator and
qemu do.

Other platforms convert the NaN payload (by truncation or expansion)
in float32->float64 and float64->float32 conversions.

Fixes: #428

7 files changed, 31 insertions, 9 deletions

diff --git a/aarch64/Archi.v b/aarch64/Archi.v
index 4911db73..e1809aba 100644
--- a/aarch64/Archi.v
+++ b/aarch64/Archi.v
@@ -80,11 +80,14 @@ Definition fma_invalid_mul_is_nan := true.
 
 Definition float_of_single_preserves_sNaN := false.
 
+Definition float_conversion_default_nan := false.
+
 Global Opaque ptr64 big_endian splitlong
               default_nan_64 choose_nan_64
               default_nan_32 choose_nan_32
               fma_order fma_invalid_mul_is_nan
-              float_of_single_preserves_sNaN.
+              float_of_single_preserves_sNaN
+              float_conversion_default_nan.
 
 (** Which ABI to implement *)
 
diff --git a/arm/Archi.v b/arm/Archi.v
index c4cb5496..a17ce79b 100644
--- a/arm/Archi.v
+++ b/arm/Archi.v
@@ -81,11 +81,14 @@ Definition fma_invalid_mul_is_nan := true.
 
 Definition float_of_single_preserves_sNaN := false.
 
+Definition float_conversion_default_nan := false.
+
 Global Opaque ptr64 big_endian splitlong
               default_nan_64 choose_nan_64
               default_nan_32 choose_nan_32
               fma_order fma_invalid_mul_is_nan
-              float_of_single_preserves_sNaN.
+              float_of_single_preserves_sNaN
+              float_conversion_default_nan.
 
 (** Which ABI to use: either the standard ARM EABI with floats passed
   in integer registers, or the "hardfloat" variant of the EABI
diff --git a/lib/Floats.v b/lib/Floats.v
index 43caebb0..fd0a3d32 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -174,7 +174,9 @@ Definition expand_nan s p H : {x | is_nan _ _ x = true} :=
 Definition of_single_nan (f : float32) : { x : float | is_nan _ _ x = true } :=
   match f with
   | B754_nan s p H =>
-    if Archi.float_of_single_preserves_sNaN
+    if Archi.float_conversion_default_nan
+    then default_nan_64
+    else if Archi.float_of_single_preserves_sNaN
     then expand_nan s p H
     else quiet_nan_64 (s, expand_nan_payload p)
   | _ => default_nan_64
@@ -189,7 +191,10 @@ Definition reduce_nan_payload (p: positive) :=
 
 Definition to_single_nan (f : float) : { x : float32 | is_nan _ _ x = true } :=
   match f with
-  | B754_nan s p H => quiet_nan_32 (s, reduce_nan_payload p)
+  | B754_nan s p H =>
+    if Archi.float_conversion_default_nan
+    then default_nan_32
+    else quiet_nan_32 (s, reduce_nan_payload p)
   | _ => default_nan_32
   end.
 
diff --git a/powerpc/Archi.v b/powerpc/Archi.v
index 28859051..9dede4c7 100644
--- a/powerpc/Archi.v
+++ b/powerpc/Archi.v
@@ -66,8 +66,11 @@ Definition fma_invalid_mul_is_nan := false.
 
 Definition float_of_single_preserves_sNaN := true.
 
+Definition float_conversion_default_nan := false.
+
 Global Opaque ptr64 big_endian splitlong
               default_nan_64 choose_nan_64
               default_nan_32 choose_nan_32
               fma_order fma_invalid_mul_is_nan
-              float_of_single_preserves_sNaN.
+              float_of_single_preserves_sNaN
+              float_conversion_default_nan.
diff --git a/riscV/Archi.v b/riscV/Archi.v
index 9e561ca8..e33c3e84 100644
--- a/riscV/Archi.v
+++ b/riscV/Archi.v
@@ -63,11 +63,14 @@ Definition fma_invalid_mul_is_nan := false.
 
 Definition float_of_single_preserves_sNaN := false.
 
+Definition float_conversion_default_nan := true.
+
 Global Opaque ptr64 big_endian splitlong
               default_nan_64 choose_nan_64
               default_nan_32 choose_nan_32
               fma_order fma_invalid_mul_is_nan
-              float_of_single_preserves_sNaN.
+              float_of_single_preserves_sNaN
+              float_conversion_default_nan.
 
 (** Whether to generate position-independent code or not *)
 
diff --git a/x86_32/Archi.v b/x86_32/Archi.v
index 0a7f365b..775bdd44 100644
--- a/x86_32/Archi.v
+++ b/x86_32/Archi.v
@@ -59,6 +59,8 @@ Definition fma_invalid_mul_is_nan := false.
 
 Definition float_of_single_preserves_sNaN := false.
 
+Definition float_conversion_default_nan := false.
+
 (** Which ABI to use. *)
 Parameter win64: bool.   (* Always false in 32 bits *)
 
@@ -66,5 +68,5 @@ Global Opaque ptr64 big_endian splitlong
               default_nan_64 choose_nan_64
               default_nan_32 choose_nan_32
               fma_order fma_invalid_mul_is_nan
-              float_of_single_preserves_sNaN.
-
+              float_of_single_preserves_sNaN
+              float_conversion_default_nan.
diff --git a/x86_64/Archi.v b/x86_64/Archi.v
index ed6dc317..9df30c88 100644
--- a/x86_64/Archi.v
+++ b/x86_64/Archi.v
@@ -59,6 +59,8 @@ Definition fma_invalid_mul_is_nan := false.
 
 Definition float_of_single_preserves_sNaN := false.
 
+Definition float_conversion_default_nan := false.
+
 (** Which ABI to use. *)
 Parameter win64: bool.
 
@@ -66,4 +68,5 @@ Global Opaque ptr64 big_endian splitlong
               default_nan_64 choose_nan_64
               default_nan_32 choose_nan_32
               fma_order fma_invalid_mul_is_nan
-              float_of_single_preserves_sNaN.
+              float_of_single_preserves_sNaN
+              float_conversion_default_nan.