Skip to content

Commit f3fa8ef

Browse files
carolynzechcarolynzech
committed
address PR feedback
1 parent f8b1afc commit f3fa8ef

File tree

3 files changed

+2
-281
lines changed

3 files changed

+2
-281
lines changed

‎.github/workflows/kani.yml

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -99,16 +99,13 @@ jobs:
9999
# explicitly list all functions (or prefixes thereof) the proofs of which
100100
# are known to pass.
101101
# Notes:
102-
# - We use >::disjoint_bitor (and >::unchecked_disjoint_bitor) as pattern
103-
# as whitespace is not supported, cf.
104-
# https://github.com/model-checking/kani/issues/4046
105102
# - core_arch::x86::__m128d::as_f64x2 is just one example of hundreds of
106103
# core_arch::x86:: functions that are known to verify successfully.
107104
- name: Run Kani Verification
108105
run: |
109106
scripts/run-kani.sh --run autoharness --kani-args \
110-
--include-pattern ">::disjoint_bitor" \
111-
--include-pattern ">::unchecked_disjoint_bitor" \
107+
--include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::disjoint_bitor" \
108+
--include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::unchecked_disjoint_bitor" \
112109
--include-pattern alloc::__default_lib_allocator:: \
113110
--include-pattern alloc::layout::Layout::from_size_align \
114111
--include-pattern ascii::ascii_char::AsciiChar::from_u8 \

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

Lines changed: 0 additions & 68 deletions
Original file line numberDiff line numberDiff line change
@@ -600,74 +600,6 @@ impl_nonzero_int_try_from_nonzero_int!(isize => u8, u16, u32, u64, u128, usize);
600600
mod verify {
601601
use super::*;
602602

603-
// Generate harnesses for `NonZero::<Large>::from(NonZero<Small>)`.
604-
macro_rules! generate_nonzero_int_from_nonzero_int_harness {
605-
($Small:ty => $Large:ty, $harness:ident) => {
606-
#[kani::proof]
607-
pub fn $harness() {
608-
let x: NonZero<$Small> = kani::any();
609-
let _ = NonZero::<$Large>::from(x);
610-
}
611-
};
612-
}
613-
614-
// This bundles the calls to `generate_nonzero_int_from_nonzero_int_harness`
615-
// macro into segregated namespaces for better organization and usability.
616-
macro_rules! generate_nonzero_int_from_nonzero_int_harnesses {
617-
($ns:ident, $Small:ty => $($Large:tt),+ $(,)?) => {
618-
mod $ns {
619-
use super::*;
620-
621-
$(
622-
mod $Large {
623-
use super::*;
624-
625-
generate_nonzero_int_from_nonzero_int_harness!(
626-
$Small => $Large,
627-
check_nonzero_int_from_nonzero_int
628-
);
629-
}
630-
)+
631-
}
632-
};
633-
}
634-
635-
// non-zero unsigned integer -> non-zero integer, infallible
636-
generate_nonzero_int_from_nonzero_int_harnesses!(
637-
check_nonzero_int_from_u8,
638-
u8 => u16, u32, u64, u128, usize, i16, i32, i64, i128, isize,
639-
);
640-
generate_nonzero_int_from_nonzero_int_harnesses!(
641-
check_nonzero_int_from_u16,
642-
u16 => u32, u64, u128, usize, i32, i64, i128,
643-
);
644-
generate_nonzero_int_from_nonzero_int_harnesses!(
645-
check_nonzero_int_from_u32,
646-
u32 => u64, u128, i64, i128,
647-
);
648-
generate_nonzero_int_from_nonzero_int_harnesses!(
649-
check_nonzero_int_from_u64,
650-
u64 => u128, i128,
651-
);
652-
653-
// non-zero signed integer -> non-zero signed integer, infallible
654-
generate_nonzero_int_from_nonzero_int_harnesses!(
655-
check_nonzero_int_from_i8,
656-
i8 => i16, i32, i64, i128, isize,
657-
);
658-
generate_nonzero_int_from_nonzero_int_harnesses!(
659-
check_nonzero_int_from_i16,
660-
i16 => i32, i64, i128, isize,
661-
);
662-
generate_nonzero_int_from_nonzero_int_harnesses!(
663-
check_nonzero_int_from_i32,
664-
i32 => i64, i128,
665-
);
666-
generate_nonzero_int_from_nonzero_int_harnesses!(
667-
check_nonzero_int_from_i64,
668-
i64 => i128,
669-
);
670-
671603
// Generates harnesses for `NonZero::<target>::try_from(NonZero<source>)`.
672604
// Since the function may be fallible or infallible depending on `source` and `target`,
673605
// this macro supports generating both cases.

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

Lines changed: 0 additions & 208 deletions
Original file line numberDiff line numberDiff line change
@@ -1681,34 +1681,6 @@ mod verify {
16811681
}
16821682
}
16831683

