[llvm] [LICM] Preserve nsw when reassociating integer adds (PR #221210)
Andrey Grabezhnoy via llvm-commits
llvm-commits at lists.llvm.org
Fri Sep 4 06:47:58 PDT 2026
agrabezh wrote:
> Proof?
Here is an [Alive2 proof](https://alive2.llvm.org/ce/#z%3AMYewtgDglgNgpgJwM4FIDMBBAhACh6SWRdDAQxigDc4UAmAYRAgBcoQA7VTAcm7vqQgArgmA0eAEzjAYpBDVoAGFAHYAQnUVQAHP01QAjJtUARYwBZFMGJTAA6JKQkS7AdyjMAFnZDUEAMxgQVzsdHB09JR0AShRFDCkZOQVFShAoCQsrG3tSJCQhMDhwg1j4uIS4fyh2FIilFEskUXDdBtoAVhtIrTblTuAjBn0%2Bug7gWliG9QrjdvHPaQBrOEyGtDMlYHIYYxmotvp9IeUVTeVLa1sHJxd3Lx8%2FQODQ7Va58aGjg4%2BJsow5v0Or5EM9XMYNpo4AAPZgIUjAZiUchCFKqDQ%2FYZRE6mX6LYArNbfRRGcrtIHsECPUFBcHrc7QkAIY4fEEBWk9OGo2bk7bWTRpDJZK65fKFYqGD6U6ns4L%2FQFjW44yFKW6aTh03ofbpYoGDHn9IG3WgQ85qpQakYfJU9MYTA2aeTMK3zY2zM6zeJSaq1F0XRTMADmzHe8x1xPqeq%2Bfrtkz2GjJhrt%2BMJps0fN20wxWt1kum50a2Wujmcbg83jZYNeoajPUjsfl5LGlY59KhsPhiORMG5WZdEZxHvmwBTqx6pIBTc60pbwTTSkZzOxrKereJXJoifTOwF6TW%2FpFdjyBSKJSlVNnrkbSc6NWRCCgpHYzrbquc6qQmvrA2jw5NW%2FmeQChgF9lBVRRzUUS1MSBcMPjvORH2fB0lCdGNOiAoQQPdMx4m4aIpnoaoQMQDAkDAEgcEIvwkDYdgSDQIA%3D) of the reassociation. It uses i8 so the public instance completes quickly; the argument is bit-width independent. The llvm.assume represents the separately established fact that C1 + C2 does not signed-overflow. Alive2 reports the transformation as correct with nsw on both generated additions.
https://github.com/llvm/llvm-project/pull/221210
More information about the llvm-commits
mailing list