1e8d8bef9SDimitry Andric //===- ConstraintSytem.cpp - A system of linear constraints. ----*- C++ -*-===// 2e8d8bef9SDimitry Andric // 3e8d8bef9SDimitry Andric // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions. 4e8d8bef9SDimitry Andric // See https://llvm.org/LICENSE.txt for license information. 5e8d8bef9SDimitry Andric // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception 6e8d8bef9SDimitry Andric // 7e8d8bef9SDimitry Andric //===----------------------------------------------------------------------===// 8e8d8bef9SDimitry Andric 9e8d8bef9SDimitry Andric #include "llvm/Analysis/ConstraintSystem.h" 10e8d8bef9SDimitry Andric #include "llvm/ADT/SmallVector.h" 11e8d8bef9SDimitry Andric #include "llvm/Support/MathExtras.h" 12e8d8bef9SDimitry Andric #include "llvm/ADT/StringExtras.h" 1306c3fb27SDimitry Andric #include "llvm/IR/Value.h" 14e8d8bef9SDimitry Andric #include "llvm/Support/Debug.h" 15e8d8bef9SDimitry Andric 16e8d8bef9SDimitry Andric #include <string> 17e8d8bef9SDimitry Andric 18e8d8bef9SDimitry Andric using namespace llvm; 19e8d8bef9SDimitry Andric 20e8d8bef9SDimitry Andric #define DEBUG_TYPE "constraint-system" 21e8d8bef9SDimitry Andric 22e8d8bef9SDimitry Andric bool ConstraintSystem::eliminateUsingFM() { 23e8d8bef9SDimitry Andric // Implementation of Fourier–Motzkin elimination, with some tricks from the 24e8d8bef9SDimitry Andric // paper Pugh, William. "The Omega test: a fast and practical integer 25e8d8bef9SDimitry Andric // programming algorithm for dependence 26e8d8bef9SDimitry Andric // analysis." 27e8d8bef9SDimitry Andric // Supercomputing'91: Proceedings of the 1991 ACM/ 28e8d8bef9SDimitry Andric // IEEE conference on Supercomputing. IEEE, 1991. 29e8d8bef9SDimitry Andric assert(!Constraints.empty() && 30e8d8bef9SDimitry Andric "should only be called for non-empty constraint systems"); 31e8d8bef9SDimitry Andric 3206c3fb27SDimitry Andric unsigned LastIdx = NumVariables - 1; 3306c3fb27SDimitry Andric 3406c3fb27SDimitry Andric // First, either remove the variable in place if it is 0 or add the row to 3506c3fb27SDimitry Andric // RemainingRows and remove it from the system. 3606c3fb27SDimitry Andric SmallVector<SmallVector<Entry, 8>, 4> RemainingRows; 3706c3fb27SDimitry Andric for (unsigned R1 = 0; R1 < Constraints.size();) { 3806c3fb27SDimitry Andric SmallVector<Entry, 8> &Row1 = Constraints[R1]; 3906c3fb27SDimitry Andric if (getLastCoefficient(Row1, LastIdx) == 0) { 4006c3fb27SDimitry Andric if (Row1.size() > 0 && Row1.back().Id == LastIdx) 4106c3fb27SDimitry Andric Row1.pop_back(); 4206c3fb27SDimitry Andric R1++; 4306c3fb27SDimitry Andric } else { 4406c3fb27SDimitry Andric std::swap(Constraints[R1], Constraints.back()); 4506c3fb27SDimitry Andric RemainingRows.push_back(std::move(Constraints.back())); 4606c3fb27SDimitry Andric Constraints.pop_back(); 47e8d8bef9SDimitry Andric } 48e8d8bef9SDimitry Andric } 49e8d8bef9SDimitry Andric 5006c3fb27SDimitry Andric // Process rows where the variable is != 0. 5106c3fb27SDimitry Andric unsigned NumRemainingConstraints = RemainingRows.size(); 5206c3fb27SDimitry Andric for (unsigned R1 = 0; R1 < NumRemainingConstraints; R1++) { 53e8d8bef9SDimitry Andric // FIXME do not use copy 5406c3fb27SDimitry Andric for (unsigned R2 = R1 + 1; R2 < NumRemainingConstraints; R2++) { 55e8d8bef9SDimitry Andric if (R1 == R2) 56e8d8bef9SDimitry Andric continue; 57e8d8bef9SDimitry Andric 5806c3fb27SDimitry Andric int64_t UpperLast = getLastCoefficient(RemainingRows[R2], LastIdx); 5906c3fb27SDimitry Andric int64_t LowerLast = getLastCoefficient(RemainingRows[R1], LastIdx); 6006c3fb27SDimitry Andric assert( 6106c3fb27SDimitry Andric UpperLast != 0 && LowerLast != 0 && 6206c3fb27SDimitry Andric "RemainingRows should only contain rows where the variable is != 0"); 63e8d8bef9SDimitry Andric 6406c3fb27SDimitry Andric if ((LowerLast < 0 && UpperLast < 0) || (LowerLast > 0 && UpperLast > 0)) 65e8d8bef9SDimitry Andric continue; 66e8d8bef9SDimitry Andric 67e8d8bef9SDimitry Andric unsigned LowerR = R1; 68e8d8bef9SDimitry Andric unsigned UpperR = R2; 6906c3fb27SDimitry Andric if (UpperLast < 0) { 70e8d8bef9SDimitry Andric std::swap(LowerR, UpperR); 7106c3fb27SDimitry Andric std::swap(LowerLast, UpperLast); 7206c3fb27SDimitry Andric } 73e8d8bef9SDimitry Andric 7406c3fb27SDimitry Andric SmallVector<Entry, 8> NR; 7506c3fb27SDimitry Andric unsigned IdxUpper = 0; 7606c3fb27SDimitry Andric unsigned IdxLower = 0; 7706c3fb27SDimitry Andric auto &LowerRow = RemainingRows[LowerR]; 7806c3fb27SDimitry Andric auto &UpperRow = RemainingRows[UpperR]; 7906c3fb27SDimitry Andric while (true) { 8006c3fb27SDimitry Andric if (IdxUpper >= UpperRow.size() || IdxLower >= LowerRow.size()) 8106c3fb27SDimitry Andric break; 82e8d8bef9SDimitry Andric int64_t M1, M2, N; 8306c3fb27SDimitry Andric int64_t UpperV = 0; 8406c3fb27SDimitry Andric int64_t LowerV = 0; 8506c3fb27SDimitry Andric uint16_t CurrentId = std::numeric_limits<uint16_t>::max(); 8606c3fb27SDimitry Andric if (IdxUpper < UpperRow.size()) { 8706c3fb27SDimitry Andric CurrentId = std::min(UpperRow[IdxUpper].Id, CurrentId); 8806c3fb27SDimitry Andric } 8906c3fb27SDimitry Andric if (IdxLower < LowerRow.size()) { 9006c3fb27SDimitry Andric CurrentId = std::min(LowerRow[IdxLower].Id, CurrentId); 9106c3fb27SDimitry Andric } 9206c3fb27SDimitry Andric 9306c3fb27SDimitry Andric if (IdxUpper < UpperRow.size() && UpperRow[IdxUpper].Id == CurrentId) { 9406c3fb27SDimitry Andric UpperV = UpperRow[IdxUpper].Coefficient; 9506c3fb27SDimitry Andric IdxUpper++; 9606c3fb27SDimitry Andric } 9706c3fb27SDimitry Andric 981db9f3b2SDimitry Andric if (MulOverflow(UpperV, -1 * LowerLast, M1)) 99e8d8bef9SDimitry Andric return false; 10006c3fb27SDimitry Andric if (IdxLower < LowerRow.size() && LowerRow[IdxLower].Id == CurrentId) { 10106c3fb27SDimitry Andric LowerV = LowerRow[IdxLower].Coefficient; 10206c3fb27SDimitry Andric IdxLower++; 10306c3fb27SDimitry Andric } 10406c3fb27SDimitry Andric 1051db9f3b2SDimitry Andric if (MulOverflow(LowerV, UpperLast, M2)) 106e8d8bef9SDimitry Andric return false; 107e8d8bef9SDimitry Andric if (AddOverflow(M1, M2, N)) 108e8d8bef9SDimitry Andric return false; 10906c3fb27SDimitry Andric if (N == 0) 11006c3fb27SDimitry Andric continue; 11106c3fb27SDimitry Andric NR.emplace_back(N, CurrentId); 112e8d8bef9SDimitry Andric } 11306c3fb27SDimitry Andric if (NR.empty()) 11406c3fb27SDimitry Andric continue; 11506c3fb27SDimitry Andric Constraints.push_back(std::move(NR)); 116e8d8bef9SDimitry Andric // Give up if the new system gets too big. 11706c3fb27SDimitry Andric if (Constraints.size() > 500) 118e8d8bef9SDimitry Andric return false; 119e8d8bef9SDimitry Andric } 120e8d8bef9SDimitry Andric } 12106c3fb27SDimitry Andric NumVariables -= 1; 122e8d8bef9SDimitry Andric 123e8d8bef9SDimitry Andric return true; 124e8d8bef9SDimitry Andric } 125e8d8bef9SDimitry Andric 126e8d8bef9SDimitry Andric bool ConstraintSystem::mayHaveSolutionImpl() { 12706c3fb27SDimitry Andric while (!Constraints.empty() && NumVariables > 1) { 128e8d8bef9SDimitry Andric if (!eliminateUsingFM()) 129e8d8bef9SDimitry Andric return true; 130e8d8bef9SDimitry Andric } 131e8d8bef9SDimitry Andric 13206c3fb27SDimitry Andric if (Constraints.empty() || NumVariables > 1) 133e8d8bef9SDimitry Andric return true; 134e8d8bef9SDimitry Andric 13506c3fb27SDimitry Andric return all_of(Constraints, [](auto &R) { 13606c3fb27SDimitry Andric if (R.empty()) 13706c3fb27SDimitry Andric return true; 13806c3fb27SDimitry Andric if (R[0].Id == 0) 13906c3fb27SDimitry Andric return R[0].Coefficient >= 0; 14006c3fb27SDimitry Andric return true; 14106c3fb27SDimitry Andric }); 142e8d8bef9SDimitry Andric } 143e8d8bef9SDimitry Andric 14406c3fb27SDimitry Andric SmallVector<std::string> ConstraintSystem::getVarNamesList() const { 14506c3fb27SDimitry Andric SmallVector<std::string> Names(Value2Index.size(), ""); 14606c3fb27SDimitry Andric #ifndef NDEBUG 14706c3fb27SDimitry Andric for (auto &[V, Index] : Value2Index) { 14806c3fb27SDimitry Andric std::string OperandName; 14906c3fb27SDimitry Andric if (V->getName().empty()) 15006c3fb27SDimitry Andric OperandName = V->getNameOrAsOperand(); 15106c3fb27SDimitry Andric else 15206c3fb27SDimitry Andric OperandName = std::string("%") + V->getName().str(); 15306c3fb27SDimitry Andric Names[Index - 1] = OperandName; 154e8d8bef9SDimitry Andric } 15506c3fb27SDimitry Andric #endif 15606c3fb27SDimitry Andric return Names; 157e8d8bef9SDimitry Andric } 158e8d8bef9SDimitry Andric 159e8d8bef9SDimitry Andric void ConstraintSystem::dump() const { 16006c3fb27SDimitry Andric #ifndef NDEBUG 16106c3fb27SDimitry Andric if (Constraints.empty()) 16206c3fb27SDimitry Andric return; 16306c3fb27SDimitry Andric SmallVector<std::string> Names = getVarNamesList(); 16406c3fb27SDimitry Andric for (const auto &Row : Constraints) { 16506c3fb27SDimitry Andric SmallVector<std::string, 16> Parts; 166*0fca6ea1SDimitry Andric for (const Entry &E : Row) { 167*0fca6ea1SDimitry Andric if (E.Id >= NumVariables) 16806c3fb27SDimitry Andric break; 169*0fca6ea1SDimitry Andric if (E.Id == 0) 17006c3fb27SDimitry Andric continue; 17106c3fb27SDimitry Andric std::string Coefficient; 172*0fca6ea1SDimitry Andric if (E.Coefficient != 1) 173*0fca6ea1SDimitry Andric Coefficient = std::to_string(E.Coefficient) + " * "; 174*0fca6ea1SDimitry Andric Parts.push_back(Coefficient + Names[E.Id - 1]); 17506c3fb27SDimitry Andric } 17606c3fb27SDimitry Andric // assert(!Parts.empty() && "need to have at least some parts"); 17706c3fb27SDimitry Andric int64_t ConstPart = 0; 17806c3fb27SDimitry Andric if (Row[0].Id == 0) 17906c3fb27SDimitry Andric ConstPart = Row[0].Coefficient; 18006c3fb27SDimitry Andric LLVM_DEBUG(dbgs() << join(Parts, std::string(" + ")) 18106c3fb27SDimitry Andric << " <= " << std::to_string(ConstPart) << "\n"); 18206c3fb27SDimitry Andric } 18306c3fb27SDimitry Andric #endif 184e8d8bef9SDimitry Andric } 185e8d8bef9SDimitry Andric 186e8d8bef9SDimitry Andric bool ConstraintSystem::mayHaveSolution() { 18706c3fb27SDimitry Andric LLVM_DEBUG(dbgs() << "---\n"); 188e8d8bef9SDimitry Andric LLVM_DEBUG(dump()); 189e8d8bef9SDimitry Andric bool HasSolution = mayHaveSolutionImpl(); 190e8d8bef9SDimitry Andric LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n"); 191e8d8bef9SDimitry Andric return HasSolution; 192e8d8bef9SDimitry Andric } 193e8d8bef9SDimitry Andric 19404eeddc0SDimitry Andric bool ConstraintSystem::isConditionImplied(SmallVector<int64_t, 8> R) const { 195e8d8bef9SDimitry Andric // If all variable coefficients are 0, we have 'C >= 0'. If the constant is >= 196e8d8bef9SDimitry Andric // 0, R is always true, regardless of the system. 197bdd1243dSDimitry Andric if (all_of(ArrayRef(R).drop_front(1), [](int64_t C) { return C == 0; })) 198e8d8bef9SDimitry Andric return R[0] >= 0; 199e8d8bef9SDimitry Andric 200e8d8bef9SDimitry Andric // If there is no solution with the negation of R added to the system, the 201e8d8bef9SDimitry Andric // condition must hold based on the existing constraints. 202e8d8bef9SDimitry Andric R = ConstraintSystem::negate(R); 20306c3fb27SDimitry Andric if (R.empty()) 20406c3fb27SDimitry Andric return false; 205e8d8bef9SDimitry Andric 206e8d8bef9SDimitry Andric auto NewSystem = *this; 207e8d8bef9SDimitry Andric NewSystem.addVariableRow(R); 208e8d8bef9SDimitry Andric return !NewSystem.mayHaveSolution(); 209e8d8bef9SDimitry Andric } 210