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/SmallBitVector.h"
11#include "llvm/ADT/SmallVector.h"
12#include "llvm/ADT/StringExtras.h"
13#include "llvm/IR/Value.h"
14#include "llvm/Support/Debug.h"
15#include "llvm/Support/MathExtras.h"
16
17#include <numeric>
18#include <string>
19
20using namespace llvm;
21
22#define DEBUG_TYPE "constraint-system"
23
24bool ConstraintSystem::eliminateUsingFM() {
25 // Implementation of Fourier–Motzkin elimination, with some tricks from the
26 // paper Pugh, William. "The Omega test: a fast and practical integer
27 // programming algorithm for dependence
28 // analysis."
29 // Supercomputing'91: Proceedings of the 1991 ACM/
30 // IEEE conference on Supercomputing. IEEE, 1991.
31 assert(!Constraints.empty() &&
32 "should only be called for non-empty constraint systems");
33
34 unsigned LastIdx = NumVariables;
35
36 // First, either remove the variable in place if it is 0 or add the row to
37 // RemainingRows and remove it from the system.
38 SmallVector<RowTy, 4> RemainingRows;
39 for (unsigned R1 = 0; R1 < Constraints.size();) {
40 RowTy &Row1 = Constraints[R1];
41 if (getLastCoefficient(R: Row1, Id: LastIdx) == 0) {
42 if (Row1.size() > 0 && Row1.back().Id == LastIdx)
43 Row1.pop_back();
44 R1++;
45 } else {
46 std::swap(LHS&: Constraints[R1], RHS&: Constraints.back());
47 RemainingRows.push_back(Elt: std::move(Constraints.back()));
48 Constraints.pop_back();
49 }
50 }
51
52 // Process rows where the variable is != 0.
53 unsigned NumRemainingConstraints = RemainingRows.size();
54 for (unsigned R1 = 0; R1 < NumRemainingConstraints; R1++) {
55 // FIXME do not use copy
56 for (unsigned R2 = R1 + 1; R2 < NumRemainingConstraints; R2++) {
57 // Examples of constraints stored as {Constant, Coeff_x, Coeff_y}
58 // R1: 0 >= 1 * x + (-2) * y => { 0, 1, -2 }
59 // R2: 3 >= 2 * x + 3 * y => { 3, 2, 3 }
60 // LastIdx = 2 (tracking coefficient of y)
61 // UpperLast: 3
62 // LowerLast: -2
63 int64_t UpperLast = getLastCoefficient(R: RemainingRows[R2], Id: LastIdx);
64 int64_t LowerLast = getLastCoefficient(R: RemainingRows[R1], Id: LastIdx);
65 assert(
66 UpperLast != 0 && LowerLast != 0 &&
67 "RemainingRows should only contain rows where the variable is != 0");
68
69 if ((LowerLast < 0 && UpperLast < 0) || (LowerLast > 0 && UpperLast > 0))
70 continue;
71
72 unsigned LowerR = R1;
73 unsigned UpperR = R2;
74 if (UpperLast < 0) {
75 std::swap(a&: LowerR, b&: UpperR);
76 std::swap(a&: LowerLast, b&: UpperLast);
77 }
78
79 RowTy NR;
80 unsigned IdxUpper = 0;
81 unsigned IdxLower = 0;
82 auto &LowerRow = RemainingRows[LowerR];
83 auto &UpperRow = RemainingRows[UpperR];
84 // Combine the two rows to eliminate the variable. If any coefficient
85 // computation overflows, skip them.
86 bool Overflow = false;
87 // Update constant and coefficients of both constraints.
88 // Stops until every coefficient is updated or overflows.
89 while (true) {
90 if (IdxUpper >= UpperRow.size() || IdxLower >= LowerRow.size())
91 break;
92 int64_t M1, M2, N;
93 // Starts with index 0 and updates every coefficients.
94 int64_t UpperV = 0;
95 int64_t LowerV = 0;
96 uint16_t CurrentId = std::numeric_limits<uint16_t>::max();
97 if (IdxUpper < UpperRow.size()) {
98 CurrentId = std::min(a: UpperRow[IdxUpper].Id, b: CurrentId);
99 }
100 if (IdxLower < LowerRow.size()) {
101 CurrentId = std::min(a: LowerRow[IdxLower].Id, b: CurrentId);
102 }
103
104 if (IdxUpper < UpperRow.size() && UpperRow[IdxUpper].Id == CurrentId) {
105 UpperV = UpperRow[IdxUpper].Coefficient;
106 IdxUpper++;
107 }
108
109 if (MulOverflow(X: UpperV, Y: -1 * LowerLast, Result&: M1)) {
110 Overflow = true;
111 break;
112 }
113 if (IdxLower < LowerRow.size() && LowerRow[IdxLower].Id == CurrentId) {
114 LowerV = LowerRow[IdxLower].Coefficient;
115 IdxLower++;
116 }
117
118 if (MulOverflow(X: LowerV, Y: UpperLast, Result&: M2)) {
119 Overflow = true;
120 break;
121 }
122 // This algorithm is a variant of sparse Gaussian elimination.
123 //
124 // The new coefficient for CurrentId is
125 // N = UpperV * (-1) * LowerLast + LowerV * UpperLast
126 //
127 // UpperRow: { 3, 2, 3 }, LowerLast: -2
128 // LowerRow: { 0, 1, -2 }, UpperLast: 3
129 //
130 // After multiplication:
131 // UpperRow: { 6, 4, 6 }
132 // LowerRow: { 0, 3, -6 }
133 //
134 // Eliminates y after addition:
135 // N: { 6, 7, 0 } => 6 >= 7 * x
136 if (AddOverflow(X: M1, Y: M2, Result&: N)) {
137 Overflow = true;
138 break;
139 }
140 // Skip variable that is completely eliminated.
141 if (N == 0)
142 continue;
143 NR.emplace_back(Args&: N, Args&: CurrentId);
144 }
145 if (Overflow || NR.empty())
146 continue;
147 normalizeByGCD(R: NR);
148 Constraints.push_back(Elt: std::move(NR));
149 // Give up if the new system gets too big.
150 if (Constraints.size() > 500)
151 return false;
152 }
153 }
154 NumVariables -= 1;
155
156 return true;
157}
158
159void ConstraintSystem::normalizeByGCD(MutableArrayRef<Entry> R) {
160 // The sum of the variable terms is a multiple of G, so it is <= C iff it is
161 // <= floor(C / G) * G.
162 int64_t G = 0;
163 for (const Entry &E : R) {
164 if (E.Id == 0)
165 continue;
166 if (E.Coefficient == std::numeric_limits<int64_t>::min())
167 return;
168 G = std::gcd(m: G, n: E.Coefficient);
169 if (G == 1)
170 return;
171 }
172 if (G == 0)
173 return;
174 for (Entry &E : R)
175 E.Coefficient =
176 E.Id == 0 ? divideFloorSigned(Numerator: E.Coefficient, Denominator: G) : E.Coefficient / G;
177}
178
179bool ConstraintSystem::mayHaveSolutionImpl() {
180 while (!Constraints.empty() && NumVariables > 0) {
181 if (!eliminateUsingFM())
182 return true;
183 }
184
185 assert((Constraints.empty() || NumVariables == 0) &&
186 "non-empty system must have all variables eliminated");
187 return all_of(Range&: Constraints,
188 P: [](ArrayRef<Entry> R) { return getConstant(R) >= 0; });
189}
190
191SmallVector<std::string> ConstraintSystem::getVarNamesList() const {
192 SmallVector<std::string> Names(Value2Index.size(), "");
193#ifndef NDEBUG
194 for (auto &[V, Index] : Value2Index) {
195 std::string OperandName;
196 if (V->getName().empty())
197 OperandName = V->getNameOrAsOperand();
198 else
199 OperandName = std::string("%") + V->getName().str();
200 Names[Index - 1] = OperandName;
201 }
202#endif
203 return Names;
204}
205
206void ConstraintSystem::dump() const {
207#ifndef NDEBUG
208 if (Constraints.empty())
209 return;
210 SmallVector<std::string> Names = getVarNamesList();
211 for (const auto &Row : Constraints) {
212 SmallVector<std::string, 16> Parts;
213 for (const Entry &E : Row) {
214 if (E.Id > NumVariables)
215 break;
216 if (E.Id == 0)
217 continue;
218 // The Value2Index map (and hence Names) may be absent, e.g. for the
219 // temporary system solved in isConditionImplied. Fall back to a generic
220 // variable name in that case.
221 std::string Name = E.Id <= Names.size() ? Names[E.Id - 1]
222 : ("%v" + std::to_string(E.Id));
223 std::string Coefficient;
224 if (E.Coefficient != 1)
225 Coefficient = std::to_string(E.Coefficient) + " * ";
226 Parts.push_back(Coefficient + Name);
227 }
228 LLVM_DEBUG(dbgs() << join(Parts, " + ") << " <= " << getConstant(Row)
229 << "\n");
230 }
231#endif
232}
233
234bool ConstraintSystem::mayHaveSolution() {
235 LLVM_DEBUG(dbgs() << "---\n");
236 LLVM_DEBUG(dump());
237 bool HasSolution = mayHaveSolutionImpl();
238 LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");
239 return HasSolution;
240}
241
242std::pair<ConstraintSystem, ConstraintSystem::RowTy>
243ConstraintSystem::getSubSystem(ArrayRef<Entry> R) const {
244 assert((R.empty() || R.back().Id <= NumVariables) &&
245 "query must only use variables of the system");
246 // Only constraints that share a variable (transitively) with a query R can
247 // affect whether system + !R has a solution.
248 //
249 // Mark variables in the query and collect to the transitive closure over
250 // variables that co-occur in a constraint row.
251 ConstraintSystem SubSystem;
252 SmallBitVector InSystem(NumVariables + 1, false);
253 for (const Entry &E : R)
254 if (E.Id != 0)
255 InSystem[E.Id] = true;
256 auto SharesVariable = [&InSystem](ArrayRef<Entry> Row) {
257 return any_of(Range&: Row, P: [&InSystem](const Entry &E) {
258 return E.Id != 0 && InSystem[E.Id];
259 });
260 };
261 bool Changed = true;
262 while (Changed) {
263 Changed = false;
264 for (const RowTy &Row : Constraints) {
265 // No common variables, skip.
266 if (!SharesVariable(Row))
267 continue;
268 for (const Entry &E : Row)
269 if (E.Id != 0 && !InSystem[E.Id]) {
270 InSystem[E.Id] = true;
271 Changed = true;
272 }
273 }
274 }
275
276 // Assign compact indices to the variables of the sub-system.
277 SmallVector<unsigned, 16> OldToNew(NumVariables + 1, 0);
278 unsigned NextIdx = 1;
279 for (unsigned Id : InSystem.set_bits())
280 OldToNew[Id] = NextIdx++;
281
282 // Build new compact set of rows.
283 SubSystem.NumVariables = NextIdx - 1;
284 for (const RowTy &Row : Constraints) {
285 if (!SharesVariable(Row))
286 continue;
287 RowTy NewRow;
288 for (const Entry &E : Row) {
289 unsigned New = OldToNew[E.Id];
290 assert((E.Id == 0) == (New == 0) && "constant entry must be preserved");
291 NewRow.emplace_back(Args: E.Coefficient, Args&: New);
292 }
293 SubSystem.Constraints.push_back(Elt: std::move(NewRow));
294 }
295
296 // Remap the query row into the component's compact index space.
297 RowTy NewR(1, Entry(getConstant(R), 0));
298 for (const Entry &E : R)
299 if (E.Id != 0)
300 NewR.emplace_back(Args: E.Coefficient, Args&: OldToNew[E.Id]);
301 return {std::move(SubSystem), std::move(NewR)};
302}
303
304bool ConstraintSystem::isImpliedBySingleRow(ArrayRef<Entry> R) const {
305 int64_t C = getConstant(R);
306 if (hasConstantEntry(R))
307 R = R.drop_front();
308 return any_of(Range: Constraints, P: [&](ArrayRef<Entry> Row) {
309 if (getConstant(R: Row) > C)
310 return false;
311 if (hasConstantEntry(R: Row))
312 Row = Row.drop_front();
313 return equal(LRange&: Row, RRange&: R, P: [](const Entry &A, const Entry &B) {
314 return A.Id == B.Id && A.Coefficient == B.Coefficient;
315 });
316 });
317}
318
319bool ConstraintSystem::isConditionImplied(RowTy R) const {
320 // If all variable coefficients are 0, we have 'C >= 0'. If the constant is >=
321 // 0, R is always true, regardless of the system.
322 if (isConstantOnly(R))
323 return getConstant(R) >= 0;
324
325 normalizeByGCD(R);
326
327 // R is trivially implied if a single row of the system implies it.
328 if (isImpliedBySingleRow(R))
329 return true;
330
331 // If there is no solution with the negation of R added to the system, the
332 // condition must hold based on the existing constraints.
333 R = ConstraintSystem::negate(R: std::move(R));
334 if (R.empty())
335 return false;
336
337 auto Copy = *this;
338 Copy.addRow(R, NumVars: NumVariables);
339 return !Copy.mayHaveSolution();
340}
341
342bool ConstraintSystem::isConditionImpliedInSubSystem(ArrayRef<Entry> R) const {
343 if (R.empty())
344 return false;
345
346 // Queries with no variables are trivially decided without building any
347 // component.
348 if (isConstantOnly(R))
349 return getConstant(R) >= 0;
350
351 // A single query: build the component and solve it in place.
352 const auto &[SubCS, NewR] = getSubSystem(R);
353 return SubCS.isConditionImplied(R: NewR);
354}
355