From 5699f3ca2b71f52e482bd21ceac46f0e53934ff4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rafael=20S=C3=A1=20Menezes?= Date: Tue, 4 Feb 2025 21:40:06 +0000 Subject: [PATCH 1/2] Add goto-transcoder.md into summary (#243) The goto-transcoder is not appearing in the book pages. This should fix it. --- doc/src/SUMMARY.md | 1 + 1 file changed, 1 insertion(+) diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index 8073d12bf1f66..86b93dea01dba 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -8,6 +8,7 @@ - [Verification Tools](./tools.md) - [Kani](./tools/kani.md) + - [GOTO Transcoder](./tools/goto-transcoder.md) --- From db8e5a729bb434eca9c93dd4f8b34279af506740 Mon Sep 17 00:00:00 2001 From: Alex Le Blanc <83725365+AlexLB99@users.noreply.github.com> Date: Tue, 4 Feb 2025 17:12:17 -0500 Subject: [PATCH 2/2] transmute_unchecked contracts and harnesses (#185) 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](https://github.com/model-checking/kani/issues/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. --------- Co-authored-by: AlexLB99 --- library/core/src/intrinsics/mod.rs | 100 +++++++++++++++++++++++++++++ 1 file changed, 100 insertions(+) diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs index 29ef19daaf679..4063cdadca8cc 100644 --- a/library/core/src/intrinsics/mod.rs +++ b/library/core/src/intrinsics/mod.rs @@ -4642,6 +4642,106 @@ 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()) } } + + //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)] + unsafe fn transmute_unchecked_wrapper(input: T) -> U { + unsafe { transmute_unchecked(input) } + } + + //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) }; + } + }; + } + + //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_zero_size() { + let empty_arr: [u8;0] = []; + let unit_val: () = unsafe { transmute_unchecked_wrapper(empty_arr) }; + assert!(unit_val == ()); + } + + //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); + } + }; + } + + //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_u32_to_f32, u32, f32); + //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_u64_to_f64, u64, f64); + //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,