[ConstraintElimination] Transfer info from ULT to signed system.

If A u< B holds, then A s>= 0 && A s< B holds if B s>= 0. https://alive2.llvm.org/ce/z/RrNxHh
llvm · Jun 23, 2022 · 316e106 · 316e106
1 parent 9ec7e4d
commit 316e106
Show file tree

Hide file tree

Showing 3 changed files with 13 additions and 5 deletions.
diff --git a/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp b/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
@@ -403,6 +403,14 @@ void ConstraintInfo::transferToOtherSystem(
   switch (Pred) {
   default:
     break;
+  case CmpInst::ICMP_ULT:
+    //  If B is a signed positive constant, A >=s 0 and A <s B.
+    if (doesHold(CmpInst::ICMP_SGE, B, ConstantInt::get(B->getType(), 0))) {
+      addFact(CmpInst::ICMP_SGE, A, ConstantInt::get(B->getType(), 0),
+              IsNegated, NumIn, NumOut, DFSInStack);
+      addFact(CmpInst::ICMP_SLT, A, B, IsNegated, 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, IsNegated, NumIn, NumOut, DFSInStack);

diff --git a/llvm/test/Transforms/ConstraintElimination/geps-unsigned-predicates.ll b/llvm/test/Transforms/ConstraintElimination/geps-unsigned-predicates.ll
@@ -531,7 +531,7 @@ define void @test.ult.gep.shl(i32* readonly %src, i32* readnone %max, i8 %idx) {
 ; CHECK-NEXT:    [[IDX_SHL_1:%.*]] = shl nuw i8 [[IDX]], 1
 ; CHECK-NEXT:    [[ADD_PTR_SHL_1:%.*]] = getelementptr inbounds i32, i32* [[SRC]], i8 [[IDX_SHL_1]]
 ; CHECK-NEXT:    [[C_MAX_0:%.*]] = icmp ult i32* [[ADD_PTR_SHL_1]], [[MAX]]
-; CHECK-NEXT:    call void @use(i1 [[C_MAX_0]])
+; CHECK-NEXT:    call void @use(i1 true)
 ; CHECK-NEXT:    [[IDX_SHL_2:%.*]] = shl nuw i8 [[IDX]], 2
 ; CHECK-NEXT:    [[ADD_PTR_SHL_2:%.*]] = getelementptr inbounds i32, i32* [[SRC]], i8 [[IDX_SHL_2]]
 ; CHECK-NEXT:    [[C_MAX_1:%.*]] = icmp ult i32* [[ADD_PTR_SHL_2]], [[MAX]]

diff --git a/llvm/test/Transforms/ConstraintElimination/transfer-unsigned-facts-to-signed.ll b/llvm/test/Transforms/ConstraintElimination/transfer-unsigned-facts-to-signed.ll
@@ -11,11 +11,11 @@ define i1 @idx_known_positive_via_len_1(i8 %len, i8 %idx) {
 ; CHECK:       then.1:
 ; CHECK-NEXT:    [[T_1:%.*]] = icmp ult i8 [[IDX]], [[LEN]]
 ; CHECK-NEXT:    [[T_2:%.*]] = icmp sge i8 [[IDX]], 0
-; CHECK-NEXT:    [[R_1:%.*]] = xor i1 true, [[T_2]]
+; CHECK-NEXT:    [[R_1:%.*]] = xor i1 true, true
 ; CHECK-NEXT:    [[C_1:%.*]] = icmp sge i8 [[IDX]], 1
 ; CHECK-NEXT:    [[R_2:%.*]] = xor i1 [[R_1]], [[C_1]]
 ; CHECK-NEXT:    [[C_2:%.*]] = icmp sge i8 [[LEN]], 1
-; CHECK-NEXT:    [[R_3:%.*]] = xor i1 [[R_2]], [[C_2]]
+; CHECK-NEXT:    [[R_3:%.*]] = xor i1 [[R_2]], true
 ; CHECK-NEXT:    ret i1 [[R_3]]
 ; CHECK:       else:
 ; CHECK-NEXT:    [[C_3:%.*]] = icmp sge i8 [[IDX]], 0
@@ -180,9 +180,9 @@ define i1 @ult_signed_pos_constant(i8 %a) {
 ; CHECK:       then:
 ; CHECK-NEXT:    [[T_0:%.*]] = icmp sge i8 [[A]], 0
 ; CHECK-NEXT:    [[T_1:%.*]] = icmp slt i8 [[A]], 4
-; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 [[T_0]], [[T_1]]
+; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 true, true
 ; CHECK-NEXT:    [[C_0:%.*]] = icmp slt i8 [[A]], 5
-; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], [[C_0]]
+; 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