-
Notifications
You must be signed in to change notification settings - Fork 10.8k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[ConstraintElimination] Extend unsigned-to-signed fact transfer #66173
[ConstraintElimination] Extend unsigned-to-signed fact transfer #66173
Conversation
@llvm/pr-subscribers-llvm-transforms ChangesMinor addition of transferring unsigned facts to signed comparisons. Proofs: https://alive2.llvm.org/ce/z/EWLPZA -- Full diff: https://github.com//pull/66173.diff3 Files Affected:
diff --git a/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp b/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp index 3c47d36cbc0a0bc..ac83e603daf0f01 100644 --- a/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp +++ b/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp @@ -25,6 +25,7 @@ #include "llvm/IR/Function.h" #include "llvm/IR/GetElementPtrTypeIterator.h" #include "llvm/IR/IRBuilder.h" +#include "llvm/IR/InstrTypes.h" #include "llvm/IR/Instructions.h" #include "llvm/IR/PatternMatch.h" #include "llvm/IR/Verifier.h" @@ -748,13 +749,23 @@ void ConstraintInfo::transferToOtherSystem( default: break; case CmpInst::ICMP_ULT: - // If B is a signed positive constant, A >=s 0 and A <s B. + case CmpInst::ICMP_ULE: + // If B is a signed positive constant, A >=s 0 and A <s (or <=s) B. if (doesHold(CmpInst::ICMP_SGE, B, ConstantInt::get(B->getType(), 0))) { addFact(CmpInst::ICMP_SGE, A, ConstantInt::get(B->getType(), 0), NumIn, NumOut, DFSInStack); - addFact(CmpInst::ICMP_SLT, A, B, NumIn, NumOut, DFSInStack); + addFact(CmpInst::getSignedPredicate(Pred), A, B, NumIn, NumOut, + DFSInStack); } break; + case CmpInst::ICMP_UGE: + case CmpInst::ICMP_UGT: + // If A and B are signed positive constants, A >s (or >=s) B. + if (doesHold(CmpInst::ICMP_SGE, B, ConstantInt::get(B->getType(), 0)) && + doesHold(CmpInst::ICMP_SGE, A, ConstantInt::get(B->getType(), 0))) + addFact(CmpInst::getSignedPredicate(Pred), A, B, NumIn, NumOut, + DFSInStack); + break; case CmpInst::ICMP_SLT: if (doesHold(CmpInst::ICMP_SGE, A, ConstantInt::get(B->getType(), 0))) addFact(CmpInst::ICMP_ULT, A, B, NumIn, NumOut, DFSInStack); diff --git a/llvm/test/Transforms/ConstraintElimination/signed-query-unsigned-system.ll b/llvm/test/Transforms/ConstraintElimination/signed-query-unsigned-system.ll index f5f7cc222f5a827..63d0c3ea3609c7e 100644 --- a/llvm/test/Transforms/ConstraintElimination/signed-query-unsigned-system.ll +++ b/llvm/test/Transforms/ConstraintElimination/signed-query-unsigned-system.ll @@ -109,8 +109,7 @@ define i1 @sge_no_const_unsigned_uge(i8 %a, i16 %b) { ; CHECK-NEXT: call void @llvm.assume(i1 [[A_UGE_B]]) ; CHECK-NEXT: [[B_POS:%.*]] = icmp sge i16 [[B]], 0 ; CHECK-NEXT: call void @llvm.assume(i1 [[B_POS]]) -; CHECK-NEXT: [[CMP:%.*]] = icmp sge i16 [[EXT]], [[B]] -; CHECK-NEXT: ret i1 [[CMP]] +; CHECK-NEXT: ret i1 true ; %ext = zext i8 %a to i16 %a.uge.b = icmp uge i16 %ext, %b diff --git a/llvm/test/Transforms/ConstraintElimination/transfer-unsigned-facts-to-signed.ll b/llvm/test/Transforms/ConstraintElimination/transfer-unsigned-facts-to-signed.ll index 34b27dd42e338aa..cff414db73a6c66 100644 --- a/llvm/test/Transforms/ConstraintElimination/transfer-unsigned-facts-to-signed.ll +++ b/llvm/test/Transforms/ConstraintElimination/transfer-unsigned-facts-to-signed.ll @@ -228,3 +228,86 @@ then: else: ret i1 0 } + +define i1 @ule_signed_pos_constant_1(i8 %a, i8 %b) { +; CHECK-LABEL: @ule_signed_pos_constant_1( +; CHECK-NEXT: [[B_NON_NEG:%.*]] = icmp sge i8 [[B:%.*]], 0 +; CHECK-NEXT: call void @llvm.assume(i1 [[B_NON_NEG]]) +; CHECK-NEXT: [[A_ULE_B:%.*]] = icmp ule i8 [[A:%.*]], [[B]] +; CHECK-NEXT: call void @llvm.assume(i1 [[A_ULE_B]]) +; CHECK-NEXT: [[RESULT_XOR:%.*]] = xor i1 true, true +; CHECK-NEXT: ret i1 [[RESULT_XOR]] +; + %b_non_neg = icmp sge i8 %b, 0 + call void @llvm.assume(i1 %b_non_neg) + %a_ule_b = icmp ule i8 %a, %b + call void @llvm.assume(i1 %a_ule_b) + + %sle_test = icmp sle i8 %a, %b + %result_xor = xor i1 %sle_test, 1 + + ret i1 %result_xor +} + +define i1 @ule_signed_pos_constant_2(i8 %a) { +; CHECK-LABEL: @ule_signed_pos_constant_2( +; CHECK-NEXT: [[A_ULT_4:%.*]] = icmp ule i8 [[A:%.*]], 4 +; CHECK-NEXT: br i1 [[A_ULT_4]], label [[THEN:%.*]], label [[ELSE:%.*]] +; CHECK: then: +; CHECK-NEXT: [[RES_1:%.*]] = xor i1 true, true +; CHECK-NEXT: [[RES_2:%.*]] = xor i1 [[RES_1]], true +; CHECK-NEXT: ret i1 [[RES_2]] +; CHECK: else: +; CHECK-NEXT: [[C_2:%.*]] = icmp sge i8 [[A]], 0 +; CHECK-NEXT: [[C_3:%.*]] = icmp sle i8 [[A]], 4 +; CHECK-NEXT: [[RES_3:%.*]] = xor i1 [[C_2]], [[C_3]] +; CHECK-NEXT: [[C_4:%.*]] = icmp sle i8 [[A]], 5 +; CHECK-NEXT: [[RES_4:%.*]] = xor i1 [[RES_3]], [[C_4]] +; CHECK-NEXT: ret i1 [[RES_4]] +; + %a.ult.4 = icmp ule i8 %a, 4 + br i1 %a.ult.4, label %then, label %else + +then: + %t.0 = icmp sge i8 %a, 0 + %t.1 = icmp sle i8 %a, 4 + %res.1 = xor i1 %t.0, %t.1 + + %c.0 = icmp sle i8 %a, 5 + %res.2 = xor i1 %res.1, %c.0 + ret i1 %res.2 + +else: + %c.2 = icmp sge i8 %a, 0 + %c.3 = icmp sle i8 %a, 4 + %res.3 = xor i1 %c.2, %c.3 + + %c.4 = icmp sle i8 %a, 5 + %res.4 = xor i1 %res.3, %c.4 + + ret i1 %res.4 +} + +define i1 @uge_assumed_positive_values(i8 %a, i8 %b) { +; CHECK-LABEL: @uge_assumed_positive_values( +; CHECK-NEXT: [[B_NON_NEG:%.*]] = icmp sge i8 [[B:%.*]], 0 +; CHECK-NEXT: call void @llvm.assume(i1 [[B_NON_NEG]]) +; CHECK-NEXT: [[A_NON_NEG:%.*]] = icmp sge i8 [[A:%.*]], 0 +; CHECK-NEXT: call void @llvm.assume(i1 [[A_NON_NEG]]) +; CHECK-NEXT: [[A_UGT_B:%.*]] = icmp uge i8 [[A]], [[B]] +; CHECK-NEXT: call void @llvm.assume(i1 [[A_UGT_B]]) +; CHECK-NEXT: ret i1 true +; + %b_non_neg = icmp sge i8 %b, 0 + call void @llvm.assume(i1 %b_non_neg) + %a_non_neg = icmp sge i8 %a, 0 + call void @llvm.assume(i1 %a_non_neg) + %a_ugt_b = icmp uge i8 %a, %b + call void @llvm.assume(i1 %a_ugt_b) + + %result = icmp sge i8 %a, %b + + ret i1 %result +} + +declare void @llvm.assume(i1) |
9cf513a
to
95367d6
Compare
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks reasonable to me. Can you please pre-commit tests (or split into separate commit) and update the alive2 link?
llvm/test/Transforms/ConstraintElimination/transfer-unsigned-facts-to-signed.ll
Outdated
Show resolved
Hide resolved
llvm/test/Transforms/ConstraintElimination/transfer-unsigned-facts-to-signed.ll
Show resolved
Hide resolved
95367d6
to
d5bf12f
Compare
Introduce test cases for extending unsigned-to-signed transfer logic.
Minor addition of transferring unsigned facts to signed comparisons. Proofs: https://alive2.llvm.org/ce/z/nqqzHb
d5bf12f
to
077c2a5
Compare
Addressed and updated proofs, thanks! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
LGTM, thanks!
Closing this as manually landed the commits. |
Minor addition of transferring unsigned facts to signed comparisons.
Proofs: https://alive2.llvm.org/ce/z/nqqzHb