From 38b1cccf11d8cacba3ea19a47d9236fbc06501c2 Mon Sep 17 00:00:00 2001 From: AlexLB99 Date: Fri, 20 Dec 2024 12:39:00 -0500 Subject: [PATCH 1/7] removed some wrappers + resolved conflicts --- library/core/src/intrinsics/mod.rs | 118 +++++++++++++++++++++++++++++ 1 file changed, 118 insertions(+) diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index 29ef19daaf679..2b09c1f80f871 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -4592,6 +4592,13 @@ pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize ) } +//We need this wrapper because transmute_unchecked is an intrinsic, for which Kani does not currently support contracts +#[requires(crate::mem::size_of::() == crate::mem::size_of::())] //T and U have same size (transmute_unchecked does not guarantee this) +#[ensures(|ret: &U| (ub_checks::can_dereference(ret as *const U)))] //output can be deref'd as value of type U +unsafe fn transmute_unchecked_wrapper(input: T) -> U { + unsafe { transmute_unchecked(input) } +} + #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] mod verify { @@ -4688,4 +4695,115 @@ mod verify { fn supported_status(status: AllocationStatus) -> bool { status != AllocationStatus::Dangling && status != AllocationStatus::DeadObject } + + //this unexpectedly doesn't compile due to different sized inputs + //Normally, transmute_unchecked should be fine as long as output is not larger + /*#[kani::proof_for_contract(transmute_unchecked_wrapper)] + fn transmute_different_sizes() { + let large_value: u64 = kani::any(); + unsafe { + let truncated_value: u32 = transmute_unchecked_wrapper(large_value); + //assert!((truncated_value as u32) == 64); + } + }*/ + + #[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(); + kani::assume((num <= 0xD7FF) || (num >= 0xE000 && num <= 0x10FFFF)); + let c: char = unsafe {transmute_unchecked_wrapper(num)}; + } + + #[kani::proof_for_contract(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(); + kani::assume(num == 0 || num == 1); + let b: bool = unsafe {transmute_unchecked_wrapper(num)}; + } + + #[kani::proof_for_contract(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, + } + + //this doesn't compile, A and B have different sizes due to padding + /*#[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); + } + + #[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); + } + + #[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); + } + + #[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); + } + } From 55d66344a422ff22ce06651a57ed3ce436538f9a Mon Sep 17 00:00:00 2001 From: AlexLB99 Date: Fri, 20 Dec 2024 12:55:32 -0500 Subject: [PATCH 2/7] moved harnesses so they can get executed --- library/core/src/intrinsics/mod.rs | 91 +++++++++++++++--------------- 1 file changed, 45 insertions(+), 46 deletions(-) diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index 2b09c1f80f871..38e62ae1f9238 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -4650,52 +4650,6 @@ mod verify { unsafe { copy_nonoverlapping(src, dst, kani::any()) } } - // FIXME: Enable this harness once is fixed. - // Harness triggers a spurious failure when writing 0 bytes to an invalid memory location, - // which is a safe operation. - #[cfg(not(kani))] - #[kani::proof_for_contract(write_bytes)] - fn check_write_bytes() { - let mut generator = PointerGenerator::<100>::new(); - let ArbitraryPointer { - ptr, - status, - .. - } = generator.any_alloc_status::(); - kani::assume(supported_status(status)); - unsafe { write_bytes(ptr, kani::any(), kani::any()) }; - } - - fn run_with_arbitrary_ptrs(harness: impl Fn(*mut T, *mut T)) { - let mut generator1 = PointerGenerator::<100>::new(); - let mut generator2 = PointerGenerator::<100>::new(); - let ArbitraryPointer { - ptr: src, - status: src_status, - .. - } = generator1.any_alloc_status::(); - let ArbitraryPointer { - ptr: dst, - status: dst_status, - .. - } = if kani::any() { - generator1.any_alloc_status::() - } else { - generator2.any_alloc_status::() - }; - kani::assume(supported_status(src_status)); - kani::assume(supported_status(dst_status)); - harness(src, dst); - } - - /// Return whether the current status is supported by Kani's contract. - /// - /// Kani memory predicates currently doesn't support pointers to dangling or dead allocations. - /// Thus, we have to explicitly exclude those cases. - fn supported_status(status: AllocationStatus) -> bool { - status != AllocationStatus::Dangling && status != AllocationStatus::DeadObject - } - //this unexpectedly doesn't compile due to different sized inputs //Normally, transmute_unchecked should be fine as long as output is not larger /*#[kani::proof_for_contract(transmute_unchecked_wrapper)] @@ -4804,6 +4758,51 @@ mod verify { let b: u8 = unsafe { transmute_unchecked_wrapper(a) }; let c: i8 = unsafe { transmute_unchecked_wrapper(b) }; assert_eq!(a,c); + } + + // FIXME: Enable this harness once is fixed. + // Harness triggers a spurious failure when writing 0 bytes to an invalid memory location, + // which is a safe operation. + #[cfg(not(kani))] + #[kani::proof_for_contract(write_bytes)] + fn check_write_bytes() { + let mut generator = PointerGenerator::<100>::new(); + let ArbitraryPointer { + ptr, + status, + .. + } = generator.any_alloc_status::(); + kani::assume(supported_status(status)); + unsafe { write_bytes(ptr, kani::any(), kani::any()) }; } + fn run_with_arbitrary_ptrs(harness: impl Fn(*mut T, *mut T)) { + let mut generator1 = PointerGenerator::<100>::new(); + let mut generator2 = PointerGenerator::<100>::new(); + let ArbitraryPointer { + ptr: src, + status: src_status, + .. + } = generator1.any_alloc_status::(); + let ArbitraryPointer { + ptr: dst, + status: dst_status, + .. + } = if kani::any() { + generator1.any_alloc_status::() + } else { + generator2.any_alloc_status::() + }; + kani::assume(supported_status(src_status)); + kani::assume(supported_status(dst_status)); + harness(src, dst); + } + + /// Return whether the current status is supported by Kani's contract. + /// + /// Kani memory predicates currently doesn't support pointers to dangling or dead allocations. + /// Thus, we have to explicitly exclude those cases. + fn supported_status(status: AllocationStatus) -> bool { + status != AllocationStatus::Dangling && status != AllocationStatus::DeadObject + } } From 2c4de37de388f589ff9f2d4ec59b0ab74cb633f4 Mon Sep 17 00:00:00 2001 From: AlexLB99 Date: Fri, 20 Dec 2024 14:51:24 -0500 Subject: [PATCH 3/7] allowed wrapper to be dead code --- library/core/src/intrinsics/mod.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index 38e62ae1f9238..0186736459678 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -4595,6 +4595,7 @@ pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize //We need this wrapper because transmute_unchecked is an intrinsic, for which Kani does not currently support contracts #[requires(crate::mem::size_of::() == crate::mem::size_of::())] //T and U have same size (transmute_unchecked does not guarantee this) #[ensures(|ret: &U| (ub_checks::can_dereference(ret as *const U)))] //output can be deref'd as value of type U +#[allow(dead_code)] unsafe fn transmute_unchecked_wrapper(input: T) -> U { unsafe { transmute_unchecked(input) } } From afa73183b4b9b2ceec2b5a75277f1f810fe4130f Mon Sep 17 00:00:00 2001 From: AlexLB99 Date: Wed, 15 Jan 2025 17:27:02 -0500 Subject: [PATCH 4/7] moved wrapper into module + moved validity check to precondition --- library/core/src/intrinsics/mod.rs | 35 ++++++++++-------------------- 1 file changed, 12 insertions(+), 23 deletions(-) diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index 0186736459678..696f602ead922 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -4592,14 +4592,6 @@ pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize ) } -//We need this wrapper because transmute_unchecked is an intrinsic, for which Kani does not currently support contracts -#[requires(crate::mem::size_of::() == crate::mem::size_of::())] //T and U have same size (transmute_unchecked does not guarantee this) -#[ensures(|ret: &U| (ub_checks::can_dereference(ret as *const U)))] //output can be deref'd as value of type U -#[allow(dead_code)] -unsafe fn transmute_unchecked_wrapper(input: T) -> U { - unsafe { transmute_unchecked(input) } -} - #[cfg(kani)] #[unstable(feature = "kani", issue = "none")] mod verify { @@ -4650,17 +4642,14 @@ mod verify { let dst = if kani::any() { gen_any_ptr(&mut buffer2) } else { gen_any_ptr(&mut buffer1) }; unsafe { copy_nonoverlapping(src, dst, kani::any()) } } - - //this unexpectedly doesn't compile due to different sized inputs - //Normally, transmute_unchecked should be fine as long as output is not larger - /*#[kani::proof_for_contract(transmute_unchecked_wrapper)] - fn transmute_different_sizes() { - let large_value: u64 = kani::any(); - unsafe { - let truncated_value: u32 = transmute_unchecked_wrapper(large_value); - //assert!((truncated_value as u32) == 64); - } - }*/ + + //We need this wrapper because transmute_unchecked is an intrinsic, for which Kani does not currently support contracts + #[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)] + unsafe fn transmute_unchecked_wrapper(input: T) -> U { + unsafe { transmute_unchecked(input) } + } #[kani::proof_for_contract(transmute_unchecked_wrapper)] fn transmute_zero_size() { @@ -4672,11 +4661,11 @@ mod verify { #[kani::proof_for_contract(transmute_unchecked_wrapper)] fn transmute_u32_to_char() { let num: u32 = kani::any(); - kani::assume((num <= 0xD7FF) || (num >= 0xE000 && num <= 0x10FFFF)); let c: char = unsafe {transmute_unchecked_wrapper(num)}; } - #[kani::proof_for_contract(transmute_unchecked_wrapper)] + #[kani::proof] + #[kani::stub_verified(transmute_unchecked_wrapper)] #[kani::should_panic] fn transmute_invalid_u32_to_char() { let num: u32 = kani::any(); @@ -4686,11 +4675,11 @@ mod verify { #[kani::proof_for_contract(transmute_unchecked_wrapper)] fn transmute_u8_to_bool() { let num: u8 = kani::any(); - kani::assume(num == 0 || num == 1); let b: bool = unsafe {transmute_unchecked_wrapper(num)}; } - #[kani::proof_for_contract(transmute_unchecked_wrapper)] + #[kani::proof] + #[kani::stub_verified(transmute_unchecked_wrapper)] #[kani::should_panic] fn transmute_invalid_u8_to_bool() { let num: u8 = kani::any(); From c9038856e07bbb4e2e3fefa0735b9a17398b4b52 Mon Sep 17 00:00:00 2001 From: AlexLB99 Date: Wed, 15 Jan 2025 17:37:45 -0500 Subject: [PATCH 5/7] fixed spacing --- library/core/src/intrinsics/mod.rs | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index 696f602ead922..84368393a2bc7 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -4643,13 +4643,13 @@ 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 - #[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)] - unsafe fn transmute_unchecked_wrapper(input: T) -> U { - unsafe { transmute_unchecked(input) } - } + //We need this wrapper because transmute_unchecked is an intrinsic, for which Kani does not currently support contracts + #[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)] + unsafe fn transmute_unchecked_wrapper(input: T) -> U { + unsafe { transmute_unchecked(input) } + } #[kani::proof_for_contract(transmute_unchecked_wrapper)] fn transmute_zero_size() { From a822c98f58e5342e53ebc5c9ff3a61d900f5cd85 Mon Sep 17 00:00:00 2001 From: AlexLB99 Date: Wed, 15 Jan 2025 17:39:29 -0500 Subject: [PATCH 6/7] other formatting fixes --- library/core/src/intrinsics/mod.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index 84368393a2bc7..7f9796749a0bd 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -4665,7 +4665,7 @@ mod verify { } #[kani::proof] - #[kani::stub_verified(transmute_unchecked_wrapper)] + #[kani::stub_verified(transmute_unchecked_wrapper)] #[kani::should_panic] fn transmute_invalid_u32_to_char() { let num: u32 = kani::any(); @@ -4679,7 +4679,7 @@ mod verify { } #[kani::proof] - #[kani::stub_verified(transmute_unchecked_wrapper)] + #[kani::stub_verified(transmute_unchecked_wrapper)] #[kani::should_panic] fn transmute_invalid_u8_to_bool() { let num: u8 = kani::any(); From c089914f8ea538e421a1b1ad177299af5631365e Mon Sep 17 00:00:00 2001 From: AlexLB99 Date: Mon, 20 Jan 2025 15:58:34 -0500 Subject: [PATCH 7/7] added comment clarifying potential Kani bug --- library/core/src/intrinsics/mod.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index 7f9796749a0bd..0f2829f6b8242 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -4707,7 +4707,8 @@ mod verify { z: u16, } - //this doesn't compile, A and B have different sizes due to padding + //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()};