llvm/test/Transforms/ConstraintElimination/partial-decomposition.ll

; NOTE: Assertions have been autogenerated by utils/update_test_checks.py UTC_ARGS: --version 6
; RUN: opt -passes=constraint-elimination -S %s | FileCheck %s


; %add = add nsw %x, %y decomposes to %x + %y, which requires %x >=s 0 and
; %y >=s 0. Those preconditions are unknown here, so %add should be used as-is,
; which still allows proving %t.
define i1 @precondition_unknown_operand_used_as_is(i16 %x, i16 %y, i16 %z) {
; CHECK-LABEL: define i1 @precondition_unknown_operand_used_as_is(
; CHECK-SAME: i16 [[X:%.*]], i16 [[Y:%.*]], i16 [[Z:%.*]]) {
; CHECK-NEXT:  [[ENTRY:.*:]]
; CHECK-NEXT:    [[ADD:%.*]] = add nsw i16 [[X]], [[Y]]
; CHECK-NEXT:    [[C:%.*]] = icmp ugt i16 [[ADD]], [[Z]]
; CHECK-NEXT:    call void @llvm.assume(i1 [[C]])
; CHECK-NEXT:    ret i1 true
;
entry:
  %add = add nsw i16 %x, %y
  %c = icmp ugt i16 %add, %z
  call void @llvm.assume(i1 %c)
  %t = icmp uge i16 %add, %z
  ret i1 %t
}

; Same as @precondition_unknown_operand_used_as_is, but with preconditions
; holding.
define i1 @decompose_used_when_precondition_holds(i16 %x, i16 %y, i16 %z) {
; CHECK-LABEL: define i1 @decompose_used_when_precondition_holds(
; CHECK-SAME: i16 [[X:%.*]], i16 [[Y:%.*]], i16 [[Z:%.*]]) {
; CHECK-NEXT:  [[ENTRY:.*:]]
; CHECK-NEXT:    [[X_POS:%.*]] = and i16 [[X]], 127
; CHECK-NEXT:    [[Y_POS:%.*]] = and i16 [[Y]], 127
; CHECK-NEXT:    [[ADD:%.*]] = add nuw nsw i16 [[X_POS]], [[Y_POS]]
; CHECK-NEXT:    [[C:%.*]] = icmp ugt i16 [[ADD]], [[Z]]
; CHECK-NEXT:    call void @llvm.assume(i1 [[C]])
; CHECK-NEXT:    ret i1 true
;
entry:
  %x.pos = and i16 %x, 127
  %y.pos = and i16 %y, 127
  %add = add nsw i16 %x.pos, %y.pos
  %c = icmp ugt i16 %add, %z
  call void @llvm.assume(i1 %c)
  %t = icmp uge i16 %add, %z
  ret i1 %t
}

; Constant operands are still folded into the offset when an operand should be
; used as-is, otherwise the constants become opaque variables and %t.1 cannot be
; proven. %t.2 must not be folded.
define void @constants_folded_for_opaque_operand(i16 %x, i16 %y) {
; CHECK-LABEL: define void @constants_folded_for_opaque_operand(
; CHECK-SAME: i16 [[X:%.*]], i16 [[Y:%.*]]) {
; CHECK-NEXT:  [[ENTRY:.*:]]
; CHECK-NEXT:    [[ADD:%.*]] = add nsw i16 [[X]], [[Y]]
; CHECK-NEXT:    [[C:%.*]] = icmp ult i16 [[ADD]], 100
; CHECK-NEXT:    br i1 [[C]], label %[[THEN:.*]], label %[[EXIT:.*]]
; CHECK:       [[THEN]]:
; CHECK-NEXT:    call void @use(i1 true)
; CHECK-NEXT:    [[T_2:%.*]] = icmp ult i16 [[ADD]], 50
; CHECK-NEXT:    call void @use(i1 [[T_2]])
; CHECK-NEXT:    ret void
; CHECK:       [[EXIT]]:
; CHECK-NEXT:    ret void
;
entry:
  %add = add nsw i16 %x, %y
  %c = icmp ult i16 %add, 100
  br i1 %c, label %then, label %exit

then:
  %t.1 = icmp ult i16 %add, 200
  call void @use(i1 %t.1)
  %t.2 = icmp ult i16 %add, 50
  call void @use(i1 %t.2)
  ret void

exit:
  ret void
}

; The precondition of %add does not hold, so %add should be used as-is, but the
; offset of the surrounding add nuw is still folded in: %add + 3 >u %z follows
; from %add >u %z.
define i1 @outer_offset_retained(i16 %x, i16 %y, i16 %z) {
; CHECK-LABEL: define i1 @outer_offset_retained(
; CHECK-SAME: i16 [[X:%.*]], i16 [[Y:%.*]], i16 [[Z:%.*]]) {
; CHECK-NEXT:  [[ENTRY:.*:]]
; CHECK-NEXT:    [[ADD:%.*]] = add nsw i16 [[X]], [[Y]]
; CHECK-NEXT:    [[ADD_3:%.*]] = add nuw i16 [[ADD]], 3
; CHECK-NEXT:    [[C:%.*]] = icmp ugt i16 [[ADD]], [[Z]]
; CHECK-NEXT:    call void @llvm.assume(i1 [[C]])
; CHECK-NEXT:    ret i1 true
;
entry:
  %add = add nsw i16 %x, %y
  %add.3 = add nuw i16 %add, 3
  %c = icmp ugt i16 %add, %z
  call void @llvm.assume(i1 %c)
  %t = icmp ugt i16 %add.3, %z
  ret i1 %t
}

; Same as @outer_offset_retained, but with the opaque expression nested deeper
; and only used in the fact.
define i1 @outer_offset_retained_nested(i16 %x, i16 %y, i16 %z) {
; CHECK-LABEL: define i1 @outer_offset_retained_nested(
; CHECK-SAME: i16 [[X:%.*]], i16 [[Y:%.*]], i16 [[Z:%.*]]) {
; CHECK-NEXT:  [[ENTRY:.*:]]
; CHECK-NEXT:    [[ADD:%.*]] = add nsw i16 [[X]], [[Y]]
; CHECK-NEXT:    [[ADD_3:%.*]] = add nuw i16 [[ADD]], 3
; CHECK-NEXT:    [[ADD_8:%.*]] = add nuw i16 [[ADD_3]], 5
; CHECK-NEXT:    [[C:%.*]] = icmp uge i16 [[Z]], [[ADD_8]]
; CHECK-NEXT:    call void @llvm.assume(i1 [[C]])
; CHECK-NEXT:    ret i1 true
;
entry:
  %add = add nsw i16 %x, %y
  %add.3 = add nuw i16 %add, 3
  %add.8 = add nuw i16 %add.3, 5
  %c = icmp uge i16 %z, %add.8
  call void @llvm.assume(i1 %c)
  %t = icmp ugt i16 %z, %add
  ret i1 %t
}

; The fact is added as %add + 10 <=u %z with %add used as-is, which implies
; %add <=u %z.
define i1 @fact_partially_decomposed(i16 %x, i16 %y, i16 %z) {
; CHECK-LABEL: define i1 @fact_partially_decomposed(
; CHECK-SAME: i16 [[X:%.*]], i16 [[Y:%.*]], i16 [[Z:%.*]]) {
; CHECK-NEXT:  [[ENTRY:.*:]]
; CHECK-NEXT:    [[ADD:%.*]] = add nsw i16 [[X]], [[Y]]
; CHECK-NEXT:    [[ADD_10:%.*]] = add nuw i16 [[ADD]], 10
; CHECK-NEXT:    [[C:%.*]] = icmp ule i16 [[ADD_10]], [[Z]]
; CHECK-NEXT:    call void @llvm.assume(i1 [[C]])
; CHECK-NEXT:    ret i1 true
;
entry:
  %add = add nsw i16 %x, %y
  %add.10 = add nuw i16 %add, 10
  %c = icmp ule i16 %add.10, %z
  call void @llvm.assume(i1 %c)
  %t = icmp ule i16 %add, %z
  ret i1 %t
}

; Looking through the sext requires %x >=s 0, which is unknown. The sext should
; be used as-is, the offset of the surrounding add nuw is still folded in.
define i1 @sext_operand_used_as_is(i16 %x, i32 %z) {
; CHECK-LABEL: define i1 @sext_operand_used_as_is(
; CHECK-SAME: i16 [[X:%.*]], i32 [[Z:%.*]]) {
; CHECK-NEXT:  [[ENTRY:.*:]]
; CHECK-NEXT:    [[EXT:%.*]] = sext i16 [[X]] to i32
; CHECK-NEXT:    [[ADD:%.*]] = add nuw i32 [[EXT]], 4
; CHECK-NEXT:    [[C:%.*]] = icmp ugt i32 [[EXT]], [[Z]]
; CHECK-NEXT:    call void @llvm.assume(i1 [[C]])
; CHECK-NEXT:    ret i1 true
;
entry:
  %ext = sext i16 %x to i32
  %add = add nuw i32 %ext, 4
  %c = icmp ugt i32 %ext, %z
  call void @llvm.assume(i1 %c)
  %t = icmp ugt i32 %add, %z
  ret i1 %t
}

; Decomposing %sub requires %x >=u 4, which is unknown.
define i1 @add_negative_constant_used_as_is(i16 %x, i16 %z) {
; CHECK-LABEL: define i1 @add_negative_constant_used_as_is(
; CHECK-SAME: i16 [[X:%.*]], i16 [[Z:%.*]]) {
; CHECK-NEXT:  [[ENTRY:.*:]]
; CHECK-NEXT:    [[SUB:%.*]] = add i16 [[X]], -4
; CHECK-NEXT:    [[ADD:%.*]] = add nuw i16 [[SUB]], 2
; CHECK-NEXT:    [[C:%.*]] = icmp ugt i16 [[SUB]], [[Z]]
; CHECK-NEXT:    call void @llvm.assume(i1 [[C]])
; CHECK-NEXT:    ret i1 true
;
entry:
  %sub = add i16 %x, -4
  %add = add nuw i16 %sub, 2
  %c = icmp ugt i16 %sub, %z
  call void @llvm.assume(i1 %c)
  %t = icmp ugt i16 %add, %z
  ret i1 %t
}

; Looking through the trunc nsw requires %x >=s 0, which is unknown.
define i1 @trunc_nsw_used_as_is(i32 %x, i16 %z) {
; CHECK-LABEL: define i1 @trunc_nsw_used_as_is(
; CHECK-SAME: i32 [[X:%.*]], i16 [[Z:%.*]]) {
; CHECK-NEXT:  [[ENTRY:.*:]]
; CHECK-NEXT:    [[TR:%.*]] = trunc nsw i32 [[X]] to i16
; CHECK-NEXT:    [[ADD:%.*]] = add nuw i16 [[TR]], 7
; CHECK-NEXT:    [[C:%.*]] = icmp ugt i16 [[TR]], [[Z]]
; CHECK-NEXT:    call void @llvm.assume(i1 [[C]])
; CHECK-NEXT:    ret i1 true
;
entry:
  %tr = trunc nsw i32 %x to i16
  %add = add nuw i16 %tr, 7
  %c = icmp ugt i16 %tr, %z
  call void @llvm.assume(i1 %c)
  %t = icmp ugt i16 %add, %z
  ret i1 %t
}

; The index of a gep nuw does not need to be proven non-negative, so the GEP is
; decomposed even though the precondition of %add does not hold and %add should
; be used as-is.
define i1 @gep_nuw_index_used_as_is(ptr %p, i64 %x, i64 %y) {
; CHECK-LABEL: define i1 @gep_nuw_index_used_as_is(
; CHECK-SAME: ptr [[P:%.*]], i64 [[X:%.*]], i64 [[Y:%.*]]) {
; CHECK-NEXT:  [[ENTRY:.*:]]
; CHECK-NEXT:    [[ADD:%.*]] = add nsw i64 [[X]], [[Y]]
; CHECK-NEXT:    [[C_0:%.*]] = icmp ule i64 [[ADD]], 100
; CHECK-NEXT:    call void @llvm.assume(i1 [[C_0]])
; CHECK-NEXT:    [[GEP:%.*]] = getelementptr nuw i8, ptr [[P]], i64 [[ADD]]
; CHECK-NEXT:    [[GEP_4:%.*]] = getelementptr nuw i8, ptr [[GEP]], i64 4
; CHECK-NEXT:    ret i1 true
;
entry:
  %add = add nsw i64 %x, %y
  %c.0 = icmp ule i64 %add, 100
  call void @llvm.assume(i1 %c.0)
  %gep = getelementptr nuw i8, ptr %p, i64 %add
  %gep.4 = getelementptr nuw i8, ptr %gep, i64 4
  %t = icmp ugt ptr %gep.4, %gep
  ret i1 %t
}

; The inner GEP is nusw but not nuw, so nuw must be proven from the index being
; non-negative. %idx cannot be proven non-negative, so the GEP should be used
; used as-is.
define i1 @gep_nusw_index_not_known_non_negative(ptr %p, i64 %idx) {
; CHECK-LABEL: define i1 @gep_nusw_index_not_known_non_negative(
; CHECK-SAME: ptr [[P:%.*]], i64 [[IDX:%.*]]) {
; CHECK-NEXT:  [[ENTRY:.*:]]
; CHECK-NEXT:    [[GEP:%.*]] = getelementptr inbounds i8, ptr [[P]], i64 [[IDX]]
; CHECK-NEXT:    [[GEP_4:%.*]] = getelementptr inbounds i8, ptr [[GEP]], i64 4
; CHECK-NEXT:    [[T:%.*]] = icmp ugt ptr [[GEP_4]], [[GEP]]
; CHECK-NEXT:    ret i1 [[T]]
;
entry:
  %gep = getelementptr inbounds i8, ptr %p, i64 %idx
  %gep.4 = getelementptr inbounds i8, ptr %gep, i64 4
  %t = icmp ugt ptr %gep.4, %gep
  ret i1 %t
}

; Same as @gep_nusw_index_not_known_non_negative, but with the precondition of
; the index holding, so nuw can be proven and the GEP is decomposed.
define i1 @gep_nusw_index_known_non_negative(ptr %p, i64 %idx) {
; CHECK-LABEL: define i1 @gep_nusw_index_known_non_negative(
; CHECK-SAME: ptr [[P:%.*]], i64 [[IDX:%.*]]) {
; CHECK-NEXT:  [[ENTRY:.*:]]
; CHECK-NEXT:    [[C:%.*]] = icmp sge i64 [[IDX]], 0
; CHECK-NEXT:    call void @llvm.assume(i1 [[C]])
; CHECK-NEXT:    [[GEP:%.*]] = getelementptr inbounds i8, ptr [[P]], i64 [[IDX]]
; CHECK-NEXT:    [[GEP_4:%.*]] = getelementptr inbounds i8, ptr [[GEP]], i64 4
; CHECK-NEXT:    ret i1 true
;
entry:
  %c = icmp sge i64 %idx, 0
  call void @llvm.assume(i1 %c)
  %gep = getelementptr inbounds i8, ptr %p, i64 %idx
  %gep.4 = getelementptr inbounds i8, ptr %gep, i64 4
  %t = icmp ugt ptr %gep.4, %gep
  ret i1 %t
}

; Only the precondition for %add fails; %y.2 must still be decomposed to
; %y + 2 to prove %t.
define i1 @only_one_side_used_as_is(i16 %x, i16 %y) {
; CHECK-LABEL: define i1 @only_one_side_used_as_is(
; CHECK-SAME: i16 [[X:%.*]], i16 [[Y:%.*]]) {
; CHECK-NEXT:  [[ENTRY:.*:]]
; CHECK-NEXT:    [[ADD:%.*]] = add nsw i16 [[X]], [[X]]
; CHECK-NEXT:    [[Y_2:%.*]] = add nuw i16 [[Y]], 2
; CHECK-NEXT:    [[C:%.*]] = icmp ugt i16 [[ADD]], [[Y_2]]
; CHECK-NEXT:    call void @llvm.assume(i1 [[C]])
; CHECK-NEXT:    ret i1 true
;
entry:
  %add = add nsw i16 %x, %x
  %y.2 = add nuw i16 %y, 2
  %c = icmp ugt i16 %add, %y.2
  call void @llvm.assume(i1 %c)
  %t = icmp ugt i16 %add, %y
  ret i1 %t
}

declare void @llvm.assume(i1)
declare void @use(i1)