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 e1b265751fd5..4f94f94d17f1 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -142,9 +142,11 @@ impl UninitPass { operation: MemoryInitOp, skip_first: &mut HashSet, ) { - if let MemoryInitOp::Unsupported { reason } = &operation { + if let MemoryInitOp::Unsupported { reason } | MemoryInitOp::TriviallyUnsafe { reason } = + &operation + { collect_skipped(&operation, body, skip_first); - self.unsupported_check(tcx, body, source, operation.position(), reason); + self.inject_assert_false(tcx, body, source, operation.position(), reason); return; }; @@ -166,7 +168,7 @@ impl UninitPass { "Kani currently doesn't support checking memory initialization for pointers to `{pointee_ty}.", ); collect_skipped(&operation, body, skip_first); - self.unsupported_check(tcx, body, source, operation.position(), &reason); + self.inject_assert_false(tcx, body, source, operation.position(), &reason); return; } } @@ -181,7 +183,7 @@ impl UninitPass { | MemoryInitOp::SetRef { .. } => { self.build_set(tcx, body, source, operation, pointee_ty_info, skip_first) } - MemoryInitOp::Unsupported { .. } => { + MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { unreachable!() } } @@ -266,7 +268,7 @@ impl UninitPass { PointeeLayout::TraitObject => { collect_skipped(&operation, body, skip_first); let reason = "Kani does not support reasoning about memory initialization of pointers to trait objects."; - self.unsupported_check(tcx, body, source, operation.position(), reason); + self.inject_assert_false(tcx, body, source, operation.position(), reason); return; } }; @@ -392,7 +394,7 @@ impl UninitPass { }; } - fn unsupported_check( + fn inject_assert_false( &self, tcx: TyCtxt, body: &mut MutableBody, 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 f68869e6681d..4c768aa2ee81 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 @@ -37,6 +37,8 @@ pub enum MemoryInitOp { SetRef { operand: Operand, value: bool, position: InsertPosition }, /// Unsupported memory initialization operation. Unsupported { reason: String }, + /// Operation that trivially accesses uninitialized memory, results in injecting `assert!(false)`. + TriviallyUnsafe { reason: String }, } impl MemoryInitOp { @@ -63,7 +65,9 @@ impl MemoryInitOp { }, projection: vec![], }), - MemoryInitOp::Unsupported { .. } => unreachable!(), + MemoryInitOp::Unsupported { .. } | MemoryInitOp::TriviallyUnsafe { .. } => { + unreachable!() + } } } @@ -74,7 +78,8 @@ impl MemoryInitOp { MemoryInitOp::Check { .. } | MemoryInitOp::Set { .. } | MemoryInitOp::SetRef { .. } - | MemoryInitOp::Unsupported { .. } => unreachable!(), + | MemoryInitOp::Unsupported { .. } + | MemoryInitOp::TriviallyUnsafe { .. } => unreachable!(), } } @@ -85,7 +90,8 @@ impl MemoryInitOp { | MemoryInitOp::SetRef { value, .. } => *value, MemoryInitOp::Check { .. } | MemoryInitOp::CheckSliceChunk { .. } - | MemoryInitOp::Unsupported { .. } => unreachable!(), + | MemoryInitOp::Unsupported { .. } + | MemoryInitOp::TriviallyUnsafe { .. } => unreachable!(), } } @@ -96,7 +102,8 @@ impl MemoryInitOp { | MemoryInitOp::SetRef { position, .. } => *position, MemoryInitOp::Check { .. } | MemoryInitOp::CheckSliceChunk { .. } - | MemoryInitOp::Unsupported { .. } => InsertPosition::Before, + | MemoryInitOp::Unsupported { .. } + | MemoryInitOp::TriviallyUnsafe { .. } => InsertPosition::Before, } } } @@ -581,6 +588,29 @@ impl<'a> MirVisitor for CheckUninitVisitor<'a> { } } } + CastKind::Transmute => { + let operand_ty = operand.ty(&self.locals).unwrap(); + if let ( + RigidTy::RawPtr(from_ty, Mutability::Mut), + RigidTy::RawPtr(to_ty, Mutability::Mut), + ) = (operand_ty.kind().rigid().unwrap(), ty.kind().rigid().unwrap()) + { + if !tys_layout_compatible(from_ty, to_ty) { + // If casting from a mutable pointer to a mutable pointer with different + // layouts, delayed UB could occur. + self.push_target(MemoryInitOp::Unsupported { + reason: "Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB.".to_string(), + }); + } + } else if !tys_layout_compatible(&operand_ty, &ty) { + // If transmuting between two types of incompatible layouts, padding + // bytes are exposed, which is UB. + self.push_target(MemoryInitOp::TriviallyUnsafe { + reason: "Transmuting between types of incompatible layouts." + .to_string(), + }); + } + } _ => {} } }; diff --git a/tests/expected/uninit/delayed-ub-transmute/delayed-ub-transmute.rs b/tests/expected/uninit/delayed-ub-transmute/delayed-ub-transmute.rs new file mode 100644 index 000000000000..df769e39a8b2 --- /dev/null +++ b/tests/expected/uninit/delayed-ub-transmute/delayed-ub-transmute.rs @@ -0,0 +1,14 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +/// Checks that Kani rejects mutable pointer casts between types of different padding. +#[kani::proof] +fn invalid_value() { + unsafe { + let mut value: u128 = 0; + let ptr: *mut (u8, u32, u64) = std::mem::transmute(&mut value as *mut _); + *ptr = (4, 4, 4); // This assignment itself does not cause UB... + let c: u128 = value; // ...but this reads a padding value! + } +} diff --git a/tests/expected/uninit/delayed-ub-transmute/expected b/tests/expected/uninit/delayed-ub-transmute/expected new file mode 100644 index 000000000000..e02883b26cdf --- /dev/null +++ b/tests/expected/uninit/delayed-ub-transmute/expected @@ -0,0 +1,5 @@ +Failed Checks: Kani does not support reasoning about memory initialization in presence of mutable raw pointer casts that could cause delayed UB. + +VERIFICATION:- FAILED + +Complete - 0 successfully verified harnesses, 1 failures, 1 total. \ No newline at end of file diff --git a/tests/expected/uninit/transmute-padding/expected b/tests/expected/uninit/transmute-padding/expected new file mode 100644 index 000000000000..980a01748fc7 --- /dev/null +++ b/tests/expected/uninit/transmute-padding/expected @@ -0,0 +1,5 @@ +Failed Checks: Transmuting between types of incompatible layouts. + +VERIFICATION:- FAILED + +Complete - 0 successfully verified harnesses, 1 failures, 1 total. \ No newline at end of file diff --git a/tests/expected/uninit/transmute-padding/transmute_padding.rs b/tests/expected/uninit/transmute-padding/transmute_padding.rs new file mode 100644 index 000000000000..b74346c98160 --- /dev/null +++ b/tests/expected/uninit/transmute-padding/transmute_padding.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z uninit-checks + +// 5 bytes of data + 3 bytes of padding. +#[repr(C)] +#[derive(kani::Arbitrary)] +struct S(u32, u8); + +/// Checks that Kani catches an attempt to access padding of a struct using transmute. +#[kani::proof] +fn check_uninit_padding() { + let s = kani::any(); + access_padding(s); +} + +fn access_padding(s: S) { + let _padding: u64 = unsafe { std::mem::transmute(s) }; // ~ERROR: padding bytes are uninitialized, so reading them is UB. +}