llvm-project
209 строк · 6.5 Кб
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
18using namespace llvm;
19
20#define DEBUG_TYPE "constraint-system"
21
22bool 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.
29assert(!Constraints.empty() &&
30"should only be called for non-empty constraint systems");
31
32unsigned 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.
36SmallVector<SmallVector<Entry, 8>, 4> RemainingRows;
37for (unsigned R1 = 0; R1 < Constraints.size();) {
38SmallVector<Entry, 8> &Row1 = Constraints[R1];
39if (getLastCoefficient(Row1, LastIdx) == 0) {
40if (Row1.size() > 0 && Row1.back().Id == LastIdx)
41Row1.pop_back();
42R1++;
43} else {
44std::swap(Constraints[R1], Constraints.back());
45RemainingRows.push_back(std::move(Constraints.back()));
46Constraints.pop_back();
47}
48}
49
50// Process rows where the variable is != 0.
51unsigned NumRemainingConstraints = RemainingRows.size();
52for (unsigned R1 = 0; R1 < NumRemainingConstraints; R1++) {
53// FIXME do not use copy
54for (unsigned R2 = R1 + 1; R2 < NumRemainingConstraints; R2++) {
55if (R1 == R2)
56continue;
57
58int64_t UpperLast = getLastCoefficient(RemainingRows[R2], LastIdx);
59int64_t LowerLast = getLastCoefficient(RemainingRows[R1], LastIdx);
60assert(
61UpperLast != 0 && LowerLast != 0 &&
62"RemainingRows should only contain rows where the variable is != 0");
63
64if ((LowerLast < 0 && UpperLast < 0) || (LowerLast > 0 && UpperLast > 0))
65continue;
66
67unsigned LowerR = R1;
68unsigned UpperR = R2;
69if (UpperLast < 0) {
70std::swap(LowerR, UpperR);
71std::swap(LowerLast, UpperLast);
72}
73
74SmallVector<Entry, 8> NR;
75unsigned IdxUpper = 0;
76unsigned IdxLower = 0;
77auto &LowerRow = RemainingRows[LowerR];
78auto &UpperRow = RemainingRows[UpperR];
79while (true) {
80if (IdxUpper >= UpperRow.size() || IdxLower >= LowerRow.size())
81break;
82int64_t M1, M2, N;
83int64_t UpperV = 0;
84int64_t LowerV = 0;
85uint16_t CurrentId = std::numeric_limits<uint16_t>::max();
86if (IdxUpper < UpperRow.size()) {
87CurrentId = std::min(UpperRow[IdxUpper].Id, CurrentId);
88}
89if (IdxLower < LowerRow.size()) {
90CurrentId = std::min(LowerRow[IdxLower].Id, CurrentId);
91}
92
93if (IdxUpper < UpperRow.size() && UpperRow[IdxUpper].Id == CurrentId) {
94UpperV = UpperRow[IdxUpper].Coefficient;
95IdxUpper++;
96}
97
98if (MulOverflow(UpperV, -1 * LowerLast, M1))
99return false;
100if (IdxLower < LowerRow.size() && LowerRow[IdxLower].Id == CurrentId) {
101LowerV = LowerRow[IdxLower].Coefficient;
102IdxLower++;
103}
104
105if (MulOverflow(LowerV, UpperLast, M2))
106return false;
107if (AddOverflow(M1, M2, N))
108return false;
109if (N == 0)
110continue;
111NR.emplace_back(N, CurrentId);
112}
113if (NR.empty())
114continue;
115Constraints.push_back(std::move(NR));
116// Give up if the new system gets too big.
117if (Constraints.size() > 500)
118return false;
119}
120}
121NumVariables -= 1;
122
123return true;
124}
125
126bool ConstraintSystem::mayHaveSolutionImpl() {
127while (!Constraints.empty() && NumVariables > 1) {
128if (!eliminateUsingFM())
129return true;
130}
131
132if (Constraints.empty() || NumVariables > 1)
133return true;
134
135return all_of(Constraints, [](auto &R) {
136if (R.empty())
137return true;
138if (R[0].Id == 0)
139return R[0].Coefficient >= 0;
140return true;
141});
142}
143
144SmallVector<std::string> ConstraintSystem::getVarNamesList() const {
145SmallVector<std::string> Names(Value2Index.size(), "");
146#ifndef NDEBUG
147for (auto &[V, Index] : Value2Index) {
148std::string OperandName;
149if (V->getName().empty())
150OperandName = V->getNameOrAsOperand();
151else
152OperandName = std::string("%") + V->getName().str();
153Names[Index - 1] = OperandName;
154}
155#endif
156return Names;
157}
158
159void ConstraintSystem::dump() const {
160#ifndef NDEBUG
161if (Constraints.empty())
162return;
163SmallVector<std::string> Names = getVarNamesList();
164for (const auto &Row : Constraints) {
165SmallVector<std::string, 16> Parts;
166for (const Entry &E : Row) {
167if (E.Id >= NumVariables)
168break;
169if (E.Id == 0)
170continue;
171std::string Coefficient;
172if (E.Coefficient != 1)
173Coefficient = std::to_string(E.Coefficient) + " * ";
174Parts.push_back(Coefficient + Names[E.Id - 1]);
175}
176// assert(!Parts.empty() && "need to have at least some parts");
177int64_t ConstPart = 0;
178if (Row[0].Id == 0)
179ConstPart = Row[0].Coefficient;
180LLVM_DEBUG(dbgs() << join(Parts, std::string(" + "))
181<< " <= " << std::to_string(ConstPart) << "\n");
182}
183#endif
184}
185
186bool ConstraintSystem::mayHaveSolution() {
187LLVM_DEBUG(dbgs() << "---\n");
188LLVM_DEBUG(dump());
189bool HasSolution = mayHaveSolutionImpl();
190LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");
191return HasSolution;
192}
193
194bool 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.
197if (all_of(ArrayRef(R).drop_front(1), [](int64_t C) { return C == 0; }))
198return 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.
202R = ConstraintSystem::negate(R);
203if (R.empty())
204return false;
205
206auto NewSystem = *this;
207NewSystem.addVariableRow(R);
208return !NewSystem.mayHaveSolution();
209}
210