[MLIR] Simplex: fix a bug when rolling back a Simplex with no solutions

[arjunp]

Summary

Previously, when adding a constraint to a Simplex that is already marked
as having no solutions (marked empty), the Simplex would be marked empty again,
and a second UnmarkEmpty entry would be pushed to the undo log. When rolling
back, Simplex should be unmarked empty only after rolling back past the
creation of the first constraint that made it empty.

[arjunp]

Note: the failing test will pass once the patch D114614 is landed.

[Groverkss]

LGTM. Just some minor comments.

mlir/lib/Analysis/Presburger/Simplex.cpp

358

mlir/unittests/Analysis/Presburger/SimplexTest.cpp

16–20

I think this doc comment should be updated to reflect the new check.

33

Could you add the comment // (u - v) <= -3 just for consistency?

[arjunp]

Address Kunwar's comments.

[arjunp]

Rebase on the landed parent patch. This should fix the build.

mlir/lib/Analysis/Presburger/Simplex.cpp

void Simplex::swapColumns(unsigned i, unsigned j) {
   if (i == j)
     return;
   tableau.swapColumns(i, j);
   std::swap(colUnknown[i], colUnknown[j]);
   unknownFromColumn(i).pos = i;
   unknownFromColumn(j).pos = j;
 }
 
 /// Mark this tableau empty and push an entry to the undo stack.
 void Simplex::markEmpty() {
+  // If the set is already empty, then we shouldn't add another UnmarkEmpty log
+  // entry, since in that case the Simplex will be erroneously marked as
+  // non-empty when rolling back past this point.
+  if (empty)
+    return;
   undoLog.push_back(UndoLogEntry::UnmarkEmpty);
   empty = true;
 }
 
 /// Add an inequality to the tableau. If coeffs is c_0, c_1, ... c_n, where n
 /// is the current number of variables, then the corresponding inequality is
 /// c_n + c_0*x_0 + c_1*x_1 + ... + c_{n-1}*x_{n-1} >= 0.
 ///

mlir/unittests/Analysis/Presburger/SimplexTest.cpp

 //===- SimplexTest.cpp - Tests for Simplex --------------------------------===//
 //
 // Part of the LLVM 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
 //
 //===----------------------------------------------------------------------===//
 
 #include "mlir/Analysis/Presburger/Simplex.h"
 
 #include <gmock/gmock.h>
 #include <gtest/gtest.h>
 
 namespace mlir {
 
 /// Take a snapshot, add constraints making the set empty, and rollback.
-/// The set should not be empty after rolling back.
+/// The set should not be empty after rolling back. We add additional
+/// constraints after the set is already empty and roll back the addition
+/// of these. The set should be marked non-empty only once we rollback
+/// past the addition of the first constraint that made it empty.
 TEST(SimplexTest, emptyRollback) {
   Simplex simplex(2);
   // (u - v) >= 0
   simplex.addInequality({1, -1, 0});
-  EXPECT_FALSE(simplex.isEmpty());
+  ASSERT_FALSE(simplex.isEmpty());
 
   unsigned snapshot = simplex.getSnapshot();
   // (u - v) <= -1
   simplex.addInequality({-1, 1, -1});
-  EXPECT_TRUE(simplex.isEmpty());
+  ASSERT_TRUE(simplex.isEmpty());
+
+  unsigned snapshot2 = simplex.getSnapshot();
+  // (u - v) <= -3
+  simplex.addInequality({-1, 1, -3});
+  ASSERT_TRUE(simplex.isEmpty());
+
+  simplex.rollback(snapshot2);
+  ASSERT_TRUE(simplex.isEmpty());
+
   simplex.rollback(snapshot);
-  EXPECT_FALSE(simplex.isEmpty());
+  ASSERT_FALSE(simplex.isEmpty());
 }
 
 /// Check that the set gets marked as empty when we add contradictory
 /// constraints.
 TEST(SimplexTest, addEquality_separate) {
   Simplex simplex(1);
   simplex.addInequality({1, -1}); // x >= 1.
   ASSERT_FALSE(simplex.isEmpty());