From e6f8a62d689d0b0ebcbabe3661be6273c5ab9be8 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Thu, 15 Aug 2024 10:31:09 -0700 Subject: [PATCH] Implement memory initialization state copy functionality (#3350) This PR adds support of copying memory initialization state without checks in-between. Every time a copy is performed, the tracked byte is non-deterministically switched. Resolves #3347 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .../kani_middle/transform/check_uninit/mod.rs | 35 ++++++++++++++++ .../check_uninit/ptr_uninit/uninit_visitor.rs | 42 +++++++------------ .../check_uninit/relevant_instruction.rs | 31 ++++++++++++-- library/kani/src/mem_init.rs | 40 ++++++++++++++++++ .../uninit/copy/copy_without_padding.expected | 1 + .../uninit/copy/copy_without_padding.rs | 23 ++++++++++ .../copy/expose_padding_via_copy.expected | 11 +++++ .../uninit/copy/expose_padding_via_copy.rs | 23 ++++++++++ ...xpose_padding_via_copy_convoluted.expected | 11 +++++ .../expose_padding_via_copy_convoluted.rs | 42 +++++++++++++++++++ .../expose_padding_via_non_byte_copy.expected | 11 +++++ .../copy/expose_padding_via_non_byte_copy.rs | 23 ++++++++++ .../non_byte_copy_without_padding.expected | 1 + .../copy/non_byte_copy_without_padding.rs | 23 ++++++++++ .../uninit/copy/read_after_copy.expected | 11 +++++ tests/expected/uninit/copy/read_after_copy.rs | 23 ++++++++++ .../expected/uninit/delayed-ub/delayed-ub.rs | 31 ++++++++++++++ tests/expected/uninit/delayed-ub/expected | 12 +++++- tests/expected/uninit/intrinsics/expected | 12 +++--- .../expected/uninit/intrinsics/intrinsics.rs | 30 ++++++++++++- 20 files changed, 397 insertions(+), 39 deletions(-) create mode 100644 tests/expected/uninit/copy/copy_without_padding.expected create mode 100644 tests/expected/uninit/copy/copy_without_padding.rs create mode 100644 tests/expected/uninit/copy/expose_padding_via_copy.expected create mode 100644 tests/expected/uninit/copy/expose_padding_via_copy.rs create mode 100644 tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected create mode 100644 tests/expected/uninit/copy/expose_padding_via_copy_convoluted.rs create mode 100644 tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected create mode 100644 tests/expected/uninit/copy/expose_padding_via_non_byte_copy.rs create mode 100644 tests/expected/uninit/copy/non_byte_copy_without_padding.expected create mode 100644 tests/expected/uninit/copy/non_byte_copy_without_padding.rs create mode 100644 tests/expected/uninit/copy/read_after_copy.expected create mode 100644 tests/expected/uninit/copy/read_after_copy.rs diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 5c7194f879d1..0a0d3c786ea9 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -178,6 +178,9 @@ impl<'a> UninitInstrumenter<'a> { | MemoryInitOp::SetRef { .. } => { self.build_set(tcx, body, source, operation, pointee_ty_info, skip_first) } + MemoryInitOp::Copy { .. } => { + self.build_copy(tcx, body, source, operation, pointee_ty_info, skip_first) + } MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { unreachable!() } @@ -397,6 +400,38 @@ impl<'a> UninitInstrumenter<'a> { }; } + /// Copy memory initialization state from one pointer to the other. + fn build_copy( + &mut self, + tcx: TyCtxt, + body: &mut MutableBody, + source: &mut SourceInstruction, + operation: MemoryInitOp, + pointee_info: PointeeInfo, + skip_first: &mut HashSet, + ) { + let ret_place = Place { + local: body.new_local(Ty::new_tuple(&[]), source.span(body.blocks()), Mutability::Not), + projection: vec![], + }; + let PointeeLayout::Sized { layout } = pointee_info.layout() else { unreachable!() }; + let copy_init_state_instance = resolve_mem_init_fn( + get_mem_init_fn_def(tcx, "KaniCopyInitState", &mut self.mem_init_fn_cache), + layout.len(), + *pointee_info.ty(), + ); + collect_skipped(&operation, body, skip_first); + let position = operation.position(); + let MemoryInitOp::Copy { from, to, count } = operation else { unreachable!() }; + body.insert_call( + ©_init_state_instance, + source, + position, + vec![from, to, count], + ret_place.clone(), + ); + } + fn inject_assert_false( &self, tcx: TyCtxt, diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index f682f93a261e..1afb151a09b5 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -88,18 +88,13 @@ impl MirVisitor for CheckUninitVisitor { match &stmt.kind { StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(copy)) => { self.super_statement(stmt, location); - // Source is a *const T and it must be initialized. - self.push_target(MemoryInitOp::CheckSliceChunk { - operand: copy.src.clone(), + // The copy is untyped, so we should copy memory initialization state from `src` + // to `dst`. + self.push_target(MemoryInitOp::Copy { + from: copy.src.clone(), + to: copy.dst.clone(), count: copy.count.clone(), }); - // Destination is a *mut T so it gets initialized. - self.push_target(MemoryInitOp::SetSliceChunk { - operand: copy.dst.clone(), - count: copy.count.clone(), - value: true, - position: InsertPosition::After, - }); } StatementKind::Assign(place, rvalue) => { // First check rvalue. @@ -219,29 +214,24 @@ impl MirVisitor for CheckUninitVisitor { }); } Intrinsic::Copy => { - self.push_target(MemoryInitOp::CheckSliceChunk { - operand: args[0].clone(), + // The copy is untyped, so we should copy memory + // initialization state from `src` to `dst`. + self.push_target(MemoryInitOp::Copy { + from: args[0].clone(), + to: args[1].clone(), count: args[2].clone(), }); - self.push_target(MemoryInitOp::SetSliceChunk { - operand: args[1].clone(), - count: args[2].clone(), - value: true, - position: InsertPosition::After, - }); } Intrinsic::VolatileCopyMemory | Intrinsic::VolatileCopyNonOverlappingMemory => { - self.push_target(MemoryInitOp::CheckSliceChunk { - operand: args[1].clone(), + // The copy is untyped, so we should copy initialization state + // from `src` to `dst`. Note that the `dst` comes before `src` + // in this case. + self.push_target(MemoryInitOp::Copy { + from: args[1].clone(), + to: args[0].clone(), count: args[2].clone(), }); - self.push_target(MemoryInitOp::SetSliceChunk { - operand: args[0].clone(), - count: args[2].clone(), - value: true, - position: InsertPosition::After, - }); } Intrinsic::TypedSwap => { self.push_target(MemoryInitOp::Check { diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs b/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs index 3bc5b534a23b..cc5a27e09925 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/relevant_instruction.rs @@ -5,7 +5,10 @@ //! character of instrumentation needed. use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction}; -use stable_mir::mir::{Mutability, Operand, Place, Rvalue}; +use stable_mir::{ + mir::{Mutability, Operand, Place, Rvalue}, + ty::RigidTy, +}; use strum_macros::AsRefStr; /// Memory initialization operations: set or get memory initialization state for a given pointer. @@ -33,6 +36,8 @@ pub enum MemoryInitOp { Unsupported { reason: String }, /// Operation that trivially accesses uninitialized memory, results in injecting `assert!(false)`. TriviallyUnsafe { reason: String }, + /// Operation that copies memory initialization state over to another operand. + Copy { from: Operand, to: Operand, count: Operand }, } impl MemoryInitOp { @@ -62,7 +67,22 @@ impl MemoryInitOp { }) } MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { - unreachable!() + unreachable!("operands do not exist for this operation") + } + MemoryInitOp::Copy { from, to, .. } => { + // It does not matter which operand to return for layout generation, since both of + // them have the same pointee type, so we assert that. + let from_kind = from.ty(body.locals()).unwrap().kind(); + let to_kind = to.ty(body.locals()).unwrap().kind(); + + let RigidTy::RawPtr(from_pointee_ty, _) = from_kind.rigid().unwrap().clone() else { + unreachable!() + }; + let RigidTy::RawPtr(to_pointee_ty, _) = to_kind.rigid().unwrap().clone() else { + unreachable!() + }; + assert!(from_pointee_ty == to_pointee_ty); + from.clone() } } } @@ -70,7 +90,8 @@ impl MemoryInitOp { pub fn expect_count(&self) -> Operand { match self { MemoryInitOp::CheckSliceChunk { count, .. } - | MemoryInitOp::SetSliceChunk { count, .. } => count.clone(), + | MemoryInitOp::SetSliceChunk { count, .. } + | MemoryInitOp::Copy { count, .. } => count.clone(), MemoryInitOp::Check { .. } | MemoryInitOp::Set { .. } | MemoryInitOp::CheckRef { .. } @@ -89,7 +110,8 @@ impl MemoryInitOp { | MemoryInitOp::CheckSliceChunk { .. } | MemoryInitOp::CheckRef { .. } | MemoryInitOp::Unsupported { .. } - | MemoryInitOp::TriviallyUnsafe { .. } => unreachable!(), + | MemoryInitOp::TriviallyUnsafe { .. } + | MemoryInitOp::Copy { .. } => unreachable!(), } } @@ -103,6 +125,7 @@ impl MemoryInitOp { | MemoryInitOp::CheckRef { .. } | MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => InsertPosition::Before, + MemoryInitOp::Copy { .. } => InsertPosition::After, } } } diff --git a/library/kani/src/mem_init.rs b/library/kani/src/mem_init.rs index 88847e9c4f3c..3755fc59a510 100644 --- a/library/kani/src/mem_init.rs +++ b/library/kani/src/mem_init.rs @@ -91,6 +91,33 @@ impl MemoryInitializationState { } } + /// Copy memory initialization state by non-deterministically switching the tracked object and + /// adjusting the tracked offset. + pub fn copy( + &mut self, + from_ptr: *const u8, + to_ptr: *const u8, + num_elts: usize, + ) { + let from_obj = crate::mem::pointer_object(from_ptr); + let from_offset = crate::mem::pointer_offset(from_ptr); + + let to_obj = crate::mem::pointer_object(to_ptr); + let to_offset = crate::mem::pointer_offset(to_ptr); + + if self.tracked_object_id == from_obj + && self.tracked_offset >= from_offset + && self.tracked_offset < from_offset + num_elts * LAYOUT_SIZE + { + let should_reset: bool = crate::any(); + if should_reset { + self.tracked_object_id = to_obj; + self.tracked_offset += to_offset - from_offset; + // Note that this preserves the value. + } + } + } + /// Return currently tracked memory initialization state if `ptr` points to the currently /// tracked object and the tracked offset lies within `LAYOUT_SIZE * num_elts` bytes of `ptr`. /// Return `true` otherwise. @@ -281,3 +308,16 @@ fn set_str_ptr_initialized( MEM_INIT_STATE.set_slice(ptr as *const u8, layout, num_elts, value); } } + +/// Copy initialization state of `size_of:: * num_elts` bytes from one pointer to the other. +#[rustc_diagnostic_item = "KaniCopyInitState"] +fn copy_init_state(from: *const T, to: *const T, num_elts: usize) { + if LAYOUT_SIZE == 0 { + return; + } + let (from_ptr, _) = from.to_raw_parts(); + let (to_ptr, _) = to.to_raw_parts(); + unsafe { + MEM_INIT_STATE.copy::(from_ptr as *const u8, to_ptr as *const u8, num_elts); + } +} diff --git a/tests/expected/uninit/copy/copy_without_padding.expected b/tests/expected/uninit/copy/copy_without_padding.expected new file mode 100644 index 000000000000..01a90d50b557 --- /dev/null +++ b/tests/expected/uninit/copy/copy_without_padding.expected @@ -0,0 +1 @@ +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/expected/uninit/copy/copy_without_padding.rs b/tests/expected/uninit/copy/copy_without_padding.rs new file mode 100644 index 000000000000..16df1dd5d2d0 --- /dev/null +++ b/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::()); + + // 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); +} diff --git a/tests/expected/uninit/copy/expose_padding_via_copy.expected b/tests/expected/uninit/copy/expose_padding_via_copy.expected new file mode 100644 index 000000000000..83d8badc8bf5 --- /dev/null +++ b/tests/expected/uninit/copy/expose_padding_via_copy.expected @@ -0,0 +1,11 @@ +std::ptr::read::.assertion.1\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\ + +std::ptr::read::.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. diff --git a/tests/expected/uninit/copy/expose_padding_via_copy.rs b/tests/expected/uninit/copy/expose_padding_via_copy.rs new file mode 100644 index 000000000000..8adb772037ca --- /dev/null +++ b/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::()); + + // This reads uninitialized bytes, which is UB. + let padding: u64 = std::ptr::read(to_ptr); +} diff --git a/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected b/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected new file mode 100644 index 000000000000..cbe7ec97cb7b --- /dev/null +++ b/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.expected @@ -0,0 +1,11 @@ +std::ptr::read::.assertion.1\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\ + +std::ptr::read::.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. diff --git a/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.rs b/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.rs new file mode 100644 index 000000000000..5feadace245d --- /dev/null +++ b/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.rs @@ -0,0 +1,42 @@ +// 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::()); + // 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::()); + // 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); + } +} diff --git a/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected b/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected new file mode 100644 index 000000000000..3fc86e45a46e --- /dev/null +++ b/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.expected @@ -0,0 +1,11 @@ +std::ptr::read::.assertion.1\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\ + +std::ptr::read::.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. diff --git a/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.rs b/tests/expected/uninit/copy/expose_padding_via_non_byte_copy.rs new file mode 100644 index 000000000000..685239b267b1 --- /dev/null +++ b/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); +} diff --git a/tests/expected/uninit/copy/non_byte_copy_without_padding.expected b/tests/expected/uninit/copy/non_byte_copy_without_padding.expected new file mode 100644 index 000000000000..01a90d50b557 --- /dev/null +++ b/tests/expected/uninit/copy/non_byte_copy_without_padding.expected @@ -0,0 +1 @@ +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/expected/uninit/copy/non_byte_copy_without_padding.rs b/tests/expected/uninit/copy/non_byte_copy_without_padding.rs new file mode 100644 index 000000000000..6f3b380cd81f --- /dev/null +++ b/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); +} diff --git a/tests/expected/uninit/copy/read_after_copy.expected b/tests/expected/uninit/copy/read_after_copy.expected new file mode 100644 index 000000000000..56a3460a1d7b --- /dev/null +++ b/tests/expected/uninit/copy/read_after_copy.expected @@ -0,0 +1,11 @@ +std::ptr::read::.assertion.1\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u64`"\ + +std::ptr::read::.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. diff --git a/tests/expected/uninit/copy/read_after_copy.rs b/tests/expected/uninit/copy/read_after_copy.rs new file mode 100644 index 000000000000..742b74099acc --- /dev/null +++ b/tests/expected/uninit/copy/read_after_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 uninitialized bytes fails an assertion even after copy. +#[kani::proof] +unsafe fn read_after_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::()); + + // Reading padding from the previous place should be UB even after copy. + let data: u64 = std::ptr::read(from_ptr as *const u64); +} diff --git a/tests/expected/uninit/delayed-ub/delayed-ub.rs b/tests/expected/uninit/delayed-ub/delayed-ub.rs index feee4bcd161f..d7f258c27ba5 100644 --- a/tests/expected/uninit/delayed-ub/delayed-ub.rs +++ b/tests/expected/uninit/delayed-ub/delayed-ub.rs @@ -124,6 +124,24 @@ fn delayed_ub_copy() { } } +/// Delayed UB via multiple mutable pointers write using `copy_nonoverlapping` and `copy` under the +/// hood. +#[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, ptr_2, 1); // This should not trigger UB since the copy is untyped. + assert!(value_2 > 0); // UB: This reads a padding value! + } +} + struct S { u: U, } @@ -164,3 +182,16 @@ fn delayed_ub_slices() { let arr_copy = arr; // UB: This reads a padding value inside the array! } } + +/// Delayed UB via mutable pointer copy, which should be the only delayed UB trigger in this case. +#[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::()); // This is a delayed UB source. + assert!(value > 0); // UB: This reads a padding value! + } +} diff --git a/tests/expected/uninit/delayed-ub/expected b/tests/expected/uninit/delayed-ub/expected index 46b6ababe85d..dc0411bdba9c 100644 --- a/tests/expected/uninit/delayed-ub/expected +++ b/tests/expected/uninit/delayed-ub/expected @@ -1,3 +1,7 @@ +delayed_ub_trigger_copy.assertion.1\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\ + delayed_ub_slices.assertion.4\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `[u128; 4]`" @@ -6,6 +10,10 @@ delayed_ub_structs.assertion.2\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `U`" +delayed_ub_double_copy.assertion.1\ + - Status: FAILURE\ + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"\ + delayed_ub_copy.assertion.1\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" @@ -35,8 +43,10 @@ delayed_ub.assertion.2\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`" Summary: +Verification failed for - delayed_ub_trigger_copy Verification failed for - delayed_ub_slices Verification failed for - delayed_ub_structs +Verification failed for - delayed_ub_double_copy Verification failed for - delayed_ub_copy Verification failed for - delayed_ub_closure_capture_laundered Verification failed for - delayed_ub_closure_laundered @@ -44,4 +54,4 @@ Verification failed for - delayed_ub_laundered Verification failed for - delayed_ub_static Verification failed for - delayed_ub_transmute Verification failed for - delayed_ub -Complete - 0 successfully verified harnesses, 9 failures, 9 total. +Complete - 0 successfully verified harnesses, 11 failures, 11 total. diff --git a/tests/expected/uninit/intrinsics/expected b/tests/expected/uninit/intrinsics/expected index cf34d305608b..e428aa605887 100644 --- a/tests/expected/uninit/intrinsics/expected +++ b/tests/expected/uninit/intrinsics/expected @@ -34,19 +34,19 @@ check_compare_bytes.assertion.2\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`" -std::intrinsics::copy::.assertion.1\ +std::ptr::read::.assertion.1\ - Status: FAILURE\ - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`" -std::intrinsics::copy_nonoverlapping::.assertion.1\ +std::ptr::read::.assertion.2\ - Status: FAILURE\ - - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `*const u8`" + - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u8`" Summary: Verification failed for - check_typed_swap_safe Verification failed for - check_typed_swap Verification failed for - check_volatile_load Verification failed for - check_compare_bytes -Verification failed for - check_copy -Verification failed for - check_copy_nonoverlapping -Complete - 5 successfully verified harnesses, 6 failures, 11 total. +Verification failed for - check_copy_read +Verification failed for - check_copy_nonoverlapping_read +Complete - 7 successfully verified harnesses, 6 failures, 13 total. diff --git a/tests/expected/uninit/intrinsics/intrinsics.rs b/tests/expected/uninit/intrinsics/intrinsics.rs index aa8a89b7b959..b023853b2fbc 100644 --- a/tests/expected/uninit/intrinsics/intrinsics.rs +++ b/tests/expected/uninit/intrinsics/intrinsics.rs @@ -14,7 +14,20 @@ fn check_copy_nonoverlapping() { let layout = Layout::from_size_align(16, 8).unwrap(); let src: *mut u8 = alloc(layout); let dst: *mut u8 = alloc(layout); - copy_nonoverlapping(src as *const u8, dst, 2); // ~ERROR: Accessing `src` here, which is uninitialized. + // This does not fail, since `copy_nonoverlapping` is untyped. + copy_nonoverlapping(src as *const u8, dst, 2); + } +} + +#[kani::proof] +fn check_copy_nonoverlapping_read() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc(layout); + let dst: *mut u8 = alloc_zeroed(layout); + copy_nonoverlapping(src as *const u8, dst, 2); + // ~ERROR: Accessing `dst` here, which became uninitialized after copy. + let uninit = std::ptr::read(dst); } } @@ -35,7 +48,20 @@ fn check_copy() { let layout = Layout::from_size_align(16, 8).unwrap(); let src: *mut u8 = alloc(layout); let dst: *mut u8 = alloc(layout); - copy(src as *const u8, dst, 2); // ~ERROR: Accessing `src` here, which is uninitialized. + // This does not fail, since `copy` is untyped. + copy(src as *const u8, dst, 2); + } +} + +#[kani::proof] +fn check_copy_read() { + unsafe { + let layout = Layout::from_size_align(16, 8).unwrap(); + let src: *mut u8 = alloc(layout); + let dst: *mut u8 = alloc_zeroed(layout); + copy(src as *const u8, dst, 2); + // ~ERROR: Accessing `dst` here, which became uninitialized after copy. + let uninit = std::ptr::read(dst); } }