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/IntegerPolyhedron.h" 15 #include "mlir/Support/LogicalResult.h" 16 #include "mlir/Support/MathExtras.h" 17 18 using namespace mlir; 19 using namespace presburger_utils; 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. 24 static void normalizeDivisionByGCD(SmallVectorImpl<int64_t> ÷nd, 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 floor(n / gcd); }); 49 divisor /= gcd; 50 } 51 52 /// Check if the pos^th identifier 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 `id` be the pos^th identifier, then `id` is equivalent to 57 /// `expr floordiv divisor` if there are constraints of the form: 58 /// 0 <= expr - divisor * id <= divisor - 1 59 /// Rearranging, we have: 60 /// divisor * id - expr + (divisor - 1) >= 0 <-- Lower bound for 'id' 61 /// -divisor * id + expr >= 0 <-- Upper bound for 'id' 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 * id <= divisor - 1, where 0 <= c <= divisor - 1 83 /// Rearranging, we have: 84 /// divisor * id - expr + (divisor - 1) >= 0 <-- Lower bound for 'id' 85 /// -divisor * id + expr - c >= 0 <-- Upper bound for 'id' 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. 90 static LogicalResult getDivRepr(const IntegerPolyhedron &cst, unsigned pos, 91 unsigned ubIneq, unsigned lbIneq, 92 SmallVector<int64_t, 8> &expr, 93 unsigned &divisor) { 94 95 assert(pos <= cst.getNumIds() && "Invalid identifier position"); 96 assert(ubIneq <= cst.getNumInequalities() && 97 "Invalid upper bound inequality position"); 98 assert(lbIneq <= cst.getNumInequalities() && 99 "Invalid upper bound inequality position"); 100 101 // Extract divisor from the lower bound. 102 divisor = cst.atIneq(lbIneq, pos); 103 104 // First, check if the constraints are opposite of each other except the 105 // constant term. 106 unsigned i = 0, e = 0; 107 for (i = 0, e = cst.getNumIds(); i < e; ++i) 108 if (cst.atIneq(ubIneq, i) != -cst.atIneq(lbIneq, i)) 109 break; 110 111 if (i < e) 112 return failure(); 113 114 // Then, check if the constant term is of the proper form. 115 // Due to the form of the upper/lower bound inequalities, the sum of their 116 // constants is `divisor - 1 - c`. From this, we can extract c: 117 int64_t constantSum = cst.atIneq(lbIneq, cst.getNumCols() - 1) + 118 cst.atIneq(ubIneq, cst.getNumCols() - 1); 119 int64_t c = divisor - 1 - constantSum; 120 121 // Check if `c` satisfies the condition `0 <= c <= divisor - 1`. This also 122 // implictly checks that `divisor` is positive. 123 if (!(c >= 0 && c <= divisor - 1)) 124 return failure(); 125 126 // The inequality pair can be used to extract the division. 127 // Set `expr` to the dividend of the division except the constant term, which 128 // is set below. 129 expr.resize(cst.getNumCols(), 0); 130 for (i = 0, e = cst.getNumIds(); 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 identifier can be expressed as a floordiv of an affine 144 /// function of other identifiers (where the divisor is a positive constant). 145 /// `foundRepr` contains a boolean for each identifier indicating if the 146 /// explicit representation for that identifier has already been computed. 147 /// Returns the upper and lower bound inequalities using which the floordiv can 148 /// be computed. If the representation could be computed, `dividend` and 149 /// `denominator` are set. If the representation could not be computed, 150 /// `llvm::None` is returned. 151 MaybeLocalRepr presburger_utils::computeSingleVarRepr( 152 const IntegerPolyhedron &cst, ArrayRef<bool> foundRepr, unsigned pos, 153 SmallVector<int64_t, 8> ÷nd, unsigned &divisor) { 154 assert(pos < cst.getNumIds() && "invalid position"); 155 assert(foundRepr.size() == cst.getNumIds() && 156 "Size of foundRepr does not match total number of variables"); 157 158 SmallVector<unsigned, 4> lbIndices, ubIndices; 159 cst.getLowerAndUpperBoundIndices(pos, &lbIndices, &ubIndices); 160 MaybeLocalRepr repr; 161 162 for (unsigned ubPos : ubIndices) { 163 for (unsigned lbPos : lbIndices) { 164 // Attempt to get divison representation from ubPos, lbPos. 165 if (failed(getDivRepr(cst, pos, ubPos, lbPos, dividend, divisor))) 166 continue; 167 168 // Check if the inequalities depend on a variable for which 169 // an explicit representation has not been found yet. 170 // Exit to avoid circular dependencies between divisions. 171 unsigned c, f; 172 for (c = 0, f = cst.getNumIds(); c < f; ++c) { 173 if (c == pos) 174 continue; 175 if (!foundRepr[c] && dividend[c] != 0) 176 break; 177 } 178 179 // Expression can't be constructed as it depends on a yet unknown 180 // identifier. 181 // TODO: Visit/compute the identifiers in an order so that this doesn't 182 // happen. More complex but much more efficient. 183 if (c < f) 184 continue; 185 186 repr.kind = ReprKind::Inequality; 187 repr.repr.inEqualityPair = {ubPos, lbPos}; 188 return repr; 189 } 190 } 191 return repr; 192 } 193 194 void presburger_utils::removeDuplicateDivs( 195 std::vector<SmallVector<int64_t, 8>> &divs, 196 SmallVectorImpl<unsigned> &denoms, unsigned localOffset, 197 llvm::function_ref<bool(unsigned i, unsigned j)> merge) { 198 199 // Find and merge duplicate divisions. 200 // TODO: Add division normalization to support divisions that differ by 201 // a constant. 202 // TODO: Add division ordering such that a division representation for local 203 // identifier at position `i` only depends on local identifiers at position < 204 // `i`. This would make sure that all divisions depending on other local 205 // variables that can be merged, are merged. 206 for (unsigned i = 0; i < divs.size(); ++i) { 207 // Check if a division representation exists for the `i^th` local id. 208 if (denoms[i] == 0) 209 continue; 210 // Check if a division exists which is a duplicate of the division at `i`. 211 for (unsigned j = i + 1; j < divs.size(); ++j) { 212 // Check if a division representation exists for the `j^th` local id. 213 if (denoms[j] == 0) 214 continue; 215 // Check if the denominators match. 216 if (denoms[i] != denoms[j]) 217 continue; 218 // Check if the representations are equal. 219 if (divs[i] != divs[j]) 220 continue; 221 222 // Merge divisions at position `j` into division at position `i`. If 223 // merge fails, do not merge these divs. 224 bool mergeResult = merge(i, j); 225 if (!mergeResult) 226 continue; 227 228 // Update division information to reflect merging. 229 for (unsigned k = 0, g = divs.size(); k < g; ++k) { 230 SmallVector<int64_t, 8> &div = divs[k]; 231 if (denoms[k] != 0) { 232 div[localOffset + i] += div[localOffset + j]; 233 div.erase(div.begin() + localOffset + j); 234 } 235 } 236 237 divs.erase(divs.begin() + j); 238 denoms.erase(denoms.begin() + j); 239 // Since `j` can never be zero, we do not need to worry about overflows. 240 --j; 241 } 242 } 243 } 244