From 1ae4c6d4958e43bda11562e832d9a28b930ba7a6 Mon Sep 17 00:00:00 2001 From: yew005 Date: Tue, 10 Sep 2024 17:11:15 -0700 Subject: [PATCH 01/25] Add Kani proofs of unchecked_add for all integer types --- .../core/tests/num/kani-proofs/i128-proofs.rs | 23 +++++++++++++++++++ .../core/tests/num/kani-proofs/i16-proofs.rs | 23 +++++++++++++++++++ .../core/tests/num/kani-proofs/i32-proofs.rs | 23 +++++++++++++++++++ .../core/tests/num/kani-proofs/i64-proofs.rs | 23 +++++++++++++++++++ .../core/tests/num/kani-proofs/i8-proofs.rs | 23 +++++++++++++++++++ .../core/tests/num/kani-proofs/u128-proofs.rs | 21 +++++++++++++++++ .../core/tests/num/kani-proofs/u16-proofs.rs | 21 +++++++++++++++++ .../core/tests/num/kani-proofs/u32-proofs.rs | 21 +++++++++++++++++ .../core/tests/num/kani-proofs/u64-proofs.rs | 21 +++++++++++++++++ .../core/tests/num/kani-proofs/u8-proofs.rs | 21 +++++++++++++++++ 10 files changed, 220 insertions(+) create mode 100644 library/core/tests/num/kani-proofs/i128-proofs.rs create mode 100644 library/core/tests/num/kani-proofs/i16-proofs.rs create mode 100644 library/core/tests/num/kani-proofs/i32-proofs.rs create mode 100644 library/core/tests/num/kani-proofs/i64-proofs.rs create mode 100644 library/core/tests/num/kani-proofs/i8-proofs.rs create mode 100644 library/core/tests/num/kani-proofs/u128-proofs.rs create mode 100644 library/core/tests/num/kani-proofs/u16-proofs.rs create mode 100644 library/core/tests/num/kani-proofs/u32-proofs.rs create mode 100644 library/core/tests/num/kani-proofs/u64-proofs.rs create mode 100644 library/core/tests/num/kani-proofs/u8-proofs.rs diff --git a/library/core/tests/num/kani-proofs/i128-proofs.rs b/library/core/tests/num/kani-proofs/i128-proofs.rs new file mode 100644 index 0000000000000..279d8f26ff947 --- /dev/null +++ b/library/core/tests/num/kani-proofs/i128-proofs.rs @@ -0,0 +1,23 @@ +#[cfg(kani)] +mod verification { + // use super::*; + + #[kani::proof] + fn verify_i128_unchecked_add() { + let num1: i128 = kani::any::(); + let num2: i128 = kani::any::(); + + // Safety preconditions: + // - Positive number addition won't overflow + // - Negative number addition won't underflow + // Addition of two integers with different signs never overflows + // Undefined behavior occurs when overflow or underflow happens + kani::assume((num1 > 0 && num2 > 0 && num1 < i128::MAX - num2) + || (num1 < 0 && num2 < 0 && num1 > i128::MIN - num2)); + + unsafe { + let result = num1.unchecked_add(num2); + assert_eq!(Some(result), num1.checked_add(num2)); + } + } +} \ No newline at end of file diff --git a/library/core/tests/num/kani-proofs/i16-proofs.rs b/library/core/tests/num/kani-proofs/i16-proofs.rs new file mode 100644 index 0000000000000..d946148d78976 --- /dev/null +++ b/library/core/tests/num/kani-proofs/i16-proofs.rs @@ -0,0 +1,23 @@ +#[cfg(kani)] +mod verification { + // use super::*; + + #[kani::proof] + fn verify_i16_unchecked_add() { + let num1: i16 = kani::any::(); + let num2: i16 = kani::any::(); + + // Safety preconditions: + // - Positive number addition won't overflow + // - Negative number addition won't underflow + // Addition of two integers with different signs never overflows + // Undefined behavior occurs when overflow or underflow happens + kani::assume((num1 > 0 && num2 > 0 && num1 < i16::MAX - num2) + || (num1 < 0 && num2 < 0 && num1 > i16::MIN - num2)); + + unsafe { + let result = num1.unchecked_add(num2); + assert_eq!(Some(result), num1.checked_add(num2)); + } + } +} \ No newline at end of file diff --git a/library/core/tests/num/kani-proofs/i32-proofs.rs b/library/core/tests/num/kani-proofs/i32-proofs.rs new file mode 100644 index 0000000000000..bb2d542dbc38f --- /dev/null +++ b/library/core/tests/num/kani-proofs/i32-proofs.rs @@ -0,0 +1,23 @@ +#[cfg(kani)] +mod verification { + // use super::*; + + #[kani::proof] + fn verify_i32_unchecked_add() { + let num1: i32 = kani::any::(); + let num2: i32 = kani::any::(); + + // Safety preconditions: + // - Positive number addition won't overflow + // - Negative number addition won't underflow + // Addition of two integers with different signs never overflows + // Undefined behavior occurs when overflow or underflow happens + kani::assume((num1 > 0 && num2 > 0 && num1 < i32::MAX - num2) + || (num1 < 0 && num2 < 0 && num1 > i32::MIN - num2)); + + unsafe { + let result = num1.unchecked_add(num2); + assert_eq!(Some(result), num1.checked_add(num2)); + } + } +} \ No newline at end of file diff --git a/library/core/tests/num/kani-proofs/i64-proofs.rs b/library/core/tests/num/kani-proofs/i64-proofs.rs new file mode 100644 index 0000000000000..822bac06eb733 --- /dev/null +++ b/library/core/tests/num/kani-proofs/i64-proofs.rs @@ -0,0 +1,23 @@ +#[cfg(kani)] +mod verification { + // use super::*; + + #[kani::proof] + fn verify_i64_unchecked_add() { + let num1: i64 = kani::any::(); + let num2: i64 = kani::any::(); + + // Safety preconditions: + // - Positive number addition won't overflow + // - Negative number addition won't underflow + // Addition of two integers with different signs never overflows + // Undefined behavior occurs when overflow or underflow happens + kani::assume((num1 > 0 && num2 > 0 && num1 < i64::MAX - num2) + || (num1 < 0 && num2 < 0 && num1 > i64::MIN - num2)); + + unsafe { + let result = num1.unchecked_add(num2); + assert_eq!(Some(result), num1.checked_add(num2)); + } + } +} \ No newline at end of file diff --git a/library/core/tests/num/kani-proofs/i8-proofs.rs b/library/core/tests/num/kani-proofs/i8-proofs.rs new file mode 100644 index 0000000000000..edc3522f42be3 --- /dev/null +++ b/library/core/tests/num/kani-proofs/i8-proofs.rs @@ -0,0 +1,23 @@ +#[cfg(kani)] +mod verification { + // use super::*; + + #[kani::proof] + fn verify_i8_unchecked_add() { + let num1: i8 = kani::any::(); + let num2: i8 = kani::any::(); + + // Safety preconditions: + // - Positive number addition won't overflow + // - Negative number addition won't underflow + // Addition of two integers with different signs never overflows + // Undefined behavior occurs when overflow or underflow happens + kani::assume((num1 > 0 && num2 > 0 && num1 < i8::MAX - num2) + || (num1 < 0 && num2 < 0 && num1 > i8::MIN - num2)); + + unsafe { + let result = num1.unchecked_add(num2); + assert_eq!(Some(result), num1.checked_add(num2)); + } + } +} \ No newline at end of file diff --git a/library/core/tests/num/kani-proofs/u128-proofs.rs b/library/core/tests/num/kani-proofs/u128-proofs.rs new file mode 100644 index 0000000000000..98d781ec024b5 --- /dev/null +++ b/library/core/tests/num/kani-proofs/u128-proofs.rs @@ -0,0 +1,21 @@ +#[cfg(kani)] +mod verification { + // use super::*; + + #[kani::proof] + fn verify_u128_unchecked_add() { + let num1: u128 = kani::any::(); + let num2: u128 = kani::any::(); + + // Safety preconditions: + // - Addition won't overflow + // Unsigned integers are always positive, so underflow won't happen + // Undefined behavior occurs when overflow happens + kani::assume(num1 < u128::MAX - num2); + + unsafe { + let result = num1.unchecked_add(num2); + assert_eq!(Some(result), num1.checked_add(num2)); + } + } +} \ No newline at end of file diff --git a/library/core/tests/num/kani-proofs/u16-proofs.rs b/library/core/tests/num/kani-proofs/u16-proofs.rs new file mode 100644 index 0000000000000..9dfff81d1abbb --- /dev/null +++ b/library/core/tests/num/kani-proofs/u16-proofs.rs @@ -0,0 +1,21 @@ +#[cfg(kani)] +mod verification { + // use super::*; + + #[kani::proof] + fn verify_u16_unchecked_add() { + let num1: u16 = kani::any::(); + let num2: u16 = kani::any::(); + + // Safety preconditions: + // - Addition won't overflow + // Unsigned integers are always positive, so underflow won't happen + // Undefined behavior occurs when overflow happens + kani::assume(num1 < u16::MAX - num2); + + unsafe { + let result = num1.unchecked_add(num2); + assert_eq!(Some(result), num1.checked_add(num2)); + } + } +} \ No newline at end of file diff --git a/library/core/tests/num/kani-proofs/u32-proofs.rs b/library/core/tests/num/kani-proofs/u32-proofs.rs new file mode 100644 index 0000000000000..0d13bdcd2dce0 --- /dev/null +++ b/library/core/tests/num/kani-proofs/u32-proofs.rs @@ -0,0 +1,21 @@ +#[cfg(kani)] +mod verification { + // use super::*; + + #[kani::proof] + fn verify_u32_unchecked_add() { + let num1: u32 = kani::any::(); + let num2: u32 = kani::any::(); + + // Safety preconditions: + // - Addition won't overflow + // Unsigned integers are always positive, so underflow won't happen + // Undefined behavior occurs when overflow happens + kani::assume(num1 < u32::MAX - num2); + + unsafe { + let result = num1.unchecked_add(num2); + assert_eq!(Some(result), num1.checked_add(num2)); + } + } +} \ No newline at end of file diff --git a/library/core/tests/num/kani-proofs/u64-proofs.rs b/library/core/tests/num/kani-proofs/u64-proofs.rs new file mode 100644 index 0000000000000..405468c96e0ba --- /dev/null +++ b/library/core/tests/num/kani-proofs/u64-proofs.rs @@ -0,0 +1,21 @@ +#[cfg(kani)] +mod verification { + // use super::*; + + #[kani::proof] + fn verify_u64_unchecked_add() { + let num1: u64 = kani::any::(); + let num2: u64 = kani::any::(); + + // Safety preconditions: + // - Addition won't overflow + // Unsigned integers are always positive, so underflow won't happen + // Undefined behavior occurs when overflow happens + kani::assume(num1 < u64::MAX - num2); + + unsafe { + let result = num1.unchecked_add(num2); + assert_eq!(Some(result), num1.checked_add(num2)); + } + } +} \ No newline at end of file diff --git a/library/core/tests/num/kani-proofs/u8-proofs.rs b/library/core/tests/num/kani-proofs/u8-proofs.rs new file mode 100644 index 0000000000000..89826fc292c4b --- /dev/null +++ b/library/core/tests/num/kani-proofs/u8-proofs.rs @@ -0,0 +1,21 @@ +#[cfg(kani)] +mod verification { + // use super::*; + + #[kani::proof] + fn verify_u8_unchecked_add() { + let num1: u8 = kani::any::(); + let num2: u8 = kani::any::(); + + // Safety preconditions: + // - Addition won't overflow + // Unsigned integers are always positive, so underflow won't happen + // Undefined behavior occurs when overflow happens + kani::assume(num1 < u8::MAX - num2); + + unsafe { + let result = num1.unchecked_add(num2); + assert_eq!(Some(result), num1.checked_add(num2)); + } + } +} \ No newline at end of file From b553678c11aec836a9cc0aba1db0cc473a70fc03 Mon Sep 17 00:00:00 2001 From: yew005 Date: Tue, 10 Sep 2024 21:07:15 -0700 Subject: [PATCH 02/25] Format proof files & Add verification function templates --- .../core/tests/num/kani-proofs/i128-proofs.rs | 55 ++++++++++++++----- .../core/tests/num/kani-proofs/i16-proofs.rs | 55 ++++++++++++++----- .../core/tests/num/kani-proofs/i32-proofs.rs | 55 ++++++++++++++----- .../core/tests/num/kani-proofs/i64-proofs.rs | 55 ++++++++++++++----- .../core/tests/num/kani-proofs/i8-proofs.rs | 55 ++++++++++++++----- .../core/tests/num/kani-proofs/u128-proofs.rs | 49 +++++++++++++---- .../core/tests/num/kani-proofs/u16-proofs.rs | 49 +++++++++++++---- .../core/tests/num/kani-proofs/u32-proofs.rs | 49 +++++++++++++---- .../core/tests/num/kani-proofs/u64-proofs.rs | 49 +++++++++++++---- .../core/tests/num/kani-proofs/u8-proofs.rs | 49 +++++++++++++---- 10 files changed, 390 insertions(+), 130 deletions(-) diff --git a/library/core/tests/num/kani-proofs/i128-proofs.rs b/library/core/tests/num/kani-proofs/i128-proofs.rs index 279d8f26ff947..4ac03ec8714fe 100644 --- a/library/core/tests/num/kani-proofs/i128-proofs.rs +++ b/library/core/tests/num/kani-proofs/i128-proofs.rs @@ -1,23 +1,50 @@ #[cfg(kani)] mod verification { - // use super::*; + // use super::*; - #[kani::proof] - fn verify_i128_unchecked_add() { - let num1: i128 = kani::any::(); - let num2: i128 = kani::any::(); + #[kani::proof] + fn verify_i128_unchecked_add() { + let num1: i128 = kani::any::(); + let num2: i128 = kani::any::(); - // Safety preconditions: - // - Positive number addition won't overflow - // - Negative number addition won't underflow - // Addition of two integers with different signs never overflows - // Undefined behavior occurs when overflow or underflow happens - kani::assume((num1 > 0 && num2 > 0 && num1 < i128::MAX - num2) - || (num1 < 0 && num2 < 0 && num1 > i128::MIN - num2)); + // Safety preconditions: + // - Positive number addition won't overflow + // - Negative number addition won't underflow + // Addition of two integers with different signs never overflows + // Undefined behavior occurs when overflow or underflow happens + kani::assume( + (num1 > 0 && num2 > 0 && num1 < i128::MAX - num2) + || (num1 < 0 && num2 < 0 && num1 > i128::MIN - num2), + ); unsafe { let result = num1.unchecked_add(num2); assert_eq!(Some(result), num1.checked_add(num2)); } - } -} \ No newline at end of file + } + + #[kani::proof] + fn verify_i128_unchecked_sub() { + // TODO + } + + #[kani::proof] + fn verify_i128_unchecked_mul() { + // TODO + } + + #[kani::proof] + fn verify_i128_unchecked_shl() { + // TODO + } + + #[kani::proof] + fn verify_i128_unchecked_shr() { + // TODO + } + + #[kani::proof] + fn verify_i128_unchecked_neg() { + // TODO + } +} diff --git a/library/core/tests/num/kani-proofs/i16-proofs.rs b/library/core/tests/num/kani-proofs/i16-proofs.rs index d946148d78976..f57591f6b8e07 100644 --- a/library/core/tests/num/kani-proofs/i16-proofs.rs +++ b/library/core/tests/num/kani-proofs/i16-proofs.rs @@ -1,23 +1,50 @@ #[cfg(kani)] mod verification { - // use super::*; + // use super::*; - #[kani::proof] - fn verify_i16_unchecked_add() { - let num1: i16 = kani::any::(); - let num2: i16 = kani::any::(); + #[kani::proof] + fn verify_i16_unchecked_add() { + let num1: i16 = kani::any::(); + let num2: i16 = kani::any::(); - // Safety preconditions: - // - Positive number addition won't overflow - // - Negative number addition won't underflow - // Addition of two integers with different signs never overflows - // Undefined behavior occurs when overflow or underflow happens - kani::assume((num1 > 0 && num2 > 0 && num1 < i16::MAX - num2) - || (num1 < 0 && num2 < 0 && num1 > i16::MIN - num2)); + // Safety preconditions: + // - Positive number addition won't overflow + // - Negative number addition won't underflow + // Addition of two integers with different signs never overflows + // Undefined behavior occurs when overflow or underflow happens + kani::assume( + (num1 > 0 && num2 > 0 && num1 < i16::MAX - num2) + || (num1 < 0 && num2 < 0 && num1 > i16::MIN - num2), + ); unsafe { let result = num1.unchecked_add(num2); assert_eq!(Some(result), num1.checked_add(num2)); } - } -} \ No newline at end of file + } + + #[kani::proof] + fn verify_i16_unchecked_sub() { + // TODO + } + + #[kani::proof] + fn verify_i16_unchecked_mul() { + // TODO + } + + #[kani::proof] + fn verify_i16_unchecked_shl() { + // TODO + } + + #[kani::proof] + fn verify_i16_unchecked_shr() { + // TODO + } + + #[kani::proof] + fn verify_i16_unchecked_neg() { + // TODO + } +} diff --git a/library/core/tests/num/kani-proofs/i32-proofs.rs b/library/core/tests/num/kani-proofs/i32-proofs.rs index bb2d542dbc38f..0c8cca6a8d9c0 100644 --- a/library/core/tests/num/kani-proofs/i32-proofs.rs +++ b/library/core/tests/num/kani-proofs/i32-proofs.rs @@ -1,23 +1,50 @@ #[cfg(kani)] mod verification { - // use super::*; + // use super::*; - #[kani::proof] - fn verify_i32_unchecked_add() { - let num1: i32 = kani::any::(); - let num2: i32 = kani::any::(); + #[kani::proof] + fn verify_i32_unchecked_add() { + let num1: i32 = kani::any::(); + let num2: i32 = kani::any::(); - // Safety preconditions: - // - Positive number addition won't overflow - // - Negative number addition won't underflow - // Addition of two integers with different signs never overflows - // Undefined behavior occurs when overflow or underflow happens - kani::assume((num1 > 0 && num2 > 0 && num1 < i32::MAX - num2) - || (num1 < 0 && num2 < 0 && num1 > i32::MIN - num2)); + // Safety preconditions: + // - Positive number addition won't overflow + // - Negative number addition won't underflow + // Addition of two integers with different signs never overflows + // Undefined behavior occurs when overflow or underflow happens + kani::assume( + (num1 > 0 && num2 > 0 && num1 < i32::MAX - num2) + || (num1 < 0 && num2 < 0 && num1 > i32::MIN - num2), + ); unsafe { let result = num1.unchecked_add(num2); assert_eq!(Some(result), num1.checked_add(num2)); } - } -} \ No newline at end of file + } + + #[kani::proof] + fn verify_i32_unchecked_sub() { + // TODO + } + + #[kani::proof] + fn verify_i32_unchecked_mul() { + // TODO + } + + #[kani::proof] + fn verify_i32_unchecked_shl() { + // TODO + } + + #[kani::proof] + fn verify_i32_unchecked_shr() { + // TODO + } + + #[kani::proof] + fn verify_i32_unchecked_neg() { + // TODO + } +} diff --git a/library/core/tests/num/kani-proofs/i64-proofs.rs b/library/core/tests/num/kani-proofs/i64-proofs.rs index 822bac06eb733..658956c110dd8 100644 --- a/library/core/tests/num/kani-proofs/i64-proofs.rs +++ b/library/core/tests/num/kani-proofs/i64-proofs.rs @@ -1,23 +1,50 @@ #[cfg(kani)] mod verification { - // use super::*; + // use super::*; - #[kani::proof] - fn verify_i64_unchecked_add() { - let num1: i64 = kani::any::(); - let num2: i64 = kani::any::(); + #[kani::proof] + fn verify_i64_unchecked_add() { + let num1: i64 = kani::any::(); + let num2: i64 = kani::any::(); - // Safety preconditions: - // - Positive number addition won't overflow - // - Negative number addition won't underflow - // Addition of two integers with different signs never overflows - // Undefined behavior occurs when overflow or underflow happens - kani::assume((num1 > 0 && num2 > 0 && num1 < i64::MAX - num2) - || (num1 < 0 && num2 < 0 && num1 > i64::MIN - num2)); + // Safety preconditions: + // - Positive number addition won't overflow + // - Negative number addition won't underflow + // Addition of two integers with different signs never overflows + // Undefined behavior occurs when overflow or underflow happens + kani::assume( + (num1 > 0 && num2 > 0 && num1 < i64::MAX - num2) + || (num1 < 0 && num2 < 0 && num1 > i64::MIN - num2), + ); unsafe { let result = num1.unchecked_add(num2); assert_eq!(Some(result), num1.checked_add(num2)); } - } -} \ No newline at end of file + } + + #[kani::proof] + fn verify_i64_unchecked_sub() { + // TODO + } + + #[kani::proof] + fn verify_i64_unchecked_mul() { + // TODO + } + + #[kani::proof] + fn verify_i64_unchecked_shl() { + // TODO + } + + #[kani::proof] + fn verify_i64_unchecked_shr() { + // TODO + } + + #[kani::proof] + fn verify_i64_unchecked_neg() { + // TODO + } +} diff --git a/library/core/tests/num/kani-proofs/i8-proofs.rs b/library/core/tests/num/kani-proofs/i8-proofs.rs index edc3522f42be3..932407510ffda 100644 --- a/library/core/tests/num/kani-proofs/i8-proofs.rs +++ b/library/core/tests/num/kani-proofs/i8-proofs.rs @@ -1,23 +1,50 @@ #[cfg(kani)] mod verification { - // use super::*; + // use super::*; - #[kani::proof] - fn verify_i8_unchecked_add() { - let num1: i8 = kani::any::(); - let num2: i8 = kani::any::(); + #[kani::proof] + fn verify_i8_unchecked_add() { + let num1: i8 = kani::any::(); + let num2: i8 = kani::any::(); - // Safety preconditions: - // - Positive number addition won't overflow - // - Negative number addition won't underflow - // Addition of two integers with different signs never overflows - // Undefined behavior occurs when overflow or underflow happens - kani::assume((num1 > 0 && num2 > 0 && num1 < i8::MAX - num2) - || (num1 < 0 && num2 < 0 && num1 > i8::MIN - num2)); + // Safety preconditions: + // - Positive number addition won't overflow + // - Negative number addition won't underflow + // Addition of two integers with different signs never overflows + // Undefined behavior occurs when overflow or underflow happens + kani::assume( + (num1 > 0 && num2 > 0 && num1 < i8::MAX - num2) + || (num1 < 0 && num2 < 0 && num1 > i8::MIN - num2), + ); unsafe { let result = num1.unchecked_add(num2); assert_eq!(Some(result), num1.checked_add(num2)); } - } -} \ No newline at end of file + } + + #[kani::proof] + fn verify_i8_unchecked_sub() { + // TODO + } + + #[kani::proof] + fn verify_i8_unchecked_mul() { + // TODO + } + + #[kani::proof] + fn verify_i8_unchecked_shl() { + // TODO + } + + #[kani::proof] + fn verify_i8_unchecked_shr() { + // TODO + } + + #[kani::proof] + fn verify_i8_unchecked_neg() { + // TODO + } +} diff --git a/library/core/tests/num/kani-proofs/u128-proofs.rs b/library/core/tests/num/kani-proofs/u128-proofs.rs index 98d781ec024b5..4746ba6f6149d 100644 --- a/library/core/tests/num/kani-proofs/u128-proofs.rs +++ b/library/core/tests/num/kani-proofs/u128-proofs.rs @@ -1,21 +1,46 @@ #[cfg(kani)] mod verification { - // use super::*; + // use super::*; - #[kani::proof] - fn verify_u128_unchecked_add() { - let num1: u128 = kani::any::(); - let num2: u128 = kani::any::(); + #[kani::proof] + fn verify_u128_unchecked_add() { + let num1: u128 = kani::any::(); + let num2: u128 = kani::any::(); - // Safety preconditions: - // - Addition won't overflow - // Unsigned integers are always positive, so underflow won't happen - // Undefined behavior occurs when overflow happens - kani::assume(num1 < u128::MAX - num2); + // Safety preconditions: + // - Addition won't overflow + // Unsigned integers are always positive, so underflow won't happen + // Undefined behavior occurs when overflow happens + kani::assume(num1 < u128::MAX - num2); unsafe { let result = num1.unchecked_add(num2); assert_eq!(Some(result), num1.checked_add(num2)); } - } -} \ No newline at end of file + } + + #[kani::proof] + fn verify_u128_unchecked_sub() { + // TODO + } + + #[kani::proof] + fn verify_u128_unchecked_mul() { + // TODO + } + + #[kani::proof] + fn verify_u128_unchecked_shl() { + // TODO + } + + #[kani::proof] + fn verify_u128_unchecked_shr() { + // TODO + } + + #[kani::proof] + fn verify_u128_unchecked_neg() { + // TODO + } +} diff --git a/library/core/tests/num/kani-proofs/u16-proofs.rs b/library/core/tests/num/kani-proofs/u16-proofs.rs index 9dfff81d1abbb..c398cc0ee474b 100644 --- a/library/core/tests/num/kani-proofs/u16-proofs.rs +++ b/library/core/tests/num/kani-proofs/u16-proofs.rs @@ -1,21 +1,46 @@ #[cfg(kani)] mod verification { - // use super::*; + // use super::*; - #[kani::proof] - fn verify_u16_unchecked_add() { - let num1: u16 = kani::any::(); - let num2: u16 = kani::any::(); + #[kani::proof] + fn verify_u16_unchecked_add() { + let num1: u16 = kani::any::(); + let num2: u16 = kani::any::(); - // Safety preconditions: - // - Addition won't overflow - // Unsigned integers are always positive, so underflow won't happen - // Undefined behavior occurs when overflow happens - kani::assume(num1 < u16::MAX - num2); + // Safety preconditions: + // - Addition won't overflow + // Unsigned integers are always positive, so underflow won't happen + // Undefined behavior occurs when overflow happens + kani::assume(num1 < u16::MAX - num2); unsafe { let result = num1.unchecked_add(num2); assert_eq!(Some(result), num1.checked_add(num2)); } - } -} \ No newline at end of file + } + + #[kani::proof] + fn verify_u16_unchecked_sub() { + // TODO + } + + #[kani::proof] + fn verify_u16_unchecked_mul() { + // TODO + } + + #[kani::proof] + fn verify_u16_unchecked_shl() { + // TODO + } + + #[kani::proof] + fn verify_u16_unchecked_shr() { + // TODO + } + + #[kani::proof] + fn verify_u16_unchecked_neg() { + // TODO + } +} diff --git a/library/core/tests/num/kani-proofs/u32-proofs.rs b/library/core/tests/num/kani-proofs/u32-proofs.rs index 0d13bdcd2dce0..8f4dfb17949a5 100644 --- a/library/core/tests/num/kani-proofs/u32-proofs.rs +++ b/library/core/tests/num/kani-proofs/u32-proofs.rs @@ -1,21 +1,46 @@ #[cfg(kani)] mod verification { - // use super::*; + // use super::*; - #[kani::proof] - fn verify_u32_unchecked_add() { - let num1: u32 = kani::any::(); - let num2: u32 = kani::any::(); + #[kani::proof] + fn verify_u32_unchecked_add() { + let num1: u32 = kani::any::(); + let num2: u32 = kani::any::(); - // Safety preconditions: - // - Addition won't overflow - // Unsigned integers are always positive, so underflow won't happen - // Undefined behavior occurs when overflow happens - kani::assume(num1 < u32::MAX - num2); + // Safety preconditions: + // - Addition won't overflow + // Unsigned integers are always positive, so underflow won't happen + // Undefined behavior occurs when overflow happens + kani::assume(num1 < u32::MAX - num2); unsafe { let result = num1.unchecked_add(num2); assert_eq!(Some(result), num1.checked_add(num2)); } - } -} \ No newline at end of file + } + + #[kani::proof] + fn verify_u32_unchecked_sub() { + // TODO + } + + #[kani::proof] + fn verify_u32_unchecked_mul() { + // TODO + } + + #[kani::proof] + fn verify_u32_unchecked_shl() { + // TODO + } + + #[kani::proof] + fn verify_u32_unchecked_shr() { + // TODO + } + + #[kani::proof] + fn verify_u32_unchecked_neg() { + // TODO + } +} diff --git a/library/core/tests/num/kani-proofs/u64-proofs.rs b/library/core/tests/num/kani-proofs/u64-proofs.rs index 405468c96e0ba..d65c6f9178857 100644 --- a/library/core/tests/num/kani-proofs/u64-proofs.rs +++ b/library/core/tests/num/kani-proofs/u64-proofs.rs @@ -1,21 +1,46 @@ #[cfg(kani)] mod verification { - // use super::*; + // use super::*; - #[kani::proof] - fn verify_u64_unchecked_add() { - let num1: u64 = kani::any::(); - let num2: u64 = kani::any::(); + #[kani::proof] + fn verify_u64_unchecked_add() { + let num1: u64 = kani::any::(); + let num2: u64 = kani::any::(); - // Safety preconditions: - // - Addition won't overflow - // Unsigned integers are always positive, so underflow won't happen - // Undefined behavior occurs when overflow happens - kani::assume(num1 < u64::MAX - num2); + // Safety preconditions: + // - Addition won't overflow + // Unsigned integers are always positive, so underflow won't happen + // Undefined behavior occurs when overflow happens + kani::assume(num1 < u64::MAX - num2); unsafe { let result = num1.unchecked_add(num2); assert_eq!(Some(result), num1.checked_add(num2)); } - } -} \ No newline at end of file + } + + #[kani::proof] + fn verify_u64_unchecked_sub() { + // TODO + } + + #[kani::proof] + fn verify_u64_unchecked_mul() { + // TODO + } + + #[kani::proof] + fn verify_u64_unchecked_shl() { + // TODO + } + + #[kani::proof] + fn verify_u64_unchecked_shr() { + // TODO + } + + #[kani::proof] + fn verify_u64_unchecked_neg() { + // TODO + } +} diff --git a/library/core/tests/num/kani-proofs/u8-proofs.rs b/library/core/tests/num/kani-proofs/u8-proofs.rs index 89826fc292c4b..ef6569ceaa3ba 100644 --- a/library/core/tests/num/kani-proofs/u8-proofs.rs +++ b/library/core/tests/num/kani-proofs/u8-proofs.rs @@ -1,21 +1,46 @@ #[cfg(kani)] mod verification { - // use super::*; + // use super::*; - #[kani::proof] - fn verify_u8_unchecked_add() { - let num1: u8 = kani::any::(); - let num2: u8 = kani::any::(); + #[kani::proof] + fn verify_u8_unchecked_add() { + let num1: u8 = kani::any::(); + let num2: u8 = kani::any::(); - // Safety preconditions: - // - Addition won't overflow - // Unsigned integers are always positive, so underflow won't happen - // Undefined behavior occurs when overflow happens - kani::assume(num1 < u8::MAX - num2); + // Safety preconditions: + // - Addition won't overflow + // Unsigned integers are always positive, so underflow won't happen + // Undefined behavior occurs when overflow happens + kani::assume(num1 < u8::MAX - num2); unsafe { let result = num1.unchecked_add(num2); assert_eq!(Some(result), num1.checked_add(num2)); } - } -} \ No newline at end of file + } + + #[kani::proof] + fn verify_u8_unchecked_sub() { + // TODO + } + + #[kani::proof] + fn verify_u8_unchecked_mul() { + // TODO + } + + #[kani::proof] + fn verify_u8_unchecked_shl() { + // TODO + } + + #[kani::proof] + fn verify_u8_unchecked_shr() { + // TODO + } + + #[kani::proof] + fn verify_u8_unchecked_neg() { + // TODO + } +} From daaaf7e1c61c9cfad8a44912ca7b66ca6432ae86 Mon Sep 17 00:00:00 2001 From: yew005 Date: Mon, 16 Sep 2024 16:53:39 -0700 Subject: [PATCH 03/25] Experiment with two verification approaches in mod.rs of core::num --- library/core/src/num/mod.rs | 60 +++++++++++++++++++++++++++++++++++++ 1 file changed, 60 insertions(+) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 309e1ba958aee..bb4a8ca6e59c2 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1580,3 +1580,63 @@ from_str_radix_size_impl! { i16 isize, u16 usize } from_str_radix_size_impl! { i32 isize, u32 usize } #[cfg(target_pointer_width = "64")] from_str_radix_size_impl! { i64 isize, u64 usize } + + +// #[feature(unchecked_math)] +#[cfg(kani)] +use crate::kani; + +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // Signed unchecked_add Safety preconditions: + // - Positive number addition won't overflow + // - Negative number addition won't underflow + // Addition of two integers with different signs never overflows + // Undefined behavior occurs when overflow or underflow happens + #[kani::requires(!num1.overflowing_add(num2).1)] + #[kani::ensures(|ret| *ret >= i8::MIN && *ret <= i8::MAX)] + fn i8_unchecked_add_wrapper(num1: i8, num2: i8) -> i8 { + unsafe { num1.unchecked_add(num2) } + } + + // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self + #[kani::proof_for_contract(i8_unchecked_add_wrapper)] + pub fn check_unchecked_add_i8() { + let num1: i8 = kani::any::(); + let num2: i8 = kani::any::(); + + // kani::assume( + // (num1 > 0 && num2 > 0 && num1 < i8::MAX - num2) + // || (num1 < 0 && num2 < 0 && num1 > i8::MIN - num2), + // ); + + unsafe { + // Kani ensures the inputs satisfy preconditions + i8_unchecked_add_wrapper(num1, num2); + // Kani ensures the output satisfy postconditions + } + } + + // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self + #[kani::proof] + pub fn check_unchecked_add_i16() { + let num1: i16 = kani::any::(); + let num2: i16 = kani::any::(); + + // overflowing_add return (result, bool) where bool is if + // add will overflow. This check takes the boolean. + kani::assume(!num1.overflowing_add(num2).1); + + unsafe { + let result = num1.unchecked_add(num2); + + // Either check result + assert_eq!(Some(result), num1.checked_add(num2)); + + // Or check range of result + assert!(result >= i16::MIN && result <= i16::MAX); + } + } +} From 1c9dbde3758ae3889aa73ca491849c3303af0fc1 Mon Sep 17 00:00:00 2001 From: yew005 Date: Wed, 18 Sep 2024 14:27:27 -0700 Subject: [PATCH 04/25] Add contracts to unchecked_add && Add i8::unchecked_add proof --- library/core/src/num/int_macros.rs | 2 ++ library/core/src/num/mod.rs | 37 ++--------------------------- library/core/src/num/uint_macros.rs | 2 ++ 3 files changed, 6 insertions(+), 35 deletions(-) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index 878a911dde50d..6e97b7999eef4 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -511,6 +511,8 @@ macro_rules! int_impl { without modifying the original"] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[kani::requires(!self.overflowing_add(rhs).1)] + #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] pub const unsafe fn unchecked_add(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index f5223023c8f2b..9cacb61a47030 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1596,48 +1596,15 @@ mod verify { // - Negative number addition won't underflow // Addition of two integers with different signs never overflows // Undefined behavior occurs when overflow or underflow happens - #[kani::requires(!num1.overflowing_add(num2).1)] - #[kani::ensures(|ret| *ret >= i8::MIN && *ret <= i8::MAX)] - fn i8_unchecked_add_wrapper(num1: i8, num2: i8) -> i8 { - unsafe { num1.unchecked_add(num2) } - } // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self - #[kani::proof_for_contract(i8_unchecked_add_wrapper)] + #[kani::proof_for_contract(i8::unchecked_add)] pub fn check_unchecked_add_i8() { let num1: i8 = kani::any::(); let num2: i8 = kani::any::(); - - // kani::assume( - // (num1 > 0 && num2 > 0 && num1 < i8::MAX - num2) - // || (num1 < 0 && num2 < 0 && num1 > i8::MIN - num2), - // ); - - unsafe { - // Kani ensures the inputs satisfy preconditions - i8_unchecked_add_wrapper(num1, num2); - // Kani ensures the output satisfy postconditions - } - } - - // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self - #[kani::proof] - pub fn check_unchecked_add_i16() { - let num1: i16 = kani::any::(); - let num2: i16 = kani::any::(); - - // overflowing_add return (result, bool) where bool is if - // add will overflow. This check takes the boolean. - kani::assume(!num1.overflowing_add(num2).1); unsafe { - let result = num1.unchecked_add(num2); - - // Either check result - assert_eq!(Some(result), num1.checked_add(num2)); - - // Or check range of result - assert!(result >= i16::MIN && result <= i16::MAX); + num1.unchecked_add(num2); } } } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index d9036abecc592..64d43c394e2b2 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -558,6 +558,8 @@ macro_rules! uint_impl { without modifying the original"] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[kani::requires(!self.overflowing_add(rhs).1)] + #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] pub const unsafe fn unchecked_add(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, From 894231fb15f248db0b76efab587e3c7cdb2ac1cb Mon Sep 17 00:00:00 2001 From: yew005 Date: Wed, 18 Sep 2024 14:31:58 -0700 Subject: [PATCH 05/25] Format core::num mod.rs --- library/core/src/num/mod.rs | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 9cacb61a47030..1ebc09815717a 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1397,7 +1397,10 @@ const fn from_str_radix_panic_ct(_radix: u32) -> ! { #[track_caller] fn from_str_radix_panic_rt(radix: u32) -> ! { - panic!("from_str_radix_int: must lie in the range `[2, 36]` - found {}", radix); + panic!( + "from_str_radix_int: must lie in the range `[2, 36]` - found {}", + radix + ); } #[cfg_attr(not(feature = "panic_immediate_abort"), inline(never))] @@ -1582,7 +1585,6 @@ from_str_radix_size_impl! { i32 isize, u32 usize } #[cfg(target_pointer_width = "64")] from_str_radix_size_impl! { i64 isize, u64 usize } - // #[feature(unchecked_math)] #[cfg(kani)] use crate::kani; @@ -1596,6 +1598,9 @@ mod verify { // - Negative number addition won't underflow // Addition of two integers with different signs never overflows // Undefined behavior occurs when overflow or underflow happens + // Target contracts: + // #[kani::requires(!self.overflowing_add(rhs).1)] + // #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self #[kani::proof_for_contract(i8::unchecked_add)] From 2bc4faf2ff544da0611eaa67e4644535a629bf8b Mon Sep 17 00:00:00 2001 From: yew005 Date: Wed, 18 Sep 2024 14:41:15 -0700 Subject: [PATCH 06/25] Add comment for unchecked_add proofs --- library/core/src/num/mod.rs | 23 +++++++++++++++++------ 1 file changed, 17 insertions(+), 6 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 1ebc09815717a..02d686519b9a2 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1593,16 +1593,27 @@ use crate::kani; mod verify { use super::*; - // Signed unchecked_add Safety preconditions: - // - Positive number addition won't overflow - // - Negative number addition won't underflow - // Addition of two integers with different signs never overflows - // Undefined behavior occurs when overflow or underflow happens + // `unchecked_add` proofs + // // Target contracts: // #[kani::requires(!self.overflowing_add(rhs).1)] // #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] - + // + // Target function: // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self + // + // Safety preconditions: + // 1. Signed integers (i8, i16, i32, i64, i128): + // - Positive number addition won't overflow + // - Negative number addition won't underflow + // Addition of two integers with different signs never overflows + // Undefined behavior occurs when overflow or underflow happens + // + // 2. Unsigned integers (u8, u16, u32, u64, u128): + // - Addition won't overflow + // Unsigned integers are always positive, so underflow won't happen + // Undefined behavior occurs when overflow happens + #[kani::proof_for_contract(i8::unchecked_add)] pub fn check_unchecked_add_i8() { let num1: i8 = kani::any::(); From d9d4b5f377b0f6a6ca7986d371961633698262e1 Mon Sep 17 00:00:00 2001 From: yew005 Date: Thu, 19 Sep 2024 15:11:12 -0700 Subject: [PATCH 07/25] Add harnesses for i16,i32,i64,i128 unchecked_add --- library/core/src/num/mod.rs | 47 +++++++++++++++++++++++++++++++++---- 1 file changed, 43 insertions(+), 4 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 02d686519b9a2..ae9762bd72d62 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1585,7 +1585,6 @@ from_str_radix_size_impl! { i32 isize, u32 usize } #[cfg(target_pointer_width = "64")] from_str_radix_size_impl! { i64 isize, u64 usize } -// #[feature(unchecked_math)] #[cfg(kani)] use crate::kani; @@ -1598,17 +1597,17 @@ mod verify { // Target contracts: // #[kani::requires(!self.overflowing_add(rhs).1)] // #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] - // + // // Target function: // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self - // + // // Safety preconditions: // 1. Signed integers (i8, i16, i32, i64, i128): // - Positive number addition won't overflow // - Negative number addition won't underflow // Addition of two integers with different signs never overflows // Undefined behavior occurs when overflow or underflow happens - // + // // 2. Unsigned integers (u8, u16, u32, u64, u128): // - Addition won't overflow // Unsigned integers are always positive, so underflow won't happen @@ -1623,4 +1622,44 @@ mod verify { num1.unchecked_add(num2); } } + + #[kani::proof_for_contract(i16::unchecked_add)] + pub fn check_unchecked_add_i16() { + let num1: i16 = kani::any::(); + let num2: i16 = kani::any::(); + + unsafe { + num1.unchecked_add(num2); + } + } + + #[kani::proof_for_contract(i32::unchecked_add)] + pub fn check_unchecked_add_i32() { + let num1: i32 = kani::any::(); + let num2: i32 = kani::any::(); + + unsafe { + num1.unchecked_add(num2); + } + } + + #[kani::proof_for_contract(i64::unchecked_add)] + pub fn check_unchecked_add_i64() { + let num1: i64 = kani::any::(); + let num2: i64 = kani::any::(); + + unsafe { + num1.unchecked_add(num2); + } + } + + #[kani::proof_for_contract(i128::unchecked_add)] + pub fn check_unchecked_add_i128() { + let num1: i128 = kani::any::(); + let num2: i128 = kani::any::(); + + unsafe { + num1.unchecked_add(num2); + } + } } From 07c8b4a5dc06a826feee8fef416955765d197d0d Mon Sep 17 00:00:00 2001 From: yew005 Date: Thu, 19 Sep 2024 15:18:50 -0700 Subject: [PATCH 08/25] Add harnesses for u8,u16,u32,u64,u128 unchecked_add --- library/core/src/num/mod.rs | 50 +++++++++++++++++++++++++++++++++++++ 1 file changed, 50 insertions(+) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index ae9762bd72d62..95984fccebc1f 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1662,4 +1662,54 @@ mod verify { num1.unchecked_add(num2); } } + + #[kani::proof_for_contract(u8::unchecked_add)] + pub fn check_unchecked_add_u8() { + let num1: u8 = kani::any::(); + let num2: u8 = kani::any::(); + + unsafe { + num1.unchecked_add(num2); + } + } + + #[kani::proof_for_contract(u16::unchecked_add)] + pub fn check_unchecked_add_u16() { + let num1: u16 = kani::any::(); + let num2: u16 = kani::any::(); + + unsafe { + num1.unchecked_add(num2); + } + } + + #[kani::proof_for_contract(u32::unchecked_add)] + pub fn check_unchecked_add_u32() { + let num1: u32 = kani::any::(); + let num2: u32 = kani::any::(); + + unsafe { + num1.unchecked_add(num2); + } + } + + #[kani::proof_for_contract(u64::unchecked_add)] + pub fn check_unchecked_add_u64() { + let num1: u64 = kani::any::(); + let num2: u64 = kani::any::(); + + unsafe { + num1.unchecked_add(num2); + } + } + + #[kani::proof_for_contract(u128::unchecked_add)] + pub fn check_unchecked_add_u128() { + let num1: u128 = kani::any::(); + let num2: u128 = kani::any::(); + + unsafe { + num1.unchecked_add(num2); + } + } } From 1fd4c6ae936496966b9f305906065d10b1c1b80a Mon Sep 17 00:00:00 2001 From: yew005 Date: Thu, 19 Sep 2024 15:22:12 -0700 Subject: [PATCH 09/25] Cleanup misplaced proofs --- .../core/tests/num/kani-proofs/i128-proofs.rs | 50 ------------------- .../core/tests/num/kani-proofs/i16-proofs.rs | 50 ------------------- .../core/tests/num/kani-proofs/i32-proofs.rs | 50 ------------------- .../core/tests/num/kani-proofs/i64-proofs.rs | 50 ------------------- .../core/tests/num/kani-proofs/i8-proofs.rs | 50 ------------------- .../core/tests/num/kani-proofs/u128-proofs.rs | 46 ----------------- .../core/tests/num/kani-proofs/u16-proofs.rs | 46 ----------------- .../core/tests/num/kani-proofs/u32-proofs.rs | 46 ----------------- .../core/tests/num/kani-proofs/u64-proofs.rs | 46 ----------------- .../core/tests/num/kani-proofs/u8-proofs.rs | 46 ----------------- 10 files changed, 480 deletions(-) delete mode 100644 library/core/tests/num/kani-proofs/i128-proofs.rs delete mode 100644 library/core/tests/num/kani-proofs/i16-proofs.rs delete mode 100644 library/core/tests/num/kani-proofs/i32-proofs.rs delete mode 100644 library/core/tests/num/kani-proofs/i64-proofs.rs delete mode 100644 library/core/tests/num/kani-proofs/i8-proofs.rs delete mode 100644 library/core/tests/num/kani-proofs/u128-proofs.rs delete mode 100644 library/core/tests/num/kani-proofs/u16-proofs.rs delete mode 100644 library/core/tests/num/kani-proofs/u32-proofs.rs delete mode 100644 library/core/tests/num/kani-proofs/u64-proofs.rs delete mode 100644 library/core/tests/num/kani-proofs/u8-proofs.rs diff --git a/library/core/tests/num/kani-proofs/i128-proofs.rs b/library/core/tests/num/kani-proofs/i128-proofs.rs deleted file mode 100644 index 4ac03ec8714fe..0000000000000 --- a/library/core/tests/num/kani-proofs/i128-proofs.rs +++ /dev/null @@ -1,50 +0,0 @@ -#[cfg(kani)] -mod verification { - // use super::*; - - #[kani::proof] - fn verify_i128_unchecked_add() { - let num1: i128 = kani::any::(); - let num2: i128 = kani::any::(); - - // Safety preconditions: - // - Positive number addition won't overflow - // - Negative number addition won't underflow - // Addition of two integers with different signs never overflows - // Undefined behavior occurs when overflow or underflow happens - kani::assume( - (num1 > 0 && num2 > 0 && num1 < i128::MAX - num2) - || (num1 < 0 && num2 < 0 && num1 > i128::MIN - num2), - ); - - unsafe { - let result = num1.unchecked_add(num2); - assert_eq!(Some(result), num1.checked_add(num2)); - } - } - - #[kani::proof] - fn verify_i128_unchecked_sub() { - // TODO - } - - #[kani::proof] - fn verify_i128_unchecked_mul() { - // TODO - } - - #[kani::proof] - fn verify_i128_unchecked_shl() { - // TODO - } - - #[kani::proof] - fn verify_i128_unchecked_shr() { - // TODO - } - - #[kani::proof] - fn verify_i128_unchecked_neg() { - // TODO - } -} diff --git a/library/core/tests/num/kani-proofs/i16-proofs.rs b/library/core/tests/num/kani-proofs/i16-proofs.rs deleted file mode 100644 index f57591f6b8e07..0000000000000 --- a/library/core/tests/num/kani-proofs/i16-proofs.rs +++ /dev/null @@ -1,50 +0,0 @@ -#[cfg(kani)] -mod verification { - // use super::*; - - #[kani::proof] - fn verify_i16_unchecked_add() { - let num1: i16 = kani::any::(); - let num2: i16 = kani::any::(); - - // Safety preconditions: - // - Positive number addition won't overflow - // - Negative number addition won't underflow - // Addition of two integers with different signs never overflows - // Undefined behavior occurs when overflow or underflow happens - kani::assume( - (num1 > 0 && num2 > 0 && num1 < i16::MAX - num2) - || (num1 < 0 && num2 < 0 && num1 > i16::MIN - num2), - ); - - unsafe { - let result = num1.unchecked_add(num2); - assert_eq!(Some(result), num1.checked_add(num2)); - } - } - - #[kani::proof] - fn verify_i16_unchecked_sub() { - // TODO - } - - #[kani::proof] - fn verify_i16_unchecked_mul() { - // TODO - } - - #[kani::proof] - fn verify_i16_unchecked_shl() { - // TODO - } - - #[kani::proof] - fn verify_i16_unchecked_shr() { - // TODO - } - - #[kani::proof] - fn verify_i16_unchecked_neg() { - // TODO - } -} diff --git a/library/core/tests/num/kani-proofs/i32-proofs.rs b/library/core/tests/num/kani-proofs/i32-proofs.rs deleted file mode 100644 index 0c8cca6a8d9c0..0000000000000 --- a/library/core/tests/num/kani-proofs/i32-proofs.rs +++ /dev/null @@ -1,50 +0,0 @@ -#[cfg(kani)] -mod verification { - // use super::*; - - #[kani::proof] - fn verify_i32_unchecked_add() { - let num1: i32 = kani::any::(); - let num2: i32 = kani::any::(); - - // Safety preconditions: - // - Positive number addition won't overflow - // - Negative number addition won't underflow - // Addition of two integers with different signs never overflows - // Undefined behavior occurs when overflow or underflow happens - kani::assume( - (num1 > 0 && num2 > 0 && num1 < i32::MAX - num2) - || (num1 < 0 && num2 < 0 && num1 > i32::MIN - num2), - ); - - unsafe { - let result = num1.unchecked_add(num2); - assert_eq!(Some(result), num1.checked_add(num2)); - } - } - - #[kani::proof] - fn verify_i32_unchecked_sub() { - // TODO - } - - #[kani::proof] - fn verify_i32_unchecked_mul() { - // TODO - } - - #[kani::proof] - fn verify_i32_unchecked_shl() { - // TODO - } - - #[kani::proof] - fn verify_i32_unchecked_shr() { - // TODO - } - - #[kani::proof] - fn verify_i32_unchecked_neg() { - // TODO - } -} diff --git a/library/core/tests/num/kani-proofs/i64-proofs.rs b/library/core/tests/num/kani-proofs/i64-proofs.rs deleted file mode 100644 index 658956c110dd8..0000000000000 --- a/library/core/tests/num/kani-proofs/i64-proofs.rs +++ /dev/null @@ -1,50 +0,0 @@ -#[cfg(kani)] -mod verification { - // use super::*; - - #[kani::proof] - fn verify_i64_unchecked_add() { - let num1: i64 = kani::any::(); - let num2: i64 = kani::any::(); - - // Safety preconditions: - // - Positive number addition won't overflow - // - Negative number addition won't underflow - // Addition of two integers with different signs never overflows - // Undefined behavior occurs when overflow or underflow happens - kani::assume( - (num1 > 0 && num2 > 0 && num1 < i64::MAX - num2) - || (num1 < 0 && num2 < 0 && num1 > i64::MIN - num2), - ); - - unsafe { - let result = num1.unchecked_add(num2); - assert_eq!(Some(result), num1.checked_add(num2)); - } - } - - #[kani::proof] - fn verify_i64_unchecked_sub() { - // TODO - } - - #[kani::proof] - fn verify_i64_unchecked_mul() { - // TODO - } - - #[kani::proof] - fn verify_i64_unchecked_shl() { - // TODO - } - - #[kani::proof] - fn verify_i64_unchecked_shr() { - // TODO - } - - #[kani::proof] - fn verify_i64_unchecked_neg() { - // TODO - } -} diff --git a/library/core/tests/num/kani-proofs/i8-proofs.rs b/library/core/tests/num/kani-proofs/i8-proofs.rs deleted file mode 100644 index 932407510ffda..0000000000000 --- a/library/core/tests/num/kani-proofs/i8-proofs.rs +++ /dev/null @@ -1,50 +0,0 @@ -#[cfg(kani)] -mod verification { - // use super::*; - - #[kani::proof] - fn verify_i8_unchecked_add() { - let num1: i8 = kani::any::(); - let num2: i8 = kani::any::(); - - // Safety preconditions: - // - Positive number addition won't overflow - // - Negative number addition won't underflow - // Addition of two integers with different signs never overflows - // Undefined behavior occurs when overflow or underflow happens - kani::assume( - (num1 > 0 && num2 > 0 && num1 < i8::MAX - num2) - || (num1 < 0 && num2 < 0 && num1 > i8::MIN - num2), - ); - - unsafe { - let result = num1.unchecked_add(num2); - assert_eq!(Some(result), num1.checked_add(num2)); - } - } - - #[kani::proof] - fn verify_i8_unchecked_sub() { - // TODO - } - - #[kani::proof] - fn verify_i8_unchecked_mul() { - // TODO - } - - #[kani::proof] - fn verify_i8_unchecked_shl() { - // TODO - } - - #[kani::proof] - fn verify_i8_unchecked_shr() { - // TODO - } - - #[kani::proof] - fn verify_i8_unchecked_neg() { - // TODO - } -} diff --git a/library/core/tests/num/kani-proofs/u128-proofs.rs b/library/core/tests/num/kani-proofs/u128-proofs.rs deleted file mode 100644 index 4746ba6f6149d..0000000000000 --- a/library/core/tests/num/kani-proofs/u128-proofs.rs +++ /dev/null @@ -1,46 +0,0 @@ -#[cfg(kani)] -mod verification { - // use super::*; - - #[kani::proof] - fn verify_u128_unchecked_add() { - let num1: u128 = kani::any::(); - let num2: u128 = kani::any::(); - - // Safety preconditions: - // - Addition won't overflow - // Unsigned integers are always positive, so underflow won't happen - // Undefined behavior occurs when overflow happens - kani::assume(num1 < u128::MAX - num2); - - unsafe { - let result = num1.unchecked_add(num2); - assert_eq!(Some(result), num1.checked_add(num2)); - } - } - - #[kani::proof] - fn verify_u128_unchecked_sub() { - // TODO - } - - #[kani::proof] - fn verify_u128_unchecked_mul() { - // TODO - } - - #[kani::proof] - fn verify_u128_unchecked_shl() { - // TODO - } - - #[kani::proof] - fn verify_u128_unchecked_shr() { - // TODO - } - - #[kani::proof] - fn verify_u128_unchecked_neg() { - // TODO - } -} diff --git a/library/core/tests/num/kani-proofs/u16-proofs.rs b/library/core/tests/num/kani-proofs/u16-proofs.rs deleted file mode 100644 index c398cc0ee474b..0000000000000 --- a/library/core/tests/num/kani-proofs/u16-proofs.rs +++ /dev/null @@ -1,46 +0,0 @@ -#[cfg(kani)] -mod verification { - // use super::*; - - #[kani::proof] - fn verify_u16_unchecked_add() { - let num1: u16 = kani::any::(); - let num2: u16 = kani::any::(); - - // Safety preconditions: - // - Addition won't overflow - // Unsigned integers are always positive, so underflow won't happen - // Undefined behavior occurs when overflow happens - kani::assume(num1 < u16::MAX - num2); - - unsafe { - let result = num1.unchecked_add(num2); - assert_eq!(Some(result), num1.checked_add(num2)); - } - } - - #[kani::proof] - fn verify_u16_unchecked_sub() { - // TODO - } - - #[kani::proof] - fn verify_u16_unchecked_mul() { - // TODO - } - - #[kani::proof] - fn verify_u16_unchecked_shl() { - // TODO - } - - #[kani::proof] - fn verify_u16_unchecked_shr() { - // TODO - } - - #[kani::proof] - fn verify_u16_unchecked_neg() { - // TODO - } -} diff --git a/library/core/tests/num/kani-proofs/u32-proofs.rs b/library/core/tests/num/kani-proofs/u32-proofs.rs deleted file mode 100644 index 8f4dfb17949a5..0000000000000 --- a/library/core/tests/num/kani-proofs/u32-proofs.rs +++ /dev/null @@ -1,46 +0,0 @@ -#[cfg(kani)] -mod verification { - // use super::*; - - #[kani::proof] - fn verify_u32_unchecked_add() { - let num1: u32 = kani::any::(); - let num2: u32 = kani::any::(); - - // Safety preconditions: - // - Addition won't overflow - // Unsigned integers are always positive, so underflow won't happen - // Undefined behavior occurs when overflow happens - kani::assume(num1 < u32::MAX - num2); - - unsafe { - let result = num1.unchecked_add(num2); - assert_eq!(Some(result), num1.checked_add(num2)); - } - } - - #[kani::proof] - fn verify_u32_unchecked_sub() { - // TODO - } - - #[kani::proof] - fn verify_u32_unchecked_mul() { - // TODO - } - - #[kani::proof] - fn verify_u32_unchecked_shl() { - // TODO - } - - #[kani::proof] - fn verify_u32_unchecked_shr() { - // TODO - } - - #[kani::proof] - fn verify_u32_unchecked_neg() { - // TODO - } -} diff --git a/library/core/tests/num/kani-proofs/u64-proofs.rs b/library/core/tests/num/kani-proofs/u64-proofs.rs deleted file mode 100644 index d65c6f9178857..0000000000000 --- a/library/core/tests/num/kani-proofs/u64-proofs.rs +++ /dev/null @@ -1,46 +0,0 @@ -#[cfg(kani)] -mod verification { - // use super::*; - - #[kani::proof] - fn verify_u64_unchecked_add() { - let num1: u64 = kani::any::(); - let num2: u64 = kani::any::(); - - // Safety preconditions: - // - Addition won't overflow - // Unsigned integers are always positive, so underflow won't happen - // Undefined behavior occurs when overflow happens - kani::assume(num1 < u64::MAX - num2); - - unsafe { - let result = num1.unchecked_add(num2); - assert_eq!(Some(result), num1.checked_add(num2)); - } - } - - #[kani::proof] - fn verify_u64_unchecked_sub() { - // TODO - } - - #[kani::proof] - fn verify_u64_unchecked_mul() { - // TODO - } - - #[kani::proof] - fn verify_u64_unchecked_shl() { - // TODO - } - - #[kani::proof] - fn verify_u64_unchecked_shr() { - // TODO - } - - #[kani::proof] - fn verify_u64_unchecked_neg() { - // TODO - } -} diff --git a/library/core/tests/num/kani-proofs/u8-proofs.rs b/library/core/tests/num/kani-proofs/u8-proofs.rs deleted file mode 100644 index ef6569ceaa3ba..0000000000000 --- a/library/core/tests/num/kani-proofs/u8-proofs.rs +++ /dev/null @@ -1,46 +0,0 @@ -#[cfg(kani)] -mod verification { - // use super::*; - - #[kani::proof] - fn verify_u8_unchecked_add() { - let num1: u8 = kani::any::(); - let num2: u8 = kani::any::(); - - // Safety preconditions: - // - Addition won't overflow - // Unsigned integers are always positive, so underflow won't happen - // Undefined behavior occurs when overflow happens - kani::assume(num1 < u8::MAX - num2); - - unsafe { - let result = num1.unchecked_add(num2); - assert_eq!(Some(result), num1.checked_add(num2)); - } - } - - #[kani::proof] - fn verify_u8_unchecked_sub() { - // TODO - } - - #[kani::proof] - fn verify_u8_unchecked_mul() { - // TODO - } - - #[kani::proof] - fn verify_u8_unchecked_shl() { - // TODO - } - - #[kani::proof] - fn verify_u8_unchecked_shr() { - // TODO - } - - #[kani::proof] - fn verify_u8_unchecked_neg() { - // TODO - } -} From b360311c955df808f38ec2c4c5ddaa57f4f810e3 Mon Sep 17 00:00:00 2001 From: yew005 Date: Fri, 20 Sep 2024 12:57:35 -0700 Subject: [PATCH 10/25] Clean up comment --- library/core/src/num/mod.rs | 13 ++----------- 1 file changed, 2 insertions(+), 11 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 95984fccebc1f..95fc1f394f63b 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1601,17 +1601,8 @@ mod verify { // Target function: // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self // - // Safety preconditions: - // 1. Signed integers (i8, i16, i32, i64, i128): - // - Positive number addition won't overflow - // - Negative number addition won't underflow - // Addition of two integers with different signs never overflows - // Undefined behavior occurs when overflow or underflow happens - // - // 2. Unsigned integers (u8, u16, u32, u64, u128): - // - Addition won't overflow - // Unsigned integers are always positive, so underflow won't happen - // Undefined behavior occurs when overflow happens + // Target types: + // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total #[kani::proof_for_contract(i8::unchecked_add)] pub fn check_unchecked_add_i8() { From 8cbca87171dc3efa4264e09df094866b499ecf07 Mon Sep 17 00:00:00 2001 From: yew005 Date: Fri, 20 Sep 2024 12:58:16 -0700 Subject: [PATCH 11/25] Format comment --- library/core/src/num/mod.rs | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 95fc1f394f63b..766b52f227ffa 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1594,16 +1594,15 @@ mod verify { // `unchecked_add` proofs // + // Target types: + // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total + // // Target contracts: // #[kani::requires(!self.overflowing_add(rhs).1)] // #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // // Target function: // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self - // - // Target types: - // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total - #[kani::proof_for_contract(i8::unchecked_add)] pub fn check_unchecked_add_i8() { let num1: i8 = kani::any::(); From 0eef8581caa0f581689307aa6c3611bde6aec4b2 Mon Sep 17 00:00:00 2001 From: yew005 Date: Fri, 20 Sep 2024 13:15:21 -0700 Subject: [PATCH 12/25] Remove before contracts. Fix import in --- library/core/src/num/int_macros.rs | 4 ++-- library/core/src/num/mod.rs | 7 ++++--- library/core/src/num/uint_macros.rs | 4 ++-- 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index 6e97b7999eef4..fa0c9c98dde74 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -511,8 +511,8 @@ macro_rules! int_impl { without modifying the original"] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - #[kani::requires(!self.overflowing_add(rhs).1)] - #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] + #[requires(!self.overflowing_add(rhs).1)] + #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] pub const unsafe fn unchecked_add(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 766b52f227ffa..28aeb1b897149 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -5,6 +5,10 @@ use crate::str::FromStr; use crate::ub_checks::assert_unsafe_precondition; use crate::{ascii, intrinsics, mem}; +use safety::{ensures, requires}; + +#[cfg(kani)] +use crate::kani; // Used because the `?` operator is not allowed in a const context. macro_rules! try_opt { @@ -1585,9 +1589,6 @@ from_str_radix_size_impl! { i32 isize, u32 usize } #[cfg(target_pointer_width = "64")] from_str_radix_size_impl! { i64 isize, u64 usize } -#[cfg(kani)] -use crate::kani; - #[unstable(feature = "kani", issue = "none")] mod verify { use super::*; diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index 64d43c394e2b2..48f0e2d4dc24b 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -558,8 +558,8 @@ macro_rules! uint_impl { without modifying the original"] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - #[kani::requires(!self.overflowing_add(rhs).1)] - #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] + #[requires(!self.overflowing_add(rhs).1)] + #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] pub const unsafe fn unchecked_add(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, From 4858a531de50d0a2654ab6cbf66461b78ef210a9 Mon Sep 17 00:00:00 2001 From: yew005 Date: Fri, 20 Sep 2024 13:43:34 -0700 Subject: [PATCH 13/25] Fix comment --- library/core/src/num/mod.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 28aeb1b897149..4dbce78394d9e 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1599,8 +1599,8 @@ mod verify { // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total // // Target contracts: - // #[kani::requires(!self.overflowing_add(rhs).1)] - // #[kani::ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] + // #[requires(!self.overflowing_add(rhs).1)] + // #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // // Target function: // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self From d99844df3a9f0bb24d973e250122eedd3542924e Mon Sep 17 00:00:00 2001 From: yew005 Date: Tue, 24 Sep 2024 14:16:46 -0700 Subject: [PATCH 14/25] Remove ensures contracts && Undo formatting on existing code --- library/core/src/num/int_macros.rs | 1 - library/core/src/num/mod.rs | 5 +---- library/core/src/num/uint_macros.rs | 1 - 3 files changed, 1 insertion(+), 6 deletions(-) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index fa0c9c98dde74..fa3e4cef9bcb4 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -512,7 +512,6 @@ macro_rules! int_impl { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires(!self.overflowing_add(rhs).1)] - #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] pub const unsafe fn unchecked_add(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 4dbce78394d9e..526b8895e89cb 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1401,10 +1401,7 @@ const fn from_str_radix_panic_ct(_radix: u32) -> ! { #[track_caller] fn from_str_radix_panic_rt(radix: u32) -> ! { - panic!( - "from_str_radix_int: must lie in the range `[2, 36]` - found {}", - radix - ); + panic!("from_str_radix_int: must lie in the range `[2, 36]` - found {}", radix); } #[cfg_attr(not(feature = "panic_immediate_abort"), inline(never))] diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index 48f0e2d4dc24b..b12d82bdc720c 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -559,7 +559,6 @@ macro_rules! uint_impl { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires(!self.overflowing_add(rhs).1)] - #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] pub const unsafe fn unchecked_add(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, From fbcf49e631daa53e111bf750c1d3c916921a016a Mon Sep 17 00:00:00 2001 From: yew005 Date: Tue, 24 Sep 2024 14:28:59 -0700 Subject: [PATCH 15/25] Add {isize, usize}::unchecked_add harnesses --- library/core/src/num/mod.rs | 23 +++++++++++++++++++++-- 1 file changed, 21 insertions(+), 2 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 526b8895e89cb..159062099dbc0 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1593,11 +1593,10 @@ mod verify { // `unchecked_add` proofs // // Target types: - // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total + // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total // // Target contracts: // #[requires(!self.overflowing_add(rhs).1)] - // #[ensures(|ret| *ret >= $SelfT::MIN && *ret <= $SelfT::MAX)] // // Target function: // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self @@ -1651,6 +1650,16 @@ mod verify { } } + #[kani::proof_for_contract(isize::unchecked_add)] + pub fn check_unchecked_add_isize() { + let num1: isize = kani::any::(); + let num2: isize = kani::any::(); + + unsafe { + num1.unchecked_add(num2); + } + } + #[kani::proof_for_contract(u8::unchecked_add)] pub fn check_unchecked_add_u8() { let num1: u8 = kani::any::(); @@ -1700,4 +1709,14 @@ mod verify { num1.unchecked_add(num2); } } + + #[kani::proof_for_contract(usize::unchecked_add)] + pub fn check_unchecked_add_usize() { + let num1: usize = kani::any::(); + let num2: usize = kani::any::(); + + unsafe { + num1.unchecked_add(num2); + } + } } From 54a03ef0c9c301d7d3aa06a82d75e305c3ee76bf Mon Sep 17 00:00:00 2001 From: yew005 Date: Fri, 27 Sep 2024 15:09:57 -0700 Subject: [PATCH 16/25] Add harness generation macros for unchecked methods && Update unchecked_add harnesses --- library/core/src/num/mod.rs | 169 +++++++++++------------------------- 1 file changed, 52 insertions(+), 117 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 159062099dbc0..8e31a0f434981 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1586,137 +1586,72 @@ from_str_radix_size_impl! { i32 isize, u32 usize } #[cfg(target_pointer_width = "64")] from_str_radix_size_impl! { i64 isize, u64 usize } +#[cfg(kani)] #[unstable(feature = "kani", issue = "none")] mod verify { use super::*; - // `unchecked_add` proofs - // - // Target types: - // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total - // - // Target contracts: - // #[requires(!self.overflowing_add(rhs).1)] - // - // Target function: - // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self - #[kani::proof_for_contract(i8::unchecked_add)] - pub fn check_unchecked_add_i8() { - let num1: i8 = kani::any::(); - let num2: i8 = kani::any::(); - - unsafe { - num1.unchecked_add(num2); - } - } - - #[kani::proof_for_contract(i16::unchecked_add)] - pub fn check_unchecked_add_i16() { - let num1: i16 = kani::any::(); - let num2: i16 = kani::any::(); - - unsafe { - num1.unchecked_add(num2); - } - } - - #[kani::proof_for_contract(i32::unchecked_add)] - pub fn check_unchecked_add_i32() { - let num1: i32 = kani::any::(); - let num2: i32 = kani::any::(); - - unsafe { - num1.unchecked_add(num2); - } - } - - #[kani::proof_for_contract(i64::unchecked_add)] - pub fn check_unchecked_add_i64() { - let num1: i64 = kani::any::(); - let num2: i64 = kani::any::(); - - unsafe { - num1.unchecked_add(num2); - } - } - - #[kani::proof_for_contract(i128::unchecked_add)] - pub fn check_unchecked_add_i128() { - let num1: i128 = kani::any::(); - let num2: i128 = kani::any::(); - - unsafe { - num1.unchecked_add(num2); - } - } - - #[kani::proof_for_contract(isize::unchecked_add)] - pub fn check_unchecked_add_isize() { - let num1: isize = kani::any::(); - let num2: isize = kani::any::(); + macro_rules! generate_unchecked_math_harness { + ($type:ty, $method:ident, $harness_name:ident) => { + #[kani::proof_for_contract($type::$method)] + pub fn $harness_name() { + let num1: $type = kani::any::<$type>(); + let num2: $type = kani::any::<$type>(); - unsafe { - num1.unchecked_add(num2); - } - } - - #[kani::proof_for_contract(u8::unchecked_add)] - pub fn check_unchecked_add_u8() { - let num1: u8 = kani::any::(); - let num2: u8 = kani::any::(); - - unsafe { - num1.unchecked_add(num2); - } - } - - #[kani::proof_for_contract(u16::unchecked_add)] - pub fn check_unchecked_add_u16() { - let num1: u16 = kani::any::(); - let num2: u16 = kani::any::(); - - unsafe { - num1.unchecked_add(num2); - } - } - - #[kani::proof_for_contract(u32::unchecked_add)] - pub fn check_unchecked_add_u32() { - let num1: u32 = kani::any::(); - let num2: u32 = kani::any::(); - - unsafe { - num1.unchecked_add(num2); + unsafe { + num1.$method(num2); + } + } } } - #[kani::proof_for_contract(u64::unchecked_add)] - pub fn check_unchecked_add_u64() { - let num1: u64 = kani::any::(); - let num2: u64 = kani::any::(); + macro_rules! generate_unchecked_shift_harness { + ($type:ty, $method:ident, $harness_name:ident) => { + #[kani::proof_for_contract($type::$method)] + pub fn $harness_name() { + let num1: $type = kani::any::<$type>(); + let num2: u32 = kani::any::(); - unsafe { - num1.unchecked_add(num2); + unsafe { + num1.$method(num2); + } + } } } - #[kani::proof_for_contract(u128::unchecked_add)] - pub fn check_unchecked_add_u128() { - let num1: u128 = kani::any::(); - let num2: u128 = kani::any::(); + macro_rules! generate_unchecked_neg_harness { + ($type:ty, $method:ident, $harness_name:ident) => { + #[kani::proof_for_contract($type::$method)] + pub fn $harness_name() { + let num1: $type = kani::any::<$type>(); - unsafe { - num1.unchecked_add(num2); + unsafe { + num1.$method(); + } + } } } - #[kani::proof_for_contract(usize::unchecked_add)] - pub fn check_unchecked_add_usize() { - let num1: usize = kani::any::(); - let num2: usize = kani::any::(); - - unsafe { - num1.unchecked_add(num2); - } - } + // `unchecked_add` proofs + // + // Target types: + // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total + // + // Target contracts: + // #[requires(!self.overflowing_add(rhs).1)] + // + // Target function: + // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self + generate_unchecked_math_harness!(i8, unchecked_add, checked_unchecked_add_i8); + generate_unchecked_math_harness!(i16, unchecked_add, checked_unchecked_add_i16); + generate_unchecked_math_harness!(i32, unchecked_add, checked_unchecked_add_i32); + generate_unchecked_math_harness!(i64, unchecked_add, checked_unchecked_add_i64); + generate_unchecked_math_harness!(i128, unchecked_add, checked_unchecked_add_i128); + generate_unchecked_math_harness!(isize, unchecked_add, checked_unchecked_add_isize); + generate_unchecked_math_harness!(u8, unchecked_add, checked_unchecked_add_u8); + generate_unchecked_math_harness!(u16, unchecked_add, checked_unchecked_add_u16); + generate_unchecked_math_harness!(u32, unchecked_add, checked_unchecked_add_u32); + generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64); + generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128); + generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize); } From 8ee56826478518f03a622803455c52af2f85f6ba Mon Sep 17 00:00:00 2001 From: yew005 Date: Sun, 29 Sep 2024 19:47:07 -0700 Subject: [PATCH 17/25] Remove unused import safety::ensures --- library/core/src/num/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 8e31a0f434981..51bc33b7b47a4 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -5,7 +5,7 @@ use crate::str::FromStr; use crate::ub_checks::assert_unsafe_precondition; use crate::{ascii, intrinsics, mem}; -use safety::{ensures, requires}; +use safety::requires; #[cfg(kani)] use crate::kani; From 02d706a2f818cdacee696763b4185458a2fc90e5 Mon Sep 17 00:00:00 2001 From: Rajath Kotyal <53811196+rajathkotyal@users.noreply.github.com> Date: Sun, 29 Sep 2024 21:15:21 -0700 Subject: [PATCH 18/25] unchecked_mul and unchecked_shr proofs (#7) * Added harnesses for unchecked multiplication (`unchecked_mul`) and shift right (`unchecked_shr`) * Added a macro and input limits for multiplication proofs * Reduced duplicity in code by using macros to generate proof harnesses --- library/core/src/num/int_macros.rs | 2 + library/core/src/num/mod.rs | 72 ++++++++++++++++++++++++++++- library/core/src/num/uint_macros.rs | 2 + 3 files changed, 75 insertions(+), 1 deletion(-) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index fa3e4cef9bcb4..a46e653de2bd0 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -816,6 +816,7 @@ macro_rules! int_impl { without modifying the original"] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(!self.overflowing_mul(rhs).1)] pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, @@ -1424,6 +1425,7 @@ macro_rules! int_impl { #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[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. pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self { assert_unsafe_precondition!( check_language_ub, diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 51bc33b7b47a4..54e90d1bff0ff 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1605,19 +1605,39 @@ mod verify { } } + macro_rules! generate_unchecked_mul_harness { + ($type:ty, $method:ident, $harness_name:ident, $min:expr, $max:expr) => { + #[kani::proof_for_contract($type::$method)] + pub fn $harness_name() { + let num1: $type = kani::any(); + let num2: $type = kani::any(); + + // Limit the values of num1 and num2 to the specified range for multiplication + kani::assume(num1 >= $min && num1 <= $max); + kani::assume(num2 >= $min && num2 <= $max); + + unsafe { + num1.$method(num2); + } + } + } + } + + macro_rules! generate_unchecked_shift_harness { ($type:ty, $method:ident, $harness_name:ident) => { #[kani::proof_for_contract($type::$method)] pub fn $harness_name() { let num1: $type = kani::any::<$type>(); let num2: u32 = kani::any::(); - + unsafe { num1.$method(num2); } } } } + macro_rules! generate_unchecked_neg_harness { ($type:ty, $method:ident, $harness_name:ident) => { @@ -1654,4 +1674,54 @@ mod verify { generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64); generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128); generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize); + + // unchecked_mul proofs + // + // Target types: + // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total + // + // Target contracts: + // #[requires(!self.overflowing_mul(rhs).1)] + // + // Target function: + // pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self + // exponential state spaces for 32,64 and 128, hence provided limited range for verification. + generate_unchecked_math_harness!(i8, unchecked_mul, checked_unchecked_mul_i8); + generate_unchecked_math_harness!(i16, unchecked_mul, checked_unchecked_mul_i16); + generate_unchecked_mul_harness!(i32, unchecked_mul, checked_unchecked_mul_i32, -10_000i32, 10_000i32); + generate_unchecked_mul_harness!(i64, unchecked_mul, checked_unchecked_mul_i64, -1_000i64, 1_000i64); + generate_unchecked_mul_harness!(i128, unchecked_mul, checked_unchecked_mul_i128, -1_000_000_000_000_000i128, 1_000_000_000_000_000i128); + generate_unchecked_mul_harness!(isize, unchecked_mul, checked_unchecked_mul_isize, -100_000isize, 100_000isize); + generate_unchecked_math_harness!(u8, unchecked_mul, checked_unchecked_mul_u8); + generate_unchecked_math_harness!(u16, unchecked_mul, checked_unchecked_mul_u16); + generate_unchecked_mul_harness!(u32, unchecked_mul, checked_unchecked_mul_u32, 0u32, 20_000u32); + generate_unchecked_mul_harness!(u64, unchecked_mul, checked_unchecked_mul_u64, 0u64, 2_000u64); + generate_unchecked_mul_harness!(u128, unchecked_mul, checked_unchecked_mul_u128, 0u128, 1_000_000_000_000_000u128); + generate_unchecked_mul_harness!(usize, unchecked_mul, checked_unchecked_mul_usize, 0usize, 100_000usize); + + + // unchecked_shr proofs + // + // Target types: + // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total + // + // Target contracts: + // #[requires(rhs < <$ActualT>::BITS)] + // + // Target function: + // pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self + generate_unchecked_shift_harness!(i8, unchecked_shr, checked_unchecked_shr_i8); + generate_unchecked_shift_harness!(i16, unchecked_shr, checked_unchecked_shr_i16); + generate_unchecked_shift_harness!(i32, unchecked_shr, checked_unchecked_shr_i32); + generate_unchecked_shift_harness!(i64, unchecked_shr, checked_unchecked_shr_i64); + generate_unchecked_shift_harness!(i128, unchecked_shr, checked_unchecked_shr_i128); + generate_unchecked_shift_harness!(isize, unchecked_shr, checked_unchecked_shr_isize); + generate_unchecked_shift_harness!(u8, unchecked_shr, checked_unchecked_shr_u8); + generate_unchecked_shift_harness!(u16, unchecked_shr, checked_unchecked_shr_u16); + generate_unchecked_shift_harness!(u32, unchecked_shr, checked_unchecked_shr_u32); + generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64); + generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128); + generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize); + } + } } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index b12d82bdc720c..8706ed8bd6d5f 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -908,6 +908,7 @@ macro_rules! uint_impl { without modifying the original"] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(!self.overflowing_mul(rhs).1)] pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, @@ -1613,6 +1614,7 @@ macro_rules! uint_impl { #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[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. pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self { assert_unsafe_precondition!( check_language_ub, From dce9e831fca8c3109a565ef1d8423ded11eac118 Mon Sep 17 00:00:00 2001 From: yew005 Date: Sun, 29 Sep 2024 21:21:41 -0700 Subject: [PATCH 19/25] Add comments. Fix spacing --- library/core/src/num/mod.rs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 54e90d1bff0ff..3a83e75b74288 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1591,6 +1591,9 @@ from_str_radix_size_impl! { i64 isize, u64 usize } mod verify { use super::*; + // Verify `unchecked_{add, sub, mul}` + // However, `unchecked_mul` harnesses have bad performance, so + // recommend to use generate_unchecked_mul_harness! to set input limits macro_rules! generate_unchecked_math_harness { ($type:ty, $method:ident, $harness_name:ident) => { #[kani::proof_for_contract($type::$method)] @@ -1605,14 +1608,15 @@ mod verify { } } + // Improve unchecked_mul performance for {32, 64, 128}-bit integer types + // by adding upper and lower limits for inputs macro_rules! generate_unchecked_mul_harness { ($type:ty, $method:ident, $harness_name:ident, $min:expr, $max:expr) => { #[kani::proof_for_contract($type::$method)] pub fn $harness_name() { - let num1: $type = kani::any(); - let num2: $type = kani::any(); - - // Limit the values of num1 and num2 to the specified range for multiplication + let num1: $type = kani::any::<$type>(); + let num2: $type = kani::any::<$type>(); + kani::assume(num1 >= $min && num1 <= $max); kani::assume(num2 >= $min && num2 <= $max); @@ -1622,8 +1626,8 @@ mod verify { } } } - + // Verify `unchecked_{shl, shr}` macro_rules! generate_unchecked_shift_harness { ($type:ty, $method:ident, $harness_name:ident) => { #[kani::proof_for_contract($type::$method)] @@ -1637,7 +1641,6 @@ mod verify { } } } - macro_rules! generate_unchecked_neg_harness { ($type:ty, $method:ident, $harness_name:ident) => { @@ -1699,7 +1702,6 @@ mod verify { generate_unchecked_mul_harness!(u128, unchecked_mul, checked_unchecked_mul_u128, 0u128, 1_000_000_000_000_000u128); generate_unchecked_mul_harness!(usize, unchecked_mul, checked_unchecked_mul_usize, 0usize, 100_000usize); - // unchecked_shr proofs // // Target types: @@ -1722,6 +1724,4 @@ mod verify { generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64); generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128); generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize); - } - } } From 3880fc7b0f50b719b934eedc5497e7d59e1687e3 Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Wed, 2 Oct 2024 12:58:43 -0700 Subject: [PATCH 20/25] Revert "Add comments. Fix spacing" This reverts commit dce9e831fca8c3109a565ef1d8423ded11eac118. --- library/core/src/num/mod.rs | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 3a83e75b74288..54e90d1bff0ff 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1591,9 +1591,6 @@ from_str_radix_size_impl! { i64 isize, u64 usize } mod verify { use super::*; - // Verify `unchecked_{add, sub, mul}` - // However, `unchecked_mul` harnesses have bad performance, so - // recommend to use generate_unchecked_mul_harness! to set input limits macro_rules! generate_unchecked_math_harness { ($type:ty, $method:ident, $harness_name:ident) => { #[kani::proof_for_contract($type::$method)] @@ -1608,15 +1605,14 @@ mod verify { } } - // Improve unchecked_mul performance for {32, 64, 128}-bit integer types - // by adding upper and lower limits for inputs macro_rules! generate_unchecked_mul_harness { ($type:ty, $method:ident, $harness_name:ident, $min:expr, $max:expr) => { #[kani::proof_for_contract($type::$method)] pub fn $harness_name() { - let num1: $type = kani::any::<$type>(); - let num2: $type = kani::any::<$type>(); - + let num1: $type = kani::any(); + let num2: $type = kani::any(); + + // Limit the values of num1 and num2 to the specified range for multiplication kani::assume(num1 >= $min && num1 <= $max); kani::assume(num2 >= $min && num2 <= $max); @@ -1626,8 +1622,8 @@ mod verify { } } } + - // Verify `unchecked_{shl, shr}` macro_rules! generate_unchecked_shift_harness { ($type:ty, $method:ident, $harness_name:ident) => { #[kani::proof_for_contract($type::$method)] @@ -1641,6 +1637,7 @@ mod verify { } } } + macro_rules! generate_unchecked_neg_harness { ($type:ty, $method:ident, $harness_name:ident) => { @@ -1702,6 +1699,7 @@ mod verify { generate_unchecked_mul_harness!(u128, unchecked_mul, checked_unchecked_mul_u128, 0u128, 1_000_000_000_000_000u128); generate_unchecked_mul_harness!(usize, unchecked_mul, checked_unchecked_mul_usize, 0usize, 100_000usize); + // unchecked_shr proofs // // Target types: @@ -1724,4 +1722,6 @@ mod verify { generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64); generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128); generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize); + } + } } From 781cb87ed6976b255bc7fffa5227d2cf815ede6a Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Wed, 2 Oct 2024 12:58:47 -0700 Subject: [PATCH 21/25] Revert "unchecked_mul and unchecked_shr proofs (#7)" This reverts commit 02d706a2f818cdacee696763b4185458a2fc90e5. --- library/core/src/num/int_macros.rs | 2 - library/core/src/num/mod.rs | 72 +---------------------------- library/core/src/num/uint_macros.rs | 2 - 3 files changed, 1 insertion(+), 75 deletions(-) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index a46e653de2bd0..fa3e4cef9bcb4 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -816,7 +816,6 @@ macro_rules! int_impl { without modifying the original"] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - #[requires(!self.overflowing_mul(rhs).1)] pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, @@ -1425,7 +1424,6 @@ macro_rules! int_impl { #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - #[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. pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self { assert_unsafe_precondition!( check_language_ub, diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 54e90d1bff0ff..51bc33b7b47a4 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1605,39 +1605,19 @@ mod verify { } } - macro_rules! generate_unchecked_mul_harness { - ($type:ty, $method:ident, $harness_name:ident, $min:expr, $max:expr) => { - #[kani::proof_for_contract($type::$method)] - pub fn $harness_name() { - let num1: $type = kani::any(); - let num2: $type = kani::any(); - - // Limit the values of num1 and num2 to the specified range for multiplication - kani::assume(num1 >= $min && num1 <= $max); - kani::assume(num2 >= $min && num2 <= $max); - - unsafe { - num1.$method(num2); - } - } - } - } - - macro_rules! generate_unchecked_shift_harness { ($type:ty, $method:ident, $harness_name:ident) => { #[kani::proof_for_contract($type::$method)] pub fn $harness_name() { let num1: $type = kani::any::<$type>(); let num2: u32 = kani::any::(); - + unsafe { num1.$method(num2); } } } } - macro_rules! generate_unchecked_neg_harness { ($type:ty, $method:ident, $harness_name:ident) => { @@ -1674,54 +1654,4 @@ mod verify { generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64); generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128); generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize); - - // unchecked_mul proofs - // - // Target types: - // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 12 types in total - // - // Target contracts: - // #[requires(!self.overflowing_mul(rhs).1)] - // - // Target function: - // pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self - // exponential state spaces for 32,64 and 128, hence provided limited range for verification. - generate_unchecked_math_harness!(i8, unchecked_mul, checked_unchecked_mul_i8); - generate_unchecked_math_harness!(i16, unchecked_mul, checked_unchecked_mul_i16); - generate_unchecked_mul_harness!(i32, unchecked_mul, checked_unchecked_mul_i32, -10_000i32, 10_000i32); - generate_unchecked_mul_harness!(i64, unchecked_mul, checked_unchecked_mul_i64, -1_000i64, 1_000i64); - generate_unchecked_mul_harness!(i128, unchecked_mul, checked_unchecked_mul_i128, -1_000_000_000_000_000i128, 1_000_000_000_000_000i128); - generate_unchecked_mul_harness!(isize, unchecked_mul, checked_unchecked_mul_isize, -100_000isize, 100_000isize); - generate_unchecked_math_harness!(u8, unchecked_mul, checked_unchecked_mul_u8); - generate_unchecked_math_harness!(u16, unchecked_mul, checked_unchecked_mul_u16); - generate_unchecked_mul_harness!(u32, unchecked_mul, checked_unchecked_mul_u32, 0u32, 20_000u32); - generate_unchecked_mul_harness!(u64, unchecked_mul, checked_unchecked_mul_u64, 0u64, 2_000u64); - generate_unchecked_mul_harness!(u128, unchecked_mul, checked_unchecked_mul_u128, 0u128, 1_000_000_000_000_000u128); - generate_unchecked_mul_harness!(usize, unchecked_mul, checked_unchecked_mul_usize, 0usize, 100_000usize); - - - // unchecked_shr proofs - // - // Target types: - // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total - // - // Target contracts: - // #[requires(rhs < <$ActualT>::BITS)] - // - // Target function: - // pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self - generate_unchecked_shift_harness!(i8, unchecked_shr, checked_unchecked_shr_i8); - generate_unchecked_shift_harness!(i16, unchecked_shr, checked_unchecked_shr_i16); - generate_unchecked_shift_harness!(i32, unchecked_shr, checked_unchecked_shr_i32); - generate_unchecked_shift_harness!(i64, unchecked_shr, checked_unchecked_shr_i64); - generate_unchecked_shift_harness!(i128, unchecked_shr, checked_unchecked_shr_i128); - generate_unchecked_shift_harness!(isize, unchecked_shr, checked_unchecked_shr_isize); - generate_unchecked_shift_harness!(u8, unchecked_shr, checked_unchecked_shr_u8); - generate_unchecked_shift_harness!(u16, unchecked_shr, checked_unchecked_shr_u16); - generate_unchecked_shift_harness!(u32, unchecked_shr, checked_unchecked_shr_u32); - generate_unchecked_shift_harness!(u64, unchecked_shr, checked_unchecked_shr_u64); - generate_unchecked_shift_harness!(u128, unchecked_shr, checked_unchecked_shr_u128); - generate_unchecked_shift_harness!(usize, unchecked_shr, checked_unchecked_shr_usize); - } - } } diff --git a/library/core/src/num/uint_macros.rs b/library/core/src/num/uint_macros.rs index 8706ed8bd6d5f..b12d82bdc720c 100644 --- a/library/core/src/num/uint_macros.rs +++ b/library/core/src/num/uint_macros.rs @@ -908,7 +908,6 @@ macro_rules! uint_impl { without modifying the original"] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - #[requires(!self.overflowing_mul(rhs).1)] pub const unsafe fn unchecked_mul(self, rhs: Self) -> Self { assert_unsafe_precondition!( check_language_ub, @@ -1614,7 +1613,6 @@ macro_rules! uint_impl { #[rustc_const_unstable(feature = "unchecked_shifts", issue = "85122")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - #[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. pub const unsafe fn unchecked_shr(self, rhs: u32) -> Self { assert_unsafe_precondition!( check_language_ub, From 1f0f5839b8db9988749a2345ea03ec4de94fa7d1 Mon Sep 17 00:00:00 2001 From: yew005 Date: Thu, 3 Oct 2024 10:45:59 -0700 Subject: [PATCH 22/25] Add unchecked_neg contracts & harnesses --- library/core/src/num/int_macros.rs | 1 + library/core/src/num/mod.rs | 23 ++++++++++++++++++++--- 2 files changed, 21 insertions(+), 3 deletions(-) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index fa3e4cef9bcb4..2be9884d41e93 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -1165,6 +1165,7 @@ macro_rules! int_impl { #[rustc_const_unstable(feature = "unchecked_neg", issue = "85122")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires(!self.overflowing_neg().1)] pub const unsafe fn unchecked_neg(self) -> Self { assert_unsafe_precondition!( check_language_ub, diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 51bc33b7b47a4..de27a52d0eb01 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1620,13 +1620,13 @@ mod verify { } macro_rules! generate_unchecked_neg_harness { - ($type:ty, $method:ident, $harness_name:ident) => { - #[kani::proof_for_contract($type::$method)] + ($type:ty, $harness_name:ident) => { + #[kani::proof_for_contract($type::unchecked_neg)] pub fn $harness_name() { let num1: $type = kani::any::<$type>(); unsafe { - num1.$method(); + num1.unchecked_neg(); } } } @@ -1654,4 +1654,21 @@ mod verify { generate_unchecked_math_harness!(u64, unchecked_add, checked_unchecked_add_u64); generate_unchecked_math_harness!(u128, unchecked_add, checked_unchecked_add_u128); generate_unchecked_math_harness!(usize, unchecked_add, checked_unchecked_add_usize); + + // `unchecked_neg` proofs + // + // Target types: + // i{8,16,32,64,128, size} -- 6 types in total + // + // Target contracts: + // #[requires(!self.overflowing_neg().1)] + // + // Target function: + // pub const unsafe fn unchecked_neg(self) -> Self + generate_unchecked_neg_harness!(i8, checked_unchecked_neg_i8); + generate_unchecked_neg_harness!(i16, checked_unchecked_neg_i16); + generate_unchecked_neg_harness!(i32, checked_unchecked_neg_i32); + generate_unchecked_neg_harness!(i64, checked_unchecked_neg_i64); + generate_unchecked_neg_harness!(i128, checked_unchecked_neg_i128); + generate_unchecked_neg_harness!(isize, checked_unchecked_neg_isize); } From ef61321725e7f06fa5fb73b80e43d5a2e607613d Mon Sep 17 00:00:00 2001 From: rajathmCMU Date: Mon, 7 Oct 2024 11:52:16 -0700 Subject: [PATCH 23/25] fixed comments --- library/core/src/num/mod.rs | 18 ++++++++---------- 1 file changed, 8 insertions(+), 10 deletions(-) diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 5086d952489a6..867a0f09329b5 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1661,11 +1661,10 @@ mod verify { // `unchecked_add` proofs // // Target types: - // i{8,16,32,64,128} and u{8,16,32,64,128} -- 10 types in total + // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total // // Target contracts: - //#[requires(!self.overflowing_sub(rhs).1)] // Preconditions: No overflow should occur - //#[ensures(|ret| *ret >= Self::MIN && *ret <= Self::MAX)] // Postconditions: Result must be within valid bounds + // #[requires(!self.overflowing_add(rhs).1)] // Preconditions: No overflow should occur // // Target function: // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self @@ -1685,7 +1684,7 @@ mod verify { // `unchecked_neg` proofs // // Target types: - // i{8,16,32,64,128, size} -- 6 types in total + // i{8,16,32,64,128,size} -- 6 types in total // // Target contracts: // #[requires(!self.overflowing_neg().1)] @@ -1702,8 +1701,8 @@ mod verify { // unchecked_mul proofs // // Target types: - // i{8,16,32,64,128, size} and u{8,16,32,64,128, size} -- 36 types in total - // + // 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. + // Total types of checks including intervals -- 36 // Target contracts: // #[requires(!self.overflowing_mul(rhs).1)] // @@ -1800,11 +1799,10 @@ mod verify { // `unchecked_shl` proofs // // Target types: - // i{8,16,32,64,128} and u{8,16,32,64,128} -- 12 types in total + // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total // // Target contracts: // #[requires(shift < Self::BITS)] - // #[ensures(|ret| *ret == self << shift)] // // Target function: // pub const unsafe fn unchecked_shl(self, shift: u32) -> Self @@ -1826,10 +1824,10 @@ mod verify { // `unchecked_sub` proofs // // Target types: - // i{8,16,32,64,128} and u{8,16,32,64,128} -- 12 types in total + // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total // // Target contracts: - // #[requires(!self.overflowing_sub(rhs).1)] // Preconditions: No overflow should occur + // #[requires(!self.overflowing_sub(rhs).1)] // // Target function: // pub const unsafe fn unchecked_sub(self, rhs: Self) -> Self From 5e1c45f639a36915750246879b1313202dc55364 Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Mon, 7 Oct 2024 17:25:42 -0700 Subject: [PATCH 24/25] Fix unchecked_neg precondition && Fix comments --- library/core/src/num/int_macros.rs | 2 +- library/core/src/num/mod.rs | 8 ++++++-- 2 files changed, 7 insertions(+), 3 deletions(-) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index 98ff857e61dc7..b7e7b2820b7be 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -1167,7 +1167,7 @@ macro_rules! int_impl { #[rustc_const_unstable(feature = "unchecked_neg", issue = "85122")] #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces - #[requires(!self.overflowing_neg().1)] + #[requires(self != $SelfT::MIN)] pub const unsafe fn unchecked_neg(self) -> Self { assert_unsafe_precondition!( check_language_ub, diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 867a0f09329b5..70218aea9cf2b 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -1664,7 +1664,8 @@ mod verify { // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total // // Target contracts: - // #[requires(!self.overflowing_add(rhs).1)] // Preconditions: No overflow should occur + // Preconditions: No overflow should occur + // #[requires(!self.overflowing_add(rhs).1)] // // Target function: // pub const unsafe fn unchecked_add(self, rhs: Self) -> Self @@ -1687,7 +1688,7 @@ mod verify { // i{8,16,32,64,128,size} -- 6 types in total // // Target contracts: - // #[requires(!self.overflowing_neg().1)] + // #[requires(self != $SelfT::MIN)] // // Target function: // pub const unsafe fn unchecked_neg(self) -> Self @@ -1703,7 +1704,9 @@ mod verify { // Target types: // 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. // Total types of checks including intervals -- 36 + // // Target contracts: + // Preconditions: No overflow should occur // #[requires(!self.overflowing_mul(rhs).1)] // // Target function: @@ -1827,6 +1830,7 @@ mod verify { // i{8,16,32,64,128,size} and u{8,16,32,64,128,size} -- 12 types in total // // Target contracts: + // Preconditions: No overflow should occur // #[requires(!self.overflowing_sub(rhs).1)] // // Target function: From cb99f76080b988f418d5da87ce3ed514e5efdc9c Mon Sep 17 00:00:00 2001 From: Yenyun035 Date: Mon, 7 Oct 2024 18:05:05 -0700 Subject: [PATCH 25/25] Add ensures for unchecked_neg && Fix import --- library/core/src/num/int_macros.rs | 1 + library/core/src/num/mod.rs | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/library/core/src/num/int_macros.rs b/library/core/src/num/int_macros.rs index b7e7b2820b7be..c84087172974a 100644 --- a/library/core/src/num/int_macros.rs +++ b/library/core/src/num/int_macros.rs @@ -1168,6 +1168,7 @@ macro_rules! int_impl { #[inline(always)] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[requires(self != $SelfT::MIN)] + #[ensures(|result| *result == -self)] pub const unsafe fn unchecked_neg(self) -> Self { assert_unsafe_precondition!( check_language_ub, diff --git a/library/core/src/num/mod.rs b/library/core/src/num/mod.rs index 70218aea9cf2b..e8b7130995831 100644 --- a/library/core/src/num/mod.rs +++ b/library/core/src/num/mod.rs @@ -5,7 +5,7 @@ use crate::str::FromStr; use crate::ub_checks::assert_unsafe_precondition; use crate::{ascii, intrinsics, mem}; -use safety::requires; +use safety::{requires, ensures}; #[cfg(kani)] use crate::kani;