[InstCombine] miscompilation of `mul (sext X), Y -> select X, -Y, 0`

[bongjunj]

llvm-project/llvm/lib/Transforms/InstCombine/InstCombineMulDivRem.cpp

Lines 474 to 479 in 6de5305

	// mul (sext X), Y -> select X, -Y, 0
	// mul Y, (sext X) -> select X, -Y, 0
	if (match(&I, m_c_Mul(m_OneUse(m_SExt(m_Value(X))), m_Value(Y))) &&
	X->getType()->isIntOrIntVectorTy(1))
	return SelectInst::Create(X, Builder.CreateNeg(Y, "", I.hasNoSignedWrap()),
	ConstantInt::getNullValue(Op0->getType()));

Alive2 report: https://alive2.llvm.org/ce/z/GmGpRE

----------------------------------------
define i8 @sext_multi_uses.2(i8 %a, i1 %b, i8 %x) {
#0:
  %#1 = sext i1 %b to i8
  %#2 = mul nsw i8 %a, %#1
  %#3 = select i1 %b, i8 %#2, i8 %a
  %#4 = sub i8 %#1, %#3
  %f = mul nuw i8 %x, %#1
  %r = add i8 %f, %#4
  ret i8 %r
}
=>
define i8 @sext_multi_uses.2(i8 %a, i1 %b, i8 %x) {
#0:
  %#1 = sub nsw i8 0, %a
  %#2 = xor i8 %x, 255
  %#3 = add i8 %a, %#2
  %r = select i1 %b, i8 %#3, i8 %#1
  ret i8 %r
}
Transformation doesn't verify!

ERROR: Target is more poisonous than source

Example:
i8 %a = #x80 (128, -128)
i1 %b = #x0 (0)
i8 %x = #x00 (0)

Source:
i8 %#1 = #x00 (0)
i8 %#2 = #x00 (0)
i8 %#3 = #x80 (128, -128)
i8 %#4 = #x80 (128, -128)
i8 %f = #x00 (0)
i8 %r = #x80 (128, -128)

Target:
i8 %#1 = poison
i8 %#2 = #xff (255, -1)
i8 %#3 = #x7f (127)
i8 %r = poison
Source value: #x80 (128, -128)
Target value: poison

Summary:
  0 correct transformations
  1 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors

[dtcxzyw]

Fixed by #112893.

----------------------------------------
define i8 @sext_multi_uses.2(i8 %a, i1 %b, i8 %x) {
#0:
  %#1 = sext i1 %b to i8
  %#2 = mul nsw i8 %a, %#1
  %#3 = select i1 %b, i8 %#2, i8 %a
  %#4 = sub i8 %#1, %#3
  %f = mul nuw i8 %x, %#1
  %r = add i8 %f, %#4
  ret i8 %r
}
=>
define i8 @sext_multi_uses.2(i8 %a, i1 %b, i8 %x) {
#0:
  %#1 = sub i8 0, %a
  %#2 = xor i8 %x, 255
  %#3 = add i8 %a, %#2
  %r = select i1 %b, i8 %#3, i8 %#1
  ret i8 %r
}
Transformation seems to be correct!

Summary:
  1 correct transformations
  0 incorrect transformations
  0 failed-to-prove transformations
  0 Alive2 errors