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

Add round_down_to_next_multiple_of_alignment #393

Merged
merged 1 commit into from
Sep 19, 2023
Merged

Conversation

joshlf
Copy link
Member

@joshlf joshlf commented Sep 18, 2023

This function implements the operation more efficiently using bitmasking instead of division and multiplication. While LLVM is probably smart enough in practice to produce this sort of code, Kani (#378) has trouble with multiplication, and so this code is hopefully more Kani-friendly.

Closes #390

@joshlf joshlf requested a review from jswrenn September 18, 2023 22:22
@jswrenn
Copy link
Collaborator

jswrenn commented Sep 18, 2023

Looks like the test is a little to much for miri to handle. Reduce the iterations, and I'll re-approve.

This function implements the operation more efficiently using bitmasking
instead of division and multiplication. While LLVM is probably smart
enough in practice to produce this sort of code, Kani (#378) has trouble
with multiplication, and so this code is hopefully more Kani-friendly.

Closes #390
@joshlf joshlf force-pushed the fast-round-down-align branch from b1d541f to fd82f80 Compare September 19, 2023 04:57
@joshlf joshlf merged commit da4c3cc into main Sep 19, 2023
@joshlf joshlf deleted the fast-round-down-align branch September 19, 2023 05:02
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

Successfully merging this pull request may close these issues.

Compute "round down to next multiple of alignment" more efficiently
2 participants