Add extra tests for copy + delayed ub, split copy tests into multiple

copy_test.rs

@@ -0,0 +1,65 @@
+#[repr(C)]
+#[derive(kani::Arbitrary)]
+struct S(u32, u8); // 5 bytes of data + 3 bytes of padding.
+
+// #[kani::proof]
+// fn delayed_ub_double_copy() {
+// unsafe {
+// let mut value: u128 = 0;
+// let ptr = &mut value as *mut _ as *mut (u8, u32, u64);
+// // Use `copy_nonoverlapping` in an attempt to remove the taint.
+// std::ptr::write(ptr, (4, 4, 4));
+// // Instead of assigning the value into a delayed UB place, copy it from another delayed UB
+// // place.
+// let mut value_2: u128 = 0; 
+// let ptr_2 = &mut value_2 as *mut _ as *mut (u8, u32, u64);
+// std::ptr::copy(ptr_2, ptr, 1); // This should not trigger UB since the copy is untyped.
+// assert!(value_2 > 0); // UB: This reads a padding value!
+// }
+// }
+
+// #[kani::proof]
+// fn delayed_ub_trigger_copy() {
+// unsafe {
+// let mut value: u128 = 0;
+// let ptr = &mut value as *mut _ as *mut u8; // This cast should not be a delayed UB source.
+// let mut value_different_padding: (u8, u32, u64) = (4, 4, 4);
+// let ptr_different_padding = &mut value_different_padding as *mut _ as *mut u8;
+// std::ptr::copy(ptr_different_padding, ptr, std::mem::size_of::<u128>()); // This is a delayed UB source.
+// assert!(value > 0); // UB: This reads a padding value!
+// }
+// }
+
+#[kani::proof]
+/// This checks that reading copied uninitialized bytes fails an assertion.
+unsafe fn expose_padding_via_copy_convoluted() {
+ unsafe fn copy_and_read_helper(from_ptr: *const S, to_ptr: *mut u64) -> u64 {
+ // This should not cause UB since `copy` is untyped.
+ std::ptr::copy(from_ptr as *const u8, to_ptr as *mut u8, std::mem::size_of::<S>());
+ // This reads uninitialized bytes, which is UB.
+ let padding: u64 = std::ptr::read(to_ptr);
+ padding
+ }
+
+ unsafe fn partial_copy_and_read_helper(from_ptr: *const S, to_ptr: *mut u64) -> u32 {
+ // This should not cause UB since `copy` is untyped.
+ std::ptr::copy(from_ptr as *const u8, to_ptr as *mut u8, std::mem::size_of::<u32>());
+ // This does not read uninitialized bytes.
+ let not_padding: u32 = std::ptr::read(to_ptr as *mut u32);
+ not_padding
+ }
+
+ let flag: bool = kani::any();
+
+ let from: S = kani::any();
+ let mut to: u64 = kani::any();
+
+ let from_ptr = &from as *const S;
+ let to_ptr = &mut to as *mut u64;
+
+ if flag {
+ copy_and_read_helper(from_ptr, to_ptr);
+ } else {
+ partial_copy_and_read_helper(from_ptr, to_ptr);
+ }
+}

tests/expected/uninit/copy/copy_without_padding.expected

@@ -0,0 +1 @@
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

tests/expected/uninit/copy/copy_without_padding.rs

@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z uninit-checks
+
+#[repr(C)]
+#[derive(kani::Arbitrary)]
+struct S(u32, u8); // 5 bytes of data + 3 bytes of padding.
+
+#[kani::proof]
+/// This checks that reading copied initialized bytes verifies correctly.
+unsafe fn copy_without_padding() {
+ let from: S = kani::any();
+ let mut to: u64 = kani::any();
+
+ let from_ptr = &from as *const S;
+ let to_ptr = &mut to as *mut u64;
+
+ // This should not cause UB since `copy` is untyped.
+ std::ptr::copy(from_ptr as *const u8, to_ptr as *mut u8, std::mem::size_of::<u32>());
+
+ // Since the previous copy only copied 4 bytes, no padding was copied, so no padding is read.
+ let data: u64 = std::ptr::read(to_ptr);
+}

tests/expected/uninit/copy/expose_padding_via_copy.expected

@@ -0,0 +1,11 @@
+std::ptr::read::<u64>.assertion.1\
+ - Status: FAILURE\
+ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\
+
+std::ptr::read::<u64>.assertion.2\
+ - Status: FAILURE\
+ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\
+
+Summary:
+Verification failed for - expose_padding_via_copy
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/expected/uninit/copy/expose_padding_via_copy.rs

@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z uninit-checks
+
+#[repr(C)]
+#[derive(kani::Arbitrary)]
+struct S(u32, u8); // 5 bytes of data + 3 bytes of padding.
+
+/// This checks that reading copied uninitialized bytes fails an assertion.
+#[kani::proof]
+unsafe fn expose_padding_via_copy() {
+ let from: S = kani::any();
+ let mut to: u64 = kani::any();
+
+ let from_ptr = &from as *const S;
+ let to_ptr = &mut to as *mut u64;
+
+ // This should not cause UB since `copy` is untyped.
+ std::ptr::copy(from_ptr as *const u8, to_ptr as *mut u8, std::mem::size_of::<S>());
+
+ // This reads uninitialized bytes, which is UB.
+ let padding: u64 = std::ptr::read(to_ptr);
+}

tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected

@@ -0,0 +1,11 @@
+std::ptr::read::<u64>.assertion.1\
+ - Status: FAILURE\
+ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\
+
+std::ptr::read::<u64>.assertion.2\
+ - Status: FAILURE\
+ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\
+
+Summary:
+Verification failed for - expose_padding_via_copy_convoluted
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/expected/uninit/copy/expose_padding_via_copy_convoluted.rs

@@ -0,0 +1,43 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z uninit-checks
+
+#[repr(C)]
+#[derive(kani::Arbitrary)]
+struct S(u32, u8); // 5 bytes of data + 3 bytes of padding.
+
+
+/// This checks that reading copied uninitialized bytes fails an assertion even if pointer are
+/// passed around different functions.
+#[kani::proof]
+unsafe fn expose_padding_via_copy_convoluted() {
+ unsafe fn copy_and_read_helper(from_ptr: *const S, to_ptr: *mut u64) -> u64 {
+ // This should not cause UB since `copy` is untyped.
+ std::ptr::copy(from_ptr as *const u8, to_ptr as *mut u8, std::mem::size_of::<S>());
+ // This reads uninitialized bytes, which is UB.
+ let padding: u64 = std::ptr::read(to_ptr);
+ padding
+ }
+
+ unsafe fn partial_copy_and_read_helper(from_ptr: *const S, to_ptr: *mut u64) -> u32 {
+ // This should not cause UB since `copy` is untyped.
+ std::ptr::copy(from_ptr as *const u8, to_ptr as *mut u8, std::mem::size_of::<u32>());
+ // This does not read uninitialized bytes.
+ let not_padding: u32 = std::ptr::read(to_ptr as *mut u32);
+ not_padding
+ }
+
+ let flag: bool = kani::any();
+
+ let from: S = kani::any();
+ let mut to: u64 = kani::any();
+
+ let from_ptr = &from as *const S;
+ let to_ptr = &mut to as *mut u64;
+
+ if flag {
+ copy_and_read_helper(from_ptr, to_ptr);
+ } else {
+ partial_copy_and_read_helper(from_ptr, to_ptr);
+ }
+}

tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected

@@ -0,0 +1,11 @@
+std::ptr::read::<u64>.assertion.1\
+ - Status: FAILURE\
+ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\
+
+std::ptr::read::<u64>.assertion.2\
+ - Status: FAILURE\
+ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\
+
+Summary:
+Verification failed for - expose_padding_via_non_byte_copy
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.

tests/expected/uninit/copy/expose_padding_via_non_byte_copy.rs

@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z uninit-checks
+
+#[repr(C)]
+#[derive(kani::Arbitrary)]
+struct S(u32, u8); // 5 bytes of data + 3 bytes of padding.
+
+/// This checks that reading copied uninitialized bytes after a multi-byte copy fails an assertion.
+#[kani::proof]
+unsafe fn expose_padding_via_non_byte_copy() {
+ let from: S = kani::any();
+ let mut to: u64 = kani::any();
+
+ let from_ptr = &from as *const S;
+ let to_ptr = &mut to as *mut u64;
+
+ // This should not cause UB since `copy` is untyped.
+ std::ptr::copy(from_ptr as *const u64, to_ptr as *mut u64, 1);
+
+ // This reads uninitialized bytes, which is UB.
+ let padding: u64 = std::ptr::read(to_ptr);
+}

tests/expected/uninit/copy/non_byte_copy_without_padding.expected

@@ -0,0 +1 @@
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

tests/expected/uninit/copy/non_byte_copy_without_padding.rs

@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z uninit-checks
+
+#[repr(C)]
+#[derive(kani::Arbitrary)]
+struct S(u32, u8); // 5 bytes of data + 3 bytes of padding.
+
+#[kani::proof]
+/// This checks that reading copied initialized bytes after a multi-byte copy verifies correctly.
+unsafe fn non_byte_copy_without_padding() {
+ let from: S = kani::any();
+ let mut to: u64 = kani::any();
+
+ let from_ptr = &from as *const S;
+ let to_ptr = &mut to as *mut u64;
+
+ // This should not cause UB since `copy` is untyped.
+ std::ptr::copy(from_ptr as *const u32, to_ptr as *mut u32, 1);
+
+ // Since the previous copy only copied 4 bytes, no padding was copied, so no padding is read.
+ let data: u64 = std::ptr::read(to_ptr);
+}

tests/expected/uninit/copy/read_after_copy.expected

@@ -0,0 +1,11 @@
+std::ptr::read::<u64>.assertion.1\
+ - Status: FAILURE\
+ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\
+
+std::ptr::read::<u64>.assertion.2\
+ - Status: FAILURE\
+ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"\
+
+Summary:
+Verification failed for - read_after_copy
+Complete - 0 successfully verified harnesses, 1 failures, 1 total.