AliveToolkit / alive2

Automatic verification of LLVM optimizations
MIT License
719 stars 93 forks source link

wrong `xor` computation #1056

Closed bonjune closed 2 weeks ago

bonjune commented 2 weeks ago

https://alive2.llvm.org/ce/z/aUbdVr

https://alive2.llvm.org/ce/z/9kl88Y

xor instruction in the optimized IR produces -3 as a result of 0 and -1. (See %$#1 = xor ... for both cases). It incurs for alive-tv to report a false value mismatch alarm.

The lli result below, for the second case, demonstrates that those xor must produces -1.

@.str = private unnamed_addr constant [12 x i8] c"Result: %d\0a\00", align 1

declare i32 @printf(i8*, ...)

define i32 @main() {
entry:
  %result0 = call i10 @fun0(i10 0)
  %result1 = call i10 @fun1(i10 0)
  %1 = sext i10 %result0 to i32
  %2 = sext i10 %result1 to i32
  %3 = call i32 (i8*, ...) @printf(i8* getelementptr inbounds ([12 x i8], [12 x i8]* @.str, i32 0, i32 0), i32 %1)
  %4 = call i32 (i8*, ...) @printf(i8* getelementptr inbounds ([12 x i8], [12 x i8]* @.str, i32 0, i32 0), i32 %2)
  ret i32 0
}

define i10 @fun0(i10 %val0) {
entry:
  %val1 = urem i10 %val0, 42
  %val2 = sub i10 0, %val1
  %val3 = and i10 %val1, %val2
  %val4 = add i10 %val3, -1
  ret i10 %val4
}

define i10 @fun1(i10 %val0) {
entry:
  %val1 = urem i10 %val0, 42
  %0 = add nsw i10 %val1, -1
  %1 = xor i10 %val1, -1
  %val4 = and i10 %0, %1
  ret i10 %val4
}
lli test.ll
Result: -1
Result: -1

nunoplopes commented 2 weeks ago

This is a bug in LLVM, not in Alive2. The optimization doesn't handle undef correctly.