Open bonjune opened 3 months ago
https://alive2.llvm.org/ce/z/Nws3Yr
---------------------------------------- define <4 x i1> @fun0(<4 x i1> %val0, <4 x i1> %val1, <4 x i1> %val2) { entry: %val3 = add <4 x i1> %val1, { 1, 1, 1, 1 } %val4 = xor <4 x i1> { 0, undef, undef, 1 }, %val0 %val5 = and <4 x i1> %val4, %val3 %val6 = sub <4 x i1> %val5, %val0 ret <4 x i1> %val6 } => define <4 x i1> @fun0(<4 x i1> %val0, <4 x i1> %val1, <4 x i1> %val2) nofree willreturn memory(none) { entry: %val4 = xor <4 x i1> %val0, { 0, undef, undef, 1 } %#0 = and <4 x i1> %val4, %val1 %val6 = xor <4 x i1> %#0, { 0, undef, undef, 1 } ret <4 x i1> %val6 } Transformation doesn't verify! ERROR: Target's return value is more undefined Example: <4 x i1> %val0 = < #x0 (0), #x0 (0), #x0 (0), #x0 (0) > <4 x i1> %val1 = < #x0 (0), #x0 (0), #x1 (1), #x0 (0) > <4 x i1> %val2 = < #x0 (0), #x0 (0), #x0 (0), #x0 (0) >
tgt produces <0, undef, undef, 1> while src produces <0, 0, undef, 1> for the given example input. This breaks refinement relation.
tgt
<0, undef, undef, 1>
src
<0, 0, undef, 1>
https://github.com/llvm/llvm-project/blob/f329e3ed9070aee3f4c0ebc80ed62f5c4b645d73/llvm/lib/Transforms/InstCombine/InstCombineAndOrXor.cpp#L4196-L4201
During the transformation, it duplicates x from ((x ^ y) & ~m) ^ y to make a canonical form of ((x ^ y) & m) ^ x (see that x now appears twice). And this miscompilation case happens when x is a vector of possible undef values.
x
((x ^ y) & ~m) ^ y
((x ^ y) & m) ^ x
Please assign this to me, I'd like to work on it, if possible?
https://alive2.llvm.org/ce/z/Nws3Yr
tgt
produces<0, undef, undef, 1>
whilesrc
produces<0, 0, undef, 1>
for the given example input. This breaks refinement relation.https://github.com/llvm/llvm-project/blob/f329e3ed9070aee3f4c0ebc80ed62f5c4b645d73/llvm/lib/Transforms/InstCombine/InstCombineAndOrXor.cpp#L4196-L4201
During the transformation, it duplicates
x
from((x ^ y) & ~m) ^ y
to make a canonical form of((x ^ y) & m) ^ x
(see thatx
now appears twice). And this miscompilation case happens whenx
is a vector of possible undef values.