Skip to content

Commit 4f945c8

Browse files
SahithiMVSahithiMV
committed
Fixes
1 parent 36e75be commit 4f945c8

File tree

1 file changed

+136
-42
lines changed

1 file changed

+136
-42
lines changed

‎library/core/src/num/nonzero.rs‎

Lines changed: 136 additions & 42 deletions
Original file line numberDiff line numberDiff line change
@@ -1010,7 +1010,7 @@ macro_rules! nonzero_integer {
10101010
without modifying the original"]
10111011
#[inline]
10121012
#[requires({
1013-
!self.get().checked_mul(other.get()).is_some()
1013+
self.get().checked_mul(other.get()).is_some()
10141014
})]
10151015
#[ensures(|result: &Self| {
10161016
self.get().checked_mul(other.get()).unwrap() == result.get()
@@ -1378,7 +1378,7 @@ macro_rules! nonzero_integer_signedness_dependent_methods {
13781378
without modifying the original"]
13791379
#[inline]
13801380
#[requires({
1381-
!self.get().checked_add(other).is_some()
1381+
self.get().checked_add(other).is_some()
13821382
})]
13831383
#[ensures(|result: &Self| {
13841384
// Postcondition: the result matches the expected addition
@@ -2228,57 +2228,151 @@ mod verify {
22282228
nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128);
22292229
nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize);
22302230

