transmute_unchecked contracts and harnesses #185

AlexLB99 · 2024-11-25T20:56:15Z

This is a draft pull request towards solving #19.

Changes

Added wrappers for transmute_unchecked()
Annotated these wrappers with contracts
Wrote harnesses that verify these wrappers

Note: the reason we write wrappers for transmute_unchecked() and we annotate those wrappers is that function contracts do not appear to be currently supported for compiler intrinsics (as discussed in #3345). Also, rather than using a single wrapper for transmute_unchecked(), we write several with different constraints on the input (since leaving the function parameters completely generic severely restricts what we can do in the contracts, e.g., testing for equality).

This is not intended to be a complete solution for verifying transmute_unchecked(), but instead a proof of concept to see how aligned this is with the expected solution. Any feedback would be greatly appreciated -- thank you!

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

patricklam · 2024-11-26T01:50:25Z

hi @celinval and @feliperodri! Thoughts most welcome.

tautschnig · 2024-11-27T19:56:37Z

Can the CI failures please be addressed?

patricklam · 2024-12-01T06:30:52Z

I guess that we can't trigger the workflow @tautschnig

tautschnig · 2024-12-01T20:01:04Z

You might unintentionally have reverted submodule changes?

patricklam · 2024-12-02T20:46:49Z

Is it supposed to say "this workflow requires approval from a maintainer"?

AlexLB99 · 2024-12-02T23:05:12Z

You might unintentionally have reverted submodule changes?

I believe the issue may have been a merge conflict caused by a recent upstream commit that moved intrinsic.rs (which is the file being modified here) to another location. I think in theory the problem should be fixed now @tautschnig

tautschnig · 2024-12-03T00:16:16Z

Is it supposed to say "this workflow requires approval from a maintainer"?

Yes, we have opted for those rules out of caution.

tautschnig · 2024-12-03T00:17:02Z

You might unintentionally have reverted submodule changes?

It looks like those are still present.

AlexLB99 · 2024-12-03T22:21:47Z

You might unintentionally have reverted submodule changes?

It looks like those are still present.

Ah yes I see what you meant, it looks like there were some changes to library/stdarch. I've reverted those changes, so I think everything should be good to go now 👍

patricklam · 2024-12-04T18:49:09Z

@tautschnig can we get the ci to run?

tautschnig · 2024-12-04T22:12:34Z

@tautschnig can we get the ci to run?

CI run has been approved and is in progress.

patricklam · 2024-12-05T19:05:40Z

Requesting a review again...

celinval · 2024-12-05T19:34:51Z

library/core/src/intrinsics/mod.rs

@@ -4537,6 +4537,32 @@ pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize
    )
 }

+#[requires(crate::mem::size_of::<T>() >= crate::mem::size_of::<U>())] //U cannot be larger than T
+#[ensures(|ret: &U| (ret as *const U as usize) % crate::mem::align_of::<U>() == 0)] //check that the output has expected alignment
+pub unsafe fn transmute_unchecked_wrapper<T,U>(input: T) -> U {    


Can you please add a comment on why we need this and make this function private?

celinval · 2024-12-05T19:35:23Z

library/core/src/intrinsics/mod.rs

+//This requires means [output is char implies input is valid unicode value]
+#[requires(type_name::<U>() != type_name::<char>() || (input <= T::from(0xD7FF) || (input >= T::from(0xE000) && input <= T::from(0x10FFFF)) ))]
+#[ensures(|ret: &U| (ret as *const U as usize) % crate::mem::align_of::<U>() == 0)] 
+pub unsafe fn transmute_unchecked_from_u32<T,U>(input: T) -> U


I don't think we want to generate type specific wrappers.

Thank you for your comments! @celinval

One thing I was wondering, we couldn't find any ways to verify type-specific properties without putting constraints on the input/output types (hence the type-specific wrappers). In that case, would it be better to leave all type-specific validity checks to the "-Z valid-value-checks" logic, and to only verify generic properties in the generic wrapper (e.g., #[ensures(|ret: &U| (ub_checks::can_dereference(ret as *const U)))])?

celinval · 2024-12-05T19:39:55Z

library/core/src/intrinsics/mod.rs

@@ -4537,6 +4537,32 @@ pub(crate) const fn miri_promise_symbolic_alignment(ptr: *const (), align: usize
    )
 }

+#[requires(crate::mem::size_of::<T>() >= crate::mem::size_of::<U>())] //U cannot be larger than T


We don't need to size requirement since this is a compilation error according to the transmute documentation. We do need to state that input T is a valid U value. One possibility would be to use the can_dereference method from ub_checks.

However, with Kani, the value validity checks are still incomplete (see model-checking/kani#3203) for current limitations.

I created some new commits with these suggestions in mind. The only thing I left unchanged for now is the check for equality in the sizes of the input and output, since according to the documentation of transmute_unchecked, it seems that the compiler allows the inputs and outputs to have different sizes (as opposed to transmute), but considers this to be UB.

tautschnig · 2024-12-20T17:38:05Z

@AlexLB99 Was closing this PR an intentional act?

AlexLB99 · 2024-12-20T17:52:47Z

@AlexLB99 Was closing this PR an intentional act?

Yes, temporarily -- I was resolving some merge conflicts (so I started by deleting the previous commits, which automatically closes the pr). I also pushed some new changes to reflect the previous comments.

AlexLB99 · 2025-01-10T22:29:04Z

Hi, I'm just following up to see if anyone would be able to review this pr, to see if everything is on the right track (@celinval or anyone else interested). Thanks in advance!

celinval

It looks much better. I think the main adjustment is to add a value validity clause as a pre-condition.

celinval · 2025-01-13T18:26:53Z

library/core/src/intrinsics/mod.rs

@@ -4592,6 +4592,14 @@ 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


Actually, we could move this to be inside the verify module, right?

celinval · 2025-01-13T18:30:18Z

library/core/src/intrinsics/mod.rs

@@ -4592,6 +4592,14 @@ 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::<T>() == crate::mem::size_of::<U>())] //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


