[Mlir-commits] [mlir] bad95b7 - [MLIR][Presburger] fourier-motzkin: check if all LCMs are 1 using a bool instead of by multiplying them

[Arjun P]

Author: Arjun P
Date: 2022-08-04T19:14:39+01:00
New Revision: bad95b72eed0d685874e19f4314f64fb081370af

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

LOG: [MLIR][Presburger] fourier-motzkin: check if all LCMs are 1 using a bool instead of by multiplying them

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

Added: 
    

Modified: 
    mlir/lib/Analysis/Presburger/IntegerRelation.cpp

Removed: 
    


################################################################################
diff  --git a/mlir/lib/Analysis/Presburger/IntegerRelation.cpp b/mlir/lib/Analysis/Presburger/IntegerRelation.cpp
index fb43d0cce86c8..cb1c13a69ab4f 100644
--- 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.