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

Split large memory accesses in stack alloc #741

Open
wants to merge 2 commits into
base: main
Choose a base branch
from

Conversation

sarranz
Copy link
Collaborator

@sarranz sarranz commented Feb 28, 2024

When stack allocation replaces x = e by [rsp + off] = e, the offset may be too large. I introduced a check at every Copn that splits this memory access into several instructions in ARM. I also added a warning. Note that when x is an array set, this can be fixed manually with reg ptrs, but if it's a variable there's no way of doing so (but this scenario is probably far-fetched).

@eponier
Copy link
Contributor

eponier commented Feb 28, 2024

opam strikes back. You used a feature (symmetry of disequality) that is not available before Coq 8.18 (cf. coq/coq#17025), and opam tests 8.16. The stupid fix is to call a lemma instead of symmetry, but maybe it is time to increase the lowest supported version to 8.18?

@sarranz
Copy link
Collaborator Author

sarranz commented Feb 29, 2024

I will use the lemma, thanks!

bgregoir
bgregoir previously approved these changes Mar 13, 2024
Copy link
Contributor

@bgregoir bgregoir left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I strongly suspect that we will have to wrote the same code for risc-V.
So maybe we should take the time to make the code a little bit more modular.

then Some (UseLea, "LEA instruction is used")
else None
| Split_memory_access ->
let msg =
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you add an option like it is done with Glob_options.lea, to say if we print the warning or not ?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Would this flag control the warning only or whether we split accesses as well?

@bgregoir bgregoir marked this pull request as draft March 20, 2024 12:11
@vbgl vbgl added the arm Related to the arm port label May 29, 2024
@sarranz sarranz marked this pull request as ready for review October 7, 2024 21:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
arm Related to the arm port
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants