bucket_mask_to_capacity() integer overflow when bucket_mask == usize::MAX

[yanfenghu]

Hi,

I found a potential integer overflow issue through Kani formal verification.

Location: src/raw.rs:189

Current Code:

fn bucket_mask_to_capacity(bucket_mask: usize) -> usize {
if bucket_mask < 8 {
bucket_mask
} else {
((bucket_mask + 1) / 8) * 7 // Overflow when bucket_mask == usize::MAX!
}
}
Problem:

When bucket_mask = usize::MAX:

bucket_mask + 1 wraps to 0

Returns 0 instead of correct capacity

Suggested Fix:

fn bucket_mask_to_capacity(bucket_mask: usize) -> usize {
if bucket_mask < 8 {
bucket_mask
} else {
bucket_mask.checked_add(1)
.map(|bm| (bm / 8) * 7)
.unwrap_or(usize::MAX)
}
}
Could you please confirm if this is a valid concern?

[Amanieu]

bucket_mask can never be that large because all memory allocations are capped to isize::MAX bytes. Even for a ZST table, there is still an allocation required for the array of control bytes, 1 per element.

[yanfenghu]

Hi,
That makes perfect sense, thank you for the explanation. I understand now that bucket_mask is physically bounded by the maximum allocation size (isize::MAX), making this overflow practically unreachable.

Since Kani explores all possible mathematical states for the inputs, it flagged this edge case regardless of runtime constraints.

While it’s not an exploitable issue, adding a checked_add or a simple debug assertion could be considered defensive programming to explicitly document this invariant and silence static analyzers/formal verification tools. However, I completely understand if you prefer to keep the code as is for simplicity and performance.

Thanks again for looking into it! I’ll close this issue if you don’t feel a change is necessary.

[Amanieu]

I'm against adding a checked_add here: having code which tries to handle cases which are impossible to reach just makes the code harder to read. However I would be OK with adding a debug assertion since that also helps document the invariant. Feel free to submit a PR.

[yanfenghu]

Makes sense. A debug_assert is definitely the right balance between keeping the code readable and documenting the invariant. Thanks for the review!