; NOTE: Assertions have been autogenerated by utils/update_test_checks.py
; RUN: opt < %s -passes=instsimplify -S | FileCheck %s
target datalayout = "p:32:32-p1:64:64"

; This is a collection of tests checking whether we can prove pointers
; derived from two allocas as inequal *via offset checks*.  Note that
; instcombine has alternate approaches (one cmp rule, and compare
; bases of common offset) that also handles these, but with different
; logic.

; %a follows %b, derived equal
define i1 @adjacent_alloca() {
; CHECK-LABEL: @adjacent_alloca(
; CHECK-NEXT:    [[A:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[B:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[B_OFF:%.*]] = getelementptr i8, ptr [[B]], i64 4
; CHECK-NEXT:    [[RES:%.*]] = icmp ne ptr [[A]], [[B_OFF]]
; CHECK-NEXT:    ret i1 [[RES]]
;
  %a = alloca i8, i32 4
  %b = alloca i8, i32 4
  %b.off = getelementptr i8, ptr %b, i64 4
  %res = icmp ne ptr %a, %b.off
  ret i1 %res
}

; %b follows %a, derived equal
define i1 @adjacent_alloca2() {
; CHECK-LABEL: @adjacent_alloca2(
; CHECK-NEXT:    [[A:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[B:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[A_OFF:%.*]] = getelementptr i8, ptr [[A]], i64 4
; CHECK-NEXT:    [[RES:%.*]] = icmp ne ptr [[A_OFF]], [[B]]
; CHECK-NEXT:    ret i1 [[RES]]
;
  %a = alloca i8, i32 4
  %b = alloca i8, i32 4
  %a.off = getelementptr i8, ptr %a, i64 4
  %res = icmp ne ptr %a.off, %b
  ret i1 %res
}

; FIXME: Can't be equal
define i1 @positive_non_equal_end() {
; CHECK-LABEL: @positive_non_equal_end(
; CHECK-NEXT:    [[A:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[B:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[A_OFF:%.*]] = getelementptr i8, ptr [[A]], i64 4
; CHECK-NEXT:    [[B_OFF:%.*]] = getelementptr i8, ptr [[B]], i64 4
; CHECK-NEXT:    [[RES:%.*]] = icmp ne ptr [[A_OFF]], [[B_OFF]]
; CHECK-NEXT:    ret i1 [[RES]]
;
  %a = alloca i8, i32 4
  %b = alloca i8, i32 4
  %a.off = getelementptr i8, ptr %a, i64 4
  %b.off = getelementptr i8, ptr %b, i64 4
  %res = icmp ne ptr %a.off, %b.off
  ret i1 %res
}

; %b follows %a, derived equal
define i1 @positive_equal_past_end() {
; CHECK-LABEL: @positive_equal_past_end(
; CHECK-NEXT:    [[A:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[B:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[A_OFF:%.*]] = getelementptr i8, ptr [[A]], i64 8
; CHECK-NEXT:    [[B_OFF:%.*]] = getelementptr i8, ptr [[B]], i64 12
; CHECK-NEXT:    [[RES:%.*]] = icmp ne ptr [[A_OFF]], [[B_OFF]]
; CHECK-NEXT:    ret i1 [[RES]]
;
  %a = alloca i8, i32 4
  %b = alloca i8, i32 4
  %a.off = getelementptr i8, ptr %a, i64 8
  %b.off = getelementptr i8, ptr %b, i64 12
  %res = icmp ne ptr %a.off, %b.off
  ret i1 %res
}

define i1 @positive_non_equal() {
; CHECK-LABEL: @positive_non_equal(
; CHECK-NEXT:    ret i1 true
;
  %a = alloca i8, i32 4
  %b = alloca i8, i32 4
  %a.off = getelementptr i8, ptr %a, i64 3
  %b.off = getelementptr i8, ptr %b, i64 3
  %res = icmp ne ptr %a.off, %b.off
  ret i1 %res
}

; %a follows %b, derived equal
define i1 @one_neg_equal1() {
; CHECK-LABEL: @one_neg_equal1(
; CHECK-NEXT:    [[A:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[B:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[A_OFF:%.*]] = getelementptr i8, ptr [[A]], i64 -1
; CHECK-NEXT:    [[B_OFF:%.*]] = getelementptr i8, ptr [[B]], i64 3
; CHECK-NEXT:    [[RES:%.*]] = icmp ne ptr [[A_OFF]], [[B_OFF]]
; CHECK-NEXT:    ret i1 [[RES]]
;
  %a = alloca i8, i32 4
  %b = alloca i8, i32 4
  %a.off = getelementptr i8, ptr %a, i64 -1
  %b.off = getelementptr i8, ptr %b, i64 3
  %res = icmp ne ptr %a.off, %b.off
  ret i1 %res
}

; %b follows %a, derived equal
define i1 @one_neg_equal2() {
; CHECK-LABEL: @one_neg_equal2(
; CHECK-NEXT:    [[A:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[B:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[A_OFF:%.*]] = getelementptr i8, ptr [[A]], i64 3
; CHECK-NEXT:    [[B_OFF:%.*]] = getelementptr i8, ptr [[B]], i64 -1
; CHECK-NEXT:    [[RES:%.*]] = icmp ne ptr [[A_OFF]], [[B_OFF]]
; CHECK-NEXT:    ret i1 [[RES]]
;
  %a = alloca i8, i32 4
  %b = alloca i8, i32 4
  %a.off = getelementptr i8, ptr %a, i64 3
  %b.off = getelementptr i8, ptr %b, i64 -1
  %res = icmp ne ptr %a.off, %b.off
  ret i1 %res
}

; %b follows %a, derived equal
define i1 @both_neg_equal() {
; CHECK-LABEL: @both_neg_equal(
; CHECK-NEXT:    [[A:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[B:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[A_OFF:%.*]] = getelementptr i8, ptr [[A]], i64 -4
; CHECK-NEXT:    [[B_OFF:%.*]] = getelementptr i8, ptr [[B]], i64 -8
; CHECK-NEXT:    [[RES:%.*]] = icmp ne ptr [[A_OFF]], [[B_OFF]]
; CHECK-NEXT:    ret i1 [[RES]]
;
  %a = alloca i8, i32 4
  %b = alloca i8, i32 4
  %a.off = getelementptr i8, ptr %a, i64 -4
  %b.off = getelementptr i8, ptr %b, i64 -8
  %res = icmp ne ptr %a.off, %b.off
  ret i1 %res
}

; FIXME: Can't be equal
define i1 @mixed_offsets1() {
; CHECK-LABEL: @mixed_offsets1(
; CHECK-NEXT:    [[A:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[B:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[A_OFF:%.*]] = getelementptr i8, ptr [[A]], i64 -1
; CHECK-NEXT:    [[B_OFF:%.*]] = getelementptr i8, ptr [[B]], i64 2
; CHECK-NEXT:    [[RES:%.*]] = icmp ne ptr [[A_OFF]], [[B_OFF]]
; CHECK-NEXT:    ret i1 [[RES]]
;
  %a = alloca i8, i32 4
  %b = alloca i8, i32 4
  %a.off = getelementptr i8, ptr %a, i64 -1
  %b.off = getelementptr i8, ptr %b, i64 2
  %res = icmp ne ptr %a.off, %b.off
  ret i1 %res
}

; FIXME: Can't be equal
define i1 @mixed_offsets2() {
; CHECK-LABEL: @mixed_offsets2(
; CHECK-NEXT:    [[A:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[B:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[A_OFF:%.*]] = getelementptr i8, ptr [[A]], i64 1
; CHECK-NEXT:    [[B_OFF:%.*]] = getelementptr i8, ptr [[B]], i64 -2
; CHECK-NEXT:    [[RES:%.*]] = icmp ne ptr [[A_OFF]], [[B_OFF]]
; CHECK-NEXT:    ret i1 [[RES]]
;
  %a = alloca i8, i32 4
  %b = alloca i8, i32 4
  %a.off = getelementptr i8, ptr %a, i64 1
  %b.off = getelementptr i8, ptr %b, i64 -2
  %res = icmp ne ptr %a.off, %b.off
  ret i1 %res
}

; FIXME: Can't be equal
define i1 @negative_in_other() {
; CHECK-LABEL: @negative_in_other(
; CHECK-NEXT:    [[A:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[B:%.*]] = alloca i8, i32 4, align 1
; CHECK-NEXT:    [[A_OFF:%.*]] = getelementptr i8, ptr [[A]], i64 -3
; CHECK-NEXT:    [[B_OFF:%.*]] = getelementptr i8, ptr [[B]], i64 -2
; CHECK-NEXT:    [[RES:%.*]] = icmp ne ptr [[A_OFF]], [[B_OFF]]
; CHECK-NEXT:    ret i1 [[RES]]
;
  %a = alloca i8, i32 4
  %b = alloca i8, i32 4
  %a.off = getelementptr i8, ptr %a, i64 -3
  %b.off = getelementptr i8, ptr %b, i64 -2
  %res = icmp ne ptr %a.off, %b.off
  ret i1 %res
}


attributes #0 = { null_pointer_is_valid }