From bf613a0305a0439c64a517c35edc6605caf116ed Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Thu, 21 Nov 2024 22:32:57 -0800 Subject: [PATCH 1/7] Test CStr safety invariant --- library/core/src/ffi/c_str.rs | 8 ++++++++ library/core/src/ffi/mod.rs | 26 ++++++++++++++++++++++++++ 2 files changed, 34 insertions(+) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 93dd351b02958..70c52e1cbda0c 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -9,6 +9,11 @@ use crate::ptr::NonNull; use crate::slice::memchr; use crate::{fmt, intrinsics, ops, slice, str}; +// use safety::{requires, ensures}; + +#[cfg(kani)] +use crate::kani; + // 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 // actually reference libstd or liballoc in intra-doc links. so, the best we can do is remove the @@ -100,6 +105,9 @@ use crate::{fmt, intrinsics, ops, slice, str}; // want `repr(transparent)` but we don't want it to show up in rustdoc, so we hide it under // `cfg(doc)`. This is an ad-hoc implementation of attribute privacy. #[repr(transparent)] +#[derive(kani::Arbitrary)] +#[derive(kani::Invariant)] +#[safety_constraint(inner.len() > 0 && inner[inner.len() - 1] == 0 && !inner[..inner.len() - 1].contains(&0))] pub struct CStr { // FIXME: this should not be represented with a DST slice but rather with // just a raw `c_char` along with some form of marker to make diff --git a/library/core/src/ffi/mod.rs b/library/core/src/ffi/mod.rs index dc107c5d22cdd..38b9974420bd5 100644 --- a/library/core/src/ffi/mod.rs +++ b/library/core/src/ffi/mod.rs @@ -20,6 +20,11 @@ pub use self::c_str::FromBytesUntilNulError; pub use self::c_str::FromBytesWithNulError; use crate::fmt; +use safety::{requires, ensures}; + +#[cfg(kani)] +use crate::kani; + #[unstable(feature = "c_str_module", issue = "112134")] pub mod c_str; @@ -223,3 +228,24 @@ impl fmt::Debug for c_void { )] #[link(name = "/defaultlib:libcmt", modifiers = "+verbatim", cfg(target_feature = "crt-static"))] extern "C" {} + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> + #[kani::proof] + #[kani::unwind(16)] // Proof bounded by array length + fn check_from_bytes_until_nul() { + const ARR_LEN: usize = 16; + let mut string: [u8; ARR_LEN] = kani::any(); + // ensure that there is at least one null byte + let idx: usize = kani::any_where(|x| *x >= 0 && *x < ARR_LEN); + string[idx] = 0; + + let c_str = CStr::from_bytes_until_nul(&string).unwrap(); + assert!(c_str.is_safe()); + } + +} \ No newline at end of file From 90ae7a5ccc9ac866056f5355fdf9325e5d8d6eb0 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Fri, 22 Nov 2024 13:00:28 -0800 Subject: [PATCH 2/7] Add CStr safety invariant && from_bytes_until_null harnesses --- library/core/src/ffi/c_str.rs | 67 +++++++++++++++++++++++++++++++++-- library/core/src/ffi/mod.rs | 26 -------------- 2 files changed, 64 insertions(+), 29 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 70c52e1cbda0c..5be4c2054809e 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 safety::{requires, ensures}; +use crate::ub_checks::Invariant; #[cfg(kani)] use crate::kani; @@ -105,9 +106,6 @@ use crate::kani; // want `repr(transparent)` but we don't want it to show up in rustdoc, so we hide it under // `cfg(doc)`. This is an ad-hoc implementation of attribute privacy. #[repr(transparent)] -#[derive(kani::Arbitrary)] -#[derive(kani::Invariant)] -#[safety_constraint(inner.len() > 0 && inner[inner.len() - 1] == 0 && !inner[..inner.len() - 1].contains(&0))] pub struct CStr { // FIXME: this should not be represented with a DST slice but rather with // just a raw `c_char` along with some form of marker to make @@ -215,6 +213,23 @@ impl fmt::Display for FromBytesWithNulError { } } +#[unstable(feature = "ub_checks", issue = "none")] +impl Invariant for &CStr { + fn is_safe(&self) -> bool { + let bytes: &[c_char] = &self.inner; + let len = bytes.len(); + + // An empty CStr should has a null byte. + // A valid CStr should end with a null-terminator and contains + // no intermediate null bytes. + if bytes.is_empty() || bytes[len - 1] != 0 || bytes[..len-1].contains(&0) { + return false; + } + + true + } +} + impl CStr { /// Wraps a raw C string with a safe C string wrapper. /// @@ -841,3 +856,49 @@ impl Iterator for Bytes<'_> { #[unstable(feature = "cstr_bytes", issue = "112115")] impl FusedIterator for Bytes<'_> {} + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> + #[kani::proof] + #[kani::unwind(32)] // Proof bounded by array length + fn check_from_bytes_until_nul_random_nul_byte() { + const ARR_LEN: usize = 1000; + let mut string: [u8; ARR_LEN] = kani::any(); + + // ensure that there is at least one null byte + let idx: usize = kani::any_where(|x: &usize| *x >= 0 && *x < ARR_LEN); + string[idx] = 0; + + let c_str = CStr::from_bytes_until_nul(&string).unwrap(); + assert!(c_str.is_safe()); + } + + #[kani::proof] + #[kani::unwind(32)] // Proof bounded by array length + fn check_from_bytes_until_nul_single_nul_byte_end() { + const ARR_LEN: usize = 1000; + // ensure that the string does not have intermediate null bytes + let mut string: [u8; ARR_LEN] = kani::any_where(|x: &[u8; ARR_LEN]| !x[..ARR_LEN-1].contains(&0)); + // ensure that the string is properly null-terminated + string[ARR_LEN - 1] = 0; + + let c_str = CStr::from_bytes_until_nul(&string).unwrap(); + assert!(c_str.is_safe()); + } + + #[kani::proof] + #[kani::unwind(8)] // Proof bounded by array length + fn check_from_bytes_until_nul_single_nul_byte_head() { + const ARR_LEN: usize = 8; + let mut string: [u8; ARR_LEN] = kani::any(); + // The first byte is a null byte should result in an empty CStr. + string[0] = 0; + + let c_str = CStr::from_bytes_until_nul(&string).unwrap(); + assert!(c_str.is_safe()); + } +} \ No newline at end of file diff --git a/library/core/src/ffi/mod.rs b/library/core/src/ffi/mod.rs index 38b9974420bd5..dc107c5d22cdd 100644 --- a/library/core/src/ffi/mod.rs +++ b/library/core/src/ffi/mod.rs @@ -20,11 +20,6 @@ pub use self::c_str::FromBytesUntilNulError; pub use self::c_str::FromBytesWithNulError; use crate::fmt; -use safety::{requires, ensures}; - -#[cfg(kani)] -use crate::kani; - #[unstable(feature = "c_str_module", issue = "112134")] pub mod c_str; @@ -228,24 +223,3 @@ impl fmt::Debug for c_void { )] #[link(name = "/defaultlib:libcmt", modifiers = "+verbatim", cfg(target_feature = "crt-static"))] extern "C" {} - -#[cfg(kani)] -#[unstable(feature = "kani", issue = "none")] -mod verify { - use super::*; - - // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> - #[kani::proof] - #[kani::unwind(16)] // Proof bounded by array length - fn check_from_bytes_until_nul() { - const ARR_LEN: usize = 16; - let mut string: [u8; ARR_LEN] = kani::any(); - // ensure that there is at least one null byte - let idx: usize = kani::any_where(|x| *x >= 0 && *x < ARR_LEN); - string[idx] = 0; - - let c_str = CStr::from_bytes_until_nul(&string).unwrap(); - assert!(c_str.is_safe()); - } - -} \ No newline at end of file From 55dfaaf031fffc47e65ef5004831a9099e2a5e5e Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Fri, 22 Nov 2024 14:43:55 -0800 Subject: [PATCH 3/7] Add comments --- library/core/src/ffi/c_str.rs | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 5be4c2054809e..44bd0a2d061ee 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -863,10 +863,18 @@ mod verify { use super::*; // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> + // Check 1: A random index in a u8 array is guaranteed to be a null byte + // Check 2: Only the last byte of a u8 array is a null byte + // Check 3: The first byte of a u8 array is a null byte + // + // Proofs are bounded (kani::unwind) by the length of the input array. + // Check 1: 2.08 sec when 32; 7.49 sec when 40 + // Check 2: 6.72 sec when 32; 9.2 sec when 40 + // Check 3: 0.33 sec when 8; 2.06 sec when 16 #[kani::proof] - #[kani::unwind(32)] // Proof bounded by array length + #[kani::unwind(32)] fn check_from_bytes_until_nul_random_nul_byte() { - const ARR_LEN: usize = 1000; + const ARR_LEN: usize = 32; let mut string: [u8; ARR_LEN] = kani::any(); // ensure that there is at least one null byte @@ -878,10 +886,11 @@ mod verify { } #[kani::proof] - #[kani::unwind(32)] // Proof bounded by array length + #[kani::unwind(32)] fn check_from_bytes_until_nul_single_nul_byte_end() { - const ARR_LEN: usize = 1000; + const ARR_LEN: usize = 32; // ensure that the string does not have intermediate null bytes + // TODO: there might be a better way let mut string: [u8; ARR_LEN] = kani::any_where(|x: &[u8; ARR_LEN]| !x[..ARR_LEN-1].contains(&0)); // ensure that the string is properly null-terminated string[ARR_LEN - 1] = 0; @@ -891,9 +900,9 @@ mod verify { } #[kani::proof] - #[kani::unwind(8)] // Proof bounded by array length + #[kani::unwind(16)] fn check_from_bytes_until_nul_single_nul_byte_head() { - const ARR_LEN: usize = 8; + const ARR_LEN: usize = 16; let mut string: [u8; ARR_LEN] = kani::any(); // The first byte is a null byte should result in an empty CStr. string[0] = 0; From 31c1d0284b08887f10b4f95dac4c2b3186e214e8 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Mon, 25 Nov 2024 14:48:06 -0800 Subject: [PATCH 4/7] Fix from_bytes_until_nul harness --- library/core/src/ffi/c_str.rs | 58 ++++++++--------------------------- 1 file changed, 13 insertions(+), 45 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 44bd0a2d061ee..f885ec803fd0b 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -863,51 +863,19 @@ mod verify { use super::*; // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> - // Check 1: A random index in a u8 array is guaranteed to be a null byte - // Check 2: Only the last byte of a u8 array is a null byte - // Check 3: The first byte of a u8 array is a null byte - // - // Proofs are bounded (kani::unwind) by the length of the input array. - // Check 1: 2.08 sec when 32; 7.49 sec when 40 - // Check 2: 6.72 sec when 32; 9.2 sec when 40 - // Check 3: 0.33 sec when 8; 2.06 sec when 16 #[kani::proof] - #[kani::unwind(32)] - fn check_from_bytes_until_nul_random_nul_byte() { - const ARR_LEN: usize = 32; - let mut string: [u8; ARR_LEN] = kani::any(); - - // ensure that there is at least one null byte - let idx: usize = kani::any_where(|x: &usize| *x >= 0 && *x < ARR_LEN); - string[idx] = 0; - - let c_str = CStr::from_bytes_until_nul(&string).unwrap(); - assert!(c_str.is_safe()); - } - - #[kani::proof] - #[kani::unwind(32)] - fn check_from_bytes_until_nul_single_nul_byte_end() { - const ARR_LEN: usize = 32; - // ensure that the string does not have intermediate null bytes - // TODO: there might be a better way - let mut string: [u8; ARR_LEN] = kani::any_where(|x: &[u8; ARR_LEN]| !x[..ARR_LEN-1].contains(&0)); - // ensure that the string is properly null-terminated - string[ARR_LEN - 1] = 0; - - let c_str = CStr::from_bytes_until_nul(&string).unwrap(); - assert!(c_str.is_safe()); - } - - #[kani::proof] - #[kani::unwind(16)] - fn check_from_bytes_until_nul_single_nul_byte_head() { - const ARR_LEN: usize = 16; - let mut string: [u8; ARR_LEN] = kani::any(); - // The first byte is a null byte should result in an empty CStr. - string[0] = 0; - - let c_str = CStr::from_bytes_until_nul(&string).unwrap(); - assert!(c_str.is_safe()); + #[kani::unwind(16)] // 7.3 seconds when 16; 33.1 seconds when 32 + fn check_from_bytes_until_nul() { + const MAX_SIZE: usize = 16; + let string: [u8; MAX_SIZE] = kani::any(); + // Covers the case of a single null byte at the end, no null bytes, as + // well as intermediate null bytes + let slice = kani::slice::any_slice_of_array(&string); + + let result = CStr::from_bytes_until_nul(slice); + if result.is_ok() { + let c_str = result.unwrap(); + assert!(c_str.is_safe()); + } } } \ No newline at end of file From 2d734df8576752dd22178af486b3bcc070ac8aeb Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Mon, 25 Nov 2024 16:17:54 -0800 Subject: [PATCH 5/7] Change array size to 32 && Add is_safe function doc && Fix harness --- library/core/src/ffi/c_str.rs | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index f885ec803fd0b..567f0fb38c583 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -215,13 +215,16 @@ impl fmt::Display for FromBytesWithNulError { #[unstable(feature = "ub_checks", issue = "none")] impl Invariant for &CStr { + /** + * Safety invariant of a valid CStr: + * 1. An empty CStr should has a null byte. + * 2. A valid CStr should end with a null-terminator and contains + * no intermediate null bytes. + */ fn is_safe(&self) -> bool { let bytes: &[c_char] = &self.inner; let len = bytes.len(); - // An empty CStr should has a null byte. - // A valid CStr should end with a null-terminator and contains - // no intermediate null bytes. if bytes.is_empty() || bytes[len - 1] != 0 || bytes[..len-1].contains(&0) { return false; } @@ -864,17 +867,16 @@ mod verify { // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> #[kani::proof] - #[kani::unwind(16)] // 7.3 seconds when 16; 33.1 seconds when 32 + #[kani::unwind(32)] // 7.3 seconds when 16; 33.1 seconds when 32 fn check_from_bytes_until_nul() { - const MAX_SIZE: usize = 16; + const MAX_SIZE: usize = 32; let string: [u8; MAX_SIZE] = kani::any(); // Covers the case of a single null byte at the end, no null bytes, as // well as intermediate null bytes let slice = kani::slice::any_slice_of_array(&string); let result = CStr::from_bytes_until_nul(slice); - if result.is_ok() { - let c_str = result.unwrap(); + if let Ok(c_str) = result { assert!(c_str.is_safe()); } } From 021c59f04dc7fe8bbc0ab3628b3adb78c117a8bf Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Mon, 25 Nov 2024 16:40:27 -0800 Subject: [PATCH 6/7] Fix typo and invariant --- library/core/src/ffi/c_str.rs | 9 ++------- 1 file changed, 2 insertions(+), 7 deletions(-) diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 567f0fb38c583..19ff29b0ba1e4 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -9,7 +9,6 @@ use crate::ptr::NonNull; use crate::slice::memchr; use crate::{fmt, intrinsics, ops, slice, str}; -// use safety::{requires, ensures}; use crate::ub_checks::Invariant; #[cfg(kani)] @@ -217,7 +216,7 @@ impl fmt::Display for FromBytesWithNulError { impl Invariant for &CStr { /** * Safety invariant of a valid CStr: - * 1. An empty CStr should has a null byte. + * 1. An empty CStr should have a null byte. * 2. A valid CStr should end with a null-terminator and contains * no intermediate null bytes. */ @@ -225,11 +224,7 @@ impl Invariant for &CStr { let bytes: &[c_char] = &self.inner; let len = bytes.len(); - if bytes.is_empty() || bytes[len - 1] != 0 || bytes[..len-1].contains(&0) { - return false; - } - - true + return !bytes.is_empty() && bytes[len - 1] == 0 && !bytes[..len-1].contains(&0); } } From 04862008aa9a3f509710b58066ffd24161dd50c2 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Mon, 25 Nov 2024 16:43:38 -0800 Subject: [PATCH 7/7] Fix invariant return --- 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 19ff29b0ba1e4..2a65b2415f7d3 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -224,7 +224,7 @@ impl Invariant for &CStr { let bytes: &[c_char] = &self.inner; let len = bytes.len(); - return !bytes.is_empty() && bytes[len - 1] == 0 && !bytes[..len-1].contains(&0); + !bytes.is_empty() && bytes[len - 1] == 0 && !bytes[..len-1].contains(&0) } }