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/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 }