diff --git a/.github/workflows/rapx.yml b/.github/workflows/rapx.yml new file mode 100644 index 0000000000000..780b612774ef6 --- /dev/null +++ b/.github/workflows/rapx.yml @@ -0,0 +1,47 @@ +name: RAPx + +on: + workflow_dispatch: + push: + branches: [main] + pull_request: + branches: [main] + +env: + RAPX_VERSION: "8864b6113c950365a74a3fa35bbfc32ad0660af5" + TOOLCHAIN: "nightly-2025-11-25" + +jobs: + verify-slice: + name: Verify core::slice with RAPx + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + with: + submodules: true + + - name: Set up Rust toolchain + run: | + rustup toolchain install $TOOLCHAIN + rustup component add rust-src --toolchain $TOOLCHAIN + + - name: Clone and install RAPx + run: | + rm -rf RAPx + git clone --branch verify-std https://github.com/safer-rust/RAPx.git + cd RAPx + git fetch origin $RAPX_VERSION + git checkout $RAPX_VERSION + ./install.sh + + - name: Run RAPx verification + run: | + export RUSTUP_TOOLCHAIN=$(rustup show active-toolchain | cut -d ' ' -f 1) + export RAPX_SYSROOT=$(rustc --print sysroot) + export LD_LIBRARY_PATH="$RAPX_SYSROOT/lib" + export RUSTFLAGS="--cfg=rapx -Zcrate-attr=feature(register_tool) -Zcrate-attr=register_tool(rapx)" + export __CARGO_TESTS_ONLY_SRC_ROOT="$(pwd)/library" + # `core` is a dependency (not a workspace member) of `library`, so RAPx + # only analyzes it as a primary package when invoked from library/core. + cd library/core + cargo +$RUSTUP_TOOLCHAIN rapx verify --module slice --mode targeted diff --git a/library/Cargo.lock b/library/Cargo.lock index 8f60cea459c7d..6847af3e7b95e 100644 --- a/library/Cargo.lock +++ b/library/Cargo.lock @@ -28,6 +28,7 @@ version = "0.0.0" dependencies = [ "compiler_builtins", "core", + "safety", ] [[package]] @@ -67,6 +68,9 @@ dependencies = [ [[package]] name = "core" version = "0.0.0" +dependencies = [ + "safety", +] [[package]] name = "coretests" @@ -213,6 +217,39 @@ dependencies = [ "unwind", ] +[[package]] +name = "proc-macro-error" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da25490ff9892aab3fcf7c36f08cfb902dd3e71ca0f9f9517bea02a73a5ce38c" +dependencies = [ + "proc-macro-error-attr", + "proc-macro2", + "quote", + "syn 1.0.109", + "version_check", +] + +[[package]] +name = "proc-macro-error-attr" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a1be40180e52ecc98ad80b184934baf3d0d29f979574e439af5a55274b35f869" +dependencies = [ + "proc-macro2", + "quote", + "version_check", +] + +[[package]] +name = "proc-macro2" +version = "1.0.106" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8fd00f0bb2e90d81d1044c2b32617f68fcb9fa3bb7640c23e9c748e53fb30934" +dependencies = [ + "unicode-ident", +] + [[package]] name = "proc_macro" version = "0.0.0" @@ -229,6 +266,15 @@ dependencies = [ "cc", ] +[[package]] +name = "quote" +version = "1.0.46" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dfbc457d0c7a0759a614551b11a6409e5951f6c7537be1f1b7682b9ae9230368" +dependencies = [ + "proc-macro2", +] + [[package]] name = "r-efi" version = "5.3.0" @@ -313,6 +359,16 @@ dependencies = [ "std", ] +[[package]] +name = "safety" +version = "0.1.0" +dependencies = [ + "proc-macro-error", + "proc-macro2", + "quote", + "syn 2.0.118", +] + [[package]] name = "shlex" version = "1.3.0" @@ -342,6 +398,7 @@ dependencies = [ "rand", "rand_xorshift", "rustc-demangle", + "safety", "std_detect", "unwind", "vex-sdk", @@ -359,6 +416,27 @@ dependencies = [ "rustc-std-workspace-core", ] +[[package]] +name = "syn" +version = "1.0.109" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" +dependencies = [ + "proc-macro2", + "unicode-ident", +] + +[[package]] +name = "syn" +version = "2.0.118" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1b9ae57f904213ebb649ce6895b8a66c66f0203b9319718f69a5612a065b1422" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + [[package]] name = "sysroot" version = "0.0.0" @@ -379,6 +457,12 @@ dependencies = [ "std", ] +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + [[package]] name = "unwind" version = "0.0.0" @@ -398,6 +482,12 @@ dependencies = [ "rustc-std-workspace-core", ] +[[package]] +name = "version_check" +version = "0.9.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" + [[package]] name = "vex-sdk" version = "0.27.1" diff --git a/library/core/Cargo.toml b/library/core/Cargo.toml index 7bf2f62b690b3..66452e569f778 100644 --- a/library/core/Cargo.toml +++ b/library/core/Cargo.toml @@ -44,7 +44,8 @@ check-cfg = [ 'cfg(target_has_reliable_f128_math)', 'cfg(llvm_enzyme)', 'cfg(kani)', - 'cfg(flux)' + 'cfg(flux)', + 'cfg(rapx)', ] [package.metadata.flux] diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs index 3619e2f544947..f3484a113c296 100644 --- a/library/core/src/lib.rs +++ b/library/core/src/lib.rs @@ -412,3 +412,6 @@ include!("primitive_docs.rs"); #[cfg(flux)] mod flux_info; + +#[cfg(rapx)] +mod rapx_macro {} diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index 52556a7019014..32617161c33ef 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -525,6 +525,12 @@ mod mut_ptr; #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_diagnostic_item = "ptr_copy_nonoverlapping"] +#[cfg_attr(rapx, rapx::requires(Align(src, T)))] +#[cfg_attr(rapx, rapx::requires(Align(dst, T)))] +#[cfg_attr(rapx, rapx::requires(ValidPtr(src, T, count)))] +#[cfg_attr(rapx, rapx::requires(ValidPtr(dst, T, count)))] +#[cfg_attr(rapx, rapx::requires(NonOverlap(dst, src, T, count)))] +#[cfg_attr(rapx, rapx::requires(ValidNum(size_of(T) * count <= isize::MAX)))] pub const unsafe fn copy_nonoverlapping(src: *const T, dst: *mut T, count: usize) { ub_checks::assert_unsafe_precondition!( check_language_ub, @@ -622,6 +628,10 @@ pub const unsafe fn copy_nonoverlapping(src: *const T, dst: *mut T, count: us #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[rustc_diagnostic_item = "ptr_copy"] +#[cfg_attr(rapx, rapx::requires(ValidPtr(src, T, count)))] +#[cfg_attr(rapx, rapx::requires(Align(src, T)))] +#[cfg_attr(rapx, rapx::requires(ValidPtr(dst, T, count)))] +#[cfg_attr(rapx, rapx::requires(Align(dst, T)))] pub const unsafe fn copy(src: *const T, dst: *mut T, count: usize) { // SAFETY: the safety contract for `copy` must be upheld by the caller. unsafe { @@ -1360,6 +1370,9 @@ pub const unsafe fn swap(x: *mut T, y: *mut T) { #[rustc_diagnostic_item = "ptr_swap_nonoverlapping"] #[rustc_allow_const_fn_unstable(const_eval_select)] // both implementations behave the same #[track_caller] +#[cfg_attr(rapx, rapx::requires(ValidPtr(x, T, count)))] +#[cfg_attr(rapx, rapx::requires(Align(x, T)))] +#[cfg_attr(rapx, rapx::requires(NonOverlap(x, y, T, count)))] pub const unsafe fn swap_nonoverlapping(x: *mut T, y: *mut T, count: usize) { ub_checks::assert_unsafe_precondition!( check_library_ub, @@ -2224,6 +2237,9 @@ pub unsafe fn write_volatile(dst: *mut T, src: T) { let new_addr = usize::wrapping_add(product, p.addr()); *result != usize::MAX && new_addr % a == 0 })] +/// # Safety +/// The alignment `a` must be a non-zero power of two. +#[cfg_attr(rapx, rapx::requires(ValidNum(a != 0)))] pub(crate) unsafe fn align_offset(p: *const T, a: usize) -> usize { // FIXME(#75598): Direct use of these intrinsics improves codegen significantly at opt-level <= // 1, where the method versions of these operations are not inlined. diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs index 8e19bbdca0cd4..9734a55c44f6e 100644 --- a/library/core/src/slice/mod.rs +++ b/library/core/src/slice/mod.rs @@ -327,6 +327,7 @@ impl [T] { #[inline] #[stable(feature = "slice_first_last_chunk", since = "1.77.0")] #[rustc_const_stable(feature = "slice_first_last_chunk", since = "1.77.0")] + #[cfg_attr(rapx, rapx::verify)] pub const fn first_chunk(&self) -> Option<&[T; N]> { if self.len() < N { None @@ -357,6 +358,7 @@ impl [T] { #[inline] #[stable(feature = "slice_first_last_chunk", since = "1.77.0")] #[rustc_const_stable(feature = "const_slice_first_last_chunk", since = "1.83.0")] + #[cfg_attr(rapx, rapx::verify)] pub const fn first_chunk_mut(&mut self) -> Option<&mut [T; N]> { if self.len() < N { None @@ -387,6 +389,7 @@ impl [T] { #[inline] #[stable(feature = "slice_first_last_chunk", since = "1.77.0")] #[rustc_const_stable(feature = "slice_first_last_chunk", since = "1.77.0")] + #[cfg_attr(rapx, rapx::verify)] pub const fn split_first_chunk(&self) -> Option<(&[T; N], &[T])> { let Some((first, tail)) = self.split_at_checked(N) else { return None }; @@ -417,6 +420,7 @@ impl [T] { #[inline] #[stable(feature = "slice_first_last_chunk", since = "1.77.0")] #[rustc_const_stable(feature = "const_slice_first_last_chunk", since = "1.83.0")] + #[cfg_attr(rapx, rapx::verify)] pub const fn split_first_chunk_mut( &mut self, ) -> Option<(&mut [T; N], &mut [T])> { @@ -447,6 +451,7 @@ impl [T] { #[inline] #[stable(feature = "slice_first_last_chunk", since = "1.77.0")] #[rustc_const_stable(feature = "slice_first_last_chunk", since = "1.77.0")] + #[cfg_attr(rapx, rapx::verify)] pub const fn split_last_chunk(&self) -> Option<(&[T], &[T; N])> { let Some(index) = self.len().checked_sub(N) else { return None }; let (init, last) = self.split_at(index); @@ -478,6 +483,7 @@ impl [T] { #[inline] #[stable(feature = "slice_first_last_chunk", since = "1.77.0")] #[rustc_const_stable(feature = "const_slice_first_last_chunk", since = "1.83.0")] + #[cfg_attr(rapx, rapx::verify)] pub const fn split_last_chunk_mut( &mut self, ) -> Option<(&mut [T], &mut [T; N])> { @@ -509,6 +515,7 @@ impl [T] { #[inline] #[stable(feature = "slice_first_last_chunk", since = "1.77.0")] #[rustc_const_stable(feature = "const_slice_last_chunk", since = "1.80.0")] + #[cfg_attr(rapx, rapx::verify)] pub const fn last_chunk(&self) -> Option<&[T; N]> { // FIXME(const-hack): Without const traits, we need this instead of `get`. let Some(index) = self.len().checked_sub(N) else { return None }; @@ -539,6 +546,7 @@ impl [T] { #[inline] #[stable(feature = "slice_first_last_chunk", since = "1.77.0")] #[rustc_const_stable(feature = "const_slice_first_last_chunk", since = "1.83.0")] + #[cfg_attr(rapx, rapx::verify)] pub const fn last_chunk_mut(&mut self) -> Option<&mut [T; N]> { // FIXME(const-hack): Without const traits, we need this instead of `get`. let Some(index) = self.len().checked_sub(N) else { return None }; @@ -639,6 +647,8 @@ impl [T] { #[must_use] #[track_caller] #[rustc_const_unstable(feature = "const_index", issue = "143775")] + #[cfg_attr(rapx, rapx::verify)] + #[cfg_attr(rapx, rapx::requires(InBound(index_access(self, index))))] pub const unsafe fn get_unchecked(&self, index: I) -> &I::Output where I: [const] SliceIndex, @@ -684,6 +694,8 @@ impl [T] { #[must_use] #[track_caller] #[rustc_const_unstable(feature = "const_index", issue = "143775")] + #[cfg_attr(rapx, rapx::verify)] + #[cfg_attr(rapx, rapx::requires(InBound(index_access(self, index))))] pub const unsafe fn get_unchecked_mut(&mut self, index: I) -> &mut I::Output where I: [const] SliceIndex, @@ -948,6 +960,9 @@ impl [T] { /// [undefined behavior]: https://doc.rust-lang.org/reference/behavior-considered-undefined.html #[unstable(feature = "slice_swap_unchecked", issue = "88539")] #[track_caller] + #[cfg_attr(rapx, rapx::verify)] + #[cfg_attr(rapx, rapx::requires(ValidNum(a, "[0,self.len())")))] + #[cfg_attr(rapx, rapx::requires(ValidNum(b, "[0,self.len())")))] pub const unsafe fn swap_unchecked(&mut self, a: usize, b: usize) { assert_unsafe_precondition!( check_library_ub, @@ -978,6 +993,7 @@ impl [T] { #[stable(feature = "rust1", since = "1.0.0")] #[rustc_const_stable(feature = "const_slice_reverse", since = "1.90.0")] #[inline] + #[cfg_attr(rapx, rapx::verify)] pub const fn reverse(&mut self) { let half_len = self.len() / 2; let Range { start, end } = self.as_mut_ptr_range(); @@ -1345,6 +1361,9 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[cfg_attr(rapx, rapx::verify)] + #[cfg_attr(rapx, rapx::requires(ValidNum(N, "[1,)")))] + #[cfg_attr(rapx, rapx::requires(ValidNum(len(self) % N == 0)))] pub const unsafe fn as_chunks_unchecked(&self) -> &[[T; N]] { assert_unsafe_precondition!( check_language_ub, @@ -1403,6 +1422,7 @@ impl [T] { #[inline] #[track_caller] #[must_use] + #[cfg_attr(rapx, rapx::verify)] pub const fn as_chunks(&self) -> (&[[T; N]], &[T]) { assert!(N != 0, "chunk size must be non-zero"); let len_rounded_down = self.len() / N * N; @@ -1450,6 +1470,7 @@ impl [T] { #[inline] #[track_caller] #[must_use] + #[cfg_attr(rapx, rapx::verify)] pub const fn as_rchunks(&self) -> (&[T], &[[T; N]]) { assert!(N != 0, "chunk size must be non-zero"); let len = self.len() / N; @@ -1505,6 +1526,9 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[cfg_attr(rapx, rapx::verify)] + #[cfg_attr(rapx, rapx::requires(ValidNum(N, "[1,)")))] + #[cfg_attr(rapx, rapx::requires(ValidNum(len(self) % N == 0)))] pub const unsafe fn as_chunks_unchecked_mut(&mut self) -> &mut [[T; N]] { assert_unsafe_precondition!( check_language_ub, @@ -1559,6 +1583,7 @@ impl [T] { #[inline] #[track_caller] #[must_use] + #[cfg_attr(rapx, rapx::verify)] pub const fn as_chunks_mut(&mut self) -> (&mut [[T; N]], &mut [T]) { assert!(N != 0, "chunk size must be non-zero"); let len_rounded_down = self.len() / N * N; @@ -2043,6 +2068,8 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[cfg_attr(rapx, rapx::verify)] + #[cfg_attr(rapx, rapx::requires(ValidNum(mid, [0,self.len()])))] pub const unsafe fn split_at_unchecked(&self, mid: usize) -> (&[T], &[T]) { // FIXME(const-hack): the const function `from_raw_parts` is used to make this // function const; previously the implementation used @@ -2097,6 +2124,8 @@ impl [T] { #[inline] #[must_use] #[track_caller] + #[cfg_attr(rapx, rapx::verify)] + #[cfg_attr(rapx, rapx::requires(ValidNum(mid, [0,self.len()])))] pub const unsafe fn split_at_mut_unchecked(&mut self, mid: usize) -> (&mut [T], &mut [T]) { let len = self.len(); let ptr = self.as_mut_ptr(); @@ -2158,6 +2187,7 @@ impl [T] { #[rustc_const_stable(feature = "split_at_checked", since = "1.80.0")] #[inline] #[must_use] + #[cfg_attr(rapx, rapx::verify)] pub const fn split_at_checked(&self, mid: usize) -> Option<(&[T], &[T])> { if mid <= self.len() { // SAFETY: `[ptr; mid]` and `[mid; len]` are inside `self`, which @@ -2197,6 +2227,7 @@ impl [T] { #[rustc_const_stable(feature = "const_slice_split_at_mut", since = "1.83.0")] #[inline] #[must_use] + #[cfg_attr(rapx, rapx::verify)] pub const fn split_at_mut_checked(&mut self, mid: usize) -> Option<(&mut [T], &mut [T])> { if mid <= self.len() { // SAFETY: `[ptr; mid]` and `[mid; len]` are inside `self`, which @@ -2975,6 +3006,7 @@ impl [T] { /// ``` #[stable(feature = "rust1", since = "1.0.0")] #[inline] + #[cfg_attr(rapx, rapx::verify)] pub fn binary_search_by<'a, F>(&'a self, mut f: F) -> Result where F: FnMut(&'a T) -> Ordering, @@ -3508,6 +3540,7 @@ impl [T] { /// ``` #[unstable(feature = "slice_partition_dedup", issue = "54279")] #[inline] + #[cfg_attr(rapx, rapx::verify)] pub fn partition_dedup_by(&mut self, mut same_bucket: F) -> (&mut [T], &mut [T]) where F: FnMut(&mut T, &mut T) -> bool, @@ -3676,6 +3709,7 @@ impl [T] { /// ``` #[stable(feature = "slice_rotate", since = "1.26.0")] #[rustc_const_stable(feature = "const_slice_rotate", since = "1.92.0")] + #[cfg_attr(rapx, rapx::verify)] pub const fn rotate_left(&mut self, mid: usize) { assert!(mid <= self.len()); let k = self.len() - mid; @@ -3722,6 +3756,7 @@ impl [T] { /// ``` #[stable(feature = "slice_rotate", since = "1.26.0")] #[rustc_const_stable(feature = "const_slice_rotate", since = "1.92.0")] + #[cfg_attr(rapx, rapx::verify)] pub const fn rotate_right(&mut self, k: usize) { assert!(k <= self.len()); let mid = self.len() - k; @@ -3898,6 +3933,7 @@ impl [T] { #[stable(feature = "copy_from_slice", since = "1.9.0")] #[rustc_const_stable(feature = "const_copy_from_slice", since = "1.87.0")] #[track_caller] + #[cfg_attr(rapx, rapx::verify)] pub const fn copy_from_slice(&mut self, src: &[T]) where T: Copy, @@ -3932,6 +3968,7 @@ impl [T] { /// ``` #[stable(feature = "copy_within", since = "1.37.0")] #[track_caller] + #[cfg_attr(rapx, rapx::verify)] pub fn copy_within>(&mut self, src: R, dest: usize) where T: Copy, @@ -4000,6 +4037,7 @@ impl [T] { #[stable(feature = "swap_with_slice", since = "1.27.0")] #[rustc_const_unstable(feature = "const_swap_with_slice", issue = "142204")] #[track_caller] + #[cfg_attr(rapx, rapx::verify)] pub const fn swap_with_slice(&mut self, other: &mut [T]) { assert!(self.len() == other.len(), "destination and source slices have different lengths"); // SAFETY: `self` is valid for `self.len()` elements by definition, and `src` was @@ -4110,6 +4148,8 @@ impl [T] { ((suffix.as_ptr()).add(suffix.len()) == (self.as_ptr()).add(self.len())) ) ) )] + #[cfg_attr(rapx, rapx::requires(ValidTransmute(T, U)))] + #[cfg_attr(rapx, rapx::verify)] pub unsafe fn align_to(&self) -> (&[T], &[U], &[T]) { // Note that most of this function will be constant-evaluated, if U::IS_ZST || T::IS_ZST { @@ -4208,6 +4248,8 @@ impl [T] { ((suffix.as_ptr()).add(suffix.len()) == old((self.as_ptr()).add(self.len()))) )) )] + #[cfg_attr(rapx, rapx::requires(ValidTransmute(T, U)))] + #[cfg_attr(rapx, rapx::verify)] pub unsafe fn align_to_mut(&mut self) -> (&mut [T], &mut [U], &mut [T]) { // Note that most of this function will be constant-evaluated, if U::IS_ZST || T::IS_ZST { @@ -4299,6 +4341,7 @@ impl [T] { /// ``` #[unstable(feature = "portable_simd", issue = "86656")] #[must_use] + #[cfg_attr(rapx, rapx::verify)] pub fn as_simd(&self) -> (&[T], &[Simd], &[T]) where Simd: AsRef<[T; LANES]>, @@ -4335,6 +4378,7 @@ impl [T] { /// method for something like `LANES == 3`. #[unstable(feature = "portable_simd", issue = "86656")] #[must_use] + #[cfg_attr(rapx, rapx::verify)] pub fn as_simd_mut(&mut self) -> (&mut [T], &mut [Simd], &mut [T]) where Simd: AsMut<[T; LANES]>, @@ -4788,6 +4832,9 @@ impl [T] { #[stable(feature = "get_many_mut", since = "1.86.0")] #[inline] #[track_caller] + #[cfg_attr(rapx, rapx::verify)] + #[cfg_attr(rapx, rapx::requires(InBound(index_access(self, indices))))] + #[cfg_attr(rapx, rapx::requires(NonOverlap(indices)))] pub unsafe fn get_disjoint_unchecked_mut( &mut self, indices: [I; N], @@ -4855,6 +4902,7 @@ impl [T] { /// ``` #[stable(feature = "get_many_mut", since = "1.86.0")] #[inline] + #[cfg_attr(rapx, rapx::verify)] pub fn get_disjoint_mut( &mut self, indices: [I; N], @@ -5068,6 +5116,8 @@ impl [[T; N]] { /// ``` #[stable(feature = "slice_flatten", since = "1.80.0")] #[rustc_const_stable(feature = "const_slice_flatten", since = "1.87.0")] + #[cfg_attr(rapx, rapx::verify)] + #[cfg_attr(rapx, rapx::requires(ValidTransmute([T; N], T)))] pub const fn as_flattened(&self) -> &[T] { let len = if T::IS_ZST { self.len().checked_mul(N).expect("slice len overflow") @@ -5110,6 +5160,8 @@ impl [[T; N]] { /// ``` #[stable(feature = "slice_flatten", since = "1.80.0")] #[rustc_const_stable(feature = "const_slice_flatten", since = "1.87.0")] + #[cfg_attr(rapx, rapx::verify)] + #[cfg_attr(rapx, rapx::requires(ValidTransmute([T; N], T)))] pub const fn as_flattened_mut(&mut self) -> &mut [T] { let len = if T::IS_ZST { self.len().checked_mul(N).expect("slice len overflow") @@ -5184,6 +5236,8 @@ impl [f64] { /// # Safety /// `T` must implement one of `Copy` or `TrivialClone`. #[track_caller] +#[cfg_attr(rapx, rapx::verify)] +#[cfg_attr(rapx, rapx::requires(any(Trait(T, Copy), Trait(T, TrivialClone))))] const unsafe fn copy_from_slice_impl(dest: &mut [T], src: &[T]) { // The panic code path was put into a cold function to not bloat the // call site. @@ -5301,6 +5355,7 @@ impl SlicePattern for [T; N] { /// This will do `binomial(N + 1, 2) = N * (N + 1) / 2 = 0, 1, 3, 6, 10, ..` /// comparison operations. #[inline] +#[cfg_attr(rapx, rapx::verify)] fn get_disjoint_check_valid( indices: &[I; N], len: usize, diff --git a/library/core/src/slice/raw.rs b/library/core/src/slice/raw.rs index 80b2176933dab..1d1f5321b70ce 100644 --- a/library/core/src/slice/raw.rs +++ b/library/core/src/slice/raw.rs @@ -121,6 +121,13 @@ use crate::{array, ptr, ub_checks}; #[must_use] #[rustc_diagnostic_item = "slice_from_raw_parts"] #[track_caller] +#[cfg_attr(rapx, rapx::requires(NonNull(data)))] +#[cfg_attr(rapx, rapx::requires(ValidPtr(data, T, len)))] +#[cfg_attr(rapx, rapx::requires(Init(data, T, len)))] +#[cfg_attr(rapx, rapx::requires(Alive(data)))] +#[cfg_attr(rapx, rapx::requires(Alias(data)))] +#[cfg_attr(rapx, rapx::requires(Align(data, T)))] +#[cfg_attr(rapx, rapx::requires(ValidNum(size_of(T) * len <= isize::MAX)))] pub const unsafe fn from_raw_parts<'a, T>(data: *const T, len: usize) -> &'a [T] { // SAFETY: the caller must uphold the safety contract for `from_raw_parts`. unsafe { @@ -176,6 +183,13 @@ pub const unsafe fn from_raw_parts<'a, T>(data: *const T, len: usize) -> &'a [T] #[must_use] #[rustc_diagnostic_item = "slice_from_raw_parts_mut"] #[track_caller] +#[cfg_attr(rapx, rapx::requires(NonNull(data)))] +#[cfg_attr(rapx, rapx::requires(ValidPtr(data, T, len)))] +#[cfg_attr(rapx, rapx::requires(Init(data, T, len)))] +#[cfg_attr(rapx, rapx::requires(Alive(data)))] +#[cfg_attr(rapx, rapx::requires(Alias(data)))] +#[cfg_attr(rapx, rapx::requires(Align(data, T)))] +#[cfg_attr(rapx, rapx::requires(ValidNum(size_of(T) * len <= isize::MAX)))] pub const unsafe fn from_raw_parts_mut<'a, T>(data: *mut T, len: usize) -> &'a mut [T] { // SAFETY: the caller must uphold the safety contract for `from_raw_parts_mut`. unsafe {