From 11400b6339a5e5729194e5404ac0b6af9860b049 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 17 Jul 2024 09:35:26 -0700 Subject: [PATCH 1/9] Tentative implementation of memory initialization copy --- .../kani_middle/transform/check_uninit/mod.rs | 35 +++++++++ .../transform/check_uninit/uninit_visitor.rs | 74 +++++++++++++------ library/kani/src/mem_init.rs | 40 ++++++++++ 3 files changed, 127 insertions(+), 22 deletions(-) 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 4f94f94d17f1..56840bb988d7 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -183,6 +183,9 @@ impl UninitPass { | 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!() } @@ -394,6 +397,38 @@ impl UninitPass { }; } + /// 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.add_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/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs index 4c768aa2ee81..96790f594a82 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/uninit_visitor.rs @@ -39,6 +39,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 { @@ -66,7 +68,22 @@ impl MemoryInitOp { projection: vec![], }), 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() } } } @@ -74,7 +91,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::SetRef { .. } @@ -91,7 +109,8 @@ impl MemoryInitOp { MemoryInitOp::Check { .. } | MemoryInitOp::CheckSliceChunk { .. } | MemoryInitOp::Unsupported { .. } - | MemoryInitOp::TriviallyUnsafe { .. } => unreachable!(), + | MemoryInitOp::TriviallyUnsafe { .. } + | MemoryInitOp::Copy { .. } => unreachable!(), } } @@ -104,6 +123,7 @@ impl MemoryInitOp { | MemoryInitOp::CheckSliceChunk { .. } | MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => InsertPosition::Before, + MemoryInitOp::Copy { .. } => InsertPosition::After, } } } @@ -181,18 +201,12 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { 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(), + // 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(), }); - // Destimation 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. @@ -327,9 +341,7 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { count: args[2].clone(), }); } - "copy" - | "volatile_copy_memory" - | "volatile_copy_nonoverlapping_memory" => { + "copy" => { assert_eq!( args.len(), 3, @@ -343,15 +355,33 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { args[1].ty(self.locals).unwrap().kind(), TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut)) )); - self.push_target(MemoryInitOp::CheckSliceChunk { - operand: args[0].clone(), + // 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(), + } + // Here, `dst` is arg[0] and `src` is arg[1], so need to swap the order. + "volatile_copy_memory" | "volatile_copy_nonoverlapping_memory" => { + assert_eq!( + args.len(), + 3, + "Unexpected number of arguments for `volatile_copy`" + ); + assert!(matches!( + args[0].ty(self.locals).unwrap().kind(), + TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut)) + )); + assert!(matches!( + args[1].ty(self.locals).unwrap().kind(), + TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not)) + )); + // Copy memory initialization state from `src` to `dst`. + self.push_target(MemoryInitOp::Copy { + from: args[1].clone(), + to: args[0].clone(), count: args[2].clone(), - value: true, - position: InsertPosition::After, }); } "typed_swap" => { diff --git a/library/kani/src/mem_init.rs b/library/kani/src/mem_init.rs index a09e515d7e17..08550fd67200 100644 --- a/library/kani/src/mem_init.rs +++ b/library/kani/src/mem_init.rs @@ -89,6 +89,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. @@ -268,3 +295,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); + } +} From c14d65c406f88d97dc24496ae55c874ed0a29275 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 17 Jul 2024 12:05:31 -0700 Subject: [PATCH 2/9] Fix `copy` intrinsic test to reflect the semantic change --- tests/expected/uninit/intrinsics/expected | 14 +++++++-- .../expected/uninit/intrinsics/intrinsics.rs | 30 +++++++++++++++++-- 2 files changed, 39 insertions(+), 5 deletions(-) diff --git a/tests/expected/uninit/intrinsics/expected b/tests/expected/uninit/intrinsics/expected index ffa98b6f1140..4c4e3336018a 100644 --- a/tests/expected/uninit/intrinsics/expected +++ b/tests/expected/uninit/intrinsics/expected @@ -46,6 +46,10 @@ VERIFICATION:- SUCCESSFUL Checking harness check_copy... +VERIFICATION:- SUCCESSFUL + +Checking harness check_copy_read... + Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` VERIFICATION:- FAILED @@ -56,6 +60,10 @@ VERIFICATION:- SUCCESSFUL Checking harness check_copy_nonoverlapping... +VERIFICATION:- SUCCESSFUL + +Checking harness check_copy_nonoverlapping_read... + Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u8` VERIFICATION:- FAILED @@ -65,6 +73,6 @@ 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); } } From 82abe74169f0e027459b89ae0c84a2daeba46828 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 17 Jul 2024 12:43:37 -0700 Subject: [PATCH 3/9] Add extra copy-specific tests --- tests/expected/uninit/copy/copy.rs | 87 +++++++++++++++++++++++++++++ tests/expected/uninit/copy/expected | 31 ++++++++++ 2 files changed, 118 insertions(+) create mode 100644 tests/expected/uninit/copy/copy.rs create mode 100644 tests/expected/uninit/copy/expected diff --git a/tests/expected/uninit/copy/copy.rs b/tests/expected/uninit/copy/copy.rs new file mode 100644 index 000000000000..f506eb25ca42 --- /dev/null +++ b/tests/expected/uninit/copy/copy.rs @@ -0,0 +1,87 @@ +// 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 uninitialized bytes fails an assertion. +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); +} + +#[kani::proof] +/// This checks that reading copied uninitialized bytes after a multi-byte copy fails an assertion. +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); +} + +#[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); +} + +#[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); +} + +#[kani::proof] +/// This checks that reading uninitialized bytes fails an assertion even after copy. +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/copy/expected b/tests/expected/uninit/copy/expected new file mode 100644 index 000000000000..a288f9f2856d --- /dev/null +++ b/tests/expected/uninit/copy/expected @@ -0,0 +1,31 @@ +Checking harness read_after_copy... + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u64` + +VERIFICATION:- FAILED + +Checking harness non_byte_copy_without_padding... + +VERIFICATION:- SUCCESSFUL + +Checking harness copy_without_padding... + +VERIFICATION:- SUCCESSFUL + +Checking harness expose_padding_via_non_byte_copy... + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u64` + +VERIFICATION:- FAILED + +Checking harness expose_padding_via_copy... + +Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u64` + +VERIFICATION:- FAILED + +Summary: +Verification failed for - read_after_copy +Verification failed for - expose_padding_via_non_byte_copy +Verification failed for - expose_padding_via_copy +Complete - 2 successfully verified harnesses, 3 failures, 5 total. From 998002de2978c134d2448e0dd4d29c36712b1e7b Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Wed, 17 Jul 2024 12:49:03 -0700 Subject: [PATCH 4/9] Code formatting --- tests/expected/uninit/copy/copy.rs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/expected/uninit/copy/copy.rs b/tests/expected/uninit/copy/copy.rs index f506eb25ca42..8d8278a6f0b9 100644 --- a/tests/expected/uninit/copy/copy.rs +++ b/tests/expected/uninit/copy/copy.rs @@ -16,7 +16,7 @@ unsafe fn expose_padding_via_copy() { 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::()); + 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); @@ -32,7 +32,7 @@ unsafe fn expose_padding_via_non_byte_copy() { 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); + 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); @@ -51,7 +51,7 @@ unsafe fn copy_without_padding() { 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); + let data: u64 = std::ptr::read(to_ptr); } #[kani::proof] @@ -67,7 +67,7 @@ unsafe fn non_byte_copy_without_padding() { 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); + let data: u64 = std::ptr::read(to_ptr); } #[kani::proof] @@ -83,5 +83,5 @@ unsafe fn read_after_copy() { 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); + let data: u64 = std::ptr::read(from_ptr as *const u64); } From 753262c2e4d0bc6abc1bfeaddc1c67adbedafc3d Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Thu, 15 Aug 2024 08:38:17 -0700 Subject: [PATCH 5/9] Add comment stating that copy is untyped --- .../transform/check_uninit/ptr_uninit/uninit_visitor.rs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) 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 910e4d938d41..1209f73bba73 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,7 +88,8 @@ impl MirVisitor for CheckUninitVisitor { match &stmt.kind { StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(copy)) => { self.super_statement(stmt, location); - // Copy memory initialization state from `src` to `dst`. + // 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(), @@ -213,7 +214,8 @@ impl MirVisitor for CheckUninitVisitor { }); } Intrinsic::Copy => { - // Copy memory initialization state from `src` to `dst`. + // 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(), @@ -222,6 +224,9 @@ impl MirVisitor for CheckUninitVisitor { } Intrinsic::VolatileCopyMemory | Intrinsic::VolatileCopyNonOverlappingMemory => { + // 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(), From ce02e28c4228f206b9866e1538bc33f53a0c22b5 Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Thu, 15 Aug 2024 08:40:51 -0700 Subject: [PATCH 6/9] Code formatting --- .../transform/check_uninit/ptr_uninit/uninit_visitor.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 1209f73bba73..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 @@ -89,7 +89,7 @@ impl MirVisitor for CheckUninitVisitor { StatementKind::Intrinsic(NonDivergingIntrinsic::CopyNonOverlapping(copy)) => { self.super_statement(stmt, location); // The copy is untyped, so we should copy memory initialization state from `src` - // to `dst`. + // to `dst`. self.push_target(MemoryInitOp::Copy { from: copy.src.clone(), to: copy.dst.clone(), From 2eca14d3a0d4b7f2568325a9e7c38941b460e89c Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Thu, 15 Aug 2024 09:38:40 -0700 Subject: [PATCH 7/9] Add extra tests for copy + delayed ub, split copy tests into multiple --- copy_test.rs | 65 ++++++++++++++ tests/expected/uninit/copy/copy.rs | 87 ------------------- .../uninit/copy/copy_without_padding.expected | 1 + .../uninit/copy/copy_without_padding.rs | 23 +++++ tests/expected/uninit/copy/expected | 31 ------- .../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 | 43 +++++++++ .../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 ++- 17 files changed, 311 insertions(+), 119 deletions(-) create mode 100644 copy_test.rs delete mode 100644 tests/expected/uninit/copy/copy.rs create mode 100644 tests/expected/uninit/copy/copy_without_padding.expected create mode 100644 tests/expected/uninit/copy/copy_without_padding.rs delete mode 100644 tests/expected/uninit/copy/expected 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/copy_test.rs b/copy_test.rs new file mode 100644 index 000000000000..c58205007d58 --- /dev/null +++ b/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::()); // 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::()); + // 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/copy.rs b/tests/expected/uninit/copy/copy.rs deleted file mode 100644 index 8d8278a6f0b9..000000000000 --- a/tests/expected/uninit/copy/copy.rs +++ /dev/null @@ -1,87 +0,0 @@ -// 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 uninitialized bytes fails an assertion. -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); -} - -#[kani::proof] -/// This checks that reading copied uninitialized bytes after a multi-byte copy fails an assertion. -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); -} - -#[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); -} - -#[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); -} - -#[kani::proof] -/// This checks that reading uninitialized bytes fails an assertion even after copy. -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/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/expected b/tests/expected/uninit/copy/expected deleted file mode 100644 index a288f9f2856d..000000000000 --- a/tests/expected/uninit/copy/expected +++ /dev/null @@ -1,31 +0,0 @@ -Checking harness read_after_copy... - -Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u64` - -VERIFICATION:- FAILED - -Checking harness non_byte_copy_without_padding... - -VERIFICATION:- SUCCESSFUL - -Checking harness copy_without_padding... - -VERIFICATION:- SUCCESSFUL - -Checking harness expose_padding_via_non_byte_copy... - -Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u64` - -VERIFICATION:- FAILED - -Checking harness expose_padding_via_copy... - -Failed Checks: Undefined Behavior: Reading from an uninitialized pointer of type `*const u64` - -VERIFICATION:- FAILED - -Summary: -Verification failed for - read_after_copy -Verification failed for - expose_padding_via_non_byte_copy -Verification failed for - expose_padding_via_copy -Complete - 2 successfully verified harnesses, 3 failures, 5 total. 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..6b1c971aa4fe --- /dev/null +++ b/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::()); + // 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..46b57e675223 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. From 4cb2ccf6648495a7aab278e66a62a4c37edd21da Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Thu, 15 Aug 2024 09:43:33 -0700 Subject: [PATCH 8/9] Formatting change --- .../uninit/copy/expose_padding_via_copy_convoluted.rs | 1 - tests/expected/uninit/delayed-ub/delayed-ub.rs | 4 ++-- 2 files changed, 2 insertions(+), 3 deletions(-) diff --git a/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.rs b/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.rs index 6b1c971aa4fe..5feadace245d 100644 --- a/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.rs +++ b/tests/expected/uninit/copy/expose_padding_via_copy_convoluted.rs @@ -6,7 +6,6 @@ #[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] diff --git a/tests/expected/uninit/delayed-ub/delayed-ub.rs b/tests/expected/uninit/delayed-ub/delayed-ub.rs index 46b57e675223..d7f258c27ba5 100644 --- a/tests/expected/uninit/delayed-ub/delayed-ub.rs +++ b/tests/expected/uninit/delayed-ub/delayed-ub.rs @@ -135,7 +135,7 @@ fn delayed_ub_double_copy() { 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 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! @@ -189,7 +189,7 @@ 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 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! From 569d4f3533912f9f77096a7c2bab03eea15f92dc Mon Sep 17 00:00:00 2001 From: Artem Agvanian Date: Thu, 15 Aug 2024 09:46:13 -0700 Subject: [PATCH 9/9] Delete accidentally committed file --- copy_test.rs | 65 ---------------------------------------------------- 1 file changed, 65 deletions(-) delete mode 100644 copy_test.rs diff --git a/copy_test.rs b/copy_test.rs deleted file mode 100644 index c58205007d58..000000000000 --- a/copy_test.rs +++ /dev/null @@ -1,65 +0,0 @@ -#[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::()); // 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::()); - // 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); - } -}