llvm/lib/Analysis/ConstraintSystem.cpp

   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/IR/Value.h"
  14 #include "llvm/Support/Debug.h"
  15
  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
  32   unsigned LastIdx = NumVariables - 1;
  33
  34   // First, either remove the variable in place if it is 0 or add the row to
  35   // RemainingRows and remove it from the system.
  36   SmallVector<SmallVector<Entry, 8>, 4> RemainingRows;
  37   for (unsigned R1 = 0; R1 < Constraints.size();) {
  38     SmallVector<Entry, 8> &Row1 = Constraints[R1];
  39     if (getLastCoefficient(Row1, LastIdx) == 0) {
  40       if (Row1.size() > 0 && Row1.back().Id == LastIdx)
  41         Row1.pop_back();
  42       R1++;
  43     } else {
  44       std::swap(Constraints[R1], Constraints.back());
  45       RemainingRows.push_back(std::move(Constraints.back()));
  46       Constraints.pop_back();
  47     }
  48   }
  49
  50   // Process rows where the variable is != 0.
  51   unsigned NumRemainingConstraints = RemainingRows.size();
  52   for (unsigned R1 = 0; R1 < NumRemainingConstraints; R1++) {
  53     // FIXME do not use copy
  54     for (unsigned R2 = R1 + 1; R2 < NumRemainingConstraints; R2++) {
  55       int64_t UpperLast = getLastCoefficient(RemainingRows[R2], LastIdx);
  56       int64_t LowerLast = getLastCoefficient(RemainingRows[R1], LastIdx);
  57       assert(
  58           UpperLast != 0 && LowerLast != 0 &&
  59           "RemainingRows should only contain rows where the variable is != 0");
  60
  61       if ((LowerLast < 0 && UpperLast < 0) || (LowerLast > 0 && UpperLast > 0))
  62         continue;
  63
  64       unsigned LowerR = R1;
  65       unsigned UpperR = R2;
  66       if (UpperLast < 0) {
  67         std::swap(LowerR, UpperR);
  68         std::swap(LowerLast, UpperLast);
  69       }
  70
  71       SmallVector<Entry, 8> NR;
  72       unsigned IdxUpper = 0;
  73       unsigned IdxLower = 0;
  74       auto &LowerRow = RemainingRows[LowerR];
  75       auto &UpperRow = RemainingRows[UpperR];
  76       while (true) {
  77         if (IdxUpper >= UpperRow.size() || IdxLower >= LowerRow.size())
  78           break;
  79         int64_t M1, M2, N;
  80         int64_t UpperV = 0;
  81         int64_t LowerV = 0;
  82         uint16_t CurrentId = std::numeric_limits<uint16_t>::max();
  83         if (IdxUpper < UpperRow.size()) {
  84           CurrentId = std::min(UpperRow[IdxUpper].Id, CurrentId);
  85         }
  86         if (IdxLower < LowerRow.size()) {
  87           CurrentId = std::min(LowerRow[IdxLower].Id, CurrentId);
  88         }
  89
  90         if (IdxUpper < UpperRow.size() && UpperRow[IdxUpper].Id == CurrentId) {
  91           UpperV = UpperRow[IdxUpper].Coefficient;
  92           IdxUpper++;
  93         }
  94
  95         if (MulOverflow(UpperV, -1 * LowerLast, M1))
  96           return false;
  97         if (IdxLower < LowerRow.size() && LowerRow[IdxLower].Id == CurrentId) {
  98           LowerV = LowerRow[IdxLower].Coefficient;
  99           IdxLower++;
 100         }
 101
 102         if (MulOverflow(LowerV, UpperLast, M2))
 103           return false;
 104         if (AddOverflow(M1, M2, N))
 105           return false;
 106         if (N == 0)
 107           continue;
 108         NR.emplace_back(N, CurrentId);
 109       }
 110       if (NR.empty())
 111         continue;
 112       Constraints.push_back(std::move(NR));
 113       // Give up if the new system gets too big.
 114       if (Constraints.size() > 500)
 115         return false;
 116     }
 117   }
 118   NumVariables -= 1;
 119
 120   return true;
 121 }
 122
 123 bool ConstraintSystem::mayHaveSolutionImpl() {
 124   while (!Constraints.empty() && NumVariables > 1) {
 125     if (!eliminateUsingFM())
 126       return true;
 127   }
 128
 129   if (Constraints.empty() || NumVariables > 1)
 130     return true;
 131
 132   return all_of(Constraints, [](auto &R) {
 133     if (R.empty())
 134       return true;
 135     if (R[0].Id == 0)
 136       return R[0].Coefficient >= 0;
 137     return true;
 138   });
 139 }
 140
 141 SmallVector<std::string> ConstraintSystem::getVarNamesList() const {
 142   SmallVector<std::string> Names(Value2Index.size(), "");
 143 #ifndef NDEBUG
 144   for (auto &[V, Index] : Value2Index) {
 145     std::string OperandName;
 146     if (V->getName().empty())
 147       OperandName = V->getNameOrAsOperand();
 148     else
 149       OperandName = std::string("%") + V->getName().str();
 150     Names[Index - 1] = OperandName;
 151   }
 152 #endif
 153   return Names;
 154 }
 155
 156 void ConstraintSystem::dump() const {
 157 #ifndef NDEBUG
 158   if (Constraints.empty())
 159     return;
 160   SmallVector<std::string> Names = getVarNamesList();
 161   for (const auto &Row : Constraints) {
 162     SmallVector<std::string, 16> Parts;
 163     for (const Entry &E : Row) {
 164       if (E.Id >= NumVariables)
 165         break;
 166       if (E.Id == 0)
 167         continue;
 168       std::string Coefficient;
 169       if (E.Coefficient != 1)
 170         Coefficient = std::to_string(E.Coefficient) + " * ";
 171       Parts.push_back(Coefficient + Names[E.Id - 1]);
 172     }
 173     // assert(!Parts.empty() && "need to have at least some parts");
 174     int64_t ConstPart = 0;
 175     if (Row[0].Id == 0)
 176       ConstPart = Row[0].Coefficient;
 177     LLVM_DEBUG(dbgs() << join(Parts, std::string(" + "))
 178                       << " <= " << std::to_string(ConstPart) << "\n");
 179   }
 180 #endif
 181 }
 182
 183 bool ConstraintSystem::mayHaveSolution() {
 184   LLVM_DEBUG(dbgs() << "---\n");
 185   LLVM_DEBUG(dump());
 186   bool HasSolution = mayHaveSolutionImpl();
 187   LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");
 188   return HasSolution;
 189 }
 190
 191 bool ConstraintSystem::isConditionImplied(SmallVector<int64_t, 8> R) const {
 192   // If all variable coefficients are 0, we have 'C >= 0'. If the constant is >=
 193   // 0, R is always true, regardless of the system.
 194   if (all_of(ArrayRef(R).drop_front(1), [](int64_t C) { return C == 0; }))
 195     return R[0] >= 0;
 196
 197   // If there is no solution with the negation of R added to the system, the
 198   // condition must hold based on the existing constraints.
 199   R = ConstraintSystem::negate(R);
 200   if (R.empty())
 201     return false;
 202
 203   auto NewSystem = *this;
 204   NewSystem.addVariableRow(R);
 205   return !NewSystem.mayHaveSolution();
 206 }