The globals a frame names, checked the way its slots already were

The globals section attributed a frame by its slot fingerprint, which is the
wrong cut for it: a redefined body can name entirely different globals while
binding identical locals, so the check saw no change and the new body's
reference set went into the union under the old body's frame, with the frame
numbers beside an entry saying so.

So a second fingerprint. Reach.ref_fingerprint hashes the set of globals a body
names — sorted and deduplicated, because a reference set is not ordered, where
slot indices make the slot fingerprint order-sensitive on purpose — and it
travels the path the first one already cut: %fninfo, flan_dev_frame_refsig, the
agent's snapshot, the backtrace line, Dev.globals_op. Different means the frame
is skipped by name with its reason, and the rest of the stack still contributes.

Two numbers rather than one, because they are two facts. A frame whose slots
match and whose globals do not has locals that are perfectly readable and
attribution that is not, and a combined hash would make locals refuse a frame
with nothing wrong with it. locals still checks the slot fingerprint alone.

It lives in reach.ml because expr_refs is already the walk that answers what a
body refers to, and is the walk the union itself is built from. One consequence:
emit now reaches reach, which closes a cycle through Load if cimport calls
Build.cachedir, so the header cache spells the object cache directory itself.

test_dev.ml drives the exact case — a body that binds identical locals and names
untouched where the stopped frame names pressure. With the check disabled it
fails twice: the missing refusal, and untouched appearing under frame 0.
This commit is contained in:
Joseph Ferano 2026-09-12 16:58:34 +07:00
parent df1a43d3ac
commit 36c3e5a56d
9 changed files with 210 additions and 39 deletions

View File

@ -1455,7 +1455,8 @@ stays in front of it because its message is the more specific one.
Computed in `emit.ml` and read from there by `dev.ml`, so there is one definition of it and the two ends cannot drift.
It stays **off the wire**: `(:op "backtrace")` still answers four fields per frame, because a hash is not something an
editor can act on and the refusal says the fact in words instead. The bound is worth stating: it is a 30-bit hash, so a
editor can act on and the refusal says the fact in words instead. The same is true of the globals fingerprint that
now travels beside it. The bound is worth stating: it is a 30-bit hash, so a
collision is possible in principle, and it would reproduce exactly the silent wrong answer this catches — but only
between two *differing* bodies of a function whose qualified name has already matched, since `find_fn` is what gates the
comparison at all.
@ -1517,14 +1518,32 @@ session; a lifted handler clause has none of its own; a frame whose body was red
body whose reference set is a claim about different code. All three go into `:skipped` with the reason, because "the
union is incomplete and here is why" and "these are all of them" are different answers and the second one is the lie.
**And the hole in that, which is narrow and is not closed.** `Emit.slot_fingerprint` hashes a body's *slots*. For
**The hole this had, and the second fingerprint that closes it.** `Emit.slot_fingerprint` hashes a body's *slots*. For
`locals` that is exactly the right cut: identical slots means the names still describe the storage, so the answer is
still true. Here it is not, because a body can change which globals it names without touching a single slot — and then
this section shows the *new* body's reference set attributed to the *old* frame. The values stay correct; they are read
from the program's storage by name. What can be wrong is one frame's membership in the union and the frame numbers
beside an entry. Closing it needs a second fingerprint over the reference set itself, in `%fninfo` and in the agent
that reads it. It is written down here and in `dev.ml` rather than papered over with a check that does not check it,
and `test_dev.ml` drives the redefinition case that *is* caught rather than asserting the one that is not.
still true. Here it was not, because a body can change which globals it names without touching a single slot — and then
this section showed the *new* body's reference set attributed to the *old* frame. The values were never at risk; they
are read from the program's storage by name. What was, is one frame's membership in the union and the frame numbers
beside an entry.
So `%fninfo` carries a second number beside the slot fingerprint: `Reach.ref_fingerprint`, over the **set** of globals
the body names — sorted and deduplicated, because a reference set is not ordered and a body that mentions the same two
globals the other way round is the same body, where slot indices make the slot fingerprint order-sensitive on purpose.
It travels the same path the first one does: `flan_dev_frame_refsig`, the agent's snapshot, the backtrace line, and
`Dev.globals_op` recomputing it from the body it holds. Different means that frame is in `:skipped` with its own
reason — *this frame's body names different globals than the one this session holds* — and the rest of the stack still
contributes.
**Two numbers and not one combined**, which is the whole reason this is a second fingerprint rather than a wider first
one. They are different facts: a frame whose slots match and whose globals do not has locals that are perfectly
readable and attribution that is not, and one hash over both would make `locals` refuse a frame with nothing wrong
with it. So `locals` still checks the slot fingerprint alone.
It lives in `reach.ml` rather than `emit.ml` because `Reach.expr_refs` is already the walk that answers "what does this
body refer to" and is the same walk the union above is built from — the two ends cannot disagree about what counts as a
reference. Which names are globals is the caller's to say: the emitter knows the program's globals, and so does the
session. `test_dev.ml` now drives the exact case — a redefinition that binds identical locals and names `untouched`
where the stopped frame's body names `pressure` — and with the check disabled it fails twice: once on the missing
refusal, once on `untouched` appearing in the union under frame 0.
### Conditions — step 2: `restart-case` and `invoke-restart`

