SDBM.h

Go to the documentation of this file.

//===- SDBM.h - MLIR SDBM declaration ---------------------------*- C++ -*-===//
//
// Part of the MLIR Project, under the Apache License v2.0 with LLVM Exceptions.
// See https://llvm.org/LICENSE.txt for license information.
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
//
//===----------------------------------------------------------------------===//
//
// A striped difference-bound matrix (SDBM) is a set in Z^N (or R^N) defined
// as {(x_1, ... x_n) | f(x_1, ... x_n) >= 0} where f is an SDBM expression.
//
//===----------------------------------------------------------------------===//

#ifndef MLIR_DIALECT_SDBM_SDBM_H
#define MLIR_DIALECT_SDBM_SDBM_H

#include "mlir/Support/LLVM.h"
#include "llvm/ADT/DenseMap.h"

namespace mlir {

class MLIRContext;
class SDBMDialect;
class SDBMExpr;
class SDBMTermExpr;

class IntInfty {
public:
  constexpr static int64_t infty = std::numeric_limits<int64_t>::max();

  /*implicit*/ IntInfty(int64_t v) : value(v) {}

  IntInfty &operator=(int64_t v) {
    value = v;
    return *this;
  }

  static IntInfty infinity() { return IntInfty(infty); }

  int64_t getValue() const { return value; }
  explicit operator int64_t() const { return value; }

  bool isFinite() { return value != infty; }

private:
  int64_t value;
};

inline IntInfty operator+(IntInfty lhs, IntInfty rhs) {
  if (!lhs.isFinite() || !rhs.isFinite())
    return IntInfty::infty;

  // Check for overflows, treating the sum of two values adding up to INT_MAX as
  // overflow.  Convert values to unsigned to get an extra bit and avoid the
  // undefined behavior of signed integer overflows.
  assert((lhs.getValue() <= 0 || rhs.getValue() <= 0 ||
          static_cast<uint64_t>(lhs.getValue()) +
                  static_cast<uint64_t>(rhs.getValue()) <
              static_cast<uint64_t>(std::numeric_limits<int64_t>::max())) &&
         "IntInfty overflow");
  // Check for underflows by converting values to unsigned to avoid undefined
  // behavior of signed integers perform the addition (bitwise result is same
  // because numbers are required to be two's complement in C++) and check if
  // the sign bit remains negative.
  assert((lhs.getValue() >= 0 || rhs.getValue() >= 0 ||
          ((static_cast<uint64_t>(lhs.getValue()) +
            static_cast<uint64_t>(rhs.getValue())) >>
           63) == 1) &&
         "IntInfty underflow");

  return lhs.getValue() + rhs.getValue();
}

inline bool operator<(IntInfty lhs, IntInfty rhs) {
  return lhs.getValue() < rhs.getValue();
}

inline bool operator<=(IntInfty lhs, IntInfty rhs) {
  return lhs.getValue() <= rhs.getValue();
}

inline bool operator==(IntInfty lhs, IntInfty rhs) {
  return lhs.getValue() == rhs.getValue();
}

inline bool operator!=(IntInfty lhs, IntInfty rhs) { return !(lhs == rhs); }

class SDBM {
public:
  static SDBM get(ArrayRef<SDBMExpr> inequalities,
                  ArrayRef<SDBMExpr> equalities);

  void getSDBMExpressions(SDBMDialect *dialect,
                          SmallVectorImpl<SDBMExpr> &inequalities,
                          SmallVectorImpl<SDBMExpr> &equalities);

  void print(raw_ostream &os);
  void dump();

  IntInfty operator()(int i, int j) { return at(i, j); }

private:
  IntInfty &at(int i, int j) { return matrix[i * getNumVariables() + j]; }

  void convertDBMElement(unsigned row, unsigned col, SDBMTermExpr rowExpr,
                         SDBMTermExpr colExpr,
                         SmallVectorImpl<SDBMExpr> &inequalities,
                         SmallVectorImpl<SDBMExpr> &equalities);

  void convertDBMDiagonalElement(unsigned pos, SDBMTermExpr expr,
                                 SmallVectorImpl<SDBMExpr> &inequalities);

  unsigned getNumVariables() const {
    return 1 + numDims + numSymbols + numTemporaries;
  }

  unsigned getDimPosition(unsigned position) const { return 1 + position; }

  unsigned getSymbolPosition(unsigned position) const {
    return 1 + numDims + position;
  }

  unsigned getTemporaryPosition(unsigned position) const {
    return 1 + numDims + numSymbols + position;
  }

  unsigned numDims;
  unsigned numSymbols;
  unsigned numTemporaries;

  std::vector<IntInfty> matrix;

  DenseMap<unsigned, SDBMExpr> stripeToPoint;
};

} // namespace mlir

#endif // MLIR_DIALECT_SDBM_SDBM_H