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 <string>
16
17 using namespace llvm;
18
19 #define DEBUG_TYPE "constraint-system"
20
eliminateUsingFM()21 bool ConstraintSystem::eliminateUsingFM() {
22 // Implementation of Fourier–Motzkin elimination, with some tricks from the
23 // paper Pugh, William. "The Omega test: a fast and practical integer
24 // programming algorithm for dependence
25 // analysis."
26 // Supercomputing'91: Proceedings of the 1991 ACM/
27 // IEEE conference on Supercomputing. IEEE, 1991.
28 assert(!Constraints.empty() &&
29 "should only be called for non-empty constraint systems");
30 unsigned NumVariables = Constraints[0].size();
31 SmallVector<SmallVector<int64_t, 8>, 4> NewSystem;
32
33 unsigned NumConstraints = Constraints.size();
34 uint32_t NewGCD = 1;
35 // FIXME do not use copy
36 for (unsigned R1 = 0; R1 < NumConstraints; R1++) {
37 if (Constraints[R1][1] == 0) {
38 SmallVector<int64_t, 8> NR;
39 NR.push_back(Constraints[R1][0]);
40 for (unsigned i = 2; i < NumVariables; i++) {
41 NR.push_back(Constraints[R1][i]);
42 }
43 NewSystem.push_back(std::move(NR));
44 continue;
45 }
46
47 // FIXME do not use copy
48 for (unsigned R2 = R1 + 1; R2 < NumConstraints; R2++) {
49 if (R1 == R2)
50 continue;
51
52 // FIXME: can we do better than just dropping things here?
53 if (Constraints[R2][1] == 0)
54 continue;
55
56 if ((Constraints[R1][1] < 0 && Constraints[R2][1] < 0) ||
57 (Constraints[R1][1] > 0 && Constraints[R2][1] > 0))
58 continue;
59
60 unsigned LowerR = R1;
61 unsigned UpperR = R2;
62 if (Constraints[UpperR][1] < 0)
63 std::swap(LowerR, UpperR);
64
65 SmallVector<int64_t, 8> NR;
66 for (unsigned I = 0; I < NumVariables; I++) {
67 if (I == 1)
68 continue;
69
70 int64_t M1, M2, N;
71 if (MulOverflow(Constraints[UpperR][I],
72 ((-1) * Constraints[LowerR][1] / GCD), M1))
73 return false;
74 if (MulOverflow(Constraints[LowerR][I],
75 (Constraints[UpperR][1] / GCD), M2))
76 return false;
77 if (AddOverflow(M1, M2, N))
78 return false;
79 NR.push_back(N);
80
81 NewGCD = APIntOps::GreatestCommonDivisor({32, (uint32_t)NR.back()},
82 {32, NewGCD})
83 .getZExtValue();
84 }
85 NewSystem.push_back(std::move(NR));
86 // Give up if the new system gets too big.
87 if (NewSystem.size() > 500)
88 return false;
89 }
90 }
91 Constraints = std::move(NewSystem);
92 GCD = NewGCD;
93
94 return true;
95 }
96
mayHaveSolutionImpl()97 bool ConstraintSystem::mayHaveSolutionImpl() {
98 while (!Constraints.empty() && Constraints[0].size() > 1) {
99 if (!eliminateUsingFM())
100 return true;
101 }
102
103 if (Constraints.empty() || Constraints[0].size() > 1)
104 return true;
105
106 return all_of(Constraints, [](auto &R) { return R[0] >= 0; });
107 }
108
dump(ArrayRef<std::string> Names) const109 void ConstraintSystem::dump(ArrayRef<std::string> Names) const {
110 if (Constraints.empty())
111 return;
112
113 for (const auto &Row : Constraints) {
114 SmallVector<std::string, 16> Parts;
115 for (unsigned I = 1, S = Row.size(); I < S; ++I) {
116 if (Row[I] == 0)
117 continue;
118 std::string Coefficient;
119 if (Row[I] != 1)
120 Coefficient = std::to_string(Row[I]) + " * ";
121 Parts.push_back(Coefficient + Names[I - 1]);
122 }
123 assert(!Parts.empty() && "need to have at least some parts");
124 LLVM_DEBUG(dbgs() << join(Parts, std::string(" + "))
125 << " <= " << std::to_string(Row[0]) << "\n");
126 }
127 }
128
dump() const129 void ConstraintSystem::dump() const {
130 SmallVector<std::string, 16> Names;
131 for (unsigned i = 1; i < Constraints.back().size(); ++i)
132 Names.push_back("x" + std::to_string(i));
133 LLVM_DEBUG(dbgs() << "---\n");
134 dump(Names);
135 }
136
mayHaveSolution()137 bool ConstraintSystem::mayHaveSolution() {
138 LLVM_DEBUG(dump());
139 bool HasSolution = mayHaveSolutionImpl();
140 LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");
141 return HasSolution;
142 }
143
isConditionImplied(SmallVector<int64_t,8> R) const144 bool ConstraintSystem::isConditionImplied(SmallVector<int64_t, 8> R) const {
145 // If all variable coefficients are 0, we have 'C >= 0'. If the constant is >=
146 // 0, R is always true, regardless of the system.
147 if (all_of(ArrayRef(R).drop_front(1), [](int64_t C) { return C == 0; }))
148 return R[0] >= 0;
149
150 // If there is no solution with the negation of R added to the system, the
151 // condition must hold based on the existing constraints.
152 R = ConstraintSystem::negate(R);
153
154 auto NewSystem = *this;
155 NewSystem.addVariableRow(R);
156 return !NewSystem.mayHaveSolution();
157 }
158