From 64ddbfffb110777c62408b642ec554a808474fd9 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Wed, 27 Nov 2024 00:00:07 -0800 Subject: [PATCH 1/7] Add to_bytes and to_bytes_with_nul harnesses --- library/core/src/ffi/c_str.rs | 38 +++++++++++++++++++++++++++++++++++ 1 file changed, 38 insertions(+) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 2a65b2415f7d3..176a760303940 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -875,4 +875,42 @@ mod verify { assert!(c_str.is_safe()); } } + + // pub const fn to_bytes(&self) -> &[u8] + #[kani::proof] + #[kani::unwind(32)] + fn check_to_bytes() { + const MAX_SIZE: usize = 32; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + + let result = CStr::from_bytes_until_nul(slice); + if let Ok(c_str) = result { + // Find the index of the first null byte in the slice since + // from_bytes_until_nul stops by there + let end_idx = slice.iter().position(|x| *x == 0).unwrap(); + // Comparison does not include the null byte + assert_eq!(c_str.to_bytes(), &slice[..end_idx]); + assert!(c_str.is_safe()); + } + } + + // pub const fn to_bytes_with_nul(&self) -> &[u8] + #[kani::proof] + #[kani::unwind(33)] // 101.7 seconds when 33; 17.9 seconds for 17 + fn check_to_bytes_with_nul() { + const MAX_SIZE: usize = 32; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + + let result = CStr::from_bytes_until_nul(slice); + if let Ok(c_str) = result { + // Find the index of the first null byte in the slice since + // from_bytes_until_nul stops by there + let end_idx = slice.iter().position(|x| *x == 0).unwrap(); + // Comparison includes the null byte + assert_eq!(c_str.to_bytes_with_nul(), &slice[..end_idx + 1]); + assert!(c_str.is_safe()); + } + } } \ No newline at end of file From 8b15d35ea25e8f946ef7ce27768c5514cb343033 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Wed, 27 Nov 2024 20:24:03 -0800 Subject: [PATCH 2/7] add bytes, to_str and as_ptr proofs --- library/core/src/ffi/c_str.rs | 72 ++++++++++++++++++++++++++++++++++- 1 file changed, 70 insertions(+), 2 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 176a760303940..f129a4dfafbde 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -860,7 +860,7 @@ impl FusedIterator for Bytes<'_> {} mod verify { use super::*; - // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> + pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> #[kani::proof] #[kani::unwind(32)] // 7.3 seconds when 16; 33.1 seconds when 32 fn check_from_bytes_until_nul() { @@ -913,4 +913,72 @@ mod verify { assert!(c_str.is_safe()); } } -} \ No newline at end of file + + // pub fn bytes(&self) -> Bytes<'_> + #[kani::proof] + #[kani::unwind(32)] + fn check_bytes() { + const MAX_SIZE: usize = 32; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + + let result = CStr::from_bytes_until_nul(slice); + if let Ok(c_str) = result { + let bytes_iterator = c_str.bytes(); + let bytes_expected = c_str.to_bytes(); + + // Compare the bytes obtained from the iterator and the slice + // bytes_expected.iter().copied() converts the slice into an iterator over u8 + assert!(bytes_iterator.eq(bytes_expected.iter().copied())); + + assert!(c_str.is_safe()); + } + } + + // pub const fn to_str(&self) -> Result<&str, str::Utf8Error> + #[kani::proof] + #[kani::unwind(32)] + fn check_to_str() { + const MAX_SIZE: usize = 32; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + + let result = CStr::from_bytes_until_nul(slice); + if let Ok(c_str) = result { + // a double conversion here and assertion, if the bytes are still the same, function is valid + let str_result = c_str.to_str(); + if let Ok(s) = str_result { + assert_eq!(s.as_bytes(), c_str.to_bytes()); + } + assert!(c_str.is_safe()); + } + } + + // pub const fn as_ptr(&self) -> *const c_char + #[kani::proof] + #[kani::unwind(33)] + fn check_as_ptr() { + const MAX_SIZE: usize = 32; + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + + let result = CStr::from_bytes_until_nul(slice); + if let Ok(c_str) = result { + let ptr = c_str.as_ptr(); + let len = c_str.to_bytes_with_nul().len(); + + // We ensure that `ptr` is valid for reads of `len` bytes + unsafe { + for i in 0..len { + // Iterate and get each byte in the C string from our raw ptr + let byte_at_ptr = *ptr.add(i); + // Get the byte at every pos from the to_bytes_with_nul method + let byte_in_cstr = c_str.to_bytes_with_nul()[i]; + // Compare the two bytes to ensure they are equal + assert_eq!(byte_at_ptr as u8, byte_in_cstr); + } + } + assert!(c_str.is_safe()); + } + } +} From ec0e94c6e2b8386efbccb0188ca7b04463d30f50 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Wed, 27 Nov 2024 20:25:03 -0800 Subject: [PATCH 3/7] Update c_str.rs --- library/core/src/ffi/c_str.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index f129a4dfafbde..d5f59fe38a84b 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -860,7 +860,7 @@ impl FusedIterator for Bytes<'_> {} mod verify { use super::*; - pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> + // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> #[kani::proof] #[kani::unwind(32)] // 7.3 seconds when 16; 33.1 seconds when 32 fn check_from_bytes_until_nul() { From 8b53c8c672c2f8c8d661babe8913dd9363610844 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Wed, 27 Nov 2024 22:42:04 -0800 Subject: [PATCH 4/7] Remove irrelevant code --- library/core/src/ffi/c_str.rs | 38 ----------------------------------- 1 file changed, 38 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index d5f59fe38a84b..7e56c13f7739e 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -876,44 +876,6 @@ mod verify { } } - // pub const fn to_bytes(&self) -> &[u8] - #[kani::proof] - #[kani::unwind(32)] - fn check_to_bytes() { - const MAX_SIZE: usize = 32; - let string: [u8; MAX_SIZE] = kani::any(); - let slice = kani::slice::any_slice_of_array(&string); - - let result = CStr::from_bytes_until_nul(slice); - if let Ok(c_str) = result { - // Find the index of the first null byte in the slice since - // from_bytes_until_nul stops by there - let end_idx = slice.iter().position(|x| *x == 0).unwrap(); - // Comparison does not include the null byte - assert_eq!(c_str.to_bytes(), &slice[..end_idx]); - assert!(c_str.is_safe()); - } - } - - // pub const fn to_bytes_with_nul(&self) -> &[u8] - #[kani::proof] - #[kani::unwind(33)] // 101.7 seconds when 33; 17.9 seconds for 17 - fn check_to_bytes_with_nul() { - const MAX_SIZE: usize = 32; - let string: [u8; MAX_SIZE] = kani::any(); - let slice = kani::slice::any_slice_of_array(&string); - - let result = CStr::from_bytes_until_nul(slice); - if let Ok(c_str) = result { - // Find the index of the first null byte in the slice since - // from_bytes_until_nul stops by there - let end_idx = slice.iter().position(|x| *x == 0).unwrap(); - // Comparison includes the null byte - assert_eq!(c_str.to_bytes_with_nul(), &slice[..end_idx + 1]); - assert!(c_str.is_safe()); - } - } - // pub fn bytes(&self) -> Bytes<'_> #[kani::proof] #[kani::unwind(32)] From c227b1676cd909ddb62af8f4a05f0cfa51668e69 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Thu, 28 Nov 2024 02:25:41 -0800 Subject: [PATCH 5/7] fix performance --- library/core/src/ffi/c_str.rs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 7e56c13f7739e..60a478a72f1dc 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -927,15 +927,16 @@ mod verify { let result = CStr::from_bytes_until_nul(slice); if let Ok(c_str) = result { let ptr = c_str.as_ptr(); - let len = c_str.to_bytes_with_nul().len(); + let bytes_with_nul = c_str.to_bytes_with_nul(); + let len = bytes_with_nul.len(); // We ensure that `ptr` is valid for reads of `len` bytes unsafe { for i in 0..len { // Iterate and get each byte in the C string from our raw ptr let byte_at_ptr = *ptr.add(i); - // Get the byte at every pos from the to_bytes_with_nul method - let byte_in_cstr = c_str.to_bytes_with_nul()[i]; + // Get the byte at every pos + let byte_in_cstr = bytes_with_nul[i]; // Compare the two bytes to ensure they are equal assert_eq!(byte_at_ptr as u8, byte_in_cstr); } From ddf3475b20a55b1929660cfb0412813e794f6cb5 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Thu, 28 Nov 2024 02:26:30 -0800 Subject: [PATCH 6/7] Update c_str.rs --- library/core/src/ffi/c_str.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 60a478a72f1dc..e35d306f747b1 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -860,7 +860,7 @@ impl FusedIterator for Bytes<'_> {} mod verify { use super::*; - // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> + // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> #[kani::proof] #[kani::unwind(32)] // 7.3 seconds when 16; 33.1 seconds when 32 fn check_from_bytes_until_nul() { From 7372ed648b50ef66d2d819059ac0bc28b77cb231 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Mon, 2 Dec 2024 22:28:32 -0800 Subject: [PATCH 7/7] use arbitrary str --- library/core/src/ffi/c_str.rs | 63 ++++++++++++++++------------------- 1 file changed, 28 insertions(+), 35 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 81ae8a95d66a0..d129adf2b3763 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -893,18 +893,15 @@ mod verify { const MAX_SIZE: usize = 32; let string: [u8; MAX_SIZE] = kani::any(); let slice = kani::slice::any_slice_of_array(&string); + let c_str = arbitrary_cstr(slice); - let result = CStr::from_bytes_until_nul(slice); - if let Ok(c_str) = result { - let bytes_iterator = c_str.bytes(); - let bytes_expected = c_str.to_bytes(); - - // Compare the bytes obtained from the iterator and the slice - // bytes_expected.iter().copied() converts the slice into an iterator over u8 - assert!(bytes_iterator.eq(bytes_expected.iter().copied())); + let bytes_iterator = c_str.bytes(); + let bytes_expected = c_str.to_bytes(); - assert!(c_str.is_safe()); - } + // Compare the bytes obtained from the iterator and the slice + // bytes_expected.iter().copied() converts the slice into an iterator over u8 + assert!(bytes_iterator.eq(bytes_expected.iter().copied())); + assert!(c_str.is_safe()); } // pub const fn to_str(&self) -> Result<&str, str::Utf8Error> @@ -914,16 +911,14 @@ mod verify { const MAX_SIZE: usize = 32; let string: [u8; MAX_SIZE] = kani::any(); let slice = kani::slice::any_slice_of_array(&string); + let c_str = arbitrary_cstr(slice); - let result = CStr::from_bytes_until_nul(slice); - if let Ok(c_str) = result { - // a double conversion here and assertion, if the bytes are still the same, function is valid - let str_result = c_str.to_str(); - if let Ok(s) = str_result { - assert_eq!(s.as_bytes(), c_str.to_bytes()); - } - assert!(c_str.is_safe()); + // a double conversion here and assertion, if the bytes are still the same, function is valid + let str_result = c_str.to_str(); + if let Ok(s) = str_result { + assert_eq!(s.as_bytes(), c_str.to_bytes()); } + assert!(c_str.is_safe()); } // pub const fn as_ptr(&self) -> *const c_char @@ -933,26 +928,24 @@ mod verify { const MAX_SIZE: usize = 32; let string: [u8; MAX_SIZE] = kani::any(); let slice = kani::slice::any_slice_of_array(&string); + let c_str = arbitrary_cstr(slice); - let result = CStr::from_bytes_until_nul(slice); - if let Ok(c_str) = result { - let ptr = c_str.as_ptr(); - let bytes_with_nul = c_str.to_bytes_with_nul(); - let len = bytes_with_nul.len(); - - // We ensure that `ptr` is valid for reads of `len` bytes - unsafe { - for i in 0..len { - // Iterate and get each byte in the C string from our raw ptr - let byte_at_ptr = *ptr.add(i); - // Get the byte at every pos - let byte_in_cstr = bytes_with_nul[i]; - // Compare the two bytes to ensure they are equal - assert_eq!(byte_at_ptr as u8, byte_in_cstr); - } + let ptr = c_str.as_ptr(); + let bytes_with_nul = c_str.to_bytes_with_nul(); + let len = bytes_with_nul.len(); + + // We ensure that `ptr` is valid for reads of `len` bytes + unsafe { + for i in 0..len { + // Iterate and get each byte in the C string from our raw ptr + let byte_at_ptr = *ptr.add(i); + // Get the byte at every pos + let byte_in_cstr = bytes_with_nul[i]; + // Compare the two bytes to ensure they are equal + assert_eq!(byte_at_ptr as u8, byte_in_cstr); } - assert!(c_str.is_safe()); } + assert!(c_str.is_safe()); } // pub const fn count_bytes(&self) -> usize