-
Notifications
You must be signed in to change notification settings - Fork 225
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Some NaN issues for RISCV-64 #428
Comments
The test was probably written before
The last time I checked, QEMU did not emulate the NaN payloads of the emulated architecture, and produced the NaN payloads of the processor running QEMU instead. (It makes sense, as NaN emulation adds run-time costs and is rarely useful.) That's why I'd rather test on real hardware. However, I don't have access to a RISC-V machine right now.
That's a plausible reading of the RISC-V specs. In this respect, it would behaves differently from the other architectures supported by CompCert. This could certainly be accommodated in CompCert's formalization, at the cost of some code duplication. However I'd like to observe what real hardware does first. |
I was able to run a smaller version of the test on a SiFive Freedom U740 SoC. The snippet of relevant C is this:
compiled with
However, when run with compcert's interpreter, we get
|
Thanks for the testing and the confirmation. (I wish I had access to real RISC-V hardware, but so far every product from SiFive has been either unavailable or unreliable.) A fix is already in AbsInt's version of CompCert, and I'll backport it to the public version shortly. |
Should be fixed by commit 967c04d . Thanks again for all the feedback. |
Calling wrong absolute value for single-precision float in regression
While I was running CompCert's test suite for RISCV-64, I noticed a few
discrepancies between QEMU emulation and CompCert's interpreter. Here
are the differences from running the following:
Gives
As it turns out, right here
CompCert/test/regression/NaNs.c
Line 92 in 9d3521b
the regression test calls
__builtin_fabs
on a single-precision floatwhen I think the desire was for
__builtin_fabsf
. As it currently iswritten, the assembly generated is:
However, what I think we want is just the
fabs.s f10 f10
, which iswhat is generated if you change Line 92 to
__builtin_fabsf
.Making this changes fixes some issues but not others, specifically
Conversion between float and double
However, these still do not match up. According to the IEEE 754-2019
standard, they are both valid treatments of NaNs. However, CompCert in
these conversion cases does propagate the sign and payload of NaNs
whereas QEMU always returns the canonical NaN (note that RISCV describes
a "canonical" NaN much more strictly than the IEEE 754 standard. For
IEEE 754, any NaN in binary format is canonical, the definition only
applies to decimal floats. For RISC-V,
I couldn't find any reference that denotes "otherwise noted" to apply to
floating-point conversions, specifically
FCVT.S.D
andFCVT.D.S
. Theonly ones which specify NaN propagation are the various loads, stores,
sign injections (
FSGN*
,FL*
,FS*
,FMV.*
,FLW
, andFSW
, to beprecise).
What's the Point?
I believe that CompCert's handling of FCVT.S.D. and FCVT.D.S. are
incorrect. If I'm interpreting the RISC-V standard correctly, if passed
in a NaN they should return the canonical NaN.
Versions
OS: Ubuntu 20.04,
Linux 23dc8915bd86 3.10.0-1160.42.2.el7.x86_64 #1 SMP Tue Aug 31 20:15:00 UTC 2021 x86_64 x86_64 x86_64 GNU/Linux
The most recent compcert version, commit 9d3521b
Configured with
./configure rv64-linux -toolprefix riscv64-linux-gnu- -clightgen
QEMU: qemu-riscv64 version 6.2.90 (v7.0.0-rc0-8-g1d60bb4b14)
GCC: riscv64-linux-gnu-gcc (Ubuntu 9.3.0-17ubuntu1~20.04) 9.3.0
The text was updated successfully, but these errors were encountered: