[Mlir-commits] [mlir] [mlir][memref] Verify out-of-bounds access for `memref.subview` (PR #131876)

[Matthias Springer]

================
@@ -1876,118 +1876,65 @@ def SubViewOp : MemRef_OpWithOffsetSizesAndStrides<"subview", [
     The representation based on offsets, sizes and strides support a
     partially-static specification via attributes specified through the
     `static_offsets`, `static_sizes` and `static_strides` arguments. A special
-    sentinel value ShapedType::kDynamic encodes that the corresponding entry has
-    a dynamic value.
+    sentinel value `ShapedType::kDynamic` encodes that the corresponding entry
+    has a dynamic value.
 
-    A subview operation may additionally reduce the rank of the resulting view
-    by removing dimensions that are statically known to be of size 1.
+    A `subview` operation may additionally reduce the rank of the resulting
+    view by removing dimensions that are statically known to be of size 1.
+
+    The offsets, sizes and strides must be in-bounds with respect to the source
+    memref. When possible, the static operation verifier will detect
+    out-of-bounds subviews. Subviews that cannot be confirmed to be in-bounds
+    or out-of-bounds based on compile-time information are valid. However,
+    performing an out-of-bounds subview at runtime is undefined behavior.
 
     Example 1:
 
     ```mlir
-    %0 = memref.alloc() : memref<64x4xf32, affine_map<(d0, d1) -> (d0 * 4 + d1)>>
-
-    // Create a sub-view of "base" memref '%0' with offset arguments '%c0',
-    // dynamic sizes for each dimension, and stride arguments '%c1'.
-    %1 = memref.subview %0[%c0, %c0][%size0, %size1][%c1, %c1]
-      : memref<64x4xf32, affine_map<(d0, d1) -> (d0 * 4 + d1)>> to
-        memref<?x?xf32, affine_map<(d0, d1)[s0, s1] -> (d0 * s1 + d1 + s0)>>
+    // Subview of static memref with identity layout at dynamic offsets, sizes
+    // and strides.
+    %1 = memref.subview %0[%off0, %off1][%sz0, %sz1][%str0, %str1]
+        : memref<64x4xf32> to memref<?x?xf32, strided<[?, ?], offset: ?>>
     ```
 
     Example 2:
 
     ```mlir
-    %0 = memref.alloc() : memref<8x16x4xf32, affine_map<(d0, d1, d2) -> (d0 * 64 + d1 * 4 + d2)>>
-
-    // Create a sub-view of "base" memref '%0' with dynamic offsets, sizes,
+    // Subview of static memref with strided layout at static offsets, sizes
     // and strides.
-    // Note that dynamic offsets are represented by the linearized dynamic
-    // offset symbol 's0' in the subview memref layout map, and that the
-    // dynamic strides operands, after being applied to the base memref
-    // strides in each dimension, are represented in the view memref layout
-    // map as symbols 's1', 's2' and 's3'.
-    %1 = memref.subview %0[%i, %j, %k][%size0, %size1, %size2][%x, %y, %z]
-      : memref<8x16x4xf32, affine_map<(d0, d1, d2) -> (d0 * 64 + d1 * 4 + d2)>> to
-        memref<?x?x?xf32,
-          affine_map<(d0, d1, d2)[s0, s1, s2, s3] -> (d0 * s1 + d1 * s2 + d2 * s3 + s0)>>
+    %1 = memref.subview %0[4, 2][8, 2][3, 2]
+        : memref<64x4xf32, strided<[7, 9], offset: 91>> to
+          memref<8x2xf32, strided<[21, 18], offset: 137>>
     ```
 
-    Example 3:
+    Example 4:
----------------
matthias-springer wrote:

My bad, the numbering got messed up.

But I reduced the number of examples by one. I think the examples cover all interesting cases:

1. static source, static offsets, static sizes, static strides => static result
2. static source, dynamic offsets, dynamic sizes, dynamic strides => dynamic result
3. dynamic source, dynamic offsets, static sizes, dynamic strides => static result size but dynamic result strides
4. rank-reducing case
5. identity case

The main change is that the documentation no longer talks about the affine_map representation, which is outdated. That makes the examples shorter because we don't have to explain which dim/symbol corresponds to which size/stride.


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