Skip to content

Commit bbd75f7

Browse files
rajathkotyalrajathkotyal
committed
unchecked multiplication and shift right
1 parent 4858a53 commit bbd75f7

File tree

3 files changed

+237
-1
lines changed

3 files changed

+237
-1
lines changed

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

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -817,6 +817,8 @@ macro_rules! int_impl {
817817
without modifying the original"]
818818
#[inline(always)]
819819
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
820+
#[requires(!self.overflowing_mul(rhs).1)]
821+
#[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
820822
pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
821823
assert_unsafe_precondition!(
822824
check_language_ub,
@@ -1423,8 +1425,10 @@ macro_rules! int_impl {
14231425
#[must_use = "this returns the result of the operation, \
14241426
without modifying the original"]
14251427
#[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
1426-
#[inline(always)]
1428+
#[inline(always)]0
14271429
#[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.
1431+
#[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // ensures result is within range after bit shift
14281432
pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
14291433
assert_unsafe_precondition!(
14301434
check_language_ub,

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

Lines changed: 228 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1703,4 +1703,232 @@ mod verify {
17031703
num1.unchecked_add(num2);
17041704
}
17051705
}
1706+
1707+
// `unchecked_mul` proofs
1708+
//
1709+
// Target types:
1710+
// i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
1711+
//
1712+
// Target Files : src/num/int_macros.rs , src/num/uint_macros.rs
1713+
//
1714+
// Target contracts :
1715+
// #[requires(!self.overflowing_mul(rhs).1)]
1716+
// #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
1717+
//
1718+
// Target function definition:
1719+
// pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self
1720+
1721+
#[kani::proof_for_contract(i8::unchecked_mul)]
1722+
pub fn check_unchecked_mul_i8() {
1723+
let num1: i8 = kani::any::<i8>();
1724+
let num2: i8 = kani::any::<i8>();
1725+
1726+
unsafe {
1727+
num1.unchecked_mul(num2);
1728+
}
1729+
}
1730+
1731+
#[kani::proof_for_contract(i16::unchecked_mul)]
1732+
pub fn check_unchecked_mul_i16() {
1733+
let num1: i16 = kani::any::<i16>();
1734+
let num2: i16 = kani::any::<i16>();
1735+
1736+
unsafe {
1737+
num1.unchecked_mul(num2);
1738+
}
1739+
}
1740+
1741+
#[kani::proof_for_contract(i32::unchecked_mul)]
1742+
pub fn check_unchecked_mul_i32() {
1743+
let num1: i32 = kani::any::<i32>();
1744+
let num2: i32 = kani::any::<i32>();
1745+
1746+
unsafe {
1747+
num1.unchecked_mul(num2);
1748+
}
1749+
}
1750+
1751+
#[kani::proof_for_contract(i64::unchecked_mul)]
1752+
pub fn check_unchecked_mul_i64() {
1753+
let num1: i64 = kani::any::<i64>();
1754+
let num2: i64 = kani::any::<i64>();
1755+
1756+
unsafe {
1757+
num1.unchecked_mul(num2);
1758+
}
1759+
}
1760+
1761+
#[kani::proof_for_contract(i128::unchecked_mul)]
1762+
pub fn check_unchecked_mul_i128() {
1763+
let num1: i128 = kani::any::<i128>();
1764+
let num2: i128 = kani::any::<i128>();
1765+
1766+
unsafe {
1767+
num1.unchecked_mul(num2);
1768+
}
1769+
}
1770+
1771+
#[kani::proof_for_contract(u8::unchecked_mul)]
1772+
pub fn check_unchecked_mul_u8() {
1773+
let num1: u8 = kani::any::<u8>();
1774+
let num2: u8 = kani::any::<u8>();
1775+
1776+
unsafe {
1777+
num1.unchecked_mul(num2);
1778+
}
1779+
}
1780+
1781+
#[kani::proof_for_contract(u16::unchecked_mul)]
1782+
pub fn check_unchecked_mul_u16() {
1783+
let num1: u16 = kani::any::<u16>();
1784+
let num2: u16 = kani::any::<u16>();
1785+
1786+
unsafe {
1787+
num1.unchecked_mul(num2);
1788+
}
1789+
}
1790+
1791+
#[kani::proof_for_contract(u32::unchecked_mul)]
1792+
pub fn check_unchecked_mul_u32() {
1793+
let num1: u32 = kani::any::<u32>();
1794+
let num2: u32 = kani::any::<u32>();
1795+
1796+
unsafe {
1797+
num1.unchecked_mul(num2);
1798+
}
1799+
}
1800+
1801+
#[kani::proof_for_contract(u64::unchecked_mul)]
1802+
pub fn check_unchecked_mul_u64() {
1803+
let num1: u64 = kani::any::<u64>();
1804+
let num2: u64 = kani::any::<u64>();
1805+
1806+
unsafe {
1807+
num1.unchecked_mul(num2);
1808+
}
1809+
}
1810+
1811+
#[kani::proof_for_contract(u128::unchecked_mul)]
1812+
pub fn check_unchecked_mul_u128() {
1813+
let num1: u128 = kani::any::<u128>();
1814+
let num2: u128 = kani::any::<u128>();
1815+
1816+
unsafe {
1817+
num1.unchecked_mul(num2);
1818+
}
1819+
}
1820+
1821+
// `unchecked_shr` proofs
1822+
//
1823+
// Target types:
1824+
// i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total
1825+
//
1826+
// Target Files : src/num/int_macros.rs , src/num/uint_macros.rs
1827+
//
1828+
// Target contracts:
1829+
// #[requires(rhs < <$ActualT>::BITS)]
1830+
// #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
1831+
//
1832+
// Target function:
1833+
// pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self
1834+
1835+
#[kani::proof_for_contract(i8::unchecked_shr)]
1836+
pub fn check_unchecked_shr_i8() {
1837+
let num: i8 = kani::any::<i8>();
1838+
let shift: u32 = kani::any::<u32>() % i8::BITS;
1839+
1840+
unsafe {
1841+
num.unchecked_shr(shift);
1842+
}
1843+
}
1844+
1845+
#[kani::proof_for_contract(i16::unchecked_shr)]
1846+
pub fn check_unchecked_shr_i16() {
1847+
let num: i16 = kani::any::<i16>();
1848+
let shift: u32 = kani::any::<u32>() % i16::BITS;
1849+
1850+
unsafe {
1851+
num.unchecked_shr(shift);
1852+
}
1853+
}
1854+
1855+
#[kani::proof_for_contract(i32::unchecked_shr)]
1856+
pub fn check_unchecked_shr_i32() {
1857+
let num: i32 = kani::any::<i32>();
1858+
let shift: u32 = kani::any::<u32>() % i32::BITS;
1859+
1860+
unsafe {
1861+
num.unchecked_shr(shift);
1862+
}
1863+
}
1864+
1865+
#[kani::proof_for_contract(i64::unchecked_shr)]
1866+
pub fn check_unchecked_shr_i64() {
1867+
let num: i64 = kani::any::<i64>();
1868+
let shift: u32 = kani::any::<u32>() % i64::BITS;
1869+
1870+
unsafe {
1871+
num.unchecked_shr(shift);
1872+
}
1873+
}
1874+
1875+
#[kani::proof_for_contract(i128::unchecked_shr)]
1876+
pub fn check_unchecked_shr_i128() {
1877+
let num: i128 = kani::any::<i128>();
1878+
let shift: u32 = kani::any::<u32>() % i128::BITS;
1879+
1880+
unsafe {
1881+
num.unchecked_shr(shift);
1882+
}
1883+
}
1884+
1885+
#[kani::proof_for_contract(u8::unchecked_shr)]
1886+
pub fn check_unchecked_shr_u8() {
1887+
let num: u8 = kani::any::<u8>();
1888+
let shift: u32 = kani::any::<u32>() % u8::BITS;
1889+
1890+
unsafe {
1891+
num.unchecked_shr(shift);
1892+
}
1893+
}
1894+
1895+
#[kani::proof_for_contract(u16::unchecked_shr)]
1896+
pub fn check_unchecked_shr_u16() {
1897+
let num: u16 = kani::any::<u16>();
1898+
let shift: u32 = kani::any::<u32>() % u16::BITS;
1899+
1900+
unsafe {
1901+
num.unchecked_shr(shift);
1902+
}
1903+
}
1904+
1905+
#[kani::proof_for_contract(u32::unchecked_shr)]
1906+
pub fn check_unchecked_shr_u32() {
1907+
let num: u32 = kani::any::<u32>();
1908+
let shift: u32 = kani::any::<u32>() % u32::BITS;
1909+
1910+
unsafe {
1911+
num.unchecked_shr(shift);
1912+
}
1913+
}
1914+
1915+
#[kani::proof_for_contract(u64::unchecked_shr)]
1916+
pub fn check_unchecked_shr_u64() {
1917+
let num: u64 = kani::any::<u64>();
1918+
let shift: u32 = kani::any::<u32>() % u64::BITS;
1919+
1920+
unsafe {
1921+
num.unchecked_shr(shift);
1922+
}
1923+
}
1924+
1925+
#[kani::proof_for_contract(u128::unchecked_shr)]
1926+
pub fn check_unchecked_shr_u128() {
1927+
let num: u128 = kani::any::<u128>();
1928+
let shift: u32 = kani::any::<u32>() % u128::BITS;
1929+
1930+
unsafe {
1931+
num.unchecked_shr(shift);
1932+
}
1933+
}
17061934
}

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -909,6 +909,8 @@ macro_rules! uint_impl {
909909
without modifying the original"]
910910
#[inline(always)]
911911
#[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
912+
#[requires(!self.overflowing_mul(rhs).1)]
913+
#[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)]
912914
pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self {
913915
assert_unsafe_precondition!(
914916
check_language_ub,
@@ -1614,6 +1616,8 @@ macro_rules! uint_impl {
16141616
#[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")]
16151617
#[inline(always)]
16161618
#[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.
1620+
#[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // ensures result is within range after bit shift
16171621
pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self {
16181622
assert_unsafe_precondition!(
16191623
check_language_ub,

0 commit comments

Comments
 (0)