Skip to content

Commit a4edf5f

Browse files
Carolyn Zechtautschnig
Carolyn Zech
and
tautschnig
authored
Run more automatic harnesses (use patterns w/ regex support) (model-checking#397)
Use the support for regexes added in model-checking/kani#4144 to run more automatic harnesses in CI. This brings us from 77 harnesses to 184. 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: Michael Tautschnig <tautschn@amazon.com>
1 parent 45ed9e9 commit a4edf5f

File tree

3 files changed

+60
-265
lines changed

3 files changed

+60
-265
lines changed

‎.github/workflows/kani.yml‎

Lines changed: 60 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -95,18 +95,73 @@ jobs:
9595
# explicitly list all functions (or prefixes thereof) the proofs of which
9696
# are known to pass.
9797
# Notes:
98-
# - We use >::disjoint_bitor (and >::unchecked_disjoint_bitor) as pattern
99-
# as whitespace is not supported, cf.
100-
# https://github.com/model-checking/kani/issues/4046
98+
# - core_arch::x86::__m128d::as_f64x2 is just one example of hundreds of
99+
# core_arch::x86:: functions that are known to verify successfully.
101100
- name: Run Kani Verification
102101
run: |
103102
scripts/run-kani.sh --run autoharness --kani-args \
104-
--include-pattern ">::disjoint_bitor" \
105-
--include-pattern ">::unchecked_disjoint_bitor" \
103+
--include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::disjoint_bitor" \
104+
--include-pattern "<(.+)[[:space:]]as[[:space:]](.+)>::unchecked_disjoint_bitor" \
106105
--include-pattern alloc::__default_lib_allocator:: \
107106
--include-pattern alloc::layout::Layout::from_size_align \
108107
--include-pattern ascii::ascii_char::AsciiChar::from_u8 \
109108
--include-pattern char::convert::from_u32_unchecked \
109+
--include-pattern core_arch::x86::__m128d::as_f64x2 \
110+
--include-pattern "convert::num::<impl.convert::From<num::nonzero::NonZero<" \
111+
--include-pattern "num::<impl.i8>::unchecked_add" \
112+
--include-pattern "num::<impl.i16>::unchecked_add" \
113+
--include-pattern "num::<impl.i32>::unchecked_add" \
114+
--include-pattern "num::<impl.i64>::unchecked_add" \
115+
--include-pattern "num::<impl.i128>::unchecked_add" \
116+
--include-pattern "num::<impl.isize>::unchecked_add" \
117+
--include-pattern "num::<impl.u8>::unchecked_add" \
118+
--include-pattern "num::<impl.u16>::unchecked_add" \
119+
--include-pattern "num::<impl.u32>::unchecked_add" \
120+
--include-pattern "num::<impl.u64>::unchecked_add" \
121+
--include-pattern "num::<impl.u128>::unchecked_add" \
122+
--include-pattern "num::<impl.usize>::unchecked_add" \
123+
--include-pattern "num::<impl.i8>::unchecked_neg" \
124+
--include-pattern "num::<impl.i16>::unchecked_neg" \
125+
--include-pattern "num::<impl.i32>::unchecked_neg" \
126+
--include-pattern "num::<impl.i64>::unchecked_neg" \
127+
--include-pattern "num::<impl.i128>::unchecked_neg" \
128+
--include-pattern "num::<impl.isize>::unchecked_neg" \
129+
--include-pattern "num::<impl.i8>::unchecked_sh" \
130+
--include-pattern "num::<impl.i16>::unchecked_sh" \
131+
--include-pattern "num::<impl.i32>::unchecked_sh" \
132+
--include-pattern "num::<impl.i64>::unchecked_sh" \
133+
--include-pattern "num::<impl.i128>::unchecked_sh" \
134+
--include-pattern "num::<impl.isize>::unchecked_sh" \
135+
--include-pattern "num::<impl.u8>::unchecked_sh" \
136+
--include-pattern "num::<impl.u16>::unchecked_sh" \
137+
--include-pattern "num::<impl.u32>::unchecked_sh" \
138+
--include-pattern "num::<impl.u64>::unchecked_sh" \
139+
--include-pattern "num::<impl.u128>::unchecked_sh" \
140+
--include-pattern "num::<impl.usize>::unchecked_sh" \
141+
--include-pattern "num::<impl.i8>::unchecked_sub" \
142+
--include-pattern "num::<impl.i16>::unchecked_sub" \
143+
--include-pattern "num::<impl.i32>::unchecked_sub" \
144+
--include-pattern "num::<impl.i64>::unchecked_sub" \
145+
--include-pattern "num::<impl.i128>::unchecked_sub" \
146+
--include-pattern "num::<impl.isize>::unchecked_sub" \
147+
--include-pattern "num::<impl.u8>::unchecked_sub" \
148+
--include-pattern "num::<impl.u16>::unchecked_sub" \
149+
--include-pattern "num::<impl.u32>::unchecked_sub" \
150+
--include-pattern "num::<impl.u64>::unchecked_sub" \
151+
--include-pattern "num::<impl.u128>::unchecked_sub" \
152+
--include-pattern "num::<impl.usize>::unchecked_sub" \
153+
--include-pattern "num::<impl.i8>::wrapping_sh" \
154+
--include-pattern "num::<impl.i16>::wrapping_sh" \
155+
--include-pattern "num::<impl.i32>::wrapping_sh" \
156+
--include-pattern "num::<impl.i64>::wrapping_sh" \
157+
--include-pattern "num::<impl.i128>::wrapping_sh" \
158+
--include-pattern "num::<impl.isize>::wrapping_sh" \
159+
--include-pattern "num::<impl.u8>::wrapping_sh" \
160+
--include-pattern "num::<impl.u16>::wrapping_sh" \
161+
--include-pattern "num::<impl.u32>::wrapping_sh" \
162+
--include-pattern "num::<impl.u64>::wrapping_sh" \
163+
--include-pattern "num::<impl.u128>::wrapping_sh" \
164+
--include-pattern "num::<impl.usize>::wrapping_sh" \
110165
--include-pattern "num::nonzero::NonZero::<i8>::count_ones" \
111166
--include-pattern "num::nonzero::NonZero::<i16>::count_ones" \
112167
--include-pattern "num::nonzero::NonZero::<i32>::count_ones" \

‎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 & 192 deletions
Original file line numberDiff line numberDiff line change
@@ -1677,34 +1677,6 @@ mod verify {
16771677
}
16781678
}
16791679

