llvm/test/Transforms/ConstraintElimination/unsigned-query-signed-system.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

define i1 @ult_query_via_signed_system(i64 %a, i64 %b, i64 %n) {
; CHECK-LABEL: define i1 @ult_query_via_signed_system(
; CHECK-SAME: i64 [[A:%.*]], i64 [[B:%.*]], i64 [[N:%.*]]) {
; CHECK-NEXT:    [[PRE_0:%.*]] = icmp sgt i64 [[B]], -1
; CHECK-NEXT:    call void @llvm.assume(i1 [[PRE_0]])
; CHECK-NEXT:    [[S:%.*]] = sub nsw i64 [[A]], [[B]]
; CHECK-NEXT:    [[PRE_1:%.*]] = icmp sgt i64 [[S]], -1
; CHECK-NEXT:    call void @llvm.assume(i1 [[PRE_1]])
; CHECK-NEXT:    [[PRE_2:%.*]] = icmp slt i64 [[A]], [[N]]
; CHECK-NEXT:    call void @llvm.assume(i1 [[PRE_2]])
; CHECK-NEXT:    ret i1 true
;
  %pre.0 = icmp sgt i64 %b, -1
  call void @llvm.assume(i1 %pre.0)
  %s = sub nsw i64 %a, %b
  %pre.1 = icmp sgt i64 %s, -1
  call void @llvm.assume(i1 %pre.1)
  %pre.2 = icmp slt i64 %a, %n
  call void @llvm.assume(i1 %pre.2)
  %c = icmp ult i64 %s, %n
  ret i1 %c
}

; Same as @ult_query_via_signed_system, but here the negation of the unsigned
; query is proven.
define i1 @uge_query_via_signed_system(i64 %a, i64 %b, i64 %n) {
; CHECK-LABEL: define i1 @uge_query_via_signed_system(
; CHECK-SAME: i64 [[A:%.*]], i64 [[B:%.*]], i64 [[N:%.*]]) {
; CHECK-NEXT:    [[PRE_0:%.*]] = icmp sgt i64 [[B]], -1
; CHECK-NEXT:    call void @llvm.assume(i1 [[PRE_0]])
; CHECK-NEXT:    [[S:%.*]] = sub nsw i64 [[A]], [[B]]
; CHECK-NEXT:    [[PRE_1:%.*]] = icmp sgt i64 [[S]], -1
; CHECK-NEXT:    call void @llvm.assume(i1 [[PRE_1]])
; CHECK-NEXT:    [[PRE_2:%.*]] = icmp slt i64 [[A]], [[N]]
; CHECK-NEXT:    call void @llvm.assume(i1 [[PRE_2]])
; CHECK-NEXT:    ret i1 false
;
  %pre.0 = icmp sgt i64 %b, -1
  call void @llvm.assume(i1 %pre.0)
  %s = sub nsw i64 %a, %b
  %pre.1 = icmp sgt i64 %s, -1
  call void @llvm.assume(i1 %pre.1)
  %pre.2 = icmp slt i64 %a, %n
  call void @llvm.assume(i1 %pre.2)
  %c = icmp uge i64 %s, %n
  ret i1 %c
}

define i1 @no_fold_operands_may_be_negative(i64 %a, i64 %b) {
; CHECK-LABEL: define i1 @no_fold_operands_may_be_negative(
; CHECK-SAME: i64 [[A:%.*]], i64 [[B:%.*]]) {
; CHECK-NEXT:    [[PRE_0:%.*]] = icmp slt i64 [[A]], [[B]]
; CHECK-NEXT:    call void @llvm.assume(i1 [[PRE_0]])
; CHECK-NEXT:    [[Q:%.*]] = icmp ult i64 [[A]], [[B]]
; CHECK-NEXT:    ret i1 [[Q]]
;
  %pre.0 = icmp slt i64 %a, %b
  call void @llvm.assume(i1 %pre.0)
  %q = icmp ult i64 %a, %b
  ret i1 %q
}

define i1 @no_fold_only_rhs_non_negative(i64 %a, i64 %b) {
; CHECK-LABEL: define i1 @no_fold_only_rhs_non_negative(
; CHECK-SAME: i64 [[A:%.*]], i64 [[B:%.*]]) {
; CHECK-NEXT:    [[PRE_0:%.*]] = icmp sgt i64 [[B]], -1
; CHECK-NEXT:    call void @llvm.assume(i1 [[PRE_0]])
; CHECK-NEXT:    [[PRE_1:%.*]] = icmp slt i64 [[A]], [[B]]
; CHECK-NEXT:    call void @llvm.assume(i1 [[PRE_1]])
; CHECK-NEXT:    [[Q:%.*]] = icmp ult i64 [[A]], [[B]]
; CHECK-NEXT:    ret i1 [[Q]]
;
  %pre.0 = icmp sgt i64 %b, -1
  call void @llvm.assume(i1 %pre.0)
  %pre.1 = icmp slt i64 %a, %b
  call void @llvm.assume(i1 %pre.1)
  %q = icmp ult i64 %a, %b
  ret i1 %q
}