From 58216f22b0ed7dd119753d14e2cfdfa09e916120 Mon Sep 17 00:00:00 2001 From: AlexLB99 Date: Tue, 13 May 2025 16:18:02 -0400 Subject: [PATCH 1/4] make_ascii_uppercase/lowercase harnesses --- library/core/src/str/mod.rs | 54 +++++++++++++++++++++++++++++++++++++ 1 file changed, 54 insertions(+) diff --git a/library/core/src/str/mod.rs b/library/core/src/str/mod.rs index 79b4953fcc11a..230ebeabf9f87 100644 --- a/library/core/src/str/mod.rs +++ b/library/core/src/str/mod.rs @@ -19,6 +19,10 @@ use crate::ops::Range; use crate::slice::{self, SliceIndex}; use crate::{ascii, mem}; +use safety::{ensures, requires}; +#[cfg(kani)] +use crate::kani; + pub mod pattern; mod lossy; @@ -3038,3 +3042,53 @@ impl_fn_for_zst! { // This is required to make `impl From<&str> for Box` and `impl From for Box` not overlap. #[stable(feature = "error_in_core_neg_impl", since = "1.65.0")] impl !crate::error::Error for &str {} + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + use crate::kani; + + #[kani::proof] + #[kani::unwind(33)] + fn check_make_ascii_uppercase() { + const MAX_SIZE: usize = 32; + let in_bytes: [u8; MAX_SIZE] = kani::any(); + + if let Ok(s) = from_utf8(&in_bytes) { + let mut in_bytes_copy = in_bytes; + //SAFETY: we know that in_bytes_copy is valid UTF-8 + let mut s_copy = unsafe { from_utf8_unchecked_mut(&mut in_bytes_copy) }; + s_copy.make_ascii_uppercase(); + let s_uppercase = s_copy.as_bytes(); + + for (i, &item) in s.as_bytes().iter().enumerate() { + if item >= b'a' && item <= b'z' { + assert_eq!(s_uppercase[i], item - 32); + } + } + } + } + + #[kani::proof] + #[kani::unwind(33)] + fn check_make_ascii_lowercase() { + const MAX_SIZE: usize = 32; + let in_bytes: [u8; MAX_SIZE] = kani::any(); + + if let Ok(s) = from_utf8(&in_bytes) { + let mut in_bytes_copy = in_bytes; + //SAFETY: we know that in_bytes_copy is valid UTF-8 + let mut s_copy = unsafe { from_utf8_unchecked_mut(&mut in_bytes_copy) }; + s_copy.make_ascii_lowercase(); + let s_lowercase = s_copy.as_bytes(); + + for (i, &item) in s.as_bytes().iter().enumerate() { + if item >= b'A' && item <= b'Z' { + assert_eq!(s_lowercase[i], item + 32); + } + } + } + } + +} From b4212196db296f0485fe2286f34f64e98556ee8c Mon Sep 17 00:00:00 2001 From: AlexLB99 Date: Tue, 13 May 2025 16:28:18 -0400 Subject: [PATCH 2/4] added extra check to make_ascii_uppercase/lowercase harnesses --- library/core/src/str/mod.rs | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/library/core/src/str/mod.rs b/library/core/src/str/mod.rs index 230ebeabf9f87..28903c33fd678 100644 --- a/library/core/src/str/mod.rs +++ b/library/core/src/str/mod.rs @@ -3065,6 +3065,8 @@ mod verify { for (i, &item) in s.as_bytes().iter().enumerate() { if item >= b'a' && item <= b'z' { assert_eq!(s_uppercase[i], item - 32); + } else { + assert_eq!(s_uppercase[i], item); } } } @@ -3086,6 +3088,8 @@ mod verify { for (i, &item) in s.as_bytes().iter().enumerate() { if item >= b'A' && item <= b'Z' { assert_eq!(s_lowercase[i], item + 32); + } else { + assert_eq!(s_lowercase[i], item); } } } From e8e95951d2d480198776d141578f2568610ef2cf Mon Sep 17 00:00:00 2001 From: AlexLB99 Date: Tue, 13 May 2025 17:25:49 -0400 Subject: [PATCH 3/4] formatting fixes --- library/core/src/str/mod.rs | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/library/core/src/str/mod.rs b/library/core/src/str/mod.rs index 28903c33fd678..19788316e72bf 100644 --- a/library/core/src/str/mod.rs +++ b/library/core/src/str/mod.rs @@ -15,14 +15,12 @@ mod validations; use self::pattern::{DoubleEndedSearcher, Pattern, ReverseSearcher, Searcher}; use crate::char::{self, EscapeDebugExtArgs}; +#[cfg(kani)] +use crate::kani; use crate::ops::Range; use crate::slice::{self, SliceIndex}; use crate::{ascii, mem}; -use safety::{ensures, requires}; -#[cfg(kani)] -use crate::kani; - pub mod pattern; mod lossy; @@ -3094,5 +3092,4 @@ mod verify { } } } - } From 08e6894bdea3cd34ed50fb0e6c01aef6f06fde7e Mon Sep 17 00:00:00 2001 From: AlexLB99 Date: Mon, 26 May 2025 17:21:07 -0400 Subject: [PATCH 4/4] added comments to uppercase/lowercase harnesses --- library/core/src/str/mod.rs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/library/core/src/str/mod.rs b/library/core/src/str/mod.rs index cda8d340afd02..6d41b022c3aad 100644 --- a/library/core/src/str/mod.rs +++ b/library/core/src/str/mod.rs @@ -3071,6 +3071,9 @@ mod verify { use super::*; use crate::kani; + //for each char in input str, if char is lowercase, then + //that char in output str is corresponding uppercase char, + //and all other chars in the output are the same as input #[kani::proof] #[kani::unwind(33)] fn check_make_ascii_uppercase() { @@ -3094,6 +3097,9 @@ mod verify { } } + //for each char in input str, if char is uppercase, then + //that char in output str is corresponding lowercase char, + //and all other chars in the output are the same as input #[kani::proof] #[kani::unwind(33)] fn check_make_ascii_lowercase() {