`tensor_to_memref` and its folding

I still totally disagree with your rational here unfortunately: I can’t follow your logic.

Your “1.” seems reversed to me, since the semantics attached to tensor_to_memref is in the first place to provide the guarantee that canonicalization relies on right now. When you write “My problem is that the canonicalization is done without any of this context/restrictions”, you’re totally missing the point of the op semantics here I believe: canonicalization is done because of this restrictions.

For “2.” you’re saying “Except that if I did have full visibility over it”, but if you have full visibility over this memref, you know it is coming from a tensor_to_memref, and so you know you can’t write to this memref.

So either writes to a memref from tensor_to_memref should be illegal,

I thought we established it is illegal? Or at least UB.
If you intend to push for a situation where everything that can’t be statically verified on the IR has to be allowed, and you’re excluding the possibility of UB, that will be a problem for many more situations (Sanjoy mentioned out-of-bound accesses for example, but use-after-free may be another one).

Not exactly, but partially true. My hope here was

  1. Can you make an illegal behavior statically verifiable. If so do that.
  2. If not, its undefined behavior.

Out-of-bounds accesses when your buffer is dynamically shaped is also UB. Agree with use-after-free as well being UB.

Anyways, I guess this has been quite a long thread. I genuinely appreciate the comments here. If the canonicalization is deemed valid, then I wont push that further.

IIUC, this analogy of comparing with another UB is taking it too far. If a memref has been defined (doesn’t matter by which op), one would expect to be able to write to it, and all writes to it are defined so long as the indices are within the logical shape dimensions. If you are enforcing constraints like memref results of certain ops are not writeable, that sounds like a design problem and you really needed a different type like a const_memref or an extra bit in the memref type like memref<1024xf32, r, #map, 0> (r, rw, etc.). Incidentally, this report talks about such a dialect-specific memref type in a different context:

%W1r, %W1w = hir.alloc() : !hir.memref<2*i32, packing=[], r>,
!hir.memref<2*i32, packing=[], w>

We could introduce a const_memref, but that’s not what MLIR is implementing right now. In absence of having a constant memref in the type system, memref is acting similarly as pointers in LLVM (const int * and int * have the same IR type emitted by clang): it erases the constness from the type system. Seems like a stretch to me to call this a “design problem” when this is really an IR and type system tradeoff.