[ConstraintElimination] Transfer info from sgt %a, %b to ugt %a, %b if %b > 0

[fhahn]

Please add a proof using Alive2 (https://alive2.llvm.org/ce/) for the newly added reasoning to the patch description.

[zjaffal]

rebase on top of main

[zjaffal]

alive 2 proof
https://alive2.llvm.org/ce/z/cCGqEb

[fhahn]

In D148326#4268548, @zjaffal wrote:

alive 2 proof
https://alive2.llvm.org/ce/z/cCGqEb

Thanks! The above only proves it for a specific constant value of B (= 2). Better to have the proof use an arbitrary value of B: https://alive2.llvm.org/ce/z/uFN8xW

LGTM. Please make sure to include the link to the alive2 proof in the commit message.

llvm/lib/Transforms/Scalar/ConstraintElimination.cpp

if (doesHold(CmpInst::ICMP_SGE, B, ConstantInt::get(B->getType(), 0))) {
               NumOut, DFSInStack);
       addFact(CmpInst::ICMP_SLT, 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);
     break;
-  case CmpInst::ICMP_SGT:
+  case CmpInst::ICMP_SGT: {
     if (doesHold(CmpInst::ICMP_SGE, B, ConstantInt::get(B->getType(), -1)))
       addFact(CmpInst::ICMP_UGE, A, ConstantInt::get(B->getType(), 0), NumIn,
               NumOut, DFSInStack);
+    if (doesHold(CmpInst::ICMP_SGE, B, ConstantInt::get(B->getType(), 0)))
+      addFact(CmpInst::ICMP_UGT, A, B, NumIn, NumOut, DFSInStack);
+
     break;
+  }
   case CmpInst::ICMP_SGE:
     if (doesHold(CmpInst::ICMP_SGE, B, ConstantInt::get(B->getType(), 0))) {
       addFact(CmpInst::ICMP_UGE, A, B, NumIn, NumOut, DFSInStack);
     }
     break;
   }
 }
 

llvm/test/Transforms/ConstraintElimination/gep-sub.ll

 ; CHECK-NEXT:    [[IDX_EXT:%.*]] = zext i8 [[IDX]] to i16
 ; CHECK-NEXT:    [[DST_ADD_IDX:%.*]] = getelementptr inbounds i8, ptr [[DST:%.*]], i16 [[IDX_EXT]]
 ; CHECK-NEXT:    [[PRE:%.*]] = icmp ult ptr [[DST_ADD_IDX]], [[UPPER:%.*]]
 ; CHECK-NEXT:    call void @llvm.assume(i1 [[PRE]])
 ; CHECK-NEXT:    [[DST_SUB_1:%.*]] = getelementptr inbounds i8, ptr [[DST_ADD_IDX]], i64 -1
 ; CHECK-NEXT:    [[CMP_SUB_1:%.*]] = icmp ult ptr [[DST_SUB_1]], [[UPPER]]
 ; CHECK-NEXT:    [[DST_SUB_2:%.*]] = getelementptr inbounds i8, ptr [[DST_ADD_IDX]], i64 -2
 ; CHECK-NEXT:    [[CMP_SUB_2:%.*]] = icmp ult ptr [[DST_SUB_2]], [[UPPER]]
-; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 [[CMP_SUB_1]], [[CMP_SUB_2]]
+; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 true, true
 ; CHECK-NEXT:    [[DST_SUB_3:%.*]] = getelementptr inbounds i8, ptr [[DST_ADD_IDX]], i64 -3
 ; CHECK-NEXT:    [[CMP_SUB_3:%.*]] = icmp ult ptr [[DST_SUB_3]], [[UPPER]]
 ; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], [[CMP_SUB_3]]
 ; CHECK-NEXT:    ret i1 [[RES_2]]
 ;
   %sgt.1 = icmp sgt i8 %idx, 1
   call void @llvm.assume(i1 %sgt.1)
   %idx.ext = zext i8 %idx to i16

llvm/test/Transforms/ConstraintElimination/signed-query-unsigned-system.ll

 }
 
 define i1 @sgt_0_unsigned_a_sgt_0(i8 %a) {
 ; CHECK-LABEL: @sgt_0_unsigned_a_sgt_0(
 ; CHECK-NEXT:    [[A_SGT_0:%.*]] = icmp sgt i8 [[A:%.*]], 0
 ; CHECK-NEXT:    call void @llvm.assume(i1 [[A_SGT_0]])
 ; CHECK-NEXT:    [[EXT:%.*]] = zext i8 [[A]] to i16
 ; CHECK-NEXT:    [[T:%.*]] = icmp sgt i16 [[EXT]], 0
-; CHECK-NEXT:    ret i1 [[T]]
+; CHECK-NEXT:    ret i1 true
 ;
   %a.sgt.0 = icmp sgt i8 %a, 0
   call void @llvm.assume(i1 %a.sgt.0)
   %ext = zext i8 %a to i16
   %t = icmp sgt i16 %ext, 0
   ret i1 %t
 }
 

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

 
 define i1 @sgt_known_pos(i8 %idx) {
 ; CHECK-LABEL: @sgt_known_pos(
 ; CHECK-NEXT:  entry:
 ; CHECK-NEXT:    [[CMP:%.*]] = icmp sgt i8 [[IDX:%.*]], 2
 ; CHECK-NEXT:    call void @llvm.assume(i1 [[CMP]])
 ; CHECK-NEXT:    [[T_1:%.*]] = icmp ugt i8 [[IDX]], 2
 ; CHECK-NEXT:    [[T_2:%.*]] = icmp ugt i8 [[IDX]], 1
-; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 [[T_1]], [[T_2]]
+; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 true, true
 ; CHECK-NEXT:    [[C_1:%.*]] = icmp ugt i8 [[IDX]], 3
 ; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], [[C_1]]
 ; CHECK-NEXT:    ret i1 [[RES_2]]
 ;
 entry:
   %cmp = icmp sgt i8 %idx, 2
   call void @llvm.assume(i1 %cmp)
   %t.1 = icmp ugt i8 %idx, 2
   %t.2 = icmp ugt i8 %idx, 1
   %res.1 = xor i1 %t.1, %t.2
   %c.1 = icmp ugt i8 %idx, 3
   %res.2 = xor i1 %res.1, %c.1
   ret i1 %res.2
 }
 
 define i1 @sgt_to_ugt(i8 %a) {
 ; CHECK-LABEL: @sgt_to_ugt(
 ; CHECK-NEXT:  entry:
 ; CHECK-NEXT:    [[CMP:%.*]] = icmp sgt i8 [[A:%.*]], 2
 ; CHECK-NEXT:    call void @llvm.assume(i1 [[CMP]])
 ; CHECK-NEXT:    [[T_1:%.*]] = icmp ugt i8 [[A]], 2
-; CHECK-NEXT:    ret i1 [[T_1]]
+; CHECK-NEXT:    ret i1 true
 ;
 entry:
   %cmp = icmp sgt i8 %a, 2
   call void @llvm.assume(i1 %cmp)
   %t.1 = icmp ugt i8 %a, 2
   ret i1 %t.1
 }
 
 define i1 @sgt_to_ugt_less(i8 %a) {
 ; CHECK-LABEL: @sgt_to_ugt_less(
 ; CHECK-NEXT:  entry:
 ; CHECK-NEXT:    [[CMP:%.*]] = icmp sgt i8 [[A:%.*]], 2
 ; CHECK-NEXT:    call void @llvm.assume(i1 [[CMP]])
 ; CHECK-NEXT:    [[T_1:%.*]] = icmp ugt i8 [[A]], 1
-; CHECK-NEXT:    ret i1 [[T_1]]
+; CHECK-NEXT:    ret i1 true
 ;
 entry:
   %cmp = icmp sgt i8 %a, 2
   call void @llvm.assume(i1 %cmp)
   %t.1 = icmp ugt i8 %a, 1
   ret i1 %t.1
 }
 
 define i1 @sgt_to_ugt_var(i8 %a, i8 %b) {
 ; CHECK-LABEL: @sgt_to_ugt_var(
 ; CHECK-NEXT:  entry:
 ; CHECK-NEXT:    [[CMP:%.*]] = icmp sgt i8 [[A:%.*]], [[B:%.*]]
 ; CHECK-NEXT:    [[CMP_2:%.*]] = icmp sgt i8 [[B]], 0
 ; CHECK-NEXT:    call void @llvm.assume(i1 [[CMP]])
 ; CHECK-NEXT:    call void @llvm.assume(i1 [[CMP_2]])
 ; CHECK-NEXT:    [[T_1:%.*]] = icmp ugt i8 [[A]], [[B]]
-; CHECK-NEXT:    ret i1 [[T_1]]
+; CHECK-NEXT:    ret i1 true
 ;
 entry:
   %cmp = icmp sgt i8 %a, %b
   %cmp.2 = icmp sgt i8 %b, 0
   call void @llvm.assume(i1 %cmp)
   call void @llvm.assume(i1 %cmp.2)
   %t.1 = icmp ugt i8 %a, %b
   ret i1 %t.1