Skip to content

Add safety preconditions to core/src/iter/range.rs #331

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.

Sign up for GitHub

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

Open
wants to merge 8 commits into
base: main
Choose a base branch
from
Open

Add safety preconditions to core/src/iter/range.rs #331

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
c2f3b8b
Add safety preconditions to core/src/iter/range.rs
tautschnig Apr 18, 2025
e2c02cf
Fix format
tautschnig Apr 18, 2025
5903dc8
Merge remote-tracking branch 'origin/main' into iter-range-rs-contracts
tautschnig Apr 29, 2025
a938e9c
Add autoharness calls
tautschnig Apr 29, 2025
171d1ab
Further contracts
tautschnig Apr 30, 2025
a8e23b3
Update char contracts
tautschnig Apr 30, 2025
3b3e4f6
Fix contracts
tautschnig Apr 30, 2025
24ea4b1
Merge branch 'main' into iter-range-rs-contracts
tautschnig May 20, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions .github/workflows/kani.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,8 @@ jobs:
- name: Run Kani Verification
run: |
scripts/run-kani.sh --run autoharness --kani-args \
--include-pattern "iter::range::Step>::backward_unchecked" \
--include-pattern "iter::range::Step>::forward_unchecked" \
--include-pattern alloc::layout::Layout::from_size_align \
--include-pattern ascii::ascii_char::AsciiChar::from_u8 \
--include-pattern char::convert::from_u32_unchecked \
Expand Down
25 changes: 25 additions & 0 deletions library/core/src/iter/range.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,7 +1,11 @@
use safety::requires;

use super::{
FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce, TrustedStep,
};
use crate::ascii::Char as AsciiChar;
#[cfg(kani)]
use crate::kani;
use crate::mem;
use crate::net::{Ipv4Addr, Ipv6Addr};
use crate::num::NonZero;
Expand Down Expand Up @@ -183,12 +187,14 @@ pub trait Step: Clone + PartialOrd + Sized {
// than the signed::MAX value. Therefore `as` casting to the signed type would be incorrect.
macro_rules! step_signed_methods {
($unsigned: ty) => {
#[requires(start.checked_add_unsigned(n as $unsigned).is_some())]
#[inline]
unsafe fn forward_unchecked(start: Self, n: usize) -> Self {
// SAFETY: the caller has to guarantee that `start + n` doesn't overflow.
unsafe { start.checked_add_unsigned(n as $unsigned).unwrap_unchecked() }
}

#[requires(start.checked_sub_unsigned(n as $unsigned).is_some())]
#[inline]
unsafe fn backward_unchecked(start: Self, n: usize) -> Self {
// SAFETY: the caller has to guarantee that `start - n` doesn't overflow.
Expand All @@ -199,12 +205,14 @@ macro_rules! step_signed_methods {

macro_rules! step_unsigned_methods {
() => {
#[requires(start.checked_add(n as Self).is_some())]
#[inline]
unsafe fn forward_unchecked(start: Self, n: usize) -> Self {
// SAFETY: the caller has to guarantee that `start + n` doesn't overflow.
unsafe { start.unchecked_add(n as Self) }
}

#[requires(start >= (n as Self))]
#[inline]
unsafe fn backward_unchecked(start: Self, n: usize) -> Self {
// SAFETY: the caller has to guarantee that `start - n` doesn't overflow.
Expand Down Expand Up @@ -494,6 +502,13 @@ impl Step for char {
Some(unsafe { char::from_u32_unchecked(res) })
}

#[requires((start as u32).checked_add(count as u32).is_some())]
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
#[requires((start as u32).checked_add(count as u32).is_some())]

Isn't this redundant, given that the next precondition has the same check?

#[requires({
let dist = (start as u32).checked_add(count as u32);
dist.is_some() &&
((start as u32) >= 0xD800 || dist.unwrap() < 0xD800 ||
dist.unwrap().checked_add(0x800).is_some())
Comment on lines +507 to +510
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nit: use is_some_and

Suggested change
let dist = (start as u32).checked_add(count as u32);
dist.is_some() &&
((start as u32) >= 0xD800 || dist.unwrap() < 0xD800 ||
dist.unwrap().checked_add(0x800).is_some())
(start as u32).checked_add(count as u32).is_some_and(|dist|
(start as u32) >= 0xD800 ||
dist < 0xD800 ||
dist.checked_add(0x800).is_some()
)

})]
#[inline]
unsafe fn forward_unchecked(start: char, count: usize) -> char {
let start = start as u32;
Expand All @@ -510,6 +525,12 @@ impl Step for char {
unsafe { char::from_u32_unchecked(res) }
}

#[requires({
let dist = (start as u32).checked_sub(count as u32);
dist.is_some() &&
((start as u32) < 0xE000 || dist.unwrap() >= 0xE000 ||
dist.unwrap().checked_sub(0x800).is_some())
})]
Comment on lines +528 to +533
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
#[requires({
let dist = (start as u32).checked_sub(count as u32);
dist.is_some() &&
((start as u32) < 0xE000 || dist.unwrap() >= 0xE000 ||
dist.unwrap().checked_sub(0x800).is_some())
})]
#[requires({
(start as u32).checked_sub(count as u32).is_some_and(|dist|
(start as u32) < 0xE000 ||
dist >= 0xE000 ||
dist.checked_sub(0x800).is_some()
)
})]

