LLVM  14.0.0git
ConstraintSystem.cpp
Go to the documentation of this file.
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 
10 #include "llvm/ADT/SmallVector.h"
12 #include "llvm/ADT/StringExtras.h"
13 #include "llvm/Support/Debug.h"
14 
15 #include <algorithm>
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  unsigned NumVariables = Constraints[0].size();
33 
34  unsigned NumConstraints = Constraints.size();
35  uint32_t NewGCD = 1;
36  // FIXME do not use copy
37  for (unsigned R1 = 0; R1 < NumConstraints; R1++) {
38  if (Constraints[R1][1] == 0) {
40  NR.push_back(Constraints[R1][0]);
41  for (unsigned i = 2; i < NumVariables; i++) {
42  NR.push_back(Constraints[R1][i]);
43  }
44  NewSystem.push_back(std::move(NR));
45  continue;
46  }
47 
48  // FIXME do not use copy
49  for (unsigned R2 = R1 + 1; R2 < NumConstraints; R2++) {
50  if (R1 == R2)
51  continue;
52 
53  // FIXME: can we do better than just dropping things here?
54  if (Constraints[R2][1] == 0)
55  continue;
56 
57  if ((Constraints[R1][1] < 0 && Constraints[R2][1] < 0) ||
58  (Constraints[R1][1] > 0 && Constraints[R2][1] > 0))
59  continue;
60 
61  unsigned LowerR = R1;
62  unsigned UpperR = R2;
63  if (Constraints[UpperR][1] < 0)
64  std::swap(LowerR, UpperR);
65 
67  for (unsigned I = 0; I < NumVariables; I++) {
68  if (I == 1)
69  continue;
70 
71  int64_t M1, M2, N;
72  if (MulOverflow(Constraints[UpperR][I],
73  ((-1) * Constraints[LowerR][1] / GCD), M1))
74  return false;
75  if (MulOverflow(Constraints[LowerR][I],
76  (Constraints[UpperR][1] / GCD), M2))
77  return false;
78  if (AddOverflow(M1, M2, N))
79  return false;
80  NR.push_back(N);
81 
82  NewGCD = APIntOps::GreatestCommonDivisor({32, (uint32_t)NR.back()},
83  {32, NewGCD})
84  .getZExtValue();
85  }
86  NewSystem.push_back(std::move(NR));
87  // Give up if the new system gets too big.
88  if (NewSystem.size() > 500)
89  return false;
90  }
91  }
92  Constraints = std::move(NewSystem);
93  GCD = NewGCD;
94 
95  return true;
96 }
97 
98 bool ConstraintSystem::mayHaveSolutionImpl() {
99  while (!Constraints.empty() && Constraints[0].size() > 1) {
100  if (!eliminateUsingFM())
101  return true;
102  }
103 
104  if (Constraints.empty() || Constraints[0].size() > 1)
105  return true;
106 
107  return all_of(Constraints, [](auto &R) { return R[0] >= 0; });
108 }
109 
110 void ConstraintSystem::dump(ArrayRef<std::string> Names) const {
111  if (Constraints.empty())
112  return;
113 
114  for (auto &Row : Constraints) {
116  for (unsigned I = 1, S = Row.size(); I < S; ++I) {
117  if (Row[I] == 0)
118  continue;
119  std::string Coefficient;
120  if (Row[I] != 1)
121  Coefficient = std::to_string(Row[I]) + " * ";
122  Parts.push_back(Coefficient + Names[I - 1]);
123  }
124  assert(!Parts.empty() && "need to have at least some parts");
125  LLVM_DEBUG(dbgs() << join(Parts, std::string(" + "))
126  << " <= " << std::to_string(Row[0]) << "\n");
127  }
128 }
129 
130 void ConstraintSystem::dump() const {
132  for (unsigned i = 1; i < Constraints.back().size(); ++i)
133  Names.push_back("x" + std::to_string(i));
134  LLVM_DEBUG(dbgs() << "---\n");
135  dump(Names);
136 }
137 
139  LLVM_DEBUG(dump());
140  bool HasSolution = mayHaveSolutionImpl();
141  LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");
142  return HasSolution;
143 }
144 
146  // If all variable coefficients are 0, we have 'C >= 0'. If the constant is >=
147  // 0, R is always true, regardless of the system.
148  if (all_of(makeArrayRef(R).drop_front(1), [](int64_t C) { return C == 0; }))
149  return R[0] >= 0;
150 
151  // If there is no solution with the negation of R added to the system, the
152  // condition must hold based on the existing constraints.
154 
155  auto NewSystem = *this;
156  NewSystem.addVariableRow(R);
157  return !NewSystem.mayHaveSolution();
158 }
i
i
Definition: README.txt:29
MathExtras.h
llvm
---------------------— PointerInfo ------------------------------------—
Definition: AllocatorList.h:23
llvm::SmallVector
This is a 'vector' (really, a variable-sized array), optimized for the case when the array is small.
Definition: SmallVector.h:1168
llvm::ConstraintSystem::isConditionImplied
bool isConditionImplied(SmallVector< int64_t, 8 > R)
Definition: ConstraintSystem.cpp:145
LLVM_DEBUG
#define LLVM_DEBUG(X)
Definition: Debug.h:101
llvm::RISCVFenceField::R
@ R
Definition: RISCVBaseInfo.h:193
llvm::dbgs
raw_ostream & dbgs()
dbgs() - This returns a reference to a raw_ostream for debugging messages.
Definition: Debug.cpp:163
R2
#define R2(n)
llvm::all_of
bool all_of(R &&range, UnaryPredicate P)
Provide wrappers to std::all_of which take ranges instead of having to pass begin/end explicitly.
Definition: STLExtras.h:1547
C
(vector float) vec_cmpeq(*A, *B) C
Definition: README_ALTIVEC.txt:86
llvm::AddOverflow
std::enable_if_t< std::is_signed< T >::value, T > AddOverflow(T X, T Y, T &Result)
Add two signed integers, computing the two's complement truncated result, returning true if overflow ...
Definition: MathExtras.h:884
llvm::ConstraintSystem::size
unsigned size() const
Returns the number of rows in the constraint system.
Definition: ConstraintSystem.h:81
ConstraintSystem.h
llvm::ConstraintSystem::negate
static SmallVector< int64_t, 8 > negate(SmallVector< int64_t, 8 > R)
Definition: ConstraintSystem.h:67
move
compiles ldr LCPI1_0 ldr ldr mov lsr tst moveq r1 ldr LCPI1_1 and r0 bx lr It would be better to do something like to fold the shift into the conditional move
Definition: README.txt:546
I
#define I(x, y, z)
Definition: MD5.cpp:59
StringExtras.h
assert
assert(ImpDefSCC.getReg()==AMDGPU::SCC &&ImpDefSCC.isDef())
std::swap
void swap(llvm::BitVector &LHS, llvm::BitVector &RHS)
Implement std::swap in terms of BitVector swap.
Definition: BitVector.h:840
llvm::ArrayRef< std::string >
uint32_t
S
add sub stmia L5 ldr r0 bl L_printf $stub Instead of a and a wouldn t it be better to do three moves *Return an aggregate type is even return S
Definition: README.txt:210
llvm::MulOverflow
std::enable_if_t< std::is_signed< T >::value, T > MulOverflow(T X, T Y, T &Result)
Multiply two signed integers, computing the two's complement truncated result, returning true if an o...
Definition: MathExtras.h:936
llvm::makeArrayRef
ArrayRef< T > makeArrayRef(const T &OneElt)
Construct an ArrayRef from a single element.
Definition: ArrayRef.h:476
SmallVector.h
llvm::APIntOps::GreatestCommonDivisor
APInt GreatestCommonDivisor(APInt A, APInt B)
Compute GCD of two unsigned APInt values.
Definition: APInt.cpp:742
N
#define N
llvm::to_string
std::string to_string(const T &Value)
Definition: ScopedPrinter.h:63
llvm::ConstraintSystem::mayHaveSolution
bool mayHaveSolution()
Returns true if there may be a solution for the constraints in the system.
Definition: ConstraintSystem.cpp:138
llvm::M1
unsigned M1(unsigned Val)
Definition: VE.h:372
Debug.h