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