Triggering pass assertions from mlir-opt: allowed?

In LLVM, we have a pretty hard rule that it should not be possible to trigger a crash or assertion by feeding verifer-valid IR to a pass. How hard of a line does it make sense to draw for this in the wider context of MLIR?

One example of where this can come up is with tensors. Our tensor type can model unranked tensors as well as various ranked cases up to the fully static case. Say we have a pass that only makes sense to run on ranked tensors (perhaps a code generation pass). Throughout this pass though one is constantly needing to do value.getType().cast<RankedTensorType>() to access the underlying RankedTensorType’s (perhaps on a std.addf op). It seems difficult to be able to avoid triggering assertions from verifier-valid input (which could include unranked tensors on the std.addf) for such a pass without littering the entire pass with rankedTensorType = ...dyn_cast<RankedTensorType>(); if (!rankedTensorType) return failure() type of noise code that “should never happen”.

I wonder if we could reuse the concept of a legalization target to help with this. For example, a pass could associate with itself an mlir::ConversionTarget, and when the verifier is enabled the addition of such a pass to a pipeline creates a “verify satisfies conversion target” pass in addition to a regular verifier pass.

I consider MLIR to have the same policy. We could spell it out in the developer guide, feel free to send a patch :wink:

The way I would write such a pass is to check its own invariant upfront and bailout immediately.

I think we should never assert or crash on verifier-valid IR. If there is a code generation pass that is only meant to run on ranked tensor types, it should just appropriately deal with / bail out / return failure() when it encounters unranked tensors. You could have a pre-transform check to make sure you only deal with input that you are able to handle, and so that the casts are guaranteed to succeed.

I think that tying verification conditions only with dialects is somewhat constraining. For instance, in the llvm dialect after it has been “legalizedForExport”, additional properties hold. I’ve wondered if it would be worthwhile attaching these properties to verification operations, which would encode the verification property. This would allow transforms to check the property by asking the “propertyOperation” to verify the condition (potentially reusing some assertion from a previous transformation which inserted the propertyOperation). This would allow encoding in the IR these secondary structural properties.

Incidentally, I agree with the others: we should never assert on verifier-valid IR, but bail out safely with an appropriate error message.

Where is the .md file for Developer Guide - MLIR ? I can’t seem to find it.

You have an Edit on GitHub link at the bottom for these pages. There aren’t generated from the code so they live in the website repo directly (pull-requests are the way to go there)

Done. PTAL: