diff --git a/lib/check.ml b/lib/check.ml index 6d6c059..4635e68 100644 --- a/lib/check.ml +++ b/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] diff --git a/test/test_flan.ml b/test/test_flan.ml index 1d82d55..6dd8849 100644 --- a/test/test_flan.ml +++ b/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"