[PATCH] D63065: [InstSimplify] Fix addo/subo undef folds (PR42209)

[Roman Lebedev via Phabricator via llvm-commits]

lebedev.ri added a comment.

In D63065#1545036 <https://reviews.llvm.org/D63065#1545036>, @nikic wrote:

> @lebedev.ri Not familiar with what exactly alive proves, but assuming you're using two separate proofs for a reason: It is possible to make the result zero, yes. But only if the overflow flag is chosen as true (rather than false) //at the same time//. Both result & overflow need to be checked together for the result to be meaningful.


Good observarvation. Close, but nope:

  $ ./src/alive2/build-Clang-release/alive -root-only /tmp/test.opt 
  OMP: Info #270: omp_set_nested routine deprecated, please use omp_set_max_active_levels instead.
  Processing /tmp/test.opt..
  
  ----------------------------------------
  Name: uadd_overflow
    %X = uadd_overflow i8 %a, undef
    %Op = extractvalue {i8, i1} %X, 0
    %Ov = extractvalue {i8, i1} %X, 1
    %OpIsZero = icmp eq %Op, 0
    %NoOverflow = icmp eq %Ov, 0
    %Zero = and i1 %OpIsZero, %NoOverflow
    ret i1 %Zero
  =>
    ret i1 1
  
  Done: 1
  Optimization is correct!

  $ ./src/alive2/build-Clang-release/alive -root-only /tmp/test.opt 
  OMP: Info #270: omp_set_nested routine deprecated, please use omp_set_max_active_levels instead.
  Processing /tmp/test.opt..
  
  ----------------------------------------
  Name: uadd_overflow
    %X = uadd_overflow i8 %a, %b
    %Op = extractvalue {i8, i1} %X, 0
    %Ov = extractvalue {i8, i1} %X, 1
    %OpIsZero = icmp eq %Op, 0
    %NoOverflow = icmp eq %Ov, 0
    %Zero = and i1 %OpIsZero, %NoOverflow
    ret i1 %Zero
  =>
    ret i1 1
  
  ERROR: Value mismatch
  
  Example:
  i8 %a = #xa0 (160)
  i8 %b = #x80 (128)
  
  Source:
  {i8, i1} %X = { #x20 (32), #x1 (0) }
  i8 %Op = #x20 (32)
  i1 %Ov = #x1 (1)
  i1 %OpIsZero = #x0 (0)
  i1 %NoOverflow = #x0 (0)
  i1 %Zero = #x0 (0)
  
  Target:
  Source value: #x0 (0)
  Target value: #x1 (1)

> (Additionally, if alive models udiv semantics correctly, any transformation will be correct by definition (IUB) after a udiv 0 -- I'm assuming that's not how it works though.)




Repository:
  rL LLVM

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

https://reviews.llvm.org/D63065