Skip to content

Commit 2409daf

Browse files
fhahnfhahn
committed
[ConstraintElim] Handle trivial (ICMP_ULE, 0, B) in doesHold.
D152730 may add trivial pre-conditions of the form (ICMP_ULE, 0, B), which won't be handled automatically by the constraint system, because we don't add Var >= 0 for all variables in the unsigned system. Handling the trivial condition explicitly here avoids having the increase the number of rows in the system per variable. https://alive2.llvm.org/ce/z/QC92ur Depends on D152730. Fixes llvm#63125. Reviewed By: nikic Differential Revision: https://reviews.llvm.org/D158776
1 parent 2019612 commit 2409daf

14 files changed

+216
-69
lines changed

‎llvm/lib/Transforms/Scalar/ConstraintElimination.cpp

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -675,6 +675,17 @@ ConstraintInfo::getConstraint(CmpInst::Predicate Pred, Value *Op0, Value *Op1,
675675
ConstraintTy ConstraintInfo::getConstraintForSolving(CmpInst::Predicate Pred,
676676
Value *Op0,
677677
Value *Op1) const {
678+
Constant *NullC = Constant::getNullValue(Op0->getType());
679+
// Handle trivially true compares directly to avoid adding V UGE 0 constraints
680+
// for all variables in the unsigned system.
681+
if ((Pred == CmpInst::ICMP_ULE && Op0 == NullC) ||
682+
(Pred == CmpInst::ICMP_UGE && Op1 == NullC)) {
683+
auto &Value2Index = getValue2Index(false);
684+
// Return constraint that's trivially true.
685+
return ConstraintTy(SmallVector<int64_t, 8>(Value2Index.size(), 0), false,
686+
false, false);
687+
}
688+
678689
// If both operands are known to be non-negative, change signed predicates to
679690
// unsigned ones. This increases the reasoning effectiveness in combination
680691
// with the signed <-> unsigned transfer logic.

‎llvm/test/Transforms/ConstraintElimination/add-nsw.ll

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -774,8 +774,7 @@ define i1 @add_neg_1_known_sge_uge_1(i32 %a) {
774774
; CHECK-NEXT: [[A_SGE:%.*]] = icmp sge i32 [[A:%.*]], 1
775775
; CHECK-NEXT: call void @llvm.assume(i1 [[A_SGE]])
776776
; CHECK-NEXT: [[SUB:%.*]] = add nsw i32 [[A]], -1
777-
; CHECK-NEXT: [[C:%.*]] = icmp uge i32 [[SUB]], 0
778-
; CHECK-NEXT: ret i1 [[C]]
777+
; CHECK-NEXT: ret i1 true
779778
;
780779
entry:
781780
%a.sge = icmp sge i32 %a, 1
@@ -808,8 +807,7 @@ define i1 @add_neg_1_not_known_sge_uge_1(i32 %a) {
808807
; CHECK-NEXT: [[A_SGE:%.*]] = icmp sge i32 [[A:%.*]], 0
809808
; CHECK-NEXT: call void @llvm.assume(i1 [[A_SGE]])
810809
; CHECK-NEXT: [[SUB:%.*]] = add nsw i32 [[A]], -1
811-
; CHECK-NEXT: [[C:%.*]] = icmp uge i32 [[SUB]], 0
812-
; CHECK-NEXT: ret i1 [[C]]
810+
; CHECK-NEXT: ret i1 true
813811
;
814812
entry:
815813
%a.sge = icmp sge i32 %a, 0
@@ -842,8 +840,7 @@ define i1 @add_neg_3_known_sge_uge_1(i32 %a) {
842840
; CHECK-NEXT: [[A_SGE:%.*]] = icmp sge i32 [[A:%.*]], 4
843841
; CHECK-NEXT: call void @llvm.assume(i1 [[A_SGE]])
844842
; CHECK-NEXT: [[SUB:%.*]] = add nsw i32 [[A]], -3
845-
; CHECK-NEXT: [[C:%.*]] = icmp uge i32 [[SUB]], 0
846-
; CHECK-NEXT: ret i1 [[C]]
843+
; CHECK-NEXT: ret i1 true
847844
;
848845
entry:
849846
%a.sge = icmp sge i32 %a, 4
@@ -876,8 +873,7 @@ define i1 @add_neg_3_not_known_sge_uge_1(i32 %a) {
876873
; CHECK-NEXT: [[A_SGE:%.*]] = icmp sge i32 [[A:%.*]], 2
877874
; CHECK-NEXT: call void @llvm.assume(i1 [[A_SGE]])
878875
; CHECK-NEXT: [[SUB:%.*]] = add nsw i32 [[A]], -3
879-
; CHECK-NEXT: [[C:%.*]] = icmp uge i32 [[SUB]], 0
880-
; CHECK-NEXT: ret i1 [[C]]
876+
; CHECK-NEXT: ret i1 true
881877
;
882878
entry:
883879
%a.sge = icmp sge i32 %a, 2

‎llvm/test/Transforms/ConstraintElimination/add-nuw.ll

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -227,9 +227,7 @@ define void @test.decompose.nonconst(i8 %a, i8 %b, i8 %c, i8 %d) {
227227
; CHECK-NEXT: [[AND_0:%.*]] = and i1 [[C_0]], [[C_1]]
228228
; CHECK-NEXT: br i1 [[AND_0]], label [[IF_THEN:%.*]], label [[IF_END:%.*]]
229229
; CHECK: if.then:
230-
; CHECK-NEXT: [[C_2:%.*]] = icmp uge i8 [[A]], 0
231-
; CHECK-NEXT: [[C_3:%.*]] = icmp uge i8 [[B]], 0
232-
; CHECK-NEXT: [[AND_1:%.*]] = and i1 [[C_2]], [[C_3]]
230+
; CHECK-NEXT: [[AND_1:%.*]] = and i1 true, true
233231
; CHECK-NEXT: br i1 [[AND_1]], label [[IF_THEN_2:%.*]], label [[IF_END]]
234232
; CHECK: if.then.2:
235233
; CHECK-NEXT: [[ADD_0:%.*]] = add nuw i8 [[A]], [[B]]

‎llvm/test/Transforms/ConstraintElimination/and.ll

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -118,10 +118,9 @@ exit:
118118
define i4 @and_compare_undef(i4 %N, i4 %step) {
119119
; CHECK-LABEL: @and_compare_undef(
120120
; CHECK-NEXT: step.check:
121-
; CHECK-NEXT: [[STEP_POS:%.*]] = icmp uge i4 [[STEP:%.*]], 0
122121
; CHECK-NEXT: [[B1:%.*]] = add i4 undef, -1
123122
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i4 [[B1]], [[N:%.*]]
124-
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 [[STEP_POS]], [[STEP_ULT_N]]
123+
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 true, [[STEP_ULT_N]]
125124
; CHECK-NEXT: br i1 [[AND_STEP]], label [[PTR_CHECK:%.*]], label [[EXIT:%.*]]
126125
; CHECK: ptr.check:
127126
; CHECK-NEXT: br label [[EXIT]]

‎llvm/test/Transforms/ConstraintElimination/gep-arithmetic-add.ll

Lines changed: 8 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,9 @@ define i1 @n_unknown(ptr %dst, i32 %n, i32 %i) {
1414
; CHECK: exit:
1515
; CHECK-NEXT: ret i1 false
1616
; CHECK: pre.bb.2:
17-
; CHECK-NEXT: [[PRE_2:%.*]] = icmp uge i32 [[I:%.*]], 0
18-
; CHECK-NEXT: br i1 [[PRE_2]], label [[TGT_BB:%.*]], label [[EXIT]]
17+
; CHECK-NEXT: br i1 true, label [[TGT_BB:%.*]], label [[EXIT]]
1918
; CHECK: tgt.bb:
20-
; CHECK-NEXT: [[CMP1:%.*]] = icmp ult i32 [[I]], [[N]]
19+
; CHECK-NEXT: [[CMP1:%.*]] = icmp ult i32 [[I:%.*]], [[N]]
2120
; CHECK-NEXT: ret i1 [[CMP1]]
2221
;
2322
entry:
@@ -50,10 +49,9 @@ define i1 @n_known_zero_due_to_nuw(ptr %dst, i32 %n, i32 %i) {
5049
; CHECK: exit:
5150
; CHECK-NEXT: ret i1 false
5251
; CHECK: pre.bb.2:
53-
; CHECK-NEXT: [[PRE_2:%.*]] = icmp uge i32 [[I:%.*]], 0
54-
; CHECK-NEXT: br i1 [[PRE_2]], label [[TGT_BB:%.*]], label [[EXIT]]
52+
; CHECK-NEXT: br i1 true, label [[TGT_BB:%.*]], label [[EXIT]]
5553
; CHECK: tgt.bb:
56-
; CHECK-NEXT: [[CMP1:%.*]] = icmp ult i32 [[I]], [[N]]
54+
; CHECK-NEXT: [[CMP1:%.*]] = icmp ult i32 [[I:%.*]], [[N]]
5755
; CHECK-NEXT: ret i1 [[CMP1]]
5856
;
5957
entry:
@@ -86,10 +84,9 @@ define i4 @inc_ptr_N_could_be_negative(ptr %src, ptr %lower, ptr %upper, i8 %N,
8684
; CHECK: trap.bb:
8785
; CHECK-NEXT: ret i4 2
8886
; CHECK: step.check:
89-
; CHECK-NEXT: [[STEP_POS:%.*]] = icmp uge i8 [[STEP:%.*]], 0
90-
; CHECK-NEXT: [[NEXT:%.*]] = add nuw nsw i8 [[STEP]], 2
87+
; CHECK-NEXT: [[NEXT:%.*]] = add nuw nsw i8 [[STEP:%.*]], 2
9188
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i8 [[NEXT]], [[N]]
92-
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 [[STEP_POS]], [[STEP_ULT_N]]
89+
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 true, [[STEP_ULT_N]]
9390
; CHECK-NEXT: br i1 [[AND_STEP]], label [[PTR_CHECK:%.*]], label [[EXIT:%.*]]
9491
; CHECK: ptr.check:
9592
; CHECK-NEXT: [[SRC_STEP:%.*]] = getelementptr inbounds i8, ptr [[SRC]], i8 [[STEP]]
@@ -141,10 +138,9 @@ define i4 @inc_ptr_src_uge_end(ptr %src, ptr %lower, ptr %upper, i16 %N, i16 %st
141138
; CHECK: trap.bb:
142139
; CHECK-NEXT: ret i4 2
143140
; CHECK: step.check:
144-
; CHECK-NEXT: [[STEP_POS:%.*]] = icmp uge i16 [[STEP:%.*]], 0
145-
; CHECK-NEXT: [[NEXT:%.*]] = add nuw nsw i16 [[STEP]], 2
141+
; CHECK-NEXT: [[NEXT:%.*]] = add nuw nsw i16 [[STEP:%.*]], 2
146142
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i16 [[NEXT]], [[N]]
147-
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 [[STEP_POS]], [[STEP_ULT_N]]
143+
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 true, [[STEP_ULT_N]]
148144
; CHECK-NEXT: br i1 [[AND_STEP]], label [[PTR_CHECK:%.*]], label [[EXIT:%.*]]
149145
; CHECK: ptr.check:
150146
; CHECK-NEXT: [[SRC_STEP:%.*]] = getelementptr inbounds i8, ptr [[SRC]], i16 [[STEP]]

‎llvm/test/Transforms/ConstraintElimination/gep-arithmetic.ll

Lines changed: 12 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -325,9 +325,8 @@ define i4 @ptr_N_and_step_signed_positive_unsigned_checks_only(ptr %src, ptr %lo
325325
; CHECK: trap.bb:
326326
; CHECK-NEXT: ret i4 2
327327
; CHECK: step.check:
328-
; CHECK-NEXT: [[STEP_UGE_0:%.*]] = icmp uge i16 [[STEP:%.*]], 0
329-
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i16 [[STEP]], [[N]]
330-
; CHECK-NEXT: [[AND_2:%.*]] = and i1 [[STEP_UGE_0]], [[STEP_ULT_N]]
328+
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i16 [[STEP:%.*]], [[N]]
329+
; CHECK-NEXT: [[AND_2:%.*]] = and i1 true, [[STEP_ULT_N]]
331330
; CHECK-NEXT: br i1 [[AND_2]], label [[PTR_CHECK:%.*]], label [[EXIT:%.*]]
332331
; CHECK: ptr.check:
333332
; CHECK-NEXT: [[SRC_STEP:%.*]] = getelementptr inbounds i8, ptr [[SRC]], i16 1
@@ -381,9 +380,8 @@ define i4 @ptr_N_signed_positive(ptr %src, ptr %lower, ptr %upper, i16 %N, i16 %
381380
; CHECK: trap.bb:
382381
; CHECK-NEXT: ret i4 2
383382
; CHECK: step.check:
384-
; CHECK-NEXT: [[STEP_POS:%.*]] = icmp uge i16 [[STEP:%.*]], 0
385-
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i16 [[STEP]], [[N]]
386-
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 [[STEP_POS]], [[STEP_ULT_N]]
383+
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i16 [[STEP:%.*]], [[N]]
384+
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 true, [[STEP_ULT_N]]
387385
; CHECK-NEXT: br i1 [[AND_STEP]], label [[PTR_CHECK:%.*]], label [[EXIT:%.*]]
388386
; CHECK: ptr.check:
389387
; CHECK-NEXT: [[SRC_STEP:%.*]] = getelementptr inbounds i8, ptr [[SRC]], i16 [[STEP]]
@@ -432,9 +430,8 @@ define i4 @ptr_N_could_be_negative(ptr %src, ptr %lower, ptr %upper, i8 %N, i8 %
432430
; CHECK: trap.bb:
433431
; CHECK-NEXT: ret i4 2
434432
; CHECK: step.check:
435-
; CHECK-NEXT: [[STEP_POS:%.*]] = icmp uge i8 [[STEP:%.*]], 0
436-
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i8 [[STEP]], [[N]]
437-
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 [[STEP_POS]], [[STEP_ULT_N]]
433+
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i8 [[STEP:%.*]], [[N]]
434+
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 true, [[STEP_ULT_N]]
438435
; CHECK-NEXT: br i1 [[AND_STEP]], label [[PTR_CHECK:%.*]], label [[EXIT:%.*]]
439436
; CHECK: ptr.check:
440437
; CHECK-NEXT: [[SRC_STEP:%.*]] = getelementptr inbounds i8, ptr [[SRC]], i8 [[STEP]]
@@ -485,9 +482,8 @@ define i4 @ptr_src_uge_end(ptr %src, ptr %lower, ptr %upper, i8 %N, i8 %step) {
485482
; CHECK: trap.bb:
486483
; CHECK-NEXT: ret i4 2
487484
; CHECK: step.check:
488-
; CHECK-NEXT: [[STEP_POS:%.*]] = icmp uge i8 [[STEP:%.*]], 0
489-
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i8 [[STEP]], [[N]]
490-
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 [[STEP_POS]], [[STEP_ULT_N]]
485+
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i8 [[STEP:%.*]], [[N]]
486+
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 true, [[STEP_ULT_N]]
491487
; CHECK-NEXT: br i1 [[AND_STEP]], label [[PTR_CHECK:%.*]], label [[EXIT:%.*]]
492488
; CHECK: ptr.check:
493489
; CHECK-NEXT: [[SRC_STEP:%.*]] = getelementptr inbounds i8, ptr [[SRC]], i8 [[STEP]]
@@ -541,9 +537,8 @@ define i4 @ptr_N_unsigned_positive(ptr %src, ptr %lower, ptr %upper, i16 %N, i16
541537
; CHECK: trap.bb:
542538
; CHECK-NEXT: ret i4 2
543539
; CHECK: step.check:
544-
; CHECK-NEXT: [[STEP_POS:%.*]] = icmp uge i16 [[STEP:%.*]], 0
545-
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i16 [[STEP]], [[N]]
546-
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 [[STEP_POS]], [[STEP_ULT_N]]
540+
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i16 [[STEP:%.*]], [[N]]
541+
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 true, [[STEP_ULT_N]]
547542
; CHECK-NEXT: br i1 [[AND_STEP]], label [[PTR_CHECK:%.*]], label [[EXIT:%.*]]
548543
; CHECK: ptr.check:
549544
; CHECK-NEXT: [[SRC_STEP:%.*]] = getelementptr inbounds i8, ptr [[SRC]], i16 [[STEP]]
@@ -596,9 +591,8 @@ define i4 @ptr_N_signed_positive_assume(ptr %src, ptr %lower, ptr %upper, i16 %N
596591
; CHECK: trap.bb:
597592
; CHECK-NEXT: ret i4 2
598593
; CHECK: step.check:
599-
; CHECK-NEXT: [[STEP_POS:%.*]] = icmp uge i16 [[STEP:%.*]], 0
600-
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i16 [[STEP]], [[N]]
601-
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 [[STEP_POS]], [[STEP_ULT_N]]
594+
; CHECK-NEXT: [[STEP_ULT_N:%.*]] = icmp ult i16 [[STEP:%.*]], [[N]]
595+
; CHECK-NEXT: [[AND_STEP:%.*]] = and i1 true, [[STEP_ULT_N]]
602596
; CHECK-NEXT: br i1 [[AND_STEP]], label [[PTR_CHECK:%.*]], label [[EXIT:%.*]]
603597
; CHECK: ptr.check:
604598
; CHECK-NEXT: [[SRC_STEP:%.*]] = getelementptr inbounds i8, ptr [[SRC]], i16 [[STEP]]

‎llvm/test/Transforms/ConstraintElimination/loops-header-tested-pointer-cmps.ll

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -572,15 +572,12 @@ define void @ne_check_in_loop_with_zext(ptr %ptr, ptr %lower, ptr %upper, i8 %n)
572572
; CHECK-NEXT: br i1 [[EXITCOND]], label [[FOR_BODY:%.*]], label [[FOR_END:%.*]]
573573
; CHECK: for.body:
574574
; CHECK-NEXT: [[GEP_IV:%.*]] = getelementptr inbounds i8, ptr [[PTR]], i16 [[IV]]
575-
; CHECK-NEXT: [[CMP_IV_UPPER:%.*]] = icmp ule ptr [[UPPER]], [[GEP_IV]]
576-
; CHECK-NEXT: [[OR:%.*]] = or i1 false, [[CMP_IV_UPPER]]
575+
; CHECK-NEXT: [[OR:%.*]] = or i1 false, false
577576
; CHECK-NEXT: br i1 [[OR]], label [[TRAP]], label [[FOR_BODY_1:%.*]]
578577
; CHECK: for.body.1:
579578
; CHECK-NEXT: [[ADD:%.*]] = add nuw nsw i16 [[IV]], 1
580579
; CHECK-NEXT: [[GEP_IV_1:%.*]] = getelementptr inbounds i8, ptr [[PTR]], i16 [[ADD]]
581-
; CHECK-NEXT: [[CMP_IV_1_LOWER:%.*]] = icmp ugt ptr [[LOWER]], [[GEP_IV_1]]
582-
; CHECK-NEXT: [[CMP_IV_1_UPPER:%.*]] = icmp ule ptr [[UPPER]], [[GEP_IV_1]]
583-
; CHECK-NEXT: [[OR_1:%.*]] = or i1 [[CMP_IV_1_LOWER]], [[CMP_IV_1_UPPER]]
580+
; CHECK-NEXT: [[OR_1:%.*]] = or i1 false, false
584581
; CHECK-NEXT: br i1 [[OR_1]], label [[TRAP]], label [[FOR_LATCH]]
585582
; CHECK: for.latch:
586583
; CHECK-NEXT: store i8 0, ptr [[GEP_IV]], align 4

‎llvm/test/Transforms/ConstraintElimination/loops-header-tested-pointer-iv.ll

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -55,8 +55,7 @@ define void @loop_pointer_iv_null_start(ptr %end, ptr %upper) {
5555
; CHECK-NEXT: [[IV:%.*]] = phi ptr [ null, [[ENTRY:%.*]] ], [ [[IV_NEXT:%.*]], [[LOOP_LATCH:%.*]] ]
5656
; CHECK-NEXT: [[C_1:%.*]] = icmp ule ptr [[IV]], [[END]]
5757
; CHECK-NEXT: call void @use(i1 [[C_1]])
58-
; CHECK-NEXT: [[C_2:%.*]] = icmp uge ptr [[IV]], null
59-
; CHECK-NEXT: call void @use(i1 [[C_2]])
58+
; CHECK-NEXT: call void @use(i1 true)
6059
; CHECK-NEXT: [[C_3:%.*]] = icmp ule ptr [[IV]], [[END]]
6160
; CHECK-NEXT: br i1 [[C_3]], label [[LOOP_LATCH]], label [[EXIT]]
6261
; CHECK: loop.latch:

0 commit comments

Comments
 (0)