Skip to content
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

Builtin memcpy in riscV target uses fld/fsd #501

Closed
xxuejie opened this issue Aug 4, 2023 · 3 comments
Closed

Builtin memcpy in riscV target uses fld/fsd #501

xxuejie opened this issue Aug 4, 2023 · 3 comments

Comments

@xxuejie
Copy link

xxuejie commented Aug 4, 2023

Hi,

I was trying to use CompCert on a RISC-V implementation that does not provide floating point operation support. While most of the codegen part is okay when we avoid floating operations in C, the current builtin memcpy still uses fld/fsd.

However, it does seem to me that we can eliminate those operations by using ld/sd directly, we also have the register X31 here as a temporary register(it is used for lw/sw, lh/sh, lb/sb anyway). I've put together a patch which works well in my environment, tho I still want to check here first: is there any particular reason we are using fld/fsd here? Or can we change them to ld/sd so CompCert can still work (mostly) without floating point support?

@xavierleroy
Copy link
Contributor

The only reason for using fld/fsd (64-bit FP loads and stores) in memcpy is that it transfers 8 bytes in one instruction even if we're on a RISC-V 32-bit machine, which lacks the ld/sd instructions But you're right that on a 64-bit RISC-V, ld/sd works just as well.

Also, the PowerPC and x86 ports avoid generating FP instructions for memcpy if the -fno-fpu flag is given. The RISC-V port should also honor this flag. I'll look into this shortly.

@xavierleroy
Copy link
Contributor

This should be fixed by 35feefd . For 64-bit RISC-V, memcpy now uses X31, like in your patch. For 32-bit RISC-V, a FP register is used unless -fno-fpu is given, in which case the copy is done through X31 by chunks of at most 32 bits.

@xxuejie
Copy link
Author

xxuejie commented Aug 4, 2023

Thank you for the super fast fix! I totally neglected the 32 bit case :) The change deployed to address the issue here is perfect.

josuemoreau pushed a commit to josuemoreau/ModifsCompCert that referenced this issue Oct 26, 2023
They should not be used if -fno-fpu is given, as in the PowerPC and x86 ports.

Moreover, if we're on a 64-bit RISC-V, we can use a 64-bit integer register
instead.

Fixes: AbsInt#501
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants