From 03c8ef6e82ddb486841dc50c62a99b41e722d37b Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 23 Aug 2024 11:36:54 -0400 Subject: [PATCH 01/12] align offset contracts --- library/core/src/ptr/mod.rs | 63 +++++++++++++++++++++++++++++++++++++ 1 file changed, 63 insertions(+) diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index 7fb8eae521fbf..e6a2296a8af22 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -1884,6 +1884,20 @@ pub unsafe fn write_volatile(dst: *mut T, src: T) { /// /// Any questions go to @nagisa. #[lang = "align_offset"] +#[safety::requires(a.is_power_of_two())] +// If T is a ZST, then answer should either be 0 or usize::MAX +#[safety::ensures(|result| + mem::size_of::() != 0 || (p.addr() % a == 0 && *result == 0) || (p.addr() % a != 0 && *result == usize::MAX) +)] +#[safety::ensures(|result| { + // If T is not a ZST and p can be aligned, then applying result as an offest should produce an aligned address + mem::size_of::() == 0 || *result == usize::MAX || + { + let product = usize::wrapping_mul(*result, mem::size_of::()); + let new_addr = usize::wrapping_add(product, p.addr()); + new_addr % a == 0 + } +})] pub(crate) const unsafe fn align_offset(p: *const T, a: usize) -> usize { // FIXME(#75598): Direct use of these intrinsics improves codegen significantly at opt-level <= // 1, where the method versions of these operations are not inlined. @@ -1901,6 +1915,8 @@ pub(crate) const unsafe fn align_offset(p: *const T, a: usize) -> usiz /// /// Implementation of this function shall not panic. Ever. #[inline] + #[safety::requires(m.is_power_of_two())] + #[safety::requires(x < m)] const unsafe fn mod_inv(x: usize, m: usize) -> usize { /// Multiplicative modular inverse table modulo 2⁴ = 16. /// @@ -2388,4 +2404,51 @@ mod verify { let copy = unsafe { read_volatile(ptr) }; assert_eq!(val, copy); } + + fn check_align_offset(p: *const T) { + let a = kani::any::(); + unsafe { align_offset(p, a) }; + } + + #[kani::proof_for_contract(align_offset)] + fn check_align_offset_zst() { + let p = kani::any::() as *const (); + check_align_offset(p); + } + + #[kani::proof_for_contract(align_offset)] + fn check_align_offset_u8() { + let p = kani::any::() as *const u8; + check_align_offset(p); + } + + #[kani::proof_for_contract(align_offset)] + fn check_align_offset_u16() { + let p = kani::any::() as *const u16; + check_align_offset(p); + } + + #[kani::proof_for_contract(align_offset)] + fn check_align_offset_u32() { + let p = kani::any::() as *const u32; + check_align_offset(p); + } + + #[kani::proof_for_contract(align_offset)] + fn check_align_offset_u64() { + let p = kani::any::() as *const u64; + check_align_offset(p); + } + + #[kani::proof_for_contract(align_offset)] + fn check_align_offset_u128() { + let p = kani::any::() as *const u128; + check_align_offset(p); + } + + #[kani::proof_for_contract(align_offset)] + fn check_align_offset_4096() { + let p = kani::any::() as *const [u128; 64]; + check_align_offset(p); + } } From b3572eaba848f6da0d704506341884cb1e903b97 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 23 Aug 2024 12:13:05 -0400 Subject: [PATCH 02/12] mod_inv proof --- library/core/src/ptr/mod.rs | 57 +++++++++++++++++++++++++++++++++++++ 1 file changed, 57 insertions(+) diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index e6a2296a8af22..eef70c833113b 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -2396,6 +2396,9 @@ mod verify { use crate::fmt::Debug; use super::*; use crate::kani; + use intrinsics::{ + mul_with_overflow, unchecked_sub, wrapping_mul, wrapping_sub + }; #[kani::proof_for_contract(read_volatile)] pub fn check_read_u128() { @@ -2451,4 +2454,58 @@ mod verify { let p = kani::any::() as *const [u128; 64]; check_align_offset(p); } + + // This function lives inside align_offset, so it is not publicly accessible (hence this copy). + #[safety::requires(m.is_power_of_two())] + #[safety::requires(x < m)] + const unsafe fn mod_inv_copy(x: usize, m: usize) -> usize { + /// Multiplicative modular inverse table modulo 2⁴ = 16. + /// + /// Note, that this table does not contain values where inverse does not exist (i.e., for + /// `0⁻¹ mod 16`, `2⁻¹ mod 16`, etc.) + const INV_TABLE_MOD_16: [u8; 8] = [1, 11, 13, 7, 9, 3, 5, 15]; + /// Modulo for which the `INV_TABLE_MOD_16` is intended. + const INV_TABLE_MOD: usize = 16; + + // SAFETY: `m` is required to be a power-of-two, hence non-zero. + let m_minus_one = unsafe { unchecked_sub(m, 1) }; + let mut inverse = INV_TABLE_MOD_16[(x & (INV_TABLE_MOD - 1)) >> 1] as usize; + let mut mod_gate = INV_TABLE_MOD; + // We iterate "up" using the following formula: + // + // $$ xy ≡ 1 (mod 2ⁿ) → xy (2 - xy) ≡ 1 (mod 2²ⁿ) $$ + // + // This application needs to be applied at least until `2²ⁿ ≥ m`, at which point we can + // finally reduce the computation to our desired `m` by taking `inverse mod m`. + // + // This computation is `O(log log m)`, which is to say, that on 64-bit machines this loop + // will always finish in at most 4 iterations. + loop { + // y = y * (2 - xy) mod n + // + // Note, that we use wrapping operations here intentionally – the original formula + // uses e.g., subtraction `mod n`. It is entirely fine to do them `mod + // usize::MAX` instead, because we take the result `mod n` at the end + // anyway. + if mod_gate >= m { + break; + } + inverse = wrapping_mul(inverse, wrapping_sub(2usize, wrapping_mul(x, inverse))); + let (new_gate, overflow) = mul_with_overflow(mod_gate, mod_gate); + if overflow { + break; + } + mod_gate = new_gate; + } + inverse & m_minus_one + } + + // The specification for mod_inv states that it cannot ever panic. + // Verify that is the case, given that the function's safety preconditions are met. + #[kani::proof_for_contract(mod_inv_copy)] + fn check_mod_inv() { + let x = kani::any::(); + let m = kani::any::(); + unsafe { mod_inv_copy(x, m) }; + } } From eaeaf027734624fa1fb0463be3b7681380412f68 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 27 Aug 2024 13:21:21 -0400 Subject: [PATCH 03/12] condense zst contract for readability Co-authored-by: Michael Tautschnig --- library/core/src/ptr/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index eef70c833113b..170499e6df86f 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -1887,7 +1887,7 @@ pub unsafe fn write_volatile(dst: *mut T, src: T) { #[safety::requires(a.is_power_of_two())] // If T is a ZST, then answer should either be 0 or usize::MAX #[safety::ensures(|result| - mem::size_of::() != 0 || (p.addr() % a == 0 && *result == 0) || (p.addr() % a != 0 && *result == usize::MAX) + mem::size_of::() != 0 || if p.addr() % a == 0 { *result == 0 } else { *result == usize::MAX}) )] #[safety::ensures(|result| { // If T is not a ZST and p can be aligned, then applying result as an offest should produce an aligned address From d5c798518e0a680926620c62ca865c09047b7815 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 27 Aug 2024 13:26:46 -0400 Subject: [PATCH 04/12] contracts wip --- library/core/src/ptr/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index eef70c833113b..927cc50ac4842 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -2458,7 +2458,7 @@ mod verify { // This function lives inside align_offset, so it is not publicly accessible (hence this copy). #[safety::requires(m.is_power_of_two())] #[safety::requires(x < m)] - const unsafe fn mod_inv_copy(x: usize, m: usize) -> usize { + unsafe fn mod_inv_copy(x: usize, m: usize) -> usize { /// Multiplicative modular inverse table modulo 2⁴ = 16. /// /// Note, that this table does not contain values where inverse does not exist (i.e., for From 2e202a4bfdaab9efa59b7e8fc5484d8f05cf02cc Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 27 Aug 2024 14:59:07 -0400 Subject: [PATCH 05/12] delete extra paren --- library/core/src/ptr/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index a4a69b4962b42..cab3bf54b5938 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -1887,7 +1887,7 @@ pub unsafe fn write_volatile(dst: *mut T, src: T) { #[safety::requires(a.is_power_of_two())] // If T is a ZST, then answer should either be 0 or usize::MAX #[safety::ensures(|result| - mem::size_of::() != 0 || if p.addr() % a == 0 { *result == 0 } else { *result == usize::MAX}) + mem::size_of::() != 0 || if p.addr() % a == 0 { *result == 0 } else { *result == usize::MAX} )] #[safety::ensures(|result| { // If T is not a ZST and p can be aligned, then applying result as an offest should produce an aligned address From e6c7ae91886280f2af0100582397833c2f96ea2a Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 29 Aug 2024 09:43:36 -0400 Subject: [PATCH 06/12] format Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- library/core/src/ptr/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index cab3bf54b5938..1f9ecd9b055ee 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -1887,7 +1887,7 @@ pub unsafe fn write_volatile(dst: *mut T, src: T) { #[safety::requires(a.is_power_of_two())] // If T is a ZST, then answer should either be 0 or usize::MAX #[safety::ensures(|result| - mem::size_of::() != 0 || if p.addr() % a == 0 { *result == 0 } else { *result == usize::MAX} + mem::size_of::() != 0 || if p.addr() % a == 0 { *result == 0 } else { *result == usize::MAX } )] #[safety::ensures(|result| { // If T is not a ZST and p can be aligned, then applying result as an offest should produce an aligned address From 31abde95ef2fc77848ae542ed1149168d6d13b36 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 29 Aug 2024 09:44:32 -0400 Subject: [PATCH 07/12] fix typo Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- library/core/src/ptr/mod.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index 1f9ecd9b055ee..df1d4ab79a984 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -1890,7 +1890,7 @@ pub unsafe fn write_volatile(dst: *mut T, src: T) { mem::size_of::() != 0 || if p.addr() % a == 0 { *result == 0 } else { *result == usize::MAX } )] #[safety::ensures(|result| { - // If T is not a ZST and p can be aligned, then applying result as an offest should produce an aligned address + // If T is not a ZST and p can be aligned, then applying result as an offset should produce an aligned address mem::size_of::() == 0 || *result == usize::MAX || { let product = usize::wrapping_mul(*result, mem::size_of::()); From 0177d4f7ff86be50e4b520597eeb3b934f8809e4 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 29 Aug 2024 13:26:27 -0400 Subject: [PATCH 08/12] add contract for usize::max case --- library/core/src/ptr/mod.rs | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index df1d4ab79a984..eb64352709d55 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -1889,13 +1889,27 @@ pub unsafe fn write_volatile(dst: *mut T, src: T) { #[safety::ensures(|result| mem::size_of::() != 0 || if p.addr() % a == 0 { *result == 0 } else { *result == usize::MAX } )] +// If T is not a ZST and p cannot be aligned, return usize::MAX +// Note that this does not cover the case where a % stride != 0, +// since that requires computing their gcd, which is too expensive #[safety::ensures(|result| { - // If T is not a ZST and p can be aligned, then applying result as an offset should produce an aligned address - mem::size_of::() == 0 || *result == usize::MAX || - { - let product = usize::wrapping_mul(*result, mem::size_of::()); + let stride = mem::size_of::(); + if stride == 0 { return true; } + if a % stride == 0 && p.addr() % stride != 0 { + *result == usize::MAX + } else { + true + } +})] +// If T is not a ZST and p can be aligned, then applying result as an offset should produce an aligned address +#[safety::ensures(|result| { + let stride = mem::size_of::(); + if stride != 0 && *result != usize::MAX { + let product = usize::wrapping_mul(*result, stride); let new_addr = usize::wrapping_add(product, p.addr()); new_addr % a == 0 + } else { + true } })] pub(crate) const unsafe fn align_offset(p: *const T, a: usize) -> usize { @@ -2458,7 +2472,7 @@ mod verify { // This function lives inside align_offset, so it is not publicly accessible (hence this copy). #[safety::requires(m.is_power_of_two())] #[safety::requires(x < m)] - unsafe fn mod_inv_copy(x: usize, m: usize) -> usize { + const unsafe fn mod_inv_copy(x: usize, m: usize) -> usize { /// Multiplicative modular inverse table modulo 2⁴ = 16. /// /// Note, that this table does not contain values where inverse does not exist (i.e., for From 501ee0a8e26c786841e23e4d3665afe5768e2fb0 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 29 Aug 2024 14:06:12 -0400 Subject: [PATCH 09/12] add TODO comment for mod_inv postcondition --- library/core/src/ptr/mod.rs | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index eb64352709d55..930e3105e901d 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -2472,6 +2472,12 @@ mod verify { // This function lives inside align_offset, so it is not publicly accessible (hence this copy). #[safety::requires(m.is_power_of_two())] #[safety::requires(x < m)] + // TODO: add ensures contract to check that the answer is indeed correct + // This will require quantifiers (https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html) + // so that we can add a precondition that gcd(x, m) = 1 like so: + // ∀d, d > 0 ∧ x % d = 0 ∧ m % d = 0 → d = 1 + // With this precondition, we can then write this postcondition to check the correctness of the answer: + // #[safety::ensures(|result| wrapping_mul(*result, x) % m == 1)] const unsafe fn mod_inv_copy(x: usize, m: usize) -> usize { /// Multiplicative modular inverse table modulo 2⁴ = 16. /// From badad7e38ddb44c21132f92dae9eaa4b7961e5bc Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 29 Aug 2024 16:36:55 -0400 Subject: [PATCH 10/12] clean up ensures contract --- library/core/src/ptr/mod.rs | 49 ++++++++++++++++++++----------------- 1 file changed, 27 insertions(+), 22 deletions(-) diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index 930e3105e901d..8a71ab20da0d1 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -1885,32 +1885,37 @@ pub unsafe fn write_volatile(dst: *mut T, src: T) { /// Any questions go to @nagisa. #[lang = "align_offset"] #[safety::requires(a.is_power_of_two())] -// If T is a ZST, then answer should either be 0 or usize::MAX -#[safety::ensures(|result| - mem::size_of::() != 0 || if p.addr() % a == 0 { *result == 0 } else { *result == usize::MAX } -)] -// If T is not a ZST and p cannot be aligned, return usize::MAX -// Note that this does not cover the case where a % stride != 0, -// since that requires computing their gcd, which is too expensive #[safety::ensures(|result| { let stride = mem::size_of::(); - if stride == 0 { return true; } - if a % stride == 0 && p.addr() % stride != 0 { - *result == usize::MAX - } else { - true + // ZSTs + if stride == 0 { + if p.addr() % a == 0 { + return *result == 0; + } else { + return *result == usize::MAX; + } } -})] -// If T is not a ZST and p can be aligned, then applying result as an offset should produce an aligned address -#[safety::ensures(|result| { - let stride = mem::size_of::(); - if stride != 0 && *result != usize::MAX { - let product = usize::wrapping_mul(*result, stride); - let new_addr = usize::wrapping_add(product, p.addr()); - new_addr % a == 0 - } else { - true + + // In this case, the pointer cannot be aligned + if (a % stride == 0) && (p.addr() % stride != 0) { + return *result == usize::MAX; } + + // Checking if the answer should indeed be usize::MAX when a % stride != 0 + // requires computing gcd(a, stride), which is too expensive without + // quantifiers (https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html). + // This should be updated once quantifiers are available. + if (a % stride != 0 && *result == usize::MAX) { + return true; + } + + // If we reach this case, either: + // - a % stride == 0 and p.addr() % stride == 0, so it is definitely possible to align the pointer + // - a % stride != 0 and result != usize::MAX, so align_offset is claiming that it's possible to align the pointer + // Check that applying the returned result does indeed produce an aligned address + let product = usize::wrapping_mul(*result, stride); + let new_addr = usize::wrapping_add(product, p.addr()); + *result != usize::MAX && new_addr % a == 0 })] pub(crate) const unsafe fn align_offset(p: *const T, a: usize) -> usize { // FIXME(#75598): Direct use of these intrinsics improves codegen significantly at opt-level <= From f94f69e5cb854c4731750ae961ac339d82db10fe Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 29 Aug 2024 17:48:23 -0400 Subject: [PATCH 11/12] add TODO to move mod_inv harness --- library/core/src/ptr/mod.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index 8a71ab20da0d1..4bf84cd2d9e2e 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -2527,6 +2527,9 @@ mod verify { // The specification for mod_inv states that it cannot ever panic. // Verify that is the case, given that the function's safety preconditions are met. + + // TODO: Once https://github.com/model-checking/kani/issues/3467 is fixed, + // move this harness inside `align_offset` and delete `mod_inv_copy` #[kani::proof_for_contract(mod_inv_copy)] fn check_mod_inv() { let x = kani::any::(); From 18ff56556552da4f05f20f769f28ba223bbc6d6e Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 30 Aug 2024 13:55:00 -0400 Subject: [PATCH 12/12] add harness for non power of two --- library/core/src/ptr/mod.rs | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs index 4bf84cd2d9e2e..b70b5fc1e84dd 100644 --- a/library/core/src/ptr/mod.rs +++ b/library/core/src/ptr/mod.rs @@ -1934,8 +1934,6 @@ pub(crate) const unsafe fn align_offset(p: *const T, a: usize) -> usiz /// /// Implementation of this function shall not panic. Ever. #[inline] - #[safety::requires(m.is_power_of_two())] - #[safety::requires(x < m)] const unsafe fn mod_inv(x: usize, m: usize) -> usize { /// Multiplicative modular inverse table modulo 2⁴ = 16. /// @@ -2474,6 +2472,12 @@ mod verify { check_align_offset(p); } + #[kani::proof_for_contract(align_offset)] + fn check_align_offset_17() { + let p = kani::any::() as *const [char; 17]; + check_align_offset(p); + } + // This function lives inside align_offset, so it is not publicly accessible (hence this copy). #[safety::requires(m.is_power_of_two())] #[safety::requires(x < m)]