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/Analysis/Presburger/PresburgerSpace.h" 16 #include "llvm/ADT/STLFunctionalExtras.h" 17 #include "llvm/ADT/SmallBitVector.h" 18 #include "llvm/Support/LogicalResult.h" 19 #include "llvm/Support/raw_ostream.h" 20 #include <cassert> 21 #include <cstdint> 22 #include <numeric> 23 #include <optional> 24 25 using namespace mlir; 26 using namespace presburger; 27 using llvm::dynamicAPIntFromInt64; 28 29 /// Normalize a division's `dividend` and the `divisor` by their GCD. For 30 /// example: if the dividend and divisor are [2,0,4] and 4 respectively, 31 /// they get normalized to [1,0,2] and 2. The divisor must be non-negative; 32 /// it is allowed for the divisor to be zero, but nothing is done in this case. 33 static void normalizeDivisionByGCD(MutableArrayRef<DynamicAPInt> dividend, 34 DynamicAPInt &divisor) { 35 assert(divisor > 0 && "divisor must be non-negative!"); 36 if (dividend.empty()) 37 return; 38 // We take the absolute value of dividend's coefficients to make sure that 39 // `gcd` is positive. 40 DynamicAPInt gcd = llvm::gcd(abs(dividend.front()), divisor); 41 42 // The reason for ignoring the constant term is as follows. 43 // For a division: 44 // floor((a + m.f(x))/(m.d)) 45 // It can be replaced by: 46 // floor((floor(a/m) + f(x))/d) 47 // Since `{a/m}/d` in the dividend satisfies 0 <= {a/m}/d < 1/d, it will not 48 // influence the result of the floor division and thus, can be ignored. 49 for (size_t i = 1, m = dividend.size() - 1; i < m; i++) { 50 gcd = llvm::gcd(abs(dividend[i]), gcd); 51 if (gcd == 1) 52 return; 53 } 54 55 // Normalize the dividend and the denominator. 56 std::transform(dividend.begin(), dividend.end(), dividend.begin(), 57 [gcd](DynamicAPInt &n) { return floorDiv(n, gcd); }); 58 divisor /= gcd; 59 } 60 61 /// Check if the pos^th variable can be represented as a division using upper 62 /// bound inequality at position `ubIneq` and lower bound inequality at position 63 /// `lbIneq`. 64 /// 65 /// Let `var` be the pos^th variable, then `var` is equivalent to 66 /// `expr floordiv divisor` if there are constraints of the form: 67 /// 0 <= expr - divisor * var <= divisor - 1 68 /// Rearranging, we have: 69 /// divisor * var - expr + (divisor - 1) >= 0 <-- Lower bound for 'var' 70 /// -divisor * var + expr >= 0 <-- Upper bound for 'var' 71 /// 72 /// For example: 73 /// 32*k >= 16*i + j - 31 <-- Lower bound for 'k' 74 /// 32*k <= 16*i + j <-- Upper bound for 'k' 75 /// expr = 16*i + j, divisor = 32 76 /// k = ( 16*i + j ) floordiv 32 77 /// 78 /// 4q >= i + j - 2 <-- Lower bound for 'q' 79 /// 4q <= i + j + 1 <-- Upper bound for 'q' 80 /// expr = i + j + 1, divisor = 4 81 /// q = (i + j + 1) floordiv 4 82 // 83 /// This function also supports detecting divisions from bounds that are 84 /// strictly tighter than the division bounds described above, since tighter 85 /// bounds imply the division bounds. For example: 86 /// 4q - i - j + 2 >= 0 <-- Lower bound for 'q' 87 /// -4q + i + j >= 0 <-- Tight upper bound for 'q' 88 /// 89 /// To extract floor divisions with tighter bounds, we assume that the 90 /// constraints are of the form: 91 /// c <= expr - divisior * var <= divisor - 1, where 0 <= c <= divisor - 1 92 /// Rearranging, we have: 93 /// divisor * var - expr + (divisor - 1) >= 0 <-- Lower bound for 'var' 94 /// -divisor * var + expr - c >= 0 <-- Upper bound for 'var' 95 /// 96 /// If successful, `expr` is set to dividend of the division and `divisor` is 97 /// set to the denominator of the division, which will be positive. 98 /// The final division expression is normalized by GCD. 99 static LogicalResult getDivRepr(const IntegerRelation &cst, unsigned pos, 100 unsigned ubIneq, unsigned lbIneq, 101 MutableArrayRef<DynamicAPInt> expr, 102 DynamicAPInt &divisor) { 103 104 assert(pos <= cst.getNumVars() && "Invalid variable position"); 105 assert(ubIneq <= cst.getNumInequalities() && 106 "Invalid upper bound inequality position"); 107 assert(lbIneq <= cst.getNumInequalities() && 108 "Invalid upper bound inequality position"); 109 assert(expr.size() == cst.getNumCols() && "Invalid expression size"); 110 assert(cst.atIneq(lbIneq, pos) > 0 && "lbIneq is not a lower bound!"); 111 assert(cst.atIneq(ubIneq, pos) < 0 && "ubIneq is not an upper bound!"); 112 113 // Extract divisor from the lower bound. 114 divisor = cst.atIneq(lbIneq, pos); 115 116 // First, check if the constraints are opposite of each other except the 117 // constant term. 118 unsigned i = 0, e = 0; 119 for (i = 0, e = cst.getNumVars(); i < e; ++i) 120 if (cst.atIneq(ubIneq, i) != -cst.atIneq(lbIneq, i)) 121 break; 122 123 if (i < e) 124 return failure(); 125 126 // Then, check if the constant term is of the proper form. 127 // Due to the form of the upper/lower bound inequalities, the sum of their 128 // constants is `divisor - 1 - c`. From this, we can extract c: 129 DynamicAPInt constantSum = cst.atIneq(lbIneq, cst.getNumCols() - 1) + 130 cst.atIneq(ubIneq, cst.getNumCols() - 1); 131 DynamicAPInt c = divisor - 1 - constantSum; 132 133 // Check if `c` satisfies the condition `0 <= c <= divisor - 1`. 134 // This also implictly checks that `divisor` is positive. 135 if (!(0 <= c && c <= divisor - 1)) // NOLINT 136 return failure(); 137 138 // The inequality pair can be used to extract the division. 139 // Set `expr` to the dividend of the division except the constant term, which 140 // is set below. 141 for (i = 0, e = cst.getNumVars(); i < e; ++i) 142 if (i != pos) 143 expr[i] = cst.atIneq(ubIneq, i); 144 145 // From the upper bound inequality's form, its constant term is equal to the 146 // constant term of `expr`, minus `c`. From this, 147 // constant term of `expr` = constant term of upper bound + `c`. 148 expr.back() = cst.atIneq(ubIneq, cst.getNumCols() - 1) + c; 149 normalizeDivisionByGCD(expr, divisor); 150 151 return success(); 152 } 153 154 /// Check if the pos^th variable can be represented as a division using 155 /// equality at position `eqInd`. 156 /// 157 /// For example: 158 /// 32*k == 16*i + j - 31 <-- `eqInd` for 'k' 159 /// expr = 16*i + j - 31, divisor = 32 160 /// k = (16*i + j - 31) floordiv 32 161 /// 162 /// If successful, `expr` is set to dividend of the division and `divisor` is 163 /// set to the denominator of the division. The final division expression is 164 /// normalized by GCD. 165 static LogicalResult getDivRepr(const IntegerRelation &cst, unsigned pos, 166 unsigned eqInd, 167 MutableArrayRef<DynamicAPInt> expr, 168 DynamicAPInt &divisor) { 169 170 assert(pos <= cst.getNumVars() && "Invalid variable position"); 171 assert(eqInd <= cst.getNumEqualities() && "Invalid equality position"); 172 assert(expr.size() == cst.getNumCols() && "Invalid expression size"); 173 174 // Extract divisor, the divisor can be negative and hence its sign information 175 // is stored in `signDiv` to reverse the sign of dividend's coefficients. 176 // Equality must involve the pos-th variable and hence `tempDiv` != 0. 177 DynamicAPInt tempDiv = cst.atEq(eqInd, pos); 178 if (tempDiv == 0) 179 return failure(); 180 int signDiv = tempDiv < 0 ? -1 : 1; 181 182 // The divisor is always a positive integer. 183 divisor = tempDiv * signDiv; 184 185 for (unsigned i = 0, e = cst.getNumVars(); i < e; ++i) 186 if (i != pos) 187 expr[i] = -signDiv * cst.atEq(eqInd, i); 188 189 expr.back() = -signDiv * cst.atEq(eqInd, cst.getNumCols() - 1); 190 normalizeDivisionByGCD(expr, divisor); 191 192 return success(); 193 } 194 195 // Returns `false` if the constraints depends on a variable for which an 196 // explicit representation has not been found yet, otherwise returns `true`. 197 static bool checkExplicitRepresentation(const IntegerRelation &cst, 198 ArrayRef<bool> foundRepr, 199 ArrayRef<DynamicAPInt> dividend, 200 unsigned pos) { 201 // Exit to avoid circular dependencies between divisions. 202 for (unsigned c = 0, e = cst.getNumVars(); c < e; ++c) { 203 if (c == pos) 204 continue; 205 206 if (!foundRepr[c] && dividend[c] != 0) { 207 // Expression can't be constructed as it depends on a yet unknown 208 // variable. 209 // 210 // TODO: Visit/compute the variables in an order so that this doesn't 211 // happen. More complex but much more efficient. 212 return false; 213 } 214 } 215 216 return true; 217 } 218 219 /// Check if the pos^th variable can be expressed as a floordiv of an affine 220 /// function of other variables (where the divisor is a positive constant). 221 /// `foundRepr` contains a boolean for each variable indicating if the 222 /// explicit representation for that variable has already been computed. 223 /// Returns the `MaybeLocalRepr` struct which contains the indices of the 224 /// constraints that can be expressed as a floordiv of an affine function. If 225 /// the representation could be computed, `dividend` and `denominator` are set. 226 /// If the representation could not be computed, the kind attribute in 227 /// `MaybeLocalRepr` is set to None. 228 MaybeLocalRepr presburger::computeSingleVarRepr( 229 const IntegerRelation &cst, ArrayRef<bool> foundRepr, unsigned pos, 230 MutableArrayRef<DynamicAPInt> dividend, DynamicAPInt &divisor) { 231 assert(pos < cst.getNumVars() && "invalid position"); 232 assert(foundRepr.size() == cst.getNumVars() && 233 "Size of foundRepr does not match total number of variables"); 234 assert(dividend.size() == cst.getNumCols() && "Invalid dividend size"); 235 236 SmallVector<unsigned, 4> lbIndices, ubIndices, eqIndices; 237 cst.getLowerAndUpperBoundIndices(pos, &lbIndices, &ubIndices, &eqIndices); 238 MaybeLocalRepr repr{}; 239 240 for (unsigned ubPos : ubIndices) { 241 for (unsigned lbPos : lbIndices) { 242 // Attempt to get divison representation from ubPos, lbPos. 243 if (getDivRepr(cst, pos, ubPos, lbPos, dividend, divisor).failed()) 244 continue; 245 246 if (!checkExplicitRepresentation(cst, foundRepr, dividend, pos)) 247 continue; 248 249 repr.kind = ReprKind::Inequality; 250 repr.repr.inequalityPair = {ubPos, lbPos}; 251 return repr; 252 } 253 } 254 for (unsigned eqPos : eqIndices) { 255 // Attempt to get divison representation from eqPos. 256 if (getDivRepr(cst, pos, eqPos, dividend, divisor).failed()) 257 continue; 258 259 if (!checkExplicitRepresentation(cst, foundRepr, dividend, pos)) 260 continue; 261 262 repr.kind = ReprKind::Equality; 263 repr.repr.equalityIdx = eqPos; 264 return repr; 265 } 266 return repr; 267 } 268 269 MaybeLocalRepr presburger::computeSingleVarRepr( 270 const IntegerRelation &cst, ArrayRef<bool> foundRepr, unsigned pos, 271 SmallVector<int64_t, 8> ÷nd, unsigned &divisor) { 272 SmallVector<DynamicAPInt, 8> dividendDynamicAPInt(cst.getNumCols()); 273 DynamicAPInt divisorDynamicAPInt; 274 MaybeLocalRepr result = computeSingleVarRepr( 275 cst, foundRepr, pos, dividendDynamicAPInt, divisorDynamicAPInt); 276 dividend = getInt64Vec(dividendDynamicAPInt); 277 divisor = unsigned(int64_t(divisorDynamicAPInt)); 278 return result; 279 } 280 281 llvm::SmallBitVector presburger::getSubrangeBitVector(unsigned len, 282 unsigned setOffset, 283 unsigned numSet) { 284 llvm::SmallBitVector vec(len, false); 285 vec.set(setOffset, setOffset + numSet); 286 return vec; 287 } 288 289 void presburger::mergeLocalVars( 290 IntegerRelation &relA, IntegerRelation &relB, 291 llvm::function_ref<bool(unsigned i, unsigned j)> merge) { 292 assert(relA.getSpace().isCompatible(relB.getSpace()) && 293 "Spaces should be compatible."); 294 295 // Merge local vars of relA and relB without using division information, 296 // i.e. append local vars of `relB` to `relA` and insert local vars of `relA` 297 // to `relB` at start of its local vars. 298 unsigned initLocals = relA.getNumLocalVars(); 299 relA.insertVar(VarKind::Local, relA.getNumLocalVars(), 300 relB.getNumLocalVars()); 301 relB.insertVar(VarKind::Local, 0, initLocals); 302 303 // Get division representations from each rel. 304 DivisionRepr divsA = relA.getLocalReprs(); 305 DivisionRepr divsB = relB.getLocalReprs(); 306 307 for (unsigned i = initLocals, e = divsB.getNumDivs(); i < e; ++i) 308 divsA.setDiv(i, divsB.getDividend(i), divsB.getDenom(i)); 309 310 // Remove duplicate divisions from divsA. The removing duplicate divisions 311 // call, calls `merge` to effectively merge divisions in relA and relB. 312 divsA.removeDuplicateDivs(merge); 313 } 314 315 SmallVector<DynamicAPInt, 8> 316 presburger::getDivUpperBound(ArrayRef<DynamicAPInt> dividend, 317 const DynamicAPInt &divisor, 318 unsigned localVarIdx) { 319 assert(divisor > 0 && "divisor must be positive!"); 320 assert(dividend[localVarIdx] == 0 && 321 "Local to be set to division must have zero coeff!"); 322 SmallVector<DynamicAPInt, 8> ineq(dividend); 323 ineq[localVarIdx] = -divisor; 324 return ineq; 325 } 326 327 SmallVector<DynamicAPInt, 8> 328 presburger::getDivLowerBound(ArrayRef<DynamicAPInt> dividend, 329 const DynamicAPInt &divisor, 330 unsigned localVarIdx) { 331 assert(divisor > 0 && "divisor must be positive!"); 332 assert(dividend[localVarIdx] == 0 && 333 "Local to be set to division must have zero coeff!"); 334 SmallVector<DynamicAPInt, 8> ineq(dividend.size()); 335 std::transform(dividend.begin(), dividend.end(), ineq.begin(), 336 std::negate<DynamicAPInt>()); 337 ineq[localVarIdx] = divisor; 338 ineq.back() += divisor - 1; 339 return ineq; 340 } 341 342 DynamicAPInt presburger::gcdRange(ArrayRef<DynamicAPInt> range) { 343 DynamicAPInt gcd(0); 344 for (const DynamicAPInt &elem : range) { 345 gcd = llvm::gcd(gcd, abs(elem)); 346 if (gcd == 1) 347 return gcd; 348 } 349 return gcd; 350 } 351 352 DynamicAPInt presburger::normalizeRange(MutableArrayRef<DynamicAPInt> range) { 353 DynamicAPInt gcd = gcdRange(range); 354 if ((gcd == 0) || (gcd == 1)) 355 return gcd; 356 for (DynamicAPInt &elem : range) 357 elem /= gcd; 358 return gcd; 359 } 360 361 void presburger::normalizeDiv(MutableArrayRef<DynamicAPInt> num, 362 DynamicAPInt &denom) { 363 assert(denom > 0 && "denom must be positive!"); 364 DynamicAPInt gcd = llvm::gcd(gcdRange(num), denom); 365 if (gcd == 1) 366 return; 367 for (DynamicAPInt &coeff : num) 368 coeff /= gcd; 369 denom /= gcd; 370 } 371 372 SmallVector<DynamicAPInt, 8> 373 presburger::getNegatedCoeffs(ArrayRef<DynamicAPInt> coeffs) { 374 SmallVector<DynamicAPInt, 8> negatedCoeffs; 375 negatedCoeffs.reserve(coeffs.size()); 376 for (const DynamicAPInt &coeff : coeffs) 377 negatedCoeffs.emplace_back(-coeff); 378 return negatedCoeffs; 379 } 380 381 SmallVector<DynamicAPInt, 8> 382 presburger::getComplementIneq(ArrayRef<DynamicAPInt> ineq) { 383 SmallVector<DynamicAPInt, 8> coeffs; 384 coeffs.reserve(ineq.size()); 385 for (const DynamicAPInt &coeff : ineq) 386 coeffs.emplace_back(-coeff); 387 --coeffs.back(); 388 return coeffs; 389 } 390 391 SmallVector<std::optional<DynamicAPInt>, 4> 392 DivisionRepr::divValuesAt(ArrayRef<DynamicAPInt> point) const { 393 assert(point.size() == getNumNonDivs() && "Incorrect point size"); 394 395 SmallVector<std::optional<DynamicAPInt>, 4> divValues(getNumDivs(), 396 std::nullopt); 397 bool changed = true; 398 while (changed) { 399 changed = false; 400 for (unsigned i = 0, e = getNumDivs(); i < e; ++i) { 401 // If division value is found, continue; 402 if (divValues[i]) 403 continue; 404 405 ArrayRef<DynamicAPInt> dividend = getDividend(i); 406 DynamicAPInt divVal(0); 407 408 // Check if we have all the division values required for this division. 409 unsigned j, f; 410 for (j = 0, f = getNumDivs(); j < f; ++j) { 411 if (dividend[getDivOffset() + j] == 0) 412 continue; 413 // Division value required, but not found yet. 414 if (!divValues[j]) 415 break; 416 divVal += dividend[getDivOffset() + j] * *divValues[j]; 417 } 418 419 // We have some division values that are still not found, but are required 420 // to find the value of this division. 421 if (j < f) 422 continue; 423 424 // Fill remaining values. 425 divVal = std::inner_product(point.begin(), point.end(), dividend.begin(), 426 divVal); 427 // Add constant. 428 divVal += dividend.back(); 429 // Take floor division with denominator. 430 divVal = floorDiv(divVal, denoms[i]); 431 432 // Set div value and continue. 433 divValues[i] = divVal; 434 changed = true; 435 } 436 } 437 438 return divValues; 439 } 440 441 void DivisionRepr::removeDuplicateDivs( 442 llvm::function_ref<bool(unsigned i, unsigned j)> merge) { 443 444 // Find and merge duplicate divisions. 445 // TODO: Add division normalization to support divisions that differ by 446 // a constant. 447 // TODO: Add division ordering such that a division representation for local 448 // variable at position `i` only depends on local variables at position < 449 // `i`. This would make sure that all divisions depending on other local 450 // variables that can be merged, are merged. 451 normalizeDivs(); 452 for (unsigned i = 0; i < getNumDivs(); ++i) { 453 // Check if a division representation exists for the `i^th` local var. 454 if (denoms[i] == 0) 455 continue; 456 // Check if a division exists which is a duplicate of the division at `i`. 457 for (unsigned j = i + 1; j < getNumDivs(); ++j) { 458 // Check if a division representation exists for the `j^th` local var. 459 if (denoms[j] == 0) 460 continue; 461 // Check if the denominators match. 462 if (denoms[i] != denoms[j]) 463 continue; 464 // Check if the representations are equal. 465 if (dividends.getRow(i) != dividends.getRow(j)) 466 continue; 467 468 // Merge divisions at position `j` into division at position `i`. If 469 // merge fails, do not merge these divs. 470 bool mergeResult = merge(i, j); 471 if (!mergeResult) 472 continue; 473 474 // Update division information to reflect merging. 475 unsigned divOffset = getDivOffset(); 476 dividends.addToColumn(divOffset + j, divOffset + i, /*scale=*/1); 477 dividends.removeColumn(divOffset + j); 478 dividends.removeRow(j); 479 denoms.erase(denoms.begin() + j); 480 481 // Since `j` can never be zero, we do not need to worry about overflows. 482 --j; 483 } 484 } 485 } 486 487 void DivisionRepr::normalizeDivs() { 488 for (unsigned i = 0, e = getNumDivs(); i < e; ++i) { 489 if (getDenom(i) == 0 || getDividend(i).empty()) 490 continue; 491 normalizeDiv(getDividend(i), getDenom(i)); 492 } 493 } 494 495 void DivisionRepr::insertDiv(unsigned pos, ArrayRef<DynamicAPInt> dividend, 496 const DynamicAPInt &divisor) { 497 assert(pos <= getNumDivs() && "Invalid insertion position"); 498 assert(dividend.size() == getNumVars() + 1 && "Incorrect dividend size"); 499 500 dividends.appendExtraRow(dividend); 501 denoms.insert(denoms.begin() + pos, divisor); 502 dividends.insertColumn(getDivOffset() + pos); 503 } 504 505 void DivisionRepr::insertDiv(unsigned pos, unsigned num) { 506 assert(pos <= getNumDivs() && "Invalid insertion position"); 507 dividends.insertColumns(getDivOffset() + pos, num); 508 dividends.insertRows(pos, num); 509 denoms.insert(denoms.begin() + pos, num, DynamicAPInt(0)); 510 } 511 512 void DivisionRepr::print(raw_ostream &os) const { 513 os << "Dividends:\n"; 514 dividends.print(os); 515 os << "Denominators\n"; 516 for (const DynamicAPInt &denom : denoms) 517 os << denom << " "; 518 os << "\n"; 519 } 520 521 void DivisionRepr::dump() const { print(llvm::errs()); } 522 523 SmallVector<DynamicAPInt, 8> 524 presburger::getDynamicAPIntVec(ArrayRef<int64_t> range) { 525 SmallVector<DynamicAPInt, 8> result(range.size()); 526 std::transform(range.begin(), range.end(), result.begin(), 527 dynamicAPIntFromInt64); 528 return result; 529 } 530 531 SmallVector<int64_t, 8> presburger::getInt64Vec(ArrayRef<DynamicAPInt> range) { 532 SmallVector<int64_t, 8> result(range.size()); 533 std::transform(range.begin(), range.end(), result.begin(), 534 int64fromDynamicAPInt); 535 return result; 536 } 537 538 Fraction presburger::dotProduct(ArrayRef<Fraction> a, ArrayRef<Fraction> b) { 539 assert(a.size() == b.size() && 540 "dot product is only valid for vectors of equal sizes!"); 541 Fraction sum = 0; 542 for (unsigned i = 0, e = a.size(); i < e; i++) 543 sum += a[i] * b[i]; 544 return sum; 545 } 546 547 /// Find the product of two polynomials, each given by an array of 548 /// coefficients, by taking the convolution. 549 std::vector<Fraction> presburger::multiplyPolynomials(ArrayRef<Fraction> a, 550 ArrayRef<Fraction> b) { 551 // The length of the convolution is the sum of the lengths 552 // of the two sequences. We pad the shorter one with zeroes. 553 unsigned len = a.size() + b.size() - 1; 554 555 // We define accessors to avoid out-of-bounds errors. 556 auto getCoeff = [](ArrayRef<Fraction> arr, unsigned i) -> Fraction { 557 if (i < arr.size()) 558 return arr[i]; 559 return 0; 560 }; 561 562 std::vector<Fraction> convolution; 563 convolution.reserve(len); 564 for (unsigned k = 0; k < len; ++k) { 565 Fraction sum(0, 1); 566 for (unsigned l = 0; l <= k; ++l) 567 sum += getCoeff(a, l) * getCoeff(b, k - l); 568 convolution.emplace_back(sum); 569 } 570 return convolution; 571 } 572 573 bool presburger::isRangeZero(ArrayRef<Fraction> arr) { 574 return llvm::all_of(arr, [](const Fraction &f) { return f == 0; }); 575 } 576