Skip to content

Separate validity and safety invariants in the specification? #150

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.

Sign up for GitHub

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

Jump to bottom
Closed
bjorn3 opened this issue Jul 26, 2022 · 0 comments · Fixed by #257
Closed

Separate validity and safety invariants in the specification? #150

bjorn3 opened this issue Jul 26, 2022 · 0 comments · Fixed by #257

Comments

@bjorn3
Copy link
Member

bjorn3 commented Jul 26, 2022

Violating either is currently considered UB, while safety invariants can be temporarily violated provided that you don't pass it to any function expecting the safety invariants to hold, while violating the validity invariants is unconditionally UB1. As an example for bool the value being 0 or 1 is a validity invariant, while for str the value being valid UTF-8 is a safety invariant2.

Footnotes

  1. https://www.ralfj.de/blog/2018/08/22/two-kinds-of-invariants.html ↩

  2. https://github.com/rust-lang/reference/pull/792 ↩
@Veykril Veykril mentioned this issue Aug 17, 2022
Merged
bors-ferrocene bot added a commit that referenced this issue Aug 22, 2022
@bors-ferrocene @Veykril
Merge #257
129edf1 
257: Define undefined behavior for valid type values in terms of invariants r=kirtchev-adacore a=Veykril

We currently specify non-utf8 str values as UB which is not quite the case,
this PR changes how we describe undefined behavior for valid values of a type
by specifying either a validity invariant or a safety invariant for them.

Closes #150

Co-authored-by: Lukas Wirth <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Define undefined behavior for valid type values in terms of invariants rust-lang/fls
1 participant
@bjorn3