2231-
macro_rules! nonzero_check_mul {
2232-
($t:ty, $nonzero_type:ty, $nonzero_unchecked_mul:ident) => {
2233-
#[kani::proof_for_contract(NonZero::unchecked_mul)]
2234-
pub fn $nonzero_unchecked_mul_for() {
2235-
let x: NonZeroI8 = kani::any();
2236-
let y: NonZeroI8 = kani::any();
2231+
2232+
macro_rules! nonzero_check_from_mut_unchecked {
2233+
($t:ty, $nonzero_type:ty, $harness_name:ident) => {
2234+
#[kani::proof]
2235+
pub fn $harness_name() {
2236+
let mut x: $t = kani::any();
2237+
kani::assume(x != 0);
22372238
unsafe {
2238-
let _ = x.unchecked_mul(y);
2239+
<$nonzero_type>::from_mut_unchecked(&mut x);
22392240
}
22402241
}
22412242
};
22422243
}
22432244

2244-
// Use the macro to generate different versions of the function for multiple types
2245-
nonzero_check!(i8, core::num::NonZeroI8, nonzero_unchecked_mul_for_i8);
2246-
nonzero_check!(i16, core::num::NonZeroI16, nonzero_unchecked_mul_for_16);
2247-
nonzero_check!(i32, core::num::NonZeroI32, nonzero_unchecked_mul_for_32);
2248-
nonzero_check!(i64, core::num::NonZeroI64, nonzero_unchecked_mul_for_64);
2249-
nonzero_check!(i128, core::num::NonZeroI128, nonzero_unchecked_mul_for_128);
2250-
nonzero_check!(isize, core::num::NonZeroIsize, nonzero_unchecked_mul_for_isize);
2251-
nonzero_check!(u8, core::num::NonZeroU8, nonzero_unchecked_mul_for_u8);
2252-
nonzero_check!(u16, core::num::NonZeroU16, nonzero_unchecked_mul_for_u16);
2253-
nonzero_check!(u32, core::num::NonZeroU32, nonzero_unchecked_mul_for_u32);
2254-
nonzero_check!(u64, core::num::NonZeroU64, nonzero_unchecked_mul_for_u64);
2255-
nonzero_check!(u128, core::num::NonZeroU128, nonzero_unchecked_mul_for_u128);
2256-
nonzero_check!(usize, core::num::NonZeroUsize, nonzero_unchecked_mul_for_usize);
2245+
// Generate harnesses for multiple types
2246+
nonzero_check_from_mut_unchecked!(i8, core::num::NonZeroI8, nonzero_check_from_mut_unchecked_i8);
2247+
nonzero_check_from_mut_unchecked!(i16, core::num::NonZeroI16, nonzero_check_from_mut_unchecked_i16);
2248+
nonzero_check_from_mut_unchecked!(i32, core::num::NonZeroI32, nonzero_check_from_mut_unchecked_i32);
2249+
nonzero_check_from_mut_unchecked!(i64, core::num::NonZeroI64, nonzero_check_from_mut_unchecked_i64);
2250+
nonzero_check_from_mut_unchecked!(i128, core::num::NonZeroI128, nonzero_check_from_mut_unchecked_i128);
2251+
nonzero_check_from_mut_unchecked!(isize, core::num::NonZeroIsize, nonzero_check_from_mut_unchecked_isize);
2252+
nonzero_check_from_mut_unchecked!(u8, core::num::NonZeroU8, nonzero_check_from_mut_unchecked_u8);
2253+
nonzero_check_from_mut_unchecked!(u16, core::num::NonZeroU16, nonzero_check_from_mut_unchecked_u16);
2254+
nonzero_check_from_mut_unchecked!(u32, core::num::NonZeroU32, nonzero_check_from_mut_unchecked_u32);
2255+
nonzero_check_from_mut_unchecked!(u64, core::num::NonZeroU64, nonzero_check_from_mut_unchecked_u64);
2256+
nonzero_check_from_mut_unchecked!(u128, core::num::NonZeroU128, nonzero_check_from_mut_unchecked_u128);
2257+
nonzero_check_from_mut_unchecked!(usize, core::num::NonZeroUsize, nonzero_check_from_mut_unchecked_usize);
2258+
2259+
2260+
2261+
macro_rules! check_mul_unchecked_small{
2262+
($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident) => {
2263+
#[kani::proof_for_contract(<$t>::unchecked_mul)]
2264+
pub fn $nonzero_check_mul_for() {
2265+
let x: $nonzero_type = kani::any();
2266+
let y: $nonzero_type = kani::any();
2267+
2268+
unsafe {
2269+
x.unchecked_mul(y);
2270+
}
2271+
}
2272+
};
2273+
}
2274+
2275+
macro_rules! check_mul_unchecked_intervals{
2276+
($t:ty, $nonzero_type:ty, $nonzero_check_mul_for:ident, $min:expr, $max:expr) => {
2277+
#[kani::proof_for_contract(<$t>::unchecked_mul)]
2278+
pub fn $nonzero_check_mul_for() {
2279+
let x = kani::any::<$t>();
2280+
let y = kani::any::<$t>();
2281+
2282+
kani::assume(x != 0 && x >= $min && x <= $max);
2283+
kani::assume(y != 0 && y >= $min && y <= $max);
2284+
2285+
let x = <$nonzero_type>::new(x).unwrap();
2286+
let y = <$nonzero_type>::new(y).unwrap();
2287+
2288+
unsafe {
2289+
x.unchecked_mul(y);
2290+
}
2291+
}
2292+
};
2293+
}
2294+
2295+
//Calls for i32
2296+
check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_small, NonZeroI32::new(-10i32).unwrap().into(), NonZeroI32::new(10i32).unwrap().into());
2297+
check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_large_pos, NonZeroI32::new(i32::MAX - 1000i32).unwrap().into(), NonZeroI32::new(i32::MAX).unwrap().into());
2298+
check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_large_neg, NonZeroI32::new(i32::MIN + 1000i32).unwrap().into(), NonZeroI32::new(i32::MIN + 1).unwrap().into());
2299+
check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_edge_pos, NonZeroI32::new(i32::MAX / 2).unwrap().into(), NonZeroI32::new(i32::MAX).unwrap().into());
2300+
check_mul_unchecked_intervals!(i32, NonZeroI32, check_mul_i32_edge_neg, NonZeroI32::new(i32::MIN / 2).unwrap().into(), NonZeroI32::new(i32::MIN + 1).unwrap().into());
2301+
2302+
//Calls for i64
2303+
check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_small, NonZeroI64::new(-10i64).unwrap().into(), NonZeroI64::new(10i64).unwrap().into());
2304+
check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_large_pos, NonZeroI64::new(i64::MAX - 1000i64).unwrap().into(), NonZeroI64::new(i64::MAX).unwrap().into());
2305+
check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_large_neg, NonZeroI64::new(i64::MIN + 1000i64).unwrap().into(), NonZeroI64::new(i64::MIN + 1).unwrap().into());
2306+
check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_edge_pos, NonZeroI64::new(i64::MAX / 2).unwrap().into(), NonZeroI64::new(i64::MAX).unwrap().into());
2307+
check_mul_unchecked_intervals!(i64, NonZeroI64, check_mul_i64_edge_neg, NonZeroI64::new(i64::MIN / 2).unwrap().into(), NonZeroI64::new(i64::MIN + 1).unwrap().into());
2308+
2309+
//calls for i128
2310+
check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_small, NonZeroI128::new(-10i128).unwrap().into(), NonZeroI128::new(10i128).unwrap().into());
2311+
check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_large_pos, NonZeroI128::new(i128::MAX - 1000i128).unwrap().into(), NonZeroI128::new(i128::MAX).unwrap().into());
2312+
check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_large_neg, NonZeroI128::new(i128::MIN + 1000i128).unwrap().into(), NonZeroI128::new(i128::MIN + 1).unwrap().into());
2313+
check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_edge_pos, NonZeroI128::new(i128::MAX / 2).unwrap().into(), NonZeroI128::new(i128::MAX).unwrap().into());
2314+
check_mul_unchecked_intervals!(i128, NonZeroI128, check_mul_i128_edge_neg, NonZeroI128::new(i128::MIN / 2).unwrap().into(), NonZeroI128::new(i128::MIN + 1).unwrap().into());
2315+
2316+
//calls for isize
2317+
check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_small, NonZeroIsize::new(-10isize).unwrap().into(), NonZeroIsize::new(10isize).unwrap().into());
2318+
check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_large_pos, NonZeroIsize::new(isize::MAX - 1000isize).unwrap().into(), NonZeroIsize::new(isize::MAX).unwrap().into());
2319+
check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_large_neg, NonZeroIsize::new(isize::MIN + 1000isize).unwrap().into(), NonZeroIsize::new(isize::MIN + 1).unwrap().into());
2320+
check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_edge_pos, NonZeroIsize::new(isize::MAX / 2).unwrap().into(), NonZeroIsize::new(isize::MAX).unwrap().into());
2321+
check_mul_unchecked_intervals!(isize, NonZeroIsize, check_mul_isize_edge_neg, NonZeroIsize::new(isize::MIN / 2).unwrap().into(), NonZeroIsize::new(isize::MIN + 1).unwrap().into());
2322+
2323+
//calls for u32
2324+
check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_small, NonZeroU32::new(1u32).unwrap().into(), NonZeroU32::new(10u32).unwrap().into());
2325+
check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_large, NonZeroU32::new(u32::MAX - 1000u32).unwrap().into(), NonZeroU32::new(u32::MAX).unwrap().into());
2326+
check_mul_unchecked_intervals!(u32, NonZeroU32, check_mul_u32_edge, NonZeroU32::new(u32::MAX / 2).unwrap().into(), NonZeroU32::new(u32::MAX).unwrap().into());
2327+
2328+
//calls for u64
2329+
check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_small, NonZeroU64::new(1u64).unwrap().into(), NonZeroU64::new(10u64).unwrap().into());
2330+
check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_large, NonZeroU64::new(u64::MAX - 1000u64).unwrap().into(), NonZeroU64::new(u64::MAX).unwrap().into());
2331+
check_mul_unchecked_intervals!(u64, NonZeroU64, check_mul_u64_edge, NonZeroU64::new(u64::MAX / 2).unwrap().into(), NonZeroU64::new(u64::MAX).unwrap().into());
2332+
2333+
//calls for u128
2334+
check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_small, NonZeroU128::new(1u128).unwrap().into(), NonZeroU128::new(10u128).unwrap().into());
2335+
check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_large, NonZeroU128::new(u128::MAX - 1000u128).unwrap().into(), NonZeroU128::new(u128::MAX).unwrap().into());
2336+
check_mul_unchecked_intervals!(u128, NonZeroU128, check_mul_u128_edge, NonZeroU128::new(u128::MAX / 2).unwrap().into(), NonZeroU128::new(u128::MAX).unwrap().into());
2337+
2338+
//calls for usize
2339+
check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_small, NonZeroUsize::new(1usize).unwrap().into(), NonZeroUsize::new(10usize).unwrap().into());
2340+
check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_large, NonZeroUsize::new(usize::MAX - 1000usize).unwrap().into(), NonZeroUsize::new(usize::MAX).unwrap().into());
2341+
check_mul_unchecked_intervals!(usize, NonZeroUsize, check_mul_usize_edge, NonZeroUsize::new(usize::MAX / 2).unwrap().into(), NonZeroUsize::new(usize::MAX).unwrap().into());
2342+
2343+
//calls for i8, i16, u8, u16
2344+
check_mul_unchecked_small!(i8, NonZeroI8, nonzero_check_mul_for_i8);
2345+
check_mul_unchecked_small!(i16, NonZeroI16, nonzero_check_mul_for_i16);
2346+
check_mul_unchecked_small!(u8, NonZeroU8, nonzero_check_mul_for_u8);
2347+
check_mul_unchecked_small!(u16, NonZeroU16, nonzero_check_mul_for_u16);
2348+
2349+
//check_mul_unchecked_large!(i16, NonZeroU16, nonzero_check_mul_for_u16);
22572350

