From c2f3b8b73c8af102f01550226aac26caece08a05 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Apr 2025 14:46:19 +0000 Subject: [PATCH 01/11] Add safety preconditions to core/src/iter/range.rs For the signed and unsigned methods in the macros, I added contracts that require the checked operations to succeed, which is what the safety comments are stating. These contracts formalize the safety requirements that were previously only documented in comments. --- library/core/src/iter/range.rs | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/library/core/src/iter/range.rs b/library/core/src/iter/range.rs index 4fa719de5ebf0..dc220a79cb5a2 100644 --- a/library/core/src/iter/range.rs +++ b/library/core/src/iter/range.rs @@ -6,6 +6,9 @@ use crate::mem; use crate::net::{Ipv4Addr, Ipv6Addr}; use crate::num::NonZero; use crate::ops::{self, Try}; +#[cfg(kani)] +use crate::kani; +use safety::requires; // Safety: All invariants are upheld. macro_rules! unsafe_impl_trusted_step { @@ -183,12 +186,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 +204,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.checked_sub(n as Self).is_some())] #[inline] unsafe fn backward_unchecked(start: Self, n: usize) -> Self { // SAFETY: the caller has to guarantee that `start - n` doesn't overflow. From e2c02cf1b18faaf910911e0b4033c54e68ae6694 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 18 Apr 2025 14:58:30 +0000 Subject: [PATCH 02/11] Fix format --- library/core/src/iter/range.rs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/library/core/src/iter/range.rs b/library/core/src/iter/range.rs index dc220a79cb5a2..ec0be9439cfe1 100644 --- a/library/core/src/iter/range.rs +++ b/library/core/src/iter/range.rs @@ -1,14 +1,15 @@ +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; use crate::ops::{self, Try}; -#[cfg(kani)] -use crate::kani; -use safety::requires; // Safety: All invariants are upheld. macro_rules! unsafe_impl_trusted_step { From a938e9cc4e18185b8221881615df7eb961604b53 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 29 Apr 2025 20:46:20 +0000 Subject: [PATCH 03/11] Add autoharness calls --- .github/workflows/kani.yml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index fd949f8eef552..ee85de8a5339e 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -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 \ From 171d1ab7ea8a441cfc93e9e75aab0860b7bdd420 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Apr 2025 09:14:36 +0000 Subject: [PATCH 04/11] Further contracts --- library/core/src/iter/range.rs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/library/core/src/iter/range.rs b/library/core/src/iter/range.rs index ec0be9439cfe1..af65a8b486921 100644 --- a/library/core/src/iter/range.rs +++ b/library/core/src/iter/range.rs @@ -502,6 +502,7 @@ impl Step for char { Some(unsafe { char::from_u32_unchecked(res) }) } + #[requires((start as u32).checked_add(count as u32).is_some())] #[inline] unsafe fn forward_unchecked(start: char, count: usize) -> char { let start = start as u32; @@ -518,6 +519,7 @@ impl Step for char { unsafe { char::from_u32_unchecked(res) } } + #[requires((start as u32).checked_sub(count as u32).is_some())] #[inline] unsafe fn backward_unchecked(start: char, count: usize) -> char { let start = start as u32; @@ -556,6 +558,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())] #[inline] unsafe fn forward_unchecked(start: AsciiChar, count: usize) -> AsciiChar { // SAFETY: Caller asserts that result is a valid ASCII character, @@ -566,6 +569,7 @@ impl Step for AsciiChar { unsafe { AsciiChar::from_u8_unchecked(end) } } + #[requires((start.to_u8() as u32).checked_sub(count as u32).is_some())] #[inline] unsafe fn backward_unchecked(start: AsciiChar, count: usize) -> AsciiChar { // SAFETY: Caller asserts that result is a valid ASCII character, @@ -594,6 +598,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, @@ -601,6 +606,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, From a8e23b368a329d5ee0c880e029c8c62d5b7c048e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Apr 2025 12:45:40 +0000 Subject: [PATCH 05/11] Update char contracts --- library/core/src/iter/range.rs | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/library/core/src/iter/range.rs b/library/core/src/iter/range.rs index af65a8b486921..f31994d29cdc9 100644 --- a/library/core/src/iter/range.rs +++ b/library/core/src/iter/range.rs @@ -212,7 +212,7 @@ macro_rules! step_unsigned_methods { unsafe { start.unchecked_add(n as Self) } } - #[requires(start.checked_sub(n as Self).is_some())] + #[requires(start >= n)] #[inline] unsafe fn backward_unchecked(start: Self, n: usize) -> Self { // SAFETY: the caller has to guarantee that `start - n` doesn't overflow. @@ -503,6 +503,12 @@ impl Step for char { } #[requires((start as u32).checked_add(count as u32).is_some())] + #[requires({ + let dist = (start as u32).checked_add(count as u32); + dist.is_some() && + (start >= 0xD800 || dist.unwrap() < 0xD800 || + dist.unwrap().checked_add(0x800).is_some()) + })] #[inline] unsafe fn forward_unchecked(start: char, count: usize) -> char { let start = start as u32; @@ -519,7 +525,12 @@ impl Step for char { unsafe { char::from_u32_unchecked(res) } } - #[requires((start as u32).checked_sub(count as u32).is_some())] + #[requires({ + let dist = (start as u32).checked_sub(count as u32); + dist.is_some() && + (start < 0xE000 || dist.unwrap() >= 0xE000 || + dist.unwrap().checked_sub(0x800).is_some()) + })] #[inline] unsafe fn backward_unchecked(start: char, count: usize) -> char { let start = start as u32; From 3b3e4f662ea18ccb4461fe5c5bc2a1e142d3da94 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 30 Apr 2025 12:57:00 +0000 Subject: [PATCH 06/11] Fix contracts --- library/core/src/iter/range.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/core/src/iter/range.rs b/library/core/src/iter/range.rs index f31994d29cdc9..c83204b7b913b 100644 --- a/library/core/src/iter/range.rs +++ b/library/core/src/iter/range.rs @@ -212,7 +212,7 @@ macro_rules! step_unsigned_methods { unsafe { start.unchecked_add(n as Self) } } - #[requires(start >= n)] + #[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. @@ -506,7 +506,7 @@ impl Step for char { #[requires({ let dist = (start as u32).checked_add(count as u32); dist.is_some() && - (start >= 0xD800 || dist.unwrap() < 0xD800 || + ((start as u32) >= 0xD800 || dist.unwrap() < 0xD800 || dist.unwrap().checked_add(0x800).is_some()) })] #[inline] @@ -528,7 +528,7 @@ impl Step for char { #[requires({ let dist = (start as u32).checked_sub(count as u32); dist.is_some() && - (start < 0xE000 || dist.unwrap() >= 0xE000 || + ((start as u32) < 0xE000 || dist.unwrap() >= 0xE000 || dist.unwrap().checked_sub(0x800).is_some()) })] #[inline] From 0ccaf2f962fdf5ba4bafb049ffe8396b549a488a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 30 May 2025 12:16:36 +0200 Subject: [PATCH 07/11] Update library/core/src/iter/range.rs Co-authored-by: Carolyn Zech --- library/core/src/iter/range.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/library/core/src/iter/range.rs b/library/core/src/iter/range.rs index c83204b7b913b..9cc54401096f8 100644 --- a/library/core/src/iter/range.rs +++ b/library/core/src/iter/range.rs @@ -502,7 +502,6 @@ impl Step for char { Some(unsafe { char::from_u32_unchecked(res) }) } - #[requires((start as u32).checked_add(count as u32).is_some())] #[requires({ let dist = (start as u32).checked_add(count as u32); dist.is_some() && From 16e6b0a54dc0d8e2b0940a81f0774b522ebb6560 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 30 May 2025 12:16:48 +0200 Subject: [PATCH 08/11] Update library/core/src/iter/range.rs Co-authored-by: Carolyn Zech --- library/core/src/iter/range.rs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/library/core/src/iter/range.rs b/library/core/src/iter/range.rs index 9cc54401096f8..39d84c069179a 100644 --- a/library/core/src/iter/range.rs +++ b/library/core/src/iter/range.rs @@ -503,10 +503,11 @@ impl Step for char { } #[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()) + (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 { From 44bf92bbc66e4844e0f40e0a664a7cd17ec203af Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 30 May 2025 12:16:56 +0200 Subject: [PATCH 09/11] Update library/core/src/iter/range.rs Co-authored-by: Carolyn Zech --- library/core/src/iter/range.rs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/library/core/src/iter/range.rs b/library/core/src/iter/range.rs index 39d84c069179a..63348a8ade384 100644 --- a/library/core/src/iter/range.rs +++ b/library/core/src/iter/range.rs @@ -526,10 +526,11 @@ impl Step for char { } #[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()) + (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 { From 8ee85f5b5c9d3ffedd5260c5e755f193c4606e4c Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 30 May 2025 10:39:07 +0000 Subject: [PATCH 10/11] Amend AsciiChar preconditions --- library/core/src/iter/range.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/iter/range.rs b/library/core/src/iter/range.rs index 63348a8ade384..ef60b70dddf7a 100644 --- a/library/core/src/iter/range.rs +++ b/library/core/src/iter/range.rs @@ -570,7 +570,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())] + #[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, @@ -581,7 +581,7 @@ impl Step for AsciiChar { unsafe { AsciiChar::from_u8_unchecked(end) } } - #[requires((start.to_u8() as u32).checked_sub(count as u32).is_some())] + #[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, From 6258c7d435b1534cb66e4354ea38926336146f96 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 30 May 2025 10:50:31 +0000 Subject: [PATCH 11/11] Remove whitespace --- library/core/src/iter/range.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/iter/range.rs b/library/core/src/iter/range.rs index ef60b70dddf7a..3f193c5144a48 100644 --- a/library/core/src/iter/range.rs +++ b/library/core/src/iter/range.rs @@ -504,7 +504,7 @@ impl Step for char { #[requires({ (start as u32).checked_add(count as u32).is_some_and(|dist| - (start as u32) >= 0xD800 || + (start as u32) >= 0xD800 || dist < 0xD800 || dist.checked_add(0x800).is_some() )