diff --git a/FIX.org b/FIX.org index e9a6da5..19fb1eb 100644 --- a/FIX.org +++ b/FIX.org @@ -2711,13 +2711,56 @@ symptoms, and the second is the serious one: stored into. An uninitialised stack read, in a program the compiler accepted, on both backends. -Fixed with ~trial~, which snapshots ~scope~, ~slots~, ~slot_tys~, -~slot_names~, ~defers~ and ~defer_slot~ and puts all six back when the trial -refuses. ~scoped~ itself is untouched — it is shared by every scope-opening -form in the file and this is not its problem to solve. ~trial~ also narrows -the catch to ~Loc.Error~: a timeout or a stack overflow is not a refusal to -reconsider, and continuing past one would turn a resource failure into a wrong -answer. Both symptoms pinned. +Fixed with ~trial~, which snapshots the context and puts it back when the +trial refuses. ~scoped~ itself is untouched — it is shared by every +scope-opening form in the file and this is not its problem to solve. ~trial~ +also narrows the catch to ~Loc.Error~: a timeout or a stack overflow is not a +refusal to reconsider, and continuing past one would turn a resource failure +into a wrong answer. + +*The first version of that fix restored six chosen fields, and the choice was +wrong.* Review round three found three more, and the worst of them inverts the +symptom: where a leaked binding produces a false *accept*, a leaked window +produces a false *refusal*. + +- ~in_frames~. ~check_frames~ sets it, threads the expectation into the body's + last form, and clears it on the way out. A trial abandoned inside that + window leaves the flag stuck, so + + : (println (+ i32-x (handler-bind [] i64-y))) + : (return 0) + + — which compiled before this lane and compiles again now — was refused with + "return is not allowed inside handler-bind yet", pointing at a line with no + ~handler-bind~ within sight of it. A valid program refused for a reason that + is not in the program. +- ~loops~, the same window via ~loop~: a leaked ~Lrecur~ made an invalid + ~break~ answer "the nearest loop is a (loop ...), which answers with the + value of its body" instead of "break is only allowed inside a loop". No bad + accept, a thoroughly misleading refusal. +- ~defer_block~, message text only, and leaked with ~loops~. + +*So the subset was replaced by the whole record.* ~trial~ now restores every +mutable field of ~ctx~ — the three above, the six from round two, and +~defer_ok~, ~tail~ and ~outer_what~, which would self-heal on their own and +are restored anyway, because "this one cannot currently leak" is precisely the +reasoning that produced two rounds of leaks. The destructuring is closed and +carries ~[@warning "+9"]~, so adding a field to ~ctx~ stops ~trial~ compiling +until somebody decides about it. *Verified that the guard guards*: removing +one field from the pattern by hand fails the build, naming the field. + +One thing is deliberately not restored, and it is on ~env~ rather than ~ctx~: +an abandoned trial that lifted a function out of an ~fn~ literal leaves it in +~env.lifted~. That is dead and harmless — the names are ~fn//N~ handed +out by count, so the live pass gets fresh ones and nothing refers to the +orphan — and it rides into the module as a function nobody calls. Left because +~env~ is the program's table rather than this form's, and rewinding it would +mean deciding what else on ~env~ a trial may have touched; the one piece of +~env~ state that genuinely needs rewinding, the generic instantiation cache, +already rewinds itself in ~instantiate~. + +All five symptoms pinned — the two accepts, the shadow, the unknown name, and +the loop diagnostic. *2. The trial reconsidered literals.* Written up under the join rule above. The short version: ~(+ u8-thing 300)~ compiled, at i32, answering 555. The diff --git a/lib/check.ml b/lib/check.ml index 503e1d2..a1b721a 100644 --- a/lib/check.ml +++ b/lib/check.ml @@ -7560,24 +7560,59 @@ and numeric_want want = Rule 2 above is not a description of the old language kept for continuity; it is what the author decided, and the kind is how the trial obeys it. *) and trial ctx f = - (* Everything a check writes into the context that is not the expression it - answers. [defers] and [defer_slot] are on the list even though a [defer] - inside an operand is already refused — [defer_ok] is cleared on entry to - [check] — because "already impossible elsewhere" is the kind of reason - that stops being true, and putting a field back costs nothing. + (* Everything a check writes into the context, put back if the check is + abandoned — and it is *everything* on purpose, not a chosen subset. + + Picking the fields that looked like they mattered was tried twice and was + wrong twice. [scope] and the slot fields were the first round, found as an + uninitialised read. The second round was worse, because the symptom was + the other way up: a form that opens a window and closes it on the way out + — [check_frames] setting [in_frames], [loop] pushing onto [loops] — leaves + that window *open* when a trial inside it is abandoned, and then refuses + a perfectly good program. + + (println (+ i32-x (handler-bind [] i64-y))) + (return 0) + + compiled before this lane and was refused after it, with "return is not + allowed inside handler-bind yet" pointing at a line with no handler-bind + anywhere near it. A false refusal is not a lesser bug than a false accept; + it is just quieter about being one. + + So the rule here is not judgement, it is the whole record. Three fields + would have self-healed anyway — [defer_ok] and [tail] are read and cleared + on entry to [check], [outer_what] is never written after the context is + built — and they are restored regardless, because "this one cannot + currently leak" is exactly the reasoning that produced two rounds of + leaks. The destructuring below is closed and warning 9 is turned on for + it, so a new field on [ctx] stops this function compiling until somebody + decides about it, rather than joining the list of things nobody noticed. + + What is *not* restored, once, deliberately: [env.lifted] keeps whatever + function an abandoned trial lifted out of an [fn] literal. It is dead — + the names are [fn//N] handed out by count, so the live pass gets + fresh ones and nothing refers to the orphan — and it rides along into the + module as a function nobody calls. Left alone because [env] is the + program's table and not this form's, and rewinding it would mean deciding + what else on [env] a trial may have touched; the generic instantiation + cache already rolls itself back, in [instantiate]. Only [Loc.Error] is caught. A timeout or a stack overflow is not a refusal to reconsider, and silently continuing past one would turn a resource failure into a wrong answer. *) - let scope = ctx.scope and slots = ctx.slots in - let slot_tys = ctx.slot_tys and slot_names = ctx.slot_names in - let defers = ctx.defers and defer_slot = ctx.defer_slot in + let[@warning "+9"] { env = _; ret = _; slots; slot_tys; slot_names; scope; + defers; defer_slot; defer_ok; defer_block; outer = _; + outer_what; in_frames; loops; tail; in_defer; + owner = _ } = ctx in match f () with | r -> Ok r | exception Loc.Error d -> - ctx.scope <- scope; ctx.slots <- slots; - ctx.slot_tys <- slot_tys; ctx.slot_names <- slot_names; + ctx.slots <- slots; ctx.slot_tys <- slot_tys; + ctx.slot_names <- slot_names; ctx.scope <- scope; ctx.defers <- defers; ctx.defer_slot <- defer_slot; + ctx.defer_ok <- defer_ok; ctx.defer_block <- defer_block; + ctx.outer_what <- outer_what; ctx.in_frames <- in_frames; + ctx.loops <- loops; ctx.tail <- tail; ctx.in_defer <- in_defer; Error d (* Whether the trial's refusal is one worth reconsidering. A literal that did diff --git a/test/test_flan.ml b/test/test_flan.ml index c7545cc..06b0698 100644 --- a/test/test_flan.ml +++ b/test/test_flan.ml @@ -1031,6 +1031,23 @@ let () = restores around each trial. Both symptoms of not doing it: a binding that outlives the pass that made it, and the same binding *shadowing* a live one, which is an uninitialised read in a program the compiler accepted. *) + (* The other half, and the one that bites harder: a form that opens a window + and closes it on the way out leaves it *open* when a trial inside it is + abandoned, and then refuses a program that is fine. Both windows — the + frames [handler-bind] establishes, and the loop [loop] pushes — with the + refusal each would wrongly produce written as the second half of the + test, so a regression shows up as the message coming back rather than as + a silent accept. *) + accepts "an abandoned trial inside handler-bind does not leave its frames up" + "(defvar n i32) (defvar w i64) \ + (defn f [] i32 (println (+ n (handler-bind [] w))) (return 0))"; + accepts "nor does one inside a loop leave the loop up" + "(defvar n i32) (defvar w i64) \ + (defn f [] i32 (println (+ n (loop [i 0] w))) (defer (println 1)) 0)"; + rejects_check "and a break outside every loop still says so plainly" + "(defvar n i32) (defvar w i64) \ + (defn f [] i32 (println (+ n (loop [i 0] w))) (break) 0)" + ~needle:"break is only allowed inside a loop"; rejects_check "an abandoned trial leaves no binding behind" "(defvar n i32) (defvar w i64) \ (defn f [] i32 (println (+ n (let [q w] q))) (println q) 0)"