22582351
macro_rules! nonzero_check_add {
2259-
($t:ty, $nonzero_type:ty, $nonzero_unchecked_add:ident) => {
2260-
#[kani::proof_for_contract(NonZero::unchecked_add)]
2261-
pub fn $nonzero_unchecked_add_for() {
2262-
let x: i8 = kani::any();
2263-
let y: i8 = kani::any();
2352+
($t:ty, $nonzero_type:ty, $nonzero_check_unchecked_add_for:ident) => {
2353+
#[kani::proof_for_contract(<$t>::unchecked_add)]
2354+
pub fn $nonzero_check_unchecked_add_for() {
2355+
let x: $nonzero_type = kani::any();
2356+
let y: $nonzero_type = kani::any();
2357+
22642358
unsafe {
2265-
let _ = x.unchecked_add(y); // Call the unchecked function
2359+
x.get().unchecked_add(y.get());
22662360
}
22672361
}
22682362
};
22692363
}
22702364

2271-
// Use the macro to generate different versions of the function for multiple types
2272-
nonzero_check!(i8, core::num::NonZeroI8, nonzero_unchecked_add_for_i8);
2273-
nonzero_check!(i16, core::num::NonZeroI16, nonzero_unchecked_add_for_16);
2274-
nonzero_check!(i32, core::num::NonZeroI32, nonzero_unchecked_add_for_32);
2275-
nonzero_check!(i64, core::num::NonZeroI64, nonzero_unchecked_add_for_64);
2276-
nonzero_check!(i128, core::num::NonZeroI128, nonzero_unchecked_add_for_128);
2277-
nonzero_check!(isize, core::num::NonZeroIsize, nonzero_unchecked_add_for_isize);
2278-
nonzero_check!(u8, core::num::NonZeroU8, nonzero_unchecked_add_for_u8);
2279-
nonzero_check!(u16, core::num::NonZeroU16, nonzero_unchecked_add_for_u16);
2280-
nonzero_check!(u32, core::num::NonZeroU32, nonzero_unchecked_add_for_u32);
2281-
nonzero_check!(u64, core::num::NonZeroU64, nonzero_unchecked_add_for_u64);
2282-
nonzero_check!(u128, core::num::NonZeroU128, nonzero_unchecked_add_for_u128);
2283-
nonzero_check!(usize, core::num::NonZeroUsize, nonzero_unchecked_add_for_usize);
2284-
}
2365+
// Generate proofs for all NonZero types
2366+
nonzero_check_add!(i8, core::num::NonZeroI8, nonzero_check_unchecked_add_for_i8);
2367+
nonzero_check_add!(i16, core::num::NonZeroI16, nonzero_check_unchecked_add_for_i16);
2368+
nonzero_check_add!(i32, core::num::NonZeroI32, nonzero_check_unchecked_add_for_i32);
2369+
nonzero_check_add!(i64, core::num::NonZeroI64, nonzero_check_unchecked_add_for_i64);
2370+
nonzero_check_add!(i128, core::num::NonZeroI128, nonzero_check_unchecked_add_for_i128);
2371+
nonzero_check_add!(isize, core::num::NonZeroIsize, nonzero_check_unchecked_add_for_isize);
2372+
nonzero_check_add!(u8, core::num::NonZeroU8, nonzero_check_unchecked_add_for_u8);
2373+
nonzero_check_add!(u16, core::num::NonZeroU16, nonzero_check_unchecked_add_for_u16);
2374+
nonzero_check_add!(u32, core::num::NonZeroU32, nonzero_check_unchecked_add_for_u32);
2375+
nonzero_check_add!(u64, core::num::NonZeroU64, nonzero_check_unchecked_add_for_u64);
2376+
nonzero_check_add!(u128, core::num::NonZeroU128, nonzero_check_unchecked_add_for_u128);
2377+
nonzero_check_add!(usize, core::num::NonZeroUsize, nonzero_check_unchecked_add_for_usize);
2378+
}

0 commit comments

Comments
 (0)