Skip to content

Commit 0de4670

Browse files
rajathkotyalyew005MWDZlanfeimaYenyun035
authored
Contracts & Harnesses for unchecked_mul , unchecked_sub, unchecked_shl and unchecked_shr (#96)
Towards : issue #59 Parent branch : [c-0011-core-nums-yenyunw-unsafe-ints](https://github.com/rajathkotyal/verify-rust-std/tree/c-0011-core-nums-yenyunw-unsafe-ints ) - Tracking PR #91 --------- Co-authored-by: yew005 <yew005@ucsd.edu> Co-authored-by: MWDZ <jinjunfeng721@gmail.com> Co-authored-by: Lanfei Ma <99311320+lanfeima@users.noreply.github.com> Co-authored-by: Yenyun035 <yenyunw@andrew.cmu.edu>
1 parent ca5334f commit 0de4670

File tree

3 files changed

+186
-2
lines changed

3 files changed

+186
-2
lines changed

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -664,6 +664,7 @@ macro_rules! int_impl {
664664
without modifying the original"]
665665
#[inline(always)]
666666
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
667+
#[requires(!self.overflowing_sub(rhs).1)] // Preconditions: No overflow should occur
667668
pub const unsafe fn unchecked_sub(self, rhs: Self) -> Self {
668669
assert_unsafe_precondition!(
669670
check_language_ub,
@@ -816,6 +817,7 @@ macro_rules! int_impl {
816817
without modifying the original"]
817818
#[inline(always)]
818819
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
820+
#[requires(!self.overflowing_mul(rhs).1)]
819821
pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
820822
assert_unsafe_precondition!(
821823
check_language_ub,
@@ -1298,6 +1300,7 @@ macro_rules! int_impl {
12981300
#[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
12991301
#[inline(always)]
13001302
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
1303+
#[requires(rhs < <$ActualT>::BITS)]
13011304
pub const unsafe fn unchecked_shl(self, rhs: u32) -> Self {
13021305
assert_unsafe_precondition!(
13031306
check_language_ub,
@@ -1424,6 +1427,7 @@ macro_rules! int_impl {
14241427
#[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
14251428
#[inline(always)]
14261429
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
1430+
#[requires(rhs < <$ActualT>::BITS)] // i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior.
14271431
pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
14281432
assert_unsafe_precondition!(
14291433
check_language_ub,

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

Lines changed: 178 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1591,6 +1591,7 @@ from_str_radix_size_impl! { i64 isize, u64 usize }
15911591
mod verify {
15921592
use super::*;
15931593

1594+
// Verify `unchecked_{add, sub, mul}`
15941595
macro_rules! generate_unchecked_math_harness {
15951596
($type:ty, $method:ident, $harness_name:ident) => {
15961597
#[kani::proof_for_contract($type::$method)]
@@ -1605,6 +1606,31 @@ mod verify {
16051606
}
16061607
}
16071608

1609+
// Improve unchecked_mul performance for {32, 64, 128}-bit integer types
1610+
// by adding upper and lower limits for inputs
1611+
macro_rules! generate_unchecked_mul_intervals {
1612+
($type:ty, $method:ident, $($harness_name:ident, $min:expr, $max:expr),+) => {
1613+
$(
1614+
#[kani::proof_for_contract($type::$method)]
1615+
pub fn $harness_name() {
1616+
let num1: $type = kani::any::<$type>();
1617+
let num2: $type = kani::any::<$type>();
1618+
1619+
kani::assume(num1 >= $min && num1 <= $max);
1620+
kani::assume(num2 >= $min && num2 <= $max);
1621+
1622+
// Ensure that multiplication does not overflow
1623+
kani::assume(!num1.overflowing_mul(num2).1);
1624+
1625+
unsafe {
1626+
num1.$method(num2);
1627+
}
1628+
}
1629+
)+
1630+
}
1631+
}
1632+
1633+
// Verify `unchecked_{shl, shr}`
16081634
macro_rules! generate_unchecked_shift_harness {
16091635
($type:ty, $method:ident, $harness_name:ident) => {
16101636
#[kani::proof_for_contract($type::$method)]
@@ -1635,10 +1661,11 @@ mod verify {
16351661
// `unchecked_add` proofs
16361662
//
16371663
// Target types:
1638-
// i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total
1664+
// i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
16391665
//
16401666
// Target contracts:
1641-
// #[requires(!self.overflowing_add(rhs).1)]
1667+
//#[requires(!self.overflowing_sub(rhs).1)] // Preconditions: No overflow should occur
1668+
//#[ensures(|ret| *ret >= Self::MIN && *ret <= Self::MAX)] // Postconditions: Result must be within valid bounds
16421669
//
16431670
// Target function:
16441671
// pub const unsafe fn unchecked_add(self, rhs: Self) -> Self
@@ -1654,4 +1681,153 @@ mod verify {
16541681
generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64);
16551682
generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128);
16561683
generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize);
1684+
1685+
// unchecked_mul proofs
1686+
//
1687+
// Target types:
1688+
// i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 36 types in total
1689+
//
1690+
// Target contracts:
1691+
// #[requires(!self.overflowing_mul(rhs).1)]
1692+
//
1693+
// Target function:
1694+
// pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self
1695+
// exponential state spaces for 32,64 and 128, hence provided limited range for verification.
1696+
generate_unchecked_math_harness!(i8, unchecked_mul, checked_unchecked_mul_i8);
1697+
generate_unchecked_math_harness!(i16, unchecked_mul, checked_unchecked_mul_i16);
1698+
1699+
// ====================== i32 Harnesses ======================
1700+
generate_unchecked_mul_intervals!(i32, unchecked_mul,
1701+
unchecked_mul_i32_small, -10i32, 10i32,
1702+
unchecked_mul_i32_large_pos, i32::MAX - 1000i32, i32::MAX,
1703+
unchecked_mul_i32_large_neg, i32::MIN, i32::MIN + 1000i32,
1704+
unchecked_mul_i32_edge_pos, i32::MAX / 2, i32::MAX,
1705+
unchecked_mul_i32_edge_neg, i32::MIN, i32::MIN / 2
1706+
);
1707+
// ====================== i64 Harnesses ======================
1708+
generate_unchecked_mul_intervals!(i64, unchecked_mul,
1709+
unchecked_mul_i64_small, -10i64, 10i64,
1710+
unchecked_mul_i64_large_pos, i64::MAX - 1000i64, i64::MAX,
1711+
unchecked_mul_i64_large_neg, i64::MIN, i64::MIN + 1000i64,
1712+
unchecked_mul_i64_edge_pos, i64::MAX / 2, i64::MAX,
1713+
unchecked_mul_i64_edge_neg, i64::MIN, i64::MIN / 2
1714+
);
1715+
// ====================== i128 Harnesses ======================
1716+
generate_unchecked_mul_intervals!(i128, unchecked_mul,
1717+
unchecked_mul_i128_small, -10i128, 10i128,
1718+
unchecked_mul_i128_large_pos, i128::MAX - 1000i128, i128::MAX,
1719+
unchecked_mul_i128_large_neg, i128::MIN, i128::MIN + 1000i128,
1720+
unchecked_mul_i128_edge_pos, i128::MAX / 2, i128::MAX,
1721+
unchecked_mul_i128_edge_neg, i128::MIN, i128::MIN / 2
1722+
);
1723+
// ====================== isize Harnesses ======================
1724+
generate_unchecked_mul_intervals!(isize, unchecked_mul,
1725+
unchecked_mul_isize_small, -10isize, 10isize,
1726+
unchecked_mul_isize_large_pos, isize::MAX - 1000isize, isize::MAX,
1727+
unchecked_mul_isize_large_neg, isize::MIN, isize::MIN + 1000isize,
1728+
unchecked_mul_isize_edge_pos, isize::MAX / 2, isize::MAX,
1729+
unchecked_mul_isize_edge_neg, isize::MIN, isize::MIN / 2
1730+
);
1731+
1732+
generate_unchecked_math_harness!(u8, unchecked_mul, checked_unchecked_mul_u8);
1733+
generate_unchecked_math_harness!(u16, unchecked_mul, checked_unchecked_mul_u16);
1734+
1735+
// ====================== u32 Harnesses ======================
1736+
generate_unchecked_mul_intervals!(u32, unchecked_mul,
1737+
unchecked_mul_u32_small, 0u32, 10u32,
1738+
unchecked_mul_u32_large, u32::MAX - 1000u32, u32::MAX,
1739+
unchecked_mul_u32_edge, u32::MAX / 2, u32::MAX
1740+
);
1741+
// ====================== u64 Harnesses ======================
1742+
generate_unchecked_mul_intervals!(u64, unchecked_mul,
1743+
unchecked_mul_u64_small, 0u64, 10u64,
1744+
unchecked_mul_u64_large, u64::MAX - 1000u64, u64::MAX,
1745+
unchecked_mul_u64_edge, u64::MAX / 2, u64::MAX
1746+
);
1747+
// ====================== u128 Harnesses ======================
1748+
generate_unchecked_mul_intervals!(u128, unchecked_mul,
1749+
unchecked_mul_u128_small, 0u128, 10u128,
1750+
unchecked_mul_u128_large, u128::MAX - 1000u128, u128::MAX,
1751+
unchecked_mul_u128_edge, u128::MAX / 2, u128::MAX
1752+
);
1753+
// ====================== usize Harnesses ======================
1754+
generate_unchecked_mul_intervals!(usize, unchecked_mul,
1755+
unchecked_mul_usize_small, 0usize, 10usize,
1756+
unchecked_mul_usize_large, usize::MAX - 1000usize, usize::MAX,
1757+
unchecked_mul_usize_edge, usize::MAX / 2, usize::MAX
1758+
);
1759+
1760+
// unchecked_shr proofs
1761+
//
1762+
// Target types:
1763+
// i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total
1764+
//
1765+
// Target contracts:
1766+
// #[requires(rhs < <$ActualT>::BITS)]
1767+
//
1768+
// Target function:
1769+
// pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self
1770+
generate_unchecked_shift_harness!(i8, unchecked_shr, checked_unchecked_shr_i8);
1771+
generate_unchecked_shift_harness!(i16, unchecked_shr, checked_unchecked_shr_i16);
1772+
generate_unchecked_shift_harness!(i32, unchecked_shr, checked_unchecked_shr_i32);
1773+
generate_unchecked_shift_harness!(i64, unchecked_shr, checked_unchecked_shr_i64);
1774+
generate_unchecked_shift_harness!(i128, unchecked_shr, checked_unchecked_shr_i128);
1775+
generate_unchecked_shift_harness!(isize, unchecked_shr, checked_unchecked_shr_isize);
1776+
generate_unchecked_shift_harness!(u8, unchecked_shr, checked_unchecked_shr_u8);
1777+
generate_unchecked_shift_harness!(u16, unchecked_shr, checked_unchecked_shr_u16);
1778+
generate_unchecked_shift_harness!(u32, unchecked_shr, checked_unchecked_shr_u32);
1779+
generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64);
1780+
generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128);
1781+
generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize);
1782+
1783+
// `unchecked_shl` proofs
1784+
//
1785+
// Target types:
1786+
// i{8,16,32,64,128} and u{8,16,32,64,128} -- 12 types in total
1787+
//
1788+
// Target contracts:
1789+
// #[requires(shift < Self::BITS)]
1790+
// #[ensures(|ret| *ret == self << shift)]
1791+
//
1792+
// Target function:
1793+
// pub const unsafe fn unchecked_shl(self, shift: u32) -> Self
1794+
//
1795+
// This function performs an unchecked bitwise left shift operation.
1796+
generate_unchecked_shift_harness!(i8, unchecked_shl, checked_unchecked_shl_i8);
1797+
generate_unchecked_shift_harness!(i16, unchecked_shl, checked_unchecked_shl_i16);
1798+
generate_unchecked_shift_harness!(i32, unchecked_shl, checked_unchecked_shl_i32);
1799+
generate_unchecked_shift_harness!(i64, unchecked_shl, checked_unchecked_shl_i64);
1800+
generate_unchecked_shift_harness!(i128, unchecked_shl, checked_unchecked_shl_i128);
1801+
generate_unchecked_shift_harness!(isize, unchecked_shl, checked_unchecked_shl_isize);
1802+
generate_unchecked_shift_harness!(u8, unchecked_shl, checked_unchecked_shl_u8);
1803+
generate_unchecked_shift_harness!(u16, unchecked_shl, checked_unchecked_shl_u16);
1804+
generate_unchecked_shift_harness!(u32, unchecked_shl, checked_unchecked_shl_u32);
1805+
generate_unchecked_shift_harness!(u64, unchecked_shl, checked_unchecked_shl_u64);
1806+
generate_unchecked_shift_harness!(u128, unchecked_shl, checked_unchecked_shl_u128);
1807+
generate_unchecked_shift_harness!(usize, unchecked_shl, checked_unchecked_shl_usize);
1808+
1809+
// `unchecked_sub` proofs
1810+
//
1811+
// Target types:
1812+
// i{8,16,32,64,128} and u{8,16,32,64,128} -- 12 types in total
1813+
//
1814+
// Target contracts:
1815+
// #[requires(!self.overflowing_sub(rhs).1)] // Preconditions: No overflow should occur
1816+
//
1817+
// Target function:
1818+
// pub const unsafe fn unchecked_sub(self, rhs: Self) -> Self
1819+
//
1820+
// This function performs an unchecked subtraction operation.
1821+
generate_unchecked_math_harness!(i8, unchecked_sub, checked_unchecked_sub_i8);
1822+
generate_unchecked_math_harness!(i16, unchecked_sub, checked_unchecked_sub_i16);
1823+
generate_unchecked_math_harness!(i32, unchecked_sub, checked_unchecked_sub_i32);
1824+
generate_unchecked_math_harness!(i64, unchecked_sub, checked_unchecked_sub_i64);
1825+
generate_unchecked_math_harness!(i128, unchecked_sub, checked_unchecked_sub_i128);
1826+
generate_unchecked_math_harness!(isize, unchecked_sub, checked_unchecked_sub_isize);
1827+
generate_unchecked_math_harness!(u8, unchecked_sub, checked_unchecked_sub_u8);
1828+
generate_unchecked_math_harness!(u16, unchecked_sub, checked_unchecked_sub_u16);
1829+
generate_unchecked_math_harness!(u32, unchecked_sub, checked_unchecked_sub_u32);
1830+
generate_unchecked_math_harness!(u64, unchecked_sub, checked_unchecked_sub_u64);
1831+
generate_unchecked_math_harness!(u128, unchecked_sub, checked_unchecked_sub_u128);
1832+
generate_unchecked_math_harness!(usize, unchecked_sub, checked_unchecked_sub_usize);
16571833
}

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -751,6 +751,7 @@ macro_rules! uint_impl {
751751
without modifying the original"]
752752
#[inline(always)]
753753
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
754+
#[requires(!self.overflowing_sub(rhs).1)] // Preconditions: No overflow should occur
754755
pub const unsafe fn unchecked_sub(self, rhs: Self) -> Self {
755756
assert_unsafe_precondition!(
756757
check_language_ub,
@@ -908,6 +909,7 @@ macro_rules! uint_impl {
908909
without modifying the original"]
909910
#[inline(always)]
910911
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
912+
#[requires(!self.overflowing_mul(rhs).1)]
911913
pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
912914
assert_unsafe_precondition!(
913915
check_language_ub,
@@ -1487,6 +1489,7 @@ macro_rules! uint_impl {
14871489
#[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
14881490
#[inline(always)]
14891491
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
1492+
#[requires(rhs < <$ActualT>::BITS)]
14901493
pub const unsafe fn unchecked_shl(self, rhs: u32) -> Self {
14911494
assert_unsafe_precondition!(
14921495
check_language_ub,
@@ -1613,6 +1616,7 @@ macro_rules! uint_impl {
16131616
#[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
16141617
#[inline(always)]
16151618
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
1619+
#[requires(rhs < <$ActualT>::BITS)]// i.e. requires the right hand side of the shift (rhs) to be less than the number of bits in the type. This prevents undefined behavior.
16161620
pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
16171621
assert_unsafe_precondition!(
16181622
check_language_ub,

0 commit comments

Comments
 (0)