agent-driven: Fix soundness in try_create_array, add safety comments#239
Conversation
| x.retain(|&c| c != 0); | ||
| // SAFETY: all zero bytes have been removed | ||
| // SAFETY: | ||
| // Contract from `CString::from_vec_unchecked`: the vector must not contain |
There was a problem hiding this comment.
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.
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)
| // 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.
Isn't the canonical name for the zero byte a null byte (not nul or nil for that matter) as per K&R =)
There was a problem hiding this comment.
nul is what it is called in the context of strings
There was a problem hiding this comment.
thanks. I had done a similar PR and debated to use null or nul when talking about an array of ascii bytes. Sounds like I should have used nul in the comment.
3 participants
Found while running a safety audit with Gemini Next
The main safety bug was that we were creating an uninitialized slice type so we could write to it.
The safety comments are also agent generated, but they seem fine. I can remove them if desired.