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

1 files changed, 7 insertions, 2 deletions

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.