xref: /llvm-project/llvm/test/Transforms/InstSimplify/implies.ll (revision 38fffa630ee80163dc65e759392ad29798905679)
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
5define 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
15define 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
27define 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
43define 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
59define 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
76define 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
88define 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
100define <4 x i1> @test5(<4 x i1> %vec) {
101; CHECK-LABEL: @test5(
102; CHECK-NEXT:    ret <4 x i1> splat (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
109define <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
119define 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
132define 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
145define 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
156define 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
175define 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
188define 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
205define 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
224define 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
236define 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
255define 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
268define 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)
286define 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)
298define 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
310define 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
322define 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
334define 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
346define 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
358define 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
371define 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
384define 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)
396define 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
412define 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)
428define 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
444define 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)
460define 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)
476define 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)
492define 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
508define 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
524define 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
539define 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
555define 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
567define 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
578define 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
588define 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
601declare void @llvm.assume(i1)
602