From 895e50362c6a907f9f82314a66ebb5fcdad2b481 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 28 Jan 2025 15:43:31 -0800 Subject: [PATCH 1/2] Fix transmute codegen when sizes are different Instead of crashing, add a safety check that ensures the transmute is not reachable. --- .../codegen_cprover_gotoc/codegen/rvalue.rs | 26 ++++++++++- .../intrinsics/transmute_diff_size.expected | 2 + .../intrinsics/transmute_diff_size.rs | 33 ++++++++++++++ .../transmute_unchecked_size.expected | 24 ++++++++++ .../intrinsics/transmute_unchecked_size.rs | 44 +++++++++++++++++++ 5 files changed, 127 insertions(+), 2 deletions(-) create mode 100644 tests/expected/intrinsics/transmute_diff_size.expected create mode 100644 tests/expected/intrinsics/transmute_diff_size.rs create mode 100644 tests/expected/intrinsics/transmute_unchecked_size.expected create mode 100644 tests/expected/intrinsics/transmute_unchecked_size.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index f4ca557afbdb..7f5568ccf152 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -801,8 +801,30 @@ impl GotocCtx<'_> { self.codegen_pointer_cast(k, e, *t, loc) } Rvalue::Cast(CastKind::Transmute, operand, ty) => { - let goto_typ = self.codegen_ty_stable(*ty); - self.codegen_operand_stable(operand).transmute_to(goto_typ, &self.symbol_table) + let src_ty = operand.ty(self.current_fn().locals()).unwrap(); + // Transmute requires sized types. + let src_sz = LayoutOf::new(src_ty).size_of().unwrap(); + let dst_sz = LayoutOf::new(*ty).size_of().unwrap(); + let dst_type = self.codegen_ty_stable(*ty); + if src_sz != dst_sz { + Expr::statement_expression( + vec![ + self.codegen_assert_assume_false( + PropertyClass::SafetyCheck, + &format!( + "Cannot transmute between types of different sizes. \ + Transmuting from `{src_sz}` to `{dst_sz}` bytes" + ), + loc, + ), + dst_type.nondet().as_stmt(loc), + ], + dst_type, + loc, + ) + } else { + self.codegen_operand_stable(operand).transmute_to(dst_type, &self.symbol_table) + } } Rvalue::BinaryOp(op, e1, e2) => self.codegen_rvalue_binary_op(res_ty, op, e1, e2, loc), Rvalue::CheckedBinaryOp(op, e1, e2) => { diff --git a/tests/expected/intrinsics/transmute_diff_size.expected b/tests/expected/intrinsics/transmute_diff_size.expected new file mode 100644 index 000000000000..efc770882422 --- /dev/null +++ b/tests/expected/intrinsics/transmute_diff_size.expected @@ -0,0 +1,2 @@ +error[E0512]: cannot transmute between types of different sizes, or dependently-sized types +error: aborting due to 3 previous errors diff --git a/tests/expected/intrinsics/transmute_diff_size.rs b/tests/expected/intrinsics/transmute_diff_size.rs new file mode 100644 index 000000000000..a38c37a379d9 --- /dev/null +++ b/tests/expected/intrinsics/transmute_diff_size.rs @@ -0,0 +1,33 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks that compilation fails when trying to transmute with different src and target sizes. + +#![feature(core_intrinsics)] +use std::intrinsics::transmute; + +/// This should fail due to UB detection. +#[kani::proof] +pub fn transmute_diff_size() { + let a: u32 = kani::any(); + if kani::any() { + let smaller: u16 = unsafe { transmute(a) }; + std::hint::black_box(smaller); + } else { + let bigger: (u64, isize) = unsafe { transmute(a) }; + std::hint::black_box(bigger); + } +} + +/// Generic transmute wrapper. +pub unsafe fn generic_transmute(src: S) -> D { + transmute(src) +} + +/// This should also fail due to UB detection. +#[kani::proof] +pub fn transmute_wrapper_diff_size() { + let a: (u32, char) = kani::any(); + let b: u128 = unsafe { generic_transmute(a) }; + std::hint::black_box(b); +} diff --git a/tests/expected/intrinsics/transmute_unchecked_size.expected b/tests/expected/intrinsics/transmute_unchecked_size.expected new file mode 100644 index 000000000000..6ff9a1f67366 --- /dev/null +++ b/tests/expected/intrinsics/transmute_unchecked_size.expected @@ -0,0 +1,24 @@ +Checking harness transmute_wrapper_diff_size... +Status: UNREACHABLE\ +Description: ""Unreachable expected"" + +Failed Checks: Cannot transmute between types of different sizes. Transmuting from `8` to `16` bytes + +VERIFICATION:- FAILED + +Checking harness transmute_diff_size... + +Status: UNREACHABLE\ +Description: ""This should never be reached"" + +Status: UNREACHABLE\ +Description: ""Neither this one"" + +Failed Checks: Cannot transmute between types of different sizes. Transmuting from `4` to `2` bytes +Failed Checks: Cannot transmute between types of different sizes. Transmuting from `4` to `16` bytes + +VERIFICATION:- FAILED + +Verification failed for - transmute_wrapper_diff_size +Verification failed for - transmute_diff_size +0 successfully verified harnesses, 2 failures, 2 total diff --git a/tests/expected/intrinsics/transmute_unchecked_size.rs b/tests/expected/intrinsics/transmute_unchecked_size.rs new file mode 100644 index 000000000000..05250636fcc0 --- /dev/null +++ b/tests/expected/intrinsics/transmute_unchecked_size.rs @@ -0,0 +1,44 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Checks that Kani correctly identify UB when invoking `transmute_unchecked` with different sizes. +//! See for more details. + +#![feature(core_intrinsics)] +use std::intrinsics::transmute_unchecked; + +/// Reachability doesn't seem to work for unreachable statements. +macro_rules! unreachable { + ($msg:literal) => { + assert!(false, $msg) + }; +} + +/// This should fail due to UB detection. +#[kani::proof] +pub fn transmute_diff_size() { + let a: u32 = kani::any(); + if kani::any() { + let smaller: u16 = unsafe { transmute_unchecked(a) }; + std::hint::black_box(smaller); + unreachable!("This should never be reached"); + } else { + let bigger: (u64, isize) = unsafe { transmute_unchecked(a) }; + std::hint::black_box(bigger); + unreachable!("Neither this one"); + } +} + +/// Generic transmute wrapper. +pub unsafe fn generic_transmute(src: S) -> D { + transmute_unchecked(src) +} + +/// This should also fail due to UB detection. +#[kani::proof] +pub fn transmute_wrapper_diff_size() { + let a: (u32, char) = kani::any(); + let b: u128 = unsafe { generic_transmute(a) }; + std::hint::black_box(b); + unreachable!("Unreachable expected"); +} From b045de0b707e67ddbc139ae5e4a858ada031194e Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 29 Jan 2025 10:11:04 -0800 Subject: [PATCH 2/2] Apply suggestions from code review --- tests/expected/intrinsics/transmute_unchecked_size.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/intrinsics/transmute_unchecked_size.rs b/tests/expected/intrinsics/transmute_unchecked_size.rs index 05250636fcc0..704448dcc6c6 100644 --- a/tests/expected/intrinsics/transmute_unchecked_size.rs +++ b/tests/expected/intrinsics/transmute_unchecked_size.rs @@ -7,7 +7,7 @@ #![feature(core_intrinsics)] use std::intrinsics::transmute_unchecked; -/// Reachability doesn't seem to work for unreachable statements. +/// Kani reachability checks are not currently applied to `unreachable` statements. macro_rules! unreachable { ($msg:literal) => { assert!(false, $msg)