Hacker News Reader

Comment by harpocrates | Hacker News Reader

For anyone too lazy: https://godbolt.org/g/jvSKCD

I would be much more impressed if I hadn't taken a compilers course. I reckon (god alone knows exactly what GCC does) this is just linear induction variable substitution[1] (so `x` gets replace with `i*2`), then associativity of integer multiplication, then some (probably builtin) rule that `n%n` is always 0. From there, it is pretty straightforward.

Don't get me wrong - the devil is in the details and getting optimizations that are both powerful and only applied when they are valid, and at the right time is difficult as hell. That said, I do expect compilers to be at least this smart.

[1]: https://en.wikipedia.org/wiki/Induction_variable#Induction_v...

View on HN

> I do expect compilers to be at least this smart.

Does anyone know if, internally, compilers second-guess / double-check themselves ? For instance, when they detect a clever shortcut do they generate and quickly run [1] the optimized bytecode on a sampling of inputs to verify it is functionally-equivalent to what non-optimized bytecode outputs ?

[1] obviously cross-compilers are a thing, so this wouldn't be possible if it were compiling/optimizing for a separate architecture.

Detecting functional equivalence of Turing-complete languages is a very non-trivial problem. So, no, compilers don't try to construct runtime proofs of their correctness.

There are people who do do more exhaustive checks of the peephole optimizations for correctness--or finding new opportunities (see John Regehr's Souper work). But production compilers are well-known (at least by anyone who works on them) for having lots of bugs in these kinds of optimizations.

I think Nuno Lopes also did some work on proving the correctness of instcombine optimizations, for instance: http://blog.regehr.org/archives/1170

> For instance, when they detect a clever shortcut do they generate and quickly run [1] the optimized bytecode on a sampling of inputs to verify it is functionally-equivalent to what non-optimized bytecode outputs ?

No. Optimization transformations are generally expected to result in provably identically-functional code (or sufficiently identical, in case of e.g. floating-point optimizations). Otherwise it is a bug.

Indeed, “provably” being the key word. If I, the compiler developer, prove (in the mathematical sense) that the transformation is functionally identical, I don’t need the compiler to run any experiments to verify it. A proof is much more solid than running a few experiments.

>then associativity of integer multiplication, then some (probably builtin) rule that `n%n` is always 0.

Is this quite right? It's not true in general that (a * b) % c = a * (b % c). E.g. it's not true for 2,3,4. The relevant generalization is that (a * b) % b = 0, which has nothing to do with associativity.

Maybe they meant distributes? Modulo (sort of) distributes over multiplication: (a * b) % c = ((a % c) * (b % c)) % c

Reply on news.ycombinator.com