xref: /freebsd-src/contrib/llvm-project/llvm/lib/Analysis/ConstraintSystem.cpp (revision 0fca6ea1d4eea4c934cfff25ac9ee8ad6fe95583)
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