Skip to content

Commit 1a42296

Browse files
citymarinacitymarina
committed
[ConstraintElim] NE implies SLT if SLE and SGT if SGE
https://alive2.llvm.org/ce/z/bsa7t5 Also, if there is an unsigned predicate but both operands are known to be >= 0, we can also check against the signed predicate information.
1 parent 0e7ec03 commit 1a42296

File tree

4 files changed

+224
-29
lines changed

4 files changed

+224
-29
lines changed

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

Lines changed: 46 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -1378,6 +1378,20 @@ void State::addInfoForInductions(BasicBlock &BB) {
13781378
void State::addInfoFor(BasicBlock &BB) {
13791379
addInfoForInductions(BB);
13801380

1381+
auto AddConditionFact = [&](DomTreeNode *DTN, CmpInst::Predicate Pred,
1382+
Value *Op0, Value *Op1) {
1383+
WorkList.emplace_back(FactOrCheck::getConditionFact(DTN, Pred, Op0, Op1));
1384+
// In the case of NE zero, we can deduce SLT if SLE and SGT if SGE.
1385+
if (Pred == CmpInst::ICMP_NE && match(Op1, m_Zero())) {
1386+
ConditionTy Precond = {CmpInst::ICMP_SLE, Op0, Op1};
1387+
WorkList.emplace_back(FactOrCheck::getConditionFact(
1388+
DTN, CmpInst::ICMP_SLT, Op0, Op1, Precond));
1389+
Precond = {CmpInst::ICMP_SGE, Op0, Op1};
1390+
WorkList.emplace_back(FactOrCheck::getConditionFact(
1391+
DTN, CmpInst::ICMP_SGT, Op0, Op1, Precond));
1392+
}
1393+
};
1394+
13811395
// True as long as long as the current instruction is guaranteed to execute.
13821396
bool GuaranteedToExecute = true;
13831397
// Queue conditions and assumes.
@@ -1418,8 +1432,7 @@ void State::addInfoFor(BasicBlock &BB) {
14181432
if (GuaranteedToExecute) {
14191433
// The assume is guaranteed to execute when BB is entered, hence Cond
14201434
// holds on entry to BB.
1421-
WorkList.emplace_back(FactOrCheck::getConditionFact(
1422-
DT.getNode(I.getParent()), Pred, A, B));
1435+
AddConditionFact(DT.getNode(I.getParent()), Pred, A, B);
14231436
} else {
14241437
WorkList.emplace_back(
14251438
FactOrCheck::getInstFact(DT.getNode(I.getParent()), &I));
@@ -1505,8 +1518,8 @@ void State::addInfoFor(BasicBlock &BB) {
15051518
Value *V = Case.getCaseValue();
15061519
if (!canAddSuccessor(BB, Succ))
15071520
continue;
1508-
WorkList.emplace_back(FactOrCheck::getConditionFact(
1509-
DT.getNode(Succ), CmpInst::ICMP_EQ, Switch->getCondition(), V));
1521+
AddConditionFact(DT.getNode(Succ), CmpInst::ICMP_EQ,
1522+
Switch->getCondition(), V);
15101523
}
15111524
return;
15121525
}
@@ -1553,8 +1566,7 @@ void State::addInfoFor(BasicBlock &BB) {
15531566
V = new ZExtInst(V, PN.getType());
15541567
ExtraCmps.push_back(cast<Instruction>(V));
15551568
}
1556-
WorkList.push_back(FactOrCheck::getConditionFact(
1557-
DT.getNode(&BB), CmpInst::ICMP_ULE, &PN, V));
1569+
AddConditionFact(DT.getNode(&BB), CmpInst::ICMP_ULE, &PN, V);
15581570
}
15591571
}
15601572

@@ -1566,12 +1578,10 @@ void State::addInfoFor(BasicBlock &BB) {
15661578
V && !NeedZExt &&
15671579
(!PN.getType()->isPointerTy() || V->getType() == PN.getType());
15681580
if (CanBuildCmp && SE.isKnownPredicate(CmpInst::ICMP_SGE, IV, StartV)) {
1569-
WorkList.push_back(FactOrCheck::getConditionFact(
1570-
DT.getNode(&BB), CmpInst::ICMP_SGE, &PN, V));
1581+
AddConditionFact(DT.getNode(&BB), CmpInst::ICMP_SGE, &PN, V);
15711582
}
15721583
if (CanBuildCmp && SE.isKnownPredicate(CmpInst::ICMP_UGE, IV, StartV)) {
1573-
WorkList.push_back(FactOrCheck::getConditionFact(
1574-
DT.getNode(&BB), CmpInst::ICMP_UGE, &PN, V));
1584+
AddConditionFact(DT.getNode(&BB), CmpInst::ICMP_UGE, &PN, V);
15751585
}
15761586
}
15771587
}
@@ -1625,11 +1635,11 @@ void State::addInfoFor(BasicBlock &BB) {
16251635
while (!CondWorkList.empty()) {
16261636
Value *Cur = CondWorkList.pop_back_val();
16271637
if (auto *Cmp = dyn_cast<ICmpInst>(Cur)) {
1628-
WorkList.emplace_back(FactOrCheck::getConditionFact(
1638+
AddConditionFact(
16291639
DT.getNode(Successor),
16301640
IsOr ? CmpInst::getInversePredicate(Cmp->getPredicate())
16311641
: Cmp->getPredicate(),
1632-
Cmp->getOperand(0), Cmp->getOperand(1)));
1642+
Cmp->getOperand(0), Cmp->getOperand(1));
16331643
continue;
16341644
}
16351645
if (IsOr && match(Cur, m_LogicalOr(m_Value(Op0), m_Value(Op1)))) {
@@ -1652,15 +1662,13 @@ void State::addInfoFor(BasicBlock &BB) {
16521662
return;
16531663
if (canAddSuccessor(BB, Br->getSuccessor(0))) {
16541664
addPointerBoundInfoFromOverflowCheck(CmpI, DT.getNode(Br->getSuccessor(0)));
1655-
WorkList.emplace_back(FactOrCheck::getConditionFact(
1656-
DT.getNode(Br->getSuccessor(0)), CmpI->getPredicate(),
1657-
CmpI->getOperand(0), CmpI->getOperand(1)));
1665+
AddConditionFact(DT.getNode(Br->getSuccessor(0)), CmpI->getPredicate(),
1666+
CmpI->getOperand(0), CmpI->getOperand(1));
16581667
}
16591668
if (canAddSuccessor(BB, Br->getSuccessor(1)))
1660-
WorkList.emplace_back(FactOrCheck::getConditionFact(
1661-
DT.getNode(Br->getSuccessor(1)),
1662-
CmpInst::getInversePredicate(CmpI->getPredicate()), CmpI->getOperand(0),
1663-
CmpI->getOperand(1)));
1669+
AddConditionFact(DT.getNode(Br->getSuccessor(1)),
1670+
CmpInst::getInversePredicate(CmpI->getPredicate()),
1671+
CmpI->getOperand(0), CmpI->getOperand(1));
16641672
}
16651673

16661674
#ifndef NDEBUG
@@ -1910,6 +1918,25 @@ static bool checkAndReplaceCondition(
19101918
checkCondition(Cmp->getPredicate(), Cmp->getOperand(0),
19111919
Cmp->getOperand(1), Cmp, Info))
19121920
return ReplaceCmpWithConstant(Cmp, *ImpliedCondition);
1921+
1922+
// If the predicate is unsigned and both operands are >= 0, then we can also
1923+
// make use of the signed predicate information.
1924+
if (Cmp->isUnsigned()) {
1925+
auto IsGE = [&](Value *Op) {
1926+
if (!Op->getType()->isIntegerTy())
1927+
return false;
1928+
auto Cond = checkCondition(CmpInst::ICMP_SGE, Op,
1929+
ConstantInt::get(Op->getType(), 0), Cmp, Info);
1930+
return Cond && *Cond;
1931+
};
1932+
if (IsGE(Cmp->getOperand(0)) && IsGE(Cmp->getOperand(1))) {
1933+
if (auto ImpliedCondition =
1934+
checkCondition(Cmp->getSignedPredicate(), Cmp->getOperand(0),
1935+
Cmp->getOperand(1), Cmp, Info))
1936+
return ReplaceCmpWithConstant(Cmp, *ImpliedCondition);
1937+
}
1938+
}
1939+
19131940
return false;
19141941
}
19151942

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

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -757,8 +757,7 @@ define i1 @add_neg_1_known_sge_ult_1(i32 %a) {
757757
; CHECK-NEXT: [[A_SGE:%.*]] = icmp sge i32 [[A:%.*]], 1
758758
; CHECK-NEXT: call void @llvm.assume(i1 [[A_SGE]])
759759
; CHECK-NEXT: [[SUB:%.*]] = add nsw i32 [[A]], -1
760-
; CHECK-NEXT: [[C:%.*]] = icmp ult i32 [[SUB]], [[A]]
761-
; CHECK-NEXT: ret i1 [[C]]
760+
; CHECK-NEXT: ret i1 true
762761
;
763762
entry:
764763
%a.sge = icmp sge i32 %a, 1
@@ -823,8 +822,7 @@ define i1 @add_neg_3_known_sge_ult_1(i32 %a) {
823822
; CHECK-NEXT: [[A_SGE:%.*]] = icmp sge i32 [[A:%.*]], 3
824823
; CHECK-NEXT: call void @llvm.assume(i1 [[A_SGE]])
825824
; CHECK-NEXT: [[SUB:%.*]] = add nsw i32 [[A]], -3
826-
; CHECK-NEXT: [[C:%.*]] = icmp ult i32 [[SUB]], [[A]]
827-
; CHECK-NEXT: ret i1 [[C]]
825+
; CHECK-NEXT: ret i1 true
828826
;
829827
entry:
830828
%a.sge = icmp sge i32 %a, 3

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

Lines changed: 173 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -425,3 +425,176 @@ define i1 @assume_4b(i64 %a, i64 %b) {
425425
%ret = icmp sle i64 %a, %b
426426
ret i1 %ret
427427
}
428+
429+
define i1 @sle_and_ne_imply_slt(i8 %a) {
430+
; CHECK-LABEL: @sle_and_ne_imply_slt(
431+
; CHECK-NEXT: [[SLE:%.*]] = icmp sle i8 [[A:%.*]], 0
432+
; CHECK-NEXT: br i1 [[SLE]], label [[LESS_OR_EQUAL:%.*]], label [[EXIT:%.*]]
433+
; CHECK: less_or_equal:
434+
; CHECK-NEXT: [[NE:%.*]] = icmp ne i8 [[A]], 0
435+
; CHECK-NEXT: br i1 [[NE]], label [[NOT_EQUAL:%.*]], label [[EXIT]]
436+
; CHECK: not_equal:
437+
; CHECK-NEXT: ret i1 true
438+
; CHECK: exit:
439+
; CHECK-NEXT: ret i1 false
440+
;
441+
%sle = icmp sle i8 %a, 0
442+
br i1 %sle, label %less_or_equal, label %exit
443+
444+
less_or_equal:
445+
%ne = icmp ne i8 %a, 0
446+
br i1 %ne, label %not_equal, label %exit
447+
448+
not_equal:
449+
%slt = icmp slt i8 %a, 0
450+
ret i1 %slt
451+
452+
exit:
453+
ret i1 0
454+
}
455+
456+
define i1 @sge_and_ne_imply_sgt(i8 %a) {
457+
; CHECK-LABEL: @sge_and_ne_imply_sgt(
458+
; CHECK-NEXT: [[SGE:%.*]] = icmp sge i8 [[A:%.*]], 0
459+
; CHECK-NEXT: br i1 [[SGE]], label [[GREATER_OR_EQUAL:%.*]], label [[EXIT:%.*]]
460+
; CHECK: greater_or_equal:
461+
; CHECK-NEXT: [[NE:%.*]] = icmp ne i8 [[A]], 0
462+
; CHECK-NEXT: br i1 [[NE]], label [[NOT_EQUAL:%.*]], label [[EXIT]]
463+
; CHECK: not_equal:
464+
; CHECK-NEXT: ret i1 true
465+
; CHECK: exit:
466+
; CHECK-NEXT: ret i1 false
467+
;
468+
%sge = icmp sge i8 %a, 0
469+
br i1 %sge, label %greater_or_equal, label %exit
470+
471+
greater_or_equal:
472+
%ne = icmp ne i8 %a, 0
473+
br i1 %ne, label %not_equal, label %exit
474+
475+
not_equal:
476+
%sgt = icmp sgt i8 %a, 0
477+
ret i1 %sgt
478+
479+
exit:
480+
ret i1 0
481+
}
482+
483+
define i1 @sge_and_ne_imply_sgt_opposite_successor(i8 %a) {
484+
; CHECK-LABEL: @sge_and_ne_imply_sgt_opposite_successor(
485+
; CHECK-NEXT: [[SLT:%.*]] = icmp slt i8 [[A:%.*]], 0
486+
; CHECK-NEXT: br i1 [[SLT]], label [[EXIT:%.*]], label [[GREATER_OR_EQUAL:%.*]]
487+
; CHECK: greater_or_equal:
488+
; CHECK-NEXT: [[EQ:%.*]] = icmp eq i8 [[A]], 0
489+
; CHECK-NEXT: br i1 [[EQ]], label [[EXIT]], label [[NOT_EQUAL:%.*]]
490+
; CHECK: not_equal:
491+
; CHECK-NEXT: ret i1 true
492+
; CHECK: exit:
493+
; CHECK-NEXT: ret i1 false
494+
;
495+
%slt = icmp slt i8 %a, 0
496+
br i1 %slt, label %exit, label %greater_or_equal
497+
498+
greater_or_equal:
499+
%eq = icmp eq i8 %a, 0
500+
br i1 %eq, label %exit, label %not_equal
501+
502+
not_equal:
503+
%sgt = icmp sgt i8 %a, 0
504+
ret i1 %sgt
505+
506+
exit:
507+
ret i1 0
508+
}
509+
510+
define i1 @sgt_implies_ugt_successful(i64 %a, i64 %b) {
511+
; CHECK-LABEL: @sgt_implies_ugt_successful(
512+
; CHECK-NEXT: [[B_SGE_0:%.*]] = icmp sge i64 [[B:%.*]], 0
513+
; CHECK-NEXT: call void @llvm.assume(i1 [[B_SGE_0]])
514+
; CHECK-NEXT: [[B_NE_0:%.*]] = icmp ne i64 [[B]], 0
515+
; CHECK-NEXT: call void @llvm.assume(i1 [[B_NE_0]])
516+
; CHECK-NEXT: [[A_SGT_B:%.*]] = icmp sgt i64 [[A:%.*]], [[B]]
517+
; CHECK-NEXT: call void @llvm.assume(i1 [[A_SGT_B]])
518+
; CHECK-NEXT: [[A_MINUS_ONE:%.*]] = add nsw i64 [[A]], -1
519+
; CHECK-NEXT: [[B_MINUS_ONE:%.*]] = add nsw i64 [[B]], -1
520+
; CHECK-NEXT: ret i1 true
521+
;
522+
%b_sge_0 = icmp sge i64 %b, 0
523+
call void @llvm.assume(i1 %b_sge_0)
524+
525+
%b_ne_0 = icmp ne i64 %b, 0
526+
call void @llvm.assume(i1 %b_ne_0)
527+
528+
%a_sgt_b = icmp sgt i64 %a, %b
529+
call void @llvm.assume(i1 %a_sgt_b)
530+
531+
%a_minus_one = add nsw i64 %a, -1
532+
%b_minus_one = add nsw i64 %b, -1
533+
%ugt = icmp ugt i64 %a_minus_one, %b_minus_one
534+
ret i1 %ugt
535+
}
536+
537+
define i1 @sgt_implies_ugt_unsuccessful1(i64 %a, i64 %b) {
538+
; CHECK-LABEL: @sgt_implies_ugt_unsuccessful1(
539+
; CHECK-NEXT: [[B_SGE_0:%.*]] = icmp sge i64 [[B:%.*]], 0
540+
; CHECK-NEXT: call void @llvm.assume(i1 [[B_SGE_0]])
541+
; CHECK-NEXT: [[A_SGT_B:%.*]] = icmp sgt i64 [[A:%.*]], [[B]]
542+
; CHECK-NEXT: call void @llvm.assume(i1 [[A_SGT_B]])
543+
; CHECK-NEXT: [[A_MINUS_ONE:%.*]] = add nsw i64 [[A]], -1
544+
; CHECK-NEXT: [[B_MINUS_ONE:%.*]] = add nsw i64 [[B]], -1
545+
; CHECK-NEXT: [[UGT:%.*]] = icmp ugt i64 [[A_MINUS_ONE]], [[B_MINUS_ONE]]
546+
; CHECK-NEXT: ret i1 [[UGT]]
547+
;
548+
%b_sge_0 = icmp sge i64 %b, 0
549+
call void @llvm.assume(i1 %b_sge_0)
550+
551+
%a_sgt_b = icmp sgt i64 %a, %b
552+
call void @llvm.assume(i1 %a_sgt_b)
553+
554+
%a_minus_one = add nsw i64 %a, -1
555+
%b_minus_one = add nsw i64 %b, -1
556+
%ugt = icmp ugt i64 %a_minus_one, %b_minus_one
557+
ret i1 %ugt
558+
}
559+
560+
define i1 @sgt_implies_ugt_unsuccessful2(i64 %a, i64 %b) {
561+
; CHECK-LABEL: @sgt_implies_ugt_unsuccessful2(
562+
; CHECK-NEXT: [[B_NE_0:%.*]] = icmp ne i64 [[B:%.*]], 0
563+
; CHECK-NEXT: call void @llvm.assume(i1 [[B_NE_0]])
564+
; CHECK-NEXT: [[A_SGT_B:%.*]] = icmp sgt i64 [[A:%.*]], [[B]]
565+
; CHECK-NEXT: call void @llvm.assume(i1 [[A_SGT_B]])
566+
; CHECK-NEXT: [[A_MINUS_ONE:%.*]] = add nsw i64 [[A]], -1
567+
; CHECK-NEXT: [[B_MINUS_ONE:%.*]] = add nsw i64 [[B]], -1
568+
; CHECK-NEXT: [[UGT:%.*]] = icmp ugt i64 [[A_MINUS_ONE]], [[B_MINUS_ONE]]
569+
; CHECK-NEXT: ret i1 [[UGT]]
570+
;
571+
%b_ne_0 = icmp ne i64 %b, 0
572+
call void @llvm.assume(i1 %b_ne_0)
573+
574+
%a_sgt_b = icmp sgt i64 %a, %b
575+
call void @llvm.assume(i1 %a_sgt_b)
576+
577+
%a_minus_one = add nsw i64 %a, -1
578+
%b_minus_one = add nsw i64 %b, -1
579+
%ugt = icmp ugt i64 %a_minus_one, %b_minus_one
580+
ret i1 %ugt
581+
}
582+
583+
define i1 @sgt_implies_ugt_unsuccessful3(i64 %a, i64 %b) {
584+
; CHECK-LABEL: @sgt_implies_ugt_unsuccessful3(
585+
; CHECK-NEXT: [[A_SGT_B:%.*]] = icmp sgt i64 [[A:%.*]], [[B:%.*]]
586+
; CHECK-NEXT: call void @llvm.assume(i1 [[A_SGT_B]])
587+
; CHECK-NEXT: [[A_MINUS_ONE:%.*]] = add nsw i64 [[A]], -1
588+
; CHECK-NEXT: [[B_MINUS_ONE:%.*]] = add nsw i64 [[B]], -1
589+
; CHECK-NEXT: [[UGT:%.*]] = icmp ugt i64 [[A_MINUS_ONE]], [[B_MINUS_ONE]]
590+
; CHECK-NEXT: ret i1 [[UGT]]
591+
;
592+
%a_sgt_b = icmp sgt i64 %a, %b
593+
call void @llvm.assume(i1 %a_sgt_b)
594+
595+
%a_minus_one = add nsw i64 %a, -1
596+
%b_minus_one = add nsw i64 %b, -1
597+
%ugt = icmp ugt i64 %a_minus_one, %b_minus_one
598+
ret i1 %ugt
599+
}
600+

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

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -267,8 +267,7 @@ define i1 @sub_nuw_i16_simp(i16 %a) {
267267
; CHECK-NEXT: [[C_1:%.*]] = icmp ugt i16 0, [[NEG2]]
268268
; CHECK-NEXT: br i1 [[C_1]], label [[EXIT_1:%.*]], label [[EXIT_2:%.*]]
269269
; CHECK: exit.1:
270-
; CHECK-NEXT: [[C_2:%.*]] = icmp ugt i16 [[A]], 0
271-
; CHECK-NEXT: ret i1 [[C_2]]
270+
; CHECK-NEXT: ret i1 true
272271
; CHECK: exit.2:
273272
; CHECK-NEXT: ret i1 true
274273
;
@@ -293,8 +292,7 @@ define i1 @sub_nuw_i64_simp(i64 %a) {
293292
; CHECK-NEXT: [[C_1:%.*]] = icmp ugt i64 0, [[NEG2]]
294293
; CHECK-NEXT: br i1 [[C_1]], label [[EXIT_1:%.*]], label [[EXIT_2:%.*]]
295294
; CHECK: exit.1:
296-
; CHECK-NEXT: [[C_2:%.*]] = icmp ugt i64 [[A]], 0
297-
; CHECK-NEXT: ret i1 [[C_2]]
295+
; CHECK-NEXT: ret i1 true
298296
; CHECK: exit.2:
299297
; CHECK-NEXT: ret i1 true
300298
;
@@ -319,8 +317,7 @@ define i1 @sub_nuw_neg_i16(i16 %a) {
319317
; CHECK-NEXT: [[C_1:%.*]] = icmp ugt i16 0, [[NEG2]]
320318
; CHECK-NEXT: br i1 [[C_1]], label [[EXIT_1:%.*]], label [[EXIT_2:%.*]]
321319
; CHECK: exit.1:
322-
; CHECK-NEXT: [[C_2:%.*]] = icmp ugt i16 [[A]], 0
323-
; CHECK-NEXT: ret i1 [[C_2]]
320+
; CHECK-NEXT: ret i1 true
324321
; CHECK: exit.2:
325322
; CHECK-NEXT: ret i1 true
326323
;

0 commit comments

Comments
 (0)