Implement SDBM and conversion between SDBM and lists of SDBMExpr

Implement the storage class for striped difference-bound matrices (SDBM) as a
    container with a difference bounds matrix and a list of stripe expressions.  An
    SDBM defines an integer set.  Provide conversion mechanisms between lists of
    SDBM expressions treated as equalities with zero or less-than-or-equal
    inequalities with zero.

--

PiperOrigin-RevId: 248702871
This commit is contained in:
Alex Zinenko 2019-05-17 05:25:07 -07:00 committed by Mehdi Amini
parent 487b5223a4
commit f06ab26acf
5 changed files with 1140 additions and 70 deletions

206
mlir/include/mlir/IR/SDBM.h Normal file
View File

@ -0,0 +1,206 @@
//===- SDBM.h - MLIR SDBM declaration ---------------------------*- C++ -*-===//
//
// Copyright 2019 The MLIR Authors.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
// =============================================================================
//
// 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 INCLUDE_MLIR_IR_SDBM_H
#define INCLUDE_MLIR_IR_SDBM_H
#include "mlir/Support/LLVM.h"
#include "llvm/ADT/DenseMap.h"
namespace mlir {
class MLIRContext;
class SDBMExpr;
class SDBMPositiveExpr;
/// A utility class for SDBM to represent an integer with potentially infinite
/// positive value. This uses the largest value of int64_t to represent infinity
/// and redefines the arithmetic operators so that the infinity "saturates":
/// inf + x = inf,
/// inf - x = inf.
/// If a sum of two finite values reaches the largest value of int64_t, the
/// behavior of IntInfty is undefined (in practice, it asserts), similarly to
/// regular signed integer overflow.
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); }
/// Striped difference-bound matrix is a representation of an integer set bound
/// by a system of SDBMExprs interpreted as inequalities "expr <= 0".
class SDBM {
public:
/// Obtain an SDBM from a list of SDBM expressions treated as inequalities and
/// equalities with zero.
static SDBM get(ArrayRef<SDBMExpr> inequalities,
ArrayRef<SDBMExpr> equalities);
void getSDBMExpressions(MLIRContext *context,
SmallVectorImpl<SDBMExpr> &inequalities,
SmallVectorImpl<SDBMExpr> &equalities);
void print(llvm::raw_ostream &os);
void dump();
IntInfty operator()(int i, int j) { return at(i, j); }
private:
/// Get the given element of the difference bounds matrix. First index
/// corresponds to the negative term of the difference, second index
/// corresponds to the positive term of the difference.
IntInfty &at(int i, int j) { return matrix[i * getNumVariables() + j]; }
/// Populate `inequalities` and `equalities` based on the values at(row,col)
/// and at(col,row) of the DBM. Depending on the values being finite and
/// being subsumed by stripe expressions, this may or may not add elements to
/// the lists of equalities and inequalities.
void convertDBMElement(MLIRContext *context, unsigned row, unsigned col,
SDBMPositiveExpr rowExpr, SDBMPositiveExpr colExpr,
SmallVectorImpl<SDBMExpr> &inequalities,
SmallVectorImpl<SDBMExpr> &equalities);
/// Populate `inequalities` based on the value at(pos,pos) of the DBM. Only
/// adds new inequalities if the inequality is not trivially true.
void convertDBMDiagonalElement(MLIRContext *context, unsigned pos,
SDBMPositiveExpr expr,
SmallVectorImpl<SDBMExpr> &inequalities);
/// Get the total number of elements in the matrix.
unsigned getNumVariables() const {
return 1 + numDims + numSymbols + numTemporaries;
}
/// Get the position in the matrix that corresponds to the given dimension.
unsigned getDimPosition(unsigned position) const { return 1 + position; }
/// Get the position in the matrix that corresponds to the given symbol.
unsigned getSymbolPosition(unsigned position) const {
return 1 + numDims + position;
}
/// Get the position in the matrix that corresponds to the given temporary.
unsigned getTemporaryPosition(unsigned position) const {
return 1 + numDims + numSymbols + position;
}
/// Number of dimensions in the system,
unsigned numDims;
/// Number of symbols in the system.
unsigned numSymbols;
/// Number of temporary variables in the system.
unsigned numTemporaries;
/// Difference bounds matrix, stored as a linearized row-major vector.
/// Each value in this matrix corresponds to an inequality
///
/// v@col - v@row <= at(row, col)
///
/// where v@col and v@row are the variables that correspond to the linearized
/// position in the matrix. The positions correspond to
///
/// - constant 0 (producing constraints v@col <= X and -v@row <= Y);
/// - SDBM expression dimensions (d0, d1, ...);
/// - SDBM expression symbols (s0, s1, ...);
/// - temporary variables (t0, t1, ...).
///
/// Temporary variables are introduced to represent expressions that are not
/// trivially a difference between two variables. For example, if one side of
/// a difference expression is itself a stripe expression, it will be replaced
/// with a temporary variable assigned equal to this expression.
///
/// Infinite entries in the matrix correspond correspond to an absence of a
/// constraint:
///
/// v@col - v@row <= infinity
///
/// is trivially true. Negated values at symmetric positions in the matrix
/// allow one to couple two inequalities into a single equality.
std::vector<IntInfty> matrix;
/// The mapping between the indices of variables in the DBM and the stripe
/// expressions they are equal to. These expressions are stored as they
/// appeared when constructing an SDBM from a SDBMExprs, in particular no
/// temporaries can appear in these expressions. This removes the need to
/// iteratively substitute definitions of the temporaries in the reverse
/// conversion.
llvm::DenseMap<unsigned, SDBMExpr> stripeToPoint;
};
} // namespace mlir
#endif // INCLUDE_MLIR_IR_SDBM_H

View File

