Skip to content

Invariant trait - #87

Merged
carolynzech merged 21 commits into
model-checking:mainfrom
carolynzech:invariant
Oct 30, 2024
Merged

Invariant trait#87
carolynzech merged 21 commits into
model-checking:mainfrom
carolynzech:invariant

Conversation

@carolynzech

@carolynzechcarolynzech commented Sep 18, 2024

Copy link
Copy Markdown

Adds an Invariant trait to core::ub_checks, and adds two invariants for Alignment and Layout.

One call-out: Kani's invariant trait enforces that the type is sized, but I wasn't sure why that would be necessary, so I didn't add it here.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@carolynzech
carolynzech requested a review from a team as a code ownerSeptember 18, 2024 17:10
celinval
celinval reviewed Sep 19, 2024
View reviewed changes

@celinvalcelinval left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks @carolynzech !

Comment threadlibrary/core/src/alloc/layout.rs Outdated
Comment threadlibrary/core/src/alloc/layout.rs Outdated
Comment threadlibrary/core/src/ptr/alignment.rs Outdated
Comment threadlibrary/core/src/ub_checks.rs
celinval
celinval reviewed Sep 19, 2024
View reviewed changes

@celinvalcelinval left a comment •
edited
Loading

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you please also add empty implementations for the Invariant trait for the primitive types?

Comment threadlibrary/core/src/alloc/layout.rs Outdated
tautschnig
tautschnig approved these changes Sep 20, 2024
View reviewed changes

@tautschnigtautschnig left a comment

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you!

Carolyn Zech@celinval
allow unused imports
917cf6a
Co-authored-by: Celina G. Val <celinval@amazon.com>
celinval
celinval suggested changes Sep 24, 2024
View reviewed changes

@celinvalcelinval left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you please remove the unsafe code.

Comment threadlibrary/contracts/safety/src/lib.rs
Comment threadlibrary/core/src/ptr/alignment.rs Outdated
@feliperodrifeliperodri added the Maintenance Maintenance related issues for the challange label Oct 8, 2024
@sgpthomassgpthomas mentioned this pull request Oct 24, 2024
Merged
celinval
celinval previously approved these changes Oct 24, 2024
View reviewed changes
Comment threadlibrary/contracts/safety/src/lib.rs Outdated
Comment threadlibrary/core/src/ub_checks.rs Outdated
Carolyn Zechand others added 2 commits October 24, 2024 19:40
Carolyn Zech@celinval
Update library/core/src/ub_checks.rs
693495a
Co-authored-by: Celina G. Val <celinval@amazon.com>
Carolyn Zech
derive Invariant for enums
48886c0
@carolynzechcarolynzech mentioned this pull request Oct 25, 2024
Open
@carolynzech
carolynzech dismissed celinval’s stale reviewOctober 25, 2024 11:00

Re-requesting review because I added an enum implementation.

carolynzech
carolynzech commented Oct 25, 2024
View reviewed changes
Comment threadlibrary/contracts/safety/src/lib.rs Outdated
celinval
celinval approved these changes Oct 29, 2024
View reviewed changes

@celinvalcelinval left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks

@carolynzech
carolynzech enabled auto-merge (squash) October 30, 2024 14:15
jaisnan
jaisnan approved these changes Oct 30, 2024
View reviewed changes

@jaisnanjaisnan left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ty

@carolynzech
carolynzech merged commit abe2354 into model-checking:mainOct 30, 2024
@carolynzech
carolynzech deleted the invariant branch October 30, 2024 15:47
github-merge-queueBot pushed a commit that referenced this pull request Dec 11, 2024
@sgpthomas@cvick32
@celinval@tautschnig
Write contracts + pre/post conditions for all unsafe methods in durat…
8a248d9
…ion (#136)
Resolves#72 We added invariants for Nanoseconds and Duration to match the safety
conditions for those types.
We add safety requirements to the following methods:
- `new`, `from_secs`, `from_millis`, `from_micros`, `from_nanos`,
`as_secs`, `as_millis`, `as_micros`, `as_nanos`, `subsec_millis`,
`subsec_micros`, `subsec_nanos`, `checked_add`, `checked_sub`,
`checked_mul`, `checked_div`
We additionally add correctness conditions to the following methods:
- `from_secs`, `as_secs`, `subsec_millis`, `subsec_micros`,
`subsec_nanos`, `as_millis`, `as_micros`
Support for `kani::Invariant` depends on #87. For the interim we
implemented a proxy trait `TempInvariant` that exposes the same
`is_safe` method. We will update this once #87 is merged.
While the safety check for `Duration::as_nanos()` succeeds, we ran into
timeouts for `Duration::as_nanos()` when we tried to use a correctness
contract and we're looking for advice on how to speed up that
verification time. We were able to prove it for `u16::MAX`, but hit
timeouts for larger numbers.
We are unsure if the pre-conditions for `Duration::new()` are acceptable
because they limit the range of values that you can call
`Duration::new()` with. However, we think it's reasonable since we limit
the values to values that don't panic. Let us know if this is a thing
that we should change.
By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
---------
Co-authored-by: Cole Vick <cole.d.vick@gmail.com>
Co-authored-by: Celina G. Val <celinval@amazon.com>
Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
@carolynzechcarolynzech mentioned this pull request Dec 18, 2024
Merged
Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tautschnigtautschnigtautschnig approved these changes
+2 more reviewers
@celinvalcelinvalcelinval approved these changes
@jaisnanjaisnanjaisnan approved these changes
Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

MaintenanceMaintenance related issues for the challange

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@carolynzech@tautschnig@celinval@jaisnan@feliperodri