This is an archive of the discontinued LLVM Phabricator instance.

[MLIR] FlatAffineConstraints::isIntegerEmpty: fix bug in computation of duals
ClosedPublic

Authored by arjunp on Nov 12 2021, 1:38 PM.

Details

Summary

The method that was previously used for computing dual variables was incorrect.
This was used in the integer emptiness check algorithm, where this bug could lead to much longer running times. (Due to the way it is used, this never results in an incorrect emptiness check result.)

This patch fixes the dual computation and adds some additional asserts that catch this bug, along with regression test cases that trigger the asserts when the incorrect dual computation is used.

Diff Detail

Event Timeline

arjunp created this revision.Nov 12 2021, 1:38 PM
arjunp requested review of this revision.Nov 12 2021, 1:38 PM
Groverkss added inline comments.Nov 12 2021, 1:50 PM
mlir/lib/Analysis/Presburger/Simplex.cpp
825–827
1013–1028

It's not obvious what this macro does. Could you write a comment about what it does?

Groverkss added inline comments.Nov 12 2021, 1:58 PM
mlir/unittests/Analysis/AffineStructuresTest.cpp
347–363

It would be nice to have comments for each equality/inequality as in other tests to keep consistency. Something like:

checkSample(true, makeFACFromConstraints(3,
                                         {
                                              {3, 3, 0, 3}, // 3x + 3y +3 >= 0
                                              {-4, -8, -1, 4}, // -4x -8y -z + 4 >= 0
                                              {-7, -4, 1, 1}, // ...
                                              {2, -7, -8, -7}, // ...
                                              {9, 8, -9, -7} // ...
                                          },
                                         {}));

Amazing. Congratulations that you identified this issue!

bondhugula added inline comments.Nov 13 2021, 7:28 PM
mlir/lib/Analysis/Presburger/Simplex.cpp
1013

Why is this under NDEBUG? The code comments completely indicate otherwise.

arjunp added inline comments.Nov 13 2021, 7:42 PM
mlir/lib/Analysis/Presburger/Simplex.cpp
1013

This section is just for doing the assert on line 101. To do the assert it's necessary to set up the correct basis. The basis is reverted at the end of the NDEBUG section. In other words, the section under NDEBUG has no functional effect except for the assert. I'll update the documentation later today.

grosser added inline comments.Nov 14 2021, 3:27 AM
mlir/lib/Analysis/Presburger/Simplex.cpp
1013

One way to clarify this could be to move all computation in the NDEBUG into a separate function and then call this function from the assert()?

arjunp updated this revision to Diff 387108.Nov 14 2021, 10:39 AM
arjunp marked 4 inline comments as done.

Address comments.

arjunp updated this revision to Diff 387115.Nov 14 2021, 11:11 AM

Rebase and write the regression tests using the new parser.

arjunp marked an inline comment as done.Nov 15 2021, 11:15 AM

@bondhugula gentle reminder :) can you take another look at the patch?

LGTM! I would just wait for @bondhugula to see if his concerns were addressed.

Did it previously just lead to longer running times or also incorrect emptiness results? It's unclear from the commit summary.

arjunp added a comment.Dec 2 2021, 8:49 AM

Did it previously just lead to longer running times or also incorrect emptiness results? It's unclear from the commit summary.

It lead to computing wrong dual coefficients.

Due to the way these are used, this in turn only leads to longer running times rather than wrong emptiness check results. i.e., it can lead to a "bad" basis that leads to longer (possibly exponentially bad) running times, but the returned basis would still always be a valid basis.

arjunp edited the summary of this revision. (Show Details)Dec 2 2021, 8:54 AM
This revision is now accepted and ready to land.Dec 9 2021, 8:33 AM