1684-
// Verify `unchecked_{shl, shr}`
1685-
macro_rules! generate_unchecked_shift_harness {
1686-
($type:ty, $method:ident, $harness_name:ident) => {
1687-
#[kani::proof_for_contract($type::$method)]
1688-
pub fn $harness_name() {
1689-
let num1: $type = kani::any::<$type>();
1690-
let num2: u32 = kani::any::<u32>();
1691-
1692-
unsafe {
1693-
num1.$method(num2);
1694-
}
1695-
}
1696-
};
1697-
}
1698-
1699-
macro_rules! generate_unchecked_neg_harness {
1700-
($type:ty, $harness_name:ident) => {
1701-
#[kani::proof_for_contract($type::unchecked_neg)]
1702-
pub fn $harness_name() {
1703-
let num1: $type = kani::any::<$type>();
1704-
1705-
unsafe {
1706-
num1.unchecked_neg();
1707-
}
1708-
}
1709-
};
1710-
}
1711-
17121684
/// A macro to generate Kani proof harnesses for the `carrying_mul` method,
17131685
///
17141686
/// The macro creates multiple harnesses for different ranges of input values,
@@ -1810,63 +1782,6 @@ mod verify {
18101782
}
18111783
}
18121784

1813-
// `unchecked_add` proofs
1814-
//
1815-
// Target types:
1816-
// i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
1817-
//
1818-
// Target contracts:
1819-
// Preconditions: No overflow should occur
1820-
// #[requires(!self.overflowing_add(rhs).1)]
1821-
//
1822-
// Target function:
1823-
// pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
1824-
generate_unchecked_math_harness!(i8, unchecked_add, checked_unchecked_add_i8);
1825-
generate_unchecked_math_harness!(i16, unchecked_add, checked_unchecked_add_i16);
1826-
generate_unchecked_math_harness!(i32, unchecked_add, checked_unchecked_add_i32);
1827-
generate_unchecked_math_harness!(i64, unchecked_add, checked_unchecked_add_i64);
1828-
generate_unchecked_math_harness!(i128, unchecked_add, checked_unchecked_add_i128);
1829-
generate_unchecked_math_harness!(isize, unchecked_add, checked_unchecked_add_isize);
1830-
generate_unchecked_math_harness!(u8, unchecked_add, checked_unchecked_add_u8);
1831-
generate_unchecked_math_harness!(u16, unchecked_add, checked_unchecked_add_u16);
1832-
generate_unchecked_math_harness!(u32, unchecked_add, checked_unchecked_add_u32);
1833-
generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64);
1834-
generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128);
1835-
generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize);
1836-
1837-
// `unchecked_neg` proofs
1838-
//
1839-
// Target types:
1840-
// i{8,16,32,64,128,size} -- 6 types in total
1841-
//
1842-
// Target contracts:
1843-
// #[requires(self != $SelfT::MIN)]
1844-
//
1845-
// Target function:
1846-
// pub const unsafe fn unchecked_neg(self) -> Self
1847-
generate_unchecked_neg_harness!(i8, checked_unchecked_neg_i8);
1848-
generate_unchecked_neg_harness!(i16, checked_unchecked_neg_i16);
1849-
generate_unchecked_neg_harness!(i32, checked_unchecked_neg_i32);
1850-
generate_unchecked_neg_harness!(i64, checked_unchecked_neg_i64);
1851-
generate_unchecked_neg_harness!(i128, checked_unchecked_neg_i128);
1852-
generate_unchecked_neg_harness!(isize, checked_unchecked_neg_isize);
1853-
1854-
// `unchecked_mul` proofs
1855-
//
1856-
// Target types:
1857-
// i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total, with different interval checks for each.
1858-
// Total types of checks including intervals -- 36
1859-
//
1860-
// Target contracts:
1861-
// Preconditions: No overflow should occur
1862-
// #[requires(!self.overflowing_mul(rhs).1)]
1863-
//
1864-
// Target function:
1865-
// pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self
1866-
// exponential state spaces for 32,64 and 128, hence provided limited range for verification.
1867-
generate_unchecked_math_harness!(i8, unchecked_mul, checked_unchecked_mul_i8);
1868-
generate_unchecked_math_harness!(i16, unchecked_mul, checked_unchecked_mul_i16);
1869-
18701785
// ====================== i32 Harnesses ======================
18711786
generate_unchecked_mul_intervals!(
18721787
i32,
@@ -2008,80 +1923,6 @@ mod verify {
20081923
usize::MAX
20091924
);
20101925

2011-
// unchecked_shr proofs
2012-
//
2013-
// Target types:
2014-
// i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
2015-
//
2016-
// Target contracts:
2017-
// #[requires(rhs < <$ActualT>::BITS)]
2018-
//
2019-
// Target function:
2020-
// pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self
2021-
generate_unchecked_shift_harness!(i8, unchecked_shr, checked_unchecked_shr_i8);
2022-
generate_unchecked_shift_harness!(i16, unchecked_shr, checked_unchecked_shr_i16);
2023-
generate_unchecked_shift_harness!(i32, unchecked_shr, checked_unchecked_shr_i32);
2024-
generate_unchecked_shift_harness!(i64, unchecked_shr, checked_unchecked_shr_i64);
2025-
generate_unchecked_shift_harness!(i128, unchecked_shr, checked_unchecked_shr_i128);
2026-
generate_unchecked_shift_harness!(isize, unchecked_shr, checked_unchecked_shr_isize);
2027-
generate_unchecked_shift_harness!(u8, unchecked_shr, checked_unchecked_shr_u8);
2028-
generate_unchecked_shift_harness!(u16, unchecked_shr, checked_unchecked_shr_u16);
2029-
generate_unchecked_shift_harness!(u32, unchecked_shr, checked_unchecked_shr_u32);
2030-
generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64);
2031-
generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128);
2032-
generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize);
2033-
2034-
// `unchecked_shl` proofs
2035-
//
2036-
// Target types:
2037-
// i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
2038-
//
2039-
// Target contracts:
2040-
// #[requires(shift < Self::BITS)]
2041-
//
2042-
// Target function:
2043-
// pub const unsafe fn unchecked_shl(self, shift: u32) -> Self
2044-
//
2045-
// This function performs an unchecked bitwise left shift operation.
2046-
generate_unchecked_shift_harness!(i8, unchecked_shl, checked_unchecked_shl_i8);
2047-
generate_unchecked_shift_harness!(i16, unchecked_shl, checked_unchecked_shl_i16);
2048-
generate_unchecked_shift_harness!(i32, unchecked_shl, checked_unchecked_shl_i32);
2049-
generate_unchecked_shift_harness!(i64, unchecked_shl, checked_unchecked_shl_i64);
2050-
generate_unchecked_shift_harness!(i128, unchecked_shl, checked_unchecked_shl_i128);
2051-
generate_unchecked_shift_harness!(isize, unchecked_shl, checked_unchecked_shl_isize);
2052-
generate_unchecked_shift_harness!(u8, unchecked_shl, checked_unchecked_shl_u8);
2053-
generate_unchecked_shift_harness!(u16, unchecked_shl, checked_unchecked_shl_u16);
2054-
generate_unchecked_shift_harness!(u32, unchecked_shl, checked_unchecked_shl_u32);
2055-
generate_unchecked_shift_harness!(u64, unchecked_shl, checked_unchecked_shl_u64);
2056-
generate_unchecked_shift_harness!(u128, unchecked_shl, checked_unchecked_shl_u128);
2057-
generate_unchecked_shift_harness!(usize, unchecked_shl, checked_unchecked_shl_usize);
2058-
2059-
// `unchecked_sub` proofs
2060-
//
2061-
// Target types:
2062-
// i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
2063-
//
2064-
// Target contracts:
2065-
// Preconditions: No overflow should occur
2066-
// #[requires(!self.overflowing_sub(rhs).1)]
2067-
//
2068-
// Target function:
2069-
// pub const unsafe fn unchecked_sub(self, rhs: Self) -> Self
2070-
//
2071-
// This function performs an unchecked subtraction operation.
2072-
generate_unchecked_math_harness!(i8, unchecked_sub, checked_unchecked_sub_i8);
2073-
generate_unchecked_math_harness!(i16, unchecked_sub, checked_unchecked_sub_i16);
2074-
generate_unchecked_math_harness!(i32, unchecked_sub, checked_unchecked_sub_i32);
2075-
generate_unchecked_math_harness!(i64, unchecked_sub, checked_unchecked_sub_i64);
2076-
generate_unchecked_math_harness!(i128, unchecked_sub, checked_unchecked_sub_i128);
2077-
generate_unchecked_math_harness!(isize, unchecked_sub, checked_unchecked_sub_isize);
2078-
generate_unchecked_math_harness!(u8, unchecked_sub, checked_unchecked_sub_u8);
2079-
generate_unchecked_math_harness!(u16, unchecked_sub, checked_unchecked_sub_u16);
2080-
generate_unchecked_math_harness!(u32, unchecked_sub, checked_unchecked_sub_u32);
2081-
generate_unchecked_math_harness!(u64, unchecked_sub, checked_unchecked_sub_u64);
2082-
generate_unchecked_math_harness!(u128, unchecked_sub, checked_unchecked_sub_u128);
2083-
generate_unchecked_math_harness!(usize, unchecked_sub, checked_unchecked_sub_usize);
2084-
20851926
// Part_2 `carrying_mul` proofs
20861927
//
20871928
// ====================== u8 Harnesses ======================
@@ -2172,55 +2013,6 @@ mod verify {
21722013
(u64::MAX / 2) + 10u64
21732014
);
21742015

