From 44824f175b73d098393f3afbb94dfe0d99f57e0f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 23 Jul 2024 10:49:15 +0000 Subject: [PATCH 01/11] Add harness for Alignment::new_unchecked In #33 a contract was added to `Alignment::new_unchecked`, but its verification was only implicit through `Layout`, and may be affected by future changes to the contract that was added to `Layout`. This commit remedies this by adding a separate harness just for `Alignment`. --- library/core/src/ptr/alignment.rs | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs index e5f5bf6a50313..f4f68c2bb45ee 100644 --- a/library/core/src/ptr/alignment.rs +++ b/library/core/src/ptr/alignment.rs @@ -370,3 +370,20 @@ enum AlignmentEnum { _Align1Shl62 = 1 << 62, _Align1Shl63 = 1 << 63, } + +#[cfg(kani)] +#[unstable(feature="kani", issue="none")] +mod verify { + use super::*; + + #[kani::proof_for_contract(Alignment::new_unchecked)] + pub fn check_new_unchecked() { + let a = kani::any::(); + + unsafe { + let alignment = Alignment::new_unchecked(a); + assert_eq!(alignment.as_usize(), a); + assert!(a.is_power_of_two()); + } + } +} From 25c9cca1ed49f49b9eea1e8f77e0be501066b611 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 23 Jul 2024 14:42:16 +0000 Subject: [PATCH 02/11] Combine requires clauses to avoid spurious overflow error --- library/core/src/ptr/alignment.rs | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs index f4f68c2bb45ee..7c6224f9ddbda 100644 --- a/library/core/src/ptr/alignment.rs +++ b/library/core/src/ptr/alignment.rs @@ -80,8 +80,7 @@ impl Alignment { #[unstable(feature = "ptr_alignment_type", issue = "102070")] #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")] #[inline] - #[requires(align > 0)] - #[requires((align & (align - 1)) == 0)] + #[requires(align > 0 && (align & (align - 1)) == 0)] pub const unsafe fn new_unchecked(align: usize) -> Self { #[cfg(debug_assertions)] assert_unsafe_precondition!( From e795a44db43b270da4462e9fec3d2b4bf0e8d00f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 24 Jul 2024 09:19:12 +0000 Subject: [PATCH 03/11] Add harnesses for all Alignment public functions --- library/core/src/ptr/alignment.rs | 65 ++++++++++++++++++++++++++++++- 1 file changed, 63 insertions(+), 2 deletions(-) diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs index 7c6224f9ddbda..e8b2dc7f4e7e0 100644 --- a/library/core/src/ptr/alignment.rs +++ b/library/core/src/ptr/alignment.rs @@ -1,4 +1,4 @@ -use safety::requires; +use safety::{ensures, requires}; use crate::num::NonZero; #[cfg(debug_assertions)] use crate::ub_checks::assert_unsafe_precondition; @@ -60,6 +60,7 @@ impl Alignment { #[unstable(feature = "ptr_alignment_type", issue = "102070")] #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")] #[inline] + #[ensures(|result| align.is_power_of_two() == result.is_some())] pub const fn new(align: usize) -> Option { if align.is_power_of_two() { // SAFETY: Just checked it only has one bit set @@ -81,6 +82,8 @@ impl Alignment { #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")] #[inline] #[requires(align > 0 && (align & (align - 1)) == 0)] + #[ensures(|result| result.as_usize() == align)] + #[ensures(|result| result.as_usize().is_power_of_two())] pub const unsafe fn new_unchecked(align: usize) -> Self { #[cfg(debug_assertions)] assert_unsafe_precondition!( @@ -98,6 +101,7 @@ impl Alignment { #[unstable(feature = "ptr_alignment_type", issue = "102070")] #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")] #[inline] + #[ensures(|result| result.is_power_of_two())] pub const fn as_usize(self) -> usize { self.0 as usize } @@ -106,6 +110,7 @@ impl Alignment { #[unstable(feature = "ptr_alignment_type", issue = "102070")] #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")] #[inline] + #[ensures(|result| result.get().is_power_of_two())] pub const fn as_nonzero(self) -> NonZero { // SAFETY: All the discriminants are non-zero. unsafe { NonZero::new_unchecked(self.as_usize()) } @@ -127,6 +132,7 @@ impl Alignment { #[unstable(feature = "ptr_alignment_type", issue = "102070")] #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")] #[inline] + #[ensures(|result| (*result as usize) < mem::size_of::() * 8)] pub const fn log2(self) -> u32 { self.as_nonzero().trailing_zeros() } @@ -157,6 +163,7 @@ impl Alignment { #[unstable(feature = "ptr_alignment_type", issue = "102070")] #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")] #[inline] + #[ensures(|result| *result > 0)] pub const fn mask(self) -> usize { // SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow. !(unsafe { self.as_usize().unchecked_sub(1) }) @@ -375,14 +382,68 @@ enum AlignmentEnum { mod verify { use super::*; + // pub const fn of() -> Self + #[kani::proof] + pub fn check_of_i32() { + let alignment = Alignment::of::(); + assert!(alignment.as_usize().is_power_of_two()); + } + + // pub const fn new(align: usize) -> Option + #[kani::proof_for_contract(Alignment::new)] + pub fn check_new() { + let a = kani::any::(); + let alignment_opt = Alignment::new(a); + match alignment_opt { + Some(alignment) => assert_eq!(alignment.as_usize(), a), + None => assert!(!a.is_power_of_two()) + } + } + + // pub const unsafe fn new_unchecked(align: usize) -> Self #[kani::proof_for_contract(Alignment::new_unchecked)] pub fn check_new_unchecked() { let a = kani::any::(); unsafe { let alignment = Alignment::new_unchecked(a); + assert!(alignment.as_usize() > 0); + } + } + + // pub const fn as_usize(self) -> usize + #[kani::proof_for_contract(Alignment::as_usize)] + pub fn check_as_usize() { + let a = kani::any::(); + if let Some(alignment) = Alignment::new(a) { assert_eq!(alignment.as_usize(), a); - assert!(a.is_power_of_two()); + } + } + + // pub const fn as_nonzero(self) -> NonZero + #[kani::proof_for_contract(Alignment::as_nonzero)] + pub fn check_as_nonzero() { + let a = kani::any::(); + if let Some(alignment) = Alignment::new(a) { + assert_eq!(alignment.as_nonzero().get(), a); + } + } + + // pub const fn log2(self) -> u32 + #[kani::proof_for_contract(Alignment::log2)] + pub fn check_log2() { + let a = kani::any::(); + if let Some(alignment) = Alignment::new(a) { + assert_eq!(1usize << alignment.log2(), a); + } + } + + // pub const fn mask(self) -> usize + #[kani::proof_for_contract(Alignment::mask)] + pub fn check_mask() { + let a = kani::any::(); + if let Some(alignment) = Alignment::new(a) { + assert_eq!(a & alignment.mask(), a); } } } From 9c1738c4bb31a7ac802b888f03379768ac35333a Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 5 Aug 2024 11:08:37 +0000 Subject: [PATCH 04/11] Add more clauses per feedback --- library/core/src/ptr/alignment.rs | 3 +++ 1 file changed, 3 insertions(+) diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs index e8b2dc7f4e7e0..2a33dbd6f8dee 100644 --- a/library/core/src/ptr/alignment.rs +++ b/library/core/src/ptr/alignment.rs @@ -61,6 +61,7 @@ impl Alignment { #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")] #[inline] #[ensures(|result| align.is_power_of_two() == result.is_some())] + #[ensures(|result| result.is_none() || result.unwrap().as_usize() == align)] pub const fn new(align: usize) -> Option { if align.is_power_of_two() { // SAFETY: Just checked it only has one bit set @@ -132,6 +133,7 @@ impl Alignment { #[unstable(feature = "ptr_alignment_type", issue = "102070")] #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")] #[inline] + #[requires(self.as_usize().is_power_of_two())] #[ensures(|result| (*result as usize) < mem::size_of::() * 8)] pub const fn log2(self) -> u32 { self.as_nonzero().trailing_zeros() @@ -164,6 +166,7 @@ impl Alignment { #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")] #[inline] #[ensures(|result| *result > 0)] + #[ensures(|result| *result == !(self.as_usize() -1))] pub const fn mask(self) -> usize { // SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow. !(unsafe { self.as_usize().unchecked_sub(1) }) From 7fdbc772e055d6a174cfc20897f337e0cd9f71f3 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Thu, 8 Aug 2024 09:39:46 +0000 Subject: [PATCH 05/11] Add ensures where possible --- library/core/src/ptr/alignment.rs | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs index 2a33dbd6f8dee..09dd17e8b8699 100644 --- a/library/core/src/ptr/alignment.rs +++ b/library/core/src/ptr/alignment.rs @@ -112,6 +112,7 @@ impl Alignment { #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")] #[inline] #[ensures(|result| result.get().is_power_of_two())] + #[ensures(|result| result.get() == self.as_usize())] pub const fn as_nonzero(self) -> NonZero { // SAFETY: All the discriminants are non-zero. unsafe { NonZero::new_unchecked(self.as_usize()) } @@ -135,6 +136,7 @@ impl Alignment { #[inline] #[requires(self.as_usize().is_power_of_two())] #[ensures(|result| (*result as usize) < mem::size_of::() * 8)] + #[ensures(|result| 1usize << *result == self.as_usize())] pub const fn log2(self) -> u32 { self.as_nonzero().trailing_zeros() } @@ -167,6 +169,7 @@ impl Alignment { #[inline] #[ensures(|result| *result > 0)] #[ensures(|result| *result == !(self.as_usize() -1))] + #[ensures(|result| self.as_usize() & *result == self.as_usize())] pub const fn mask(self) -> usize { // SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow. !(unsafe { self.as_usize().unchecked_sub(1) }) @@ -396,21 +399,15 @@ mod verify { #[kani::proof_for_contract(Alignment::new)] pub fn check_new() { let a = kani::any::(); - let alignment_opt = Alignment::new(a); - match alignment_opt { - Some(alignment) => assert_eq!(alignment.as_usize(), a), - None => assert!(!a.is_power_of_two()) - } + let _ = Alignment::new(a); } // pub const unsafe fn new_unchecked(align: usize) -> Self #[kani::proof_for_contract(Alignment::new_unchecked)] pub fn check_new_unchecked() { let a = kani::any::(); - unsafe { - let alignment = Alignment::new_unchecked(a); - assert!(alignment.as_usize() > 0); + let _ = Alignment::new_unchecked(a); } } @@ -428,7 +425,7 @@ mod verify { pub fn check_as_nonzero() { let a = kani::any::(); if let Some(alignment) = Alignment::new(a) { - assert_eq!(alignment.as_nonzero().get(), a); + let _ = alignment.as_nonzero(); } } @@ -437,7 +434,7 @@ mod verify { pub fn check_log2() { let a = kani::any::(); if let Some(alignment) = Alignment::new(a) { - assert_eq!(1usize << alignment.log2(), a); + let _ = alignment.log2(); } } @@ -446,7 +443,7 @@ mod verify { pub fn check_mask() { let a = kani::any::(); if let Some(alignment) = Alignment::new(a) { - assert_eq!(a & alignment.mask(), a); + let _ = alignment.mask(); } } } From 16f40c716edff6e5980469edbeb58fa43b82f0bb Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 16 Aug 2024 11:26:59 +0000 Subject: [PATCH 06/11] Try to use Arbitrary --- library/core/src/ptr/alignment.rs | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs index 09dd17e8b8699..0bd9088362aa5 100644 --- a/library/core/src/ptr/alignment.rs +++ b/library/core/src/ptr/alignment.rs @@ -388,6 +388,13 @@ enum AlignmentEnum { mod verify { use super::*; + impl kani::Arbitrary for Alignment { + fn any() -> Self { + let align = kani::any_where(|a: &usize| a.is_power_of_two()); + unsafe { mem::transmute::(align) } + } + } + // pub const fn of() -> Self #[kani::proof] pub fn check_of_i32() { @@ -423,10 +430,8 @@ mod verify { // pub const fn as_nonzero(self) -> NonZero #[kani::proof_for_contract(Alignment::as_nonzero)] pub fn check_as_nonzero() { - let a = kani::any::(); - if let Some(alignment) = Alignment::new(a) { - let _ = alignment.as_nonzero(); - } + let alignment = kani::any::(); + let _ = alignment.as_nonzero(); } // pub const fn log2(self) -> u32 From 729fbc08694261f242d45973df30bd027380b289 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 16 Aug 2024 11:40:00 +0000 Subject: [PATCH 07/11] Revert "Try to use Arbitrary" This reverts commit 16f40c716edff6e5980469edbeb58fa43b82f0bb. --- library/core/src/ptr/alignment.rs | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs index 0bd9088362aa5..09dd17e8b8699 100644 --- a/library/core/src/ptr/alignment.rs +++ b/library/core/src/ptr/alignment.rs @@ -388,13 +388,6 @@ enum AlignmentEnum { mod verify { use super::*; - impl kani::Arbitrary for Alignment { - fn any() -> Self { - let align = kani::any_where(|a: &usize| a.is_power_of_two()); - unsafe { mem::transmute::(align) } - } - } - // pub const fn of() -> Self #[kani::proof] pub fn check_of_i32() { @@ -430,8 +423,10 @@ mod verify { // pub const fn as_nonzero(self) -> NonZero #[kani::proof_for_contract(Alignment::as_nonzero)] pub fn check_as_nonzero() { - let alignment = kani::any::(); - let _ = alignment.as_nonzero(); + let a = kani::any::(); + if let Some(alignment) = Alignment::new(a) { + let _ = alignment.as_nonzero(); + } } // pub const fn log2(self) -> u32 From 974be230fd2c51bdcdcca13d27f268b43c5961aa Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 20 Aug 2024 11:43:26 +0000 Subject: [PATCH 08/11] Reapply "Try to use Arbitrary" This reverts commit 729fbc08694261f242d45973df30bd027380b289. --- library/core/src/ptr/alignment.rs | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs index 09dd17e8b8699..0bd9088362aa5 100644 --- a/library/core/src/ptr/alignment.rs +++ b/library/core/src/ptr/alignment.rs @@ -388,6 +388,13 @@ enum AlignmentEnum { mod verify { use super::*; + impl kani::Arbitrary for Alignment { + fn any() -> Self { + let align = kani::any_where(|a: &usize| a.is_power_of_two()); + unsafe { mem::transmute::(align) } + } + } + // pub const fn of() -> Self #[kani::proof] pub fn check_of_i32() { @@ -423,10 +430,8 @@ mod verify { // pub const fn as_nonzero(self) -> NonZero #[kani::proof_for_contract(Alignment::as_nonzero)] pub fn check_as_nonzero() { - let a = kani::any::(); - if let Some(alignment) = Alignment::new(a) { - let _ = alignment.as_nonzero(); - } + let alignment = kani::any::(); + let _ = alignment.as_nonzero(); } // pub const fn log2(self) -> u32 From c08b98d737ed9763d3d4fd9ef2c03770d238ed08 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 20 Aug 2024 11:48:00 +0000 Subject: [PATCH 09/11] Consistently use kani::any --- library/backtrace | 2 +- library/core/src/ptr/alignment.rs | 12 ++++-------- library/stdarch | 2 +- 3 files changed, 6 insertions(+), 10 deletions(-) diff --git a/library/backtrace b/library/backtrace index fd0aed536dd9d..72265bea21089 160000 --- a/library/backtrace +++ b/library/backtrace @@ -1 +1 @@ -Subproject commit fd0aed536dd9d6ad1511a4ab3c350409f36ee52a +Subproject commit 72265bea210891ae47bbe6d4f17b493ef0606619 diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs index 0bd9088362aa5..36063989a350c 100644 --- a/library/core/src/ptr/alignment.rs +++ b/library/core/src/ptr/alignment.rs @@ -437,18 +437,14 @@ mod verify { // pub const fn log2(self) -> u32 #[kani::proof_for_contract(Alignment::log2)] pub fn check_log2() { - let a = kani::any::(); - if let Some(alignment) = Alignment::new(a) { - let _ = alignment.log2(); - } + let alignment = kani::any::(); + let _ = alignment.log2(); } // pub const fn mask(self) -> usize #[kani::proof_for_contract(Alignment::mask)] pub fn check_mask() { - let a = kani::any::(); - if let Some(alignment) = Alignment::new(a) { - let _ = alignment.mask(); - } + let alignment = kani::any::(); + let _ = alignment.mask(); } } diff --git a/library/stdarch b/library/stdarch index a5709ad53ceef..df3618d9f3516 160000 --- a/library/stdarch +++ b/library/stdarch @@ -1 +1 @@ -Subproject commit a5709ad53ceef016902faf349f0d48aff1826f22 +Subproject commit df3618d9f35165f4bc548114e511c49c29e1fd9b From fe4ba8899568e0493433ca8be9562e9e17903902 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 20 Aug 2024 11:53:44 +0000 Subject: [PATCH 10/11] Add contract to of --- library/core/src/ptr/alignment.rs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs index 36063989a350c..d51f2ef7edff3 100644 --- a/library/core/src/ptr/alignment.rs +++ b/library/core/src/ptr/alignment.rs @@ -48,6 +48,8 @@ impl Alignment { #[unstable(feature = "ptr_alignment_type", issue = "102070")] #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")] #[inline] + #[requires(mem::align_of::().is_power_of_two())] + #[ensures(|result| result.as_usize().is_power_of_two())] pub const fn of() -> Self { // SAFETY: rustc ensures that type alignment is always a power of two. unsafe { Alignment::new_unchecked(mem::align_of::()) } @@ -396,10 +398,9 @@ mod verify { } // pub const fn of() -> Self - #[kani::proof] + #[kani::proof_for_contract(Alignment::of)] pub fn check_of_i32() { - let alignment = Alignment::of::(); - assert!(alignment.as_usize().is_power_of_two()); + let _ = Alignment::of::(); } // pub const fn new(align: usize) -> Option From 69e759494ae74d8edb1e29821faad60d5e8effba Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 20 Aug 2024 12:05:42 +0000 Subject: [PATCH 11/11] Fixup submodules --- library/backtrace | 2 +- library/stdarch | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/library/backtrace b/library/backtrace index 72265bea21089..fd0aed536dd9d 160000 --- a/library/backtrace +++ b/library/backtrace @@ -1 +1 @@ -Subproject commit 72265bea210891ae47bbe6d4f17b493ef0606619 +Subproject commit fd0aed536dd9d6ad1511a4ab3c350409f36ee52a diff --git a/library/stdarch b/library/stdarch index df3618d9f3516..a5709ad53ceef 160000 --- a/library/stdarch +++ b/library/stdarch @@ -1 +1 @@ -Subproject commit df3618d9f35165f4bc548114e511c49c29e1fd9b +Subproject commit a5709ad53ceef016902faf349f0d48aff1826f22