Re: C aggregate passing (Rust kernel policy)
From: Ralf Jung
Date: Wed Feb 26 2025 - 17:29:01 EST
Hi all,
On 26.02.25 19:09, Ventura Jack wrote:
On Wed, Feb 26, 2025 at 9:32 AM Ralf Jung <post@xxxxxxxx> wrote:
Hi VJ,
- Rust has not defined its aliasing model.
Correct. But then, neither has C. The C aliasing rules are described in English
prose that is prone to ambiguities and misintepretation. The strict aliasing
analysis implemented in GCC is not compatible with how most people read the
standard (https://bugs.llvm.org/show_bug.cgi?id=21725). There is no tool to
check whether code follows the C aliasing rules, and due to the aforementioned
ambiguities it would be hard to write such a tool and be sure it interprets the
standard the same way compilers do.
For Rust, we at least have two candidate models that are defined in full
mathematical rigor, and a tool that is widely used in the community, ensuring
the models match realistic use of Rust.
But it is much more significant for Rust than for C, at least in
regards to C's "restrict", since "restrict" is rarely used in C, while
aliasing optimizations are pervasive in Rust. For C's "strict aliasing",
I think you have a good point, but "strict aliasing" is still easier to
reason about in my opinion than C's "restrict". Especially if you
never have any type casts of any kind nor union type punning.
Is it easier to reason about? At least GCC got it wrong, making no-aliasing
assumptions that are not justified by most people's interpretation of the model:
https://bugs.llvm.org/show_bug.cgi?id=21725
(But yes that does involve unions.)
For that specific bug issue, there is a GitHub issue for it.
https://github.com/llvm/llvm-project/issues/22099
Yeah sorry this was an LLVM issue, not a GCC issue. I mixed things up.
And the original test case appears to have been a compiler bug
and have been fixed, at least when I run on Godbolt against
a recent version of Clang. Another comment says.
"The original testcase seems to be fixed now but replacing
the union by allocated memory makes the problem come back."
And the new test case the user mentions involves a void pointer.
I wonder if they could close the issue and open a new issue
in its stead that only contains the currently relevant compiler
bugs if there are any. And have this new issue refer to the old
issue. They brought the old issue over from the old bug tracker.
But I do not have a good handle on that issue.
Unions in C, C++ and Rust (not Rust "enum"/tagged union) are
generally sharp. In Rust, it requires unsafe Rust to read from
a union.
Definitely sharp. At least in Rust we have a very clear specification though,
since we do allow arbitrary type punning -- you "just" reinterpret whatever
bytes are stored in the union, at whatever type you are reading things. There is
also no "active variant" or anything like that, you can use any variant at any
time, as long as the bytes are "valid" for the variant you are using. (So for
instance if you are trying to read a value 0x03 at type `bool`, that is UB.)
I think this means we have strictly less UB here than C or C++, removing as many
of the sharp edges as we can without impacting the rest of the language.
In contrast, Miri checks for all the UB that is used anywhere in the Rust
compiler -- everything else would be a critical bug in either Miri or the compiler.
But yes, it only does so on the code paths you are actually testing. And yes, it
is very slow.
I may have been ambiguous again, or unclear or misleading,
I need to work on that.
The description you have here indicates that Miri is in many ways
significantly better than sanitizers in general.
I think it is more accurate of me to say that Miri in some aspects
shares some of the advantages and disadvantages of sanitizers,
and in other aspects is much better than sanitizers.
I can agree with that. :)
Is Miri the only one of its kind in the programming world?
There are not many system languages in mass use, and
those are the languages that first and foremost deal
with undefined behavior. That would make Miri extra impressive.
I am not aware of a comparable tool that would be in wide-spread use, or that is
carefully aligned with the semantics of an actual compiler.
For C, there is Cerberus (https://www.cl.cam.ac.uk/~pes20/cerberus/) as an
executable version of the C specification, but it can only run tiny examples.
The verified CompCert compiler comes with a semantics one could interpret, but
that only checks code for compatibility with CompCert C, which has a lot less
(and a bit more) UB than real C.
There are also two efforts that turned into commercial tools that I have not
tried, and for which there is hardly any documentation of how they interpret the
C standard so it's not clear what a green light from them means when compiling
with gcc or clang. I also don't know how much real-world code they can actually run.
- TrustInSoft/tis-interpreter, mostly gone from the web but still available in
the wayback machine
(https://web.archive.org/web/20200804061411/https://github.com/TrustInSoft/tis-interpreter/);
I assume this got integrated into their "TrustInSoft Analyzer" product.
- kcc, a K-framework based formalization of C that is executable. The public
repo is dead (https://github.com/kframework/c-semantics) and when I tried to
build their tool that didn't work. The people behind this have a company that
offers "RV-Match" as a commercial product claiming to find bugs in C based on "a
complete formal ISO C11 semantics" so I guess that is where their efforts go now.
For C++ and Zig, I am not aware of anything comparable.
Part of the problem is that in C, 2 people will have 3 ideas for what the
standard means. Compiler writers and programmers regularly have wildly
conflicting ideas of what is and is not allowed. There are many different places
in the standard that have to be scanned to answer "is this well-defined" even
for very simple programs. (https://godbolt.org/z/rjaWc6EzG is one of my favorite
examples.) A tool can check a single well-defined semantics, but who gets to
decide what exactly those semantics are?
Formalizing the C standard requires extensive interpretation, so I am skeptical
of everyone who claims that they "formalized the C standard" and built a tool on
that without extensive evaluation of how their formalization compares to what
compilers do and what programmers rely on. The Cerberus people have done that
evaluation (see e.g. https://dl.acm.org/doi/10.1145/2980983.2908081), but none
of the other efforts have (to my knowledge). Ideally such a formalization effort
would be done in close collaboration with compiler authors and the committee so
that the ambiguities in the standard can be resolved and the formalization
becomes the one canonical interpretation. The Cerberus people are the ones that
pushed the C provenance formalization through, so they made great progress here.
However, many issues remain, some quite long-standing (e.g.
https://www.open-std.org/jtc1/sc22/wg14/www/docs/dr_260.htm and
https://www.open-std.org/jtc1/sc22/wg14/www/docs/dr_451.htm, which in my eyes
never got properly resolved by clarifying the standard). Martin and a few others
are slowly pushing things in the right direction, but it takes a long time.
Rust, by having a single project in charge of the one canonical implementation
and the specification, and having an open process that is well-suited for
incorporating user concerns, can move a lot quicker here. C has a huge
head-start, Rust has nothing like the C standard, but we are catching up -- and
our goal is more ambitious than that; we are doing our best to learn from C and
C++ and concluded that that style of specification is too prone to ambiguity, so
we are trying to achieve a formally precise unambiguous specification. Wasm
shows that this can be done, at industry scale, albeit for a small language --
time we do it for a large one. :)
So, yes I think Miri is fairly unique. But please let me know if I missed something!
(As an aside, the above hopefully also explains why some people in Rust are
concerned about alternative implementations. We do *not* want the current
de-factor behavior to ossify and become the specification. We do *not* want the
specification to just be a description of what the existing implementations at
the time happen to do, and declare all behavior differences to be UB or
unspecified or so just because no implementation is willing to adjust their
behavior to match the rest. We want the specification to be prescriptive, not
descriptive, and we will adjust the implementation as we see fit to achieve that
-- within the scope of Rust's stability guarantees. That's also why we are so
cagey about spelling out the aliasing rules until we are sure we have a good
enough model.)
There are some issues in Rust that I am curious as to
your views on. rustc or the Rust language has some type
system holes, which still causes problems for rustc and
their developers.
https://github.com/lcnr/solver-woes/issues/1
https://github.com/rust-lang/rust/issues/75992
Those kinds of issues seem difficult to solve.
In your opinion, is it accurate to say that the Rust language
developers are working on a new type system for
Rust-the-language and a new solver for rustc, and that
they are trying to make the new type system and new solver
as backwards compatible as possible?
It's not really a new type system. It's a new implementation for the same type
system. But yes there is work on a new "solver" (that I am not involved in) that
should finally fix some of the long-standing type system bugs. Specifically,
this is a "trait solver", i.e. it is the component responsible for dealing with
trait constraints. Due to some unfortunate corner-case behaviors of the old,
organically grown solver, it's very hard to do this in a backwards-compatible
way, but we have infrastructure for extensive ecosystem-wide testing to judge
the consequences of any given potential breaking change and ensure that almost
all existing code keeps working. In fact, Rust 1.84 already started using the
new solver for some things
(https://blog.rust-lang.org/2025/01/09/Rust-1.84.0.html) -- did you notice?
Hopefully not. :)
Kind regards,
Ralf