A while condition runs every trip, so it may not move what it stands on

The condition was checked before in_loop, outside the diff that catches a
loop giving away what the next iteration needs. Emit puts the condition in
the loop header, so it runs again every trip: a condition that frees a
local freed it once per trip. It is now diffed against the same dead set,
with its own reason. A dotimes count and a loop's initial values stay
outside: those are evaluated exactly once.

lib/check.ml

@@ -1686,7 +1686,25 @@ let rec check ctx ?want (e : Ast.expr) : Tast.expr =
   | Ast.Let (bs, body) -> check_let ctx ~tail ?want ~defer_ok loc bs body
   | Ast.If (c, t, e') -> check_if ctx ~tail ?want loc c t e'
   | Ast.While (label, c, body) ->
+    (* The condition is part of the loop even though it is written outside the
+       braces: emit puts it in the header block, so it is re-evaluated at the
+       top of every trip, and a condition that gives a value away frees it once
+       per trip. So it is held to the loop's rule on moves and to nothing else
+       the loop changes: it stays outside [in_loop], because a [break] in a
+       condition still means the enclosing loop and a [defer] there is still
+       the outer block's, but its moves are diffed against the same dead set.
+       [dotimes]' count and a [loop]'s initial values are checked outside this
+       regime on purpose: they are evaluated exactly once, before the first
+       trip, so giving one away there is no more than giving it away before
+       the loop. *)
+    let before = ctx.dead in
+    let outer = List.map (fun (_, b) -> b.slot) ctx.scope in
     let c = check ctx ~want:Types.Bool c in
+    moved_across_iterations ctx ~before ~outer
+      "this while condition moves a value that was bound outside the loop, and \
+       the condition is evaluated again at the top of every trip, so the second \
+       one would use what the first gave away. Move it out of the loop, or \
+       test something the loop does not give away";
     let body = in_loop ctx ?label (fun () ->
       scoped ctx (fun () -> map_lr (fun b -> check ctx b) body))
     in
@@ -2431,15 +2449,25 @@ and in_loop ctx ?label ?entry ?(fresh = []) f =
   let r = f () in
   ctx.defer_block <- blocker;
   ctx.loops <- loops;
+  moved_across_iterations ctx ~before ~outer:outer_slots
+    "this moves a value that was bound outside the loop, so the next \
+     iteration would use what this one gave away. Move it out of the loop, \
+     or bind a fresh value inside it";
+  r
+
+(* The rule a loop adds to the move checker, in one place because two forms
+   need it and they need it for the same reason. Everything that runs more
+   than once runs against the dead set it left behind last time: a slot that
+   was live on the way in and is dead on the way out was given away by code
+   that is about to run again, and the second run would be using what the
+   first one released. Slots bound inside the repeated region are not in
+   [outer] and are not the question — they are born again every trip. *)
+and moved_across_iterations ctx ~before ~outer why =
   List.iter
     (fun (slot, where) ->
-       if (not (List.mem_assoc slot before)) && List.mem slot outer_slots then
-         fail where
-           "this moves a value that was bound outside the loop, so the next \
-            iteration would use what this one gave away. Move it out of the \
-            loop, or bind a fresh value inside it")
-    ctx.dead;
-  r
+       if (not (List.mem_assoc slot before)) && List.mem slot outer then
+         fail where "%s" why)
+    ctx.dead
 
 (* Which loop a [break] or a [continue] means, as a count of loops outwards
    from the innermost — which is what [Tast.Break] carries and what [emit]

test/test_flan.ml

@@ -1198,6 +1198,16 @@ let () =
   rejects_check "a labelled break may not leave a loop"
     "(defn f [] () (while :o true (loop [i 0] (break :o))))"
     ~needle:"no value to give";
+  (* A while's condition runs once per trip, so it lives under the same rule
+     as the body: what it gives away, it gives away again next time round.
+     Before this was checked the program below compiled and aborted in free(). *)
+  rejects_check "a while condition may not move what the loop is standing on"
+    "(defn eat [v (Vec i32)] bool (do (free v) true)) \
+     (defn f [] () (let [v (vec-new i32)] (while (eat v) (break))))"
+    ~needle:"evaluated again at the top of every trip";
+  accepts "a condition that only looks at what it tests is fine"
+    "(defn f [] () (let [v (vec-new i32)  n 0] \
+       (while (and (< n 10) (> (len v) 0)) (set n (+ n 1))) (free v)))";
   rejects_check "loop takes no label"
     "(defn f [] () (loop :o [i 0] (recur i)))" ~needle:"loop takes no label";
   rejects_check "a loop binding is a plain name"