-
Notifications
You must be signed in to change notification settings - Fork 17
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Contracts & Harnesses for add
, addr
, and align_offset
#105
base: main
Are you sure you want to change the base?
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
First round of comments.
@@ -279,6 +279,8 @@ impl<T: ?Sized> NonNull<T> { | |||
#[must_use] | |||
#[inline] | |||
#[unstable(feature = "strict_provenance", issue = "95228")] | |||
#[requires(!self.as_ptr().is_null())] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This requires clause is not needed since this is an invariant of this type.
@@ -279,6 +279,8 @@ impl<T: ?Sized> NonNull<T> { | |||
#[must_use] | |||
#[inline] | |||
#[unstable(feature = "strict_provenance", issue = "95228")] | |||
#[requires(!self.as_ptr().is_null())] | |||
#[ensures(|result| result.get() != 0)] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think this can be strengthened to result.get() == self.as_ptr() as usize
.
@@ -560,6 +566,8 @@ impl<T: ?Sized> NonNull<T> { | |||
// Additionally safety contract of `offset` guarantees that the resulting pointer is | |||
// pointing to an allocation, there can't be an allocation at null, thus it's safe to | |||
// construct `NonNull`. | |||
assert!(core::mem::size_of::<T>() == 1, "element size is 1"); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This assert and the next one were added as part of our debugging of the failure in offset
and should now be removed.
@@ -552,6 +554,10 @@ impl<T: ?Sized> NonNull<T> { | |||
#[must_use = "returns a new pointer rather than modifying its argument"] | |||
#[stable(feature = "non_null_convenience", since = "1.80.0")] | |||
#[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] | |||
#[requires(count.checked_mul(core::mem::size_of::<T>()).is_some())] // Prevent offset overflow | |||
#[requires(count * core::mem::size_of::<T>() <= isize::MAX as usize)] // SAFETY: count * size_of::<T>() does not overflow isize | |||
//#[requires(ub_checks::can_write(self.as_ptr().offset(count as isize)))] // not working |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As mentioned in #99 (comment), the solution is to combine this requires clause with the count.checked_mul
one to make sure they're properly applied.
@@ -1177,6 +1185,37 @@ impl<T: ?Sized> NonNull<T> { | |||
#[must_use] | |||
#[stable(feature = "non_null_convenience", since = "1.80.0")] | |||
#[rustc_const_unstable(feature = "const_align_offset", issue = "90962")] | |||
#[requires(!self.pointer.is_null())] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is not needed.
@@ -1785,6 +1824,7 @@ impl<T: ?Sized> From<&T> for NonNull<T> { | |||
mod verify { | |||
use super::*; | |||
use crate::ptr::null_mut; | |||
use crate::mem::align_of; |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Is this used anywhere?
Towards #53
Changes
Three function contracts & four harnesses:
non_null::add
non_null::addr
non_null::align_offset
, including both positive and negative harness that triggers panic. The ensures clause foralign_offset
is referenced fromalign_offset
inlibrary/core/src/ptr/mod.rs
.Revalidation
To revalidate the verification results, run
kani verify-std -Z unstable-options "path/to/library" -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify
. This will run all six harnesses in the module. All default checks should pass:❗ Warning
Running the above command with the default installed cargo kani will result in compilation error due to the latest merged from PR#91. Detailed errors are commented under that PR. This issue is waiting to be resolved.
TODO:
Layout
to create dynamically sized arrays in place of fixed size array in harnesses. This approach currently has errors and is documented in discussion.requires
clause in contract to constraincount
to be within object memory size: there is a current issue with usingub_checks::can_write
to get the object size. A workaround is implemented in the harness.By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.