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:    ret i1 true
 159 ;
 160   %x = and i32 %x.full, 4294901760  ;; 4294901760 == 0xffff0000
 161   %large = or i32 %x, 100
 162   %small = or i32 %x, 90
 163   %known = icmp ult i32 %large, %length.i
 164   %to.prove = icmp ult i32 %small, %length.i
 165   %res = icmp ule i1 %known, %to.prove
 166   ret i1 %res
 167 }
 168
 169 define i1 @test11(i32 %length.i, i32 %x) {
 170 ; CHECK-LABEL: @test11(
 171 ; CHECK-NEXT:    [[LARGE:%.*]] = or i32 [[X:%.*]], 100
 172 ; CHECK-NEXT:    [[SMALL:%.*]] = or i32 [[X]], 90
 173 ; CHECK-NEXT:    [[KNOWN:%.*]] = icmp ult i32 [[LARGE]], [[LENGTH_I:%.*]]
 174 ; CHECK-NEXT:    [[TO_PROVE:%.*]] = icmp ult i32 [[SMALL]], [[LENGTH_I]]
 175 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[KNOWN]], [[TO_PROVE]]
 176 ; CHECK-NEXT:    ret i1 [[RES]]
 177 ;
 178   %large = or i32 %x, 100
 179   %small = or i32 %x, 90
 180   %known = icmp ult i32 %large, %length.i
 181   %to.prove = icmp ult i32 %small, %length.i
 182   %res = icmp ule i1 %known, %to.prove
 183   ret i1 %res
 184 }
 185
 186 define i1 @test12(i32 %length.i, i32 %x.full) {
 187 ; CHECK-LABEL: @test12(
 188 ; CHECK-NEXT:    [[X:%.*]] = and i32 [[X_FULL:%.*]], -65536
 189 ; CHECK-NEXT:    [[LARGE:%.*]] = or i32 [[X]], 65536
 190 ; CHECK-NEXT:    [[SMALL:%.*]] = or i32 [[X]], 90
 191 ; CHECK-NEXT:    [[KNOWN:%.*]] = icmp ult i32 [[LARGE]], [[LENGTH_I:%.*]]
 192 ; CHECK-NEXT:    [[TO_PROVE:%.*]] = icmp ult i32 [[SMALL]], [[LENGTH_I]]
 193 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[KNOWN]], [[TO_PROVE]]
 194 ; CHECK-NEXT:    ret i1 [[RES]]
 195 ;
 196   %x = and i32 %x.full, 4294901760  ;; 4294901760 == 0xffff0000
 197   %large = or i32 %x, 65536 ;; 65536 == 0x00010000
 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 @test13(i32 %length.i, i32 %x) {
 206 ; CHECK-LABEL: @test13(
 207 ; CHECK-NEXT:    ret i1 true
 208 ;
 209   %large = add nuw i32 %x, 100
 210   %small = add nuw i32 %x, 90
 211   %known = icmp ult i32 %large, %length.i
 212   %to.prove = icmp ult i32 %small, %length.i
 213   %res = icmp ule i1 %known, %to.prove
 214   ret i1 %res
 215 }
 216
 217 define i1 @test14(i32 %length.i, i32 %x.full) {
 218 ; CHECK-LABEL: @test14(
 219 ; CHECK-NEXT:    ret i1 true
 220 ;
 221   %x = and i32 %x.full, 4294905615  ;; 4294905615 == 0xffff0f0f
 222   %large = or i32 %x, 8224 ;; == 0x2020
 223   %small = or i32 %x, 4112 ;; == 0x1010
 224   %known = icmp ult i32 %large, %length.i
 225   %to.prove = icmp ult i32 %small, %length.i
 226   %res = icmp ule i1 %known, %to.prove
 227   ret i1 %res
 228 }
 229
 230 define i1 @test15(i32 %length.i, i32 %x) {
 231 ; CHECK-LABEL: @test15(
 232 ; CHECK-NEXT:    [[LARGE:%.*]] = add nuw i32 [[X:%.*]], 100
 233 ; CHECK-NEXT:    [[SMALL:%.*]] = add nuw i32 [[X]], 110
 234 ; CHECK-NEXT:    [[KNOWN:%.*]] = icmp ult i32 [[LARGE]], [[LENGTH_I:%.*]]
 235 ; CHECK-NEXT:    [[TO_PROVE:%.*]] = icmp ult i32 [[SMALL]], [[LENGTH_I]]
 236 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[KNOWN]], [[TO_PROVE]]
 237 ; CHECK-NEXT:    ret i1 [[RES]]
 238 ;
 239   %large = add nuw i32 %x, 100
 240   %small = add nuw i32 %x, 110
 241   %known = icmp ult i32 %large, %length.i
 242   %to.prove = icmp ult i32 %small, %length.i
 243   %res = icmp ule i1 %known, %to.prove
 244   ret i1 %res
 245 }
 246
 247 ; X >=(s) Y == X ==> Y (i1 1 becomes -1 for reasoning)
 248 define i1 @test_sge(i32 %length.i, i32 %i) {
 249 ; CHECK-LABEL: @test_sge(
 250 ; CHECK-NEXT:    ret i1 true
 251 ;
 252   %iplus1 = add nsw nuw i32 %i, 1
 253   %var29 = icmp ult i32 %i, %length.i
 254   %var30 = icmp ult i32 %iplus1, %length.i
 255   %res = icmp sge i1 %var30, %var29
 256   ret i1 %res
 257 }
 258
 259 ; X <=(s) Y == Y ==> X (i1 1 becomes -1 for reasoning)
 260 define i1 @test_sle(i32 %length.i, i32 %i) {
 261 ; CHECK-LABEL: @test_sle(
 262 ; CHECK-NEXT:    ret i1 true
 263 ;
 264   %iplus1 = add nsw nuw i32 %i, 1
 265   %var29 = icmp ult i32 %i, %length.i
 266   %var30 = icmp ult i32 %iplus1, %length.i
 267   %res = icmp sle i1 %var29, %var30
 268   ret i1 %res
 269 }
 270
 271 ; X +_{nsw} 1 <(s) Y ==> X <(s) Y
 272 define i1 @test_sgt_icmp(i32 %length.i, i32 %i) {
 273 ; CHECK-LABEL: @test_sgt_icmp(
 274 ; CHECK-NEXT:    ret i1 true
 275 ;
 276   %iplus1 = add nsw i32 %i, 1
 277   %var29 = icmp sgt i32 %length.i, %i
 278   %var30 = icmp sgt i32 %length.i, %iplus1
 279   %res = icmp ule i1 %var30, %var29
 280   ret i1 %res
 281 }
 282
 283 ; X +_{nsw} 1 <=(s) Y ==> X <=(s) Y
 284 define i1 @test_sge_icmp(i32 %length.i, i32 %i) {
 285 ; CHECK-LABEL: @test_sge_icmp(
 286 ; CHECK-NEXT:    ret i1 true
 287 ;
 288   %iplus1 = add nsw i32 %i, 1
 289   %var29 = icmp sge i32 %length.i, %i
 290   %var30 = icmp sge i32 %length.i, %iplus1
 291   %res = icmp ule i1 %var30, %var29
 292   ret i1 %res
 293 }
 294
 295 ; X +_{nuw} 1 <(u) Y ==> X <(u) Y
 296 define i1 @test_ugt_icmp(i32 %length.i, i32 %i) {
 297 ; CHECK-LABEL: @test_ugt_icmp(
 298 ; CHECK-NEXT:    ret i1 true
 299 ;
 300   %iplus1 = add nuw i32 %i, 1
 301   %var29 = icmp ugt i32 %length.i, %i
 302   %var30 = icmp ugt i32 %length.i, %iplus1
 303   %res = icmp ule i1 %var30, %var29
 304   ret i1 %res
 305 }
 306
 307 ; X +_{nuw} 1 <=(u) Y ==> X <=(u) Y
 308 define i1 @test_uge_icmp(i32 %length.i, i32 %i) {
 309 ; CHECK-LABEL: @test_uge_icmp(
 310 ; CHECK-NEXT:    ret i1 true
 311 ;
 312   %iplus1 = add nuw i32 %i, 1
 313   %var29 = icmp uge i32 %length.i, %i
 314   %var30 = icmp uge i32 %length.i, %iplus1
 315   %res = icmp ule i1 %var30, %var29
 316   ret i1 %res
 317 }
 318
 319 ; negative case, X + 1 <(s) Y !==> X <(s) Y (X = 0x7fffffff, Y = 0x7fbfffff)
 320 define i1 @test_sgt_icmp_no_nsw(i32 %length.i, i32 %i) {
 321 ; CHECK-LABEL: @test_sgt_icmp_no_nsw(
 322 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add i32 [[I:%.*]], 1
 323 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp sgt i32 [[LENGTH_I:%.*]], [[I]]
 324 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp sgt i32 [[LENGTH_I]], [[IPLUS1]]
 325 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 326 ; CHECK-NEXT:    ret i1 [[RES]]
 327 ;
 328   %iplus1 = add i32 %i, 1
 329   %var29 = icmp sgt i32 %length.i, %i
 330   %var30 = icmp sgt i32 %length.i, %iplus1
 331   %res = icmp ule i1 %var30, %var29
 332   ret i1 %res
 333 }
 334
 335 ; negative case, X +_{nuw} 1 <(s) Y !==> X <(s) Y
 336 define i1 @test_sgt_icmp_nuw(i32 %length.i, i32 %i) {
 337 ; CHECK-LABEL: @test_sgt_icmp_nuw(
 338 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add nuw i32 [[I:%.*]], 1
 339 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp sgt i32 [[I]], [[LENGTH_I:%.*]]
 340 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp sgt i32 [[IPLUS1]], [[LENGTH_I]]
 341 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 342 ; CHECK-NEXT:    ret i1 [[RES]]
 343 ;
 344   %iplus1 = add nuw i32 %i, 1
 345   %var29 = icmp sgt i32 %i, %length.i
 346   %var30 = icmp sgt i32 %iplus1, %length.i
 347   %res = icmp ule i1 %var30, %var29
 348   ret i1 %res
 349 }
 350
 351 ; negative case, X + 1 <=(s) Y !==> X <=(s) Y (X = 0x7fffffff, Y = 0x80000000)
 352 define i1 @test_sge_icmp_no_nsw(i32 %length.i, i32 %i) {
 353 ; CHECK-LABEL: @test_sge_icmp_no_nsw(
 354 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add i32 [[I:%.*]], 1
 355 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp sge i32 [[LENGTH_I:%.*]], [[I]]
 356 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp sge i32 [[LENGTH_I]], [[IPLUS1]]
 357 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 358 ; CHECK-NEXT:    ret i1 [[RES]]
 359 ;
 360   %iplus1 = add i32 %i, 1
 361   %var29 = icmp sge i32 %length.i, %i
 362   %var30 = icmp sge i32 %length.i, %iplus1
 363   %res = icmp ule i1 %var30, %var29
 364   ret i1 %res
 365 }
 366
 367 ; negative case, X +_{nuw} 1 <=(s) Y !==> X <=(s) Y
 368 define i1 @test_sge_icmp_nuw(i32 %length.i, i32 %i) {
 369 ; CHECK-LABEL: @test_sge_icmp_nuw(
 370 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add nuw i32 [[I:%.*]], 1
 371 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp sge i32 [[I]], [[LENGTH_I:%.*]]
 372 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp sge i32 [[IPLUS1]], [[LENGTH_I]]
 373 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 374 ; CHECK-NEXT:    ret i1 [[RES]]
 375 ;
 376   %iplus1 = add nuw i32 %i, 1
 377   %var29 = icmp sge i32 %i, %length.i
 378   %var30 = icmp sge i32 %iplus1, %length.i
 379   %res = icmp ule i1 %var30, %var29
 380   ret i1 %res
 381 }
 382
 383 ;negative case, X + 1 <(u) Y !==> X <(u) Y (X = Y = 0xffffffff)
 384 define i1 @test_ugt_icmp_no_nuw(i32 %length.i, i32 %i) {
 385 ; CHECK-LABEL: @test_ugt_icmp_no_nuw(
 386 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add i32 [[I:%.*]], 1
 387 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp ugt i32 [[LENGTH_I:%.*]], [[I]]
 388 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp ugt i32 [[LENGTH_I]], [[IPLUS1]]
 389 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 390 ; CHECK-NEXT:    ret i1 [[RES]]
 391 ;
 392   %iplus1 = add i32 %i, 1
 393   %var29 = icmp ugt i32 %length.i, %i
 394   %var30 = icmp ugt i32 %length.i, %iplus1
 395   %res = icmp ule i1 %var30, %var29
 396   ret i1 %res
 397 }
 398
 399 ; negative case, X +_{nsw} 1 <(u) Y !==> X <(u) Y (X = 0xffffffff, Y = 0xfffffffe)
 400 define i1 @test_ugt_icmp_nsw(i32 %length.i, i32 %i) {
 401 ; CHECK-LABEL: @test_ugt_icmp_nsw(
 402 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add nsw i32 [[I:%.*]], 1
 403 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp ugt i32 [[LENGTH_I:%.*]], [[I]]
 404 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp ugt i32 [[LENGTH_I]], [[IPLUS1]]
 405 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 406 ; CHECK-NEXT:    ret i1 [[RES]]
 407 ;
 408   %iplus1 = add nsw i32 %i, 1
 409   %var29 = icmp ugt i32 %length.i, %i
 410   %var30 = icmp ugt i32 %length.i, %iplus1
 411   %res = icmp ule i1 %var30, %var29
 412   ret i1 %res
 413 }
 414
 415 ; negative case, X + 1 <=(u) Y !==> X <=(u) Y (X = 0xffffffff, Y = 0x0)
 416 define i1 @test_uge_icmp_no_nuw(i32 %length.i, i32 %i) {
 417 ; CHECK-LABEL: @test_uge_icmp_no_nuw(
 418 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add i32 [[I:%.*]], 1
 419 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp uge i32 [[LENGTH_I:%.*]], [[I]]
 420 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp uge i32 [[LENGTH_I]], [[IPLUS1]]
 421 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 422 ; CHECK-NEXT:    ret i1 [[RES]]
 423 ;
 424   %iplus1 = add i32 %i, 1
 425   %var29 = icmp uge i32 %length.i, %i
 426   %var30 = icmp uge i32 %length.i, %iplus1
 427   %res = icmp ule i1 %var30, %var29
 428   ret i1 %res
 429 }
 430
 431 ; negative case, X +_{nsw} 1 <=(u) Y !==> X <=(u) Y
 432 define i1 @test_uge_icmp_nsw(i32 %length.i, i32 %i) {
 433 ; CHECK-LABEL: @test_uge_icmp_nsw(
 434 ; CHECK-NEXT:    [[IPLUS1:%.*]] = add nsw i32 [[I:%.*]], 1
 435 ; CHECK-NEXT:    [[VAR29:%.*]] = icmp uge i32 [[I]], [[LENGTH_I:%.*]]
 436 ; CHECK-NEXT:    [[VAR30:%.*]] = icmp uge i32 [[IPLUS1]], [[LENGTH_I]]
 437 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[VAR30]], [[VAR29]]
 438 ; CHECK-NEXT:    ret i1 [[RES]]
 439 ;
 440   %iplus1 = add nsw i32 %i, 1
 441   %var29 = icmp uge i32 %i, %length.i
 442   %var30 = icmp uge i32 %iplus1, %length.i
 443   %res = icmp ule i1 %var30, %var29
 444   ret i1 %res
 445 }
 446
 447 ; (X >> Z) <=(u) Y ==> X <=(u) Y
 448 define i1 @test_shift(i64 %x, i64 %y, i64 %shift) {
 449 ; CHECK-LABEL: @test_shift(
 450 ; CHECK-NEXT:    [[LSHR:%.*]] = lshr i64 [[X:%.*]], [[SHIFT:%.*]]
 451 ; CHECK-NEXT:    [[ICMP1:%.*]] = icmp ugt i64 [[LSHR]], [[Y:%.*]]
 452 ; CHECK-NEXT:    call void @llvm.assume(i1 [[ICMP1]])
 453 ; CHECK-NEXT:    ret i1 true
 454 ;
 455   %lshr = lshr i64 %x, %shift
 456   %icmp1 = icmp ugt i64 %lshr, %y
 457   %icmp2 = icmp ugt i64 %x, %y
 458   call void @llvm.assume(i1 %icmp1)
 459   ret i1 %icmp2
 460 }
 461
 462 ; (X > Y +_{nuw} 1) ==> X != Y
 463 define i1 @assume_x_ugt_y_plus_1(i64  %x, i64  %y)  {
 464 ; CHECK-LABEL: @assume_x_ugt_y_plus_1(
 465 ; CHECK-NEXT:    [[TMP1:%.*]] = add nuw i64 [[Y:%.*]], 1
 466 ; CHECK-NEXT:    [[TMP2:%.*]] = icmp ugt i64 [[X:%.*]], [[TMP1]]
 467 ; CHECK-NEXT:    tail call void @llvm.assume(i1 [[TMP2]])
 468 ; CHECK-NEXT:    [[TMP3:%.*]] = icmp eq i64 [[X]], [[Y]]
 469 ; CHECK-NEXT:    ret i1 [[TMP3]]
 470 ;
 471   %1 = add nuw i64 %y, 1
 472   %2 = icmp ugt i64 %x, %1
 473   tail call void @llvm.assume(i1 %2)
 474   %3 = icmp eq i64 %x, %y
 475   ret i1 %3
 476 }
 477
 478 ; i <u L ==> i >> C <u L
 479 define i1 @lshr_constant(i32 %length.i, i32 %i) {
 480 ; CHECK-LABEL: @lshr_constant(
 481 ; CHECK-NEXT:    ret i1 true
 482 ;
 483   %shl = lshr i32 %i, 1
 484   %var29 = icmp ult i32 %i, %length.i
 485   %var30 = icmp ult i32 %shl, %length.i
 486   %res = icmp ule i1 %var29, %var30
 487   ret i1 %res
 488 }
 489
 490 ; i <u L ==> i >> V <u L
 491 define i1 @lshr_value(i32 %length.i, i32 %i, i32 %v) {
 492 ; CHECK-LABEL: @lshr_value(
 493 ; CHECK-NEXT:    ret i1 true
 494 ;
 495   %shl = lshr i32 %i, %v
 496   %var29 = icmp ult i32 %i, %length.i
 497   %var30 = icmp ult i32 %shl, %length.i
 498   %res = icmp ule i1 %var29, %var30
 499   ret i1 %res
 500 }
 501
 502 define i1 @same_ops_with_constant(i8 %x) {
 503 ; CHECK-LABEL: @same_ops_with_constant(
 504 ; CHECK-NEXT:    ret i1 true
 505 ;
 506   %cmp1 = icmp sgt i8 %x, 5
 507   %cmp2 = icmp ugt i8 %x, 5
 508   %res = icmp ule i1 %cmp1, %cmp2
 509   ret i1 %res
 510 }
 511
 512 define i1 @same_ops_with_constant_wrong_sign(i8 %x) {
 513 ; CHECK-LABEL: @same_ops_with_constant_wrong_sign(
 514 ; CHECK-NEXT:    [[CMP1:%.*]] = icmp sgt i8 [[X:%.*]], -5
 515 ; CHECK-NEXT:    [[CMP2:%.*]] = icmp ugt i8 [[X]], -5
 516 ; CHECK-NEXT:    [[RES:%.*]] = icmp ule i1 [[CMP1]], [[CMP2]]
 517 ; CHECK-NEXT:    ret i1 [[RES]]
 518 ;
 519   %cmp1 = icmp sgt i8 %x, -5
 520   %cmp2 = icmp ugt i8 %x, -5
 521   %res = icmp ule i1 %cmp1, %cmp2
 522   ret i1 %res
 523 }
 524
 525 declare void @llvm.assume(i1)