From c2f3b8b73c8af102f01550226aac26caece08a05 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 18 Apr 2025 14:46:19 +0000
Subject: [PATCH 01/13] 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 <tautschn@amazon.com>
Date: Fri, 18 Apr 2025 14:58:30 +0000
Subject: [PATCH 02/13] 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 <tautschn@amazon.com>
Date: Tue, 29 Apr 2025 20:46:20 +0000
Subject: [PATCH 03/13] 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 <tautschn@amazon.com>
Date: Wed, 30 Apr 2025 09:14:36 +0000
Subject: [PATCH 04/13] 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 <tautschn@amazon.com>
Date: Wed, 30 Apr 2025 12:45:40 +0000
Subject: [PATCH 05/13] 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 <tautschn@amazon.com>
Date: Wed, 30 Apr 2025 12:57:00 +0000
Subject: [PATCH 06/13] 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 <mt@debian.org>
Date: Fri, 30 May 2025 12:16:36 +0200
Subject: [PATCH 07/13] Update library/core/src/iter/range.rs
Co-authored-by: Carolyn Zech <carolynzech@gmail.com>
---
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 <mt@debian.org>
Date: Fri, 30 May 2025 12:16:48 +0200
Subject: [PATCH 08/13] Update library/core/src/iter/range.rs
Co-authored-by: Carolyn Zech <carolynzech@gmail.com>
---
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 <mt@debian.org>
Date: Fri, 30 May 2025 12:16:56 +0200
Subject: [PATCH 09/13] Update library/core/src/iter/range.rs
Co-authored-by: Carolyn Zech <carolynzech@gmail.com>
---
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 <tautschn@amazon.com>
Date: Fri, 30 May 2025 10:39:07 +0000
Subject: [PATCH 10/13] 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 <tautschn@amazon.com>
Date: Fri, 30 May 2025 10:50:31 +0000
Subject: [PATCH 11/13] 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()
)
From 07490e9decbf6e829db6a5947f54d5a3955bc125 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 10 Jul 2025 17:40:34 +0000
Subject: [PATCH 12/13] Ipv6Addr
---
library/core/src/iter/range.rs | 2 ++
1 file changed, 2 insertions(+)
diff --git a/library/core/src/iter/range.rs b/library/core/src/iter/range.rs
index 33d16e0d39a02..70a38eafaa443 100644
--- a/library/core/src/iter/range.rs
+++ b/library/core/src/iter/range.rs
@@ -645,6 +645,7 @@ impl Step for Ipv6Addr {
u128::backward_checked(start.to_bits(), count).map(Ipv6Addr::from_bits)
}
+ #[requires(start.to_bits().checked_add(count as u128).is_some())]
#[inline]
unsafe fn forward_unchecked(start: Ipv6Addr, count: usize) -> Ipv6Addr {
// SAFETY: Since u128 and Ipv6Addr are losslessly convertible,
@@ -652,6 +653,7 @@ impl Step for Ipv6Addr {
Ipv6Addr::from_bits(unsafe { u128::forward_unchecked(start.to_bits(), count) })
}
+ #[requires(start.to_bits().checked_sub(count as u128).is_some())]
#[inline]
unsafe fn backward_unchecked(start: Ipv6Addr, count: usize) -> Ipv6Addr {
// SAFETY: Since u128 and Ipv6Addr are losslessly convertible,
From d9d43697d50272b99d41affa88d19f1d91a3579a Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 10 Jul 2025 19:55:29 +0000
Subject: [PATCH 13/13] Fix
---
.github/workflows/kani.yml | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index d7300c1777543..b342518a5a7ea 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -102,8 +102,8 @@ jobs:
scripts/run-kani.sh --run autoharness --kani-args \
--include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::disjoint_bitor" \
--include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::unchecked_disjoint_bitor" \
- --include-pattern "<(.+)[[:space:]]as[[:space:]]iter::range::Step>::backward_unchecked \
- --include-pattern "<(.+)[[:space:]]as[[:space:]]iter::range::Step>::forward_unchecked \
+ --include-pattern "<(.+)[[:space:]]as[[:space:]]iter::range::Step>::backward_unchecked" \
+ --include-pattern "<(.+)[[:space:]]as[[:space:]]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 \