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