[Mlir-commits] [mlir] [mlir][arith] Add more canonicalization and integration tests coverage (PR #92272)

[Andrzej Warzyński]

banach-space wrote:

> As far as I can see, unit tests don't verify that a pattern is correct: I mean correct in the sense that for a pattern source -> target, source and target have the same semantics, in all contexts.

Thanks for clarifying, now I see what you meant. Still, I think that one of Mehdi's previous comments is quite fitting here:

> Again virtually the entirety of transformations in LLVM are developed that way ~ forever, we could change our testing approach of course, but IMO that's an RFC for the LLVM discourse.

I will paraphrase - you are proposing a different approach towards testing compared to what's normally done in LLVM/MLIR. We could change that, sure, but it's a discussion beyond Arith and MLIR, and more suitable for LLVM Discourse.

> Indeed the formula (or, the correctness of the lowering pattern) is the part that wasn't able to be tested by a unit test - and an e2e test would be able to provide test coverage for it. 

Right, but I don't believe that we should be using MLIR integration tests to verify that a particular Mathematical formula is correct. Instead, we should select a formula that is known to be correct (surely there are some good references) and implement that. Testing in MLIR should focus on making sure that the implementation itself is correct, not the formula. Does it make sense?

Having said that, IMHO, it would be totally fine to have e2e for things like `floordivsi`. That's a good example of "this is complex and let's complement unit tests with integration tests".

> I am actually currently developing semi-formal semantics in Haskell for some MLIR operations.

Exciting! It would be interesting to see how you make sure that the semantics in Haskell match MLIR (and whether there's scope for writing a test-suite). That's a completely different thread though 😅 

https://github.com/llvm/llvm-project/pull/92272