@@ -1591,9 +1591,6 @@ from_str_radix_size_impl! { i64 isize, u64 usize }
1591
1591
mod verify {
1592
1592
use super :: * ;
1593
1593
1594
- // Verify `unchecked_{add, sub, mul}`
1595
- // However, `unchecked_mul` harnesses have bad performance, so
1596
- // recommend to use generate_unchecked_mul_harness! to set input limits
1597
1594
macro_rules! generate_unchecked_math_harness {
1598
1595
( $type: ty, $method: ident, $harness_name: ident) => {
1599
1596
#[ kani:: proof_for_contract( $type:: $method) ]
@@ -1608,15 +1605,14 @@ mod verify {
1608
1605
}
1609
1606
}
1610
1607
1611
- // Improve unchecked_mul performance for {32, 64, 128}-bit integer types
1612
- // by adding upper and lower limits for inputs
1613
1608
macro_rules! generate_unchecked_mul_harness {
1614
1609
( $type: ty, $method: ident, $harness_name: ident, $min: expr, $max: expr) => {
1615
1610
#[ kani:: proof_for_contract( $type:: $method) ]
1616
1611
pub fn $harness_name( ) {
1617
- let num1: $type = kani:: any:: <$type>( ) ;
1618
- let num2: $type = kani:: any:: <$type>( ) ;
1619
-
1612
+ let num1: $type = kani:: any( ) ;
1613
+ let num2: $type = kani:: any( ) ;
1614
+
1615
+ // Limit the values of num1 and num2 to the specified range for multiplication
1620
1616
kani:: assume( num1 >= $min && num1 <= $max) ;
1621
1617
kani:: assume( num2 >= $min && num2 <= $max) ;
1622
1618
@@ -1626,8 +1622,8 @@ mod verify {
1626
1622
}
1627
1623
}
1628
1624
}
1625
+
1629
1626
1630
- // Verify `unchecked_{shl, shr}`
1631
1627
macro_rules! generate_unchecked_shift_harness {
1632
1628
( $type: ty, $method: ident, $harness_name: ident) => {
1633
1629
#[ kani:: proof_for_contract( $type:: $method) ]
@@ -1641,6 +1637,7 @@ mod verify {
1641
1637
}
1642
1638
}
1643
1639
}
1640
+
1644
1641
1645
1642
macro_rules! generate_unchecked_neg_harness {
1646
1643
( $type: ty, $method: ident, $harness_name: ident) => {
@@ -1702,6 +1699,7 @@ mod verify {
1702
1699
generate_unchecked_mul_harness ! ( u128 , unchecked_mul, checked_unchecked_mul_u128, 0u128 , 1_000_000_000_000_000u128 ) ;
1703
1700
generate_unchecked_mul_harness ! ( usize , unchecked_mul, checked_unchecked_mul_usize, 0usize , 100_000usize ) ;
1704
1701
1702
+
1705
1703
// unchecked_shr proofs
1706
1704
//
1707
1705
// Target types:
@@ -1724,4 +1722,6 @@ mod verify {
1724
1722
generate_unchecked_shift_harness ! ( u64 , unchecked_shr, checked_unchecked_shr_u64) ;
1725
1723
generate_unchecked_shift_harness ! ( u128 , unchecked_shr, checked_unchecked_shr_u128) ;
1726
1724
generate_unchecked_shift_harness ! ( usize , unchecked_shr, checked_unchecked_shr_usize) ;
1725
+ }
1726
+ }
1727
1727
}
0 commit comments