diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 06049d4317f29..7a85eeeee51f3 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -87,6 +87,8 @@ jobs: scripts/run-kani.sh --run autoharness --kani-args \ --include-pattern ">::disjoint_bitor" \ --include-pattern ">::unchecked_disjoint_bitor" \ + --include-pattern "iter::range::Step>::backward_unchecked" \ + --include-pattern "iter::range::Step>::forward_unchecked" \ --include-pattern alloc::__default_lib_allocator:: \ --include-pattern alloc::layout::Layout::from_size_align \ --include-pattern ascii::ascii_char::AsciiChar::from_u8 \ diff --git a/library/core/src/iter/range.rs b/library/core/src/iter/range.rs index 4fa719de5ebf0..3f193c5144a48 100644 --- a/library/core/src/iter/range.rs +++ b/library/core/src/iter/range.rs @@ -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; @@ -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. @@ -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. @@ -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_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; @@ -510,6 +525,13 @@ impl Step for char { unsafe { char::from_u32_unchecked(res) } } + #[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; @@ -548,6 +570,7 @@ impl Step for AsciiChar { Some(unsafe { AsciiChar::from_u8_unchecked(end) }) } + #[requires(count < 256 && start.to_u8().checked_add(count as u8).is_some())] #[inline] unsafe fn forward_unchecked(start: AsciiChar, count: usize) -> AsciiChar { // SAFETY: Caller asserts that result is a valid ASCII character, @@ -558,6 +581,7 @@ impl Step for AsciiChar { unsafe { AsciiChar::from_u8_unchecked(end) } } + #[requires(count < 256 && start.to_u8().checked_sub(count as u8).is_some())] #[inline] unsafe fn backward_unchecked(start: AsciiChar, count: usize) -> AsciiChar { // SAFETY: Caller asserts that result is a valid ASCII character, @@ -586,6 +610,7 @@ 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, @@ -593,6 +618,7 @@ impl Step for Ipv4Addr { 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,