A second fingerprint for the globals a body names, and the header caches at both levels
This commit is contained in:
commit
f3f973d775
100
BUILT.md
100
BUILT.md
@ -290,6 +290,71 @@ importing at build time**, on the branch where the dev loop is the priority. It
|
||||
is the strongest case for the third option — generate from the header, commit
|
||||
the result, regenerate when the library moves — and that decision is open.
|
||||
|
||||
#### Where that 15.5ms actually is — and it is not the header
|
||||
|
||||
Written above as though a redefinition were re-reading the header on every
|
||||
reload. It is not, and the number was never taken apart. Taken apart now, with a
|
||||
timer around each stage of the same `flan reload` (raylib 5.5, sand.flan, one
|
||||
`defn` in the forms file, warm caches):
|
||||
|
||||
| | no header | header imported | delta |
|
||||
|---|---|---|---|
|
||||
| `Session.create` | 7.0ms | 21.5ms | +14.5 |
|
||||
| `Session.eval` | 4.8ms | 8.4ms | +3.6 |
|
||||
| `llc` + `ld` | 21ms | 21ms | 0 |
|
||||
|
||||
And inside that `create`, the header's own share: reading the cached dump
|
||||
**0.33ms**, turning it into declarations **3.3ms**, checking the package's
|
||||
layouts and its hand-written signatures against it **0.55ms**. Roughly 4ms of
|
||||
the 14.5, once. The other ~10ms is `Load` and `Check` doing their ordinary work
|
||||
over 256 more declarations, and so is the +3.6ms on `eval`.
|
||||
|
||||
**So a `C-c C-c` in a daemon pays no header cost at all, and never did.**
|
||||
`Session.eval` puts the evaluated forms through `Load.program`, and a form list
|
||||
with no `(import …)` in it reads no package and therefore no header. The import
|
||||
runs when the session is created, and again on a `C-c C-k` whose buffer carries
|
||||
the package's own `import` line. `flan reload` is a fresh process per
|
||||
redefinition, which is why its number carries a session's startup cost — it is
|
||||
the CLI's shape, not the dev loop's.
|
||||
|
||||
What a redefinition does pay for an imported package is the +3.6ms of checking
|
||||
and emitting against a program with 256 more declarations in it. That is in
|
||||
`Check` and in `Emit.redefinition` declaring every sibling; it is real, it is
|
||||
the number to attack next, and no cache touches it.
|
||||
|
||||
#### Two caches, and what a header change mid-session means
|
||||
|
||||
Both levels exist now. **On disk**, keyed on the header's realpath, size, mtime,
|
||||
the full flag list and a format version — the object cache's own convention, and
|
||||
it now lives in the object cache directory rather than a second one beside it.
|
||||
Cold that read is 50ms of clang and parse; served from the file it is 0.33ms.
|
||||
|
||||
**In the session**, two tables in `Cimport`: the extracted dump by header, and
|
||||
the generated declarations by header *and* by what the package already declares
|
||||
(names taken, structs and enums known, C symbols bound by hand), so a package an
|
||||
evaluation has added a decl to is worked out again rather than served a stale
|
||||
answer. A repeat import in one process goes from 3.65ms to nothing — measured on
|
||||
a whole-buffer evaluation, which imports twice.
|
||||
|
||||
**A header edited mid-session does not take effect until the session is
|
||||
restarted**, and that is deliberate rather than incidental: the in-memory key is
|
||||
the header's path and flags, with no mtime and no `stat`. It is the rule a
|
||||
changed `.c` file already follows — the daemon compiled the package's C at
|
||||
startup and a redefinition does not recompile it — and the rule the running
|
||||
program follows, since its struct layouts are the ones it was built with. Taking
|
||||
a new header mid-session would mean type-checking new signatures against a
|
||||
process still running the old layouts, which is the silent disagreement the
|
||||
whole header check exists to catch. The disk cache does key on mtime, so the
|
||||
next session reads the new header rather than the old dump.
|
||||
|
||||
One attribution to not repeat: the disk cache is **not** what the dev build's
|
||||
+333ms cold is about. Measured on this machine, a cold dev build of sand.flan is
|
||||
1.37s without the header and 1.83s with it and both caches cold; clear only the
|
||||
header cache and the same build is 0.92s against 0.83s. So the header read is
|
||||
~60–90ms of a fresh session and the rest of the cold delta is the object cache
|
||||
compiling a shim with 428 wrappers in it, which is the object cache's business
|
||||
and already warm after one build.
|
||||
|
||||
### What a headless FFI test can and cannot pin
|
||||
|
||||
Worth knowing before writing another one, because two plausible tests in a row turned out to check nothing.
|
||||
@ -1411,7 +1476,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.
|
||||
@ -1473,14 +1539,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`
|
||||
|
||||
|
||||
21
NEXT.md
21
NEXT.md
@ -62,6 +62,15 @@ a wrapper nothing reachable calls, confirmed on the wasm32 case it exists for wi
|
||||
Redefinition 31.0ms → 46.5ms. Dev build +333ms cold, once per session, since `Build.shared` compiles no C. Reading the
|
||||
header is cached (64ms → 17ms), keyed like the object cache; the cache was built against a measurement, not a guess.
|
||||
|
||||
**Re-measured, and the 15.5ms was misattributed** — see BUILT.md, "Where that 15.5ms actually is". A `C-c C-c` reads
|
||||
no header: `Session.eval` puts the forms through `Load`, and forms with no `(import …)` in them touch no package. The
|
||||
15.5ms is `flan reload`'s, and `flan reload` is a fresh process — ~14.5ms of it is session startup and ~4ms of *that*
|
||||
is the header. What a redefinition really pays for an imported package is **+3.6ms per eval** in `Check` and in
|
||||
`Emit.redefinition` declaring 256 more siblings, and no cache touches that; it is the number to attack next. The
|
||||
header is now cached in the session as well as on disk, so a repeat import (a `C-c C-k` of a buffer carrying its own
|
||||
`import` line) costs nothing, and a header edited mid-session is not picked up until the session restarts — the same
|
||||
rule a changed `.c` file follows.
|
||||
|
||||
**Opt-in on purpose.** `vendor/raylib/headers` is `?${FLAN_RAYLIB_H}`. "A build needs libraylib linkable and not
|
||||
raylib-devel installed" is a property chosen deliberately, and requiring a header would take it from everyone to give
|
||||
the check to whoever has one. Unset means off; set-and-wrong is an error naming the path.
|
||||
@ -84,8 +93,9 @@ Worth knowing before touching it:
|
||||
|
||||
Two things that are *not* done, and are 6a and 6b in DISCUSS.md: whether the header stays a build-time read or becomes
|
||||
a committed generator (`flan import-c` already prints the lines, so it costs nothing more to switch), and whether the
|
||||
172 hand-written lines migrate. Neither is blocked on correctness. The 15.5ms on redefinition is the argument for the
|
||||
first; needing the header at every build — vendoring raylib.h or requiring raylib-devel — is the argument on the
|
||||
172 hand-written lines migrate. Neither is blocked on correctness. The argument for the first is weaker than it
|
||||
looked — committing the generated lines would save ~4ms of session startup and none of the +3.6ms per redefinition,
|
||||
since that cost is the 256 declarations existing at all and not where they came from; needing the header at every build — vendoring raylib.h or requiring raylib-devel — is the argument on the
|
||||
second.
|
||||
|
||||
One smaller thing found and worth not re-deriving: an enum parameter imports as `i32`, because the header says
|
||||
@ -395,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
|
||||
|
||||
@ -678,7 +678,7 @@ let dump_of_clang ~loc ~header ~flags =
|
||||
in
|
||||
read_dump ~header json
|
||||
|
||||
(* ── The cache ─────────────────────────────────────────────────────── *)
|
||||
(* ── The caches, two of them ───────────────────────────────────────── *)
|
||||
|
||||
(* Measured, not assumed: reading raylib.h costs 64ms — 30ms for clang to write
|
||||
1.8 MB of JSON and the rest to parse it and map it — against an 8ms check
|
||||
@ -697,16 +697,26 @@ let dump_of_clang ~loc ~header ~flags =
|
||||
compiler whose [dump] type has changed must not read one written by the old
|
||||
one. [Marshal] does not check that for you and a mismatch is a segfault
|
||||
rather than an exception, so the discipline is: **change the [dump] type,
|
||||
bump [cache_format] in the same commit.** Nothing enforces it. *)
|
||||
bump [cache_format] in the same commit.** Nothing enforces it.
|
||||
|
||||
It lives under the object cache directory, beside the [.o] files, because it
|
||||
is the same kind of thing: derived from an input the compiler did not write,
|
||||
stable across builds, and safe to delete. One directory to clear rather than
|
||||
two. *)
|
||||
|
||||
let cache_format = 1
|
||||
|
||||
(* 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-cimport" in
|
||||
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 ~loc ~header ~flags =
|
||||
let dump_of_disk ~loc ~header ~flags =
|
||||
let st = try Some (Unix.stat header) with Unix.Unix_error _ -> None in
|
||||
match st with
|
||||
| None -> dump_of_clang ~loc ~header ~flags
|
||||
@ -753,12 +763,75 @@ let dump_of ~loc ~header ~flags =
|
||||
with Sys_error _ -> ());
|
||||
d)
|
||||
|
||||
(* And in front of that file, the session's own copy — which is the level that
|
||||
matters for the dev loop, because the daemon is a process that lives for as
|
||||
long as the editor does and re-reads the file once per evaluation that
|
||||
imports the package again. Reading the cached dump is 0.33ms and extracting
|
||||
the declarations from it is another 3.3ms, so this is small; it is here
|
||||
because *nothing* is the right amount for a long-lived process to pay twice
|
||||
for an answer it already has.
|
||||
|
||||
**Keyed on the header's path and the flags, and deliberately not on its
|
||||
mtime.** That is the whole of the mid-session question: a header edited
|
||||
while a session is running is not re-read, and the session keeps the
|
||||
signatures it started with until it is restarted. It is the same rule a
|
||||
changed [.c] file follows — the daemon compiled the package's C once, at
|
||||
startup, and a redefinition does not recompile it — and the same rule the
|
||||
running program itself follows, since its layouts are the ones it was built
|
||||
with. The alternative is worse in both directions: keying on mtime would put
|
||||
a [stat] on a path that is supposed to cost nothing, and it would let a
|
||||
header change take effect on the next [C-c C-c] in a *program that is still
|
||||
running with the old layouts*, which is precisely the silent disagreement
|
||||
the header check exists to prevent. A new session reads the new header, and
|
||||
the disk cache above keys on mtime so it does not serve it the old one.
|
||||
|
||||
Two tables rather than one, because the two answers have different inputs.
|
||||
The *dump* is the header's alone, so a second package importing the same
|
||||
header shares it. The *declarations* are the dump read against one package —
|
||||
which names it already has taken, which structs and enums it knows, which C
|
||||
symbols it binds by hand — so they are keyed on those too, and a package
|
||||
whose decls an evaluation has added to gets its declarations worked out
|
||||
again rather than served an answer about the decls it used to have. *)
|
||||
|
||||
let dumps : (string, dump) Hashtbl.t = Hashtbl.create 4
|
||||
let imports : (string, imported * dump * env) Hashtbl.t = Hashtbl.create 4
|
||||
|
||||
let header_key ~header ~flags =
|
||||
String.concat "\000"
|
||||
((try Unix.realpath header with Unix.Unix_error _ -> header) :: flags)
|
||||
|
||||
let dump_of ~loc ~header ~flags =
|
||||
let k = header_key ~header ~flags in
|
||||
match Hashtbl.find_opt dumps k with
|
||||
| Some d -> d
|
||||
| None ->
|
||||
let d = dump_of_disk ~loc ~header ~flags in
|
||||
Hashtbl.replace dumps k d;
|
||||
d
|
||||
|
||||
let env_of ~known_structs ~known_enums d = { known_structs; known_enums; d }
|
||||
|
||||
let header ~loc ~header:h ~flags ~known_structs ~known_enums ~taken ~bound_syms =
|
||||
let d = dump_of ~loc ~header:h ~flags in
|
||||
let env = env_of ~known_structs ~known_enums d in
|
||||
(of_dump ~env ~taken ~bound_syms d, d, env)
|
||||
let k =
|
||||
(* Sorted, because neither the taken table nor the declaration order is a
|
||||
fact about the package — two loads of the same file that enumerate them
|
||||
differently are the same question and must not miss each other. *)
|
||||
let sorted xs = List.sort compare xs in
|
||||
String.concat "\000"
|
||||
(header_key ~header:h ~flags
|
||||
:: "\001" :: sorted known_structs
|
||||
@ ("\001" :: sorted known_enums)
|
||||
@ ("\001" :: sorted (Hashtbl.fold (fun n () acc -> n :: acc) taken []))
|
||||
@ ("\001" :: sorted bound_syms))
|
||||
in
|
||||
match Hashtbl.find_opt imports k with
|
||||
| Some r -> r
|
||||
| None ->
|
||||
let d = dump_of ~loc ~header:h ~flags in
|
||||
let env = env_of ~known_structs ~known_enums d in
|
||||
let r = (of_dump ~env ~taken ~bound_syms d, d, env) in
|
||||
Hashtbl.replace imports k r;
|
||||
r
|
||||
|
||||
(* ── Printing a declaration back as source ─────────────────────────── *)
|
||||
|
||||
|
||||
68
lib/dev.ml
68
lib/dev.ml
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
|
||||
34
lib/reach.ml
34
lib/reach.ml
@ -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. *)
|
||||
|
||||
@ -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
|
||||
|
||||
@ -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
|
||||
|
||||
11
vendor/agent/flan_agent.c
vendored
11
vendor/agent/flan_agent.c
vendored
@ -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);
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user