View File

@ -405,8 +405,11 @@ reason there is no collector.
**Globals in the break buffer — built.** One section under the stack, holding the union of the globals every frame on
the current stack references, each entry annotated with the frames that touch it and ordered by the innermost one. It
is `(:op "globals")` in `dev.ml` and `flan-cnr--insert-globals` in the break buffer. See BUILT.md, "Globals of a
stopped stack" — including the one hole left open, which is that the redefinition check is a fingerprint over a body's
*slots* and so does not catch a new body that names different globals while binding the same locals.
stopped stack". ~~The one hole left open — the redefinition check is a fingerprint over a body's *slots*, so a new body
that names different globals while binding the same locals is not caught.~~ **Closed**: `Reach.ref_fingerprint` is a
second fingerprint over the set of globals a body names, carried beside the slot one in `%fninfo` and checked the same
way, and such a frame is now refused by name. Kept separate from the slot fingerprint deliberately, so `locals` still
reads a frame whose locals are fine and whose global attribution is not.
**The break buffer opens by itself when the program stops.** Today a condition stops the program and the buffer appears
only when `C-c C-b` is typed. `flan-dev--absorb` already inspects every reply for `:stopped` and a poll covers the case

View File

@ -706,7 +706,15 @@ let dump_of_clang ~loc ~header ~flags =
let cache_format = 1
let cachedir () = Build.cachedir ()
(* The same directory [Build.cachedir] makes, spelled here rather than called:
[Load] is upstream of this file and downstream of [Reach], so reaching
[Build] from here closes a cycle. Two lines that have to agree, and the
consequence of their disagreeing is a second cache directory rather than a
wrong answer. *)
let cachedir () =
let d = Filename.concat (Filename.get_temp_dir_name ()) "flan-objcache" in
(try Unix.mkdir d 0o700 with Unix.Unix_error (Unix.EEXIST, _, _) -> ());
d
let dump_of_disk ~loc ~header ~flags =
let st = try Some (Unix.stat header) with Unix.Unix_error _ -> None in

View File

