[ConstraintElim] Infer linear constraints from udiv and urem (#180689)
urem x, n: result < n (remainder is always less than divisor) urem x, n: result <= x (remainder is at most the dividend) udiv x, n: result <= x (quotient is at most the dividend) https://alive2.llvm.org/ce/z/ezzsjQ
This commit is contained in:
Manasij Mukherjee
GitHub
parent
6c0ff8d12f
commit
0fdf9b9676
@ -1223,6 +1223,16 @@ void State::addInfoFor(BasicBlock &BB) {
|
||||
break;
|
||||
}
|
||||
|
||||
// Add facts from unsigned division and remainder.
|
||||
// urem x, n: result < n and result <= x
|
||||
// udiv x, n: result <= x
|
||||
if (auto *BO = dyn_cast<BinaryOperator>(&I)) {
|
||||
if ((BO->getOpcode() == Instruction::URem ||
|
||||
BO->getOpcode() == Instruction::UDiv) &&
|
||||
isGuaranteedNotToBePoison(BO))
|
||||
WorkList.push_back(FactOrCheck::getInstFact(DT.getNode(&BB), BO));
|
||||
}
|
||||
|
||||
GuaranteedToExecute &= isGuaranteedToTransferExecutionToSuccessor(&I);
|
||||
}
|
||||
|
||||
@ -2000,6 +2010,21 @@ static bool eliminateConstraints(Function &F, DominatorTree &DT, LoopInfo &LI,
|
||||
continue;
|
||||
}
|
||||
|
||||
if (auto *BO = dyn_cast<BinaryOperator>(CB.Inst)) {
|
||||
if (BO->getOpcode() == Instruction::URem) {
|
||||
// urem x, n: result < n (remainder is always less than divisor)
|
||||
AddFact(CmpInst::ICMP_ULT, BO, BO->getOperand(1));
|
||||
// urem x, n: result <= x (remainder is at most the dividend)
|
||||
AddFact(CmpInst::ICMP_ULE, BO, BO->getOperand(0));
|
||||
continue;
|
||||
}
|
||||
if (BO->getOpcode() == Instruction::UDiv) {
|
||||
// udiv x, n: result <= x (quotient is at most the dividend)
|
||||
AddFact(CmpInst::ICMP_ULE, BO, BO->getOperand(0));
|
||||
continue;
|
||||
}
|
||||
}
|
||||
|
||||
auto &DL = F.getDataLayout();
|
||||
auto AddFactsAboutIndices = [&](Value *Ptr, Type *AccessType) {
|
||||
CmpPredicate Pred;
|
||||
|
||||
361
llvm/test/Transforms/ConstraintElimination/urem-udiv.ll
Normal file
361
llvm/test/Transforms/ConstraintElimination/urem-udiv.ll
Normal file
@ -0,0 +1,361 @@
|
||||
; NOTE: Assertions have been autogenerated by utils/update_test_checks.py UTC_ARGS: --version 4
|
||||
; RUN: opt -passes=constraint-elimination -S %s | FileCheck %s
|
||||
|
||||
; n < m /\ r = urem x, n ==> r < n < m ==> r < m
|
||||
define i1 @urem_ult_divisor_bound(i32 noundef %x, i32 noundef %n, i32 noundef %m) {
|
||||
; CHECK-LABEL: define i1 @urem_ult_divisor_bound(
|
||||
; CHECK-SAME: i32 noundef [[X:%.*]], i32 noundef [[N:%.*]], i32 noundef [[M:%.*]]) {
|
||||
; CHECK-NEXT: entry:
|
||||
; CHECK-NEXT: [[CMP:%.*]] = icmp ult i32 [[N]], [[M]]
|
||||
; CHECK-NEXT: br i1 [[CMP]], label [[MID:%.*]], label [[ELSE:%.*]]
|
||||
; CHECK: mid:
|
||||
; CHECK-NEXT: [[R:%.*]] = urem i32 [[X]], [[N]]
|
||||
; CHECK-NEXT: br label [[CHECK:%.*]]
|
||||
; CHECK: check:
|
||||
; CHECK-NEXT: ret i1 true
|
||||
; CHECK: else:
|
||||
; CHECK-NEXT: ret i1 false
|
||||
;
|
||||
entry:
|
||||
%cmp = icmp ult i32 %n, %m
|
||||
br i1 %cmp, label %mid, label %else
|
||||
|
||||
mid:
|
||||
%r = urem i32 %x, %n
|
||||
br label %check
|
||||
|
||||
check:
|
||||
%v = icmp ult i32 %r, %m
|
||||
ret i1 %v
|
||||
|
||||
else:
|
||||
ret i1 false
|
||||
}
|
||||
|
||||
; n <= m /\ r = urem x, n ==> r < n <= m ==> r ule m
|
||||
define i1 @urem_ule_divisor_bound(i32 noundef %x, i32 noundef %n, i32 noundef %m) {
|
||||
; CHECK-LABEL: define i1 @urem_ule_divisor_bound(
|
||||
; CHECK-SAME: i32 noundef [[X:%.*]], i32 noundef [[N:%.*]], i32 noundef [[M:%.*]]) {
|
||||
; CHECK-NEXT: entry:
|
||||
; CHECK-NEXT: [[CMP:%.*]] = icmp ule i32 [[N]], [[M]]
|
||||
; CHECK-NEXT: br i1 [[CMP]], label [[MID:%.*]], label [[ELSE:%.*]]
|
||||
; CHECK: mid:
|
||||
; CHECK-NEXT: [[R:%.*]] = urem i32 [[X]], [[N]]
|
||||
; CHECK-NEXT: br label [[CHECK:%.*]]
|
||||
; CHECK: check:
|
||||
; CHECK-NEXT: ret i1 true
|
||||
; CHECK: else:
|
||||
; CHECK-NEXT: ret i1 false
|
||||
;
|
||||
entry:
|
||||
%cmp = icmp ule i32 %n, %m
|
||||
br i1 %cmp, label %mid, label %else
|
||||
|
||||
mid:
|
||||
%r = urem i32 %x, %n
|
||||
br label %check
|
||||
|
||||
check:
|
||||
%v = icmp ule i32 %r, %m
|
||||
ret i1 %v
|
||||
|
||||
else:
|
||||
ret i1 false
|
||||
}
|
||||
|
||||
; x <= limit /\ r = urem x, n ==> r <= x <= limit
|
||||
define i1 @urem_ule_dividend_bound(i32 noundef %x, i32 noundef %n, i32 noundef %limit) {
|
||||
; CHECK-LABEL: define i1 @urem_ule_dividend_bound(
|
||||
; CHECK-SAME: i32 noundef [[X:%.*]], i32 noundef [[N:%.*]], i32 noundef [[LIMIT:%.*]]) {
|
||||
; CHECK-NEXT: entry:
|
||||
; CHECK-NEXT: [[CMP:%.*]] = icmp ule i32 [[X]], [[LIMIT]]
|
||||
; CHECK-NEXT: br i1 [[CMP]], label [[MID:%.*]], label [[ELSE:%.*]]
|
||||
; CHECK: mid:
|
||||
; CHECK-NEXT: [[R:%.*]] = urem i32 [[X]], [[N]]
|
||||
; CHECK-NEXT: br label [[CHECK:%.*]]
|
||||
; CHECK: check:
|
||||
; CHECK-NEXT: ret i1 true
|
||||
; CHECK: else:
|
||||
; CHECK-NEXT: ret i1 false
|
||||
;
|
||||
entry:
|
||||
%cmp = icmp ule i32 %x, %limit
|
||||
br i1 %cmp, label %mid, label %else
|
||||
|
||||
mid:
|
||||
%r = urem i32 %x, %n
|
||||
br label %check
|
||||
|
||||
check:
|
||||
%v = icmp ule i32 %r, %limit
|
||||
ret i1 %v
|
||||
|
||||
else:
|
||||
ret i1 false
|
||||
}
|
||||
|
||||
; x <= limit /\ q = udiv x, n ==> q <= x <= limit
|
||||
define i1 @udiv_ule_dividend_bound(i32 noundef %x, i32 noundef %n, i32 noundef %limit) {
|
||||
; CHECK-LABEL: define i1 @udiv_ule_dividend_bound(
|
||||
; CHECK-SAME: i32 noundef [[X:%.*]], i32 noundef [[N:%.*]], i32 noundef [[LIMIT:%.*]]) {
|
||||
; CHECK-NEXT: entry:
|
||||
; CHECK-NEXT: [[CMP:%.*]] = icmp ule i32 [[X]], [[LIMIT]]
|
||||
; CHECK-NEXT: br i1 [[CMP]], label [[MID:%.*]], label [[ELSE:%.*]]
|
||||
; CHECK: mid:
|
||||
; CHECK-NEXT: [[Q:%.*]] = udiv i32 [[X]], [[N]]
|
||||
; CHECK-NEXT: br label [[CHECK:%.*]]
|
||||
; CHECK: check:
|
||||
; CHECK-NEXT: ret i1 true
|
||||
; CHECK: else:
|
||||
; CHECK-NEXT: ret i1 false
|
||||
;
|
||||
entry:
|
||||
%cmp = icmp ule i32 %x, %limit
|
||||
br i1 %cmp, label %mid, label %else
|
||||
|
||||
mid:
|
||||
%q = udiv i32 %x, %n
|
||||
br label %check
|
||||
|
||||
check:
|
||||
%v = icmp ule i32 %q, %limit
|
||||
ret i1 %v
|
||||
|
||||
else:
|
||||
ret i1 false
|
||||
}
|
||||
|
||||
; n < m /\ m < k /\ r = urem x, n ==> r < n < m < k ==> r < k
|
||||
define i1 @urem_chain_three_hops(i32 noundef %x, i32 noundef %n, i32 noundef %m, i32 noundef %k) {
|
||||
; CHECK-LABEL: define i1 @urem_chain_three_hops(
|
||||
; CHECK-SAME: i32 noundef [[X:%.*]], i32 noundef [[N:%.*]], i32 noundef [[M:%.*]], i32 noundef [[K:%.*]]) {
|
||||
; CHECK-NEXT: entry:
|
||||
; CHECK-NEXT: [[C1:%.*]] = icmp ult i32 [[N]], [[M]]
|
||||
; CHECK-NEXT: br i1 [[C1]], label [[BB1:%.*]], label [[OUT:%.*]]
|
||||
; CHECK: bb1:
|
||||
; CHECK-NEXT: [[R:%.*]] = urem i32 [[X]], [[N]]
|
||||
; CHECK-NEXT: [[C2:%.*]] = icmp ult i32 [[M]], [[K]]
|
||||
; CHECK-NEXT: br i1 [[C2]], label [[BB2:%.*]], label [[OUT]]
|
||||
; CHECK: bb2:
|
||||
; CHECK-NEXT: ret i1 true
|
||||
; CHECK: out:
|
||||
; CHECK-NEXT: ret i1 false
|
||||
;
|
||||
entry:
|
||||
%c1 = icmp ult i32 %n, %m
|
||||
br i1 %c1, label %bb1, label %out
|
||||
|
||||
bb1:
|
||||
%r = urem i32 %x, %n
|
||||
%c2 = icmp ult i32 %m, %k
|
||||
br i1 %c2, label %bb2, label %out
|
||||
|
||||
bb2:
|
||||
%v = icmp ult i32 %r, %k
|
||||
ret i1 %v
|
||||
|
||||
out:
|
||||
ret i1 false
|
||||
}
|
||||
|
||||
define i1 @udiv_urem_combined(i32 noundef %x, i32 noundef %n, i32 noundef %limit) {
|
||||
; CHECK-LABEL: define i1 @udiv_urem_combined(
|
||||
; CHECK-SAME: i32 noundef [[X:%.*]], i32 noundef [[N:%.*]], i32 noundef [[LIMIT:%.*]]) {
|
||||
; CHECK-NEXT: [[CMP1:%.*]] = icmp ult i32 [[N]], [[LIMIT]]
|
||||
; CHECK-NEXT: [[CMP2:%.*]] = icmp ule i32 [[X]], [[LIMIT]]
|
||||
; CHECK-NEXT: [[AND:%.*]] = and i1 [[CMP1]], [[CMP2]]
|
||||
; CHECK-NEXT: br i1 [[AND]], label [[THEN:%.*]], label [[ELSE:%.*]]
|
||||
; CHECK: then:
|
||||
; CHECK-NEXT: [[R:%.*]] = urem i32 [[X]], [[N]]
|
||||
; CHECK-NEXT: [[Q:%.*]] = udiv i32 [[X]], [[N]]
|
||||
; CHECK-NEXT: [[RES:%.*]] = and i1 true, true
|
||||
; CHECK-NEXT: ret i1 [[RES]]
|
||||
; CHECK: else:
|
||||
; CHECK-NEXT: ret i1 false
|
||||
;
|
||||
%cmp1 = icmp ult i32 %n, %limit
|
||||
%cmp2 = icmp ule i32 %x, %limit
|
||||
%and = and i1 %cmp1, %cmp2
|
||||
br i1 %and, label %then, label %else
|
||||
|
||||
then:
|
||||
%r = urem i32 %x, %n
|
||||
%q = udiv i32 %x, %n
|
||||
%cmp3 = icmp ule i32 %r, %limit
|
||||
%cmp4 = icmp ule i32 %q, %limit
|
||||
%res = and i1 %cmp3, %cmp4
|
||||
ret i1 %res
|
||||
|
||||
else:
|
||||
ret i1 false
|
||||
}
|
||||
|
||||
define i1 @urem_i64(i64 noundef %x, i64 noundef %n, i64 noundef %m) {
|
||||
; CHECK-LABEL: define i1 @urem_i64(
|
||||
; CHECK-SAME: i64 noundef [[X:%.*]], i64 noundef [[N:%.*]], i64 noundef [[M:%.*]]) {
|
||||
; CHECK-NEXT: entry:
|
||||
; CHECK-NEXT: [[CMP:%.*]] = icmp ult i64 [[N]], [[M]]
|
||||
; CHECK-NEXT: br i1 [[CMP]], label [[MID:%.*]], label [[ELSE:%.*]]
|
||||
; CHECK: mid:
|
||||
; CHECK-NEXT: [[R:%.*]] = urem i64 [[X]], [[N]]
|
||||
; CHECK-NEXT: br label [[CHECK:%.*]]
|
||||
; CHECK: check:
|
||||
; CHECK-NEXT: ret i1 true
|
||||
; CHECK: else:
|
||||
; CHECK-NEXT: ret i1 false
|
||||
;
|
||||
entry:
|
||||
%cmp = icmp ult i64 %n, %m
|
||||
br i1 %cmp, label %mid, label %else
|
||||
|
||||
mid:
|
||||
%r = urem i64 %x, %n
|
||||
br label %check
|
||||
|
||||
check:
|
||||
%v = icmp ult i64 %r, %m
|
||||
ret i1 %v
|
||||
|
||||
else:
|
||||
ret i1 false
|
||||
}
|
||||
|
||||
; Without noundef, isGuaranteedNotToBePoison may fail; don't add facts.
|
||||
define i1 @neg_urem_no_noundef(i32 %x, i32 %n, i32 %m) {
|
||||
; CHECK-LABEL: define i1 @neg_urem_no_noundef(
|
||||
; CHECK-SAME: i32 [[X:%.*]], i32 [[N:%.*]], i32 [[M:%.*]]) {
|
||||
; CHECK-NEXT: entry:
|
||||
; CHECK-NEXT: [[CMP:%.*]] = icmp ult i32 [[N]], [[M]]
|
||||
; CHECK-NEXT: br i1 [[CMP]], label [[MID:%.*]], label [[ELSE:%.*]]
|
||||
; CHECK: mid:
|
||||
; CHECK-NEXT: [[R:%.*]] = urem i32 [[X]], [[N]]
|
||||
; CHECK-NEXT: br label [[CHECK:%.*]]
|
||||
; CHECK: check:
|
||||
; CHECK-NEXT: [[V:%.*]] = icmp ult i32 [[R]], [[M]]
|
||||
; CHECK-NEXT: ret i1 [[V]]
|
||||
; CHECK: else:
|
||||
; CHECK-NEXT: ret i1 false
|
||||
;
|
||||
entry:
|
||||
%cmp = icmp ult i32 %n, %m
|
||||
br i1 %cmp, label %mid, label %else
|
||||
|
||||
mid:
|
||||
%r = urem i32 %x, %n
|
||||
br label %check
|
||||
|
||||
check:
|
||||
%v = icmp ult i32 %r, %m
|
||||
ret i1 %v
|
||||
|
||||
else:
|
||||
ret i1 false
|
||||
}
|
||||
|
||||
define i1 @neg_udiv_no_noundef(i32 %x, i32 %n, i32 %limit) {
|
||||
; CHECK-LABEL: define i1 @neg_udiv_no_noundef(
|
||||
; CHECK-SAME: i32 [[X:%.*]], i32 [[N:%.*]], i32 [[LIMIT:%.*]]) {
|
||||
; CHECK-NEXT: entry:
|
||||
; CHECK-NEXT: [[CMP:%.*]] = icmp ule i32 [[X]], [[LIMIT]]
|
||||
; CHECK-NEXT: br i1 [[CMP]], label [[MID:%.*]], label [[ELSE:%.*]]
|
||||
; CHECK: mid:
|
||||
; CHECK-NEXT: [[Q:%.*]] = udiv i32 [[X]], [[N]]
|
||||
; CHECK-NEXT: br label [[CHECK:%.*]]
|
||||
; CHECK: check:
|
||||
; CHECK-NEXT: [[V:%.*]] = icmp ule i32 [[Q]], [[LIMIT]]
|
||||
; CHECK-NEXT: ret i1 [[V]]
|
||||
; CHECK: else:
|
||||
; CHECK-NEXT: ret i1 false
|
||||
;
|
||||
entry:
|
||||
%cmp = icmp ule i32 %x, %limit
|
||||
br i1 %cmp, label %mid, label %else
|
||||
|
||||
mid:
|
||||
%q = udiv i32 %x, %n
|
||||
br label %check
|
||||
|
||||
check:
|
||||
%v = icmp ule i32 %q, %limit
|
||||
ret i1 %v
|
||||
|
||||
else:
|
||||
ret i1 false
|
||||
}
|
||||
|
||||
; srem/sdiv are NOT handled.
|
||||
define i1 @neg_srem_not_handled(i32 noundef %x, i32 noundef %n, i32 noundef %m) {
|
||||
; CHECK-LABEL: define i1 @neg_srem_not_handled(
|
||||
; CHECK-SAME: i32 noundef [[X:%.*]], i32 noundef [[N:%.*]], i32 noundef [[M:%.*]]) {
|
||||
; CHECK-NEXT: entry:
|
||||
; CHECK-NEXT: [[CMP:%.*]] = icmp ult i32 [[N]], [[M]]
|
||||
; CHECK-NEXT: br i1 [[CMP]], label [[MID:%.*]], label [[ELSE:%.*]]
|
||||
; CHECK: mid:
|
||||
; CHECK-NEXT: [[R:%.*]] = srem i32 [[X]], [[N]]
|
||||
; CHECK-NEXT: br label [[CHECK:%.*]]
|
||||
; CHECK: check:
|
||||
; CHECK-NEXT: [[V:%.*]] = icmp ult i32 [[R]], [[M]]
|
||||
; CHECK-NEXT: ret i1 [[V]]
|
||||
; CHECK: else:
|
||||
; CHECK-NEXT: ret i1 false
|
||||
;
|
||||
entry:
|
||||
%cmp = icmp ult i32 %n, %m
|
||||
br i1 %cmp, label %mid, label %else
|
||||
|
||||
mid:
|
||||
%r = srem i32 %x, %n
|
||||
br label %check
|
||||
|
||||
check:
|
||||
%v = icmp ult i32 %r, %m
|
||||
ret i1 %v
|
||||
|
||||
else:
|
||||
ret i1 false
|
||||
}
|
||||
|
||||
; No dominating constraint relating n to m; can't simplify.
|
||||
define i1 @neg_no_dominating_fact(i32 noundef %x, i32 noundef %n, i32 noundef %m) {
|
||||
; CHECK-LABEL: define i1 @neg_no_dominating_fact(
|
||||
; CHECK-SAME: i32 noundef [[X:%.*]], i32 noundef [[N:%.*]], i32 noundef [[M:%.*]]) {
|
||||
; CHECK-NEXT: [[R:%.*]] = urem i32 [[X]], [[N]]
|
||||
; CHECK-NEXT: [[V:%.*]] = icmp ult i32 [[R]], [[M]]
|
||||
; CHECK-NEXT: ret i1 [[V]]
|
||||
;
|
||||
%r = urem i32 %x, %n
|
||||
%v = icmp ult i32 %r, %m
|
||||
ret i1 %v
|
||||
}
|
||||
|
||||
; Wrong direction: m < n, r < n, but r < m is NOT implied.
|
||||
define i1 @neg_wrong_direction(i32 noundef %x, i32 noundef %n, i32 noundef %m) {
|
||||
; CHECK-LABEL: define i1 @neg_wrong_direction(
|
||||
; CHECK-SAME: i32 noundef [[X:%.*]], i32 noundef [[N:%.*]], i32 noundef [[M:%.*]]) {
|
||||
; CHECK-NEXT: entry:
|
||||
; CHECK-NEXT: [[CMP:%.*]] = icmp ult i32 [[M]], [[N]]
|
||||
; CHECK-NEXT: br i1 [[CMP]], label [[MID:%.*]], label [[ELSE:%.*]]
|
||||
; CHECK: mid:
|
||||
; CHECK-NEXT: [[R:%.*]] = urem i32 [[X]], [[N]]
|
||||
; CHECK-NEXT: br label [[CHECK:%.*]]
|
||||
; CHECK: check:
|
||||
; CHECK-NEXT: [[V:%.*]] = icmp ult i32 [[R]], [[M]]
|
||||
; CHECK-NEXT: ret i1 [[V]]
|
||||
; CHECK: else:
|
||||
; CHECK-NEXT: ret i1 false
|
||||
;
|
||||
entry:
|
||||
%cmp = icmp ult i32 %m, %n
|
||||
br i1 %cmp, label %mid, label %else
|
||||
|
||||
mid:
|
||||
%r = urem i32 %x, %n
|
||||
br label %check
|
||||
|
||||
check:
|
||||
%v = icmp ult i32 %r, %m
|
||||
ret i1 %v
|
||||
|
||||
else:
|
||||
ret i1 false
|
||||
}
|
||||
Loading…
x
Reference in New Issue
Block a user