[llvm] 7f3ff9d - [ConstraintElimination] Track if variables are positive in constraint.

Florian Hahn via llvm-commits llvm-commits at lists.llvm.org
Wed Sep 14 10:44:32 PDT 2022


Author: Florian Hahn
Date: 2022-09-14T18:43:54+01:00
New Revision: 7f3ff9d3c0ba6a1ac2beb80adfe6d76e10f29da7

URL: https://github.com/llvm/llvm-project/commit/7f3ff9d3c0ba6a1ac2beb80adfe6d76e10f29da7
DIFF: https://github.com/llvm/llvm-project/commit/7f3ff9d3c0ba6a1ac2beb80adfe6d76e10f29da7.diff

LOG: [ConstraintElimination] Track if variables are positive in constraint.

Keep track if variables are known positive during constraint
decomposition, aggregate the information when building the constraint
object and encode the extra information as constraints to be used during
reasoning.

Added: 
    

Modified: 
    llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
    llvm/test/Transforms/ConstraintElimination/zext-for-per-formula-reasoning.ll

Removed: 
    


################################################################################
diff  --git a/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp b/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
index 41d9dd995dcea..fea23796a8c66 100644
--- a/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
+++ b/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
@@ -78,6 +78,8 @@ struct ConstraintTy {
   SmallVector<int64_t, 8> Coefficients;
   SmallVector<PreconditionTy, 2> Preconditions;
 
+  SmallVector<SmallVector<int64_t, 8>> ExtraInfo;
+
   bool IsSigned = false;
   bool IsEq = false;
 
@@ -160,9 +162,13 @@ class ConstraintInfo {
 struct DecompEntry {
   int64_t Coefficient;
   Value *Variable;
+  /// True if the variable is known positive in the current constraint.
+  bool IsKnownPositive;
 
-  DecompEntry(int64_t Coefficient, Value *Variable)
-      : Coefficient(Coefficient), Variable(Variable) {}
+  DecompEntry(int64_t Coefficient, Value *Variable,
+              bool IsKnownPositive = false)
+      : Coefficient(Coefficient), Variable(Variable),
+        IsKnownPositive(IsKnownPositive) {}
 };
 
 } // namespace
@@ -212,7 +218,7 @@ decompose(Value *V, SmallVector<PreconditionTy, 4> &Preconditions,
         return {{CI->getSExtValue(), nullptr},
                 {1, GEP->getPointerOperand()},
                 {1, Op1}};
-      return {{0, nullptr}, {1, GEP->getPointerOperand()}, {1, Op0}};
+      return {{0, nullptr}, {1, GEP->getPointerOperand()}, {1, Op0, true}};
     }
 
     if (match(GEP->getOperand(GEP->getNumOperands() - 1), m_ConstantInt(CI)) &&
@@ -244,8 +250,11 @@ decompose(Value *V, SmallVector<PreconditionTy, 4> &Preconditions,
   }
 
   Value *Op0;
-  if (match(V, m_ZExt(m_Value(Op0))))
+  bool IsKnownPositive = false;
+  if (match(V, m_ZExt(m_Value(Op0)))) {
+    IsKnownPositive = true;
     V = Op0;
+  }
 
   Value *Op1;
   ConstantInt *CI;
@@ -277,7 +286,7 @@ decompose(Value *V, SmallVector<PreconditionTy, 4> &Preconditions,
   if (match(V, m_NUWSub(m_Value(Op0), m_Value(Op1))))
     return {{0, nullptr}, {1, Op0}, {-1, Op1}};
 
-  return {{0, nullptr}, {1, V}};
+  return {{0, nullptr}, {1, V, IsKnownPositive}};
 }
 
 ConstraintTy
@@ -356,13 +365,22 @@ ConstraintInfo::getConstraint(CmpInst::Predicate Pred, Value *Op0, Value *Op1,
   ConstraintTy Res(
       SmallVector<int64_t, 8>(Value2Index.size() + NewIndices.size() + 1, 0),
       IsSigned);
+  // Collect variables that are known to be positive in all uses in the
+  // constraint.
+  DenseMap<Value *, bool> KnownPositiveVariables;
   Res.IsEq = IsEq;
   auto &R = Res.Coefficients;
-  for (const auto &KV : VariablesA)
+  for (const auto &KV : VariablesA) {
     R[GetOrAddIndex(KV.Variable)] += KV.Coefficient;
+    auto I = KnownPositiveVariables.insert({KV.Variable, KV.IsKnownPositive});
+    I.first->second &= KV.IsKnownPositive;
+  }
 
-  for (const auto &KV : VariablesB)
+  for (const auto &KV : VariablesB) {
     R[GetOrAddIndex(KV.Variable)] -= KV.Coefficient;
+    auto I = KnownPositiveVariables.insert({KV.Variable, KV.IsKnownPositive});
+    I.first->second &= KV.IsKnownPositive;
+  }
 
   int64_t OffsetSum;
   if (AddOverflow(Offset1, Offset2, OffsetSum))
@@ -389,6 +407,14 @@ ConstraintInfo::getConstraint(CmpInst::Predicate Pred, Value *Op0, Value *Op1,
   if (!NewIndexNeeded)
     NewIndices.clear();
 
+  // Add extra constraints for variables that are known positive.
+  for (auto &KV : KnownPositiveVariables) {
+    if (!KV.second)
+      continue;
+    SmallVector<int64_t, 8> C(Value2Index.size() + NewIndices.size() + 1, 0);
+    C[GetOrAddIndex(KV.first)] = -1;
+    Res.ExtraInfo.push_back(C);
+  }
   return Res;
 }
 
@@ -772,6 +798,17 @@ static bool eliminateConstraints(Function &F, DominatorTree &DT) {
           continue;
 
         auto &CSToUse = Info.getCS(R.IsSigned);
+
+        // If there was extra information collected during decomposition, apply
+        // it now and remove it immediately once we are done with reasoning
+        // about the constraint.
+        for (auto &Row : R.ExtraInfo)
+          CSToUse.addVariableRow(Row);
+        auto InfoRestorer = make_scope_exit([&]() {
+          for (unsigned I = 0; I < R.ExtraInfo.size(); ++I)
+            CSToUse.popLastConstraint();
+        });
+
         if (CSToUse.isConditionImplied(R.Coefficients)) {
           if (!DebugCounter::shouldExecute(EliminatedCounter))
             continue;

diff  --git a/llvm/test/Transforms/ConstraintElimination/zext-for-per-formula-reasoning.ll b/llvm/test/Transforms/ConstraintElimination/zext-for-per-formula-reasoning.ll
index ea9e5079a12b6..54cb7127d0688 100644
--- a/llvm/test/Transforms/ConstraintElimination/zext-for-per-formula-reasoning.ll
+++ b/llvm/test/Transforms/ConstraintElimination/zext-for-per-formula-reasoning.ll
@@ -11,7 +11,7 @@ define i1 @test(i8 %x, i8 %y) {
 ; CHECK-NEXT:    [[EXT:%.*]] = zext i8 [[X]] to i16
 ; CHECK-NEXT:    [[T_1:%.*]] = icmp uge i16 [[EXT]], 0
 ; CHECK-NEXT:    [[C_1:%.*]] = icmp uge i16 [[EXT]], 1
-; CHECK-NEXT:    [[RES:%.*]] = xor i1 [[T_1]], [[C_1]]
+; CHECK-NEXT:    [[RES:%.*]] = xor i1 true, [[C_1]]
 ; CHECK-NEXT:    ret i1 [[RES]]
 ;
   %add = add nuw nsw i8 %x, %y
@@ -34,8 +34,8 @@ define i1 @test2(i8 %x, i8 %y) {
 ; CHECK-NEXT:    [[T_1:%.*]] = icmp uge i16 [[ADD_1]], 1
 ; CHECK-NEXT:    [[C_1:%.*]] = icmp uge i16 [[ADD_1]], 2
 ; CHECK-NEXT:    [[F_1:%.*]] = icmp ult i16 [[ADD_1]], 1
-; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 [[T_1]], [[C_1]]
-; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], [[F_1]]
+; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 true, [[C_1]]
+; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], false
 ; CHECK-NEXT:    [[C_2:%.*]] = icmp sge i16 [[ADD_1]], 1
 ; CHECK-NEXT:    [[RES_3:%.*]] = xor i1 [[RES_2]], [[C_2]]
 ; CHECK-NEXT:    ret i1 [[RES_3]]
@@ -67,7 +67,7 @@ define i1 @gep_zext_idx(ptr %p, i8 %cnt, i8 %off) {
 ; CHECK-NEXT:    [[F_1:%.*]] = icmp ult ptr [[ADD_PTR]], [[P]]
 ; CHECK-NEXT:    [[GEP_11:%.*]] = getelementptr inbounds i32, ptr [[P]], i16 11
 ; CHECK-NEXT:    [[C_1:%.*]] = icmp ugt ptr [[ADD_PTR]], [[GEP_11]]
-; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 [[T_1]], [[F_1]]
+; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 true, false
 ; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], [[C_1]]
 ; CHECK-NEXT:    ret i1 [[RES_2]]
 ;


        


More information about the llvm-commits mailing list