AliveToolkit / alive2

Automatic verification of LLVM optimizations
MIT License
766 stars 97 forks source link

False positive when both `noundef` and `range` attrs are specified #1048

Closed dtcxzyw closed 3 months ago

dtcxzyw commented 3 months ago

Reproducer: https://alive2.llvm.org/ce/z/5Acnpt

define i1 @test(i1 %1, i8 noundef range(i8 -32, -16) %2) {
  %5 = trunc nuw nsw i8 %2 to i4
  %6 = select i1 %1, i4 3, i4 %5
  %7 = trunc i4 %6 to i1
  ret i1 %7
}

----------------------------------------
define i1 @test(i1 %#0, i8 noundef %#1) {
init:
  %#range_%#1 = !range i8 noundef %#1, i8 224, i8 240
  br label %#2

#2:
  %#3 = trunc nsw nuw i8 %#range_%#1 to i4
  %#4 = select i1 %#0, i4 3, i4 %#3
  %#5 = trunc i4 %#4 to i1
  ret i1 %#5
}
=>
define i1 @test(i1 %#0, i8 noundef %#1) nofree willreturn memory(none) {
init:
  %#range_%#1 = !range i8 noundef %#1, i8 224, i8 240
  br label %#2

#2:
  %#3 = trunc i8 %#range_%#1 to i1
  %#4 = or i1 %#3, %#0
  ret i1 %#4
}
Transformation doesn't verify!

ERROR: Target is more poisonous than source

Example:
i1 %#0 = #x1 (1)
i8 noundef %#1 = #x00 (0)

Source:
i8 %#range_%#1 = poison
UB triggered on br

Target:
i8 %#range_%#1 = poison
UB triggered on br
Source value: #x1 (1)
Target value: poison

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

%1 = 0 is an invalid input since it triggers an immediate UB.

cc @nikic