Page MenuHomePhabricator

Exact integer emptiness checks for FlatAffineConstraints
ClosedPublic

Authored by arjunp on May 29 2020, 11:19 PM.

Details

Summary

This patch adds the capability to perform exact integer emptiness checks for FlatAffineConstraints using the General Basis Reduction algorithm (GBR). Previously, only a heuristic was available for emptiness checks, which was not guaranteed to always give a conclusive result.

This patch adds a Simplex class, which can be constructed using a FlatAffineConstraints, and can find an integer sample point (if one exists) using the GBR algorithm. Additionally, it adds two classes Matrix and Fraction, which are used by Simplex.

The integer emptiness check functionality can be accessed through the new FlatAffineConstraints::isIntegerEmpty() function, which runs the existing heuristic first and, if that proves to be inconclusive, runs the GBR algorithm to produce a conclusive result.

Diff Detail

Event Timeline

There are a very large number of changes, so older changes are hidden. Show Older Changes
arjunp updated this revision to Diff 270901.Jun 15 2020, 4:15 PM
arjunp marked 5 inline comments as done.

Address comments. Made findIntegerSample iterative.

arjunp marked 3 inline comments as done.Jun 15 2020, 4:19 PM
arjunp added inline comments.
mlir/include/mlir/Analysis/Presburger/Simplex.h
123

:)

mlir/lib/Analysis/Presburger/Simplex.cpp
867

It could theoretically grow arbitrarily large, although it may not happen in practice. I've made findIntegerSample iterative.

945

(I think this is no longer applicable since findIntegerSample is iterative now)

bondhugula requested changes to this revision.Jun 15 2020, 8:05 PM

Thanks very much for all the changes. A few more requests - a couple on test cases and other minor ones.

mlir/lib/Analysis/Presburger/Simplex.cpp
455–459

A short comment here please.

576

Comment here please.

mlir/unittests/Analysis/AffineStructuresTest.cpp
179

I think you are missing a test case involving equalities that is integer empty but not rational empty - a flat one along the lines of the test case added with purely inequalities. It could just be a 1-d line segment in a 2-d space that passes in between and thus misses all integer points - it could be potentially slanted as well.

mlir/unittests/Analysis/Presburger/SimplexTest.cpp
17

It may be good to add a line on what the test is testing.

23

Avoid auto here please.

87–88

Missing a test case here that involves equalities?

This revision now requires changes to proceed.Jun 15 2020, 8:05 PM
bondhugula added a comment.EditedJun 15 2020, 8:13 PM

Not for this patch, but if you want to just quickly try and test it on more cases, you could just replace mlir::boundCheckLoadOrStoreOp's isEmpty() with isIntegerEmpty() and see if -test-memref-bound-check test cases pass. The -test-memref-bound-check pass tests for out of bound memref accesses and actually needs an integer exact method (whenever it determines non-empty) to be accurate. This way you would also have a speed comparison, and it would also be a practical application of this technique for an analysis pass.

tests/Transforms/memref-bound-check.mlir

arjunp updated this revision to Diff 271040.Jun 16 2020, 4:19 AM
arjunp marked 6 inline comments as done.

Addressed comments.

I've added some more tests and documentation as requested.

bondhugula added inline comments.Jun 17 2020, 12:01 AM
mlir/unittests/Analysis/AffineStructuresTest.cpp
187

I'm sorry this would be caught by the GCD test itself. Instead, could you please replace the equality with something to the effect:

3x - 3y >= -2
3x - 3y  <= -1

This should be empty as well but would exercise your method given how isIntegerEmpty() is structured now.

bondhugula added inline comments.Jun 17 2020, 12:50 AM
mlir/include/mlir/Analysis/Presburger/Fraction.h
66

Are you assuming f.den is always positive? If both num and den are both negative, you'd want to add one.

arjunp updated this revision to Diff 271290.Jun 17 2020, 12:53 AM
arjunp marked 2 inline comments as done.

Added the requested test.

arjunp updated this revision to Diff 271292.Jun 17 2020, 12:55 AM

Fix a comment in Fraction.

arjunp marked 2 inline comments as done.Jun 17 2020, 12:57 AM
arjunp added inline comments.
mlir/include/mlir/Analysis/Presburger/Fraction.h
66

Yes, den is always positive. There was an incomplete comment for the member declaration that I've fixed. (This is also documented in the top-level class documentation)

mlir/unittests/Analysis/AffineStructuresTest.cpp
187

Since checkSample directly calls findIntegerSample() rather than isIntegerEmpty(), this shouldn't be an issue. Nonetheless, I've also added the test you requested.

Harbormaster completed remote builds in B60595: Diff 271292.
ftynse accepted this revision.Jun 22 2020, 6:00 AM

Thanks for providing more detailed documentation!

I did not extensively analyze the algorithms. At a glance, the implementation looks plausible. Again, given the complexity, I would encourage you to get 100% test coverage on the core functions. Another way to stress-test this would be to generate a bunch of arbitrary sets and run this + gcd emptiness checks and analyze the differences manually to make sure they only happen when gcd is not supposed to be correct.

I don't have any further comments.

@andydavis1 had a bug which might have been related to integer exactness, but I don't know if it is still active.

mlir/include/mlir/Analysis/Presburger/Simplex.h
38

Nit: SImplex -> simplex

46

Nit: 2x - 3y >= 0 (currently uses z)

bondhugula requested changes to this revision.Jun 22 2020, 8:40 AM
bondhugula added inline comments.
mlir/include/mlir/Analysis/Presburger/Fraction.h
66

If den is positive, this can be simplified to avoid an extra check.

f.num % f.den > 0 ? f.num / f.den + 1 : f.num / f.den;

(one comparison instead of two comparisons)

