fix(ownership): clear the enclosing killed set when a while condition contains break or continue

compiler/noirc_frontend/src/ownership/last_uses.rs

@@ -311,6 +311,11 @@ impl LastUseContext {
             }
         }
         self.killed = saved_killed;
+        // A `break`/`continue` in the condition targets the enclosing loop, so its
+        // `killed.clear()` must apply to the enclosing set we just restored.
+        if condition_has_break {
+            self.killed.clear();
+        }
         self.has_break = saved_has_break || condition_has_break;
     }
 

compiler/noirc_frontend/src/ownership/tests.rs

@@ -2280,3 +2280,105 @@ fn closure_captured_array_used_twice_clones_first_use() {
     }
     ");
 }
+
+#[test]
+fn break_in_nested_while_condition_clears_killed() {
+    // The `break` in the inner `while`'s condition targets the OUTER loop, so it can skip
+    // the reassignment `x = [v, v, v]`. `x`'s old value is then still live after the loop,
+    // so its use in `let mut y = x` must be cloned, not moved: `x` may not stay in the
+    // `killed` set that exempts it from loop-exit truncation, even though that set is
+    // saved away while the inner loop (and its condition) is traversed.
+    let src = "
+    unconstrained fn main(v: Field, n: u32) -> pub [Field; 2] {
+        let mut x = [v, v, v];
+        let mut z = [0, 0, 0];
+        let mut i = 0;
+        while i < n {
+            let mut y = x;
+            y[0] = 9;
+            z = y;
+            let mut j = 0;
+            while ({ if i == 1 { break; } j < 3 }) { j = j + 1; }
+            x = [v, v, v];
+            i = i + 1;
+        }
+        [x[0], z[0]]
+    }
+    ";
+
+    let program = get_monomorphized(src).unwrap();
+    insta::assert_snapshot!(program, @r"
+    unconstrained fn main$f0(v$l0: Field, n$l1: u32) -> pub [Field; 2] {
+        let mut x$l2 = [v$l0, v$l0, v$l0];
+        let mut z$l3 = [0, 0, 0];
+        let mut i$l4 = 0;
+        while (i$l4 < n$l1) {
+            let mut y$l5 = x$l2.clone();
+            y$l5[0] = 9;
+            z$l3 = y$l5;
+            let mut j$l6 = 0;
+            while {
+                if (i$l4 == 1) {
+                    break
+                };
+                (j$l6 < 3)
+            } {
+                j$l6 = (j$l6 + 1)
+            };
+            x$l2 = [v$l0, v$l0, v$l0];
+            i$l4 = (i$l4 + 1)
+        };
+        [x$l2[0], z$l3[0]]
+    }
+    ");
+}
+
+#[test]
+fn continue_in_nested_while_condition_clears_killed() {
+    // The `continue` spelling of `break_in_nested_while_condition_clears_killed`: it also
+    // targets the outer loop and can also skip the reassignment `x = [v, v, v]`, so the use
+    // of `x` in `let mut y = x` must be cloned, not moved.
+    let src = "
+    unconstrained fn main(v: Field, n: u32) -> pub [Field; 2] {
+        let mut x = [v, v, v];
+        let mut z = [0, 0, 0];
+        let mut i = 0;
+        while i < n {
+            let mut y = x;
+            y[0] = 9;
+            z = y;
+            i = i + 1;
+            let mut j = 0;
+            while ({ if i == n { continue; } j < 3 }) { j = j + 1; }
+            x = [v, v, v];
+        }
+        [x[0], z[0]]
+    }
+    ";
+
+    let program = get_monomorphized(src).unwrap();
+    insta::assert_snapshot!(program, @r"
+    unconstrained fn main$f0(v$l0: Field, n$l1: u32) -> pub [Field; 2] {
+        let mut x$l2 = [v$l0, v$l0, v$l0];
+        let mut z$l3 = [0, 0, 0];
+        let mut i$l4 = 0;
+        while (i$l4 < n$l1) {
+            let mut y$l5 = x$l2.clone();
+            y$l5[0] = 9;
+            z$l3 = y$l5;
+            i$l4 = (i$l4 + 1);
+            let mut j$l6 = 0;
+            while {
+                if (i$l4 == n$l1) {
+                    continue
+                };
+                (j$l6 < 3)
+            } {
+                j$l6 = (j$l6 + 1)
+            };
+            x$l2 = [v$l0, v$l0, v$l0]
+        };
+        [x$l2[0], z$l3[0]]
+    }
+    ");
+}

test_programs/execution_success/regression_while_condition_break_killed/Nargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "regression_while_condition_break_killed"
+type = "bin"
+authors = [""]
+
+[dependencies]

test_programs/execution_success/regression_while_condition_break_killed/Prover.toml

@@ -0,0 +1,3 @@
+v = "1"
+n = "5"
+return = ["1", "9"]

test_programs/execution_success/regression_while_condition_break_killed/src/main.nr

@@ -0,0 +1,34 @@
+// Regression for the `killed` set being restored across a loop boundary, discarding the
+// `killed.clear()` performed by a `break` in a nested `while` condition.
+//
+// The `break` in the inner `while`'s condition targets the OUTER loop, so it can skip the
+// reassignment `x = [v, v, v]`. The old value of `x` is then still live after the loop, so
+// `let mut y = x` must clone rather than move: otherwise `y` aliases `x` and `y[0] = 9`
+// corrupts the value read afterwards. `z = y` keeps the in-place `array_set` from being
+// optimized away. With `v = 1` and `n = 5` the `break` fires on the last executed iteration
+// (`i == 1`), so nothing repairs the corruption: the correct result is `[1, 9]`; the missing
+// clone produces `[9, 9]` (or fails SSA validation in a debug build).
+unconstrained fn main(v: Field, n: u32) -> pub [Field; 2] {
+    let mut x = [v, v, v];
+    let mut z = [0, 0, 0];
+    let mut i = 0;
+    while i < n {
+        let mut y = x;
+        y[0] = 9;
+        z = y;
+        let mut j = 0;
+        while (
+            {
+                if i == 1 {
+                    break;
+                }
+                j < 3
+            }
+        ) {
+            j = j + 1;
+        }
+        x = [v, v, v];
+        i = i + 1;
+    }
+    [x[0], z[0]]
+}

test_programs/execution_success/regression_while_condition_continue_killed/Nargo.toml

@@ -0,0 +1,6 @@
+[package]
+name = "regression_while_condition_continue_killed"
+type = "bin"
+authors = [""]
+
+[dependencies]

test_programs/execution_success/regression_while_condition_continue_killed/Prover.toml

@@ -0,0 +1,3 @@
+v = "1"
+n = "5"
+return = ["1", "9"]

test_programs/execution_success/regression_while_condition_continue_killed/src/main.nr

@@ -0,0 +1,33 @@
+// The `continue` spelling of `regression_while_condition_break_killed`: a `continue` in a
+// nested `while` condition also targets the OUTER loop and also clears the `killed` set,
+// and that clear must survive the loop boundary just like for `break`.
+//
+// `i` is incremented before the inner `while`, so when the `continue` fires (`i == n`, the
+// final iteration) it jumps to the outer condition, which is now false: the loop exits with
+// the reassignment `x = [v, v, v]` skipped. The old value of `x` is still live after the
+// loop, so `let mut y = x` must clone rather than move. The correct result is `[1, 9]`; the
+// missing clone produces `[9, 9]` (or fails SSA validation in a debug build).
+unconstrained fn main(v: Field, n: u32) -> pub [Field; 2] {
+    let mut x = [v, v, v];
+    let mut z = [0, 0, 0];
+    let mut i = 0;
+    while i < n {
+        let mut y = x;
+        y[0] = 9;
+        z = y;
+        i = i + 1;
+        let mut j = 0;
+        while (
+            {
+                if i == n {
+                    continue;
+                }
+                j < 3
+            }
+        ) {
+            j = j + 1;
+        }
+        x = [v, v, v];
+    }
+    [x[0], z[0]]
+}