Skip to content

Commit

Permalink
Added macros and removed padding harnesses
Browse files Browse the repository at this point in the history
  • Loading branch information
AlexLB99 committed Feb 4, 2025
1 parent 07f07b2 commit 7ec0651
Showing 1 changed file with 87 additions and 91 deletions.
178 changes: 87 additions & 91 deletions library/core/src/intrinsics/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4643,113 +4643,109 @@ 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::<T>() == crate::mem::size_of::<U>())] //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<T,U>(input: T) -> U {
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 <https://github.com/model-checking/kani/issues/90> is fixed.
// Harness triggers a spurious failure when writing 0 bytes to an invalid memory location,
Expand Down

0 comments on commit 7ec0651

Please sign in to comment.