llvm/test/Transforms/InstSimplify/implies.ll

   1 ; NOTE: Assertions have been autogenerated by utils/update_test_checks.py
   2 ; RUN: opt -S %s -passes=instsimplify | FileCheck %s
   3
   4 ; A ==> A -> true
   5 define i1 @test(i32 %length.i, i32 %i) {
   6 ; CHECK-LABEL: @test(
   7 ; CHECK-NEXT:    ret i1 true
   8 ;
   9   %var29 = icmp slt i32 %i, %length.i
  10   %res = icmp uge i1 %var29, %var29
  11   ret i1 %res
  12 }
  13
  14 ; i +_{nsw} C_{>0} <s L ==> i <s L -> true
  15 define i1 @test2(i32 %length.i, i32 %i) {
  16 ; CHECK-LABEL: @test2(
  17 ; CHECK-NEXT:    ret i1 true
  18 ;
  19   %iplus1 = add nsw i32 %i, 1
  20   %var29 = icmp slt i32 %i, %length.i
  21   %var30 = icmp slt i32 %iplus1, %length.i
  22   %res = icmp ule i1 %var30, %var29
  23   ret i1 %res
  24 }
  25
  26 ; i + C_{>0} <s L ==> i <s L -> unknown without the nsw
  27 define i1 @test2_neg(i32 %length.i, i32 %i) {
  28 ; CHECK-LABEL: @test2_neg(
  29 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add i32 [[I:%.*]], 1
  30 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp slt i32 [[I]], [[LENGTH_I:%.*]]
  31 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp slt i32 [[IPLUS1]], [[LENGTH_I]]
  32 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
  33 ; CHECK-NEXT:    ret i1 [[RES]]
  34 ;
  35   %iplus1 = add i32 %i, 1
  36   %var29 = icmp slt i32 %i, %length.i
  37   %var30 = icmp slt i32 %iplus1, %length.i
  38   %res = icmp ule i1 %var30, %var29
  39   ret i1 %res
  40 }
  41
  42 ; sle is not implication
  43 define i1 @test2_neg2(i32 %length.i, i32 %i) {
  44 ; CHECK-LABEL: @test2_neg2(
  45 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add i32 [[I:%.*]], 1
  46 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp slt i32 [[I]], [[LENGTH_I:%.*]]
  47 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp slt i32 [[IPLUS1]], [[LENGTH_I]]
  48 ; CHECK-NEXT:    [[RES:%.*]] = icmp sle i1 [[VAR30]], [[VAR29]]
  49 ; CHECK-NEXT:    ret i1 [[RES]]
  50 ;
  51   %iplus1 = add i32 %i, 1
  52   %var29 = icmp slt i32 %i, %length.i
  53   %var30 = icmp slt i32 %iplus1, %length.i
  54   %res = icmp sle i1 %var30, %var29
  55   ret i1 %res
  56 }
  57
  58 ; The binary operator has to be an add
  59 define i1 @test2_neg3(i32 %length.i, i32 %i) {
  60 ; CHECK-LABEL: @test2_neg3(
  61 ; CHECK-NEXT:    [[IPLUS1:%.*]] = sub nsw i32 [[I:%.*]], 1
  62 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp slt i32 [[I]], [[LENGTH_I:%.*]]
  63 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp slt i32 [[IPLUS1]], [[LENGTH_I]]
  64 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
  65 ; CHECK-NEXT:    ret i1 [[RES]]
  66 ;
  67   %iplus1 = sub nsw i32 %i, 1
  68   %var29 = icmp slt i32 %i, %length.i
  69   %var30 = icmp slt i32 %iplus1, %length.i
  70   %res = icmp ule i1 %var30, %var29
  71   ret i1 %res
  72 }
  73
  74 ; i +_{nsw} C_{>0} <s L ==> i <s L -> true
  75 ; With an inverted conditional (ule B A rather than canonical ugt A B
  76 define i1 @test3(i32 %length.i, i32 %i) {
  77 ; CHECK-LABEL: @test3(
  78 ; CHECK-NEXT:    ret i1 true
  79 ;
  80   %iplus1 = add nsw i32 %i, 1
  81   %var29 = icmp slt i32 %i, %length.i
  82   %var30 = icmp slt i32 %iplus1, %length.i
  83   %res = icmp uge i1 %var29, %var30
  84   ret i1 %res
  85 }
  86
  87 ; i +_{nuw} C <u L ==> i <u L
  88 define i1 @test4(i32 %length.i, i32 %i) {
  89 ; CHECK-LABEL: @test4(
  90 ; CHECK-NEXT:    ret i1 true
  91 ;
  92   %iplus1 = add nuw i32 %i, 1
  93   %var29 = icmp ult i32 %i, %length.i
  94   %var30 = icmp ult i32 %iplus1, %length.i
  95   %res = icmp ule i1 %var30, %var29
  96   ret i1 %res
  97 }
  98
  99 ; A ==> A for vectors
 100 define <4 x i1> @test5(<4 x i1> %vec) {
 101 ; CHECK-LABEL: @test5(
 102 ; CHECK-NEXT:    ret <4 x i1> <i1 true, i1 true, i1 true, i1 true>
 103 ;
 104   %res = icmp ule <4 x i1> %vec, %vec
 105   ret <4 x i1> %res
 106 }
 107
 108 ; Don't crash on vector inputs - pr25040
 109 define <4 x i1> @test6(<4 x i1> %a, <4 x i1> %b) {
 110 ; CHECK-LABEL: @test6(
 111 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule <4 x i1> [[A:%.*]], [[B:%.*]]
 112 ; CHECK-NEXT:    ret <4 x i1> [[RES]]
 113 ;
 114   %res = icmp ule <4 x i1> %a, %b
 115   ret <4 x i1> %res
 116 }
 117
 118 ; i +_{nsw} 1 <s L  ==> i < L +_{nsw} 1
 119 define i1 @test7(i32 %length.i, i32 %i) {
 120 ; CHECK-LABEL: @test7(
 121 ; CHECK-NEXT:    ret i1 true
 122 ;
 123   %iplus1 = add nsw i32 %i, 1
 124   %len.plus.one = add nsw i32 %length.i, 1
 125   %var29 = icmp slt i32 %i, %len.plus.one
 126   %var30 = icmp slt i32 %iplus1, %length.i
 127   %res = icmp ule i1 %var30, %var29
 128   ret i1 %res
 129 }
 130
 131 ; i +_{nuw} 1 <u L  ==> i < L +_{nuw} 1
 132 define i1 @test8(i32 %length.i, i32 %i) {
 133 ; CHECK-LABEL: @test8(
 134 ; CHECK-NEXT:    ret i1 true
 135 ;
 136   %iplus1 = add nuw i32 %i, 1
 137   %len.plus.one = add nuw i32 %length.i, 1
 138   %var29 = icmp ult i32 %i, %len.plus.one
 139   %var30 = icmp ult i32 %iplus1, %length.i
 140   %res = icmp ule i1 %var30, %var29
 141   ret i1 %res
 142 }
 143
 144 ; i +_{nuw} C <u L ==> i < L, even if C is negative
 145 define i1 @test9(i32 %length.i, i32 %i) {
 146 ; CHECK-LABEL: @test9(
 147 ; CHECK-NEXT:    ret i1 true
 148 ;
 149   %iplus1 = add nuw i32 %i, -100
 150   %var29 = icmp ult i32 %i, %length.i
 151   %var30 = icmp ult i32 %iplus1, %length.i
 152   %res = icmp ule i1 %var30, %var29
 153   ret i1 %res
 154 }
 155
 156 define i1 @test10(i32 %length.i, i32 %x.full) {
 157 ; CHECK-LABEL: @test10(
 158 ; CHECK-NEXT:    [[X:%.*]] = and i32 [[X_FULL:%.*]], -65536
 159 ; CHECK-NEXT:    [[LARGE:%.*]] = or i32 [[X]], 100
 160 ; CHECK-NEXT:    [[SMALL:%.*]] = or i32 [[X]], 90
 161 ; CHECK-NEXT:    [[KNOWN:%.*]] = icmp ult i32 [[LARGE]], [[LENGTH_I:%.*]]
 162 ; CHECK-NEXT:    [[TO_PROVE:%.*]] = icmp ult i32 [[SMALL]], [[LENGTH_I]]
 163 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[KNOWN]], [[TO_PROVE]]
 164 ; CHECK-NEXT:    ret i1 [[RES]]
 165 ;
 166   %x = and i32 %x.full, 4294901760  ;; 4294901760 == 0xffff0000
 167   %large = or i32 %x, 100
 168   %small = or i32 %x, 90
 169   %known = icmp ult i32 %large, %length.i
 170   %to.prove = icmp ult i32 %small, %length.i
 171   %res = icmp ule i1 %known, %to.prove
 172   ret i1 %res
 173 }
 174
 175 define i1 @test10_with_disjoint(i32 %length.i, i32 %x.full) {
 176 ; CHECK-LABEL: @test10_with_disjoint(
 177 ; CHECK-NEXT:    ret i1 true
 178 ;
 179   %x = and i32 %x.full, 4294901760  ;; 4294901760 == 0xffff0000
 180   %large = or disjoint i32 %x, 100
 181   %small = or disjoint i32 %x, 90
 182   %known = icmp ult i32 %large, %length.i
 183   %to.prove = icmp ult i32 %small, %length.i
 184   %res = icmp ule i1 %known, %to.prove
 185   ret i1 %res
 186 }
 187
 188 define i1 @test11(i32 %length.i, i32 %x) {
 189 ; CHECK-LABEL: @test11(
 190 ; CHECK-NEXT:    [[LARGE:%.*]] = or i32 [[X:%.*]], 100
 191 ; CHECK-NEXT:    [[SMALL:%.*]] = or i32 [[X]], 90
 192 ; CHECK-NEXT:    [[KNOWN:%.*]] = icmp ult i32 [[LARGE]], [[LENGTH_I:%.*]]
 193 ; CHECK-NEXT:    [[TO_PROVE:%.*]] = icmp ult i32 [[SMALL]], [[LENGTH_I]]
 194 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[KNOWN]], [[TO_PROVE]]
 195 ; CHECK-NEXT:    ret i1 [[RES]]
 196 ;
 197   %large = or i32 %x, 100
 198   %small = or i32 %x, 90
 199   %known = icmp ult i32 %large, %length.i
 200   %to.prove = icmp ult i32 %small, %length.i
 201   %res = icmp ule i1 %known, %to.prove
 202   ret i1 %res
 203 }
 204
 205 define i1 @test12(i32 %length.i, i32 %x.full) {
 206 ; CHECK-LABEL: @test12(
 207 ; CHECK-NEXT:    [[X:%.*]] = and i32 [[X_FULL:%.*]], -65536
 208 ; CHECK-NEXT:    [[LARGE:%.*]] = or i32 [[X]], 65536
 209 ; CHECK-NEXT:    [[SMALL:%.*]] = or i32 [[X]], 90
 210 ; CHECK-NEXT:    [[KNOWN:%.*]] = icmp ult i32 [[LARGE]], [[LENGTH_I:%.*]]
 211 ; CHECK-NEXT:    [[TO_PROVE:%.*]] = icmp ult i32 [[SMALL]], [[LENGTH_I]]
 212 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[KNOWN]], [[TO_PROVE]]
 213 ; CHECK-NEXT:    ret i1 [[RES]]
 214 ;
 215   %x = and i32 %x.full, 4294901760  ;; 4294901760 == 0xffff0000
 216   %large = or i32 %x, 65536 ;; 65536 == 0x00010000
 217   %small = or i32 %x, 90
 218   %known = icmp ult i32 %large, %length.i
 219   %to.prove = icmp ult i32 %small, %length.i
 220   %res = icmp ule i1 %known, %to.prove
 221   ret i1 %res
 222 }
 223
 224 define i1 @test13(i32 %length.i, i32 %x) {
 225 ; CHECK-LABEL: @test13(
 226 ; CHECK-NEXT:    ret i1 true
 227 ;
 228   %large = add nuw i32 %x, 100
 229   %small = add nuw i32 %x, 90
 230   %known = icmp ult i32 %large, %length.i
 231   %to.prove = icmp ult i32 %small, %length.i
 232   %res = icmp ule i1 %known, %to.prove
 233   ret i1 %res
 234 }
 235
 236 define i1 @test14(i32 %length.i, i32 %x.full) {
 237 ; CHECK-LABEL: @test14(
 238 ; CHECK-NEXT:    [[X:%.*]] = and i32 [[X_FULL:%.*]], -61681
 239 ; CHECK-NEXT:    [[LARGE:%.*]] = or i32 [[X]], 8224
 240 ; CHECK-NEXT:    [[SMALL:%.*]] = or i32 [[X]], 4112
 241 ; CHECK-NEXT:    [[KNOWN:%.*]] = icmp ult i32 [[LARGE]], [[LENGTH_I:%.*]]
 242 ; CHECK-NEXT:    [[TO_PROVE:%.*]] = icmp ult i32 [[SMALL]], [[LENGTH_I]]
 243 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[KNOWN]], [[TO_PROVE]]
 244 ; CHECK-NEXT:    ret i1 [[RES]]
 245 ;
 246   %x = and i32 %x.full, 4294905615  ;; 4294905615 == 0xffff0f0f
 247   %large = or i32 %x, 8224 ;; == 0x2020
 248   %small = or i32 %x, 4112 ;; == 0x1010
 249   %known = icmp ult i32 %large, %length.i
 250   %to.prove = icmp ult i32 %small, %length.i
 251   %res = icmp ule i1 %known, %to.prove
 252   ret i1 %res
 253 }
 254
 255 define i1 @test14_with_disjoint(i32 %length.i, i32 %x.full) {
 256 ; CHECK-LABEL: @test14_with_disjoint(
 257 ; CHECK-NEXT:    ret i1 true
 258 ;
 259   %x = and i32 %x.full, 4294905615  ;; 4294905615 == 0xffff0f0f
 260   %large = or disjoint i32 %x, 8224 ;; == 0x2020
 261   %small = or disjoint i32 %x, 4112 ;; == 0x1010
 262   %known = icmp ult i32 %large, %length.i
 263   %to.prove = icmp ult i32 %small, %length.i
 264   %res = icmp ule i1 %known, %to.prove
 265   ret i1 %res
 266 }
 267
 268 define i1 @test15(i32 %length.i, i32 %x) {
 269 ; CHECK-LABEL: @test15(
 270 ; CHECK-NEXT:    [[LARGE:%.*]] = add nuw i32 [[X:%.*]], 100
 271 ; CHECK-NEXT:    [[SMALL:%.*]] = add nuw i32 [[X]], 110
 272 ; CHECK-NEXT:    [[KNOWN:%.*]] = icmp ult i32 [[LARGE]], [[LENGTH_I:%.*]]
 273 ; CHECK-NEXT:    [[TO_PROVE:%.*]] = icmp ult i32 [[SMALL]], [[LENGTH_I]]
 274 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[KNOWN]], [[TO_PROVE]]
 275 ; CHECK-NEXT:    ret i1 [[RES]]
 276 ;
 277   %large = add nuw i32 %x, 100
 278   %small = add nuw i32 %x, 110
 279   %known = icmp ult i32 %large, %length.i
 280   %to.prove = icmp ult i32 %small, %length.i
 281   %res = icmp ule i1 %known, %to.prove
 282   ret i1 %res
 283 }
 284
 285 ; X >=(s) Y == X ==> Y (i1 1 becomes -1 for reasoning)
 286 define i1 @test_sge(i32 %length.i, i32 %i) {
 287 ; CHECK-LABEL: @test_sge(
 288 ; CHECK-NEXT:    ret i1 true
 289 ;
 290   %iplus1 = add nsw nuw i32 %i, 1
 291   %var29 = icmp ult i32 %i, %length.i
 292   %var30 = icmp ult i32 %iplus1, %length.i
 293   %res = icmp sge i1 %var30, %var29
 294   ret i1 %res
 295 }
 296
 297 ; X <=(s) Y == Y ==> X (i1 1 becomes -1 for reasoning)
 298 define i1 @test_sle(i32 %length.i, i32 %i) {
 299 ; CHECK-LABEL: @test_sle(
 300 ; CHECK-NEXT:    ret i1 true
 301 ;
 302   %iplus1 = add nsw nuw i32 %i, 1
 303   %var29 = icmp ult i32 %i, %length.i
 304   %var30 = icmp ult i32 %iplus1, %length.i
 305   %res = icmp sle i1 %var29, %var30
 306   ret i1 %res
 307 }
 308
 309 ; X +_{nsw} 1 <(s) Y ==> X <(s) Y
 310 define i1 @test_sgt_icmp(i32 %length.i, i32 %i) {
 311 ; CHECK-LABEL: @test_sgt_icmp(
 312 ; CHECK-NEXT:    ret i1 true
 313 ;
 314   %iplus1 = add nsw i32 %i, 1
 315   %var29 = icmp sgt i32 %length.i, %i
 316   %var30 = icmp sgt i32 %length.i, %iplus1
 317   %res = icmp ule i1 %var30, %var29
 318   ret i1 %res
 319 }
 320
 321 ; X +_{nsw} 1 <=(s) Y ==> X <=(s) Y
 322 define i1 @test_sge_icmp(i32 %length.i, i32 %i) {
 323 ; CHECK-LABEL: @test_sge_icmp(
 324 ; CHECK-NEXT:    ret i1 true
 325 ;
 326   %iplus1 = add nsw i32 %i, 1
 327   %var29 = icmp sge i32 %length.i, %i
 328   %var30 = icmp sge i32 %length.i, %iplus1
 329   %res = icmp ule i1 %var30, %var29
 330   ret i1 %res
 331 }
 332
 333 ; X +_{nuw} 1 <(u) Y ==> X <(u) Y
 334 define i1 @test_ugt_icmp(i32 %length.i, i32 %i) {
 335 ; CHECK-LABEL: @test_ugt_icmp(
 336 ; CHECK-NEXT:    ret i1 true
 337 ;
 338   %iplus1 = add nuw i32 %i, 1
 339   %var29 = icmp ugt i32 %length.i, %i
 340   %var30 = icmp ugt i32 %length.i, %iplus1
 341   %res = icmp ule i1 %var30, %var29
 342   ret i1 %res
 343 }
 344
 345 ; X +_{nuw} 1 <=(u) Y ==> X <=(u) Y
 346 define i1 @test_uge_icmp(i32 %length.i, i32 %i) {
 347 ; CHECK-LABEL: @test_uge_icmp(
 348 ; CHECK-NEXT:    ret i1 true
 349 ;
 350   %iplus1 = add nuw i32 %i, 1
 351   %var29 = icmp uge i32 %length.i, %i
 352   %var30 = icmp uge i32 %length.i, %iplus1
 353   %res = icmp ule i1 %var30, %var29
 354   ret i1 %res
 355 }
 356
 357 ; Test from PR70374
 358 define i1 @pr70374(i32 %x, i32 %y, i32 %z) {
 359 ; CHECK-LABEL: @pr70374(
 360 ; CHECK-NEXT:    [[ADD:%.*]] = add nuw i32 [[Y:%.*]], [[Z:%.*]]
 361 ; CHECK-NEXT:    [[CMP1:%.*]] = icmp ule i32 [[ADD]], [[X:%.*]]
 362 ; CHECK-NEXT:    ret i1 [[CMP1]]
 363 ;
 364   %add = add nuw i32 %y, %z
 365   %cmp1 = icmp ule i32 %add, %x
 366   %cmp2 = icmp uge i32 %x, %y
 367   %res = and i1 %cmp2, %cmp1
 368   ret i1 %res
 369 }
 370
 371 define i1 @pr70374_commuted_add(i32 %x, i32 %y, i32 %z) {
 372 ; CHECK-LABEL: @pr70374_commuted_add(
 373 ; CHECK-NEXT:    [[ADD:%.*]] = add nuw i32 [[Z:%.*]], [[Y:%.*]]
 374 ; CHECK-NEXT:    [[CMP1:%.*]] = icmp ule i32 [[ADD]], [[X:%.*]]
 375 ; CHECK-NEXT:    ret i1 [[CMP1]]
 376 ;
 377   %add = add nuw i32 %z, %y
 378   %cmp1 = icmp ule i32 %add, %x
 379   %cmp2 = icmp uge i32 %x, %y
 380   %res = and i1 %cmp2, %cmp1
 381   ret i1 %res
 382 }
 383
 384 define i1 @test_uge_icmp_value(i32 %length.i, i32 %i, i32 %j) {
 385 ; CHECK-LABEL: @test_uge_icmp_value(
 386 ; CHECK-NEXT:    ret i1 true
 387 ;
 388   %iplusj = add nuw i32 %i, %j
 389   %var29 = icmp uge i32 %length.i, %i
 390   %var30 = icmp uge i32 %length.i, %iplusj
 391   %res = icmp ule i1 %var30, %var29
 392   ret i1 %res
 393 }
 394
 395 ; negative case, X + 1 <(s) Y !==> X <(s) Y (X = 0x7fffffff, Y = 0x7fbfffff)
 396 define i1 @test_sgt_icmp_no_nsw(i32 %length.i, i32 %i) {
 397 ; CHECK-LABEL: @test_sgt_icmp_no_nsw(
 398 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add i32 [[I:%.*]], 1
 399 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp sgt i32 [[LENGTH_I:%.*]], [[I]]
 400 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp sgt i32 [[LENGTH_I]], [[IPLUS1]]
 401 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 402 ; CHECK-NEXT:    ret i1 [[RES]]
 403 ;
 404   %iplus1 = add i32 %i, 1
 405   %var29 = icmp sgt i32 %length.i, %i
 406   %var30 = icmp sgt i32 %length.i, %iplus1
 407   %res = icmp ule i1 %var30, %var29
 408   ret i1 %res
 409 }
 410
 411 ; negative case, X +_{nuw} 1 <(s) Y !==> X <(s) Y
 412 define i1 @test_sgt_icmp_nuw(i32 %length.i, i32 %i) {
 413 ; CHECK-LABEL: @test_sgt_icmp_nuw(
 414 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add nuw i32 [[I:%.*]], 1
 415 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp sgt i32 [[I]], [[LENGTH_I:%.*]]
 416 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp sgt i32 [[IPLUS1]], [[LENGTH_I]]
 417 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 418 ; CHECK-NEXT:    ret i1 [[RES]]
 419 ;
 420   %iplus1 = add nuw i32 %i, 1
 421   %var29 = icmp sgt i32 %i, %length.i
 422   %var30 = icmp sgt i32 %iplus1, %length.i
 423   %res = icmp ule i1 %var30, %var29
 424   ret i1 %res
 425 }
 426
 427 ; negative case, X + 1 <=(s) Y !==> X <=(s) Y (X = 0x7fffffff, Y = 0x80000000)
 428 define i1 @test_sge_icmp_no_nsw(i32 %length.i, i32 %i) {
 429 ; CHECK-LABEL: @test_sge_icmp_no_nsw(
 430 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add i32 [[I:%.*]], 1
 431 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp sge i32 [[LENGTH_I:%.*]], [[I]]
 432 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp sge i32 [[LENGTH_I]], [[IPLUS1]]
 433 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 434 ; CHECK-NEXT:    ret i1 [[RES]]
 435 ;
 436   %iplus1 = add i32 %i, 1
 437   %var29 = icmp sge i32 %length.i, %i
 438   %var30 = icmp sge i32 %length.i, %iplus1
 439   %res = icmp ule i1 %var30, %var29
 440   ret i1 %res
 441 }
 442
 443 ; negative case, X +_{nuw} 1 <=(s) Y !==> X <=(s) Y
 444 define i1 @test_sge_icmp_nuw(i32 %length.i, i32 %i) {
 445 ; CHECK-LABEL: @test_sge_icmp_nuw(
 446 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add nuw i32 [[I:%.*]], 1
 447 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp sge i32 [[I]], [[LENGTH_I:%.*]]
 448 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp sge i32 [[IPLUS1]], [[LENGTH_I]]
 449 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 450 ; CHECK-NEXT:    ret i1 [[RES]]
 451 ;
 452   %iplus1 = add nuw i32 %i, 1
 453   %var29 = icmp sge i32 %i, %length.i
 454   %var30 = icmp sge i32 %iplus1, %length.i
 455   %res = icmp ule i1 %var30, %var29
 456   ret i1 %res
 457 }
 458
 459 ;negative case, X + 1 <(u) Y !==> X <(u) Y (X = Y = 0xffffffff)
 460 define i1 @test_ugt_icmp_no_nuw(i32 %length.i, i32 %i) {
 461 ; CHECK-LABEL: @test_ugt_icmp_no_nuw(
 462 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add i32 [[I:%.*]], 1
 463 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp ugt i32 [[LENGTH_I:%.*]], [[I]]
 464 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp ugt i32 [[LENGTH_I]], [[IPLUS1]]
 465 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 466 ; CHECK-NEXT:    ret i1 [[RES]]
 467 ;
 468   %iplus1 = add i32 %i, 1
 469   %var29 = icmp ugt i32 %length.i, %i
 470   %var30 = icmp ugt i32 %length.i, %iplus1
 471   %res = icmp ule i1 %var30, %var29
 472   ret i1 %res
 473 }
 474
 475 ; negative case, X +_{nsw} 1 <(u) Y !==> X <(u) Y (X = 0xffffffff, Y = 0xfffffffe)
 476 define i1 @test_ugt_icmp_nsw(i32 %length.i, i32 %i) {
 477 ; CHECK-LABEL: @test_ugt_icmp_nsw(
 478 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add nsw i32 [[I:%.*]], 1
 479 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp ugt i32 [[LENGTH_I:%.*]], [[I]]
 480 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp ugt i32 [[LENGTH_I]], [[IPLUS1]]
 481 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 482 ; CHECK-NEXT:    ret i1 [[RES]]
 483 ;
 484   %iplus1 = add nsw i32 %i, 1
 485   %var29 = icmp ugt i32 %length.i, %i
 486   %var30 = icmp ugt i32 %length.i, %iplus1
 487   %res = icmp ule i1 %var30, %var29
 488   ret i1 %res
 489 }
 490
 491 ; negative case, X + 1 <=(u) Y !==> X <=(u) Y (X = 0xffffffff, Y = 0x0)
 492 define i1 @test_uge_icmp_no_nuw(i32 %length.i, i32 %i) {
 493 ; CHECK-LABEL: @test_uge_icmp_no_nuw(
 494 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add i32 [[I:%.*]], 1
 495 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp uge i32 [[LENGTH_I:%.*]], [[I]]
 496 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp uge i32 [[LENGTH_I]], [[IPLUS1]]
 497 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 498 ; CHECK-NEXT:    ret i1 [[RES]]
 499 ;
 500   %iplus1 = add i32 %i, 1
 501   %var29 = icmp uge i32 %length.i, %i
 502   %var30 = icmp uge i32 %length.i, %iplus1
 503   %res = icmp ule i1 %var30, %var29
 504   ret i1 %res
 505 }
 506
 507 ; negative case, X +_{nsw} 1 <=(u) Y !==> X <=(u) Y
 508 define i1 @test_uge_icmp_nsw(i32 %length.i, i32 %i) {
 509 ; CHECK-LABEL: @test_uge_icmp_nsw(
 510 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add nsw i32 [[I:%.*]], 1
 511 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp uge i32 [[I]], [[LENGTH_I:%.*]]
 512 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp uge i32 [[IPLUS1]], [[LENGTH_I]]
 513 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 514 ; CHECK-NEXT:    ret i1 [[RES]]
 515 ;
 516   %iplus1 = add nsw i32 %i, 1
 517   %var29 = icmp uge i32 %i, %length.i
 518   %var30 = icmp uge i32 %iplus1, %length.i
 519   %res = icmp ule i1 %var30, %var29
 520   ret i1 %res
 521 }
 522
 523 ; (X >> Z) <=(u) Y ==> X <=(u) Y
 524 define i1 @test_shift(i64 %x, i64 %y, i64 %shift) {
 525 ; CHECK-LABEL: @test_shift(
 526 ; CHECK-NEXT:    [[LSHR:%.*]] = lshr i64 [[X:%.*]], [[SHIFT:%.*]]
 527 ; CHECK-NEXT:    [[ICMP1:%.*]] = icmp ugt i64 [[LSHR]], [[Y:%.*]]
 528 ; CHECK-NEXT:    call void @llvm.assume(i1 [[ICMP1]])
 529 ; CHECK-NEXT:    ret i1 true
 530 ;
 531   %lshr = lshr i64 %x, %shift
 532   %icmp1 = icmp ugt i64 %lshr, %y
 533   %icmp2 = icmp ugt i64 %x, %y
 534   call void @llvm.assume(i1 %icmp1)
 535   ret i1 %icmp2
 536 }
 537
 538 ; (X > Y +_{nuw} 1) ==> X != Y
 539 define i1 @assume_x_ugt_y_plus_1(i64  %x, i64  %y)  {
 540 ; CHECK-LABEL: @assume_x_ugt_y_plus_1(
 541 ; CHECK-NEXT:    [[TMP1:%.*]] = add nuw i64 [[Y:%.*]], 1
 542 ; CHECK-NEXT:    [[TMP2:%.*]] = icmp ugt i64 [[X:%.*]], [[TMP1]]
 543 ; CHECK-NEXT:    tail call void @llvm.assume(i1 [[TMP2]])
 544 ; CHECK-NEXT:    [[TMP3:%.*]] = icmp eq i64 [[X]], [[Y]]
 545 ; CHECK-NEXT:    ret i1 [[TMP3]]
 546 ;
 547   %1 = add nuw i64 %y, 1
 548   %2 = icmp ugt i64 %x, %1
 549   tail call void @llvm.assume(i1 %2)
 550   %3 = icmp eq i64 %x, %y
 551   ret i1 %3
 552 }
 553
 554 ; i <u L ==> i >> C <u L
 555 define i1 @lshr_constant(i32 %length.i, i32 %i) {
 556 ; CHECK-LABEL: @lshr_constant(
 557 ; CHECK-NEXT:    ret i1 true
 558 ;
 559   %shl = lshr i32 %i, 1
 560   %var29 = icmp ult i32 %i, %length.i
 561   %var30 = icmp ult i32 %shl, %length.i
 562   %res = icmp ule i1 %var29, %var30
 563   ret i1 %res
 564 }
 565
 566 ; i <u L ==> i >> V <u L
 567 define i1 @lshr_value(i32 %length.i, i32 %i, i32 %v) {
 568 ; CHECK-LABEL: @lshr_value(
 569 ; CHECK-NEXT:    ret i1 true
 570 ;
 571   %shl = lshr i32 %i, %v
 572   %var29 = icmp ult i32 %i, %length.i
 573   %var30 = icmp ult i32 %shl, %length.i
 574   %res = icmp ule i1 %var29, %var30
 575   ret i1 %res
 576 }
 577
 578 define i1 @same_ops_with_constant(i8 %x) {
 579 ; CHECK-LABEL: @same_ops_with_constant(
 580 ; CHECK-NEXT:    ret i1 true
 581 ;
 582   %cmp1 = icmp sgt i8 %x, 5
 583   %cmp2 = icmp ugt i8 %x, 5
 584   %res = icmp ule i1 %cmp1, %cmp2
 585   ret i1 %res
 586 }
 587
 588 define i1 @same_ops_with_constant_wrong_sign(i8 %x) {
 589 ; CHECK-LABEL: @same_ops_with_constant_wrong_sign(
 590 ; CHECK-NEXT:    [[CMP1:%.*]] = icmp sgt i8 [[X:%.*]], -5
 591 ; CHECK-NEXT:    [[CMP2:%.*]] = icmp ugt i8 [[X]], -5
 592 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[CMP1]], [[CMP2]]
 593 ; CHECK-NEXT:    ret i1 [[RES]]
 594 ;
 595   %cmp1 = icmp sgt i8 %x, -5
 596   %cmp2 = icmp ugt i8 %x, -5
 597   %res = icmp ule i1 %cmp1, %cmp2
 598   ret i1 %res
 599 }
 600
 601 declare void @llvm.assume(i1)