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