[MLIR][Presburger] fourier-motzkin: check if all LCMs are 1 using a bool instead...

This can easily overflow and it is possible for these unsigned overflows to result in incorrect results.
For example, the two LCMs could be 641 and 6700417, which multiply to 2^32 + 1, which overflows to 1.
Unsigned overflows already occur in the existing tests.

Also, when switching to arbitrary-precision arithmetic, this results in a many
large integer multiplications resulting in a significant slowdown.

Reviewed By: Groverkss

Differential Revision: https://reviews.llvm.org/D131184

diff --git a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
index fb43d0c..cb1c13a 100644 (file)
--- a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
+++ b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
@@ -1802,7 +1802,7 @@ void IntegerRelation::fourierMotzkinEliminate(unsigned pos, bool darkShadow,
                          getNumEqualities(), getNumCols() - 1, newSpace);
 
   // This will be used to check if the elimination was integer exact.
-  unsigned lcmProducts = 1;
+  bool allLCMsAreOne = true;
 
   // Let x be the variable we are eliminating.
   // For each lower bound, lb <= c_l*x, and each upper bound c_u*x <= ub, (note
@@ -1831,7 +1831,9 @@ void IntegerRelation::fourierMotzkinEliminate(unsigned pos, bool darkShadow,
         int64_t lcm = mlir::lcm(lbCoeff, ubCoeff);
         ineq.push_back(atIneq(ubPos, l) * (lcm / ubCoeff) +
                        atIneq(lbPos, l) * (lcm / lbCoeff));
-        lcmProducts *= lcm;
+        assert(lcm > 0 && "lcm should be positive!");
+        if (lcm != 1)
+          allLCMsAreOne = false;
       }
       if (darkShadow) {
         // The dark shadow is a convex subset of the exact integer shadow. If
@@ -1844,9 +1846,9 @@ void IntegerRelation::fourierMotzkinEliminate(unsigned pos, bool darkShadow,
     }
   }
 
-  LLVM_DEBUG(llvm::dbgs() << "FM isResultIntegerExact: " << (lcmProducts == 1)
+  LLVM_DEBUG(llvm::dbgs() << "FM isResultIntegerExact: " << allLCMsAreOne
                           << "\n");
-  if (lcmProducts == 1 && isResultIntegerExact)
+  if (allLCMsAreOne && isResultIntegerExact)
     *isResultIntegerExact = true;
 
   // Copy over the constraints not involving this variable.