@ -235,13 +235,17 @@ let restarts t =
framing [restarts] uses, terminated by a lone dot, because it comes back
over the same one-line-out socket.
Each line is [I ± NSLOTS SIG LOC NAME]. [SIG] is the slot fingerprint of
the body this frame was compiled from [Emit.slot_fingerprint] over the
Each line is [I ± NSLOTS SIG RSIG LOC NAME]. [SIG] is the slot fingerprint
of the body this frame was compiled from [Emit.slot_fingerprint] over the
name and the type of every slot and it is how [locals] tells a frame whose
body has been redefined underneath it from one that still matches. It stays
off the wire: a hash is not something a client can act on, and the refusal
it produces says the fact in words instead. It sits before [LOC] because
[NAME] is the only field that can contain a space and so has to be last.
body has been redefined underneath it from one that still matches. [RSIG] is
[Reach.ref_fingerprint] over the globals that body names, which is the same
question asked about a different part of the body: the slots can be
identical while the globals are not, and then it is the globals section that
must not trust the frame while [locals] still can. Both stay off the wire: a
hash is not something a client can act on, and the refusals they produce say
the fact in words instead. They sit before [LOC] because [NAME] is the only
field that can contain a space and so has to be last.
The flag says whether the frame belongs
to the program or to the C-x C-e thunk the break happens to be inside: a
@ -272,14 +276,14 @@ let backtrace t =
end
else
match String.split_on_char ' ' line with
| idx :: flag :: nslots :: sig_ :: loc :: rest when rest <> [] ->
| idx :: flag :: nslots :: sig_ :: rsig :: loc :: rest when rest <> [] ->
(match
int_of_string_opt idx, int_of_string_opt nslots,
int_of_string_opt sig_
int_of_string_opt sig_, int_of_string_opt rsig
with
| Some _, Some k, Some g ->
| Some _, Some k, Some g, Some r ->
Some (String.concat " " rest, (if loc = "?" then "" else loc),
flag = "+", k, g)
flag = "+", k, g, r)
| _ -> None)
| _ -> None
in
@ -711,7 +715,7 @@ let backtrace_op t =
[ ":frames "
^ Wire.list
(List.map
(fun (name, loc, mine, nslots, _sig) ->
(fun (name, loc, mine, nslots, _sig, _rsig) ->
Wire.list
[ Wire.quote name; Wire.quote loc;
Wire.quote (if mine then "program" else "eval");
@ -771,7 +775,7 @@ let locals t ~frame =
error
(Printf.sprintf "there is no frame %d; the backtrace has %d" frame
(List.length frames))
| Some (name, _, mine, nslots, sig_) ->
| Some (name, _, mine, nslots, sig_, _rsig) ->
if not mine then
error
(name
@ -915,22 +919,24 @@ let locals t ~frame =
union it says it is. The *values* would still have been right; the
attribution is what goes wrong, and attribution is what this op is for.
**And the hole in that, stated rather than papered over.**
**And the frame check that [locals]'s is not.**
[Emit.slot_fingerprint] hashes a body's *slots* every slot's name with the
spelling of its type so it catches a redefinition that binds differently
and misses one that does not. For [locals] that is exactly the right cut:
if the slots are identical then the names still describe the storage and
the answer is still true. Here it is not, because a body can change which
globals it names without touching a single slot, and then this section
shows the *new* body's reference set attributed to the *old* frame.
would show the *new* body's reference set attributed to the *old* frame.
The values stay correct they come from the program's storage by name
and so does everything the other frames contribute. What can be wrong is
one frame's membership in the union and the frame numbers beside an entry.
Closing it means a second fingerprint over the reference set itself, which
is a change to [%fninfo] and to the agent that reads it; it is not done,
and the failure it leaves is narrow enough to name here rather than to
pretend away with a check that does not check it.
So a second fingerprint, [Reach.ref_fingerprint], over the set of globals
the body names, carried beside the slot one in [%fninfo] and checked here
the same way. Two numbers and not one, because they are two facts: a frame
whose slots match and whose globals do not has readable locals and
unusable attribution, and combining the hashes would make [locals] refuse
a frame nothing is wrong with. The values were never the exposure they
come from the program's storage by name and what was, one frame's
membership in the union and the frame numbers beside an entry, is now a
named refusal like every other.
Nothing is copied out of the program here either, and the mechanism is one
step simpler than [locals]: a global is reached by name rather than by
@ -959,7 +965,7 @@ let globals_op t =
let touched : (string, int list) Hashtbl.t = Hashtbl.create 32 in
let skipped = ref [] in
List.iteri
(fun i (name, _, mine, nslots, sig_) ->
(fun i (name, _, mine, nslots, sig_, rsig) ->
let skip why =
skipped := (Printf.sprintf "%d: %s" i name, why) :: !skipped
in
@ -984,6 +990,24 @@ let globals_op t =
skip
"this frame's body was redefined since it was entered, so \
what it refers to here is a claim about different code"
else if rsig <> Reach.ref_fingerprint ~is_global fn then
(* The check the slot fingerprint cannot make. A body that
binds the same locals and names different globals passes
every test above and is still the wrong body to read a
reference set out of: what would go into the union is
the *new* body's globals, attributed to the frame of the
old one, and the frame numbers beside an entry would say
a frame touches something it does not. The values are
not what breaks those are read from the program's own
storage by name so this refuses the frame's
attribution and nothing else. [locals] deliberately does
not make this check: the slots still describe the
storage, so that frame is still readable. *)
skip
"this frame's body names different globals than the one \
this session holds, so which globals it contributes to \
this union would be the new body's answer about the old \
body's frame"
else begin
(* Once per frame per name: a body that reads the grid in
four places touches it once as far as this is

View File

@ -610,8 +610,9 @@ let fninfo m (fn : Tast.fn) ~nslots =
m.nfi <- m.nfi + 1;
Buffer.add_string m.strs
(Printf.sprintf
"%s = private unnamed_addr constant %%fninfo { ptr %s, i64 %d, ptr %s, i64 %d, i32 %d, i32 %d }\n"
id nid nlen lid llen nslots (slot_fingerprint fn));
"%s = private unnamed_addr constant %%fninfo { ptr %s, i64 %d, ptr %s, i64 %d, i32 %d, i32 %d, i32 %d }\n"
id nid nlen lid llen nslots (slot_fingerprint fn)
(Reach.ref_fingerprint ~is_global:(Hashtbl.mem m.globals) fn));
id
(* ── Bounds checks ───────────────────────────────────────────────────── *)
@ -2002,7 +2003,7 @@ let header = {|; Generated by flan. The layout is C's: no object headers anywher
; it (runtime/flan_dev.c). Dev builds only: [emit_fn] pushes one on entry and
; every [ret] restores the head, the transfer path included. A release build
; emits neither, and the head below is then a symbol nothing in the .ll names.
%fninfo = type { ptr, i64, ptr, i64, i32, i32 }
%fninfo = type { ptr, i64, ptr, i64, i32, i32, i32 }
%flanframe = type { ptr, ptr, ptr }
@flan_frame_head = external global ptr

View File

@ -79,6 +79,40 @@ and place_refs f (p : Tast.place) =
| Tast.Pindex (t, idx) -> expr_refs f t; List.iter (expr_refs f) idx
| Tast.Pderef t -> expr_refs f t
(* ── What a body names, as one number ──────────────────────────────── *)
(* The globals half of what the two ends of a break loop compare about a frame,
and the companion to [Emit.slot_fingerprint] rather than a replacement for
it. The slot fingerprint is the right cut for [locals]: if the slots are
identical then the names still describe the storage, whatever else the body
changed. It is the wrong cut for the globals section, because a redefined
body can name entirely different globals while binding identical locals
and then the section shows the new body's reference set attributed to the
frame of the old one.
Two fingerprints and not one combined, because the two facts are separately
useful: a frame can have perfectly readable locals and untrustworthy global
attribution, and the user should be told which. One hash over both would
make [locals] refuse a frame nothing is wrong with.
**A set, sorted and deduplicated, not the order the walk found them in.**
Slot indices make the slot fingerprint order-sensitive on purpose; a
reference set is not ordered, and a body that mentions the same two globals
the other way round is the same body as far as this is concerned.
Computed from [expr_refs], which is the walk that already answers "what does
this body refer to" — the same one [Dev]'s globals section uses to build the
union, so the two cannot disagree about what counts as a reference. Which
names are globals is the caller's to say: the emitter knows the program's
globals, and so does the session. *)
let ref_fingerprint ~is_global (fn : Tast.fn) =
let seen = Hashtbl.create 16 in
let note n = if is_global n && not (Hashtbl.mem seen n) then Hashtbl.add seen n () in
List.iter (expr_refs note) fn.Tast.body;
List.iter (expr_refs note) fn.Tast.fdefers;
let names = List.sort compare (Hashtbl.fold (fun n () acc -> n :: acc) seen []) in
Hashtbl.hash (String.concat ";" names) land 0x3fffffff
(* Every name reachable from [main] and from the globals, which run before it.
A name that is neither a function nor an extern a global, a struct is
still recorded; it costs a hashtable entry and saves asking twice. *)

View File

@ -342,6 +342,12 @@ typedef struct {
difference means the frame is running a superseded body. A count alone
cannot see a rename, which is the case this exists for. */
int32_t slotsig;
/* And the globals half, from [Reach.ref_fingerprint]: a hash over the set of
globals the body names. Separate from [slotsig] on purpose a body can
name different globals while binding identical locals, so a frame's locals
can be trustworthy while its contribution to the globals section is not,
and one number over both would refuse a frame that reads perfectly. */
int32_t refsig;
} flan_fninfo;
typedef struct flan_frame {
@ -404,6 +410,14 @@ int32_t flan_dev_frame_slotsig(const void *frame) {
return (f == NULL || f->info == NULL) ? 0 : f->info->slotsig;
}
/* The fingerprint of the globals that body names. Zero for a frame with no
* description, the same "nothing to compare" the slot count and the slot
* fingerprint already mean. */
int32_t flan_dev_frame_refsig(const void *frame) {
const flan_frame *f = frame;
return (f == NULL || f->info == NULL) ? 0 : f->info->refsig;
}
/* Where slot [i] of this frame lives, or NULL — which means one of three
* things, all of which are "there is nothing to read here": this build records
* no slots, the index is not one of them, or the binding that fills it had not

View File

@ -1028,6 +1028,69 @@ let () =
frame on the stack does not. *)
if List.exists (fun (n, _, _, _) -> n = "untouched") got then
fail "a superseded frame contributed the *new* body's references"
end;
(* And the case the slot fingerprint cannot see, which is the one this
section needs its own fingerprint for. This body binds exactly the
locals the frame on the stack binds none, and the same
temporaries, because every expression in it has the same shape
and names [untouched] where the frame's body names [pressure]. The
slot check passes; only [Reach.ref_fingerprint] can tell that what
this session now holds refers to different program state.
Refused by name and for that reason, like everything else in the
break loop. What would happen without it is not an error message:
it is [untouched] appearing in the union marked as touched by frame
0, and [pressure] missing from it, both of which read as facts
about the stopped program and are not. *)
let r =
ask
"(:op \"eval\" :code \"(defn inner [] i64 (set untouched 12) (set (at grid 0) 7) (error (Boom {.why 3})) 0)\" :file \"/tmp/buf.flan\")"
in
if status r <> "ok" then
fail "installing a body with the same slots and other globals: %s"
(Option.value ~default:"" (Wire.string_field r "message"))
else begin
let r = ask "(:op \"globals\")" in
if status r <> "ok" then
fail "globals after a reference-set change: %s"
(Option.value ~default:(status r) (Wire.string_field r "message"));
let whys =
match Wire.field r "skipped" with
| Some { Form.v = Form.List l; _ } ->
List.filter_map
(fun (e : Form.t) ->
match e.Form.v with
| Form.List [ _; { Form.v = Form.Str w; _ } ] -> Some w
| _ -> None)
l
| _ -> []
in
let mentions hay needle =
let n = String.length needle in
let rec go i =
i + n <= String.length hay
&& (String.equal (String.sub hay i n) needle || go (i + 1))
in
go 0
in
if not
(List.exists
(fun w -> mentions w "names different globals")
whys)
then
fail
"a frame whose body now names different globals was attributed \
anyway (skipped: %s)"
(String.concat " | " whys);
let got = rows r in
(* The new body's globals must not have leaked in under the old
frame, and the frame that did not change must still contribute:
a refusal that swallowed the whole stack would satisfy the check
above and say nothing. *)
if List.exists (fun (n, _, _, _) -> n = "untouched") got then
fail "the new body's globals were attributed to the old frame";
if not (List.exists (fun (n, _, _, _) -> n = "label") got) then
fail "refusing one frame dropped an untouched frame's globals"
end
end;
(* Nothing handled the condition, so there is no restart to resume by

View File

@ -156,6 +156,7 @@ extern const char *flan_dev_frame_name(const void *frame, int64_t *len);
extern const char *flan_dev_frame_loc(const void *frame, int64_t *len);
extern int32_t flan_dev_frame_nslots(const void *frame);
extern int32_t flan_dev_frame_slotsig(const void *frame);
extern int32_t flan_dev_frame_refsig(const void *frame);
extern void *flan_dev_frame_slot(const void *frame, int32_t i);
extern const uint8_t *flan_restart_name(int32_t i, int64_t *len);
extern void *flan_restart_frame(int32_t i);
@ -262,6 +263,8 @@ typedef struct {
int32_t fslots[FRAME_MAX];
int32_t fsig[FRAME_MAX]; /* the slot fingerprint of the body
* this frame was compiled from */
int32_t frsig[FRAME_MAX]; /* and the fingerprint of the
* globals that body names */
int32_t fmine[FRAME_MAX]; /* 0 = the evaluation's, not the
* program's */
char ftext[FRAME_TEXT];
@ -370,6 +373,7 @@ static int snap_push(void) {
* module this description lives in can be unloaded once the daemon
* installs a replacement, and the comparison happens after that. */
s->fsig[s->fn] = flan_dev_frame_slotsig(fr);
s->frsig[s->fn] = flan_dev_frame_refsig(fr);
/* The outermost [frame_floor] frames are the program's; anything above
* them belongs to the evaluation this break is inside. */
s->fmine[s->fn] = (frame_floor < 0) || (i >= fn - frame_floor);
@ -674,11 +678,12 @@ static void serve(int fd) {
}
for (int32_t i = 0; i < s->fn; i++) {
char hdr[64];
/* The fingerprint goes before the location and the location before
/* Both fingerprints go before the location and the location before
* the name, because the name is the one field that can contain a
* space and so has to be last. */
int k = snprintf(hdr, sizeof hdr, "%d %c %d %d ", i,
s->fmine[i] ? '+' : '-', s->fslots[i], s->fsig[i]);
int k = snprintf(hdr, sizeof hdr, "%d %c %d %d %d ", i,
s->fmine[i] ? '+' : '-', s->fslots[i], s->fsig[i],
s->frsig[i]);
if (k > 0) send(fd, hdr, (size_t)k, MSG_NOSIGNAL);
if (s->fllen[i] > 0)
send(fd, s->ftext + s->floff[i], (size_t)s->fllen[i], MSG_NOSIGNAL);