Add new tests and split old ones

tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/expected

@@ -0,0 +1,2 @@
+FAILURE\
+copy_nonoverlapping: attempt to compute number in bytes which would overflow

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);
+    }
+}

tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/expected

@@ -0,0 +1 @@
+memcpy src/dst overlap

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);
+    }
+}

tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/expected

@@ -0,0 +1,2 @@
+FAILURE\
+`dst` is properly aligned

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` fails when `dst` is not aligned.
+#[kani::proof]
+fn test_copy_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(src, dst_unaligned, 1);
+    }
+}

tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/expected

@@ -0,0 +1,2 @@
+FAILURE\
+`src` is properly aligned

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);
+    }
+}

tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/expected

@@ -0,0 +1,2 @@
+FAILURE\
+memcpy source region readable

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);
+    }
+}

tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/expected

@@ -0,0 +1,2 @@
+FAILURE\
+memcpy destination region writeable

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);
+    }
+}

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<T>(dst: &mut Vec<T>, src: &mut Vec<T>) {
-    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<T>(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();
-}

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<T>(dst: &mut Vec<T>, src: &mut Vec<T>) {
+    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);
+    }
+}

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<T>(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);
+    }
+}