diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index ac8d805e2d80..bca3a9ad1b1a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -467,7 +467,7 @@ impl<'tcx> GotocCtx<'tcx> { "ceilf64" => codegen_unimplemented_intrinsic!( "https://github.com/model-checking/kani/issues/1025" ), - "copy" => self.codegen_copy_intrinsic(intrinsic, fargs, farg_types, p, loc), + "copy" => self.codegen_copy(intrinsic, false, fargs, farg_types, Some(p), loc), "copy_nonoverlapping" => unreachable!( "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`" ), @@ -897,21 +897,31 @@ impl<'tcx> GotocCtx<'tcx> { Stmt::atomic_block(vec![skip_stmt], loc) } - /// An intrinsic that translates directly into `memmove` - /// https://doc.rust-lang.org/core/intrinsics/fn.copy.html + /// Copies `count * size_of::()` bytes from `src` to `dst`. + /// + /// Note that this function handles code generation for: + /// 1. The `copy` intrinsic. + /// https://doc.rust-lang.org/core/intrinsics/fn.copy.html + /// 2. The `CopyNonOverlapping` statement. + /// https://doc.rust-lang.org/core/intrinsics/fn.copy_nonoverlapping.html /// /// Undefined behavior if any of these conditions are violated: /// * Both `src`/`dst` must be properly aligned (done by alignment checks) /// * Both `src`/`dst` must be valid for reads/writes of `count * /// size_of::()` bytes (done by calls to `memmove`) + /// * (Exclusive to nonoverlapping copy) The region of memory beginning + /// at `src` with a size of `count * size_of::()` bytes must *not* + /// overlap with the region of memory beginning at `dst` with the same + /// size. /// In addition, we check that computing `count` in bytes (i.e., the third - /// argument for the `memmove` call) would not overflow. - fn codegen_copy_intrinsic( + /// argument of the copy built-in call) would not overflow. + pub fn codegen_copy( &mut self, intrinsic: &str, + is_non_overlapping: bool, mut fargs: Vec, farg_types: &[Ty<'tcx>], - p: &Place<'tcx>, + p: Option<&Place<'tcx>>, loc: Location, ) -> Stmt { // The two first arguments are pointers. It's safe to cast them to void @@ -924,14 +934,14 @@ impl<'tcx> GotocCtx<'tcx> { let src_align_check = self.codegen_assert( src_align, PropertyClass::DefaultAssertion, - "`src` is properly aligned", + "`src` must be properly aligned", loc, ); let dst_align = self.is_ptr_aligned(farg_types[1], dst.clone()); let dst_align_check = self.codegen_assert( dst_align, PropertyClass::DefaultAssertion, - "`dst` is properly aligned", + "`dst` must be properly aligned", loc, ); @@ -941,18 +951,23 @@ impl<'tcx> GotocCtx<'tcx> { let (count_bytes, overflow_check) = self.count_in_bytes(count, pointee_type, Type::size_t(), intrinsic, loc); - // Build the call to `memmove` - let call_memmove = - BuiltinFn::Memmove.call(vec![dst.clone(), src, count_bytes.clone()], loc); + // Build the call to the copy built-in (`memmove` or `memcpy`) + let copy_builtin = if is_non_overlapping { BuiltinFn::Memcpy } else { BuiltinFn::Memmove }; + let copy_call = copy_builtin.call(vec![dst.clone(), src, count_bytes.clone()], loc); - // The C implementation of `memmove` does not allow an invalid pointer for - // `src` nor `dst`, but the LLVM implementation specifies that a copy with - // length zero is a no-op. This comes up specifically when handling - // the empty string; CBMC will fail on passing a reference to empty - // string unless we codegen this zero check. + // The C implementations of `memmove` and `memcpy` do not allow an + // invalid pointer for `src` nor `dst`, but the LLVM implementations + // specify that a zero-length copy is a no-op: // https://llvm.org/docs/LangRef.html#llvm-memmove-intrinsic - let copy_if_nontrivial = count_bytes.is_zero().ternary(dst, call_memmove); - let copy_expr = self.codegen_expr_to_place(p, copy_if_nontrivial); + // https://llvm.org/docs/LangRef.html#llvm-memcpy-intrinsic + // This comes up specifically when handling the empty string; CBMC will + // fail on passing a reference to it unless we codegen this zero check. + let copy_if_nontrivial = count_bytes.is_zero().ternary(dst, copy_call); + let copy_expr = if p.is_some() { + self.codegen_expr_to_place(p.unwrap(), copy_if_nontrivial) + } else { + copy_if_nontrivial.as_stmt(loc) + }; Stmt::block(vec![src_align_check, dst_align_check, overflow_check, copy_expr], loc) } @@ -1274,7 +1289,7 @@ impl<'tcx> GotocCtx<'tcx> { let align_check = self.codegen_assert( align, PropertyClass::DefaultAssertion, - "`dst` is properly aligned", + "`dst` must be properly aligned", loc, ); let expr = dst.dereference().assign(src, loc); @@ -1299,13 +1314,13 @@ impl<'tcx> GotocCtx<'tcx> { let val = fargs.remove(0).cast_to(Type::c_int()); let count = fargs.remove(0); - // Check that `dst` is properly aligned + // Check that `dst` must be properly aligned let dst_typ = farg_types[0]; let align = self.is_ptr_aligned(dst_typ, dst.clone()); let align_check = self.codegen_assert( align, PropertyClass::DefaultAssertion, - "`dst` is properly aligned", + "`dst` must be properly aligned", loc, ); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index f8b8ee4323f7..8a5ba1370d7a 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs @@ -731,22 +731,15 @@ impl<'tcx> GotocCtx<'tcx> { ref dst, ref count, }) => { - let src = self.codegen_operand(src).cast_to(Type::void_pointer()); - let dst = self.codegen_operand(dst); - let count = self.codegen_operand(count); - let sz = dst.typ().base_type().unwrap().sizeof(&self.symbol_table); - let sz = Expr::int_constant(sz, Type::size_t()); - let n = sz.mul(count); - let dst = dst.cast_to(Type::void_pointer()); - let e = BuiltinFn::Memcpy.call(vec![dst, src, n.clone()], location.clone()); - - // The C implementation of memcpy does not allow an invalid pointer for - // the src/dst, but the LLVM implementation specifies that a copy with - // length zero is a no-op. This comes up specifically when handling - // the empty string; CBMC will fail on passing a reference to empty - // string unless we codegen this zero check. - // https://llvm.org/docs/LangRef.html#llvm-memcpy-intrinsic - Stmt::if_then_else(n.is_zero().not(), e.as_stmt(location.clone()), None, location) + // Pack the operands and their types, then call `codegen_copy` + let fargs = vec![ + self.codegen_operand(src), + self.codegen_operand(dst), + self.codegen_operand(count), + ]; + let farg_types = + &[self.operand_ty(src), self.operand_ty(dst), self.operand_ty(count)]; + self.codegen_copy("copy_nonoverlapping", true, fargs, farg_types, None, location) } StatementKind::FakeRead(_) | StatementKind::Retag(_, _) diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/expected b/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/expected new file mode 100644 index 000000000000..ac218a7a2596 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/expected @@ -0,0 +1,2 @@ +FAILURE\ +copy_nonoverlapping: attempt to compute number in bytes which would overflow \ No newline at end of file diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs new file mode 100644 index 000000000000..c1c655f3f1ed --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `copy_nonoverlapping` triggers an overflow failure if the `count` +// argument can overflow a `usize` +#[kani::proof] +fn test_copy_nonoverlapping_unaligned() { + let arr: [i32; 3] = [0, 1, 0]; + let src: *const i32 = arr.as_ptr(); + // Passing `max_count` is guaranteed to overflow + // the count in bytes for `i32` pointers + let max_count = usize::MAX / 4 + 1; + + unsafe { + let dst = src.add(1) as *mut i32; + core::intrinsics::copy_nonoverlapping(src, dst, max_count); + } +} diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/expected b/tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/expected new file mode 100644 index 000000000000..9ebadf73b291 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/expected @@ -0,0 +1 @@ +memcpy src/dst overlap \ No newline at end of file diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/main.rs new file mode 100644 index 000000000000..bcfa5dae79a4 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/main.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that `copy_nonoverlapping` fails if the `src`/`dst` regions overlap. +#[kani::proof] +fn test_copy_nonoverlapping_with_overlap() { + let arr: [i32; 3] = [0, 1, 0]; + let src: *const i32 = arr.as_ptr(); + + unsafe { + // The call to `copy_nonoverlapping` is expected to fail because + // the `src` region and the `dst` region overlap in `arr[1]` + let dst = src.add(1) as *mut i32; + core::intrinsics::copy_nonoverlapping(src, dst, 2); + } +} diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/expected b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/expected new file mode 100644 index 000000000000..1c1e00c0cb0a --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/expected @@ -0,0 +1,2 @@ +FAILURE\ +`dst` must be properly aligned \ No newline at end of file diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs new file mode 100644 index 000000000000..82c33d60c0c0 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `copy_nonoverlapping` fails when `dst` is not aligned. +#[kani::proof] +fn test_copy_nonoverlapping_unaligned() { + let arr: [i32; 3] = [0, 1, 0]; + let src: *const i32 = arr.as_ptr(); + + unsafe { + // Get an unaligned pointer with a single-byte offset + let dst_i8: *const i8 = src.add(1) as *mut i8; + let dst_unaligned = unsafe { dst_i8.add(1) as *mut i32 }; + core::intrinsics::copy_nonoverlapping(src, dst_unaligned, 1); + } +} diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/expected b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/expected new file mode 100644 index 000000000000..485accebd53c --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/expected @@ -0,0 +1,2 @@ +FAILURE\ +`src` must be properly aligned \ No newline at end of file diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/main.rs new file mode 100644 index 000000000000..ad93c761df81 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/main.rs @@ -0,0 +1,17 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `copy_nonoverlapping` fails when `src` is not aligned. +#[kani::proof] +fn test_copy_nonoverlapping_unaligned() { + let arr: [i32; 3] = [0, 1, 0]; + let src: *const i32 = arr.as_ptr(); + + unsafe { + // Get an unaligned pointer with a single-byte offset + let src_i8: *const i8 = src as *const i8; + let src_unaligned = unsafe { src_i8.add(1) as *const i32 }; + let dst = src.add(1) as *mut i32; + core::intrinsics::copy_nonoverlapping(src_unaligned, dst, 1); + } +} diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/expected b/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/expected new file mode 100644 index 000000000000..3fe1563c21c2 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/expected @@ -0,0 +1,2 @@ +FAILURE\ +memcpy source region readable \ No newline at end of file diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs new file mode 100644 index 000000000000..ff2d54e7ca6b --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `copy_nonoverlapping` fails when `src` is not valid for reads. +#[kani::proof] +fn test_copy_nonoverlapping_invalid() { + let arr: [i32; 3] = [0, 1, 0]; + let src: *const i32 = arr.as_ptr(); + + unsafe { + // Get an invalid pointer with a negative offset + let src_invalid = unsafe { src.sub(1) as *const i32 }; + let dst = src.add(1) as *mut i32; + core::intrinsics::copy_nonoverlapping(src_invalid, dst, 1); + } +} diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/expected b/tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/expected new file mode 100644 index 000000000000..78e53fb3a882 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/expected @@ -0,0 +1,2 @@ +FAILURE\ +memcpy destination region writeable \ No newline at end of file diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/main.rs new file mode 100644 index 000000000000..34c7832267e0 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/main.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `copy_nonoverlapping` fails when `dst` is not valid for writes. +#[kani::proof] +fn test_copy_nonoverlapping_invalid() { + let arr: [i32; 3] = [0, 1, 0]; + let src: *const i32 = arr.as_ptr(); + + unsafe { + // Get an invalid pointer with an out-of-bounds offset + let dst_invalid = src.add(3) as *mut i32; + core::intrinsics::copy_nonoverlapping(src, dst_invalid, 1); + } +} diff --git a/tests/expected/intrinsics/copy/copy-unaligned-dst/expected b/tests/expected/intrinsics/copy/copy-unaligned-dst/expected index 0fe63b4113d4..1c1e00c0cb0a 100644 --- a/tests/expected/intrinsics/copy/copy-unaligned-dst/expected +++ b/tests/expected/intrinsics/copy/copy-unaligned-dst/expected @@ -1,2 +1,2 @@ FAILURE\ -`dst` is properly aligned \ No newline at end of file +`dst` must be properly aligned \ No newline at end of file diff --git a/tests/expected/intrinsics/copy/copy-unaligned-src/expected b/tests/expected/intrinsics/copy/copy-unaligned-src/expected index 047a4db37da1..485accebd53c 100644 --- a/tests/expected/intrinsics/copy/copy-unaligned-src/expected +++ b/tests/expected/intrinsics/copy/copy-unaligned-src/expected @@ -1,2 +1,2 @@ FAILURE\ -`src` is properly aligned \ No newline at end of file +`src` must be properly aligned \ No newline at end of file diff --git a/tests/expected/intrinsics/write_bytes/unaligned/expected b/tests/expected/intrinsics/write_bytes/unaligned/expected index 0fe63b4113d4..1c1e00c0cb0a 100644 --- a/tests/expected/intrinsics/write_bytes/unaligned/expected +++ b/tests/expected/intrinsics/write_bytes/unaligned/expected @@ -1,2 +1,2 @@ FAILURE\ -`dst` is properly aligned \ No newline at end of file +`dst` must be properly aligned \ No newline at end of file diff --git a/tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs b/tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs index c0633fce4d0e..bec748bfa7a3 100644 --- a/tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs +++ b/tests/kani/Intrinsics/Copy/copy_nonoverlapping.rs @@ -1,84 +1,18 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -#![feature(core_intrinsics)] -/// kani main.rs -- --default-unwind 20 --unwinding-assertions -use std::mem; -use std::ptr; -// Note: Calls to `copy_nonoverlapping` are handled by `codegen_statement` -// and not `codegen_intrinsic`: https://github.com/model-checking/kani/issues/1198 +// Check that `copy_nonoverlapping` works as expected: Copies a number `n` of elements from +// pointer `src` to pointer `dst`. Their regions of memory do not overlap, otherwise the +// call to `copy_nonoverlapping` would fail (a separate test checks for this). -/// https://doc.rust-lang.org/std/ptr/fn.copy_nonoverlapping.html -/// Moves all the elements of `src` into `dst`, leaving `src` empty. -fn append(dst: &mut Vec, src: &mut Vec) { - let src_len = src.len(); - let dst_len = dst.len(); - - // Ensure that `dst` has enough capacity to hold all of `src`. - dst.reserve(src_len); - - unsafe { - // The call to offset is always safe because `Vec` will never - // allocate more than `isize::MAX` bytes. - let dst_ptr = dst.as_mut_ptr().offset(dst_len as isize); - let src_ptr = src.as_ptr(); - - // Truncate `src` without dropping its contents. We do this first, - // to avoid problems in case something further down panics. - src.set_len(0); - - // The two regions cannot overlap because mutable references do - // not alias, and two different vectors cannot own the same - // memory. - ptr::copy_nonoverlapping(src_ptr, dst_ptr, src_len); - - // Notify `dst` that it now holds the contents of `src`. - dst.set_len(dst_len + src_len); - } -} - -fn test_append() { - let mut a = vec!['r']; - let mut b = vec!['u', 's', 't']; - - append(&mut a, &mut b); - - assert!(a == &['r', 'u', 's', 't']); - assert!(b.is_empty()); -} - -/// Test the swap example from https://doc.redox-os.org/std/std/intrinsics/fn.copy_nonoverlapping.html -/// Using T as uninitialized as in the example gives other errors, which we will solve later. -/// For this test, passing in a default value that gets overridden is sufficient. -fn swap_with_default(x: &mut T, y: &mut T, default: T) { +#[kani::proof] +fn test_copy_nonoverlapping_simple() { + let mut expected_val = 42; + let src: *mut i32 = &mut expected_val as *mut i32; + let mut old_val = 99; + let dst: *mut i32 = &mut old_val; unsafe { - // Give ourselves some scratch space to work with - // let mut t: T = mem::uninitialized(); - let mut t: T = default; - - // Perform the swap, `&mut` pointers never alias - ptr::copy_nonoverlapping(x, &mut t, 1); - ptr::copy_nonoverlapping(y, x, 1); - ptr::copy_nonoverlapping(&t, y, 1); - - // y and t now point to the same thing, but we need to completely forget `tmp` - // because it's no longer relevant. - mem::forget(t); + core::intrinsics::copy_nonoverlapping(src, dst, 1); + assert!(*dst == expected_val); } } - -/// another test for copy_nonoverlapping, from -/// https://doc.redox-os.org/std/std/intrinsics/fn.copy_nonoverlapping.html -fn test_swap() { - let mut x = 12; - let mut y = 13; - swap_with_default(&mut x, &mut y, 3); - assert!(x == 13); - assert!(y == 12); -} - -#[kani::proof] -fn main() { - test_swap(); - test_append(); -} diff --git a/tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs b/tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs new file mode 100644 index 000000000000..a9c0d3a5eb9a --- /dev/null +++ b/tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs @@ -0,0 +1,45 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test the append example from +// https://doc.rust-lang.org/core/intrinsics/fn.copy_nonoverlapping.html +use std::ptr; + +#[kani::proof] +fn test_append() { + let mut a = vec!['r']; + let mut b = vec!['u', 's', 't']; + + append(&mut a, &mut b); + + assert!(a == &['r', 'u', 's', 't']); + assert!(b.is_empty()); +} + +/// Moves all the elements of `src` into `dst`, leaving `src` empty. +fn append(dst: &mut Vec, src: &mut Vec) { + let src_len = src.len(); + let dst_len = dst.len(); + + // Ensure that `dst` has enough capacity to hold all of `src`. + dst.reserve(src_len); + + unsafe { + // The call to offset is always safe because `Vec` will never + // allocate more than `isize::MAX` bytes. + let dst_ptr = dst.as_mut_ptr().offset(dst_len as isize); + let src_ptr = src.as_ptr(); + + // Truncate `src` without dropping its contents. We do this first, + // to avoid problems in case something further down panics. + src.set_len(0); + + // The two regions cannot overlap because mutable references do + // not alias, and two different vectors cannot own the same + // memory. + ptr::copy_nonoverlapping(src_ptr, dst_ptr, src_len); + + // Notify `dst` that it now holds the contents of `src`. + dst.set_len(dst_len + src_len); + } +} diff --git a/tests/kani/Intrinsics/Copy/copy_nonoverlapping_swap.rs b/tests/kani/Intrinsics/Copy/copy_nonoverlapping_swap.rs new file mode 100644 index 000000000000..6e36d4c297ff --- /dev/null +++ b/tests/kani/Intrinsics/Copy/copy_nonoverlapping_swap.rs @@ -0,0 +1,32 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Test the swap example from +// https://doc.redox-os.org/std/std/intrinsics/fn.copy_nonoverlapping.html +use std::mem; +use std::ptr; + +#[kani::proof] +fn test_swap() { + let mut x = 12; + let mut y = 13; + swap(&mut x, &mut y); + assert!(x == 13); + assert!(y == 12); +} + +fn swap(x: &mut T, y: &mut T) { + unsafe { + // Give ourselves some scratch space to work with + let mut t: T = mem::uninitialized(); + + // Perform the swap, `&mut` pointers never alias + ptr::copy_nonoverlapping(x, &mut t, 1); + ptr::copy_nonoverlapping(y, x, 1); + ptr::copy_nonoverlapping(&t, y, 1); + + // y and t now point to the same thing, but we need to completely forget `tmp` + // because it's no longer relevant. + mem::forget(t); + } +}