[Mlir-commits] [mlir] [mlir][affine] Allow `memref.cast` in `isDimOpValidSymbol` (PR #74401)

[Oleksandr Alex Zinenko]

ftynse wrote:

The change by itself LGTM.

How to structure the verifiers is a complex discussion that deserves more visibility on Discourse. We have more "non-local" verifiers in various places, and it looks important to verify such things as existence of symbols referenced by calls or presence of data layout / kernel attribute on the surrounding module. So far, I have written verifiers with the assumption that (1) verifiers can look at ancestor operations (otherwise, we cannot verify, e.g., that a terminator is nested in a specific operation) and (2) verifiers can inspect the region freely as it is a part of the operation being verified (otherwise, we cannot verify traits such as single-block regions). This was based on some discussion on the order of verification. I have implemented two-stage verifications to inspect siblings: (a) an operation verifies that its ancestor has a specific condition (typically an attribute is present); (b) when that condition is true for the parent operation, it verifies the relation between child operations in its regions. An example that you'd be familiar with is the `transform.with_named_sqeuence` attribute the verification of which checks of absence of recursive includes.

Affine rules are a different class because they imply traversing use-def chains, so inspecting _sibling_ operations at various levels. Not sure if they can get into a catastrophic case where the verifier assumes that another operation was verified, e.g. to APIs of this operation, but the operation is in fact invalid and hasn't been verified. If it is, that would be a good argument for changing. Abstractly, the two-staged approach described above can be used here, too. But there is a caveat: function-level values are accepted as affine, but we don't want function op interface to be aware of the affine dialect.

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