A trial puts the whole context back, and the compiler now insists on it
This commit is contained in:
parent
114ea391aa
commit
0d34831199
57
FIX.org
57
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
|
stored into. An uninitialised stack read, in a program the compiler
|
||||||
accepted, on both backends.
|
accepted, on both backends.
|
||||||
|
|
||||||
Fixed with ~trial~, which snapshots ~scope~, ~slots~, ~slot_tys~,
|
Fixed with ~trial~, which snapshots the context and puts it back when the
|
||||||
~slot_names~, ~defers~ and ~defer_slot~ and puts all six back when the trial
|
trial refuses. ~scoped~ itself is untouched — it is shared by every
|
||||||
refuses. ~scoped~ itself is untouched — it is shared by every scope-opening
|
scope-opening form in the file and this is not its problem to solve. ~trial~
|
||||||
form in the file and this is not its problem to solve. ~trial~ also narrows
|
also narrows the catch to ~Loc.Error~: a timeout or a stack overflow is not a
|
||||||
the catch to ~Loc.Error~: a timeout or a stack overflow is not a refusal to
|
refusal to reconsider, and continuing past one would turn a resource failure
|
||||||
reconsider, and continuing past one would turn a resource failure into a wrong
|
into a wrong answer.
|
||||||
answer. Both symptoms pinned.
|
|
||||||
|
*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/<owner>/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.
|
*2. The trial reconsidered literals.* Written up under the join rule above.
|
||||||
The short version: ~(+ u8-thing 300)~ compiled, at i32, answering 555. The
|
The short version: ~(+ u8-thing 300)~ compiled, at i32, answering 555. The
|
||||||
|
|||||||
55
lib/check.ml
55
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;
|
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. *)
|
it is what the author decided, and the kind is how the trial obeys it. *)
|
||||||
and trial ctx f =
|
and trial ctx f =
|
||||||
(* Everything a check writes into the context that is not the expression it
|
(* Everything a check writes into the context, put back if the check is
|
||||||
answers. [defers] and [defer_slot] are on the list even though a [defer]
|
abandoned — and it is *everything* on purpose, not a chosen subset.
|
||||||
inside an operand is already refused — [defer_ok] is cleared on entry to
|
|
||||||
[check] — because "already impossible elsewhere" is the kind of reason
|
Picking the fields that looked like they mattered was tried twice and was
|
||||||
that stops being true, and putting a field back costs nothing.
|
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/<owner>/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
|
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
|
refusal to reconsider, and silently continuing past one would turn a
|
||||||
resource failure into a wrong answer. *)
|
resource failure into a wrong answer. *)
|
||||||
let scope = ctx.scope and slots = ctx.slots in
|
let[@warning "+9"] { env = _; ret = _; slots; slot_tys; slot_names; scope;
|
||||||
let slot_tys = ctx.slot_tys and slot_names = ctx.slot_names in
|
defers; defer_slot; defer_ok; defer_block; outer = _;
|
||||||
let defers = ctx.defers and defer_slot = ctx.defer_slot in
|
outer_what; in_frames; loops; tail; in_defer;
|
||||||
|
owner = _ } = ctx in
|
||||||
match f () with
|
match f () with
|
||||||
| r -> Ok r
|
| r -> Ok r
|
||||||
| exception Loc.Error d ->
|
| exception Loc.Error d ->
|
||||||
ctx.scope <- scope; ctx.slots <- slots;
|
ctx.slots <- slots; ctx.slot_tys <- slot_tys;
|
||||||
ctx.slot_tys <- slot_tys; ctx.slot_names <- slot_names;
|
ctx.slot_names <- slot_names; ctx.scope <- scope;
|
||||||
ctx.defers <- defers; ctx.defer_slot <- defer_slot;
|
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
|
Error d
|
||||||
|
|
||||||
(* Whether the trial's refusal is one worth reconsidering. A literal that did
|
(* Whether the trial's refusal is one worth reconsidering. A literal that did
|
||||||
|
|||||||
@ -1031,6 +1031,23 @@ let () =
|
|||||||
restores around each trial. Both symptoms of not doing it: a binding that
|
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
|
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. *)
|
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"
|
rejects_check "an abandoned trial leaves no binding behind"
|
||||||
"(defvar n i32) (defvar w i64) \
|
"(defvar n i32) (defvar w i64) \
|
||||||
(defn f [] i32 (println (+ n (let [q w] q))) (println q) 0)"
|
(defn f [] i32 (println (+ n (let [q w] q))) (println q) 0)"
|
||||||
|
|||||||
Loading…
x
Reference in New Issue
Block a user