Skip to content

Commit b1d541f

Browse files
committed
Add round_down_to_next_multiple_of_alignment
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
1 parent f192b86 commit b1d541f

File tree

2 files changed

+46
-12
lines changed

2 files changed

+46
-12
lines changed

src/lib.rs

Lines changed: 2 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -484,21 +484,12 @@ impl DstLayout {
484484
(0, size)
485485
}
486486
SizeInfo::SliceDst(TrailingSliceLayout { _offset: offset, _elem_size: elem_size }) => {
487-
let align = self._align.get();
488-
489487
// Calculate the maximum number of bytes that could be consumed
490488
// - any number of bytes larger than this will either not be a
491489
// multiple of the alignment, or will be larger than
492490
// `bytes_len`.
493-
//
494-
// Guaranteed not to:
495-
// - divide by zero: `align` is non-zero.
496-
// - overflow on multiplication: `usize::MAX >= bytes_len >=
497-
// (bytes_len / align) * align`
498-
//
499-
// TODO(#390): Compute this more efficiently.
500-
#[allow(clippy::arithmetic_side_effects)]
501-
let max_total_bytes = (bytes_len / align) * align;
491+
let max_total_bytes =
492+
util::_round_down_to_next_multiple_of_alignment(bytes_len, self._align);
502493
// Calculate the maximum number of bytes that could be consumed
503494
// by the trailing slice.
504495
//

src/util.rs

Lines changed: 44 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
#[path = "third_party/rust/layout.rs"]
66
pub(crate) mod core_layout;
77

8-
use core::mem;
8+
use core::{mem, num::NonZeroUsize};
99

1010
pub(crate) trait AsAddress {
1111
fn addr(self) -> usize;
@@ -56,6 +56,27 @@ pub(crate) fn aligned_to<T: AsAddress, U>(t: T) -> bool {
5656
remainder == 0
5757
}
5858

59+
/// Round `n` down to the largest value `m` such that `m <= n` and `m % align ==
60+
/// 0`.
61+
///
62+
/// # Panics
63+
///
64+
/// May panic if `align` is not a power of two. Even if it doesn't panic in this
65+
/// case, it will produce nonsense results.
66+
#[inline(always)]
67+
pub(crate) const fn _round_down_to_next_multiple_of_alignment(
68+
n: usize,
69+
align: NonZeroUsize,
70+
) -> usize {
71+
let align = align.get();
72+
debug_assert!(align.is_power_of_two());
73+
74+
// Subtraction can't underflow because `align.get() >= 1`.
75+
#[allow(clippy::arithmetic_side_effects)]
76+
let mask = !(align - 1);
77+
n & mask
78+
}
79+
5980
#[cfg(test)]
6081
pub(crate) mod testutil {
6182
use core::fmt::{self, Display, Formatter};
@@ -106,3 +127,25 @@ pub(crate) mod testutil {
106127

107128
impl_known_layout!(AU64);
108129
}
130+
131+
#[cfg(test)]
132+
mod tests {
133+
use super::*;
134+
135+
#[test]
136+
fn test_round_down_to_next_multiple_of_alignment() {
137+
fn alt_impl(n: usize, align: NonZeroUsize) -> usize {
138+
let mul = n / align.get();
139+
mul * align.get()
140+
}
141+
142+
for align in [1, 2, 4, 8, 16] {
143+
for n in 0..256 {
144+
let align = NonZeroUsize::new(align).unwrap();
145+
let want = alt_impl(n, align);
146+
let got = _round_down_to_next_multiple_of_alignment(n, align);
147+
assert_eq!(got, want, "round_down_to_next_multiple_of_alignment({n}, {align})");
148+
}
149+
}
150+
}
151+
}

0 commit comments

Comments
 (0)