From 86f700d7dae1a4108f9bcdb5db4fb1dc5646c596 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Sat, 30 Nov 2024 02:51:37 -0800 Subject: [PATCH 1/4] add proof from_bytes_with_null --- library/core/src/ffi/c_str.rs | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 05506aa4fb19..0781085668e3 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -876,6 +876,32 @@ mod verify { } } + // pub const fn from_bytes_with_nul(bytes: &[u8]) -> Result<&Self, FromBytesWithNulError> + #[kani::proof] + #[kani::unwind(33)] + fn check_from_bytes_with_nul() { + const MAX_SIZE: usize = 32; + let mut buffer: [u8; MAX_SIZE] = kani::any(); + + // last byte == null + buffer[MAX_SIZE - 1] = 0; + + // check to see all bytes before the last are non-null + for i in 0..MAX_SIZE - 1 { + kani::assume(buffer[i] != 0); + } + let slice = &buffer[..]; + let result = CStr::from_bytes_with_nul(slice); + + if let Ok(c_str) = result { + assert!(c_str.is_safe()); + // check that the byte slice without the null terminator matches the expected bytes + assert_eq!(c_str.to_bytes(), &buffer[..MAX_SIZE - 1]); + // check that the byte slice with the null terminator matches the original buffer + assert_eq!(c_str.to_bytes_with_nul(), &buffer[..]); + } + } + #[kani::proof] #[kani::unwind(32)] fn check_count_bytes() { @@ -898,4 +924,4 @@ mod verify { // Verify that count_bytes matches the adjusted length assert_eq!(c_str.count_bytes(), len); } -} \ No newline at end of file +} From 007a60453bef112f611b541cd02345ed1873106c Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Sat, 30 Nov 2024 20:08:08 -0800 Subject: [PATCH 2/4] optimize from_bytes_with_nul --- library/core/src/ffi/c_str.rs | 32 +++++++++++++++++--------------- 1 file changed, 17 insertions(+), 15 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 9cc4b7e716c0..bc3ec49c0de1 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -883,29 +883,31 @@ mod verify { } } - // pub const fn from_bytes_with_nul(bytes: &[u8]) -> Result<&Self, FromBytesWithNulError> #[kani::proof] #[kani::unwind(33)] fn check_from_bytes_with_nul() { const MAX_SIZE: usize = 32; let mut buffer: [u8; MAX_SIZE] = kani::any(); - // last byte == null - buffer[MAX_SIZE - 1] = 0; + // Iterate over all possible slice lengths from 1 to MAX_SIZE + for slice_length in 1..=MAX_SIZE { + // Ensure the slice is valid by setting the last byte to null + buffer[slice_length - 1] = 0; - // check to see all bytes before the last are non-null - for i in 0..MAX_SIZE - 1 { - kani::assume(buffer[i] != 0); - } - let slice = &buffer[..]; - let result = CStr::from_bytes_with_nul(slice); + // Assume all bytes before the last are non-null + for i in 0..slice_length - 1 { + kani::assume(buffer[i] != 0); + } - if let Ok(c_str) = result { - assert!(c_str.is_safe()); - // check that the byte slice without the null terminator matches the expected bytes - assert_eq!(c_str.to_bytes(), &buffer[..MAX_SIZE - 1]); - // check that the byte slice with the null terminator matches the original buffer - assert_eq!(c_str.to_bytes_with_nul(), &buffer[..]); + // Create the slice up to the current slice_length + let slice = &buffer[..slice_length]; + let result = CStr::from_bytes_with_nul(slice); + + if let Ok(c_str) = result { + assert!(c_str.is_safe()); + assert_eq!(c_str.to_bytes(), &buffer[..slice_length - 1]); + assert_eq!(c_str.to_bytes_with_nul(), &buffer[..slice_length]); + } } } From e685483e5e9b7b3aa9b6ad6b5cd3041064f6b484 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Sun, 1 Dec 2024 21:48:41 -0800 Subject: [PATCH 3/4] modify with_null check --- library/core/src/ffi/c_str.rs | 45 ++++++++++++++++------------------- 1 file changed, 21 insertions(+), 24 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index bc3ec49c0de1..033bfadcde12 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -883,34 +883,31 @@ mod verify { } } + // pub const fn from_bytes_with_nul(bytes: &[u8]) -> Result<&Self, FromBytesWithNulError> #[kani::proof] - #[kani::unwind(33)] + #[kani::unwind(17)] fn check_from_bytes_with_nul() { - const MAX_SIZE: usize = 32; - let mut buffer: [u8; MAX_SIZE] = kani::any(); - - // Iterate over all possible slice lengths from 1 to MAX_SIZE - for slice_length in 1..=MAX_SIZE { - // Ensure the slice is valid by setting the last byte to null - buffer[slice_length - 1] = 0; - - // Assume all bytes before the last are non-null - for i in 0..slice_length - 1 { - kani::assume(buffer[i] != 0); - } - - // Create the slice up to the current slice_length - let slice = &buffer[..slice_length]; - let result = CStr::from_bytes_with_nul(slice); - - if let Ok(c_str) = result { - assert!(c_str.is_safe()); - assert_eq!(c_str.to_bytes(), &buffer[..slice_length - 1]); - assert_eq!(c_str.to_bytes_with_nul(), &buffer[..slice_length]); - } + const MAX_SIZE: usize = 16; + let mut string: [u8; MAX_SIZE] = kani::any(); + let null_pos: usize = kani::any_where(|x| *x < MAX_SIZE); + + string[null_pos] = 0; + // check to make sure all bytes are non null + for i in 0..null_pos { + string[i] = kani::any_where(|x| *x != 0); } + + let slice = &string[..=null_pos]; + let result = CStr::from_bytes_with_nul(slice); + assert!(result.is_ok()); + + let c_str = result.unwrap(); + assert!(c_str.is_safe()); + // additional checks + assert_eq!(c_str.to_bytes_with_nul(), slice); + assert_eq!(c_str.to_bytes(), &slice[..slice.len() - 1]); } - + // pub const fn count_bytes(&self) -> usize #[kani::proof] #[kani::unwind(32)] From 89769223217c33ab627bb052c1a9cbc4a90db7e3 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Mon, 2 Dec 2024 14:52:47 -0800 Subject: [PATCH 4/4] Update c_str.rs --- library/core/src/ffi/c_str.rs | 26 +++++++------------------- 1 file changed, 7 insertions(+), 19 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 1cfcad083617..22dcbdd83474 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -886,29 +886,17 @@ mod verify { } } - // pub const fn from_bytes_with_nul(bytes: &[u8]) -> Result<&Self, FromBytesWithNulError> #[kani::proof] - #[kani::unwind(17)] + #[kani::unwind(17)] fn check_from_bytes_with_nul() { const MAX_SIZE: usize = 16; - let mut string: [u8; MAX_SIZE] = kani::any(); - let null_pos: usize = kani::any_where(|x| *x < MAX_SIZE); - - string[null_pos] = 0; - // check to make sure all bytes are non null - for i in 0..null_pos { - string[i] = kani::any_where(|x| *x != 0); - } - - let slice = &string[..=null_pos]; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + let result = CStr::from_bytes_with_nul(slice); - assert!(result.is_ok()); - - let c_str = result.unwrap(); - assert!(c_str.is_safe()); - // additional checks - assert_eq!(c_str.to_bytes_with_nul(), slice); - assert_eq!(c_str.to_bytes(), &slice[..slice.len() - 1]); + if let Ok(c_str) = result { + assert!(c_str.is_safe()); + } } // pub const fn count_bytes(&self) -> usize