#[inline]
unsafe fn backward_unchecked(start: char, count: usize) -> char {
let start = start as u32;
Expand Down Expand Up @@ -548,6 +569,7 @@ impl Step for AsciiChar {
Some(unsafe { AsciiChar::from_u8_unchecked(end) })
}

#[requires((start.to_u8() as u32).checked_add(count as u32).is_some())]
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this enough? The precondition is that "the result is a valid ASCII character," so wouldn't we need a precondition to encode that expectation? I'm envisioning 1) doing the computation in a safe way 2) asserting that the outcome of that is valid ASCII?

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The documentation for the trait says:

Safety
It is undefined behavior for this operation to overflow the range of values supported by Self. If you cannot guarantee that this will not overflow, use forward or forward_checked instead.

and the documentation for AsciiCharsays:

/// # Layout
///
/// This type is guaranteed to have a size and alignment of 1 byte.

This precondition says that the result doesn't overflow a u32, but shouldn't it say that it doesn't overflow "the range of values supported by Self," i.e. a u8?

#[inline]
unsafe fn forward_unchecked(start: AsciiChar, count: usize) -> AsciiChar {
// SAFETY: Caller asserts that result is a valid ASCII character,
Expand All @@ -558,6 +580,7 @@ impl Step for AsciiChar {
unsafe { AsciiChar::from_u8_unchecked(end) }
}

#[requires((start.to_u8() as u32).checked_sub(count as u32).is_some())]
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Same question as above re: precondition.

#[inline]
unsafe fn backward_unchecked(start: AsciiChar, count: usize) -> AsciiChar {
// SAFETY: Caller asserts that result is a valid ASCII character,
Expand Down Expand Up @@ -586,13 +609,15 @@ impl Step for Ipv4Addr {
u32::backward_checked(start.to_bits(), count).map(Ipv4Addr::from_bits)
}

#[requires(start.to_bits().checked_add(count as u32).is_some())]
#[inline]
unsafe fn forward_unchecked(start: Ipv4Addr, count: usize) -> Ipv4Addr {
// SAFETY: Since u32 and Ipv4Addr are losslessly convertible,
// this is as safe as the u32 version.
Ipv4Addr::from_bits(unsafe { u32::forward_unchecked(start.to_bits(), count) })
}

#[requires(start.to_bits().checked_sub(count as u32).is_some())]
#[inline]
unsafe fn backward_unchecked(start: Ipv4Addr, count: usize) -> Ipv4Addr {
// SAFETY: Since u32 and Ipv4Addr are losslessly convertible,
Expand Down
Loading