From 967c04de6c02bef349df579cddbfcac8cf262e6d Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 22 Mar 2022 16:03:57 +0100 Subject: 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 --- aarch64/Archi.v | 5 ++++- arm/Archi.v | 5 ++++- lib/Floats.v | 9 +++++++-- powerpc/Archi.v | 5 ++++- riscV/Archi.v | 5 ++++- x86_32/Archi.v | 6 ++++-- x86_64/Archi.v | 5 ++++- 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. -- cgit