[PATCH] D85593: [InstCombine] ~(~X + Y) -> X - Y

[Juneyoung Lee via Phabricator via llvm-commits]

aqjune added a comment.

To prove correctness of a transformation of expressions with constants and undefs, following these steps is sufficient:
(1) Replace an undef with a set of all possible values. For example, i8 undef is {0, 1, 2, ..., 255}.
(2) Evaluate each operation by pairwisely picking elements from operands' sets.
(3) If the final result is in a subset relation, the transformation is correct.

  define i8 @src() {
    %a = add i8 255, undef // %a = {0, ... ,255}
    %nota = xor i8 %a, 255 // %nota = {0, ..., 255}
    call void @use(i8 %a)  // use({0, ..., 255})
    ret i8 %nota           // return {0, ..., 255}
  }
  =>
  define i8 @tgt(i8 %y) {
    %a = add i8 255, undef
    %s = sub i8 0, undef
    call void @use(i8 %a) // use({0, ..., 255})
    ret i8 %s             // return {0, ..., 255}
  }

Since the sets given to `@use()` as well as `ret` are equal between the source and target, this transformation is correct.

Checking whether the number of uses is increased globally is a quick way to check whether the optimization is incorrect. It has to introduce new uses that was guaranteed not to be undef before.

An example that converts `mul x, 2` to `add x, x`:

  // Let's assume that x = undef = {0, ..., 255}
  y = mul x, 2 // y = {0, 2, 4, ..., 254}
  =>
   y = add x, x // y = {0, 0+1, 1+0, 0+2, 1+1, ..., 255} = {0, ..., 255}

Since the target's `y` contains {1, 3, 5, ...}, which did not appear at the source, this transformation is incorrect.


CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D85593/new/

https://reviews.llvm.org/D85593