[Mlir-commits] [mlir] [mlir][tensor] Verify that `tensor.pad` padding is non-negative (PR #231389)

[Federico Bruzzone]

FedericoBruzzone wrote:

In essence, I'm working on a research project that analyzes MLIR programs and verifies op preconditions. Unfortunately I cannot share it at the moment, but I would like to. While doing that, I noticed this omission (if we agree it is :'D).

> Why the dynamic nature of this dimension changes how negative padding is treated?
> 
> If it is "meaningful" to have negative padding at all, it should work for both static and dynamic. If it's not, then it should not work for either.

They are not treated differently by design, dynamic are simply not checked. The verifier can only reject what is known at comp time, right?
The scope of this PR is limited to constant values (eventually propagated). If we also want to catch something like:
```mlir
%c = arith.constant -2 : index
%0 = tensor.pad %a low[%c] high[0] { ... }
```
we can change the verification to something like:
```c++
for (OpFoldResult pad : llvm::concat<OpFoldResult>(getMixedLowPad(), getMixedHighPad()))
```
Also, if we want to say that a _negative_ dynamic padding value is UB is open for discussion.

> Do you have more information if people use negative padding values today?

Unfortunately, no. However, I believe negative padding is not meaningful for `tensor.pad`:

* The op description defines low/high as "**how many** padded values are prepended/appended"
* When bufferizing, `low[-2]` produces a `memref.subview` with offset `-2`, which is rejected
* `tosa.pad` rejects negative padding values, as well


> I'm not saying I know of such cases or need this, but before we add such verification we should make sure it agrees with the semantics expectation and hopefully document it at the same time in the pad op.

Agreed, this change needs to be discussed, in particular whether we want this semantics. The PR already adds the documentation, if I understand correctly what you mean here.

---

If somebody knows of a user that relies on negative padding, I'm more than happy to revisit.






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