You actually want check value validity as a precondition. Since the return is by value, it would be immediate UB to return an invalid value.

celinval · 2025-01-13T18:40:03Z

library/core/src/intrinsics/mod.rs

+    #[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));


Can you please remove this assumption. This should be part of the precondition of the function.

celinval

Be aware that the value validity check is not currently enabled in this repository.

celinval · 2025-01-15T22:44:15Z

library/core/src/intrinsics/mod.rs

+    }
+
+    //this doesn't compile, A and B have different sizes due to padding
+    /*#[kani::proof_for_contract(transmute_unchecked_wrapper)]


I believe this is a bug in Kani. The following test compiles with rustc.

#![feature(core_intrinsics)] use std::intrinsics::transmute_unchecked; #[repr(C)] struct A { x: u8, y: u16, z: u8, } #[repr(C)] struct B { x: u8, y: u8, z: u16, } //this doesn't compile, A and B have different sizes due to padding fn main() { let a = A { x: 0, y: 0, z: 0 }; let x = a.x; let b: B = unsafe { transmute_unchecked(a) }; assert!(b.x == x); }

Can you please create an issue in Kani and update this comment?

celinval · 2025-01-15T22:45:33Z

library/core/src/intrinsics/mod.rs

+        z: u8,
+    }
+
+    #[repr(C)]


Are you able to catch issues where the structure representation is not C?

AlexLB99 changed the title ~~Transmute unchecked~~ transmute_unchecked contracts and harnesses Nov 27, 2024

tautschnig assigned AlexLB99 Nov 27, 2024

AlexLB99 closed this Dec 2, 2024

AlexLB99 force-pushed the transmute_unchecked branch from b163ae0 to 7e8a03d Compare December 2, 2024 19:56

AlexLB99 reopened this Dec 2, 2024

celinval reviewed Dec 5, 2024

View reviewed changes

tautschnig assigned celinval Dec 11, 2024

AlexLB99 closed this Dec 20, 2024

AlexLB99 force-pushed the transmute_unchecked branch from b86e230 to 5da586f Compare December 20, 2024 16:56

removed some wrappers + resolved conflicts

38b1ccc

AlexLB99 reopened this Dec 20, 2024

AlexLB99 added 2 commits December 20, 2024 12:55

moved harnesses so they can get executed

55d6634

allowed wrapper to be dead code

2c4de37

celinval reviewed Jan 13, 2025

View reviewed changes

Merge branch 'model-checking:main' into transmute_unchecked

126f945

AlexLB99 added 3 commits January 15, 2025 17:27

moved wrapper into module + moved validity check to precondition

afa7318

fixed spacing

c903885

other formatting fixes

a822c98

celinval reviewed Jan 15, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

transmute_unchecked contracts and harnesses #185

transmute_unchecked contracts and harnesses #185

AlexLB99 commented Nov 25, 2024

patricklam commented Nov 26, 2024

tautschnig commented Nov 27, 2024

patricklam commented Dec 1, 2024

tautschnig commented Dec 1, 2024

patricklam commented Dec 2, 2024

AlexLB99 commented Dec 2, 2024

tautschnig commented Dec 3, 2024

tautschnig commented Dec 3, 2024

AlexLB99 commented Dec 3, 2024

patricklam commented Dec 4, 2024

tautschnig commented Dec 4, 2024

patricklam commented Dec 5, 2024

celinval Dec 5, 2024

celinval Dec 5, 2024

AlexLB99 Dec 10, 2024 •

edited

Loading

celinval Dec 5, 2024

AlexLB99 Dec 20, 2024

tautschnig commented Dec 20, 2024

AlexLB99 commented Dec 20, 2024

AlexLB99 commented Jan 10, 2025

celinval left a comment

celinval Jan 13, 2025

celinval Jan 13, 2025

celinval Jan 13, 2025

celinval left a comment

celinval Jan 15, 2025

celinval Jan 15, 2025

transmute_unchecked contracts and harnesses #185

Are you sure you want to change the base?

transmute_unchecked contracts and harnesses #185

Conversation

AlexLB99 commented Nov 25, 2024

Changes

patricklam commented Nov 26, 2024

tautschnig commented Nov 27, 2024

patricklam commented Dec 1, 2024

tautschnig commented Dec 1, 2024

patricklam commented Dec 2, 2024

AlexLB99 commented Dec 2, 2024

tautschnig commented Dec 3, 2024

tautschnig commented Dec 3, 2024

AlexLB99 commented Dec 3, 2024

patricklam commented Dec 4, 2024

tautschnig commented Dec 4, 2024

patricklam commented Dec 5, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

AlexLB99 Dec 10, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tautschnig commented Dec 20, 2024

AlexLB99 commented Dec 20, 2024

AlexLB99 commented Jan 10, 2025

celinval left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

celinval left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

AlexLB99 Dec 10, 2024 •

edited

Loading