1 //===- Utils.cpp - General utilities for Presburger library ---------------===//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //
7 //===----------------------------------------------------------------------===//
8 //
9 // Utility functions required by the Presburger Library.
10 //
11 //===----------------------------------------------------------------------===//
12 
13 #include "mlir/Analysis/Presburger/Utils.h"
14 #include "mlir/Analysis/Presburger/IntegerRelation.h"
15 #include "mlir/Support/LogicalResult.h"
16 #include "mlir/Support/MathExtras.h"
17 
18 using namespace mlir;
19 using namespace presburger;
20 
21 /// Normalize a division's `dividend` and the `divisor` by their GCD. For
22 /// example: if the dividend and divisor are [2,0,4] and 4 respectively,
23 /// they get normalized to [1,0,2] and 2.
normalizeDivisionByGCD(MutableArrayRef<int64_t> dividend,unsigned & divisor)24 static void normalizeDivisionByGCD(MutableArrayRef<int64_t> dividend,
25                                    unsigned &divisor) {
26   if (divisor == 0 || dividend.empty())
27     return;
28   // We take the absolute value of dividend's coefficients to make sure that
29   // `gcd` is positive.
30   int64_t gcd =
31       llvm::greatestCommonDivisor(std::abs(dividend.front()), int64_t(divisor));
32 
33   // The reason for ignoring the constant term is as follows.
34   // For a division:
35   //      floor((a + m.f(x))/(m.d))
36   // It can be replaced by:
37   //      floor((floor(a/m) + f(x))/d)
38   // Since `{a/m}/d` in the dividend satisfies 0 <= {a/m}/d < 1/d, it will not
39   // influence the result of the floor division and thus, can be ignored.
40   for (size_t i = 1, m = dividend.size() - 1; i < m; i++) {
41     gcd = llvm::greatestCommonDivisor(std::abs(dividend[i]), gcd);
42     if (gcd == 1)
43       return;
44   }
45 
46   // Normalize the dividend and the denominator.
47   std::transform(dividend.begin(), dividend.end(), dividend.begin(),
48                  [gcd](int64_t &n) { return floorDiv(n, gcd); });
49   divisor /= gcd;
50 }
51 
52 /// Check if the pos^th variable can be represented as a division using upper
53 /// bound inequality at position `ubIneq` and lower bound inequality at position
54 /// `lbIneq`.
55 ///
56 /// Let `var` be the pos^th variable, then `var` is equivalent to
57 /// `expr floordiv divisor` if there are constraints of the form:
58 ///      0 <= expr - divisor * var <= divisor - 1
59 /// Rearranging, we have:
60 ///       divisor * var - expr + (divisor - 1) >= 0  <-- Lower bound for 'var'
61 ///      -divisor * var + expr                 >= 0  <-- Upper bound for 'var'
62 ///
63 /// For example:
64 ///     32*k >= 16*i + j - 31                 <-- Lower bound for 'k'
65 ///     32*k  <= 16*i + j                     <-- Upper bound for 'k'
66 ///     expr = 16*i + j, divisor = 32
67 ///     k = ( 16*i + j ) floordiv 32
68 ///
69 ///     4q >= i + j - 2                       <-- Lower bound for 'q'
70 ///     4q <= i + j + 1                       <-- Upper bound for 'q'
71 ///     expr = i + j + 1, divisor = 4
72 ///     q = (i + j + 1) floordiv 4
73 //
74 /// This function also supports detecting divisions from bounds that are
75 /// strictly tighter than the division bounds described above, since tighter
76 /// bounds imply the division bounds. For example:
77 ///     4q - i - j + 2 >= 0                       <-- Lower bound for 'q'
78 ///    -4q + i + j     >= 0                       <-- Tight upper bound for 'q'
79 ///
80 /// To extract floor divisions with tighter bounds, we assume that that the
81 /// constraints are of the form:
82 ///     c <= expr - divisior * var <= divisor - 1, where 0 <= c <= divisor - 1
83 /// Rearranging, we have:
84 ///     divisor * var - expr + (divisor - 1) >= 0  <-- Lower bound for 'var'
85 ///    -divisor * var + expr - c             >= 0  <-- Upper bound for 'var'
86 ///
87 /// If successful, `expr` is set to dividend of the division and `divisor` is
88 /// set to the denominator of the division. The final division expression is
89 /// normalized by GCD.
getDivRepr(const IntegerRelation & cst,unsigned pos,unsigned ubIneq,unsigned lbIneq,MutableArrayRef<int64_t> expr,unsigned & divisor)90 static LogicalResult getDivRepr(const IntegerRelation &cst, unsigned pos,
91                                 unsigned ubIneq, unsigned lbIneq,
92                                 MutableArrayRef<int64_t> expr,
93                                 unsigned &divisor) {
94 
95   assert(pos <= cst.getNumVars() && "Invalid variable position");
96   assert(ubIneq <= cst.getNumInequalities() &&
97          "Invalid upper bound inequality position");
98   assert(lbIneq <= cst.getNumInequalities() &&
99          "Invalid upper bound inequality position");
100   assert(expr.size() == cst.getNumCols() && "Invalid expression size");
101 
102   // Extract divisor from the lower bound.
103   divisor = cst.atIneq(lbIneq, pos);
104 
105   // First, check if the constraints are opposite of each other except the
106   // constant term.
107   unsigned i = 0, e = 0;
108   for (i = 0, e = cst.getNumVars(); i < e; ++i)
109     if (cst.atIneq(ubIneq, i) != -cst.atIneq(lbIneq, i))
110       break;
111 
112   if (i < e)
113     return failure();
114 
115   // Then, check if the constant term is of the proper form.
116   // Due to the form of the upper/lower bound inequalities, the sum of their
117   // constants is `divisor - 1 - c`. From this, we can extract c:
118   int64_t constantSum = cst.atIneq(lbIneq, cst.getNumCols() - 1) +
119                         cst.atIneq(ubIneq, cst.getNumCols() - 1);
120   int64_t c = divisor - 1 - constantSum;
121 
122   // Check if `c` satisfies the condition `0 <= c <= divisor - 1`. This also
123   // implictly checks that `divisor` is positive.
124   if (!(0 <= c && c <= divisor - 1)) // NOLINT
125     return failure();
126 
127   // The inequality pair can be used to extract the division.
128   // Set `expr` to the dividend of the division except the constant term, which
129   // is set below.
130   for (i = 0, e = cst.getNumVars(); i < e; ++i)
131     if (i != pos)
132       expr[i] = cst.atIneq(ubIneq, i);
133 
134   // From the upper bound inequality's form, its constant term is equal to the
135   // constant term of `expr`, minus `c`. From this,
136   // constant term of `expr` = constant term of upper bound + `c`.
137   expr.back() = cst.atIneq(ubIneq, cst.getNumCols() - 1) + c;
138   normalizeDivisionByGCD(expr, divisor);
139 
140   return success();
141 }
142 
143 /// Check if the pos^th variable can be represented as a division using
144 /// equality at position `eqInd`.
145 ///
146 /// For example:
147 ///     32*k == 16*i + j - 31                 <-- `eqInd` for 'k'
148 ///     expr = 16*i + j - 31, divisor = 32
149 ///     k = (16*i + j - 31) floordiv 32
150 ///
151 /// If successful, `expr` is set to dividend of the division and `divisor` is
152 /// set to the denominator of the division. The final division expression is
153 /// normalized by GCD.
getDivRepr(const IntegerRelation & cst,unsigned pos,unsigned eqInd,MutableArrayRef<int64_t> expr,unsigned & divisor)154 static LogicalResult getDivRepr(const IntegerRelation &cst, unsigned pos,
155                                 unsigned eqInd, MutableArrayRef<int64_t> expr,
156                                 unsigned &divisor) {
157 
158   assert(pos <= cst.getNumVars() && "Invalid variable position");
159   assert(eqInd <= cst.getNumEqualities() && "Invalid equality position");
160   assert(expr.size() == cst.getNumCols() && "Invalid expression size");
161 
162   // Extract divisor, the divisor can be negative and hence its sign information
163   // is stored in `signDiv` to reverse the sign of dividend's coefficients.
164   // Equality must involve the pos-th variable and hence `tempDiv` != 0.
165   int64_t tempDiv = cst.atEq(eqInd, pos);
166   if (tempDiv == 0)
167     return failure();
168   int64_t signDiv = tempDiv < 0 ? -1 : 1;
169 
170   // The divisor is always a positive integer.
171   divisor = tempDiv * signDiv;
172 
173   for (unsigned i = 0, e = cst.getNumVars(); i < e; ++i)
174     if (i != pos)
175       expr[i] = -signDiv * cst.atEq(eqInd, i);
176 
177   expr.back() = -signDiv * cst.atEq(eqInd, cst.getNumCols() - 1);
178   normalizeDivisionByGCD(expr, divisor);
179 
180   return success();
181 }
182 
183 // Returns `false` if the constraints depends on a variable for which an
184 // explicit representation has not been found yet, otherwise returns `true`.
checkExplicitRepresentation(const IntegerRelation & cst,ArrayRef<bool> foundRepr,ArrayRef<int64_t> dividend,unsigned pos)185 static bool checkExplicitRepresentation(const IntegerRelation &cst,
186                                         ArrayRef<bool> foundRepr,
187                                         ArrayRef<int64_t> dividend,
188                                         unsigned pos) {
189   // Exit to avoid circular dependencies between divisions.
190   for (unsigned c = 0, e = cst.getNumVars(); c < e; ++c) {
191     if (c == pos)
192       continue;
193 
194     if (!foundRepr[c] && dividend[c] != 0) {
195       // Expression can't be constructed as it depends on a yet unknown
196       // variable.
197       //
198       // TODO: Visit/compute the variables in an order so that this doesn't
199       // happen. More complex but much more efficient.
200       return false;
201     }
202   }
203 
204   return true;
205 }
206 
207 /// Check if the pos^th variable can be expressed as a floordiv of an affine
208 /// function of other variables (where the divisor is a positive constant).
209 /// `foundRepr` contains a boolean for each variable indicating if the
210 /// explicit representation for that variable has already been computed.
211 /// Returns the `MaybeLocalRepr` struct which contains the indices of the
212 /// constraints that can be expressed as a floordiv of an affine function. If
213 /// the representation could be computed, `dividend` and `denominator` are set.
214 /// If the representation could not be computed, the kind attribute in
215 /// `MaybeLocalRepr` is set to None.
computeSingleVarRepr(const IntegerRelation & cst,ArrayRef<bool> foundRepr,unsigned pos,MutableArrayRef<int64_t> dividend,unsigned & divisor)216 MaybeLocalRepr presburger::computeSingleVarRepr(
217     const IntegerRelation &cst, ArrayRef<bool> foundRepr, unsigned pos,
218     MutableArrayRef<int64_t> dividend, unsigned &divisor) {
219   assert(pos < cst.getNumVars() && "invalid position");
220   assert(foundRepr.size() == cst.getNumVars() &&
221          "Size of foundRepr does not match total number of variables");
222   assert(dividend.size() == cst.getNumCols() && "Invalid dividend size");
223 
224   SmallVector<unsigned, 4> lbIndices, ubIndices, eqIndices;
225   cst.getLowerAndUpperBoundIndices(pos, &lbIndices, &ubIndices, &eqIndices);
226   MaybeLocalRepr repr{};
227 
228   for (unsigned ubPos : ubIndices) {
229     for (unsigned lbPos : lbIndices) {
230       // Attempt to get divison representation from ubPos, lbPos.
231       if (failed(getDivRepr(cst, pos, ubPos, lbPos, dividend, divisor)))
232         continue;
233 
234       if (!checkExplicitRepresentation(cst, foundRepr, dividend, pos))
235         continue;
236 
237       repr.kind = ReprKind::Inequality;
238       repr.repr.inequalityPair = {ubPos, lbPos};
239       return repr;
240     }
241   }
242   for (unsigned eqPos : eqIndices) {
243     // Attempt to get divison representation from eqPos.
244     if (failed(getDivRepr(cst, pos, eqPos, dividend, divisor)))
245       continue;
246 
247     if (!checkExplicitRepresentation(cst, foundRepr, dividend, pos))
248       continue;
249 
250     repr.kind = ReprKind::Equality;
251     repr.repr.equalityIdx = eqPos;
252     return repr;
253   }
254   return repr;
255 }
256 
getSubrangeBitVector(unsigned len,unsigned setOffset,unsigned numSet)257 llvm::SmallBitVector presburger::getSubrangeBitVector(unsigned len,
258                                                       unsigned setOffset,
259                                                       unsigned numSet) {
260   llvm::SmallBitVector vec(len, false);
261   vec.set(setOffset, setOffset + numSet);
262   return vec;
263 }
264 
mergeLocalVars(IntegerRelation & relA,IntegerRelation & relB,llvm::function_ref<bool (unsigned i,unsigned j)> merge)265 void presburger::mergeLocalVars(
266     IntegerRelation &relA, IntegerRelation &relB,
267     llvm::function_ref<bool(unsigned i, unsigned j)> merge) {
268   assert(relA.getSpace().isCompatible(relB.getSpace()) &&
269          "Spaces should be compatible.");
270 
271   // Merge local vars of relA and relB without using division information,
272   // i.e. append local vars of `relB` to `relA` and insert local vars of `relA`
273   // to `relB` at start of its local vars.
274   unsigned initLocals = relA.getNumLocalVars();
275   relA.insertVar(VarKind::Local, relA.getNumLocalVars(),
276                  relB.getNumLocalVars());
277   relB.insertVar(VarKind::Local, 0, initLocals);
278 
279   // Get division representations from each rel.
280   DivisionRepr divsA = relA.getLocalReprs();
281   DivisionRepr divsB = relB.getLocalReprs();
282 
283   for (unsigned i = initLocals, e = divsB.getNumDivs(); i < e; ++i) {
284     divsA.setDividend(i, divsB.getDividend(i));
285     divsA.getDenom(i) = divsB.getDenom(i);
286   }
287 
288   // Remove duplicate divisions from divsA. The removing duplicate divisions
289   // call, calls `merge` to effectively merge divisions in relA and relB.
290   divsA.removeDuplicateDivs(merge);
291 }
292 
getDivUpperBound(ArrayRef<int64_t> dividend,int64_t divisor,unsigned localVarIdx)293 SmallVector<int64_t, 8> presburger::getDivUpperBound(ArrayRef<int64_t> dividend,
294                                                      int64_t divisor,
295                                                      unsigned localVarIdx) {
296   assert(dividend[localVarIdx] == 0 &&
297          "Local to be set to division must have zero coeff!");
298   SmallVector<int64_t, 8> ineq(dividend.begin(), dividend.end());
299   ineq[localVarIdx] = -divisor;
300   return ineq;
301 }
302 
getDivLowerBound(ArrayRef<int64_t> dividend,int64_t divisor,unsigned localVarIdx)303 SmallVector<int64_t, 8> presburger::getDivLowerBound(ArrayRef<int64_t> dividend,
304                                                      int64_t divisor,
305                                                      unsigned localVarIdx) {
306   assert(dividend[localVarIdx] == 0 &&
307          "Local to be set to division must have zero coeff!");
308   SmallVector<int64_t, 8> ineq(dividend.size());
309   std::transform(dividend.begin(), dividend.end(), ineq.begin(),
310                  std::negate<int64_t>());
311   ineq[localVarIdx] = divisor;
312   ineq.back() += divisor - 1;
313   return ineq;
314 }
315 
gcdRange(ArrayRef<int64_t> range)316 int64_t presburger::gcdRange(ArrayRef<int64_t> range) {
317   int64_t gcd = 0;
318   for (int64_t elem : range) {
319     gcd = llvm::GreatestCommonDivisor64(gcd, std::abs(elem));
320     if (gcd == 1)
321       return gcd;
322   }
323   return gcd;
324 }
325 
normalizeRange(MutableArrayRef<int64_t> range)326 int64_t presburger::normalizeRange(MutableArrayRef<int64_t> range) {
327   int64_t gcd = gcdRange(range);
328   if (gcd == 0 || gcd == 1)
329     return gcd;
330   for (int64_t &elem : range)
331     elem /= gcd;
332   return gcd;
333 }
334 
normalizeDiv(MutableArrayRef<int64_t> num,int64_t & denom)335 void presburger::normalizeDiv(MutableArrayRef<int64_t> num, int64_t &denom) {
336   assert(denom > 0 && "denom must be positive!");
337   int64_t gcd = llvm::greatestCommonDivisor(gcdRange(num), denom);
338   for (int64_t &coeff : num)
339     coeff /= gcd;
340   denom /= gcd;
341 }
342 
getNegatedCoeffs(ArrayRef<int64_t> coeffs)343 SmallVector<int64_t, 8> presburger::getNegatedCoeffs(ArrayRef<int64_t> coeffs) {
344   SmallVector<int64_t, 8> negatedCoeffs;
345   negatedCoeffs.reserve(coeffs.size());
346   for (int64_t coeff : coeffs)
347     negatedCoeffs.emplace_back(-coeff);
348   return negatedCoeffs;
349 }
350 
getComplementIneq(ArrayRef<int64_t> ineq)351 SmallVector<int64_t, 8> presburger::getComplementIneq(ArrayRef<int64_t> ineq) {
352   SmallVector<int64_t, 8> coeffs;
353   coeffs.reserve(ineq.size());
354   for (int64_t coeff : ineq)
355     coeffs.emplace_back(-coeff);
356   --coeffs.back();
357   return coeffs;
358 }
359 
removeDuplicateDivs(llvm::function_ref<bool (unsigned i,unsigned j)> merge)360 void DivisionRepr::removeDuplicateDivs(
361     llvm::function_ref<bool(unsigned i, unsigned j)> merge) {
362 
363   // Find and merge duplicate divisions.
364   // TODO: Add division normalization to support divisions that differ by
365   // a constant.
366   // TODO: Add division ordering such that a division representation for local
367   // variable at position `i` only depends on local variables at position <
368   // `i`. This would make sure that all divisions depending on other local
369   // variables that can be merged, are merged.
370   for (unsigned i = 0; i < getNumDivs(); ++i) {
371     // Check if a division representation exists for the `i^th` local var.
372     if (denoms[i] == 0)
373       continue;
374     // Check if a division exists which is a duplicate of the division at `i`.
375     for (unsigned j = i + 1; j < getNumDivs(); ++j) {
376       // Check if a division representation exists for the `j^th` local var.
377       if (denoms[j] == 0)
378         continue;
379       // Check if the denominators match.
380       if (denoms[i] != denoms[j])
381         continue;
382       // Check if the representations are equal.
383       if (dividends.getRow(i) != dividends.getRow(j))
384         continue;
385 
386       // Merge divisions at position `j` into division at position `i`. If
387       // merge fails, do not merge these divs.
388       bool mergeResult = merge(i, j);
389       if (!mergeResult)
390         continue;
391 
392       // Update division information to reflect merging.
393       unsigned divOffset = getDivOffset();
394       dividends.addToColumn(divOffset + j, divOffset + i, /*scale=*/1);
395       dividends.removeColumn(divOffset + j);
396       dividends.removeRow(j);
397       denoms.erase(denoms.begin() + j);
398 
399       // Since `j` can never be zero, we do not need to worry about overflows.
400       --j;
401     }
402   }
403 }
404 
print(raw_ostream & os) const405 void DivisionRepr::print(raw_ostream &os) const {
406   os << "Dividends:\n";
407   dividends.print(os);
408   os << "Denominators\n";
409   for (unsigned i = 0, e = denoms.size(); i < e; ++i)
410     os << denoms[i] << " ";
411   os << "\n";
412 }
413 
dump() const414 void DivisionRepr::dump() const { print(llvm::errs()); }
415 
getMPIntVec(ArrayRef<int64_t> range)416 SmallVector<MPInt, 8> presburger::getMPIntVec(ArrayRef<int64_t> range) {
417   SmallVector<MPInt, 8> result(range.size());
418   std::transform(range.begin(), range.end(), result.begin(), mpintFromInt64);
419   return result;
420 }
421 
getInt64Vec(ArrayRef<MPInt> range)422 SmallVector<int64_t, 8> presburger::getInt64Vec(ArrayRef<MPInt> range) {
423   SmallVector<int64_t, 8> result(range.size());
424   std::transform(range.begin(), range.end(), result.begin(), int64FromMPInt);
425   return result;
426 }
427