superty / llvm-project Goto Github PK

Running the following snippet, results in a crash on my machine:

TEST(CoalesceTest, failing) {
 PresburgerSet curr =
       setFromString("(d0, d1, d2)[] : (d0 >= 0 and d1 >= 0 and -d0 + -d1 + "
                   "1199 >= 0 and d2 + -1400 >= 0  or d0  >= 0 and d1  >= 0 "
                     "and -d0 + -d1 + 1199 >= 0 and -d2 + 1398 >= 0 )");
   PresburgerSet newSet =
       setFromString("(d0, d1, d2)[] : (d0 >= 0 and d1 >= 0 and -d0 - d1 + 1199 "
                     ">= 0 and d2 - 1400 >= 0 or d0 >= 0 and d1 >= 0 and -d0 - "
                     "d1 + 1199 >= 0 and -d2 + 1398 >= 0)");
   EXPECT_TRUE(PresburgerSet::equal(newSet, curr));
}

Those are actually the same set.

All of the simplification and lowering passes need access to the operation that define the Presburger sets in play. As this cannot be done if sets are passed as function parameters, we have to add verification steps that ensure all set definitions are accessible.

To go further in the direction of a complete dialect, we need these additional operations.

Also add canonicalisation passes.

I think a CI would be great.

We should definitely consider using cashing of the build as it otherwise takes a very long time.

I got the following warning, when compiling the current patch of @Dinistro :

home/webmiche/Desktop/ETH/llvm-project/mlir/lib/Dialect/Presburger/Parser.cpp: In member function ‘mlir::LogicalResult mlir::presburger::PresburgerSetParser::parseFlatAffineConstraints(mlir::presburger::Expr*, mlir::FlatAffineConstraints&)’:
/home/webmiche/Desktop/ETH/llvm-project/mlir/lib/Dialect/Presburger/Parser.cpp:543:74: warning: implicitly-declared ‘mlir::FlatAffineConstraints& mlir::FlatAffineConstraints::operator=(const mlir::FlatAffineConstraints&)’ is deprecated [-Wdeprecated-copy]
543 | cs = FlatAffineConstraints(dimNameToIndex.size(), symNameToIndex.size());
| ^
In file included from /home/webmiche/Desktop/ETH/llvm-project/mlir/include/mlir/Dialect/Presburger/Parser.h:9,
from /home/webmiche/Desktop/ETH/llvm-project/mlir/lib/Dialect/Presburger/Parser.cpp:6:
/home/webmiche/Desktop/ETH/llvm-project/mlir/include/mlir/Analysis/AffineStructures.h:110:3: note: because ‘mlir::FlatAffineConstraints’ has user-provided ‘mlir::FlatAffineConstraints::FlatAffineConstraints(const mlir::FlatAffineConstraints&)’
110 | FlatAffineConstraints(const FlatAffineConstraints &other);
| ^~~~~~~~~~~~~~~~~~~~~

As I already informed @Superty, the following test are failing on feature-expr-from-set :

MLIR-Unit :: Analysis/./MLIRAnalysisTests/FlatAffineConstraintsTest.FindSampleTest
MLIR-Unit :: Analysis/./MLIRAnalysisTests/FlatAffineConstraintsTest.IsIntegerEmptyTest

Both of them are violating the same assertion:

mlir/lib/Analysis/Presburger/Simplex.cpp:929: 
mlir::Fraction mlir::GBRSimplex::computeWidthAndDuals(ArrayRef<int64_t>, SmallVectorImpl<int64_t> &, int64_t &): 
Assertion `maybeWidth.hasValue() && "Width should not be unbounded!"' failed.

The problem started appearing after the commit "feature: Simplex::killCol and Simplex::closeRow": 8110c33

This commit introduces not only killCol and closeRow but also changes in makeProduct that I wasn't able to understand. Actually I'm even somewhat sure that this is the place where we / I broke it.
Note that makeProduct is executed in the constructor of GBRSimplex and there is not much more functionality that could break with this commit.

When the prototype was created I blindly ported the symbols from FlatAffineConstraints to the PresburgerSet without much thought. Now that this prototype is growing, we should think about the semantics of symbols. Therefore I list all the facts I know of yet:

• Symbols are used to make constraints dependent on specified SSA values, e.g. memref sizes. They are constant in a region of interest.
• From the previous, we get that we cannot eliminate the symbols during compile time as their values might be unknown.
• They can currently only appear as constant in constraints. Changing this might complicate transformations.
• Sampling is in general impossible if we have symbols. Consider the set (x)[s] : x >= s and assume we do not know s during compile time. Note that this might also be a problem for the MLIR patch.

Questions / Unclarities:

• Do we need symbols at all? I don't know now that I wrote all of this down.
• How should we treat symbols in operations? Currently, we assert that the count of symbols for both participating sets is equal and we do not add new once to the result.
  It would perhaps make sense to have union with to following type:
  (!presburger.set<d, s1>, !presburger.set<d,s2>) -> !presburger.set<d, s1 + s2>

Some inputs of you @tobiasgrosser and @Superty would be much appreciated.

It would be great, if we could type constraints as adjacent to an equality.

There are still some parsing errors that do not point to the exact point of failure.

I need to investigate all messages and make sure that they point to the correct location.

In my PR 3 testcases, which are not from me, fail. 2 of which are the ones we already know of, the third one comes from the dialect i think. Maybe @Dinistro can take a look at it :)

I think it would be a good idea to just be able to run the presburger related tests. Currently I have to build mutliple mlir binarys that are huge if I want to execute tests. Additionally always all tests FileCheck tests are executed. Overall this takes 5 to 10 minutes.

If we can split the tests into multiple targets, this would be nice for development speed.

As we already have a presburger.contains lowering I started working on a design for piecewise presburger expressions.
Before I show my different ideas, lets recap the pw_aff syntax used in ISL and the one for affine_map in MLIR:

ISL:

[n] -> { [x] → [x + 1] : 0 ≤ x < n − 1; [x] → [0] : x = n − 1 }

MLIR:

(d0, d1)[s0] -> (d0, d0 + d1 + s0)

First of all, I think that sticking to the dimension and symbol list syntax (the (d0, d1)[s0] in the above example) would be great, as this was consistently done till now. Therefore we should base the design on the MLIR example and extend the affine_map with informations about the different domains.

(x)[n] -> (x + 1) : (0 <= x and x < n - 1); (x)[n] -> (0) : (x = n - 1)

Alternatively with additional parenthesis:

((x)[n] -> (x + 1) : (0 <= x and x < n - 1)); ((x)[n] -> (0) : (x = n - 1))

Or with just one dimension and symbol list:

(x)[n] -> (x + 1) : (0 <= x and x < n - 1) ; (0) : (x = n - 1)

// Or

(x)[n] -> ((x + 1) : (0 <= x and x < n - 1)) ; ((0) : (x = n - 1))

I know that all these approaches are kind of hard to read, but I'm not sure if there is any representation thats really great for so much information. As we didn't use {} for Presburger sets and the usage of them outside of sets could be confusing, I decided to not use them in the above drafts.
In my opinion the second last option would be my preferred approach for now, but what do you think?