Comment by rtpg | Hacker News Reader

Comment by rtpg | Hacker News Reader

> The issue was labeled p-critical and i-miscompile, out of +61K rust issues there only 7 (including this one) that are both p-critical and i-miscompile, to me those are the most dangerous kind of bugs a compiler can have, given that they violate the contract between the programmer and the language. They show that not every safe code you write is safe. And also more generally there are only 247 p-critical issues to begin with.

I don't mean this in a snarky way or the like... and I guess the fact there are so few of these are a good indicator that the current processes are working decently well... but I would be very curious on a post-mortem from maintainers on how this bug got through. Miscompiles feel like the scariest sort of thing.

Maybe the deep and dark secret is simply that compiler optimizations are just extremely prone to mistakes and we all are just lucky enough that most messed up optimizations will break _something somewhere_ early enough to not get merged.

> how this bug got through.

Simplest answer is that there's no representative test case in the test suite yet.

Unfortunately the problem of compiler testing is a very challenging one IMO. You can't test it exhaustively, or perhaps if you did write such a suite it would take longer to execute than is feasible.

> we all are just lucky enough that most messed up optimizations will break _something somewhere_ early enough to not get merged

Your compiler is only as good as the set of code people routinely use it on. Rust has exploded in popularity but it's still much less popular than C, C++.

> compiler optimizations are just extremely prone to mistakes

This is definitely true - there has been quite a lot of formal work done to prove that optimisation passes don't change semantics. I guess it hasn't made it into Rust yet. Or maybe even LLVM.

Formal proofs for specific instruction sequence substitution (e.g. LLVM's instcombine) are simple-ish enough via just throwing SMT at it, ...as long as the source pattern and target replacement are in a format from which both the compiler code and verification source+target can be automatically derived from; though you'd still need manual proofs for anything with unbounded configurations that can't be exhaustively checked if you aren't satisfied with just checking some subset.

Larger-scale things operating over an unbounded amount of instructions require significant amounts of effort of verification on each pass. CompCert apparently has 1200LoC of proving DCE, one of the simplest whole-function passes - https://github.com/AbsInt/CompCert/blob/02fc017cf69210db5fd5...

Not to minimise compcert's work nor to trivialise the equivalent kind of work in Rust but I wonder how much of the Compcert difficulty on dead code elimination is downstream of C semantic futziness. I know that CompCert has a whole notion of external visibility that it has to deal with that I _think_ would be way more straightforward in Rust.

My experience writing Roq (very limited!!!) is that it also lends towards kinda brute forcing your way through something. If you have your set of proof lemmas and you tie it all together there's not that much incentive to simplify the proofs (that are irrelevant anyways, according to the theories). So the 1200 LoC might be "oh we could have maybe done this in 400 with more thinking but ... well... this is working yeah?"

trying not to trivialize it all. Just kinda hoping that we do have a more provable future ahead of us, and that CompCert represents (hopefully) an upper bound of difficulty just due to the nature of the source language.

Perhaps some early things in the pipeline could be easier with a saner language, but I can't imagine it affecting much of the core optimizations, which'd all benefit from being ran on some messy low-level intermediate form equivalent to what C converts to anyway (if not more complex if preserving precise aliasing info). Would be curious to hear about that external visibility thing, doesn't feel like it could make optimizations (beyond inlining, perhaps?) harder.

Reply on news.ycombinator.com