llvm-project

d746b8a1 - [ConstraintElim] Rewrite usub.sat to sub when it cannot saturate. (#220865)

[ConstraintElim] Rewrite usub.sat to sub when it cannot saturate. (#220865) usub.sat(A, B) is max(A - B, 0), so it is exactly A - B when A >=u B. Check if we can prove the precondition, and if so replace it with a plain sub nuw. We can also add NSW if A is non-negative. This helps to both remove unnecessary usub.sat, as well as enables a number of additional folds (once the usub.sat has been replaced by sub it can be decomposed when checking conditions involving it, as we do the rewrite before simplifying any condition involving it): https://github.com/dtcxzyw/llvm-opt-benchmark-nightly/pull/1181 Alive2 Proofs: https://alive2.llvm.org/ce/z/v6gZwL PR: https://github.com/llvm/llvm-project/pull/220865