llvm-project

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 (const Entry &E : Row) {
167
      if (E.Id >= NumVariables)
168
        break;
169
      if (E.Id == 0)
170
        continue;
171
      std::string Coefficient;
172
      if (E.Coefficient != 1)
173
        Coefficient = std::to_string(E.Coefficient) + " * ";
174
      Parts.push_back(Coefficient + Names[E.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