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.