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

LLVM backend: Compute size_t instead of hardcoded 64-bit #1959

Open
bollu opened this issue Dec 16, 2022 · 0 comments
Open

LLVM backend: Compute size_t instead of hardcoded 64-bit #1959

bollu opened this issue Dec 16, 2022 · 0 comments
Milestone

Comments

@bollu
Copy link
Contributor

bollu commented Dec 16, 2022

The LLVM backend (#1837) currently assumes that size_t is 64bit. I believe the correct way to do this is to:

  1. Create a notion of target architecture in Lean (to support cross compilation)
  2. Load the information about the target architecture, using LLVMCreateTargetData
  3. Use LLVMPointerSize to get the number of bytes. We should then use the corresponding i(<number_of_bytes>*8) type instead of assuming i64 everywhere.
@Kha Kha added this to the LLVM MVP milestone Dec 16, 2022
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