2175-
// Part_2 `wrapping_shl` proofs
2176-
//
2177-
// Target types:
2178-
// i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
2179-
//
2180-
// Target contracts:
2181-
// #[ensures(|result| *result == self << (rhs & (Self::BITS - 1)))]
2182-
//
2183-
// Target function:
2184-
// pub const fn wrapping_shl(self, rhs: u32) -> Self
2185-
//
2186-
// This function performs an panic-free bitwise left shift operation.
2187-
generate_wrapping_shift_harness!(i8, wrapping_shl, checked_wrapping_shl_i8);
2188-
generate_wrapping_shift_harness!(i16, wrapping_shl, checked_wrapping_shl_i16);
2189-
generate_wrapping_shift_harness!(i32, wrapping_shl, checked_wrapping_shl_i32);
2190-
generate_wrapping_shift_harness!(i64, wrapping_shl, checked_wrapping_shl_i64);
2191-
generate_wrapping_shift_harness!(i128, wrapping_shl, checked_wrapping_shl_i128);
2192-
generate_wrapping_shift_harness!(isize, wrapping_shl, checked_wrapping_shl_isize);
2193-
generate_wrapping_shift_harness!(u8, wrapping_shl, checked_wrapping_shl_u8);
2194-
generate_wrapping_shift_harness!(u16, wrapping_shl, checked_wrapping_shl_u16);
2195-
generate_wrapping_shift_harness!(u32, wrapping_shl, checked_wrapping_shl_u32);
2196-
generate_wrapping_shift_harness!(u64, wrapping_shl, checked_wrapping_shl_u64);
2197-
generate_wrapping_shift_harness!(u128, wrapping_shl, checked_wrapping_shl_u128);
2198-
generate_wrapping_shift_harness!(usize, wrapping_shl, checked_wrapping_shl_usize);
2199-
2200-
// Part_2 `wrapping_shr` proofs
2201-
//
2202-
// Target types:
2203-
// i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
2204-
//
2205-
// Target contracts:
2206-
// #[ensures(|result| *result == self >> (rhs & (Self::BITS - 1)))]
2207-
// Target function:
2208-
// pub const fn wrapping_shr(self, rhs: u32) -> Self {
2209-
//
2210-
// This function performs an panic-free bitwise right shift operation.
2211-
generate_wrapping_shift_harness!(i8, wrapping_shr, checked_wrapping_shr_i8);
2212-
generate_wrapping_shift_harness!(i16, wrapping_shr, checked_wrapping_shr_i16);
2213-
generate_wrapping_shift_harness!(i32, wrapping_shr, checked_wrapping_shr_i32);
2214-
generate_wrapping_shift_harness!(i64, wrapping_shr, checked_wrapping_shr_i64);
2215-
generate_wrapping_shift_harness!(i128, wrapping_shr, checked_wrapping_shr_i128);
2216-
generate_wrapping_shift_harness!(isize, wrapping_shr, checked_wrapping_shr_isize);
2217-
generate_wrapping_shift_harness!(u8, wrapping_shr, checked_wrapping_shr_u8);
2218-
generate_wrapping_shift_harness!(u16, wrapping_shr, checked_wrapping_shr_u16);
2219-
generate_wrapping_shift_harness!(u32, wrapping_shr, checked_wrapping_shr_u32);
2220-
generate_wrapping_shift_harness!(u64, wrapping_shr, checked_wrapping_shr_u64);
2221-
generate_wrapping_shift_harness!(u128, wrapping_shr, checked_wrapping_shr_u128);
2222-
generate_wrapping_shift_harness!(usize, wrapping_shr, checked_wrapping_shr_usize);
2223-
22242016
// `f{16,32,64,128}::to_int_unchecked` proofs
22252017
//
22262018
// Target integer types:

0 commit comments

Comments
 (0)