Remove verify from OperationBuilder and SameOperandsAndResultType verification implementation

[lima-limon-inc]

Closes #456

The issue states that currently Operation::verify is called inside the OperationBuilder which is called before operations are added to blocks, which could lead to failure in operation verification. Because of this, SameTypeOperands' verification function had been commented out.

This PR removes the call to Operation::verify from the OperationBuilder and moves it to the beggining of PassManager::run. Operation::verify was already called inside the PassManager::run (more precisely, inside the OpToOpPassAdaptor::run_pipeline). An additional verify call was added at the beginning of the PassManager pipeline to "compensate" its removal in the OperationBuilder and ensure Operation integrity before applying passes. Now, the PassManger is responsible for Operation integrity verification, which is done before passes are applied and also after each pass applies its modifications.

With the call to verify in the OperationBuilder now removed, SameTypeOperands' verification function was re-enabled and so was its test (derived_op_verifier_test).

Additionally, an implementation for SameOperandsAndResultType's verification function was added (which was marked here as a TODO item). Following the comment's requirements, SameTypeOperands was marked as a super-trait.

To support this, the derive! macro was expanded to support super-traits. The macro supports an arbitrary amount of traits; but it is important to note that the traits must be comma separated instead of the usual "+" separated format. As far as I am aware, it is not possible to use "+" as a separator inside a macro_rules! context.

With the super-trait now added, operations that implemented SameOperandsAndResultType but did not implement SameTypeOperands were updated to now explicitly implement both. This was done explicitly in order to replicate Rust's #[derive] macro's behavior of explicitly declaring all derived traits.

Finally, a unit test was added to test SameOperandsAndResultType's verify function. For this, a test operation InvalidOpsWithReturn was added and registered in the test dialect.

Side note: I tried to keep the SameOperandsAndResultType's doc comment relatively short in order for it to show up in its entirety when a compilation error shows up, it is currently displayed like so:

72  | / derive! {
73  | |     /// Op expects all operands and results to be of the same type.
74  | |     /// NOTE: Operations that implement this trait must also explicitly implement
75  | |     /// [`SameTypeOperands`]. This can be achieved by using the "traits" filed in the [#operation]
...   |
87  | |     pub trait SameOperandsAndResultType: SameTypeOperands {}
    | |               ------------------------- required by a bound in this trait

[lima-limon-inc]

Update: The tests are now failing because cfg_to_scf_lift_conditional_early_exit builds a Neg operation with a i1 and u32 as operands. So SameTypeOperands' verify function fails (since it was enabled in the PR).

I'm working on a fix

Edit: This commit upcasts v345 type to U32 as required by the following Neq. Is this the intended way to upcast the type?

[bitwalker]

Nice work! I've noted a couple of small changes to make, but otherwise it looks good to me!

[bitwalker]

You shouldn't need to define a new operation type to test the verifier. I would instead simply construct an Add operation with mismatched operand types to trigger a verification error.

Since this operation implements InferTypeOpInterface (and Add does as well), by definition the result type will be inferred to match the operand type, so we're really just testing that verification fails if the operand types are mismatched, and that's fine for the purpose of the test anyway.

[lima-limon-inc]

You shouldn't need to define a new operation type to test the verifier. I would instead simply construct an Add operation with mismatched operand types to trigger a verification error.

Question, which verifier are you referring to? Wouldn't constructing an Add operation with mismatched operand types trigger SameTypeOperands's verification function to error instead of SameOperandsAndResultType's?

If I'm not mistaken, construction of an Add op with mismatched operand types is being tested in the derived_op_verifier_test test, note these lines.

The initial idea behind InvalidOpsWithReturn was for it to test SameOperandsAndResultType verification function, hence the new test added here.

Since this operation implements InferTypeOpInterface (and Add does as well), by definition the result type will be inferred to match the operand type, so we're really just testing that verification fails if the operand types are mismatched, and that's fine for the purpose of the test anyway.

I hardcoded InferTypeOpInterface implementation for InvalidOpsWithReturn so it always returned U64 (see here). It was the only way I managed to make InvalidOpsWithReturn build correctly, but fail during trait validation. Is there a mechanism that I'm missing? As an aside if I remove the InferTypeOpInterface trait from the operation, then it fails to build the op, stating: invalid operation

Do note that if this test is contrived, then it can be removed all together.

Thanks in advance and apologies if I'm missing something

[bitwalker]

So in general, SameOperandsAndResultType, pretty much implies InferTypeOpInterface (not literally, but if you are defining an op whose result type must be the same as the operands, then implementing InferTypeOpInterface is trivial, and would guarantee that the result always matches the operand type from which it is inferred.

With that in mind, testing SameOperandsAndResultType pretty much requires doing so with an op that doesn't implement InferTypeOpInterface (which would be weird, but is allowed), or overriding the result type after inference. As you found, all of our current test ops that implement SameOperandsAndResultType also implement InferTypeOpInterface (and that's the case with all of our other dialects as well), so I think the best way to test the verifier here is to simply override the result type after inference (e.g. with Add), just to force invalid IR to trip the verifier.

[lima-limon-inc]

Great! Thanks for the clarification.

With this in mind, what do you think about this refactor: 10728a7

I think I do have to use the set_type method in this case, right? I tried to do a proper cast via zext/sext, but I was not able to use that method. As far as I can tell, that method is implemented for the ArithOpBuilder trait, which is implemented in the midenc-dialect-arith crate. So when I try to import it in derive.rs' Cargo.toml (hir/Cargo.toml), I get a cyclic package dependency error.

Regardless, maybe in this case does merit the use of set_type use, since it is more of an explicit override rather than a proper cast.

[bitwalker]

I think I do have to use the set_type method in this case, right?

Yes, correct, we're basically creating invalid IR on purpose, and the only real way to do it is to use low-level APIs like set_type.

With this in mind, what do you think about this refactor: 10728a7

LGTM!