-
Notifications
You must be signed in to change notification settings - Fork 94
agent-driven: Fix soundness in try_create_array, add safety comments #239
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
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -7,7 +7,12 @@ impl<'a> Arbitrary<'a> for CString { | |
| fn arbitrary(u: &mut Unstructured<'a>) -> Result<Self> { | ||
| <Vec<u8> as Arbitrary>::arbitrary(u).map(|mut x| { | ||
| x.retain(|&c| c != 0); | ||
| // SAFETY: all zero bytes have been removed | ||
| // SAFETY: | ||
| // Contract from `CString::from_vec_unchecked`: the vector must not contain | ||
| // any interior nul (zero) bytes. | ||
|
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Isn't the canonical name for the zero byte a
Member
Author
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. nul is what it is called in the context of strings There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. thanks. I had done a similar PR and debated to use |
||
| // Evidence: `x.retain(|&c| c != 0)` removes all bytes equal to `0` from the | ||
| // vector `x`. Consequently, `x` contains no nul bytes, which guarantees | ||
| // it has no interior nul bytes. | ||
| unsafe { Self::from_vec_unchecked(x) } | ||
| }) | ||
| } | ||
|
|
||
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.
That's a neat way to write down safety comments in a more structured way. I will, um, yoink this.
If only there was a way to reference the contracts without repeating them a bunch from what's already in the doc for the method... 🤔
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.
Yeah that's been my rule about good safety comments for a while: list the things you need to prove, then prove them.
Review becomes double checking you got all the invariants (easy if occasionally tedious) and then checking the local proof (usually easy, sometimes not)