Also, if there is a doc comment here, please mention that den is positive. Actually, you don't even need this logic; mlir::ceilDiv does exactly this.

This revision now requires changes to proceed.Jun 22 2020, 8:40 AM

Thanks for providing more detailed documentation!

I did not extensively analyze the algorithms. At a glance, the implementation looks plausible. Again, given the complexity, I would encourage you to get 100% test coverage

+1 I don't think it's practical to have a review checking each of the steps of the algorithm. I would just rely on (1) good test case coverage, and (2) sufficient documentation/comments for now. Other implementation aspects can be brought up and revised later when there are other users with a specialized interest in digging deeper.

Thanks for your contribution!

It would be great to have tests on integer sets which resulting in an over approximation using the existing FM algorithm, but which returned integer exact results using GBR from this change.

Also wondering what the plan is to check for integer overflow of coefficient values for some of these algorithms?

arjunp updated this revision to Diff 273566.EditedJun 25 2020, 5:25 PM
arjunp marked 4 inline comments as done.

Improved test coverage. There is still one uncovered line; it seems quite difficult to find a case that covers this. I ran hundreds of tests with randomly generated sets intersected with a 1000 x 1000 x 1000 cube. Whenever GBR and the FM/GCD-based algorithm disagreed, I checked against a brute-force that checks every point in this cube. All these tests passed, as well as tests from some other types of generated cases.

Added some tests that GBR detects as empty but the existing FM/GCD-based algorithm does not.

Regarding overflow issues, it does not seem to be something specific to this patch. It looks to me like there already exists other functionality in FlatAffineConstraints, like FM, that performs operations without complete overflow checks. I feel that all these need to be addressed together by, say, introducing arbitrary-precision arithmetic, which is beyond the scope of this patch.

Thanks again for all your help with improving this patch!

bondhugula accepted this revision.Jun 27 2020, 3:12 AM
bondhugula added inline comments.Jun 27 2020, 3:30 AM
mlir/include/mlir/Analysis/Presburger/Fraction.h
39

This has to be a /// comment.

Added some tests that GBR detects as empty but the existing FM/GCD-based algorithm does not.

It'll be useful if you marked these tests with a comment to that effect. I might have missed it if you already did.

bondhugula requested changes to this revision.Jun 28 2020, 1:22 AM

A bunch of mostly minor comments.

mlir/lib/Analysis/Presburger/Simplex.cpp
707

Can you rephrase this? <dir, x-y> is unclear.

711

Please use coeffs.reserve since you know big it's going to be.

712–714

Why emplace_back instead of push_back for a POD?

719–723

Triple comments please.

866–867

Reflow - use the width?

875

Please make this a complete sentence.

961

You can use llvm::to_vector.

1011

llvm::to_vector

mlir/unittests/Analysis/AffineStructuresTest.cpp
30

Nit: hasValue -> 'hasValue'

56

SmallVector -> ArrayRef

57

Likewise.

68

Typo: least

72–73

Please pass ArrayRef instead of SmallVector for inputs. (If these were output args or inouts, SmallVectorImpl is to be used.)

mlir/unittests/Analysis/Presburger/SimplexTest.cpp
54

SmallVector 4?

60

Likewise.

This revision now requires changes to proceed.Jun 28 2020, 1:22 AM
arjunp updated this revision to Diff 274666.EditedJun 30 2020, 7:08 PM
arjunp marked 16 inline comments as done.

Addressed comments.

arjunp marked an inline comment as done.Jun 30 2020, 7:11 PM

Added some tests that GBR detects as empty but the existing FM/GCD-based algorithm does not.

It'll be useful if you marked these tests with a comment to that effect. I might have missed it if you already did.

This is marked at AffineStructuresTest.cpp:247.

mlir/lib/Analysis/Presburger/Simplex.cpp
707

I've replaced it with the more explicit dotProduct everywhere now. (this was originally explained in the top-level class comment)

mlir/unittests/Analysis/AffineStructuresTest.cpp
65

Is there a better way? This is needed since we moved to ArrayRefs for arguments but in checkPermutationsSample below we need to pass SmallVectors of SmallVectors to makeFACFromConstraints.

bondhugula added inline comments.Jul 1 2020, 12:04 AM
mlir/unittests/Analysis/AffineStructuresTest.cpp
65

We don't need to switch to ArrayRef of ArrayRef if you have SmallVector of SmallVector, but only to ArrayRef of SmallVector.

bondhugula accepted this revision.Jul 1 2020, 12:06 AM
bondhugula added inline comments.
mlir/unittests/Analysis/AffineStructuresTest.cpp
65

I actually meant ArrayRef<SmallVector,...> as the function argument instead of SmallVector<SmallVector<.... Make sure you don't run into underlying storage lifetime issues. ArrayRef<SmallVector..> should be fine.

arjunp updated this revision to Diff 274730.Jul 1 2020, 2:43 AM

Switched from ArrayRef of ArrayRef to ArrayRef of SmallVectors.

ftynse added a comment.Jul 1 2020, 3:25 AM

@Kayjukh your review is blocking this revision, have your concerns been addressed?

Kayjukh accepted this revision.Jul 1 2020, 3:53 AM

Yes, sorry about blocking the revision. Note that there is still a clang-format issue in one of the files.

mlir/unittests/Analysis/AffineStructuresTest.cpp
89

Please fix formatting

This revision is now accepted and ready to land.Jul 1 2020, 3:53 AM
arjunp updated this revision to Diff 274760.Jul 1 2020, 4:44 AM

clang-format.

arjunp marked an inline comment as done.Jul 2 2020, 6:23 AM

I don't have commit access yet, so I think someone else will need to land this.

I don't have commit access yet, so I think someone else will need to land this.

I've committed this.

This revision was automatically updated to reflect the committed changes.