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/ADT/StringExtras.h"
12 #include "llvm/Support/Debug.h"
13 
14 #include <algorithm>
15 #include <string>
16 
17 using namespace llvm;
18 
19 #define DEBUG_TYPE "constraint-system"
20 
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     bool EliminatedInRow = false;
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 
66       SmallVector<int64_t, 8> NR;
67       for (unsigned I = 0; I < NumVariables; I++) {
68         if (I == 1)
69           continue;
70 
71         int64_t M1, M2, N;
72         if (__builtin_mul_overflow(Constraints[UpperR][I],
73                                    ((-1) * Constraints[LowerR][1] / GCD), &M1))
74           return false;
75         if (__builtin_mul_overflow(Constraints[LowerR][I],
76                                    (Constraints[UpperR][1] / GCD), &M2))
77           return false;
78         if (__builtin_add_overflow(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       EliminatedInRow = true;
88     }
89   }
90   Constraints = std::move(NewSystem);
91   GCD = NewGCD;
92 
93   return true;
94 }
95 
96 bool ConstraintSystem::mayHaveSolutionImpl() {
97   while (!Constraints.empty() && Constraints[0].size() > 1) {
98     if (!eliminateUsingFM())
99       return true;
100   }
101 
102   if (Constraints.empty() || Constraints[0].size() > 1)
103     return true;
104 
105   return all_of(Constraints, [](auto &R) { return R[0] >= 0; });
106 }
107 
108 void ConstraintSystem::dump(ArrayRef<std::string> Names) const {
109   if (Constraints.empty())
110     return;
111 
112   for (auto &Row : Constraints) {
113     SmallVector<std::string, 16> Parts;
114     for (unsigned I = 1, S = Row.size(); I < S; ++I) {
115       if (Row[I] == 0)
116         continue;
117       std::string Coefficient = "";
118       if (Row[I] != 1)
119         Coefficient = std::to_string(Row[I]) + " * ";
120       Parts.push_back(Coefficient + Names[I - 1]);
121     }
122     assert(!Parts.empty() && "need to have at least some parts");
123     LLVM_DEBUG(dbgs() << join(Parts, std::string(" + "))
124                       << " <= " << std::to_string(Row[0]) << "\n");
125   }
126 }
127 
128 void ConstraintSystem::dump() const {
129   SmallVector<std::string, 16> Names;
130   for (unsigned i = 1; i < Constraints.back().size(); ++i)
131     Names.push_back("x" + std::to_string(i));
132   LLVM_DEBUG(dbgs() << "---\n");
133   dump(Names);
134 }
135 
136 bool ConstraintSystem::mayHaveSolution() {
137   dump();
138   bool HasSolution = mayHaveSolutionImpl();
139   LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");
140   return HasSolution;
141 }
142