[Mlir-commits] [mlir] [mlir][VectorToLLVM] emit `inbounds|nuw` GEP flags when lowering `vector.load/store` (PR #202118)

[Federico Bruzzone]

================
@@ -256,10 +256,19 @@ class VectorLoadStoreConversion : public ConvertOpToLLVMPattern<LoadOrStoreOp> {
                                          "could not resolve alignment");
 
     // Resolve address.
+    // Per vector.load/store spec, indices must be in-bounds (0 <= idx <
+    // dim_size). Emit inbounds|nuw so LLVM can apply no-wrap optimizations on
----------------
FedericoBruzzone wrote:

I apologize if this response took a little while to arrive.
Thanks again. I've been new to this world for about two weeks, and your comments are very helpful.

However, I'm a little confused. 
The spec doesn't require in-bounds indices. It explicitly permits OOB reads (e.g., `vector.load %memref[%c0] : memref<7xf32>, vector<8xf32>`).

But I think it's worth separating two cases:
1. `inbounds` (and the implied nusw/nsw on the index arithmetic) reduce to a single assumption: the addressed element lies within the allocation. 
     
     The [GEP](https://llvm.org/docs/LangRef.html#getelementptr-instruction) only computes the start address, it doesn't access memory. The `inbounds` rules constrain the computed pointer, not the width of any later access through it (I think `inrange` attribute is for this case). With a valid memref descriptor, all the `nusw` rules are "discharged" by the in-bounds assumption via the [allocated-objects rules](https://llvm.org/docs/LangRef.html#allocated-objects). That is, the object size cannot exceed the largest signed value of the index type and objects cannot cross the address-space boundary.

    This covers the vector spec's ["Explicit out-of-bound vector load"](https://mlir.llvm.org/docs/Dialects/Vector/#vectorload-vectorloadop), e.g., `vector.load %memref[%c0] : memref<7xf32>, vector<8xf32>`. The start address is in bounds, so the GEP flags are not violated (If I understood correctly). The OOB part is the plain `llvm.load` itself, that is already UB today, independently of this patch. The [Pointer Aliasing Rules](https://llvm.org/docs/LangRef.html#pointer-aliasing-rules) say: "any memory access must be done through a pointer value associated with an address range of the memory access, otherwise the behavior is undefined", where the address range of a `load <8 x float>` is all 32 bytes accessed. 
    
    Note the vector.load spec is careful to distinguish two failure modes: OOB elements have undefined values, and only the alignment clause triggers immediate undefined behavior, but the lowering to a plain load doesn't preserve that distinction. Again, it might be possibile that the current conversion already doesn't honor the documented OOB semantics, with or without the GEP flags (prob a pre-existing inconsistency between the spec and the lowering). Consider:
    ```mlir
    %buf = memref.alloca() : memref<7xf32>
    // fill the 7 elements
    %v = vector.load %buf[%c0] : memref<7xf32>, vector<8xf32>
    ```
    the vector spec essentially says: "Ehi, this op is valid and lane 0–6 contains your data, on lane 7 no assumptions should be made on the value". It's lowered to:
    ```llvm
    %a = alloca [7 x float]
    %v = load <8 x float>, ptr %a ; reads 32 byte from a 28-byte object
    ```
    In LLVM IR this is **not** "the lane 7 is undefined": for the Pointer Aliasing Rules it is simply UB (if I understood correctly).

2. `nuw` needs strictly more than in-bounds (not the flag :'D). The `nuw` rules require every term of the offset computation to be non-negative when interpreted as unsigned, meaning non-negative indices and non-negative strides. This is a strictly stronger condition. Correct me if I'm wrong, but we can land `inbounds` while violating `nuw` if you get there by walking backwards (also in memref maybe). E.g., a flipped view (from `[0, 1000)` -> `[900, 1000)`):
    ```mlir
    %flip = memref.reinterpret_cast %base to offset: [1000], sizes: [100], strides: [-1]
             : memref<2000xf32> to memref<100xf32, strided<[-1], offset: 1000>>
    %v = vector.load %flip[%c5] : memref<100xf32, strided<[-1], offset: 1000>>, vector<1xf32>
    ```
    Index 5 is in `[0, 100)`. The addressed element is at `base + 1000 + 5*(−1) = base + 995` inside the allocation. `inbounds` is satisfied. `nsw` is satisfied. But `mul nuw 5, −1` (read as unsigned `−1` is `2^64 − 1`), so the product wraps (poison) and the load is UB (again, if I understood correctly). See the second bullet under the `nuw` flag explanation of  [GEP docs](https://llvm.org/docs/LangRef.html#getelementptr-instruction).
    
    That's to say, it's not correct to put a priori `nuw` here. But then the same goes for `memref`, am I missing something?


I think that we should clarify the `vector.load/vector.store` index semantics. E.g., requiring the start address to be in-bounds, and stating the non-negativity conditions under which lowerings may emit inbounds/nuw, mirroring the memref.load/memref.store wording. 


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