From c25e44531500488508de217ac9df2c96f51e81f9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios Date: Mon, 16 May 2022 20:45:02 +0000 Subject: [PATCH] Add new tests and split old ones --- .../copy-overflow/expected | 2 + .../copy-nonoverlapping/copy-overflow/main.rs | 18 ++++ .../copy-overlapping/expected | 1 + .../copy-overlapping/main.rs | 16 ++++ .../copy-unaligned-dst/expected | 2 + .../copy-unaligned-dst/main.rs | 16 ++++ .../copy-unaligned-src/expected | 2 + .../copy-unaligned-src/main.rs | 17 ++++ .../copy-unreadable-src/expected | 2 + .../copy-unreadable-src/main.rs | 16 ++++ .../copy-unwritable-dst/expected | 2 + .../copy-unwritable-dst/main.rs | 15 ++++ .../Intrinsics/Copy/copy_nonoverlapping.rs | 88 +++---------------- .../Copy/copy_nonoverlapping_append.rs | 45 ++++++++++ .../Copy/copy_nonoverlapping_swap.rs | 32 +++++++ 15 files changed, 197 insertions(+), 77 deletions(-) create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/expected create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-overflow/main.rs create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/expected create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-overlapping/main.rs create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/expected create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/main.rs create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/expected create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/main.rs create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/expected create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/expected create mode 100644 tests/expected/intrinsics/copy-nonoverlapping/copy-unwritable-dst/main.rs create mode 100644 tests/kani/Intrinsics/Copy/copy_nonoverlapping_append.rs create mode 100644 tests/kani/Intrinsics/Copy/copy_nonoverlapping_swap.rs 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..0fe63b4113d4 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-dst/expected @@ -0,0 +1,2 @@ +FAILURE\ +`dst` is 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..bc711e19a80a --- /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` 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); + } +} 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..047a4db37da1 --- /dev/null +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unaligned-src/expected @@ -0,0 +1,2 @@ +FAILURE\ +`src` is 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/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); + } +}