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