From 64ddbfffb110777c62408b642ec554a808474fd9 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Wed, 27 Nov 2024 00:00:07 -0800 Subject: [PATCH 01/19] 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 02/19] 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 03/19] 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 e70a1efbdf087558de4f158537c5e203c3552326 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Wed, 27 Nov 2024 22:12:30 -0800 Subject: [PATCH 04/19] add harness for `from_ptr`, `from_bytes_with_nul_unchecked`, `strlen` . And stub for strlen + better documentation --- library/core/src/ffi/c_str.rs | 89 ++++++++++++++++++++++++++++++++--- 1 file changed, 83 insertions(+), 6 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index d5f59fe38a84b..bb129bdd95329 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> + // Proof harness for 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() { @@ -876,7 +876,7 @@ mod verify { } } - // pub const fn to_bytes(&self) -> &[u8] + // Proof harness for pub const fn to_bytes(&self) -> &[u8] #[kani::proof] #[kani::unwind(32)] fn check_to_bytes() { @@ -895,7 +895,7 @@ mod verify { } } - // pub const fn to_bytes_with_nul(&self) -> &[u8] + // Proof harness for 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() { @@ -914,7 +914,7 @@ mod verify { } } - // pub fn bytes(&self) -> Bytes<'_> + // Proof harness for pub fn bytes(&self) -> Bytes<'_> #[kani::proof] #[kani::unwind(32)] fn check_bytes() { @@ -935,7 +935,7 @@ mod verify { } } - // pub const fn to_str(&self) -> Result<&str, str::Utf8Error> + // Proof harness for pub const fn to_str(&self) -> Result<&str, str::Utf8Error> #[kani::proof] #[kani::unwind(32)] fn check_to_str() { @@ -954,7 +954,7 @@ mod verify { } } - // pub const fn as_ptr(&self) -> *const c_char + // Proof harness for pub const fn as_ptr(&self) -> *const c_char #[kani::proof] #[kani::unwind(33)] fn check_as_ptr() { @@ -981,4 +981,81 @@ mod verify { assert!(c_str.is_safe()); } } + + // Stub implementation for strlen --> https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html + #[cfg(kani)] + unsafe fn stub_strlen(s: *const c_char) -> usize { + let mut len = 0; + unsafe { + while *s.add(len) != 0 { + len += 1; + } + } + len + } + + // Proof harness for pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr + #[cfg(kani)] + #[kani::proof] + #[kani::unwind(33)] + #[kani::stub(strlen, stub_strlen)] + fn check_from_ptr() { + const MAX_SIZE: usize = 32; + //generating an arbitrary byte array with a max size + let mut string: [u8; MAX_SIZE] = kani::any(); + // need At least one nul terminator is present within the array + let nul_position = kani::any::() % MAX_SIZE; + string[nul_position] = 0; + // Make sure that there are no other nul bytes before `nul_position` + for i in 0..nul_position { + kani::assume(string[i] != 0); + } + // start from the beginning of the string + let ptr = string.as_ptr().cast::(); + let c_str = unsafe { CStr::from_ptr(ptr) }; + // Compute the expected length up to the nul terminator + let len = unsafe { strlen(ptr) }; + // Check that `c_str` has the correct length + assert_eq!(c_str.to_bytes().len(), len); + assert!(c_str.is_safe()); + } + + // Proof harness for const unsafe fn strlen(ptr: *const c_char) -> usize + #[cfg(kani)] + #[kani::proof] + #[kani::unwind(32)] + #[kani::stub(strlen, stub_strlen)] + fn check_strlen() { + const MAX_SIZE: usize = 32; + let mut string: [u8; MAX_SIZE] = kani::any(); + let nul_position = kani::any::() % MAX_SIZE; + string[nul_position] = 0; + // Make sure that there are no other nul bytes before `nul_position` + for i in 0..nul_position { + kani::assume(string[i] != 0); + } + let ptr = string.as_ptr().cast::(); + // Call strlen with the pointer + let len = unsafe { strlen(ptr) }; + // Check that len matches the expected position of the nul terminator + assert_eq!(len, nul_position); + } + + // Proof harness for fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr + #[kani::proof] + #[kani::unwind(32)] + fn check_from_bytes_with_nul_unchecked() { + const MAX_SIZE: usize = 32; + let mut bytes: [u8; MAX_SIZE] = kani::any(); + bytes[MAX_SIZE - 1] = 0; + // Ensure that there are no nul bytes in the rest of the array + for i in 0..(MAX_SIZE - 1) { + kani::assume(bytes[i] != 0); + } + // Create a slice including the nul terminator + let slice = &bytes[..]; + // Call from_bytes_with_nul_unchecked with the slice + let c_str = unsafe { CStr::from_bytes_with_nul_unchecked(slice) }; + assert!(c_str.is_safe()); + } } From 7ddf9decb82b62ac9a6f33486b160761a44dbc10 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Wed, 27 Nov 2024 22:39:24 -0800 Subject: [PATCH 05/19] Fix contracts and harnesses --- library/core/src/ffi/c_str.rs | 144 ++++++---------------------------- 1 file changed, 22 insertions(+), 122 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index bb129bdd95329..9e217067ad5f7 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -10,6 +10,7 @@ use crate::slice::memchr; use crate::{fmt, intrinsics, ops, slice, str}; use crate::ub_checks::Invariant; +use safety::{requires, ensures}; #[cfg(kani)] use crate::kani; @@ -431,6 +432,10 @@ impl CStr { #[stable(feature = "cstr_from_bytes", since = "1.10.0")] #[rustc_const_stable(feature = "const_cstr_unchecked", since = "1.59.0")] #[rustc_allow_const_fn_unstable(const_eval_select)] + // Preconditions: Null-terminated and no intermediate null bytes + #[requires(!bytes.is_empty() && bytes[bytes.len() - 1] == 0 && !bytes[..bytes.len()-1].contains(&0))] + // Postcondition: The resulting CStr satisfies the same conditions as preconditions + #[ensures(|result| result.is_safe())] pub const unsafe fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr { #[inline] fn rt_impl(bytes: &[u8]) -> &CStr { @@ -876,113 +881,7 @@ mod verify { } } - // Proof harness for 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()); - } - } - - // Proof harness for 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()); - } - } - - // Proof harness for 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()); - } - } - - // Proof harness for 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()); - } - } - - // Proof harness for 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()); - } - } - - // Stub implementation for strlen --> https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html + // Stub implementation for strlen: https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html #[cfg(kani)] unsafe fn stub_strlen(s: *const c_char) -> usize { let mut len = 0; @@ -1004,7 +903,7 @@ mod verify { //generating an arbitrary byte array with a max size let mut string: [u8; MAX_SIZE] = kani::any(); // need At least one nul terminator is present within the array - let nul_position = kani::any::() % MAX_SIZE; + let nul_position: usize = kani::any_where(|x| *x >= 0 && *x < MAX_SIZE); string[nul_position] = 0; // Make sure that there are no other nul bytes before `nul_position` for i in 0..nul_position { @@ -1028,7 +927,7 @@ mod verify { fn check_strlen() { const MAX_SIZE: usize = 32; let mut string: [u8; MAX_SIZE] = kani::any(); - let nul_position = kani::any::() % MAX_SIZE; + let nul_position: usize = kani::any_where(|x| *x >= 0 && *x < MAX_SIZE); string[nul_position] = 0; // Make sure that there are no other nul bytes before `nul_position` for i in 0..nul_position { @@ -1041,21 +940,22 @@ mod verify { assert_eq!(len, nul_position); } - // Proof harness for fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr - #[kani::proof] - #[kani::unwind(32)] + // pub const unsafe fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr + #[kani::proof_for_contract(CStr::from_bytes_with_nul_unchecked)] + #[kani::unwind(33)] fn check_from_bytes_with_nul_unchecked() { const MAX_SIZE: usize = 32; - let mut bytes: [u8; MAX_SIZE] = kani::any(); - bytes[MAX_SIZE - 1] = 0; - // Ensure that there are no nul bytes in the rest of the array - for i in 0..(MAX_SIZE - 1) { - kani::assume(bytes[i] != 0); - } - // Create a slice including the nul terminator - let slice = &bytes[..]; - // Call from_bytes_with_nul_unchecked with the slice + let string: [u8; MAX_SIZE] = kani::any(); + let slice = kani::slice::any_slice_of_array(&string); + + // Kani assumes that the input slice is null-terminated and contains + // no intermediate null bytes let c_str = unsafe { CStr::from_bytes_with_nul_unchecked(slice) }; - assert!(c_str.is_safe()); + // Kani ensures that the output CStr holds the CStr safety invariant + + // Correctness check + let bytes = c_str.to_bytes(); + let len = bytes.len(); + assert_eq!(bytes, &slice[..len]); } } From 0a372c16c772c84308b3477e3ae1d5014706e439 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Sat, 30 Nov 2024 19:47:26 -0800 Subject: [PATCH 06/19] update stubbing and const proof --- library/core/src/ffi/c_str.rs | 156 +++++++++++++++++++++------------- 1 file changed, 97 insertions(+), 59 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index fe8b89a174af1..b37958171f276 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -760,6 +760,33 @@ impl AsRef for CStr { #[unstable(feature = "cstr_internals", issue = "none")] #[cfg_attr(bootstrap, rustc_const_stable(feature = "const_cstr_from_ptr", since = "1.81.0"))] #[rustc_allow_const_fn_unstable(const_eval_select)] +// Preconditions: +// - ptr must be non-null +// - ptr must point to a valid null-terminated string +// - null terminator must be within isize::MAX bytes from ptr +#[requires(!ptr.is_null() && { + let mut found_null = false; + for i in 0..isize::MAX as usize { + if unsafe { *ptr.add(i) } == 0 { + found_null = true; + break; + } + } + found_null +})] +// Postconditions: +// - Returns length before null terminator +// - Length must be less than isize::MAX +#[ensures(|&result| result < isize::MAX as usize && { + let mut valid = true; + for i in 0..result { + if unsafe { *ptr.add(i) } == 0 { + valid = false; + break; + } + } + valid && unsafe { *ptr.add(result) } == 0 +})] const unsafe fn strlen(ptr: *const c_char) -> usize { const_eval_select!( @capture { s: *const c_char = ptr } -> usize: @@ -888,65 +915,6 @@ mod verify { } } - // Stub implementation for strlen: https://model-checking.github.io/kani/rfc/rfcs/0002-function-stubbing.html - #[cfg(kani)] - unsafe fn stub_strlen(s: *const c_char) -> usize { - let mut len = 0; - unsafe { - while *s.add(len) != 0 { - len += 1; - } - } - len - } - - // Proof harness for pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr - #[cfg(kani)] - #[kani::proof] - #[kani::unwind(33)] - #[kani::stub(strlen, stub_strlen)] - fn check_from_ptr() { - const MAX_SIZE: usize = 32; - //generating an arbitrary byte array with a max size - let mut string: [u8; MAX_SIZE] = kani::any(); - // need At least one nul terminator is present within the array - let nul_position: usize = kani::any_where(|x| *x >= 0 && *x < MAX_SIZE); - string[nul_position] = 0; - // Make sure that there are no other nul bytes before `nul_position` - for i in 0..nul_position { - kani::assume(string[i] != 0); - } - // start from the beginning of the string - let ptr = string.as_ptr().cast::(); - let c_str = unsafe { CStr::from_ptr(ptr) }; - // Compute the expected length up to the nul terminator - let len = unsafe { strlen(ptr) }; - // Check that `c_str` has the correct length - assert_eq!(c_str.to_bytes().len(), len); - assert!(c_str.is_safe()); - } - - // Proof harness for const unsafe fn strlen(ptr: *const c_char) -> usize - #[cfg(kani)] - #[kani::proof] - #[kani::unwind(32)] - #[kani::stub(strlen, stub_strlen)] - fn check_strlen() { - const MAX_SIZE: usize = 32; - let mut string: [u8; MAX_SIZE] = kani::any(); - let nul_position: usize = kani::any_where(|x| *x >= 0 && *x < MAX_SIZE); - string[nul_position] = 0; - // Make sure that there are no other nul bytes before `nul_position` - for i in 0..nul_position { - kani::assume(string[i] != 0); - } - let ptr = string.as_ptr().cast::(); - // Call strlen with the pointer - let len = unsafe { strlen(ptr) }; - // Check that len matches the expected position of the nul terminator - assert_eq!(len, nul_position); - } - // pub const unsafe fn from_bytes_with_nul_unchecked(bytes: &[u8]) -> &CStr #[kani::proof_for_contract(CStr::from_bytes_with_nul_unchecked)] #[kani::unwind(33)] @@ -1022,5 +990,75 @@ mod verify { assert_eq!(bytes, &slice[..end_idx]); assert!(c_str.is_safe()); } + + + // Stub for external C strlen + #[allow(dead_code)] + mod stubs { + use super::*; + + #[no_mangle] + pub unsafe extern "C" fn strlen(s: *const c_char) -> usize { + 4 + } + } + + // Proof harness that uses the const-evaluated length + #[kani::proof_for_contract(strlen)] + #[kani::unwind(32)] + fn check_strlen_const_path() { + // Get the compile-time computed length + const BYTES: &[u8] = b"test\0"; + const PTR: *const c_char = BYTES.as_ptr() as *const c_char; + + // This must be evaluated at compile time + const COMPUTED_LEN: usize = unsafe { strlen(PTR) }; + + // Verify the const-computed length + assert_eq!(COMPUTED_LEN, 4); + + // Additional compile-time verifications + const BYTES1: &[u8] = b"test\0"; + const PTR1: *const c_char = BYTES1.as_ptr() as *const c_char; + + // Verify the string properties using the const-computed length + unsafe { + // These assertions will use the const-computed values + assert_eq!(*PTR1.add(COMPUTED_LEN), 0); + + let mut i = 0; + while i < COMPUTED_LEN { + assert_ne!(*PTR1.add(i), 0); + i += 1; + } + } + } + + /// **Proof Harness for External `strlen` Function with Stubbing** + /// + /// This harness should verify that the `else` block of the cstr `strlen` function + /// correctly interacts with the external `strlen` function, which is stubbed. + #[kani::proof] + #[kani::stub(strlen, stubs::strlen)] + fn check_external_strlen() { + const MAX_SIZE: usize = 32; + let mut string: [u8; MAX_SIZE] = kani::any(); + + // Generate position for null terminator + let nul_position: usize = kani::any_where(|x| *x > 0 && *x < MAX_SIZE); + string[nul_position] = 0; + + // Ensure no null bytes before nul_position + for i in 0..nul_position { + kani::assume(string[i] != 0); + } + + let ptr = string.as_ptr() as *const c_char; + unsafe { + let len = strlen(ptr); + // Verify stub returns fixed value 4 + assert_eq!(len, 4); + } + } } From e323bf30c603c33757dcb769ad01ea2fbda029c3 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Sat, 30 Nov 2024 20:47:41 -0800 Subject: [PATCH 07/19] update stub and cstr compile time proof --- library/core/src/ffi/c_str.rs | 34 +++++++++++++++++----------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index b37958171f276..1b5594b09135c 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -991,20 +991,9 @@ mod verify { assert!(c_str.is_safe()); } - - // Stub for external C strlen - #[allow(dead_code)] - mod stubs { - use super::*; - - #[no_mangle] - pub unsafe extern "C" fn strlen(s: *const c_char) -> usize { - 4 - } - } - // Proof harness that uses the const-evaluated length - #[kani::proof_for_contract(strlen)] + // #[kani::proof_for_contract(strlen)] + #[kani::proof] #[kani::unwind(32)] fn check_strlen_const_path() { // Get the compile-time computed length @@ -1034,10 +1023,21 @@ mod verify { } } - /// **Proof Harness for External `strlen` Function with Stubbing** - /// - /// This harness should verify that the `else` block of the cstr `strlen` function - /// correctly interacts with the external `strlen` function, which is stubbed. + Stub for external C strlen + #[allow(dead_code)] + mod stubs { + use super::*; + + #[no_mangle] + pub unsafe extern "C" fn strlen(s: *const c_char) -> usize { + 4 + } + } + + // **Proof Harness for External `strlen` Function with Stubbing** + // + // This harness should verify that the `else` block of the cstr `strlen` function + // correctly interacts with the external `strlen` function, which is stubbed. #[kani::proof] #[kani::stub(strlen, stubs::strlen)] fn check_external_strlen() { From e054f35d5f0a5915b084d9679fccf674bc82a5a5 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Sat, 30 Nov 2024 21:09:17 -0800 Subject: [PATCH 08/19] comment --- 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 1b5594b09135c..5e7914f229101 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -1023,7 +1023,7 @@ mod verify { } } - Stub for external C strlen + // Stub for external C strlen #[allow(dead_code)] mod stubs { use super::*; From 8b95cb1ee6630a861c0841748501793f866ec326 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Sun, 1 Dec 2024 19:57:51 -0800 Subject: [PATCH 09/19] update cstr strlen --- library/core/src/ffi/c_str.rs | 74 +++++++++-------------------------- 1 file changed, 18 insertions(+), 56 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 5e7914f229101..d8096c4607b80 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -991,73 +991,35 @@ mod verify { assert!(c_str.is_safe()); } - // Proof harness that uses the const-evaluated length - // #[kani::proof_for_contract(strlen)] - #[kani::proof] + #[kani::proof_for_contract(super::strlen)] #[kani::unwind(32)] - fn check_strlen_const_path() { - // Get the compile-time computed length - const BYTES: &[u8] = b"test\0"; - const PTR: *const c_char = BYTES.as_ptr() as *const c_char; - - // This must be evaluated at compile time - const COMPUTED_LEN: usize = unsafe { strlen(PTR) }; - - // Verify the const-computed length - assert_eq!(COMPUTED_LEN, 4); - - // Additional compile-time verifications - const BYTES1: &[u8] = b"test\0"; - const PTR1: *const c_char = BYTES1.as_ptr() as *const c_char; - - // Verify the string properties using the const-computed length - unsafe { - // These assertions will use the const-computed values - assert_eq!(*PTR1.add(COMPUTED_LEN), 0); - - let mut i = 0; - while i < COMPUTED_LEN { - assert_ne!(*PTR1.add(i), 0); - i += 1; - } - } - } - - // Stub for external C strlen - #[allow(dead_code)] - mod stubs { - use super::*; - - #[no_mangle] - pub unsafe extern "C" fn strlen(s: *const c_char) -> usize { - 4 - } - } - - // **Proof Harness for External `strlen` Function with Stubbing** - // - // This harness should verify that the `else` block of the cstr `strlen` function - // correctly interacts with the external `strlen` function, which is stubbed. - #[kani::proof] - #[kani::stub(strlen, stubs::strlen)] - fn check_external_strlen() { + fn check_strlen_contract() { const MAX_SIZE: usize = 32; let mut string: [u8; MAX_SIZE] = kani::any(); - - // Generate position for null terminator - let nul_position: usize = kani::any_where(|x| *x > 0 && *x < MAX_SIZE); + let nul_position: usize = kani::any_where(|x| *x < MAX_SIZE); string[nul_position] = 0; // Ensure no null bytes before nul_position for i in 0..nul_position { kani::assume(string[i] != 0); } - + let ptr = string.as_ptr() as *const c_char; + unsafe { - let len = strlen(ptr); - // Verify stub returns fixed value 4 - assert_eq!(len, 4); + let len = super::strlen(ptr); + + // Length must be less than isize::MAX + assert!(len < isize::MAX as usize); + // Length must equal nul_position + assert_eq!(len, nul_position); + // no null in between + for i in 0..len { + assert!(*ptr.add(i) != 0); + } + // additional checks + assert_eq!(*ptr.add(len), 0); + assert!(len <= MAX_SIZE - 1); } } } From c54a51e6264ea7f05c8434e71e19651f26f16d5d Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Mon, 2 Dec 2024 15:38:48 -0800 Subject: [PATCH 10/19] Update c_str.rs --- library/core/src/ffi/c_str.rs | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index b2396fa290859..aaeb4275e83f7 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -766,13 +766,19 @@ impl AsRef for CStr { // - null terminator must be within isize::MAX bytes from ptr #[requires(!ptr.is_null() && { let mut found_null = false; + let mut valid = true; for i in 0..isize::MAX as usize { if unsafe { *ptr.add(i) } == 0 { + if found_null { + // Already found a null before, so this is an extra null + valid = false; + break; + } found_null = true; break; } } - found_null + found_null && valid })] // Postconditions: // - Returns length before null terminator @@ -994,6 +1000,7 @@ mod verify { assert!(c_str.is_safe()); } + // const unsafe fn strlen(ptr: *const c_char) -> usize #[kani::proof_for_contract(super::strlen)] #[kani::unwind(32)] fn check_strlen_contract() { From 00365ed26384d1a4062568b1560e34cc6726a19b Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Mon, 2 Dec 2024 23:27:54 -0800 Subject: [PATCH 11/19] update pre and post conditions --- library/core/src/ffi/c_str.rs | 35 ++++++++++++++--------------------- 1 file changed, 14 insertions(+), 21 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index aaeb4275e83f7..a0fd71f3863be 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -15,6 +15,8 @@ use safety::{requires, ensures}; #[cfg(kani)] use crate::kani; +#[cfg(kani)] +use crate::ub_checks::can_dereference; // FIXME: because this is doc(inline)d, we *have* to use intra-doc links because the actual link // depends on where the item is being documented. however, since this is libcore, we can't @@ -761,37 +763,28 @@ impl AsRef for CStr { #[cfg_attr(bootstrap, rustc_const_stable(feature = "const_cstr_from_ptr", since = "1.81.0"))] #[rustc_allow_const_fn_unstable(const_eval_select)] // Preconditions: -// - ptr must be non-null -// - ptr must point to a valid null-terminated string -// - null terminator must be within isize::MAX bytes from ptr +// - ptr must be non-null and properly aligned +// - ptr must point to a valid null-terminated string within isize::MAX bytes #[requires(!ptr.is_null() && { + let mut next = ptr; let mut found_null = false; - let mut valid = true; - for i in 0..isize::MAX as usize { - if unsafe { *ptr.add(i) } == 0 { - if found_null { - // Already found a null before, so this is an extra null - valid = false; - break; - } + while can_dereference(next) { + if unsafe { *next == 0 } { found_null = true; break; } + next = next.wrapping_add(1); } - found_null && valid + found_null })] // Postconditions: // - Returns length before null terminator // - Length must be less than isize::MAX -#[ensures(|&result| result < isize::MAX as usize && { - let mut valid = true; - for i in 0..result { - if unsafe { *ptr.add(i) } == 0 { - valid = false; - break; - } - } - valid && unsafe { *ptr.add(result) } == 0 +// - No null bytes before returned length +#[ensures(|&result| result < isize::MAX as usize && unsafe { + let slice = core::slice::from_raw_parts(ptr, result + 1); + // Check no nulls before result and null at result + !slice[..result].contains(&0) && slice[result] == 0 })] const unsafe fn strlen(ptr: *const c_char) -> usize { const_eval_select!( From b21eb00d7d5072954c6fb0a9254a444307f1da5c Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Thu, 5 Dec 2024 01:02:50 -0800 Subject: [PATCH 12/19] delimiter typo --- library/core/src/ffi/c_str.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 071b2e8725b48..ce651d5fc4bd1 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -934,6 +934,7 @@ mod verify { let bytes = c_str.to_bytes(); let len = bytes.len(); assert_eq!(bytes, &slice[..len]); + } // pub fn bytes(&self) -> Bytes<'_> #[kani::proof] @@ -1112,5 +1113,5 @@ mod verify { let expected_is_empty = bytes.len() == 0; assert_eq!(expected_is_empty, c_str.is_empty()); assert!(c_str.is_safe()); - } + } } From 3f4be6d5aacebbd6b8f7b34d99617d2c70b4f074 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Thu, 5 Dec 2024 01:36:04 -0800 Subject: [PATCH 13/19] retained only necessary checks pertaining to the function, cleaned up code --- library/core/src/ffi/c_str.rs | 70 +++++++++++------------------------ 1 file changed, 21 insertions(+), 49 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index ce651d5fc4bd1..0d276980256b0 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -232,6 +232,23 @@ impl Invariant for &CStr { } } +#[requires(!ptr.is_null())] +fn is_null_terminated(ptr: *const c_char) -> bool { + let mut next = ptr; + let mut found_null = false; + while can_dereference(next) { + if unsafe { *next == 0 } { + found_null = true; + break; + } + next = next.wrapping_add(1); + } + if (next.addr() - ptr.addr()) >= isize::MAX as usize { + return false; + } + found_null +} + impl CStr { /// Wraps a raw C string with a safe C string wrapper. /// @@ -762,30 +779,8 @@ impl AsRef for CStr { #[unstable(feature = "cstr_internals", issue = "none")] #[cfg_attr(bootstrap, rustc_const_stable(feature = "const_cstr_from_ptr", since = "1.81.0"))] #[rustc_allow_const_fn_unstable(const_eval_select)] -// Preconditions: -// - ptr must be non-null and properly aligned -// - ptr must point to a valid null-terminated string within isize::MAX bytes -#[requires(!ptr.is_null() && { - let mut next = ptr; - let mut found_null = false; - while can_dereference(next) { - if unsafe { *next == 0 } { - found_null = true; - break; - } - next = next.wrapping_add(1); - } - found_null -})] -// Postconditions: -// - Returns length before null terminator -// - Length must be less than isize::MAX -// - No null bytes before returned length -#[ensures(|&result| result < isize::MAX as usize && unsafe { - let slice = core::slice::from_raw_parts(ptr, result + 1); - // Check no nulls before result and null at result - !slice[..result].contains(&0) && slice[result] == 0 -})] +#[requires(!ptr.is_null() && is_null_terminated(ptr))] +#[ensures(|&result| result < isize::MAX as usize && unsafe { *ptr.add(result) } == 0)] const unsafe fn strlen(ptr: *const c_char) -> usize { const_eval_select!( @capture { s: *const c_char = ptr } -> usize: @@ -1070,35 +1065,12 @@ mod verify { // const unsafe fn strlen(ptr: *const c_char) -> usize #[kani::proof_for_contract(super::strlen)] - #[kani::unwind(32)] + #[kani::unwind(33)] fn check_strlen_contract() { const MAX_SIZE: usize = 32; let mut string: [u8; MAX_SIZE] = kani::any(); - let nul_position: usize = kani::any_where(|x| *x < MAX_SIZE); - string[nul_position] = 0; - - // Ensure no null bytes before nul_position - for i in 0..nul_position { - kani::assume(string[i] != 0); - } - let ptr = string.as_ptr() as *const c_char; - - unsafe { - let len = super::strlen(ptr); - - // Length must be less than isize::MAX - assert!(len < isize::MAX as usize); - // Length must equal nul_position - assert_eq!(len, nul_position); - // no null in between - for i in 0..len { - assert!(*ptr.add(i) != 0); - } - // additional checks - assert_eq!(*ptr.add(len), 0); - assert!(len <= MAX_SIZE - 1); - } + unsafe {super::strlen(ptr);} } #[kani::proof] From 53588b4e4c2f387d5a18dafbfd0cda7801ce3f0b Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Fri, 6 Dec 2024 14:15:42 -0800 Subject: [PATCH 14/19] removed redundant check --- 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 0d276980256b0..b815e67d33d20 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -779,7 +779,7 @@ impl AsRef for CStr { #[unstable(feature = "cstr_internals", issue = "none")] #[cfg_attr(bootstrap, rustc_const_stable(feature = "const_cstr_from_ptr", since = "1.81.0"))] #[rustc_allow_const_fn_unstable(const_eval_select)] -#[requires(!ptr.is_null() && is_null_terminated(ptr))] +#[requires(is_null_terminated(ptr))] #[ensures(|&result| result < isize::MAX as usize && unsafe { *ptr.add(result) } == 0)] const unsafe fn strlen(ptr: *const c_char) -> usize { const_eval_select!( From dbf278b7b4215334ae915b6932a8e741678e5b0f Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Fri, 6 Dec 2024 19:41:16 -0800 Subject: [PATCH 15/19] Fix import --- library/core/src/ffi/c_str.rs | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index b815e67d33d20..bb441d4a021f7 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -11,12 +11,11 @@ use crate::slice::memchr; use crate::{fmt, ops, slice, str}; use crate::ub_checks::Invariant; +use crate::ub_checks::can_dereference; use safety::{requires, ensures}; #[cfg(kani)] use crate::kani; -#[cfg(kani)] -use crate::ub_checks::can_dereference; // FIXME: because this is doc(inline)d, we *have* to use intra-doc links because the actual link // depends on where the item is being documented. however, since this is libcore, we can't @@ -1070,7 +1069,8 @@ mod verify { const MAX_SIZE: usize = 32; let mut string: [u8; MAX_SIZE] = kani::any(); let ptr = string.as_ptr() as *const c_char; - unsafe {super::strlen(ptr);} + + unsafe { super::strlen(ptr); } } #[kani::proof] From c5d8da33ca81d4e150e6d19a2788a151faf3fabf Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Tue, 10 Dec 2024 13:09:18 -0800 Subject: [PATCH 16/19] Fix is_null_terminated not use issue --- library/core/src/ffi/c_str.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index bb441d4a021f7..ca35a7940c907 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -231,6 +231,7 @@ impl Invariant for &CStr { } } +#[cfg(kani)] #[requires(!ptr.is_null())] fn is_null_terminated(ptr: *const c_char) -> bool { let mut next = ptr; From 0f075fcc07a6d96230d9b9078269c16cc37c3ad4 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 10 Dec 2024 16:28:06 -0500 Subject: [PATCH 17/19] Fix unused import error --- library/core/src/ffi/c_str.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index ca35a7940c907..50905c767a46c 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -11,6 +11,7 @@ use crate::slice::memchr; use crate::{fmt, ops, slice, str}; use crate::ub_checks::Invariant; +#[allow(unused_imports)] use crate::ub_checks::can_dereference; use safety::{requires, ensures}; From 2789d9530f1d7c3449d8174a4b9f15bd8c90e957 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Wed, 11 Dec 2024 10:34:28 -0800 Subject: [PATCH 18/19] Fix format && comments --- library/core/src/ffi/c_str.rs | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index de6730c38e57d..f29e125c16833 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -232,7 +232,6 @@ impl Invariant for &CStr { } } - // Helper function #[cfg(kani)] #[requires(!ptr.is_null())] @@ -901,7 +900,7 @@ mod verify { c_str } - // Proof harness for 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() { @@ -998,6 +997,7 @@ mod verify { assert!(c_str.is_safe()); } + // pub const fn from_bytes_with_nul(bytes: &[u8]) -> Result<&Self, FromBytesWithNulError> #[kani::proof] #[kani::unwind(17)] fn check_from_bytes_with_nul() { @@ -1079,6 +1079,7 @@ mod verify { unsafe { super::strlen(ptr); } } + // pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr #[kani::proof_for_contract(CStr::from_ptr)] #[kani::unwind(33)] fn check_from_ptr_contract() { @@ -1089,6 +1090,7 @@ mod verify { unsafe { CStr::from_ptr(ptr); } } + // pub const fn is_empty(&self) -> bool #[kani::proof] #[kani::unwind(33)] fn check_is_empty() { From 23c66a3c9b3556c83528506ccbe23f2731b4e59e Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Wed, 11 Dec 2024 10:35:32 -0800 Subject: [PATCH 19/19] Formatting --- 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 f29e125c16833..ef01d20b7fc38 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -900,7 +900,7 @@ mod verify { c_str } - // 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() {