Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

It's not me, it's the compiler

parsa.wtf

Post reply on HN
Print view View original

21–27 of 27 posts

Re: It's not me, it's the compiler

#21

Post by dzaima »

jpollock wrote: post #11
recursivedoubts wrote: post #2

interesting story as an aside, I think the original code, with the if statement, was clearer and would be easier to debug, etc, even if it was a bit longer

I prefer the second. :) It's about the cognitive load and having to follow branches. The second version minimizes the cyclomatic complexity, taking it to 1. The reader doesn't have to keep the if statement in mind when reading through the code, and doesn't have to worry about all the ways the code can get there if they want to modify it (e.g. to add logging, metrics, other logic). Whether or not consume should be a s…

..except, if you want to add logging/metrics/other logic, it's quite possible you'll want it to be conditional on the boolean anyway, bringing branching back, now mixed with the non-branching code.

And even if you don't need to keep an if statement in mind, you still need to keep the variable in mind anyway.

Re: It's not me, it's the compiler

#22

Post by tialaramex »

Surac wrote: post #16

can someone explain what the self.0 means? im not a rust speaker

self.0 is the zeroth field of self,

self is the name for a value of this type, apparently a type named LexerConsumer, this function took "&mut self" a mutable reference to a LexerConsumer. In Rust using any variety of "self" in this way means the function can (if you want) be called as a method on a LexerConsumer like this:

foo.consume(); // If foo is a LexerConsumer, we will call that `consume` function and pass it a mutable reference to foo.

Presumably the LexerConsumer doesn't give its fields names, so hence self.0 meaning just the zeroth field. Perhaps the author couldn't think of a good name for it.

Re: It's not me, it's the compiler

#23

Post by wyldfire »

rtpg wrote: post #12

> 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 b…

> 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++.

Re: It's not me, it's the compiler

#24

Post by IshKebab »

rtpg wrote: post #12

> 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 b…

> 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.

Re: It's not me, it's the compiler

#25

Post by dzaima »

IshKebab wrote: post #24
rtpg wrote: post #12

> 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 b…

> 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...

Re: It's not me, it's the compiler

#26

Post by rtpg »

dzaima wrote: post #25
IshKebab wrote: post #24

Earlier quoted context omitted.

> 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 ch…

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.

Re: It's not me, it's the compiler

#27

Post by dzaima »

rtpg wrote: post #26
dzaima wrote: post #25

Earlier quoted context omitted.

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 ch…

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 k…

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.
Post reply on HN