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

src/lib.rs

@@ -484,21 +484,12 @@ impl DstLayout {
                 (0, size)
             }
             SizeInfo::SliceDst(TrailingSliceLayout { _offset: offset, _elem_size: elem_size }) => {
-                let align = self._align.get();
-
                 // Calculate the maximum number of bytes that could be consumed
                 // - any number of bytes larger than this will either not be a
                 // multiple of the alignment, or will be larger than
                 // `bytes_len`.
-                //
-                // Guaranteed not to:
-                // - divide by zero: `align` is non-zero.
-                // - overflow on multiplication: `usize::MAX >= bytes_len >=
-                //   (bytes_len / align) * align`
-                //
-                // TODO(#390): Compute this more efficiently.
-                #[allow(clippy::arithmetic_side_effects)]
-                let max_total_bytes = (bytes_len / align) * align;
+                let max_total_bytes =
+                    util::_round_down_to_next_multiple_of_alignment(bytes_len, self._align);
                 // Calculate the maximum number of bytes that could be consumed
                 // by the trailing slice.
                 //

src/util.rs

@@ -5,7 +5,7 @@
 #[path = "third_party/rust/layout.rs"]
 pub(crate) mod core_layout;
 
-use core::mem;
+use core::{mem, num::NonZeroUsize};
 
 pub(crate) trait AsAddress {
     fn addr(self) -> usize;
@@ -56,6 +56,27 @@ pub(crate) fn aligned_to<T: AsAddress, U>(t: T) -> bool {
     remainder == 0
 }
 
+/// Round `n` down to the largest value `m` such that `m <= n` and `m % align ==
+/// 0`.
+///
+/// # Panics
+///
+/// May panic if `align` is not a power of two. Even if it doesn't panic in this
+/// case, it will produce nonsense results.
+#[inline(always)]
+pub(crate) const fn _round_down_to_next_multiple_of_alignment(
+    n: usize,
+    align: NonZeroUsize,
+) -> usize {
+    let align = align.get();
+    debug_assert!(align.is_power_of_two());
+
+    // Subtraction can't underflow because `align.get() >= 1`.
+    #[allow(clippy::arithmetic_side_effects)]
+    let mask = !(align - 1);
+    n & mask
+}
+
 #[cfg(test)]
 pub(crate) mod testutil {
     use core::fmt::{self, Display, Formatter};
@@ -106,3 +127,25 @@ pub(crate) mod testutil {
 
     impl_known_layout!(AU64);
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_round_down_to_next_multiple_of_alignment() {
+        fn alt_impl(n: usize, align: NonZeroUsize) -> usize {
+            let mul = n / align.get();
+            mul * align.get()
+        }
+
+        for align in [1, 2, 4, 8, 16] {
+            for n in 0..256 {
+                let align = NonZeroUsize::new(align).unwrap();
+                let want = alt_impl(n, align);
+                let got = _round_down_to_next_multiple_of_alignment(n, align);
+                assert_eq!(got, want, "round_down_to_next_multiple_of_alignment({n}, {align})");
+            }
+        }
+    }
+}