From 7ec065114eeb9d5e5159b6be72c5761d140f9d56 Mon Sep 17 00:00:00 2001 From: AlexLB99 Date: Mon, 3 Feb 2025 21:22:39 -0500 Subject: [PATCH] Added macros and removed padding harnesses --- library/core/src/intrinsics/mod.rs | 178 ++++++++++++++--------------- 1 file changed, 87 insertions(+), 91 deletions(-) diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index 0f2829f6b8242..5f20feb6fb31e 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -4643,7 +4643,8 @@ mod verify { unsafe { copy_nonoverlapping(src, dst, kani::any()) } } - //We need this wrapper because transmute_unchecked is an intrinsic, for which Kani does not currently support contracts + //We need this wrapper because transmute_unchecked is an intrinsic, for which Kani does + //not currently support contracts (https://github.com/model-checking/kani/issues/3345) #[requires(crate::mem::size_of::() == crate::mem::size_of::())] //T and U have same size (transmute_unchecked does not guarantee this) #[requires(ub_checks::can_dereference(&input as *const T as *const U))] //output can be deref'd as value of type U #[allow(dead_code)] @@ -4651,105 +4652,100 @@ mod verify { unsafe { transmute_unchecked(input) } } - #[kani::proof_for_contract(transmute_unchecked_wrapper)] - fn transmute_zero_size() { - let empty_arr: [u8;0] = []; - let unit_val: () = unsafe { transmute_unchecked_wrapper(empty_arr) }; - assert!(unit_val == ()); - } - - #[kani::proof_for_contract(transmute_unchecked_wrapper)] - fn transmute_u32_to_char() { - let num: u32 = kani::any(); - let c: char = unsafe {transmute_unchecked_wrapper(num)}; - } - - #[kani::proof] - #[kani::stub_verified(transmute_unchecked_wrapper)] - #[kani::should_panic] - fn transmute_invalid_u32_to_char() { - let num: u32 = kani::any(); - let c: char = unsafe {transmute_unchecked_wrapper(num)}; - } - - #[kani::proof_for_contract(transmute_unchecked_wrapper)] - fn transmute_u8_to_bool() { - let num: u8 = kani::any(); - let b: bool = unsafe {transmute_unchecked_wrapper(num)}; - } - - #[kani::proof] - #[kani::stub_verified(transmute_unchecked_wrapper)] - #[kani::should_panic] - fn transmute_invalid_u8_to_bool() { - let num: u8 = kani::any(); - let b: bool = unsafe {transmute_unchecked_wrapper(num)}; - } - - #[repr(C)] - struct A { - x: u8, - y: u16, - z: u8, - } - - #[repr(C)] - struct B { - x: u8, - y: u8, - z: u16, - } - - #[repr(C)] - struct C { - x: u16, - y: u16, - z: u16, + //generates harness that transmutes arbitrary values of input type to output type + //use when you expect all resulting bit patterns of output type to be valid + macro_rules! transmute_unchecked_should_succeed { + ($harness:ident, $src:ty, $dst:ty) => { + #[kani::proof_for_contract(transmute_unchecked_wrapper)] + fn $harness() { + let src: $src = kani::any(); + let dst: $dst = unsafe { transmute_unchecked_wrapper(src) }; + } + }; } - //This doesn't compile, A and B have different sizes due to padding - //This is likely due to a bug in Kani, see Kani issue 3839 - /*#[kani::proof_for_contract(transmute_unchecked_wrapper)] - fn transmute_unchecked_padding() { - let a = A {x: kani::any(), y: kani::any(), z: kani::any()}; - let x = a.x; - - let b: B = unsafe { transmute_unchecked_wrapper(a) }; - assert!(b.x == x); - }*/ - - #[kani::proof_for_contract(transmute_unchecked_wrapper)] - fn transmute_unchecked_padding() { - let a = A {x: kani::any(), y: kani::any(), z: kani::any()}; - let x = a.x; - - let c: C = unsafe { transmute_unchecked_wrapper(a) }; - assert!(c.x as u8 == x); + //generates harness that transmutes arbitrary values of input type to output type + //use when you expect some resulting bit patterns of output type to be invalid + macro_rules! transmute_unchecked_should_fail { + ($harness:ident, $src:ty, $dst:ty) => { + #[kani::proof] + #[kani::stub_verified(transmute_unchecked_wrapper)] + #[kani::should_panic] + fn $harness() { + let src: $src = kani::any(); + let dst: $dst = unsafe { transmute_unchecked_wrapper(src) }; + } + }; } + //transmute between the 4-byte numerical types + transmute_unchecked_should_succeed!(transmute_unchecked_i32_to_u32, i32, u32); + transmute_unchecked_should_succeed!(transmute_unchecked_u32_to_i32, u32, i32); + transmute_unchecked_should_succeed!(transmute_unchecked_i32_to_f32, i32, f32); + transmute_unchecked_should_succeed!(transmute_unchecked_f32_to_i32, f32, i32); + transmute_unchecked_should_succeed!(transmute_unchecked_u32_to_f32, u32, f32); + transmute_unchecked_should_succeed!(transmute_unchecked_f32_to_u32, f32, u32); + //transmute between the 8-byte numerical types + transmute_unchecked_should_succeed!(transmute_unchecked_i64_to_u64, i64, u64); + transmute_unchecked_should_succeed!(transmute_unchecked_u64_to_i64, u64, i64); + transmute_unchecked_should_succeed!(transmute_unchecked_i64_to_f64, i64, f64); + transmute_unchecked_should_succeed!(transmute_unchecked_f64_to_i64, f64, i64); + transmute_unchecked_should_succeed!(transmute_unchecked_u64_to_f64, u64, f64); + transmute_unchecked_should_succeed!(transmute_unchecked_f64_to_u64, f64, u64); + //transmute between arrays of bytes and numerical types + transmute_unchecked_should_succeed!(transmute_unchecked_arr_to_u32, [u8; 4], u32); + transmute_unchecked_should_succeed!(transmute_unchecked_u32_to_arr, u32, [u8; 4]); + transmute_unchecked_should_succeed!(transmute_unchecked_arr_to_u64, [u8; 8], u64); + transmute_unchecked_should_succeed!(transmute_unchecked_u64_to_arr, u64, [u8; 8]); + //transmute to type with potentially invalid bit patterns + transmute_unchecked_should_fail!(transmute_unchecked_u8_to_bool, u8, bool); + transmute_unchecked_should_fail!(transmute_unchecked_u32_to_char, u32, char); + + //tests that transmute works correctly when transmuting something with zero size #[kani::proof_for_contract(transmute_unchecked_wrapper)] - fn transmute_unchecked_2ways_i64_u64() { - let a: i64 = kani::any(); - let b: u64 = unsafe { transmute_unchecked_wrapper(a) }; - let c: i64 = unsafe { transmute_unchecked_wrapper(b) }; - assert_eq!(a,c); + fn transmute_zero_size() { + let empty_arr: [u8;0] = []; + let unit_val: () = unsafe { transmute_unchecked_wrapper(empty_arr) }; + assert!(unit_val == ()); } - #[kani::proof_for_contract(transmute_unchecked_wrapper)] - fn transmute_unchecked_2ways_i32_u32() { - let a: i32 = kani::any(); - let b: u32 = unsafe { transmute_unchecked_wrapper(a) }; - let c: i32 = unsafe { transmute_unchecked_wrapper(b) }; - assert_eq!(a,c); + //generates harness that transmutes arbitrary values two ways + //i.e. (src -> dest) then (dest -> src) + //We then check that the output is equal to the input + //This tests that transmute does not mutate the bit patterns + //Note: this would not catch reversible mutations + //e.g., deterministically flipping a bit + macro_rules! transmute_unchecked_two_ways { + ($harness:ident, $src:ty, $dst:ty) => { + #[kani::proof_for_contract(transmute_unchecked_wrapper)] + fn $harness() { + let src: $src = kani::any(); + let dst: $dst = unsafe { transmute_unchecked_wrapper(src) }; + let src2: $src = unsafe { transmute_unchecked_wrapper(dst) }; + assert_eq!(src,src2); + } + }; } - #[kani::proof_for_contract(transmute_unchecked_wrapper)] - fn transmute_unchecked_2ways_i8_u8() { - let a: i8 = kani::any(); - let b: u8 = unsafe { transmute_unchecked_wrapper(a) }; - let c: i8 = unsafe { transmute_unchecked_wrapper(b) }; - assert_eq!(a,c); - } + //transmute 2-ways between the 4-byte numerical types + transmute_unchecked_two_ways!(transmute_unchecked_2ways_i32_to_u32, i32, u32); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_u32_to_i32, u32, i32); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_i32_to_f32, i32, f32); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_f32_to_i32, f32, i32); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_u32_to_f32, u32, f32); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_f32_to_u32, f32, u32); + //transmute 2-ways between the 8-byte numerical types + transmute_unchecked_two_ways!(transmute_unchecked_2ways_i64_to_u64, i64, u64); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_u64_to_i64, u64, i64); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_i64_to_f64, i64, f64); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_f64_to_i64, f64, i64); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_u64_to_f64, u64, f64); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_f64_to_u64, f64, u64); + //transmute 2-ways between arrays of bytes and numerical types + transmute_unchecked_two_ways!(transmute_unchecked_2ways_arr_to_u32, [u8; 4], u32); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_u32_to_arr, u32, [u8; 4]); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_arr_to_u64, [u8; 8], u64); + transmute_unchecked_two_ways!(transmute_unchecked_2ways_u64_to_arr, u64, [u8; 8]); // FIXME: Enable this harness once is fixed. // Harness triggers a spurious failure when writing 0 bytes to an invalid memory location,