From 64ddbfffb110777c62408b642ec554a808474fd9 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Wed, 27 Nov 2024 00:00:07 -0800 Subject: [PATCH 1/2] 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 74153adc68bd5c9d7a280c8f0ce779d0846505cd Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Wed, 27 Nov 2024 19:03:36 -0800 Subject: [PATCH 2/2] Add arbitrary_cstr && Modify harnesses --- library/core/src/ffi/c_str.rs | 41 +++++++++++++++++++---------------- 1 file changed, 22 insertions(+), 19 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 176a760303940..9d2122413b0fd 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -859,6 +859,15 @@ impl FusedIterator for Bytes<'_> {} #[unstable(feature = "kani", issue = "none")] mod verify { use super::*; + + // Helper function + fn arbitrary_cstr(slice: &[u8]) -> &CStr { + let result = CStr::from_bytes_until_nul(&slice); + kani::assume(result.is_ok()); + let c_str = result.unwrap(); + assert!(c_str.is_safe()); + c_str + } // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> #[kani::proof] @@ -883,34 +892,28 @@ 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 { - // 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()); - } + let bytes = c_str.to_bytes(); + let end_idx = bytes.len(); + // Comparison does not include the null byte + assert_eq!(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 + #[kani::unwind(33)] 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 c_str = arbitrary_cstr(slice); - 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()); - } + let bytes = c_str.to_bytes_with_nul(); + let end_idx = bytes.len(); + // Comparison includes the null byte + assert_eq!(bytes, &slice[..end_idx]); + assert!(c_str.is_safe()); } } \ No newline at end of file