1680-
// Verify `unchecked_{shl, shr}`
1681-
macro_rules! generate_unchecked_shift_harness {
1682-
($type:ty, $method:ident, $harness_name:ident) => {
1683-
#[kani::proof_for_contract($type::$method)]
1684-
pub fn $harness_name() {
1685-
let num1: $type = kani::any::<$type>();
1686-
let num2: u32 = kani::any::<u32>();
1687-
1688-
unsafe {
1689-
num1.$method(num2);
1690-
}
1691-
}
1692-
};
1693-
}
1694-
1695-
macro_rules! generate_unchecked_neg_harness {
1696-
($type:ty, $harness_name:ident) => {
1697-
#[kani::proof_for_contract($type::unchecked_neg)]
1698-
pub fn $harness_name() {
1699-
let num1: $type = kani::any::<$type>();
1700-
1701-
unsafe {
1702-
num1.unchecked_neg();
1703-
}
1704-
}
1705-
};
1706-
}
1707-
17081680
/// A macro to generate Kani proof harnesses for the `carrying_mul` method,
17091681
///
17101682
/// The macro creates multiple harnesses for different ranges of input values,
@@ -1806,47 +1778,6 @@ mod verify {
18061778
}
18071779
}
18081780

1809-
// `unchecked_add` proofs
1810-
//
1811-
// Target types:
1812-
// i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
1813-
//
1814-
// Target contracts:
1815-
// Preconditions: No overflow should occur
1816-
// #[requires(!self.overflowing_add(rhs).1)]
1817-
//
1818-
// Target function:
1819-
// pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
1820-
generate_unchecked_math_harness!(i8, unchecked_add, checked_unchecked_add_i8);
1821-
generate_unchecked_math_harness!(i16, unchecked_add, checked_unchecked_add_i16);
1822-
generate_unchecked_math_harness!(i32, unchecked_add, checked_unchecked_add_i32);
1823-
generate_unchecked_math_harness!(i64, unchecked_add, checked_unchecked_add_i64);
1824-
generate_unchecked_math_harness!(i128, unchecked_add, checked_unchecked_add_i128);
1825-
generate_unchecked_math_harness!(isize, unchecked_add, checked_unchecked_add_isize);
1826-
generate_unchecked_math_harness!(u8, unchecked_add, checked_unchecked_add_u8);
1827-
generate_unchecked_math_harness!(u16, unchecked_add, checked_unchecked_add_u16);
1828-
generate_unchecked_math_harness!(u32, unchecked_add, checked_unchecked_add_u32);
1829-
generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64);
1830-
generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128);
1831-
generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize);
1832-
1833-
// `unchecked_neg` proofs
1834-
//
1835-
// Target types:
1836-
// i{8,16,32,64,128,size} -- 6 types in total
1837-
//
1838-
// Target contracts:
1839-
// #[requires(self != $SelfT::MIN)]
1840-
//
1841-
// Target function:
1842-
// pub const unsafe fn unchecked_neg(self) -> Self
1843-
generate_unchecked_neg_harness!(i8, checked_unchecked_neg_i8);
1844-
generate_unchecked_neg_harness!(i16, checked_unchecked_neg_i16);
1845-
generate_unchecked_neg_harness!(i32, checked_unchecked_neg_i32);
1846-
generate_unchecked_neg_harness!(i64, checked_unchecked_neg_i64);
1847-
generate_unchecked_neg_harness!(i128, checked_unchecked_neg_i128);
1848-
generate_unchecked_neg_harness!(isize, checked_unchecked_neg_isize);
1849-
18501781
// `unchecked_mul` proofs
18511782
//
18521783
// Target types:
@@ -2004,80 +1935,6 @@ mod verify {
20041935
usize::MAX
20051936
);
20061937

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

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

0 commit comments

Comments
 (0)