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

Allow crucible_alloc_aligned to specify less alignment than default for type #647

Closed
brianhuffman opened this issue Feb 10, 2020 · 0 comments · Fixed by #648
Closed

Allow crucible_alloc_aligned to specify less alignment than default for type #647

brianhuffman opened this issue Feb 10, 2020 · 0 comments · Fixed by #648
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm

Comments

@brianhuffman
Copy link
Contributor

Currently crucible_alloc_aligned can only be used to specify a stronger alignment constraint than the default alignment for the type of the memory region. For example, a pointer to i32 has a default alignment of 4 bytes; crucible_alloc_aligned can be used to specify a stronger 8-byte alignment, but trying to specify an i32 pointer with 1- or 2-byte alignment will yield an error message.

We should relax this check, and allow things like crucible_alloc_aligned 1 i32 to specify a pointer to 32-bit integer with only 1-byte alignment.

LLVM allows us to write functions using unaligned read and write instructions. For example, we can have a function that takes an argument pointer of type i32* and then uses it with load statements that only assert 1-byte alignment (which might compile to special unaligned-read instructions on some architectures). Relaxing the minimum alignment check allows us to write accurate SAW specifications of such functions.

@langston-barrett langston-barrett added the subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm label Feb 10, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm
Projects
None yet
Development

Successfully merging a pull request may close this issue.

2 participants