@ -86,6 +86,9 @@ public:
explicit operator bool() const { return impl != nullptr; }
bool operator!() const { return !static_cast<bool>(*this); }
/// Negate the given SDBM expression.
SDBMExpr operator-();
/// Prints the SDBM expression.
void print(raw_ostream &os) const;
void dump() const;
@ -298,9 +301,126 @@ public:
SDBMPositiveExpr getVar() const;
};
/// A visitor class for SDBM expressions. Calls the kind-specific function
/// depending on the kind of expression it visits.
template <typename Derived, typename Result = void> class SDBMVisitor {
public:
/// Visit the given SDBM expression, dispatching to kind-specific functions.
Result visit(SDBMExpr expr) {
auto *derived = static_cast<Derived *>(this);
switch (expr.getKind()) {
case SDBMExprKind::Add:
case SDBMExprKind::Diff:
case SDBMExprKind::DimId:
case SDBMExprKind::SymbolId:
case SDBMExprKind::Neg:
case SDBMExprKind::Stripe:
return derived->visitVarying(expr.cast<SDBMVaryingExpr>());
case SDBMExprKind::Constant:
return derived->visitConstant(expr.cast<SDBMConstantExpr>());
}
llvm_unreachable("unsupported SDBM expression kind");
}
/// Traverse the SDBM expression tree calling `visit` on each node
/// in depth-first preorder.
void walkPreorder(SDBMExpr expr) { return walk</*isPreorder=*/true>(expr); }
/// Traverse the SDBM expression tree calling `visit` on each node in
/// depth-first postorder.
void walkPostorder(SDBMExpr expr) { return walk</*isPreorder=*/false>(expr); }
protected:
/// Default visitors do nothing.
void visitSum(SDBMSumExpr) {}
void visitDiff(SDBMDiffExpr) {}
void visitStripe(SDBMStripeExpr) {}
void visitDim(SDBMDimExpr) {}
void visitSymbol(SDBMSymbolExpr) {}
void visitNeg(SDBMNegExpr) {}
void visitConstant(SDBMConstantExpr) {}
/// Default implementation of visitPositive dispatches to the special
/// functions for stripes and other variables. Concrete visitors can override
/// it.
Result visitPositive(SDBMPositiveExpr expr) {
auto *derived = static_cast<Derived *>(this);
if (expr.getKind() == SDBMExprKind::Stripe)
return derived->visitStripe(expr.cast<SDBMStripeExpr>());
else
return derived->visitInput(expr.cast<SDBMInputExpr>());
}
/// Default implementation of visitInput dispatches to the special
/// functions for dimensions or symbols. Concrete visitors can override it to
/// visit all variables instead.
Result visitInput(SDBMInputExpr expr) {
auto *derived = static_cast<Derived *>(this);
if (expr.getKind() == SDBMExprKind::DimId)
return derived->visitDim(expr.cast<SDBMDimExpr>());
else
return derived->visitSymbol(expr.cast<SDBMSymbolExpr>());
}
/// Default implementation of visitVarying dispatches to the special
/// functions for variables and negations thereof. Concerete visitors can
/// override it to visit all variables and negations instead.
Result visitVarying(SDBMVaryingExpr expr) {
auto *derived = static_cast<Derived *>(this);
if (auto var = expr.dyn_cast<SDBMPositiveExpr>())
return derived->visitPositive(var);
else if (auto neg = expr.dyn_cast<SDBMNegExpr>())
return derived->visitNeg(neg);
else if (auto sum = expr.dyn_cast<SDBMSumExpr>())
return derived->visitSum(sum);
else if (auto diff = expr.dyn_cast<SDBMDiffExpr>())
return derived->visitDiff(diff);
llvm_unreachable("unhandled subtype of varying SDBM expression");
}
template <bool isPreorder> void walk(SDBMExpr expr) {
if (isPreorder)
visit(expr);
if (auto sumExpr = expr.dyn_cast<SDBMSumExpr>()) {
walk<isPreorder>(sumExpr.getLHS());
walk<isPreorder>(sumExpr.getRHS());
} else if (auto diffExpr = expr.dyn_cast<SDBMDiffExpr>()) {
walk<isPreorder>(diffExpr.getLHS());
walk<isPreorder>(diffExpr.getRHS());
} else if (auto stripeExpr = expr.dyn_cast<SDBMStripeExpr>()) {
walk<isPreorder>(stripeExpr.getVar());
walk<isPreorder>(stripeExpr.getStripeFactor());
} else if (auto negExpr = expr.dyn_cast<SDBMNegExpr>()) {
walk<isPreorder>(negExpr.getVar());
}
if (!isPreorder)
visit(expr);
}
};
} // end namespace mlir
namespace llvm {
// SDBMExpr hash just like pointers.
template <> struct DenseMapInfo<mlir::SDBMExpr> {
static mlir::SDBMExpr getEmptyKey() {
auto *pointer = llvm::DenseMapInfo<void *>::getEmptyKey();
return mlir::SDBMExpr(static_cast<mlir::SDBMExpr::ImplType *>(pointer));
}
static mlir::SDBMExpr getTombstoneKey() {
auto *pointer = llvm::DenseMapInfo<void *>::getTombstoneKey();
return mlir::SDBMExpr(static_cast<mlir::SDBMExpr::ImplType *>(pointer));
}
static unsigned getHashValue(mlir::SDBMExpr expr) {
return expr.hash_value();
}
static bool isEqual(mlir::SDBMExpr lhs, mlir::SDBMExpr rhs) {
return lhs == rhs;
}
};
// SDBMVaryingExpr hash just like pointers.
template <> struct DenseMapInfo<mlir::SDBMVaryingExpr> {
static mlir::SDBMVaryingExpr getEmptyKey() {

566
mlir/lib/IR/SDBM.cpp Normal file
View File

@ -0,0 +1,566 @@
//===- SDBM.cpp - MLIR SDBM implementation --------------------------------===//
//
// Copyright 2019 The MLIR Authors.
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
// http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
// =============================================================================
//
// 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.
//
//===----------------------------------------------------------------------===//
#include "mlir/IR/SDBM.h"
#include "mlir/IR/SDBMExpr.h"
#include "llvm/ADT/DenseMap.h"
#include "llvm/ADT/SetVector.h"
#include "llvm/Support/FormatVariadic.h"
#include "llvm/Support/raw_ostream.h"
using namespace mlir;
// Helper function for SDBM construction that collects information necessary to
// start building an SDBM in one sweep. In particular, it records the largest
// position of a dimension in `dim`, that of a symbol in `symbol` as well as
// collects all unique stripe expressions in `stripes`. Uses SetVector to
// ensure these expressions always have the same order.
static void collectSDBMBuildInfo(SDBMExpr expr, int &dim, int &symbol,
llvm::SmallSetVector<SDBMExpr, 8> &stripes) {
struct Visitor : public SDBMVisitor<Visitor> {
void visitDim(SDBMDimExpr dimExpr) {
int p = dimExpr.getPosition();
if (p > maxDimPosition)
maxDimPosition = p;
}
void visitSymbol(SDBMSymbolExpr symbExpr) {
int p = symbExpr.getPosition();
if (p > maxSymbPosition)
maxSymbPosition = p;
}
void visitStripe(SDBMStripeExpr stripeExpr) { stripes.insert(stripeExpr); }
Visitor(llvm::SmallSetVector<SDBMExpr, 8> &stripes) : stripes(stripes) {}
int maxDimPosition = -1;
int maxSymbPosition = -1;
llvm::SmallSetVector<SDBMExpr, 8> &stripes;
};
Visitor visitor(stripes);
visitor.walkPostorder(expr);
dim = std::max(dim, visitor.maxDimPosition);
symbol = std::max(symbol, visitor.maxSymbPosition);
}
namespace {
// Utility class for SDBMBuilder. Represents a value that can be inserted in
// the SDB matrix that corresponds to "v0 - v1 + C <= 0", where v0 and v1 is
// any combination of the positive and negative positions. Since multiple
// variables can be declared equal to the same stripe expression, the
// constraints on this expression must be reflected to all these variables. For
// example, if
// d0 = s0 # 42
// d1 = s0 # 42
// d2 = s1 # 2
// d3 = s1 # 2
// the constraint
// s0 # 42 - s1 # 2 <= C
// should be reflected in the DB matrix as
// d0 - d2 <= C
// d1 - d2 <= C
// d0 - d3 <= C
// d1 - d3 <= C
// since the DB matrix has no knowledge of the transitive equality between d0,
// d1 and s0 # 42 as well as between d2, d3 and s1 # 2. This knowledge can be
// obtained by computing a transitive closure, which is impossible until the
// DBM is actually built.
struct SDBMBuilderResult {
// Positions in the matrix of the variables taken with the "+" sign in the
// difference expression, 0 if it is a constant rather than a variable.
llvm::SmallVector<unsigned, 2> positivePos;
// Positions in the matrix of the variables taken with the "-" sign in the
// difference expression, 0 if it is a constant rather than a variable.
llvm::SmallVector<unsigned, 2> negativePos;
// Constant value in the difference expression.
int64_t value = 0;
};
// Visitor for building an SDBM from SDBM expressions. After traversing an SDBM
// expression, produces an update to the SDB matrix specifying the positions in
// the matrix and the negated value that should be stored. Both the positive
// and the negative positions may be lists of indices in cases where multiple
// variables are equal to the same stripe expression. In such cases, the update
// applies to the cross product of positions because elements involved in the
// update are (transitively) equal and should have the same constraints, but we
// may not have an explicit equality for them.
struct SDBMBuilder : public SDBMVisitor<SDBMBuilder, SDBMBuilderResult> {
public:
// A difference expression produces both the positive and the negative
// coordinate in the matrix, recursively traversing the LHS and the RHS. The
// value is the difference between values obtained from LHS and RHS.
SDBMBuilderResult visitDiff(SDBMDiffExpr diffExpr) {
auto lhs = visit(diffExpr.getLHS());
auto rhs = visit(diffExpr.getRHS());
assert(lhs.negativePos.size() == 1 && lhs.negativePos[0] == 0 &&
"unexpected negative expression in a difference expression");
assert(rhs.negativePos.size() == 1 && lhs.negativePos[0] == 0 &&
"unexpected negative expression in a difference expression");
SDBMBuilderResult result;
result.positivePos = lhs.positivePos;
result.negativePos = rhs.positivePos;
result.value = lhs.value - rhs.value;
return result;
}
// An input expression is always taken with the "+" sign and therefore
// produces a positive coordinate keeping the negative coordinate zero for an
// eventual constant.
SDBMBuilderResult visitInput(SDBMInputExpr expr) {
SDBMBuilderResult r;
r.positivePos.push_back(linearPosition(expr));
r.negativePos.push_back(0);
return r;
}
// A stripe expression is always equal to one or more variables, which may be
// temporaries, and appears with a "+" sign in the SDBM expression tree. Take
// the positions of the corresponding variables as positive coordinates.
SDBMBuilderResult visitStripe(SDBMStripeExpr expr) {
SDBMBuilderResult r;
assert(pointExprToStripe.count(expr));
r.positivePos = pointExprToStripe[expr];
r.negativePos.push_back(0);
return r;
}
// A constant expression has both coordinates at zero.
SDBMBuilderResult visitConstant(SDBMConstantExpr expr) {
SDBMBuilderResult r;
r.positivePos.push_back(0);
r.negativePos.push_back(0);
r.value = expr.getValue();
return r;
}
// A negation expression swaps the positive and the negative coordinates
// and also negates the constant value.
SDBMBuilderResult visitNeg(SDBMNegExpr expr) {
SDBMBuilderResult result = visit(expr.getVar());
std::swap(result.positivePos, result.negativePos);
result.value = -result.value;
return result;
}
// The RHS of a sum expression must be a constant and therefore must have both
// positive and negative coordinates at zero. Take the sum of the values
// between LHS and RHS and keep LHS coordinates.
SDBMBuilderResult visitSum(SDBMSumExpr expr) {
auto lhs = visit(expr.getLHS());
auto rhs = visit(expr.getRHS());
for (auto pos : rhs.negativePos)
assert(pos == 0 && "unexpected variable on the RHS of SDBM sum");
for (auto pos : rhs.positivePos)
assert(pos == 0 && "unexpected variable on the RHS of SDBM sum");
lhs.value += rhs.value;
return lhs;
}
SDBMBuilder(llvm::DenseMap<SDBMExpr, llvm::SmallVector<unsigned, 2>>
&pointExprToStripe,
llvm::function_ref<unsigned(SDBMInputExpr)> callback)
: pointExprToStripe(pointExprToStripe), linearPosition(callback) {}
llvm::DenseMap<SDBMExpr, llvm::SmallVector<unsigned, 2>> &pointExprToStripe;
llvm::function_ref<unsigned(SDBMInputExpr)> linearPosition;
};
} // namespace
SDBM SDBM::get(ArrayRef<SDBMExpr> inequalities, ArrayRef<SDBMExpr> equalities) {
SDBM result;
// TODO(zinenko): consider detecting equalities in the list of inequalities.
// This is potentially expensive and requires to
// - create a list of negated inequalities (may allocate under lock);
// - perform a pairwise comparison of direct and negated inequalities;
// - copy the lists of equalities and inequalities, and move entries between
// them;
// only for the purpose of sparing a temporary variable in cases where an
// implicit equality between a variable and a stripe expression is present in
// the input.
// Do the first sweep over (in)equalities to collect the information necessary
// to allocate the SDB matrix (number of dimensions, symbol and temporary
// variables required for stripe expressions).
llvm::SmallSetVector<SDBMExpr, 8> stripes;
int maxDim = -1;
int maxSymbol = -1;
for (auto expr : inequalities)
collectSDBMBuildInfo(expr, maxDim, maxSymbol, stripes);
for (auto expr : equalities)
collectSDBMBuildInfo(expr, maxDim, maxSymbol, stripes);
// Indexing of dimensions starts with 0, obtain the number of dimensions by
// incrementing the maximal position of the dimension seen in expressions.
result.numDims = maxDim + 1;
result.numSymbols = maxSymbol + 1;
result.numTemporaries = 0;
// Helper function that returns the position of the variable represented by
// an SDBM input expression.
auto linearPosition = [result](SDBMInputExpr expr) {
if (expr.isa<SDBMDimExpr>())
return result.getDimPosition(expr.getPosition());
return result.getSymbolPosition(expr.getPosition());
};
// Check if some stripe expressions are equal to another variable. In
// particular, look for the equalities of the form
// d0 - stripe-expression = 0, or
// stripe-expression - d0 = 0.
// There may be multiple variables that are equal to the same stripe
// expression. Keep track of those in pointExprToStripe.
// There may also be multiple stripe expressions equal to the same variable.
// Introduce a temporary variable for each of those.
llvm::DenseMap<SDBMExpr, llvm::SmallVector<unsigned, 2>> pointExprToStripe;
unsigned numTemporaries = 0;
auto updateStripePointMaps = [&numTemporaries, &result, &pointExprToStripe,
linearPosition](SDBMInputExpr input,
SDBMExpr expr) {
unsigned position = linearPosition(input);
if (result.stripeToPoint.count(position) &&
result.stripeToPoint[position] != expr) {
position = result.getNumVariables() + numTemporaries++;
}
pointExprToStripe[expr].push_back(position);
result.stripeToPoint.insert(std::make_pair(position, expr));
};
for (auto eq : equalities) {
auto diffExpr = eq.dyn_cast<SDBMDiffExpr>();
if (!diffExpr)
continue;
auto lhs = diffExpr.getLHS();
auto rhs = diffExpr.getRHS();
auto lhsInput = lhs.dyn_cast<SDBMInputExpr>();
auto rhsInput = rhs.dyn_cast<SDBMInputExpr>();
if (lhsInput && stripes.count(rhs))
updateStripePointMaps(lhsInput, rhs);
if (rhsInput && stripes.count(lhs))
updateStripePointMaps(rhsInput, lhs);
}
// Assign the remaining stripe expressions to temporary variables. These
// expressions are the ones hat could not be associated with an existing
// variable in the previous step.
for (auto expr : stripes) {
if (pointExprToStripe.count(expr))
continue;
unsigned position = result.getNumVariables() + numTemporaries++;
pointExprToStripe[expr].push_back(position);
result.stripeToPoint.insert(std::make_pair(position, expr));
}
// Create the DBM matrix, initialized to infinity values for the least tight
// possible bound (x - y <= infinity is always true).
result.numTemporaries = numTemporaries;
result.matrix.resize(result.getNumVariables() * result.getNumVariables(),
IntInfty::infinity());
SDBMBuilder builder(pointExprToStripe, linearPosition);
// Only keep the tightest constraint. Since we transform everything into
// less-than-or-equals-to inequalities, keep the smallest constant. For
// example, if we have d0 - d1 <= 42 and d0 - d1 <= 2, we keep the latter.
// Note that the input expressions are in the shape of d0 - d1 + -42 <= 0
// so we negate the value before storing it.
// In case where the positive and the negative positions are equal, the
// corresponding expression has the form d0 - d0 + -42 <= 0. If the constant
// value is positive, the set defined by SDBM is trivially empty. We store
// this value anyway and continue processing to maintain the correspondence
// between the matrix form and the list-of-SDBMExpr form.
// TODO(zinenko): we may want to reconsider this once we have canonicalization
// or simplification in place
auto updateMatrix = [](SDBM &sdbm, const SDBMBuilderResult &r) {
for (auto positivePos : r.positivePos) {
for (auto negativePos : r.negativePos) {
auto &m = sdbm.at(negativePos, positivePos);
m = m < -r.value ? m : -r.value;
}
}
};
// Do the second sweep on (in)equalities, updating the SDB matrix to reflect
// the constraints.
for (auto ineq : inequalities)
updateMatrix(result, builder.visit(ineq));
// An equality f(x) = 0 is represented as a pair of inequalities {f(x) >= 0;
// f(x) <= 0} or, alternatively, {-f(x) <= 0 and f(x) <= 0}.
for (auto eq : equalities) {
updateMatrix(result, builder.visit(eq));
updateMatrix(result, builder.visit(-eq));
}
// Add the inequalities induced by stripe equalities.
// t = x # C => x <= t <= x + C - 1
// which is equivalent to
// {x - t <= 0;
// t - x - (C - 1) <= 0}.
for (const auto &pair : result.stripeToPoint) {
auto stripe = pair.second.cast<SDBMStripeExpr>();
SDBMBuilderResult update = builder.visit(stripe.getVar());
assert(update.negativePos.size() == 1 && update.negativePos[0] == 0 &&
"unexpected negated variable in stripe expression");
assert(update.value == 0 &&
"unexpected non-zero value in stripe expression");
update.negativePos.clear();
update.negativePos.push_back(pair.first);
updateMatrix(result, update);
std::swap(update.negativePos, update.positivePos);
update.value -= stripe.getStripeFactor().getValue() - 1;
updateMatrix(result, update);
}
return result;
}
// Given a row and a column position in the square DBM, insert one equality
// or up to two inequalities that correspond the entries (col, row) and (row,
// col) in the DBM. `rowExpr` and `colExpr` contain the expressions such that
// colExpr - rowExpr <= V where V is the value at (row, col) in the DBM.
// If one of the expressions is derived from another using a stripe operation,
// check if the inequalities induced by the stripe operation subsume the
// inequalities defined in the DBM and if so, elide these inequalities.
void SDBM::convertDBMElement(MLIRContext *context, unsigned row, unsigned col,
SDBMPositiveExpr rowExpr, SDBMPositiveExpr colExpr,
SmallVectorImpl<SDBMExpr> &inequalities,
SmallVectorImpl<SDBMExpr> &equalities) {
auto diffIJValue = at(col, row);
auto diffJIValue = at(row, col);
auto diffIJValueExpr =
SDBMConstantExpr::get(context, -diffIJValue.getValue());
auto diffIJExpr = SDBMDiffExpr::get(rowExpr, colExpr);
// If symmetric entries are equal, so are the corresponding expressions.
if (diffIJValue.isFinite() &&
diffIJValue.getValue() == -diffJIValue.getValue()) {
equalities.push_back(SDBMSumExpr::get(diffIJExpr, diffIJValueExpr));
return;
}
// Given an inequality x0 - x1 <= A, check if x0 is a stripe variable derived
// from x1: x0 = x1 # B. If so, it would imply the constraints
// x1 <= x0 <= x1 + (B - 1) <=> x1 - x0 <= 0 and x0 - x1 <= (B - 1).
// Therefore, if A >= (B - 1), this inequality is subsumed by that implied
// by the stripe equality and thus can be elided.
// Similarly, check if x1 is a stripe variable derived from x0: x1 = x0 # C.
// If so, it would imply the constraints x0 <= x1 <= x0 + (C - 1) <=>
// <=> x0 - x1 <= 0 and x1 - x0 <= (C - 1). Therefore, if A >= 0, this
// inequality can be elided.
//
// Note: x0 and x1 may be a stripe expressions themselves, we rely on stripe
// expressions being stored without temporaries on the RHS and being passed
// into this function as is.
auto canElide = [this](unsigned x0, unsigned x1, SDBMExpr x0Expr,
SDBMExpr x1Expr, int64_t value) {
if (stripeToPoint.count(x0)) {
auto stripe = stripeToPoint[x0].cast<SDBMStripeExpr>();
SDBMPositiveExpr var = stripe.getVar();
if (x1Expr == var && value >= stripe.getStripeFactor().getValue() - 1)
return true;
}
if (stripeToPoint.count(x1)) {
auto stripe = stripeToPoint[x1].cast<SDBMStripeExpr>();
SDBMPositiveExpr var = stripe.getVar();
if (x0Expr == var && value >= 0)
return true;
}
return false;
};
// Check row - col.
if (diffIJValue.isFinite() &&
!canElide(row, col, rowExpr, colExpr, diffIJValue.getValue())) {
inequalities.push_back(SDBMSumExpr::get(diffIJExpr, diffIJValueExpr));
}
// Check col - row.
if (diffJIValue.isFinite() &&
!canElide(col, row, colExpr, rowExpr, diffJIValue.getValue())) {
auto diffJIExpr = SDBMDiffExpr::get(colExpr, rowExpr);
auto diffJIValueExpr =
SDBMConstantExpr::get(context, -diffJIValue.getValue());
inequalities.push_back(SDBMSumExpr::get(diffJIExpr, diffJIValueExpr));
}
}
// The values on the main diagonal correspond to the upper bound on the
// difference between a variable and itself: d0 - d0 <= C, or alternatively
// to -C <= 0. Only construct the inequalities when C is negative, which
// are trivially false but necessary for the returned system of inequalities
// to indicate that the set it defines is empty.
void SDBM::convertDBMDiagonalElement(MLIRContext *context, unsigned pos,
SDBMPositiveExpr expr,
SmallVectorImpl<SDBMExpr> &inequalities) {
auto selfDifference = at(pos, pos);
if (selfDifference.isFinite() && selfDifference < 0) {
auto selfDifferenceExpr = SDBMDiffExpr::get(expr, expr);
auto selfDifferenceValueExpr =
SDBMConstantExpr::get(context, -selfDifference.getValue());
inequalities.push_back(
SDBMSumExpr::get(selfDifferenceExpr, selfDifferenceValueExpr));
}
}
void SDBM::getSDBMExpressions(MLIRContext *context,
SmallVectorImpl<SDBMExpr> &inequalities,
SmallVectorImpl<SDBMExpr> &equalities) {
// Helper function that creates an SDBMInputExpr given the linearized position
// of variable in the DBM.
auto getInput = [context, this](unsigned matrixPos) -> SDBMInputExpr {
if (matrixPos < numDims)
return SDBMDimExpr::get(context, matrixPos);
return SDBMSymbolExpr::get(context, matrixPos - numDims);
};
// The top-left value corresponds to inequality 0 <= C. If C is negative, the
// set defined by SDBM is trivially empty and we add the constraint -C <= 0 to
// the list of inequalities. Otherwise, the constraint is trivially true and
// we ignore it.
auto difference = at(0, 0);
if (difference.isFinite() && difference < 0) {
inequalities.push_back(
SDBMConstantExpr::get(context, -difference.getValue()));
}
// Traverse the segment of the matrix that involves non-temporary variables.
unsigned numTrueVariables = numDims + numSymbols;
for (unsigned i = 0; i < numTrueVariables; ++i) {
// The first row and column represent numerical upper and lower bound on
// each variable. Transform them into inequalities if they are finite.
auto upperBound = at(0, 1 + i);
auto lowerBound = at(1 + i, 0);
auto upperBoundExpr =
SDBMConstantExpr::get(context, -upperBound.getValue());
auto inputExpr = getInput(i);
if (upperBound.isFinite() &&
upperBound.getValue() == -lowerBound.getValue()) {
equalities.push_back(SDBMSumExpr::get(inputExpr, upperBoundExpr));
} else if (upperBound.isFinite()) {
inequalities.push_back(SDBMSumExpr::get(inputExpr, upperBoundExpr));
} else if (lowerBound.isFinite()) {
auto lowerBoundExpr =
SDBMConstantExpr::get(context, -lowerBound.getValue());
inequalities.push_back(
SDBMSumExpr::get(SDBMNegExpr::get(inputExpr), lowerBoundExpr));
}
// Introduce trivially false inequalities if required by diagonal elements.
convertDBMDiagonalElement(context, 1 + i, inputExpr, inequalities);
// Introduce equalities or inequalities between non-temporary variables.
for (unsigned j = 0; j < i; ++j) {
convertDBMElement(context, 1 + i, 1 + j, getInput(i), getInput(j),
inequalities, equalities);
}
}
// Add equalities for stripe expressions that define non-temporary
// variables. Temporary variables will be substituted into their uses and
// should not appear in the resulting equalities.
for (const auto &stripePair : stripeToPoint) {
unsigned position = stripePair.first;
if (position < 1 + numTrueVariables) {
equalities.push_back(SDBMDiffExpr::get(
getInput(position - 1), stripePair.second.cast<SDBMStripeExpr>()));
}
}
// Add equalities / inequalities involving temporaries by replacing the
// temporaries with stripe expressions that define them.
for (unsigned i = 1 + numTrueVariables, e = getNumVariables(); i < e; ++i) {
// Mixed constraints involving one temporary (j) and one non-temporary (i)
// variable.
for (unsigned j = 0; j < numTrueVariables; ++j) {
convertDBMElement(context, i, 1 + j,
stripeToPoint[i].cast<SDBMStripeExpr>(), getInput(j),
inequalities, equalities);
}
// Constraints involving only temporary variables.
for (unsigned j = 1 + numTrueVariables; j < i; ++j) {
convertDBMElement(context, i, j, stripeToPoint[i].cast<SDBMStripeExpr>(),
stripeToPoint[j].cast<SDBMStripeExpr>(), inequalities,
equalities);
}
// Introduce trivially false inequalities if required by diagonal elements.
convertDBMDiagonalElement(
context, i, stripeToPoint[i].cast<SDBMStripeExpr>(), inequalities);
}
}
void SDBM::print(llvm::raw_ostream &os) {
unsigned numVariables = getNumVariables();
// Helper function that prints the name of the variable given its linearized
// position in the DBM.
auto getVarName = [this](unsigned matrixPos) -> std::string {
if (matrixPos == 0)
return "cst";
matrixPos -= 1;
if (matrixPos < numDims)
return llvm::formatv("d{0}", matrixPos);
matrixPos -= numDims;
if (matrixPos < numSymbols)
return llvm::formatv("s{0}", matrixPos);
matrixPos -= numSymbols;
return llvm::formatv("t{0}", matrixPos);
};
// Header row.
os << " cst";
for (unsigned i = 1; i < numVariables; ++i) {
os << llvm::formatv(" {0,4}", getVarName(i));
}
os << '\n';
// Data rows.
for (unsigned i = 0; i < numVariables; ++i) {
os << llvm::formatv("{0,-4}", getVarName(i));
for (unsigned j = 0; j < numVariables; ++j) {
IntInfty value = operator()(i, j);
if (!value.isFinite())
os << " inf";
else
os << llvm::formatv(" {0,4}", value.getValue());
}
os << '\n';
}
// Explanation of temporaries.
for (const auto &pair : stripeToPoint) {
os << getVarName(pair.first) << " = ";
pair.second.print(os);
os << '\n';
}
}
void SDBM::dump() { print(llvm::errs()); }

View File

@ -1,4 +1,4 @@
//===- SDBMExpr.h - MLIR SDBM Expression implementation -------------------===//
//===- SDBMExpr.cpp - MLIR SDBM Expression implementation -----------------===//
//
// Copyright 2019 The MLIR Authors.
//
@ -151,75 +151,6 @@ SDBMExprKind SDBMExpr::getKind() const { return impl->getKind(); }
MLIRContext *SDBMExpr::getContext() const { return impl->getContext(); }
template <typename Derived, typename Result = void> class SDBMVisitor {
public:
/// Visit the given SDBM expression, dispatching to kind-specific functions.
Result visit(SDBMExpr expr) {
auto *derived = static_cast<Derived *>(this);
switch (expr.getKind()) {
case SDBMExprKind::Add:
case SDBMExprKind::Diff:
case SDBMExprKind::DimId:
case SDBMExprKind::SymbolId:
case SDBMExprKind::Neg:
case SDBMExprKind::Stripe:
return derived->visitVarying(expr.cast<SDBMVaryingExpr>());
case SDBMExprKind::Constant:
return derived->visitConstant(expr.cast<SDBMConstantExpr>());
}
llvm_unreachable("Unknown SDBMExpr Kind");
}
protected:
/// Default visitors do nothing.
void visitSum(SDBMSumExpr) {}
void visitDiff(SDBMDiffExpr) {}
void visitStripe(SDBMStripeExpr) {}
void visitDim(SDBMDimExpr) {}
void visitSymbol(SDBMSymbolExpr) {}
void visitNeg(SDBMNegExpr) {}
void visitConstant(SDBMConstantExpr) {}
/// Default implementation of visitPositive dispatches to the special
/// functions for stripes and other variables. Concrete visitors can override
/// it.
Result visitPositive(SDBMPositiveExpr expr) {
auto *derived = static_cast<Derived *>(this);
if (expr.getKind() == SDBMExprKind::Stripe)
return derived->visitStripe(expr.cast<SDBMStripeExpr>());
else
return derived->visitInput(expr.cast<SDBMInputExpr>());
}
/// Default implementation of visitInput dispatches to the special
/// functions for dimensions or symbols. Concrete visitors can override it to
/// visit all variables instead.
Result visitInput(SDBMInputExpr expr) {
auto *derived = static_cast<Derived *>(this);
if (expr.getKind() == SDBMExprKind::DimId)
return derived->visitDim(expr.cast<SDBMDimExpr>());
else
return derived->visitSymbol(expr.cast<SDBMSymbolExpr>());
}
/// Default implementation of visitVarying dispatches to the special
/// functions for variables and negations thereof. Concerete visitors can
/// override it to visit all variables and negations isntead.
Result visitVarying(SDBMVaryingExpr expr) {
auto *derived = static_cast<Derived *>(this);
if (auto var = expr.dyn_cast<SDBMPositiveExpr>())
return derived->visitPositive(var);
else if (auto neg = expr.dyn_cast<SDBMNegExpr>())
return derived->visitNeg(neg);
else if (auto sum = expr.dyn_cast<SDBMSumExpr>())
return derived->visitSum(sum);
else if (auto diff = expr.dyn_cast<SDBMDiffExpr>())
return derived->visitDiff(diff);
llvm_unreachable("unhandled subtype of varying SDBM expression");
}
};
void SDBMExpr::print(raw_ostream &os) const {
struct Printer : public SDBMVisitor<Printer> {
Printer(raw_ostream &ostream) : prn(ostream) {}
@ -258,6 +189,36 @@ void SDBMExpr::dump() const {
llvm::errs() << '\n';
}
namespace {
// Helper class to perform negation of an SDBM expression.
struct SDBMNegator : public SDBMVisitor<SDBMNegator, SDBMExpr> {
// Any positive expression is wrapped into a negation expression.
// -(x) = -x
SDBMExpr visitPositive(SDBMPositiveExpr expr) {
return SDBMNegExpr::get(expr);
}
// A negation expression is unwrapped.
// -(-x) = x
SDBMExpr visitNeg(SDBMNegExpr expr) { return expr.getVar(); }
// The value of the constant is negated.
SDBMExpr visitConstant(SDBMConstantExpr expr) {
return SDBMConstantExpr::get(expr.getContext(), -expr.getValue());
}
// Both terms of the sum are negated recursively.
SDBMExpr visitSum(SDBMSumExpr expr) {
return SDBMSumExpr::get(visit(expr.getLHS()).cast<SDBMVaryingExpr>(),
visit(expr.getRHS()).cast<SDBMConstantExpr>());
}
// Terms of a difference are interchanged.
// -(x - y) = y - x
SDBMExpr visitDiff(SDBMDiffExpr expr) {
return SDBMDiffExpr::get(expr.getRHS(), expr.getLHS());
}
};
} // namespace
SDBMExpr SDBMExpr::operator-() { return SDBMNegator().visit(*this); }
//===----------------------------------------------------------------------===//
// SDBMSumExpr
//===----------------------------------------------------------------------===//

View File

@ -15,11 +15,14 @@
// limitations under the License.
// =============================================================================
#include "mlir/IR/SDBM.h"
#include "mlir/IR/AffineExpr.h"
#include "mlir/IR/MLIRContext.h"
#include "mlir/IR/SDBMExpr.h"
#include "gtest/gtest.h"
#include "llvm/ADT/DenseSet.h"
using namespace mlir;
static MLIRContext *ctx() {
@ -29,6 +32,220 @@ static MLIRContext *ctx() {
namespace {
TEST(SDBM, SingleConstraint) {
// Build an SDBM defined by
//
// d0 - 3 <= 0 <=> d0 <= 3.
//
// cst d0
// cst inf 3
// d0 inf inf
auto cst3 = SDBMConstantExpr::get(ctx(), -3);
auto dim0 = SDBMDimExpr::get(ctx(), 0);
auto expr = SDBMSumExpr::get(dim0, cst3);
auto sdbm = SDBM::get(expr, llvm::None);
EXPECT_EQ(sdbm(0, 1), 3);
}
TEST(SDBM, Equality) {
// Build an SDBM defined by
//
// d0 - d1 - 3 = 0 <=> {d0 - d1 - 3 <= 0 and d0 - d1 - 3 >= 0} <=>
// <=> {d0 - d1 <= 3 and d1 - d0 <= -3}.
//
// cst d0 d1
// cst inf inf inf
// d0 inf inf -3
// d1 inf 3 inf
auto cst3 = SDBMConstantExpr::get(ctx(), -3);
auto dim0 = SDBMDimExpr::get(ctx(), 0);
auto dim1 = SDBMDimExpr::get(ctx(), 1);
auto expr = SDBMSumExpr::get(SDBMDiffExpr::get(dim0, dim1), cst3);
auto sdbm = SDBM::get(llvm::None, expr);
EXPECT_EQ(sdbm(1, 2), -3);
EXPECT_EQ(sdbm(2, 1), 3);
}
TEST(SDBM, TrivialSimplification) {
// Build an SDBM defined by
//
// d0 - 3 <= 0 <=> d0 <= 3
// d0 - 5 <= 0 <=> d0 <= 5
//
// which should get simplifed on construction to only the former.
//
// cst d0
// cst inf 3
// d0 inf inf
auto cst5 = SDBMConstantExpr::get(ctx(), -5);
auto cst3 = SDBMConstantExpr::get(ctx(), -3);
auto dim0 = SDBMDimExpr::get(ctx(), 0);
auto expr5 = SDBMSumExpr::get(dim0, cst5);
auto expr3 = SDBMSumExpr::get(dim0, cst3);
auto sdbm = SDBM::get({expr3, expr5}, llvm::None);
EXPECT_EQ(sdbm(0, 1), 3);
}
TEST(SDBM, StripeInducedIneqs) {
// Build an SDBM defined by d1 = d0 # 3, which induces the constraints
//
// d1 - d0 <= 0
// d0 - d1 <= 3 - 1 = 2
//
// cst d0 d1
// cst inf inf inf
// d0 inf inf 2
// d1 inf 0 0
auto dim0 = SDBMDimExpr::get(ctx(), 0);
auto dim1 = SDBMDimExpr::get(ctx(), 1);
auto cst3 = SDBMConstantExpr::get(ctx(), 3);
auto stripe = SDBMStripeExpr::get(dim0, cst3);
auto expr = SDBMDiffExpr::get(dim1, stripe);
auto sdbm = SDBM::get(llvm::None, expr);
EXPECT_EQ(sdbm(1, 2), 2);
EXPECT_EQ(sdbm(2, 1), 0);
}
TEST(SDBM, StripeTemporaries) {
// Build an SDBM defined by d0 # 3 <= 0, which creates a temporary
// t0 = d0 # 3 leading to a constraint t0 <= 0 and the stripe-induced
// constraints
//
// t0 - d0 <= 0
// d0 - t0 <= 3 - 1 = 2
//
// cst d0 t0
// cst inf inf 0
// d0 inf inf 2
// t0 inf 0 inf
auto dim0 = SDBMDimExpr::get(ctx(), 0);
auto cst3 = SDBMConstantExpr::get(ctx(), 3);
auto stripe = SDBMStripeExpr::get(dim0, cst3);
auto sdbm = SDBM::get(stripe, llvm::None);
EXPECT_EQ(sdbm(0, 2), 0);
EXPECT_EQ(sdbm(1, 2), 2);
EXPECT_EQ(sdbm(2, 1), 0);
}
TEST(SDBM, RoundTripEqs) {
// Build and SDBM defined by
//
// d0 = s0 # 3 # 5
// s0 # 3 # 5 - d1 + 42 = 0
//
// and perform a double round-trip between the "list of equalities" and SDBM
// representation. After the first round-trip, the equalities may be
// different due to simplification or equivalent substitutions (e.g., the
// second equality may become d0 - d1 + 42 = 0). However, there should not
// be any further simplification after the second round-trip,
auto cst3 = SDBMConstantExpr::get(ctx(), 3);
auto cst5 = SDBMConstantExpr::get(ctx(), 5);
auto dim0 = SDBMSymbolExpr::get(ctx(), 0);
auto stripe = SDBMStripeExpr::get(SDBMStripeExpr::get(dim0, cst3), cst5);
auto foo = SDBMDiffExpr::get(stripe, SDBMDimExpr::get(ctx(), 0));
auto bar =
SDBMSumExpr::get(SDBMDiffExpr::get(stripe, SDBMDimExpr::get(ctx(), 1)),
SDBMConstantExpr::get(ctx(), 42));
// Build the SDBM from a pair of equalities and extract back the lists of
// inequalities and equalities. Check that all equalities are properly
// detected and none of them decayed into inequalities.
auto sdbm = SDBM::get(llvm::None, {foo, bar});
SmallVector<SDBMExpr, 4> eqs, ineqs;
sdbm.getSDBMExpressions(ctx(), ineqs, eqs);
ASSERT_TRUE(ineqs.empty());
// Do the second round-trip.
auto sdbm2 = SDBM::get(llvm::None, eqs);
SmallVector<SDBMExpr, 4> eqs2, ineqs2;
sdbm2.getSDBMExpressions(ctx(), ineqs2, eqs2);
ASSERT_EQ(eqs.size(), eqs2.size());
// Convert that the sets of equalities are equal, their order is not relevant.
llvm::DenseSet<SDBMExpr> eqSet, eq2Set;
eqSet.insert(eqs.begin(), eqs.end());
eq2Set.insert(eqs2.begin(), eqs2.end());
EXPECT_EQ(eqSet, eq2Set);
}
TEST(SDBM, StripeTightening) {
// Build an SDBM defined by
//
// d0 = s0 # 3 # 5
// s0 # 3 # 5 - d1 + 42 = 0
// d0 - s0 # 3 <= 2
//
// where the last inequality is tighter than that induced by the first stripe
// equality (d0 - s0 # 3 <= 5 - 1 = 4). Check that the conversion from SDBM
// back to the lists of constraints conserves both the stripe equality and the
// tighter inequality.
auto cst3 = SDBMConstantExpr::get(ctx(), 3);
auto cst5 = SDBMConstantExpr::get(ctx(), 5);
auto dim0 = SDBMSymbolExpr::get(ctx(), 0);
auto stripe = SDBMStripeExpr::get(SDBMStripeExpr::get(dim0, cst3), cst5);
auto foo = SDBMDiffExpr::get(stripe, SDBMDimExpr::get(ctx(), 0));
auto bar = SDBMSumExpr::get(
SDBMDiffExpr::get(SDBMDimExpr::get(ctx(), 0), SDBMDimExpr::get(ctx(), 1)),
SDBMConstantExpr::get(ctx(), 42));
auto tight =
SDBMSumExpr::get(SDBMDiffExpr::get(SDBMDimExpr::get(ctx(), 0),
SDBMStripeExpr::get(dim0, cst3)),
SDBMConstantExpr::get(ctx(), -2));
auto sdbm = SDBM::get({tight}, {foo, bar});
SmallVector<SDBMExpr, 4> eqs, ineqs;
sdbm.getSDBMExpressions(ctx(), ineqs, eqs);
ASSERT_EQ(ineqs.size(), 1u);
EXPECT_EQ(ineqs[0], tight);
EXPECT_EQ(eqs.size(), 2u);
}
TEST(SDBM, StripeTransitive) {
// Build an SDBM defined by
//
// d0 = d1 # 3
// d0 = d2 # 7
//
// where the same dimension is declared equal to two stripe expressions over
// different variables. This is practically handled by introducing a
// temporary variable for the second stripe expression and adding an equality
// constraint between this variable and the original dimension variable.
//
// cst d0 d1 d2 t0
// cst inf inf inf inf inf
// d0 inf 0 0 inf 0
// d1 inf 2 inf inf inf
// d2 inf inf inf inf 6
// t0 inf 0 inf 0 inf
auto cst3 = SDBMConstantExpr::get(ctx(), 3);
auto cst7 = SDBMConstantExpr::get(ctx(), 7);
auto dim0 = SDBMDimExpr::get(ctx(), 0);
auto dim1 = SDBMDimExpr::get(ctx(), 1);
auto dim2 = SDBMDimExpr::get(ctx(), 2);
auto stripe1 = SDBMStripeExpr::get(dim1, cst3);
auto stripe2 = SDBMStripeExpr::get(dim2, cst7);
auto diff1 = SDBMDiffExpr::get(stripe1, dim0);
auto diff2 = SDBMDiffExpr::get(stripe2, dim0);
auto sdbm = SDBM::get(llvm::None, {diff1, diff2});
// Induced by d0 = d1 # 3.
EXPECT_EQ(sdbm(1, 2), 0);
EXPECT_EQ(sdbm(2, 1), 2);
// Equality d0 = t0.
EXPECT_EQ(sdbm(1, 4), 0);
EXPECT_EQ(sdbm(4, 1), 0);
// Induced by t0 = d2 # 7.
EXPECT_EQ(sdbm(3, 4), 6);
EXPECT_EQ(sdbm(4, 3), 0);
}
TEST(SDBMExpr, Constant) {
// We can create consants and query them.
auto expr = SDBMConstantExpr::get(ctx(), 42);