[ConstraintSystem] Relax system if elimination not possible

When constructing a new constraint from a pair of lower/upper
constraints on the variable to eliminate, it simply ignores the new
constraint by not adding it if an overflow occurs when computing one
of its coefficients or if there are already too many constraints.

Previously, it simply stopped at this stage and considered the system
as having solution. Thus adding new constraints could turn a
unsatisfiable system into a possibly satisfiable one which is a little
bit strange.

Unsatisfiability of the new system still implies unsatisfiability of
the former one (the projected solution set of the original system is
included in the solution set of the new system).

Author: v01dxyz

llvm/include/llvm/Analysis/ConstraintSystem.h

@@ -43,6 +43,8 @@ class ConstraintSystem {
     return 0;
   }
 
+  // WARNING: it represents rather the maximum number of coefficients in the constraints
+  // which is actually the number of variables PLUS one (for the constant part).
   size_t NumVariables = 0;
 
   /// Current linear constraints in the system.
@@ -54,7 +56,13 @@ class ConstraintSystem {
   /// constraint system.
   DenseMap<Value *, unsigned> Value2Index;
 
-  // Eliminate constraints from the system using Fourier–Motzkin elimination.
+  // Eliminate the last variable from the system using Fourier–Motzkin
+  // elimination, while possibly relaxing it if it is beyond
+  // acceptable means (too many created constraints, overflow when
+  // computing the coefficients)
+  //
+  // return true if the updated system is equivalent, otherwise return
+  // false if it is relaxed.
   bool eliminateUsingFM();
 
   /// Returns true if there may be a solution for the constraints in the system.

llvm/lib/Analysis/ConstraintSystem.cpp

@@ -47,6 +47,9 @@ bool ConstraintSystem::eliminateUsingFM() {
     }
   }
 
+  // Track if an overflow occurred when computing coefficents
+  bool Overflow = false;
+
   // Process rows where the variable is != 0.
   unsigned NumRemainingConstraints = RemainingRows.size();
   for (unsigned R1 = 0; R1 < NumRemainingConstraints; R1++) {
@@ -95,14 +98,11 @@ bool ConstraintSystem::eliminateUsingFM() {
           IdxLower += 1;
         }
 
-        if (MulOverflow(UpperV, -1 * LowerLast, M1))
-          return false;
-
-        if (MulOverflow(LowerV, UpperLast, M2))
-          return false;
-
-        if (AddOverflow(M1, M2, N))
-          return false;
+        if (MulOverflow(UpperV, -1 * LowerLast, M1) ||
+            MulOverflow(LowerV, UpperLast, M2) || AddOverflow(M1, M2, N)) {
+          Overflow = true;
+          continue;
+        }
 
         // useless to add a 0 to a sparse vector
         if (N == 0)
@@ -120,13 +120,16 @@ bool ConstraintSystem::eliminateUsingFM() {
   }
   NumVariables -= 1;
 
-  return true;
+  return !Overflow;
 }
 
 bool ConstraintSystem::mayHaveSolutionImpl() {
-  while (!Constraints.empty() && NumVariables > 1) {
-    if (!eliminateUsingFM())
-      return true;
+  while (!Constraints.empty() && Constraints.size() <= 500 && NumVariables > 1) {
+    if(!eliminateUsingFM()) {
+      LLVM_DEBUG(
+          dbgs()
+          << "Some new constraints has been ignored during elimination.\n");
+    };
   }
 
   if (Constraints.empty() || NumVariables > 1)

llvm/test/Transforms/ConstraintElimination/constraint-overflow.ll

@@ -13,8 +13,7 @@ define i32 @f(i64 %a3, i64 %numElements) {
 ; CHECK-NEXT:    [[CMP:%.*]] = icmp ugt i64 [[A1]], [[A3]]
 ; CHECK-NEXT:    br i1 [[CMP]], label [[IF_END_I:%.*]], label [[ABORT:%.*]]
 ; CHECK:       if.end.i:
-; CHECK-NEXT:    [[CMP2_NOT_I:%.*]] = icmp ult i64 [[A1]], [[A3]]
-; CHECK-NEXT:    br i1 [[CMP2_NOT_I]], label [[ABORT]], label [[EXIT:%.*]]
+; CHECK-NEXT:    br i1 false, label [[ABORT]], label [[EXIT:%.*]]
 ; CHECK:       abort:
 ; CHECK-NEXT:    ret i32 -1
 ; CHECK:       exit: