[all-commits] [llvm/llvm-project] 60246d: [InstCombine] Generalize zext(add X, -C) + C foldi...

[Maiowaa via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: 60246dc28d170447299babf2f14706a2156b5488
      https://github.com/llvm/llvm-project/commit/60246dc28d170447299babf2f14706a2156b5488
  Author: Maiowaa <soodkushagar387 at gmail.com>
  Date:   2026-04-15 (Wed, 15 Apr 2026)

  Changed paths:
    M llvm/lib/Transforms/InstCombine/InstCombineAddSub.cpp
    M llvm/test/Transforms/InstCombine/add.ll

  Log Message:
  -----------
  [InstCombine] Generalize zext(add X, -C) + C folding (#191723)

This patch generalizes an existing InstCombine optimization:

  zext(X - 1) + 1 → zext(X)

to support arbitrary constants C:

  zext(X - C) + C → zext(X)

when X is known to be >= C using KnownBits analysis.

This avoids missed simplifications for non-unit constants while ensuring
correctness under wrap semantics.

Includes test coverage for:
- Positive case where the fold applies
- Negative case where the fold must not apply


### Correctness Proof

We consider the transform:

  zext(add(X, -C)) + C → zext(X)

under the conditions:
  1) X u>= C (unsigned comparison)
  2) C fits in the bitwidth of X (i.e., representable in NarrowBW bits)

The inner operation is performed in the narrower bitwidth n:

  add(X, -C) = (X - C) mod 2^n

Since X u>= C, the subtraction does not underflow, so:

  (X - C) mod 2^n = X - C

Applying zero extension:

  zext(X - C) + C = (X - C) + C = X

Thus:
  = zext(X)

---

### Alive2 Validation

The transform was validated using Alive2 with symbolic C.
The constraint that C fits in NarrowBW bits is modeled using llvm.ctlz,
and the precondition X u>= C is enforced via llvm.assume.

Alive2 verifies the transformation under these conditions:

https://alive2.llvm.org/ce/z/jCVPWr



To unsubscribe from these emails, change your notification settings at https://github.com/llvm/llvm-project/settings/notifications