IsolatedFromAbove and scoping

MLIR
1

Bringing a discord chat here:

module {
  %c = constant 1 : index
  func @scope() -> (index) {
    %c = constant 1 : index
    return %c
  }  
}

results in the verifier failing:

test.mlir:5:7: error: redefinition of SSA value '%c'
      %c = constant 1 : index

This is somewhat unintuitive, since functions can’t access variables outside their scope. While this may not be a great decision, it’s unclear whether the above code (which is clearly well-defined) should actually be illegal.
@mehdi_amini pointed out that code like this could be confusing:

  %c = constant 1 : index
  func @scope() -> (index) {
    ...
    return %c
    ...
  ^bb13:
    %c = constant 1 : index
    ...
  }

Note that a similar message appears with arguments:

module {
  %c = constant 1 : index
  func @scope(%c : index) -> (index) {
    return %c
  }  
}

producing

test.mlir:3:15: error: region entry argument '%c' is already in use
  func @scope(%c : index) -> (index) {
              ^
test.mlir:2:3: note: previously referenced here
  %c = constant 1 : in

Currently, the behavior of the verifier does depend on Traits and Interfaces (in particular, GraphRegions change the behavior of the verifier). @mehdi_amini pointed out that we want to ensure that IR can be round-tripped without loading any dialects. In this case, the IR that is generated by mlir-opt --mlir-print-op-generic would still be round-trippable, since the above cases would never be generated.

So: should we change the behavior of the verifier/parser to understand IsolatedFromAbove, expanding the space of valid programs to include the cases above? Does anyone feel strongly that this is a bad idea?

Edit: I realize that this may be more of a parsing problem than a verification problem, which makes it a bigger deal, I think.

2

Yeah, this has nothing to do with the verifier. This is solely related to the parser/printer. We already allow this to a certain degree via the enableNameShadowing flag(i.e. we already have the logic in the parser/printer for distinct name scopes), but it isn’t automatic. If you wanted to extend that to always treat isolated regions as different name scopes it would probably be fine, but that would only be allowed when parsing/printing the custom form. This isn’t something that I’d be interested in supporting in the generic form.

3

I’m sure I’m missing something here on the custom form vs the generic form. I thought this was about the isolated trait which could be checked irrespective of whether the custom form was being parsed or the generic one. What are the implications of supporting nested name scopes on the generic form? I understand that if the op isn’t registered when the printed form is reparsed, the parsing would fail since the trait won’t be there. But this is a different issue?

4

This is the issue w.r.t the generic form. I’m okay with using traits to make the custom form more readable/functional, but the generic form is something that should always be parsable in an unregistered context. That to me is a major cornerstone of the generic form. We could support it when parsing the generic form, but this isn’t something that the printer should ever generate when printing in the generic form. That is where the complication comes in with adding support for this in general; during value naming we would need to know how we are going to print the operation so that it gets numbered differently. Region argument name shadowing skirts around this because it changes the numbering when printing the parent operation. It could work though, AsmState would just need to default to the behavior that currently exists and only number using traits if explicitly asked to.

5

Thanks - this makes perfect sense to me.