Home | History | Annotate | Line # | Download | only in Analysis 
      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 <algorithm>
     16 #include <string>
     17 
     18 using namespace llvm;
     19 
     20 #define DEBUG_TYPE "constraint-system"
     21 
     22 bool ConstraintSystem::eliminateUsingFM() {
     23   // Implementation of FourierMotzkin 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();
     32   SmallVector<SmallVector<int64_t, 8>, 4> NewSystem;
     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) {
     39       SmallVector<int64_t, 8> NR;
     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 
     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 (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) {
    115     SmallVector<std::string, 16> Parts;
    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 {
    131   SmallVector<std::string, 16> Names;
    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 
    138 bool ConstraintSystem::mayHaveSolution() {
    139   LLVM_DEBUG(dump());
    140   bool HasSolution = mayHaveSolutionImpl();
    141   LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");
    142   return HasSolution;
    143 }
    144 
    145 bool ConstraintSystem::isConditionImplied(SmallVector<int64_t, 8> R) {
    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.
    153   R = ConstraintSystem::negate(R);
    154 
    155   auto NewSystem = *this;
    156   NewSystem.addVariableRow(R);
    157   return !NewSystem.mayHaveSolution();
    158 }
    159