explicit validity check rule

[rcseacord]

@PLeVasseur I think we should make another required rule which enforces that explicit validity checks are performed before any reads if we don't force that here.

It's important to enforce that anyone writing code be encouraged to write a deviation report.

@rcseacord What do you mean by "before"? And what is a validity check? These are real questions. If the logic dictates that the value is valid, do you have to perform another redundant test each time the value is "used"?

You probably mean deviation records, and they are what makes MISRA unusable. Deviation records should be required sparingly. If you have to write a deviation record for every three lines of code, people will not use your standard and for good reason.

[workingjubilee]

Is this about a read on raw pointers? You kinda can't truly require a validity check in the fully general case, because there's no way at runtime to dynamically compute whether a pointer is valid for a read based solely on "you have a pointer". You can compute whether it is in an allocation from the allocator's perspective if you happen to be the allocator, but the answer is transient, and that wouldn't guarantee the pointer hasn't been e.g. copied somewhere else and then freed after you answered the question. It also doesn't answer type-level validity (e.g. initness) for every byte because while we know the allocator has to track allocations per se, those are pointers to MaybeUninit, in effect: there is no language property that guarantees you carry initness data in a particular form at runtime as it is not really something that translates to the machines we use. You could ask people to design ownership-conveying abstractions, but in Rust there isn't a particular shape that those must come in, and there's reasons to use different ones, and none of them are a particular way.

Pointers being valid for reads is about something the language already says is unsafe, and requires unsafe {} to do. I would expect the safety-critical guidelines to mostly just insist on people adhering to the common style regarding "unsafe APIs (traits and fns) must document their impl/caller requirements in their doc-comments", and "unsafe {} has a comment explaining its usage". Often a terse "// SAFETY: due to requirements imposed on caller" is intrusive enough, and is essentially just // SAFETY: しょうがない, so I would expect purely mechanical tooling to accept even an empty string if not further directed otherwise. Maybe the unsafe code actually is self-explanatory!

...I mean, that's a joke, but my point is that I don't expect any mandated formula for answering that question will actually improve the soundness of code. At some point everything devolves to "you have to actually read their reasoning and evaluate it against the code". Nowadays there are machines which will happily generate pages of pro-forma blather for you given a few words to start, so imposing a rule simply because it will force people to write more often, when such writing ought to be redundant with the basic style expected for use of the language's trickier corners, seems more likely to make it harder to evaluate the soundness of the code rather than easier.

[PLeVasseur]

Hey @workingjubilee -- is there a good comprehensive spot to read up more on this?

I would expect the safety-critical guidelines to mostly just insist on people adhering to the common style regarding "unsafe APIs (traits and fns) must document their impl/caller requirements in their doc-comments", and "unsafe {} has a comment explaining its usage".

From what I've read elsewhere part of the challenge is that this kind of knowledge may not be coalesced into one nice tidy spot. I've read a bit of the Rustnomicon and the Unsafe Code Guidelines, but they both appear to be out of date (explicitly). And Learn unsafe Rust is a work in progress.

---

Often a terse "// SAFETY: due to requirements imposed on caller" is intrusive enough, and is essentially just // SAFETY: しょうがない, so I would expect purely mechanical tooling to accept even an empty string if not further directed otherwise. Maybe the unsafe code actually is self-explanatory!

when such writing ought to be redundant with the basic style expected for use of the language's trickier corners, seems more likely to make it harder to evaluate the soundness of the code rather than easier.

These are fair points.

@rcseacord -- there are tools to help with these sorts of things like kani, but that feels to deviate outside of a coding guideline. How might we address the fact that // SAFETY: comments are kind of a pinky promise?

[workingjubilee]

Yes, I agree that it's hard to point to a specific place for norms re: unsafe code style, and in that sense I think these guidelines/this standard/whatever-you-wanna-call-it can be valuable by, er, doing that!