Rename typed_swap to typed_swap_nonoverlapping.

Propagated from rust-lang/rust#134757.

Author: Remi Delmas

docs/src/rust-feature-support/intrinsics.md

@@ -220,7 +220,7 @@ truncf64 | Yes | |
 try | No | [#267](https://github.com/model-checking/kani/issues/267) |
 type_id | Yes | |
 type_name | Yes | |
-typed_swap | Yes | |
+typed_swap_nonoverlapping | Yes | |
 unaligned_volatile_load | No | See [Notes - Concurrency](#concurrency) |
 unaligned_volatile_store | No | See [Notes - Concurrency](#concurrency) |
 unchecked_add | Yes | |

kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs

@@ -1864,7 +1864,7 @@ impl GotocCtx<'_> {
     }
 
     /// Swaps the memory contents pointed to by arguments `x` and `y`, respectively, which is
-    /// required for the `typed_swap` intrinsic.
+    /// required for the `typed_swap_nonoverlapping` intrinsic.
     ///
     /// The standard library API requires that `x` and `y` are readable and writable as their
     /// (common) type (which auto-generated checks for dereferencing will take care of), and the

kani-compiler/src/intrinsics.rs

@@ -389,7 +389,7 @@ impl Intrinsic {
                 assert_sig_matches!(sig, => RigidTy::Ref(_, _, Mutability::Not));
                 Self::TypeName
             }
-            "typed_swap" => {
+            "typed_swap_nonoverlapping" => {
                 assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::RawPtr(_, Mutability::Mut) => RigidTy::Tuple(_));
                 Self::TypedSwap
             }

tests/expected/uninit/intrinsics/expected

@@ -6,11 +6,11 @@ std::ptr::write::<std::mem::MaybeUninit<u8>>.assertion.1\
 	 - Status: FAILURE\
 	 - Description: "Interaction between raw pointers and unions is not yet supported."\
 
-check_typed_swap.assertion.1\
+check_typed_swap_nonoverlapping.assertion.1\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`"
 
-check_typed_swap.assertion.2\
+check_typed_swap_nonoverlapping.assertion.2\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*mut u8`"
 
@@ -35,8 +35,8 @@ std::ptr::read::<u8>.assertion.2\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u8`"
 
 Summary:
-Verification failed for - check_typed_swap_safe
-Verification failed for - check_typed_swap
+Verification failed for - check_typed_swap_nonoverlapping_safe
+Verification failed for - check_typed_swap_nonoverlapping
 Verification failed for - check_volatile_load
 Verification failed for - check_compare_bytes
 Verification failed for - check_copy_read

tests/expected/uninit/intrinsics/intrinsics.rs

@@ -131,23 +131,23 @@ fn check_volatile_store_and_load_safe() {
 }
 
 #[kani::proof]
-fn check_typed_swap() {
+fn check_typed_swap_nonoverlapping() {
     unsafe {
         let layout = Layout::from_size_align(16, 8).unwrap();
         let left: *mut u8 = alloc(layout);
         let right: *mut u8 = alloc(layout);
         // ~ERROR: Accessing `left` and `right` here, both of which are uninitialized.
-        typed_swap(left, right);
+        typed_swap_nonoverlapping(left, right);
     }
 }
 
 #[kani::proof]
-fn check_typed_swap_safe() {
+fn check_typed_swap_nonoverlapping_safe() {
     unsafe {
         let layout = Layout::from_size_align(16, 8).unwrap();
         let left: *mut u8 = alloc_zeroed(layout);
         let right: *mut u8 = alloc_zeroed(layout);
         // Both `left` and `right` are initialized here.
-        typed_swap(left, right);
+        typed_swap_nonoverlapping(left, right);
     }
 }

tests/kani/Intrinsics/typed_swap.rs renamed to tests/kani/Intrinsics/typed_swap_nonoverlapping.rs

@@ -1,20 +1,20 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-// Check that `typed_swap` yields the expected results.
-// https://doc.rust-lang.org/nightly/std/intrinsics/fn.typed_swap.html
+// Check that `typed_swap_nonoverlapping` yields the expected results.
+// https://doc.rust-lang.org/nightly/std/intrinsics/fn.typed_swap_nonoverlapping.html
 
 #![feature(core_intrinsics)]
 #![allow(internal_features)]
 
 #[kani::proof]
-fn test_typed_swap_u32() {
+fn test_typed_swap_nonoverlapping_u32() {
     let mut a: u32 = kani::any();
     let a_before = a;
     let mut b: u32 = kani::any();
     let b_before = b;
     unsafe {
-        std::intrinsics::typed_swap(&mut a, &mut b);
+        std::intrinsics::typed_swap_nonoverlapping(&mut a, &mut b);
     }
     assert!(b == a_before);
     assert!(a == b_before);