[ConstraintElimination] Extend unsigned-to-signed fact transfer

Minor addition of transferring unsigned facts to signed comparisons.

Proofs: https://alive2.llvm.org/ce/z/nqqzHb

Author: antoniofrighetto

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,11 +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, then 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 is a signed positive constant, then B >=s 0 and A >s (or >=s) B.
+    if (doesHold(CmpInst::ICMP_SGE, A, ConstantInt::get(B->getType(), 0))) {
+      addFact(CmpInst::ICMP_SGE, B, ConstantInt::get(B->getType(), 0), NumIn,
+              NumOut, DFSInStack);
+      addFact(CmpInst::getSignedPredicate(Pred), A, B, NumIn, NumOut,
+              DFSInStack);
     }
     break;
   case CmpInst::ICMP_SLT:

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

llvm/test/Transforms/ConstraintElimination/transfer-unsigned-facts-to-signed.ll

@@ -235,9 +235,8 @@ define i1 @ule_signed_pos_constant_1(i8 %a, i8 %b) {
 ; 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:    [[SLE_TEST:%.*]] = icmp sle i8 [[A]], [[B]]
 ; CHECK-NEXT:    [[SLT_TEST:%.*]] = icmp slt i8 [[A]], [[B]]
-; CHECK-NEXT:    [[RESULT_XOR:%.*]] = xor i1 [[SLE_TEST]], [[SLT_TEST]]
+; CHECK-NEXT:    [[RESULT_XOR:%.*]] = xor i1 true, [[SLT_TEST]]
 ; CHECK-NEXT:    ret i1 [[RESULT_XOR]]
 ;
   %b_non_neg = icmp sge i8 %b, 0
@@ -257,11 +256,8 @@ define i1 @ule_signed_pos_constant_2(i8 %a) {
 ; 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:    [[T_0:%.*]] = icmp sge i8 [[A]], 0
-; CHECK-NEXT:    [[T_1:%.*]] = icmp sle i8 [[A]], 4
-; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 [[T_0]], [[T_1]]
-; CHECK-NEXT:    [[C_0:%.*]] = icmp sle i8 [[A]], 5
-; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], [[C_0]]
+; 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
@@ -300,8 +296,7 @@ define i1 @uge_assumed_positive_values(i8 %a, i8 %b) {
 ; 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:    [[RESULT:%.*]] = icmp sge i8 [[A]], [[B]]
-; CHECK-NEXT:    ret i1 [[RESULT]]
+; CHECK-NEXT:    ret i1 true
 ;
   %a_non_neg = icmp sge i8 %a, 0
   call void @llvm.assume(i1 %a_non_neg)
@@ -319,8 +314,7 @@ define i1 @ugt_assumed_positive_values(i8 %a, i8 %b) {
 ; CHECK-NEXT:    call void @llvm.assume(i1 [[A_NON_NEG]])
 ; CHECK-NEXT:    [[A_UGT_B:%.*]] = icmp ugt i8 [[A]], [[B:%.*]]
 ; CHECK-NEXT:    call void @llvm.assume(i1 [[A_UGT_B]])
-; CHECK-NEXT:    [[RESULT:%.*]] = icmp sgt i8 [[A]], [[B]]
-; CHECK-NEXT:    ret i1 [[RESULT]]
+; CHECK-NEXT:    ret i1 true
 ;
   %a_non_neg = icmp sge i8 %a, 0
   call void @llvm.assume(i1 %a_non_neg)