Re: C aggregate passing (Rust kernel policy)

[Miguel Ojeda <miguel.ojeda.sandonis@gmail.com>]

On Wed, Feb 26, 2025 at 1:36 PM Ventura Jack <venturajack85@gmail.com> wrote:
>
> In a preprint paper, both stacked borrows and tree burrows are as
> far as I can tell described as having false positives.
>
> Are you sure that both stacked borrows and tree borrows are
> meant to be full models with no false positives and false negatives,
> and no uncertainty, if I understand you correctly? It should be
> noted that they are both works in progress.

I think you are mixing up two things: "a new model does not allow
every single unsafe code pattern out there" with "a new model, if
adopted, would still not be able to tell if something is UB or not".

> The aliasing rules being tied to a specific compiler backend,
> instead of a specification, might make it harder for other
> Rust compilers, like gccrs, to implement the same behavior for
> compiled programs, as what the sole major Rust compiler,
> rustc, has of behavior for compiled programs.

It is not "tied to a specific compiler backend". The reference (or
e.g. the standard library implementation, which you mentioned) may
mention LLVM, as well as other backends, but that does not imply the
final rules will (or need to) refer to the LLVM reference. And even if
a spec refers to a given revision of another spec (it is not
uncommon), that is different from being "tied to a specific compiler
backend".

Moreover, if it makes it easier, another compiler could always assume less.

> I am also skeptical of the apparent reliance on MIRI in the
> blog post and by some other Rust developers, since
> MiRI according to its own documentation cannot catch
> everything. It is better not to rely on a sanitizer for trying
> to figure out the correctness of a program. Sanitizers are
> useful for purposes like mitigation and debugging, not
> necessarily for determining correctness.

Please see the earlier reply from Ralf on this.

Cheers,
Miguel