From 2b2baa820494b069a2c6cc7cd623535e1635537b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 3 Jan 2025 16:33:31 -0800 Subject: [PATCH] Run format check in our CI and fix repo format (#205) Changed the `check-rustc.sh` script to run the format check. Also added a `--bless` mode to apply the changes locally. This change also includes the result of running the script with the `--bless` mode on. Related to #38 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Co-authored-by: Carolyn Zech --- .github/workflows/rustc.yml | 8 +- .../alloc/src/collections/vec_deque/mod.rs | 2 +- library/alloc/src/vec/mod.rs | 14 +- library/core/src/alloc/layout.rs | 26 +- library/core/src/ascii/ascii_char.rs | 9 +- library/core/src/char/convert.rs | 10 +- library/core/src/char/methods.rs | 12 +- library/core/src/ffi/c_str.rs | 39 +- library/core/src/mem/mod.rs | 7 +- library/core/src/num/f128.rs | 9 +- library/core/src/num/f16.rs | 9 +- library/core/src/num/f32.rs | 10 +- library/core/src/num/f64.rs | 9 +- library/core/src/num/int_macros.rs | 2 +- library/core/src/num/mod.rs | 456 ++++++++++++------ library/core/src/num/nonzero.rs | 32 +- library/core/src/ptr/alignment.rs | 9 +- library/core/src/ptr/const_ptr.rs | 38 +- library/core/src/ptr/mod.rs | 22 +- library/core/src/ptr/mut_ptr.rs | 240 ++++----- library/core/src/ptr/non_null.rs | 209 ++++---- library/core/src/ptr/unique.rs | 22 +- library/core/src/slice/ascii.rs | 7 +- library/core/src/slice/iter.rs | 14 +- library/core/src/str/lossy.rs | 1 - library/core/src/str/pattern.rs | 9 +- library/core/src/str/validations.rs | 5 +- library/core/src/time.rs | 13 +- library/core/src/ub_checks.rs | 9 +- library/core/src/unicode/mod.rs | 2 +- scripts/check_rustc.sh | 111 ++++- scripts/run-kani.sh | 4 +- 32 files changed, 821 insertions(+), 548 deletions(-) mode change 100644 => 100755 scripts/check_rustc.sh diff --git a/.github/workflows/rustc.yml b/.github/workflows/rustc.yml index 498c64c3b447f..abc2a1a31552b 100644 --- a/.github/workflows/rustc.yml +++ b/.github/workflows/rustc.yml @@ -19,7 +19,7 @@ defaults: shell: bash jobs: - build: + upstream_test: runs-on: ${{ matrix.os }} strategy: matrix: @@ -28,8 +28,8 @@ jobs: steps: - name: Checkout Library uses: actions/checkout@v4 - with: - path: head - name: Run rustc script - run: bash ./head/scripts/check_rustc.sh ${{github.workspace}}/head + env: + GH_TOKEN: ${{ secrets.GITHUB_TOKEN }} + run: ./scripts/check_rustc.sh diff --git a/library/alloc/src/collections/vec_deque/mod.rs b/library/alloc/src/collections/vec_deque/mod.rs index a0d34f8bb8c48..f41fef719c098 100644 --- a/library/alloc/src/collections/vec_deque/mod.rs +++ b/library/alloc/src/collections/vec_deque/mod.rs @@ -3087,6 +3087,7 @@ impl From<[T; N]> for VecDeque { #[unstable(feature = "kani", issue = "none")] mod verify { use core::kani; + use crate::collections::VecDeque; #[kani::proof] @@ -3120,5 +3121,4 @@ mod verify { assert!(deque[k] == arr[k]); } } - } diff --git a/library/alloc/src/vec/mod.rs b/library/alloc/src/vec/mod.rs index 370c412af83a2..7e299b67641ce 100644 --- a/library/alloc/src/vec/mod.rs +++ b/library/alloc/src/vec/mod.rs @@ -4037,15 +4037,15 @@ impl TryFrom> for [T; N] { #[unstable(feature = "kani", issue = "none")] mod verify { use core::kani; + use crate::vec::Vec; - - // Size chosen for testing the empty vector (0), middle element removal (1) - // and last element removal (2) cases while keeping verification tractable + + // Size chosen for testing the empty vector (0), middle element removal (1) + // and last element removal (2) cases while keeping verification tractable const ARRAY_LEN: usize = 3; #[kani::proof] pub fn verify_swap_remove() { - // Creating a vector directly from a fixed length arbitrary array let mut arr: [i32; ARRAY_LEN] = kani::Arbitrary::any_array(); let mut vect = Vec::from(&arr); @@ -4067,7 +4067,10 @@ mod verify { // Verifying that the removed index now contains the element originally at the vector's last index if applicable if index < original_len - 1 { - assert!(vect[index] == original_vec[original_len - 1], "Index should contain last element"); + assert!( + vect[index] == original_vec[original_len - 1], + "Index should contain last element" + ); } // Check that all other unaffected elements remain unchanged @@ -4075,6 +4078,5 @@ mod verify { if k != index { assert!(vect[k] == arr[k]); } - } } diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs index 808e2245045e0..78f0290ad604b 100644 --- a/library/core/src/alloc/layout.rs +++ b/library/core/src/alloc/layout.rs @@ -4,21 +4,20 @@ // collections, resulting in having to optimize down excess IR multiple times. // Your performance intuition is useless. Run perf. -use safety::{ensures, Invariant, requires}; +use safety::{Invariant, ensures, requires}; + +#[cfg(kani)] +use crate::cmp; use crate::error::Error; use crate::intrinsics::{unchecked_add, unchecked_mul, unchecked_sub}; -use crate::mem::SizedTypeProperties; -use crate::ptr::{Alignment, NonNull}; -use crate::{assert_unsafe_precondition, fmt, mem}; - #[cfg(kani)] use crate::kani; -#[cfg(kani)] -use crate::cmp; - +use crate::mem::SizedTypeProperties; +use crate::ptr::{Alignment, NonNull}; // Used only for contract verification. #[allow(unused_imports)] use crate::ub_checks::Invariant; +use crate::{assert_unsafe_precondition, fmt, mem}; // While this function is used in one place and its implementation // could be inlined, the previous attempts to do so made rustc @@ -624,14 +623,15 @@ impl fmt::Display for LayoutError { } #[cfg(kani)] -#[unstable(feature="kani", issue="none")] +#[unstable(feature = "kani", issue = "none")] mod verify { use super::*; impl kani::Arbitrary for Layout { fn any() -> Self { let align = kani::any::(); - let size = kani::any_where(|s: &usize| *s <= isize::MAX as usize - (align.as_usize() - 1)); + let size = + kani::any_where(|s: &usize| *s <= isize::MAX as usize - (align.as_usize() - 1)); unsafe { Layout { size, align } } } } @@ -684,8 +684,8 @@ mod verify { pub fn check_for_value_i32() { let x = kani::any::(); let _ = Layout::for_value::(&x); - let array : [i32; 2] = [1, 2]; - let _ = Layout::for_value::<[i32]>(&array[1 .. 1]); + let array: [i32; 2] = [1, 2]; + let _ = Layout::for_value::<[i32]>(&array[1..1]); let trait_ref: &dyn core::fmt::Debug = &x; let _ = Layout::for_value::(trait_ref); // TODO: the case of an extern type as unsized tail is not yet covered @@ -724,7 +724,7 @@ mod verify { pub fn check_padding_needed_for() { let layout = kani::any::(); let a2 = kani::any::(); - if(a2.is_power_of_two() && a2 <= layout.align()) { + if (a2.is_power_of_two() && a2 <= layout.align()) { let _ = layout.padding_needed_for(a2); } } diff --git a/library/core/src/ascii/ascii_char.rs b/library/core/src/ascii/ascii_char.rs index 84267c38b5973..aca4503f5a6c0 100644 --- a/library/core/src/ascii/ascii_char.rs +++ b/library/core/src/ascii/ascii_char.rs @@ -4,11 +4,11 @@ //! helps with clarity as we're also referring to `char` intentionally in here. use safety::{ensures, requires}; -use crate::mem::transmute; -use crate::{assert_unsafe_precondition, fmt}; #[cfg(kani)] use crate::kani; +use crate::mem::transmute; +use crate::{assert_unsafe_precondition, fmt}; /// One of the 128 Unicode characters from U+0000 through U+007F, /// often known as the [ASCII] subset. @@ -623,11 +623,12 @@ impl fmt::Debug for AsciiChar { } #[cfg(kani)] -#[unstable(feature="kani", issue="none")] +#[unstable(feature = "kani", issue = "none")] mod verify { - use super::*; use AsciiChar; + use super::*; + #[kani::proof_for_contract(AsciiChar::from_u8)] fn check_from_u8() { let b: u8 = kani::any(); diff --git a/library/core/src/char/convert.rs b/library/core/src/char/convert.rs index c4aa33afd6ad3..6c12c278dfb88 100644 --- a/library/core/src/char/convert.rs +++ b/library/core/src/char/convert.rs @@ -1,16 +1,16 @@ //! Character conversions. -use safety::{requires, ensures}; +use safety::{ensures, requires}; + use crate::char::TryFromCharError; use crate::error::Error; use crate::fmt; +#[cfg(kani)] +use crate::kani; use crate::mem::transmute; use crate::str::FromStr; use crate::ub_checks::assert_unsafe_precondition; -#[cfg(kani)] -use crate::kani; - /// Converts a `u32` to a `char`. See [`char::from_u32`]. #[must_use] #[inline] @@ -298,7 +298,7 @@ pub(super) const fn from_digit(num: u32, radix: u32) -> Option { } #[cfg(kani)] -#[unstable(feature="kani", issue="none")] +#[unstable(feature = "kani", issue = "none")] mod verify { use super::*; diff --git a/library/core/src/char/methods.rs b/library/core/src/char/methods.rs index 683fb008eb11a..9727d87f266e1 100644 --- a/library/core/src/char/methods.rs +++ b/library/core/src/char/methods.rs @@ -1,15 +1,14 @@ //! impl char {} use super::*; +#[cfg(kani)] +use crate::kani; use crate::panic::const_panic; use crate::slice; use crate::str::from_utf8_unchecked_mut; use crate::unicode::printable::is_printable; use crate::unicode::{self, conversions}; -#[cfg(kani)] -use crate::kani; - impl char { /// The lowest valid code point a `char` can have, `'\0'`. /// @@ -1871,11 +1870,12 @@ pub const fn encode_utf16_raw(mut code: u32, dst: &mut [u16]) -> &mut [u16] { } #[cfg(kani)] -#[unstable(feature="kani", issue="none")] +#[unstable(feature = "kani", issue = "none")] mod verify { - use super::*; use safety::ensures; + use super::*; + #[ensures(|result| c.is_ascii() == (result.is_some() && (result.unwrap() as u8 as char == *c)))] fn as_ascii_clone(c: &char) -> Option { c.as_ascii() @@ -1883,7 +1883,7 @@ mod verify { #[kani::proof_for_contract(as_ascii_clone)] fn check_as_ascii_ascii_char() { - let ascii: char = kani::any_where(|c : &char| c.is_ascii()); + let ascii: char = kani::any_where(|c: &char| c.is_ascii()); as_ascii_clone(&ascii); } diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index ef01d20b7fc38..f6b229e0f12a8 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -1,22 +1,21 @@ //! [`CStr`] and its related types. +use safety::{ensures, requires}; + use crate::cmp::Ordering; use crate::error::Error; use crate::ffi::c_char; use crate::intrinsics::const_eval_select; use crate::iter::FusedIterator; +#[cfg(kani)] +use crate::kani; use crate::marker::PhantomData; use crate::ptr::NonNull; use crate::slice::memchr; -use crate::{fmt, ops, slice, str}; -use safety::{requires, ensures}; - use crate::ub_checks::Invariant; #[allow(unused_imports)] use crate::ub_checks::can_dereference; - -#[cfg(kani)] -use crate::kani; +use crate::{fmt, ops, slice, str}; // 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 @@ -228,7 +227,7 @@ impl Invariant for &CStr { let bytes: &[c_char] = &self.inner; let len = bytes.len(); - !bytes.is_empty() && bytes[len - 1] == 0 && !bytes[..len-1].contains(&0) + !bytes.is_empty() && bytes[len - 1] == 0 && !bytes[..len - 1].contains(&0) } } @@ -887,7 +886,7 @@ impl FusedIterator for Bytes<'_> {} #[unstable(feature = "kani", issue = "none")] mod verify { use super::*; - + // Helper function fn arbitrary_cstr(slice: &[u8]) -> &CStr { // At a minimum, the slice has a null terminator to form a valid CStr. @@ -934,7 +933,7 @@ mod verify { let len = bytes.len(); assert_eq!(bytes, &slice[..len]); } - + // pub fn bytes(&self) -> Bytes<'_> #[kani::proof] #[kani::unwind(32)] @@ -972,7 +971,7 @@ mod verify { // pub const fn as_ptr(&self) -> *const c_char #[kani::proof] - #[kani::unwind(33)] + #[kani::unwind(33)] fn check_as_ptr() { const MAX_SIZE: usize = 32; let string: [u8; MAX_SIZE] = kani::any(); @@ -996,10 +995,10 @@ mod verify { } assert!(c_str.is_safe()); } - + // 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 string: [u8; MAX_SIZE] = kani::any(); @@ -1017,10 +1016,10 @@ mod verify { fn check_count_bytes() { const MAX_SIZE: usize = 32; let mut bytes: [u8; MAX_SIZE] = kani::any(); - + // Non-deterministically generate a length within the valid range [0, MAX_SIZE] let mut len: usize = kani::any_where(|&x| x < MAX_SIZE); - + // If a null byte exists before the generated length // adjust len to its position if let Some(pos) = bytes[..len].iter().position(|&x| x == 0) { @@ -1029,7 +1028,7 @@ mod verify { // If no null byte, insert one at the chosen length bytes[len] = 0; } - + let c_str = CStr::from_bytes_until_nul(&bytes).unwrap(); // Verify that count_bytes matches the adjusted length assert_eq!(c_str.count_bytes(), len); @@ -1076,7 +1075,9 @@ mod verify { 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); + } } // pub const unsafe fn from_ptr<'a>(ptr: *const c_char) -> &'a CStr @@ -1087,9 +1088,11 @@ mod verify { let string: [u8; MAX_SIZE] = kani::any(); let ptr = string.as_ptr() as *const c_char; - unsafe { CStr::from_ptr(ptr); } + unsafe { + CStr::from_ptr(ptr); + } } - + // pub const fn is_empty(&self) -> bool #[kani::proof] #[kani::unwind(33)] diff --git a/library/core/src/mem/mod.rs b/library/core/src/mem/mod.rs index 28b2b406c9bcc..4778c11eca434 100644 --- a/library/core/src/mem/mod.rs +++ b/library/core/src/mem/mod.rs @@ -6,11 +6,10 @@ #![stable(feature = "rust1", since = "1.0.0")] use crate::alloc::Layout; -use crate::marker::DiscriminantKind; -use crate::{clone, cmp, fmt, hash, intrinsics, ptr}; - #[cfg(kani)] use crate::kani; +use crate::marker::DiscriminantKind; +use crate::{clone, cmp, fmt, hash, intrinsics, ptr}; mod manually_drop; #[stable(feature = "manually_drop", since = "1.20.0")] @@ -1372,7 +1371,7 @@ pub macro offset_of($Container:ty, $($fields:expr)+ $(,)?) { } #[cfg(kani)] -#[unstable(feature="kani", issue="none")] +#[unstable(feature = "kani", issue = "none")] mod verify { use super::*; use crate::kani; diff --git a/library/core/src/num/f128.rs b/library/core/src/num/f128.rs index 1bccfe4f7f278..69c5aa99e7804 100644 --- a/library/core/src/num/f128.rs +++ b/library/core/src/num/f128.rs @@ -11,17 +11,16 @@ #![unstable(feature = "f128", issue = "116909")] +use safety::requires; + use crate::convert::FloatToInt; #[cfg(not(test))] use crate::intrinsics; +#[cfg(kani)] +use crate::kani; use crate::mem; use crate::num::FpCategory; use crate::panic::const_assert; -use safety::requires; - -#[cfg(kani)] -use crate::kani; - #[allow(unused_imports)] use crate::ub_checks::float_to_int_in_range; /// Basic mathematical constants. diff --git a/library/core/src/num/f16.rs b/library/core/src/num/f16.rs index 41a37321f4870..35079ea941f62 100644 --- a/library/core/src/num/f16.rs +++ b/library/core/src/num/f16.rs @@ -11,17 +11,16 @@ #![unstable(feature = "f16", issue = "116909")] +use safety::requires; + use crate::convert::FloatToInt; #[cfg(not(test))] use crate::intrinsics; +#[cfg(kani)] +use crate::kani; use crate::mem; use crate::num::FpCategory; use crate::panic::const_assert; -use safety::requires; - -#[cfg(kani)] -use crate::kani; - #[allow(unused_imports)] use crate::ub_checks::float_to_int_in_range; /// Basic mathematical constants. diff --git a/library/core/src/num/f32.rs b/library/core/src/num/f32.rs index fffc403470508..d5eeace861ade 100644 --- a/library/core/src/num/f32.rs +++ b/library/core/src/num/f32.rs @@ -11,18 +11,16 @@ #![stable(feature = "rust1", since = "1.0.0")] +use safety::requires; + use crate::convert::FloatToInt; #[cfg(not(test))] use crate::intrinsics; +#[cfg(kani)] +use crate::kani; use crate::mem; use crate::num::FpCategory; use crate::panic::const_assert; - -use safety::requires; - -#[cfg(kani)] -use crate::kani; - #[allow(unused_imports)] use crate::ub_checks::float_to_int_in_range; diff --git a/library/core/src/num/f64.rs b/library/core/src/num/f64.rs index 166fb2d329a5a..6990ef372c648 100644 --- a/library/core/src/num/f64.rs +++ b/library/core/src/num/f64.rs @@ -11,17 +11,16 @@ #![stable(feature = "rust1", since = "1.0.0")] +use safety::requires; + use crate::convert::FloatToInt; #[cfg(not(test))] use crate::intrinsics; +#[cfg(kani)] +use crate::kani; use crate::mem; use crate::num::FpCategory; use crate::panic::const_assert; -use safety::requires; - -#[cfg(kani)] -use crate::kani; - #[allow(unused_imports)] use crate::ub_checks::float_to_int_in_range; diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index f8e16d93d9bf3..0fa057c001be3 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -1290,7 +1290,7 @@ macro_rules! int_impl { #[cfg_attr(bootstrap, rustc_const_unstable(feature = "unchecked_shifts", issue = "85122"))] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - #[requires(rhs < <$ActualT>::BITS)] + #[requires(rhs < <$ActualT>::BITS)] pub const unsafe fn unchecked_shl(self, rhs: u32) -> Self { assert_unsafe_precondition!( check_language_ub, diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index a561eb3f9375b..f22b8ade0387e 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -2,14 +2,14 @@ #![stable(feature = "rust1", since = "1.0.0")] +use safety::{ensures, requires}; + +#[cfg(kani)] +use crate::kani; use crate::panic::const_panic; use crate::str::FromStr; use crate::ub_checks::assert_unsafe_precondition; use crate::{ascii, intrinsics, mem}; -use safety::{requires, ensures}; - -#[cfg(kani)] -use crate::kani; // FIXME(const-hack): Used because the `?` operator is not allowed in a const context. macro_rules! try_opt { @@ -1689,7 +1689,7 @@ mod verify { num1.$method(num2); } } - } + }; } // Improve unchecked_mul performance for {32, 64, 128}-bit integer types @@ -1701,13 +1701,13 @@ mod verify { pub fn $harness_name() { let num1: $type = kani::any::<$type>(); let num2: $type = kani::any::<$type>(); - + kani::assume(num1 >= $min && num1 <= $max); kani::assume(num2 >= $min && num2 <= $max); - + // Ensure that multiplication does not overflow kani::assume(!num1.overflowing_mul(num2).1); - + unsafe { num1.$method(num2); } @@ -1728,7 +1728,7 @@ mod verify { num1.$method(num2); } } - } + }; } macro_rules! generate_unchecked_neg_harness { @@ -1741,9 +1741,9 @@ mod verify { num1.unchecked_neg(); } } - } + }; } - + /// A macro to generate Kani proof harnesses for the `carrying_mul` method, /// /// The macro creates multiple harnesses for different ranges of input values, @@ -1764,22 +1764,22 @@ mod verify { let lhs: $type = kani::any::<$type>(); let rhs: $type = kani::any::<$type>(); let carry_in: $type = kani::any::<$type>(); - + kani::assume(lhs >= $min && lhs <= $max); kani::assume(rhs >= $min && rhs <= $max); kani::assume(carry_in >= $min && carry_in <= $max); - + // Perform the carrying multiplication let (result, carry_out) = lhs.carrying_mul(rhs, carry_in); - + // Manually compute the expected result and carry using wider type let wide_result = (lhs as $wide_type) .wrapping_mul(rhs as $wide_type) .wrapping_add(carry_in as $wide_type); - + let expected_result = wide_result as $type; let expected_carry = (wide_result >> <$type>::BITS) as $type; - + // Assert the result and carry are correct assert_eq!(result, expected_result); assert_eq!(carry_out, expected_carry); @@ -1787,8 +1787,6 @@ mod verify { )+ } } - - // Part 2 : Nested unsafe functions Generation Macros --> https://github.com/verify-rust-std/blob/main/doc/src/challenges/0011-floats-ints.md @@ -1829,7 +1827,7 @@ mod verify { let _ = num1.$method(num2); } - } + }; } // Part 3: Float to Integer Conversion function Harness Generation Macro @@ -1905,64 +1903,144 @@ mod verify { generate_unchecked_math_harness!(i16, unchecked_mul, checked_unchecked_mul_i16); // ====================== i32 Harnesses ====================== - generate_unchecked_mul_intervals!(i32, unchecked_mul, - unchecked_mul_i32_small, -10i32, 10i32, - unchecked_mul_i32_large_pos, i32::MAX - 1000i32, i32::MAX, - unchecked_mul_i32_large_neg, i32::MIN, i32::MIN + 1000i32, - unchecked_mul_i32_edge_pos, i32::MAX / 2, i32::MAX, - unchecked_mul_i32_edge_neg, i32::MIN, i32::MIN / 2 + generate_unchecked_mul_intervals!( + i32, + unchecked_mul, + unchecked_mul_i32_small, + -10i32, + 10i32, + unchecked_mul_i32_large_pos, + i32::MAX - 1000i32, + i32::MAX, + unchecked_mul_i32_large_neg, + i32::MIN, + i32::MIN + 1000i32, + unchecked_mul_i32_edge_pos, + i32::MAX / 2, + i32::MAX, + unchecked_mul_i32_edge_neg, + i32::MIN, + i32::MIN / 2 ); // ====================== i64 Harnesses ====================== - generate_unchecked_mul_intervals!(i64, unchecked_mul, - unchecked_mul_i64_small, -10i64, 10i64, - unchecked_mul_i64_large_pos, i64::MAX - 1000i64, i64::MAX, - unchecked_mul_i64_large_neg, i64::MIN, i64::MIN + 1000i64, - unchecked_mul_i64_edge_pos, i64::MAX / 2, i64::MAX, - unchecked_mul_i64_edge_neg, i64::MIN, i64::MIN / 2 + generate_unchecked_mul_intervals!( + i64, + unchecked_mul, + unchecked_mul_i64_small, + -10i64, + 10i64, + unchecked_mul_i64_large_pos, + i64::MAX - 1000i64, + i64::MAX, + unchecked_mul_i64_large_neg, + i64::MIN, + i64::MIN + 1000i64, + unchecked_mul_i64_edge_pos, + i64::MAX / 2, + i64::MAX, + unchecked_mul_i64_edge_neg, + i64::MIN, + i64::MIN / 2 ); // ====================== i128 Harnesses ====================== - generate_unchecked_mul_intervals!(i128, unchecked_mul, - unchecked_mul_i128_small, -10i128, 10i128, - unchecked_mul_i128_large_pos, i128::MAX - 1000i128, i128::MAX, - unchecked_mul_i128_large_neg, i128::MIN, i128::MIN + 1000i128, - unchecked_mul_i128_edge_pos, i128::MAX / 2, i128::MAX, - unchecked_mul_i128_edge_neg, i128::MIN, i128::MIN / 2 + generate_unchecked_mul_intervals!( + i128, + unchecked_mul, + unchecked_mul_i128_small, + -10i128, + 10i128, + unchecked_mul_i128_large_pos, + i128::MAX - 1000i128, + i128::MAX, + unchecked_mul_i128_large_neg, + i128::MIN, + i128::MIN + 1000i128, + unchecked_mul_i128_edge_pos, + i128::MAX / 2, + i128::MAX, + unchecked_mul_i128_edge_neg, + i128::MIN, + i128::MIN / 2 ); // ====================== isize Harnesses ====================== - generate_unchecked_mul_intervals!(isize, unchecked_mul, - unchecked_mul_isize_small, -10isize, 10isize, - unchecked_mul_isize_large_pos, isize::MAX - 1000isize, isize::MAX, - unchecked_mul_isize_large_neg, isize::MIN, isize::MIN + 1000isize, - unchecked_mul_isize_edge_pos, isize::MAX / 2, isize::MAX, - unchecked_mul_isize_edge_neg, isize::MIN, isize::MIN / 2 + generate_unchecked_mul_intervals!( + isize, + unchecked_mul, + unchecked_mul_isize_small, + -10isize, + 10isize, + unchecked_mul_isize_large_pos, + isize::MAX - 1000isize, + isize::MAX, + unchecked_mul_isize_large_neg, + isize::MIN, + isize::MIN + 1000isize, + unchecked_mul_isize_edge_pos, + isize::MAX / 2, + isize::MAX, + unchecked_mul_isize_edge_neg, + isize::MIN, + isize::MIN / 2 ); generate_unchecked_math_harness!(u8, unchecked_mul, checked_unchecked_mul_u8); generate_unchecked_math_harness!(u16, unchecked_mul, checked_unchecked_mul_u16); // ====================== u32 Harnesses ====================== - generate_unchecked_mul_intervals!(u32, unchecked_mul, - unchecked_mul_u32_small, 0u32, 10u32, - unchecked_mul_u32_large, u32::MAX - 1000u32, u32::MAX, - unchecked_mul_u32_edge, u32::MAX / 2, u32::MAX + generate_unchecked_mul_intervals!( + u32, + unchecked_mul, + unchecked_mul_u32_small, + 0u32, + 10u32, + unchecked_mul_u32_large, + u32::MAX - 1000u32, + u32::MAX, + unchecked_mul_u32_edge, + u32::MAX / 2, + u32::MAX ); // ====================== u64 Harnesses ====================== - generate_unchecked_mul_intervals!(u64, unchecked_mul, - unchecked_mul_u64_small, 0u64, 10u64, - unchecked_mul_u64_large, u64::MAX - 1000u64, u64::MAX, - unchecked_mul_u64_edge, u64::MAX / 2, u64::MAX + generate_unchecked_mul_intervals!( + u64, + unchecked_mul, + unchecked_mul_u64_small, + 0u64, + 10u64, + unchecked_mul_u64_large, + u64::MAX - 1000u64, + u64::MAX, + unchecked_mul_u64_edge, + u64::MAX / 2, + u64::MAX ); // ====================== u128 Harnesses ====================== - generate_unchecked_mul_intervals!(u128, unchecked_mul, - unchecked_mul_u128_small, 0u128, 10u128, - unchecked_mul_u128_large, u128::MAX - 1000u128, u128::MAX, - unchecked_mul_u128_edge, u128::MAX / 2, u128::MAX + generate_unchecked_mul_intervals!( + u128, + unchecked_mul, + unchecked_mul_u128_small, + 0u128, + 10u128, + unchecked_mul_u128_large, + u128::MAX - 1000u128, + u128::MAX, + unchecked_mul_u128_edge, + u128::MAX / 2, + u128::MAX ); // ====================== usize Harnesses ====================== - generate_unchecked_mul_intervals!(usize, unchecked_mul, - unchecked_mul_usize_small, 0usize, 10usize, - unchecked_mul_usize_large, usize::MAX - 1000usize, usize::MAX, - unchecked_mul_usize_edge, usize::MAX / 2, usize::MAX + generate_unchecked_mul_intervals!( + usize, + unchecked_mul, + unchecked_mul_usize_small, + 0usize, + 10usize, + unchecked_mul_usize_large, + usize::MAX - 1000usize, + usize::MAX, + unchecked_mul_usize_edge, + usize::MAX / 2, + usize::MAX ); // unchecked_shr proofs @@ -2020,7 +2098,7 @@ mod verify { // // Target contracts: // Preconditions: No overflow should occur - // #[requires(!self.overflowing_sub(rhs).1)] + // #[requires(!self.overflowing_sub(rhs).1)] // // Target function: // pub const unsafe fn unchecked_sub(self, rhs: Self) -> Self @@ -2039,60 +2117,94 @@ mod verify { generate_unchecked_math_harness!(u128, unchecked_sub, checked_unchecked_sub_u128); generate_unchecked_math_harness!(usize, unchecked_sub, checked_unchecked_sub_usize); - - // Part_2 `carrying_mul` proofs - // + // Part_2 `carrying_mul` proofs + // // ====================== u8 Harnesses ====================== /// Kani proof harness for `carrying_mul` on `u8` type with full range of values. - generate_carrying_mul_intervals!(u8, u16, - carrying_mul_u8_full_range, 0u8, u8::MAX - ); + generate_carrying_mul_intervals!(u8, u16, carrying_mul_u8_full_range, 0u8, u8::MAX); // ====================== u16 Harnesses ====================== /// Kani proof harness for `carrying_mul` on `u16` type with full range of values. - generate_carrying_mul_intervals!(u16, u32, - carrying_mul_u16_full_range, 0u16, u16::MAX - ); + generate_carrying_mul_intervals!(u16, u32, carrying_mul_u16_full_range, 0u16, u16::MAX); // ====================== u32 Harnesses ====================== - generate_carrying_mul_intervals!(u32, u64, - carrying_mul_u32_small, 0u32, 10u32, - carrying_mul_u32_large, u32::MAX - 10u32, u32::MAX, - carrying_mul_u32_mid_edge, (u32::MAX / 2) - 10u32, (u32::MAX / 2) + 10u32 + generate_carrying_mul_intervals!( + u32, + u64, + carrying_mul_u32_small, + 0u32, + 10u32, + carrying_mul_u32_large, + u32::MAX - 10u32, + u32::MAX, + carrying_mul_u32_mid_edge, + (u32::MAX / 2) - 10u32, + (u32::MAX / 2) + 10u32 ); // ====================== u64 Harnesses ====================== - generate_carrying_mul_intervals!(u64, u128, - carrying_mul_u64_small, 0u64, 10u64, - carrying_mul_u64_large, u64::MAX - 10u64, u64::MAX, - carrying_mul_u64_mid_edge, (u64::MAX / 2) - 10u64, (u64::MAX / 2) + 10u64 + generate_carrying_mul_intervals!( + u64, + u128, + carrying_mul_u64_small, + 0u64, + 10u64, + carrying_mul_u64_large, + u64::MAX - 10u64, + u64::MAX, + carrying_mul_u64_mid_edge, + (u64::MAX / 2) - 10u64, + (u64::MAX / 2) + 10u64 ); - // Part_2 `widening_mul` proofs - + // ====================== u8 Harnesses ====================== generate_widening_mul_intervals!(u8, u16, widening_mul_u8, 0u8, u8::MAX); - + // ====================== u16 Harnesses ====================== - generate_widening_mul_intervals!(u16, u32, - widening_mul_u16_small, 0u16, 10u16, - widening_mul_u16_large, u16::MAX - 10u16, u16::MAX, - widening_mul_u16_mid_edge, (u16::MAX / 2) - 10u16, (u16::MAX / 2) + 10u16 + generate_widening_mul_intervals!( + u16, + u32, + widening_mul_u16_small, + 0u16, + 10u16, + widening_mul_u16_large, + u16::MAX - 10u16, + u16::MAX, + widening_mul_u16_mid_edge, + (u16::MAX / 2) - 10u16, + (u16::MAX / 2) + 10u16 ); // ====================== u32 Harnesses ====================== - generate_widening_mul_intervals!(u32, u64, - widening_mul_u32_small, 0u32, 10u32, - widening_mul_u32_large, u32::MAX - 10u32, u32::MAX, - widening_mul_u32_mid_edge, (u32::MAX / 2) - 10u32, (u32::MAX / 2) + 10u32 + generate_widening_mul_intervals!( + u32, + u64, + widening_mul_u32_small, + 0u32, + 10u32, + widening_mul_u32_large, + u32::MAX - 10u32, + u32::MAX, + widening_mul_u32_mid_edge, + (u32::MAX / 2) - 10u32, + (u32::MAX / 2) + 10u32 ); // ====================== u64 Harnesses ====================== - generate_widening_mul_intervals!(u64, u128, - widening_mul_u64_small, 0u64, 10u64, - widening_mul_u64_large, u64::MAX - 10u64, u64::MAX, - widening_mul_u64_mid_edge, (u64::MAX / 2) - 10u64, (u64::MAX / 2) + 10u64 + generate_widening_mul_intervals!( + u64, + u128, + widening_mul_u64_small, + 0u64, + 10u64, + widening_mul_u64_large, + u64::MAX - 10u64, + u64::MAX, + widening_mul_u64_mid_edge, + (u64::MAX / 2) - 10u64, + (u64::MAX / 2) + 10u64 ); // Part_2 `wrapping_shl` proofs @@ -2157,63 +2269,115 @@ mod verify { // // Target function: // pub unsafe fn to_int_unchecked(self) -> Int where Self: FloatToInt - generate_to_int_unchecked_harness!(f32, - i8, checked_f32_to_int_unchecked_i8, - i16, checked_f32_to_int_unchecked_i16, - i32, checked_f32_to_int_unchecked_i32, - i64, checked_f32_to_int_unchecked_i64, - i128, checked_f32_to_int_unchecked_i128, - isize, checked_f32_to_int_unchecked_isize, - u8, checked_f32_to_int_unchecked_u8, - u16, checked_f32_to_int_unchecked_u16, - u32, checked_f32_to_int_unchecked_u32, - u64, checked_f32_to_int_unchecked_u64, - u128, checked_f32_to_int_unchecked_u128, - usize, checked_f32_to_int_unchecked_usize + generate_to_int_unchecked_harness!( + f32, + i8, + checked_f32_to_int_unchecked_i8, + i16, + checked_f32_to_int_unchecked_i16, + i32, + checked_f32_to_int_unchecked_i32, + i64, + checked_f32_to_int_unchecked_i64, + i128, + checked_f32_to_int_unchecked_i128, + isize, + checked_f32_to_int_unchecked_isize, + u8, + checked_f32_to_int_unchecked_u8, + u16, + checked_f32_to_int_unchecked_u16, + u32, + checked_f32_to_int_unchecked_u32, + u64, + checked_f32_to_int_unchecked_u64, + u128, + checked_f32_to_int_unchecked_u128, + usize, + checked_f32_to_int_unchecked_usize ); - generate_to_int_unchecked_harness!(f64, - i8, checked_f64_to_int_unchecked_i8, - i16, checked_f64_to_int_unchecked_i16, - i32, checked_f64_to_int_unchecked_i32, - i64, checked_f64_to_int_unchecked_i64, - i128, checked_f64_to_int_unchecked_i128, - isize, checked_f64_to_int_unchecked_isize, - u8, checked_f64_to_int_unchecked_u8, - u16, checked_f64_to_int_unchecked_u16, - u32, checked_f64_to_int_unchecked_u32, - u64, checked_f64_to_int_unchecked_u64, - u128, checked_f64_to_int_unchecked_u128, - usize, checked_f64_to_int_unchecked_usize + generate_to_int_unchecked_harness!( + f64, + i8, + checked_f64_to_int_unchecked_i8, + i16, + checked_f64_to_int_unchecked_i16, + i32, + checked_f64_to_int_unchecked_i32, + i64, + checked_f64_to_int_unchecked_i64, + i128, + checked_f64_to_int_unchecked_i128, + isize, + checked_f64_to_int_unchecked_isize, + u8, + checked_f64_to_int_unchecked_u8, + u16, + checked_f64_to_int_unchecked_u16, + u32, + checked_f64_to_int_unchecked_u32, + u64, + checked_f64_to_int_unchecked_u64, + u128, + checked_f64_to_int_unchecked_u128, + usize, + checked_f64_to_int_unchecked_usize ); - - generate_to_int_unchecked_harness!(f16, - i8, checked_f16_to_int_unchecked_i8, - i16, checked_f16_to_int_unchecked_i16, - i32, checked_f16_to_int_unchecked_i32, - i64, checked_f16_to_int_unchecked_i64, - i128, checked_f16_to_int_unchecked_i128, - isize, checked_f16_to_int_unchecked_isize, - u8, checked_f16_to_int_unchecked_u8, - u16, checked_f16_to_int_unchecked_u16, - u32, checked_f16_to_int_unchecked_u32, - u64, checked_f16_to_int_unchecked_u64, - u128, checked_f16_to_int_unchecked_u128, - usize, checked_f16_to_int_unchecked_usize + + generate_to_int_unchecked_harness!( + f16, + i8, + checked_f16_to_int_unchecked_i8, + i16, + checked_f16_to_int_unchecked_i16, + i32, + checked_f16_to_int_unchecked_i32, + i64, + checked_f16_to_int_unchecked_i64, + i128, + checked_f16_to_int_unchecked_i128, + isize, + checked_f16_to_int_unchecked_isize, + u8, + checked_f16_to_int_unchecked_u8, + u16, + checked_f16_to_int_unchecked_u16, + u32, + checked_f16_to_int_unchecked_u32, + u64, + checked_f16_to_int_unchecked_u64, + u128, + checked_f16_to_int_unchecked_u128, + usize, + checked_f16_to_int_unchecked_usize ); - - generate_to_int_unchecked_harness!(f128, - i8, checked_f128_to_int_unchecked_i8, - i16, checked_f128_to_int_unchecked_i16, - i32, checked_f128_to_int_unchecked_i32, - i64, checked_f128_to_int_unchecked_i64, - i128, checked_f128_to_int_unchecked_i128, - isize, checked_f128_to_int_unchecked_isize, - u8, checked_f128_to_int_unchecked_u8, - u16, checked_f128_to_int_unchecked_u16, - u32, checked_f128_to_int_unchecked_u32, - u64, checked_f128_to_int_unchecked_u64, - u128, checked_f128_to_int_unchecked_u128, - usize, checked_f128_to_int_unchecked_usize + + generate_to_int_unchecked_harness!( + f128, + i8, + checked_f128_to_int_unchecked_i8, + i16, + checked_f128_to_int_unchecked_i16, + i32, + checked_f128_to_int_unchecked_i32, + i64, + checked_f128_to_int_unchecked_i64, + i128, + checked_f128_to_int_unchecked_i128, + isize, + checked_f128_to_int_unchecked_isize, + u8, + checked_f128_to_int_unchecked_u8, + u16, + checked_f128_to_int_unchecked_u16, + u32, + checked_f128_to_int_unchecked_u32, + u64, + checked_f128_to_int_unchecked_u64, + u128, + checked_f128_to_int_unchecked_u128, + usize, + checked_f128_to_int_unchecked_usize ); } diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index c03021f009703..085510f78e783 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -1,16 +1,17 @@ //! Definitions of integer that is known not to equal zero. +use safety::{ensures, requires}; + use super::{IntErrorKind, ParseIntError}; use crate::cmp::Ordering; use crate::hash::{Hash, Hasher}; +#[cfg(kani)] +use crate::kani; use crate::marker::{Freeze, StructuralPartialEq}; use crate::ops::{BitOr, BitOrAssign, Div, DivAssign, Neg, Rem, RemAssign}; use crate::panic::{RefUnwindSafe, UnwindSafe}; use crate::str::FromStr; use crate::{fmt, intrinsics, ptr, ub_checks}; -use safety::{ensures, requires}; -#[cfg(kani)] -use crate::kani; /// A marker trait for primitive types which can be zero. /// /// This is an implementation detail for [NonZero]\ which may disappear or be replaced at any time. @@ -380,9 +381,9 @@ where #[rustc_const_stable(feature = "nonzero", since = "1.28.0")] #[must_use] #[inline] - // #[rustc_allow_const_fn_unstable(const_refs_to_cell)] enables byte-level - // comparisons within const functions. This is needed here to validate the - // contents of `T` by converting a pointer to a `u8` slice for our `requires` + // #[rustc_allow_const_fn_unstable(const_refs_to_cell)] enables byte-level + // comparisons within const functions. This is needed here to validate the + // contents of `T` by converting a pointer to a `u8` slice for our `requires` // and `ensures` checks. #[rustc_allow_const_fn_unstable(const_refs_to_cell)] #[requires({ @@ -398,7 +399,6 @@ where let result_ptr: *const T = &result_inner; let n_slice = unsafe { core::slice::from_raw_parts(n_ptr as *const u8, size) }; let result_slice = unsafe { core::slice::from_raw_parts(result_ptr as *const u8, size) }; - n_slice == result_slice })] pub const unsafe fn new_unchecked(n: T) -> Self { @@ -2233,24 +2233,24 @@ nonzero_integer! { reversed = "0x6a2c48091e6a2c48", } -#[unstable(feature="kani", issue="none")] +#[unstable(feature = "kani", issue = "none")] #[cfg(kani)] mod verify { - use super::*; + use super::*; macro_rules! nonzero_check { ($t:ty, $nonzero_type:ty, $nonzero_check_new_unchecked_for:ident) => { #[kani::proof_for_contract(NonZero::new_unchecked)] pub fn $nonzero_check_new_unchecked_for() { - let x: $t = kani::any(); // Generates a symbolic value of the provided type + let x: $t = kani::any(); // Generates a symbolic value of the provided type unsafe { - <$nonzero_type>::new_unchecked(x); // Calls NonZero::new_unchecked for the specified NonZero type + <$nonzero_type>::new_unchecked(x); // Calls NonZero::new_unchecked for the specified NonZero type } } }; } - + // Use the macro to generate different versions of the function for multiple types nonzero_check!(i8, core::num::NonZeroI8, nonzero_check_new_unchecked_for_i8); nonzero_check!(i16, core::num::NonZeroI16, nonzero_check_new_unchecked_for_16); @@ -2295,8 +2295,7 @@ mod verify { nonzero_check_cmp!(core::num::NonZeroU64, nonzero_check_cmp_for_u64); nonzero_check_cmp!(core::num::NonZeroU128, nonzero_check_cmp_for_u128); nonzero_check_cmp!(core::num::NonZeroUsize, nonzero_check_cmp_for_usize); - - + macro_rules! nonzero_check_max { ($nonzero_type:ty, $nonzero_check_max_for:ident) => { #[kani::proof] @@ -2326,7 +2325,6 @@ mod verify { nonzero_check_max!(core::num::NonZeroU128, nonzero_check_max_for_u128); nonzero_check_max!(core::num::NonZeroUsize, nonzero_check_max_for_usize); - macro_rules! nonzero_check_min { ($nonzero_type:ty, $nonzero_check_min_for:ident) => { #[kani::proof] @@ -2356,7 +2354,6 @@ mod verify { nonzero_check_min!(core::num::NonZeroU128, nonzero_check_min_for_u128); nonzero_check_min!(core::num::NonZeroUsize, nonzero_check_min_for_usize); - macro_rules! nonzero_check_clamp { ($nonzero_type:ty, $nonzero_check_clamp_for:ident) => { #[kani::proof] @@ -2393,7 +2390,6 @@ mod verify { nonzero_check_clamp!(core::num::NonZeroU128, nonzero_check_clamp_for_u128); nonzero_check_clamp!(core::num::NonZeroUsize, nonzero_check_clamp_for_usize); - macro_rules! nonzero_check_clamp_panic { ($nonzero_type:ty, $nonzero_check_clamp_for:ident) => { #[kani::proof] @@ -2431,7 +2427,6 @@ mod verify { nonzero_check_clamp_panic!(core::num::NonZeroU128, nonzero_check_clamp_panic_for_u128); nonzero_check_clamp_panic!(core::num::NonZeroUsize, nonzero_check_clamp_panic_for_usize); - macro_rules! nonzero_check_count_ones { ($nonzero_type:ty, $nonzero_check_count_ones_for:ident) => { #[kani::proof] @@ -2458,7 +2453,6 @@ mod verify { nonzero_check_count_ones!(core::num::NonZeroU128, nonzero_check_count_ones_for_u128); nonzero_check_count_ones!(core::num::NonZeroUsize, nonzero_check_count_ones_for_usize); - macro_rules! nonzero_check_rotate_left_and_right { ($nonzero_type:ty, $nonzero_check_rotate_for:ident) => { #[kani::proof] diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs index 9ae3b7e6ea889..54c661cd75efb 100644 --- a/library/core/src/ptr/alignment.rs +++ b/library/core/src/ptr/alignment.rs @@ -1,13 +1,12 @@ use safety::{ensures, invariant, requires}; -use crate::num::NonZero; -use crate::ub_checks::assert_unsafe_precondition; -use crate::{cmp, fmt, hash, mem, num}; #[cfg(kani)] use crate::kani; - +use crate::num::NonZero; #[cfg(kani)] use crate::ub_checks::Invariant; +use crate::ub_checks::assert_unsafe_precondition; +use crate::{cmp, fmt, hash, mem, num}; /// A type storing a `usize` which is a power of two, and thus /// represents a possible alignment in the Rust abstract machine. @@ -394,7 +393,7 @@ enum AlignmentEnum { } #[cfg(kani)] -#[unstable(feature="kani", issue="none")] +#[unstable(feature = "kani", issue = "none")] mod verify { use super::*; diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 637d9b65af426..46925739384dc 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -1,13 +1,14 @@ +use core::mem; + +use safety::{ensures, requires}; + use super::*; use crate::cmp::Ordering::{Equal, Greater, Less}; use crate::intrinsics::const_eval_select; -use crate::mem::SizedTypeProperties; -use crate::slice::{self, SliceIndex}; -use safety::{ensures, requires}; - #[cfg(kani)] use crate::kani; -use core::mem; +use crate::mem::SizedTypeProperties; +use crate::slice::{self, SliceIndex}; impl *const T { /// Returns `true` if the pointer is null. @@ -1824,10 +1825,12 @@ impl PartialOrd for *const T { #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] mod verify { - use crate::kani; use core::mem; + use kani::PointerGenerator; + use crate::kani; + /// This macro generates a single verification harness for the `offset`, `add`, or `sub` /// pointer operations, supporting integer, composite, or unit types. /// - `$ty`: The type of the slice's elements (e.g., `i32`, `u32`, tuples). @@ -2134,10 +2137,7 @@ mod verify { let self_ptr: *const u32 = unsafe { origin_ptr.byte_offset(offset as isize) }; let result: isize = unsafe { self_ptr.byte_offset_from(origin_ptr) }; assert_eq!(result, offset as isize); - assert_eq!( - result, - (self_ptr.addr() as isize - origin_ptr.addr() as isize) - ); + assert_eq!(result, (self_ptr.addr() as isize - origin_ptr.addr() as isize)); } macro_rules! generate_offset_from_harness { @@ -2193,11 +2193,7 @@ mod verify { } // fn <*const T>::offset_from() integer and integer slice types verification - generate_offset_from_harness!( - u8, - check_const_offset_from_u8, - check_const_offset_from_u8_arr - ); + generate_offset_from_harness!(u8, check_const_offset_from_u8, check_const_offset_from_u8_arr); generate_offset_from_harness!( u16, check_const_offset_from_u16, @@ -2223,11 +2219,7 @@ mod verify { check_const_offset_from_usize, check_const_offset_from_usize_arr ); - generate_offset_from_harness!( - i8, - check_const_offset_from_i8, - check_const_offset_from_i8_arr - ); + generate_offset_from_harness!(i8, check_const_offset_from_i8, check_const_offset_from_i8_arr); generate_offset_from_harness!( i16, check_const_offset_from_i16, @@ -2442,11 +2434,7 @@ mod verify { gen_const_byte_arith_harness!(usize, byte_offset, check_const_byte_offset_usize); gen_const_byte_arith_harness!((i8, i8), byte_offset, check_const_byte_offset_tuple_1); gen_const_byte_arith_harness!((f64, bool), byte_offset, check_const_byte_offset_tuple_2); - gen_const_byte_arith_harness!( - (i32, f64, bool), - byte_offset, - check_const_byte_offset_tuple_3 - ); + gen_const_byte_arith_harness!((i32, f64, bool), byte_offset, check_const_byte_offset_tuple_3); gen_const_byte_arith_harness!( (i8, u16, i32, u64, isize), byte_offset, diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index e84352958e398..20fa692f1336b 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -394,13 +394,12 @@ #![allow(clippy::not_unsafe_ptr_arg_deref)] use crate::cmp::Ordering; +#[cfg(kani)] +use crate::kani; use crate::marker::FnPtr; use crate::mem::{self, MaybeUninit, SizedTypeProperties}; use crate::{fmt, hash, intrinsics, ub_checks}; -#[cfg(kani)] -use crate::kani; - mod alignment; #[unstable(feature = "ptr_alignment_type", issue = "102070")] pub use alignment::Alignment; @@ -1860,9 +1859,9 @@ pub unsafe fn write_volatile(dst: *mut T, src: T) { let stride = mem::size_of::(); // ZSTs if stride == 0 { - if p.addr() % a == 0 { + if p.addr() % a == 0 { return *result == 0; - } else { + } else { return *result == usize::MAX; } } @@ -1876,8 +1875,8 @@ pub unsafe fn write_volatile(dst: *mut T, src: T) { // requires computing gcd(a, stride), which is too expensive without // quantifiers (https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html). // This should be updated once quantifiers are available. - if (a % stride != 0 && *result == usize::MAX) { - return true; + if (a % stride != 0 && *result == usize::MAX) { + return true; } // If we reach this case, either: @@ -2442,14 +2441,13 @@ pub macro addr_of_mut($place:expr) { } #[cfg(kani)] -#[unstable(feature="kani", issue="none")] +#[unstable(feature = "kani", issue = "none")] mod verify { - use crate::fmt::Debug; + use intrinsics::{mul_with_overflow, unchecked_sub, wrapping_mul, wrapping_sub}; + use super::*; + use crate::fmt::Debug; use crate::kani; - use intrinsics::{ - mul_with_overflow, unchecked_sub, wrapping_mul, wrapping_sub - }; #[kani::proof_for_contract(read_volatile)] pub fn check_read_u128() { diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs index 8f3ae4f746b9f..a307b69dfb4c7 100644 --- a/library/core/src/ptr/mut_ptr.rs +++ b/library/core/src/ptr/mut_ptr.rs @@ -1,13 +1,14 @@ +use core::mem; + +use safety::{ensures, requires}; + use super::*; use crate::cmp::Ordering::{Equal, Greater, Less}; use crate::intrinsics::const_eval_select; -use crate::mem::SizedTypeProperties; -use crate::slice::{self, SliceIndex}; -use safety::{ensures, requires}; - #[cfg(kani)] use crate::kani; -use core::mem; +use crate::mem::SizedTypeProperties; +use crate::slice::{self, SliceIndex}; impl *mut T { /// Returns `true` if the pointer is null. @@ -402,7 +403,8 @@ impl *mut T { #[must_use = "returns a new pointer rather than modifying its argument"] #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")] #[inline(always)] - #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[cfg_attr(miri, track_caller)] + // even without panics, this helps for Miri backtraces // Note: It is the caller's responsibility to ensure that `self` is non-null and properly aligned. // These conditions are not verified as part of the preconditions. #[requires( @@ -1049,7 +1051,8 @@ impl *mut T { #[must_use = "returns a new pointer rather than modifying its argument"] #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")] #[inline(always)] - #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[cfg_attr(miri, track_caller)] + // even without panics, this helps for Miri backtraces // Note: It is the caller's responsibility to ensure that `self` is non-null and properly aligned. // These conditions are not verified as part of the preconditions. #[requires( @@ -1189,7 +1192,8 @@ impl *mut T { #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")] #[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_neg))] #[inline(always)] - #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[cfg_attr(miri, track_caller)] + // even without panics, this helps for Miri backtraces // Note: It is the caller's responsibility to ensure that `self` is non-null and properly aligned. // These conditions are not verified as part of the preconditions. #[requires( @@ -2240,13 +2244,14 @@ impl PartialOrd for *mut T { #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] mod verify { - use crate::kani; use core::mem; + use crate::kani; + // Chosen for simplicity and sufficient size to test edge cases effectively // Represents the number of elements in the slice or array being tested. - // Doesn't need to be large because all possible values for the slice are explored, - // including edge cases like pointers at the start, middle, and end of the slice. + // Doesn't need to be large because all possible values for the slice are explored, + // including edge cases like pointers at the start, middle, and end of the slice. // Symbolic execution generalizes across all possible elements, regardless of the actual array size. const ARRAY_SIZE: usize = 5; @@ -2262,7 +2267,7 @@ mod verify { let offset: usize = kani::any(); let count: isize = kani::any(); kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); - let ptr_with_offset: *mut $ty = test_ptr.wrapping_byte_add(offset); + let ptr_with_offset: *mut $ty = test_ptr.wrapping_byte_add(offset); unsafe { ptr_with_offset.offset(count); } @@ -2276,7 +2281,7 @@ mod verify { let offset: usize = kani::any(); let count: usize = kani::any(); kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); - let ptr_with_offset: *mut $ty = test_ptr.wrapping_byte_add(offset); + let ptr_with_offset: *mut $ty = test_ptr.wrapping_byte_add(offset); unsafe { ptr_with_offset.add(count); } @@ -2290,7 +2295,7 @@ mod verify { let offset: usize = kani::any(); let count: usize = kani::any(); kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>()); - let ptr_with_offset: *mut $ty = test_ptr.wrapping_byte_add(offset); + let ptr_with_offset: *mut $ty = test_ptr.wrapping_byte_add(offset); unsafe { ptr_with_offset.sub(count); } @@ -2299,24 +2304,104 @@ mod verify { } // Generate pointer harnesses for various types (offset, add, sub) - generate_mut_slice_harnesses!(i8, check_mut_offset_slice_i8, check_mut_add_slice_i8, check_mut_sub_slice_i8); - generate_mut_slice_harnesses!(i16, check_mut_offset_slice_i16, check_mut_add_slice_i16, check_mut_sub_slice_i16); - generate_mut_slice_harnesses!(i32, check_mut_offset_slice_i32, check_mut_add_slice_i32, check_mut_sub_slice_i32); - generate_mut_slice_harnesses!(i64, check_mut_offset_slice_i64, check_mut_add_slice_i64, check_mut_sub_slice_i64); - generate_mut_slice_harnesses!(i128, check_mut_offset_slice_i128, check_mut_add_slice_i128, check_mut_sub_slice_i128); - generate_mut_slice_harnesses!(isize, check_mut_offset_slice_isize, check_mut_add_slice_isize, check_mut_sub_slice_isize); - generate_mut_slice_harnesses!(u8, check_mut_offset_slice_u8, check_mut_add_slice_u8, check_mut_sub_slice_u8); - generate_mut_slice_harnesses!(u16, check_mut_offset_slice_u16, check_mut_add_slice_u16, check_mut_sub_slice_u16); - generate_mut_slice_harnesses!(u32, check_mut_offset_slice_u32, check_mut_add_slice_u32, check_mut_sub_slice_u32); - generate_mut_slice_harnesses!(u64, check_mut_offset_slice_u64, check_mut_add_slice_u64, check_mut_sub_slice_u64); - generate_mut_slice_harnesses!(u128, check_mut_offset_slice_u128, check_mut_add_slice_u128, check_mut_sub_slice_u128); - generate_mut_slice_harnesses!(usize, check_mut_offset_slice_usize, check_mut_add_slice_usize, check_mut_sub_slice_usize); + generate_mut_slice_harnesses!( + i8, + check_mut_offset_slice_i8, + check_mut_add_slice_i8, + check_mut_sub_slice_i8 + ); + generate_mut_slice_harnesses!( + i16, + check_mut_offset_slice_i16, + check_mut_add_slice_i16, + check_mut_sub_slice_i16 + ); + generate_mut_slice_harnesses!( + i32, + check_mut_offset_slice_i32, + check_mut_add_slice_i32, + check_mut_sub_slice_i32 + ); + generate_mut_slice_harnesses!( + i64, + check_mut_offset_slice_i64, + check_mut_add_slice_i64, + check_mut_sub_slice_i64 + ); + generate_mut_slice_harnesses!( + i128, + check_mut_offset_slice_i128, + check_mut_add_slice_i128, + check_mut_sub_slice_i128 + ); + generate_mut_slice_harnesses!( + isize, + check_mut_offset_slice_isize, + check_mut_add_slice_isize, + check_mut_sub_slice_isize + ); + generate_mut_slice_harnesses!( + u8, + check_mut_offset_slice_u8, + check_mut_add_slice_u8, + check_mut_sub_slice_u8 + ); + generate_mut_slice_harnesses!( + u16, + check_mut_offset_slice_u16, + check_mut_add_slice_u16, + check_mut_sub_slice_u16 + ); + generate_mut_slice_harnesses!( + u32, + check_mut_offset_slice_u32, + check_mut_add_slice_u32, + check_mut_sub_slice_u32 + ); + generate_mut_slice_harnesses!( + u64, + check_mut_offset_slice_u64, + check_mut_add_slice_u64, + check_mut_sub_slice_u64 + ); + generate_mut_slice_harnesses!( + u128, + check_mut_offset_slice_u128, + check_mut_add_slice_u128, + check_mut_sub_slice_u128 + ); + generate_mut_slice_harnesses!( + usize, + check_mut_offset_slice_usize, + check_mut_add_slice_usize, + check_mut_sub_slice_usize + ); // Generate pointer harnesses for tuples (offset, add, sub) - generate_mut_slice_harnesses!((i8, i8), check_mut_offset_slice_tuple_1, check_mut_add_slice_tuple_1, check_mut_sub_slice_tuple_1); - generate_mut_slice_harnesses!((f64, bool), check_mut_offset_slice_tuple_2, check_mut_add_slice_tuple_2, check_mut_sub_slice_tuple_2); - generate_mut_slice_harnesses!((i32, f64, bool), check_mut_offset_slice_tuple_3, check_mut_add_slice_tuple_3, check_mut_sub_slice_tuple_3); - generate_mut_slice_harnesses!((i8, u16, i32, u64, isize), check_mut_offset_slice_tuple_4, check_mut_add_slice_tuple_4, check_mut_sub_slice_tuple_4); + generate_mut_slice_harnesses!( + (i8, i8), + check_mut_offset_slice_tuple_1, + check_mut_add_slice_tuple_1, + check_mut_sub_slice_tuple_1 + ); + generate_mut_slice_harnesses!( + (f64, bool), + check_mut_offset_slice_tuple_2, + check_mut_add_slice_tuple_2, + check_mut_sub_slice_tuple_2 + ); + generate_mut_slice_harnesses!( + (i32, f64, bool), + check_mut_offset_slice_tuple_3, + check_mut_add_slice_tuple_3, + check_mut_sub_slice_tuple_3 + ); + generate_mut_slice_harnesses!( + (i8, u16, i32, u64, isize), + check_mut_offset_slice_tuple_4, + check_mut_add_slice_tuple_4, + check_mut_sub_slice_tuple_4 + ); use kani::PointerGenerator; @@ -2370,24 +2455,9 @@ mod verify { // Generate harnesses for integer types (add, sub, offset) generate_arithmetic_harnesses!(i8, check_mut_add_i8, check_mut_sub_i8, check_mut_offset_i8); - generate_arithmetic_harnesses!( - i16, - check_mut_add_i16, - check_mut_sub_i16, - check_mut_offset_i16 - ); - generate_arithmetic_harnesses!( - i32, - check_mut_add_i32, - check_mut_sub_i32, - check_mut_offset_i32 - ); - generate_arithmetic_harnesses!( - i64, - check_mut_add_i64, - check_mut_sub_i64, - check_mut_offset_i64 - ); + generate_arithmetic_harnesses!(i16, check_mut_add_i16, check_mut_sub_i16, check_mut_offset_i16); + generate_arithmetic_harnesses!(i32, check_mut_add_i32, check_mut_sub_i32, check_mut_offset_i32); + generate_arithmetic_harnesses!(i64, check_mut_add_i64, check_mut_sub_i64, check_mut_offset_i64); generate_arithmetic_harnesses!( i128, check_mut_add_i128, @@ -2403,24 +2473,9 @@ mod verify { // Due to a bug of kani the test `check_mut_add_u8` is malfunctioning for now. // Tracking issue: https://github.com/model-checking/kani/issues/3743 // generate_arithmetic_harnesses!(u8, check_mut_add_u8, check_mut_sub_u8, check_mut_offset_u8); - generate_arithmetic_harnesses!( - u16, - check_mut_add_u16, - check_mut_sub_u16, - check_mut_offset_u16 - ); - generate_arithmetic_harnesses!( - u32, - check_mut_add_u32, - check_mut_sub_u32, - check_mut_offset_u32 - ); - generate_arithmetic_harnesses!( - u64, - check_mut_add_u64, - check_mut_sub_u64, - check_mut_offset_u64 - ); + generate_arithmetic_harnesses!(u16, check_mut_add_u16, check_mut_sub_u16, check_mut_offset_u16); + generate_arithmetic_harnesses!(u32, check_mut_add_u32, check_mut_sub_u32, check_mut_offset_u32); + generate_arithmetic_harnesses!(u64, check_mut_add_u64, check_mut_sub_u64, check_mut_offset_u64); generate_arithmetic_harnesses!( u128, check_mut_add_u128, @@ -2517,21 +2572,9 @@ mod verify { } generate_offset_from_harness!(u8, check_mut_offset_from_u8, check_mut_offset_from_u8_array); - generate_offset_from_harness!( - u16, - check_mut_offset_from_u16, - check_mut_offset_from_u16_array - ); - generate_offset_from_harness!( - u32, - check_mut_offset_from_u32, - check_mut_offset_from_u32_array - ); - generate_offset_from_harness!( - u64, - check_mut_offset_from_u64, - check_mut_offset_from_u64_array - ); + generate_offset_from_harness!(u16, check_mut_offset_from_u16, check_mut_offset_from_u16_array); + generate_offset_from_harness!(u32, check_mut_offset_from_u32, check_mut_offset_from_u32_array); + generate_offset_from_harness!(u64, check_mut_offset_from_u64, check_mut_offset_from_u64_array); generate_offset_from_harness!( u128, check_mut_offset_from_u128, @@ -2544,21 +2587,9 @@ mod verify { ); generate_offset_from_harness!(i8, check_mut_offset_from_i8, check_mut_offset_from_i8_array); - generate_offset_from_harness!( - i16, - check_mut_offset_from_i16, - check_mut_offset_from_i16_array - ); - generate_offset_from_harness!( - i32, - check_mut_offset_from_i32, - check_mut_offset_from_i32_array - ); - generate_offset_from_harness!( - i64, - check_mut_offset_from_i64, - check_mut_offset_from_i64_array - ); + generate_offset_from_harness!(i16, check_mut_offset_from_i16, check_mut_offset_from_i16_array); + generate_offset_from_harness!(i32, check_mut_offset_from_i32, check_mut_offset_from_i32_array); + generate_offset_from_harness!(i64, check_mut_offset_from_i64, check_mut_offset_from_i64_array); generate_offset_from_harness!( i128, check_mut_offset_from_i128, @@ -2715,11 +2746,7 @@ mod verify { gen_mut_byte_arith_harness!((i8, i8), byte_add, check_mut_byte_add_tuple_1); gen_mut_byte_arith_harness!((f64, bool), byte_add, check_mut_byte_add_tuple_2); gen_mut_byte_arith_harness!((i32, f64, bool), byte_add, check_mut_byte_add_tuple_3); - gen_mut_byte_arith_harness!( - (i8, u16, i32, u64, isize), - byte_add, - check_mut_byte_add_tuple_4 - ); + gen_mut_byte_arith_harness!((i8, u16, i32, u64, isize), byte_add, check_mut_byte_add_tuple_4); gen_mut_byte_arith_harness!(i8, byte_sub, check_mut_byte_sub_i8); gen_mut_byte_arith_harness!(i16, byte_sub, check_mut_byte_sub_i16); @@ -2736,11 +2763,7 @@ mod verify { gen_mut_byte_arith_harness!((i8, i8), byte_sub, check_mut_byte_sub_tuple_1); gen_mut_byte_arith_harness!((f64, bool), byte_sub, check_mut_byte_sub_tuple_2); gen_mut_byte_arith_harness!((i32, f64, bool), byte_sub, check_mut_byte_sub_tuple_3); - gen_mut_byte_arith_harness!( - (i8, u16, i32, u64, isize), - byte_sub, - check_mut_byte_sub_tuple_4 - ); + gen_mut_byte_arith_harness!((i8, u16, i32, u64, isize), byte_sub, check_mut_byte_sub_tuple_4); gen_mut_byte_arith_harness!(i8, byte_offset, check_mut_byte_offset_i8); gen_mut_byte_arith_harness!(i16, byte_offset, check_mut_byte_offset_i16); @@ -2903,10 +2926,7 @@ mod verify { let self_ptr: *mut u32 = unsafe { origin_ptr.byte_offset(offset as isize) }; let result: isize = unsafe { self_ptr.byte_offset_from(origin_ptr) }; assert_eq!(result, offset as isize); - assert_eq!( - result, - (self_ptr.addr() as isize - origin_ptr.addr() as isize) - ); + assert_eq!(result, (self_ptr.addr() as isize - origin_ptr.addr() as isize)); } // Proof for unit size diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 714104930dd5a..c9361e4d7b4bd 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1,4 +1,8 @@ +use safety::{ensures, requires}; + use crate::cmp::Ordering; +#[cfg(kani)] +use crate::kani; use crate::marker::Unsize; use crate::mem::{MaybeUninit, SizedTypeProperties}; use crate::num::NonZero; @@ -6,14 +10,10 @@ use crate::ops::{CoerceUnsized, DispatchFromDyn}; use crate::pin::PinCoerceUnsized; use crate::ptr::Unique; use crate::slice::{self, SliceIndex}; -use crate::ub_checks::assert_unsafe_precondition; -use crate::{fmt, hash, intrinsics, ptr}; -use safety::{ensures, requires}; - -#[cfg(kani)] -use crate::kani; #[cfg(kani)] use crate::ub_checks; +use crate::ub_checks::assert_unsafe_precondition; +use crate::{fmt, hash, intrinsics, ptr}; /// `*mut T` but non-zero and [covariant]. /// @@ -138,8 +138,8 @@ impl NonNull { #[inline] #[must_use] #[unstable(feature = "ptr_as_uninit", issue = "75402")] - #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure the pointer is valid to create a reference. - #[ensures(|result: &&MaybeUninit| core::ptr::eq(*result, self.cast().as_ptr()))] // Ensure returned reference points to the correct memory location. + #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure the pointer is valid to create a reference. + #[ensures(|result: &&MaybeUninit| core::ptr::eq(*result, self.cast().as_ptr()))] // Ensure returned reference points to the correct memory location. pub const unsafe fn as_uninit_ref<'a>(self) -> &'a MaybeUninit { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a reference. @@ -163,8 +163,8 @@ impl NonNull { #[inline] #[must_use] #[unstable(feature = "ptr_as_uninit", issue = "75402")] - #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure pointer is valid to create a mutable reference. - #[ensures(|result: &&mut MaybeUninit| core::ptr::eq(*result, self.cast().as_ptr()))] // Ensure the returned reference points to the correct memory. + #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure pointer is valid to create a mutable reference. + #[ensures(|result: &&mut MaybeUninit| core::ptr::eq(*result, self.cast().as_ptr()))] // Ensure the returned reference points to the correct memory. pub const unsafe fn as_uninit_mut<'a>(self) -> &'a mut MaybeUninit { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a reference. @@ -392,7 +392,7 @@ impl NonNull { #[must_use] #[inline(always)] #[requires(ub_checks::can_dereference(self.as_ptr() as *const()))] // Ensure input is convertible to a reference - #[ensures(|result: &&T| core::ptr::eq(*result, self.as_ptr()))] // Ensure returned reference matches pointer + #[ensures(|result: &&T| core::ptr::eq(*result, self.as_ptr()))] // Ensure returned reference matches pointer pub const unsafe fn as_ref<'a>(&self) -> &'a T { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a reference. @@ -682,7 +682,7 @@ impl NonNull { #[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_neg))] #[requires( count.checked_mul(core::mem::size_of::()).is_some() && - count * core::mem::size_of::() <= isize::MAX as usize && + count * core::mem::size_of::() <= isize::MAX as usize && kani::mem::same_allocation(self.as_ptr(), self.as_ptr().wrapping_sub(count)) )] #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(-(count as isize)))] @@ -823,8 +823,8 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] - #[requires( - (kani::mem::same_allocation(self.as_ptr(), origin.as_ptr()) && + #[requires( + (kani::mem::same_allocation(self.as_ptr(), origin.as_ptr()) && ((self.as_ptr().addr() - origin.as_ptr().addr()) % core::mem::size_of::() == 0)) )] // Ensure both pointers meet safety conditions for offset_from #[ensures(|result: &isize| *result == (self.as_ptr() as isize - origin.as_ptr() as isize) / core::mem::size_of::() as isize)] @@ -1656,7 +1656,7 @@ impl NonNull<[T]> { #[requires(self.len().checked_mul(core::mem::size_of::()).is_some() && self.len() * core::mem::size_of::() <= isize::MAX as usize)] // Ensure the slice size does not exceed isize::MAX #[requires(kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_add(self.len() * core::mem::size_of::()) as *const()))] // Ensure the slice is contained within a single allocation #[ensures(|result: &&mut [MaybeUninit]| result.len() == self.len())] // Length check - #[ensures(|result: &&mut [MaybeUninit]| core::ptr::eq(result.as_ptr(), self.cast().as_ptr()))] // Address check + #[ensures(|result: &&mut [MaybeUninit]| core::ptr::eq(result.as_ptr(), self.cast().as_ptr()))] // Address check pub const unsafe fn as_uninit_slice_mut<'a>(self) -> &'a mut [MaybeUninit] { // SAFETY: the caller must uphold the safety contract for `as_uninit_slice_mut`. unsafe { slice::from_raw_parts_mut(self.cast().as_ptr(), self.len()) } @@ -1799,15 +1799,17 @@ impl From<&T> for NonNull { } #[cfg(kani)] -#[unstable(feature="kani", issue="none")] +#[unstable(feature = "kani", issue = "none")] mod verify { - use super::*; - use crate::mem; - use crate::ptr::null_mut; use core::num::NonZeroUsize; use core::ptr::NonNull; + use kani::PointerGenerator; + use super::*; + use crate::mem; + use crate::ptr::null_mut; + trait SampleTrait { fn get_value(&self) -> i32; } @@ -1844,7 +1846,7 @@ mod verify { pub fn non_null_check_new() { let mut x: i32 = kani::any(); let xptr = &mut x; - let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() }; + let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() }; let _ = NonNull::new(maybe_null_ptr); } @@ -1862,10 +1864,10 @@ mod verify { const ARR_LEN: usize = 10000; let mut generator = PointerGenerator::::new(); let raw_ptr: *mut i8 = generator.any_in_bounds().ptr; - let nonnull_ptr = unsafe { NonNull::new(raw_ptr).unwrap()}; + let nonnull_ptr = unsafe { NonNull::new(raw_ptr).unwrap() }; unsafe { let result = nonnull_ptr.read(); - kani::assert( *nonnull_ptr.as_ptr() == result, "read returns the correct value"); + kani::assert(*nonnull_ptr.as_ptr() == result, "read returns the correct value"); } } @@ -1883,10 +1885,10 @@ mod verify { const ARR_LEN: usize = 10000; let mut generator = PointerGenerator::::new(); let raw_ptr: *mut i8 = generator.any_in_bounds().ptr; - let nonnull_ptr = unsafe { NonNull::new(raw_ptr).unwrap()}; + let nonnull_ptr = unsafe { NonNull::new(raw_ptr).unwrap() }; unsafe { let result = nonnull_ptr.read_volatile(); - kani::assert( *nonnull_ptr.as_ptr() == result, "read returns the correct value"); + kani::assert(*nonnull_ptr.as_ptr() == result, "read returns the correct value"); } } @@ -1905,15 +1907,15 @@ mod verify { let unaligned_nonnull_ptr = NonNull::new(unaligned_ptr).unwrap(); unsafe { let result = unaligned_nonnull_ptr.read_unaligned(); - kani::assert( *unaligned_nonnull_ptr.as_ptr() == result, "read returns the correct value"); + kani::assert( + *unaligned_nonnull_ptr.as_ptr() == result, + "read returns the correct value", + ); } // read an unaligned value from a packed struct let unaligned_value: u32 = kani::any(); - let packed = Packed { - _padding: kani::any::(), - unaligned: unaligned_value, - }; + let packed = Packed { _padding: kani::any::(), unaligned: unaligned_value }; let unaligned_ptr = ptr::addr_of!(packed.unaligned); let nonnull_packed_ptr = NonNull::new(unaligned_ptr as *mut u32).unwrap(); @@ -1927,7 +1929,7 @@ mod verify { const SIZE: usize = 100000; let mut generator = PointerGenerator::<100000>::new(); let raw_ptr: *mut i8 = generator.any_in_bounds().ptr; - let ptr = unsafe { NonNull::new(raw_ptr).unwrap()}; + let ptr = unsafe { NonNull::new(raw_ptr).unwrap() }; // Create a non-deterministic count value let count: usize = kani::any(); @@ -1941,7 +1943,9 @@ mod verify { pub fn non_null_check_addr() { // Create NonNull pointer & get pointer address let x = kani::any::() as *mut i32; - let Some(nonnull_xptr) = NonNull::new(x) else { return; }; + let Some(nonnull_xptr) = NonNull::new(x) else { + return; + }; let address = nonnull_xptr.addr(); } @@ -1950,7 +1954,9 @@ mod verify { pub fn non_null_check_align_offset() { // Create NonNull pointer let x = kani::any::() as *mut i32; - let Some(nonnull_xptr) = NonNull::new(x) else { return; }; + let Some(nonnull_xptr) = NonNull::new(x) else { + return; + }; // Call align_offset with valid align value let align: usize = kani::any(); @@ -1964,7 +1970,9 @@ mod verify { pub fn non_null_check_align_offset_negative() { // Create NonNull pointer let x = kani::any::() as *mut i8; - let Some(nonnull_xptr) = NonNull::new(x) else { return; }; + let Some(nonnull_xptr) = NonNull::new(x) else { + return; + }; // Generate align value that is not necessarily a power of two let invalid_align: usize = kani::any(); @@ -1993,7 +2001,7 @@ mod verify { // unit type let ptr_unit = NonNull::<()>::dangling(); // zero length slice from dangling unit pointer - let zero_len_slice = NonNull::slice_from_raw_parts(ptr_unit, 0); + let zero_len_slice = NonNull::slice_from_raw_parts(ptr_unit, 0); } // pub const fn from_raw_parts(data_pointer: NonNull<()>, metadata: ::Metadata,) -> NonNull @@ -2030,11 +2038,15 @@ mod verify { let metadata = core::ptr::metadata(trait_object); // Create NonNull from the data pointer and metadata - let nonnull_trait_object: NonNull = NonNull::from_raw_parts(trait_ptr, metadata); + let nonnull_trait_object: NonNull = + NonNull::from_raw_parts(trait_ptr, metadata); unsafe { // Ensure trait method and member is preserved - kani::assert( trait_object.get_value() == nonnull_trait_object.as_ref().get_value(), "trait method and member must correctly preserve"); + kani::assert( + trait_object.get_value() == nonnull_trait_object.as_ref().get_value(), + "trait method and member must correctly preserve", + ); } } @@ -2054,7 +2066,10 @@ mod verify { let nonnull_slice = NonNull::<[i8]>::slice_from_raw_parts(arr_raw_ptr, slice_len); // Ensure slice content is preserved, runtime at this step is proportional to ARR_LEN unsafe { - kani::assert(&arr[..slice_len] == nonnull_slice.as_ref(), "slice content must be preserve"); + kani::assert( + &arr[..slice_len] == nonnull_slice.as_ref(), + "slice content must be preserve", + ); } // TODO: zero-length example blocked by kani issue [#3670](https://github.com/model-checking/kani/issues/3670) @@ -2062,7 +2077,6 @@ mod verify { //let zero_length = NonNull::<[()]>::slice_from_raw_parts(dangling_ptr, 0); } - // pub const fn to_raw_parts(self) -> (NonNull<()>, ::Metadata) #[kani::proof_for_contract(NonNull::to_raw_parts)] pub fn non_null_check_to_raw_parts() { @@ -2077,11 +2091,12 @@ mod verify { let metadata = core::ptr::metadata(trait_object); // Create NonNull from the data pointer and metadata - let nonnull_trait_object: NonNull = NonNull::from_raw_parts(trait_ptr, metadata); - let (decomposed_data_ptr, decomposed_metadata) = NonNull::to_raw_parts(nonnull_trait_object); + let nonnull_trait_object: NonNull = + NonNull::from_raw_parts(trait_ptr, metadata); + let (decomposed_data_ptr, decomposed_metadata) = + NonNull::to_raw_parts(nonnull_trait_object); } - #[kani::proof_for_contract(NonNull::as_mut)] pub fn non_null_check_as_mut() { let mut x: i32 = kani::any(); @@ -2167,10 +2182,7 @@ mod verify { const ARR_SIZE: usize = 100000; let mut arr: [i32; ARR_SIZE] = kani::any(); let raw_ptr = arr.as_mut_ptr(); - let ptr = NonNull::slice_from_raw_parts( - NonNull::new(raw_ptr).unwrap(), - ARR_SIZE, - ); + let ptr = NonNull::slice_from_raw_parts(NonNull::new(raw_ptr).unwrap(), ARR_SIZE); let lower = kani::any_where(|x| *x < ARR_SIZE); let upper = kani::any_where(|x| *x < ARR_SIZE && *x >= lower); unsafe { @@ -2206,8 +2218,7 @@ mod verify { value: i32, } impl Drop for Droppable { - fn drop(&mut self) { - } + fn drop(&mut self) {} } let mut droppable = Droppable { value: kani::any() }; @@ -2244,9 +2255,8 @@ mod verify { if let Some(ptr) = NonNull::new(non_null_ptr) { let result = ptr.as_ptr(); } - } - + #[kani::proof_for_contract(NonNull::<[T]>::as_mut_ptr)] pub fn non_null_check_as_mut_ptr() { const ARR_LEN: usize = 100; @@ -2263,7 +2273,7 @@ mod verify { let result: NonNull = ptr.cast(); } } - + #[kani::proof_for_contract(NonNull::<[T]>::as_non_null_ptr)] pub fn non_null_check_as_non_null_ptr() { const ARR_LEN: usize = 100; @@ -2271,8 +2281,8 @@ mod verify { let slice = kani::slice::any_slice_of_array_mut(&mut values); let non_null_ptr = NonNull::new(slice as *mut [i32]).unwrap(); let result = non_null_ptr.as_non_null_ptr(); - } - + } + #[kani::proof] pub fn non_null_check_len() { // Create a non-deterministic NonNull pointer using kani::any() @@ -2295,7 +2305,8 @@ mod verify { let size: usize = 0; // Create a NonNull slice from the non-null pointer and size - let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(non_null_ptr, size) }; + let non_null_slice: NonNull<[i8]> = + unsafe { NonNull::slice_from_raw_parts(non_null_ptr, size) }; // Perform the is_empty check let is_empty = non_null_slice.is_empty(); @@ -2309,7 +2320,6 @@ mod verify { // Perform the alignment check let result = non_null_ptr.is_aligned(); - } #[kani::proof_for_contract(NonNull::is_aligned_to)] @@ -2323,7 +2333,6 @@ mod verify { // Perform the alignment check let result = non_null_ptr.is_aligned_to(align); - } #[kani::proof] @@ -2384,7 +2393,7 @@ mod verify { let new_addr = NonZeroUsize::new(ptr.as_ptr().addr() + new_offset).unwrap(); let result = ptr.with_addr(new_addr); } - + #[kani::proof_for_contract(NonNull::sub)] pub fn non_null_check_sub() { const SIZE: usize = 10000; @@ -2400,7 +2409,7 @@ mod verify { let result = ptr.sub(count); } } - + #[kani::proof_for_contract(NonNull::sub_ptr)] pub fn non_null_check_sub_ptr() { const SIZE: usize = core::mem::size_of::() * 1000; @@ -2487,13 +2496,21 @@ mod verify { generate_write_volatile_harness!(i32, 4, non_null_check_write_volatile_i32); generate_write_volatile_harness!(i64, 8, non_null_check_write_volatile_i64); generate_write_volatile_harness!(i128, 16, non_null_check_write_volatile_i128); - generate_write_volatile_harness!(isize, {core::mem::size_of::()}, non_null_check_write_volatile_isize); + generate_write_volatile_harness!( + isize, + { core::mem::size_of::() }, + non_null_check_write_volatile_isize + ); generate_write_volatile_harness!(u8, 1, non_null_check_write_volatile_u8); generate_write_volatile_harness!(u16, 2, non_null_check_write_volatile_u16); generate_write_volatile_harness!(u32, 4, non_null_check_write_volatile_u32); generate_write_volatile_harness!(u64, 8, non_null_check_write_volatile_u64); generate_write_volatile_harness!(u128, 16, non_null_check_write_volatile_u128); - generate_write_volatile_harness!(usize, {core::mem::size_of::()}, non_null_check_write_volatile_usize); + generate_write_volatile_harness!( + usize, + { core::mem::size_of::() }, + non_null_check_write_volatile_usize + ); generate_write_volatile_harness!((), 1, non_null_check_write_volatile_unit); #[kani::proof_for_contract(NonNull::byte_add)] @@ -2572,54 +2589,62 @@ mod verify { // Generate arbitrary pointers for src and dest let src_ptr = generator.any_in_bounds::().ptr; let dest_ptr = generator.any_in_bounds::().ptr; - // Wrap the raw pointers in NonNull + // Wrap the raw pointers in NonNull let src = NonNull::new(src_ptr).unwrap(); let dest = NonNull::new(dest_ptr).unwrap(); // Generate an arbitrary count using kani::any let count: usize = kani::any(); - unsafe { src.copy_to(dest, count);} + unsafe { + src.copy_to(dest, count); + } } #[kani::proof_for_contract(NonNull::::copy_from)] pub fn non_null_check_copy_from() { - // PointerGenerator instance - let mut generator = PointerGenerator::<16>::new(); - // Generate arbitrary pointers for src and dest - let src_ptr = generator.any_in_bounds::().ptr; - let dest_ptr = generator.any_in_bounds::().ptr; + // PointerGenerator instance + let mut generator = PointerGenerator::<16>::new(); + // Generate arbitrary pointers for src and dest + let src_ptr = generator.any_in_bounds::().ptr; + let dest_ptr = generator.any_in_bounds::().ptr; // Wrap the raw pointers in NonNull - let src = NonNull::new(src_ptr).unwrap(); - let dest = NonNull::new(dest_ptr).unwrap(); - // Generate an arbitrary count using kani::any - let count: usize = kani::any(); - unsafe { src.copy_from(dest, count);} + let src = NonNull::new(src_ptr).unwrap(); + let dest = NonNull::new(dest_ptr).unwrap(); + // Generate an arbitrary count using kani::any + let count: usize = kani::any(); + unsafe { + src.copy_from(dest, count); + } } #[kani::proof_for_contract(NonNull::::copy_to_nonoverlapping)] pub fn non_null_check_copy_to_nonoverlapping() { - // PointerGenerator instance - let mut generator = PointerGenerator::<16>::new(); - // Generate arbitrary pointers for src and dest - let src_ptr = generator.any_in_bounds::().ptr; - let dest_ptr = generator.any_in_bounds::().ptr; + // PointerGenerator instance + let mut generator = PointerGenerator::<16>::new(); + // Generate arbitrary pointers for src and dest + let src_ptr = generator.any_in_bounds::().ptr; + let dest_ptr = generator.any_in_bounds::().ptr; // Wrap the raw pointers in NonNull - let src = NonNull::new(src_ptr).unwrap(); - let dest = NonNull::new(dest_ptr).unwrap(); - // Generate an arbitrary count using kani::any - let count: usize = kani::any(); - unsafe { src.copy_to_nonoverlapping(dest, count);} + let src = NonNull::new(src_ptr).unwrap(); + let dest = NonNull::new(dest_ptr).unwrap(); + // Generate an arbitrary count using kani::any + let count: usize = kani::any(); + unsafe { + src.copy_to_nonoverlapping(dest, count); + } } #[kani::proof_for_contract(NonNull::::copy_from_nonoverlapping)] pub fn non_null_check_copy_from_nonoverlapping() { - // PointerGenerator instance - let mut generator = PointerGenerator::<16>::new(); - // Generate arbitrary pointers for src and dest - let src_ptr = generator.any_in_bounds::().ptr; - let dest_ptr = generator.any_in_bounds::().ptr; - // Wrap the raw pointers in NonNull - let src = NonNull::new(src_ptr).unwrap(); - let dest = NonNull::new(dest_ptr).unwrap(); - // Generate an arbitrary count using kani::any - let count: usize = kani::any(); - unsafe { src.copy_from_nonoverlapping(dest, count);} + // PointerGenerator instance + let mut generator = PointerGenerator::<16>::new(); + // Generate arbitrary pointers for src and dest + let src_ptr = generator.any_in_bounds::().ptr; + let dest_ptr = generator.any_in_bounds::().ptr; + // Wrap the raw pointers in NonNull + let src = NonNull::new(src_ptr).unwrap(); + let dest = NonNull::new(dest_ptr).unwrap(); + // Generate an arbitrary count using kani::any + let count: usize = kani::any(); + unsafe { + src.copy_from_nonoverlapping(dest, count); + } } } diff --git a/library/core/src/ptr/unique.rs b/library/core/src/ptr/unique.rs index fd0dd6c46681f..ec3c8a533fc7c 100644 --- a/library/core/src/ptr/unique.rs +++ b/library/core/src/ptr/unique.rs @@ -1,13 +1,13 @@ use safety::{ensures, requires}; + use crate::fmt; +#[cfg(kani)] +use crate::kani; use crate::marker::{PhantomData, Unsize}; use crate::ops::{CoerceUnsized, DispatchFromDyn}; use crate::pin::PinCoerceUnsized; use crate::ptr::NonNull; -#[cfg(kani)] -use crate::kani; - /// A wrapper around a raw non-null `*mut T` that indicates that the possessor /// of this wrapper owns the referent. Useful for building abstractions like /// `Box`, `Vec`, `String`, and `HashMap`. @@ -218,14 +218,14 @@ impl From> for Unique { } #[cfg(kani)] -#[unstable(feature="kani", issue="none")] +#[unstable(feature = "kani", issue = "none")] mod verify { use super::*; // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self #[kani::proof_for_contract(Unique::new_unchecked)] pub fn check_new_unchecked() { - let mut x : i32 = kani::any(); + let mut x: i32 = kani::any(); let xptr = &mut x; unsafe { let _ = Unique::new_unchecked(xptr as *mut i32); @@ -235,7 +235,7 @@ mod verify { // pub const fn new(ptr: *mut T) -> Option #[kani::proof_for_contract(Unique::new)] pub fn check_new() { - let mut x : i32 = kani::any(); + let mut x: i32 = kani::any(); let xptr = &mut x; let _ = Unique::new(xptr as *mut i32); } @@ -243,7 +243,7 @@ mod verify { // pub const fn as_ptr(self) -> *mut T #[kani::proof_for_contract(Unique::as_ptr)] pub fn check_as_ptr() { - let mut x : i32 = kani::any(); + let mut x: i32 = kani::any(); let xptr = &mut x; unsafe { let unique = Unique::new_unchecked(xptr as *mut i32); @@ -254,7 +254,7 @@ mod verify { // pub const fn as_non_null_ptr(self) -> NonNull #[kani::proof_for_contract(Unique::as_non_null_ptr)] pub fn check_as_non_null_ptr() { - let mut x : i32 = kani::any(); + let mut x: i32 = kani::any(); let xptr = &mut x; unsafe { let unique = Unique::new_unchecked(xptr as *mut i32); @@ -265,7 +265,7 @@ mod verify { // pub const unsafe fn as_ref(&self) -> &T #[kani::proof] pub fn check_as_ref() { - let mut x : i32 = kani::any(); + let mut x: i32 = kani::any(); let xptr = &mut x; unsafe { let unique = Unique::new_unchecked(xptr as *mut i32); @@ -276,7 +276,7 @@ mod verify { // pub const unsafe fn as_mut(&mut self) -> &mut T #[kani::proof] pub fn check_as_mut() { - let mut x : i32 = kani::any(); + let mut x: i32 = kani::any(); let xptr = &mut x; unsafe { let mut unique = Unique::new_unchecked(xptr as *mut i32); @@ -287,7 +287,7 @@ mod verify { // pub const fn cast(self) -> Unique #[kani::proof] pub fn check_cast() { - let mut x : i32 = kani::any(); + let mut x: i32 = kani::any(); let xptr = &mut x; unsafe { let unique = Unique::new_unchecked(xptr as *mut i32); diff --git a/library/core/src/slice/ascii.rs b/library/core/src/slice/ascii.rs index cae485a2051a6..072900a8c8bc7 100644 --- a/library/core/src/slice/ascii.rs +++ b/library/core/src/slice/ascii.rs @@ -4,10 +4,9 @@ use core::ascii::EscapeDefault; use crate::fmt::{self, Write}; use crate::intrinsics::const_eval_select; -use crate::{ascii, iter, mem, ops}; - #[cfg(kani)] use crate::kani; +use crate::{ascii, iter, mem, ops}; #[cfg(not(test))] impl [u8] { @@ -428,7 +427,7 @@ const fn is_ascii(s: &[u8]) -> bool { // Read subsequent words until the last aligned word, excluding the last // aligned word by itself to be done in tail check later, to ensure that // tail is always one `usize` at most to extra branch `byte_pos == len`. - #[safety::loop_invariant(byte_pos <= len + #[safety::loop_invariant(byte_pos <= len && byte_pos >= offset_to_aligned && word_ptr.addr() >= start.addr() + offset_to_aligned && byte_pos == word_ptr.addr() - start.addr())] @@ -481,7 +480,7 @@ pub mod verify { } else { let ptr = kani::any_where::(|val| *val != 0) as *const u8; kani::assume(ptr.is_aligned()); - unsafe{ + unsafe { assert_eq!(is_ascii(crate::slice::from_raw_parts(ptr, 0)), true); } } diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs index fcf901e3c9f43..12ec352f7c352 100644 --- a/library/core/src/slice/iter.rs +++ b/library/core/src/slice/iter.rs @@ -14,8 +14,8 @@ use crate::marker::PhantomData; use crate::mem::{self, SizedTypeProperties}; use crate::num::NonZero; use crate::ptr::{NonNull, without_provenance, without_provenance_mut}; -use crate::{cmp, fmt}; use crate::ub_checks::Invariant; +use crate::{cmp, fmt}; #[stable(feature = "boxed_slice_into_iter", since = "1.80.0")] impl !Iterator for [T] {} @@ -3628,12 +3628,18 @@ mod verify { check_safe_abstraction!(check_size_hint, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.size_hint(); }); - check_safe_abstraction!(check_nth, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth(kani::any()); }); - check_safe_abstraction!(check_advance_by, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.advance_by(kani::any()); }); + check_safe_abstraction!(check_nth, $ty, |iter: &mut Iter<'_, $ty>| { + let _ = iter.nth(kani::any()); + }); + check_safe_abstraction!(check_advance_by, $ty, |iter: &mut Iter<'_, $ty>| { + let _ = iter.advance_by(kani::any()); + }); check_safe_abstraction!(check_next_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.next_back(); }); - check_safe_abstraction!(check_nth_back, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.nth_back(kani::any()); }); + check_safe_abstraction!(check_nth_back, $ty, |iter: &mut Iter<'_, $ty>| { + let _ = iter.nth_back(kani::any()); + }); check_safe_abstraction!(check_next, $ty, |iter: &mut Iter<'_, $ty>| { let _ = iter.next(); }); diff --git a/library/core/src/str/lossy.rs b/library/core/src/str/lossy.rs index d6786eff487f3..e9f72155f39ba 100644 --- a/library/core/src/str/lossy.rs +++ b/library/core/src/str/lossy.rs @@ -3,7 +3,6 @@ use super::validations::utf8_char_width; use crate::fmt; use crate::fmt::{Formatter, Write}; use crate::iter::FusedIterator; - #[cfg(kani)] use crate::kani; diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index 6540608344fa1..0cb017a7ee3b6 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -38,16 +38,15 @@ issue = "27721" )] -use crate::cmp::Ordering; -use crate::convert::TryInto as _; -use crate::slice::memchr; -use crate::{cmp, fmt}; - #[cfg(all(target_arch = "x86_64", any(kani, target_feature = "sse2")))] use safety::{loop_invariant, requires}; +use crate::cmp::Ordering; +use crate::convert::TryInto as _; #[cfg(kani)] use crate::kani; +use crate::slice::memchr; +use crate::{cmp, fmt}; // Pattern diff --git a/library/core/src/str/validations.rs b/library/core/src/str/validations.rs index 4f344702df4ba..d8a4ebcfa42ca 100644 --- a/library/core/src/str/validations.rs +++ b/library/core/src/str/validations.rs @@ -2,10 +2,9 @@ use super::Utf8Error; use crate::intrinsics::const_eval_select; -use crate::mem; - #[cfg(kani)] use crate::kani; +use crate::mem; /// Returns the initial codepoint accumulator for the first byte. /// The first byte is special, only want bottom 5 bits for width 2, 4 bits @@ -306,7 +305,7 @@ pub mod verify { } else { let ptr = kani::any_where::(|val| *val != 0) as *const u8; kani::assume(ptr.is_aligned()); - unsafe{ + unsafe { run_utf8_validation(crate::slice::from_raw_parts(ptr, 0)); } } diff --git a/library/core/src/time.rs b/library/core/src/time.rs index 21b92453ecd26..cece16b96c9ce 100644 --- a/library/core/src/time.rs +++ b/library/core/src/time.rs @@ -19,14 +19,13 @@ //! assert_eq!(total, Duration::new(10, 7)); //! ``` -use safety::{ensures, Invariant}; +use safety::{Invariant, ensures}; + use crate::fmt; use crate::iter::Sum; -use crate::ops::{Add, AddAssign, Div, DivAssign, Mul, MulAssign, Sub, SubAssign}; - #[cfg(kani)] use crate::kani; - +use crate::ops::{Add, AddAssign, Div, DivAssign, Mul, MulAssign, Sub, SubAssign}; use crate::ub_checks::Invariant; const NANOS_PER_SEC: u32 = 1_000_000_000; @@ -1732,8 +1731,8 @@ impl Duration { #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] pub mod duration_verify { - use crate::kani; use super::*; + use crate::kani; impl kani::Arbitrary for Duration { fn any() -> Duration { @@ -1746,7 +1745,9 @@ pub mod duration_verify { fn safe_duration() -> Duration { let secs = kani::any::(); let nanos = kani::any::(); - kani::assume(nanos < NANOS_PER_SEC || secs.checked_add((nanos / NANOS_PER_SEC) as u64).is_some()); + kani::assume( + nanos < NANOS_PER_SEC || secs.checked_add((nanos / NANOS_PER_SEC) as u64).is_some(), + ); Duration::new(secs, nanos) } diff --git a/library/core/src/ub_checks.rs b/library/core/src/ub_checks.rs index 9b7a64a43000e..1fc87469263a0 100644 --- a/library/core/src/ub_checks.rs +++ b/library/core/src/ub_checks.rs @@ -223,7 +223,7 @@ mod predicates { /// Check if a float is representable in the given integer type pub fn float_to_int_in_range(value: Float) -> bool where - Float: core::convert::FloatToInt + Float: core::convert::FloatToInt, { let _ = value; true @@ -232,9 +232,10 @@ mod predicates { #[cfg(kani)] mod predicates { - pub use crate::kani::mem::{can_dereference, can_write, can_read_unaligned, can_write_unaligned, - same_allocation}; pub use crate::kani::float::float_to_int_in_range; + pub use crate::kani::mem::{ + can_dereference, can_read_unaligned, can_write, can_write_unaligned, same_allocation, + }; } /// This trait should be used to specify and check type safety invariants for a @@ -253,7 +254,7 @@ mod predicates { /// Therefore, validity invariants must be upheld at all times, while safety /// invariants only need to be upheld at the boundaries to safe code. pub trait Invariant { - /// Specify the type's safety invariants + /// Specify the type's safety invariants fn is_safe(&self) -> bool; } diff --git a/library/core/src/unicode/mod.rs b/library/core/src/unicode/mod.rs index 5ee17570bbc42..5cb495c287c64 100644 --- a/library/core/src/unicode/mod.rs +++ b/library/core/src/unicode/mod.rs @@ -34,7 +34,7 @@ pub const UNICODE_VERSION: (u8, u8, u8) = unicode_data::UNICODE_VERSION; #[cfg(kani)] mod verify { - use super::conversions::{to_upper, to_lower}; + use super::conversions::{to_lower, to_upper}; use crate::kani; /// Checks that `to_upper` does not trigger UB or panics for all valid characters. diff --git a/scripts/check_rustc.sh b/scripts/check_rustc.sh old mode 100644 new mode 100755 index 610f6157b20ce..52d9037d36565 --- a/scripts/check_rustc.sh +++ b/scripts/check_rustc.sh @@ -1,44 +1,123 @@ #!/bin/bash +# Runs the Rust bootstrap script in order to ensure the changes to this repo +# are compliant with the Rust repository tests. +# +# TODO: Need to enable full tidy run. -set -e +set -eu + +usage() { + echo "Usage: $0 [--help] [--bless]" + echo "Options:" + echo " -h, --help Show this help message" + echo " --bless Update library files using tidy" +} + +TIDY_MODE="" +# Parse command line arguments +while [[ $# -gt 0 ]]; do + case $1 in + -h|--help) + usage + exit 0 + ;; + --bless) + TIDY_MODE="--bless" + shift 1 + ;; + *) + echo "Error: Unknown option `$1`" + usage + exit 1 + ;; + esac +done # Set the working directory for your local repository -HEAD_DIR=$1 +REPO_DIR=$(git rev-parse --show-toplevel) # Temporary directory for upstream repository -TEMP_DIR=$(mktemp -d) +TMP_RUST_DIR=$(mktemp -d -t "check_rustc_XXXXXX") # Checkout your local repository echo "Checking out local repository..." -cd "$HEAD_DIR" +cd "$REPO_DIR" -# Get the commit ID from rustc --version +# Get the (short hash) commit ID from rustc --version echo "Retrieving commit ID..." COMMIT_ID=$(rustc --version | sed -e "s/.*(\(.*\) .*/\1/") -echo "$COMMIT_ID for rustc is" + +# Get the full commit ID for shallow clone +echo "Full commit id for $COMMIT_ID for is:" + +if [ -z "${GH_TOKEN:-}" ]; then + curl -o "${TMP_RUST_DIR}/output.json" -s --show-error \ + "https://api.github.com/repos/rust-lang/rust/commits?sha=${COMMIT_ID}&per_page=1" +else + # Use token if possible to avoid being throttled + curl -o "${TMP_RUST_DIR}/output.json" -s --show-error \ + --request GET \ + --url "https://api.github.com/repos/rust-lang/rust/commits?sha=${COMMIT_ID}&per_page=1" \ + --header "Accept: application/vnd.github+json" \ + --header "Authorization: Bearer $GH_TOKEN" +fi +cat "${TMP_RUST_DIR}/output.json" # Dump the file in case `curl` fails. + +COMMIT_ID=$(cat "${TMP_RUST_DIR}/output.json" | jq -r '.[0].sha') +echo "- $COMMIT_ID" # Clone the rust-lang/rust repository -echo "Cloning rust-lang/rust repository..." -git clone https://github.com/rust-lang/rust.git "$TEMP_DIR/upstream" +echo "Cloning rust-lang/rust repository into ${TMP_RUST_DIR}..." +pushd "$TMP_RUST_DIR" > /dev/null +git init +git remote add origin https://github.com/rust-lang/rust.git +git fetch --depth 1 origin $COMMIT_ID -# Checkout the specific commit echo "Checking out commit $COMMIT_ID..." -cd "$TEMP_DIR/upstream" git checkout "$COMMIT_ID" +git submodule update --init --depth 1 +popd # Copy your library to the upstream directory echo "Copying library to upstream directory..." -rm -rf "$TEMP_DIR/upstream/library" -cp -r "$HEAD_DIR/library" "$TEMP_DIR/upstream" +rm -rf "${TMP_RUST_DIR}/library" +cp -r "${REPO_DIR}/library" "${TMP_RUST_DIR}" -# Run the tests -cd "$TEMP_DIR/upstream" +# Configure repository +pushd "${TMP_RUST_DIR}" +# Download LLVM binaries from Rust's CI instead of building them +./configure --set=llvm.download-ci-llvm=true export RUSTFLAGS="--check-cfg cfg(kani) --check-cfg cfg(feature,values(any()))" +export RUST_BACKTRACE=1 +unset GITHUB_ACTIONS # Bootstrap script requires specific repo layout when run from an action. Disable that. + +# Run tidy +if [ "${TIDY_MODE}" == "--bless" ]; +then + echo "Run rustfmt" + # TODO: This should be: + # ./x test tidy --bless + ./x fmt + cp -r "${TMP_RUST_DIR}/library" "${REPO_DIR}" +else + # TODO: This should be: + # ./x test tidy + echo "Check format" + if ! ./x fmt --check; then + echo "Format check failed. Run $0 --bless to fix the failures." + # Clean up the temporary directory + popd + rm -rf "$TMP_RUST_DIR" + exit 1 + fi +fi + +# Run tests +cd "$TMP_RUST_DIR" echo "Running tests..." -./configure --set=llvm.download-ci-llvm=true ./x test --stage 0 library/std echo "Tests completed." # Clean up the temporary directory -rm -rf "$TEMP_DIR" +rm -rf "$TMP_RUST_DIR" diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 63df2886d0d71..b0018b720265c 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -144,7 +144,9 @@ build_kani() { pushd "$directory" source "kani-dependencies" # Check if installed versions are correct. - if ./scripts/check-cbmc-version.py --major ${CBMC_MAJOR} --minor ${CBMC_MINOR} && ./scripts/check_kissat_version.sh; then + if ./scripts/check-cbmc-version.py \ + --major ${CBMC_MAJOR} --minor ${CBMC_MINOR} --patch ${CBMC_PATCH} \ + && ./scripts/check_kissat_version.sh; then echo "Dependencies are up-to-date" else os_name=$(uname -s)