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 (unsigned I = 0, S = Row.size(); I < S; ++I) {
167       if (Row[I].Id >= NumVariables)
168         break;
169       if (Row[I].Id == 0)
170         continue;
171       std::string Coefficient;
172       if (Row[I].Coefficient != 1)
173         Coefficient = std::to_string(Row[I].Coefficient) + " * ";
174       Parts.push_back(Coefficient + Names[Row[I].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 }
210