Poison value wrongly propagates through vector operations on an optimized code

[bongjunj]

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

Lines 1050 to 1060 in 5d4a0d5

	// The 'not' op may be included in the sum but not the compare.
	// Strictness of the comparison is irrelevant.
	X = Cmp0;
	Y = Cmp1;
	if (match(FVal, m_c_Add(m_Not(m_Specific(X)), m_Specific(Y)))) {
	// (X u< Y) ? -1 : (~X + Y) --> uadd.sat(~X, Y)
	// (X u< Y) ? -1 : (Y + ~X) --> uadd.sat(Y, ~X)
	BinaryOperator *BO = cast<BinaryOperator>(FVal);
	return Builder.CreateBinaryIntrinsic(
	Intrinsic::uadd_sat, BO->getOperand(0), BO->getOperand(1));
	}

Alive2 report: https://alive2.llvm.org/ce/z/6tSdhb

----------------------------------------
define <2 x i32> @uadd_sat_not_ugt_commute_add.2(<2 x i32> %x, <2 x i32> %yp) {
#0:
  %#1 = sdiv <2 x i32> { 2442, 4242 }, %yp
  %notx = xor <2 x i32> %x, { 4294967295, poison }
  %a = add nuw <2 x i32> %#1, %notx
  %c = icmp ugt <2 x i32> %#1, %x
  %r = select <2 x i1> %c, <2 x i32> { 4294967295, 4294967295 }, <2 x i32> %a
  ret <2 x i32> %r
}
=>
define <2 x i32> @uadd_sat_not_ugt_commute_add.2(<2 x i32> %x, <2 x i32> %yp) {
#0:
  %#1 = sdiv <2 x i32> { 2442, 4242 }, %yp
  %notx = xor <2 x i32> %x, { 4294967295, poison }
  %r = uadd_sat <2 x i32> %#1, %notx
  ret <2 x i32> %r
}
Transformation doesn't verify!

ERROR: Target is more poisonous than source

Example:
<2 x i32> %x = < poison, #x00000000 (0) >
<2 x i32> %yp = < #x00000008 (8), #x0000000e (14) >

Source:
<2 x i32> %#1 = < #x00000131 (305), #x0000012f (303) >
<2 x i32> %notx = < poison, poison >
<2 x i32> %a = < poison, poison >
<2 x i1> %c = < poison, #x1 (1) >
<2 x i32> %r = < poison, #xffffffff (4294967295, -1) >

Target:
<2 x i32> %#1 = < #x00000131 (305), #x0000012f (303) >
<2 x i32> %notx = < poison, poison >
<2 x i32> %r = < poison, poison >
Source value: < poison, #xffffffff (4294967295, -1) >
Target value: < poison, poison >

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