SDBM: fix the order of variables in the stripe-induced inequalities

The initial implementation of SDBM mistakenly swapped the order of variables in
the inequalities induced by a stripe equality: y = x # B actually implies
y - x <= 0 and x - y <= B - 1 rather than x - y <= 0 and y - x <= B - 1 as
implemented.  Textual comments in the test files were correct but did not
correspond to the emitted IR.  Round-tripping between SDBM and expression lists
was not affected because the wrong order was used in both directions of the
conversion.  Use the correct order.

PiperOrigin-RevId: 251252980
This commit is contained in:
Alex Zinenko
2019-06-03 10:00:16 -07:00
committed by Mehdi Amini
parent c263ae9104
commit f5e736c448
2 changed files with 54 additions and 29 deletions

View File

@@ -271,7 +271,7 @@ SDBM SDBM::get(ArrayRef<SDBMExpr> inequalities, ArrayRef<SDBMExpr> equalities) {
}
// Assign the remaining stripe expressions to temporary variables. These
// expressions are the ones hat could not be associated with an existing
// expressions are the ones that could not be associated with an existing
// variable in the previous step.
for (auto expr : stripes) {
if (pointExprToStripe.count(expr))
@@ -323,10 +323,10 @@ SDBM SDBM::get(ArrayRef<SDBMExpr> inequalities, ArrayRef<SDBMExpr> equalities) {
}
// Add the inequalities induced by stripe equalities.
// t = x # C => x <= t <= x + C - 1
// t = x # C => t <= x <= t + C - 1
// which is equivalent to
// {x - t <= 0;
// t - x - (C - 1) <= 0}.
// {t - x <= 0;
// x - t - (C - 1) <= 0}.
for (const auto &pair : result.stripeToPoint) {
auto stripe = pair.second.cast<SDBMStripeExpr>();
SDBMBuilderResult update = builder.visit(stripe.getVar());
@@ -336,10 +336,11 @@ SDBM SDBM::get(ArrayRef<SDBMExpr> inequalities, ArrayRef<SDBMExpr> equalities) {
"unexpected non-zero value in stripe expression");
update.negativePos.clear();
update.negativePos.push_back(pair.first);
update.value = -(stripe.getStripeFactor().getValue() - 1);
updateMatrix(result, update);
std::swap(update.negativePos, update.positivePos);
update.value -= stripe.getStripeFactor().getValue() - 1;
update.value = 0;
updateMatrix(result, update);
}
@@ -363,7 +364,7 @@ void SDBM::convertDBMElement(unsigned row, unsigned col,
auto diffIJValue = at(col, row);
auto diffJIValue = at(row, col);
// If symmetric entries are equal, so are the corresponding expressions.
// If symmetric entries are opposite, the corresponding expressions are equal.
if (diffIJValue.isFinite() &&
diffIJValue.getValue() == -diffJIValue.getValue()) {
equalities.push_back(rowExpr - colExpr - diffIJValue.getValue());
@@ -372,12 +373,12 @@ void SDBM::convertDBMElement(unsigned row, unsigned col,
// 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
// x0 <= x1 <= x0 + (B - 1) <=> x0 - x1 <= 0 and x1 - x0 <= (B - 1).
// Therefore, if A >= 0, 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
// If so, it would imply the constraints x1 <= x0 <= x1 + (C - 1) <=>
// <=> x1 - x0 <= 0 and x0 - x1 <= (C - 1). Therefore, if A >= (C - 1), this
// inequality can be elided.
//
// Note: x0 and x1 may be a stripe expressions themselves, we rely on stripe
@@ -388,13 +389,13 @@ void SDBM::convertDBMElement(unsigned row, unsigned col,
if (stripeToPoint.count(x0)) {
auto stripe = stripeToPoint[x0].cast<SDBMStripeExpr>();
SDBMPositiveExpr var = stripe.getVar();
if (x1Expr == var && value >= stripe.getStripeFactor().getValue() - 1)
if (x1Expr == var && value >= 0)
return true;
}
if (stripeToPoint.count(x1)) {
auto stripe = stripeToPoint[x1].cast<SDBMStripeExpr>();
SDBMPositiveExpr var = stripe.getVar();
if (x0Expr == var && value >= 0)
if (x0Expr == var && value >= stripe.getStripeFactor().getValue() - 1)
return true;
}
return false;

View File

@@ -101,8 +101,8 @@ TEST_FUNC(SDBM_StripeInducedIneqs) {
// CHECK: cst d0 d1
// CHECK-NEXT: cst inf inf inf
// CHECK-NEXT: d0 inf inf 2
// CHECK-NEXT: d1 inf 0 0
// CHECK-NEXT: d0 inf inf 0
// CHECK-NEXT: d1 inf 2 0
// CHECK-NEXT: d1 = d0 # 3
sdbm.print(llvm::outs());
}
@@ -118,36 +118,60 @@ TEST_FUNC(SDBM_StripeTemporaries) {
// CHECK: cst d0 t0
// CHECK-NEXT: cst inf inf 0
// CHECK-NEXT: d0 inf inf 2
// CHECK-NEXT: t0 inf 0 inf
// CHECK-NEXT: d0 inf inf 0
// CHECK-NEXT: t0 inf 2 inf
// CHECK-NEXT: t0 = d0 # 3
sdbm.print(llvm::outs());
}
TEST_FUNC(SDBM_ElideInducedInequalities) {
// Build an SDBM defined by a single stripe equality d0 = s0 # 3 and make sure
// the induced inequalities are not present after converting the SDBM back
// into lists of expressions.
auto sdbm = SDBM::get(llvm::None, {dim(0) - stripe(symb(0), 3)});
SmallVector<SDBMExpr, 4> eqs, ineqs;
sdbm.getSDBMExpressions(dialect(), ineqs, eqs);
// CHECK-EMPTY:
for (auto ineq : ineqs)
ineq.print(llvm::outs() << '\n');
llvm::outs() << "\n";
// CHECK: d0 - s0 # 3
// CHECK-EMPTY:
for (auto eq : eqs)
eq.print(llvm::outs() << '\n');
llvm::outs() << "\n\n";
}
TEST_FUNC(SDBM_StripeTightening) {
// Build an SDBM defined by
//
// d0 = s0 # 3 # 5
// s0 # 3 # 5 - d1 + 42 = 0
// d0 - s0 # 3 <= 2
// s0 # 3 - d0 <= 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
// equality (s0 # 3 - d0 <= 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 s = stripe(stripe(symb(0), 3), 5);
auto tight = dim(0) - stripe(symb(0), 3) - 2;
auto tight = stripe(symb(0), 3) - dim(0) - 2;
auto sdbm = SDBM::get({tight}, {s - dim(0), s - dim(1) + 42});
SmallVector<SDBMExpr, 4> eqs, ineqs;
sdbm.getSDBMExpressions(dialect(), ineqs, eqs);
// CHECK-DAG: d0 - s0 # 3 + -2
// CHECK-DAG: d1 - d0 + -42
// CHEKC-DAG: d0 - s0 # 3 # 5
// CHECK: s0 # 3 - d0 + -2
// CHECK-EMPTY:
for (auto ineq : ineqs)
ineq.print(llvm::outs());
ineq.print(llvm::outs() << '\n');
llvm::outs() << "\n";
// CHECK-DAG: d1 - d0 + -42
// CHECK-DAG: d0 - s0 # 3 # 5
for (auto eq : eqs)
eq.print(llvm::outs());
eq.print(llvm::outs() << '\n');
llvm::outs() << "\n\n";
}
TEST_FUNC(SDBM_StripeTransitive) {
@@ -165,10 +189,10 @@ TEST_FUNC(SDBM_StripeTransitive) {
// CHECK: cst d0 d1 d2 t0
// CHECK-NEXT: cst inf inf inf inf inf
// CHECK-NEXT: d0 inf 0 0 inf 0
// CHECK-NEXT: d1 inf 2 inf inf inf
// CHECK-NEXT: d2 inf inf inf inf 6
// CHECK-NEXT: t0 inf 0 inf 0 inf
// CHECK-NEXT: d0 inf 0 2 inf 0
// CHECK-NEXT: d1 inf 0 inf inf inf
// CHECK-NEXT: d2 inf inf inf inf 0
// CHECK-NEXT: t0 inf 0 inf 6 inf
// CHECK-NEXT: t0 = d2 # 7
// CHECK-NEXT: d0 = d1 # 3
sdbm.print(llvm::outs());