1 //===- ConstraintSytem.cpp - A system of linear constraints. ----*- C++ -*-===// 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 #include "llvm/Analysis/ConstraintSystem.h" 10 #include "llvm/ADT/SmallVector.h" 11 #include "llvm/Support/MathExtras.h" 12 #include "llvm/ADT/StringExtras.h" 13 #include "llvm/Support/Debug.h" 14 15 #include <string> 16 17 using namespace llvm; 18 19 #define DEBUG_TYPE "constraint-system" 20 21 bool ConstraintSystem::eliminateUsingFM() { 22 // Implementation of Fourier–Motzkin elimination, with some tricks from the 23 // paper Pugh, William. "The Omega test: a fast and practical integer 24 // programming algorithm for dependence 25 // analysis." 26 // Supercomputing'91: Proceedings of the 1991 ACM/ 27 // IEEE conference on Supercomputing. IEEE, 1991. 28 assert(!Constraints.empty() && 29 "should only be called for non-empty constraint systems"); 30 unsigned NumVariables = Constraints[0].size(); 31 32 uint32_t NewGCD = 1; 33 unsigned LastIdx = NumVariables - 1; 34 35 // First, either remove the variable in place if it is 0 or add the row to 36 // RemainingRows and remove it from the system. 37 SmallVector<SmallVector<int64_t, 8>, 4> RemainingRows; 38 for (unsigned R1 = 0; R1 < Constraints.size();) { 39 SmallVector<int64_t, 8> &Row1 = Constraints[R1]; 40 int64_t LowerLast = Row1[LastIdx]; 41 if (LowerLast == 0) { 42 Row1.pop_back(); 43 R1++; 44 } else { 45 std::swap(Constraints[R1], Constraints.back()); 46 RemainingRows.push_back(std::move(Constraints.back())); 47 Constraints.pop_back(); 48 } 49 } 50 51 // Process rows where the variable is != 0. 52 unsigned NumRemainingConstraints = RemainingRows.size(); 53 for (unsigned R1 = 0; R1 < NumRemainingConstraints; R1++) { 54 // FIXME do not use copy 55 for (unsigned R2 = R1 + 1; R2 < NumRemainingConstraints; R2++) { 56 if (R1 == R2) 57 continue; 58 59 int64_t UpperLast = RemainingRows[R2][LastIdx]; 60 int64_t LowerLast = RemainingRows[R1][LastIdx]; 61 assert( 62 UpperLast != 0 && LowerLast != 0 && 63 "RemainingRows should only contain rows where the variable is != 0"); 64 if ((LowerLast < 0 && UpperLast < 0) || (LowerLast > 0 && UpperLast > 0)) 65 continue; 66 67 unsigned LowerR = R1; 68 unsigned UpperR = R2; 69 if (UpperLast < 0) { 70 std::swap(LowerR, UpperR); 71 std::swap(LowerLast, UpperLast); 72 } 73 74 SmallVector<int64_t, 8> NR; 75 for (unsigned I = 0; I < LastIdx; I++) { 76 int64_t M1, M2, N; 77 int64_t UpperV = RemainingRows[UpperR][I]; 78 if (MulOverflow(UpperV, ((-1) * LowerLast / GCD), M1)) 79 return false; 80 int64_t LowerV = RemainingRows[LowerR][I]; 81 if (MulOverflow(LowerV, (UpperLast / GCD), M2)) 82 return false; 83 if (AddOverflow(M1, M2, N)) 84 return false; 85 NR.push_back(N); 86 87 NewGCD = 88 APIntOps::GreatestCommonDivisor({32, (uint32_t)N}, {32, NewGCD}) 89 .getZExtValue(); 90 } 91 Constraints.push_back(std::move(NR)); 92 // Give up if the new system gets too big. 93 if (Constraints.size() > 500) 94 return false; 95 } 96 } 97 GCD = NewGCD; 98 99 return true; 100 } 101 102 bool ConstraintSystem::mayHaveSolutionImpl() { 103 while (!Constraints.empty() && Constraints[0].size() > 1) { 104 if (!eliminateUsingFM()) 105 return true; 106 } 107 108 if (Constraints.empty() || Constraints[0].size() > 1) 109 return true; 110 111 return all_of(Constraints, [](auto &R) { return R[0] >= 0; }); 112 } 113 114 void ConstraintSystem::dump(ArrayRef<std::string> Names) const { 115 if (Constraints.empty()) 116 return; 117 118 for (const auto &Row : Constraints) { 119 SmallVector<std::string, 16> Parts; 120 for (unsigned I = 1, S = Row.size(); I < S; ++I) { 121 if (Row[I] == 0) 122 continue; 123 std::string Coefficient; 124 if (Row[I] != 1) 125 Coefficient = std::to_string(Row[I]) + " * "; 126 Parts.push_back(Coefficient + Names[I - 1]); 127 } 128 assert(!Parts.empty() && "need to have at least some parts"); 129 LLVM_DEBUG(dbgs() << join(Parts, std::string(" + ")) 130 << " <= " << std::to_string(Row[0]) << "\n"); 131 } 132 } 133 134 void ConstraintSystem::dump() const { 135 SmallVector<std::string, 16> Names; 136 for (unsigned i = 1; i < Constraints.back().size(); ++i) 137 Names.push_back("x" + std::to_string(i)); 138 LLVM_DEBUG(dbgs() << "---\n"); 139 dump(Names); 140 } 141 142 bool ConstraintSystem::mayHaveSolution() { 143 LLVM_DEBUG(dump()); 144 bool HasSolution = mayHaveSolutionImpl(); 145 LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n"); 146 return HasSolution; 147 } 148 149 bool ConstraintSystem::isConditionImplied(SmallVector<int64_t, 8> R) const { 150 // If all variable coefficients are 0, we have 'C >= 0'. If the constant is >= 151 // 0, R is always true, regardless of the system. 152 if (all_of(ArrayRef(R).drop_front(1), [](int64_t C) { return C == 0; })) 153 return R[0] >= 0; 154 155 // If there is no solution with the negation of R added to the system, the 156 // condition must hold based on the existing constraints. 157 R = ConstraintSystem::negate(R); 158 159 auto NewSystem = *this; 160 NewSystem.addVariableRow(R); 161 return !NewSystem.mayHaveSolution(); 162 } 163