3 ms·

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:/

• dzaima 10mo ago
  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`?)
  • gfaster 10mo ago
    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:OYLghAFBqd5QCxAYwPYBMCmBRdBLAF1QCcAaPECAM1QDsCBlZAQwBtMQBGAFlICsupVs1qhWrAG4BbUgGdM7ZATx1KmWugDCqVgFcptLgFZS69ABk8tTADl9AI0zFjpAA6pZhFbW16DL909lOktrOylHZ04TeUVg2gYCZmICX31DaLkFTCVvROSCUNsHJxdZJJS0/0zygqLwyOMASjlUXWJkDgByLCorTABqPE4ANgGAAVkOiGGx2jaNTCoBgFIAJiMAD1Ih0YH53UXl9aMATybVgHYAIRWABgBBdQJiU5B7h4GB%2B2IB4UdWKsNuhUAA6ewYU4fD4g8GQ96PL4nU6g5jodDEUF3VYAZgAIgNXAg8LsxisjNcgWcdidnq9VkY8TSKVTNiQacCwRD0KcGXiPkiNptUejMdiVvjCcTSQzKSdtlS6bzyUzZVTZAhWByjLDucrGQKqSJ0LiCcaZfKRRisdqUWjrXdDfKSKaBmzfrNWVaxbbvVinRsNYCJQSgxaNsadpwA0YiBCdKD5gRXXhkFJXANMABHcNGSMDR2I74ezhUuOoBNJnb/BRU2FmavMAF1rmQ6GPesaBGfAbETDJz3O4jQy78x4wpb9GXjAjAAgzPYHI6snaepe9KnnK63IuCvPo1323MK5GGr59gd7E72kd4rotVggLpGLqkQxdO6v1BP8zmABqACyAwAJIAEoDLIbQdIM6w4pwr4EE%2Bn5NC0ADWIDcAAnKCRhYZwmGcPhRiYSMmFrLwj5dNwr7vp%2BpDfl0r6yCAdykIhH73qQcCwEgaDpng7BkBQEB8a4AmlGweASJgpB9KwBBOMxED2Ehr72FYyRvF08GkHxUjPAA8rQrBaXRWBSCIwDsKppD4H2uTScxHGmJsOS6ApT46VYCmUXRrB4D8mnaFgnkIcQeBSKFLQ0PQTBsBwPD8IIwiiCA4jSEIAXMZALSoK48ROQAtIVUzIIVhzEDorAhjiaxMdkuSqBAZhVBkpgaPUJRRG4HheHQrWCIEfW0J1ESlJwWRxHkFSpDo6SCLEOTxPkKSjY0E21JUc3VHIM1reNLSQe0nRcA%2BT4vm%2BNkMZJ0mFQQEgDBAuCEC6sETQM2j8YJQJwRcv6ASBoEIapKGkOhRh3KC3AQwAHHcMNw9wdw4nclwjBRT7UZdzkMUxLFsSDZ1dHV2N0bjBMcaD0nEJ4qjcEAA%3D https://alive2.llvm.org/ce/#z:OYLghAFBqd5QCxAYwPYBMCmBRdBLAF...
• thaumasiotes 10mo ago
  > In C, I'm pretty confident the loop is defined by the standard to terminate. Huh? What's that supposed to mean?
  • gfaster 10mo ago
    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:(filename:'1',fontScale:14,fontUsePx:'0',j:1,lang:___c,selection:(endColumn:4,endLineNumber:1,positionColumn:4,positionLineNumber:1,selectionStartColumn:4,selectionStartLineNumber:1,startColumn:4,startLineNumber:1),source:'void+%0Acollatz(long+n)%0A%7B%0A++++while+(n+!!%3D+1)+%7B%0A++++++++if+(n+%25+2+%3D%3D+0)+%7B%0A++++++++++++n+/%3D+2%3B%0A++++++++%7D+else+%7B%0A++++++++++++n+%3D+n+*+3+%2B+1%3B%0A++++++++%7D%0A++++%7D%0A++++return%3B%0A%7D'),l:'5',n:'0',o:'C+source+%231',t:'0')),k:36.16150836001423,l:'4',n:'0',o:'',s:0,t:'0'),(g:!((h:compiler,i:(compiler:cclang2110,filters:(b:'0',binary:'1',binaryObject:'1',commentOnly:'0',debugCalls:'1',demangle:'0',directives:'0',execute:'0',intel:'0',libraryCode:'0',trim:'1',verboseDemangling:'0'),flagsViewOpen:'1',fontScale:14,fontUsePx:'0',j:1,lang:___c,libs:!(),options:'-O3',overrides:!(),selection:(endColumn:1,endLineNumber:1,positionColumn:1,positionLineNumber:1,selectionStartColumn:1,selectionStartLineNumber:1,startColumn:1,startLineNumber:1),source:1),l:'5',n:'0',o:'+x86-64+clang+21.1.0+(Editor+%231)',t:'0')),header:(),k:63.838491639985776,l:'4',n:'0',o:'',s:0,t:'0')),l:'2',n:'0',o:'',t:'0')),version:4 https://gcc.godbolt.org/#g:!((g:!((g:!((h:codeEditor,i:(file...