4 ms·

For anyone too lazy: https://godbolt.org/g/jvSKCD https://godbolt.org/g/jvSKCD I would be much more impressed if I hadn't taken a compilers course. I reckon (g

For anyone too lazy: https://godbolt.org/g/jvSKCD 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_variable_substitution https://en.wikipedia.org/wiki/Induction_variable#Induction_v...

digler999 10y ago
> 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.
- jcranmer 10y ago
  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.
  - drdrey 10y ago
    I think Nuno Lopes also did some work on proving the correctness of instcombine optimizations, for instance: http://blog.regehr.org/archives/1170 http://blog.regehr.org/archives/1170
- CyberShadow 10y ago
  > 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.
  - vsl 10y ago
    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.
foldr 10y ago
>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.
- widdma 10y ago
  Maybe they meant distributes? Modulo (sort of) distributes over multiplication: (a * b) % c = ((a % c) * (b % c)) % c

digler999 10y ago

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

jcranmer 10y ago
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.
- drdrey 10y ago
  I think Nuno Lopes also did some work on proving the correctness of instcombine optimizations, for instance: http://blog.regehr.org/archives/1170 http://blog.regehr.org/archives/1170
CyberShadow 10y ago
> 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.
- vsl 10y ago
  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.

foldr 10y ago

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

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