fix: Fix linearity checking bug (#441)

Fixes #438.

When checking that all live linear places in scope are definitely used,
we have to be more careful about determining whether variables are
*actually* live rather than only being included in scope because of the
less precise first pass of liveness analysis.

guppylang/checker/linearity_checker.py

@@ -425,6 +425,8 @@ def check_cfg_linearity(
     checked: dict[BB, CheckedBB[Place]] = {}
 
     for bb, scope in scopes.items():
+        live_before_bb = live_before[bb]
+
         # We have to check that used linear variables are not being outputted
         for succ in bb.successors:
             live = live_before[succ]
@@ -457,6 +459,12 @@ def check_cfg_linearity(
             for place in scope.values():
                 for leaf in leaf_places(place):
                     x = leaf.id
+                    # Some values are just in scope because the type checker determined
+                    # them as live in the first (less precises) dataflow analysis. It
+                    # might be the case that x is actually not live when considering
+                    # the second, more fine-grained, analysis based on places.
+                    if x not in live_before_bb and x not in scope.vars:
+                        continue
                     used_later = x in live
                     if leaf.ty.linear and not scope.used(x) and not used_later:
                         # TODO: This should be "Variable x with linear type ty is not

tests/integration/test_inout.py

@@ -266,7 +266,6 @@ def main(s: MyStruct, t: MyStruct) -> MyStruct:
     validate(module.compile())
 
 
-@pytest.mark.skip("Fails due to https://github.com/CQCL/guppylang/issues/337")
 def test_move_back_branch(validate):
     module = GuppyModule("test")
     module.load(quantum)

tests/integration/test_linear.py

@@ -329,6 +329,30 @@ def foo(i: bool) -> bool:
         return b
 
 
+def test_while_move_back(validate):
+    module = GuppyModule("test")
+    module.load(quantum)
+
+    @guppy.struct(module)
+    class MyStruct:
+        q: qubit
+
+    @guppy.declare(module)
+    def use(q: qubit) -> None: ...
+
+    @guppy(module)
+    def test(s: MyStruct) -> MyStruct:
+        use(s.q)
+        while True:
+            s.q = qubit()
+            return s
+        # Guppy is not yet smart enough to detect that this code is unreachable
+        s.q = qubit()
+        return s
+
+    validate(module.compile())
+
+
 def test_for(validate):
     module = GuppyModule("test")
     module.load(quantum)