Test Failure: Transforms/InstCombine/rem.ll

Test source: git

Log:

Source: <stdin>
-- 1. ModuleToFunctionPassAdaptor
ERROR: Unsupported instruction:   %v = load volatile i32, ptr %p, align 4
ERROR: Unsupported instruction:   %v = load volatile i32, ptr %p, align 4
ERROR: Unsupported instruction:   %v = load volatile i32, ptr %p, align 4
ERROR: Unsupported instruction:   %v = load volatile i32, ptr %p, align 4
ERROR: Unsupported instruction:   %v = load volatile i32, ptr %p, align 4
-- 1. PassManager<Function> : Skipping NOP
-- 2. InstCombinePass

----------------------------------------
define i64 @rem_signed(i64 %x1, i64 %y2) {
%0:
  %r = sdiv i64 %x1, %y2
  %r7 = mul i64 %r, %y2
  %r8 = sub i64 %x1, %r7
  ret i64 %r8
}
Transformation seems to be correct! (syntactically equal)

-- 3. InstCombinePass

----------------------------------------
define i64 @rem_signed(i64 %x1, i64 %y2) {
%0:
  %r = sdiv i64 %x1, %y2
  %r7 = mul i64 %r, %y2
  %r8 = sub i64 %x1, %r7
  ret i64 %r8
}
=>
define i64 @rem_signed(i64 %x1, i64 %y2) {
%0:
  %x1.fr = freeze i64 %x1
  %1 = srem i64 %x1.fr, %y2
  ret i64 %1
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 4. PassManager<Function> : Skipping NOP
-- 5. PassManager<Function> : Skipping NOP
-- 6. InstCombinePass

----------------------------------------
define <4 x i32> @rem_signed_vec(<4 x i32> %t, <4 x i32> %u) {
%0:
  %k = sdiv <4 x i32> %t, %u
  %l = mul <4 x i32> %k, %u
  %m = sub <4 x i32> %t, %l
  ret <4 x i32> %m
}
Transformation seems to be correct! (syntactically equal)

-- 7. InstCombinePass

----------------------------------------
define <4 x i32> @rem_signed_vec(<4 x i32> %t, <4 x i32> %u) {
%0:
  %k = sdiv <4 x i32> %t, %u
  %l = mul <4 x i32> %k, %u
  %m = sub <4 x i32> %t, %l
  ret <4 x i32> %m
}
=>
define <4 x i32> @rem_signed_vec(<4 x i32> %t, <4 x i32> %u) {
%0:
  %t.fr = freeze <4 x i32> %t
  %1 = srem <4 x i32> %t.fr, %u
  ret <4 x i32> %1
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 8. PassManager<Function> : Skipping NOP
-- 9. PassManager<Function> : Skipping NOP
-- 10. InstCombinePass

----------------------------------------
define i64 @rem_unsigned(i64 %x1, i64 %y2) {
%0:
  %r = udiv i64 %x1, %y2
  %r7 = mul i64 %r, %y2
  %r8 = sub i64 %x1, %r7
  ret i64 %r8
}
Transformation seems to be correct! (syntactically equal)

-- 11. InstCombinePass

----------------------------------------
define i64 @rem_unsigned(i64 %x1, i64 %y2) {
%0:
  %r = udiv i64 %x1, %y2
  %r7 = mul i64 %r, %y2
  %r8 = sub i64 %x1, %r7
  ret i64 %r8
}
=>
define i64 @rem_unsigned(i64 %x1, i64 %y2) {
%0:
  %x1.fr = freeze i64 %x1
  %1 = urem i64 %x1.fr, %y2
  ret i64 %1
}
Transformation doesn't verify! (not unsound)
ERROR: Timeout
-- 12. PassManager<Function> : Skipping NOP
-- 13. PassManager<Function> : Skipping NOP
-- 14. InstCombinePass

----------------------------------------
define i8 @big_divisor(i8 %x) {
%0:
  %rem = urem i8 %x, 129
  ret i8 %rem
}
Transformation seems to be correct! (syntactically equal)

-- 15. InstCombinePass

----------------------------------------
define i8 @big_divisor(i8 %x) {
%0:
  %rem = urem i8 %x, 129
  ret i8 %rem
}
=>
define i8 @big_divisor(i8 %x) {
%0:
  %x.fr = freeze i8 %x
  %1 = icmp ult i8 %x.fr, 129
  %2 = add i8 %x.fr, 127
  %rem = select i1 %1, i8 %x.fr, i8 %2
  ret i8 %rem
}
Transformation seems to be correct!

-- 16. PassManager<Function> : Skipping NOP
-- 17. PassManager<Function> : Skipping NOP
-- 18. InstCombinePass

----------------------------------------
define i5 @biggest_divisor(i5 %x) {
%0:
  %rem = urem i5 %x, 31
  ret i5 %rem
}
Transformation seems to be correct! (syntactically equal)

-- 19. InstCombinePass

----------------------------------------
define i5 @biggest_divisor(i5 %x) {
%0:
  %rem = urem i5 %x, 31
  ret i5 %rem
}
=>
define i5 @biggest_divisor(i5 %x) {
%0:
  %x.fr = freeze i5 %x
  %.not = icmp eq i5 %x.fr, 31
  %rem = select i1 %.not, i5 0, i5 %x.fr
  ret i5 %rem
}
Transformation seems to be correct!

-- 20. PassManager<Function> : Skipping NOP
-- 21. PassManager<Function> : Skipping NOP
-- 22. InstCombinePass

----------------------------------------
define i8 @urem_with_sext_bool_divisor(i1 %x, i8 %y) {
%0:
  %s = sext i1 %x to i8
  %rem = urem i8 %y, %s
  ret i8 %rem
}
Transformation seems to be correct! (syntactically equal)

-- 23. InstCombinePass

----------------------------------------
define i8 @urem_with_sext_bool_divisor(i1 %x, i8 %y) {
%0:
  %s = sext i1 %x to i8
  %rem = urem i8 %y, %s
  ret i8 %rem
}
=>
define i8 @urem_with_sext_bool_divisor(i1 %x, i8 %y) {
%0:
  %1 = icmp eq i8 %y, 255
  %rem = select i1 %1, i8 0, i8 %y
  ret i8 %rem
}
Transformation doesn't verify! (unsound)
ERROR: Value mismatch

Example:
i1 %x = #x1 (1)
i8 %y = undef

Source:
i8 %s = #xff (255, -1)
i8 %rem = #x00 (0)	[based on undef value]

Target:
i1 %1 = #x0 (0)
i8 %rem = #xff (255, -1)
Source value: #x00 (0)
Target value: #xff (255, -1)

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'


------------------- SMT STATS -------------------
Num queries: 31
Num invalid: 0
Num skips:   0
Num trivial: 26 (45.6%)
Num timeout: 3 (9.7%)
Num errors:  0 (0.0%)
Num SAT:     19 (61.3%)
Num UNSAT:   9 (29.0%)
Alive2: Transform doesn't verify; aborting!

stderr:

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

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

NOTE: This test would pass if undef didn't exist!

<-- Back