diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2022-03-22 16:03:57 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-04-25 16:34:11 +0200 |
| commit | 967c04de6c02bef349df579cddbfcac8cf262e6d (patch) | |
| tree | 65be52a638e7f7ff559ea90a4111da0278b032bf /riscV | |
| parent | 9d3521b4db46773239a2c5f9f6970de826075508 (diff) | |
| download | compcert-967c04de6c02bef349df579cddbfcac8cf262e6d.tar.gz compcert-967c04de6c02bef349df579cddbfcac8cf262e6d.zip | |
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
Diffstat (limited to 'riscV')
| -rw-r--r-- | riscV/Archi.v | 5 |
1 files changed, 4 insertions, 1 deletions
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 *) |