[PATCH] D142445: [mlir][tensor|memref] Harden the checks on dim op

[Mehdi AMINI via Phabricator via llvm-commits]

mehdi_amini added a comment.

In D142445#4079181 <https://reviews.llvm.org/D142445#4079181>, @qcolombet wrote:

>> Yes but you can't prove this path will be executed at runtime...
>
> Although true, I feel that if anything this change makes the verifier more consistent.
> Right now, the verifier will reject dim ops that are known to be out-of-bound for non-0-ranked shapes. This patch extends the check to 0-ranked shapes.

While I'm not sure about your patch (that is: it may very well be reasonable!), I am quite concerned about the out-of-bound check: any folding can make it so that we go from a dynamic offset to a constant one which would trigger a verifier failure (I need to craft a test-case...)

> If we follow the UB argument, we should not reject out-of-bound accesses for the non-0-ranked shapes either and instead generate unreachable.

Yes absolutely :)

> What I am saying is I feel the UB semantic is usually our way out of things we can't check statically

I think this is too limited of a view: this is a problem of scaling and "action at a distance": invalid IR differs from UB to me in terms of construction, and in particular the "dynamically reachable" is a critical aspect, take for example:

  if (cond()) *(int*)nullptr;

We can very well statically check and forbid this, however it is possible that `cond()` is always false. While you can design a language where "by construction" this can't happen, you would still need to think what kind of program transformation can lead there.

> The bottom line is for me it feels arbitrary to decide that 0-ranked should produce unreachable whereas non-0-ranked don't.

I agree, and as mentioned above, the 0-ranked is much more defendable than the other one to me! (That is because I'm not entirely sure about rank-reduction operation or how a transformation would expose the pattern in a way that justifies the original IR)


Repository:
  rG LLVM Github Monorepo

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D142445/new/

https://reviews.llvm.org/D142445