Enforce linearity in MLIR verifier.#11
Conversation
ausbin
left a comment
ausbin
left a comment
There was a problem hiding this comment.
Just some formatting/naming suggestions, except I do want to test it on one more case that I'm curious about
| // RUN: qwerty-opt %s --split-input-file --verify-diagnostics | ||
|
|
||
| module { | ||
| qwerty.func @sciff_iff_0[]() irrev-> !qwerty<bitbundle[1]> { |
There was a problem hiding this comment.
It might help to rename this to something like @linearity_scf_if_result_used_twice or something
| qwerty.func @no_cloning_0[]() irrev-> !qwerty<bitbundle[1]> { | ||
| %0 = qwerty.qbprep X<PLUS>[1] : () -> !qwerty<qbundle[1]> | ||
| %1 = qwerty.qbmeas %0 by {std: Z[1]} : !qwerty<qbundle[1]> -> !qwerty<bitbundle[1]> | ||
| qwerty.return %1 : !qwerty<bitbundle[1]> | ||
| } |
There was a problem hiding this comment.
am I correct that this isn't used?
| %1 = qwerty.qbmeas %0 by {std: Z[1]} : !qwerty<qbundle[1]> -> !qwerty<bitbundle[1]> | ||
| qwerty.return %1 : !qwerty<bitbundle[1]> | ||
| } | ||
| qwerty.func @unpack_this_1[]() irrev-> !qwerty<bitbundle[4]> { |
There was a problem hiding this comment.
Suggested alternative name: @linearity_unpack_used_twice_pack_unused
| %15 = qwerty.qbunpack %13 : (!qwerty<qbundle[1]>) -> !qcirc.qubit | ||
| %16 = qwerty.qbpack(%8, %9, %14, %15) : (!qcirc.qubit, !qcirc.qubit, !qcirc.qubit, !qcirc.qubit) -> !qwerty<qbundle[4]> | ||
| %17 = qwerty.qbmeas %16 by {std: Z[4]} : !qwerty<qbundle[4]> -> !qwerty<bitbundle[4]> | ||
| %18 = qwerty.qbpack(%2#0) : (!qcirc.qubit) -> !qwerty<qbundle[1]> |
There was a problem hiding this comment.
I think this would fail the linearity check here since it's not used. You could add one of those cool expected-error assertions here too
| // ----- | ||
|
|
||
| module { | ||
| qwerty.func @sciff_iff_0[]() irrev-> !qwerty<bitbundle[1]> { |
There was a problem hiding this comment.
This is a good idea for a test.
Suggested name: @linearity_qbprep_used_twice_in_nested_block
| // ----- | ||
|
|
||
| module { | ||
| qwerty.func @sciff_iff_0[]() irrev-> !qwerty<bitbundle[1]> { |
There was a problem hiding this comment.
This is also a good test.
Suggested name: @linearity_scf_if_used_twice_in_nested_block
| } | ||
|
|
||
| // Now we just check if all values that need to be linear are, in fact, linear. | ||
| for (mlir::Block& b : getBody()) { |
There was a problem hiding this comment.
| for (mlir::Block& b : getBody()) { | |
| for (mlir::Block &b : getBody()) { |
There was a problem hiding this comment.
My reasoning is that x has type int &, and y has type int in the following code:
int& x, y;| return op.emitOpError("Result (") | ||
| << idx | ||
| << ") is not linear with this IR instruction"; |
There was a problem hiding this comment.
Thank you for cleaning up the error message
2 participants
Addresses #9 in the general case. Moves linearity-checking logic to apply to all
mlir::Values in aqwerty.func's body that have linear types. This check also correctly handles regions within other regions, as verified by the included tests.