Hacker News new | ask | show | jobs
by gfaster 203 days ago
In C, I'm pretty confident the loop is defined by the standard to terminate.

Also I did take the excuse to plug it (the optimized llvm ir) into Alive:

https://alive2.llvm.org/ce/#g:!((g:!((g:!((h:codeEditor,i:(f...

2 comments

Alive2 does not handle loops; don't know what exactly it does by default, but changing the `shl i32 %and, 1` to `shl i32 %and, 2` has it still report the transformation as valid. You can add `--src-unroll=2` for it to check up to two loop iterations, which does catch such an error (and does still report the original as valid), but of course that's quite limited. (maybe the default is like `--src-unroll=1`?)
Oh wow nice catch - I was not at all familiar with the limitations. I would've hoped for a warning there, but I suppose it is a research project.

I was able to get it working with unrolling and narrower integers:

https://alive2.llvm.org/ce/#z:OYLghAFBqd5QCxAYwPYBMCmBRdBLAF...

> In C, I'm pretty confident the loop is defined by the standard to terminate.

Huh? What's that supposed to mean?

That it is Undefined Behavior for a loop with a non-constant conditional and that doesn't cause side effects in its body to not terminate.

For example, you can use this make the compiler "prove" the Collatz Conjecture:

https://gcc.godbolt.org/#g:!((g:!((g:!((h:codeEditor,i:(file...