tests: Add various struct linearity and field access tests #293
Conversation
| 23: def foo(qs: linst[MyStruct]) -> linst[qubit]: | ||
| 24: return [s.q2 for s in qs if bar(s.q1)] | ||
| ^ | ||
| GuppyTypeError: Field `s.q2` with linear type `qubit` is not used on all control-flow paths of the list comprehension |
There was a problem hiding this comment.
I think talking about "control-flow paths" of a list comprehension could be a bit misleading, not sure what the better wording is. I'm thinking Field ... with linear type ... may not be used by this comprehension but that's not great either
There was a problem hiding this comment.
Ideally, you'd want to say that s.q2 is not used if bar(s.q1) is false.
Our dataflow analysis can already exactly identify which branch leads to a non-use, so we are actually not far off from having this better error message. However, we need to extend our error framework so that it can point to this location in the message.
I think something like this would be nice:
23: def foo(qs: linst[MyStruct]) -> linst[qubit]:
24: return [s.q2 for s in qs if bar(s.q1)]
^ Field `s.q2` with linear type `qubit` is not always used
24: return [s.q2 for s in qs if bar(s.q1)]
--------- `s.q2` is not used if this expression is `False`
There was a problem hiding this comment.
Added to issue #306
| 17: def foo(b: bool) -> bool: | ||
| 18: s = MyStruct(qubit()) | ||
| ^ | ||
| GuppyError: Field `s.q` with linear type `qubit` is not used on all control-flow paths |
There was a problem hiding this comment.
This seems wrong - the error should be highlighting lines 19 and 20?
There was a problem hiding this comment.
Mhm but 20 is an actual use? I think it makes more sense to point out that a variable is not used at the place where it is defined?
| 20: measure(s.q2) | ||
| 21: return s | ||
| ^ | ||
| GuppyError: Field `s.q2` with linear type `qubit` was already used (at 20:16) |
There was a problem hiding this comment.
Maybe "already used in some control flow paths"?
There was a problem hiding this comment.
Agreed, this would be better. However, we need to do some extra checks to determine if it's in "some" or "all" control-flow paths.
I'd prefer leaving this to another PR since it's not directly related to structs (the same error shows up if you use a regular variable instead of a struct access). See #306
| 16: def foo(s: MyStruct) -> tuple[MyStruct, qubit]: | ||
| 17: return s, s.q | ||
| ^^^ | ||
| GuppyError: Field `s.q` with linear type `qubit` was already used (at 17:11) |
There was a problem hiding this comment.
Can we record the use site of linear variables and point to where they were used when we give these error messages? I guess this requires upgrading the error framework to handle multiple locations
There was a problem hiding this comment.
We're already tracking the point where the variable has been used (that's the (at 17:11) part in the message). But it would be better to show this with a separate span 👍
Added to #306
|
|
||
|
|
||
| @guppy(module) | ||
| def foo(b: bool, s: MyStruct) -> MyStruct: |
There was a problem hiding this comment.
This I could imagine being fine, so maybe the error message needs to be more explicit. "Field is implicitly discarded by reassignment"?
There was a problem hiding this comment.
Yes, once we can point to multiple error locations, we could do
Guppy compilation failed. Error in file $FILE:16
15: @guppy(module)
16: def foo(s: MyStruct) -> MyStruct:
^^^^^^^^^^^ Field `s.q` with linear type `qubit` is not used
19: s.q = qubit()
--- `s.q` reassigned without use of the previous value
Added to #306
| 16: @guppy(module) | ||
| 17: def foo(s: MyStruct) -> int: | ||
| ^^^^^^^^^^^ | ||
| GuppyError: Field `s.q` with linear type `qubit` is not used on all control-flow paths |
There was a problem hiding this comment.
How does this error end up talking about control flow paths? It'd make more sense to that a linear field on the argument to the function isn't used as in the above errors
There was a problem hiding this comment.
The above errors where found while checking a single BB. This one is found via global dataflow analysis since there is an unconditional branch to the return BB.
We currently always add the "on all control-flow paths" suffix if errrors are found using the latter method, even if the branches are unconditional. I think this wouldn't be too hard to fix, but again adding it to #306 since it's not directly related to structs
| 16: @guppy(module) | ||
| 17: def foo(s: MyStruct) -> qubit: | ||
| ^^^^^^^^^^^ | ||
| GuppyError: Field `s.q2` with linear type `qubit` is not used on all control-flow paths |
| 14: def foo(s: MyStruct) -> None: | ||
| 15: s.z | ||
| ^^^ | ||
| GuppyTypeError: Expression of type `MyStruct` has no attribute `z` |
There was a problem hiding this comment.
I guess "attribute" is the general term for something that's either a field or a function?
There was a problem hiding this comment.
| 17: t = s | ||
| 18: t.x += 1 | ||
| ^^^ | ||
| GuppyError: Mutation of classical fields is not supported yet |
|
|
||
| @guppy(module) | ||
| def test(ss: linst[MyStruct]) -> linst[qubit]: | ||
| return [h(q) for s in ss for q in s.qs] |
| 18: if b: | ||
| 19: s = MyStruct(qubit()) | ||
| ^ | ||
| GuppyError: Field `s.q` with linear type `qubit` is not used on all control-flow paths |
There was a problem hiding this comment.
This is interesting. Instead of a linear variable in an outer context not being used in some control flow paths, there are variables created within certain control flow paths that are never used. I have no idea what the error should say
There was a problem hiding this comment.
Again, probably not for this PR
There was a problem hiding this comment.
Yeah this is the same problem as in #293 (comment)
See #295 for context, the tests are at #293 The basic idea is that we implicitly "unfold" structs into tuples and then rely on the existing linearity checking logic. The example from #295 is checked as follows: ```python @guppy.struct class MyStruct: q1: qubit q2: qubit x: int def main(s: MyStruct): s_q1, s_q2, s_x = s q = h(s_q1) t = h(s_q2) y = s_x + s_x use((s_q1, s_q2, s_x)) # Error ... ``` This is implemented using the `leaf_places()` iterator that gives us the leaf projections of places with (nested) struct types.
See #295 for context, the tests are at #293 The idea is to implement a similar logic to one used for linearity checking in #290. As soon as we assign a variable with struct type, we immediately unpack the struct to make the individual fields available. We only repack once the whole struct value is requested.
See #295 for context, the tests are at #293. * Moves the checking logic for captured linear variables from the `StmtChecker` into the `BBLinearityChecker` * This requires annotating the captured variables of a function with a usage location, so we know which location to use for the error * Also fixes how assignments to struct fields is handled in the `VariableVisitor`: In an assignment `s.x = ...`, we should record that `s` has been used (otherwise, we don't notice if `s` has been captured from an outer scope)
This is the feature branch for enabling struct field access and mutation of linear fields. Closes #276, closes #280, and closes #156. The difficult bit is that we want to track linearity of individual struct fields separately (akin to Rust's partial moves): ```python @guppy.struct class MyStruct: q1: qubit q2: qubit x: int def main(s: MyStruct): q = h(s.q1) t = h(s.q2) # Using s.q2 is fine, only s.q1 has been used y = s.x + s.x # Classical fields can be used multiple times use(s) # Error: Linear fields of s have already been used ... ``` This is the plan: * We introduce a new notion called `Place`: A place is a description for a storage location of a local value that users can refer to in their program. Roughly, these are values that can be lowered to a static wire within the Hugr and are tracked separately when checking linearity. * For the purposes of this PR, a place is either a local variable or a field projection of another place that holds a struct. I.e. places are paths `a.b.c.d` of zero or more nested struct accesses. In the future, indexing into an array etc will also become a place. * During type checking, we figure out which AST nodes correspond to places and annotate them as such * For linearity checking, we run a liveness analysis pass that tracks usage and assignment of places across the CFG. This way, linearity of different struct fields is tracked individually. * When compiling to Hugr, we keep track of a mapping from places to wires/ports Tracked PRs: * #288: Precursor PR to generalise our program analysis framework to run on places in the future. * #289: Adds the `Place` type and implements the type checking logic to turn `ast.Name` and `ast.Attribute` nodes into places. * #290: Update linearity checker to operate on places instead of variables * #291: Lower places to Hugr * #292: Some missing pieces to handle nested functions correctlt * #293
🤖 I have created a release *beep* *boop* --- ## [0.7.0](v0.6.2...v0.7.0) (2024-07-25) ### ⚠ BREAKING CHANGES * `qubit`s are now reset on allocation ### Features * `qubit`s are now reset on allocation, and `dirty_qubit` added ([#325](#325)) ([4a9e205](4a9e205)) * Allow access to struct fields and mutation of linear ones ([#295](#295)) ([6698b75](6698b75)), closes [#293](#293) * Allow redefinition of names in guppy modules ([#326](#326)) ([314409c](314409c)), closes [#307](#307) ### Bug Fixes * Use correct hook for error printing inside jupyter notebooks ([#324](#324)) ([bfdb003](bfdb003)), closes [#323](#323) --- This PR was generated with [Release Please](https://github.com/googleapis/release-please). See [documentation](https://github.com/googleapis/release-please#release-please).
See #295 for context