Test Failure: Transforms/InstCombine/masked-merge-add.ll

Test source: git

Log:

Source: <stdin>
-- 1. ModuleToFunctionPassAdaptor
-- 1. PassManager<Function> : Skipping NOP
-- 2. InstCombinePass

----------------------------------------
define i32 @p(i32 %x, i32 %y, i32 noundef %m) {
#0:
  %and = and i32 %x, noundef %m
  %neg = xor i32 noundef %m, 4294967295
  %and1 = and i32 %neg, %y
  %ret = add i32 %and, %and1
  ret i32 %ret
}
Transformation seems to be correct! (syntactically equal)

-- 3. InstCombinePass

----------------------------------------
define i32 @p(i32 %x, i32 %y, i32 noundef %m) {
#0:
  %and = and i32 %x, noundef %m
  %neg = xor i32 noundef %m, 4294967295
  %and1 = and i32 %neg, %y
  %ret = add i32 %and, %and1
  ret i32 %ret
}
=>
define i32 @p(i32 %x, i32 %y, i32 noundef %m) {
#0:
  %and = and i32 %x, noundef %m
  %neg = xor i32 noundef %m, 4294967295
  %and1 = and i32 %neg, %y
  %ret = or disjoint i32 %and, %and1
  ret i32 %ret
}
Transformation seems to be correct!

-- 4. PassManager<Function> : Skipping NOP
-- 5. PassManager<Function> : Skipping NOP
-- 6. InstCombinePass

----------------------------------------
define <2 x i32> @p_splatvec(<2 x i32> %x, <2 x i32> %y, <2 x i32> noundef %m) {
#0:
  %and = and <2 x i32> %x, noundef %m
  %neg = xor <2 x i32> noundef %m, { 4294967295, 4294967295 }
  %and1 = and <2 x i32> %neg, %y
  %ret = add <2 x i32> %and, %and1
  ret <2 x i32> %ret
}
Transformation seems to be correct! (syntactically equal)

-- 7. InstCombinePass

----------------------------------------
define <2 x i32> @p_splatvec(<2 x i32> %x, <2 x i32> %y, <2 x i32> noundef %m) {
#0:
  %and = and <2 x i32> %x, noundef %m
  %neg = xor <2 x i32> noundef %m, { 4294967295, 4294967295 }
  %and1 = and <2 x i32> %neg, %y
  %ret = add <2 x i32> %and, %and1
  ret <2 x i32> %ret
}
=>
define <2 x i32> @p_splatvec(<2 x i32> %x, <2 x i32> %y, <2 x i32> noundef %m) {
#0:
  %and = and <2 x i32> %x, noundef %m
  %neg = xor <2 x i32> noundef %m, { 4294967295, 4294967295 }
  %and1 = and <2 x i32> %neg, %y
  %ret = or disjoint <2 x i32> %and, %and1
  ret <2 x i32> %ret
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 8. PassManager<Function> : Skipping NOP
-- 9. PassManager<Function> : Skipping NOP
-- 10. InstCombinePass

----------------------------------------
define <3 x i32> @p_vec_undef(<3 x i32> %x, <3 x i32> %y, <3 x i32> noundef %m) {
#0:
  %and = and <3 x i32> %x, noundef %m
  %neg = xor <3 x i32> noundef %m, { 4294967295, undef, 4294967295 }
  %and1 = and <3 x i32> %neg, %y
  %ret = add <3 x i32> %and, %and1
  ret <3 x i32> %ret
}
Transformation seems to be correct! (syntactically equal)

-- 11. InstCombinePass

----------------------------------------
define <3 x i32> @p_vec_undef(<3 x i32> %x, <3 x i32> %y, <3 x i32> noundef %m) {
#0:
  %and = and <3 x i32> %x, noundef %m
  %neg = xor <3 x i32> noundef %m, { 4294967295, undef, 4294967295 }
  %and1 = and <3 x i32> %neg, %y
  %ret = add <3 x i32> %and, %and1
  ret <3 x i32> %ret
}
=>
define <3 x i32> @p_vec_undef(<3 x i32> %x, <3 x i32> %y, <3 x i32> noundef %m) {
#0:
  %and = and <3 x i32> %x, noundef %m
  %neg = xor <3 x i32> noundef %m, { 4294967295, undef, 4294967295 }
  %and1 = and <3 x i32> %neg, %y
  %ret = or disjoint <3 x i32> %and, %and1
  ret <3 x i32> %ret
}
Transformation doesn't verify! (unsound)
ERROR: Target is more poisonous than source

Example:
<3 x i32> %x = < poison, #x0000000f (15), poison >
<3 x i32> %y = < poison, #x0000000f (15), poison >
<3 x i32> noundef %m = < #x00000000 (0), #x0000000f (15), #x00000000 (0) >

Source:
<3 x i32> %and = < poison, #x0000000f (15), poison >
<3 x i32> %neg = < #xffffffff (4294967295, -1), #x0000000f (15)	[based on undef value], #xffffffff (4294967295, -1) >
<3 x i32> %and1 = < poison, #x0000000f (15), poison >
<3 x i32> %ret = < poison, #x0000001e (30), poison >

Target:
<3 x i32> %and = < poison, #x0000000f (15), poison >
<3 x i32> %neg = < #xffffffff (4294967295, -1), #x0000000f (15), #xffffffff (4294967295, -1) >
<3 x i32> %and1 = < poison, #x0000000f (15), poison >
<3 x i32> %ret = < poison, poison, poison >
Source value: < poison, #x0000001e (30), poison >
Target value: < poison, poison, poison >

Pass: InstCombinePass
Command line: '/home/nlopes/llvm/build/bin/opt' '-load=/home/nlopes/alive2/build/tv/tv.so' '-load-pass-plugin=/home/nlopes/alive2/build/tv/tv.so' '-tv-exit-on-error' '-passes=instcombine' '-S' '-tv-smt-to=20000' '-tv-report-dir=/home/nlopes/alive2/build/logs' '-tv-smt-stats'
Wrote bitcode to: "/home/nlopes/alive2/build/logs/in_GbekqNK9_RgYS.bc"


------------------- SMT STATS -------------------
Num queries: 51
Num invalid: 0
Num skips:   0
Num trivial: 26 (33.8%)
Num timeout: 1 (2.0%)
Num errors:  0 (0.0%)
Num SAT:     44 (86.3%)
Num UNSAT:   6 (11.8%)
Alive2: Transform doesn't verify; aborting!

stderr:

RUN: at line 2: /home/nlopes/alive2/build/opt-alive.sh < /bitbucket/nlopes/llvm/llvm/test/Transforms/InstCombine/masked-merge-add.ll -passes=instcombine -S | /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/InstCombine/masked-merge-add.ll
+ /home/nlopes/alive2/build/opt-alive.sh -passes=instcombine -S
+ /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/InstCombine/masked-merge-add.ll

FileCheck error: '<stdin>' is empty.
FileCheck command line:  /bitbucket/nlopes/llvm/build/bin/FileCheck /bitbucket/nlopes/llvm/llvm/test/Transforms/InstCombine/masked-merge-add.ll

<-- Back