immunant / c2rust

Migrate C code to Rust
https://c2rust.com/
Other
3.91k stars 229 forks source link

Feature suggestion: Stronger handling of `restrict` qualifier? #946

Open Dante-Broggi opened 1 year ago

Dante-Broggi commented 1 year ago

This is probably difficult and unnecessary to implement, but it seems correct to me, based on the definition of restrict in N1256:

I believe that a dereferenced T const *restrict qualified pointer actually is guaranteed to have the same UB as a reference, within the domain the access can be reordered. Specifically, const guarantees[^1] that this pointer does not modify the value, and restrict guarantees that, if accessed and modified it is only accessed via this pointer. In contrast, a reference is dereferenceable and read only, except in UnsafeCell. Thus if a T const *restrict pointer is accessed, within the C-block it is declared in, it is dereferenceable and read only[^1].

Similarly, if a T *restrict qualified pointer is written to, then within the C-block it is declared in it is at least as strong as a &Cell<T> as it is immutable or only accessed via this pointer, and might be as strong as &mut T depending on the precise rules for sending &mut T around[^2].

[^1]: except via locally casting away const? [^2]: specifically I am worried about floating pointer provenance, restrict should be enough to require disjoint accesses.